author  wenzelm 
Sun, 11 Jan 2009 21:49:59 +0100  
changeset 29450  ac7f67be7f1f 
parent 20049  f48c4a3a34bc 
child 31166  a90fe83f58ea 
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 

17002  60 
val rearrange_all: theory > simpset > term > thm option 
61 
val rearrange_ex: theory > simpset > term > thm option 

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

63 
val rearrange_bex: (simpset > tactic) > theory > simpset > 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 
15531  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)) 
15531  78 
 NONE => false 
12523
0d8d5bf549b0
now permutations of quantifiers are allowed as well.
nipkow
parents:
11232
diff
changeset

79 
end; 
4319  80 

15531  81 
fun extract_conj xs t = case dest_conj t of NONE => NONE 
82 
 SOME(conj,P,Q) => 

83 
(if def xs P then SOME(xs,P,Q) else 

84 
if def xs Q then SOME(xs,Q,P) else 

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

85 
(case extract_conj xs P of 
15531  86 
SOME(xs,eq,P') => SOME(xs,eq, conj $ P' $ Q) 
87 
 NONE => (case extract_conj xs Q of 

88 
SOME(xs,eq,Q') => SOME(xs,eq,conj $ P $ Q') 

89 
 NONE => NONE))); 

11232  90 

15531  91 
fun extract_imp xs t = case dest_imp t of NONE => NONE 
92 
 SOME(imp,P,Q) => if def xs P then SOME(xs,P,Q) 

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

93 
else (case extract_conj xs P of 
15531  94 
SOME(xs,eq,P') => SOME(xs, eq, imp $ P' $ Q) 
95 
 NONE => (case extract_imp xs Q of 

96 
NONE => NONE 

97 
 SOME(xs,eq,Q') => 

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

12523
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)) = 
15531  102 
if qa = q then exqu ((qC,x,T)::xs) Q else NONE 
12523
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 

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

4319  109 

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

110 
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

111 

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

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

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

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

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

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

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

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

121 
end; 
11221  122 

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

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

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

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

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

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

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

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

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

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

136 
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

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

138 
 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

139 
 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

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

141 

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

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

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

144 
 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

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

146 
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

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

148 

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

150 
(case extract_quant extract_imp q [] P of 
15531  151 
NONE => NONE 
152 
 SOME(xs,eq,Q) => 

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

153 
let val R = quantify all x T xs (imp $ eq $ Q) 
17002  154 
in SOME(prove_conv prove_one_point_all_tac thy (F,R)) end) 
15531  155 
 rearrange_all _ _ _ = NONE; 
4319  156 

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

158 
(case extract_imp [] P of 
15531  159 
NONE => NONE 
160 
 SOME(xs,eq,Q) => if not(null xs) then NONE else 

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

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

166 
(case extract_quant extract_conj q [] P of 
15531  167 
NONE => NONE 
168 
 SOME(xs,eq,Q) => 

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

169 
let val R = quantify ex x T xs (conj $ eq $ Q) 
17002  170 
in SOME(prove_conv prove_one_point_ex_tac thy (F,R)) end) 
15531  171 
 rearrange_ex _ _ _ = NONE; 
4319  172 

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

174 
(case extract_conj [] P of 
15531  175 
NONE => NONE 
176 
 SOME(xs,eq,Q) => if not(null xs) then NONE else 

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

4319  180 
end; 