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 |
|
|
144 |
section {* type definition for the quotient type *}
|
|
145 |
|
71
|
146 |
use "quotient.ML"
|
0
|
147 |
|
79
c0c41fefeb06
added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
148 |
term EQUIV
|
c0c41fefeb06
added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
149 |
|
14
|
150 |
ML {*
|
|
151 |
val no_vars = Thm.rule_attribute (fn context => fn th =>
|
|
152 |
let
|
|
153 |
val ctxt = Variable.set_body false (Context.proof_of context);
|
|
154 |
val ((_, [th']), _) = Variable.import true [th] ctxt;
|
|
155 |
in th' end);
|
|
156 |
*}
|
|
157 |
|
0
|
158 |
section {* various tests for quotient types*}
|
|
159 |
datatype trm =
|
15
|
160 |
var "nat"
|
0
|
161 |
| app "trm" "trm"
|
|
162 |
| lam "nat" "trm"
|
13
|
163 |
|
49
|
164 |
axiomatization
|
|
165 |
RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"
|
26
|
166 |
where
|
14
|
167 |
r_eq: "EQUIV RR"
|
0
|
168 |
|
81
|
169 |
quotient qtrm = trm / "RR"
|
79
c0c41fefeb06
added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
170 |
apply(rule r_eq)
|
c0c41fefeb06
added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
171 |
done
|
c0c41fefeb06
added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
172 |
|
c0c41fefeb06
added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
173 |
typ qtrm
|
0
|
174 |
term Rep_qtrm
|
2
|
175 |
term REP_qtrm
|
0
|
176 |
term Abs_qtrm
|
|
177 |
term ABS_qtrm
|
|
178 |
thm QUOT_TYPE_qtrm
|
|
179 |
thm QUOTIENT_qtrm
|
79
c0c41fefeb06
added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
180 |
thm REP_qtrm_def
|
2
|
181 |
|
16
|
182 |
(* Test interpretation *)
|
|
183 |
thm QUOT_TYPE_I_qtrm.thm11
|
26
|
184 |
thm QUOT_TYPE.thm11
|
16
|
185 |
|
21
|
186 |
print_theorems
|
|
187 |
|
0
|
188 |
thm Rep_qtrm
|
|
189 |
|
|
190 |
text {* another test *}
|
|
191 |
datatype 'a trm' =
|
15
|
192 |
var' "'a"
|
0
|
193 |
| app' "'a trm'" "'a trm'"
|
|
194 |
| lam' "'a" "'a trm'"
|
15
|
195 |
|
0
|
196 |
consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"
|
|
197 |
axioms r_eq': "EQUIV R'"
|
|
198 |
|
81
|
199 |
quotient qtrm' = "'a trm'" / "R'"
|
79
c0c41fefeb06
added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
200 |
apply(rule r_eq')
|
c0c41fefeb06
added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
201 |
done
|
0
|
202 |
|
14
|
203 |
print_theorems
|
|
204 |
|
0
|
205 |
term ABS_qtrm'
|
|
206 |
term REP_qtrm'
|
|
207 |
thm QUOT_TYPE_qtrm'
|
|
208 |
thm QUOTIENT_qtrm'
|
|
209 |
thm Rep_qtrm'
|
|
210 |
|
14
|
211 |
|
0
|
212 |
text {* a test with lists of terms *}
|
|
213 |
datatype t =
|
|
214 |
vr "string"
|
|
215 |
| ap "t list"
|
|
216 |
| lm "string" "t"
|
|
217 |
|
|
218 |
consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
|
|
219 |
axioms t_eq: "EQUIV Rt"
|
|
220 |
|
81
|
221 |
quotient qt = "t" / "Rt"
|
79
c0c41fefeb06
added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
222 |
by (rule t_eq)
|
0
|
223 |
|
|
224 |
section {* lifting of constants *}
|
|
225 |
|
|
226 |
text {* information about map-functions for type-constructor *}
|
|
227 |
ML {*
|
75
|
228 |
type typ_info = {mapfun: string, relfun: string}
|
0
|
229 |
|
|
230 |
local
|
59
1a92820a5b85
simplified the storage of the map-functions by using TheoryDataFun
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
231 |
structure Data = TheoryDataFun
|
0
|
232 |
(type T = typ_info Symtab.table
|
|
233 |
val empty = Symtab.empty
|
59
1a92820a5b85
simplified the storage of the map-functions by using TheoryDataFun
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
234 |
val copy = I
|
0
|
235 |
val extend = I
|
|
236 |
fun merge _ = Symtab.merge (K true))
|
|
237 |
in
|
46
|
238 |
val lookup = Symtab.lookup o Data.get
|
|
239 |
fun update k v = Data.map (Symtab.update (k, v))
|
0
|
240 |
end
|
|
241 |
*}
|
|
242 |
|
|
243 |
(* mapfuns for some standard types *)
|
|
244 |
setup {*
|
75
|
245 |
update @{type_name "list"} {mapfun = @{const_name "map"}, relfun = @{const_name "LIST_REL"}} #>
|
|
246 |
update @{type_name "*"} {mapfun = @{const_name "prod_fun"}, relfun = "???"} #>
|
|
247 |
update @{type_name "fun"} {mapfun = @{const_name "fun_map"}, relfun = @{const_name "FUN_REL"}}
|
0
|
248 |
*}
|
|
249 |
|
59
1a92820a5b85
simplified the storage of the map-functions by using TheoryDataFun
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
250 |
ML {* lookup @{theory} @{type_name list} *}
|
0
|
251 |
|
|
252 |
ML {*
|
46
|
253 |
datatype flag = absF | repF
|
0
|
254 |
|
46
|
255 |
fun get_fun flag rty qty lthy ty =
|
0
|
256 |
let
|
|
257 |
val qty_name = Long_Name.base_name (fst (dest_Type qty))
|
15
|
258 |
|
0
|
259 |
fun get_fun_aux s fs_tys =
|
|
260 |
let
|
|
261 |
val (fs, tys) = split_list fs_tys
|
15
|
262 |
val (otys, ntys) = split_list tys
|
0
|
263 |
val oty = Type (s, otys)
|
|
264 |
val nty = Type (s, ntys)
|
|
265 |
val ftys = map (op -->) tys
|
|
266 |
in
|
59
1a92820a5b85
simplified the storage of the map-functions by using TheoryDataFun
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
267 |
(case (lookup (ProofContext.theory_of lthy) s) of
|
0
|
268 |
SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty))
|
41
|
269 |
| NONE => raise ERROR ("no map association for type " ^ s))
|
0
|
270 |
end
|
|
271 |
|
46
|
272 |
fun get_const absF = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty))
|
|
273 |
| get_const repF = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty))
|
41
|
274 |
|
70
f3cbda066c3a
consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
275 |
fun mk_identity ty = Abs ("", ty, Bound 0)
|
41
|
276 |
|
0
|
277 |
in
|
|
278 |
if ty = qty
|
46
|
279 |
then (get_const flag)
|
0
|
280 |
else (case ty of
|
41
|
281 |
TFree _ => (mk_identity ty, (ty, ty))
|
|
282 |
| Type (_, []) => (mk_identity ty, (ty, ty))
|
46
|
283 |
| Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys)
|
41
|
284 |
| _ => raise ERROR ("no type variables")
|
0
|
285 |
)
|
|
286 |
end
|
|
287 |
*}
|
|
288 |
|
|
289 |
ML {*
|
75
|
290 |
get_fun repF @{typ t} @{typ qt} @{context} @{typ "((t \<Rightarrow> t) list) * nat"}
|
2
|
291 |
|> fst
|
|
292 |
|> Syntax.string_of_term @{context}
|
|
293 |
|> writeln
|
|
294 |
*}
|
|
295 |
|
46
|
296 |
ML {*
|
|
297 |
get_fun absF @{typ t} @{typ qt} @{context} @{typ "t * nat"}
|
|
298 |
|> fst
|
|
299 |
|> Syntax.string_of_term @{context}
|
|
300 |
|> writeln
|
|
301 |
*}
|
2
|
302 |
|
84
|
303 |
text {* tyRel takes a type and builds a relation that a quantifier over this
|
|
304 |
type needs to respect. *}
|
75
|
305 |
ML {*
|
|
306 |
fun tyRel ty rty rel lthy =
|
76
|
307 |
if ty = rty then rel
|
75
|
308 |
else (case ty of
|
76
|
309 |
Type (s, tys) =>
|
|
310 |
let
|
|
311 |
val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
|
|
312 |
val ty_out = ty --> ty --> @{typ bool};
|
|
313 |
val tys_out = tys_rel ---> ty_out;
|
|
314 |
in
|
75
|
315 |
(case (lookup (ProofContext.theory_of lthy) s) of
|
76
|
316 |
SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
|
|
317 |
| NONE => Const (@{const_name "op ="}, ty --> ty --> @{typ bool})
|
75
|
318 |
)
|
76
|
319 |
end
|
|
320 |
| _ => Const (@{const_name "op ="}, ty --> ty --> @{typ bool}))
|
75
|
321 |
*}
|
|
322 |
|
|
323 |
ML {*
|
76
|
324 |
cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context})
|
|
325 |
*}
|
86
|
326 |
|
|
327 |
definition
|
|
328 |
"(x : p) \<Longrightarrow> (Babs p m x = m x)"
|
|
329 |
|
87
|
330 |
(*definition BAll :: "('a \<Rightarrow> prop) \<Rightarrow> ('a \<Rightarrow> prop) \<Rightarrow> prop" where
|
|
331 |
"BAll (R :: 'a \<Rightarrow> prop) (P :: 'a \<Rightarrow> prop) \<equiv> (\<And>x. (PROP R x \<Longrightarrow> PROP P x))"*)
|
86
|
332 |
|
75
|
333 |
|
84
|
334 |
ML {*
|
|
335 |
(* trm \<Rightarrow> new_trm *)
|
|
336 |
fun regularise trm rty rel lthy =
|
|
337 |
case trm of
|
|
338 |
Abs (x, T, t) =>
|
|
339 |
if T = rty then let
|
|
340 |
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
|
|
341 |
val v = Free (x', rty);
|
|
342 |
val t' = subst_bound (v, t);
|
|
343 |
val rec_term = regularise t' rty rel lthy2;
|
|
344 |
val lam_term = Term.lambda_name (x, v) rec_term;
|
|
345 |
val sub_res_term = tyRel T rty rel lthy;
|
|
346 |
val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
|
|
347 |
val res_term = respects $ sub_res_term;
|
|
348 |
val ty = fastype_of trm;
|
|
349 |
val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty);
|
86
|
350 |
val rabs_term = (rabs $ res_term) $ lam_term;
|
84
|
351 |
in
|
|
352 |
rabs_term
|
|
353 |
end else let
|
|
354 |
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
|
|
355 |
val v = Free (x', rty);
|
|
356 |
val t' = subst_bound (v, t);
|
|
357 |
val rec_term = regularise t' rty rel lthy2;
|
|
358 |
in
|
|
359 |
Term.lambda_name (x, v) rec_term
|
|
360 |
end
|
86
|
361 |
| ((Const (@{const_name "All"}, _)) $ (Abs (x, T, t))) =>
|
|
362 |
if T = rty then let
|
|
363 |
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
|
|
364 |
val v = Free (x', rty);
|
|
365 |
val t' = subst_bound (v, t);
|
|
366 |
val rec_term = regularise t' rty rel lthy2;
|
|
367 |
val lam_term = Term.lambda_name (x, v) rec_term;
|
|
368 |
val sub_res_term = tyRel T rty rel lthy;
|
|
369 |
val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
|
|
370 |
val res_term = respects $ sub_res_term;
|
|
371 |
val ty = fastype_of lam_term;
|
|
372 |
val rall = Const (@{const_name Ball}, (fastype_of res_term) --> ty --> @{typ bool});
|
|
373 |
val rall_term = (rall $ res_term) $ lam_term;
|
|
374 |
in
|
|
375 |
rall_term
|
|
376 |
end else let
|
|
377 |
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
|
|
378 |
val v = Free (x', rty);
|
|
379 |
val t' = subst_bound (v, t);
|
|
380 |
val rec_term = regularise t' rty rel lthy2;
|
|
381 |
in
|
|
382 |
Term.lambda_name (x, v) rec_term
|
|
383 |
end
|
87
|
384 |
| ((Const (@{const_name "Ex"}, _)) $ (Abs (x, T, t))) =>
|
|
385 |
if T = rty then let
|
|
386 |
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
|
|
387 |
val v = Free (x', rty);
|
|
388 |
val t' = subst_bound (v, t);
|
|
389 |
val rec_term = regularise t' rty rel lthy2;
|
|
390 |
val lam_term = Term.lambda_name (x, v) rec_term;
|
|
391 |
val sub_res_term = tyRel T rty rel lthy;
|
|
392 |
val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
|
|
393 |
val res_term = respects $ sub_res_term;
|
|
394 |
val ty = fastype_of lam_term;
|
|
395 |
val rall = Const (@{const_name Bex}, (fastype_of res_term) --> ty --> @{typ bool});
|
|
396 |
val rall_term = (rall $ res_term) $ lam_term;
|
|
397 |
in
|
|
398 |
rall_term
|
|
399 |
end else let
|
|
400 |
val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
|
|
401 |
val v = Free (x', rty);
|
|
402 |
val t' = subst_bound (v, t);
|
|
403 |
val rec_term = regularise t' rty rel lthy2;
|
|
404 |
in
|
|
405 |
Term.lambda_name (x, v) rec_term
|
|
406 |
end
|
84
|
407 |
| _ => trm
|
|
408 |
|
75
|
409 |
*}
|
85
dbffc6477c08
":" is used for being in a set, "IN" means something else...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
410 |
|
dbffc6477c08
":" is used for being in a set, "IN" means something else...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
411 |
ML {*
|
86
|
412 |
cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
|
87
|
413 |
cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
|
|
414 |
cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context})
|
|
415 |
*}
|
|
416 |
|
|
417 |
|
|
418 |
ML {*
|
88
|
419 |
fun atomize_thm thm =
|
|
420 |
let
|
|
421 |
val thm' = forall_intr_vars thm
|
|
422 |
val thm'' = ObjectLogic.atomize (cprop_of thm')
|
|
423 |
in
|
|
424 |
Simplifier.rewrite_rule [thm''] thm'
|
|
425 |
end
|
85
dbffc6477c08
":" is used for being in a set, "IN" means something else...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
426 |
*}
|
dbffc6477c08
":" is used for being in a set, "IN" means something else...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
427 |
|
88
|
428 |
thm list.induct
|
|
429 |
ML {* atomize_thm @{thm list.induct} *}
|
87
|
430 |
|
86
|
431 |
(*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
|
75
|
432 |
trm == new_trm
|
|
433 |
*)
|
|
434 |
|
86
|
435 |
|
41
|
436 |
text {* produces the definition for a lifted constant *}
|
86
|
437 |
|
2
|
438 |
ML {*
|
0
|
439 |
fun get_const_def nconst oconst rty qty lthy =
|
|
440 |
let
|
|
441 |
val ty = fastype_of nconst
|
|
442 |
val (arg_tys, res_ty) = strip_type ty
|
14
|
443 |
|
0
|
444 |
val fresh_args = arg_tys |> map (pair "x")
|
15
|
445 |
|> Variable.variant_frees lthy [nconst, oconst]
|
0
|
446 |
|> map Free
|
|
447 |
|
46
|
448 |
val rep_fns = map (fst o get_fun repF rty qty lthy) arg_tys
|
|
449 |
val abs_fn = (fst o get_fun absF rty qty lthy) res_ty
|
0
|
450 |
|
|
451 |
in
|
|
452 |
map (op $) (rep_fns ~~ fresh_args)
|
|
453 |
|> curry list_comb oconst
|
|
454 |
|> curry (op $) abs_fn
|
|
455 |
|> fold_rev lambda fresh_args
|
|
456 |
end
|
|
457 |
*}
|
|
458 |
|
|
459 |
ML {*
|
15
|
460 |
fun exchange_ty rty qty ty =
|
49
|
461 |
if ty = rty
|
41
|
462 |
then qty
|
15
|
463 |
else
|
0
|
464 |
(case ty of
|
|
465 |
Type (s, tys) => Type (s, map (exchange_ty rty qty) tys)
|
41
|
466 |
| _ => ty
|
|
467 |
)
|
0
|
468 |
*}
|
|
469 |
|
|
470 |
ML {*
|
17
|
471 |
fun make_const_def nconst_bname oconst mx rty qty lthy =
|
0
|
472 |
let
|
|
473 |
val oconst_ty = fastype_of oconst
|
|
474 |
val nconst_ty = exchange_ty rty qty oconst_ty
|
17
|
475 |
val nconst = Const (Binding.name_of nconst_bname, nconst_ty)
|
0
|
476 |
val def_trm = get_const_def nconst oconst rty qty lthy
|
|
477 |
in
|
79
c0c41fefeb06
added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
478 |
define (nconst_bname, mx, def_trm) lthy
|
15
|
479 |
end
|
0
|
480 |
*}
|
|
481 |
|
2
|
482 |
local_setup {*
|
41
|
483 |
make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>
|
|
484 |
make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>
|
17
|
485 |
make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd
|
2
|
486 |
*}
|
|
487 |
|
41
|
488 |
term vr
|
|
489 |
term ap
|
|
490 |
term lm
|
|
491 |
thm VR_def AP_def LM_def
|
14
|
492 |
term LM
|
2
|
493 |
term VR
|
|
494 |
term AP
|
|
495 |
|
0
|
496 |
text {* a test with functions *}
|
|
497 |
datatype 'a t' =
|
|
498 |
vr' "string"
|
|
499 |
| ap' "('a t') * ('a t')"
|
|
500 |
| lm' "'a" "string \<Rightarrow> ('a t')"
|
|
501 |
|
|
502 |
consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
|
|
503 |
axioms t_eq': "EQUIV Rt'"
|
|
504 |
|
81
|
505 |
quotient qt' = "'a t'" / "Rt'"
|
79
c0c41fefeb06
added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
506 |
apply(rule t_eq')
|
c0c41fefeb06
added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
507 |
done
|
0
|
508 |
|
14
|
509 |
print_theorems
|
2
|
510 |
|
0
|
511 |
local_setup {*
|
41
|
512 |
make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>
|
|
513 |
make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>
|
17
|
514 |
make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
|
0
|
515 |
*}
|
|
516 |
|
41
|
517 |
term vr'
|
|
518 |
term ap'
|
|
519 |
term ap'
|
|
520 |
thm VR'_def AP'_def LM'_def
|
14
|
521 |
term LM'
|
0
|
522 |
term VR'
|
|
523 |
term AP'
|
|
524 |
|
14
|
525 |
|
0
|
526 |
text {* finite set example *}
|
13
|
527 |
print_syntax
|
14
|
528 |
inductive
|
13
|
529 |
list_eq (infix "\<approx>" 50)
|
0
|
530 |
where
|
|
531 |
"a#b#xs \<approx> b#a#xs"
|
|
532 |
| "[] \<approx> []"
|
|
533 |
| "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"
|
|
534 |
| "a#a#xs \<approx> a#xs"
|
|
535 |
| "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"
|
|
536 |
| "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"
|
|
537 |
|
47
|
538 |
lemma list_eq_refl:
|
0
|
539 |
shows "xs \<approx> xs"
|
13
|
540 |
apply (induct xs)
|
|
541 |
apply (auto intro: list_eq.intros)
|
|
542 |
done
|
0
|
543 |
|
|
544 |
lemma equiv_list_eq:
|
|
545 |
shows "EQUIV list_eq"
|
13
|
546 |
unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def
|
47
|
547 |
apply(auto intro: list_eq.intros list_eq_refl)
|
13
|
548 |
done
|
0
|
549 |
|
81
|
550 |
quotient fset = "'a list" / "list_eq"
|
79
c0c41fefeb06
added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
551 |
apply(rule equiv_list_eq)
|
c0c41fefeb06
added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
552 |
done
|
0
|
553 |
|
14
|
554 |
print_theorems
|
|
555 |
|
0
|
556 |
typ "'a fset"
|
|
557 |
thm "Rep_fset"
|
|
558 |
|
|
559 |
local_setup {*
|
17
|
560 |
make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
|
0
|
561 |
*}
|
|
562 |
|
14
|
563 |
term Nil
|
0
|
564 |
term EMPTY
|
2
|
565 |
thm EMPTY_def
|
|
566 |
|
0
|
567 |
|
|
568 |
local_setup {*
|
17
|
569 |
make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
|
0
|
570 |
*}
|
|
571 |
|
14
|
572 |
term Cons
|
0
|
573 |
term INSERT
|
2
|
574 |
thm INSERT_def
|
0
|
575 |
|
|
576 |
local_setup {*
|
17
|
577 |
make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
|
0
|
578 |
*}
|
|
579 |
|
15
|
580 |
term append
|
0
|
581 |
term UNION
|
2
|
582 |
thm UNION_def
|
|
583 |
|
7
|
584 |
|
0
|
585 |
thm QUOTIENT_fset
|
|
586 |
|
14
|
587 |
thm QUOT_TYPE_I_fset.thm11
|
9
|
588 |
|
|
589 |
|
13
|
590 |
fun
|
|
591 |
membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100)
|
0
|
592 |
where
|
|
593 |
m1: "(x memb []) = False"
|
|
594 |
| m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"
|
|
595 |
|
2
|
596 |
lemma mem_respects:
|
9
|
597 |
fixes z
|
2
|
598 |
assumes a: "list_eq x y"
|
9
|
599 |
shows "(z memb x) = (z memb y)"
|
13
|
600 |
using a by induct auto
|
|
601 |
|
2
|
602 |
|
29
|
603 |
fun
|
|
604 |
card1 :: "'a list \<Rightarrow> nat"
|
|
605 |
where
|
|
606 |
card1_nil: "(card1 []) = 0"
|
|
607 |
| card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"
|
|
608 |
|
|
609 |
local_setup {*
|
|
610 |
make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
|
|
611 |
*}
|
|
612 |
|
|
613 |
term card1
|
|
614 |
term card
|
|
615 |
thm card_def
|
|
616 |
|
|
617 |
(* text {*
|
|
618 |
Maybe make_const_def should require a theorem that says that the particular lifted function
|
|
619 |
respects the relation. With it such a definition would be impossible:
|
|
620 |
make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
|
41
|
621 |
*}*)
|
29
|
622 |
|
|
623 |
lemma card1_rsp:
|
|
624 |
fixes a b :: "'a list"
|
|
625 |
assumes e: "a \<approx> b"
|
|
626 |
shows "card1 a = card1 b"
|
|
627 |
using e apply induct
|
|
628 |
apply (simp_all add:mem_respects)
|
|
629 |
done
|
|
630 |
|
|
631 |
lemma card1_0:
|
|
632 |
fixes a :: "'a list"
|
|
633 |
shows "(card1 a = 0) = (a = [])"
|
|
634 |
apply (induct a)
|
|
635 |
apply (simp)
|
|
636 |
apply (simp_all)
|
|
637 |
apply meson
|
|
638 |
apply (simp_all)
|
|
639 |
done
|
|
640 |
|
|
641 |
lemma not_mem_card1:
|
|
642 |
fixes x :: "'a"
|
|
643 |
fixes xs :: "'a list"
|
|
644 |
shows "~(x memb xs) \<Longrightarrow> card1 (x # xs) = Suc (card1 xs)"
|
|
645 |
by simp
|
|
646 |
|
|
647 |
|
|
648 |
lemma mem_cons:
|
|
649 |
fixes x :: "'a"
|
|
650 |
fixes xs :: "'a list"
|
|
651 |
assumes a : "x memb xs"
|
|
652 |
shows "x # xs \<approx> xs"
|
49
|
653 |
using a
|
38
|
654 |
apply (induct xs)
|
|
655 |
apply (auto intro: list_eq.intros)
|
|
656 |
done
|
29
|
657 |
|
|
658 |
lemma card1_suc:
|
|
659 |
fixes xs :: "'a list"
|
|
660 |
fixes n :: "nat"
|
|
661 |
assumes c: "card1 xs = Suc n"
|
|
662 |
shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)"
|
49
|
663 |
using c
|
38
|
664 |
apply(induct xs)
|
|
665 |
apply (metis Suc_neq_Zero card1_0)
|
47
|
666 |
apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_refl mem_cons)
|
38
|
667 |
done
|
29
|
668 |
|
12
|
669 |
lemma cons_preserves:
|
|
670 |
fixes z
|
|
671 |
assumes a: "xs \<approx> ys"
|
|
672 |
shows "(z # xs) \<approx> (z # ys)"
|
13
|
673 |
using a by (rule QuotMain.list_eq.intros(5))
|
12
|
674 |
|
60
4826ad24f772
First theorem with quantifiers. Learned how to use sledgehammer.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
675 |
lemma fs1_strong_cases:
|
4826ad24f772
First theorem with quantifiers. Learned how to use sledgehammer.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
676 |
fixes X :: "'a list"
|
4826ad24f772
First theorem with quantifiers. Learned how to use sledgehammer.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
677 |
shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"
|
4826ad24f772
First theorem with quantifiers. Learned how to use sledgehammer.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
678 |
apply (induct X)
|
4826ad24f772
First theorem with quantifiers. Learned how to use sledgehammer.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
679 |
apply (simp)
|
72
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
680 |
apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons QuotMain.m1)
|
60
4826ad24f772
First theorem with quantifiers. Learned how to use sledgehammer.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
681 |
done
|
29
|
682 |
|
72
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
683 |
|
29
|
684 |
text {*
|
68
e8660818c755
renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
685 |
Unabs_def converts a definition given as
|
40
|
686 |
|
|
687 |
c \<equiv> %x. %y. f x y
|
|
688 |
|
49
|
689 |
to a theorem of the form
|
|
690 |
|
|
691 |
c x y \<equiv> f x y
|
40
|
692 |
|
|
693 |
This function is needed to rewrite the right-hand
|
|
694 |
side to the left-hand side.
|
29
|
695 |
*}
|
|
696 |
|
11
|
697 |
ML {*
|
68
e8660818c755
renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
698 |
fun unabs_def ctxt def =
|
64
|
699 |
let
|
|
700 |
val (lhs, rhs) = Thm.dest_equals (cprop_of def)
|
|
701 |
val xs = strip_abs_vars (term_of rhs)
|
|
702 |
val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
|
65
|
703 |
|
|
704 |
val thy = ProofContext.theory_of ctxt'
|
66
|
705 |
val cxs = map (cterm_of thy o Free) xs
|
|
706 |
val new_lhs = Drule.list_comb (lhs, cxs)
|
64
|
707 |
|
|
708 |
fun get_conv [] = Conv.rewr_conv def
|
|
709 |
| get_conv (x::xs) = Conv.fun_conv (get_conv xs)
|
|
710 |
in
|
66
|
711 |
get_conv xs new_lhs |>
|
64
|
712 |
singleton (ProofContext.export ctxt' ctxt)
|
|
713 |
end
|
10
|
714 |
*}
|
9
|
715 |
|
10
|
716 |
local_setup {*
|
17
|
717 |
make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
|
10
|
718 |
*}
|
|
719 |
|
0
|
720 |
term membship
|
|
721 |
term IN
|
2
|
722 |
thm IN_def
|
66
|
723 |
|
68
e8660818c755
renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
724 |
(* unabs_def tests *)
|
67
|
725 |
ML {* (Conv.fun_conv (Conv.fun_conv (Conv.rewr_conv @{thm IN_def}))) @{cterm "IN x y"} *}
|
64
|
726 |
ML {* MetaSimplifier.rewrite_rule @{thms IN_def} @{thm IN_def}*}
|
68
e8660818c755
renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
727 |
ML {* @{thm IN_def}; unabs_def @{context} @{thm IN_def} *}
|
0
|
728 |
|
2
|
729 |
lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset]
|
|
730 |
thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a]
|
0
|
731 |
|
2
|
732 |
lemma yy:
|
|
733 |
shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"
|
|
734 |
unfolding IN_def EMPTY_def
|
|
735 |
apply(rule_tac f="(op =) False" in arg_cong)
|
|
736 |
apply(rule mem_respects)
|
14
|
737 |
apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
|
2
|
738 |
apply(rule list_eq.intros)
|
0
|
739 |
done
|
|
740 |
|
2
|
741 |
lemma
|
|
742 |
shows "IN (x::nat) EMPTY = False"
|
|
743 |
using m1
|
|
744 |
apply -
|
|
745 |
apply(rule yy[THEN iffD1, symmetric])
|
|
746 |
apply(simp)
|
0
|
747 |
done
|
|
748 |
|
2
|
749 |
lemma
|
|
750 |
shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) =
|
23
|
751 |
((x=y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))"
|
2
|
752 |
unfolding IN_def INSERT_def
|
|
753 |
apply(rule_tac f="(op \<or>) (x=y)" in arg_cong)
|
|
754 |
apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong)
|
|
755 |
apply(rule mem_respects)
|
|
756 |
apply(rule list_eq.intros(3))
|
|
757 |
apply(unfold REP_fset_def ABS_fset_def)
|
5
|
758 |
apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
|
47
|
759 |
apply(rule list_eq_refl)
|
2
|
760 |
done
|
0
|
761 |
|
7
|
762 |
lemma append_respects_fst:
|
14
|
763 |
assumes a : "list_eq l1 l2"
|
4
|
764 |
shows "list_eq (l1 @ s) (l2 @ s)"
|
3
|
765 |
using a
|
|
766 |
apply(induct)
|
4
|
767 |
apply(auto intro: list_eq.intros)
|
47
|
768 |
apply(simp add: list_eq_refl)
|
3
|
769 |
done
|
|
770 |
|
18
|
771 |
lemma yyy:
|
3
|
772 |
shows "
|
|
773 |
(
|
|
774 |
(UNION EMPTY s = s) &
|
|
775 |
((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))
|
|
776 |
) = (
|
|
777 |
((ABS_fset ([] @ REP_fset s)) = s) &
|
|
778 |
((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2)))
|
|
779 |
)"
|
|
780 |
unfolding UNION_def EMPTY_def INSERT_def
|
|
781 |
apply(rule_tac f="(op &)" in arg_cong2)
|
|
782 |
apply(rule_tac f="(op =)" in arg_cong2)
|
14
|
783 |
apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
|
7
|
784 |
apply(rule append_respects_fst)
|
18
|
785 |
apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
|
47
|
786 |
apply(rule list_eq_refl)
|
3
|
787 |
apply(simp)
|
|
788 |
apply(rule_tac f="(op =)" in arg_cong2)
|
14
|
789 |
apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
|
7
|
790 |
apply(rule append_respects_fst)
|
14
|
791 |
apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
|
47
|
792 |
apply(rule list_eq_refl)
|
14
|
793 |
apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
|
3
|
794 |
apply(rule list_eq.intros(5))
|
14
|
795 |
apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
|
47
|
796 |
apply(rule list_eq_refl)
|
3
|
797 |
done
|
|
798 |
|
|
799 |
lemma
|
|
800 |
shows "
|
|
801 |
(UNION EMPTY s = s) &
|
7
|
802 |
((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))"
|
|
803 |
apply (simp add: yyy)
|
24
|
804 |
apply (simp add: QUOT_TYPE_I_fset.thm10)
|
7
|
805 |
done
|
3
|
806 |
|
8
|
807 |
ML {*
|
55
|
808 |
fun mk_rep x = @{term REP_fset} $ x;
|
|
809 |
fun mk_abs x = @{term ABS_fset} $ x;
|
49
|
810 |
val consts = [@{const_name "Nil"}, @{const_name "append"},
|
|
811 |
@{const_name "Cons"}, @{const_name "membship"},
|
41
|
812 |
@{const_name "card1"}]
|
8
|
813 |
*}
|
|
814 |
|
56
|
815 |
ML {* val qty = @{typ "'a fset"} *}
|
|
816 |
ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *}
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
817 |
ML {* val fall = Const(@{const_name all}, dummyT) *}
|
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
818 |
|
8
|
819 |
ML {*
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
820 |
fun build_goal_term ctxt thm constructors rty qty mk_rep mk_abs =
|
49
|
821 |
let
|
55
|
822 |
fun mk_rep_abs x = mk_rep (mk_abs x);
|
|
823 |
|
49
|
824 |
fun is_constructor (Const (x, _)) = member (op =) constructors x
|
|
825 |
| is_constructor _ = false;
|
|
826 |
|
43
|
827 |
fun maybe_mk_rep_abs t =
|
49
|
828 |
let
|
|
829 |
val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t)
|
|
830 |
in
|
55
|
831 |
if fastype_of t = rty then mk_rep_abs t else t
|
49
|
832 |
end;
|
|
833 |
|
56
|
834 |
fun is_all (Const ("all", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty
|
|
835 |
| is_all _ = false;
|
|
836 |
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
837 |
fun is_ex (Const ("Ex", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty
|
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
838 |
| is_ex _ = false;
|
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
839 |
|
49
|
840 |
fun build_aux ctxt1 tm =
|
|
841 |
let
|
|
842 |
val (head, args) = Term.strip_comb tm;
|
|
843 |
val args' = map (build_aux ctxt1) args;
|
|
844 |
in
|
|
845 |
(case head of
|
|
846 |
Abs (x, T, t) =>
|
55
|
847 |
if T = rty then let
|
|
848 |
val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;
|
|
849 |
val v = Free (x', qty);
|
|
850 |
val t' = subst_bound (mk_rep v, t);
|
|
851 |
val rec_term = build_aux ctxt2 t';
|
|
852 |
val _ = tracing (Syntax.string_of_term ctxt2 t')
|
|
853 |
val _ = tracing (Syntax.string_of_term ctxt2 (Term.lambda_name (x, v) rec_term))
|
|
854 |
in
|
|
855 |
Term.lambda_name (x, v) rec_term
|
|
856 |
end else let
|
49
|
857 |
val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;
|
|
858 |
val v = Free (x', T);
|
|
859 |
val t' = subst_bound (v, t);
|
|
860 |
val rec_term = build_aux ctxt2 t';
|
|
861 |
in Term.lambda_name (x, v) rec_term end
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
862 |
| _ => (* I assume that we never lift 'prop' since it is not of sort type *)
|
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
863 |
if is_all head then
|
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
864 |
list_comb (Const(@{const_name all}, dummyT), args') |> Syntax.check_term ctxt1
|
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
865 |
else if is_ex head then
|
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
866 |
list_comb (Const(@{const_name Ex}, dummyT), args') |> Syntax.check_term ctxt1
|
56
|
867 |
else if is_constructor head then
|
49
|
868 |
maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args'))
|
56
|
869 |
else
|
|
870 |
maybe_mk_rep_abs (list_comb (head, args'))
|
|
871 |
)
|
49
|
872 |
end;
|
|
873 |
in
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
874 |
build_aux ctxt (Thm.prop_of thm)
|
49
|
875 |
end
|
|
876 |
*}
|
|
877 |
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
878 |
ML {*
|
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
879 |
fun build_goal ctxt thm cons rty qty mk_rep mk_abs =
|
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
880 |
Logic.mk_equals ((build_goal_term ctxt thm cons rty qty mk_rep mk_abs), (Thm.prop_of thm))
|
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
881 |
*}
|
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
882 |
|
67
|
883 |
ML {*
|
|
884 |
val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
|
|
885 |
*}
|
|
886 |
|
|
887 |
ML {*
|
|
888 |
m1_novars |> prop_of
|
|
889 |
|> Syntax.string_of_term @{context}
|
|
890 |
|> writeln;
|
|
891 |
build_goal_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
|
|
892 |
|> Syntax.string_of_term @{context}
|
|
893 |
|> writeln
|
|
894 |
*}
|
|
895 |
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
896 |
|
29
|
897 |
ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
|
68
e8660818c755
renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
898 |
ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}
|
18
|
899 |
|
|
900 |
ML {*
|
|
901 |
fun dest_cbinop t =
|
|
902 |
let
|
|
903 |
val (t2, rhs) = Thm.dest_comb t;
|
|
904 |
val (bop, lhs) = Thm.dest_comb t2;
|
|
905 |
in
|
|
906 |
(bop, (lhs, rhs))
|
|
907 |
end
|
|
908 |
*}
|
38
|
909 |
|
18
|
910 |
ML {*
|
|
911 |
fun dest_ceq t =
|
|
912 |
let
|
|
913 |
val (bop, pair) = dest_cbinop t;
|
49
|
914 |
val (bop_s, _) = Term.dest_Const (Thm.term_of bop);
|
18
|
915 |
in
|
|
916 |
if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))
|
|
917 |
end
|
|
918 |
*}
|
38
|
919 |
|
19
|
920 |
ML Thm.instantiate
|
|
921 |
ML {*@{thm arg_cong2}*}
|
|
922 |
ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *}
|
|
923 |
ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *}
|
25
|
924 |
ML {*
|
19
|
925 |
Toplevel.program (fn () =>
|
50
18d8bcd769b3
Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
926 |
Drule.instantiate' [SOME cT, SOME cT, SOME @{ctyp bool}] [NONE, NONE, NONE, NONE, SOME (@{cpat "op ="})] @{thm arg_cong2}
|
19
|
927 |
)
|
|
928 |
*}
|
|
929 |
|
18
|
930 |
ML {*
|
49
|
931 |
fun split_binop_conv t =
|
18
|
932 |
let
|
|
933 |
val (lhs, rhs) = dest_ceq t;
|
|
934 |
val (bop, _) = dest_cbinop lhs;
|
19
|
935 |
val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
|
|
936 |
val [cmT, crT] = Thm.dest_ctyp cr2;
|
18
|
937 |
in
|
49
|
938 |
Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}
|
|
939 |
end
|
|
940 |
*}
|
|
941 |
|
|
942 |
ML {*
|
|
943 |
fun split_arg_conv t =
|
|
944 |
let
|
|
945 |
val (lhs, rhs) = dest_ceq t;
|
|
946 |
val (lop, larg) = Thm.dest_comb lhs;
|
|
947 |
val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
|
|
948 |
in
|
|
949 |
Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}
|
35
|
950 |
end
|
|
951 |
*}
|
|
952 |
|
|
953 |
ML {*
|
49
|
954 |
fun split_binop_tac n thm =
|
18
|
955 |
let
|
19
|
956 |
val concl = Thm.cprem_of thm n;
|
|
957 |
val (_, cconcl) = Thm.dest_comb concl;
|
49
|
958 |
val rewr = split_binop_conv cconcl;
|
|
959 |
in
|
|
960 |
rtac rewr n thm
|
|
961 |
end
|
|
962 |
handle CTERM _ => Seq.empty
|
|
963 |
*}
|
|
964 |
|
|
965 |
ML {*
|
|
966 |
fun split_arg_tac n thm =
|
|
967 |
let
|
|
968 |
val concl = Thm.cprem_of thm n;
|
|
969 |
val (_, cconcl) = Thm.dest_comb concl;
|
|
970 |
val rewr = split_arg_conv cconcl;
|
18
|
971 |
in
|
19
|
972 |
rtac rewr n thm
|
18
|
973 |
end
|
19
|
974 |
handle CTERM _ => Seq.empty
|
18
|
975 |
*}
|
19
|
976 |
|
20
|
977 |
(* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
|
|
978 |
|
32
|
979 |
lemma trueprop_cong:
|
|
980 |
shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
|
|
981 |
by auto
|
|
982 |
|
57
|
983 |
ML {*
|
|
984 |
Cong_Tac.cong_tac
|
|
985 |
*}
|
49
|
986 |
|
|
987 |
thm QUOT_TYPE_I_fset.R_trans2
|
19
|
988 |
ML {*
|
25
|
989 |
fun foo_tac' ctxt =
|
|
990 |
REPEAT_ALL_NEW (FIRST' [
|
49
|
991 |
(* rtac @{thm trueprop_cong},*)
|
47
|
992 |
rtac @{thm list_eq_refl},
|
19
|
993 |
rtac @{thm cons_preserves},
|
|
994 |
rtac @{thm mem_respects},
|
49
|
995 |
rtac @{thm card1_rsp},
|
25
|
996 |
rtac @{thm QUOT_TYPE_I_fset.R_trans2},
|
|
997 |
CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
|
57
|
998 |
Cong_Tac.cong_tac @{thm cong},
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
999 |
rtac @{thm ext}
|
51
32c0985563a8
Tested new build_goal and removed old one, eq_reflection is included in atomize, card_suc tests.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1000 |
(* rtac @{thm eq_reflection},*)
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1001 |
(* CHANGED o (ObjectLogic.full_atomize_tac)*)
|
25
|
1002 |
])
|
19
|
1003 |
*}
|
|
1004 |
|
20
|
1005 |
ML {*
|
49
|
1006 |
val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
|
55
|
1007 |
val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
|
20
|
1008 |
val cgoal = cterm_of @{theory} goal
|
21
|
1009 |
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
|
20
|
1010 |
*}
|
|
1011 |
|
30
e35198635d64
Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1012 |
(*notation ( output) "prop" ("#_" [1000] 1000) *)
|
e35198635d64
Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1013 |
notation ( output) "Trueprop" ("#_" [1000] 1000)
|
29
|
1014 |
|
70
f3cbda066c3a
consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1015 |
lemma atomize_eqv[atomize]:
|
f3cbda066c3a
consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1016 |
shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
|
49
|
1017 |
proof
|
70
f3cbda066c3a
consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1018 |
assume "A \<equiv> B"
|
f3cbda066c3a
consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1019 |
then show "Trueprop A \<equiv> Trueprop B" by unfold
|
49
|
1020 |
next
|
70
f3cbda066c3a
consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1021 |
assume *: "Trueprop A \<equiv> Trueprop B"
|
49
|
1022 |
have "A = B"
|
|
1023 |
proof (cases A)
|
|
1024 |
case True
|
70
f3cbda066c3a
consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1025 |
have "A" by fact
|
f3cbda066c3a
consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1026 |
then show "A = B" using * by simp
|
49
|
1027 |
next
|
|
1028 |
case False
|
70
f3cbda066c3a
consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1029 |
have "\<not>A" by fact
|
f3cbda066c3a
consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1030 |
then show "A = B" using * by auto
|
49
|
1031 |
qed
|
70
f3cbda066c3a
consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1032 |
then show "A \<equiv> B" by (rule eq_reflection)
|
49
|
1033 |
qed
|
|
1034 |
|
30
e35198635d64
Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1035 |
prove {* (Thm.term_of cgoal2) *}
|
21
|
1036 |
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1037 |
apply (atomize(full))
|
25
|
1038 |
apply (tactic {* foo_tac' @{context} 1 *})
|
30
e35198635d64
Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1039 |
done
|
18
|
1040 |
|
20
|
1041 |
thm length_append (* Not true but worth checking that the goal is correct *)
|
|
1042 |
ML {*
|
49
|
1043 |
val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append}))
|
55
|
1044 |
val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
|
20
|
1045 |
val cgoal = cterm_of @{theory} goal
|
21
|
1046 |
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
|
20
|
1047 |
*}
|
30
e35198635d64
Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1048 |
prove {* Thm.term_of cgoal2 *}
|
21
|
1049 |
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1050 |
apply (atomize(full))
|
30
e35198635d64
Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1051 |
apply (tactic {* foo_tac' @{context} 1 *})
|
25
|
1052 |
sorry
|
19
|
1053 |
|
20
|
1054 |
thm m2
|
|
1055 |
ML {*
|
49
|
1056 |
val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
|
55
|
1057 |
val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
|
20
|
1058 |
val cgoal = cterm_of @{theory} goal
|
21
|
1059 |
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
|
20
|
1060 |
*}
|
30
e35198635d64
Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1061 |
prove {* Thm.term_of cgoal2 *}
|
21
|
1062 |
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1063 |
apply (atomize(full))
|
30
e35198635d64
Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1064 |
apply (tactic {* foo_tac' @{context} 1 *})
|
e35198635d64
Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1065 |
done
|
21
|
1066 |
|
|
1067 |
thm list_eq.intros(4)
|
|
1068 |
ML {*
|
49
|
1069 |
val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))
|
55
|
1070 |
val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
|
21
|
1071 |
val cgoal = cterm_of @{theory} goal
|
|
1072 |
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
|
24
|
1073 |
val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2)
|
21
|
1074 |
*}
|
|
1075 |
|
24
|
1076 |
(* It is the same, but we need a name for it. *)
|
52
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1077 |
prove zzz : {* Thm.term_of cgoal3 *}
|
21
|
1078 |
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1079 |
apply (atomize(full))
|
25
|
1080 |
apply (tactic {* foo_tac' @{context} 1 *})
|
21
|
1081 |
done
|
|
1082 |
|
24
|
1083 |
lemma zzz' :
|
|
1084 |
"(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))"
|
|
1085 |
using list_eq.intros(4) by (simp only: zzz)
|
|
1086 |
|
|
1087 |
thm QUOT_TYPE_I_fset.REPS_same
|
25
|
1088 |
ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}
|
|
1089 |
|
46
|
1090 |
|
21
|
1091 |
thm list_eq.intros(5)
|
|
1092 |
ML {*
|
49
|
1093 |
val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
|
55
|
1094 |
val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
|
38
|
1095 |
*}
|
|
1096 |
ML {*
|
49
|
1097 |
val cgoal =
|
29
|
1098 |
Toplevel.program (fn () =>
|
|
1099 |
cterm_of @{theory} goal
|
|
1100 |
)
|
|
1101 |
*}
|
|
1102 |
ML {*
|
49
|
1103 |
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
|
21
|
1104 |
*}
|
30
e35198635d64
Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1105 |
prove {* Thm.term_of cgoal2 *}
|
21
|
1106 |
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1107 |
apply (atomize(full))
|
25
|
1108 |
apply (tactic {* foo_tac' @{context} 1 *})
|
21
|
1109 |
done
|
18
|
1110 |
|
29
|
1111 |
thm list.induct
|
|
1112 |
|
88
|
1113 |
ML {* val li = atomize_thm @{thm list.induct} *}
|
87
|
1114 |
|
|
1115 |
ML {* (* Doesn't recognize that 'a list = '?a list *)
|
|
1116 |
cterm_of @{theory} (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})
|
|
1117 |
*}
|
|
1118 |
|
|
1119 |
|
|
1120 |
|
29
|
1121 |
ML {*
|
50
18d8bcd769b3
Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1122 |
val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct}))
|
29
|
1123 |
*}
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1124 |
|
29
|
1125 |
ML {*
|
|
1126 |
val goal =
|
|
1127 |
Toplevel.program (fn () =>
|
55
|
1128 |
build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
|
29
|
1129 |
)
|
|
1130 |
*}
|
|
1131 |
ML {*
|
55
|
1132 |
val cgoal =
|
|
1133 |
Toplevel.program (fn () =>
|
|
1134 |
cterm_of @{theory} goal
|
|
1135 |
)
|
49
|
1136 |
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
|
35
|
1137 |
*}
|
50
18d8bcd769b3
Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1138 |
|
33
e8f1fa50329a
Found the source for the exception and added a handle for it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1139 |
prove {* (Thm.term_of cgoal2) *}
|
e8f1fa50329a
Found the source for the exception and added a handle for it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1140 |
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1141 |
apply (atomize(full))
|
49
|
1142 |
apply (tactic {* foo_tac' @{context} 1 *})
|
33
e8f1fa50329a
Found the source for the exception and added a handle for it.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1143 |
sorry
|
29
|
1144 |
|
49
|
1145 |
ML {*
|
|
1146 |
fun lift_theorem_fset_aux thm lthy =
|
|
1147 |
let
|
|
1148 |
val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;
|
55
|
1149 |
val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs;
|
49
|
1150 |
val cgoal = cterm_of @{theory} goal;
|
|
1151 |
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1152 |
val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (ObjectLogic.full_atomize_tac 1) THEN (foo_tac' @{context}) 1;
|
49
|
1153 |
val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac);
|
|
1154 |
val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm)))
|
|
1155 |
val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm;
|
|
1156 |
val [nthm3] = ProofContext.export lthy2 lthy [nthm2]
|
|
1157 |
in
|
|
1158 |
nthm3
|
|
1159 |
end
|
|
1160 |
*}
|
|
1161 |
|
|
1162 |
ML {* lift_theorem_fset_aux @{thm m1} @{context} *}
|
|
1163 |
|
|
1164 |
ML {*
|
|
1165 |
fun lift_theorem_fset name thm lthy =
|
|
1166 |
let
|
|
1167 |
val lifted_thm = lift_theorem_fset_aux thm lthy;
|
88
|
1168 |
val (_, lthy2) = note (name, lifted_thm) lthy;
|
49
|
1169 |
in
|
|
1170 |
lthy2
|
|
1171 |
end;
|
|
1172 |
*}
|
|
1173 |
|
|
1174 |
local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *}
|
|
1175 |
local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}
|
|
1176 |
local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
|
|
1177 |
local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1178 |
(*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} @{context}) *}
|
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1179 |
local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*)
|
49
|
1180 |
|
|
1181 |
thm m1_lift
|
|
1182 |
thm leqi4_lift
|
|
1183 |
thm leqi5_lift
|
|
1184 |
thm m2_lift
|
56
|
1185 |
(*thm card_suc*)
|
49
|
1186 |
|
|
1187 |
thm leqi4_lift
|
|
1188 |
ML {*
|
62
|
1189 |
val (nam, typ) = hd (Term.add_vars (prop_of @{thm leqi4_lift}) [])
|
49
|
1190 |
val (_, l) = dest_Type typ
|
|
1191 |
val t = Type ("QuotMain.fset", l)
|
|
1192 |
val v = Var (nam, t)
|
|
1193 |
val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v)
|
|
1194 |
*}
|
|
1195 |
|
|
1196 |
ML {*
|
|
1197 |
Toplevel.program (fn () =>
|
|
1198 |
MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
|
|
1199 |
Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift}
|
|
1200 |
)
|
|
1201 |
)
|
|
1202 |
*}
|
|
1203 |
|
56
|
1204 |
(*
|
52
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1205 |
thm card_suc
|
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1206 |
ML {*
|
62
|
1207 |
val (nam, typ) = hd (tl (Term.add_vars (prop_of @{thm card_suc})) [])
|
52
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1208 |
val (_, l) = dest_Type typ
|
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1209 |
val t = Type ("QuotMain.fset", l)
|
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1210 |
val v = Var (nam, t)
|
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1211 |
val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v)
|
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1212 |
*}
|
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1213 |
|
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1214 |
ML {*
|
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1215 |
Toplevel.program (fn () =>
|
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1216 |
MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
|
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1217 |
Drule.instantiate' [] [SOME (cv)] @{thm card_suc}
|
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1218 |
)
|
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1219 |
)
|
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1220 |
*}
|
56
|
1221 |
*)
|
52
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1222 |
|
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1223 |
|
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1224 |
|
6584b1ceedce
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1225 |
|
29
|
1226 |
thm card1_suc
|
|
1227 |
|
|
1228 |
ML {*
|
50
18d8bcd769b3
Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1229 |
val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm card1_suc}))
|
29
|
1230 |
*}
|
|
1231 |
ML {*
|
55
|
1232 |
val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
|
29
|
1233 |
*}
|
56
|
1234 |
ML {* term_of @{cpat "all"} *}
|
29
|
1235 |
ML {*
|
56
|
1236 |
val cgoal =
|
|
1237 |
Toplevel.program (fn () =>
|
|
1238 |
cterm_of @{theory} goal
|
|
1239 |
);
|
49
|
1240 |
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
|
29
|
1241 |
*}
|
73
|
1242 |
|
77
|
1243 |
lemma "(Ball (Respects ((op \<approx>) ===> (op =)))
|
72
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1244 |
(((REP_fset ---> id) ---> id)
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1245 |
(((ABS_fset ---> id) ---> id)
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1246 |
(\<lambda>P.
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1247 |
(ABS_fset ---> id) ((REP_fset ---> id) P)
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1248 |
(REP_fset (ABS_fset [])) \<and>
|
77
|
1249 |
Ball (Respects (op \<approx>))
|
72
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1250 |
((ABS_fset ---> id)
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1251 |
((REP_fset ---> id)
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1252 |
(\<lambda>t.
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1253 |
((ABS_fset ---> id)
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1254 |
((REP_fset ---> id) P)
|
73
|
1255 |
(REP_fset (ABS_fset t))) \<longrightarrow>
|
72
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1256 |
(!h.
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1257 |
(ABS_fset ---> id)
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1258 |
((REP_fset ---> id) P)
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1259 |
(REP_fset
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1260 |
(ABS_fset
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1261 |
(h #
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1262 |
REP_fset
|
73
|
1263 |
(ABS_fset t)))))))) \<longrightarrow>
|
77
|
1264 |
Ball (Respects (op \<approx>))
|
72
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1265 |
((ABS_fset ---> id)
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1266 |
((REP_fset ---> id)
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1267 |
(\<lambda>l.
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1268 |
(ABS_fset ---> id)
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1269 |
((REP_fset ---> id) P)
|
74
|
1270 |
(REP_fset (ABS_fset l)))))))))
|
|
1271 |
|
77
|
1272 |
= Ball (Respects ((op \<approx>) ===> (op =)))
|
|
1273 |
(\<lambda>P. ((P []) \<and> (Ball (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow>
|
|
1274 |
(Ball (Respects (op \<approx>)) (\<lambda>l. P l)))"
|
74
|
1275 |
term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))"
|
73
|
1276 |
thm LAMBDA_PRS1[symmetric]
|
|
1277 |
(*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*)
|
77
|
1278 |
apply (unfold Ball_def)
|
74
|
1279 |
apply (simp only: IN_RESPECTS)
|
|
1280 |
apply (simp only:list_eq_refl)
|
72
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1281 |
apply (unfold id_def)
|
74
|
1282 |
(*apply (simp only: FUN_MAP_I)*)
|
|
1283 |
apply (simp)
|
|
1284 |
apply (simp only: QUOT_TYPE_I_fset.thm10)
|
|
1285 |
apply (tactic {* foo_tac' @{context} 1 *})
|
|
1286 |
|
|
1287 |
..
|
73
|
1288 |
apply (simp add:IN_RESPECTS)
|
74
|
1289 |
|
73
|
1290 |
|
|
1291 |
|
|
1292 |
|
|
1293 |
apply (simp add: QUOT_TYPE_I_fset.R_trans2)
|
|
1294 |
|
|
1295 |
apply (rule ext)
|
|
1296 |
apply (simp add:QUOT_TYPE_I_fset.REP_ABS_rsp)
|
|
1297 |
apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *} )
|
|
1298 |
apply (simp add:cons_preserves)
|
|
1299 |
|
|
1300 |
|
72
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1301 |
|
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1302 |
(*prove aaa: {* (Thm.term_of cgoal2) *}
|
45
|
1303 |
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
|
58
f2565006dc5a
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1304 |
apply (atomize(full))
|
49
|
1305 |
apply (tactic {* foo_tac' @{context} 1 *})
|
72
4efc9e6661a4
Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
1306 |
done*)
|
29
|
1307 |
|
18
|
1308 |
(*
|
|
1309 |
datatype obj1 =
|
|
1310 |
OVAR1 "string"
|
|
1311 |
| OBJ1 "(string * (string \<Rightarrow> obj1)) list"
|
|
1312 |
| INVOKE1 "obj1 \<Rightarrow> string"
|
|
1313 |
| UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"
|
|
1314 |
*)
|
53
|
1315 |
|
57
|
1316 |
end
|