author  wenzelm 
Fri, 08 Jan 2021 22:30:32 +0100  
changeset 73110  c87ca43ebd3b 
parent 71916  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) *) 
71916
435cdc772110
specific atomization inert to later rule set modifications
haftmann
parents:
71915
diff
changeset

63 
val atomize: Proof.context > conv 
4319  64 
end; 
65 

66 
signature QUANTIFIER1 = 

67 
sig 

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

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

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

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

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

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

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

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

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

86 
end 

87 
 NONE => false); 

4319  88 

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

91 
NONE => NONE 

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

95 
else 

96 
(case extract_conj false xs P of 

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

98 
 NONE => 

99 
(case extract_conj false xs Q of 

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

101 
 NONE => NONE))); 

11232  102 

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

105 
NONE => NONE 

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

109 
(case extract_conj false xs P of 

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

111 
 NONE => 

112 
(case extract_imp false xs Q of 

113 
NONE => NONE 

114 
 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

115 

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

116 
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

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

118 
then 
71773  119 
let 
120 
val judg $ t' = t 

121 
in 

122 
case extract_conj fst xs t' of 

123 
NONE => NONE 

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

125 
end 

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

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

127 

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

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

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

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

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

132 
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

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

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

135 
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

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

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

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

139 
 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

140 

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

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

145 
 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

146 
in exqu [] end; 
4319  147 

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

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

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

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

151 
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

152 
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

153 

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

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

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

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

159 
in 
71886  160 
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

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

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

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

166 
end; 
11221  167 

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

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

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

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

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

175 
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

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

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

179 
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

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

183 
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

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

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

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

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

189 
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

190 
resolve_tac ctxt [@{thm equal_allI}], 
71916
435cdc772110
specific atomization inert to later rule set modifications
haftmann
parents:
71915
diff
changeset

191 
CONVERSION (Data.atomize ctxt), 
71512
fe93a863d946
infrastructure for extraction of equations x = t from premises beneath metaall
haftmann
parents:
60774
diff
changeset

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

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

194 
tac ctxt]; 
11232  195 
end 
4319  196 

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

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

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

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

200 
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

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

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

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

204 
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

205 

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

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

209 
 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

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

211 

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

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

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

216 
val n = length xs; 

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

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

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

219 

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

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

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

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

229 

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

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

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

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

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

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

42459  238 
 _ => NONE); 
4319  239 

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

247 
else 

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

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

42459  251 
 _ => NONE); 
4319  252 

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

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

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

71886  270 
else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) 
271 
(iff_reflection_tac THEN' tac THEN' prove_one_point_Ex_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 metaall
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 