author  wenzelm 
Thu, 08 Aug 2002 23:46:09 +0200  
changeset 13480  bb72bd43c6c3 
parent 12523  0d8d5bf549b0 
child 15027  d23887300b96 
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)". 
4319  24 

11232  25 

11221  26 
And similarly for the bounded quantifiers. 
27 

4319  28 
Gries etc call this the "1 point rules" 
29 
*) 

30 

31 
signature QUANTIFIER1_DATA = 

32 
sig 

33 
(*abstract syntax*) 

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

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

11232  36 
val dest_imp: term > (term*term*term)option 
4319  37 
val conj: term 
38 
val imp: term 

39 
(*rules*) 

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

41 
val iffI: thm 

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

42 
val iff_trans: thm 
4319  43 
val conjI: thm 
44 
val conjE: thm 

45 
val impI: thm 

46 
val mp: thm 

47 
val exI: thm 

48 
val exE: thm 

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

51 
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

52 
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

53 
val ex_comm: thm (* (? x y. P x y) = (? y x. P x y) *) 
4319  54 
end; 
55 

56 
signature QUANTIFIER1 = 

57 
sig 

11221  58 
val prove_one_point_all_tac: tactic 
59 
val prove_one_point_ex_tac: tactic 

4319  60 
val rearrange_all: Sign.sg > thm list > term > thm option 
61 
val rearrange_ex: Sign.sg > thm list > term > thm option 

11221  62 
val rearrange_ball: tactic > Sign.sg > thm list > term > thm option 
63 
val rearrange_bex: tactic > Sign.sg > thm list > term > thm option 

4319  64 
end; 
65 

66 
functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 = 

67 
struct 

68 

69 
open Data; 

70 

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

72 
fun def xs eq = 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

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

74 
in case dest_eq eq of 
4319  75 
Some(c,s,t) => 
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

76 
s = Bound n andalso not(loose_bvar1(t,n)) orelse 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

77 
t = Bound n andalso not(loose_bvar1(s,n)) 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

78 
 None => false 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

79 
end; 
4319  80 

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

81 
fun extract_conj xs t = case dest_conj t of None => None 
11232  82 
 Some(conj,P,Q) => 
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

83 
(if def xs P then Some(xs,P,Q) else 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

84 
if def xs Q then Some(xs,Q,P) else 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

85 
(case extract_conj xs P of 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

86 
Some(xs,eq,P') => Some(xs,eq, conj $ P' $ Q) 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

87 
 None => (case extract_conj xs Q of 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

88 
Some(xs,eq,Q') => Some(xs,eq,conj $ P $ Q') 
11232  89 
 None => None))); 
90 

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

91 
fun extract_imp xs t = case dest_imp t of None => None 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

92 
 Some(imp,P,Q) => if def xs P then Some(xs,P,Q) 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

93 
else (case extract_conj xs P of 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

94 
Some(xs,eq,P') => Some(xs, eq, imp $ P' $ Q) 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

95 
 None => (case extract_imp xs Q of 
11232  96 
None => None 
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

97 
 Some(xs,eq,Q') => 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

98 
Some(xs,eq,imp$P$Q'))); 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

99 

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

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

101 
let fun exqu xs ((qC as Const(qa,_)) $ Abs(x,T,Q)) = 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

102 
if qa = q then exqu ((qC,x,T)::xs) Q else None 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

103 
 exqu xs P = extract xs P 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

104 
in exqu end; 
4319  105 

106 
fun prove_conv tac sg tu = 

13480
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
12523
diff
changeset

107 
Tactic.prove sg [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac)); 
4319  108 

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

109 
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

110 

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

111 
(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...) 
11221  112 
Better: instantiate exI 
113 
*) 

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

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

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

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

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

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

120 
end; 
11221  121 

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

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

123 
(! x1..xn x0. x0 = t > (... & ...) > P x0) 
11221  124 
*) 
11232  125 
local 
126 
val tac = SELECT_GOAL 

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

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

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

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

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

132 
EVERY1[qcomm_tac allcomm iff_allI,rtac iff_allI, rtac iffI, tac, tac] 
11232  133 
end 
4319  134 

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

135 
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

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

137 
 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

138 
 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

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

140 

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

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

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

143 
 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

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

145 
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

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

147 

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

148 
fun rearrange_all sg _ (F as (all as Const(q,_)) $ Abs(x,T, P)) = 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

149 
(case extract_quant extract_imp q [] P of 
4319  150 
None => None 
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

151 
 Some(xs,eq,Q) => 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

152 
let val R = quantify all x T xs (imp $ eq $ Q) 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

153 
in Some(prove_conv prove_one_point_all_tac sg (F,R)) end) 
4319  154 
 rearrange_all _ _ _ = None; 
155 

11232  156 
fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,P)) = 
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

157 
(case extract_imp [] P of 
11221  158 
None => None 
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

159 
 Some(xs,eq,Q) => if not(null xs) then None else 
11232  160 
let val R = imp $ eq $ Q 
11221  161 
in Some(prove_conv tac sg (F,Ball $ A $ Abs(x,T,R))) end) 
162 
 rearrange_ball _ _ _ _ = None; 

4319  163 

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

164 
fun rearrange_ex sg _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) = 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

165 
(case extract_quant extract_conj q [] P of 
4319  166 
None => None 
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

167 
 Some(xs,eq,Q) => 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

168 
let val R = quantify ex x T xs (conj $ eq $ Q) 
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

169 
in Some(prove_conv prove_one_point_ex_tac sg (F,R)) end) 
4319  170 
 rearrange_ex _ _ _ = None; 
171 

11221  172 
fun rearrange_bex tac sg _ (F as Bex $ A $ Abs(x,T,P)) = 
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

173 
(case extract_conj [] P of 
11221  174 
None => None 
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

175 
 Some(xs,eq,Q) => if not(null xs) then None else 
11221  176 
Some(prove_conv tac sg (F,Bex $ A $ Abs(x,T,conj$eq$Q)))) 
177 
 rearrange_bex _ _ _ _ = None; 

178 

4319  179 
end; 