Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Lift.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/HOLCF/Lift.thy
    Author:     Olaf Müller
*)

section \<open>Lifting types of class type to flat pcpo's\<close>

theory Lift
imports Discrete Up
begin

default_sort type

pcpodef 'a lift = "UNIV :: 'a discr u set"
by simp_all

lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]

definition
  Def :: "'a \ 'a lift" where
  "Def x = Abs_lift (up\(Discr x))"

subsection \<open>Lift as a datatype\<close>

lemma lift_induct: "\P \; \x. P (Def x)\ \ P y"
apply (induct y)
apply (rule_tac p=y in upE)
apply (simp add: Abs_lift_strict)
apply (case_tac x)
apply (simp add: Def_def)
done

old_rep_datatype "\::'a lift" Def
  by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo)

text \<open>\<^term>\<open>bottom\<close> and \<^term>\<open>Def\<close>\<close>

lemma not_Undef_is_Def: "(x \ \) = (\y. x = Def y)"
  by (cases x) simp_all

lemma lift_definedE: "\x \ \; \a. x = Def a \ R\ \ R"
  by (cases x) simp_all

text \<open>
  For \<^term>\<open>x ~= \<bottom>\<close> in assumptions \<open>defined\<close> replaces \<open>x\<close> by \<open>Def a\<close> in conclusion.\<close>

method_setup defined = \<open>
  Scan.succeed (fn ctxt => SIMPLE_METHOD'
    (eresolve_tac ctxt @{thms lift_definedE} THEN' asm_simp_tac ctxt))
\<close>

lemma DefE: "Def x = \ \ R"
  by simp

lemma DefE2: "\x = Def s; x = \\ \ R"
  by simp

lemma Def_below_Def: "Def x \ Def y \ x = y"
by (simp add: below_lift_def Def_def Abs_lift_inverse)

lemma Def_below_iff [simp]: "Def x \ y \ Def x = y"
by (induct y, simp, simp add: Def_below_Def)

subsection \<open>Lift is flat\<close>

instance lift :: (type) flat
proof
  fix x y :: "'a lift"
  assume "x \ y" thus "x = \ \ x = y"
    by (induct x) auto
qed

subsection \<open>Continuity of \<^const>\<open>case_lift\<close>\<close>

lemma case_lift_eq: "case_lift \ f x = fup\(\ y. f (undiscr y))\(Rep_lift x)"
apply (induct x, unfold lift.case)
apply (simp add: Rep_lift_strict)
apply (simp add: Def_def Abs_lift_inverse)
done

lemma cont2cont_case_lift [simp]:
  "\\y. cont (\x. f x y); cont g\ \ cont (\x. case_lift \ (f x) (g x))"
unfolding case_lift_eq by (simp add: cont_Rep_lift)

subsection \<open>Further operations\<close>

definition
  flift1 :: "('a \ 'b::pcpo) \ ('a lift \ 'b)" (binder "FLIFT " 10) where
  "flift1 = (\f. (\ x. case_lift \ f x))"

translations
  "\(XCONST Def x). t" => "CONST flift1 (\x. t)"
  "\(CONST Def x). FLIFT y. t" <= "FLIFT x y. t"
  "\(CONST Def x). t" <= "FLIFT x. t"

definition
  flift2 :: "('a \ 'b) \ ('a lift \ 'b lift)" where
  "flift2 f = (FLIFT x. Def (f x))"

lemma flift1_Def [simp]: "flift1 f\(Def x) = (f x)"
by (simp add: flift1_def)

lemma flift2_Def [simp]: "flift2 f\(Def x) = Def (f x)"
by (simp add: flift2_def)

lemma flift1_strict [simp]: "flift1 f\\ = \"
by (simp add: flift1_def)

lemma flift2_strict [simp]: "flift2 f\\ = \"
by (simp add: flift2_def)

lemma flift2_defined [simp]: "x \ \ \ (flift2 f)\x \ \"
by (erule lift_definedE, simp)

lemma flift2_bottom_iff [simp]: "(flift2 f\x = \) = (x = \)"
by (cases x, simp_all)

lemma FLIFT_mono:
  "(\x. f x \ g x) \ (FLIFT x. f x) \ (FLIFT x. g x)"
by (rule cfun_belowI, case_tac x, simp_all)

lemma cont2cont_flift1 [simp, cont2cont]:
  "\\y. cont (\x. f x y)\ \ cont (\x. FLIFT y. f x y)"
by (simp add: flift1_def cont2cont_LAM)

end

¤ Dauer der Verarbeitung: 0.15 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.