# Theory Opt

Up to index of Isabelle/HOL/HOL-MicroJava-skip_proofs

theory Opt
imports Err
`(*  Title:      HOL/MicroJava/DFA/Opt.thy    Author:     Tobias Nipkow    Copyright   2000 TUM*)header {* \isaheader{More about Options} *}theory Optimports Errbegindefinition le :: "'a ord => 'a option ord" where"le r o1 o2 == case o2 of None => o1=None |                              Some y => (case o1 of None => True                                                  | Some x => x <=_r y)"definition opt :: "'a set => 'a option set" where"opt A == insert None {x . ? y:A. x = Some y}"definition sup :: "'a ebinop => 'a option ebinop" where"sup f o1 o2 ==   case o1 of None => OK o2 | Some x => (case o2 of None => OK o1     | Some y => (case f x y of Err => Err | OK z => OK (Some z)))"definition esl :: "'a esl => 'a option esl" where"esl == %(A,r,f). (opt A, le r, sup f)"lemma unfold_le_opt:  "o1 <=_(le r) o2 =   (case o2 of None => o1=None |               Some y => (case o1 of None => True | Some x => x <=_r y))"apply (unfold lesub_def le_def)apply (rule refl)donelemma le_opt_refl:  "order r ==> o1 <=_(le r) o1"by (simp add: unfold_le_opt split: option.split)lemma le_opt_trans [rule_format]:  "order r ==>    o1 <=_(le r) o2 --> o2 <=_(le r) o3 --> o1 <=_(le r) o3"apply (simp add: unfold_le_opt split: option.split)apply (blast intro: order_trans)donelemma le_opt_antisym [rule_format]:  "order r ==> o1 <=_(le r) o2 --> o2 <=_(le r) o1 --> o1=o2"apply (simp add: unfold_le_opt split: option.split)apply (blast intro: order_antisym)donelemma order_le_opt [intro!,simp]:  "order r ==> order(le r)"apply (subst Semilat.order_def)apply (blast intro: le_opt_refl le_opt_trans le_opt_antisym)done lemma None_bot [iff]:   "None <=_(le r) ox"apply (unfold lesub_def le_def)apply (simp split: option.split)done lemma Some_le [iff]:  "(Some x <=_(le r) ox) = (? y. ox = Some y & x <=_r y)"apply (unfold lesub_def le_def)apply (simp split: option.split)done lemma le_None [iff]:  "(ox <=_(le r) None) = (ox = None)";apply (unfold lesub_def le_def)apply (simp split: option.split)done lemma OK_None_bot [iff]:  "OK None <=_(Err.le (le r)) x"  by (simp add: lesub_def Err.le_def le_def split: option.split err.split)lemma sup_None1 [iff]:  "x +_(sup f) None = OK x"  by (simp add: plussub_def sup_def split: option.split)lemma sup_None2 [iff]:  "None +_(sup f) x = OK x"  by (simp add: plussub_def sup_def split: option.split)lemma None_in_opt [iff]:  "None : opt A"by (simp add: opt_def)lemma Some_in_opt [iff]:  "(Some x : opt A) = (x:A)"apply (unfold opt_def)apply autodone lemma semilat_opt [intro, simp]:  "!!L. err_semilat L ==> err_semilat (Opt.esl L)"proof (unfold Opt.esl_def Err.sl_def, simp add: split_tupled_all)    fix A r f  assume s: "semilat (err A, Err.le r, lift2 f)"   let ?A0 = "err A"  let ?r0 = "Err.le r"  let ?f0 = "lift2 f"  from s  obtain    ord: "order ?r0" and    clo: "closed ?A0 ?f0" and    ub1: "∀x∈?A0. ∀y∈?A0. x <=_?r0 x +_?f0 y" and    ub2: "∀x∈?A0. ∀y∈?A0. y <=_?r0 x +_?f0 y" and    lub: "∀x∈?A0. ∀y∈?A0. ∀z∈?A0. x <=_?r0 z ∧ y <=_?r0 z --> x +_?f0 y <=_?r0 z"    by (unfold semilat_def) simp  let ?A = "err (opt A)"   let ?r = "Err.le (Opt.le r)"  let ?f = "lift2 (Opt.sup f)"  from ord  have "order ?r"    by simp  moreover  have "closed ?A ?f"  proof (unfold closed_def, intro strip)    fix x y        assume x: "x : ?A"     assume y: "y : ?A"     { fix a b      assume ab: "x = OK a" "y = OK b"            with x       have a: "!!c. a = Some c ==> c : A"        by (clarsimp simp add: opt_def)      from ab y      have b: "!!d. b = Some d ==> d : A"        by (clarsimp simp add: opt_def)            { fix c d assume "a = Some c" "b = Some d"        with ab x y        have "c:A & d:A"          by (simp add: err_def opt_def Bex_def)        with clo        have "f c d : err A"          by (simp add: closed_def plussub_def err_def lift2_def)        moreover        fix z assume "f c d = OK z"        ultimately        have "z : A" by simp      } note f_closed = this          have "sup f a b : ?A"      proof (cases a)        case None        thus ?thesis          by (simp add: sup_def opt_def) (cases b, simp, simp add: b Bex_def)      next        case Some        thus ?thesis          by (auto simp add: sup_def opt_def Bex_def a b f_closed split: err.split option.split)      qed    }    thus "x +_?f y : ?A"      by (simp add: plussub_def lift2_def split: err.split)  qed      moreover  { fix a b c     assume "a ∈ opt A" "b ∈ opt A" "a +_(sup f) b = OK c"     moreover    from ord have "order r" by simp    moreover    { fix x y z      assume "x ∈ A" "y ∈ A"       hence "OK x ∈ err A ∧ OK y ∈ err A" by simp      with ub1 ub2      have "(OK x) <=_(Err.le r) (OK x) +_(lift2 f) (OK y) ∧            (OK y) <=_(Err.le r) (OK x) +_(lift2 f) (OK y)"        by blast      moreover      assume "x +_f y = OK z"      ultimately      have "x <=_r z ∧ y <=_r z"        by (auto simp add: plussub_def lift2_def Err.le_def lesub_def)    }    ultimately    have "a <=_(le r) c ∧ b <=_(le r) c"      by (auto simp add: sup_def le_def lesub_def plussub_def                dest: order_refl split: option.splits err.splits)  }       hence "(∀x∈?A. ∀y∈?A. x <=_?r x +_?f y) ∧ (∀x∈?A. ∀y∈?A. y <=_?r x +_?f y)"    by (auto simp add: lesub_def plussub_def Err.le_def lift2_def split: err.split)  moreover  have "∀x∈?A. ∀y∈?A. ∀z∈?A. x <=_?r z ∧ y <=_?r z --> x +_?f y <=_?r z"  proof (intro strip, elim conjE)    fix x y z    assume xyz: "x : ?A" "y : ?A" "z : ?A"    assume xz: "x <=_?r z"    assume yz: "y <=_?r z"    { fix a b c      assume ok: "x = OK a" "y = OK b" "z = OK c"      { fix d e g        assume some: "a = Some d" "b = Some e" "c = Some g"                with ok xyz        obtain "OK d:err A" "OK e:err A" "OK g:err A"          by simp        with lub        have "[| (OK d) <=_(Err.le r) (OK g); (OK e) <=_(Err.le r) (OK g) |]          ==> (OK d) +_(lift2 f) (OK e) <=_(Err.le r) (OK g)"          by blast        hence "[| d <=_r g; e <=_r g |] ==> ∃y. d +_f e = OK y ∧ y <=_r g"          by simp        with ok some xyz xz yz        have "x +_?f y <=_?r z"          by (auto simp add: sup_def le_def lesub_def lift2_def plussub_def Err.le_def)      } note this [intro!]      from ok xyz xz yz      have "x +_?f y <=_?r z"        by - (cases a, simp, cases b, simp, cases c, simp, blast)    }        with xyz xz yz    show "x +_?f y <=_?r z"      by - (cases x, simp, cases y, simp, cases z, simp+)  qed  ultimately  show "semilat (?A,?r,?f)"    by (unfold semilat_def) simpqed lemma top_le_opt_Some [iff]:   "top (le r) (Some T) = top r T"apply (unfold top_def)apply (rule iffI) apply blastapply (rule allI)apply (case_tac "x")apply simp+done lemma Top_le_conv:  "[| order r; top r T |] ==> (T <=_r x) = (x = T)"apply (unfold top_def)apply (blast intro: order_antisym)done lemma acc_le_optI [intro!]:  "acc r ==> acc(le r)"apply (unfold acc_def lesub_def le_def lesssub_def)apply (simp add: wf_eq_minimal split: option.split)apply clarifyapply (case_tac "? a. Some a : Q") apply (erule_tac x = "{a . Some a : Q}" in allE) apply blastapply (case_tac "x") apply blastapply blastdone lemma option_map_in_optionI:  "[| ox : opt S; !x:S. ox = Some x --> f x : S |]   ==> Option.map f ox : opt S";apply (unfold Option.map_def)apply (simp split: option.split)apply blastdone end`