author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
Fri, 04 Dec 2009 15:41:09 +0100 | |
changeset 536 | 44fa9df44e6f |
parent 529 | 6348c2a57ec2 |
child 537 | 57073b0b8fac |
permissions | -rw-r--r-- |
0 | 1 |
theory QuotMain |
6 | 2 |
imports QuotScript QuotList Prove |
264
d0581fbc096c
split quotient.ML into two files
Christian Urban <urbanc@in.tum.de>
parents:
263
diff
changeset
|
3 |
uses ("quotient_info.ML") |
d0581fbc096c
split quotient.ML into two files
Christian Urban <urbanc@in.tum.de>
parents:
263
diff
changeset
|
4 |
("quotient.ML") |
277
37636f2b1c19
separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
275
diff
changeset
|
5 |
("quotient_def.ML") |
0 | 6 |
begin |
7 |
||
8 |
locale QUOT_TYPE = |
|
9 |
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
10 |
and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
|
11 |
and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
|
529 | 12 |
assumes equiv: "equivp R" |
0 | 13 |
and rep_prop: "\<And>y. \<exists>x. Rep y = R x" |
14 |
and rep_inverse: "\<And>x. Abs (Rep x) = x" |
|
15 |
and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)" |
|
16 |
and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)" |
|
15 | 17 |
begin |
0 | 18 |
|
19 |
definition |
|
200
d6a24dad5882
made quotients compatiple with Nominal; updated keyword file
Christian Urban <urbanc@in.tum.de>
parents:
198
diff
changeset
|
20 |
ABS::"'a \<Rightarrow> 'b" |
d6a24dad5882
made quotients compatiple with Nominal; updated keyword file
Christian Urban <urbanc@in.tum.de>
parents:
198
diff
changeset
|
21 |
where |
0 | 22 |
"ABS x \<equiv> Abs (R x)" |
23 |
||
24 |
definition |
|
200
d6a24dad5882
made quotients compatiple with Nominal; updated keyword file
Christian Urban <urbanc@in.tum.de>
parents:
198
diff
changeset
|
25 |
REP::"'b \<Rightarrow> 'a" |
d6a24dad5882
made quotients compatiple with Nominal; updated keyword file
Christian Urban <urbanc@in.tum.de>
parents:
198
diff
changeset
|
26 |
where |
0 | 27 |
"REP a = Eps (Rep a)" |
28 |
||
15 | 29 |
lemma lem9: |
0 | 30 |
shows "R (Eps (R x)) = R x" |
31 |
proof - |
|
529 | 32 |
have a: "R x x" using equiv by (simp add: equivp_reflp_symp_transp reflp_def) |
0 | 33 |
then have "R x (Eps (R x))" by (rule someI) |
15 | 34 |
then show "R (Eps (R x)) = R x" |
529 | 35 |
using equiv unfolding equivp_def by simp |
0 | 36 |
qed |
37 |
||
38 |
theorem thm10: |
|
24
6885fa184e89
Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
23
diff
changeset
|
39 |
shows "ABS (REP a) \<equiv> a" |
6885fa184e89
Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
23
diff
changeset
|
40 |
apply (rule eq_reflection) |
6885fa184e89
Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
23
diff
changeset
|
41 |
unfolding ABS_def REP_def |
0 | 42 |
proof - |
15 | 43 |
from rep_prop |
0 | 44 |
obtain x where eq: "Rep a = R x" by auto |
45 |
have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp |
|
46 |
also have "\<dots> = Abs (R x)" using lem9 by simp |
|
47 |
also have "\<dots> = Abs (Rep a)" using eq by simp |
|
48 |
also have "\<dots> = a" using rep_inverse by simp |
|
49 |
finally |
|
50 |
show "Abs (R (Eps (Rep a))) = a" by simp |
|
51 |
qed |
|
52 |
||
15 | 53 |
lemma REP_refl: |
0 | 54 |
shows "R (REP a) (REP a)" |
55 |
unfolding REP_def |
|
529 | 56 |
by (simp add: equiv[simplified equivp_def]) |
0 | 57 |
|
58 |
lemma lem7: |
|
22 | 59 |
shows "(R x = R y) = (Abs (R x) = Abs (R y))" |
0 | 60 |
apply(rule iffI) |
61 |
apply(simp) |
|
62 |
apply(drule rep_inject[THEN iffD2]) |
|
63 |
apply(simp add: abs_inverse) |
|
64 |
done |
|
15 | 65 |
|
0 | 66 |
theorem thm11: |
67 |
shows "R r r' = (ABS r = ABS r')" |
|
68 |
unfolding ABS_def |
|
529 | 69 |
by (simp only: equiv[simplified equivp_def] lem7) |
0 | 70 |
|
4 | 71 |
|
2 | 72 |
lemma REP_ABS_rsp: |
4 | 73 |
shows "R f (REP (ABS g)) = R f g" |
74 |
and "R (REP (ABS g)) f = R g f" |
|
23 | 75 |
by (simp_all add: thm10 thm11) |
4 | 76 |
|
529 | 77 |
lemma Quotient: |
78 |
"Quotient R ABS REP" |
|
79 |
apply(unfold Quotient_def) |
|
0 | 80 |
apply(simp add: thm10) |
81 |
apply(simp add: REP_refl) |
|
82 |
apply(subst thm11[symmetric]) |
|
529 | 83 |
apply(simp add: equiv[simplified equivp_def]) |
0 | 84 |
done |
85 |
||
21
d15121412caa
Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
20
diff
changeset
|
86 |
lemma R_trans: |
49 | 87 |
assumes ab: "R a b" |
88 |
and bc: "R b c" |
|
22 | 89 |
shows "R a c" |
21
d15121412caa
Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
20
diff
changeset
|
90 |
proof - |
529 | 91 |
have tr: "transp R" using equiv equivp_reflp_symp_transp[of R] by simp |
21
d15121412caa
Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
20
diff
changeset
|
92 |
moreover have ab: "R a b" by fact |
d15121412caa
Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
20
diff
changeset
|
93 |
moreover have bc: "R b c" by fact |
529 | 94 |
ultimately show "R a c" unfolding transp_def by blast |
21
d15121412caa
Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
20
diff
changeset
|
95 |
qed |
d15121412caa
Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
20
diff
changeset
|
96 |
|
d15121412caa
Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
20
diff
changeset
|
97 |
lemma R_sym: |
49 | 98 |
assumes ab: "R a b" |
22 | 99 |
shows "R b a" |
21
d15121412caa
Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
20
diff
changeset
|
100 |
proof - |
529 | 101 |
have re: "symp R" using equiv equivp_reflp_symp_transp[of R] by simp |
102 |
then show "R b a" using ab unfolding symp_def by blast |
|
21
d15121412caa
Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
20
diff
changeset
|
103 |
qed |
d15121412caa
Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
20
diff
changeset
|
104 |
|
49 | 105 |
lemma R_trans2: |
106 |
assumes ac: "R a c" |
|
22 | 107 |
and bd: "R b d" |
21
d15121412caa
Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
20
diff
changeset
|
108 |
shows "R a b = R c d" |
200
d6a24dad5882
made quotients compatiple with Nominal; updated keyword file
Christian Urban <urbanc@in.tum.de>
parents:
198
diff
changeset
|
109 |
using ac bd |
d6a24dad5882
made quotients compatiple with Nominal; updated keyword file
Christian Urban <urbanc@in.tum.de>
parents:
198
diff
changeset
|
110 |
by (blast intro: R_trans R_sym) |
21
d15121412caa
Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
20
diff
changeset
|
111 |
|
d15121412caa
Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
20
diff
changeset
|
112 |
lemma REPS_same: |
25
9020ee23a020
The tactic with REPEAT, CHANGED and a proper simpset.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
24
diff
changeset
|
113 |
shows "R (REP a) (REP b) \<equiv> (a = b)" |
38 | 114 |
proof - |
115 |
have "R (REP a) (REP b) = (a = b)" |
|
116 |
proof |
|
117 |
assume as: "R (REP a) (REP b)" |
|
118 |
from rep_prop |
|
119 |
obtain x y |
|
120 |
where eqs: "Rep a = R x" "Rep b = R y" by blast |
|
121 |
from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp |
|
122 |
then have "R x (Eps (R y))" using lem9 by simp |
|
123 |
then have "R (Eps (R y)) x" using R_sym by blast |
|
124 |
then have "R y x" using lem9 by simp |
|
125 |
then have "R x y" using R_sym by blast |
|
126 |
then have "ABS x = ABS y" using thm11 by simp |
|
127 |
then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp |
|
128 |
then show "a = b" using rep_inverse by simp |
|
129 |
next |
|
130 |
assume ab: "a = b" |
|
529 | 131 |
have "reflp R" using equiv equivp_reflp_symp_transp[of R] by simp |
132 |
then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto |
|
38 | 133 |
qed |
134 |
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
|
135 |
qed |
d15121412caa
Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
20
diff
changeset
|
136 |
|
0 | 137 |
end |
138 |
||
139 |
section {* type definition for the quotient type *} |
|
140 |
||
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents:
267
diff
changeset
|
141 |
(* the auxiliary data for the quotient types *) |
264
d0581fbc096c
split quotient.ML into two files
Christian Urban <urbanc@in.tum.de>
parents:
263
diff
changeset
|
142 |
use "quotient_info.ML" |
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents:
267
diff
changeset
|
143 |
|
185
929bc55efff7
added code for declaring map-functions
Christian Urban <urbanc@in.tum.de>
parents:
182
diff
changeset
|
144 |
declare [[map list = (map, LIST_REL)]] |
929bc55efff7
added code for declaring map-functions
Christian Urban <urbanc@in.tum.de>
parents:
182
diff
changeset
|
145 |
declare [[map * = (prod_fun, prod_rel)]] |
536
44fa9df44e6f
More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
529
diff
changeset
|
146 |
declare [[map "fun" = (fun_map, fun_rel)]] |
185
929bc55efff7
added code for declaring map-functions
Christian Urban <urbanc@in.tum.de>
parents:
182
diff
changeset
|
147 |
|
506
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
505
diff
changeset
|
148 |
lemmas [quotient_thm] = |
529 | 149 |
FUN_Quotient LIST_Quotient |
506
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
505
diff
changeset
|
150 |
|
185
929bc55efff7
added code for declaring map-functions
Christian Urban <urbanc@in.tum.de>
parents:
182
diff
changeset
|
151 |
ML {* maps_lookup @{theory} "List.list" *} |
929bc55efff7
added code for declaring map-functions
Christian Urban <urbanc@in.tum.de>
parents:
182
diff
changeset
|
152 |
ML {* maps_lookup @{theory} "*" *} |
929bc55efff7
added code for declaring map-functions
Christian Urban <urbanc@in.tum.de>
parents:
182
diff
changeset
|
153 |
ML {* maps_lookup @{theory} "fun" *} |
174
09048a951dca
moved the map_funs setup into QuotMain
Christian Urban <urbanc@in.tum.de>
parents:
170
diff
changeset
|
154 |
|
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents:
267
diff
changeset
|
155 |
|
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents:
267
diff
changeset
|
156 |
(* definition of the quotient types *) |
277
37636f2b1c19
separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
275
diff
changeset
|
157 |
(* FIXME: should be called quotient_typ.ML *) |
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents:
267
diff
changeset
|
158 |
use "quotient.ML" |
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents:
267
diff
changeset
|
159 |
|
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
parents:
267
diff
changeset
|
160 |
|
277
37636f2b1c19
separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
275
diff
changeset
|
161 |
(* lifting of constants *) |
37636f2b1c19
separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
275
diff
changeset
|
162 |
use "quotient_def.ML" |
37636f2b1c19
separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
275
diff
changeset
|
163 |
|
381
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
164 |
(* TODO: Consider defining it with an "if"; sth like: |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
165 |
Babs p m = \<lambda>x. if x \<in> p then m x else undefined |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
166 |
*) |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
167 |
definition |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
168 |
Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
169 |
where |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
170 |
"(x \<in> p) \<Longrightarrow> (Babs p m x = m x)" |
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
parents:
307
diff
changeset
|
171 |
|
139 | 172 |
section {* ATOMIZE *} |
173 |
||
381
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
174 |
lemma atomize_eqv[atomize]: |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
175 |
shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
139 | 176 |
proof |
381
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
177 |
assume "A \<equiv> B" |
139 | 178 |
then show "Trueprop A \<equiv> Trueprop B" by unfold |
179 |
next |
|
180 |
assume *: "Trueprop A \<equiv> Trueprop B" |
|
181 |
have "A = B" |
|
182 |
proof (cases A) |
|
183 |
case True |
|
184 |
have "A" by fact |
|
185 |
then show "A = B" using * by simp |
|
186 |
next |
|
187 |
case False |
|
188 |
have "\<not>A" by fact |
|
189 |
then show "A = B" using * by auto |
|
190 |
qed |
|
191 |
then show "A \<equiv> B" by (rule eq_reflection) |
|
192 |
qed |
|
193 |
||
194 |
ML {* |
|
195 |
fun atomize_thm thm = |
|
196 |
let |
|
221 | 197 |
val thm' = Thm.freezeT (forall_intr_vars thm) |
139 | 198 |
val thm'' = ObjectLogic.atomize (cprop_of thm') |
199 |
in |
|
404 | 200 |
@{thm equal_elim_rule1} OF [thm'', thm'] |
139 | 201 |
end |
202 |
*} |
|
203 |
||
387 | 204 |
section {* infrastructure about id *} |
381
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
205 |
|
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
206 |
lemma prod_fun_id: "prod_fun id id \<equiv> id" |
415
5a9bdf81672d
More cleaning in QuotMain, identity handling.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
413
diff
changeset
|
207 |
by (rule eq_reflection) (simp add: prod_fun_def) |
381
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
208 |
|
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
209 |
lemma map_id: "map id \<equiv> id" |
415
5a9bdf81672d
More cleaning in QuotMain, identity handling.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
413
diff
changeset
|
210 |
apply (rule eq_reflection) |
5a9bdf81672d
More cleaning in QuotMain, identity handling.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
413
diff
changeset
|
211 |
apply (rule ext) |
5a9bdf81672d
More cleaning in QuotMain, identity handling.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
413
diff
changeset
|
212 |
apply (rule_tac list="x" in list.induct) |
5a9bdf81672d
More cleaning in QuotMain, identity handling.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
413
diff
changeset
|
213 |
apply (simp_all) |
5a9bdf81672d
More cleaning in QuotMain, identity handling.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
413
diff
changeset
|
214 |
done |
381
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
215 |
|
409
6b59a3844055
introduced a separate lemma for id_simps
Christian Urban <urbanc@in.tum.de>
parents:
408
diff
changeset
|
216 |
lemmas id_simps = |
6b59a3844055
introduced a separate lemma for id_simps
Christian Urban <urbanc@in.tum.de>
parents:
408
diff
changeset
|
217 |
FUN_MAP_I[THEN eq_reflection] |
6b59a3844055
introduced a separate lemma for id_simps
Christian Urban <urbanc@in.tum.de>
parents:
408
diff
changeset
|
218 |
id_apply[THEN eq_reflection] |
415
5a9bdf81672d
More cleaning in QuotMain, identity handling.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
413
diff
changeset
|
219 |
id_def[THEN eq_reflection,symmetric] |
5a9bdf81672d
More cleaning in QuotMain, identity handling.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
413
diff
changeset
|
220 |
prod_fun_id map_id |
409
6b59a3844055
introduced a separate lemma for id_simps
Christian Urban <urbanc@in.tum.de>
parents:
408
diff
changeset
|
221 |
|
381
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
222 |
ML {* |
409
6b59a3844055
introduced a separate lemma for id_simps
Christian Urban <urbanc@in.tum.de>
parents:
408
diff
changeset
|
223 |
fun simp_ids thm = |
6b59a3844055
introduced a separate lemma for id_simps
Christian Urban <urbanc@in.tum.de>
parents:
408
diff
changeset
|
224 |
MetaSimplifier.rewrite_rule @{thms id_simps} thm |
381
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
225 |
*} |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
226 |
|
407
d387743f022b
tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents:
405
diff
changeset
|
227 |
section {* Debugging infrastructure for testing tactics *} |
381
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
228 |
|
447
3e7ee6f5437d
selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
Christian Urban <urbanc@in.tum.de>
parents:
446
diff
changeset
|
229 |
ML {* |
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents:
449
diff
changeset
|
230 |
fun my_print_tac ctxt s i thm = |
407
d387743f022b
tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents:
405
diff
changeset
|
231 |
let |
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents:
449
diff
changeset
|
232 |
val prem_str = nth (prems_of thm) (i - 1) |
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents:
449
diff
changeset
|
233 |
|> Syntax.string_of_term ctxt |
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents:
449
diff
changeset
|
234 |
handle Subscript => "no subgoal" |
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents:
449
diff
changeset
|
235 |
val _ = tracing (s ^ "\n" ^ prem_str) |
407
d387743f022b
tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents:
405
diff
changeset
|
236 |
in |
d387743f022b
tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents:
405
diff
changeset
|
237 |
Seq.single thm |
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents:
449
diff
changeset
|
238 |
end *} |
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents:
449
diff
changeset
|
239 |
|
407
d387743f022b
tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents:
405
diff
changeset
|
240 |
|
447
3e7ee6f5437d
selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
Christian Urban <urbanc@in.tum.de>
parents:
446
diff
changeset
|
241 |
ML {* |
3e7ee6f5437d
selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
Christian Urban <urbanc@in.tum.de>
parents:
446
diff
changeset
|
242 |
fun DT ctxt s tac i thm = |
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents:
449
diff
changeset
|
243 |
let |
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents:
449
diff
changeset
|
244 |
val before_goal = nth (prems_of thm) (i - 1) |
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents:
449
diff
changeset
|
245 |
|> Syntax.string_of_term ctxt |
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents:
449
diff
changeset
|
246 |
val before_msg = ["before: " ^ s, before_goal, "after: " ^ s] |
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents:
449
diff
changeset
|
247 |
|> cat_lines |
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents:
449
diff
changeset
|
248 |
in |
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents:
449
diff
changeset
|
249 |
EVERY [tac i, my_print_tac ctxt before_msg i] thm |
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
parents:
449
diff
changeset
|
250 |
end |
444 | 251 |
|
447
3e7ee6f5437d
selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
Christian Urban <urbanc@in.tum.de>
parents:
446
diff
changeset
|
252 |
fun NDT ctxt s tac thm = tac thm |
407
d387743f022b
tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents:
405
diff
changeset
|
253 |
*} |
d387743f022b
tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents:
405
diff
changeset
|
254 |
|
453
c22ab554a32d
started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
parents:
452
diff
changeset
|
255 |
|
407
d387743f022b
tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents:
405
diff
changeset
|
256 |
section {* Infrastructure for collecting theorems for starting the lifting *} |
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
264
diff
changeset
|
257 |
|
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
264
diff
changeset
|
258 |
ML {* |
239
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
259 |
fun lookup_quot_data lthy qty = |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
260 |
let |
311
77fc6f3c0343
changed the quotdata to be a symtab table (needs fixing)
Christian Urban <urbanc@in.tum.de>
parents:
310
diff
changeset
|
261 |
val qty_name = fst (dest_Type qty) |
314 | 262 |
val SOME quotdata = quotdata_lookup lthy qty_name |
311
77fc6f3c0343
changed the quotdata to be a symtab table (needs fixing)
Christian Urban <urbanc@in.tum.de>
parents:
310
diff
changeset
|
263 |
(* cu: Changed the lookup\<dots>not sure whether this works *) |
303
991b0e53f9dc
More code cleaning and commenting
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
302
diff
changeset
|
264 |
(* TODO: Should no longer be needed *) |
257
68bd5c2a1b96
Fixed quotdata_lookup.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
255
diff
changeset
|
265 |
val rty = Logic.unvarifyT (#rtyp quotdata) |
239
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
266 |
val rel = #rel quotdata |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
267 |
val rel_eqv = #equiv_thm quotdata |
529 | 268 |
val rel_refl = @{thm equivp_reflp} OF [rel_eqv] |
239
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
269 |
in |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
270 |
(rty, rel, rel_refl, rel_eqv) |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
271 |
end |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
272 |
*} |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
273 |
|
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
274 |
ML {* |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
275 |
fun lookup_quot_thms lthy qty_name = |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
276 |
let |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
277 |
val thy = ProofContext.theory_of lthy; |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
278 |
val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2") |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
279 |
val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same") |
269 | 280 |
val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10") |
529 | 281 |
val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name) |
239
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
282 |
in |
269 | 283 |
(trans2, reps_same, absrep, quot) |
239
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
284 |
end |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
285 |
*} |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
286 |
|
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
287 |
ML {* |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
288 |
fun lookup_quot_consts defs = |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
289 |
let |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
290 |
fun dest_term (a $ b) = (a, b); |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
291 |
val def_terms = map (snd o Logic.dest_equals o concl_of) defs; |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
292 |
in |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
293 |
map (fst o dest_Const o snd o dest_term) def_terms |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
294 |
end |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
295 |
*} |
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
296 |
|
402
dd64cca9265c
recommited changes of comments
Christian Urban <urbanc@in.tum.de>
parents:
401
diff
changeset
|
297 |
section {* Regularization *} |
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
298 |
|
383
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
299 |
(* |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
300 |
Regularizing an rtrm means: |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
301 |
- quantifiers over a type that needs lifting are replaced by |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
302 |
bounded quantifiers, for example: |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
303 |
\<forall>x. P \<Longrightarrow> \<forall>x \<in> (Respects R). P / All (Respects R) P |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
304 |
|
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
305 |
the relation R is given by the rty and qty; |
330
1a0f0b758071
a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents:
326
diff
changeset
|
306 |
|
383
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
307 |
- abstractions over a type that needs lifting are replaced |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
308 |
by bounded abstractions: |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
309 |
\<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P) |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
310 |
|
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
311 |
- equalities over the type being lifted are replaced by |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
312 |
corresponding relations: |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
313 |
A = B \<Longrightarrow> A \<approx> B |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
314 |
|
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
315 |
example with more complicated types of A, B: |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
316 |
A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A B |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
317 |
*) |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
318 |
|
404 | 319 |
ML {* |
383
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
320 |
(* builds the relation that is the argument of respects *) |
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
321 |
fun mk_resp_arg lthy (rty, qty) = |
319 | 322 |
let |
323 |
val thy = ProofContext.theory_of lthy |
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
324 |
in |
334 | 325 |
if rty = qty |
326 |
then HOLogic.eq_const rty |
|
327 |
else |
|
328 |
case (rty, qty) of |
|
329 |
(Type (s, tys), Type (s', tys')) => |
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
330 |
if s = s' |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
331 |
then let |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
332 |
val SOME map_info = maps_lookup thy s |
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents:
320
diff
changeset
|
333 |
val args = map (mk_resp_arg lthy) (tys ~~ tys') |
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
334 |
in |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
335 |
list_comb (Const (#relfun map_info, dummyT), args) |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
336 |
end |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
337 |
else let |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
338 |
val SOME qinfo = quotdata_lookup_thy thy s' |
330
1a0f0b758071
a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents:
326
diff
changeset
|
339 |
(* FIXME: check in this case that the rty and qty *) |
1a0f0b758071
a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents:
326
diff
changeset
|
340 |
(* FIXME: correspond to each other *) |
353
9a0e8ab42ee8
fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
Christian Urban <urbanc@in.tum.de>
parents:
351
diff
changeset
|
341 |
val (s, _) = dest_Const (#rel qinfo) |
407
d387743f022b
tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents:
405
diff
changeset
|
342 |
(* FIXME: the relation should only be the string *) |
d387743f022b
tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents:
405
diff
changeset
|
343 |
(* FIXME: and the type needs to be calculated as below; *) |
d387743f022b
tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents:
405
diff
changeset
|
344 |
(* FIXME: maybe one should actually have a term *) |
d387743f022b
tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents:
405
diff
changeset
|
345 |
(* FIXME: and one needs to force it to have this type *) |
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
346 |
in |
353
9a0e8ab42ee8
fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
Christian Urban <urbanc@in.tum.de>
parents:
351
diff
changeset
|
347 |
Const (s, rty --> rty --> @{typ bool}) |
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
348 |
end |
334 | 349 |
| _ => HOLogic.eq_const dummyT |
351 | 350 |
(* FIXME: check that the types correspond to each other? *) |
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
351 |
end |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
352 |
*} |
239
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
353 |
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
354 |
ML {* |
467 | 355 |
val mk_babs = Const (@{const_name Babs}, dummyT) |
356 |
val mk_ball = Const (@{const_name Ball}, dummyT) |
|
357 |
val mk_bex = Const (@{const_name Bex}, dummyT) |
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
358 |
val mk_resp = Const (@{const_name Respects}, dummyT) |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
359 |
*} |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
360 |
|
323 | 361 |
ML {* |
330
1a0f0b758071
a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents:
326
diff
changeset
|
362 |
(* - applies f to the subterm of an abstraction, *) |
1a0f0b758071
a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents:
326
diff
changeset
|
363 |
(* otherwise to the given term, *) |
405
8bc7428745ad
renamed REGULARIZE to be regularize
Christian Urban <urbanc@in.tum.de>
parents:
404
diff
changeset
|
364 |
(* - used by regularize, therefore abstracted *) |
330
1a0f0b758071
a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents:
326
diff
changeset
|
365 |
(* variables do not have to be treated specially *) |
1a0f0b758071
a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents:
326
diff
changeset
|
366 |
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
367 |
fun apply_subt f trm1 trm2 = |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
368 |
case (trm1, trm2) of |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
369 |
(Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t') |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
370 |
| _ => f trm1 trm2 |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
371 |
|
330
1a0f0b758071
a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents:
326
diff
changeset
|
372 |
(* the major type of All and Ex quantifiers *) |
334 | 373 |
fun qnt_typ ty = domain_type (domain_type ty) |
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
374 |
*} |
319 | 375 |
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
376 |
ML {* |
330
1a0f0b758071
a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents:
326
diff
changeset
|
377 |
(* produces a regularized version of rtm *) |
1a0f0b758071
a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents:
326
diff
changeset
|
378 |
(* - the result is still not completely typed *) |
1a0f0b758071
a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents:
326
diff
changeset
|
379 |
(* - does not need any special treatment of *) |
1a0f0b758071
a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents:
326
diff
changeset
|
380 |
(* bound variables *) |
1a0f0b758071
a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents:
326
diff
changeset
|
381 |
|
405
8bc7428745ad
renamed REGULARIZE to be regularize
Christian Urban <urbanc@in.tum.de>
parents:
404
diff
changeset
|
382 |
fun regularize_trm lthy rtrm qtrm = |
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
383 |
case (rtrm, qtrm) of |
325 | 384 |
(Abs (x, ty, t), Abs (x', ty', t')) => |
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
385 |
let |
405
8bc7428745ad
renamed REGULARIZE to be regularize
Christian Urban <urbanc@in.tum.de>
parents:
404
diff
changeset
|
386 |
val subtrm = regularize_trm lthy t t' |
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
387 |
in |
325 | 388 |
if ty = ty' |
389 |
then Abs (x, ty, subtrm) |
|
326
e755a5da14c8
my first version of repabs injection
Christian Urban <urbanc@in.tum.de>
parents:
325
diff
changeset
|
390 |
else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm |
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
391 |
end |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
392 |
| (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
393 |
let |
405
8bc7428745ad
renamed REGULARIZE to be regularize
Christian Urban <urbanc@in.tum.de>
parents:
404
diff
changeset
|
394 |
val subtrm = apply_subt (regularize_trm lthy) t t' |
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
395 |
in |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
396 |
if ty = ty' |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
397 |
then Const (@{const_name "All"}, ty) $ subtrm |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
398 |
else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
399 |
end |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
400 |
| (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
401 |
let |
405
8bc7428745ad
renamed REGULARIZE to be regularize
Christian Urban <urbanc@in.tum.de>
parents:
404
diff
changeset
|
402 |
val subtrm = apply_subt (regularize_trm lthy) t t' |
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
403 |
in |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
404 |
if ty = ty' |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
405 |
then Const (@{const_name "Ex"}, ty) $ subtrm |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
406 |
else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
407 |
end |
351 | 408 |
(* FIXME: Should = only be replaced, when fully applied? *) |
409 |
(* Then there must be a 2nd argument *) |
|
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
410 |
| (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') => |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
411 |
let |
405
8bc7428745ad
renamed REGULARIZE to be regularize
Christian Urban <urbanc@in.tum.de>
parents:
404
diff
changeset
|
412 |
val subtrm = regularize_trm lthy t t' |
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
413 |
in |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
414 |
if ty = ty' |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
415 |
then Const (@{const_name "op ="}, ty) $ subtrm |
349
f507f088de73
domain_type in regularizing equality
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
348
diff
changeset
|
416 |
else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm |
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
417 |
end |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
418 |
| (t1 $ t2, t1' $ t2') => |
405
8bc7428745ad
renamed REGULARIZE to be regularize
Christian Urban <urbanc@in.tum.de>
parents:
404
diff
changeset
|
419 |
(regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') |
453
c22ab554a32d
started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
parents:
452
diff
changeset
|
420 |
| (Free (x, ty), Free (x', ty')) => |
c22ab554a32d
started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
parents:
452
diff
changeset
|
421 |
(* this case cannot arrise as we start with two fully atomized terms *) |
c22ab554a32d
started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
parents:
452
diff
changeset
|
422 |
raise (LIFT_MATCH "regularize (frees)") |
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
423 |
| (Bound i, Bound i') => |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
424 |
if i = i' |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
425 |
then rtrm |
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
426 |
else raise (LIFT_MATCH "regularize (bounds)") |
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
427 |
| (Const (s, ty), Const (s', ty')) => |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
428 |
if s = s' andalso ty = ty' |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
429 |
then rtrm |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
430 |
else rtrm (* FIXME: check correspondence according to definitions *) |
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
431 |
| (rt, qt) => |
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
432 |
raise (LIFT_MATCH "regularize (default)") |
320
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
433 |
*} |
7d3d86beacd6
started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de>
parents:
319
diff
changeset
|
434 |
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents:
320
diff
changeset
|
435 |
(* |
407
d387743f022b
tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents:
405
diff
changeset
|
436 |
FIXME / TODO: needs to be adapted |
d387743f022b
tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de>
parents:
405
diff
changeset
|
437 |
|
383
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
438 |
To prove that the raw theorem implies the regularised one, |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
439 |
we try in order: |
330
1a0f0b758071
a little tuning of comments
Christian Urban <urbanc@in.tum.de>
parents:
326
diff
changeset
|
440 |
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents:
320
diff
changeset
|
441 |
- Reflexivity of the relation |
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents:
320
diff
changeset
|
442 |
- Assumption |
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents:
320
diff
changeset
|
443 |
- Elimnating quantifiers on both sides of toplevel implication |
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents:
320
diff
changeset
|
444 |
- Simplifying implications on both sides of toplevel implication |
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents:
320
diff
changeset
|
445 |
- Ball (Respects ?E) ?P = All ?P |
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents:
320
diff
changeset
|
446 |
- (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q |
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents:
320
diff
changeset
|
447 |
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents:
320
diff
changeset
|
448 |
*) |
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
parents:
320
diff
changeset
|
449 |
|
442
7beed9b75ea2
renamed LAMBDA_RES_TAC and WEAK_LAMBDA_RES_TAC to lower case names
Christian Urban <urbanc@in.tum.de>
parents:
440
diff
changeset
|
450 |
(* FIXME: they should be in in the new Isabelle *) |
404 | 451 |
lemma [mono]: |
452 |
"(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)" |
|
400 | 453 |
by blast |
454 |
||
455 |
lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P" |
|
456 |
by auto |
|
457 |
||
529 | 458 |
(* FIXME: OPTION_equivp, PAIR_equivp, ... *) |
400 | 459 |
ML {* |
460 |
fun equiv_tac rel_eqvs = |
|
420
dcfe009c98aa
replaced FIRST' (map rtac list) with resolve_tac list
Christian Urban <urbanc@in.tum.de>
parents:
419
diff
changeset
|
461 |
REPEAT_ALL_NEW (FIRST' |
dcfe009c98aa
replaced FIRST' (map rtac list) with resolve_tac list
Christian Urban <urbanc@in.tum.de>
parents:
419
diff
changeset
|
462 |
[resolve_tac rel_eqvs, |
529 | 463 |
rtac @{thm IDENTITY_equivp}, |
464 |
rtac @{thm LIST_equivp}]) |
|
400 | 465 |
*} |
466 |
||
467 |
ML {* |
|
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
468 |
fun ball_reg_eqv_simproc rel_eqvs ss redex = |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
469 |
let |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
470 |
val ctxt = Simplifier.the_context ss |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
471 |
val thy = ProofContext.theory_of ctxt |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
472 |
in |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
473 |
case redex of |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
474 |
(ogl as ((Const (@{const_name "Ball"}, _)) $ |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
475 |
((Const (@{const_name "Respects"}, _)) $ R) $ P1)) => |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
476 |
(let |
529 | 477 |
val gl = Const (@{const_name "equivp"}, dummyT) $ R; |
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
478 |
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
479 |
val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
480 |
val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]); |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
481 |
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
482 |
in |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
483 |
SOME thm |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
484 |
end |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
485 |
handle _ => NONE |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
486 |
) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
487 |
| _ => NONE |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
488 |
end |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
489 |
*} |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
490 |
|
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
491 |
ML {* |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
492 |
fun bex_reg_eqv_simproc rel_eqvs ss redex = |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
493 |
let |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
494 |
val ctxt = Simplifier.the_context ss |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
495 |
val thy = ProofContext.theory_of ctxt |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
496 |
in |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
497 |
case redex of |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
498 |
(ogl as ((Const (@{const_name "Bex"}, _)) $ |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
499 |
((Const (@{const_name "Respects"}, _)) $ R) $ P1)) => |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
500 |
(let |
529 | 501 |
val gl = Const (@{const_name "equivp"}, dummyT) $ R; |
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
502 |
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
503 |
val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
504 |
val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]); |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
505 |
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
506 |
in |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
507 |
SOME thm |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
508 |
end |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
509 |
handle _ => NONE |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
510 |
) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
511 |
| _ => NONE |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
512 |
end |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
513 |
*} |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
514 |
|
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
515 |
ML {* |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
516 |
fun prep_trm thy (x, (T, t)) = |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
517 |
(cterm_of thy (Var (x, T)), cterm_of thy t) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
518 |
|
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
519 |
fun prep_ty thy (x, (S, ty)) = |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
520 |
(ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
521 |
*} |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
522 |
|
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
523 |
ML {* |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
524 |
fun matching_prs thy pat trm = |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
525 |
let |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
526 |
val univ = Unify.matchers thy [(pat, trm)] |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
527 |
val SOME (env, _) = Seq.pull univ |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
528 |
val tenv = Vartab.dest (Envir.term_env env) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
529 |
val tyenv = Vartab.dest (Envir.type_env env) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
530 |
in |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
531 |
(map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
532 |
end |
400 | 533 |
*} |
534 |
||
535 |
ML {* |
|
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
536 |
fun ball_reg_eqv_range_simproc rel_eqvs ss redex = |
400 | 537 |
let |
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
538 |
val ctxt = Simplifier.the_context ss |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
539 |
val thy = ProofContext.theory_of ctxt |
400 | 540 |
in |
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
541 |
case redex of |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
542 |
(ogl as ((Const (@{const_name "Ball"}, _)) $ |
536
44fa9df44e6f
More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
529
diff
changeset
|
543 |
((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) => |
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
544 |
(let |
529 | 545 |
val gl = Const (@{const_name "equivp"}, dummyT) $ R2; |
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
546 |
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
487
f5db9ede89b0
Experiments with OPTION_map
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
486
diff
changeset
|
547 |
(* val _ = tracing (Syntax.string_of_term ctxt glc);*) |
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
548 |
val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
549 |
val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]); |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
550 |
val R1c = cterm_of thy R1; |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
551 |
val thmi = Drule.instantiate' [] [SOME R1c] thm; |
487
f5db9ede89b0
Experiments with OPTION_map
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
486
diff
changeset
|
552 |
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi));*) |
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
553 |
val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
554 |
val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); |
487
f5db9ede89b0
Experiments with OPTION_map
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
486
diff
changeset
|
555 |
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); *) |
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
556 |
in |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
557 |
SOME thm2 |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
558 |
end |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
559 |
handle _ => NONE |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
560 |
|
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
561 |
) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
562 |
| _ => NONE |
400 | 563 |
end |
564 |
*} |
|
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
565 |
|
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
566 |
ML {* |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
567 |
fun bex_reg_eqv_range_simproc rel_eqvs ss redex = |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
568 |
let |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
569 |
val ctxt = Simplifier.the_context ss |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
570 |
val thy = ProofContext.theory_of ctxt |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
571 |
in |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
572 |
case redex of |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
573 |
(ogl as ((Const (@{const_name "Bex"}, _)) $ |
536
44fa9df44e6f
More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
529
diff
changeset
|
574 |
((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) => |
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
575 |
(let |
529 | 576 |
val gl = Const (@{const_name "equivp"}, dummyT) $ R2; |
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
577 |
val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
487
f5db9ede89b0
Experiments with OPTION_map
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
486
diff
changeset
|
578 |
(* val _ = tracing (Syntax.string_of_term ctxt glc); *) |
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
579 |
val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
580 |
val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]); |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
581 |
val R1c = cterm_of thy R1; |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
582 |
val thmi = Drule.instantiate' [] [SOME R1c] thm; |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
583 |
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
584 |
val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
585 |
val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); |
487
f5db9ede89b0
Experiments with OPTION_map
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
486
diff
changeset
|
586 |
(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));*) |
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
587 |
in |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
588 |
SOME thm2 |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
589 |
end |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
590 |
handle _ => NONE |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
591 |
|
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
592 |
) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
593 |
| _ => NONE |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
594 |
end |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
595 |
*} |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
596 |
|
529 | 597 |
lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
598 |
by (simp add: equivp_reflp) |
|
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
599 |
|
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
600 |
ML {* |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
601 |
fun regularize_tac ctxt rel_eqvs = |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
602 |
let |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
603 |
val pat1 = [@{term "Ball (Respects R) P"}]; |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
604 |
val pat2 = [@{term "Bex (Respects R) P"}]; |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
605 |
val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}]; |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
606 |
val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}]; |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
607 |
val thy = ProofContext.theory_of ctxt |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
608 |
val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs)) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
609 |
val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc rel_eqvs)) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
610 |
val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs)) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
611 |
val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs)) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
612 |
val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4] |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
613 |
(* TODO: Make sure that there are no LIST_REL, PAIR_REL etc involved *) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
614 |
val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) rel_eqvs |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
615 |
in |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
616 |
ObjectLogic.full_atomize_tac THEN' |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
617 |
simp_tac simp_ctxt THEN' |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
618 |
REPEAT_ALL_NEW (FIRST' [ |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
619 |
rtac @{thm ball_reg_right}, |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
620 |
rtac @{thm bex_reg_left}, |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
621 |
resolve_tac (Inductive.get_monos ctxt), |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
622 |
rtac @{thm ball_all_comm}, |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
623 |
rtac @{thm bex_ex_comm}, |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
624 |
resolve_tac eq_eqvs, |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
625 |
simp_tac simp_ctxt |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
626 |
]) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
627 |
end |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
628 |
*} |
390 | 629 |
|
630 |
section {* Injections of REP and ABSes *} |
|
383
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
631 |
|
381
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
632 |
(* |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
633 |
Injecting REPABS means: |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
634 |
|
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
635 |
For abstractions: |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
636 |
* If the type of the abstraction doesn't need lifting we recurse. |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
637 |
* If it does we add RepAbs around the whole term and check if the |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
638 |
variable needs lifting. |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
639 |
* If it doesn't then we recurse |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
640 |
* If it does we recurse and put 'RepAbs' around all occurences |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
641 |
of the variable in the obtained subterm. This in combination |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
642 |
with the RepAbs above will let us change the type of the |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
643 |
abstraction with rewriting. |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
644 |
For applications: |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
645 |
* If the term is 'Respects' applied to anything we leave it unchanged |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
646 |
* If the term needs lifting and the head is a constant that we know |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
647 |
how to lift, we put a RepAbs and recurse |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
648 |
* If the term needs lifting and the head is a free applied to subterms |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
649 |
(if it is not applied we treated it in Abs branch) then we |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
650 |
put RepAbs and recurse |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
651 |
* Otherwise just recurse. |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
652 |
*) |
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
653 |
|
336
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
654 |
ML {* |
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
655 |
fun mk_repabs lthy (T, T') trm = |
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
656 |
Quotient_Def.get_fun repF lthy (T, T') |
354
2eb6d527dfe4
addded a tactic, which sets up the three goals of the `algorithm'
Christian Urban <urbanc@in.tum.de>
parents:
353
diff
changeset
|
657 |
$ (Quotient_Def.get_fun absF lthy (T, T') $ trm) |
336
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
658 |
*} |
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
659 |
|
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
660 |
ML {* |
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
661 |
(* bound variables need to be treated properly, *) |
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
662 |
(* as the type of subterms need to be calculated *) |
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
663 |
|
408
1056861b562c
renamed inj_REPABS to inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents:
407
diff
changeset
|
664 |
fun inj_repabs_trm lthy (rtrm, qtrm) = |
336
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
665 |
let |
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
666 |
val rty = fastype_of rtrm |
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
667 |
val qty = fastype_of qtrm |
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
668 |
in |
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
669 |
case (rtrm, qtrm) of |
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
670 |
(Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
408
1056861b562c
renamed inj_REPABS to inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents:
407
diff
changeset
|
671 |
Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
336
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
672 |
| (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => |
408
1056861b562c
renamed inj_REPABS to inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents:
407
diff
changeset
|
673 |
Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
336
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
674 |
| (Const (@{const_name "Babs"}, T) $ r $ t, t') => |
408
1056861b562c
renamed inj_REPABS to inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents:
407
diff
changeset
|
675 |
Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
336
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
676 |
| (Abs (x, T, t), Abs (x', T', t')) => |
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
677 |
let |
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
678 |
val (y, s) = Term.dest_abs (x, T, t) |
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
679 |
val (_, s') = Term.dest_abs (x', T', t') |
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
680 |
val yvar = Free (y, T) |
453
c22ab554a32d
started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de>
parents:
452
diff
changeset
|
681 |
val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s')) |
336
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
682 |
in |
345
573e2b625e8e
a version of inj_REPABS (needs to be looked at again later)
Christian Urban <urbanc@in.tum.de>
parents:
341
diff
changeset
|
683 |
if rty = qty |
573e2b625e8e
a version of inj_REPABS (needs to be looked at again later)
Christian Urban <urbanc@in.tum.de>
parents:
341
diff
changeset
|
684 |
then result |
573e2b625e8e
a version of inj_REPABS (needs to be looked at again later)
Christian Urban <urbanc@in.tum.de>
parents:
341
diff
changeset
|
685 |
else mk_repabs lthy (rty, qty) result |
336
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
686 |
end |
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
687 |
| _ => |
455
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
parents:
453
diff
changeset
|
688 |
let |
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
parents:
453
diff
changeset
|
689 |
val (rhead, rargs) = strip_comb rtrm |
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
parents:
453
diff
changeset
|
690 |
val (qhead, qargs) = strip_comb qtrm |
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
parents:
453
diff
changeset
|
691 |
val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) |
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
parents:
453
diff
changeset
|
692 |
in |
464 | 693 |
case (rhead, qhead) of |
694 |
(Const _, Const _) => |
|
455
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
parents:
453
diff
changeset
|
695 |
if rty = qty |
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
parents:
453
diff
changeset
|
696 |
then list_comb (rhead, rargs') |
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
parents:
453
diff
changeset
|
697 |
else mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) |
464 | 698 |
| (Free (x, T), Free (x', T')) => |
699 |
if T = T' |
|
455
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
parents:
453
diff
changeset
|
700 |
then list_comb (rhead, rargs') |
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
parents:
453
diff
changeset
|
701 |
else list_comb (mk_repabs lthy (T, T') rhead, rargs') |
464 | 702 |
| (Abs _, Abs _) => |
455
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
parents:
453
diff
changeset
|
703 |
list_comb (inj_repabs_trm lthy (rhead, qhead), rargs') |
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
parents:
453
diff
changeset
|
704 |
| _ => raise (LIFT_MATCH "injection") |
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
parents:
453
diff
changeset
|
705 |
end |
336
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
706 |
end |
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
707 |
*} |
e6b6e5ba0cc5
Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
334
diff
changeset
|
708 |
|
404 | 709 |
section {* RepAbs Injection Tactic *} |
387 | 710 |
|
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
502
diff
changeset
|
711 |
(* FIXME/TODO: do not handle everything *) |
387 | 712 |
ML {* |
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents:
420
diff
changeset
|
713 |
fun instantiate_tac thm = |
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents:
420
diff
changeset
|
714 |
Subgoal.FOCUS (fn {concl, ...} => |
387 | 715 |
let |
716 |
val pat = Drule.strip_imp_concl (cprop_of thm) |
|
481
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
480
diff
changeset
|
717 |
val insts = Thm.first_order_match (pat, concl) |
387 | 718 |
in |
719 |
rtac (Drule.instantiate insts thm) 1 |
|
720 |
end |
|
721 |
handle _ => no_tac) |
|
722 |
*} |
|
723 |
||
724 |
ML {* |
|
506
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
505
diff
changeset
|
725 |
fun quotient_tac ctxt = |
468 | 726 |
REPEAT_ALL_NEW (FIRST' |
529 | 727 |
[rtac @{thm IDENTITY_Quotient}, |
510
8dbc521ee97f
Even better: Completely got rid of the simps in both quotient_tac and inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
509
diff
changeset
|
728 |
resolve_tac (quotient_rules_get ctxt)]) |
387 | 729 |
*} |
730 |
||
536
44fa9df44e6f
More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
529
diff
changeset
|
731 |
lemma fun_rel_id: |
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents:
420
diff
changeset
|
732 |
assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents:
420
diff
changeset
|
733 |
shows "(R1 ===> R2) f g" |
466 | 734 |
using a by simp |
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents:
420
diff
changeset
|
735 |
|
480
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
479
diff
changeset
|
736 |
definition |
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
479
diff
changeset
|
737 |
"QUOT_TRUE x \<equiv> True" |
472
cb03d4b3f059
fixed problems with FOCUS
Christian Urban <urbanc@in.tum.de>
parents:
471
diff
changeset
|
738 |
|
387 | 739 |
ML {* |
480
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
479
diff
changeset
|
740 |
fun find_qt_asm asms = |
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
479
diff
changeset
|
741 |
let |
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
479
diff
changeset
|
742 |
fun find_fun trm = |
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
479
diff
changeset
|
743 |
case trm of |
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
479
diff
changeset
|
744 |
(Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true |
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
479
diff
changeset
|
745 |
| _ => false |
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
479
diff
changeset
|
746 |
in |
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
479
diff
changeset
|
747 |
case find_first find_fun asms of |
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
479
diff
changeset
|
748 |
SOME (_ $ (_ $ (f $ a))) => (f, a) |
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
479
diff
changeset
|
749 |
| _ => error "find_qt_asm" |
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
479
diff
changeset
|
750 |
end |
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
479
diff
changeset
|
751 |
*} |
7fbbb2690bc5
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
479
diff
changeset
|
752 |
|
529 | 753 |
(* It proves the Quotient assumptions by calling quotient_tac *) |
517
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
754 |
ML {* |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
755 |
fun solve_quotient_assum i ctxt thm = |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
756 |
let |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
757 |
val tac = |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
758 |
(compose_tac (false, thm, i)) THEN_ALL_NEW |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
759 |
(quotient_tac ctxt); |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
760 |
val gc = Drule.strip_imp_concl (cprop_of thm); |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
761 |
in |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
762 |
Goal.prove_internal [] gc (fn _ => tac 1) |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
763 |
end |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
764 |
handle _ => error "solve_quotient_assum" |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
765 |
*} |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
766 |
|
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
767 |
ML {* |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
768 |
fun solve_quotient_assums ctxt thm = |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
769 |
let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
770 |
thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)] |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
771 |
end |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
772 |
handle _ => error "solve_quotient_assums" |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
773 |
*} |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
774 |
|
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
775 |
ML {* |
527
9b1ad366827f
code cleaning and renaming
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
526
diff
changeset
|
776 |
val apply_rsp_tac = |
517
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
777 |
Subgoal.FOCUS (fn {concl, asms, context,...} => |
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
778 |
case ((HOLogic.dest_Trueprop (term_of concl))) of |
518
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
779 |
((R2 $ (f $ x) $ (g $ y))) => |
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
780 |
let |
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
781 |
val (asmf, asma) = find_qt_asm (map term_of asms); |
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
782 |
in |
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
783 |
if (fastype_of asmf) = (fastype_of f) then no_tac else let |
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
784 |
val ty_a = fastype_of x; |
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
785 |
val ty_b = fastype_of asma; |
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
786 |
val ty_c = range_type (type_of f); |
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
787 |
val thy = ProofContext.theory_of context; |
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
788 |
val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c]; |
527
9b1ad366827f
code cleaning and renaming
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
526
diff
changeset
|
789 |
val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp} |
518
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
790 |
val te = solve_quotient_assums context thm |
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
791 |
val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
792 |
val thm = Drule.instantiate' [] t_inst te |
517
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
793 |
in |
518
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
794 |
compose_tac (false, thm, 2) 1 |
517
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
795 |
end |
518
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
796 |
end |
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
797 |
| _ => no_tac) |
517
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
798 |
*} |
482
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
481
diff
changeset
|
799 |
|
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
481
diff
changeset
|
800 |
ML {* |
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
801 |
fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
802 |
*} |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
803 |
|
398
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
804 |
(* |
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
805 |
To prove that the regularised theorem implies the abs/rep injected, |
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
806 |
we try: |
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
807 |
|
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
808 |
1) theorems 'trans2' from the appropriate QUOT_TYPE |
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
475
diff
changeset
|
809 |
2) remove lambdas from both sides: lambda_rsp_tac |
398
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
810 |
3) remove Ball/Bex from the right hand side |
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
811 |
4) use user-supplied RSP theorems |
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
812 |
5) remove rep_abs from the right side |
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
813 |
6) reflexivity of equality |
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
814 |
7) split applications of lifted type (apply_rsp) |
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
815 |
8) split applications of non-lifted type (cong_tac) |
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
816 |
9) apply extentionality |
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents:
420
diff
changeset
|
817 |
A) reflexivity of the relation |
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents:
420
diff
changeset
|
818 |
B) assumption |
398
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
819 |
(Lambdas under respects may have left us some assumptions) |
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents:
420
diff
changeset
|
820 |
C) proving obvious higher order equalities by simplifying fun_rel |
398
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
821 |
(not sure if it is still needed?) |
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents:
420
diff
changeset
|
822 |
D) unfolding lambda on one side |
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
parents:
420
diff
changeset
|
823 |
E) simplifying (= ===> =) for simpler respectfulness |
398
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
824 |
|
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
825 |
*) |
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
826 |
|
469 | 827 |
lemma quot_true_dests: |
828 |
shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P" |
|
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
475
diff
changeset
|
829 |
and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P" |
469 | 830 |
and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))" |
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
475
diff
changeset
|
831 |
and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)" |
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
475
diff
changeset
|
832 |
apply(simp_all add: QUOT_TRUE_def ext) |
469 | 833 |
done |
834 |
||
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
475
diff
changeset
|
835 |
lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P" |
470
fc16faef5dfa
Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
469
diff
changeset
|
836 |
by (simp add: QUOT_TRUE_def) |
fc16faef5dfa
Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
469
diff
changeset
|
837 |
|
479
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
838 |
lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b" |
470
fc16faef5dfa
Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
469
diff
changeset
|
839 |
by (simp add: QUOT_TRUE_def) |
fc16faef5dfa
Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
469
diff
changeset
|
840 |
|
fc16faef5dfa
Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
469
diff
changeset
|
841 |
ML {* |
479
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
842 |
fun quot_true_conv1 ctxt fnctn ctrm = |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
843 |
case (term_of ctrm) of |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
844 |
(Const (@{const_name QUOT_TRUE}, _) $ x) => |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
845 |
let |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
846 |
val fx = fnctn x; |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
847 |
val thy = ProofContext.theory_of ctxt; |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
848 |
val cx = cterm_of thy x; |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
849 |
val cfx = cterm_of thy fx; |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
850 |
val cxt = ctyp_of thy (fastype_of x); |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
851 |
val cfxt = ctyp_of thy (fastype_of fx); |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
852 |
val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp} |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
853 |
in |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
854 |
Conv.rewr_conv thm ctrm |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
855 |
end |
470
fc16faef5dfa
Transformation of QUOT_TRUE assumption by any given function
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
469
diff
changeset
|
856 |
*} |
469 | 857 |
|
479
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
858 |
ML {* |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
859 |
fun quot_true_conv ctxt fnctn ctrm = |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
860 |
case (term_of ctrm) of |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
861 |
(Const (@{const_name QUOT_TRUE}, _) $ _) => |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
862 |
quot_true_conv1 ctxt fnctn ctrm |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
863 |
| _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
864 |
| Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
865 |
| _ => Conv.all_conv ctrm |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
866 |
*} |
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
867 |
|
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
868 |
ML {* |
493 | 869 |
fun quot_true_tac ctxt fnctn = CONVERSION |
870 |
((Conv.params_conv ~1 (fn ctxt => |
|
871 |
(Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) |
|
479
24799397a3ce
The conversion approach works.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
476
diff
changeset
|
872 |
*} |
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
475
diff
changeset
|
873 |
|
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
475
diff
changeset
|
874 |
ML {* fun dest_comb (f $ a) = (f, a) *} |
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
475
diff
changeset
|
875 |
ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *} |
481
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
480
diff
changeset
|
876 |
(* TODO: Can this be done easier? *) |
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
480
diff
changeset
|
877 |
ML {* |
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
480
diff
changeset
|
878 |
fun unlam t = |
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
480
diff
changeset
|
879 |
case t of |
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
480
diff
changeset
|
880 |
(Abs a) => snd (Term.dest_abs a) |
525
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
881 |
| _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) |
398
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
882 |
*} |
fafcc54e531d
some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de>
parents:
391
diff
changeset
|
883 |
|
522
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
884 |
ML {* |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
885 |
fun dest_fun_type (Type("fun", [T, S])) = (T, S) |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
886 |
| dest_fun_type _ = error "dest_fun_type" |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
887 |
*} |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
888 |
|
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
889 |
ML {* |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
890 |
val rep_abs_rsp_tac = |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
891 |
Subgoal.FOCUS (fn {concl, context, ...} => |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
892 |
case HOLogic.dest_Trueprop (term_of concl) of (rel $ lhs $ (rep $ (abs $ rhs))) => |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
893 |
(let |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
894 |
val thy = ProofContext.theory_of context; |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
895 |
val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
896 |
val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
897 |
val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
898 |
val thm = Drule.instantiate' ty_inst t_inst @{thm REP_ABS_RSP} |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
899 |
val te = solve_quotient_assums context thm |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
900 |
val t_inst = map (SOME o (cterm_of thy)) [lhs, rhs]; |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
901 |
val thm = Drule.instantiate' [] t_inst te |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
902 |
in |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
903 |
compose_tac (false, thm, 1) 1 |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
904 |
end |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
905 |
handle _ => no_tac) |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
906 |
| _ => no_tac) |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
907 |
*} |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
908 |
|
512
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
909 |
ML {* |
525
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
910 |
fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) => |
512
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
911 |
(case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
525
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
912 |
(* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
536
44fa9df44e6f
More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
529
diff
changeset
|
913 |
((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)) |
44fa9df44e6f
More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
529
diff
changeset
|
914 |
=> rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
525
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
915 |
(* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
512
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
916 |
| (Const (@{const_name "op ="},_) $ |
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
917 |
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
918 |
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
919 |
=> rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} |
525
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
920 |
(* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *) |
536
44fa9df44e6f
More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
529
diff
changeset
|
921 |
| (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
512
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
922 |
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
923 |
(Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
536
44fa9df44e6f
More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
529
diff
changeset
|
924 |
=> rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
525
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
925 |
(* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
512
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
926 |
| Const (@{const_name "op ="},_) $ |
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
927 |
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
928 |
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
929 |
=> rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} |
525
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
930 |
(* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *) |
536
44fa9df44e6f
More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
529
diff
changeset
|
931 |
| (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
512
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
932 |
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
933 |
(Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
536
44fa9df44e6f
More code cleaning and name changes
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
529
diff
changeset
|
934 |
=> rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
512
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
935 |
| Const (@{const_name "op ="},_) $ _ $ _ => |
525
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
936 |
(* reflexivity of operators arising from Cong_tac *) |
512
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
937 |
rtac @{thm refl} ORELSE' |
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
938 |
(resolve_tac trans2 THEN' RANGE [ |
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
939 |
quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) |
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
940 |
| _ $ _ $ _ => |
525
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
941 |
(* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
942 |
(* observe ---> *) |
522
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
943 |
rep_abs_rsp_tac ctxt |
6b77cfd508e9
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
519
diff
changeset
|
944 |
| _ => error "inj_repabs_tac not a relation" |
512
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
945 |
) i) |
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
946 |
*} |
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
947 |
|
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
948 |
ML {* |
525
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
949 |
fun inj_repabs_tac ctxt rel_refl trans2 = |
512
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
950 |
(FIRST' [ |
525
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
951 |
inj_repabs_tac_match ctxt trans2, |
527
9b1ad366827f
code cleaning and renaming
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
526
diff
changeset
|
952 |
(* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp provided type of t needs lifting *) |
9b1ad366827f
code cleaning and renaming
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
526
diff
changeset
|
953 |
NDT ctxt "A" (apply_rsp_tac ctxt THEN' |
517
ede7f9622a54
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
516
diff
changeset
|
954 |
(RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
525
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
955 |
(* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
956 |
(* merge with previous tactic *) |
512
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
957 |
NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' |
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
958 |
(RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
525
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
959 |
(* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
512
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
960 |
NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), |
525
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
961 |
(* resolving with R x y assumptions *) |
512
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
962 |
NDT ctxt "E" (atac), |
525
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
963 |
(* reflexivity of the basic relations *) |
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
964 |
(* R \<dots> \<dots> *) |
512
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
965 |
NDT ctxt "D" (resolve_tac rel_refl), |
525
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
966 |
(* respectfulness of constants *) |
515
b00a9b58264d
Fixes after big merge.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
514
diff
changeset
|
967 |
NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)) |
b00a9b58264d
Fixes after big merge.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
514
diff
changeset
|
968 |
]) |
512
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
969 |
*} |
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
970 |
|
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
971 |
ML {* |
525
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
972 |
fun all_inj_repabs_tac ctxt rel_refl trans2 = |
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
973 |
REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2) |
512
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
974 |
*} |
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
975 |
|
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
976 |
|
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
505
diff
changeset
|
977 |
|
399 | 978 |
section {* Cleaning of the theorem *} |
387 | 979 |
|
980 |
ML {* |
|
440
0af649448a11
Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
436
diff
changeset
|
981 |
fun make_inst lhs t = |
0af649448a11
Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
436
diff
changeset
|
982 |
let |
0af649448a11
Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
436
diff
changeset
|
983 |
val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
0af649448a11
Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
436
diff
changeset
|
984 |
val _ $ (Abs (_, _, g)) = t; |
0af649448a11
Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
436
diff
changeset
|
985 |
fun mk_abs i t = |
0af649448a11
Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
436
diff
changeset
|
986 |
if incr_boundvars i u aconv t then Bound i |
0af649448a11
Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
436
diff
changeset
|
987 |
else (case t of |
0af649448a11
Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
436
diff
changeset
|
988 |
t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
469 | 989 |
| Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t') |
440
0af649448a11
Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
436
diff
changeset
|
990 |
| Bound j => if i = j then error "make_inst" else t |
0af649448a11
Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
436
diff
changeset
|
991 |
| _ => t); |
0af649448a11
Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
436
diff
changeset
|
992 |
in (f, Abs ("x", T, mk_abs 0 g)) end; |
490
5214ec75add4
simplified lambda_prs_conv
Christian Urban <urbanc@in.tum.de>
parents:
489
diff
changeset
|
993 |
*} |
440
0af649448a11
Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
436
diff
changeset
|
994 |
|
492
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
995 |
ML {* |
506
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
505
diff
changeset
|
996 |
fun lambda_allex_prs_simple_conv ctxt ctrm = |
492
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
997 |
case (term_of ctrm) of |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
998 |
((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
387 | 999 |
let |
518
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
1000 |
val (ty_b, ty_a) = dest_fun_type (fastype_of r1); |
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
1001 |
val (ty_c, ty_d) = dest_fun_type (fastype_of a2); |
387 | 1002 |
val thy = ProofContext.theory_of ctxt; |
518
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
1003 |
val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
387 | 1004 |
val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
527
9b1ad366827f
code cleaning and renaming
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
526
diff
changeset
|
1005 |
val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}; |
518
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
1006 |
val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
415
5a9bdf81672d
More cleaning in QuotMain, identity handling.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
413
diff
changeset
|
1007 |
val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
440
0af649448a11
Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
436
diff
changeset
|
1008 |
val tl = Thm.lhs_of ts; |
0af649448a11
Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
436
diff
changeset
|
1009 |
val (insp, inst) = make_inst (term_of tl) (term_of ctrm); |
0af649448a11
Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
436
diff
changeset
|
1010 |
val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; |
492
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1011 |
in |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1012 |
Conv.rewr_conv ti ctrm |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1013 |
end |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1014 |
| (Const (@{const_name Ball}, _) $ (Const (@{const_name Respects}, _) $ R) $ |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1015 |
(((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) => |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1016 |
let |
518
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
1017 |
val (ty_a, ty_b) = dest_fun_type (fastype_of absf); |
492
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1018 |
val thy = ProofContext.theory_of ctxt; |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1019 |
val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b); |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1020 |
val tyinst = [SOME cty_a, SOME cty_b]; |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1021 |
val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1022 |
val thm = Drule.instantiate' tyinst tinst @{thm all_prs}; |
518
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
1023 |
val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm]; |
492
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1024 |
in |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1025 |
Conv.rewr_conv ti ctrm |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1026 |
end |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1027 |
| (Const (@{const_name Bex}, _) $ (Const (@{const_name Respects}, _) $ R) $ |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1028 |
(((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) => |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1029 |
let |
518
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
1030 |
val (ty_a, ty_b) = dest_fun_type (fastype_of absf); |
492
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1031 |
val thy = ProofContext.theory_of ctxt; |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1032 |
val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b); |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1033 |
val tyinst = [SOME cty_a, SOME cty_b]; |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1034 |
val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; |
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1035 |
val thm = Drule.instantiate' tyinst tinst @{thm ex_prs}; |
518
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
1036 |
val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm]; |
387 | 1037 |
in |
1038 |
Conv.rewr_conv ti ctrm |
|
1039 |
end |
|
490
5214ec75add4
simplified lambda_prs_conv
Christian Urban <urbanc@in.tum.de>
parents:
489
diff
changeset
|
1040 |
| _ => Conv.all_conv ctrm |
387 | 1041 |
*} |
1042 |
||
1043 |
ML {* |
|
506
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
505
diff
changeset
|
1044 |
val lambda_allex_prs_conv = |
518
14f68c1f4d12
compose_tac instead of rtac to avoid unification; some code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
517
diff
changeset
|
1045 |
More_Conv.top_conv lambda_allex_prs_simple_conv |
387 | 1046 |
*} |
1047 |
||
1048 |
ML {* |
|
506
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
505
diff
changeset
|
1049 |
fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt) |
387 | 1050 |
*} |
1051 |
||
457 | 1052 |
(* |
465 | 1053 |
Cleaning the theorem consists of 6 kinds of rewrites. |
1054 |
The first two need to be done before fun_map is unfolded |
|
457 | 1055 |
|
527
9b1ad366827f
code cleaning and renaming
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
526
diff
changeset
|
1056 |
- lambda_prs: |
469 | 1057 |
(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f |
1058 |
||
527
9b1ad366827f
code cleaning and renaming
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
526
diff
changeset
|
1059 |
- all_prs (and the same for exists: ex_prs) |
469 | 1060 |
\<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f |
1061 |
||
457 | 1062 |
- Rewriting with definitions from the argument defs |
469 | 1063 |
NewConst ----> (rep ---> abs) oldConst |
1064 |
||
529 | 1065 |
- Quotient_REL_REP: |
469 | 1066 |
Rel (Rep x) (Rep y) ----> x = y |
1067 |
||
465 | 1068 |
- ABS_REP |
469 | 1069 |
Abs (Rep x) ----> x |
1070 |
||
465 | 1071 |
- id_simps; fun_map.simps |
457 | 1072 |
|
1073 |
The first one is implemented as a conversion (fast). |
|
465 | 1074 |
The second one is an EqSubst (slow). |
1075 |
The rest are a simp_tac and are fast. |
|
457 | 1076 |
*) |
469 | 1077 |
|
387 | 1078 |
ML {* |
506
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
505
diff
changeset
|
1079 |
fun clean_tac lthy = |
387 | 1080 |
let |
498
e7bb6bbe7576
defs used automatically by clean_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
495
diff
changeset
|
1081 |
val thy = ProofContext.theory_of lthy; |
506
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
505
diff
changeset
|
1082 |
val quotients = quotient_rules_get lthy |
501
375e28eedee7
Reintroduced varifyT; we still need it for permutation definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
499
diff
changeset
|
1083 |
val defs = map (Thm.varifyT o #def) (qconsts_dest thy); |
529 | 1084 |
val absrep = map (fn x => @{thm Quotient_ABS_REP} OF [x]) quotients |
462
0911d3aabf47
clean_tac rewrites the definitions the other way
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
459
diff
changeset
|
1085 |
val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; |
529 | 1086 |
val reps_same = map (fn x => @{thm Quotient_REL_REP} OF [x]) quotients |
440
0af649448a11
Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
436
diff
changeset
|
1087 |
val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
462
0911d3aabf47
clean_tac rewrites the definitions the other way
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
459
diff
changeset
|
1088 |
val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps |
0911d3aabf47
clean_tac rewrites the definitions the other way
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
459
diff
changeset
|
1089 |
(@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs) |
387 | 1090 |
in |
490
5214ec75add4
simplified lambda_prs_conv
Christian Urban <urbanc@in.tum.de>
parents:
489
diff
changeset
|
1091 |
EVERY' [ |
5214ec75add4
simplified lambda_prs_conv
Christian Urban <urbanc@in.tum.de>
parents:
489
diff
changeset
|
1092 |
(* (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f *) |
492
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1093 |
(* \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f *) |
506
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
505
diff
changeset
|
1094 |
NDT lthy "a" (TRY o lambda_allex_prs_tac lthy), |
490
5214ec75add4
simplified lambda_prs_conv
Christian Urban <urbanc@in.tum.de>
parents:
489
diff
changeset
|
1095 |
|
5214ec75add4
simplified lambda_prs_conv
Christian Urban <urbanc@in.tum.de>
parents:
489
diff
changeset
|
1096 |
(* NewConst ----> (rep ---> abs) oldConst *) |
5214ec75add4
simplified lambda_prs_conv
Christian Urban <urbanc@in.tum.de>
parents:
489
diff
changeset
|
1097 |
(* Abs (Rep x) ----> x *) |
5214ec75add4
simplified lambda_prs_conv
Christian Urban <urbanc@in.tum.de>
parents:
489
diff
changeset
|
1098 |
(* id_simps; fun_map.simps *) |
492
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1099 |
NDT lthy "c" (TRY o simp_tac simp_ctxt), |
490
5214ec75add4
simplified lambda_prs_conv
Christian Urban <urbanc@in.tum.de>
parents:
489
diff
changeset
|
1100 |
|
5214ec75add4
simplified lambda_prs_conv
Christian Urban <urbanc@in.tum.de>
parents:
489
diff
changeset
|
1101 |
(* final step *) |
492
6793659d38d6
Included all_prs and ex_prs in the lambda_prs conversion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
491
diff
changeset
|
1102 |
NDT lthy "d" (TRY o rtac refl) |
490
5214ec75add4
simplified lambda_prs_conv
Christian Urban <urbanc@in.tum.de>
parents:
489
diff
changeset
|
1103 |
] |
387 | 1104 |
end |
1105 |
*} |
|
381
991db758a72d
More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
379
diff
changeset
|
1106 |
|
404 | 1107 |
section {* Genralisation of free variables in a goal *} |
347
7e82493c6253
Finished temporary goal-directed lift_theorem wrapper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
346
diff
changeset
|
1108 |
|
7e82493c6253
Finished temporary goal-directed lift_theorem wrapper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
346
diff
changeset
|
1109 |
ML {* |
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1110 |
fun inst_spec ctrm = |
411
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
parents:
410
diff
changeset
|
1111 |
Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} |
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1112 |
|
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1113 |
fun inst_spec_tac ctrms = |
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1114 |
EVERY' (map (dtac o inst_spec) ctrms) |
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1115 |
|
412 | 1116 |
fun all_list xs trm = |
411
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
parents:
410
diff
changeset
|
1117 |
fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm |
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
parents:
410
diff
changeset
|
1118 |
|
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
parents:
410
diff
changeset
|
1119 |
fun apply_under_Trueprop f = |
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
parents:
410
diff
changeset
|
1120 |
HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop |
362 | 1121 |
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1122 |
fun gen_frees_tac ctxt = |
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1123 |
SUBGOAL (fn (concl, i) => |
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1124 |
let |
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1125 |
val thy = ProofContext.theory_of ctxt |
411
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
parents:
410
diff
changeset
|
1126 |
val vrs = Term.add_frees concl [] |
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1127 |
val cvrs = map (cterm_of thy o Free) vrs |
412 | 1128 |
val concl' = apply_under_Trueprop (all_list vrs) concl |
411
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
parents:
410
diff
changeset
|
1129 |
val goal = Logic.mk_implies (concl', concl) |
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1130 |
val rule = Goal.prove ctxt [] [] goal |
411
c10e314761fa
simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de>
parents:
410
diff
changeset
|
1131 |
(K (EVERY1 [inst_spec_tac (rev cvrs), atac])) |
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1132 |
in |
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1133 |
rtac rule i |
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1134 |
end) |
362 | 1135 |
*} |
1136 |
||
402
dd64cca9265c
recommited changes of comments
Christian Urban <urbanc@in.tum.de>
parents:
401
diff
changeset
|
1137 |
section {* General outline of the lifting procedure *} |
dd64cca9265c
recommited changes of comments
Christian Urban <urbanc@in.tum.de>
parents:
401
diff
changeset
|
1138 |
|
383
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
1139 |
(* - A is the original raw theorem *) |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
1140 |
(* - B is the regularized theorem *) |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
1141 |
(* - C is the rep/abs injected version of B *) |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
1142 |
(* - D is the lifted theorem *) |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
1143 |
(* *) |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
1144 |
(* - b is the regularization step *) |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
1145 |
(* - c is the rep/abs injection step *) |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
1146 |
(* - d is the cleaning part *) |
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
1147 |
|
413 | 1148 |
lemma lifting_procedure: |
360
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1149 |
assumes a: "A" |
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1150 |
and b: "A \<Longrightarrow> B" |
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1151 |
and c: "B = C" |
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1152 |
and d: "C = D" |
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1153 |
shows "D" |
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1154 |
using a b c d |
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1155 |
by simp |
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1156 |
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1157 |
ML {* |
412 | 1158 |
fun lift_match_error ctxt fun_str rtrm qtrm = |
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1159 |
let |
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1160 |
val rtrm_str = Syntax.string_of_term ctxt rtrm |
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1161 |
val qtrm_str = Syntax.string_of_term ctxt qtrm |
388 | 1162 |
val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str, |
1163 |
"and the lifted theorem\n", rtrm_str, "do not match"] |
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1164 |
in |
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1165 |
error (space_implode " " msg) |
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1166 |
end |
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1167 |
*} |
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1168 |
|
360
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1169 |
ML {* |
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1170 |
fun procedure_inst ctxt rtrm qtrm = |
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1171 |
let |
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1172 |
val thy = ProofContext.theory_of ctxt |
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1173 |
val rtrm' = HOLogic.dest_Trueprop rtrm |
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1174 |
val qtrm' = HOLogic.dest_Trueprop qtrm |
383
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
1175 |
val reg_goal = |
405
8bc7428745ad
renamed REGULARIZE to be regularize
Christian Urban <urbanc@in.tum.de>
parents:
404
diff
changeset
|
1176 |
Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') |
412 | 1177 |
handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
383
73a3670fb00e
comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de>
parents:
382
diff
changeset
|
1178 |
val inj_goal = |
408
1056861b562c
renamed inj_REPABS to inj_repabs_trm
Christian Urban <urbanc@in.tum.de>
parents:
407
diff
changeset
|
1179 |
Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) |
412 | 1180 |
handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
360
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1181 |
in |
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1182 |
Drule.instantiate' [] |
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1183 |
[SOME (cterm_of thy rtrm'), |
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1184 |
SOME (cterm_of thy reg_goal), |
413 | 1185 |
SOME (cterm_of thy inj_goal)] @{thm lifting_procedure} |
360
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1186 |
end |
362 | 1187 |
*} |
389 | 1188 |
|
1189 |
(* Left for debugging *) |
|
362 | 1190 |
ML {* |
389 | 1191 |
fun procedure_tac lthy rthm = |
1192 |
ObjectLogic.full_atomize_tac |
|
1193 |
THEN' gen_frees_tac lthy |
|
374
980fdf92a834
fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de>
parents:
372
diff
changeset
|
1194 |
THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
389 | 1195 |
let |
1196 |
val rthm' = atomize_thm rthm |
|
1197 |
val rule = procedure_inst context (prop_of rthm') (term_of concl) |
|
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
475
diff
changeset
|
1198 |
val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i} |
389 | 1199 |
in |
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
475
diff
changeset
|
1200 |
EVERY1 [rtac rule, rtac rthm'] THEN RANGE [(fn _ => all_tac), rtac thm] 1 |
412 | 1201 |
end) lthy |
360
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1202 |
*} |
07fb696efa3d
Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
359
diff
changeset
|
1203 |
|
361 | 1204 |
ML {* |
413 | 1205 |
(* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
489
2b7b349e470f
deleted now obsolete argument rty everywhere
Christian Urban <urbanc@in.tum.de>
parents:
488
diff
changeset
|
1206 |
|
506
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
505
diff
changeset
|
1207 |
fun lift_tac lthy rthm rel_eqv = |
389 | 1208 |
ObjectLogic.full_atomize_tac |
1209 |
THEN' gen_frees_tac lthy |
|
1210 |
THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
|
1211 |
let |
|
1212 |
val rthm' = atomize_thm rthm |
|
1213 |
val rule = procedure_inst context (prop_of rthm') (term_of concl) |
|
529 | 1214 |
val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) rel_eqv |
519
ebfd747b47ab
Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
518
diff
changeset
|
1215 |
val quotients = quotient_rules_get lthy |
527
9b1ad366827f
code cleaning and renaming
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
526
diff
changeset
|
1216 |
val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients |
476
325d6e9a7515
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
475
diff
changeset
|
1217 |
val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i} |
389 | 1218 |
in |
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
1219 |
EVERY1 |
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
1220 |
[rtac rule, |
413 | 1221 |
RANGE [rtac rthm', |
432
9c33c0809733
Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
427
diff
changeset
|
1222 |
regularize_tac lthy rel_eqv, |
525
3f657c4fbefa
Removed previous inj_repabs_tac
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
523
diff
changeset
|
1223 |
rtac thm THEN' all_inj_repabs_tac lthy rel_refl trans2, |
506
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
505
diff
changeset
|
1224 |
clean_tac lthy]] |
412 | 1225 |
end) lthy |
361 | 1226 |
*} |
1227 |
||
198
ff4425e000db
Completely cleaned Int.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
197
diff
changeset
|
1228 |
end |
239
02b14a21761a
Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
236
diff
changeset
|
1229 |