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 |
|
458
|
139 |
(* EQUALS_RSP is stronger *)
|
419
|
140 |
lemma equiv_trans2:
|
|
141 |
assumes e: "EQUIV R"
|
|
142 |
and ac: "R a c"
|
|
143 |
and bd: "R b d"
|
|
144 |
shows "R a b = R c d"
|
|
145 |
using ac bd e
|
|
146 |
unfolding EQUIV_REFL_SYM_TRANS TRANS_def SYM_def
|
|
147 |
by (blast)
|
|
148 |
|
0
|
149 |
section {* type definition for the quotient type *}
|
|
150 |
|
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
|
151 |
(* the auxiliary data for the quotient types *)
|
264
|
152 |
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
|
153 |
|
185
|
154 |
declare [[map list = (map, LIST_REL)]]
|
|
155 |
declare [[map * = (prod_fun, prod_rel)]]
|
|
156 |
declare [[map "fun" = (fun_map, FUN_REL)]]
|
|
157 |
|
|
158 |
ML {* maps_lookup @{theory} "List.list" *}
|
|
159 |
ML {* maps_lookup @{theory} "*" *}
|
|
160 |
ML {* maps_lookup @{theory} "fun" *}
|
174
|
161 |
|
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
|
162 |
|
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
|
163 |
(* definition of the quotient types *)
|
277
|
164 |
(* 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
|
165 |
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
|
166 |
|
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
|
167 |
|
277
|
168 |
(* lifting of constants *)
|
|
169 |
use "quotient_def.ML"
|
|
170 |
|
381
|
171 |
(* TODO: Consider defining it with an "if"; sth like:
|
|
172 |
Babs p m = \<lambda>x. if x \<in> p then m x else undefined
|
|
173 |
*)
|
|
174 |
definition
|
|
175 |
Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
|
|
176 |
where
|
|
177 |
"(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
|
178 |
|
139
|
179 |
section {* ATOMIZE *}
|
|
180 |
|
381
|
181 |
lemma atomize_eqv[atomize]:
|
|
182 |
shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
|
139
|
183 |
proof
|
381
|
184 |
assume "A \<equiv> B"
|
139
|
185 |
then show "Trueprop A \<equiv> Trueprop B" by unfold
|
|
186 |
next
|
|
187 |
assume *: "Trueprop A \<equiv> Trueprop B"
|
|
188 |
have "A = B"
|
|
189 |
proof (cases A)
|
|
190 |
case True
|
|
191 |
have "A" by fact
|
|
192 |
then show "A = B" using * by simp
|
|
193 |
next
|
|
194 |
case False
|
|
195 |
have "\<not>A" by fact
|
|
196 |
then show "A = B" using * by auto
|
|
197 |
qed
|
|
198 |
then show "A \<equiv> B" by (rule eq_reflection)
|
|
199 |
qed
|
|
200 |
|
|
201 |
ML {*
|
|
202 |
fun atomize_thm thm =
|
|
203 |
let
|
221
|
204 |
val thm' = Thm.freezeT (forall_intr_vars thm)
|
139
|
205 |
val thm'' = ObjectLogic.atomize (cprop_of thm')
|
|
206 |
in
|
404
|
207 |
@{thm equal_elim_rule1} OF [thm'', thm']
|
139
|
208 |
end
|
|
209 |
*}
|
|
210 |
|
387
|
211 |
section {* infrastructure about id *}
|
381
|
212 |
|
|
213 |
lemma prod_fun_id: "prod_fun id id \<equiv> id"
|
415
|
214 |
by (rule eq_reflection) (simp add: prod_fun_def)
|
381
|
215 |
|
|
216 |
lemma map_id: "map id \<equiv> id"
|
415
|
217 |
apply (rule eq_reflection)
|
|
218 |
apply (rule ext)
|
|
219 |
apply (rule_tac list="x" in list.induct)
|
|
220 |
apply (simp_all)
|
|
221 |
done
|
381
|
222 |
|
409
|
223 |
lemmas id_simps =
|
|
224 |
FUN_MAP_I[THEN eq_reflection]
|
|
225 |
id_apply[THEN eq_reflection]
|
415
|
226 |
id_def[THEN eq_reflection,symmetric]
|
|
227 |
prod_fun_id map_id
|
409
|
228 |
|
381
|
229 |
ML {*
|
409
|
230 |
fun simp_ids thm =
|
|
231 |
MetaSimplifier.rewrite_rule @{thms id_simps} thm
|
381
|
232 |
*}
|
|
233 |
|
407
|
234 |
section {* Debugging infrastructure for testing tactics *}
|
381
|
235 |
|
447
3e7ee6f5437d
selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
236 |
ML {*
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
237 |
fun my_print_tac ctxt s i thm =
|
407
|
238 |
let
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
239 |
val prem_str = nth (prems_of thm) (i - 1)
|
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
240 |
|> Syntax.string_of_term ctxt
|
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
241 |
handle Subscript => "no subgoal"
|
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
242 |
val _ = tracing (s ^ "\n" ^ prem_str)
|
407
|
243 |
in
|
|
244 |
Seq.single thm
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
245 |
end *}
|
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
246 |
|
407
|
247 |
|
447
3e7ee6f5437d
selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
248 |
ML {*
|
3e7ee6f5437d
selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
249 |
fun DT ctxt s tac i thm =
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
250 |
let
|
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
251 |
val before_goal = nth (prems_of thm) (i - 1)
|
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
252 |
|> Syntax.string_of_term ctxt
|
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
253 |
val before_msg = ["before: " ^ s, before_goal, "after: " ^ s]
|
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
254 |
|> cat_lines
|
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
255 |
in
|
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
256 |
EVERY [tac i, my_print_tac ctxt before_msg i] thm
|
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
257 |
end
|
444
|
258 |
|
447
3e7ee6f5437d
selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
259 |
fun NDT ctxt s tac thm = tac thm
|
407
|
260 |
*}
|
|
261 |
|
453
c22ab554a32d
started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
262 |
|
407
|
263 |
section {* Infrastructure for collecting theorems for starting the lifting *}
|
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
264 |
|
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
265 |
ML {*
|
239
|
266 |
fun lookup_quot_data lthy qty =
|
|
267 |
let
|
311
|
268 |
val qty_name = fst (dest_Type qty)
|
314
|
269 |
val SOME quotdata = quotdata_lookup lthy qty_name
|
311
|
270 |
(* cu: Changed the lookup\<dots>not sure whether this works *)
|
303
|
271 |
(* TODO: Should no longer be needed *)
|
257
|
272 |
val rty = Logic.unvarifyT (#rtyp quotdata)
|
239
|
273 |
val rel = #rel quotdata
|
|
274 |
val rel_eqv = #equiv_thm quotdata
|
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
275 |
val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv]
|
239
|
276 |
in
|
|
277 |
(rty, rel, rel_refl, rel_eqv)
|
|
278 |
end
|
|
279 |
*}
|
|
280 |
|
|
281 |
ML {*
|
|
282 |
fun lookup_quot_thms lthy qty_name =
|
|
283 |
let
|
|
284 |
val thy = ProofContext.theory_of lthy;
|
|
285 |
val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")
|
|
286 |
val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")
|
269
|
287 |
val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")
|
239
|
288 |
val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name)
|
|
289 |
in
|
269
|
290 |
(trans2, reps_same, absrep, quot)
|
239
|
291 |
end
|
|
292 |
*}
|
|
293 |
|
|
294 |
ML {*
|
|
295 |
fun lookup_quot_consts defs =
|
|
296 |
let
|
|
297 |
fun dest_term (a $ b) = (a, b);
|
|
298 |
val def_terms = map (snd o Logic.dest_equals o concl_of) defs;
|
|
299 |
in
|
|
300 |
map (fst o dest_Const o snd o dest_term) def_terms
|
|
301 |
end
|
|
302 |
*}
|
|
303 |
|
402
|
304 |
section {* Regularization *}
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
305 |
|
383
|
306 |
(*
|
|
307 |
Regularizing an rtrm means:
|
|
308 |
- quantifiers over a type that needs lifting are replaced by
|
|
309 |
bounded quantifiers, for example:
|
|
310 |
\<forall>x. P \<Longrightarrow> \<forall>x \<in> (Respects R). P / All (Respects R) P
|
|
311 |
|
|
312 |
the relation R is given by the rty and qty;
|
330
|
313 |
|
383
|
314 |
- abstractions over a type that needs lifting are replaced
|
|
315 |
by bounded abstractions:
|
|
316 |
\<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P)
|
|
317 |
|
|
318 |
- equalities over the type being lifted are replaced by
|
|
319 |
corresponding relations:
|
|
320 |
A = B \<Longrightarrow> A \<approx> B
|
|
321 |
|
|
322 |
example with more complicated types of A, B:
|
|
323 |
A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A B
|
|
324 |
*)
|
|
325 |
|
404
|
326 |
ML {*
|
383
|
327 |
(* 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
|
328 |
fun mk_resp_arg lthy (rty, qty) =
|
319
|
329 |
let
|
|
330 |
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
|
331 |
in
|
334
|
332 |
if rty = qty
|
|
333 |
then HOLogic.eq_const rty
|
|
334 |
else
|
|
335 |
case (rty, qty) of
|
|
336 |
(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
|
337 |
if s = s'
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
338 |
then let
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
339 |
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
|
340 |
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
|
341 |
in
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
342 |
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
|
343 |
end
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
344 |
else let
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
345 |
val SOME qinfo = quotdata_lookup_thy thy s'
|
330
|
346 |
(* FIXME: check in this case that the rty and qty *)
|
|
347 |
(* 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
|
348 |
val (s, _) = dest_Const (#rel qinfo)
|
407
|
349 |
(* FIXME: the relation should only be the string *)
|
|
350 |
(* FIXME: and the type needs to be calculated as below; *)
|
|
351 |
(* FIXME: maybe one should actually have a term *)
|
|
352 |
(* FIXME: and one needs to force it to have this type *)
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
353 |
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
|
354 |
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
|
355 |
end
|
334
|
356 |
| _ => HOLogic.eq_const dummyT
|
351
|
357 |
(* 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
|
358 |
end
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
359 |
*}
|
239
|
360 |
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
361 |
ML {*
|
467
|
362 |
val mk_babs = Const (@{const_name Babs}, dummyT)
|
|
363 |
val mk_ball = Const (@{const_name Ball}, dummyT)
|
|
364 |
val mk_bex = Const (@{const_name Bex}, dummyT)
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
365 |
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
|
366 |
*}
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
367 |
|
323
|
368 |
ML {*
|
330
|
369 |
(* - applies f to the subterm of an abstraction, *)
|
|
370 |
(* otherwise to the given term, *)
|
405
|
371 |
(* - used by regularize, therefore abstracted *)
|
330
|
372 |
(* variables do not have to be treated specially *)
|
|
373 |
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
374 |
fun apply_subt f trm1 trm2 =
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
375 |
case (trm1, trm2) of
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
376 |
(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
|
377 |
| _ => f trm1 trm2
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
378 |
|
330
|
379 |
(* the major type of All and Ex quantifiers *)
|
334
|
380 |
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
|
381 |
*}
|
319
|
382 |
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
383 |
ML {*
|
330
|
384 |
(* produces a regularized version of rtm *)
|
|
385 |
(* - the result is still not completely typed *)
|
|
386 |
(* - does not need any special treatment of *)
|
|
387 |
(* bound variables *)
|
|
388 |
|
405
|
389 |
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
|
390 |
case (rtrm, qtrm) of
|
325
|
391 |
(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
|
392 |
let
|
405
|
393 |
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
|
394 |
in
|
325
|
395 |
if ty = ty'
|
|
396 |
then Abs (x, ty, subtrm)
|
326
|
397 |
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
|
398 |
end
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
399 |
| (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
|
400 |
let
|
405
|
401 |
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
|
402 |
in
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
403 |
if ty = ty'
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
404 |
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
|
405 |
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
|
406 |
end
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
407 |
| (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
|
408 |
let
|
405
|
409 |
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
|
410 |
in
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
411 |
if ty = ty'
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
412 |
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
|
413 |
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
|
414 |
end
|
351
|
415 |
(* FIXME: Should = only be replaced, when fully applied? *)
|
|
416 |
(* 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
|
417 |
| (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
|
418 |
let
|
405
|
419 |
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
|
420 |
in
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
421 |
if ty = ty'
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
422 |
then Const (@{const_name "op ="}, ty) $ subtrm
|
349
|
423 |
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
|
424 |
end
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
425 |
| (t1 $ t2, t1' $ t2') =>
|
405
|
426 |
(regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')
|
453
c22ab554a32d
started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
427 |
| (Free (x, ty), Free (x', ty')) =>
|
c22ab554a32d
started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
428 |
(* this case cannot arrise as we start with two fully atomized terms *)
|
c22ab554a32d
started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
429 |
raise (LIFT_MATCH "regularize (frees)")
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
430 |
| (Bound i, Bound i') =>
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
431 |
if i = i'
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
432 |
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
|
433 |
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
|
434 |
| (Const (s, ty), Const (s', ty')) =>
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
435 |
if s = s' andalso ty = ty'
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
436 |
then rtrm
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
437 |
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
|
438 |
| (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
|
439 |
raise (LIFT_MATCH "regularize (default)")
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
440 |
*}
|
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
441 |
|
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 |
(*
|
407
|
443 |
FIXME / TODO: needs to be adapted
|
|
444 |
|
383
|
445 |
To prove that the raw theorem implies the regularised one,
|
|
446 |
we try in order:
|
330
|
447 |
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
448 |
- 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
|
449 |
- Assumption
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
450 |
- 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
|
451 |
- 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
|
452 |
- 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
|
453 |
- (\<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
|
454 |
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
455 |
*)
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
456 |
|
442
7beed9b75ea2
renamed LAMBDA_RES_TAC and WEAK_LAMBDA_RES_TAC to lower case names
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
457 |
(* FIXME: they should be in in the new Isabelle *)
|
404
|
458 |
lemma [mono]:
|
|
459 |
"(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
|
400
|
460 |
by blast
|
|
461 |
|
|
462 |
lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
|
|
463 |
by auto
|
|
464 |
|
|
465 |
(* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *)
|
|
466 |
ML {*
|
|
467 |
fun equiv_tac rel_eqvs =
|
420
|
468 |
REPEAT_ALL_NEW (FIRST'
|
|
469 |
[resolve_tac rel_eqvs,
|
|
470 |
rtac @{thm IDENTITY_EQUIV},
|
|
471 |
rtac @{thm LIST_EQUIV}])
|
400
|
472 |
*}
|
|
473 |
|
|
474 |
ML {*
|
432
|
475 |
fun ball_reg_eqv_simproc rel_eqvs ss redex =
|
|
476 |
let
|
|
477 |
val ctxt = Simplifier.the_context ss
|
|
478 |
val thy = ProofContext.theory_of ctxt
|
|
479 |
in
|
|
480 |
case redex of
|
|
481 |
(ogl as ((Const (@{const_name "Ball"}, _)) $
|
|
482 |
((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
|
|
483 |
(let
|
|
484 |
val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;
|
|
485 |
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
|
|
486 |
val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
|
|
487 |
val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]);
|
|
488 |
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
|
|
489 |
in
|
|
490 |
SOME thm
|
|
491 |
end
|
|
492 |
handle _ => NONE
|
|
493 |
)
|
|
494 |
| _ => NONE
|
|
495 |
end
|
|
496 |
*}
|
|
497 |
|
|
498 |
ML {*
|
|
499 |
fun bex_reg_eqv_simproc rel_eqvs ss redex =
|
|
500 |
let
|
|
501 |
val ctxt = Simplifier.the_context ss
|
|
502 |
val thy = ProofContext.theory_of ctxt
|
|
503 |
in
|
|
504 |
case redex of
|
|
505 |
(ogl as ((Const (@{const_name "Bex"}, _)) $
|
|
506 |
((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
|
|
507 |
(let
|
|
508 |
val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;
|
|
509 |
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
|
|
510 |
val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
|
|
511 |
val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]);
|
|
512 |
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
|
|
513 |
in
|
|
514 |
SOME thm
|
|
515 |
end
|
|
516 |
handle _ => NONE
|
|
517 |
)
|
|
518 |
| _ => NONE
|
|
519 |
end
|
|
520 |
*}
|
|
521 |
|
|
522 |
ML {*
|
|
523 |
fun prep_trm thy (x, (T, t)) =
|
|
524 |
(cterm_of thy (Var (x, T)), cterm_of thy t)
|
|
525 |
|
|
526 |
fun prep_ty thy (x, (S, ty)) =
|
|
527 |
(ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
|
|
528 |
*}
|
|
529 |
|
|
530 |
ML {*
|
|
531 |
fun matching_prs thy pat trm =
|
|
532 |
let
|
|
533 |
val univ = Unify.matchers thy [(pat, trm)]
|
|
534 |
val SOME (env, _) = Seq.pull univ
|
|
535 |
val tenv = Vartab.dest (Envir.term_env env)
|
|
536 |
val tyenv = Vartab.dest (Envir.type_env env)
|
|
537 |
in
|
|
538 |
(map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
|
|
539 |
end
|
400
|
540 |
*}
|
|
541 |
|
|
542 |
ML {*
|
432
|
543 |
fun ball_reg_eqv_range_simproc rel_eqvs ss redex =
|
400
|
544 |
let
|
432
|
545 |
val ctxt = Simplifier.the_context ss
|
|
546 |
val thy = ProofContext.theory_of ctxt
|
400
|
547 |
in
|
432
|
548 |
case redex of
|
|
549 |
(ogl as ((Const (@{const_name "Ball"}, _)) $
|
|
550 |
((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>
|
|
551 |
(let
|
|
552 |
val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;
|
|
553 |
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
|
487
|
554 |
(* val _ = tracing (Syntax.string_of_term ctxt glc);*)
|
432
|
555 |
val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
|
|
556 |
val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]);
|
|
557 |
val R1c = cterm_of thy R1;
|
|
558 |
val thmi = Drule.instantiate' [] [SOME R1c] thm;
|
487
|
559 |
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi));*)
|
432
|
560 |
val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
|
|
561 |
val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
|
487
|
562 |
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); *)
|
432
|
563 |
in
|
|
564 |
SOME thm2
|
|
565 |
end
|
|
566 |
handle _ => NONE
|
|
567 |
|
|
568 |
)
|
|
569 |
| _ => NONE
|
400
|
570 |
end
|
|
571 |
*}
|
432
|
572 |
|
|
573 |
ML {*
|
|
574 |
fun bex_reg_eqv_range_simproc rel_eqvs ss redex =
|
|
575 |
let
|
|
576 |
val ctxt = Simplifier.the_context ss
|
|
577 |
val thy = ProofContext.theory_of ctxt
|
|
578 |
in
|
|
579 |
case redex of
|
|
580 |
(ogl as ((Const (@{const_name "Bex"}, _)) $
|
|
581 |
((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>
|
|
582 |
(let
|
|
583 |
val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;
|
|
584 |
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
|
487
|
585 |
(* val _ = tracing (Syntax.string_of_term ctxt glc); *)
|
432
|
586 |
val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
|
|
587 |
val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]);
|
|
588 |
val R1c = cterm_of thy R1;
|
|
589 |
val thmi = Drule.instantiate' [] [SOME R1c] thm;
|
|
590 |
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)
|
|
591 |
val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
|
|
592 |
val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
|
487
|
593 |
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));*)
|
432
|
594 |
in
|
|
595 |
SOME thm2
|
|
596 |
end
|
|
597 |
handle _ => NONE
|
|
598 |
|
|
599 |
)
|
|
600 |
| _ => NONE
|
|
601 |
end
|
|
602 |
*}
|
|
603 |
|
|
604 |
lemma eq_imp_rel: "EQUIV R \<Longrightarrow> a = b \<longrightarrow> R a b"
|
|
605 |
by (simp add: EQUIV_REFL)
|
|
606 |
|
|
607 |
ML {*
|
|
608 |
fun regularize_tac ctxt rel_eqvs =
|
|
609 |
let
|
|
610 |
val pat1 = [@{term "Ball (Respects R) P"}];
|
|
611 |
val pat2 = [@{term "Bex (Respects R) P"}];
|
|
612 |
val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}];
|
|
613 |
val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}];
|
|
614 |
val thy = ProofContext.theory_of ctxt
|
|
615 |
val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs))
|
|
616 |
val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc rel_eqvs))
|
|
617 |
val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs))
|
|
618 |
val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs))
|
|
619 |
val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4]
|
|
620 |
(* TODO: Make sure that there are no LIST_REL, PAIR_REL etc involved *)
|
|
621 |
val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) rel_eqvs
|
|
622 |
in
|
|
623 |
ObjectLogic.full_atomize_tac THEN'
|
|
624 |
simp_tac simp_ctxt THEN'
|
|
625 |
REPEAT_ALL_NEW (FIRST' [
|
|
626 |
rtac @{thm ball_reg_right},
|
|
627 |
rtac @{thm bex_reg_left},
|
|
628 |
resolve_tac (Inductive.get_monos ctxt),
|
|
629 |
rtac @{thm ball_all_comm},
|
|
630 |
rtac @{thm bex_ex_comm},
|
|
631 |
resolve_tac eq_eqvs,
|
|
632 |
simp_tac simp_ctxt
|
|
633 |
])
|
|
634 |
end
|
|
635 |
*}
|
390
|
636 |
|
|
637 |
section {* Injections of REP and ABSes *}
|
383
|
638 |
|
381
|
639 |
(*
|
|
640 |
Injecting REPABS means:
|
|
641 |
|
|
642 |
For abstractions:
|
|
643 |
* If the type of the abstraction doesn't need lifting we recurse.
|
|
644 |
* If it does we add RepAbs around the whole term and check if the
|
|
645 |
variable needs lifting.
|
|
646 |
* If it doesn't then we recurse
|
|
647 |
* If it does we recurse and put 'RepAbs' around all occurences
|
|
648 |
of the variable in the obtained subterm. This in combination
|
|
649 |
with the RepAbs above will let us change the type of the
|
|
650 |
abstraction with rewriting.
|
|
651 |
For applications:
|
|
652 |
* If the term is 'Respects' applied to anything we leave it unchanged
|
|
653 |
* If the term needs lifting and the head is a constant that we know
|
|
654 |
how to lift, we put a RepAbs and recurse
|
|
655 |
* If the term needs lifting and the head is a free applied to subterms
|
|
656 |
(if it is not applied we treated it in Abs branch) then we
|
|
657 |
put RepAbs and recurse
|
|
658 |
* Otherwise just recurse.
|
|
659 |
*)
|
|
660 |
|
336
|
661 |
ML {*
|
|
662 |
fun mk_repabs lthy (T, T') trm =
|
|
663 |
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
|
664 |
$ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
|
336
|
665 |
*}
|
|
666 |
|
|
667 |
ML {*
|
|
668 |
(* bound variables need to be treated properly, *)
|
|
669 |
(* as the type of subterms need to be calculated *)
|
|
670 |
|
408
|
671 |
fun inj_repabs_trm lthy (rtrm, qtrm) =
|
336
|
672 |
let
|
|
673 |
val rty = fastype_of rtrm
|
|
674 |
val qty = fastype_of qtrm
|
|
675 |
in
|
|
676 |
case (rtrm, qtrm) of
|
|
677 |
(Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
|
408
|
678 |
Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
|
336
|
679 |
| (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
|
408
|
680 |
Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
|
336
|
681 |
| (Const (@{const_name "Babs"}, T) $ r $ t, t') =>
|
408
|
682 |
Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
|
336
|
683 |
| (Abs (x, T, t), Abs (x', T', t')) =>
|
|
684 |
let
|
|
685 |
val (y, s) = Term.dest_abs (x, T, t)
|
|
686 |
val (_, s') = Term.dest_abs (x', T', t')
|
|
687 |
val yvar = Free (y, T)
|
453
c22ab554a32d
started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
688 |
val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))
|
336
|
689 |
in
|
345
|
690 |
if rty = qty
|
|
691 |
then result
|
|
692 |
else mk_repabs lthy (rty, qty) result
|
336
|
693 |
end
|
|
694 |
| _ =>
|
455
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
695 |
let
|
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
696 |
val (rhead, rargs) = strip_comb rtrm
|
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
697 |
val (qhead, qargs) = strip_comb qtrm
|
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
698 |
val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs)
|
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
699 |
in
|
464
|
700 |
case (rhead, qhead) of
|
|
701 |
(Const _, Const _) =>
|
455
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
702 |
if rty = qty
|
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
703 |
then list_comb (rhead, rargs')
|
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
704 |
else mk_repabs lthy (rty, qty) (list_comb (rhead, rargs'))
|
464
|
705 |
| (Free (x, T), Free (x', T')) =>
|
|
706 |
if T = T'
|
455
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
707 |
then list_comb (rhead, rargs')
|
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
708 |
else list_comb (mk_repabs lthy (T, T') rhead, rargs')
|
464
|
709 |
| (Abs _, Abs _) =>
|
455
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
710 |
list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')
|
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
711 |
| _ => raise (LIFT_MATCH "injection")
|
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
712 |
end
|
336
|
713 |
end
|
|
714 |
*}
|
|
715 |
|
404
|
716 |
section {* RepAbs Injection Tactic *}
|
387
|
717 |
|
|
718 |
ML {*
|
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
719 |
fun instantiate_tac thm =
|
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
720 |
Subgoal.FOCUS (fn {concl, ...} =>
|
387
|
721 |
let
|
|
722 |
val pat = Drule.strip_imp_concl (cprop_of thm)
|
481
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
723 |
val insts = Thm.first_order_match (pat, concl)
|
387
|
724 |
in
|
|
725 |
rtac (Drule.instantiate insts thm) 1
|
|
726 |
end
|
|
727 |
handle _ => no_tac)
|
|
728 |
*}
|
|
729 |
|
|
730 |
ML {*
|
468
|
731 |
fun quotient_tac ctxt quot_thms =
|
|
732 |
REPEAT_ALL_NEW (FIRST'
|
420
|
733 |
[rtac @{thm FUN_QUOTIENT},
|
|
734 |
resolve_tac quot_thms,
|
|
735 |
rtac @{thm IDENTITY_QUOTIENT},
|
485
4efb104514f7
More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
736 |
rtac @{thm LIST_QUOTIENT},
|
420
|
737 |
(* For functional identity quotients, (op = ---> op =) *)
|
|
738 |
(* TODO: think about the other way around, if we need to shorten the relation *)
|
468
|
739 |
CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))])
|
387
|
740 |
*}
|
|
741 |
|
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
742 |
lemma FUN_REL_I:
|
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
743 |
assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
|
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
744 |
shows "(R1 ===> R2) f g"
|
466
|
745 |
using a by simp
|
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
746 |
|
387
|
747 |
ML {*
|
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
748 |
val lambda_rsp_tac =
|
472
|
749 |
SUBGOAL (fn (goal, i) =>
|
475
|
750 |
case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
|
472
|
751 |
(_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} i
|
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
752 |
| _ => no_tac)
|
387
|
753 |
*}
|
|
754 |
|
|
755 |
ML {*
|
434
|
756 |
val ball_rsp_tac =
|
472
|
757 |
SUBGOAL (fn (goal, i) =>
|
475
|
758 |
case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
|
448
|
759 |
(_ $ (Const (@{const_name Ball}, _) $ _)
|
473
|
760 |
$ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} i
|
434
|
761 |
|_ => no_tac)
|
|
762 |
*}
|
|
763 |
|
|
764 |
ML {*
|
|
765 |
val bex_rsp_tac =
|
472
|
766 |
SUBGOAL (fn (goal, i) =>
|
475
|
767 |
case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
|
448
|
768 |
(_ $ (Const (@{const_name Bex}, _) $ _)
|
473
|
769 |
$ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} i
|
434
|
770 |
| _ => no_tac)
|
|
771 |
*}
|
|
772 |
|
480
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
773 |
definition
|
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
774 |
"QUOT_TRUE x \<equiv> True"
|
472
|
775 |
|
387
|
776 |
ML {*
|
480
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
777 |
fun find_qt_asm asms =
|
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
778 |
let
|
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
779 |
fun find_fun trm =
|
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
780 |
case trm of
|
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
781 |
(Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true
|
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
782 |
| _ => false
|
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
783 |
in
|
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
784 |
case find_first find_fun asms of
|
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
785 |
SOME (_ $ (_ $ (f $ a))) => (f, a)
|
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
786 |
| _ => error "find_qt_asm"
|
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
787 |
end
|
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
788 |
*}
|
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
789 |
|
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
790 |
ML {*
|
495
|
791 |
val APPLY_RSP_TAC =
|
482
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
792 |
Subgoal.FOCUS (fn {concl, asms, context,...} =>
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
793 |
case ((HOLogic.dest_Trueprop (term_of concl))) of
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
794 |
((R2 $ (f $ x) $ (g $ y))) =>
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
795 |
let
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
796 |
val (asmf, asma) = find_qt_asm (map term_of asms);
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
797 |
in
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
798 |
if (fastype_of asmf) = (fastype_of f) then no_tac else let
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
799 |
val ty_a = fastype_of x;
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
800 |
val ty_b = fastype_of asma;
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
801 |
val ty_c = range_type (type_of f);
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
802 |
val ty_d = range_type (type_of asmf);
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
803 |
val thy = ProofContext.theory_of context;
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
804 |
val ty_inst = map (fn x => SOME (ctyp_of thy x)) [ty_a, ty_b, ty_c, ty_d];
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
805 |
val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y];
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
806 |
val t_inst = [NONE, NONE, NONE, SOME R2, NONE, NONE, SOME f, SOME g, SOME x, SOME y];
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
807 |
val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP}
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
808 |
(*val _ = tracing (Syntax.string_of_term @{context} (prop_of thm))*)
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
809 |
in
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
810 |
rtac thm 1
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
811 |
end
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
812 |
end
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
813 |
| _ => no_tac)
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
814 |
*}
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
815 |
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
816 |
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
817 |
ML {*
|
432
|
818 |
fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
|
|
819 |
*}
|
|
820 |
|
398
|
821 |
(*
|
|
822 |
To prove that the regularised theorem implies the abs/rep injected,
|
|
823 |
we try:
|
|
824 |
|
|
825 |
1) theorems 'trans2' from the appropriate QUOT_TYPE
|
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
826 |
2) remove lambdas from both sides: lambda_rsp_tac
|
398
|
827 |
3) remove Ball/Bex from the right hand side
|
|
828 |
4) use user-supplied RSP theorems
|
|
829 |
5) remove rep_abs from the right side
|
|
830 |
6) reflexivity of equality
|
|
831 |
7) split applications of lifted type (apply_rsp)
|
|
832 |
8) split applications of non-lifted type (cong_tac)
|
|
833 |
9) apply extentionality
|
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
834 |
A) reflexivity of the relation
|
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
835 |
B) assumption
|
398
|
836 |
(Lambdas under respects may have left us some assumptions)
|
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
837 |
C) proving obvious higher order equalities by simplifying fun_rel
|
398
|
838 |
(not sure if it is still needed?)
|
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
839 |
D) unfolding lambda on one side
|
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
840 |
E) simplifying (= ===> =) for simpler respectfulness
|
398
|
841 |
|
|
842 |
*)
|
|
843 |
|
469
|
844 |
lemma quot_true_dests:
|
|
845 |
shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
|
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
846 |
and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
|
469
|
847 |
and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))"
|
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
848 |
and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
849 |
apply(simp_all add: QUOT_TRUE_def ext)
|
469
|
850 |
done
|
|
851 |
|
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
852 |
lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P"
|
470
fc16faef5dfa
Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
853 |
by (simp add: QUOT_TRUE_def)
|
fc16faef5dfa
Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
854 |
|
479
|
855 |
lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
|
470
fc16faef5dfa
Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
856 |
by (simp add: QUOT_TRUE_def)
|
fc16faef5dfa
Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
857 |
|
fc16faef5dfa
Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
858 |
ML {*
|
479
|
859 |
fun quot_true_conv1 ctxt fnctn ctrm =
|
|
860 |
case (term_of ctrm) of
|
|
861 |
(Const (@{const_name QUOT_TRUE}, _) $ x) =>
|
|
862 |
let
|
|
863 |
val fx = fnctn x;
|
|
864 |
val thy = ProofContext.theory_of ctxt;
|
|
865 |
val cx = cterm_of thy x;
|
|
866 |
val cfx = cterm_of thy fx;
|
|
867 |
val cxt = ctyp_of thy (fastype_of x);
|
|
868 |
val cfxt = ctyp_of thy (fastype_of fx);
|
|
869 |
val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp}
|
|
870 |
in
|
|
871 |
Conv.rewr_conv thm ctrm
|
|
872 |
end
|
470
fc16faef5dfa
Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
873 |
*}
|
469
|
874 |
|
479
|
875 |
ML {*
|
|
876 |
fun quot_true_conv ctxt fnctn ctrm =
|
|
877 |
case (term_of ctrm) of
|
|
878 |
(Const (@{const_name QUOT_TRUE}, _) $ _) =>
|
|
879 |
quot_true_conv1 ctxt fnctn ctrm
|
|
880 |
| _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
|
|
881 |
| Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
|
|
882 |
| _ => Conv.all_conv ctrm
|
|
883 |
*}
|
|
884 |
|
|
885 |
ML {*
|
493
|
886 |
fun quot_true_tac ctxt fnctn = CONVERSION
|
|
887 |
((Conv.params_conv ~1 (fn ctxt =>
|
|
888 |
(Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
|
479
|
889 |
*}
|
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
890 |
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
891 |
ML {* fun dest_comb (f $ a) = (f, a) *}
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
892 |
ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *}
|
481
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
893 |
(* TODO: Can this be done easier? *)
|
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
894 |
ML {*
|
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
895 |
fun unlam t =
|
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
896 |
case t of
|
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
897 |
(Abs a) => snd (Term.dest_abs a)
|
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
898 |
| _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) *}
|
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
899 |
|
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
900 |
|
443
|
901 |
ML {*
|
489
|
902 |
fun inj_repabs_tac ctxt quot_thms rel_refl trans2 =
|
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
903 |
(FIRST' [
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
904 |
(* "cong" rule of the of the relation / transitivity*)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
905 |
(* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
|
482
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
906 |
NDT ctxt "1" (resolve_tac trans2 THEN' RANGE [
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
907 |
quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]),
|
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
908 |
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
909 |
(* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
910 |
NDT ctxt "2" (lambda_rsp_tac THEN' quot_true_tac ctxt unlam),
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
911 |
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
912 |
(* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
913 |
NDT ctxt "3" (rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}),
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
914 |
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
915 |
(* R2 is always equality *)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
916 |
(* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
917 |
NDT ctxt "4" (ball_rsp_tac THEN' quot_true_tac ctxt unlam),
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
918 |
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
919 |
(* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
920 |
NDT ctxt "5" (rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}),
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
921 |
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
922 |
(* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
923 |
NDT ctxt "6" (bex_rsp_tac THEN' dtac @{thm QT_ext}),
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
924 |
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
925 |
(* respectfulness of constants *)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
926 |
NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
927 |
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
928 |
(* reflexivity of operators arising from Cong_tac *)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
929 |
NDT ctxt "8" (rtac @{thm refl}),
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
930 |
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
931 |
(* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
932 |
(* observe ---> *)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
933 |
NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
934 |
THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))),
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
935 |
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
936 |
(* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *)
|
495
|
937 |
NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN'
|
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
938 |
(RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms),
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
939 |
quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
940 |
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
941 |
(* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
942 |
(* merge with previous tactic *)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
943 |
NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
944 |
(RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
945 |
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
946 |
(* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
947 |
NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
948 |
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
949 |
(* reflexivity of the basic relations *)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
950 |
(* R \<dots> \<dots> *)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
951 |
NDT ctxt "D" (resolve_tac rel_refl),
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
952 |
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
953 |
(* resolving with R x y assumptions *)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
954 |
NDT ctxt "E" (atac),
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
955 |
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
956 |
(* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
957 |
(* global simplification *)
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
958 |
NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
959 |
*}
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
960 |
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
961 |
ML {*
|
489
|
962 |
fun all_inj_repabs_tac ctxt quot_thms rel_refl trans2 =
|
|
963 |
REPEAT_ALL_NEW (inj_repabs_tac ctxt quot_thms rel_refl trans2)
|
398
|
964 |
*}
|
|
965 |
|
399
|
966 |
section {* Cleaning of the theorem *}
|
387
|
967 |
|
389
|
968 |
|
462
|
969 |
(* TODO: This is slow *)
|
389
|
970 |
ML {*
|
468
|
971 |
fun allex_prs_tac ctxt quot =
|
|
972 |
(EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt quot)
|
387
|
973 |
*}
|
|
974 |
|
|
975 |
ML {*
|
440
|
976 |
fun make_inst lhs t =
|
|
977 |
let
|
|
978 |
val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
|
|
979 |
val _ $ (Abs (_, _, g)) = t;
|
|
980 |
fun mk_abs i t =
|
|
981 |
if incr_boundvars i u aconv t then Bound i
|
|
982 |
else (case t of
|
|
983 |
t1 $ t2 => mk_abs i t1 $ mk_abs i t2
|
469
|
984 |
| Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')
|
440
|
985 |
| Bound j => if i = j then error "make_inst" else t
|
|
986 |
| _ => t);
|
|
987 |
in (f, Abs ("x", T, mk_abs 0 g)) end;
|
490
|
988 |
*}
|
440
|
989 |
|
492
|
990 |
(* It proves the QUOTIENT assumptions by calling quotient_tac *)
|
490
|
991 |
ML {*
|
492
|
992 |
fun solve_quotient_assum i quot_thms ctxt thm =
|
|
993 |
let
|
|
994 |
val tac =
|
|
995 |
(compose_tac (false, thm, i)) THEN_ALL_NEW
|
|
996 |
(quotient_tac ctxt quot_thms);
|
|
997 |
val gc = Drule.strip_imp_concl (cprop_of thm);
|
|
998 |
in
|
|
999 |
Goal.prove_internal [] gc (fn _ => tac 1)
|
|
1000 |
end
|
|
1001 |
handle _ => error "solve_quotient_assum"
|
|
1002 |
*}
|
|
1003 |
|
|
1004 |
ML {*
|
|
1005 |
fun lambda_allex_prs_simple_conv quot_thms ctxt ctrm =
|
|
1006 |
case (term_of ctrm) of
|
|
1007 |
((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
|
387
|
1008 |
let
|
|
1009 |
val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);
|
|
1010 |
val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2);
|
|
1011 |
val thy = ProofContext.theory_of ctxt;
|
|
1012 |
val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
|
|
1013 |
val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d];
|
|
1014 |
val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
|
|
1015 |
val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};
|
492
|
1016 |
val te = @{thm eq_reflection} OF [solve_quotient_assum 2 quot_thms ctxt lpi]
|
415
|
1017 |
val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
|
440
|
1018 |
val tl = Thm.lhs_of ts;
|
|
1019 |
val (insp, inst) = make_inst (term_of tl) (term_of ctrm);
|
|
1020 |
val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts;
|
492
|
1021 |
in
|
|
1022 |
Conv.rewr_conv ti ctrm
|
|
1023 |
end
|
|
1024 |
| (Const (@{const_name Ball}, _) $ (Const (@{const_name Respects}, _) $ R) $
|
|
1025 |
(((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) =>
|
|
1026 |
let
|
|
1027 |
val (_, [ty_a, ty_b]) = dest_Type (fastype_of absf);
|
|
1028 |
val thy = ProofContext.theory_of ctxt;
|
|
1029 |
val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b);
|
|
1030 |
val tyinst = [SOME cty_a, SOME cty_b];
|
|
1031 |
val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)];
|
|
1032 |
val thm = Drule.instantiate' tyinst tinst @{thm all_prs};
|
|
1033 |
val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 quot_thms ctxt thm];
|
|
1034 |
in
|
|
1035 |
Conv.rewr_conv ti ctrm
|
|
1036 |
end
|
|
1037 |
| (Const (@{const_name Bex}, _) $ (Const (@{const_name Respects}, _) $ R) $
|
|
1038 |
(((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) =>
|
|
1039 |
let
|
|
1040 |
val (_, [ty_a, ty_b]) = dest_Type (fastype_of absf);
|
|
1041 |
val thy = ProofContext.theory_of ctxt;
|
|
1042 |
val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b);
|
|
1043 |
val tyinst = [SOME cty_a, SOME cty_b];
|
|
1044 |
val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)];
|
|
1045 |
val thm = Drule.instantiate' tyinst tinst @{thm ex_prs};
|
|
1046 |
val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 quot_thms ctxt thm];
|
387
|
1047 |
in
|
|
1048 |
Conv.rewr_conv ti ctrm
|
|
1049 |
end
|
490
|
1050 |
| _ => Conv.all_conv ctrm
|
387
|
1051 |
*}
|
|
1052 |
|
440
|
1053 |
(* quot stands for the QUOTIENT theorems: *)
|
387
|
1054 |
(* could be potentially all of them *)
|
|
1055 |
ML {*
|
492
|
1056 |
fun lambda_allex_prs_conv quot =
|
|
1057 |
More_Conv.top_conv (lambda_allex_prs_simple_conv quot)
|
387
|
1058 |
*}
|
|
1059 |
|
|
1060 |
ML {*
|
492
|
1061 |
fun lambda_allex_prs_tac quot ctxt = CONVERSION (lambda_allex_prs_conv quot ctxt)
|
387
|
1062 |
*}
|
|
1063 |
|
457
|
1064 |
(*
|
465
|
1065 |
Cleaning the theorem consists of 6 kinds of rewrites.
|
|
1066 |
The first two need to be done before fun_map is unfolded
|
457
|
1067 |
|
|
1068 |
- LAMBDA_PRS:
|
469
|
1069 |
(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f
|
|
1070 |
|
465
|
1071 |
- FORALL_PRS (and the same for exists: EXISTS_PRS)
|
469
|
1072 |
\<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f
|
|
1073 |
|
457
|
1074 |
- Rewriting with definitions from the argument defs
|
469
|
1075 |
NewConst ----> (rep ---> abs) oldConst
|
|
1076 |
|
457
|
1077 |
- QUOTIENT_REL_REP:
|
469
|
1078 |
Rel (Rep x) (Rep y) ----> x = y
|
|
1079 |
|
465
|
1080 |
- ABS_REP
|
469
|
1081 |
Abs (Rep x) ----> x
|
|
1082 |
|
465
|
1083 |
- id_simps; fun_map.simps
|
457
|
1084 |
|
|
1085 |
The first one is implemented as a conversion (fast).
|
465
|
1086 |
The second one is an EqSubst (slow).
|
|
1087 |
The rest are a simp_tac and are fast.
|
457
|
1088 |
*)
|
469
|
1089 |
|
387
|
1090 |
ML {*
|
498
|
1091 |
fun clean_tac lthy quot =
|
387
|
1092 |
let
|
498
|
1093 |
val thy = ProofContext.theory_of lthy;
|
|
1094 |
val defs = map (#def) (qconsts_dest thy);
|
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1095 |
val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot
|
462
|
1096 |
val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep;
|
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1097 |
val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
|
440
|
1098 |
val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
|
462
|
1099 |
val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps
|
|
1100 |
(@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)
|
387
|
1101 |
in
|
490
|
1102 |
EVERY' [
|
|
1103 |
(* (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f *)
|
492
|
1104 |
(* \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f *)
|
|
1105 |
NDT lthy "a" (TRY o lambda_allex_prs_tac quot lthy),
|
490
|
1106 |
|
|
1107 |
(* NewConst ----> (rep ---> abs) oldConst *)
|
|
1108 |
(* Abs (Rep x) ----> x *)
|
|
1109 |
(* id_simps; fun_map.simps *)
|
492
|
1110 |
NDT lthy "c" (TRY o simp_tac simp_ctxt),
|
490
|
1111 |
|
|
1112 |
(* final step *)
|
492
|
1113 |
NDT lthy "d" (TRY o rtac refl)
|
490
|
1114 |
]
|
387
|
1115 |
end
|
|
1116 |
*}
|
381
|
1117 |
|
404
|
1118 |
section {* Genralisation of free variables in a goal *}
|
347
|
1119 |
|
|
1120 |
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
|
1121 |
fun inst_spec ctrm =
|
411
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1122 |
Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
|
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 |
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1124 |
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
|
1125 |
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
|
1126 |
|
412
|
1127 |
fun all_list xs trm =
|
411
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1128 |
fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
|
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1129 |
|
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1130 |
fun apply_under_Trueprop f =
|
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1131 |
HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
|
362
|
1132 |
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1133 |
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
|
1134 |
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
|
1135 |
let
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1136 |
val thy = ProofContext.theory_of ctxt
|
411
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1137 |
val vrs = Term.add_frees concl []
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1138 |
val cvrs = map (cterm_of thy o Free) vrs
|
412
|
1139 |
val concl' = apply_under_Trueprop (all_list vrs) concl
|
411
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1140 |
val goal = Logic.mk_implies (concl', concl)
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1141 |
val rule = Goal.prove ctxt [] [] goal
|
411
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1142 |
(K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1143 |
in
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1144 |
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
|
1145 |
end)
|
362
|
1146 |
*}
|
|
1147 |
|
402
|
1148 |
section {* General outline of the lifting procedure *}
|
|
1149 |
|
383
|
1150 |
(* - A is the original raw theorem *)
|
|
1151 |
(* - B is the regularized theorem *)
|
|
1152 |
(* - C is the rep/abs injected version of B *)
|
|
1153 |
(* - D is the lifted theorem *)
|
|
1154 |
(* *)
|
|
1155 |
(* - b is the regularization step *)
|
|
1156 |
(* - c is the rep/abs injection step *)
|
|
1157 |
(* - d is the cleaning part *)
|
|
1158 |
|
413
|
1159 |
lemma lifting_procedure:
|
360
|
1160 |
assumes a: "A"
|
|
1161 |
and b: "A \<Longrightarrow> B"
|
|
1162 |
and c: "B = C"
|
|
1163 |
and d: "C = D"
|
|
1164 |
shows "D"
|
|
1165 |
using a b c d
|
|
1166 |
by simp
|
|
1167 |
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1168 |
ML {*
|
412
|
1169 |
fun lift_match_error ctxt fun_str rtrm qtrm =
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1170 |
let
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1171 |
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
|
1172 |
val qtrm_str = Syntax.string_of_term ctxt qtrm
|
388
|
1173 |
val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str,
|
|
1174 |
"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
|
1175 |
in
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1176 |
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
|
1177 |
end
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1178 |
*}
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1179 |
|
360
|
1180 |
ML {*
|
|
1181 |
fun procedure_inst ctxt rtrm qtrm =
|
|
1182 |
let
|
|
1183 |
val thy = ProofContext.theory_of ctxt
|
|
1184 |
val rtrm' = HOLogic.dest_Trueprop rtrm
|
|
1185 |
val qtrm' = HOLogic.dest_Trueprop qtrm
|
383
|
1186 |
val reg_goal =
|
405
|
1187 |
Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')
|
412
|
1188 |
handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
|
383
|
1189 |
val inj_goal =
|
408
|
1190 |
Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))
|
412
|
1191 |
handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
|
360
|
1192 |
in
|
|
1193 |
Drule.instantiate' []
|
|
1194 |
[SOME (cterm_of thy rtrm'),
|
|
1195 |
SOME (cterm_of thy reg_goal),
|
413
|
1196 |
SOME (cterm_of thy inj_goal)] @{thm lifting_procedure}
|
360
|
1197 |
end
|
362
|
1198 |
*}
|
389
|
1199 |
|
|
1200 |
(* Left for debugging *)
|
362
|
1201 |
ML {*
|
389
|
1202 |
fun procedure_tac lthy rthm =
|
|
1203 |
ObjectLogic.full_atomize_tac
|
|
1204 |
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
|
1205 |
THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
|
389
|
1206 |
let
|
|
1207 |
val rthm' = atomize_thm rthm
|
|
1208 |
val rule = procedure_inst context (prop_of rthm') (term_of concl)
|
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1209 |
val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i}
|
389
|
1210 |
in
|
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1211 |
EVERY1 [rtac rule, rtac rthm'] THEN RANGE [(fn _ => all_tac), rtac thm] 1
|
412
|
1212 |
end) lthy
|
360
|
1213 |
*}
|
|
1214 |
|
361
|
1215 |
ML {*
|
413
|
1216 |
(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
|
489
|
1217 |
|
498
|
1218 |
fun lift_tac lthy rthm rel_eqv quot =
|
389
|
1219 |
ObjectLogic.full_atomize_tac
|
|
1220 |
THEN' gen_frees_tac lthy
|
|
1221 |
THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
|
|
1222 |
let
|
|
1223 |
val rthm' = atomize_thm rthm
|
|
1224 |
val rule = procedure_inst context (prop_of rthm') (term_of concl)
|
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1225 |
val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
|
419
|
1226 |
val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv
|
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1227 |
val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i}
|
389
|
1228 |
in
|
432
|
1229 |
EVERY1
|
|
1230 |
[rtac rule,
|
413
|
1231 |
RANGE [rtac rthm',
|
432
|
1232 |
regularize_tac lthy rel_eqv,
|
489
|
1233 |
rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2,
|
498
|
1234 |
clean_tac lthy quot]]
|
412
|
1235 |
end) lthy
|
361
|
1236 |
*}
|
|
1237 |
|
198
|
1238 |
end
|
239
|
1239 |
|