# HG changeset patch
# User oheimb
# Date 936634729 -7200
# Node ID affcfd2830b7b87b4562e47f440a4bf09e878fbe
# Parent  45905028bb1d0ddcbd9beb72692131be701f7ef1
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc

diff -r 45905028bb1d -r affcfd2830b7 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Mon Sep 06 18:18:40 1999 +0200
+++ b/src/HOL/Prod.ML	Mon Sep 06 18:18:49 1999 +0200
@@ -33,14 +33,21 @@
 qed "Pair_eq";
 AddIffs [Pair_eq];
 
-Goalw [fst_def] "fst((a,b)) = a";
+Goalw [fst_def] "fst (a,b) = a";
 by (Blast_tac 1);
 qed "fst_conv";
-Goalw [snd_def] "snd((a,b)) = b";
+Goalw [snd_def] "snd (a,b) = b";
 by (Blast_tac 1);
 qed "snd_conv";
 Addsimps [fst_conv, snd_conv];
 
+Goal "fst (x, y) = a ==> x = a";
+by (Asm_full_simp_tac 1);
+qed "fst_eqD";
+Goal "snd (x, y) = a ==> y = a";
+by (Asm_full_simp_tac 1);
+qed "snd_eqD";
+
 Goalw [Pair_def] "? x y. p = (x,y)";
 by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1);
 by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
@@ -146,42 +153,54 @@
 
 (*simplification procedure for cond_split_eta. 
   using split_eta a rewrite rule is not general enough, and using 
-  cond_split_eta directly would render some existing proofs very inefficient*)
+  cond_split_eta directly would render some existing proofs very inefficient.
+  similarly for split_beta. *)
 local
-  val split_eta_pat = Thm.read_cterm (Theory.sign_of thy) 
-		("split (%x. split (%y. f x y))", HOLogic.termTVar);
-  val split_eta_meta_eq = standard (mk_meta_eq cond_split_eta);
-  fun  Pair_pat 0      (Bound 0) = true
-  |    Pair_pat k      (Const ("Pair",  _) $ Bound m $ t) = 
-			m = k andalso Pair_pat (k-1) t
-  |    Pair_pat _ _ = false;
-  fun split_pat k (Abs  (_, _, f $ 
-			(Const ("Pair",_) $ Bound m $ 
-			(Const ("Pair",_) $ Bound n $ t)))) =
-			if m = k andalso n = k-1 andalso Pair_pat (k-2) t
-			then Some f else None
-  |   split_pat k (Const ("split", _) $ Abs (_, _, t)) = split_pat (k+1) t
-  |   split_pat k _ = None;
-  fun proc sg _	(s as
-	(Const ("split", _) $ Abs (_, _, 
-	(Const ("split", _) $ Abs (_, _, t))))) = (case split_pat 2 t of
-	  Some f => (let val fvar = Free ("f", fastype_of f);
-			 fun atom_fun t = if t = f then fvar else atom t
-			 and atom     (Abs (x, T, t)) = Abs (x, T,atom_fun t)
-			   | atom     (t $ u)         = atom_fun t $ atom_fun u
-			   | atom     x               = x;
-			 val ct   = cterm_of sg (HOLogic.mk_Trueprop
-				   (HOLogic.mk_eq (atom_fun s,fvar)));
-			 val ss   = HOL_basic_ss addsimps [cond_split_eta];
-         in Some (mk_meta_eq (prove_goalw_cterm [] ct (K [simp_tac ss 1]))) end)
+  fun  Pair_pat k 0 (Bound m) = (m = k)
+  |    Pair_pat k i (Const ("Pair",  _) $ Bound m $ t) = i > 0 andalso
+			m = k+i andalso Pair_pat k (i-1) t
+  |    Pair_pat _ _ _ = false;
+  fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t
+  |   no_args k i (t $ u) = no_args k i t andalso no_args k i u
+  |   no_args k i (Bound m) = m < k orelse m > k+i
+  |   no_args _ _ _ = true;
+  fun split_pat tp i (Abs  (_,_,t)) = if tp 0 i t then Some (i,t) else None
+  |   split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
+  |   split_pat tp i _ = None;
+  fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm [] 
+	(cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
+	(K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
+  fun simproc name patstr = Simplifier.mk_simproc name 
+		[Thm.read_cterm (sign_of Prod.thy) (patstr, HOLogic.termTVar)];
+
+  val beta_patstr = "split f z";
+  val  eta_patstr = "split f";
+  fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
+  |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
+			(beta_term_pat k i t andalso beta_term_pat k i u)
+  |   beta_term_pat k i t = no_args k i t;
+  fun  eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg
+  |    eta_term_pat _ _ _ = false;
+  fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t)
+  |   subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg
+			      else (subst arg k i t $ subst arg k i u)
+  |   subst arg k i t = t;
+  fun beta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) = 
+	(case split_pat beta_term_pat 1 t of 
+	Some (i,f) => Some (metaeq sg s (subst arg 0 i f))
 	| None => None)
-  |   proc _ _ _ = None;
-
+  |   beta_proc _ _ _ = None;
+  fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) = 
+	(case split_pat eta_term_pat 1 t of
+	  Some (_,ft) => Some (metaeq sg s (let val (f $ arg) = ft in f end))
+ 	| None => None)
+  |   eta_proc _ _ _ = None;
 in
-  val split_eta_proc = Simplifier.mk_simproc "split_eta" [split_eta_pat] proc;
+  val split_beta_proc = simproc "split_beta" beta_patstr beta_proc;
+  val split_eta_proc  = simproc "split_eta"   eta_patstr  eta_proc;
 end;
 
-Addsimprocs [split_eta_proc];
+Addsimprocs [split_beta_proc,split_eta_proc];
 
 Goal "(%(x,y). P x y) z = P (fst z) (snd z)";
 by (stac surjective_pairing 1 THEN rtac split 1);