# HG changeset patch
# User oheimb
# Date 878922325 -3600
# Node ID b8c7a6bc6c169f6b1694e084cb017a35c30d415e
# Parent  1025a27b08f942d63465160df482472cfed25775
added split_prem_tac

diff -r 1025a27b08f9 -r b8c7a6bc6c16 NEWS
--- a/NEWS	Fri Nov 07 18:02:15 1997 +0100
+++ b/NEWS	Fri Nov 07 18:05:25 1997 +0100
@@ -95,6 +95,9 @@
 
 *** HOL ***
 
+* HOL: there is a new splitter `split_prem_tac' that can be used e.g. 
+  with `addloop' of the simplifier to faciliate case splitting in premises.
+
 * HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions;
 
 * HOL/Auth: new protocol proofs including some for the Internet
@@ -121,13 +124,23 @@
   P(t_case f1 ... fn x) =
      ( (!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1)) &
         ...
-        (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
+       (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
      )
 
   which can be added to a simpset via `addsplits'. The existing theorems
   expand_list_case and expand_option_case have been renamed to
   split_list_case and split_option_case.
 
+  Additionally, there is a theorem `split_t_case_prem' of the form
+
+  P(t_case f1 ... fn x) =
+    ~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) |
+        ...
+       (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn))
+     )
+
+  it be used with the new `split_prem_tac'.
+
 * HOL/Lists: the function "set_of_list" has been renamed "set"
   (and its theorems too);
 
@@ -162,6 +175,9 @@
 
 *** FOL and ZF ***
 
+* FOL: there is a new splitter `split_prem_tac' that can be used e.g. 
+  with `addloop' of the simplifier to faciliate case splitting in premises.
+
 * qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as
 in HOL, they strip ALL and --> from proved theorems;
 
diff -r 1025a27b08f9 -r b8c7a6bc6c16 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Fri Nov 07 18:02:15 1997 +0100
+++ b/src/FOL/simpdata.ML	Fri Nov 07 18:05:25 1997 +0100
@@ -183,6 +183,8 @@
 fun split_inside_tac splits = mktac (map mk_meta_eq splits)
 end;
 
+val split_prem_tac = mk_case_split_prem_tac split_tac disjE conjE exE contrapos
+					    contrapos2 notnotD;
 
 (*** Standard simpsets ***)
 
diff -r 1025a27b08f9 -r b8c7a6bc6c16 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Nov 07 18:02:15 1997 +0100
+++ b/src/HOL/simpdata.ML	Fri Nov 07 18:05:25 1997 +0100
@@ -364,6 +364,9 @@
 fun split_inside_tac splits = mktac (map mk_meta_eq splits)
 end;
 
+val split_prem_tac = mk_case_split_prem_tac split_tac disjE conjE exE contrapos
+					    contrapos2 notnotD;
+
 infix 4 addsplits;
 fun ss addsplits splits = ss addloop (split_tac splits);
 
diff -r 1025a27b08f9 -r b8c7a6bc6c16 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Fri Nov 07 18:02:15 1997 +0100
+++ b/src/Provers/splitter.ML	Fri Nov 07 18:05:25 1997 +0100
@@ -9,7 +9,7 @@
 
 val split_tac = mk_case_split_tac iffD;
 
-by(case_split_tac splits i);
+by(split_tac splits i);
 
 where splits = [P(elim(...)) == rhs, ...]
       iffD  = [| P <-> Q; Q |] ==> P (* is called iffD2 in HOL *)
@@ -283,10 +283,60 @@
 
 in split_tac end;
 
+
+fun mk_case_split_prem_tac split_tac disjE conjE exE contrapos 
+			   contrapos2 notnotD = 
+let
+
+(*****************************************************************************
+   The split-tactic for premises
+   
+   splits : list of split-theorems to be tried
+   i      : number of subgoal the tactic should be applied to
+*****************************************************************************)
+
+fun split_prem_tac []     = K no_tac
+  | split_prem_tac splits = 
+  let fun const thm =
+            (case concl_of thm of Const ("Trueprop",_)$
+				 (Const ("op =", _)$(Var _$t)$_) =>
+               (case strip_comb t of (Const(a,_),_) => a
+                | _ => error("Wrong format for split rule"))
+             | _ =>    error("Wrong format for split rule"))
+      val cname_list = map const splits;
+      fun is_case (a,_) = a mem cname_list;
+      fun tac (t,i) = 
+	  let val n = find_index (exists_Const is_case) 
+				 (Logic.strip_assums_hyp t);
+	      fun first_prem_is_disj (Const ("==>", _) $ (Const ("Trueprop", _)
+				 $ (Const ("op |", _) $ _ $ _ )) $ _ ) = true
+	      |   first_prem_is_disj _ = false;
+	      fun flat_prems_tac j = SUBGOAL (fn (t,i) => 
+				   (if first_prem_is_disj t
+				    then EVERY[etac disjE i, rotate_tac ~1 i,
+					       rotate_tac ~1  (i+1),
+					       flat_prems_tac (i+1)]
+				    else all_tac) 
+				   THEN REPEAT (eresolve_tac [conjE,exE] i)
+				   THEN REPEAT (dresolve_tac [notnotD]   i)) j;
+	  in if n<0 then no_tac else DETERM (EVERY'
+		[rotate_tac n, etac contrapos2,
+		 split_tac splits, 
+		 rotate_tac ~1, etac contrapos, rotate_tac ~1, 
+		 SELECT_GOAL (flat_prems_tac 1)] i)
+	  end;
+  in SUBGOAL tac
+  end;
+
+in split_prem_tac end;
+
+
 in
 
 fun mk_case_split_tac iffD = mk_case_split_tac_2 iffD (op <=) ;
 
 fun mk_case_split_inside_tac iffD = mk_case_split_tac_2 iffD (op >=) ;
 
+val mk_case_split_prem_tac = mk_case_split_prem_tac;
+
 end;