author | wenzelm |
Wed, 22 Apr 2020 19:22:43 +0200 | |
changeset 71787 | acfe72ff00c2 |
parent 71773 | 7c2f4dd48fb6 |
child 71886 | 4f4695757980 |
permissions | -rw-r--r-- |
35762 | 1 |
(* Title: Provers/quantifier1.ML |
4319 | 2 |
Author: Tobias Nipkow |
3 |
Copyright 1997 TU Munich |
|
4 |
||
5 |
Simplification procedures for turning |
|
6 |
||
7 |
? x. ... & x = t & ... |
|
8 |
into ? x. x = t & ... & ... |
|
11232 | 9 |
where the `? x. x = t &' in the latter formula must be eliminated |
42458 | 10 |
by ordinary simplification. |
4319 | 11 |
|
12 |
and ! x. (... & x = t & ...) --> P x |
|
13 |
into ! x. x = t --> (... & ...) --> P x |
|
14 |
where the `!x. x=t -->' in the latter formula is eliminated |
|
15 |
by ordinary simplification. |
|
16 |
||
11232 | 17 |
And analogously for t=x, but the eqn is not turned around! |
18 |
||
4319 | 19 |
NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)"; |
38456 | 20 |
"!x. x=t --> P(x)" is covered by the congruence rule for -->; |
4319 | 21 |
"!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule. |
11232 | 22 |
As must be "? x. t=x & P(x)". |
42458 | 23 |
|
11221 | 24 |
And similarly for the bounded quantifiers. |
25 |
||
4319 | 26 |
Gries etc call this the "1 point rules" |
31166
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
20049
diff
changeset
|
27 |
|
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
20049
diff
changeset
|
28 |
The above also works for !x1..xn. and ?x1..xn by moving the defined |
38456 | 29 |
quantifier inside first, but not for nested bounded quantifiers. |
31166
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
20049
diff
changeset
|
30 |
|
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
20049
diff
changeset
|
31 |
For set comprehensions the basic permutations |
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
20049
diff
changeset
|
32 |
... & x = t & ... -> x = t & (... & ...) |
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
20049
diff
changeset
|
33 |
... & t = x & ... -> t = x & (... & ...) |
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
20049
diff
changeset
|
34 |
are also exported. |
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
20049
diff
changeset
|
35 |
|
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
20049
diff
changeset
|
36 |
To avoid looping, NONE is returned if the term cannot be rearranged, |
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
20049
diff
changeset
|
37 |
esp if x=t/t=x sits at the front already. |
4319 | 38 |
*) |
39 |
||
40 |
signature QUANTIFIER1_DATA = |
|
41 |
sig |
|
42 |
(*abstract syntax*) |
|
42460 | 43 |
val dest_eq: term -> (term * term) option |
44 |
val dest_conj: term -> (term * term) option |
|
45 |
val dest_imp: term -> (term * term) option |
|
4319 | 46 |
val conj: term |
42458 | 47 |
val imp: term |
4319 | 48 |
(*rules*) |
49 |
val iff_reflection: thm (* P <-> Q ==> P == Q *) |
|
42458 | 50 |
val iffI: thm |
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset
|
51 |
val iff_trans: thm |
4319 | 52 |
val conjI: thm |
53 |
val conjE: thm |
|
42458 | 54 |
val impI: thm |
55 |
val mp: thm |
|
56 |
val exI: thm |
|
57 |
val exE: thm |
|
11232 | 58 |
val uncurry: thm (* P --> Q --> R ==> P & Q --> R *) |
59 |
val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *) |
|
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset
|
60 |
val iff_exI: thm (* !!x. P x <-> Q x ==> (? x. P x) = (? x. Q x) *) |
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset
|
61 |
val all_comm: thm (* (!x y. P x y) = (!y x. P x y) *) |
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset
|
62 |
val ex_comm: thm (* (? x y. P x y) = (? y x. P x y) *) |
4319 | 63 |
end; |
64 |
||
65 |
signature QUANTIFIER1 = |
|
66 |
sig |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
67 |
val prove_one_point_all_tac: Proof.context -> tactic |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
68 |
val prove_one_point_ex_tac: Proof.context -> tactic |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42460
diff
changeset
|
69 |
val rearrange_all: Proof.context -> cterm -> thm option |
71512
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
70 |
val rearrange_All: Proof.context -> cterm -> thm option |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42460
diff
changeset
|
71 |
val rearrange_ex: Proof.context -> cterm -> thm option |
54998 | 72 |
val rearrange_ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option |
73 |
val rearrange_bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option |
|
74 |
val rearrange_Collect: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option |
|
4319 | 75 |
end; |
76 |
||
42458 | 77 |
functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 = |
4319 | 78 |
struct |
79 |
||
11232 | 80 |
(* FIXME: only test! *) |
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset
|
81 |
fun def xs eq = |
42457 | 82 |
(case Data.dest_eq eq of |
42460 | 83 |
SOME (s, t) => |
42458 | 84 |
let val n = length xs in |
85 |
s = Bound n andalso not (loose_bvar1 (t, n)) orelse |
|
86 |
t = Bound n andalso not (loose_bvar1 (s, n)) |
|
87 |
end |
|
88 |
| NONE => false); |
|
4319 | 89 |
|
42458 | 90 |
fun extract_conj fst xs t = |
91 |
(case Data.dest_conj t of |
|
92 |
NONE => NONE |
|
42460 | 93 |
| SOME (P, Q) => |
42458 | 94 |
if def xs P then (if fst then NONE else SOME (xs, P, Q)) |
95 |
else if def xs Q then SOME (xs, Q, P) |
|
96 |
else |
|
97 |
(case extract_conj false xs P of |
|
98 |
SOME (xs, eq, P') => SOME (xs, eq, Data.conj $ P' $ Q) |
|
99 |
| NONE => |
|
100 |
(case extract_conj false xs Q of |
|
101 |
SOME (xs, eq, Q') => SOME (xs, eq, Data.conj $ P $ Q') |
|
102 |
| NONE => NONE))); |
|
11232 | 103 |
|
42458 | 104 |
fun extract_imp fst xs t = |
105 |
(case Data.dest_imp t of |
|
106 |
NONE => NONE |
|
42460 | 107 |
| SOME (P, Q) => |
42458 | 108 |
if def xs P then (if fst then NONE else SOME (xs, P, Q)) |
109 |
else |
|
110 |
(case extract_conj false xs P of |
|
111 |
SOME (xs, eq, P') => SOME (xs, eq, Data.imp $ P' $ Q) |
|
112 |
| NONE => |
|
113 |
(case extract_imp false xs Q of |
|
114 |
NONE => NONE |
|
115 |
| SOME (xs, eq, Q') => SOME (xs, eq, Data.imp $ P $ Q')))); |
|
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset
|
116 |
|
71512
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
117 |
fun extract_conj_from_judgment ctxt fst xs t = |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
118 |
if Object_Logic.is_judgment ctxt t |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
119 |
then |
71773 | 120 |
let |
121 |
val judg $ t' = t |
|
122 |
in |
|
123 |
case extract_conj fst xs t' of |
|
124 |
NONE => NONE |
|
125 |
| SOME (xs, eq, P) => SOME (xs, judg $ eq, judg $ P) |
|
126 |
end |
|
71512
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
127 |
else NONE; |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
128 |
|
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
129 |
fun extract_implies ctxt fst xs t = |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
130 |
(case try Logic.dest_implies t of |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
131 |
NONE => NONE |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
132 |
| SOME (P, Q) => |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
133 |
if def xs P then (if fst then NONE else SOME (xs, P, Q)) |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
134 |
else |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
135 |
(case extract_conj_from_judgment ctxt false xs P of |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
136 |
SOME (xs, eq, P') => SOME (xs, eq, Logic.implies $ P' $ Q) |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
137 |
| NONE => |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
138 |
(case extract_implies ctxt false xs Q of |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
139 |
NONE => NONE |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
140 |
| SOME (xs, eq, Q') => (SOME (xs, eq, Logic.implies $ P $ Q'))))); |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
141 |
|
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
142 |
fun extract_quant ctxt extract q = |
42458 | 143 |
let |
42460 | 144 |
fun exqu xs ((qC as Const (qa, _)) $ Abs (x, T, Q)) = |
42458 | 145 |
if qa = q then exqu ((qC, x, T) :: xs) Q else NONE |
71512
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
146 |
| exqu xs P = extract ctxt (null xs) xs P |
31166
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
20049
diff
changeset
|
147 |
in exqu [] end; |
4319 | 148 |
|
71512
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
149 |
fun iff_reflection_tac ctxt = |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
150 |
resolve_tac ctxt [Data.iff_reflection] 1; |
4319 | 151 |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
152 |
fun qcomm_tac ctxt qcomm qI i = |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
153 |
REPEAT_DETERM (resolve_tac ctxt [qcomm] i THEN resolve_tac ctxt [qI] i); |
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset
|
154 |
|
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset
|
155 |
(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...) |
11221 | 156 |
Better: instantiate exI |
157 |
*) |
|
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset
|
158 |
local |
42458 | 159 |
val excomm = Data.ex_comm RS Data.iff_trans; |
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset
|
160 |
in |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
161 |
fun prove_one_point_ex_tac ctxt = |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
162 |
qcomm_tac ctxt excomm Data.iff_exI 1 THEN resolve_tac ctxt [Data.iffI] 1 THEN |
42458 | 163 |
ALLGOALS |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
164 |
(EVERY' [eresolve_tac ctxt [Data.exE], REPEAT_DETERM o eresolve_tac ctxt [Data.conjE], |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
165 |
resolve_tac ctxt [Data.exI], |
60774 | 166 |
DEPTH_SOLVE_1 o ares_tac ctxt [Data.conjI]]) |
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset
|
167 |
end; |
11221 | 168 |
|
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset
|
169 |
(* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) = |
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset
|
170 |
(! x1..xn x0. x0 = t --> (... & ...) --> P x0) |
11221 | 171 |
*) |
11232 | 172 |
local |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
173 |
fun tac ctxt = |
42458 | 174 |
SELECT_GOAL |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
175 |
(EVERY1 [REPEAT o dresolve_tac ctxt [Data.uncurry], |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
176 |
REPEAT o resolve_tac ctxt [Data.impI], |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
177 |
eresolve_tac ctxt [Data.mp], |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
178 |
REPEAT o eresolve_tac ctxt [Data.conjE], |
60774 | 179 |
REPEAT o ares_tac ctxt [Data.conjI]]); |
71512
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
180 |
val all_comm = Data.all_comm RS Data.iff_trans; |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
181 |
val All_comm = @{thm swap_params [THEN transitive]}; |
11232 | 182 |
in |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
183 |
fun prove_one_point_all_tac ctxt = |
71512
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
184 |
EVERY1 [qcomm_tac ctxt all_comm Data.iff_allI, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
185 |
resolve_tac ctxt [Data.iff_allI], |
71512
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
186 |
resolve_tac ctxt [Data.iffI], |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
187 |
tac ctxt, |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
188 |
tac ctxt]; |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
189 |
fun prove_one_point_All_tac ctxt = |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
190 |
EVERY1 [qcomm_tac ctxt All_comm @{thm equal_allI}, |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
191 |
resolve_tac ctxt [@{thm equal_allI}], |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
192 |
resolve_tac ctxt [@{thm equal_intr_rule}], |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
193 |
Object_Logic.atomize_prems_tac ctxt, |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
194 |
tac ctxt, |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
195 |
Object_Logic.atomize_prems_tac ctxt, |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
196 |
tac ctxt]; |
11232 | 197 |
end |
4319 | 198 |
|
71512
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
199 |
fun prove_conv ctxt tu tac = |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
200 |
let |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
201 |
val (goal, ctxt') = |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
202 |
yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt; |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
203 |
val thm = |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
204 |
Goal.prove ctxt' [] [] goal |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
205 |
(fn {context = ctxt'', ...} => tac ctxt''); |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
206 |
in singleton (Variable.export ctxt' ctxt) thm end; |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
207 |
|
42458 | 208 |
fun renumber l u (Bound i) = |
209 |
Bound (if i < l orelse i > u then i else if i = u then l else i + 1) |
|
210 |
| renumber l u (s $ t) = renumber l u s $ renumber l u t |
|
211 |
| renumber l u (Abs (x, T, t)) = Abs (x, T, renumber (l + 1) (u + 1) t) |
|
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset
|
212 |
| renumber _ _ atom = atom; |
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset
|
213 |
|
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset
|
214 |
fun quantify qC x T xs P = |
42458 | 215 |
let |
216 |
fun quant [] P = P |
|
217 |
| quant ((qC, x, T) :: xs) P = quant xs (qC $ Abs (x, T, P)); |
|
218 |
val n = length xs; |
|
219 |
val Q = if n = 0 then P else renumber 0 n P; |
|
220 |
in quant xs (qC $ Abs (x, T, Q)) end; |
|
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset
|
221 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42460
diff
changeset
|
222 |
fun rearrange_all ctxt ct = |
59582 | 223 |
(case Thm.term_of ct of |
42459 | 224 |
F as (all as Const (q, _)) $ Abs (x, T, P) => |
71512
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
225 |
(case extract_quant ctxt (K extract_imp) q P of |
15531 | 226 |
NONE => NONE |
42458 | 227 |
| SOME (xs, eq, Q) => |
42457 | 228 |
let val R = quantify all x T xs (Data.imp $ eq $ Q) |
71512
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
229 |
in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_all_tac)) end) |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
230 |
| _ => NONE); |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
231 |
|
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
232 |
fun rearrange_All ctxt ct = |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
233 |
(case Thm.term_of ct of |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
234 |
F as (all as Const (q, _)) $ Abs (x, T, P) => |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
235 |
(case extract_quant ctxt extract_implies q P of |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
236 |
NONE => NONE |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
237 |
| SOME (xs, eq, Q) => |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
238 |
let val R = quantify all x T xs (Logic.implies $ eq $ Q) |
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
239 |
in SOME (prove_conv ctxt (F, R) prove_one_point_All_tac) end) |
42459 | 240 |
| _ => NONE); |
4319 | 241 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42460
diff
changeset
|
242 |
fun rearrange_ball tac ctxt ct = |
59582 | 243 |
(case Thm.term_of ct of |
42459 | 244 |
F as Ball $ A $ Abs (x, T, P) => |
42458 | 245 |
(case extract_imp true [] P of |
15531 | 246 |
NONE => NONE |
42458 | 247 |
| SOME (xs, eq, Q) => |
248 |
if not (null xs) then NONE |
|
249 |
else |
|
250 |
let val R = Data.imp $ eq $ Q |
|
71512
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
251 |
in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R)) (iff_reflection_tac THEN' tac)) end) |
42459 | 252 |
| _ => NONE); |
4319 | 253 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42460
diff
changeset
|
254 |
fun rearrange_ex ctxt ct = |
59582 | 255 |
(case Thm.term_of ct of |
42459 | 256 |
F as (ex as Const (q, _)) $ Abs (x, T, P) => |
71512
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
257 |
(case extract_quant ctxt (K extract_conj) q P of |
15531 | 258 |
NONE => NONE |
42458 | 259 |
| SOME (xs, eq, Q) => |
42457 | 260 |
let val R = quantify ex x T xs (Data.conj $ eq $ Q) |
71512
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
261 |
in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_ex_tac)) end) |
42459 | 262 |
| _ => NONE); |
4319 | 263 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42460
diff
changeset
|
264 |
fun rearrange_bex tac ctxt ct = |
59582 | 265 |
(case Thm.term_of ct of |
42459 | 266 |
F as Bex $ A $ Abs (x, T, P) => |
42458 | 267 |
(case extract_conj true [] P of |
15531 | 268 |
NONE => NONE |
42458 | 269 |
| SOME (xs, eq, Q) => |
270 |
if not (null xs) then NONE |
|
71512
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
271 |
else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) (iff_reflection_tac THEN' tac))) |
42459 | 272 |
| _ => NONE); |
11221 | 273 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42460
diff
changeset
|
274 |
fun rearrange_Collect tac ctxt ct = |
59582 | 275 |
(case Thm.term_of ct of |
42459 | 276 |
F as Collect $ Abs (x, T, P) => |
42458 | 277 |
(case extract_conj true [] P of |
31166
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
20049
diff
changeset
|
278 |
NONE => NONE |
42458 | 279 |
| SOME (_, eq, Q) => |
280 |
let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q) |
|
71512
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath meta-all
haftmann
parents:
60774
diff
changeset
|
281 |
in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' tac)) end) |
42459 | 282 |
| _ => NONE); |
31166
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
20049
diff
changeset
|
283 |
|
4319 | 284 |
end; |
42460 | 285 |