src/HOL/simpdata.ML
 changeset 4032 4b1c69d8b767 parent 3919 c036caebfc75 child 4086 958806f7e840
```--- a/src/HOL/simpdata.ML	Wed Oct 29 16:03:19 1997 +0100
+++ b/src/HOL/simpdata.ML	Thu Oct 30 09:45:03 1997 +0100
@@ -145,10 +145,22 @@
"(ALL x. P x --> Q) = ((EX x. P x) --> Q)",
"(ALL x. P --> Q x) = (P --> (ALL x. Q x))"];

-(*** Simplification procedure for turning  ? x. ... & x = t & ...
-     into                                  ? x. x = t & ... & ...
-     where the latter can be rewritten via (? x. x = t & P(x)) = P(t)
- ***)
+(*** Simplification procedures for turning
+
+            ? x. ... & x = t & ...
+     into   ? x. x = t & ... & ...
+     where the `? x. x = t &' in the latter formula is eliminated
+           by ordinary simplification.
+
+     and   ! x. (... & x = t & ...) --> P x
+     into  ! x. x = t --> (... & ...) --> P x
+     where the `!x. x=t -->' in the latter formula is eliminated
+           by ordinary simplification.
+
+NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)"
+   "!x. x=t --> P(x)" and "!x. t=x --> P(x)"
+   must be taken care of by ordinary rewrite rules.
+***)

local

@@ -171,25 +183,49 @@
| None => None))))
| extract _ = None;

-fun prove_eq(ceqt) =
+fun prove_ex_eq(ceqt) =
let val tac = rtac eq_reflection 1 THEN rtac iffI 1 THEN
ALLGOALS(EVERY'[etac exE, REPEAT o (etac conjE),
rtac exI, REPEAT o (ares_tac [conjI] ORELSE' etac sym)])
in rule_by_tactic tac (trivial ceqt) end;

-fun rearrange sg _ (F as ex \$ Abs(x,T,P)) =
+fun rearrange_ex sg _ (F as ex \$ Abs(x,T,P)) =
(case extract P of
None => None
| Some(eq,Q) =>
let val ceqt = cterm_of sg
(Logic.mk_equals(F,ex \$ Abs(x,T,HOLogic.conj\$eq\$Q)))
-          in Some(prove_eq ceqt) end)
-  | rearrange _ _ _ = None;
+          in Some(prove_ex_eq ceqt) end)
+  | rearrange_ex _ _ _ = None;
+
+val ex_pattern =
+  read_cterm (sign_of HOL.thy) ("? x. P(x) & Q(x)",HOLogic.boolT)

-val pattern = read_cterm (sign_of HOL.thy) ("? x. P(x) & Q(x)",HOLogic.boolT)
+fun prove_all_eq(ceqt) =
+  let fun tac _ = [EVERY1[rtac eq_reflection, 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])]]
+  in prove_goalw_cterm [] ceqt tac end;
+
+fun rearrange_all sg _ (F as all \$ Abs(x,T,Const("op -->",_)\$P\$Q)) =
+     (case extract P of
+        None => None
+      | Some(eq,P') =>
+          let val R = HOLogic.imp \$ eq \$ (HOLogic.imp \$ P' \$ Q)
+              val ceqt = cterm_of sg (Logic.mk_equals(F,all\$Abs(x,T,R)))
+          in Some(prove_all_eq ceqt) end)
+  | rearrange_all _ _ _ = None;
+
+val all_pattern =
+  read_cterm (sign_of HOL.thy) ("! x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)

in
-val defEX_regroup = mk_simproc "defined EX" [pattern] rearrange;
+val defEX_regroup = mk_simproc "defined EX" [ex_pattern] rearrange_ex;
+val defALL_regroup = mk_simproc "defined ALL" [all_pattern] rearrange_all;
end;

@@ -386,7 +422,7 @@
de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
not_all, not_ex, cases_simp]
@ ex_simps @ all_simps @ simp_thms)