src/HOL/MicroJava/DFA/Opt.thy
changeset 33954 1bc3b688548c
child 35416 d8d7d1b785af
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/MicroJava/DFA/Opt.thy	Tue Nov 24 14:37:23 2009 +0100
     1.3 @@ -0,0 +1,292 @@
     1.4 +(*  Title:      HOL/MicroJava/BV/Opt.thy
     1.5 +    Author:     Tobias Nipkow
     1.6 +    Copyright   2000 TUM
     1.7 +*)
     1.8 +
     1.9 +header {* \isaheader{More about Options} *}
    1.10 +
    1.11 +theory Opt
    1.12 +imports Err
    1.13 +begin
    1.14 +
    1.15 +constdefs
    1.16 + le :: "'a ord \<Rightarrow> 'a option ord"
    1.17 +"le r o1 o2 == case o2 of None \<Rightarrow> o1=None |
    1.18 +                              Some y \<Rightarrow> (case o1 of None \<Rightarrow> True
    1.19 +                                                  | Some x \<Rightarrow> x <=_r y)"
    1.20 +
    1.21 + opt :: "'a set \<Rightarrow> 'a option set"
    1.22 +"opt A == insert None {x . ? y:A. x = Some y}"
    1.23 +
    1.24 + sup :: "'a ebinop \<Rightarrow> 'a option ebinop"
    1.25 +"sup f o1 o2 ==  
    1.26 + case o1 of None \<Rightarrow> OK o2 | Some x \<Rightarrow> (case o2 of None \<Rightarrow> OK o1
    1.27 +     | Some y \<Rightarrow> (case f x y of Err \<Rightarrow> Err | OK z \<Rightarrow> OK (Some z)))"
    1.28 +
    1.29 + esl :: "'a esl \<Rightarrow> 'a option esl"
    1.30 +"esl == %(A,r,f). (opt A, le r, sup f)"
    1.31 +
    1.32 +lemma unfold_le_opt:
    1.33 +  "o1 <=_(le r) o2 = 
    1.34 +  (case o2 of None \<Rightarrow> o1=None | 
    1.35 +              Some y \<Rightarrow> (case o1 of None \<Rightarrow> True | Some x \<Rightarrow> x <=_r y))"
    1.36 +apply (unfold lesub_def le_def)
    1.37 +apply (rule refl)
    1.38 +done
    1.39 +
    1.40 +lemma le_opt_refl:
    1.41 +  "order r \<Longrightarrow> o1 <=_(le r) o1"
    1.42 +by (simp add: unfold_le_opt split: option.split)
    1.43 +
    1.44 +lemma le_opt_trans [rule_format]:
    1.45 +  "order r \<Longrightarrow> 
    1.46 +   o1 <=_(le r) o2 \<longrightarrow> o2 <=_(le r) o3 \<longrightarrow> o1 <=_(le r) o3"
    1.47 +apply (simp add: unfold_le_opt split: option.split)
    1.48 +apply (blast intro: order_trans)
    1.49 +done
    1.50 +
    1.51 +lemma le_opt_antisym [rule_format]:
    1.52 +  "order r \<Longrightarrow> o1 <=_(le r) o2 \<longrightarrow> o2 <=_(le r) o1 \<longrightarrow> o1=o2"
    1.53 +apply (simp add: unfold_le_opt split: option.split)
    1.54 +apply (blast intro: order_antisym)
    1.55 +done
    1.56 +
    1.57 +lemma order_le_opt [intro!,simp]:
    1.58 +  "order r \<Longrightarrow> order(le r)"
    1.59 +apply (subst Semilat.order_def)
    1.60 +apply (blast intro: le_opt_refl le_opt_trans le_opt_antisym)
    1.61 +done 
    1.62 +
    1.63 +lemma None_bot [iff]: 
    1.64 +  "None <=_(le r) ox"
    1.65 +apply (unfold lesub_def le_def)
    1.66 +apply (simp split: option.split)
    1.67 +done 
    1.68 +
    1.69 +lemma Some_le [iff]:
    1.70 +  "(Some x <=_(le r) ox) = (? y. ox = Some y & x <=_r y)"
    1.71 +apply (unfold lesub_def le_def)
    1.72 +apply (simp split: option.split)
    1.73 +done 
    1.74 +
    1.75 +lemma le_None [iff]:
    1.76 +  "(ox <=_(le r) None) = (ox = None)";
    1.77 +apply (unfold lesub_def le_def)
    1.78 +apply (simp split: option.split)
    1.79 +done 
    1.80 +
    1.81 +
    1.82 +lemma OK_None_bot [iff]:
    1.83 +  "OK None <=_(Err.le (le r)) x"
    1.84 +  by (simp add: lesub_def Err.le_def le_def split: option.split err.split)
    1.85 +
    1.86 +lemma sup_None1 [iff]:
    1.87 +  "x +_(sup f) None = OK x"
    1.88 +  by (simp add: plussub_def sup_def split: option.split)
    1.89 +
    1.90 +lemma sup_None2 [iff]:
    1.91 +  "None +_(sup f) x = OK x"
    1.92 +  by (simp add: plussub_def sup_def split: option.split)
    1.93 +
    1.94 +
    1.95 +lemma None_in_opt [iff]:
    1.96 +  "None : opt A"
    1.97 +by (simp add: opt_def)
    1.98 +
    1.99 +lemma Some_in_opt [iff]:
   1.100 +  "(Some x : opt A) = (x:A)"
   1.101 +apply (unfold opt_def)
   1.102 +apply auto
   1.103 +done 
   1.104 +
   1.105 +
   1.106 +lemma semilat_opt [intro, simp]:
   1.107 +  "\<And>L. err_semilat L \<Longrightarrow> err_semilat (Opt.esl L)"
   1.108 +proof (unfold Opt.esl_def Err.sl_def, simp add: split_tupled_all)
   1.109 +  
   1.110 +  fix A r f
   1.111 +  assume s: "semilat (err A, Err.le r, lift2 f)"
   1.112 + 
   1.113 +  let ?A0 = "err A"
   1.114 +  let ?r0 = "Err.le r"
   1.115 +  let ?f0 = "lift2 f"
   1.116 +
   1.117 +  from s
   1.118 +  obtain
   1.119 +    ord: "order ?r0" and
   1.120 +    clo: "closed ?A0 ?f0" and
   1.121 +    ub1: "\<forall>x\<in>?A0. \<forall>y\<in>?A0. x <=_?r0 x +_?f0 y" and
   1.122 +    ub2: "\<forall>x\<in>?A0. \<forall>y\<in>?A0. y <=_?r0 x +_?f0 y" and
   1.123 +    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"
   1.124 +    by (unfold semilat_def) simp
   1.125 +
   1.126 +  let ?A = "err (opt A)" 
   1.127 +  let ?r = "Err.le (Opt.le r)"
   1.128 +  let ?f = "lift2 (Opt.sup f)"
   1.129 +
   1.130 +  from ord
   1.131 +  have "order ?r"
   1.132 +    by simp
   1.133 +
   1.134 +  moreover
   1.135 +
   1.136 +  have "closed ?A ?f"
   1.137 +  proof (unfold closed_def, intro strip)
   1.138 +    fix x y    
   1.139 +    assume x: "x : ?A" 
   1.140 +    assume y: "y : ?A" 
   1.141 +
   1.142 +    { fix a b
   1.143 +      assume ab: "x = OK a" "y = OK b"
   1.144 +      
   1.145 +      with x 
   1.146 +      have a: "\<And>c. a = Some c \<Longrightarrow> c : A"
   1.147 +        by (clarsimp simp add: opt_def)
   1.148 +
   1.149 +      from ab y
   1.150 +      have b: "\<And>d. b = Some d \<Longrightarrow> d : A"
   1.151 +        by (clarsimp simp add: opt_def)
   1.152 +      
   1.153 +      { fix c d assume "a = Some c" "b = Some d"
   1.154 +        with ab x y
   1.155 +        have "c:A & d:A"
   1.156 +          by (simp add: err_def opt_def Bex_def)
   1.157 +        with clo
   1.158 +        have "f c d : err A"
   1.159 +          by (simp add: closed_def plussub_def err_def lift2_def)
   1.160 +        moreover
   1.161 +        fix z assume "f c d = OK z"
   1.162 +        ultimately
   1.163 +        have "z : A" by simp
   1.164 +      } note f_closed = this    
   1.165 +
   1.166 +      have "sup f a b : ?A"
   1.167 +      proof (cases a)
   1.168 +        case None
   1.169 +        thus ?thesis
   1.170 +          by (simp add: sup_def opt_def) (cases b, simp, simp add: b Bex_def)
   1.171 +      next
   1.172 +        case Some
   1.173 +        thus ?thesis
   1.174 +          by (auto simp add: sup_def opt_def Bex_def a b f_closed split: err.split option.split)
   1.175 +      qed
   1.176 +    }
   1.177 +
   1.178 +    thus "x +_?f y : ?A"
   1.179 +      by (simp add: plussub_def lift2_def split: err.split)
   1.180 +  qed
   1.181 +    
   1.182 +  moreover
   1.183 +
   1.184 +  { fix a b c 
   1.185 +    assume "a \<in> opt A" "b \<in> opt A" "a +_(sup f) b = OK c" 
   1.186 +    moreover
   1.187 +    from ord have "order r" by simp
   1.188 +    moreover
   1.189 +    { fix x y z
   1.190 +      assume "x \<in> A" "y \<in> A" 
   1.191 +      hence "OK x \<in> err A \<and> OK y \<in> err A" by simp
   1.192 +      with ub1 ub2
   1.193 +      have "(OK x) <=_(Err.le r) (OK x) +_(lift2 f) (OK y) \<and>
   1.194 +            (OK y) <=_(Err.le r) (OK x) +_(lift2 f) (OK y)"
   1.195 +        by blast
   1.196 +      moreover
   1.197 +      assume "x +_f y = OK z"
   1.198 +      ultimately
   1.199 +      have "x <=_r z \<and> y <=_r z"
   1.200 +        by (auto simp add: plussub_def lift2_def Err.le_def lesub_def)
   1.201 +    }
   1.202 +    ultimately
   1.203 +    have "a <=_(le r) c \<and> b <=_(le r) c"
   1.204 +      by (auto simp add: sup_def le_def lesub_def plussub_def 
   1.205 +               dest: order_refl split: option.splits err.splits)
   1.206 +  }
   1.207 +     
   1.208 +  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)"
   1.209 +    by (auto simp add: lesub_def plussub_def Err.le_def lift2_def split: err.split)
   1.210 +
   1.211 +  moreover
   1.212 +
   1.213 +  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"
   1.214 +  proof (intro strip, elim conjE)
   1.215 +    fix x y z
   1.216 +    assume xyz: "x : ?A" "y : ?A" "z : ?A"
   1.217 +    assume xz: "x <=_?r z"
   1.218 +    assume yz: "y <=_?r z"
   1.219 +
   1.220 +    { fix a b c
   1.221 +      assume ok: "x = OK a" "y = OK b" "z = OK c"
   1.222 +
   1.223 +      { fix d e g
   1.224 +        assume some: "a = Some d" "b = Some e" "c = Some g"
   1.225 +        
   1.226 +        with ok xyz
   1.227 +        obtain "OK d:err A" "OK e:err A" "OK g:err A"
   1.228 +          by simp
   1.229 +        with lub
   1.230 +        have "\<lbrakk> (OK d) <=_(Err.le r) (OK g); (OK e) <=_(Err.le r) (OK g) \<rbrakk>
   1.231 +          \<Longrightarrow> (OK d) +_(lift2 f) (OK e) <=_(Err.le r) (OK g)"
   1.232 +          by blast
   1.233 +        hence "\<lbrakk> d <=_r g; e <=_r g \<rbrakk> \<Longrightarrow> \<exists>y. d +_f e = OK y \<and> y <=_r g"
   1.234 +          by simp
   1.235 +
   1.236 +        with ok some xyz xz yz
   1.237 +        have "x +_?f y <=_?r z"
   1.238 +          by (auto simp add: sup_def le_def lesub_def lift2_def plussub_def Err.le_def)
   1.239 +      } note this [intro!]
   1.240 +
   1.241 +      from ok xyz xz yz
   1.242 +      have "x +_?f y <=_?r z"
   1.243 +        by - (cases a, simp, cases b, simp, cases c, simp, blast)
   1.244 +    }
   1.245 +    
   1.246 +    with xyz xz yz
   1.247 +    show "x +_?f y <=_?r z"
   1.248 +      by - (cases x, simp, cases y, simp, cases z, simp+)
   1.249 +  qed
   1.250 +
   1.251 +  ultimately
   1.252 +
   1.253 +  show "semilat (?A,?r,?f)"
   1.254 +    by (unfold semilat_def) simp
   1.255 +qed 
   1.256 +
   1.257 +lemma top_le_opt_Some [iff]: 
   1.258 +  "top (le r) (Some T) = top r T"
   1.259 +apply (unfold top_def)
   1.260 +apply (rule iffI)
   1.261 + apply blast
   1.262 +apply (rule allI)
   1.263 +apply (case_tac "x")
   1.264 +apply simp+
   1.265 +done 
   1.266 +
   1.267 +lemma Top_le_conv:
   1.268 +  "\<lbrakk> order r; top r T \<rbrakk> \<Longrightarrow> (T <=_r x) = (x = T)"
   1.269 +apply (unfold top_def)
   1.270 +apply (blast intro: order_antisym)
   1.271 +done 
   1.272 +
   1.273 +
   1.274 +lemma acc_le_optI [intro!]:
   1.275 +  "acc r \<Longrightarrow> acc(le r)"
   1.276 +apply (unfold acc_def lesub_def le_def lesssub_def)
   1.277 +apply (simp add: wf_eq_minimal split: option.split)
   1.278 +apply clarify
   1.279 +apply (case_tac "? a. Some a : Q")
   1.280 + apply (erule_tac x = "{a . Some a : Q}" in allE)
   1.281 + apply blast
   1.282 +apply (case_tac "x")
   1.283 + apply blast
   1.284 +apply blast
   1.285 +done 
   1.286 +
   1.287 +lemma option_map_in_optionI:
   1.288 +  "\<lbrakk> ox : opt S; !x:S. ox = Some x \<longrightarrow> f x : S \<rbrakk> 
   1.289 +  \<Longrightarrow> Option.map f ox : opt S";
   1.290 +apply (unfold Option.map_def)
   1.291 +apply (simp split: option.split)
   1.292 +apply blast
   1.293 +done 
   1.294 +
   1.295 +end