products/Sources/formale Sprachen/Isabelle/HOL/MicroJava/DFA/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: IO.vdmrt   Sprache: Isabelle

Original von: Isabelle©
(*  Title:      HOL/MicroJava/DFA/Opt.thy
    Author:     Tobias Nipkow
    Copyright   2000 TUM
*)

section \<open>More about Options\<close>

theory Opt
imports Err
begin

definition le :: "'a ord \ 'a option ord" where
"le r o1 o2 == case o2 of None \ o1=None |
                              Some y \<Rightarrow> (case o1 of None \<Rightarrow> True
                                                  | Some x \<Rightarrow> 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 \<Rightarrow> OK o2 | Some x \<Rightarrow> (case o2 of None \<Rightarrow> OK o1
     | Some y \<Rightarrow> (case f x y of Err \<Rightarrow> Err | OK z \<Rightarrow> 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 \<Rightarrow> o1=None | 
              Some y \<Rightarrow> (case o1 of None \<Rightarrow> True | Some x \<Rightarrow> x <=_r y))"
apply (unfold lesub_def le_def)
apply (rule refl)
done

lemma 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 \<longrightarrow> o2 <=_(le r) o3 \<longrightarrow> o1 <=_(le r) o3"
apply (simp add: unfold_le_opt split: option.split)
apply (blast intro: order_trans)
done

lemma 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)
done

lemma 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 auto
done 


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) \
          \<Longrightarrow> (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) 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 <=_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 \
  \<Longrightarrow> map_option f ox \<in> opt S"
apply (unfold map_option_case)
apply (simp split: option.split)
apply blast
done 

end

¤ Dauer der Verarbeitung: 0.21 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff