Theory Opt

(*  Title:      HOL/MicroJava/BV/Opt.thy
    ID:         $Id: Opt.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Tobias Nipkow
    Copyright   2000 TUM

More about options
*)

header {* \isaheader{More about Options} *}

theory Opt = Err:

constdefs
  le :: "'a ord => 'a option ord"
  "le r o1 o2 ≡
  case o2 of None => o1=None | Some y => (case o1 of None => True | Some x => x \<sqsubseteq>r y)"

  opt :: "'a set => 'a option set"
  "opt A ≡ insert None {Some y |y. y ∈ A}"

  sup :: "'a ebinop => 'a option ebinop"
  "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)))"

  esl :: "'a esl => 'a option esl"
  "esl ≡ λ(A,r,f). (opt A, le r, sup f)"


lemma unfold_le_opt:
  "o1 \<sqsubseteq>le r o2 = 
  (case o2 of None => o1=None | 
              Some y => (case o1 of None => True | Some x => x \<sqsubseteq>r y))"
(*<*)
apply (unfold lesub_def le_def)
apply (rule refl)
done
(*>*)

lemma le_opt_refl: "order r ==> x \<sqsubseteq>le r x"
(*<*) by (simp add: unfold_le_opt split: option.split) (*<*)

lemma le_opt_trans [rule_format]:
  "order r ==> x \<sqsubseteq>le r y --> y \<sqsubseteq>le r z --> x \<sqsubseteq>le r z"
(*<*)
apply (simp add: unfold_le_opt split: option.split)
apply (blast intro: order_trans)
done
(*>*)

lemma le_opt_antisym [rule_format]:
  "order r ==> x \<sqsubseteq>le r y --> y \<sqsubseteq>le r x --> x=y"
(*<*)
apply (simp add: unfold_le_opt split: option.split)
apply (blast intro: order_antisym)
done
(*>*)

lemma order_le_opt [intro!,simp]: "order r ==> order(le r)"
(*<*)
apply (subst order_def)
apply (blast intro: le_opt_refl le_opt_trans le_opt_antisym)
done 
(*>*)

lemma None_bot [iff]:  "None \<sqsubseteq>le r ox"
(*<*)
apply (unfold lesub_def le_def)
apply (simp split: option.split)
done 
(*>*)

lemma Some_le [iff]: "(Some x \<sqsubseteq>le r z) = (∃y. z = Some y ∧ x \<sqsubseteq>r y)"
(*<*)
apply (unfold lesub_def le_def)
apply (simp split: option.split)
done 
(*>*)

lemma le_None [iff]: "(x \<sqsubseteq>le r None) = (x = None)";
(*<*)
apply (unfold lesub_def le_def)
apply (simp split: option.split)
done 
(*>*)

lemma OK_None_bot [iff]: "OK None \<sqsubseteq>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 \<squnion>sup f None = OK x"
(*<*) by (simp add: plussub_def sup_def split: option.split) (*>*)

lemma sup_None2 [iff]: "None \<squnion>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)"
(*<*) by (unfold opt_def) auto (*>*)

lemma semilat_opt [intro, simp]:
  "err_semilat L ==> err_semilat (Opt.esl L)"
(*<*)
proof -
  assume s: "err_semilat L" 
  obtain A r f where [simp]: "L = (A,r,f)" by (cases L)
  let ?A0 = "err A" and ?r0 = "Err.le r" and ?f0 = "lift2 f"
  from s obtain
    ord: "order ?r0" and
    clo: "closed ?A0 ?f0" and
    ub1: "∀x∈?A0. ∀y∈?A0. x \<sqsubseteq>?r0 x \<squnion>?f0 y" and
    ub2: "∀x∈?A0. ∀y∈?A0. y \<sqsubseteq>?r0 x \<squnion>?f0 y" and
    lub: "∀x∈?A0. ∀y∈?A0. ∀z∈?A0. x \<sqsubseteq>?r0 z ∧ y \<sqsubseteq>?r0 z --> x \<squnion>?f0 y \<sqsubseteq>?r0 z"
    by (unfold semilat_def sl_def) simp

  let ?A = "err (opt A)" and ?r = "Err.le (Opt.le r)" and ?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" and 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 \<squnion>?f y ∈ ?A" by (simp add: plussub_def lift2_def split: err.split)
  qed
  moreover
  { fix a b c assume "a ∈ opt A" and "b ∈ opt A" and "a \<squnion>sup f b = OK c" 
    moreover from ord have "order r" by simp
    moreover
    { fix x y z assume "x ∈ A" and "y ∈ A" 
      hence "OK x ∈ err A ∧ OK y ∈ err A" by simp
      with ub1 ub2
      have "(OK x) \<sqsubseteq>Err.le r (OK x) \<squnion>lift2 f (OK y) ∧
            (OK y) \<sqsubseteq>Err.le r (OK x) \<squnion>lift2 f (OK y)"
        by blast
      moreover assume "x \<squnion>f y = OK z"
      ultimately have "x \<sqsubseteq>r z ∧ y \<sqsubseteq>r z"
        by (auto simp add: plussub_def lift2_def Err.le_def lesub_def)
    }
    ultimately have "a \<sqsubseteq>le r c ∧ b \<sqsubseteq>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 \<sqsubseteq>?r x \<squnion>?f y) ∧ (∀x∈?A. ∀y∈?A. y \<sqsubseteq>?r x \<squnion>?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 \<sqsubseteq>?r z ∧ y \<sqsubseteq>?r z --> x \<squnion>?f y \<sqsubseteq>?r z"
  proof (intro strip, elim conjE)
    fix x y z
    assume xyz: "x ∈ ?A"   "y ∈ ?A"   "z ∈ ?A"
    assume xz: "x \<sqsubseteq>?r z" and yz: "y \<sqsubseteq>?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 \<sqsubseteq>Err.le r OK g; OK e \<sqsubseteq>Err.le r OK g |] ==> OK d \<squnion>lift2 f OK e \<sqsubseteq>Err.le r OK g"
          by blast
        hence "[| d \<sqsubseteq>r g; e \<sqsubseteq>r g |] ==> ∃y. d \<squnion>f e = OK y ∧ y \<sqsubseteq>r g" by simp
        with ok some xyz xz yz have "x \<squnion>?f y \<sqsubseteq>?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 \<squnion>?f y \<sqsubseteq>?r z"
        by - (cases a, simp, cases b, simp, cases c, simp, blast)
    }    
    with xyz xz yz show "x \<squnion>?f y \<sqsubseteq>?r z"
      by - (cases x, simp, cases y, simp, cases z, simp+)
  qed
  ultimately show "err_semilat (Opt.esl L)"
    by (unfold semilat_def esl_def sl_def) simp
qed 
(*>*)

lemma top_le_opt_Some [iff]: "top (le r) (Some T) = top r T"
(*<*)
apply (unfold top_def)
apply (rule iffI)
 apply blast
apply (rule allI)
apply (case_tac "x")
apply simp+
done 
(*>*)

lemma Top_le_conv:  "[| order r; top r T |] ==> (T \<sqsubseteq>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 clarify
apply (case_tac "∃a. Some a ∈ Q")
 apply (erule_tac x = "{a . Some a ∈ Q}" in allE)
 apply blast
apply (case_tac "x")
 apply blast
apply blast
done 
(*>*)

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 blast
done 
(*>*)

end