src/HOL/MicroJava/BV/Opt.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 22271 51a80e238b29
child 27680 5a557a5afc48
permissions -rw-r--r--
Name.uu, Name.aT;
kleing@12516
     1
(*  Title:      HOL/MicroJava/BV/Opt.thy
kleing@10496
     2
    ID:         $Id$
kleing@10496
     3
    Author:     Tobias Nipkow
kleing@10496
     4
    Copyright   2000 TUM
kleing@10496
     5
kleing@10496
     6
More about options
kleing@10496
     7
*)
kleing@10496
     8
kleing@12911
     9
header {* \isaheader{More about Options} *}
kleing@10496
    10
haftmann@16417
    11
theory Opt imports Err begin
kleing@10496
    12
kleing@10496
    13
constdefs
kleing@13006
    14
 le :: "'a ord \<Rightarrow> 'a option ord"
kleing@13006
    15
"le r o1 o2 == case o2 of None \<Rightarrow> o1=None |
kleing@13006
    16
                              Some y \<Rightarrow> (case o1 of None \<Rightarrow> True
kleing@13006
    17
                                                  | Some x \<Rightarrow> x <=_r y)"
kleing@10496
    18
kleing@13006
    19
 opt :: "'a set \<Rightarrow> 'a option set"
kleing@10496
    20
"opt A == insert None {x . ? y:A. x = Some y}"
kleing@10496
    21
kleing@13006
    22
 sup :: "'a ebinop \<Rightarrow> 'a option ebinop"
kleing@10496
    23
"sup f o1 o2 ==  
kleing@13006
    24
 case o1 of None \<Rightarrow> OK o2 | Some x \<Rightarrow> (case o2 of None \<Rightarrow> OK o1
kleing@13006
    25
     | Some y \<Rightarrow> (case f x y of Err \<Rightarrow> Err | OK z \<Rightarrow> OK (Some z)))"
kleing@10496
    26
kleing@13006
    27
 esl :: "'a esl \<Rightarrow> 'a option esl"
kleing@10496
    28
"esl == %(A,r,f). (opt A, le r, sup f)"
kleing@10496
    29
kleing@10496
    30
lemma unfold_le_opt:
kleing@10496
    31
  "o1 <=_(le r) o2 = 
kleing@13006
    32
  (case o2 of None \<Rightarrow> o1=None | 
kleing@13006
    33
              Some y \<Rightarrow> (case o1 of None \<Rightarrow> True | Some x \<Rightarrow> x <=_r y))"
kleing@10496
    34
apply (unfold lesub_def le_def)
kleing@10496
    35
apply (rule refl)
kleing@10496
    36
done
kleing@10496
    37
kleing@10496
    38
lemma le_opt_refl:
kleing@13006
    39
  "order r \<Longrightarrow> o1 <=_(le r) o1"
kleing@10496
    40
by (simp add: unfold_le_opt split: option.split)
kleing@10496
    41
kleing@10496
    42
lemma le_opt_trans [rule_format]:
kleing@13006
    43
  "order r \<Longrightarrow> 
kleing@13006
    44
   o1 <=_(le r) o2 \<longrightarrow> o2 <=_(le r) o3 \<longrightarrow> o1 <=_(le r) o3"
kleing@10496
    45
apply (simp add: unfold_le_opt split: option.split)
kleing@10496
    46
apply (blast intro: order_trans)
kleing@10496
    47
done
kleing@10496
    48
kleing@10496
    49
lemma le_opt_antisym [rule_format]:
kleing@13006
    50
  "order r \<Longrightarrow> o1 <=_(le r) o2 \<longrightarrow> o2 <=_(le r) o1 \<longrightarrow> o1=o2"
kleing@10496
    51
apply (simp add: unfold_le_opt split: option.split)
kleing@10496
    52
apply (blast intro: order_antisym)
kleing@10496
    53
done
kleing@10496
    54
kleing@10496
    55
lemma order_le_opt [intro!,simp]:
kleing@13006
    56
  "order r \<Longrightarrow> order(le r)"
haftmann@22068
    57
apply (subst Semilat.order_def)
kleing@10496
    58
apply (blast intro: le_opt_refl le_opt_trans le_opt_antisym)
kleing@10496
    59
done 
kleing@10496
    60
kleing@10496
    61
lemma None_bot [iff]: 
kleing@10496
    62
  "None <=_(le r) ox"
kleing@10496
    63
apply (unfold lesub_def le_def)
kleing@10496
    64
apply (simp split: option.split)
kleing@10496
    65
done 
kleing@10496
    66
kleing@10496
    67
lemma Some_le [iff]:
kleing@10496
    68
  "(Some x <=_(le r) ox) = (? y. ox = Some y & x <=_r y)"
kleing@10496
    69
apply (unfold lesub_def le_def)
kleing@10496
    70
apply (simp split: option.split)
kleing@10496
    71
done 
kleing@10496
    72
kleing@10496
    73
lemma le_None [iff]:
kleing@10496
    74
  "(ox <=_(le r) None) = (ox = None)";
kleing@10496
    75
apply (unfold lesub_def le_def)
kleing@10496
    76
apply (simp split: option.split)
kleing@10496
    77
done 
kleing@10496
    78
kleing@10496
    79
kleing@10496
    80
lemma OK_None_bot [iff]:
kleing@10496
    81
  "OK None <=_(Err.le (le r)) x"
kleing@10496
    82
  by (simp add: lesub_def Err.le_def le_def split: option.split err.split)
kleing@10496
    83
kleing@10496
    84
lemma sup_None1 [iff]:
kleing@10496
    85
  "x +_(sup f) None = OK x"
kleing@10496
    86
  by (simp add: plussub_def sup_def split: option.split)
kleing@10496
    87
kleing@10496
    88
lemma sup_None2 [iff]:
kleing@10496
    89
  "None +_(sup f) x = OK x"
kleing@10496
    90
  by (simp add: plussub_def sup_def split: option.split)
kleing@10496
    91
kleing@10496
    92
kleing@10496
    93
lemma None_in_opt [iff]:
kleing@10496
    94
  "None : opt A"
kleing@10496
    95
by (simp add: opt_def)
kleing@10496
    96
kleing@10496
    97
lemma Some_in_opt [iff]:
kleing@10496
    98
  "(Some x : opt A) = (x:A)"
kleing@10496
    99
apply (unfold opt_def)
kleing@10496
   100
apply auto
kleing@10496
   101
done 
kleing@10496
   102
kleing@10496
   103
kleing@13062
   104
lemma semilat_opt [intro, simp]:
kleing@13006
   105
  "\<And>L. err_semilat L \<Longrightarrow> err_semilat (Opt.esl L)"
kleing@10496
   106
proof (unfold Opt.esl_def Err.sl_def, simp add: split_tupled_all)
kleing@10496
   107
  
kleing@10496
   108
  fix A r f
kleing@10496
   109
  assume s: "semilat (err A, Err.le r, lift2 f)"
kleing@10496
   110
 
kleing@10496
   111
  let ?A0 = "err A"
kleing@10496
   112
  let ?r0 = "Err.le r"
kleing@10496
   113
  let ?f0 = "lift2 f"
kleing@10496
   114
kleing@10496
   115
  from s
kleing@10496
   116
  obtain
kleing@10496
   117
    ord: "order ?r0" and
kleing@10496
   118
    clo: "closed ?A0 ?f0" and
kleing@10496
   119
    ub1: "\<forall>x\<in>?A0. \<forall>y\<in>?A0. x <=_?r0 x +_?f0 y" and
kleing@10496
   120
    ub2: "\<forall>x\<in>?A0. \<forall>y\<in>?A0. y <=_?r0 x +_?f0 y" and
kleing@10496
   121
    lub: "\<forall>x\<in>?A0. \<forall>y\<in>?A0. \<forall>z\<in>?A0. x <=_?r0 z \<and> y <=_?r0 z \<longrightarrow> x +_?f0 y <=_?r0 z"
kleing@10496
   122
    by (unfold semilat_def) simp
kleing@10496
   123
kleing@10496
   124
  let ?A = "err (opt A)" 
kleing@10496
   125
  let ?r = "Err.le (Opt.le r)"
kleing@10496
   126
  let ?f = "lift2 (Opt.sup f)"
kleing@10496
   127
kleing@10496
   128
  from ord
kleing@10496
   129
  have "order ?r"
kleing@10496
   130
    by simp
kleing@10496
   131
kleing@10496
   132
  moreover
kleing@10496
   133
kleing@10496
   134
  have "closed ?A ?f"
kleing@10496
   135
  proof (unfold closed_def, intro strip)
kleing@10496
   136
    fix x y    
kleing@10496
   137
    assume x: "x : ?A" 
kleing@10496
   138
    assume y: "y : ?A" 
kleing@10496
   139
kleing@11085
   140
    { fix a b
kleing@10496
   141
      assume ab: "x = OK a" "y = OK b"
kleing@10496
   142
      
kleing@10496
   143
      with x 
kleing@13006
   144
      have a: "\<And>c. a = Some c \<Longrightarrow> c : A"
kleing@10496
   145
        by (clarsimp simp add: opt_def)
kleing@10496
   146
kleing@10496
   147
      from ab y
kleing@13006
   148
      have b: "\<And>d. b = Some d \<Longrightarrow> d : A"
kleing@10496
   149
        by (clarsimp simp add: opt_def)
kleing@10496
   150
      
kleing@10496
   151
      { fix c d assume "a = Some c" "b = Some d"
kleing@10496
   152
        with ab x y
kleing@10496
   153
        have "c:A & d:A"
kleing@10496
   154
          by (simp add: err_def opt_def Bex_def)
kleing@10496
   155
        with clo
kleing@10496
   156
        have "f c d : err A"
kleing@10496
   157
          by (simp add: closed_def plussub_def err_def lift2_def)
kleing@10496
   158
        moreover
kleing@10496
   159
        fix z assume "f c d = OK z"
kleing@10496
   160
        ultimately
kleing@10496
   161
        have "z : A" by simp
kleing@10496
   162
      } note f_closed = this    
kleing@10496
   163
kleing@10496
   164
      have "sup f a b : ?A"
kleing@10496
   165
      proof (cases a)
kleing@10496
   166
        case None
kleing@10496
   167
        thus ?thesis
kleing@10496
   168
          by (simp add: sup_def opt_def) (cases b, simp, simp add: b Bex_def)
kleing@10496
   169
      next
kleing@10496
   170
        case Some
kleing@10496
   171
        thus ?thesis
kleing@10496
   172
          by (auto simp add: sup_def opt_def Bex_def a b f_closed split: err.split option.split)
kleing@10496
   173
      qed
kleing@10496
   174
    }
kleing@10496
   175
kleing@10496
   176
    thus "x +_?f y : ?A"
kleing@10496
   177
      by (simp add: plussub_def lift2_def split: err.split)
kleing@10496
   178
  qed
kleing@10496
   179
    
kleing@10496
   180
  moreover
kleing@10496
   181
kleing@11085
   182
  { fix a b c 
kleing@11085
   183
    assume "a \<in> opt A" "b \<in> opt A" "a +_(sup f) b = OK c" 
kleing@11085
   184
    moreover
kleing@11085
   185
    from ord have "order r" by simp
kleing@11085
   186
    moreover
kleing@11085
   187
    { fix x y z
kleing@11085
   188
      assume "x \<in> A" "y \<in> A" 
kleing@11085
   189
      hence "OK x \<in> err A \<and> OK y \<in> err A" by simp
kleing@11085
   190
      with ub1 ub2
kleing@11085
   191
      have "(OK x) <=_(Err.le r) (OK x) +_(lift2 f) (OK y) \<and>
kleing@11085
   192
            (OK y) <=_(Err.le r) (OK x) +_(lift2 f) (OK y)"
kleing@11085
   193
        by blast
kleing@11085
   194
      moreover
kleing@11085
   195
      assume "x +_f y = OK z"
kleing@11085
   196
      ultimately
kleing@11085
   197
      have "x <=_r z \<and> y <=_r z"
kleing@11085
   198
        by (auto simp add: plussub_def lift2_def Err.le_def lesub_def)
kleing@11085
   199
    }
kleing@11085
   200
    ultimately
kleing@11085
   201
    have "a <=_(le r) c \<and> b <=_(le r) c"
kleing@11085
   202
      by (auto simp add: sup_def le_def lesub_def plussub_def 
kleing@11085
   203
               dest: order_refl split: option.splits err.splits)
kleing@11085
   204
  }
kleing@11085
   205
     
kleing@11085
   206
  hence "(\<forall>x\<in>?A. \<forall>y\<in>?A. x <=_?r x +_?f y) \<and> (\<forall>x\<in>?A. \<forall>y\<in>?A. y <=_?r x +_?f y)"
kleing@11085
   207
    by (auto simp add: lesub_def plussub_def Err.le_def lift2_def split: err.split)
kleing@10496
   208
kleing@10496
   209
  moreover
kleing@10496
   210
kleing@10496
   211
  have "\<forall>x\<in>?A. \<forall>y\<in>?A. \<forall>z\<in>?A. x <=_?r z \<and> y <=_?r z \<longrightarrow> x +_?f y <=_?r z"
kleing@10496
   212
  proof (intro strip, elim conjE)
kleing@10496
   213
    fix x y z
kleing@10496
   214
    assume xyz: "x : ?A" "y : ?A" "z : ?A"
kleing@10496
   215
    assume xz: "x <=_?r z"
kleing@10496
   216
    assume yz: "y <=_?r z"
kleing@10496
   217
kleing@10496
   218
    { fix a b c
kleing@10496
   219
      assume ok: "x = OK a" "y = OK b" "z = OK c"
kleing@10496
   220
kleing@10496
   221
      { fix d e g
kleing@10496
   222
        assume some: "a = Some d" "b = Some e" "c = Some g"
kleing@10496
   223
        
kleing@10496
   224
        with ok xyz
kleing@10496
   225
        obtain "OK d:err A" "OK e:err A" "OK g:err A"
kleing@10496
   226
          by simp
kleing@10496
   227
        with lub
kleing@13006
   228
        have "\<lbrakk> (OK d) <=_(Err.le r) (OK g); (OK e) <=_(Err.le r) (OK g) \<rbrakk>
kleing@13006
   229
          \<Longrightarrow> (OK d) +_(lift2 f) (OK e) <=_(Err.le r) (OK g)"
kleing@10496
   230
          by blast
kleing@13006
   231
        hence "\<lbrakk> d <=_r g; e <=_r g \<rbrakk> \<Longrightarrow> \<exists>y. d +_f e = OK y \<and> y <=_r g"
kleing@10496
   232
          by simp
kleing@10496
   233
kleing@10496
   234
        with ok some xyz xz yz
kleing@10496
   235
        have "x +_?f y <=_?r z"
kleing@10496
   236
          by (auto simp add: sup_def le_def lesub_def lift2_def plussub_def Err.le_def)
kleing@10496
   237
      } note this [intro!]
kleing@10496
   238
kleing@10496
   239
      from ok xyz xz yz
kleing@10496
   240
      have "x +_?f y <=_?r z"
kleing@10496
   241
        by - (cases a, simp, cases b, simp, cases c, simp, blast)
kleing@10496
   242
    }
kleing@10496
   243
    
kleing@10496
   244
    with xyz xz yz
kleing@10496
   245
    show "x +_?f y <=_?r z"
kleing@10496
   246
      by - (cases x, simp, cases y, simp, cases z, simp+)
kleing@10496
   247
  qed
kleing@10496
   248
kleing@10496
   249
  ultimately
kleing@10496
   250
kleing@10496
   251
  show "semilat (?A,?r,?f)"
kleing@10496
   252
    by (unfold semilat_def) simp
kleing@10496
   253
qed 
kleing@10496
   254
kleing@10496
   255
lemma top_le_opt_Some [iff]: 
kleing@10496
   256
  "top (le r) (Some T) = top r T"
kleing@10496
   257
apply (unfold top_def)
kleing@10496
   258
apply (rule iffI)
kleing@10496
   259
 apply blast
kleing@10496
   260
apply (rule allI)
kleing@10496
   261
apply (case_tac "x")
kleing@10496
   262
apply simp+
kleing@10496
   263
done 
kleing@10496
   264
kleing@10496
   265
lemma Top_le_conv:
kleing@13006
   266
  "\<lbrakk> order r; top r T \<rbrakk> \<Longrightarrow> (T <=_r x) = (x = T)"
kleing@10496
   267
apply (unfold top_def)
kleing@10496
   268
apply (blast intro: order_antisym)
kleing@10496
   269
done 
kleing@10496
   270
kleing@10496
   271
kleing@10496
   272
lemma acc_le_optI [intro!]:
kleing@13006
   273
  "acc r \<Longrightarrow> acc(le r)"
kleing@10496
   274
apply (unfold acc_def lesub_def le_def lesssub_def)
berghofe@22271
   275
apply (simp add: wfP_eq_minimal split: option.split)
kleing@10496
   276
apply clarify
kleing@10496
   277
apply (case_tac "? a. Some a : Q")
kleing@10496
   278
 apply (erule_tac x = "{a . Some a : Q}" in allE)
kleing@10496
   279
 apply blast
kleing@10496
   280
apply (case_tac "x")
kleing@10496
   281
 apply blast
kleing@10496
   282
apply blast
kleing@10496
   283
done 
kleing@10496
   284
kleing@10496
   285
lemma option_map_in_optionI:
kleing@13006
   286
  "\<lbrakk> ox : opt S; !x:S. ox = Some x \<longrightarrow> f x : S \<rbrakk> 
kleing@13006
   287
  \<Longrightarrow> option_map f ox : opt S";
kleing@10496
   288
apply (unfold option_map_def)
kleing@10496
   289
apply (simp split: option.split)
kleing@10496
   290
apply blast
kleing@10496
   291
done 
kleing@10496
   292
kleing@10496
   293
end