author | mueller |
Tue, 20 May 1997 16:02:36 +0200 | |
changeset 3250 | 9328e9ebe325 |
parent 3041 | bdd21deed6ea |
child 3324 | 6b26b886ff69 |
permissions | -rw-r--r-- |
2357 | 1 |
(* Title: HOLCF/Lift3.ML |
2 |
ID: $Id$ |
|
3035 | 3 |
Author: Olaf Mueller |
2357 | 4 |
Copyright 1996 Technische Universitaet Muenchen |
5 |
||
6 |
Theorems for Lift3.thy |
|
7 |
*) |
|
8 |
||
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
9 |
|
2640 | 10 |
(* for compatibility with old HOLCF-Version *) |
11 |
qed_goal "inst_lift_pcpo" thy "UU = Undef" |
|
12 |
(fn prems => |
|
13 |
[ |
|
14 |
(simp_tac (HOL_ss addsimps [UU_def,UU_lift_def]) 1) |
|
15 |
]); |
|
16 |
||
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
17 |
(* ----------------------------------------------------------- *) |
3035 | 18 |
(* In lift.simps Undef is replaced by UU *) |
19 |
(* Undef should be invisible from now on *) |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
20 |
(* ----------------------------------------------------------- *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
21 |
|
3035 | 22 |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
23 |
Addsimps [inst_lift_pcpo]; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
24 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
25 |
local |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
26 |
|
3035 | 27 |
val case1' = prove_goal thy "lift_case f1 f2 UU = f1" |
3041 | 28 |
(fn _ => [simp_tac (!simpset addsimps lift.simps) 1]); |
3035 | 29 |
val case2' = prove_goal thy "lift_case f1 f2 (Def a) = f2 a" |
3041 | 30 |
(fn _ => [Simp_tac 1]); |
3035 | 31 |
val distinct1' = prove_goal thy "UU ~= Def a" |
3041 | 32 |
(fn _ => [Simp_tac 1]); |
3035 | 33 |
val distinct2' = prove_goal thy "Def a ~= UU" |
3041 | 34 |
(fn _ => [Simp_tac 1]); |
3035 | 35 |
val inject' = prove_goal thy "Def a = Def aa = (a = aa)" |
3041 | 36 |
(fn _ => [Simp_tac 1]); |
3035 | 37 |
val rec1' = prove_goal thy "lift_rec f1 f2 UU = f1" |
3041 | 38 |
(fn _ => [Simp_tac 1]); |
3035 | 39 |
val rec2' = prove_goal thy "lift_rec f1 f2 (Def a) = f2 a" |
3041 | 40 |
(fn _ => [Simp_tac 1]); |
3035 | 41 |
val induct' = prove_goal thy "[| P UU; !a. P (Def a) |] ==> P lift" |
3041 | 42 |
(fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1, |
43 |
etac Lift1.lift.induct 1,fast_tac HOL_cs 1]); |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
44 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
45 |
in |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
46 |
|
3035 | 47 |
val Def_not_UU = distinct2'; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
48 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
49 |
structure lift = |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
50 |
struct |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
51 |
val cases = [case1',case2']; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
52 |
val distinct = [distinct1',distinct2']; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
53 |
val inject = [inject']; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
54 |
val induct = allI RSN(2,induct'); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
55 |
val recs = [rec1',rec2']; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
56 |
val simps = cases@distinct@inject@recs; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
57 |
fun induct_tac (s:string) (i:int) = |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
58 |
(res_inst_tac [("lift",s)] induct i); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
59 |
end; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
60 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
61 |
end; (* local *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
62 |
|
3250 | 63 |
Delsimps Lift1.lift.simps; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
64 |
Delsimps [inst_lift_pcpo]; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
65 |
Addsimps [inst_lift_pcpo RS sym]; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
66 |
Addsimps lift.simps; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
67 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
68 |
|
3035 | 69 |
(* --------------------------------------------------------*) |
70 |
section"less_lift"; |
|
71 |
(* --------------------------------------------------------*) |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
72 |
|
3035 | 73 |
goal thy "(x::'a lift) << y = (x=y | x=UU)"; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
74 |
br (inst_lift_po RS ssubst) 1; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
75 |
by (Simp_tac 1); |
3035 | 76 |
qed"less_lift"; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
77 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
78 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
79 |
(* ---------------------------------------------------------- *) |
3035 | 80 |
section"UU and Def"; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
81 |
(* ---------------------------------------------------------- *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
82 |
|
3035 | 83 |
goal thy "x=UU | (? y.x=Def y)"; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
84 |
by (lift.induct_tac "x" 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
85 |
by (Asm_simp_tac 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
86 |
by (rtac disjI2 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
87 |
by (rtac exI 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
88 |
by (Asm_simp_tac 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
89 |
qed"Lift_exhaust"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
90 |
|
3035 | 91 |
val prems = goal thy |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
92 |
"[| x = UU ==> P; ? a. x = Def a ==> P |] ==> P"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
93 |
by (cut_facts_tac [Lift_exhaust] 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
94 |
by (fast_tac (HOL_cs addSEs prems) 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
95 |
qed"Lift_cases"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
96 |
|
2841
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2648
diff
changeset
|
97 |
goal thy |
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2648
diff
changeset
|
98 |
"P(lift_case a b x) = ((x=UU --> P a) & (!y. x = Def y --> P(b y)))"; |
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2648
diff
changeset
|
99 |
by(lift.induct_tac "x" 1); |
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2648
diff
changeset
|
100 |
by(ALLGOALS Asm_simp_tac); |
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2648
diff
changeset
|
101 |
qed "expand_lift_case"; |
c2508f4ab739
Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
2648
diff
changeset
|
102 |
|
3035 | 103 |
goal thy "(x~=UU)=(? y.x=Def y)"; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
104 |
br iffI 1; |
3035 | 105 |
br Lift_cases 1; |
106 |
by (REPEAT (fast_tac (HOL_cs addSIs lift.distinct) 1)); |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
107 |
qed"not_Undef_is_Def"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
108 |
|
3035 | 109 |
(* For x~=UU in assumptions def_tac replaces x by (Def a) in conclusion *) |
110 |
val def_tac = etac (not_Undef_is_Def RS iffD1 RS exE) THEN' Asm_simp_tac; |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
111 |
|
3035 | 112 |
bind_thm("Undef_eq_UU", inst_lift_pcpo RS sym); |
113 |
||
114 |
val DefE = prove_goal thy "Def x = UU ==> R" |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
115 |
(fn prems => [ |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
116 |
cut_facts_tac prems 1, |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
117 |
asm_full_simp_tac (HOL_ss addsimps [Def_not_UU]) 1]); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
118 |
|
3035 | 119 |
val prems = goal thy "[| x = Def s; x = UU |] ==> R"; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
120 |
by (cut_facts_tac prems 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
121 |
by (fast_tac (HOL_cs addSDs [DefE]) 1); |
3035 | 122 |
qed"DefE2"; |
123 |
||
124 |
goal thy "Def x << Def y = (x = y)"; |
|
125 |
by (stac (hd lift.inject RS sym) 1); |
|
126 |
back(); |
|
127 |
by (rtac iffI 1); |
|
128 |
by (asm_full_simp_tac (!simpset addsimps [inst_lift_po] ) 1); |
|
129 |
be (antisym_less_inverse RS conjunct1) 1; |
|
130 |
qed"Def_inject_less_eq"; |
|
131 |
||
132 |
goal thy "Def x << y = (Def x = y)"; |
|
133 |
by (simp_tac (!simpset addsimps [less_lift]) 1); |
|
134 |
qed"Def_less_is_eq"; |
|
135 |
||
136 |
Addsimps [Def_less_is_eq]; |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
137 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
138 |
(* ---------------------------------------------------------- *) |
3035 | 139 |
section"Lift is flat"; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
140 |
(* ---------------------------------------------------------- *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
141 |
|
3035 | 142 |
goalw thy [flat_def] "flat (x::'a lift)"; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
143 |
by (simp_tac (!simpset addsimps [less_lift]) 1); |
3035 | 144 |
qed"flat_lift"; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
145 |
|
2640 | 146 |
bind_thm("ax_flat_lift",flat_lift RS flatE); |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
147 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
148 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
149 |
(* ---------------------------------------------------------- *) |
3035 | 150 |
section"Continuity Proofs for flift1, flift2, if"; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
151 |
(* ---------------------------------------------------------- *) |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
152 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
153 |
|
3035 | 154 |
(* flift1 is continuous in its argument itself*) |
155 |
||
156 |
goal thy "cont (lift_case UU f)"; |
|
157 |
br flatdom_strict2cont 1; |
|
158 |
br flat_lift 1; |
|
159 |
by (Simp_tac 1); |
|
160 |
qed"cont_flift1_arg"; |
|
161 |
||
162 |
(* flift1 is continuous in a variable that occurs only |
|
163 |
in the Def branch *) |
|
164 |
||
165 |
goal thy "!!f. [| !! a.cont (%y. (f y) a) |] ==> \ |
|
166 |
\ cont (%y. lift_case UU (f y))"; |
|
167 |
br cont2cont_CF1L_rev 1; |
|
168 |
by (strip_tac 1); |
|
169 |
by (res_inst_tac [("x","y")] Lift_cases 1); |
|
170 |
by (Asm_simp_tac 1); |
|
171 |
by (fast_tac (HOL_cs addss !simpset) 1); |
|
172 |
qed"cont_flift1_not_arg"; |
|
173 |
||
174 |
(* flift1 is continuous in a variable that occurs either |
|
175 |
in the Def branch or in the argument *) |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
176 |
|
3035 | 177 |
goal thy "!!f. [| !! a.cont (%y. (f y) a); cont g|] ==> \ |
178 |
\ cont (%y. lift_case UU (f y) (g y))"; |
|
179 |
br cont2cont_app 1; |
|
180 |
back(); |
|
181 |
by (safe_tac set_cs); |
|
182 |
br cont_flift1_not_arg 1; |
|
183 |
auto(); |
|
184 |
br cont_flift1_arg 1; |
|
185 |
qed"cont_flift1_arg_and_not_arg"; |
|
186 |
||
187 |
(* flift2 is continuous in its argument itself *) |
|
188 |
||
189 |
goal thy "cont (lift_case UU (%y. Def (f y)))"; |
|
190 |
br flatdom_strict2cont 1; |
|
191 |
br flat_lift 1; |
|
192 |
by (Simp_tac 1); |
|
193 |
qed"cont_flift2_arg"; |
|
194 |
||
195 |
(* Two specific lemmas for the combination of LCF and HOL terms *) |
|
196 |
||
197 |
goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)"; |
|
198 |
br cont2cont_CF1L 1; |
|
199 |
by (REPEAT (resolve_tac cont_lemmas1 1)); |
|
200 |
auto(); |
|
201 |
qed"cont_fapp_app"; |
|
202 |
||
203 |
goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)"; |
|
204 |
br cont2cont_CF1L 1; |
|
205 |
be cont_fapp_app 1; |
|
206 |
ba 1; |
|
207 |
qed"cont_fapp_app_app"; |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
208 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
209 |
|
3035 | 210 |
(* continuity of if then else *) |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
211 |
|
3035 | 212 |
val prems = goal thy "[| cont f1; cont f2 |] ==> \ |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
213 |
\ cont (%x. if b then f1 x else f2 x)"; |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
214 |
by (cut_facts_tac prems 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
215 |
by (case_tac "b" 1); |
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
216 |
by (TRYALL (fast_tac (HOL_cs addss HOL_ss))); |
3035 | 217 |
qed"cont_if"; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
218 |
|
3035 | 219 |
|
220 |
(* ---------------------------------------------------------- *) |
|
221 |
(* Extension of cont_tac and installation of simplifier *) |
|
222 |
(* ---------------------------------------------------------- *) |
|
223 |
||
224 |
bind_thm("cont2cont_CF1L_rev2",allI RS cont2cont_CF1L_rev); |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
225 |
|
3035 | 226 |
val cont_lemmas_ext = [cont_flift1_arg,cont_flift2_arg, |
227 |
cont_flift1_arg_and_not_arg,cont2cont_CF1L_rev2, |
|
228 |
cont_fapp_app,cont_fapp_app_app,cont_if]; |
|
229 |
||
230 |
val cont_lemmas2 = cont_lemmas1 @ cont_lemmas_ext; |
|
3041 | 231 |
|
232 |
Addsimps cont_lemmas_ext; |
|
3035 | 233 |
|
234 |
fun cont_tac i = resolve_tac cont_lemmas2 i; |
|
235 |
fun cont_tacR i = REPEAT (cont_tac i); |
|
236 |
||
237 |
fun cont_tacRs i = simp_tac (!simpset addsimps [flift1_def,flift2_def]) i THEN |
|
3041 | 238 |
REPEAT (cont_tac i); |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
239 |
|
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
240 |
|
3035 | 241 |
simpset := !simpset addSolver (K (DEPTH_SOLVE_1 o cont_tac)); |
242 |
||
243 |
(* ---------------------------------------------------------- *) |
|
244 |
section"flift1, flift2"; |
|
245 |
(* ---------------------------------------------------------- *) |
|
246 |
||
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
247 |
|
3035 | 248 |
goal thy "flift1 f`(Def x) = (f x)"; |
249 |
by (simp_tac (!simpset addsimps [flift1_def]) 1); |
|
250 |
qed"flift1_Def"; |
|
251 |
||
252 |
goal thy "flift2 f`(Def x) = Def (f x)"; |
|
253 |
by (simp_tac (!simpset addsimps [flift2_def]) 1); |
|
254 |
qed"flift2_Def"; |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
255 |
|
3035 | 256 |
goal thy "flift1 f`UU = UU"; |
257 |
by (simp_tac (!simpset addsimps [flift1_def]) 1); |
|
258 |
qed"flift1_UU"; |
|
259 |
||
260 |
goal thy "flift2 f`UU = UU"; |
|
261 |
by (simp_tac (!simpset addsimps [flift2_def]) 1); |
|
262 |
qed"flift2_UU"; |
|
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
263 |
|
3035 | 264 |
Addsimps [flift1_Def,flift2_Def,flift1_UU,flift2_UU]; |
2356
125260ef480c
Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
sandnerr
parents:
diff
changeset
|
265 |
|
3035 | 266 |
goal thy "!!x. x~=UU ==> (flift2 f)`x~=UU"; |
267 |
by (def_tac 1); |
|
268 |
qed"flift2_nUU"; |
|
269 |
||
270 |
Addsimps [flift2_nUU]; |
|
271 |
||
272 |