added split_prem_tac
authoroheimb
Fri Nov 07 18:05:25 1997 +0100 (1997-11-07)
changeset 4189b8c7a6bc6c16
parent 4188 1025a27b08f9
child 4190 e377947fe1ec
added split_prem_tac
NEWS
src/FOL/simpdata.ML
src/HOL/simpdata.ML
src/Provers/splitter.ML
     1.1 --- a/NEWS	Fri Nov 07 18:02:15 1997 +0100
     1.2 +++ b/NEWS	Fri Nov 07 18:05:25 1997 +0100
     1.3 @@ -95,6 +95,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* HOL: there is a new splitter `split_prem_tac' that can be used e.g. 
     1.8 +  with `addloop' of the simplifier to faciliate case splitting in premises.
     1.9 +
    1.10  * HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions;
    1.11  
    1.12  * HOL/Auth: new protocol proofs including some for the Internet
    1.13 @@ -121,13 +124,23 @@
    1.14    P(t_case f1 ... fn x) =
    1.15       ( (!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1)) &
    1.16          ...
    1.17 -        (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
    1.18 +       (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
    1.19       )
    1.20  
    1.21    which can be added to a simpset via `addsplits'. The existing theorems
    1.22    expand_list_case and expand_option_case have been renamed to
    1.23    split_list_case and split_option_case.
    1.24  
    1.25 +  Additionally, there is a theorem `split_t_case_prem' of the form
    1.26 +
    1.27 +  P(t_case f1 ... fn x) =
    1.28 +    ~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) |
    1.29 +        ...
    1.30 +       (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn))
    1.31 +     )
    1.32 +
    1.33 +  it be used with the new `split_prem_tac'.
    1.34 +
    1.35  * HOL/Lists: the function "set_of_list" has been renamed "set"
    1.36    (and its theorems too);
    1.37  
    1.38 @@ -162,6 +175,9 @@
    1.39  
    1.40  *** FOL and ZF ***
    1.41  
    1.42 +* FOL: there is a new splitter `split_prem_tac' that can be used e.g. 
    1.43 +  with `addloop' of the simplifier to faciliate case splitting in premises.
    1.44 +
    1.45  * qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as
    1.46  in HOL, they strip ALL and --> from proved theorems;
    1.47  
     2.1 --- a/src/FOL/simpdata.ML	Fri Nov 07 18:02:15 1997 +0100
     2.2 +++ b/src/FOL/simpdata.ML	Fri Nov 07 18:05:25 1997 +0100
     2.3 @@ -183,6 +183,8 @@
     2.4  fun split_inside_tac splits = mktac (map mk_meta_eq splits)
     2.5  end;
     2.6  
     2.7 +val split_prem_tac = mk_case_split_prem_tac split_tac disjE conjE exE contrapos
     2.8 +					    contrapos2 notnotD;
     2.9  
    2.10  (*** Standard simpsets ***)
    2.11  
     3.1 --- a/src/HOL/simpdata.ML	Fri Nov 07 18:02:15 1997 +0100
     3.2 +++ b/src/HOL/simpdata.ML	Fri Nov 07 18:05:25 1997 +0100
     3.3 @@ -364,6 +364,9 @@
     3.4  fun split_inside_tac splits = mktac (map mk_meta_eq splits)
     3.5  end;
     3.6  
     3.7 +val split_prem_tac = mk_case_split_prem_tac split_tac disjE conjE exE contrapos
     3.8 +					    contrapos2 notnotD;
     3.9 +
    3.10  infix 4 addsplits;
    3.11  fun ss addsplits splits = ss addloop (split_tac splits);
    3.12  
     4.1 --- a/src/Provers/splitter.ML	Fri Nov 07 18:02:15 1997 +0100
     4.2 +++ b/src/Provers/splitter.ML	Fri Nov 07 18:05:25 1997 +0100
     4.3 @@ -9,7 +9,7 @@
     4.4  
     4.5  val split_tac = mk_case_split_tac iffD;
     4.6  
     4.7 -by(case_split_tac splits i);
     4.8 +by(split_tac splits i);
     4.9  
    4.10  where splits = [P(elim(...)) == rhs, ...]
    4.11        iffD  = [| P <-> Q; Q |] ==> P (* is called iffD2 in HOL *)
    4.12 @@ -283,10 +283,60 @@
    4.13  
    4.14  in split_tac end;
    4.15  
    4.16 +
    4.17 +fun mk_case_split_prem_tac split_tac disjE conjE exE contrapos 
    4.18 +			   contrapos2 notnotD = 
    4.19 +let
    4.20 +
    4.21 +(*****************************************************************************
    4.22 +   The split-tactic for premises
    4.23 +   
    4.24 +   splits : list of split-theorems to be tried
    4.25 +   i      : number of subgoal the tactic should be applied to
    4.26 +*****************************************************************************)
    4.27 +
    4.28 +fun split_prem_tac []     = K no_tac
    4.29 +  | split_prem_tac splits = 
    4.30 +  let fun const thm =
    4.31 +            (case concl_of thm of Const ("Trueprop",_)$
    4.32 +				 (Const ("op =", _)$(Var _$t)$_) =>
    4.33 +               (case strip_comb t of (Const(a,_),_) => a
    4.34 +                | _ => error("Wrong format for split rule"))
    4.35 +             | _ =>    error("Wrong format for split rule"))
    4.36 +      val cname_list = map const splits;
    4.37 +      fun is_case (a,_) = a mem cname_list;
    4.38 +      fun tac (t,i) = 
    4.39 +	  let val n = find_index (exists_Const is_case) 
    4.40 +				 (Logic.strip_assums_hyp t);
    4.41 +	      fun first_prem_is_disj (Const ("==>", _) $ (Const ("Trueprop", _)
    4.42 +				 $ (Const ("op |", _) $ _ $ _ )) $ _ ) = true
    4.43 +	      |   first_prem_is_disj _ = false;
    4.44 +	      fun flat_prems_tac j = SUBGOAL (fn (t,i) => 
    4.45 +				   (if first_prem_is_disj t
    4.46 +				    then EVERY[etac disjE i, rotate_tac ~1 i,
    4.47 +					       rotate_tac ~1  (i+1),
    4.48 +					       flat_prems_tac (i+1)]
    4.49 +				    else all_tac) 
    4.50 +				   THEN REPEAT (eresolve_tac [conjE,exE] i)
    4.51 +				   THEN REPEAT (dresolve_tac [notnotD]   i)) j;
    4.52 +	  in if n<0 then no_tac else DETERM (EVERY'
    4.53 +		[rotate_tac n, etac contrapos2,
    4.54 +		 split_tac splits, 
    4.55 +		 rotate_tac ~1, etac contrapos, rotate_tac ~1, 
    4.56 +		 SELECT_GOAL (flat_prems_tac 1)] i)
    4.57 +	  end;
    4.58 +  in SUBGOAL tac
    4.59 +  end;
    4.60 +
    4.61 +in split_prem_tac end;
    4.62 +
    4.63 +
    4.64  in
    4.65  
    4.66  fun mk_case_split_tac iffD = mk_case_split_tac_2 iffD (op <=) ;
    4.67  
    4.68  fun mk_case_split_inside_tac iffD = mk_case_split_tac_2 iffD (op >=) ;
    4.69  
    4.70 +val mk_case_split_prem_tac = mk_case_split_prem_tac;
    4.71 +
    4.72  end;