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