# HG changeset patch
# User nipkow
# Date 869672622 -7200
# Node ID 36ff1ab12021f21d31b794c47abbaf1c39c5a068
# Parent  e2539e1980b43e1ce409187b1ac2fa3febdebc0e
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
automate reasoning about products.

simpdata.ML: added simplification procedure for simplifying existential
statements of the form ? x. ... & x = t & ...

diff -r e2539e1980b4 -r 36ff1ab12021 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Wed Jul 23 16:03:19 1997 +0200
+++ b/src/HOL/Prod.ML	Wed Jul 23 17:43:42 1997 +0200
@@ -78,16 +78,62 @@
 
 end;
 
+(* Could be nice, but breaks too many proofs:
+claset := !claset addbefore split_all_tac;
+*)
+
+(*** lemmas for splitting paired `!!'
+Does not work with simplifier because it also affects premises in
+congrence rules, where is can lead to premises of the form
+!!a b. ... = ?P(a,b)
+which cannot be solved by reflexivity.
+   
+val [prem] = goal Prod.thy "(!!x.PROP P x) ==> (!!a b. PROP P(a,b))";
+br prem 1;
+val lemma1 = result();
+
+local
+    val psig = sign_of Prod.thy;
+    val pT = Sign.read_typ (psig, K None) "?'a*?'b=>prop";
+    val PeqP = reflexive(read_cterm psig ("P", pT));
+    val psplit = zero_var_indexes(read_instantiate [("p","x")]
+                                  surjective_pairing RS eq_reflection)
+in
+val adhoc = combination PeqP psplit
+end;
+
+
+val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> PROP P x";
+bw adhoc;
+br prem 1;
+val lemma = result();
+
+val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> (!!x. PROP P x)";
+br lemma 1;
+br prem 1;
+val lemma2 = result();
+
+bind_thm("split_paired_all", equal_intr lemma1 lemma2);
+Addsimps [split_paired_all];
+***)
+
 goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
 by (fast_tac (!claset addbefore split_all_tac) 1);
 qed "split_paired_All";
+Addsimps [split_paired_All];
+(* AddIffs is not a good idea because it makes Blast_tac loop *)
+
+goal Prod.thy "(? x. P x) = (? a b. P(a,b))";
+by (fast_tac (!claset addbefore split_all_tac) 1);
+qed "split_paired_Ex";
+(* Addsimps [split_paired_Ex]; breaks a number of IOA proofs *)
 
 goalw Prod.thy [split_def] "split c (a,b) = c a b";
 by (EVERY1[stac fst_conv, stac snd_conv]);
 by (rtac refl 1);
 qed "split";
 
-Addsimps [fst_conv, snd_conv, split_paired_All, split];
+Addsimps [fst_conv, snd_conv, split];
 
 goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
 by (res_inst_tac[("p","s")] PairE 1);
@@ -121,6 +167,12 @@
 by (Blast_tac 1);
 qed "expand_split";
 
+(* could be done after split_tac has been speeded up significantly:
+simpset := (!simpset setloop split_tac[expand_split]);
+   precompute the constants involved and don't do anything unless
+   the current goal contains one of those constants
+*)
+
 (** split used as a logical connective or set former **)
 
 (*These rules are for use with blast_tac.
@@ -252,7 +304,7 @@
 goal Prod.thy "((a,b): Sigma A B) = (a:A & b:B(a))";
 by (Blast_tac 1);
 qed "mem_Sigma_iff";
-Addsimps [mem_Sigma_iff]; 
+AddIffs [mem_Sigma_iff]; 
 
 
 (*Suggested by Pierre Chartier*)
diff -r e2539e1980b4 -r 36ff1ab12021 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Jul 23 16:03:19 1997 +0200
+++ b/src/HOL/simpdata.ML	Wed Jul 23 17:43:42 1997 +0200
@@ -103,8 +103,8 @@
    "(P | P) = P", "(P | (P | Q)) = (P | Q)",
    "((~P) = (~Q)) = (P=Q)",
    "(!x.P) = P", "(? x.P) = P", "? x. x=t", "? x. t=x", 
-   "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)", 
-   "(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ];
+   "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)",
+   "(! x. t=x --> P(x)) = P(t)" ];
 
 (*Add congruence rules for = (instead of ==) *)
 infix 4 addcongs delcongs;
@@ -138,6 +138,52 @@
                  "(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)
+ ***)
+
+local
+
+fun def(eq as (c as Const("op =",_)) $ 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
+  | def _ = None;
+
+fun extract(Const("op &",_) $ 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, HOLogic.conj $ P' $ Q)
+       | None => (case extract Q of
+                   Some(eq,Q') => Some(eq,HOLogic.conj $ P $ Q')
+                 | None => None))))
+  | extract _ = None;
+
+fun prove_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)) =
+     (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;
+
+val pattern = read_cterm (sign_of HOL.thy) ("? x.P(x) & Q(x)",HOLogic.boolT)
+
+in
+val defEX_regroup = mk_simproc "defined EX" [pattern] rearrange;
+end;
 
 
 (* elimination of existential quantifiers in assumptions *)
@@ -314,6 +360,7 @@
        de_Morgan_conj, de_Morgan_disj, not_imp,
        not_all, not_ex, cases_simp]
      @ ex_simps @ all_simps @ simp_thms)
+     addsimprocs [defEX_regroup]
      addcongs [imp_cong];
 
 qed_goal "if_distrib" HOL.thy