author  wenzelm 
Fri, 02 Oct 2009 22:15:08 +0200  
changeset 32861  105f40051387 
parent 31197  c1c163ec6c44 
child 35762  af3ff2ba4c54 
permissions  rwrr 
4319  1 
(* Title: Provers/quantifier1 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

4 
Copyright 1997 TU Munich 

5 

6 
Simplification procedures for turning 

7 

8 
? x. ... & x = t & ... 

9 
into ? x. x = t & ... & ... 

11232  10 
where the `? x. x = t &' in the latter formula must be eliminated 
4319  11 
by ordinary simplification. 
12 

13 
and ! x. (... & x = t & ...) > P x 

14 
into ! x. x = t > (... & ...) > P x 

15 
where the `!x. x=t >' in the latter formula is eliminated 

16 
by ordinary simplification. 

17 

11232  18 
And analogously for t=x, but the eqn is not turned around! 
19 

4319  20 
NB Simproc is only triggered by "!x. P(x) & P'(x) > Q(x)"; 
21 
"!x. x=t > P(x)" is covered by the congreunce rule for >; 

22 
"!x. t=x > P(x)" must be taken care of by an ordinary rewrite rule. 

11232  23 
As must be "? x. t=x & P(x)". 
24 

11221  25 
And similarly for the bounded quantifiers. 
26 

4319  27 
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

28 

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

29 
The above also works for !x1..xn. and ?x1..xn by moving the defined 
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 
qunatifier inside first, but not for nested bounded quantifiers. 
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 

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

33 
... & 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

34 
... & 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

35 
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

36 

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

38 
esp if x=t/t=x sits at the front already. 
4319  39 
*) 
40 

41 
signature QUANTIFIER1_DATA = 

42 
sig 

43 
(*abstract syntax*) 

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

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

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

49 
(*rules*) 

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

51 
val iffI: thm 

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

52 
val iff_trans: thm 
4319  53 
val conjI: thm 
54 
val conjE: thm 

55 
val impI: thm 

56 
val mp: thm 

57 
val exI: thm 

58 
val exE: thm 

11232  59 
val uncurry: thm (* P > Q > R ==> P & Q > R *) 
60 
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

61 
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

62 
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

63 
val ex_comm: thm (* (? x y. P x y) = (? y x. P x y) *) 
4319  64 
end; 
65 

66 
signature QUANTIFIER1 = 

67 
sig 

11221  68 
val prove_one_point_all_tac: tactic 
69 
val prove_one_point_ex_tac: tactic 

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

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

73 
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

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

77 
functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 = 

78 
struct 

79 

80 
open Data; 

81 

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

83 
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

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

85 
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

86 
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

87 
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

88 
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

89 
 NONE => false); 
4319  90 

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

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

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

95 
(case extract_conj false xs P of 
15531  96 
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

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

11232  100 

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

101 
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

102 
 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

103 
else (case extract_conj false xs P of 
15531  104 
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

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

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

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

109 

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

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

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

113 
 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

114 
in exqu [] end; 
4319  115 

17002  116 
fun prove_conv tac thy tu = 
20049  117 
Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu) 
118 
(K (rtac iff_reflection 1 THEN tac)); 

4319  119 

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

120 
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

121 

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

122 
(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...) 
11221  123 
Better: instantiate exI 
124 
*) 

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

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

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

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

128 
val prove_one_point_ex_tac = qcomm_tac excomm iff_exI 1 THEN rtac iffI 1 THEN 
11221  129 
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

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

131 
end; 
11221  132 

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

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

134 
(! x1..xn x0. x0 = t > (... & ...) > P x0) 
11221  135 
*) 
11232  136 
local 
137 
val tac = SELECT_GOAL 

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

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

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

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

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

143 
EVERY1[qcomm_tac allcomm iff_allI,rtac iff_allI, rtac iffI, tac, tac] 
11232  144 
end 
4319  145 

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

146 
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

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

148 
 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

149 
 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

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

151 

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

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

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

154 
 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

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

156 
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

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

158 

17002  159 
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

160 
(case extract_quant extract_imp q P of 
15531  161 
NONE => NONE 
162 
 SOME(xs,eq,Q) => 

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

163 
let val R = quantify all x T xs (imp $ eq $ Q) 
17002  164 
in SOME(prove_conv prove_one_point_all_tac thy (F,R)) end) 
15531  165 
 rearrange_all _ _ _ = NONE; 
4319  166 

17002  167 
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

168 
(case extract_imp true [] P of 
15531  169 
NONE => NONE 
170 
 SOME(xs,eq,Q) => if not(null xs) then NONE else 

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

17002  175 
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

176 
(case extract_quant extract_conj q P of 
15531  177 
NONE => NONE 
178 
 SOME(xs,eq,Q) => 

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

179 
let val R = quantify ex x T xs (conj $ eq $ Q) 
17002  180 
in SOME(prove_conv prove_one_point_ex_tac thy (F,R)) end) 
15531  181 
 rearrange_ex _ _ _ = NONE; 
4319  182 

17002  183 
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

184 
(case extract_conj true [] P of 
15531  185 
NONE => NONE 
186 
 SOME(xs,eq,Q) => if not(null xs) then NONE else 

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

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

190 
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

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

192 
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

193 
 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

194 
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

195 
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

196 

4319  197 
end; 