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