author | huffman |
Fri, 04 Jan 2008 00:01:02 +0100 | |
changeset 25827 | c2adeb1bae5c |
parent 25723 | 80c06e4d4db6 |
child 25920 | 8df5eabda5f6 |
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 |
|
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25723
diff
changeset
|
17 |
instance lift :: (finite) finite_po |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25723
diff
changeset
|
18 |
by (rule typedef_finite_po [OF type_definition_lift]) |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25723
diff
changeset
|
19 |
|
16748 | 20 |
lemmas inst_lift_pcpo = Abs_lift_strict [symmetric] |
12026 | 21 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
22 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
23 |
Def :: "'a \<Rightarrow> 'a lift" where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
24 |
"Def x = Abs_lift (up\<cdot>(Discr x))" |
12026 | 25 |
|
26 |
subsection {* Lift as a datatype *} |
|
27 |
||
16748 | 28 |
lemma lift_distinct1: "\<bottom> \<noteq> Def x" |
29 |
by (simp add: Def_def Abs_lift_inject lift_def inst_lift_pcpo) |
|
12026 | 30 |
|
16748 | 31 |
lemma lift_distinct2: "Def x \<noteq> \<bottom>" |
32 |
by (simp add: Def_def Abs_lift_inject lift_def inst_lift_pcpo) |
|
12026 | 33 |
|
16748 | 34 |
lemma Def_inject: "(Def x = Def y) = (x = y)" |
35 |
by (simp add: Def_def Abs_lift_inject lift_def) |
|
12026 | 36 |
|
16748 | 37 |
lemma lift_induct: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> P y" |
38 |
apply (induct y) |
|
16755
fd02f9d06e43
renamed upE1 to upE; added simp rule cont2cont_flift1
huffman
parents:
16749
diff
changeset
|
39 |
apply (rule_tac p=y in upE) |
16748 | 40 |
apply (simp add: Abs_lift_strict) |
41 |
apply (case_tac x) |
|
42 |
apply (simp add: Def_def) |
|
43 |
done |
|
12026 | 44 |
|
45 |
rep_datatype lift |
|
46 |
distinct lift_distinct1 lift_distinct2 |
|
47 |
inject Def_inject |
|
48 |
induction lift_induct |
|
49 |
||
16748 | 50 |
lemma Def_not_UU: "Def a \<noteq> UU" |
12026 | 51 |
by simp |
52 |
||
53 |
||
16748 | 54 |
text {* @{term UU} and @{term Def} *} |
12026 | 55 |
|
16748 | 56 |
lemma Lift_exhaust: "x = \<bottom> \<or> (\<exists>y. x = Def y)" |
12026 | 57 |
by (induct x) simp_all |
58 |
||
16748 | 59 |
lemma Lift_cases: "\<lbrakk>x = \<bottom> \<Longrightarrow> P; \<exists>a. x = Def a \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
12026 | 60 |
by (insert Lift_exhaust) blast |
61 |
||
16748 | 62 |
lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)" |
12026 | 63 |
by (cases x) simp_all |
64 |
||
16630
83bf468b1dc7
added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents:
16555
diff
changeset
|
65 |
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
|
66 |
by (cases x) simp_all |
83bf468b1dc7
added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents:
16555
diff
changeset
|
67 |
|
12026 | 68 |
text {* |
69 |
For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text |
|
70 |
x} by @{text "Def a"} in conclusion. *} |
|
71 |
||
16121 | 72 |
ML {* |
16630
83bf468b1dc7
added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents:
16555
diff
changeset
|
73 |
local val lift_definedE = thm "lift_definedE" |
12026 | 74 |
in val def_tac = SIMPSET' (fn ss => |
16630
83bf468b1dc7
added theorem lift_definedE; moved cont_if to Cont.thy
huffman
parents:
16555
diff
changeset
|
75 |
etac lift_definedE THEN' asm_simp_tac ss) |
12026 | 76 |
end; |
77 |
*} |
|
78 |
||
16748 | 79 |
lemma DefE: "Def x = \<bottom> \<Longrightarrow> R" |
80 |
by simp |
|
12026 | 81 |
|
16748 | 82 |
lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R" |
12026 | 83 |
by simp |
84 |
||
16748 | 85 |
lemma Def_inject_less_eq: "Def x \<sqsubseteq> Def y = (x = y)" |
86 |
by (simp add: less_lift_def Def_def Abs_lift_inverse lift_def) |
|
12026 | 87 |
|
16748 | 88 |
lemma Def_less_is_eq [simp]: "Def x \<sqsubseteq> y = (Def x = y)" |
89 |
apply (induct y) |
|
19440 | 90 |
apply simp |
16748 | 91 |
apply (simp add: Def_inject_less_eq) |
92 |
done |
|
12026 | 93 |
|
94 |
||
95 |
subsection {* Lift is flat *} |
|
96 |
||
16748 | 97 |
lemma less_lift: "(x::'a lift) \<sqsubseteq> y = (x = y \<or> x = \<bottom>)" |
98 |
by (induct x, simp_all) |
|
99 |
||
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12026
diff
changeset
|
100 |
instance lift :: (type) flat |
16748 | 101 |
by (intro_classes, simp add: less_lift) |
12026 | 102 |
|
103 |
text {* |
|
104 |
\medskip Two specific lemmas for the combination of LCF and HOL |
|
105 |
terms. |
|
106 |
*} |
|
107 |
||
16748 | 108 |
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
|
109 |
by (rule cont2cont_Rep_CFun [THEN cont2cont_fun]) |
12026 | 110 |
|
16748 | 111 |
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
|
112 |
by (rule cont_Rep_CFun_app [THEN cont2cont_fun]) |
2640 | 113 |
|
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
114 |
subsection {* Further operations *} |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
115 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
116 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
117 |
flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)" (binder "FLIFT " 10) where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
118 |
"flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))" |
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
119 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
120 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
121 |
flift2 :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a lift \<rightarrow> 'b lift)" where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
122 |
"flift2 f = (FLIFT x. Def (f x))" |
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
123 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
124 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
125 |
liftpair :: "'a lift \<times> 'b lift \<Rightarrow> ('a \<times> 'b) lift" where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19764
diff
changeset
|
126 |
"liftpair x = csplit\<cdot>(FLIFT x y. Def (x, y))\<cdot>x" |
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
127 |
|
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
128 |
subsection {* Continuity Proofs for flift1, flift2 *} |
12026 | 129 |
|
130 |
text {* Need the instance of @{text flat}. *} |
|
131 |
||
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
132 |
lemma cont_lift_case1: "cont (\<lambda>f. lift_case a f x)" |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
133 |
apply (induct x) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
134 |
apply simp |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
135 |
apply simp |
18092
2c5d5da79a1e
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
huffman
parents:
17612
diff
changeset
|
136 |
apply (rule cont_id [THEN cont2cont_fun]) |
16695
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 |
|
25723 | 139 |
lemma cont_lift_case2: "cont (\<lambda>x. lift_case \<bottom> f x)" |
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
140 |
apply (rule flatdom_strict2cont) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
141 |
apply simp |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
142 |
done |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
143 |
|
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
144 |
lemma cont_flift1: "cont flift1" |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
145 |
apply (unfold flift1_def) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
146 |
apply (rule cont2cont_LAM) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
147 |
apply (rule cont_lift_case2) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
148 |
apply (rule cont_lift_case1) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
149 |
done |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
150 |
|
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
151 |
lemma cont2cont_flift1: |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
152 |
"\<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
|
153 |
apply (rule cont_flift1 [THEN cont2cont_app3]) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
154 |
apply (simp add: cont2cont_lambda) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
155 |
done |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
156 |
|
16757
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset
|
157 |
lemma cont2cont_lift_case: |
25723 | 158 |
"\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case UU (f x) (g x))" |
16757
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset
|
159 |
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
|
160 |
apply (simp add: flift1_def cont_lift_case2) |
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset
|
161 |
apply (simp add: cont2cont_flift1) |
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset
|
162 |
done |
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset
|
163 |
|
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset
|
164 |
text {* rewrites for @{term flift1}, @{term flift2} *} |
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset
|
165 |
|
16695
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
166 |
lemma flift1_Def [simp]: "flift1 f\<cdot>(Def x) = (f x)" |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
167 |
by (simp add: flift1_def cont_lift_case2) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
168 |
|
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
169 |
lemma flift2_Def [simp]: "flift2 f\<cdot>(Def x) = Def (f x)" |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
170 |
by (simp add: flift2_def) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
171 |
|
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
172 |
lemma flift1_strict [simp]: "flift1 f\<cdot>\<bottom> = \<bottom>" |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
173 |
by (simp add: flift1_def cont_lift_case2) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
174 |
|
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
175 |
lemma flift2_strict [simp]: "flift2 f\<cdot>\<bottom> = \<bottom>" |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
176 |
by (simp add: flift2_def) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
177 |
|
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
178 |
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
|
179 |
by (erule lift_definedE, simp) |
dc8c868e910b
simplified definitions of flift1, flift2, liftpair;
huffman
parents:
16630
diff
changeset
|
180 |
|
19520 | 181 |
lemma flift2_defined_iff [simp]: "(flift2 f\<cdot>x = \<bottom>) = (x = \<bottom>)" |
182 |
by (cases x, simp_all) |
|
183 |
||
12026 | 184 |
text {* |
14096 | 185 |
\medskip Extension of @{text cont_tac} and installation of simplifier. |
12026 | 186 |
*} |
187 |
||
188 |
lemmas cont_lemmas_ext [simp] = |
|
16757
b8bfd086f7d4
replaced old continuity rules with new lemma cont2cont_lift_case
huffman
parents:
16755
diff
changeset
|
189 |
cont2cont_flift1 cont2cont_lift_case cont2cont_lambda |
12026 | 190 |
cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if |
191 |
||
16121 | 192 |
ML {* |
19764 | 193 |
local |
194 |
val cont_lemmas2 = thms "cont_lemmas1" @ thms "cont_lemmas_ext"; |
|
195 |
val flift1_def = thm "flift1_def"; |
|
196 |
in |
|
12026 | 197 |
|
198 |
fun cont_tac i = resolve_tac cont_lemmas2 i; |
|
199 |
fun cont_tacR i = REPEAT (cont_tac i); |
|
200 |
||
19764 | 201 |
fun cont_tacRs ss i = |
17612 | 202 |
simp_tac ss i THEN |
12026 | 203 |
REPEAT (cont_tac i) |
204 |
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
|
205 |
*} |
12026 | 206 |
|
2640 | 207 |
end |