--- 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;
--- 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 ***)
--- 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);
--- 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;