--- a/src/Provers/quantifier1.ML Thu Mar 29 12:26:37 2001 +0200
+++ b/src/Provers/quantifier1.ML Thu Mar 29 13:59:54 2001 +0200
@@ -7,7 +7,7 @@
? x. ... & x = t & ...
into ? x. x = t & ... & ...
- where the `? x. x = t &' in the latter formula is eliminated
+ where the `? x. x = t &' in the latter formula must be eliminated
by ordinary simplification.
and ! x. (... & x = t & ...) --> P x
@@ -15,10 +15,14 @@
where the `!x. x=t -->' in the latter formula is eliminated
by ordinary simplification.
+ And analogously for t=x, but the eqn is not turned around!
+
NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
"!x. x=t --> P(x)" is covered by the congreunce rule for -->;
"!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
+ As must be "? x. t=x & P(x)".
+
And similarly for the bounded quantifiers.
Gries etc call this the "1 point rules"
@@ -29,21 +33,20 @@
(*abstract syntax*)
val dest_eq: term -> (term*term*term)option
val dest_conj: term -> (term*term*term)option
+ val dest_imp: term -> (term*term*term)option
val conj: term
val imp: term
(*rules*)
val iff_reflection: thm (* P <-> Q ==> P == Q *)
val iffI: thm
- val sym: thm
val conjI: thm
val conjE: thm
val impI: thm
- val impE: thm
val mp: thm
val exI: thm
val exE: thm
- val allI: thm
- val allE: thm
+ val uncurry: thm (* P --> Q --> R ==> P & Q --> R *)
+ val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *)
end;
signature QUANTIFIER1 =
@@ -61,28 +64,31 @@
open Data;
+(* FIXME: only test! *)
fun def eq = case dest_eq eq of
Some(c,s,t) =>
- if s = Bound 0 andalso not(loose_bvar1(t,0)) then Some eq else
- if t = Bound 0 andalso not(loose_bvar1(s,0)) then Some(c$t$s)
- else None
- | None => None;
+ s = Bound 0 andalso not(loose_bvar1(t,0)) orelse
+ t = Bound 0 andalso not(loose_bvar1(s,0))
+ | None => false;
-fun extract conj = case dest_conj conj of
- Some(conj,P,Q) =>
- (case def P of
- Some eq => Some(eq,Q)
- | None =>
- (case def Q of
- Some eq => Some(eq,P)
- | None =>
- (case extract P of
- Some(eq,P') => Some(eq, conj $ P' $ Q)
- | None =>
- (case extract Q of
- Some(eq,Q') => Some(eq,conj $ P $ Q')
- | None => None))))
- | None => None;
+fun extract_conj t = case dest_conj t of None => None
+ | Some(conj,P,Q) =>
+ (if def P then Some(P,Q) else
+ if def Q then Some(Q,P) else
+ (case extract_conj P of
+ Some(eq,P') => Some(eq, conj $ P' $ Q)
+ | None => (case extract_conj Q of
+ Some(eq,Q') => Some(eq,conj $ P $ Q')
+ | None => None)));
+
+fun extract_imp t = case dest_imp t of None => None
+ | Some(imp,P,Q) => if def P then Some(P,Q)
+ else (case extract_conj P of
+ Some(eq,P') => Some(eq, imp $ P' $ Q)
+ | None => (case extract_imp Q of
+ None => None
+ | Some(eq,Q') => Some(eq, imp$P$Q')));
+
fun prove_conv tac sg tu =
let val meta_eq = cterm_of sg (Logic.mk_equals tu)
@@ -97,44 +103,44 @@
*)
val prove_one_point_ex_tac = rtac iffI 1 THEN
ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
- DEPTH_SOLVE_1 o (ares_tac [conjI] APPEND' etac sym)]);
+ DEPTH_SOLVE_1 o (ares_tac [conjI])]);
(* Proves (! x. (... & x = t & ...) --> P x) =
(! x. x = t --> (... & ...) --> P x)
*)
-val prove_one_point_all_tac = EVERY1[rtac iffI,
- rtac allI, etac allE, rtac impI, rtac impI, etac mp,
- REPEAT o (etac conjE),
- REPEAT o (ares_tac [conjI] ORELSE' etac sym),
- rtac allI, etac allE, rtac impI, REPEAT o (etac conjE),
- etac impE, atac ORELSE' etac sym, etac mp,
- REPEAT o (ares_tac [conjI])];
+local
+val tac = SELECT_GOAL
+ (EVERY1[REPEAT o (dtac uncurry), REPEAT o (rtac impI), etac mp,
+ REPEAT o (etac conjE), REPEAT o (ares_tac [conjI])])
+in
+val prove_one_point_all_tac = EVERY1[rtac iff_allI, rtac iffI, tac, tac]
+end
-fun rearrange_all sg _ (F as all $ Abs(x,T,(* --> *)_ $ P $ Q)) =
- (case extract P of
+fun rearrange_all sg _ (F as all $ Abs(x,T, P)) =
+ (case extract_imp P of
None => None
- | Some(eq,P') =>
- let val R = imp $ eq $ (imp $ P' $ Q)
+ | Some(eq,Q) =>
+ let val R = imp $ eq $ Q
in Some(prove_conv prove_one_point_all_tac sg (F,all$Abs(x,T,R))) end)
| rearrange_all _ _ _ = None;
-fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,(* --> *)_ $ P $ Q)) =
- (case extract P of
+fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,P)) =
+ (case extract_imp P of
None => None
- | Some(eq,P') =>
- let val R = imp $ eq $ (imp $ P' $ Q)
+ | Some(eq,Q) =>
+ let val R = imp $ eq $ Q
in Some(prove_conv tac sg (F,Ball $ A $ Abs(x,T,R))) end)
| rearrange_ball _ _ _ _ = None;
fun rearrange_ex sg _ (F as ex $ Abs(x,T,P)) =
- (case extract P of
+ (case extract_conj P of
None => None
| Some(eq,Q) =>
Some(prove_conv prove_one_point_ex_tac sg (F,ex $ Abs(x,T,conj$eq$Q))))
| rearrange_ex _ _ _ = None;
fun rearrange_bex tac sg _ (F as Bex $ A $ Abs(x,T,P)) =
- (case extract P of
+ (case extract_conj P of
None => None
| Some(eq,Q) =>
Some(prove_conv tac sg (F,Bex $ A $ Abs(x,T,conj$eq$Q))))