0
|
1 |
theory QuotMain
|
6
|
2 |
imports QuotScript QuotList Prove
|
0
|
3 |
begin
|
|
4 |
|
|
5 |
locale QUOT_TYPE =
|
|
6 |
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
|
|
7 |
and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
|
|
8 |
and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
|
|
9 |
assumes equiv: "EQUIV R"
|
|
10 |
and rep_prop: "\<And>y. \<exists>x. Rep y = R x"
|
|
11 |
and rep_inverse: "\<And>x. Abs (Rep x) = x"
|
|
12 |
and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
|
|
13 |
and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
|
15
|
14 |
begin
|
0
|
15 |
|
|
16 |
definition
|
|
17 |
"ABS x \<equiv> Abs (R x)"
|
|
18 |
|
|
19 |
definition
|
|
20 |
"REP a = Eps (Rep a)"
|
|
21 |
|
15
|
22 |
lemma lem9:
|
0
|
23 |
shows "R (Eps (R x)) = R x"
|
|
24 |
proof -
|
|
25 |
have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
|
|
26 |
then have "R x (Eps (R x))" by (rule someI)
|
15
|
27 |
then show "R (Eps (R x)) = R x"
|
0
|
28 |
using equiv unfolding EQUIV_def by simp
|
|
29 |
qed
|
|
30 |
|
|
31 |
theorem thm10:
|
|
32 |
shows "ABS (REP a) = a"
|
|
33 |
unfolding ABS_def REP_def
|
|
34 |
proof -
|
15
|
35 |
from rep_prop
|
0
|
36 |
obtain x where eq: "Rep a = R x" by auto
|
|
37 |
have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
|
|
38 |
also have "\<dots> = Abs (R x)" using lem9 by simp
|
|
39 |
also have "\<dots> = Abs (Rep a)" using eq by simp
|
|
40 |
also have "\<dots> = a" using rep_inverse by simp
|
|
41 |
finally
|
|
42 |
show "Abs (R (Eps (Rep a))) = a" by simp
|
|
43 |
qed
|
|
44 |
|
15
|
45 |
lemma REP_refl:
|
0
|
46 |
shows "R (REP a) (REP a)"
|
|
47 |
unfolding REP_def
|
|
48 |
by (simp add: equiv[simplified EQUIV_def])
|
|
49 |
|
|
50 |
lemma lem7:
|
|
51 |
"(R x = R y) = (Abs (R x) = Abs (R y))"
|
|
52 |
apply(rule iffI)
|
|
53 |
apply(simp)
|
|
54 |
apply(drule rep_inject[THEN iffD2])
|
|
55 |
apply(simp add: abs_inverse)
|
|
56 |
done
|
15
|
57 |
|
0
|
58 |
theorem thm11:
|
|
59 |
shows "R r r' = (ABS r = ABS r')"
|
|
60 |
unfolding ABS_def
|
|
61 |
by (simp only: equiv[simplified EQUIV_def] lem7)
|
|
62 |
|
4
|
63 |
|
2
|
64 |
lemma REP_ABS_rsp:
|
4
|
65 |
shows "R f (REP (ABS g)) = R f g"
|
|
66 |
and "R (REP (ABS g)) f = R g f"
|
|
67 |
apply(subst thm11)
|
|
68 |
apply(simp add: thm10 thm11)
|
|
69 |
apply(subst thm11)
|
|
70 |
apply(simp add: thm10 thm11)
|
|
71 |
done
|
|
72 |
|
0
|
73 |
lemma QUOTIENT:
|
|
74 |
"QUOTIENT R ABS REP"
|
|
75 |
apply(unfold QUOTIENT_def)
|
|
76 |
apply(simp add: thm10)
|
|
77 |
apply(simp add: REP_refl)
|
|
78 |
apply(subst thm11[symmetric])
|
|
79 |
apply(simp add: equiv[simplified EQUIV_def])
|
|
80 |
done
|
|
81 |
|
21
|
82 |
lemma R_trans:
|
|
83 |
assumes ab: "R a b" and bc: "R b c" shows "R a c"
|
|
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
|
|
88 |
ultimately show ?thesis unfolding TRANS_def by blast
|
|
89 |
qed
|
|
90 |
|
|
91 |
lemma R_sym:
|
|
92 |
assumes ab: "R a b" shows "R b a"
|
|
93 |
proof -
|
|
94 |
have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
|
|
95 |
then show ?thesis using ab unfolding SYM_def by blast
|
|
96 |
qed
|
|
97 |
|
|
98 |
lemma R_trans2:
|
|
99 |
assumes ac: "R a c" and bd: "R b d"
|
|
100 |
shows "R a b = R c d"
|
|
101 |
proof
|
|
102 |
assume ab: "R a b"
|
|
103 |
then have "R b a" using R_sym by blast
|
|
104 |
then have "R b c" using ac R_trans by blast
|
|
105 |
then have "R c b" using R_sym by blast
|
|
106 |
then show "R c d" using bd R_trans by blast
|
|
107 |
next
|
|
108 |
assume ccd: "R c d"
|
|
109 |
then have "R a d" using ac R_trans by blast
|
|
110 |
then have "R d a" using R_sym by blast
|
|
111 |
then have "R b a" using bd R_trans by blast
|
|
112 |
then show "R a b" using R_sym by blast
|
|
113 |
qed
|
|
114 |
|
|
115 |
lemma REPS_same:
|
|
116 |
shows "R (REP a) (REP b) = (a = b)"
|
|
117 |
proof
|
|
118 |
assume as: "R (REP a) (REP b)"
|
|
119 |
from rep_prop
|
|
120 |
obtain x where eq: "Rep a = R x" by auto
|
|
121 |
also
|
|
122 |
from rep_prop
|
|
123 |
obtain y where eq2: "Rep b = R y" by auto
|
|
124 |
then have "R (Eps (R x)) (Eps (R y))" using as eq unfolding REP_def by simp
|
|
125 |
then have "R x (Eps (R y))" using lem9 by simp
|
|
126 |
then have "R (Eps (R y)) x" using R_sym by blast
|
|
127 |
then have "R y x" using lem9 by simp
|
|
128 |
then have "R x y" using R_sym by blast
|
|
129 |
then have "ABS x = ABS y" using thm11 by simp
|
|
130 |
then have "Abs (Rep a) = Abs (Rep b)" using eq eq2 unfolding ABS_def by simp
|
|
131 |
then show "a = b" using rep_inverse by simp
|
|
132 |
next
|
|
133 |
assume ab: "a = b"
|
|
134 |
have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
|
|
135 |
then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto
|
|
136 |
qed
|
|
137 |
|
0
|
138 |
end
|
|
139 |
|
|
140 |
section {* type definition for the quotient type *}
|
|
141 |
|
|
142 |
ML {*
|
1
|
143 |
(* constructs the term \<lambda>(c::ty \<Rightarrow> bool). \<exists>x. c = rel x *)
|
0
|
144 |
fun typedef_term rel ty lthy =
|
15
|
145 |
let
|
|
146 |
val [x, c] = [("x", ty), ("c", ty --> @{typ bool})]
|
0
|
147 |
|> Variable.variant_frees lthy [rel]
|
|
148 |
|> map Free
|
|
149 |
in
|
15
|
150 |
lambda c
|
|
151 |
(HOLogic.mk_exists
|
1
|
152 |
("x", ty, HOLogic.mk_eq (c, (rel $ x))))
|
0
|
153 |
end
|
|
154 |
*}
|
|
155 |
|
14
|
156 |
(*
|
0
|
157 |
ML {*
|
14
|
158 |
typedef_term @{term R} @{typ "nat"} @{context}
|
2
|
159 |
|> Syntax.string_of_term @{context}
|
|
160 |
|> writeln
|
14
|
161 |
*}*)
|
2
|
162 |
|
|
163 |
ML {*
|
15
|
164 |
val typedef_tac =
|
0
|
165 |
EVERY1 [rewrite_goal_tac @{thms mem_def},
|
|
166 |
rtac @{thm exI}, rtac @{thm exI}, rtac @{thm refl}]
|
|
167 |
*}
|
|
168 |
|
|
169 |
ML {*
|
|
170 |
(* makes the new type definitions *)
|
|
171 |
fun typedef_make (qty_name, rel, ty) lthy =
|
|
172 |
LocalTheory.theory_result
|
15
|
173 |
(Typedef.add_typedef false NONE
|
0
|
174 |
(qty_name, map fst (Term.add_tfreesT ty []), NoSyn)
|
|
175 |
(typedef_term rel ty lthy)
|
|
176 |
NONE typedef_tac) lthy
|
|
177 |
*}
|
|
178 |
|
2
|
179 |
text {* proves the QUOT_TYPE theorem for the new type *}
|
0
|
180 |
ML {*
|
15
|
181 |
fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
|
0
|
182 |
let
|
|
183 |
val rep_thm = #Rep typedef_info
|
|
184 |
val rep_inv = #Rep_inverse typedef_info
|
|
185 |
val abs_inv = #Abs_inverse typedef_info
|
|
186 |
val rep_inj = #Rep_inject typedef_info
|
|
187 |
|
|
188 |
val ss = HOL_basic_ss addsimps @{thms mem_def}
|
|
189 |
val rep_thm_simpd = Simplifier.asm_full_simplify ss rep_thm
|
|
190 |
val abs_inv_simpd = Simplifier.asm_full_simplify ss abs_inv
|
|
191 |
in
|
|
192 |
EVERY1 [rtac @{thm QUOT_TYPE.intro},
|
15
|
193 |
rtac equiv_thm,
|
|
194 |
rtac rep_thm_simpd,
|
|
195 |
rtac rep_inv,
|
0
|
196 |
rtac abs_inv_simpd, rtac @{thm exI}, rtac @{thm refl},
|
|
197 |
rtac rep_inj]
|
|
198 |
end
|
|
199 |
*}
|
|
200 |
|
2
|
201 |
term QUOT_TYPE
|
|
202 |
ML {* HOLogic.mk_Trueprop *}
|
|
203 |
ML {* Goal.prove *}
|
|
204 |
ML {* Syntax.check_term *}
|
|
205 |
|
15
|
206 |
ML {*
|
0
|
207 |
fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
|
|
208 |
let
|
|
209 |
val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT)
|
|
210 |
val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
|
|
211 |
|> Syntax.check_term lthy
|
|
212 |
in
|
|
213 |
Goal.prove lthy [] [] goal
|
|
214 |
(fn _ => typedef_quot_type_tac equiv_thm typedef_info)
|
|
215 |
end
|
|
216 |
*}
|
|
217 |
|
|
218 |
ML {*
|
|
219 |
fun typedef_quotient_thm_tac defs quot_type_thm =
|
15
|
220 |
EVERY1 [K (rewrite_goals_tac defs),
|
|
221 |
rtac @{thm QUOT_TYPE.QUOTIENT},
|
0
|
222 |
rtac quot_type_thm]
|
|
223 |
*}
|
|
224 |
|
15
|
225 |
ML {*
|
0
|
226 |
fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy =
|
|
227 |
let
|
|
228 |
val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT)
|
|
229 |
val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep)
|
|
230 |
|> Syntax.check_term lthy
|
|
231 |
in
|
|
232 |
Goal.prove lthy [] [] goal
|
|
233 |
(fn _ => typedef_quotient_thm_tac [abs_def, rep_def] quot_type_thm)
|
|
234 |
end
|
|
235 |
*}
|
|
236 |
|
|
237 |
text {* two wrappers for define and note *}
|
15
|
238 |
ML {*
|
17
|
239 |
fun make_def (name, mx, rhs) lthy =
|
15
|
240 |
let
|
17
|
241 |
val ((rhs, (_ , thm)), lthy') =
|
|
242 |
LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy
|
0
|
243 |
in
|
17
|
244 |
((rhs, thm), lthy')
|
0
|
245 |
end
|
|
246 |
*}
|
|
247 |
|
|
248 |
ML {*
|
15
|
249 |
fun reg_thm (name, thm) lthy =
|
0
|
250 |
let
|
15
|
251 |
val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy
|
0
|
252 |
in
|
16
|
253 |
(thm', lthy')
|
0
|
254 |
end
|
|
255 |
*}
|
|
256 |
|
14
|
257 |
ML {*
|
|
258 |
val no_vars = Thm.rule_attribute (fn context => fn th =>
|
|
259 |
let
|
|
260 |
val ctxt = Variable.set_body false (Context.proof_of context);
|
|
261 |
val ((_, [th']), _) = Variable.import true [th] ctxt;
|
|
262 |
in th' end);
|
|
263 |
*}
|
|
264 |
|
|
265 |
ML {*
|
0
|
266 |
fun typedef_main (qty_name, rel, ty, equiv_thm) lthy =
|
15
|
267 |
let
|
0
|
268 |
(* generates typedef *)
|
16
|
269 |
val ((_, typedef_info), lthy') = typedef_make (qty_name, rel, ty) lthy
|
0
|
270 |
|
|
271 |
(* abs and rep functions *)
|
|
272 |
val abs_ty = #abs_type typedef_info
|
|
273 |
val rep_ty = #rep_type typedef_info
|
|
274 |
val abs_name = #Abs_name typedef_info
|
|
275 |
val rep_name = #Rep_name typedef_info
|
|
276 |
val abs = Const (abs_name, rep_ty --> abs_ty)
|
|
277 |
val rep = Const (rep_name, abs_ty --> rep_ty)
|
|
278 |
|
|
279 |
(* ABS and REP definitions *)
|
|
280 |
val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT )
|
|
281 |
val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT )
|
15
|
282 |
val ABS_trm = Syntax.check_term lthy' (ABS_const $ rel $ abs)
|
|
283 |
val REP_trm = Syntax.check_term lthy' (REP_const $ rep)
|
0
|
284 |
val ABS_name = Binding.prefix_name "ABS_" qty_name
|
15
|
285 |
val REP_name = Binding.prefix_name "REP_" qty_name
|
|
286 |
val (((ABS, ABS_def), (REP, REP_def)), lthy'') =
|
0
|
287 |
lthy' |> make_def (ABS_name, NoSyn, ABS_trm)
|
|
288 |
||>> make_def (REP_name, NoSyn, REP_trm)
|
|
289 |
|
|
290 |
(* quot_type theorem *)
|
|
291 |
val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy''
|
|
292 |
val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name
|
|
293 |
|
|
294 |
(* quotient theorem *)
|
|
295 |
val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy''
|
|
296 |
val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
|
|
297 |
|
14
|
298 |
(* interpretation *)
|
|
299 |
val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
|
|
300 |
val ((_, [eqn1pre]), lthy''') = Variable.import true [ABS_def] lthy'';
|
|
301 |
val eqn1i = Thm.prop_of (symmetric eqn1pre)
|
|
302 |
val ((_, [eqn2pre]), lthy'''') = Variable.import true [REP_def] lthy''';
|
|
303 |
val eqn2i = Thm.prop_of (symmetric eqn2pre)
|
|
304 |
|
|
305 |
val exp_morphism = ProofContext.export_morphism lthy'''' (ProofContext.init (ProofContext.theory_of lthy''''));
|
|
306 |
val exp_term = Morphism.term exp_morphism;
|
|
307 |
val exp = Morphism.thm exp_morphism;
|
|
308 |
|
|
309 |
val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN
|
16
|
310 |
ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))])))
|
14
|
311 |
val mthdt = Method.Basic (fn _ => mthd)
|
|
312 |
val bymt = Proof.global_terminal_proof (mthdt, NONE)
|
16
|
313 |
val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
|
14
|
314 |
Expression.Named [
|
|
315 |
("R", rel),
|
|
316 |
("Abs", abs),
|
|
317 |
("Rep", rep)
|
|
318 |
]))]
|
0
|
319 |
in
|
14
|
320 |
lthy''''
|
|
321 |
|> reg_thm (quot_thm_name, quot_thm)
|
0
|
322 |
||>> reg_thm (quotient_thm_name, quotient_thm)
|
14
|
323 |
||> LocalTheory.theory (fn thy =>
|
|
324 |
let
|
|
325 |
val global_eqns = map exp_term [eqn2i, eqn1i];
|
16
|
326 |
(* Not sure if the following context should not be used *)
|
14
|
327 |
val (global_eqns2, lthy''''') = Variable.import_terms true global_eqns lthy'''';
|
|
328 |
val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;
|
|
329 |
in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
|
0
|
330 |
end
|
|
331 |
*}
|
|
332 |
|
|
333 |
section {* various tests for quotient types*}
|
|
334 |
datatype trm =
|
15
|
335 |
var "nat"
|
0
|
336 |
| app "trm" "trm"
|
|
337 |
| lam "nat" "trm"
|
13
|
338 |
|
14
|
339 |
axiomatization RR :: "trm \<Rightarrow> trm \<Rightarrow> bool" where
|
|
340 |
r_eq: "EQUIV RR"
|
0
|
341 |
|
2
|
342 |
ML {*
|
15
|
343 |
typedef_main
|
2
|
344 |
*}
|
|
345 |
|
0
|
346 |
local_setup {*
|
16
|
347 |
typedef_main (@{binding "qtrm"}, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd
|
0
|
348 |
*}
|
|
349 |
|
|
350 |
term Rep_qtrm
|
2
|
351 |
term REP_qtrm
|
0
|
352 |
term Abs_qtrm
|
|
353 |
term ABS_qtrm
|
|
354 |
thm QUOT_TYPE_qtrm
|
|
355 |
thm QUOTIENT_qtrm
|
2
|
356 |
|
16
|
357 |
(* Test interpretation *)
|
|
358 |
thm QUOT_TYPE_I_qtrm.thm11
|
|
359 |
|
21
|
360 |
print_theorems
|
|
361 |
|
0
|
362 |
thm Rep_qtrm
|
|
363 |
|
|
364 |
text {* another test *}
|
13
|
365 |
datatype 'a my = Foo
|
0
|
366 |
consts Rmy :: "'a my \<Rightarrow> 'a my \<Rightarrow> bool"
|
|
367 |
axioms rmy_eq: "EQUIV Rmy"
|
|
368 |
|
|
369 |
term "\<lambda>(c::'a my\<Rightarrow>bool). \<exists>x. c = Rmy x"
|
|
370 |
|
|
371 |
datatype 'a trm' =
|
15
|
372 |
var' "'a"
|
0
|
373 |
| app' "'a trm'" "'a trm'"
|
|
374 |
| lam' "'a" "'a trm'"
|
15
|
375 |
|
0
|
376 |
consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"
|
|
377 |
axioms r_eq': "EQUIV R'"
|
|
378 |
|
14
|
379 |
|
0
|
380 |
local_setup {*
|
16
|
381 |
typedef_main (@{binding "qtrm'"}, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd
|
0
|
382 |
*}
|
|
383 |
|
14
|
384 |
print_theorems
|
|
385 |
|
0
|
386 |
term ABS_qtrm'
|
|
387 |
term REP_qtrm'
|
|
388 |
thm QUOT_TYPE_qtrm'
|
|
389 |
thm QUOTIENT_qtrm'
|
|
390 |
thm Rep_qtrm'
|
|
391 |
|
14
|
392 |
|
0
|
393 |
text {* a test with lists of terms *}
|
|
394 |
datatype t =
|
|
395 |
vr "string"
|
|
396 |
| ap "t list"
|
|
397 |
| lm "string" "t"
|
|
398 |
|
|
399 |
consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
|
|
400 |
axioms t_eq: "EQUIV Rt"
|
|
401 |
|
|
402 |
local_setup {*
|
|
403 |
typedef_main (@{binding "qt"}, @{term "Rt"}, @{typ "t"}, @{thm t_eq}) #> snd
|
|
404 |
*}
|
|
405 |
|
|
406 |
section {* lifting of constants *}
|
|
407 |
|
|
408 |
text {* information about map-functions for type-constructor *}
|
|
409 |
ML {*
|
|
410 |
type typ_info = {mapfun: string}
|
|
411 |
|
|
412 |
local
|
|
413 |
structure Data = GenericDataFun
|
|
414 |
(type T = typ_info Symtab.table
|
|
415 |
val empty = Symtab.empty
|
|
416 |
val extend = I
|
|
417 |
fun merge _ = Symtab.merge (K true))
|
|
418 |
in
|
|
419 |
val lookup = Symtab.lookup o Data.get
|
15
|
420 |
fun update k v = Data.map (Symtab.update (k, v))
|
0
|
421 |
end
|
|
422 |
*}
|
|
423 |
|
|
424 |
(* mapfuns for some standard types *)
|
|
425 |
setup {*
|
|
426 |
Context.theory_map (update @{type_name "list"} {mapfun = @{const_name "map"}})
|
|
427 |
#> Context.theory_map (update @{type_name "*"} {mapfun = @{const_name "prod_fun"}})
|
|
428 |
#> Context.theory_map (update @{type_name "fun"} {mapfun = @{const_name "fun_map"}})
|
|
429 |
*}
|
|
430 |
|
2
|
431 |
|
0
|
432 |
ML {* lookup (Context.Proof @{context}) @{type_name list} *}
|
|
433 |
|
|
434 |
ML {*
|
|
435 |
datatype abs_or_rep = abs | rep
|
|
436 |
|
15
|
437 |
fun get_fun abs_or_rep rty qty lthy ty =
|
0
|
438 |
let
|
|
439 |
val qty_name = Long_Name.base_name (fst (dest_Type qty))
|
15
|
440 |
|
0
|
441 |
fun get_fun_aux s fs_tys =
|
|
442 |
let
|
|
443 |
val (fs, tys) = split_list fs_tys
|
15
|
444 |
val (otys, ntys) = split_list tys
|
0
|
445 |
val oty = Type (s, otys)
|
|
446 |
val nty = Type (s, ntys)
|
|
447 |
val ftys = map (op -->) tys
|
|
448 |
in
|
15
|
449 |
(case (lookup (Context.Proof lthy) s) of
|
0
|
450 |
SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty))
|
|
451 |
| NONE => raise ERROR ("no map association for type " ^ s))
|
|
452 |
end
|
|
453 |
|
|
454 |
fun get_const abs = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty))
|
|
455 |
| get_const rep = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty))
|
|
456 |
in
|
|
457 |
if ty = qty
|
|
458 |
then (get_const abs_or_rep)
|
|
459 |
else (case ty of
|
|
460 |
TFree _ => (Abs ("x", ty, Bound 0), (ty, ty))
|
|
461 |
| Type (_, []) => (Abs ("x", ty, Bound 0), (ty, ty))
|
15
|
462 |
| Type (s, tys) => get_fun_aux s (map (get_fun abs_or_rep rty qty lthy) tys)
|
0
|
463 |
| _ => raise ERROR ("no variables")
|
|
464 |
)
|
|
465 |
end
|
|
466 |
*}
|
|
467 |
|
|
468 |
ML {*
|
2
|
469 |
get_fun rep @{typ t} @{typ qt} @{context} @{typ "t * nat"}
|
|
470 |
|> fst
|
|
471 |
|> Syntax.string_of_term @{context}
|
|
472 |
|> writeln
|
|
473 |
*}
|
|
474 |
|
|
475 |
|
|
476 |
ML {*
|
0
|
477 |
fun get_const_def nconst oconst rty qty lthy =
|
|
478 |
let
|
|
479 |
val ty = fastype_of nconst
|
|
480 |
val (arg_tys, res_ty) = strip_type ty
|
14
|
481 |
|
0
|
482 |
val fresh_args = arg_tys |> map (pair "x")
|
15
|
483 |
|> Variable.variant_frees lthy [nconst, oconst]
|
0
|
484 |
|> map Free
|
|
485 |
|
|
486 |
val rep_fns = map (fst o get_fun rep rty qty lthy) arg_tys
|
|
487 |
val abs_fn = (fst o get_fun abs rty qty lthy) res_ty
|
|
488 |
|
|
489 |
in
|
|
490 |
map (op $) (rep_fns ~~ fresh_args)
|
|
491 |
|> curry list_comb oconst
|
|
492 |
|> curry (op $) abs_fn
|
|
493 |
|> fold_rev lambda fresh_args
|
|
494 |
end
|
|
495 |
*}
|
|
496 |
|
|
497 |
ML {*
|
15
|
498 |
fun exchange_ty rty qty ty =
|
0
|
499 |
if ty = rty then qty
|
15
|
500 |
else
|
0
|
501 |
(case ty of
|
|
502 |
Type (s, tys) => Type (s, map (exchange_ty rty qty) tys)
|
|
503 |
| _ => ty)
|
|
504 |
*}
|
|
505 |
|
|
506 |
ML {*
|
17
|
507 |
fun make_const_def nconst_bname oconst mx rty qty lthy =
|
0
|
508 |
let
|
|
509 |
val oconst_ty = fastype_of oconst
|
|
510 |
val nconst_ty = exchange_ty rty qty oconst_ty
|
17
|
511 |
val nconst = Const (Binding.name_of nconst_bname, nconst_ty)
|
0
|
512 |
val def_trm = get_const_def nconst oconst rty qty lthy
|
|
513 |
in
|
17
|
514 |
make_def (nconst_bname, mx, def_trm) lthy
|
15
|
515 |
end
|
0
|
516 |
*}
|
|
517 |
|
2
|
518 |
local_setup {*
|
17
|
519 |
make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd
|
2
|
520 |
*}
|
|
521 |
|
|
522 |
local_setup {*
|
17
|
523 |
make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd
|
2
|
524 |
*}
|
|
525 |
|
|
526 |
local_setup {*
|
17
|
527 |
make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd
|
2
|
528 |
*}
|
|
529 |
|
|
530 |
thm VR_def
|
|
531 |
thm AP_def
|
|
532 |
thm LM_def
|
14
|
533 |
term LM
|
2
|
534 |
term VR
|
|
535 |
term AP
|
|
536 |
|
|
537 |
|
0
|
538 |
text {* a test with functions *}
|
|
539 |
datatype 'a t' =
|
|
540 |
vr' "string"
|
|
541 |
| ap' "('a t') * ('a t')"
|
|
542 |
| lm' "'a" "string \<Rightarrow> ('a t')"
|
|
543 |
|
|
544 |
consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
|
|
545 |
axioms t_eq': "EQUIV Rt'"
|
|
546 |
|
14
|
547 |
|
0
|
548 |
local_setup {*
|
|
549 |
typedef_main (@{binding "qt'"}, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd
|
|
550 |
*}
|
|
551 |
|
14
|
552 |
print_theorems
|
2
|
553 |
|
0
|
554 |
local_setup {*
|
17
|
555 |
make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
|
0
|
556 |
*}
|
|
557 |
|
|
558 |
local_setup {*
|
17
|
559 |
make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
|
0
|
560 |
*}
|
|
561 |
|
|
562 |
local_setup {*
|
17
|
563 |
make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
|
0
|
564 |
*}
|
|
565 |
|
|
566 |
thm VR'_def
|
|
567 |
thm AP'_def
|
|
568 |
thm LM'_def
|
14
|
569 |
term LM'
|
0
|
570 |
term VR'
|
|
571 |
term AP'
|
|
572 |
|
14
|
573 |
|
0
|
574 |
text {* finite set example *}
|
13
|
575 |
print_syntax
|
14
|
576 |
inductive
|
13
|
577 |
list_eq (infix "\<approx>" 50)
|
0
|
578 |
where
|
|
579 |
"a#b#xs \<approx> b#a#xs"
|
|
580 |
| "[] \<approx> []"
|
|
581 |
| "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"
|
|
582 |
| "a#a#xs \<approx> a#xs"
|
|
583 |
| "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"
|
|
584 |
| "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"
|
|
585 |
|
|
586 |
lemma list_eq_sym:
|
|
587 |
shows "xs \<approx> xs"
|
13
|
588 |
apply (induct xs)
|
|
589 |
apply (auto intro: list_eq.intros)
|
|
590 |
done
|
0
|
591 |
|
|
592 |
lemma equiv_list_eq:
|
|
593 |
shows "EQUIV list_eq"
|
13
|
594 |
unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def
|
|
595 |
apply(auto intro: list_eq.intros list_eq_sym)
|
|
596 |
done
|
0
|
597 |
|
|
598 |
local_setup {*
|
|
599 |
typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd
|
|
600 |
*}
|
|
601 |
|
14
|
602 |
print_theorems
|
|
603 |
|
0
|
604 |
typ "'a fset"
|
|
605 |
thm "Rep_fset"
|
|
606 |
|
|
607 |
local_setup {*
|
17
|
608 |
make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
|
0
|
609 |
*}
|
|
610 |
|
14
|
611 |
term Nil
|
0
|
612 |
term EMPTY
|
2
|
613 |
thm EMPTY_def
|
|
614 |
|
0
|
615 |
|
|
616 |
local_setup {*
|
17
|
617 |
make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
|
0
|
618 |
*}
|
|
619 |
|
14
|
620 |
term Cons
|
0
|
621 |
term INSERT
|
2
|
622 |
thm INSERT_def
|
0
|
623 |
|
|
624 |
local_setup {*
|
17
|
625 |
make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
|
0
|
626 |
*}
|
|
627 |
|
15
|
628 |
term append
|
0
|
629 |
term UNION
|
2
|
630 |
thm UNION_def
|
|
631 |
|
18
|
632 |
(* Maybe the infrastructure should not allow this kind of definition, without showing that
|
|
633 |
the relation respects lenght... *)
|
7
|
634 |
local_setup {*
|
17
|
635 |
make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
|
7
|
636 |
*}
|
|
637 |
|
|
638 |
term length
|
|
639 |
term CARD
|
|
640 |
thm CARD_def
|
|
641 |
|
0
|
642 |
thm QUOTIENT_fset
|
|
643 |
|
14
|
644 |
thm QUOT_TYPE_I_fset.thm11
|
9
|
645 |
|
|
646 |
|
13
|
647 |
fun
|
|
648 |
membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100)
|
0
|
649 |
where
|
|
650 |
m1: "(x memb []) = False"
|
|
651 |
| m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"
|
|
652 |
|
2
|
653 |
lemma mem_respects:
|
9
|
654 |
fixes z
|
2
|
655 |
assumes a: "list_eq x y"
|
9
|
656 |
shows "(z memb x) = (z memb y)"
|
13
|
657 |
using a by induct auto
|
|
658 |
|
2
|
659 |
|
12
|
660 |
lemma cons_preserves:
|
|
661 |
fixes z
|
|
662 |
assumes a: "xs \<approx> ys"
|
|
663 |
shows "(z # xs) \<approx> (z # ys)"
|
13
|
664 |
using a by (rule QuotMain.list_eq.intros(5))
|
12
|
665 |
|
11
|
666 |
ML {*
|
|
667 |
fun unlam_def orig_ctxt ctxt t =
|
13
|
668 |
let val rhs = Thm.rhs_of t in
|
|
669 |
(case try (Thm.dest_abs NONE) rhs of
|
|
670 |
SOME (v, vt) =>
|
|
671 |
let
|
|
672 |
val (vname, vt) = Term.dest_Free (Thm.term_of v)
|
|
673 |
val ([vnname], ctxt) = Variable.variant_fixes [vname] ctxt
|
|
674 |
val nv = Free(vnname, vt)
|
|
675 |
val t2 = Drule.fun_cong_rule t (Thm.cterm_of (ProofContext.theory_of ctxt) nv)
|
|
676 |
val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2
|
|
677 |
in unlam_def orig_ctxt ctxt tnorm end
|
|
678 |
| NONE => singleton (ProofContext.export ctxt orig_ctxt) t)
|
|
679 |
end
|
10
|
680 |
*}
|
9
|
681 |
|
10
|
682 |
local_setup {*
|
17
|
683 |
make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
|
10
|
684 |
*}
|
|
685 |
|
0
|
686 |
term membship
|
|
687 |
term IN
|
2
|
688 |
thm IN_def
|
18
|
689 |
ML {* unlam_def @{context} @{context} @{thm IN_def} *}
|
0
|
690 |
|
2
|
691 |
lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset]
|
|
692 |
thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a]
|
0
|
693 |
|
2
|
694 |
lemma yy:
|
|
695 |
shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"
|
|
696 |
unfolding IN_def EMPTY_def
|
|
697 |
apply(rule_tac f="(op =) False" in arg_cong)
|
|
698 |
apply(rule mem_respects)
|
14
|
699 |
apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
|
2
|
700 |
apply(rule list_eq.intros)
|
0
|
701 |
done
|
|
702 |
|
2
|
703 |
lemma
|
|
704 |
shows "IN (x::nat) EMPTY = False"
|
|
705 |
using m1
|
|
706 |
apply -
|
|
707 |
apply(rule yy[THEN iffD1, symmetric])
|
|
708 |
apply(simp)
|
0
|
709 |
done
|
|
710 |
|
2
|
711 |
lemma
|
|
712 |
shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) =
|
|
713 |
((x = y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))"
|
|
714 |
unfolding IN_def INSERT_def
|
|
715 |
apply(rule_tac f="(op \<or>) (x=y)" in arg_cong)
|
|
716 |
apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong)
|
|
717 |
apply(rule mem_respects)
|
|
718 |
apply(rule list_eq.intros(3))
|
|
719 |
apply(unfold REP_fset_def ABS_fset_def)
|
5
|
720 |
apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
|
2
|
721 |
apply(rule list_eq_sym)
|
|
722 |
done
|
0
|
723 |
|
7
|
724 |
lemma append_respects_fst:
|
14
|
725 |
assumes a : "list_eq l1 l2"
|
4
|
726 |
shows "list_eq (l1 @ s) (l2 @ s)"
|
3
|
727 |
using a
|
|
728 |
apply(induct)
|
4
|
729 |
apply(auto intro: list_eq.intros)
|
|
730 |
apply(simp add: list_eq_sym)
|
3
|
731 |
done
|
|
732 |
|
18
|
733 |
lemma yyy:
|
3
|
734 |
shows "
|
|
735 |
(
|
|
736 |
(UNION EMPTY s = s) &
|
|
737 |
((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))
|
|
738 |
) = (
|
|
739 |
((ABS_fset ([] @ REP_fset s)) = s) &
|
|
740 |
((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2)))
|
|
741 |
)"
|
|
742 |
unfolding UNION_def EMPTY_def INSERT_def
|
|
743 |
apply(rule_tac f="(op &)" in arg_cong2)
|
|
744 |
apply(rule_tac f="(op =)" in arg_cong2)
|
14
|
745 |
apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
|
7
|
746 |
apply(rule append_respects_fst)
|
18
|
747 |
apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
|
3
|
748 |
apply(rule list_eq_sym)
|
|
749 |
apply(simp)
|
|
750 |
apply(rule_tac f="(op =)" in arg_cong2)
|
14
|
751 |
apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
|
7
|
752 |
apply(rule append_respects_fst)
|
14
|
753 |
apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
|
3
|
754 |
apply(rule list_eq_sym)
|
14
|
755 |
apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
|
3
|
756 |
apply(rule list_eq.intros(5))
|
14
|
757 |
apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
|
3
|
758 |
apply(rule list_eq_sym)
|
|
759 |
done
|
|
760 |
|
|
761 |
lemma
|
|
762 |
shows "
|
|
763 |
(UNION EMPTY s = s) &
|
7
|
764 |
((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))"
|
|
765 |
apply (simp add: yyy)
|
14
|
766 |
apply (rule QUOT_TYPE_I_fset.thm10)
|
7
|
767 |
done
|
3
|
768 |
|
8
|
769 |
ML {*
|
|
770 |
fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x)
|
12
|
771 |
val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}]
|
8
|
772 |
*}
|
|
773 |
|
|
774 |
ML {*
|
12
|
775 |
fun build_goal thm constructors lifted_type mk_rep_abs =
|
8
|
776 |
let
|
|
777 |
fun is_const (Const (x, t)) = x mem constructors
|
|
778 |
| is_const _ = false
|
12
|
779 |
fun maybe_mk_rep_abs t =
|
|
780 |
let
|
|
781 |
val _ = writeln ("Maybe: " ^ Syntax.string_of_term @{context} t)
|
|
782 |
in
|
|
783 |
if type_of t = lifted_type then mk_rep_abs t else t
|
|
784 |
end
|
8
|
785 |
fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr))
|
|
786 |
| build_aux (f $ a) =
|
11
|
787 |
let
|
16
|
788 |
val (f, args) = strip_comb (f $ a)
|
12
|
789 |
val _ = writeln (Syntax.string_of_term @{context} f)
|
11
|
790 |
in
|
12
|
791 |
(if is_const f then maybe_mk_rep_abs (list_comb (f, (map maybe_mk_rep_abs (map build_aux args))))
|
11
|
792 |
else list_comb ((build_aux f), (map build_aux args)))
|
|
793 |
end
|
8
|
794 |
| build_aux x =
|
12
|
795 |
if is_const x then maybe_mk_rep_abs x else x
|
9
|
796 |
val concl = HOLogic.dest_Trueprop (Thm.concl_of thm)
|
8
|
797 |
in
|
|
798 |
HOLogic.mk_eq ((build_aux concl), concl)
|
|
799 |
end *}
|
|
800 |
|
16
|
801 |
ML {* val emptyt = (symmetric (unlam_def @{context} @{context} @{thm EMPTY_def})) *}
|
|
802 |
ML {* val in_t = (symmetric (unlam_def @{context} @{context} @{thm IN_def})) *}
|
|
803 |
ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *}
|
|
804 |
ML {* val cardt = symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *}
|
|
805 |
ML {* val insertt = symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *}
|
21
|
806 |
ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def CARD_def INSERT_def} *}
|
|
807 |
ML {* val fset_defs_sym = [emptyt, in_t, uniont, cardt, insertt] *}
|
18
|
808 |
|
|
809 |
ML {*
|
|
810 |
fun dest_cbinop t =
|
|
811 |
let
|
|
812 |
val (t2, rhs) = Thm.dest_comb t;
|
|
813 |
val (bop, lhs) = Thm.dest_comb t2;
|
|
814 |
in
|
|
815 |
(bop, (lhs, rhs))
|
|
816 |
end
|
|
817 |
*}
|
|
818 |
ML {*
|
|
819 |
fun dest_ceq t =
|
|
820 |
let
|
|
821 |
val (bop, pair) = dest_cbinop t;
|
|
822 |
val (bop_s, _) = Term.dest_Const (Thm.term_of bop);
|
|
823 |
in
|
|
824 |
if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))
|
|
825 |
end
|
|
826 |
*}
|
19
|
827 |
ML Thm.instantiate
|
|
828 |
ML {*@{thm arg_cong2}*}
|
|
829 |
ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *}
|
|
830 |
ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *}
|
|
831 |
ML {*
|
|
832 |
Toplevel.program (fn () =>
|
|
833 |
Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2}
|
|
834 |
)
|
|
835 |
*}
|
|
836 |
|
18
|
837 |
ML {*
|
19
|
838 |
fun foo_conv t =
|
18
|
839 |
let
|
|
840 |
val (lhs, rhs) = dest_ceq t;
|
|
841 |
val (bop, _) = dest_cbinop lhs;
|
19
|
842 |
val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
|
|
843 |
val [cmT, crT] = Thm.dest_ctyp cr2;
|
18
|
844 |
in
|
19
|
845 |
Drule.instantiate' [SOME clT,SOME cmT,SOME crT] [NONE,NONE,NONE,NONE,SOME bop] @{thm arg_cong2}
|
18
|
846 |
end
|
|
847 |
*}
|
19
|
848 |
|
18
|
849 |
ML {*
|
19
|
850 |
fun foo_tac n thm =
|
18
|
851 |
let
|
19
|
852 |
val concl = Thm.cprem_of thm n;
|
|
853 |
val (_, cconcl) = Thm.dest_comb concl;
|
|
854 |
val rewr = foo_conv cconcl;
|
|
855 |
val _ = tracing (Display.string_of_thm @{context} rewr)
|
|
856 |
val _ = tracing (Display.string_of_thm @{context} thm)
|
18
|
857 |
in
|
19
|
858 |
rtac rewr n thm
|
18
|
859 |
end
|
19
|
860 |
handle CTERM _ => Seq.empty
|
18
|
861 |
*}
|
19
|
862 |
|
20
|
863 |
(* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
|
|
864 |
|
19
|
865 |
ML {*
|
|
866 |
val foo_tac' =
|
|
867 |
FIRST' [
|
|
868 |
rtac @{thm list_eq_sym},
|
|
869 |
rtac @{thm cons_preserves},
|
|
870 |
rtac @{thm mem_respects},
|
|
871 |
foo_tac,
|
|
872 |
simp_tac (@{simpset} addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})
|
|
873 |
]
|
|
874 |
*}
|
|
875 |
|
20
|
876 |
thm m1
|
|
877 |
|
|
878 |
ML {*
|
|
879 |
val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
|
|
880 |
val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
|
|
881 |
val cgoal = cterm_of @{theory} goal
|
21
|
882 |
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
|
20
|
883 |
*}
|
|
884 |
|
|
885 |
prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
|
21
|
886 |
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
|
20
|
887 |
apply (tactic {* foo_tac' 1 *})
|
|
888 |
apply (tactic {* foo_tac' 1 *})
|
|
889 |
apply (tactic {* foo_tac' 1 *})
|
|
890 |
apply (tactic {* foo_tac' 1 *})
|
|
891 |
apply (tactic {* foo_tac' 1 *})
|
|
892 |
done
|
|
893 |
|
18
|
894 |
|
20
|
895 |
thm length_append (* Not true but worth checking that the goal is correct *)
|
|
896 |
ML {*
|
|
897 |
val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append}))
|
|
898 |
val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
|
|
899 |
val cgoal = cterm_of @{theory} goal
|
21
|
900 |
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
|
20
|
901 |
*}
|
|
902 |
(* prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
|
21
|
903 |
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
|
|
904 |
apply (tactic {* foo_tac' 1 *})
|
|
905 |
apply (tactic {* foo_tac' 2 *})
|
|
906 |
apply (tactic {* foo_tac' 2 *})
|
|
907 |
apply (tactic {* foo_tac' 2 *})
|
|
908 |
apply (tactic {* foo_tac' 1 *}) *)
|
19
|
909 |
|
20
|
910 |
thm m2
|
|
911 |
ML {*
|
|
912 |
val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2}))
|
|
913 |
val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
|
|
914 |
val cgoal = cterm_of @{theory} goal
|
21
|
915 |
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
|
20
|
916 |
*}
|
18
|
917 |
prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
|
21
|
918 |
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
|
|
919 |
apply (tactic {* foo_tac' 1 *})
|
|
920 |
apply (tactic {* foo_tac' 1 *})
|
|
921 |
apply (tactic {* foo_tac' 1 *})
|
|
922 |
apply (tactic {* foo_tac' 1 *})
|
|
923 |
apply (tactic {* foo_tac' 1 *})
|
|
924 |
apply (tactic {* foo_tac' 1 *})
|
|
925 |
apply (tactic {* foo_tac' 1 *})
|
|
926 |
apply (tactic {* foo_tac' 1 *})
|
|
927 |
apply (tactic {* foo_tac' 1 *})
|
|
928 |
apply (tactic {* foo_tac' 1 *})
|
|
929 |
apply (tactic {* foo_tac' 1 *})
|
|
930 |
apply (tactic {* foo_tac' 1 *})
|
|
931 |
apply (tactic {* foo_tac' 1 *})
|
|
932 |
done
|
|
933 |
|
|
934 |
thm list_eq.intros(4)
|
|
935 |
ML {*
|
|
936 |
val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(4)}))
|
|
937 |
val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
|
|
938 |
val cgoal = cterm_of @{theory} goal
|
|
939 |
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
|
|
940 |
(* Why doesn't this work? *)
|
|
941 |
val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10 QUOT_TYPE_I_fset.REPS_same} cgoal2)
|
|
942 |
*}
|
|
943 |
thm QUOT_TYPE_I_fset.thm10
|
|
944 |
thm QUOT_TYPE_I_fset.REPS_same
|
|
945 |
|
|
946 |
(* keep it commented out, until we get a proving mechanism *)
|
|
947 |
(*prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *}*)
|
|
948 |
lemma zzz :
|
|
949 |
"(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx>
|
|
950 |
REP_fset (INSERT a (ABS_fset xs))) = (a # a # xs \<approx> a # xs)"
|
|
951 |
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
|
|
952 |
apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
|
|
953 |
(* apply (simp only: QUOT_TYPE_I_fset.thm10)*)
|
|
954 |
apply (rule QUOT_TYPE_I_fset.R_trans2)
|
|
955 |
apply (tactic {* foo_tac' 1 *})
|
|
956 |
apply (tactic {* foo_tac' 1 *})
|
|
957 |
apply (tactic {* foo_tac' 1 *})
|
|
958 |
apply (tactic {* foo_tac' 1 *})
|
|
959 |
apply (tactic {* foo_tac' 1 *})
|
|
960 |
apply (tactic {* foo_tac' 1 *})
|
|
961 |
apply (tactic {* foo_tac' 1 *})
|
|
962 |
apply (tactic {* foo_tac' 1 *})
|
|
963 |
done
|
|
964 |
|
|
965 |
thm list_eq.intros(5)
|
|
966 |
ML {*
|
|
967 |
val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)}))
|
|
968 |
val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
|
|
969 |
val cgoal = cterm_of @{theory} goal
|
|
970 |
val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
|
|
971 |
*}
|
|
972 |
prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
|
|
973 |
apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
|
|
974 |
apply (rule QUOT_TYPE_I_fset.R_trans2)
|
|
975 |
apply (tactic {* foo_tac' 1 *})
|
|
976 |
apply (tactic {* foo_tac' 1 *})
|
|
977 |
apply (tactic {* foo_tac' 1 *})
|
|
978 |
apply (tactic {* foo_tac' 1 *})
|
|
979 |
apply (tactic {* foo_tac' 1 *})
|
|
980 |
apply (tactic {* foo_tac' 1 *})
|
|
981 |
apply (tactic {* foo_tac' 1 *})
|
|
982 |
apply (tactic {* foo_tac' 1 *})
|
|
983 |
done
|
18
|
984 |
|
|
985 |
(*
|
|
986 |
datatype obj1 =
|
|
987 |
OVAR1 "string"
|
|
988 |
| OBJ1 "(string * (string \<Rightarrow> obj1)) list"
|
|
989 |
| INVOKE1 "obj1 \<Rightarrow> string"
|
|
990 |
| UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"
|
|
991 |
*)
|
21
|
992 |
|
|
993 |
|