# HG changeset patch
# User oheimb
# Date 982691314 -3600
# Node ID 015af2fc7026a660081cccf17c3bcb2a99d244c1
# Parent  98c2f741e32bfecff412e3ef26cd750bde463fff
simplified proofs for splitI and splitD, added splitD'
added split_conv_tac (also to claset()) as an optimization
made split_all_tac safe introducing safe_full_simp_tac,EXISTING PROOFS MAY FAIL

diff -r 98c2f741e32b -r 015af2fc7026 src/HOL/Product_Type_lemmas.ML
--- a/src/HOL/Product_Type_lemmas.ML	Tue Feb 20 18:47:34 2001 +0100
+++ b/src/HOL/Product_Type_lemmas.ML	Tue Feb 20 18:48:34 2001 +0100
@@ -140,7 +140,9 @@
 which cannot be solved by reflexivity.
 *)
 
+
 (* replace parameters of product type by individual component parameters *)
+val safe_full_simp_tac = generic_simp_tac true (true, false, false);
 local
   fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) =
         can HOLogic.dest_prodT T orelse exists_paired_all t
@@ -152,13 +154,14 @@
     addsimprocs [unit_eq_proc];
 in
   val split_all_tac = SUBGOAL (fn (t, i) =>
+    if exists_paired_all t then safe_full_simp_tac ss i else no_tac);
+  val unsafe_split_all_tac = SUBGOAL (fn (t, i) =>
     if exists_paired_all t then full_simp_tac ss i else no_tac);
   fun split_all th =
-    if exists_paired_all (#prop (Thm.rep_thm th)) then full_simplify ss th else th;
+ if exists_paired_all (#prop (Thm.rep_thm th)) then full_simplify ss th else th;
 end;
 
-claset_ref() := claset()
-  addSWrapper ("split_all_tac", fn tac2 => split_all_tac ORELSE' tac2);
+claset_ref() := claset() addSbefore ("split_all_tac", split_all_tac);
 
 Goal "(!x. P x) = (!a b. P(a,b))";
 by (Fast_tac 1);
@@ -180,6 +183,9 @@
 Addsimps [split_conv];
 bind_thm ("split", split_conv);                  (*for compatibility*)
 
+bind_thm ("splitI", split_conv RS iffD2);
+bind_thm ("splitD", split_conv RS iffD1);
+
 (*Subsumes the old split_Pair when f is the identity function*)
 Goal "split (%x y. f(x,y)) = f";
 by (rtac ext 1);
@@ -310,10 +316,6 @@
 by (Asm_simp_tac 1);
 qed "splitI2'";
 
-Goal "c a b ==> split c (a,b)";
-by (Asm_simp_tac 1);
-qed "splitI";
-
 val prems = Goalw [split_def]
     "[| split c p;  !!x y. [| p = (x,y);  c x y |] ==> Q |] ==> Q";
 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
@@ -331,9 +333,9 @@
 by (rtac (split_beta RS subst) 1 THEN rtac major 1);
 qed "splitE2";
 
-Goal "split R (a,b) ==> R a b";
-by (etac (split_conv RS iffD1) 1);
-qed "splitD";
+Goal "split R (a,b) c ==> R a b c";
+by (Asm_full_simp_tac 1);
+qed "splitD'";
 
 Goal "z: c a b ==> z: split c (a,b)";
 by (Asm_simp_tac 1);
@@ -352,6 +354,12 @@
 AddSIs [splitI, splitI2, splitI2', mem_splitI, mem_splitI2];
 AddSEs [splitE, splitE', mem_splitE];
 
+(* Optimization: prevents applications of splitE for already splitted arguments
+leading to quite time-consuming computations (in particular for nested tuples)*)
+val split_conv_tac = let val ss = HOL_basic_ss addsimps [split_conv] in 
+  CHANGED o safe_full_simp_tac ss end;
+claset_ref() := claset() addSbefore ("split_conv_tac", split_conv_tac);
+
 Goal "(%u. ? x y. u = (x, y) & P (x, y)) = P";
 by (rtac ext 1);
 by (Fast_tac 1);
diff -r 98c2f741e32b -r 015af2fc7026 src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Tue Feb 20 18:47:34 2001 +0100
+++ b/src/HOL/UNITY/Extend.ML	Tue Feb 20 18:48:34 2001 +0100
@@ -753,6 +753,9 @@
 by (auto_tac (claset(), simpset() addsimps [ok_def]));  
 qed "ok_extend_iff";
 
+Unify.search_bound := 40;
+Unify.trace_bound  := 40;
+
 Goal "OK I (%i. extend h (F i)) = (OK I F)";
 by (auto_tac (claset(), simpset() addsimps [OK_def]));  
 by (dres_inst_tac [("x","i")] bspec 1); 
diff -r 98c2f741e32b -r 015af2fc7026 src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Tue Feb 20 18:47:34 2001 +0100
+++ b/src/HOL/UNITY/Lift_prog.ML	Tue Feb 20 18:48:34 2001 +0100
@@ -448,9 +448,10 @@
 Goal "[| ALL i:I. F i : preserves snd;  \
 \        ALL i:I. UNION (preserves fst) Acts <= AllowedActs (F i) |] \
 \     ==> OK I (%i. lift i (F i))";
-by (auto_tac (claset(), 
-      simpset() addsimps [OK_def, lift_def, rename_def, export Acts_extend,
-                export AllowedActs_extend, project_act_extend_act]));
+by (auto_tac (claset(),
+    simpset() addsimps [OK_def, lift_def, rename_def, export Acts_extend]));
+by (simp_tac (
+    simpset() addsimps [export AllowedActs_extend,project_act_extend_act]) 1);
 by (rename_tac "act" 1);
 by (subgoal_tac
     "{(x, x'). EX s f u s' f' u'.   \
diff -r 98c2f741e32b -r 015af2fc7026 src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Tue Feb 20 18:47:34 2001 +0100
+++ b/src/HOL/UNITY/Project.ML	Tue Feb 20 18:48:34 2001 +0100
@@ -202,8 +202,9 @@
 by (force_tac (claset() addSIs [reachable.Init],
 	       simpset() addsimps [split_extended_all]) 1);
 by Auto_tac;
-by (force_tac (claset() addIs [project_act_I RSN (3,reachable.Acts)],
-	       simpset()) 2);
+by (force_tac (claset() delSWrapper "split_all_tac" addSbefore 
+   ("unsafe_split_all_tac", unsafe_split_all_tac) 
+   addIs [project_act_I RSN (3,reachable.Acts)], simpset()) 2);
 by (res_inst_tac [("act","x")] reachable.Acts 1);
 by Auto_tac;
 by (etac extend_act_D 1);
@@ -247,12 +248,10 @@
 \        x : reachable (F Join project h C G) |] \
 \     ==> EX y. h(x,y) : reachable (extend h F Join G)";
 by (etac reachable.induct 1);
-by (ALLGOALS Asm_full_simp_tac);
-by (force_tac (claset() delrules [Id_in_Acts]
-		        addIs [reachable.Acts, extend_act_D],
-	       simpset() addsimps [project_act_def]) 2);
-by (force_tac (claset() addIs [reachable.Init],
-	       simpset()) 1);
+by  (force_tac (claset() addIs [reachable.Init], simpset()) 1);
+by (auto_tac (claset(), simpset()addsimps [project_act_def]));
+by (ALLGOALS (force_tac (claset() delrules [Id_in_Acts]
+		        addIs [reachable.Acts, extend_act_D], simpset())));
 qed "reachable_project_imp_reachable";
 
 Goal "project_set h (reachable (extend h F Join G)) = \
@@ -595,18 +594,20 @@
 (*** Guarantees ***)
 
 Goal "project_act h (Restrict C act) <= project_act h act";
-by (auto_tac (claset(), simpset() addsimps [project_act_def]));  
+by (auto_tac (claset(), simpset() addsimps [project_act_def]));
 qed "project_act_Restrict_subset_project_act";
 					   
 							   
 Goal "[| extend h F ok G; subset_closed (AllowedActs F) |] \
 \     ==> F ok project h C G";
 by (auto_tac (claset(), simpset() addsimps [ok_def]));
-by (dtac subsetD 1);   
-by (Blast_tac 1); 
-by (force_tac (claset() addSIs [rev_image_eqI], simpset()) 1);
+by (dtac subsetD 1);
+by (Blast_tac 1);
+by (force_tac (claset() delSWrapper "split_all_tac" addSbefore 
+                    ("unsafe_split_all_tac", unsafe_split_all_tac) 
+                     addSIs [rev_image_eqI], simpset()) 1);
 by (cut_facts_tac [project_act_Restrict_subset_project_act] 1);
-by (auto_tac (claset(), simpset() addsimps [subset_closed_def]));  
+by (auto_tac (claset(), simpset() addsimps [subset_closed_def]));
 qed "subset_closed_ok_extend_imp_ok_project";