author  immler 
Sun, 27 Oct 2019 21:51:14 0400  
changeset 71035  6fe5a0e1fa8e 
parent 60774  6c28d8ed2488 
child 71512  fe93a863d946 
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 

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 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42460
diff
changeset

70 
val rearrange_ex: Proof.context > cterm > thm option 
54998  71 
val rearrange_ball: (Proof.context > tactic) > Proof.context > cterm > thm option 
72 
val rearrange_bex: (Proof.context > tactic) > Proof.context > cterm > thm option 

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 

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

116 
fun extract_quant extract q = 
42458  117 
let 
42460  118 
fun exqu xs ((qC as Const (qa, _)) $ Abs (x, T, Q)) = 
42458  119 
if qa = q then exqu ((qC, x, T) :: xs) Q else NONE 
120 
 exqu xs P = extract (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

121 
in exqu [] end; 
4319  122 

54998  123 
fun prove_conv ctxt tu tac = 
42456
13b4b6ba3593
proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents:
42361
diff
changeset

124 
let 
13b4b6ba3593
proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents:
42361
diff
changeset

125 
val (goal, ctxt') = 
13b4b6ba3593
proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents:
42361
diff
changeset

126 
yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt; 
13b4b6ba3593
proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents:
42361
diff
changeset

127 
val thm = 
54998  128 
Goal.prove ctxt' [] [] goal 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset

129 
(fn {context = ctxt'', ...} => 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset

130 
resolve_tac ctxt'' [Data.iff_reflection] 1 THEN tac ctxt''); 
42456
13b4b6ba3593
proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
wenzelm
parents:
42361
diff
changeset

131 
in singleton (Variable.export ctxt' ctxt) thm end; 
4319  132 

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

133 
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

134 
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

135 

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

136 
(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...) 
11221  137 
Better: instantiate exI 
138 
*) 

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

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

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

142 
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

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

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

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

148 
end; 
11221  149 

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

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

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

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

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

157 
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

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

159 
REPEAT o eresolve_tac ctxt [Data.conjE], 
60774  160 
REPEAT o ares_tac ctxt [Data.conjI]]); 
42458  161 
val allcomm = Data.all_comm RS Data.iff_trans; 
11232  162 
in 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset

163 
fun prove_one_point_all_tac ctxt = 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset

164 
EVERY1 [qcomm_tac ctxt allcomm Data.iff_allI, 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset

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

166 
resolve_tac ctxt [Data.iffI], tac ctxt, tac ctxt]; 
11232  167 
end 
4319  168 

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

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

172 
 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

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

174 

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

175 
fun quantify qC x T xs P = 
42458  176 
let 
177 
fun quant [] P = P 

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

179 
val n = length xs; 

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

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

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

182 

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

183 
fun rearrange_all ctxt ct = 
59582  184 
(case Thm.term_of ct of 
42459  185 
F as (all as Const (q, _)) $ Abs (x, T, P) => 
42458  186 
(case extract_quant extract_imp q P of 
15531  187 
NONE => NONE 
42458  188 
 SOME (xs, eq, Q) => 
42457  189 
let val R = quantify all x T xs (Data.imp $ eq $ Q) 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset

190 
in SOME (prove_conv ctxt (F, R) prove_one_point_all_tac) end) 
42459  191 
 _ => NONE); 
4319  192 

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

193 
fun rearrange_ball tac ctxt ct = 
59582  194 
(case Thm.term_of ct of 
42459  195 
F as Ball $ A $ Abs (x, T, P) => 
42458  196 
(case extract_imp true [] P of 
15531  197 
NONE => NONE 
42458  198 
 SOME (xs, eq, Q) => 
199 
if not (null xs) then NONE 

200 
else 

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

54998  202 
in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R)) tac) end) 
42459  203 
 _ => NONE); 
4319  204 

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

205 
fun rearrange_ex ctxt ct = 
59582  206 
(case Thm.term_of ct of 
42459  207 
F as (ex as Const (q, _)) $ Abs (x, T, P) => 
42458  208 
(case extract_quant extract_conj q P of 
15531  209 
NONE => NONE 
42458  210 
 SOME (xs, eq, Q) => 
42457  211 
let val R = quantify ex x T xs (Data.conj $ eq $ Q) 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset

212 
in SOME (prove_conv ctxt (F, R) prove_one_point_ex_tac) end) 
42459  213 
 _ => NONE); 
4319  214 

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

215 
fun rearrange_bex tac ctxt ct = 
59582  216 
(case Thm.term_of ct of 
42459  217 
F as Bex $ A $ Abs (x, T, P) => 
42458  218 
(case extract_conj true [] P of 
15531  219 
NONE => NONE 
42458  220 
 SOME (xs, eq, Q) => 
221 
if not (null xs) then NONE 

54998  222 
else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) tac)) 
42459  223 
 _ => NONE); 
11221  224 

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

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

229 
NONE => NONE 
42458  230 
 SOME (_, eq, Q) => 
231 
let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q) 

54998  232 
in SOME (prove_conv ctxt (F, R) tac) end) 
42459  233 
 _ => 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

234 

4319  235 
end; 
42460  236 