0
|
1 |
theory QuotMain
|
6
|
2 |
imports QuotScript QuotList Prove
|
71
|
3 |
uses ("quotient.ML")
|
0
|
4 |
begin
|
|
5 |
|
|
6 |
locale QUOT_TYPE =
|
|
7 |
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
|
|
8 |
and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
|
|
9 |
and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
|
|
10 |
assumes equiv: "EQUIV R"
|
|
11 |
and rep_prop: "\<And>y. \<exists>x. Rep y = R x"
|
|
12 |
and rep_inverse: "\<And>x. Abs (Rep x) = x"
|
|
13 |
and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
|
|
14 |
and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
|
15
|
15 |
begin
|
0
|
16 |
|
|
17 |
definition
|
|
18 |
"ABS x \<equiv> Abs (R x)"
|
|
19 |
|
|
20 |
definition
|
|
21 |
"REP a = Eps (Rep a)"
|
|
22 |
|
15
|
23 |
lemma lem9:
|
0
|
24 |
shows "R (Eps (R x)) = R x"
|
|
25 |
proof -
|
|
26 |
have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
|
|
27 |
then have "R x (Eps (R x))" by (rule someI)
|
15
|
28 |
then show "R (Eps (R x)) = R x"
|
0
|
29 |
using equiv unfolding EQUIV_def by simp
|
|
30 |
qed
|
|
31 |
|
|
32 |
theorem thm10:
|
24
|
33 |
shows "ABS (REP a) \<equiv> a"
|
|
34 |
apply (rule eq_reflection)
|
|
35 |
unfolding ABS_def REP_def
|
0
|
36 |
proof -
|
15
|
37 |
from rep_prop
|
0
|
38 |
obtain x where eq: "Rep a = R x" by auto
|
|
39 |
have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
|
|
40 |
also have "\<dots> = Abs (R x)" using lem9 by simp
|
|
41 |
also have "\<dots> = Abs (Rep a)" using eq by simp
|
|
42 |
also have "\<dots> = a" using rep_inverse by simp
|
|
43 |
finally
|
|
44 |
show "Abs (R (Eps (Rep a))) = a" by simp
|
|
45 |
qed
|
|
46 |
|
15
|
47 |
lemma REP_refl:
|
0
|
48 |
shows "R (REP a) (REP a)"
|
|
49 |
unfolding REP_def
|
|
50 |
by (simp add: equiv[simplified EQUIV_def])
|
|
51 |
|
|
52 |
lemma lem7:
|
22
|
53 |
shows "(R x = R y) = (Abs (R x) = Abs (R y))"
|
0
|
54 |
apply(rule iffI)
|
|
55 |
apply(simp)
|
|
56 |
apply(drule rep_inject[THEN iffD2])
|
|
57 |
apply(simp add: abs_inverse)
|
|
58 |
done
|
15
|
59 |
|
0
|
60 |
theorem thm11:
|
|
61 |
shows "R r r' = (ABS r = ABS r')"
|
|
62 |
unfolding ABS_def
|
|
63 |
by (simp only: equiv[simplified EQUIV_def] lem7)
|
|
64 |
|
4
|
65 |
|
2
|
66 |
lemma REP_ABS_rsp:
|
4
|
67 |
shows "R f (REP (ABS g)) = R f g"
|
|
68 |
and "R (REP (ABS g)) f = R g f"
|
23
|
69 |
by (simp_all add: thm10 thm11)
|
4
|
70 |
|
0
|
71 |
lemma QUOTIENT:
|
|
72 |
"QUOTIENT R ABS REP"
|
|
73 |
apply(unfold QUOTIENT_def)
|
|
74 |
apply(simp add: thm10)
|
|
75 |
apply(simp add: REP_refl)
|
|
76 |
apply(subst thm11[symmetric])
|
|
77 |
apply(simp add: equiv[simplified EQUIV_def])
|
|
78 |
done
|
|
79 |
|
21
|
80 |
lemma R_trans:
|
49
|
81 |
assumes ab: "R a b"
|
|
82 |
and bc: "R b c"
|
22
|
83 |
shows "R a c"
|
21
|
84 |
proof -
|
|
85 |
have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
|
|
86 |
moreover have ab: "R a b" by fact
|
|
87 |
moreover have bc: "R b c" by fact
|
22
|
88 |
ultimately show "R a c" unfolding TRANS_def by blast
|
21
|
89 |
qed
|
|
90 |
|
|
91 |
lemma R_sym:
|
49
|
92 |
assumes ab: "R a b"
|
22
|
93 |
shows "R b a"
|
21
|
94 |
proof -
|
|
95 |
have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
|
22
|
96 |
then show "R b a" using ab unfolding SYM_def by blast
|
21
|
97 |
qed
|
|
98 |
|
49
|
99 |
lemma R_trans2:
|
|
100 |
assumes ac: "R a c"
|
22
|
101 |
and bd: "R b d"
|
21
|
102 |
shows "R a b = R c d"
|
|
103 |
proof
|
23
|
104 |
assume "R a b"
|
21
|
105 |
then have "R b a" using R_sym by blast
|
|
106 |
then have "R b c" using ac R_trans by blast
|
|
107 |
then have "R c b" using R_sym by blast
|
|
108 |
then show "R c d" using bd R_trans by blast
|
|
109 |
next
|
23
|
110 |
assume "R c d"
|
21
|
111 |
then have "R a d" using ac R_trans by blast
|
|
112 |
then have "R d a" using R_sym by blast
|
|
113 |
then have "R b a" using bd R_trans by blast
|
|
114 |
then show "R a b" using R_sym by blast
|
|
115 |
qed
|
|
116 |
|
|
117 |
lemma REPS_same:
|
25
|
118 |
shows "R (REP a) (REP b) \<equiv> (a = b)"
|
38
|
119 |
proof -
|
|
120 |
have "R (REP a) (REP b) = (a = b)"
|
|
121 |
proof
|
|
122 |
assume as: "R (REP a) (REP b)"
|
|
123 |
from rep_prop
|
|
124 |
obtain x y
|
|
125 |
where eqs: "Rep a = R x" "Rep b = R y" by blast
|
|
126 |
from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
|
|
127 |
then have "R x (Eps (R y))" using lem9 by simp
|
|
128 |
then have "R (Eps (R y)) x" using R_sym by blast
|
|
129 |
then have "R y x" using lem9 by simp
|
|
130 |
then have "R x y" using R_sym by blast
|
|
131 |
then have "ABS x = ABS y" using thm11 by simp
|
|
132 |
then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
|
|
133 |
then show "a = b" using rep_inverse by simp
|
|
134 |
next
|
|
135 |
assume ab: "a = b"
|
|
136 |
have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
|
|
137 |
then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto
|
|
138 |
qed
|
|
139 |
then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
|
21
|
140 |
qed
|
|
141 |
|
0
|
142 |
end
|
|
143 |
|
127
b054cf6bd179
the command "quotient" can now define more than one quotient at the same time; quotients need to be separated by and
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
144 |
|
0
|
145 |
section {* type definition for the quotient type *}
|
|
146 |
|
185
|
147 |
ML {* Toplevel.theory *}
|
|
148 |
|
71
|
149 |
use "quotient.ML"
|
0
|
150 |
|
185
|
151 |
declare [[map list = (map, LIST_REL)]]
|
|
152 |
declare [[map * = (prod_fun, prod_rel)]]
|
|
153 |
declare [[map "fun" = (fun_map, FUN_REL)]]
|
|
154 |
|
|
155 |
ML {* maps_lookup @{theory} "List.list" *}
|
|
156 |
ML {* maps_lookup @{theory} "*" *}
|
|
157 |
ML {* maps_lookup @{theory} "fun" *}
|
174
|
158 |
|
14
|
159 |
ML {*
|
|
160 |
val no_vars = Thm.rule_attribute (fn context => fn th =>
|
|
161 |
let
|
|
162 |
val ctxt = Variable.set_body false (Context.proof_of context);
|
|
163 |
val ((_, [th']), _) = Variable.import true [th] ctxt;
|
|
164 |
in th' end);
|
|
165 |
*}
|
|
166 |
|
0
|
167 |
section {* lifting of constants *}
|
|
168 |
|
|
169 |
ML {*
|
185
|
170 |
|
|
171 |
*}
|
|
172 |
|
|
173 |
ML {*
|
118
|
174 |
(* calculates the aggregate abs and rep functions for a given type;
|
|
175 |
repF is for constants' arguments; absF is for constants;
|
|
176 |
function types need to be treated specially, since repF and absF
|
163
|
177 |
change
|
118
|
178 |
*)
|
46
|
179 |
datatype flag = absF | repF
|
0
|
180 |
|
109
386671ef36bd
fixed the problem with function types; but only type_of works; cterm_of does not work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
181 |
fun negF absF = repF
|
386671ef36bd
fixed the problem with function types; but only type_of works; cterm_of does not work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
182 |
| negF repF = absF
|
386671ef36bd
fixed the problem with function types; but only type_of works; cterm_of does not work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
183 |
|
46
|
184 |
fun get_fun flag rty qty lthy ty =
|
0
|
185 |
let
|
|
186 |
val qty_name = Long_Name.base_name (fst (dest_Type qty))
|
15
|
187 |
|
0
|
188 |
fun get_fun_aux s fs_tys =
|
|
189 |
let
|
|
190 |
val (fs, tys) = split_list fs_tys
|
15
|
191 |
val (otys, ntys) = split_list tys
|
0
|
192 |
val oty = Type (s, otys)
|
|
193 |
val nty = Type (s, ntys)
|
|
194 |
val ftys = map (op -->) tys
|
|
195 |
in
|
130
|
196 |
(case (maps_lookup (ProofContext.theory_of lthy) s) of
|
110
|
197 |
SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty))
|
|
198 |
| NONE => raise ERROR ("no map association for type " ^ s))
|
|
199 |
end
|
|
200 |
|
118
|
201 |
fun get_fun_fun fs_tys =
|
110
|
202 |
let
|
|
203 |
val (fs, tys) = split_list fs_tys
|
|
204 |
val ([oty1, oty2], [nty1, nty2]) = split_list tys
|
128
|
205 |
val oty = nty1 --> oty2
|
|
206 |
val nty = oty1 --> nty2
|
110
|
207 |
val ftys = map (op -->) tys
|
|
208 |
in
|
118
|
209 |
(list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
|
0
|
210 |
end
|
|
211 |
|
170
|
212 |
val thy = ProofContext.theory_of lthy
|
|
213 |
|
|
214 |
fun get_const absF = (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty))
|
|
215 |
| get_const repF = (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty))
|
41
|
216 |
|
70
f3cbda066c3a
consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
217 |
fun mk_identity ty = Abs ("", ty, Bound 0)
|
41
|
218 |
|
0
|
219 |
in
|
|
220 |
if ty = qty
|
46
|
221 |
then (get_const flag)
|
0
|
222 |
else (case ty of
|
41
|
223 |
TFree _ => (mk_identity ty, (ty, ty))
|
118
|
224 |
| Type (_, []) => (mk_identity ty, (ty, ty))
|
109
386671ef36bd
fixed the problem with function types; but only type_of works; cterm_of does not work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
225 |
| Type ("fun" , [ty1, ty2]) =>
|
118
|
226 |
get_fun_fun [get_fun (negF flag) rty qty lthy ty1, get_fun flag rty qty lthy ty2]
|
46
|
227 |
| Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys)
|
41
|
228 |
| _ => raise ERROR ("no type variables")
|
0
|
229 |
)
|
|
230 |
end
|
|
231 |
*}
|
|
232 |
|
180
|
233 |
|
41
|
234 |
text {* produces the definition for a lifted constant *}
|
86
|
235 |
|
2
|
236 |
ML {*
|
0
|
237 |
fun get_const_def nconst oconst rty qty lthy =
|
|
238 |
let
|
|
239 |
val ty = fastype_of nconst
|
|
240 |
val (arg_tys, res_ty) = strip_type ty
|
14
|
241 |
|
0
|
242 |
val fresh_args = arg_tys |> map (pair "x")
|
15
|
243 |
|> Variable.variant_frees lthy [nconst, oconst]
|
0
|
244 |
|> map Free
|
|
245 |
|
46
|
246 |
val rep_fns = map (fst o get_fun repF rty qty lthy) arg_tys
|
|
247 |
val abs_fn = (fst o get_fun absF rty qty lthy) res_ty
|
0
|
248 |
|
180
|
249 |
fun mk_fun_map (t1,t2) = Const (@{const_name "fun_map"}, dummyT) $ t1 $ t2
|
|
250 |
|
|
251 |
val fns = Library.foldr (mk_fun_map) (rep_fns, abs_fn)
|
|
252 |
|> Syntax.check_term lthy
|
0
|
253 |
in
|
180
|
254 |
fns $ oconst
|
0
|
255 |
end
|
|
256 |
*}
|
|
257 |
|
|
258 |
ML {*
|
15
|
259 |
fun exchange_ty rty qty ty =
|
49
|
260 |
if ty = rty
|
41
|
261 |
then qty
|
15
|
262 |
else
|
0
|
263 |
(case ty of
|
|
264 |
Type (s, tys) => Type (s, map (exchange_ty rty qty) tys)
|
41
|
265 |
| _ => ty
|
|
266 |
)
|
0
|
267 |
*}
|
|
268 |
|
|
269 |
ML {*
|
17
|
270 |
fun make_const_def nconst_bname oconst mx rty qty lthy =
|
0
|
271 |
let
|
|
272 |
val oconst_ty = fastype_of oconst
|
|
273 |
val nconst_ty = exchange_ty rty qty oconst_ty
|
17
|
274 |
val nconst = Const (Binding.name_of nconst_bname, nconst_ty)
|
0
|
275 |
val def_trm = get_const_def nconst oconst rty qty lthy
|
|
276 |
in
|
79
c0c41fefeb06
added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
277 |
define (nconst_bname, mx, def_trm) lthy
|
15
|
278 |
end
|
0
|
279 |
*}
|
|
280 |
|
139
|
281 |
section {* ATOMIZE *}
|
|
282 |
|
|
283 |
text {*
|
|
284 |
Unabs_def converts a definition given as
|
|
285 |
|
|
286 |
c \<equiv> %x. %y. f x y
|
|
287 |
|
|
288 |
to a theorem of the form
|
|
289 |
|
|
290 |
c x y \<equiv> f x y
|
|
291 |
|
|
292 |
This function is needed to rewrite the right-hand
|
|
293 |
side to the left-hand side.
|
|
294 |
*}
|
|
295 |
|
|
296 |
ML {*
|
|
297 |
fun unabs_def ctxt def =
|
|
298 |
let
|
|
299 |
val (lhs, rhs) = Thm.dest_equals (cprop_of def)
|
|
300 |
val xs = strip_abs_vars (term_of rhs)
|
|
301 |
val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
|
|
302 |
|
|
303 |
val thy = ProofContext.theory_of ctxt'
|
|
304 |
val cxs = map (cterm_of thy o Free) xs
|
|
305 |
val new_lhs = Drule.list_comb (lhs, cxs)
|
|
306 |
|
|
307 |
fun get_conv [] = Conv.rewr_conv def
|
|
308 |
| get_conv (x::xs) = Conv.fun_conv (get_conv xs)
|
|
309 |
in
|
|
310 |
get_conv xs new_lhs |>
|
|
311 |
singleton (ProofContext.export ctxt' ctxt)
|
|
312 |
end
|
|
313 |
*}
|
|
314 |
|
|
315 |
lemma atomize_eqv[atomize]:
|
|
316 |
shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
|
|
317 |
proof
|
|
318 |
assume "A \<equiv> B"
|
|
319 |
then show "Trueprop A \<equiv> Trueprop B" by unfold
|
|
320 |
next
|
|
321 |
assume *: "Trueprop A \<equiv> Trueprop B"
|
|
322 |
have "A = B"
|
|
323 |
proof (cases A)
|
|
324 |
case True
|
|
325 |
have "A" by fact
|
|
326 |
then show "A = B" using * by simp
|
|
327 |
next
|
|
328 |
case False
|
|
329 |
have "\<not>A" by fact
|
|
330 |
then show "A = B" using * by auto
|
|
331 |
qed
|
|
332 |
then show "A \<equiv> B" by (rule eq_reflection)
|
|
333 |
qed
|
|
334 |
|
|
335 |
ML {*
|
|
336 |
fun atomize_thm thm =
|
|
337 |
let
|
|
338 |
val thm' = forall_intr_vars thm
|
|
339 |
val thm'' = ObjectLogic.atomize (cprop_of thm')
|
|
340 |
in
|
140
|
341 |
Thm.freezeT (Simplifier.rewrite_rule [thm''] thm')
|
139
|
342 |
end
|
|
343 |
*}
|
|
344 |
|
140
|
345 |
ML {* atomize_thm @{thm list.induct} *}
|
139
|
346 |
|
|
347 |
section {* REGULARIZE *}
|
|
348 |
|
|
349 |
text {* tyRel takes a type and builds a relation that a quantifier over this
|
|
350 |
type needs to respect. *}
|
|
351 |
ML {*
|
|
352 |
fun tyRel ty rty rel lthy =
|
|
353 |
if ty = rty
|
|
354 |
then rel
|
|
355 |
else (case ty of
|
|
356 |
Type (s, tys) =>
|
|
357 |
let
|
|
358 |
val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
|
|
359 |
val ty_out = ty --> ty --> @{typ bool};
|
|
360 |
val tys_out = tys_rel ---> ty_out;
|
|
361 |
in
|
|
362 |
(case (maps_lookup (ProofContext.theory_of lthy) s) of
|
|
363 |
SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
|
|
364 |
| NONE => HOLogic.eq_const ty
|
|
365 |
)
|
|
366 |
end
|
|
367 |
| _ => HOLogic.eq_const ty)
|
|
368 |
*}
|
|
369 |
|
|
370 |
definition
|
|
371 |
Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
|
|
372 |
where
|
|
373 |
"(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
|
|
374 |
(* TODO: Consider defining it with an "if"; sth like:
|
|
375 |
Babs p m = \<lambda>x. if x \<in> p then m x else undefined
|
|
376 |
*)
|
|
377 |
|
|
378 |
ML {*
|
|
379 |
fun needs_lift (rty as Type (rty_s, _)) ty =
|
|
380 |
case ty of
|
|
381 |
Type (s, tys) =>
|
|
382 |
(s = rty_s) orelse (exists (needs_lift rty) tys)
|
|
383 |
| _ => false
|
|
384 |
|
|
385 |
*}
|
|
386 |
|
|
387 |
ML {*
|
|
388 |
(* trm \<Rightarrow> new_trm *)
|
|
389 |
fun regularise trm rty rel lthy =
|
|
390 |
case trm of
|
|
391 |
Abs (x, T, t) =>
|
|
392 |
if (needs_lift rty T) then let
|
|
393 |
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
|
|
394 |
val v = Free (x', T);
|
|
395 |
val t' = subst_bound (v, t);
|
|
396 |
val rec_term = regularise t' rty rel lthy2;
|
|
397 |
val lam_term = Term.lambda_name (x, v) rec_term;
|
|
398 |
val sub_res_term = tyRel T rty rel lthy;
|
|
399 |
val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
|
|
400 |
val res_term = respects $ sub_res_term;
|
|
401 |
val ty = fastype_of trm;
|
|
402 |
val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty);
|
|
403 |
val rabs_term = (rabs $ res_term) $ lam_term;
|
|
404 |
in
|
|
405 |
rabs_term
|
|
406 |
end else let
|
|
407 |
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
|
|
408 |
val v = Free (x', T);
|
|
409 |
val t' = subst_bound (v, t);
|
|
410 |
val rec_term = regularise t' rty rel lthy2;
|
|
411 |
in
|
|
412 |
Term.lambda_name (x, v) rec_term
|
|
413 |
end
|
|
414 |
| ((Const (@{const_name "All"}, at)) $ (Abs (x, T, t))) =>
|
|
415 |
if (needs_lift rty T) then let
|
|
416 |
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
|
|
417 |
val v = Free (x', T);
|
|
418 |
val t' = subst_bound (v, t);
|
|
419 |
val rec_term = regularise t' rty rel lthy2;
|
|
420 |
val lam_term = Term.lambda_name (x, v) rec_term;
|
|
421 |
val sub_res_term = tyRel T rty rel lthy;
|
|
422 |
val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
|
|
423 |
val res_term = respects $ sub_res_term;
|
|
424 |
val ty = fastype_of lam_term;
|
|
425 |
val rall = Const (@{const_name Ball}, (fastype_of res_term) --> ty --> @{typ bool});
|
|
426 |
val rall_term = (rall $ res_term) $ lam_term;
|
|
427 |
in
|
|
428 |
rall_term
|
|
429 |
end else let
|
|
430 |
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
|
|
431 |
val v = Free (x', T);
|
|
432 |
val t' = subst_bound (v, t);
|
|
433 |
val rec_term = regularise t' rty rel lthy2;
|
|
434 |
val lam_term = Term.lambda_name (x, v) rec_term
|
|
435 |
in
|
|
436 |
Const(@{const_name "All"}, at) $ lam_term
|
|
437 |
end
|
|
438 |
| ((Const (@{const_name "All"}, at)) $ P) =>
|
|
439 |
let
|
|
440 |
val (_, [al, _]) = dest_Type (fastype_of P);
|
|
441 |
val ([x], lthy2) = Variable.variant_fixes [""] lthy;
|
|
442 |
val v = (Free (x, al));
|
|
443 |
val abs = Term.lambda_name (x, v) (P $ v);
|
|
444 |
in regularise ((Const (@{const_name "All"}, at)) $ abs) rty rel lthy2 end
|
|
445 |
| ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) =>
|
|
446 |
if (needs_lift rty T) then let
|
|
447 |
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
|
|
448 |
val v = Free (x', T);
|
|
449 |
val t' = subst_bound (v, t);
|
|
450 |
val rec_term = regularise t' rty rel lthy2;
|
|
451 |
val lam_term = Term.lambda_name (x, v) rec_term;
|
|
452 |
val sub_res_term = tyRel T rty rel lthy;
|
|
453 |
val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
|
|
454 |
val res_term = respects $ sub_res_term;
|
|
455 |
val ty = fastype_of lam_term;
|
|
456 |
val rall = Const (@{const_name Bex}, (fastype_of res_term) --> ty --> @{typ bool});
|
|
457 |
val rall_term = (rall $ res_term) $ lam_term;
|
|
458 |
in
|
|
459 |
rall_term
|
|
460 |
end else let
|
|
461 |
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
|
|
462 |
val v = Free (x', T);
|
|
463 |
val t' = subst_bound (v, t);
|
|
464 |
val rec_term = regularise t' rty rel lthy2;
|
|
465 |
val lam_term = Term.lambda_name (x, v) rec_term
|
|
466 |
in
|
|
467 |
Const(@{const_name "Ex"}, at) $ lam_term
|
|
468 |
end
|
|
469 |
| ((Const (@{const_name "Ex"}, at)) $ P) =>
|
|
470 |
let
|
|
471 |
val (_, [al, _]) = dest_Type (fastype_of P);
|
|
472 |
val ([x], lthy2) = Variable.variant_fixes [""] lthy;
|
|
473 |
val v = (Free (x, al));
|
|
474 |
val abs = Term.lambda_name (x, v) (P $ v);
|
|
475 |
in regularise ((Const (@{const_name "Ex"}, at)) $ abs) rty rel lthy2 end
|
|
476 |
| a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy)
|
|
477 |
| _ => trm
|
|
478 |
|
|
479 |
*}
|
|
480 |
|
|
481 |
(* my version of regularise *)
|
|
482 |
(****************************)
|
|
483 |
|
|
484 |
(* some helper functions *)
|
|
485 |
|
|
486 |
|
|
487 |
ML {*
|
|
488 |
fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)
|
|
489 |
fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
|
|
490 |
fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
|
|
491 |
fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})
|
|
492 |
*}
|
|
493 |
|
|
494 |
(* applies f to the subterm of an abstractions, otherwise to the given term *)
|
|
495 |
ML {*
|
|
496 |
fun apply_subt f trm =
|
|
497 |
case trm of
|
145
|
498 |
Abs (x, T, t) =>
|
|
499 |
let
|
|
500 |
val (x', t') = Term.dest_abs (x, T, t)
|
|
501 |
in
|
|
502 |
Term.absfree (x', T, f t')
|
|
503 |
end
|
139
|
504 |
| _ => f trm
|
|
505 |
*}
|
|
506 |
|
|
507 |
|
|
508 |
(* FIXME: assumes always the typ is qty! *)
|
|
509 |
(* FIXME: if there are more than one quotient, then you have to look up the relation *)
|
|
510 |
ML {*
|
|
511 |
fun my_reg rel trm =
|
|
512 |
case trm of
|
|
513 |
Abs (x, T, t) =>
|
|
514 |
let
|
|
515 |
val ty1 = fastype_of trm
|
|
516 |
in
|
146
|
517 |
(mk_babs ty1 T) $ (mk_resp T $ rel) $ (apply_subt (my_reg rel) trm)
|
139
|
518 |
end
|
|
519 |
| Const (@{const_name "All"}, ty) $ t =>
|
|
520 |
let
|
|
521 |
val ty1 = domain_type ty
|
|
522 |
val ty2 = domain_type ty1
|
|
523 |
in
|
|
524 |
(mk_ball ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)
|
|
525 |
end
|
|
526 |
| Const (@{const_name "Ex"}, ty) $ t =>
|
|
527 |
let
|
|
528 |
val ty1 = domain_type ty
|
|
529 |
val ty2 = domain_type ty1
|
|
530 |
in
|
|
531 |
(mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)
|
|
532 |
end
|
|
533 |
| t1 $ t2 => (my_reg rel t1) $ (my_reg rel t2)
|
|
534 |
| _ => trm
|
|
535 |
*}
|
|
536 |
|
|
537 |
|
|
538 |
(*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
|
|
539 |
trm == new_trm
|
|
540 |
*)
|
|
541 |
|
141
|
542 |
text {* Assumes that the given theorem is atomized *}
|
140
|
543 |
ML {*
|
|
544 |
fun build_regularize_goal thm rty rel lthy =
|
|
545 |
Logic.mk_implies
|
|
546 |
((prop_of thm),
|
|
547 |
(regularise (prop_of thm) rty rel lthy))
|
|
548 |
*}
|
|
549 |
|
187
|
550 |
ML {*
|
|
551 |
fun regularize thm rty rel rel_eqv lthy =
|
|
552 |
let
|
|
553 |
val g = build_regularize_goal thm rty rel lthy;
|
|
554 |
fun tac ctxt =
|
|
555 |
(asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
|
|
556 |
[(@{thm equiv_res_forall} OF [rel_eqv]),
|
|
557 |
(@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW
|
|
558 |
(((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN'
|
|
559 |
(MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt []));
|
|
560 |
val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);
|
|
561 |
in
|
|
562 |
cthm OF [thm]
|
|
563 |
end
|
|
564 |
*}
|
|
565 |
|
140
|
566 |
section {* RepAbs injection *}
|
139
|
567 |
|
161
|
568 |
(* Needed to have a meta-equality *)
|
|
569 |
lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
|
|
570 |
by (simp add: id_def)
|
|
571 |
|
139
|
572 |
ML {*
|
140
|
573 |
fun build_repabs_term lthy thm constructors rty qty =
|
139
|
574 |
let
|
|
575 |
fun mk_rep tm =
|
|
576 |
let
|
|
577 |
val ty = exchange_ty rty qty (fastype_of tm)
|
|
578 |
in fst (get_fun repF rty qty lthy ty) $ tm end
|
|
579 |
|
|
580 |
fun mk_abs tm =
|
|
581 |
let
|
|
582 |
val ty = exchange_ty rty qty (fastype_of tm) in
|
|
583 |
fst (get_fun absF rty qty lthy ty) $ tm end
|
|
584 |
|
|
585 |
fun is_constructor (Const (x, _)) = member (op =) constructors x
|
|
586 |
| is_constructor _ = false;
|
|
587 |
|
|
588 |
fun build_aux lthy tm =
|
|
589 |
case tm of
|
|
590 |
Abs (a as (_, vty, _)) =>
|
|
591 |
let
|
|
592 |
val (vs, t) = Term.dest_abs a;
|
|
593 |
val v = Free(vs, vty);
|
|
594 |
val t' = lambda v (build_aux lthy t)
|
|
595 |
in
|
|
596 |
if (not (needs_lift rty (fastype_of tm))) then t'
|
|
597 |
else mk_rep (mk_abs (
|
|
598 |
if not (needs_lift rty vty) then t'
|
|
599 |
else
|
|
600 |
let
|
|
601 |
val v' = mk_rep (mk_abs v);
|
|
602 |
val t1 = Envir.beta_norm (t' $ v')
|
|
603 |
in
|
|
604 |
lambda v t1
|
|
605 |
end
|
|
606 |
))
|
|
607 |
end
|
|
608 |
| x =>
|
|
609 |
let
|
|
610 |
val (opp, tms0) = Term.strip_comb tm
|
|
611 |
val tms = map (build_aux lthy) tms0
|
|
612 |
val ty = fastype_of tm
|
|
613 |
in
|
|
614 |
if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false)
|
|
615 |
then (list_comb (opp, (hd tms0) :: (tl tms)))
|
|
616 |
else if (is_constructor opp andalso needs_lift rty ty) then
|
|
617 |
mk_rep (mk_abs (list_comb (opp,tms)))
|
|
618 |
else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
|
149
|
619 |
mk_rep(mk_abs(list_comb(opp,tms)))
|
139
|
620 |
else if tms = [] then opp
|
|
621 |
else list_comb(opp, tms)
|
|
622 |
end
|
|
623 |
in
|
161
|
624 |
MetaSimplifier.rewrite_term @{theory} @{thms id_def_sym} []
|
|
625 |
(build_aux lthy (Thm.prop_of thm))
|
139
|
626 |
end
|
|
627 |
*}
|
|
628 |
|
141
|
629 |
text {* Assumes that it is given a regularized theorem *}
|
139
|
630 |
ML {*
|
140
|
631 |
fun build_repabs_goal ctxt thm cons rty qty =
|
|
632 |
Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))
|
139
|
633 |
*}
|
|
634 |
|
187
|
635 |
ML {*
|
|
636 |
fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
|
|
637 |
let
|
|
638 |
val pat = Drule.strip_imp_concl (cprop_of thm)
|
|
639 |
val insts = Thm.match (pat, concl)
|
|
640 |
in
|
|
641 |
rtac (Drule.instantiate insts thm) 1
|
152
53277fbb2dba
Simplified the proof with some tactic... Still hangs sometimes.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
642 |
end
|
187
|
643 |
handle _ => no_tac
|
|
644 |
)
|
|
645 |
*}
|
|
646 |
|
|
647 |
ML {*
|
|
648 |
fun res_forall_rsp_tac ctxt =
|
|
649 |
(simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
|
|
650 |
THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
|
|
651 |
THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
|
|
652 |
(simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
|
|
653 |
*}
|
|
654 |
|
|
655 |
ML {*
|
|
656 |
fun res_exists_rsp_tac ctxt =
|
|
657 |
(simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
|
|
658 |
THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
|
|
659 |
THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
|
|
660 |
(simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
|
|
661 |
*}
|
|
662 |
|
|
663 |
|
|
664 |
ML {*
|
|
665 |
fun quotient_tac quot_thm =
|
|
666 |
REPEAT_ALL_NEW (FIRST' [
|
|
667 |
rtac @{thm FUN_QUOTIENT},
|
|
668 |
rtac quot_thm,
|
|
669 |
rtac @{thm IDENTITY_QUOTIENT}
|
|
670 |
])
|
|
671 |
*}
|
|
672 |
|
|
673 |
ML {*
|
|
674 |
fun LAMBDA_RES_TAC ctxt i st =
|
|
675 |
(case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
|
|
676 |
(_ $ (_ $ (Abs(_,_,_))$(Abs(_,_,_)))) =>
|
|
677 |
(EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
|
|
678 |
(rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
|
|
679 |
| _ => fn _ => no_tac) i st
|
|
680 |
*}
|
|
681 |
|
|
682 |
ML {*
|
|
683 |
fun WEAK_LAMBDA_RES_TAC ctxt i st =
|
|
684 |
(case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
|
|
685 |
(_ $ (_ $ _$(Abs(_,_,_)))) =>
|
|
686 |
(EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
|
|
687 |
(rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
|
|
688 |
| (_ $ (_ $ (Abs(_,_,_))$_)) =>
|
|
689 |
(EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
|
|
690 |
(rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
|
|
691 |
| _ => fn _ => no_tac) i st
|
|
692 |
*}
|
|
693 |
|
|
694 |
|
|
695 |
ML {*
|
|
696 |
fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms =
|
|
697 |
(FIRST' [
|
|
698 |
rtac @{thm FUN_QUOTIENT},
|
|
699 |
rtac quot_thm,
|
|
700 |
rtac @{thm IDENTITY_QUOTIENT},
|
|
701 |
rtac @{thm ext},
|
|
702 |
rtac trans_thm,
|
|
703 |
LAMBDA_RES_TAC ctxt,
|
|
704 |
res_forall_rsp_tac ctxt,
|
|
705 |
res_exists_rsp_tac ctxt,
|
|
706 |
(
|
|
707 |
(simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms))
|
|
708 |
THEN_ALL_NEW (fn _ => no_tac)
|
|
709 |
),
|
|
710 |
(instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
|
|
711 |
rtac refl,
|
|
712 |
(instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
|
|
713 |
rtac reflex_thm,
|
|
714 |
atac,
|
|
715 |
(
|
|
716 |
(simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
|
|
717 |
THEN_ALL_NEW (fn _ => no_tac)
|
|
718 |
),
|
|
719 |
WEAK_LAMBDA_RES_TAC ctxt
|
|
720 |
])
|
|
721 |
*}
|
|
722 |
|
|
723 |
section {* Cleaning the goal *}
|
|
724 |
|
|
725 |
text {* Does the same as 'subst' in a given theorem *}
|
|
726 |
ML {*
|
|
727 |
fun eqsubst_thm ctxt thms thm =
|
|
728 |
let
|
|
729 |
val goalstate = Goal.init (Thm.cprop_of thm)
|
|
730 |
val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
|
|
731 |
NONE => error "eqsubst_thm"
|
|
732 |
| SOME th => cprem_of th 1
|
|
733 |
val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
|
|
734 |
val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))
|
|
735 |
val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));
|
|
736 |
in
|
|
737 |
Simplifier.rewrite_rule [rt] thm
|
|
738 |
end
|
|
739 |
*}
|
|
740 |
|
|
741 |
end
|