0
|
1 |
theory QuotMain
|
6
|
2 |
imports QuotScript QuotList Prove
|
264
|
3 |
uses ("quotient_info.ML")
|
|
4 |
("quotient.ML")
|
277
|
5 |
("quotient_def.ML")
|
0
|
6 |
begin
|
|
7 |
|
|
8 |
locale QUOT_TYPE =
|
|
9 |
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
|
|
10 |
and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
|
|
11 |
and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
|
|
12 |
assumes equiv: "EQUIV R"
|
|
13 |
and rep_prop: "\<And>y. \<exists>x. Rep y = R x"
|
|
14 |
and rep_inverse: "\<And>x. Abs (Rep x) = x"
|
|
15 |
and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
|
|
16 |
and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
|
15
|
17 |
begin
|
0
|
18 |
|
|
19 |
definition
|
200
|
20 |
ABS::"'a \<Rightarrow> 'b"
|
|
21 |
where
|
0
|
22 |
"ABS x \<equiv> Abs (R x)"
|
|
23 |
|
|
24 |
definition
|
200
|
25 |
REP::"'b \<Rightarrow> 'a"
|
|
26 |
where
|
0
|
27 |
"REP a = Eps (Rep a)"
|
|
28 |
|
15
|
29 |
lemma lem9:
|
0
|
30 |
shows "R (Eps (R x)) = R x"
|
|
31 |
proof -
|
|
32 |
have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
|
|
33 |
then have "R x (Eps (R x))" by (rule someI)
|
15
|
34 |
then show "R (Eps (R x)) = R x"
|
0
|
35 |
using equiv unfolding EQUIV_def by simp
|
|
36 |
qed
|
|
37 |
|
|
38 |
theorem thm10:
|
24
|
39 |
shows "ABS (REP a) \<equiv> a"
|
|
40 |
apply (rule eq_reflection)
|
|
41 |
unfolding ABS_def REP_def
|
0
|
42 |
proof -
|
15
|
43 |
from rep_prop
|
0
|
44 |
obtain x where eq: "Rep a = R x" by auto
|
|
45 |
have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
|
|
46 |
also have "\<dots> = Abs (R x)" using lem9 by simp
|
|
47 |
also have "\<dots> = Abs (Rep a)" using eq by simp
|
|
48 |
also have "\<dots> = a" using rep_inverse by simp
|
|
49 |
finally
|
|
50 |
show "Abs (R (Eps (Rep a))) = a" by simp
|
|
51 |
qed
|
|
52 |
|
15
|
53 |
lemma REP_refl:
|
0
|
54 |
shows "R (REP a) (REP a)"
|
|
55 |
unfolding REP_def
|
|
56 |
by (simp add: equiv[simplified EQUIV_def])
|
|
57 |
|
|
58 |
lemma lem7:
|
22
|
59 |
shows "(R x = R y) = (Abs (R x) = Abs (R y))"
|
0
|
60 |
apply(rule iffI)
|
|
61 |
apply(simp)
|
|
62 |
apply(drule rep_inject[THEN iffD2])
|
|
63 |
apply(simp add: abs_inverse)
|
|
64 |
done
|
15
|
65 |
|
0
|
66 |
theorem thm11:
|
|
67 |
shows "R r r' = (ABS r = ABS r')"
|
|
68 |
unfolding ABS_def
|
|
69 |
by (simp only: equiv[simplified EQUIV_def] lem7)
|
|
70 |
|
4
|
71 |
|
2
|
72 |
lemma REP_ABS_rsp:
|
4
|
73 |
shows "R f (REP (ABS g)) = R f g"
|
|
74 |
and "R (REP (ABS g)) f = R g f"
|
23
|
75 |
by (simp_all add: thm10 thm11)
|
4
|
76 |
|
0
|
77 |
lemma QUOTIENT:
|
|
78 |
"QUOTIENT R ABS REP"
|
|
79 |
apply(unfold QUOTIENT_def)
|
|
80 |
apply(simp add: thm10)
|
|
81 |
apply(simp add: REP_refl)
|
|
82 |
apply(subst thm11[symmetric])
|
|
83 |
apply(simp add: equiv[simplified EQUIV_def])
|
|
84 |
done
|
|
85 |
|
21
|
86 |
lemma R_trans:
|
49
|
87 |
assumes ab: "R a b"
|
|
88 |
and bc: "R b c"
|
22
|
89 |
shows "R a c"
|
21
|
90 |
proof -
|
|
91 |
have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
|
|
92 |
moreover have ab: "R a b" by fact
|
|
93 |
moreover have bc: "R b c" by fact
|
22
|
94 |
ultimately show "R a c" unfolding TRANS_def by blast
|
21
|
95 |
qed
|
|
96 |
|
|
97 |
lemma R_sym:
|
49
|
98 |
assumes ab: "R a b"
|
22
|
99 |
shows "R b a"
|
21
|
100 |
proof -
|
|
101 |
have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
|
22
|
102 |
then show "R b a" using ab unfolding SYM_def by blast
|
21
|
103 |
qed
|
|
104 |
|
49
|
105 |
lemma R_trans2:
|
|
106 |
assumes ac: "R a c"
|
22
|
107 |
and bd: "R b d"
|
21
|
108 |
shows "R a b = R c d"
|
200
|
109 |
using ac bd
|
|
110 |
by (blast intro: R_trans R_sym)
|
21
|
111 |
|
|
112 |
lemma REPS_same:
|
25
|
113 |
shows "R (REP a) (REP b) \<equiv> (a = b)"
|
38
|
114 |
proof -
|
|
115 |
have "R (REP a) (REP b) = (a = b)"
|
|
116 |
proof
|
|
117 |
assume as: "R (REP a) (REP b)"
|
|
118 |
from rep_prop
|
|
119 |
obtain x y
|
|
120 |
where eqs: "Rep a = R x" "Rep b = R y" by blast
|
|
121 |
from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
|
|
122 |
then have "R x (Eps (R y))" using lem9 by simp
|
|
123 |
then have "R (Eps (R y)) x" using R_sym by blast
|
|
124 |
then have "R y x" using lem9 by simp
|
|
125 |
then have "R x y" using R_sym by blast
|
|
126 |
then have "ABS x = ABS y" using thm11 by simp
|
|
127 |
then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
|
|
128 |
then show "a = b" using rep_inverse by simp
|
|
129 |
next
|
|
130 |
assume ab: "a = b"
|
|
131 |
have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
|
|
132 |
then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto
|
|
133 |
qed
|
|
134 |
then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
|
21
|
135 |
qed
|
|
136 |
|
0
|
137 |
end
|
|
138 |
|
|
139 |
section {* type definition for the quotient type *}
|
|
140 |
|
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
141 |
(* the auxiliary data for the quotient types *)
|
264
|
142 |
use "quotient_info.ML"
|
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
143 |
|
185
|
144 |
declare [[map list = (map, LIST_REL)]]
|
|
145 |
declare [[map * = (prod_fun, prod_rel)]]
|
|
146 |
declare [[map "fun" = (fun_map, FUN_REL)]]
|
|
147 |
|
|
148 |
ML {* maps_lookup @{theory} "List.list" *}
|
|
149 |
ML {* maps_lookup @{theory} "*" *}
|
|
150 |
ML {* maps_lookup @{theory} "fun" *}
|
174
|
151 |
|
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
152 |
|
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
153 |
(* definition of the quotient types *)
|
277
|
154 |
(* FIXME: should be called quotient_typ.ML *)
|
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
155 |
use "quotient.ML"
|
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
156 |
|
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
157 |
|
277
|
158 |
(* lifting of constants *)
|
|
159 |
use "quotient_def.ML"
|
|
160 |
|
381
|
161 |
(* TODO: Consider defining it with an "if"; sth like:
|
|
162 |
Babs p m = \<lambda>x. if x \<in> p then m x else undefined
|
|
163 |
*)
|
|
164 |
definition
|
|
165 |
Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
|
|
166 |
where
|
|
167 |
"(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
168 |
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
169 |
|
139
|
170 |
section {* ATOMIZE *}
|
|
171 |
|
381
|
172 |
lemma atomize_eqv[atomize]:
|
|
173 |
shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
|
139
|
174 |
proof
|
381
|
175 |
assume "A \<equiv> B"
|
139
|
176 |
then show "Trueprop A \<equiv> Trueprop B" by unfold
|
|
177 |
next
|
|
178 |
assume *: "Trueprop A \<equiv> Trueprop B"
|
|
179 |
have "A = B"
|
|
180 |
proof (cases A)
|
|
181 |
case True
|
|
182 |
have "A" by fact
|
|
183 |
then show "A = B" using * by simp
|
|
184 |
next
|
|
185 |
case False
|
|
186 |
have "\<not>A" by fact
|
|
187 |
then show "A = B" using * by auto
|
|
188 |
qed
|
|
189 |
then show "A \<equiv> B" by (rule eq_reflection)
|
|
190 |
qed
|
|
191 |
|
|
192 |
ML {*
|
|
193 |
fun atomize_thm thm =
|
|
194 |
let
|
221
|
195 |
val thm' = Thm.freezeT (forall_intr_vars thm)
|
139
|
196 |
val thm'' = ObjectLogic.atomize (cprop_of thm')
|
|
197 |
in
|
221
|
198 |
@{thm Pure.equal_elim_rule1} OF [thm'', thm']
|
139
|
199 |
end
|
|
200 |
*}
|
|
201 |
|
140
|
202 |
ML {* atomize_thm @{thm list.induct} *}
|
139
|
203 |
|
387
|
204 |
section {* infrastructure about id *}
|
381
|
205 |
|
|
206 |
(* Need to have a meta-equality *)
|
|
207 |
lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
|
|
208 |
by (simp add: id_def)
|
|
209 |
(* TODO: can be also obtained with: *)
|
|
210 |
ML {* symmetric (eq_reflection OF @{thms id_def}) *}
|
|
211 |
|
|
212 |
lemma prod_fun_id: "prod_fun id id \<equiv> id"
|
|
213 |
by (rule eq_reflection) (simp add: prod_fun_def)
|
|
214 |
|
|
215 |
lemma map_id: "map id \<equiv> id"
|
|
216 |
apply (rule eq_reflection)
|
|
217 |
apply (rule ext)
|
|
218 |
apply (rule_tac list="x" in list.induct)
|
|
219 |
apply (simp_all)
|
|
220 |
done
|
|
221 |
|
|
222 |
ML {*
|
|
223 |
fun simp_ids lthy thm =
|
|
224 |
MetaSimplifier.rewrite_rule @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} thm
|
|
225 |
*}
|
|
226 |
|
387
|
227 |
section {* Does the same as 'subst' in a given theorem *}
|
381
|
228 |
|
|
229 |
ML {*
|
|
230 |
fun eqsubst_thm ctxt thms thm =
|
|
231 |
let
|
|
232 |
val goalstate = Goal.init (Thm.cprop_of thm)
|
|
233 |
val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
|
|
234 |
NONE => error "eqsubst_thm"
|
|
235 |
| SOME th => cprem_of th 1
|
|
236 |
val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
|
|
237 |
val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a');
|
|
238 |
val cgoal = cterm_of (ProofContext.theory_of ctxt) goal
|
|
239 |
val rt = Goal.prove_internal [] cgoal (fn _ => tac);
|
|
240 |
in
|
|
241 |
@{thm Pure.equal_elim_rule1} OF [rt, thm]
|
|
242 |
end
|
|
243 |
*}
|
|
244 |
|
387
|
245 |
section {* Infrastructure about definitions *}
|
|
246 |
|
381
|
247 |
text {* expects atomized definition *}
|
|
248 |
ML {*
|
|
249 |
fun add_lower_defs_aux lthy thm =
|
|
250 |
let
|
|
251 |
val e1 = @{thm fun_cong} OF [thm];
|
|
252 |
val f = eqsubst_thm lthy @{thms fun_map.simps} e1;
|
|
253 |
val g = simp_ids lthy f
|
|
254 |
in
|
|
255 |
(simp_ids lthy thm) :: (add_lower_defs_aux lthy g)
|
|
256 |
end
|
|
257 |
handle _ => [simp_ids lthy thm]
|
|
258 |
*}
|
|
259 |
|
|
260 |
ML {*
|
|
261 |
fun add_lower_defs lthy def =
|
|
262 |
let
|
|
263 |
val def_pre_sym = symmetric def
|
|
264 |
val def_atom = atomize_thm def_pre_sym
|
|
265 |
val defs_all = add_lower_defs_aux lthy def_atom
|
|
266 |
in
|
|
267 |
map Thm.varifyT defs_all
|
|
268 |
end
|
|
269 |
*}
|
|
270 |
|
387
|
271 |
section {* infrastructure about collecting theorems for calling lifting *}
|
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
272 |
|
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
273 |
ML {*
|
239
|
274 |
fun lookup_quot_data lthy qty =
|
|
275 |
let
|
311
|
276 |
val qty_name = fst (dest_Type qty)
|
314
|
277 |
val SOME quotdata = quotdata_lookup lthy qty_name
|
311
|
278 |
(* cu: Changed the lookup\<dots>not sure whether this works *)
|
303
|
279 |
(* TODO: Should no longer be needed *)
|
257
|
280 |
val rty = Logic.unvarifyT (#rtyp quotdata)
|
239
|
281 |
val rel = #rel quotdata
|
|
282 |
val rel_eqv = #equiv_thm quotdata
|
|
283 |
val rel_refl_pre = @{thm EQUIV_REFL} OF [rel_eqv]
|
|
284 |
val rel_refl = @{thm spec} OF [MetaSimplifier.rewrite_rule [@{thm REFL_def}] rel_refl_pre]
|
|
285 |
in
|
|
286 |
(rty, rel, rel_refl, rel_eqv)
|
|
287 |
end
|
|
288 |
*}
|
|
289 |
|
|
290 |
ML {*
|
|
291 |
fun lookup_quot_thms lthy qty_name =
|
|
292 |
let
|
|
293 |
val thy = ProofContext.theory_of lthy;
|
|
294 |
val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")
|
|
295 |
val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")
|
269
|
296 |
val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")
|
239
|
297 |
val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name)
|
|
298 |
in
|
269
|
299 |
(trans2, reps_same, absrep, quot)
|
239
|
300 |
end
|
|
301 |
*}
|
|
302 |
|
|
303 |
ML {*
|
|
304 |
fun lookup_quot_consts defs =
|
|
305 |
let
|
|
306 |
fun dest_term (a $ b) = (a, b);
|
|
307 |
val def_terms = map (snd o Logic.dest_equals o concl_of) defs;
|
|
308 |
in
|
|
309 |
map (fst o dest_Const o snd o dest_term) def_terms
|
|
310 |
end
|
|
311 |
*}
|
|
312 |
|
275
|
313 |
|
273
|
314 |
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
315 |
(******************************************)
|
325
|
316 |
(******************************************)
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
317 |
(* version with explicit qtrm *)
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
318 |
(******************************************)
|
325
|
319 |
(******************************************)
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
320 |
|
348
|
321 |
|
338
|
322 |
ML {*
|
383
|
323 |
(*
|
|
324 |
Regularizing an rtrm means:
|
|
325 |
- quantifiers over a type that needs lifting are replaced by
|
|
326 |
bounded quantifiers, for example:
|
|
327 |
\<forall>x. P \<Longrightarrow> \<forall>x \<in> (Respects R). P / All (Respects R) P
|
|
328 |
|
|
329 |
the relation R is given by the rty and qty;
|
330
|
330 |
|
383
|
331 |
- abstractions over a type that needs lifting are replaced
|
|
332 |
by bounded abstractions:
|
|
333 |
\<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P)
|
|
334 |
|
|
335 |
- equalities over the type being lifted are replaced by
|
|
336 |
corresponding relations:
|
|
337 |
A = B \<Longrightarrow> A \<approx> B
|
|
338 |
|
|
339 |
example with more complicated types of A, B:
|
|
340 |
A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A B
|
|
341 |
*)
|
|
342 |
|
|
343 |
|
|
344 |
(* builds the relation that is the argument of respects *)
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
345 |
fun mk_resp_arg lthy (rty, qty) =
|
319
|
346 |
let
|
|
347 |
val thy = ProofContext.theory_of lthy
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
348 |
in
|
334
|
349 |
if rty = qty
|
|
350 |
then HOLogic.eq_const rty
|
|
351 |
else
|
|
352 |
case (rty, qty) of
|
|
353 |
(Type (s, tys), Type (s', tys')) =>
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
354 |
if s = s'
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
355 |
then let
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
356 |
val SOME map_info = maps_lookup thy s
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
357 |
val args = map (mk_resp_arg lthy) (tys ~~ tys')
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
358 |
in
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
359 |
list_comb (Const (#relfun map_info, dummyT), args)
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
360 |
end
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
361 |
else let
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
362 |
val SOME qinfo = quotdata_lookup_thy thy s'
|
330
|
363 |
(* FIXME: check in this case that the rty and qty *)
|
|
364 |
(* FIXME: correspond to each other *)
|
353
9a0e8ab42ee8
fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
365 |
val (s, _) = dest_Const (#rel qinfo)
|
9a0e8ab42ee8
fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
366 |
(* FIXME: the relation should only be the string *)
|
9a0e8ab42ee8
fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
367 |
(* FIXME: and the type needs to be calculated as below *)
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
368 |
in
|
353
9a0e8ab42ee8
fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
369 |
Const (s, rty --> rty --> @{typ bool})
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
370 |
end
|
334
|
371 |
| _ => HOLogic.eq_const dummyT
|
351
|
372 |
(* FIXME: check that the types correspond to each other? *)
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
373 |
end
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
374 |
*}
|
239
|
375 |
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
376 |
ML {*
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
377 |
val mk_babs = Const (@{const_name "Babs"}, dummyT)
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
378 |
val mk_ball = Const (@{const_name "Ball"}, dummyT)
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
379 |
val mk_bex = Const (@{const_name "Bex"}, dummyT)
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
380 |
val mk_resp = Const (@{const_name Respects}, dummyT)
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
381 |
*}
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
382 |
|
323
|
383 |
|
|
384 |
ML {*
|
330
|
385 |
(* - applies f to the subterm of an abstraction, *)
|
|
386 |
(* otherwise to the given term, *)
|
351
|
387 |
(* - used by REGULARIZE, therefore abstracted *)
|
330
|
388 |
(* variables do not have to be treated specially *)
|
|
389 |
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
390 |
fun apply_subt f trm1 trm2 =
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
391 |
case (trm1, trm2) of
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
392 |
(Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t')
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
393 |
| _ => f trm1 trm2
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
394 |
|
330
|
395 |
(* the major type of All and Ex quantifiers *)
|
334
|
396 |
fun qnt_typ ty = domain_type (domain_type ty)
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
397 |
*}
|
319
|
398 |
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
399 |
ML {*
|
330
|
400 |
(* produces a regularized version of rtm *)
|
|
401 |
(* - the result is still not completely typed *)
|
|
402 |
(* - does not need any special treatment of *)
|
|
403 |
(* bound variables *)
|
|
404 |
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
405 |
fun REGULARIZE_trm lthy rtrm qtrm =
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
406 |
case (rtrm, qtrm) of
|
325
|
407 |
(Abs (x, ty, t), Abs (x', ty', t')) =>
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
408 |
let
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
409 |
val subtrm = REGULARIZE_trm lthy t t'
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
410 |
in
|
325
|
411 |
if ty = ty'
|
|
412 |
then Abs (x, ty, subtrm)
|
326
|
413 |
else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
414 |
end
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
415 |
| (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
416 |
let
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
417 |
val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
418 |
in
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
419 |
if ty = ty'
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
420 |
then Const (@{const_name "All"}, ty) $ subtrm
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
421 |
else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
422 |
end
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
423 |
| (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
424 |
let
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
425 |
val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
426 |
in
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
427 |
if ty = ty'
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
428 |
then Const (@{const_name "Ex"}, ty) $ subtrm
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
429 |
else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
430 |
end
|
351
|
431 |
(* FIXME: Should = only be replaced, when fully applied? *)
|
|
432 |
(* Then there must be a 2nd argument *)
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
433 |
| (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
434 |
let
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
435 |
val subtrm = REGULARIZE_trm lthy t t'
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
436 |
in
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
437 |
if ty = ty'
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
438 |
then Const (@{const_name "op ="}, ty) $ subtrm
|
349
|
439 |
else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
440 |
end
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
441 |
| (t1 $ t2, t1' $ t2') =>
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
442 |
(REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2')
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
443 |
| (Free (x, ty), Free (x', ty')) =>
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
444 |
if x = x'
|
330
|
445 |
then rtrm (* FIXME: check whether types corresponds *)
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
446 |
else raise (LIFT_MATCH "regularize (frees)")
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
447 |
| (Bound i, Bound i') =>
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
448 |
if i = i'
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
449 |
then rtrm
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
450 |
else raise (LIFT_MATCH "regularize (bounds)")
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
451 |
| (Const (s, ty), Const (s', ty')) =>
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
452 |
if s = s' andalso ty = ty'
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
453 |
then rtrm
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
454 |
else rtrm (* FIXME: check correspondence according to definitions *)
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
455 |
| (rt, qt) =>
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
456 |
raise (LIFT_MATCH "regularize (default)")
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
457 |
*}
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
458 |
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
459 |
ML {*
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
460 |
fun mk_REGULARIZE_goal lthy rtrm qtrm =
|
330
|
461 |
Logic.mk_implies (rtrm, Syntax.check_term lthy (REGULARIZE_trm lthy rtrm qtrm))
|
319
|
462 |
*}
|
293
|
463 |
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
464 |
(*
|
383
|
465 |
To prove that the raw theorem implies the regularised one,
|
|
466 |
we try in order:
|
330
|
467 |
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
468 |
- Reflexivity of the relation
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
469 |
- Assumption
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
470 |
- Elimnating quantifiers on both sides of toplevel implication
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
471 |
- Simplifying implications on both sides of toplevel implication
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
472 |
- Ball (Respects ?E) ?P = All ?P
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
473 |
- (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
474 |
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
475 |
*)
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
476 |
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
477 |
lemma my_equiv_res_forall2:
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
478 |
fixes P::"'a \<Rightarrow> bool"
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
479 |
fixes Q::"'b \<Rightarrow> bool"
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
480 |
assumes a: "(All Q) \<longrightarrow> (All P)"
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
481 |
shows "(All Q) \<longrightarrow> Ball (Respects E) P"
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
482 |
using a by auto
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
483 |
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
484 |
lemma my_equiv_res_exists:
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
485 |
fixes P::"'a \<Rightarrow> bool"
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
486 |
fixes Q::"'b \<Rightarrow> bool"
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
487 |
assumes a: "EQUIV E"
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
488 |
and b: "(Ex Q) \<longrightarrow> (Ex P)"
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
489 |
shows "(Ex Q) \<longrightarrow> Bex (Respects E) P"
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
490 |
apply(subst equiv_res_exists)
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
491 |
apply(rule a)
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
492 |
apply(rule b)
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
493 |
done
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
494 |
|
381
|
495 |
lemma universal_twice:
|
|
496 |
assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
|
|
497 |
shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
|
|
498 |
using * by auto
|
|
499 |
|
|
500 |
lemma implication_twice:
|
|
501 |
assumes a: "c \<longrightarrow> a"
|
|
502 |
assumes b: "a \<Longrightarrow> b \<longrightarrow> d"
|
|
503 |
shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
|
|
504 |
using a b by auto
|
|
505 |
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
506 |
ML {*
|
330
|
507 |
(* FIXME: get_rid of rel_refl rel_eqv *)
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
508 |
fun REGULARIZE_tac lthy rel_refl rel_eqv =
|
325
|
509 |
(REPEAT1 o FIRST1)
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
510 |
[rtac rel_refl,
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
511 |
atac,
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
512 |
rtac @{thm universal_twice},
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
513 |
rtac @{thm impI} THEN' atac,
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
514 |
rtac @{thm implication_twice},
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
515 |
rtac @{thm my_equiv_res_forall2},
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
516 |
rtac (rel_eqv RS @{thm my_equiv_res_exists}),
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
517 |
(* For a = b \<longrightarrow> a \<approx> b *)
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
518 |
rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl,
|
325
|
519 |
rtac @{thm RIGHT_RES_FORALL_REGULAR}]
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
520 |
*}
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
521 |
|
330
|
522 |
(* version of REGULARIZE_tac including debugging information *)
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
523 |
ML {*
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
524 |
fun my_print_tac ctxt s thm =
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
525 |
let
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
526 |
val prems_str = prems_of thm
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
527 |
|> map (Syntax.string_of_term ctxt)
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
528 |
|> cat_lines
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
529 |
val _ = tracing (s ^ "\n" ^ prems_str)
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
530 |
in
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
531 |
Seq.single thm
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
532 |
end
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
533 |
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
534 |
fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))]
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
535 |
*}
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
536 |
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
537 |
ML {*
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
538 |
fun REGULARIZE_tac' lthy rel_refl rel_eqv =
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
539 |
(REPEAT1 o FIRST1)
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
540 |
[(K (print_tac "start")) THEN' (K no_tac),
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
541 |
DT lthy "1" (rtac rel_refl),
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
542 |
DT lthy "2" atac,
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
543 |
DT lthy "3" (rtac @{thm universal_twice}),
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
544 |
DT lthy "4" (rtac @{thm impI} THEN' atac),
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
545 |
DT lthy "5" (rtac @{thm implication_twice}),
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
546 |
DT lthy "6" (rtac @{thm my_equiv_res_forall2}),
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
547 |
DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_exists})),
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
548 |
(* For a = b \<longrightarrow> a \<approx> b *)
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
549 |
DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
550 |
DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})]
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
551 |
*}
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
552 |
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
553 |
ML {*
|
383
|
554 |
fun regularize_tac ctxt rel_eqv rel_refl =
|
|
555 |
(ObjectLogic.full_atomize_tac) THEN'
|
|
556 |
REPEAT_ALL_NEW (FIRST' [
|
|
557 |
rtac rel_refl,
|
|
558 |
atac,
|
|
559 |
rtac @{thm universal_twice},
|
|
560 |
(rtac @{thm impI} THEN' atac),
|
|
561 |
rtac @{thm implication_twice},
|
|
562 |
EqSubst.eqsubst_tac ctxt [0]
|
|
563 |
[(@{thm equiv_res_forall} OF [rel_eqv]),
|
|
564 |
(@{thm equiv_res_exists} OF [rel_eqv])],
|
|
565 |
(* For a = b \<longrightarrow> a \<approx> b *)
|
|
566 |
(rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
|
|
567 |
(rtac @{thm RIGHT_RES_FORALL_REGULAR})
|
|
568 |
]);
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
569 |
*}
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
570 |
|
383
|
571 |
|
381
|
572 |
(*
|
383
|
573 |
Injections of REP and Abses
|
|
574 |
***************************
|
|
575 |
|
381
|
576 |
Injecting REPABS means:
|
|
577 |
|
|
578 |
For abstractions:
|
|
579 |
* If the type of the abstraction doesn't need lifting we recurse.
|
|
580 |
* If it does we add RepAbs around the whole term and check if the
|
|
581 |
variable needs lifting.
|
|
582 |
* If it doesn't then we recurse
|
|
583 |
* If it does we recurse and put 'RepAbs' around all occurences
|
|
584 |
of the variable in the obtained subterm. This in combination
|
|
585 |
with the RepAbs above will let us change the type of the
|
|
586 |
abstraction with rewriting.
|
|
587 |
For applications:
|
|
588 |
* If the term is 'Respects' applied to anything we leave it unchanged
|
|
589 |
* If the term needs lifting and the head is a constant that we know
|
|
590 |
how to lift, we put a RepAbs and recurse
|
|
591 |
* If the term needs lifting and the head is a free applied to subterms
|
|
592 |
(if it is not applied we treated it in Abs branch) then we
|
|
593 |
put RepAbs and recurse
|
|
594 |
* Otherwise just recurse.
|
|
595 |
*)
|
|
596 |
|
336
|
597 |
ML {*
|
|
598 |
fun mk_repabs lthy (T, T') trm =
|
|
599 |
Quotient_Def.get_fun repF lthy (T, T')
|
354
2eb6d527dfe4
addded a tactic, which sets up the three goals of the `algorithm'
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
600 |
$ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
|
336
|
601 |
*}
|
|
602 |
|
|
603 |
ML {*
|
|
604 |
(* bound variables need to be treated properly, *)
|
|
605 |
(* as the type of subterms need to be calculated *)
|
|
606 |
|
|
607 |
fun inj_REPABS lthy (rtrm, qtrm) =
|
|
608 |
let
|
|
609 |
val rty = fastype_of rtrm
|
|
610 |
val qty = fastype_of qtrm
|
|
611 |
in
|
|
612 |
case (rtrm, qtrm) of
|
|
613 |
(Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
|
|
614 |
Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t'))
|
|
615 |
| (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
|
|
616 |
Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t'))
|
|
617 |
| (Const (@{const_name "Babs"}, T) $ r $ t, t') =>
|
|
618 |
Const (@{const_name "Babs"}, T) $ r $ (inj_REPABS lthy (t, t'))
|
|
619 |
| (Abs (x, T, t), Abs (x', T', t')) =>
|
|
620 |
let
|
|
621 |
val (y, s) = Term.dest_abs (x, T, t)
|
|
622 |
val (_, s') = Term.dest_abs (x', T', t')
|
|
623 |
val yvar = Free (y, T)
|
345
|
624 |
val result = lambda yvar (inj_REPABS lthy (s, s'))
|
336
|
625 |
in
|
345
|
626 |
if rty = qty
|
|
627 |
then result
|
|
628 |
else mk_repabs lthy (rty, qty) result
|
336
|
629 |
end
|
|
630 |
| _ =>
|
345
|
631 |
(* FIXME / TODO: this is a case that needs to be looked at *)
|
|
632 |
(* - variables get a rep-abs insde and outside an application *)
|
|
633 |
(* - constants only get a rep-abs on the outside of the application *)
|
|
634 |
(* - applications get a rep-abs insde and outside an application *)
|
336
|
635 |
let
|
|
636 |
val (rhead, rargs) = strip_comb rtrm
|
|
637 |
val (qhead, qargs) = strip_comb qtrm
|
345
|
638 |
val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs)
|
336
|
639 |
in
|
345
|
640 |
if rty = qty
|
355
|
641 |
then
|
|
642 |
case (rhead, qhead) of
|
|
643 |
(Free (_, T), Free (_, T')) =>
|
|
644 |
if T = T' then list_comb (rhead, rargs')
|
|
645 |
else list_comb (mk_repabs lthy (T, T') rhead, rargs')
|
|
646 |
| _ => list_comb (rhead, rargs')
|
345
|
647 |
else
|
|
648 |
case (rhead, qhead, length rargs') of
|
|
649 |
(Const _, Const _, 0) => mk_repabs lthy (rty, qty) rhead
|
355
|
650 |
| (Free (_, T), Free (_, T'), 0) => mk_repabs lthy (T, T') rhead
|
345
|
651 |
| (Const _, Const _, _) => mk_repabs lthy (rty, qty) (list_comb (rhead, rargs'))
|
|
652 |
| (Free (x, T), Free (x', T'), _) =>
|
|
653 |
mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs'))
|
|
654 |
| (Abs _, Abs _, _ ) =>
|
|
655 |
mk_repabs lthy (rty, qty) (list_comb (inj_REPABS lthy (rhead, qhead), rargs'))
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
656 |
| _ => raise (LIFT_MATCH "injection")
|
336
|
657 |
end
|
|
658 |
end
|
|
659 |
*}
|
|
660 |
|
|
661 |
ML {*
|
|
662 |
fun mk_inj_REPABS_goal lthy (rtrm, qtrm) =
|
|
663 |
Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm)))
|
|
664 |
*}
|
|
665 |
|
387
|
666 |
section {* RepAbs injection tactic *}
|
|
667 |
(*
|
|
668 |
|
|
669 |
To prove that the regularised theorem implies the abs/rep injected, we first
|
|
670 |
atomize it and then try:
|
|
671 |
|
|
672 |
1) theorems 'trans2' from the appropriate QUOT_TYPE
|
|
673 |
2) remove lambdas from both sides (LAMBDA_RES_TAC)
|
|
674 |
3) remove Ball/Bex from the right hand side
|
|
675 |
4) use user-supplied RSP theorems
|
|
676 |
5) remove rep_abs from the right side
|
|
677 |
6) reflexivity of equality
|
|
678 |
7) split applications of lifted type (apply_rsp)
|
|
679 |
8) split applications of non-lifted type (cong_tac)
|
|
680 |
9) apply extentionality
|
|
681 |
10) reflexivity of the relation
|
|
682 |
11) assumption
|
|
683 |
(Lambdas under respects may have left us some assumptions)
|
|
684 |
12) proving obvious higher order equalities by simplifying fun_rel
|
|
685 |
(not sure if it is still needed?)
|
|
686 |
13) unfolding lambda on one side
|
|
687 |
14) simplifying (= ===> =) for simpler respectfullness
|
|
688 |
|
|
689 |
*)
|
|
690 |
|
|
691 |
ML {*
|
|
692 |
fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
|
|
693 |
let
|
|
694 |
val pat = Drule.strip_imp_concl (cprop_of thm)
|
|
695 |
val insts = Thm.match (pat, concl)
|
|
696 |
in
|
|
697 |
rtac (Drule.instantiate insts thm) 1
|
|
698 |
end
|
|
699 |
handle _ => no_tac)
|
|
700 |
*}
|
|
701 |
|
|
702 |
ML {*
|
|
703 |
fun CHANGED' tac = (fn i => CHANGED (tac i))
|
|
704 |
*}
|
|
705 |
|
|
706 |
ML {*
|
|
707 |
fun quotient_tac quot_thm =
|
|
708 |
REPEAT_ALL_NEW (FIRST' [
|
|
709 |
rtac @{thm FUN_QUOTIENT},
|
|
710 |
rtac quot_thm,
|
|
711 |
rtac @{thm IDENTITY_QUOTIENT},
|
|
712 |
(* For functional identity quotients, (op = ---> op =) *)
|
|
713 |
CHANGED' (
|
|
714 |
(simp_tac (HOL_ss addsimps @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}
|
|
715 |
)))
|
|
716 |
])
|
|
717 |
*}
|
|
718 |
|
|
719 |
ML {*
|
|
720 |
fun LAMBDA_RES_TAC ctxt i st =
|
|
721 |
(case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
|
|
722 |
(_ $ (_ $ (Abs(_, _, _)) $ (Abs(_, _, _)))) =>
|
|
723 |
(EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
|
|
724 |
(rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
|
|
725 |
| _ => fn _ => no_tac) i st
|
|
726 |
*}
|
|
727 |
|
|
728 |
ML {*
|
|
729 |
fun WEAK_LAMBDA_RES_TAC ctxt i st =
|
|
730 |
(case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
|
|
731 |
(_ $ (_ $ _ $ (Abs(_, _, _)))) =>
|
|
732 |
(EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
|
|
733 |
(rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
|
|
734 |
| (_ $ (_ $ (Abs(_, _, _)) $ _)) =>
|
|
735 |
(EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
|
|
736 |
(rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
|
|
737 |
| _ => fn _ => no_tac) i st
|
|
738 |
*}
|
|
739 |
|
|
740 |
ML {* (* Legacy *)
|
|
741 |
fun needs_lift (rty as Type (rty_s, _)) ty =
|
|
742 |
case ty of
|
|
743 |
Type (s, tys) =>
|
|
744 |
(s = rty_s) orelse (exists (needs_lift rty) tys)
|
|
745 |
| _ => false
|
|
746 |
|
|
747 |
*}
|
|
748 |
|
|
749 |
ML {*
|
|
750 |
fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>
|
|
751 |
let
|
|
752 |
val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
|
|
753 |
val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
|
|
754 |
val insts = Thm.match (pat, concl)
|
|
755 |
in
|
|
756 |
if needs_lift rty (type_of f) then
|
|
757 |
rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
|
|
758 |
else no_tac
|
|
759 |
end
|
|
760 |
handle _ => no_tac)
|
|
761 |
*}
|
|
762 |
|
|
763 |
ML {*
|
|
764 |
val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
|
|
765 |
let
|
|
766 |
val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
|
|
767 |
(Const (@{const_name Ball}, _) $ _)) = term_of concl
|
|
768 |
in
|
|
769 |
((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
|
|
770 |
THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
|
|
771 |
THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
|
|
772 |
(simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
|
|
773 |
end
|
|
774 |
handle _ => no_tac)
|
|
775 |
*}
|
|
776 |
|
|
777 |
ML {*
|
|
778 |
val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
|
|
779 |
let
|
|
780 |
val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
|
|
781 |
(Const (@{const_name Bex}, _) $ _)) = term_of concl
|
|
782 |
in
|
|
783 |
((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
|
|
784 |
THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
|
|
785 |
THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
|
|
786 |
(simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
|
|
787 |
end
|
|
788 |
handle _ => no_tac)
|
|
789 |
*}
|
|
790 |
|
|
791 |
ML {*
|
|
792 |
fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
|
|
793 |
*}
|
|
794 |
|
|
795 |
ML {*
|
|
796 |
fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
|
|
797 |
(FIRST' [
|
|
798 |
rtac trans_thm,
|
|
799 |
LAMBDA_RES_TAC ctxt,
|
389
|
800 |
rtac @{thm RES_FORALL_RSP},
|
387
|
801 |
ball_rsp_tac ctxt,
|
389
|
802 |
rtac @{thm RES_EXISTS_RSP},
|
387
|
803 |
bex_rsp_tac ctxt,
|
|
804 |
FIRST' (map rtac rsp_thms),
|
|
805 |
rtac refl,
|
|
806 |
(instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm)])),
|
|
807 |
(APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])),
|
|
808 |
Cong_Tac.cong_tac @{thm cong},
|
|
809 |
rtac @{thm ext},
|
|
810 |
rtac reflex_thm,
|
|
811 |
atac,
|
|
812 |
SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
|
|
813 |
WEAK_LAMBDA_RES_TAC ctxt,
|
|
814 |
CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
|
|
815 |
])
|
|
816 |
*}
|
|
817 |
|
|
818 |
|
|
819 |
(****************************************)
|
|
820 |
(* cleaning of the theorem *)
|
|
821 |
(****************************************)
|
|
822 |
|
|
823 |
|
|
824 |
|
|
825 |
(* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)
|
|
826 |
ML {*
|
|
827 |
fun exchange_ty lthy rty qty ty =
|
|
828 |
let
|
|
829 |
val thy = ProofContext.theory_of lthy
|
|
830 |
in
|
|
831 |
if Sign.typ_instance thy (ty, rty) then
|
|
832 |
let
|
|
833 |
val inst = Sign.typ_match thy (rty, ty) Vartab.empty
|
|
834 |
in
|
|
835 |
Envir.subst_type inst qty
|
|
836 |
end
|
|
837 |
else
|
|
838 |
let
|
|
839 |
val (s, tys) = dest_Type ty
|
|
840 |
in
|
|
841 |
Type (s, map (exchange_ty lthy rty qty) tys)
|
|
842 |
end
|
|
843 |
end
|
|
844 |
handle TYPE _ => ty (* for dest_Type *)
|
|
845 |
*}
|
|
846 |
|
|
847 |
|
|
848 |
ML {*
|
|
849 |
fun find_matching_types rty ty =
|
|
850 |
if Type.raw_instance (Logic.varifyT ty, rty)
|
|
851 |
then [ty]
|
|
852 |
else
|
|
853 |
let val (s, tys) = dest_Type ty in
|
|
854 |
flat (map (find_matching_types rty) tys)
|
|
855 |
end
|
|
856 |
handle TYPE _ => []
|
|
857 |
*}
|
|
858 |
|
|
859 |
ML {*
|
|
860 |
fun negF absF = repF
|
|
861 |
| negF repF = absF
|
|
862 |
|
|
863 |
fun get_fun flag qenv lthy ty =
|
|
864 |
let
|
|
865 |
|
|
866 |
fun get_fun_aux s fs =
|
|
867 |
(case (maps_lookup (ProofContext.theory_of lthy) s) of
|
|
868 |
SOME info => list_comb (Const (#mapfun info, dummyT), fs)
|
|
869 |
| NONE => error ("no map association for type " ^ s))
|
|
870 |
|
|
871 |
fun get_const flag qty =
|
|
872 |
let
|
|
873 |
val thy = ProofContext.theory_of lthy
|
|
874 |
val qty_name = Long_Name.base_name (fst (dest_Type qty))
|
|
875 |
in
|
|
876 |
case flag of
|
|
877 |
absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)
|
|
878 |
| repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
|
|
879 |
end
|
|
880 |
|
|
881 |
fun mk_identity ty = Abs ("", ty, Bound 0)
|
|
882 |
|
|
883 |
in
|
|
884 |
if (AList.defined (op=) qenv ty)
|
|
885 |
then (get_const flag ty)
|
|
886 |
else (case ty of
|
|
887 |
TFree _ => mk_identity ty
|
|
888 |
| Type (_, []) => mk_identity ty
|
|
889 |
| Type ("fun" , [ty1, ty2]) =>
|
|
890 |
let
|
|
891 |
val fs_ty1 = get_fun (negF flag) qenv lthy ty1
|
|
892 |
val fs_ty2 = get_fun flag qenv lthy ty2
|
|
893 |
in
|
|
894 |
get_fun_aux "fun" [fs_ty1, fs_ty2]
|
|
895 |
end
|
|
896 |
| Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
|
|
897 |
| _ => error ("no type variables allowed"))
|
|
898 |
end
|
|
899 |
*}
|
|
900 |
|
|
901 |
ML {*
|
|
902 |
fun get_fun_OLD flag (rty, qty) lthy ty =
|
|
903 |
let
|
|
904 |
val tys = find_matching_types rty ty;
|
|
905 |
val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;
|
|
906 |
val xchg_ty = exchange_ty lthy rty qty ty
|
|
907 |
in
|
|
908 |
get_fun flag qenv lthy xchg_ty
|
|
909 |
end
|
|
910 |
*}
|
|
911 |
|
|
912 |
ML {*
|
389
|
913 |
fun applic_prs_old lthy rty qty absrep ty =
|
387
|
914 |
let
|
|
915 |
val rty = Logic.varifyT rty;
|
|
916 |
val qty = Logic.varifyT qty;
|
|
917 |
fun absty ty =
|
|
918 |
exchange_ty lthy rty qty ty
|
|
919 |
fun mk_rep tm =
|
|
920 |
let
|
|
921 |
val ty = exchange_ty lthy qty rty (fastype_of tm)
|
|
922 |
in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ tm) end;
|
|
923 |
fun mk_abs tm =
|
|
924 |
let
|
|
925 |
val ty = fastype_of tm
|
|
926 |
in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end
|
|
927 |
val (l, ltl) = Term.strip_type ty;
|
|
928 |
val nl = map absty l;
|
|
929 |
val vs = map (fn _ => "x") l;
|
|
930 |
val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
|
|
931 |
val args = map Free (vfs ~~ nl);
|
|
932 |
val lhs = list_comb((Free (fname, nl ---> ltl)), args);
|
|
933 |
val rargs = map mk_rep args;
|
|
934 |
val f = Free (fname, nl ---> ltl);
|
|
935 |
val rhs = mk_abs (list_comb((mk_rep f), rargs));
|
|
936 |
val eq = Logic.mk_equals (rhs, lhs);
|
|
937 |
val ceq = cterm_of (ProofContext.theory_of lthy') eq;
|
|
938 |
val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps});
|
|
939 |
val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
|
|
940 |
val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t;
|
|
941 |
in
|
|
942 |
singleton (ProofContext.export lthy' lthy) t_id
|
|
943 |
end
|
|
944 |
*}
|
|
945 |
|
389
|
946 |
ML {*
|
|
947 |
fun applic_prs lthy absrep (rty, qty) =
|
|
948 |
let
|
|
949 |
fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm;
|
|
950 |
fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm;
|
|
951 |
val (raty, rgty) = Term.strip_type rty;
|
|
952 |
val (qaty, qgty) = Term.strip_type qty;
|
|
953 |
val vs = map (fn _ => "x") qaty;
|
|
954 |
val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
|
|
955 |
val f = Free (fname, qaty ---> qgty);
|
|
956 |
val args = map Free (vfs ~~ qaty);
|
|
957 |
val rhs = list_comb(f, args);
|
|
958 |
val largs = map2 mk_rep (raty ~~ qaty) args;
|
|
959 |
val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs));
|
|
960 |
val llhs = Syntax.check_term lthy lhs;
|
|
961 |
val eq = Logic.mk_equals (llhs, rhs);
|
|
962 |
val ceq = cterm_of (ProofContext.theory_of lthy') eq;
|
|
963 |
val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps map_id id_apply});
|
|
964 |
val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
|
|
965 |
val t_id = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply] id_def_sym} t;
|
|
966 |
in
|
|
967 |
singleton (ProofContext.export lthy' lthy) t_id
|
|
968 |
end
|
|
969 |
*}
|
387
|
970 |
|
|
971 |
ML {*
|
|
972 |
fun findaps_all rty tm =
|
|
973 |
case tm of
|
|
974 |
Abs(_, T, b) =>
|
|
975 |
findaps_all rty (subst_bound ((Free ("x", T)), b))
|
|
976 |
| (f $ a) => (findaps_all rty f @ findaps_all rty a)
|
|
977 |
| Free (_, (T as (Type ("fun", (_ :: _))))) =>
|
|
978 |
(if needs_lift rty T then [T] else [])
|
|
979 |
| _ => [];
|
|
980 |
fun findaps rty tm = distinct (op =) (findaps_all rty tm)
|
|
981 |
*}
|
|
982 |
|
|
983 |
|
|
984 |
ML {*
|
389
|
985 |
fun find_aps_all rtm qtm =
|
|
986 |
case (rtm, qtm) of
|
|
987 |
(Abs(_, T1, s1), Abs(_, T2, s2)) =>
|
|
988 |
find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2))
|
|
989 |
| (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) =>
|
|
990 |
let
|
|
991 |
val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2)
|
|
992 |
in
|
|
993 |
if T1 = T2 then sub else (T1, T2) :: sub
|
|
994 |
end
|
|
995 |
| ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2)
|
|
996 |
| _ => [];
|
|
997 |
|
|
998 |
fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm)
|
|
999 |
*}
|
|
1000 |
|
|
1001 |
ML {*
|
387
|
1002 |
(* FIXME: allex_prs and lambda_prs can be one function *)
|
|
1003 |
fun allex_prs_tac lthy quot =
|
|
1004 |
(EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
|
|
1005 |
THEN' (quotient_tac quot);
|
|
1006 |
*}
|
|
1007 |
|
|
1008 |
ML {*
|
|
1009 |
let
|
|
1010 |
val parser = Args.context -- Scan.lift Args.name_source
|
|
1011 |
fun term_pat (ctxt, str) =
|
|
1012 |
str |> ProofContext.read_term_pattern ctxt
|
|
1013 |
|> ML_Syntax.print_term
|
|
1014 |
|> ML_Syntax.atomic
|
|
1015 |
in
|
|
1016 |
ML_Antiquote.inline "term_pat" (parser >> term_pat)
|
|
1017 |
end
|
|
1018 |
*}
|
|
1019 |
|
|
1020 |
ML {*
|
|
1021 |
fun prep_trm thy (x, (T, t)) =
|
|
1022 |
(cterm_of thy (Var (x, T)), cterm_of thy t)
|
|
1023 |
|
|
1024 |
fun prep_ty thy (x, (S, ty)) =
|
|
1025 |
(ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
|
|
1026 |
*}
|
|
1027 |
|
|
1028 |
ML {*
|
|
1029 |
fun matching_prs thy pat trm =
|
|
1030 |
let
|
|
1031 |
val univ = Unify.matchers thy [(pat, trm)]
|
|
1032 |
val SOME (env, _) = Seq.pull univ
|
|
1033 |
val tenv = Vartab.dest (Envir.term_env env)
|
|
1034 |
val tyenv = Vartab.dest (Envir.type_env env)
|
|
1035 |
in
|
|
1036 |
(map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
|
|
1037 |
end
|
|
1038 |
*}
|
|
1039 |
|
|
1040 |
ML {*
|
|
1041 |
fun lambda_prs_conv1 ctxt quot ctrm =
|
|
1042 |
case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>
|
|
1043 |
let
|
|
1044 |
val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);
|
|
1045 |
val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2);
|
|
1046 |
val thy = ProofContext.theory_of ctxt;
|
|
1047 |
val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
|
|
1048 |
val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d];
|
|
1049 |
val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
|
|
1050 |
val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};
|
|
1051 |
val tac =
|
|
1052 |
(compose_tac (false, lpi, 2)) THEN_ALL_NEW
|
|
1053 |
(quotient_tac quot);
|
|
1054 |
val gc = Drule.strip_imp_concl (cprop_of lpi);
|
|
1055 |
val t = Goal.prove_internal [] gc (fn _ => tac 1)
|
|
1056 |
val te = @{thm eq_reflection} OF [t]
|
|
1057 |
val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te
|
|
1058 |
val tl = Thm.lhs_of ts
|
|
1059 |
(* val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));*)
|
|
1060 |
(* val _ = tracing (Syntax.string_of_term @{context} (term_of tl));*)
|
|
1061 |
val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm);
|
|
1062 |
val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts);
|
|
1063 |
(* val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
|
|
1064 |
in
|
|
1065 |
Conv.rewr_conv ti ctrm
|
|
1066 |
end
|
|
1067 |
(* TODO: We can add a proper error message... *)
|
|
1068 |
handle Bind => Conv.all_conv ctrm
|
|
1069 |
|
|
1070 |
*}
|
|
1071 |
|
|
1072 |
(* quot stands for the QUOTIENT theorems: *)
|
|
1073 |
(* could be potentially all of them *)
|
|
1074 |
ML {*
|
|
1075 |
fun lambda_prs_conv ctxt quot ctrm =
|
|
1076 |
case (term_of ctrm) of
|
|
1077 |
(Const (@{const_name "fun_map"}, _) $ _ $ _) $ (Abs _) =>
|
|
1078 |
(Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt)
|
|
1079 |
then_conv (lambda_prs_conv1 ctxt quot)) ctrm
|
|
1080 |
| _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm
|
|
1081 |
| Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm
|
|
1082 |
| _ => Conv.all_conv ctrm
|
|
1083 |
*}
|
|
1084 |
|
|
1085 |
ML {*
|
|
1086 |
fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>
|
|
1087 |
CONVERSION
|
|
1088 |
(Conv.params_conv ~1 (fn ctxt =>
|
|
1089 |
(Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv
|
|
1090 |
Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
|
|
1091 |
*}
|
|
1092 |
|
|
1093 |
ML {*
|
389
|
1094 |
fun clean_tac lthy quot defs reps_same absrep aps =
|
387
|
1095 |
let
|
|
1096 |
val lower = flat (map (add_lower_defs lthy) defs)
|
389
|
1097 |
val aps_thms = map (applic_prs lthy absrep) aps
|
387
|
1098 |
in
|
|
1099 |
EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
|
|
1100 |
lambda_prs_tac lthy quot,
|
389
|
1101 |
TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms),
|
387
|
1102 |
TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower),
|
|
1103 |
simp_tac (HOL_ss addsimps [reps_same])]
|
|
1104 |
end
|
|
1105 |
*}
|
381
|
1106 |
|
383
|
1107 |
(* Genralisation of free variables in a goal *)
|
347
|
1108 |
|
|
1109 |
ML {*
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1110 |
fun inst_spec ctrm =
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1111 |
let
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1112 |
val cty = ctyp_of_term ctrm
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1113 |
in
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1114 |
Drule.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec}
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1115 |
end
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1116 |
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1117 |
fun inst_spec_tac ctrms =
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1118 |
EVERY' (map (dtac o inst_spec) ctrms)
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1119 |
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1120 |
fun abs_list (xs, t) =
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1121 |
fold (fn (x, T) => fn t' => HOLogic.all_const T $ (lambda (Free (x, T)) t')) xs t
|
362
|
1122 |
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1123 |
fun gen_frees_tac ctxt =
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1124 |
SUBGOAL (fn (concl, i) =>
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1125 |
let
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1126 |
val thy = ProofContext.theory_of ctxt
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1127 |
val concl' = HOLogic.dest_Trueprop concl
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1128 |
val vrs = Term.add_frees concl' []
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1129 |
val cvrs = map (cterm_of thy o Free) vrs
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1130 |
val concl'' = HOLogic.mk_Trueprop (abs_list (vrs, concl'))
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1131 |
val goal = Logic.mk_implies (concl'', concl)
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1132 |
val rule = Goal.prove ctxt [] [] goal
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1133 |
(K ((inst_spec_tac (rev cvrs) THEN' atac) 1))
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1134 |
in
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1135 |
rtac rule i
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1136 |
end)
|
362
|
1137 |
*}
|
|
1138 |
|
383
|
1139 |
(* General outline of the lifting procedure *)
|
|
1140 |
(* **************************************** *)
|
|
1141 |
(* *)
|
|
1142 |
(* - A is the original raw theorem *)
|
|
1143 |
(* - B is the regularized theorem *)
|
|
1144 |
(* - C is the rep/abs injected version of B *)
|
|
1145 |
(* - D is the lifted theorem *)
|
|
1146 |
(* *)
|
|
1147 |
(* - b is the regularization step *)
|
|
1148 |
(* - c is the rep/abs injection step *)
|
|
1149 |
(* - d is the cleaning part *)
|
|
1150 |
|
360
|
1151 |
lemma procedure:
|
|
1152 |
assumes a: "A"
|
|
1153 |
and b: "A \<Longrightarrow> B"
|
|
1154 |
and c: "B = C"
|
|
1155 |
and d: "C = D"
|
|
1156 |
shows "D"
|
|
1157 |
using a b c d
|
|
1158 |
by simp
|
|
1159 |
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1160 |
ML {*
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1161 |
fun lift_error ctxt fun_str rtrm qtrm =
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1162 |
let
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1163 |
val rtrm_str = Syntax.string_of_term ctxt rtrm
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1164 |
val qtrm_str = Syntax.string_of_term ctxt qtrm
|
388
|
1165 |
val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str,
|
|
1166 |
"and the lifted theorem\n", rtrm_str, "do not match"]
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1167 |
in
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1168 |
error (space_implode " " msg)
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1169 |
end
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1170 |
*}
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1171 |
|
360
|
1172 |
ML {*
|
|
1173 |
fun procedure_inst ctxt rtrm qtrm =
|
|
1174 |
let
|
|
1175 |
val thy = ProofContext.theory_of ctxt
|
|
1176 |
val rtrm' = HOLogic.dest_Trueprop rtrm
|
|
1177 |
val qtrm' = HOLogic.dest_Trueprop qtrm
|
383
|
1178 |
val reg_goal =
|
|
1179 |
Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm')
|
|
1180 |
handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
|
|
1181 |
val inj_goal =
|
|
1182 |
Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))
|
|
1183 |
handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
|
360
|
1184 |
in
|
|
1185 |
Drule.instantiate' []
|
|
1186 |
[SOME (cterm_of thy rtrm'),
|
|
1187 |
SOME (cterm_of thy reg_goal),
|
|
1188 |
SOME (cterm_of thy inj_goal)]
|
|
1189 |
@{thm procedure}
|
|
1190 |
end
|
362
|
1191 |
*}
|
389
|
1192 |
|
|
1193 |
(* Left for debugging *)
|
362
|
1194 |
ML {*
|
389
|
1195 |
fun procedure_tac lthy rthm =
|
|
1196 |
ObjectLogic.full_atomize_tac
|
|
1197 |
THEN' gen_frees_tac lthy
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1198 |
THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
|
389
|
1199 |
let
|
|
1200 |
val rthm' = atomize_thm rthm
|
|
1201 |
val rule = procedure_inst context (prop_of rthm') (term_of concl)
|
|
1202 |
in
|
|
1203 |
rtac rule THEN' rtac rthm'
|
|
1204 |
end 1) lthy
|
360
|
1205 |
*}
|
|
1206 |
|
361
|
1207 |
ML {*
|
389
|
1208 |
fun lift_tac lthy rthm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs =
|
|
1209 |
ObjectLogic.full_atomize_tac
|
|
1210 |
THEN' gen_frees_tac lthy
|
|
1211 |
THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
|
|
1212 |
let
|
|
1213 |
val rthm' = atomize_thm rthm
|
|
1214 |
val rule = procedure_inst context (prop_of rthm') (term_of concl)
|
|
1215 |
val aps = find_aps (prop_of rthm') (term_of concl)
|
|
1216 |
in
|
|
1217 |
rtac rule THEN' RANGE [
|
|
1218 |
rtac rthm',
|
|
1219 |
regularize_tac lthy rel_eqv rel_refl,
|
|
1220 |
REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
|
|
1221 |
clean_tac lthy quot defs reps_same absrep aps
|
|
1222 |
]
|
|
1223 |
end 1) lthy
|
361
|
1224 |
*}
|
|
1225 |
|
198
|
1226 |
end
|
239
|
1227 |
|
347
|
1228 |
|