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