author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 54998  8601434fa334 
child 58838  59203adfc33f 
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 

11221  67 
val prove_one_point_all_tac: tactic 
68 
val prove_one_point_ex_tac: 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 
129 
(fn {context = ctxt'', ...} => rtac 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

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

42458  132 
fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i); 
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

133 

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

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

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

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

139 
in 
42458  140 
val prove_one_point_ex_tac = 
141 
qcomm_tac excomm Data.iff_exI 1 THEN rtac Data.iffI 1 THEN 

142 
ALLGOALS 

143 
(EVERY' [etac Data.exE, REPEAT_DETERM o etac Data.conjE, rtac Data.exI, 

144 
DEPTH_SOLVE_1 o ares_tac [Data.conjI]]) 

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

145 
end; 
11221  146 

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

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

148 
(! x1..xn x0. x0 = t > (... & ...) > P x0) 
11221  149 
*) 
11232  150 
local 
42458  151 
val tac = 
152 
SELECT_GOAL 

153 
(EVERY1 [REPEAT o dtac Data.uncurry, REPEAT o rtac Data.impI, etac Data.mp, 

154 
REPEAT o etac Data.conjE, REPEAT o ares_tac [Data.conjI]]); 

155 
val allcomm = Data.all_comm RS Data.iff_trans; 

11232  156 
in 
42458  157 
val prove_one_point_all_tac = 
158 
EVERY1 [qcomm_tac allcomm Data.iff_allI, rtac Data.iff_allI, rtac Data.iffI, tac, tac]; 

11232  159 
end 
4319  160 

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

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

164 
 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

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

166 

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

167 
fun quantify qC x T xs P = 
42458  168 
let 
169 
fun quant [] P = P 

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

171 
val n = length xs; 

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

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

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

174 

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

175 
fun rearrange_all ctxt ct = 
42459  176 
(case term_of ct of 
177 
F as (all as Const (q, _)) $ Abs (x, T, P) => 

42458  178 
(case extract_quant extract_imp q P of 
15531  179 
NONE => NONE 
42458  180 
 SOME (xs, eq, Q) => 
42457  181 
let val R = quantify all x T xs (Data.imp $ eq $ Q) 
54998  182 
in SOME (prove_conv ctxt (F, R) (K prove_one_point_all_tac)) end) 
42459  183 
 _ => NONE); 
4319  184 

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

185 
fun rearrange_ball tac ctxt ct = 
42459  186 
(case term_of ct of 
187 
F as Ball $ A $ Abs (x, T, P) => 

42458  188 
(case extract_imp true [] P of 
15531  189 
NONE => NONE 
42458  190 
 SOME (xs, eq, Q) => 
191 
if not (null xs) then NONE 

192 
else 

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

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

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

197 
fun rearrange_ex ctxt ct = 
42459  198 
(case term_of ct of 
199 
F as (ex as Const (q, _)) $ Abs (x, T, P) => 

42458  200 
(case extract_quant extract_conj q P of 
15531  201 
NONE => NONE 
42458  202 
 SOME (xs, eq, Q) => 
42457  203 
let val R = quantify ex x T xs (Data.conj $ eq $ Q) 
54998  204 
in SOME (prove_conv ctxt (F, R) (K prove_one_point_ex_tac)) end) 
42459  205 
 _ => NONE); 
4319  206 

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

207 
fun rearrange_bex tac ctxt ct = 
42459  208 
(case term_of ct of 
209 
F as Bex $ A $ Abs (x, T, P) => 

42458  210 
(case extract_conj true [] P of 
15531  211 
NONE => NONE 
42458  212 
 SOME (xs, eq, Q) => 
213 
if not (null xs) then NONE 

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

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

217 
fun rearrange_Collect tac ctxt ct = 
42459  218 
(case term_of ct of 
219 
F as Collect $ Abs (x, T, P) => 

42458  220 
(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

221 
NONE => NONE 
42458  222 
 SOME (_, eq, Q) => 
223 
let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q) 

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

226 

4319  227 
end; 
42460  228 