author  blanchet 
Tue, 07 Dec 2010 11:56:01 +0100  
changeset 41051  2ed1b971fc20 
parent 38457  b8760b6e7c65 
child 42361  23f352990944 
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 
4319  10 
by ordinary simplification. 
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)". 
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*) 

43 
val dest_eq: term > (term*term*term)option 

44 
val dest_conj: term > (term*term*term)option 

11232  45 
val dest_imp: term > (term*term*term)option 
4319  46 
val conj: term 
47 
val imp: term 

48 
(*rules*) 

49 
val iff_reflection: thm (* P <> Q ==> P == Q *) 

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 

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 

17002  69 
val rearrange_all: theory > simpset > term > thm option 
70 
val rearrange_ex: theory > simpset > term > thm option 

71 
val rearrange_ball: (simpset > tactic) > theory > simpset > term > thm option 

72 
val rearrange_bex: (simpset > tactic) > theory > simpset > term > thm option 

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

73 
val rearrange_Coll: tactic > theory > simpset > term > thm option 
4319  74 
end; 
75 

76 
functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 = 

77 
struct 

78 

79 
open Data; 

80 

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

82 
fun def xs eq = 
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

83 
(case dest_eq eq of 
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

84 
SOME(c,s,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

85 
let val n = length xs 
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

86 
in s = Bound n andalso not(loose_bvar1(t,n)) orelse 
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

87 
t = Bound n andalso not(loose_bvar1(s,n)) end 
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

88 
 NONE => false); 
4319  89 

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

90 
fun extract_conj fst xs t = case dest_conj t of NONE => NONE 
15531  91 
 SOME(conj,P,Q) => 
31197
c1c163ec6c44
finetuned elimination of comprehensions involving x=t.
nipkow
parents:
31166
diff
changeset

92 
(if def xs P then (if fst then NONE else SOME(xs,P,Q)) else 
15531  93 
if def xs Q then SOME(xs,Q,P) else 
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

94 
(case extract_conj false xs P of 
15531  95 
SOME(xs,eq,P') => SOME(xs,eq, conj $ P' $ Q) 
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

96 
 NONE => (case extract_conj false xs Q of 
15531  97 
SOME(xs,eq,Q') => SOME(xs,eq,conj $ P $ Q') 
98 
 NONE => NONE))); 

11232  99 

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

100 
fun extract_imp fst xs t = case dest_imp t of NONE => NONE 
31197
c1c163ec6c44
finetuned elimination of comprehensions involving x=t.
nipkow
parents:
31166
diff
changeset

101 
 SOME(imp,P,Q) => if def xs P then (if fst then NONE else SOME(xs,P,Q)) 
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

102 
else (case extract_conj false xs P of 
15531  103 
SOME(xs,eq,P') => SOME(xs, eq, imp $ P' $ Q) 
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

104 
 NONE => (case extract_imp false xs Q of 
15531  105 
NONE => NONE 
106 
 SOME(xs,eq,Q') => 

107 
SOME(xs,eq,imp$P$Q'))); 

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

108 

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

109 
fun extract_quant extract q = 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

110 
let fun exqu xs ((qC as Const(qa,_)) $ Abs(x,T,Q)) = 
15531  111 
if qa = q then exqu ((qC,x,T)::xs) Q else 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

112 
 exqu xs P = extract (null xs) xs P 
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

113 
in exqu [] end; 
4319  114 

17002  115 
fun prove_conv tac thy tu = 
38452
abc655166d61
now works for schematic terms as well, thanks to Alex for the `howto'
nipkow
parents:
36610
diff
changeset

116 
let val ctxt = ProofContext.init_global thy; 
abc655166d61
now works for schematic terms as well, thanks to Alex for the `howto'
nipkow
parents:
36610
diff
changeset

117 
val eq_tu = Logic.mk_equals tu; 
abc655166d61
now works for schematic terms as well, thanks to Alex for the `howto'
nipkow
parents:
36610
diff
changeset

118 
val ([fixed_goal], ctxt') = Variable.import_terms true [eq_tu] ctxt; 
abc655166d61
now works for schematic terms as well, thanks to Alex for the `howto'
nipkow
parents:
36610
diff
changeset

119 
val thm = Goal.prove ctxt' [] [] fixed_goal 
abc655166d61
now works for schematic terms as well, thanks to Alex for the `howto'
nipkow
parents:
36610
diff
changeset

120 
(K (rtac iff_reflection 1 THEN tac)); 
abc655166d61
now works for schematic terms as well, thanks to Alex for the `howto'
nipkow
parents:
36610
diff
changeset

121 
val [gen_thm] = Variable.export ctxt' ctxt [thm]; 
abc655166d61
now works for schematic terms as well, thanks to Alex for the `howto'
nipkow
parents:
36610
diff
changeset

122 
in gen_thm end; 
4319  123 

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

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

125 

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

126 
(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...) 
11221  127 
Better: instantiate exI 
128 
*) 

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

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

130 
val excomm = ex_comm RS iff_trans 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

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

132 
val prove_one_point_ex_tac = qcomm_tac excomm iff_exI 1 THEN rtac iffI 1 THEN 
11221  133 
ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI, 
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

134 
DEPTH_SOLVE_1 o (ares_tac [conjI])]) 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

135 
end; 
11221  136 

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

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

138 
(! x1..xn x0. x0 = t > (... & ...) > P x0) 
11221  139 
*) 
11232  140 
local 
141 
val tac = SELECT_GOAL 

142 
(EVERY1[REPEAT o (dtac uncurry), REPEAT o (rtac impI), etac mp, 

143 
REPEAT o (etac conjE), REPEAT o (ares_tac [conjI])]) 

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

144 
val allcomm = all_comm RS iff_trans 
11232  145 
in 
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

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

147 
EVERY1[qcomm_tac allcomm iff_allI,rtac iff_allI, rtac iffI, tac, tac] 
11232  148 
end 
4319  149 

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

150 
fun renumber l u (Bound i) = Bound(if i < l orelse i > u then i else 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

151 
if i=u then l else i+1) 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

152 
 renumber l u (s$t) = renumber l u s $ renumber l u t 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

153 
 renumber l u (Abs(x,T,t)) = Abs(x,T,renumber (l+1) (u+1) t) 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

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

155 

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

156 
fun quantify qC x T xs P = 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

157 
let fun quant [] P = P 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

158 
 quant ((qC,x,T)::xs) P = quant xs (qC $ Abs(x,T,P)) 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

159 
val n = length xs 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

160 
val Q = if n=0 then P else renumber 0 n P 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

161 
in quant xs (qC $ Abs(x,T,Q)) end; 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

162 

17002  163 
fun rearrange_all thy _ (F as (all as Const(q,_)) $ Abs(x,T, 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

164 
(case extract_quant extract_imp q P of 
15531  165 
NONE => NONE 
166 
 SOME(xs,eq,Q) => 

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

167 
let val R = quantify all x T xs (imp $ eq $ Q) 
17002  168 
in SOME(prove_conv prove_one_point_all_tac thy (F,R)) end) 
15531  169 
 rearrange_all _ _ _ = NONE; 
4319  170 

17002  171 
fun rearrange_ball tac thy ss (F as Ball $ A $ Abs(x,T,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

172 
(case extract_imp true [] P of 
15531  173 
NONE => NONE 
174 
 SOME(xs,eq,Q) => if not(null xs) then NONE else 

11232  175 
let val R = imp $ eq $ Q 
17002  176 
in SOME(prove_conv (tac ss) thy (F,Ball $ A $ Abs(x,T,R))) end) 
15531  177 
 rearrange_ball _ _ _ _ = NONE; 
4319  178 

17002  179 
fun rearrange_ex thy _ (F as (ex as Const(q,_)) $ Abs(x,T,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

180 
(case extract_quant extract_conj q P of 
15531  181 
NONE => NONE 
182 
 SOME(xs,eq,Q) => 

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

183 
let val R = quantify ex x T xs (conj $ eq $ Q) 
17002  184 
in SOME(prove_conv prove_one_point_ex_tac thy (F,R)) end) 
15531  185 
 rearrange_ex _ _ _ = NONE; 
4319  186 

17002  187 
fun rearrange_bex tac thy ss (F as Bex $ A $ Abs(x,T,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

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

17002  191 
SOME(prove_conv (tac ss) thy (F,Bex $ A $ Abs(x,T,conj$eq$Q)))) 
15531  192 
 rearrange_bex _ _ _ _ = NONE; 
11221  193 

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

194 
fun rearrange_Coll tac thy _ (F as Coll $ Abs(x,T,P)) = 
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

195 
(case extract_conj true [] P of 
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

196 
NONE => NONE 
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

197 
 SOME(_,eq,Q) => 
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

198 
let val R = Coll $ Abs(x,T, conj $ eq $ Q) 
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

199 
in SOME(prove_conv tac thy (F,R)) end); 
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

200 

4319  201 
end; 