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