author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 19764  372065f34795 
child 25131  2c8caac48ade 
permissions  rwrr 
2640  1 
(* Title: HOLCF/Lift.thy 
2 
ID: $Id$ 

12026  3 
Author: Olaf Mueller 
2640  4 
*) 
5 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12026
diff
changeset

6 
header {* Lifting types of class type to flat pcpo's *} 
12026  7 

15577  8 
theory Lift 
16748  9 
imports Discrete Up Cprod 
15577  10 
begin 
12026  11 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12026
diff
changeset

12 
defaultsort type 
12026  13 

16748  14 
pcpodef 'a lift = "UNIV :: 'a discr u set" 
15 
by simp 

12026  16 

16748  17 
lemmas inst_lift_pcpo = Abs_lift_strict [symmetric] 
12026  18 

19 
constdefs 

16748  20 
Def :: "'a \<Rightarrow> 'a lift" 
21 
"Def x \<equiv> Abs_lift (up\<cdot>(Discr x))" 

12026  22 

23 
subsection {* Lift as a datatype *} 

24 

16748  25 
lemma lift_distinct1: "\<bottom> \<noteq> Def x" 
26 
by (simp add: Def_def Abs_lift_inject lift_def inst_lift_pcpo) 

12026  27 

16748  28 
lemma lift_distinct2: "Def x \<noteq> \<bottom>" 
29 
by (simp add: Def_def Abs_lift_inject lift_def inst_lift_pcpo) 

12026  30 

16748  31 
lemma Def_inject: "(Def x = Def y) = (x = y)" 
32 
by (simp add: Def_def Abs_lift_inject lift_def) 

12026  33 

16748  34 
lemma lift_induct: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> P y" 
35 
apply (induct y) 

16755
fd02f9d06e43
renamed upE1 to upE; added simp rule cont2cont_flift1
huffman
parents:
16749
diff
changeset

36 
apply (rule_tac p=y in upE) 
16748  37 
apply (simp add: Abs_lift_strict) 
38 
apply (case_tac x) 

39 
apply (simp add: Def_def) 

40 
done 

12026  41 

42 
rep_datatype lift 

43 
distinct lift_distinct1 lift_distinct2 

44 
inject Def_inject 

45 
induction lift_induct 

46 

16748  47 
lemma Def_not_UU: "Def a \<noteq> UU" 
12026  48 
by simp 
49 

50 

16748  51 
text {* @{term UU} and @{term Def} *} 
12026  52 

16748  53 
lemma Lift_exhaust: "x = \<bottom> \<or> (\<exists>y. x = Def y)" 
12026  54 
by (induct x) simp_all 
55 

16748  56 
lemma Lift_cases: "\<lbrakk>x = \<bottom> \<Longrightarrow> P; \<exists>a. x = Def a \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 
12026  57 
by (insert Lift_exhaust) blast 
58 

16748  59 
lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)" 
12026  60 
by (cases x) simp_all 
61 

16630
83bf468b1dc7
added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents:
16555
diff
changeset

62 
lemma lift_definedE: "\<lbrakk>x \<noteq> \<bottom>; \<And>a. x = Def a \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 
83bf468b1dc7
added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents:
16555
diff
changeset

63 
by (cases x) simp_all 
83bf468b1dc7
added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents:
16555
diff
changeset

64 

12026  65 
text {* 
66 
For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text 

67 
x} by @{text "Def a"} in conclusion. *} 

68 

16121  69 
ML {* 
16630
83bf468b1dc7
added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents:
16555
diff
changeset

70 
local val lift_definedE = thm "lift_definedE" 
12026  71 
in val def_tac = SIMPSET' (fn ss => 
16630
83bf468b1dc7
added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents:
16555
diff
changeset

72 
etac lift_definedE THEN' asm_simp_tac ss) 
12026  73 
end; 
74 
*} 

75 

16748  76 
lemma DefE: "Def x = \<bottom> \<Longrightarrow> R" 
77 
by simp 

12026  78 

16748  79 
lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R" 
12026  80 
by simp 
81 

16748  82 
lemma Def_inject_less_eq: "Def x \<sqsubseteq> Def y = (x = y)" 
83 
by (simp add: less_lift_def Def_def Abs_lift_inverse lift_def) 

12026  84 

16748  85 
lemma Def_less_is_eq [simp]: "Def x \<sqsubseteq> y = (Def x = y)" 
86 
apply (induct y) 

19440  87 
apply simp 
16748  88 
apply (simp add: Def_inject_less_eq) 
89 
done 

12026  90 

91 

92 
subsection {* Lift is flat *} 

93 

16748  94 
lemma less_lift: "(x::'a lift) \<sqsubseteq> y = (x = y \<or> x = \<bottom>)" 
95 
by (induct x, simp_all) 

96 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12026
diff
changeset

97 
instance lift :: (type) flat 
16748  98 
by (intro_classes, simp add: less_lift) 
12026  99 

100 
text {* 

101 
\medskip Two specific lemmas for the combination of LCF and HOL 

102 
terms. 

103 
*} 

104 

16748  105 
lemma cont_Rep_CFun_app: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s)" 
18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
17612
diff
changeset

106 
by (rule cont2cont_Rep_CFun [THEN cont2cont_fun]) 
12026  107 

16748  108 
lemma cont_Rep_CFun_app_app: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s t)" 
18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
17612
diff
changeset

109 
by (rule cont_Rep_CFun_app [THEN cont2cont_fun]) 
2640  110 

16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

111 
subsection {* Further operations *} 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

112 

dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

113 
constdefs 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

114 
flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)" (binder "FLIFT " 10) 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

115 
"flift1 \<equiv> \<lambda>f. (\<Lambda> x. lift_case \<bottom> f x)" 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

116 

dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

117 
flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

118 
"flift2 f \<equiv> FLIFT x. Def (f x)" 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

119 

dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

120 
liftpair :: "'a lift \<times> 'b lift \<Rightarrow> ('a \<times> 'b) lift" 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

121 
"liftpair x \<equiv> csplit\<cdot>(FLIFT x y. Def (x, y))\<cdot>x" 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

122 

dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

123 
subsection {* Continuity Proofs for flift1, flift2 *} 
12026  124 

125 
text {* Need the instance of @{text flat}. *} 

126 

16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

127 
lemma cont_lift_case1: "cont (\<lambda>f. lift_case a f x)" 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

128 
apply (induct x) 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

129 
apply simp 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

130 
apply simp 
18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
17612
diff
changeset

131 
apply (rule cont_id [THEN cont2cont_fun]) 
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

132 
done 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

133 

dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

134 
lemma cont_lift_case2: "cont (\<lambda>x. lift_case \<bottom> f x)" 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

135 
apply (rule flatdom_strict2cont) 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

136 
apply simp 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

137 
done 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

138 

dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

139 
lemma cont_flift1: "cont flift1" 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

140 
apply (unfold flift1_def) 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

141 
apply (rule cont2cont_LAM) 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

142 
apply (rule cont_lift_case2) 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

143 
apply (rule cont_lift_case1) 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

144 
done 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

145 

dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

146 
lemma cont2cont_flift1: 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

147 
"\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)" 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

148 
apply (rule cont_flift1 [THEN cont2cont_app3]) 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

149 
apply (simp add: cont2cont_lambda) 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

150 
done 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

151 

16757
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset

152 
lemma cont2cont_lift_case: 
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset

153 
"\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case UU (f x) (g x))" 
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset

154 
apply (subgoal_tac "cont (\<lambda>x. (FLIFT y. f x y)\<cdot>(g x))") 
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset

155 
apply (simp add: flift1_def cont_lift_case2) 
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset

156 
apply (simp add: cont2cont_flift1) 
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset

157 
done 
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset

158 

b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset

159 
text {* rewrites for @{term flift1}, @{term flift2} *} 
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset

160 

16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

161 
lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)" 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

162 
by (simp add: flift1_def cont_lift_case2) 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

163 

dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

164 
lemma flift2_Def [simp]: "flift2 f\<cdot>(Def x) = Def (f x)" 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

165 
by (simp add: flift2_def) 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

166 

dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

167 
lemma flift1_strict [simp]: "flift1 f\<cdot>\<bottom> = \<bottom>" 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

168 
by (simp add: flift1_def cont_lift_case2) 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

169 

dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

170 
lemma flift2_strict [simp]: "flift2 f\<cdot>\<bottom> = \<bottom>" 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

171 
by (simp add: flift2_def) 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

172 

dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

173 
lemma flift2_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> (flift2 f)\<cdot>x \<noteq> \<bottom>" 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

174 
by (erule lift_definedE, simp) 
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset

175 

19520  176 
lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)" 
177 
by (cases x, simp_all) 

178 

12026  179 
text {* 
14096  180 
\medskip Extension of @{text cont_tac} and installation of simplifier. 
12026  181 
*} 
182 

183 
lemmas cont_lemmas_ext [simp] = 

16757
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset

184 
cont2cont_flift1 cont2cont_lift_case cont2cont_lambda 
12026  185 
cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if 
186 

16121  187 
ML {* 
19764  188 
local 
189 
val cont_lemmas2 = thms "cont_lemmas1" @ thms "cont_lemmas_ext"; 

190 
val flift1_def = thm "flift1_def"; 

191 
in 

12026  192 

193 
fun cont_tac i = resolve_tac cont_lemmas2 i; 

194 
fun cont_tacR i = REPEAT (cont_tac i); 

195 

19764  196 
fun cont_tacRs ss i = 
17612  197 
simp_tac ss i THEN 
12026  198 
REPEAT (cont_tac i) 
199 
end; 

15651
4b393520846e
Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used.
huffman
parents:
15577
diff
changeset

200 
*} 
12026  201 

2640  202 
end 