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