Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: HOLZF.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/MicroJava/DFA/Err.thy
    Author:     Tobias Nipkow
    Copyright   2000 TUM
*)

section \<open>The Error Type\<close>

theory Err
imports Semilat
begin

datatype 'a err = Err | OK 'a

type_synonym 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err"
type_synonym 'a esl = "'a set * 'a ord * 'a ebinop"

primrec ok_val :: "'a err \ 'a" where
  "ok_val (OK x) = x"

definition lift :: "('a \ 'b err) \ ('a err \ 'b err)" where
"lift f e == case e of Err \ Err | OK x \ f x"

definition lift2 :: "('a \ 'b \ 'c err) \ 'a err \ 'b err \ 'c err" where
"lift2 f e1 e2 ==
case e1 of Err  \<Rightarrow> Err
          | OK x \<Rightarrow> (case e2 of Err \<Rightarrow> Err | OK y \<Rightarrow> f x y)"

definition le :: "'a ord \ 'a err ord" where
"le r e1 e2 ==
        case e2 of Err \<Rightarrow> True |
                   OK y \<Rightarrow> (case e1 of Err \<Rightarrow> False | OK x \<Rightarrow> x <=_r y)"

definition sup :: "('a \ 'b \ 'c) \ ('a err \ 'b err \ 'c err)" where
"sup f == lift2(%x y. OK(x +_f y))"

definition err :: "'a set \ 'a err set" where
"err A == insert Err {x . \y\A. x = OK y}"

definition esl :: "'a sl \ 'a esl" where
"esl == %(A,r,f). (A,r, %x y. OK(f x y))"

definition sl :: "'a esl \ 'a err sl" where
"sl == %(A,r,f). (err A, le r, lift2 f)"

abbreviation
  err_semilat :: "'a esl \ bool"
  where "err_semilat L == semilat(Err.sl L)"

primrec strict :: "('a \ 'b err) \ ('a err \ 'b err)" where
  "strict f Err = Err"
| "strict f (OK x) = f x"

lemma strict_Some [simp]:
  "(strict f x = OK y) = (\ z. x = OK z \ f z = OK y)"
  by (cases x, auto)

lemma not_Err_eq:
  "(x \ Err) = (\a. x = OK a)"
  by (cases x) auto

lemma not_OK_eq:
  "(\y. x \ OK y) = (x = Err)"
  by (cases x) auto

lemma unfold_lesub_err:
  "e1 <=_(le r) e2 == le r e1 e2"
  by (simp add: lesub_def)

lemma le_err_refl:
  "\x. x <=_r x \ e <=_(Err.le r) e"
apply (unfold lesub_def Err.le_def)
apply (simp split: err.split)
done

lemma le_err_trans [rule_format]:
  "order r \ e1 <=_(le r) e2 \ e2 <=_(le r) e3 \ e1 <=_(le r) e3"
apply (unfold unfold_lesub_err le_def)
apply (simp split: err.split)
apply (blast intro: order_trans)
done

lemma le_err_antisym [rule_format]:
  "order r \ e1 <=_(le r) e2 \ e2 <=_(le r) e1 \ e1=e2"
apply (unfold unfold_lesub_err le_def)
apply (simp split: err.split)
apply (blast intro: order_antisym)
done

lemma OK_le_err_OK:
  "(OK x <=_(le r) OK y) = (x <=_r y)"
  by (simp add: unfold_lesub_err le_def)

lemma order_le_err [iff]:
  "order(le r) = order r"
apply (rule iffI)
apply (subst Semilat.order_def)
apply (blast dest: order_antisym OK_le_err_OK [THEN iffD2]
              intro: order_trans OK_le_err_OK [THEN iffD1])
apply (subst Semilat.order_def)
apply (blast intro: le_err_refl le_err_trans le_err_antisym
             dest: order_refl)
done

lemma le_Err [iff]:  "e <=_(le r) Err"
  by (simp add: unfold_lesub_err le_def)

lemma Err_le_conv [iff]:
"Err <=_(le r) e = (e = Err)"
  by (simp add: unfold_lesub_err le_def  split: err.split)

lemma le_OK_conv [iff]:
  "e <=_(le r) OK x = (\y. e = OK y & y <=_r x)"
  by (simp add: unfold_lesub_err le_def split: err.split)

lemma OK_le_conv:
"OK x <=_(le r) e = (e = Err | (\y. e = OK y & x <=_r y))"
  by (simp add: unfold_lesub_err le_def split: err.split)

lemma top_Err [iff]: "top (le r) Err"
  by (simp add: top_def)

lemma OK_less_conv [rule_format, iff]:
  "OK x <_(le r) e = (e=Err | (\y. e = OK y & x <_r y))"
  by (simp add: lesssub_def lesub_def le_def split: err.split)

lemma not_Err_less [rule_format, iff]:
  "~(Err <_(le r) x)"
  by (simp add: lesssub_def lesub_def le_def split: err.split)

lemma semilat_errI [intro]:
  assumes semilat: "semilat (A, r, f)"
  shows "semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
  using semilat
  apply (simp only: semilat_Def closed_def plussub_def lesub_def
    lift2_def Err.le_def err_def)
  apply (simp split: err.split)
  done

lemma err_semilat_eslI_aux:
  assumes semilat: "semilat (A, r, f)"
  shows "err_semilat(esl(A,r,f))"
  apply (unfold sl_def esl_def)
  apply (simp add: semilat_errI[OF semilat])
  done

lemma err_semilat_eslI [intro, simp]:
"\L. semilat L \ err_semilat(esl L)"
by(simp add: err_semilat_eslI_aux split_tupled_all)

lemma acc_err [simp, intro!]:  "acc r \ acc(le r)"
apply (unfold acc_def lesub_def le_def lesssub_def)
apply (simp add: wf_eq_minimal split: err.split)
apply clarify
apply (case_tac "Err \ Q")
apply blast
apply (erule_tac x = "{a . OK a \ Q}" in allE)
apply (case_tac "x")
apply fast
apply blast
done

lemma Err_in_err [iff]: "Err \ err A"
  by (simp add: err_def)

lemma Ok_in_err [iff]: "(OK x \ err A) = (x\A)"
  by (auto simp add: err_def)

subsection \<open>lift\<close>

lemma lift_in_errI:
  "\ e \ err S; \x\S. e = OK x \ f x \ err S \ \ lift f e \ err S"
apply (unfold lift_def)
apply (simp split: err.split)
apply blast
done

lemma Err_lift2 [simp]:
  "Err +_(lift2 f) x = Err"
  by (simp add: lift2_def plussub_def)

lemma lift2_Err [simp]:
  "x +_(lift2 f) Err = Err"
  by (simp add: lift2_def plussub_def split: err.split)

lemma OK_lift2_OK [simp]:
  "OK x +_(lift2 f) OK y = x +_f y"
  by (simp add: lift2_def plussub_def split: err.split)

subsection \<open>sup\<close>

lemma Err_sup_Err [simp]:
  "Err +_(Err.sup f) x = Err"
  by (simp add: plussub_def Err.sup_def Err.lift2_def)

lemma Err_sup_Err2 [simp]:
  "x +_(Err.sup f) Err = Err"
  by (simp add: plussub_def Err.sup_def Err.lift2_def split: err.split)

lemma Err_sup_OK [simp]:
  "OK x +_(Err.sup f) OK y = OK(x +_f y)"
  by (simp add: plussub_def Err.sup_def Err.lift2_def)

lemma Err_sup_eq_OK_conv [iff]:
  "(Err.sup f ex ey = OK z) = (\x y. ex = OK x & ey = OK y & f x y = z)"
apply (unfold Err.sup_def lift2_def plussub_def)
apply (rule iffI)
apply (simp split: err.split_asm)
apply clarify
apply simp
done

lemma Err_sup_eq_Err [iff]:
  "(Err.sup f ex ey = Err) = (ex=Err | ey=Err)"
apply (unfold Err.sup_def lift2_def plussub_def)
apply (simp split: err.split)
done

subsection \<open>semilat (err A) (le r) f\<close>

lemma semilat_le_err_Err_plus [simp]:
  "\ x \ err A; semilat(err A, le r, f) \ \ Err +_f x = Err"
  by (blast intro: Semilat.le_iff_plus_unchanged [OF Semilat.intro, THEN iffD1]
                   Semilat.le_iff_plus_unchanged2 [OF Semilat.intro, THEN iffD1])

lemma semilat_le_err_plus_Err [simp]:
  "\ x \ err A; semilat(err A, le r, f) \ \ x +_f Err = Err"
  by (blast intro: Semilat.le_iff_plus_unchanged [OF Semilat.intro, THEN iffD1]
                   Semilat.le_iff_plus_unchanged2 [OF Semilat.intro, THEN iffD1])

lemma semilat_le_err_OK1:
  "\ x \ A; y \ A; semilat(err A, le r, f); OK x +_f OK y = OK z \
  \<Longrightarrow> x <=_r z"
apply (rule OK_le_err_OK [THEN iffD1])
apply (erule subst)
apply (simp add: Semilat.ub1 [OF Semilat.intro])
done

lemma semilat_le_err_OK2:
  "\ x \ A; y \ A; semilat(err A, le r, f); OK x +_f OK y = OK z \
  \<Longrightarrow> y <=_r z"
apply (rule OK_le_err_OK [THEN iffD1])
apply (erule subst)
apply (simp add: Semilat.ub2 [OF Semilat.intro])
done

lemma eq_order_le:
  "\ x=y; order r \ \ x <=_r y"
apply (unfold Semilat.order_def)
apply blast
done

lemma OK_plus_OK_eq_Err_conv [simp]:
  assumes "x \ A" and "y \ A" and "semilat(err A, le r, fe)"
  shows "((OK x) +_fe (OK y) = Err) = (\(\z\A. x <=_r z & y <=_r z))"
proof -
  have plus_le_conv3: "\A x y z f r.
    \<lbrakk> semilat (A,r,f); x +_f y <=_r z; x \<in> A; y \<in> A; z \<in> A \<rbrakk>
    \<Longrightarrow> x <=_r z \<and> y <=_r z"
    by (rule Semilat.plus_le_conv [OF Semilat.intro, THEN iffD1])
  from assms show ?thesis
  apply (rule_tac iffI)
   apply clarify
   apply (drule OK_le_err_OK [THEN iffD2])
   apply (drule OK_le_err_OK [THEN iffD2])
   apply (drule Semilat.lub [OF Semilat.intro, of _ _ _ "OK x" _ "OK y"])
        apply assumption
       apply assumption
      apply simp
     apply simp
    apply simp
   apply simp
  apply (case_tac "(OK x) +_fe (OK y)")
   apply assumption
  apply (rename_tac z)
  apply (subgoal_tac "OK z \ err A")
  apply (drule eq_order_le)
    apply (erule Semilat.orderI [OF Semilat.intro])
   apply (blast dest: plus_le_conv3)
  apply (erule subst)
  apply (blast intro: Semilat.closedI [OF Semilat.intro] closedD)
  done
qed

subsection \<open>semilat (err (Union AS))\<close>

(* FIXME? *)
lemma all_bex_swap_lemma [iff]:
  "(\x. (\y\A. x = f y) \ P x) = (\y\A. P(f y))"
  by blast

lemma closed_err_Union_lift2I:
  "\ \A\AS. closed (err A) (lift2 f); AS \ {};
      \<forall>A\<in>AS. \<forall>B\<in>AS. A\<noteq>B \<longrightarrow> (\<forall>a\<in>A. \<forall>b\<in>B. a +_f b = Err) \<rbrakk>
  \<Longrightarrow> closed (err (\<Union>AS)) (lift2 f)"
apply (unfold closed_def err_def)
apply simp
apply clarify
apply simp
apply fast
done

text \<open>
  If \<^term>\<open>AS = {}\<close> the thm collapses to
  \<^prop>\<open>order r & closed {Err} f & Err +_f Err = Err\<close>
  which may not hold
\<close>
lemma err_semilat_UnionI:
  "\ \A\AS. err_semilat(A, r, f); AS \ {};
      \<forall>A\<in>AS. \<forall>B\<in>AS. A\<noteq>B \<longrightarrow> (\<forall>a\<in>A. \<forall>b\<in>B. \<not> a <=_r b & a +_f b = Err) \<rbrakk>
  \<Longrightarrow> err_semilat (\<Union>AS, r, f)"
apply (unfold semilat_def sl_def)
apply (simp add: closed_err_Union_lift2I)
apply (rule conjI)
apply blast
apply (simp add: err_def)
apply (rule conjI)
apply clarify
apply (rename_tac A a u B b)
apply (case_tac "A = B")
  apply simp
apply simp
apply (rule conjI)
apply clarify
apply (rename_tac A a u B b)
apply (case_tac "A = B")
  apply simp
apply simp
apply clarify
apply (rename_tac A ya yb B yd z C c a b)
apply (case_tac "A = B")
apply (case_tac "A = C")
  apply simp
apply (rotate_tac -1)
apply simp
apply (rotate_tac -1)
apply (case_tac "B = C")
apply simp
apply (rotate_tac -1)
apply simp
done

end

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.