author  haftmann 
Sat, 30 May 2020 11:48:28 +0000  
changeset 72142  3956d85e8e81 
parent 72112  4f4695757980 
child 72143  435cdc772110 
permissions  rwrr 
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 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42460
diff
changeset

67 
val rearrange_all: Proof.context > cterm > thm option 
71726
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

68 
val rearrange_All: Proof.context > cterm > thm option 
72112  69 
val rearrange_Ball: (Proof.context > tactic) > Proof.context > cterm > thm option 
70 
val rearrange_Ex: Proof.context > cterm > thm option 

71 
val rearrange_Bex: (Proof.context > tactic) > Proof.context > cterm > thm option 

54998  72 
val rearrange_Collect: (Proof.context > tactic) > Proof.context > cterm > thm option 
4319  73 
end; 
74 

42458  75 
functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 = 
4319  76 
struct 
77 

11232  78 
(* FIXME: only test! *) 
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

79 
fun def xs eq = 
42457  80 
(case Data.dest_eq eq of 
42460  81 
SOME (s, t) => 
42458  82 
let val n = length xs in 
83 
s = Bound n andalso not (loose_bvar1 (t, n)) orelse 

84 
t = Bound n andalso not (loose_bvar1 (s, n)) 

85 
end 

86 
 NONE => false); 

4319  87 

42458  88 
fun extract_conj fst xs t = 
89 
(case Data.dest_conj t of 

90 
NONE => NONE 

42460  91 
 SOME (P, Q) => 
42458  92 
if def xs P then (if fst then NONE else SOME (xs, P, Q)) 
93 
else if def xs Q then SOME (xs, Q, P) 

94 
else 

95 
(case extract_conj false xs P of 

96 
SOME (xs, eq, P') => SOME (xs, eq, Data.conj $ P' $ Q) 

97 
 NONE => 

98 
(case extract_conj false xs Q of 

99 
SOME (xs, eq, Q') => SOME (xs, eq, Data.conj $ P $ Q') 

100 
 NONE => NONE))); 

11232  101 

42458  102 
fun extract_imp fst xs t = 
103 
(case Data.dest_imp t of 

104 
NONE => NONE 

42460  105 
 SOME (P, Q) => 
42458  106 
if def xs P then (if fst then NONE else SOME (xs, P, Q)) 
107 
else 

108 
(case extract_conj false xs P of 

109 
SOME (xs, eq, P') => SOME (xs, eq, Data.imp $ P' $ Q) 

110 
 NONE => 

111 
(case extract_imp false xs Q of 

112 
NONE => NONE 

113 
 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

114 

71726
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

115 
fun extract_conj_from_judgment ctxt fst xs t = 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

116 
if Object_Logic.is_judgment ctxt t 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

117 
then 
71988  118 
let 
119 
val judg $ t' = t 

120 
in 

121 
case extract_conj fst xs t' of 

122 
NONE => NONE 

123 
 SOME (xs, eq, P) => SOME (xs, judg $ eq, judg $ P) 

124 
end 

71726
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

125 
else NONE; 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

126 

fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

127 
fun extract_implies ctxt fst xs t = 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

128 
(case try Logic.dest_implies t of 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

129 
NONE => NONE 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

130 
 SOME (P, Q) => 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

131 
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 metaall
haftmann
parents:
60774
diff
changeset

132 
else 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

133 
(case extract_conj_from_judgment ctxt false xs P of 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

134 
SOME (xs, eq, P') => SOME (xs, eq, Logic.implies $ P' $ Q) 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

135 
 NONE => 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

136 
(case extract_implies ctxt false xs Q of 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

137 
NONE => NONE 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

138 
 SOME (xs, eq, Q') => (SOME (xs, eq, Logic.implies $ P $ Q'))))); 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

139 

fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

140 
fun extract_quant ctxt extract q = 
42458  141 
let 
42460  142 
fun exqu xs ((qC as Const (qa, _)) $ Abs (x, T, Q)) = 
42458  143 
if qa = q then exqu ((qC, x, T) :: xs) Q else NONE 
71726
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

144 
 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

145 
in exqu [] end; 
4319  146 

71726
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

147 
fun iff_reflection_tac ctxt = 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

148 
resolve_tac ctxt [Data.iff_reflection] 1; 
4319  149 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset

150 
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

151 
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

152 

0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

153 
(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...) 
11221  154 
Better: instantiate exI 
155 
*) 

12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

156 
local 
42458  157 
val excomm = Data.ex_comm RS Data.iff_trans; 
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

158 
in 
72112  159 
fun prove_one_point_Ex_tac ctxt = 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset

160 
qcomm_tac ctxt excomm Data.iff_exI 1 THEN resolve_tac ctxt [Data.iffI] 1 THEN 
42458  161 
ALLGOALS 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset

162 
(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

163 
resolve_tac ctxt [Data.exI], 
60774  164 
DEPTH_SOLVE_1 o ares_tac ctxt [Data.conjI]]) 
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

165 
end; 
11221  166 

12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

167 
(* Proves (! x0..xn. (... & x0 = t & ...) > P x0) = 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

168 
(! x1..xn x0. x0 = t > (... & ...) > P x0) 
11221  169 
*) 
11232  170 
local 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset

171 
fun tac ctxt = 
42458  172 
SELECT_GOAL 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset

173 
(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

174 
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

175 
eresolve_tac ctxt [Data.mp], 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset

176 
REPEAT o eresolve_tac ctxt [Data.conjE], 
60774  177 
REPEAT o ares_tac ctxt [Data.conjI]]); 
71726
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

178 
val all_comm = Data.all_comm RS Data.iff_trans; 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

179 
val All_comm = @{thm swap_params [THEN transitive]}; 
11232  180 
in 
72112  181 
fun prove_one_point_All_tac ctxt = 
71726
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

182 
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

183 
resolve_tac ctxt [Data.iff_allI], 
71726
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

184 
resolve_tac ctxt [Data.iffI], 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

185 
tac ctxt, 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

186 
tac ctxt]; 
72112  187 
fun prove_one_point_all_tac ctxt = 
71726
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

188 
EVERY1 [qcomm_tac ctxt All_comm @{thm equal_allI}, 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

189 
resolve_tac ctxt [@{thm equal_allI}], 
72142  190 
Object_Logic.full_atomize_tac ctxt, 
71726
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

191 
resolve_tac ctxt [@{thm equal_intr_rule}], 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

192 
tac ctxt, 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

193 
tac ctxt]; 
11232  194 
end 
4319  195 

71726
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

196 
fun prove_conv ctxt tu tac = 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

197 
let 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

198 
val (goal, ctxt') = 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

199 
yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt; 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

200 
val thm = 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

201 
Goal.prove ctxt' [] [] goal 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

202 
(fn {context = ctxt'', ...} => tac ctxt''); 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

203 
in singleton (Variable.export ctxt' ctxt) thm end; 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

204 

42458  205 
fun renumber l u (Bound i) = 
206 
Bound (if i < l orelse i > u then i else if i = u then l else i + 1) 

207 
 renumber l u (s $ t) = renumber l u s $ renumber l u t 

208 
 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

209 
 renumber _ _ atom = atom; 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

210 

0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

211 
fun quantify qC x T xs P = 
42458  212 
let 
213 
fun quant [] P = P 

214 
 quant ((qC, x, T) :: xs) P = quant xs (qC $ Abs (x, T, P)); 

215 
val n = length xs; 

216 
val Q = if n = 0 then P else renumber 0 n P; 

217 
in quant xs (qC $ Abs (x, T, Q)) end; 

12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

218 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42460
diff
changeset

219 
fun rearrange_all ctxt ct = 
59582  220 
(case Thm.term_of ct of 
42459  221 
F as (all as Const (q, _)) $ Abs (x, T, P) => 
72112  222 
(case extract_quant ctxt extract_implies q P of 
15531  223 
NONE => NONE 
42458  224 
 SOME (xs, eq, Q) => 
72112  225 
let val R = quantify all x T xs (Logic.implies $ eq $ Q) 
226 
in SOME (prove_conv ctxt (F, R) prove_one_point_all_tac) end) 

71726
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

227 
 _ => NONE); 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

228 

fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

229 
fun rearrange_All ctxt ct = 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

230 
(case Thm.term_of ct of 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

231 
F as (all as Const (q, _)) $ Abs (x, T, P) => 
72112  232 
(case extract_quant ctxt (K extract_imp) q P of 
71726
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

233 
NONE => NONE 
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

234 
 SOME (xs, eq, Q) => 
72112  235 
let val R = quantify all x T xs (Data.imp $ eq $ Q) 
236 
in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_All_tac)) end) 

42459  237 
 _ => NONE); 
4319  238 

72112  239 
fun rearrange_Ball tac ctxt ct = 
59582  240 
(case Thm.term_of ct of 
42459  241 
F as Ball $ A $ Abs (x, T, P) => 
42458  242 
(case extract_imp true [] P of 
15531  243 
NONE => NONE 
42458  244 
 SOME (xs, eq, Q) => 
245 
if not (null xs) then NONE 

246 
else 

247 
let val R = Data.imp $ eq $ Q 

72112  248 
in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R)) 
249 
(iff_reflection_tac THEN' tac THEN' prove_one_point_All_tac)) end) 

42459  250 
 _ => NONE); 
4319  251 

72112  252 
fun rearrange_Ex ctxt ct = 
59582  253 
(case Thm.term_of ct of 
42459  254 
F as (ex as Const (q, _)) $ Abs (x, T, P) => 
71726
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

255 
(case extract_quant ctxt (K extract_conj) q P of 
15531  256 
NONE => NONE 
42458  257 
 SOME (xs, eq, Q) => 
42457  258 
let val R = quantify ex x T xs (Data.conj $ eq $ Q) 
72112  259 
in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_Ex_tac)) end) 
42459  260 
 _ => NONE); 
4319  261 

72112  262 
fun rearrange_Bex tac ctxt ct = 
59582  263 
(case Thm.term_of ct of 
42459  264 
F as Bex $ A $ Abs (x, T, P) => 
42458  265 
(case extract_conj true [] P of 
15531  266 
NONE => NONE 
42458  267 
 SOME (xs, eq, Q) => 
268 
if not (null xs) then NONE 

72112  269 
else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) 
270 
(iff_reflection_tac THEN' tac THEN' prove_one_point_Ex_tac))) 

42459  271 
 _ => NONE); 
11221  272 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42460
diff
changeset

273 
fun rearrange_Collect tac ctxt ct = 
59582  274 
(case Thm.term_of ct of 
42459  275 
F as Collect $ Abs (x, T, P) => 
42458  276 
(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

277 
NONE => NONE 
42458  278 
 SOME (_, eq, Q) => 
279 
let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q) 

71726
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

280 
in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' tac)) end) 
42459  281 
 _ => 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

282 

4319  283 
end; 
42460  284 