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