author nipkow Fri, 23 Mar 2001 10:12:12 +0100 changeset 11221 60c6e91f6079 parent 11220 db536a42dfc5 child 11222 72c5997e1145
```--- a/src/Provers/quantifier1.ML	Fri Mar 23 10:10:53 2001 +0100
+++ b/src/Provers/quantifier1.ML	Fri Mar 23 10:12:12 2001 +0100
@@ -19,6 +19,8 @@
"!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.

+     And similarly for the bounded quantifiers.
+
Gries etc call this the "1 point rules"
*)

@@ -46,8 +48,12 @@

signature QUANTIFIER1 =
sig
+  val prove_one_point_all_tac: tactic
+  val prove_one_point_ex_tac: tactic
val rearrange_all: Sign.sg -> thm list -> term -> thm option
val rearrange_ex:  Sign.sg -> thm list -> term -> thm option
+  val rearrange_ball: tactic -> Sign.sg -> thm list -> term -> thm option
+  val rearrange_bex:  tactic -> Sign.sg -> thm list -> term -> thm option
end;

functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
@@ -86,7 +92,17 @@
string_of_cterm meta_eq)
end;

-val prove_all_tac = EVERY1[rtac iffI,
+(* Proves (? x. ... & x = t & ...) = (? x. x = t & ... & ...)
+   Better: instantiate exI
+*)
+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)]);
+
+(* 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),
@@ -99,19 +115,29 @@
None => None
| Some(eq,P') =>
let val R = imp \$ eq \$ (imp \$ P' \$ Q)
-          in Some(prove_conv prove_all_tac sg (F,all\$Abs(x,T,R))) end)
+          in Some(prove_conv prove_one_point_all_tac sg (F,all\$Abs(x,T,R))) end)
| rearrange_all _ _ _ = None;

-(* Better: instantiate exI *)
-val prove_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)]);
+fun rearrange_ball tac sg _ (F as Ball \$ A \$ Abs(x,T,(* --> *)_ \$ P \$ Q)) =
+     (case extract P of
+        None => None
+      | Some(eq,P') =>
+          let val R = imp \$ eq \$ (imp \$ P' \$ 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
None => None
| Some(eq,Q) =>
-          Some(prove_conv prove_ex_tac sg (F,ex \$ Abs(x,T,conj\$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
+        None => None
+      | Some(eq,Q) =>
+          Some(prove_conv tac sg (F,Bex \$ A \$ Abs(x,T,conj\$eq\$Q))))
+  | rearrange_bex _ _ _ _ = None;
+
end;```