author | aspinall |
Wed, 13 Jul 2005 20:07:01 +0200 | |
changeset 16821 | ba1f6aba44ed |
parent 16757 | b8bfd086f7d4 |
child 17612 | 5b37787d2d9e |
permissions | -rw-r--r-- |
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) |
|
87 |
apply (simp add: eq_UU_iff) |
|
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)" |
106 |
by (rule cont2cont_Rep_CFun [THEN cont2cont_CF1L]) |
|
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)" |
109 |
by (rule cont_Rep_CFun_app [THEN cont2cont_CF1L]) |
|
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 |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
131 |
apply (rule cont_id [THEN cont2cont_CF1L]) |
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 |
|
12026 | 176 |
text {* |
14096 | 177 |
\medskip Extension of @{text cont_tac} and installation of simplifier. |
12026 | 178 |
*} |
179 |
||
180 |
lemmas cont_lemmas_ext [simp] = |
|
16757
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset
|
181 |
cont2cont_flift1 cont2cont_lift_case cont2cont_lambda |
12026 | 182 |
cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if |
183 |
||
16121 | 184 |
ML {* |
12026 | 185 |
val cont_lemmas2 = cont_lemmas1 @ thms "cont_lemmas_ext"; |
186 |
||
187 |
fun cont_tac i = resolve_tac cont_lemmas2 i; |
|
188 |
fun cont_tacR i = REPEAT (cont_tac i); |
|
189 |
||
16749 | 190 |
local val flift1_def = thm "flift1_def" |
12026 | 191 |
in fun cont_tacRs i = |
16757
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset
|
192 |
simp_tac (simpset()) i THEN |
12026 | 193 |
REPEAT (cont_tac i) |
194 |
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
|
195 |
*} |
12026 | 196 |
|
2640 | 197 |
end |