466
|
1 |
(* Code for getting the goal *)
|
|
2 |
apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
|
|
3 |
ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
|
|
4 |
|
|
5 |
|
467
|
6 |
section {* Infrastructure about definitions *}
|
|
7 |
|
|
8 |
(* Does the same as 'subst' in a given theorem *)
|
|
9 |
ML {*
|
|
10 |
fun eqsubst_thm ctxt thms thm =
|
|
11 |
let
|
|
12 |
val goalstate = Goal.init (Thm.cprop_of thm)
|
|
13 |
val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
|
|
14 |
NONE => error "eqsubst_thm"
|
|
15 |
| SOME th => cprem_of th 1
|
|
16 |
val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
|
|
17 |
val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a');
|
|
18 |
val cgoal = cterm_of (ProofContext.theory_of ctxt) goal
|
|
19 |
val rt = Goal.prove_internal [] cgoal (fn _ => tac);
|
|
20 |
in
|
|
21 |
@{thm equal_elim_rule1} OF [rt, thm]
|
|
22 |
end
|
|
23 |
*}
|
|
24 |
|
|
25 |
(* expects atomized definitions *)
|
|
26 |
ML {*
|
|
27 |
fun add_lower_defs_aux lthy thm =
|
|
28 |
let
|
|
29 |
val e1 = @{thm fun_cong} OF [thm];
|
|
30 |
val f = eqsubst_thm lthy @{thms fun_map.simps} e1;
|
|
31 |
val g = simp_ids f
|
|
32 |
in
|
|
33 |
(simp_ids thm) :: (add_lower_defs_aux lthy g)
|
|
34 |
end
|
|
35 |
handle _ => [simp_ids thm]
|
|
36 |
*}
|
|
37 |
|
|
38 |
ML {*
|
|
39 |
fun add_lower_defs lthy def =
|
|
40 |
let
|
|
41 |
val def_pre_sym = symmetric def
|
|
42 |
val def_atom = atomize_thm def_pre_sym
|
|
43 |
val defs_all = add_lower_defs_aux lthy def_atom
|
|
44 |
in
|
|
45 |
map Thm.varifyT defs_all
|
|
46 |
end
|
|
47 |
*}
|
|
48 |
|
|
49 |
|
|
50 |
|
381
|
51 |
ML {*
|
|
52 |
fun repeat_eqsubst_thm ctxt thms thm =
|
|
53 |
repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)
|
|
54 |
handle _ => thm
|
|
55 |
*}
|
|
56 |
|
|
57 |
|
|
58 |
ML {*
|
|
59 |
fun eqsubst_prop ctxt thms t =
|
|
60 |
let
|
|
61 |
val goalstate = Goal.init (cterm_of (ProofContext.theory_of ctxt) t)
|
|
62 |
val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
|
|
63 |
NONE => error "eqsubst_prop"
|
|
64 |
| SOME th => cprem_of th 1
|
|
65 |
in term_of a' end
|
|
66 |
*}
|
|
67 |
|
|
68 |
ML {*
|
|
69 |
fun repeat_eqsubst_prop ctxt thms t =
|
|
70 |
repeat_eqsubst_prop ctxt thms (eqsubst_prop ctxt thms t)
|
|
71 |
handle _ => t
|
|
72 |
*}
|
|
73 |
|
379
|
74 |
|
|
75 |
text {* tyRel takes a type and builds a relation that a quantifier over this
|
|
76 |
type needs to respect. *}
|
|
77 |
ML {*
|
|
78 |
fun tyRel ty rty rel lthy =
|
|
79 |
if Sign.typ_instance (ProofContext.theory_of lthy) (ty, rty)
|
|
80 |
then rel
|
|
81 |
else (case ty of
|
|
82 |
Type (s, tys) =>
|
|
83 |
let
|
|
84 |
val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
|
|
85 |
val ty_out = ty --> ty --> @{typ bool};
|
|
86 |
val tys_out = tys_rel ---> ty_out;
|
|
87 |
in
|
|
88 |
(case (maps_lookup (ProofContext.theory_of lthy) s) of
|
|
89 |
SOME (info) => list_comb (Const (#relfun info, tys_out),
|
|
90 |
map (fn ty => tyRel ty rty rel lthy) tys)
|
|
91 |
| NONE => HOLogic.eq_const ty
|
|
92 |
)
|
|
93 |
end
|
|
94 |
| _ => HOLogic.eq_const ty)
|
|
95 |
*}
|
|
96 |
|
|
97 |
(*
|
|
98 |
ML {* cterm_of @{theory}
|
|
99 |
(tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"})
|
|
100 |
@{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context})
|
|
101 |
*}
|
|
102 |
*)
|
|
103 |
|
|
104 |
|
|
105 |
ML {*
|
|
106 |
fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)
|
|
107 |
fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
|
|
108 |
fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
|
|
109 |
fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})
|
|
110 |
*}
|
|
111 |
|
|
112 |
(* applies f to the subterm of an abstractions, otherwise to the given term *)
|
|
113 |
ML {*
|
|
114 |
fun apply_subt f trm =
|
|
115 |
case trm of
|
|
116 |
Abs (x, T, t) =>
|
|
117 |
let
|
|
118 |
val (x', t') = Term.dest_abs (x, T, t)
|
|
119 |
in
|
|
120 |
Term.absfree (x', T, f t')
|
|
121 |
end
|
|
122 |
| _ => f trm
|
|
123 |
*}
|
|
124 |
|
|
125 |
|
|
126 |
|
|
127 |
(* FIXME: if there are more than one quotient, then you have to look up the relation *)
|
|
128 |
ML {*
|
|
129 |
fun my_reg lthy rel rty trm =
|
|
130 |
case trm of
|
|
131 |
Abs (x, T, t) =>
|
|
132 |
if (needs_lift rty T) then
|
|
133 |
let
|
|
134 |
val rrel = tyRel T rty rel lthy
|
|
135 |
in
|
|
136 |
(mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm)
|
|
137 |
end
|
|
138 |
else
|
|
139 |
Abs(x, T, (apply_subt (my_reg lthy rel rty) t))
|
|
140 |
| Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) =>
|
|
141 |
let
|
|
142 |
val ty1 = domain_type ty
|
|
143 |
val ty2 = domain_type ty1
|
|
144 |
val rrel = tyRel T rty rel lthy
|
|
145 |
in
|
|
146 |
if (needs_lift rty T) then
|
|
147 |
(mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
|
|
148 |
else
|
|
149 |
Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t
|
|
150 |
end
|
|
151 |
| Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) =>
|
|
152 |
let
|
|
153 |
val ty1 = domain_type ty
|
|
154 |
val ty2 = domain_type ty1
|
|
155 |
val rrel = tyRel T rty rel lthy
|
|
156 |
in
|
|
157 |
if (needs_lift rty T) then
|
|
158 |
(mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
|
|
159 |
else
|
|
160 |
Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t
|
|
161 |
end
|
|
162 |
| Const (@{const_name "op ="}, ty) $ t =>
|
|
163 |
if needs_lift rty (fastype_of t) then
|
|
164 |
(tyRel (fastype_of t) rty rel lthy) $ t (* FIXME: t should be regularised too *)
|
|
165 |
else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t)
|
|
166 |
| t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)
|
|
167 |
| _ => trm
|
|
168 |
*}
|
|
169 |
|
|
170 |
(* For polymorphic types we need to find the type of the Relation term. *)
|
|
171 |
(* TODO: we assume that the relation is a Constant. Is this always true? *)
|
|
172 |
ML {*
|
|
173 |
fun my_reg_inst lthy rel rty trm =
|
|
174 |
case rel of
|
|
175 |
Const (n, _) => Syntax.check_term lthy
|
|
176 |
(my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm)
|
|
177 |
*}
|
|
178 |
|
|
179 |
(*
|
|
180 |
ML {*
|
|
181 |
val r = Free ("R", dummyT);
|
|
182 |
val t = (my_reg_inst @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"});
|
|
183 |
val t2 = Syntax.check_term @{context} t;
|
|
184 |
cterm_of @{theory} t2
|
|
185 |
*}
|
|
186 |
*)
|
|
187 |
|
|
188 |
text {* Assumes that the given theorem is atomized *}
|
|
189 |
ML {*
|
|
190 |
fun build_regularize_goal thm rty rel lthy =
|
|
191 |
Logic.mk_implies
|
|
192 |
((prop_of thm),
|
|
193 |
(my_reg_inst lthy rel rty (prop_of thm)))
|
|
194 |
*}
|
|
195 |
|
|
196 |
ML {*
|
|
197 |
fun regularize thm rty rel rel_eqv rel_refl lthy =
|
|
198 |
let
|
|
199 |
val goal = build_regularize_goal thm rty rel lthy;
|
|
200 |
fun tac ctxt =
|
|
201 |
(ObjectLogic.full_atomize_tac) THEN'
|
|
202 |
REPEAT_ALL_NEW (FIRST' [
|
|
203 |
rtac rel_refl,
|
|
204 |
atac,
|
|
205 |
rtac @{thm universal_twice},
|
|
206 |
(rtac @{thm impI} THEN' atac),
|
|
207 |
rtac @{thm implication_twice},
|
|
208 |
EqSubst.eqsubst_tac ctxt [0]
|
|
209 |
[(@{thm equiv_res_forall} OF [rel_eqv]),
|
|
210 |
(@{thm equiv_res_exists} OF [rel_eqv])],
|
|
211 |
(* For a = b \<longrightarrow> a \<approx> b *)
|
|
212 |
(rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
|
|
213 |
(rtac @{thm RIGHT_RES_FORALL_REGULAR})
|
|
214 |
]);
|
|
215 |
val cthm = Goal.prove lthy [] [] goal
|
|
216 |
(fn {context, ...} => tac context 1);
|
|
217 |
in
|
|
218 |
cthm OF [thm]
|
|
219 |
end
|
|
220 |
*}
|
|
221 |
|
|
222 |
(*consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
|
|
223 |
axioms Rl_eq: "EQUIV Rl"
|
|
224 |
|
|
225 |
quotient ql = "'a list" / "Rl"
|
|
226 |
by (rule Rl_eq)
|
|
227 |
ML {*
|
|
228 |
ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"});
|
|
229 |
ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"})
|
|
230 |
*}
|
|
231 |
*)
|
|
232 |
|
|
233 |
ML {*
|
|
234 |
(* returns all subterms where two types differ *)
|
|
235 |
fun diff (T, S) Ds =
|
|
236 |
case (T, S) of
|
|
237 |
(TVar v, TVar u) => if v = u then Ds else (T, S)::Ds
|
|
238 |
| (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds
|
|
239 |
| (Type (a, Ts), Type (b, Us)) =>
|
|
240 |
if a = b then diffs (Ts, Us) Ds else (T, S)::Ds
|
|
241 |
| _ => (T, S)::Ds
|
|
242 |
and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds)
|
|
243 |
| diffs ([], []) Ds = Ds
|
|
244 |
| diffs _ _ = error "Unequal length of type arguments"
|
|
245 |
|
|
246 |
*}
|
|
247 |
|
|
248 |
ML {*
|
|
249 |
fun build_repabs_term lthy thm consts rty qty =
|
|
250 |
let
|
|
251 |
(* TODO: The rty and qty stored in the quotient_info should
|
|
252 |
be varified, so this will soon not be needed *)
|
|
253 |
val rty = Logic.varifyT rty;
|
|
254 |
val qty = Logic.varifyT qty;
|
|
255 |
|
|
256 |
fun mk_abs tm =
|
|
257 |
let
|
|
258 |
val ty = fastype_of tm
|
|
259 |
in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end
|
|
260 |
fun mk_repabs tm =
|
|
261 |
let
|
|
262 |
val ty = fastype_of tm
|
|
263 |
in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end
|
|
264 |
|
|
265 |
fun is_lifted_const (Const (x, _)) = member (op =) consts x
|
|
266 |
| is_lifted_const _ = false;
|
|
267 |
|
|
268 |
fun build_aux lthy tm =
|
|
269 |
case tm of
|
|
270 |
Abs (a as (_, vty, _)) =>
|
|
271 |
let
|
|
272 |
val (vs, t) = Term.dest_abs a;
|
|
273 |
val v = Free(vs, vty);
|
|
274 |
val t' = lambda v (build_aux lthy t)
|
|
275 |
in
|
|
276 |
if (not (needs_lift rty (fastype_of tm))) then t'
|
|
277 |
else mk_repabs (
|
|
278 |
if not (needs_lift rty vty) then t'
|
|
279 |
else
|
|
280 |
let
|
|
281 |
val v' = mk_repabs v;
|
|
282 |
(* TODO: I believe 'beta' is not needed any more *)
|
|
283 |
val t1 = (* Envir.beta_norm *) (t' $ v')
|
|
284 |
in
|
|
285 |
lambda v t1
|
|
286 |
end)
|
|
287 |
end
|
|
288 |
| x =>
|
|
289 |
case Term.strip_comb tm of
|
|
290 |
(Const(@{const_name Respects}, _), _) => tm
|
|
291 |
| (opp, tms0) =>
|
|
292 |
let
|
|
293 |
val tms = map (build_aux lthy) tms0
|
|
294 |
val ty = fastype_of tm
|
|
295 |
in
|
|
296 |
if (is_lifted_const opp andalso needs_lift rty ty) then
|
|
297 |
mk_repabs (list_comb (opp, tms))
|
|
298 |
else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
|
|
299 |
mk_repabs (list_comb (opp, tms))
|
|
300 |
else if tms = [] then opp
|
|
301 |
else list_comb(opp, tms)
|
|
302 |
end
|
|
303 |
in
|
|
304 |
repeat_eqsubst_prop lthy @{thms id_def_sym}
|
|
305 |
(build_aux lthy (Thm.prop_of thm))
|
|
306 |
end
|
|
307 |
*}
|
|
308 |
|
|
309 |
text {* Builds provable goals for regularized theorems *}
|
|
310 |
ML {*
|
|
311 |
fun build_repabs_goal ctxt thm cons rty qty =
|
|
312 |
Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))
|
|
313 |
*}
|
|
314 |
|
|
315 |
ML {*
|
|
316 |
fun repabs lthy thm consts rty qty quot_thm reflex_thm trans_thm rsp_thms =
|
|
317 |
let
|
|
318 |
val rt = build_repabs_term lthy thm consts rty qty;
|
|
319 |
val rg = Logic.mk_equals ((Thm.prop_of thm), rt);
|
|
320 |
fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
|
|
321 |
(REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));
|
|
322 |
val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
|
|
323 |
in
|
|
324 |
@{thm Pure.equal_elim_rule1} OF [cthm, thm]
|
|
325 |
end
|
|
326 |
*}
|
|
327 |
|
|
328 |
|
|
329 |
(* TODO: Check if it behaves properly with varifyed rty *)
|
|
330 |
ML {*
|
|
331 |
fun findabs_all rty tm =
|
|
332 |
case tm of
|
|
333 |
Abs(_, T, b) =>
|
|
334 |
let
|
|
335 |
val b' = subst_bound ((Free ("x", T)), b);
|
|
336 |
val tys = findabs_all rty b'
|
|
337 |
val ty = fastype_of tm
|
|
338 |
in if needs_lift rty ty then (ty :: tys) else tys
|
|
339 |
end
|
|
340 |
| f $ a => (findabs_all rty f) @ (findabs_all rty a)
|
|
341 |
| _ => [];
|
|
342 |
fun findabs rty tm = distinct (op =) (findabs_all rty tm)
|
|
343 |
*}
|
|
344 |
|
|
345 |
|
|
346 |
(* Currently useful only for LAMBDA_PRS *)
|
|
347 |
ML {*
|
|
348 |
fun make_simp_prs_thm lthy quot_thm thm typ =
|
|
349 |
let
|
|
350 |
val (_, [lty, rty]) = dest_Type typ;
|
|
351 |
val thy = ProofContext.theory_of lthy;
|
|
352 |
val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
|
|
353 |
val inst = [SOME lcty, NONE, SOME rcty];
|
|
354 |
val lpi = Drule.instantiate' inst [] thm;
|
|
355 |
val tac =
|
|
356 |
(compose_tac (false, lpi, 2)) THEN_ALL_NEW
|
|
357 |
(quotient_tac quot_thm);
|
|
358 |
val gc = Drule.strip_imp_concl (cprop_of lpi);
|
|
359 |
val t = Goal.prove_internal [] gc (fn _ => tac 1)
|
|
360 |
in
|
|
361 |
MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t
|
|
362 |
end
|
|
363 |
*}
|
|
364 |
|
|
365 |
ML {*
|
|
366 |
fun findallex_all rty qty tm =
|
|
367 |
case tm of
|
|
368 |
Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) =>
|
|
369 |
let
|
|
370 |
val (tya, tye) = findallex_all rty qty s
|
|
371 |
in if needs_lift rty T then
|
|
372 |
((T :: tya), tye)
|
|
373 |
else (tya, tye) end
|
|
374 |
| Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) =>
|
|
375 |
let
|
|
376 |
val (tya, tye) = findallex_all rty qty s
|
|
377 |
in if needs_lift rty T then
|
|
378 |
(tya, (T :: tye))
|
|
379 |
else (tya, tye) end
|
|
380 |
| Abs(_, T, b) =>
|
|
381 |
findallex_all rty qty (subst_bound ((Free ("x", T)), b))
|
|
382 |
| f $ a =>
|
|
383 |
let
|
|
384 |
val (a1, e1) = findallex_all rty qty f;
|
|
385 |
val (a2, e2) = findallex_all rty qty a;
|
|
386 |
in (a1 @ a2, e1 @ e2) end
|
|
387 |
| _ => ([], []);
|
|
388 |
*}
|
|
389 |
|
|
390 |
ML {*
|
|
391 |
fun findallex lthy rty qty tm =
|
|
392 |
let
|
|
393 |
val (a, e) = findallex_all rty qty tm;
|
|
394 |
val (ad, ed) = (map domain_type a, map domain_type e);
|
|
395 |
val (au, eu) = (distinct (op =) ad, distinct (op =) ed);
|
|
396 |
val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty)
|
|
397 |
in
|
|
398 |
(map (exchange_ty lthy rty qty) au, map (exchange_ty lthy rty qty) eu)
|
|
399 |
end
|
|
400 |
*}
|
|
401 |
|
|
402 |
ML {*
|
|
403 |
fun make_allex_prs_thm lthy quot_thm thm typ =
|
|
404 |
let
|
|
405 |
val (_, [lty, rty]) = dest_Type typ;
|
|
406 |
val thy = ProofContext.theory_of lthy;
|
|
407 |
val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
|
|
408 |
val inst = [NONE, SOME lcty];
|
|
409 |
val lpi = Drule.instantiate' inst [] thm;
|
|
410 |
val tac =
|
|
411 |
(compose_tac (false, lpi, 1)) THEN_ALL_NEW
|
|
412 |
(quotient_tac quot_thm);
|
|
413 |
val gc = Drule.strip_imp_concl (cprop_of lpi);
|
|
414 |
val t = Goal.prove_internal [] gc (fn _ => tac 1)
|
|
415 |
val t_noid = MetaSimplifier.rewrite_rule
|
|
416 |
[@{thm eq_reflection} OF @{thms id_apply}] t;
|
|
417 |
val t_sym = @{thm "HOL.sym"} OF [t_noid];
|
|
418 |
val t_eq = @{thm "eq_reflection"} OF [t_sym]
|
|
419 |
in
|
|
420 |
t_eq
|
|
421 |
end
|
|
422 |
*}
|
|
423 |
|
|
424 |
ML {*
|
|
425 |
fun lift_thm lthy qty qty_name rsp_thms defs rthm =
|
|
426 |
let
|
|
427 |
val _ = tracing ("raw theorem:\n" ^ Syntax.string_of_term lthy (prop_of rthm))
|
|
428 |
|
|
429 |
val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;
|
|
430 |
val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;
|
|
431 |
val consts = lookup_quot_consts defs;
|
|
432 |
val t_a = atomize_thm rthm;
|
|
433 |
|
|
434 |
val _ = tracing ("raw atomized theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_a))
|
|
435 |
|
|
436 |
val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
|
|
437 |
|
|
438 |
val _ = tracing ("regularised theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_r))
|
|
439 |
|
|
440 |
val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
|
|
441 |
|
|
442 |
val _ = tracing ("rep/abs injected theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_t))
|
|
443 |
|
|
444 |
val (alls, exs) = findallex lthy rty qty (prop_of t_a);
|
|
445 |
val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls
|
|
446 |
val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs
|
|
447 |
val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
|
|
448 |
|
|
449 |
val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_a))
|
|
450 |
|
|
451 |
val abs = findabs rty (prop_of t_a);
|
|
452 |
val aps = findaps rty (prop_of t_a);
|
|
453 |
val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;
|
|
454 |
val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
|
|
455 |
val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
|
|
456 |
|
|
457 |
val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_l))
|
|
458 |
|
|
459 |
val defs_sym = flat (map (add_lower_defs lthy) defs);
|
|
460 |
val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;
|
|
461 |
val t_id = simp_ids lthy t_l;
|
|
462 |
|
|
463 |
val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_id))
|
|
464 |
|
|
465 |
val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;
|
|
466 |
|
|
467 |
val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d0))
|
|
468 |
|
|
469 |
val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
|
|
470 |
|
|
471 |
val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d))
|
|
472 |
|
|
473 |
val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
|
|
474 |
|
|
475 |
val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_r))
|
|
476 |
|
|
477 |
val t_rv = ObjectLogic.rulify t_r
|
|
478 |
|
|
479 |
val _ = tracing ("lifted theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_rv))
|
|
480 |
in
|
|
481 |
Thm.varifyT t_rv
|
|
482 |
end
|
|
483 |
*}
|
|
484 |
|
|
485 |
ML {*
|
|
486 |
fun lift_thm_note qty qty_name rsp_thms defs thm name lthy =
|
|
487 |
let
|
|
488 |
val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm;
|
|
489 |
val (_, lthy2) = note (name, lifted_thm) lthy;
|
|
490 |
in
|
|
491 |
lthy2
|
|
492 |
end
|
|
493 |
*}
|
|
494 |
|
|
495 |
|
|
496 |
ML {*
|
|
497 |
fun regularize_goal lthy thm rel_eqv rel_refl qtrm =
|
|
498 |
let
|
|
499 |
val reg_trm = mk_REGULARIZE_goal lthy (prop_of thm) qtrm;
|
|
500 |
fun tac lthy = regularize_tac lthy rel_eqv rel_refl;
|
|
501 |
val cthm = Goal.prove lthy [] [] reg_trm
|
|
502 |
(fn {context, ...} => tac context 1);
|
|
503 |
in
|
|
504 |
cthm OF [thm]
|
|
505 |
end
|
|
506 |
*}
|
|
507 |
|
|
508 |
ML {*
|
|
509 |
fun repabs_goal lthy thm rty quot_thm reflex_thm trans_thm rsp_thms qtrm =
|
|
510 |
let
|
|
511 |
val rg = Syntax.check_term lthy (mk_inj_REPABS_goal lthy ((prop_of thm), qtrm));
|
|
512 |
fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
|
|
513 |
(REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));
|
|
514 |
val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
|
|
515 |
in
|
|
516 |
@{thm Pure.equal_elim_rule1} OF [cthm, thm]
|
|
517 |
end
|
|
518 |
*}
|
|
519 |
|
381
|
520 |
|
|
521 |
ML {*
|
|
522 |
fun atomize_goal thy gl =
|
|
523 |
let
|
|
524 |
val vars = map Free (Term.add_frees gl []);
|
|
525 |
val all = if fastype_of gl = @{typ bool} then HOLogic.all_const else Term.all;
|
|
526 |
fun lambda_all (var as Free(_, T)) trm = (all T) $ lambda var trm;
|
|
527 |
val glv = fold lambda_all vars gl
|
|
528 |
val gla = (term_of o snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glv))
|
|
529 |
val glf = Type.legacy_freeze gla
|
|
530 |
in
|
|
531 |
if fastype_of gl = @{typ bool} then @{term Trueprop} $ glf else glf
|
|
532 |
end
|
|
533 |
*}
|
|
534 |
|
|
535 |
|
|
536 |
ML {* atomize_goal @{theory} @{term "x memb [] = False"} *}
|
399
|
537 |
ML {* atomize_goal @{theory} @{term "x = xa ? a # x = a # xa"} *}
|
381
|
538 |
|
|
539 |
|
466
|
540 |
ML {*
|
|
541 |
fun applic_prs lthy absrep (rty, qty) =
|
|
542 |
let
|
|
543 |
fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm;
|
|
544 |
fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm;
|
|
545 |
val (raty, rgty) = Term.strip_type rty;
|
|
546 |
val (qaty, qgty) = Term.strip_type qty;
|
|
547 |
val vs = map (fn _ => "x") qaty;
|
|
548 |
val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
|
|
549 |
val f = Free (fname, qaty ---> qgty);
|
|
550 |
val args = map Free (vfs ~~ qaty);
|
|
551 |
val rhs = list_comb(f, args);
|
|
552 |
val largs = map2 mk_rep (raty ~~ qaty) args;
|
|
553 |
val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs));
|
|
554 |
val llhs = Syntax.check_term lthy lhs;
|
|
555 |
val eq = Logic.mk_equals (llhs, rhs);
|
|
556 |
val ceq = cterm_of (ProofContext.theory_of lthy') eq;
|
|
557 |
val sctxt = HOL_ss addsimps (@{thms fun_map.simps id_simps} @ absrep);
|
|
558 |
val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
|
|
559 |
val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t;
|
|
560 |
in
|
|
561 |
singleton (ProofContext.export lthy' lthy) t_id
|
|
562 |
end
|
|
563 |
*}
|
|
564 |
|
|
565 |
ML {*
|
|
566 |
fun find_aps_all rtm qtm =
|
|
567 |
case (rtm, qtm) of
|
|
568 |
(Abs(_, T1, s1), Abs(_, T2, s2)) =>
|
|
569 |
find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2))
|
|
570 |
| (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) =>
|
|
571 |
let
|
|
572 |
val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2)
|
|
573 |
in
|
|
574 |
if T1 = T2 then sub else (T1, T2) :: sub
|
|
575 |
end
|
|
576 |
| ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2)
|
|
577 |
| _ => [];
|
|
578 |
|
|
579 |
fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm)
|
|
580 |
*}
|
|
581 |
|
|
582 |
|
381
|
583 |
|
379
|
584 |
ML {*
|
|
585 |
fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal =
|
|
586 |
let
|
|
587 |
val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;
|
|
588 |
val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;
|
|
589 |
val t_a = atomize_thm rthm;
|
|
590 |
val goal_a = atomize_goal (ProofContext.theory_of lthy) goal;
|
|
591 |
val t_r = regularize_goal lthy t_a rel_eqv rel_refl goal_a;
|
|
592 |
val t_t = repabs_goal lthy t_r rty quot rel_refl trans2 rsp_thms goal_a;
|
|
593 |
val (alls, exs) = findallex lthy rty qty (prop_of t_a);
|
|
594 |
val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls
|
|
595 |
val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs
|
|
596 |
val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
|
|
597 |
val abs = findabs rty (prop_of t_a);
|
|
598 |
val aps = findaps rty (prop_of t_a);
|
|
599 |
val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;
|
|
600 |
val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
|
|
601 |
val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
|
|
602 |
val defs_sym = flat (map (add_lower_defs lthy) defs);
|
|
603 |
val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;
|
|
604 |
val t_id = simp_ids lthy t_l;
|
|
605 |
val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;
|
|
606 |
val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
|
|
607 |
val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
|
|
608 |
val t_rv = ObjectLogic.rulify t_r
|
|
609 |
in
|
|
610 |
Thm.varifyT t_rv
|
|
611 |
end
|
|
612 |
*}
|
|
613 |
|
|
614 |
ML {*
|
|
615 |
fun lift_thm_goal_note lthy qty qty_name rsp_thms defs thm name goal =
|
|
616 |
let
|
|
617 |
val lifted_thm = lift_thm_goal lthy qty qty_name rsp_thms defs thm goal;
|
|
618 |
val (_, lthy2) = note (name, lifted_thm) lthy;
|
|
619 |
in
|
|
620 |
lthy2
|
|
621 |
end
|
|
622 |
*}
|
|
623 |
|
381
|
624 |
ML {*
|
|
625 |
fun simp_ids_trm trm =
|
|
626 |
trm |>
|
|
627 |
MetaSimplifier.rewrite false @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}
|
|
628 |
|> cprop_of |> Thm.dest_equals |> snd
|
|
629 |
|
|
630 |
*}
|
693
|
631 |
|
|
632 |
(* Unused part of the locale *)
|
|
633 |
|
|
634 |
lemma R_trans:
|
|
635 |
assumes ab: "R a b"
|
|
636 |
and bc: "R b c"
|
|
637 |
shows "R a c"
|
|
638 |
proof -
|
|
639 |
have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp
|
|
640 |
moreover have ab: "R a b" by fact
|
|
641 |
moreover have bc: "R b c" by fact
|
|
642 |
ultimately show "R a c" unfolding transp_def by blast
|
|
643 |
qed
|
|
644 |
|
|
645 |
lemma R_sym:
|
|
646 |
assumes ab: "R a b"
|
|
647 |
shows "R b a"
|
|
648 |
proof -
|
|
649 |
have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp
|
|
650 |
then show "R b a" using ab unfolding symp_def by blast
|
|
651 |
qed
|
|
652 |
|
|
653 |
lemma R_trans2:
|
|
654 |
assumes ac: "R a c"
|
|
655 |
and bd: "R b d"
|
|
656 |
shows "R a b = R c d"
|
|
657 |
using ac bd
|
|
658 |
by (blast intro: R_trans R_sym)
|
|
659 |
|
|
660 |
lemma REPS_same:
|
|
661 |
shows "R (REP a) (REP b) \<equiv> (a = b)"
|
|
662 |
proof -
|
|
663 |
have "R (REP a) (REP b) = (a = b)"
|
|
664 |
proof
|
|
665 |
assume as: "R (REP a) (REP b)"
|
|
666 |
from rep_prop
|
|
667 |
obtain x y
|
|
668 |
where eqs: "Rep a = R x" "Rep b = R y" by blast
|
|
669 |
from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
|
|
670 |
then have "R x (Eps (R y))" using lem9 by simp
|
|
671 |
then have "R (Eps (R y)) x" using R_sym by blast
|
|
672 |
then have "R y x" using lem9 by simp
|
|
673 |
then have "R x y" using R_sym by blast
|
|
674 |
then have "ABS x = ABS y" using thm11 by simp
|
|
675 |
then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
|
|
676 |
then show "a = b" using rep_inverse by simp
|
|
677 |
next
|
|
678 |
assume ab: "a = b"
|
|
679 |
have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp
|
|
680 |
then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto
|
|
681 |
qed
|
|
682 |
then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
|
|
683 |
qed
|
|
684 |
|
|
685 |
|
|
686 |
|
|
687 |
|