1(* Title: HOL/HOLCF/Lift.thy 2 Author: Olaf Mueller 3*) 4 5section \<open>Lifting types of class type to flat pcpo's\<close> 6 7theory Lift 8imports Discrete Up 9begin 10 11default_sort type 12 13pcpodef 'a lift = "UNIV :: 'a discr u set" 14by simp_all 15 16lemmas inst_lift_pcpo = Abs_lift_strict [symmetric] 17 18definition 19 Def :: "'a \<Rightarrow> 'a lift" where 20 "Def x = Abs_lift (up\<cdot>(Discr x))" 21 22subsection \<open>Lift as a datatype\<close> 23 24lemma lift_induct: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> P y" 25apply (induct y) 26apply (rule_tac p=y in upE) 27apply (simp add: Abs_lift_strict) 28apply (case_tac x) 29apply (simp add: Def_def) 30done 31 32old_rep_datatype "\<bottom>::'a lift" Def 33 by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo) 34 35text \<open>\<^term>\<open>bottom\<close> and \<^term>\<open>Def\<close>\<close> 36 37lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)" 38 by (cases x) simp_all 39 40lemma lift_definedE: "\<lbrakk>x \<noteq> \<bottom>; \<And>a. x = Def a \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 41 by (cases x) simp_all 42 43text \<open> 44 For \<^term>\<open>x ~= \<bottom>\<close> in assumptions \<open>defined\<close> replaces \<open>x\<close> by \<open>Def a\<close> in conclusion.\<close> 45 46method_setup defined = \<open> 47 Scan.succeed (fn ctxt => SIMPLE_METHOD' 48 (eresolve_tac ctxt @{thms lift_definedE} THEN' asm_simp_tac ctxt)) 49\<close> 50 51lemma DefE: "Def x = \<bottom> \<Longrightarrow> R" 52 by simp 53 54lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R" 55 by simp 56 57lemma Def_below_Def: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y" 58by (simp add: below_lift_def Def_def Abs_lift_inverse) 59 60lemma Def_below_iff [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y" 61by (induct y, simp, simp add: Def_below_Def) 62 63 64subsection \<open>Lift is flat\<close> 65 66instance lift :: (type) flat 67proof 68 fix x y :: "'a lift" 69 assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y" 70 by (induct x) auto 71qed 72 73subsection \<open>Continuity of \<^const>\<open>case_lift\<close>\<close> 74 75lemma case_lift_eq: "case_lift \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)" 76apply (induct x, unfold lift.case) 77apply (simp add: Rep_lift_strict) 78apply (simp add: Def_def Abs_lift_inverse) 79done 80 81lemma cont2cont_case_lift [simp]: 82 "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. case_lift \<bottom> (f x) (g x))" 83unfolding case_lift_eq by (simp add: cont_Rep_lift) 84 85subsection \<open>Further operations\<close> 86 87definition 88 flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)" (binder "FLIFT " 10) where 89 "flift1 = (\<lambda>f. (\<Lambda> x. case_lift \<bottom> f x))" 90 91translations 92 "\<Lambda>(XCONST Def x). t" => "CONST flift1 (\<lambda>x. t)" 93 "\<Lambda>(CONST Def x). FLIFT y. t" <= "FLIFT x y. t" 94 "\<Lambda>(CONST Def x). t" <= "FLIFT x. t" 95 96definition 97 flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where 98 "flift2 f = (FLIFT x. Def (f x))" 99 100lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)" 101by (simp add: flift1_def) 102 103lemma flift2_Def [simp]: "flift2 f\<cdot>(Def x) = Def (f x)" 104by (simp add: flift2_def) 105 106lemma flift1_strict [simp]: "flift1 f\<cdot>\<bottom> = \<bottom>" 107by (simp add: flift1_def) 108 109lemma flift2_strict [simp]: "flift2 f\<cdot>\<bottom> = \<bottom>" 110by (simp add: flift2_def) 111 112lemma flift2_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> (flift2 f)\<cdot>x \<noteq> \<bottom>" 113by (erule lift_definedE, simp) 114 115lemma flift2_bottom_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)" 116by (cases x, simp_all) 117 118lemma FLIFT_mono: 119 "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)" 120by (rule cfun_belowI, case_tac x, simp_all) 121 122lemma cont2cont_flift1 [simp, cont2cont]: 123 "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)" 124by (simp add: flift1_def cont2cont_LAM) 125 126end 127