src/Provers/splitter.ML
changeset 4189 b8c7a6bc6c16
parent 3918 94e0fdcb7b91
child 4202 96876d71eef5
     1.1 --- a/src/Provers/splitter.ML	Fri Nov 07 18:02:15 1997 +0100
     1.2 +++ b/src/Provers/splitter.ML	Fri Nov 07 18:05:25 1997 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  val split_tac = mk_case_split_tac iffD;
     1.6  
     1.7 -by(case_split_tac splits i);
     1.8 +by(split_tac splits i);
     1.9  
    1.10  where splits = [P(elim(...)) == rhs, ...]
    1.11        iffD  = [| P <-> Q; Q |] ==> P (* is called iffD2 in HOL *)
    1.12 @@ -283,10 +283,60 @@
    1.13  
    1.14  in split_tac end;
    1.15  
    1.16 +
    1.17 +fun mk_case_split_prem_tac split_tac disjE conjE exE contrapos 
    1.18 +			   contrapos2 notnotD = 
    1.19 +let
    1.20 +
    1.21 +(*****************************************************************************
    1.22 +   The split-tactic for premises
    1.23 +   
    1.24 +   splits : list of split-theorems to be tried
    1.25 +   i      : number of subgoal the tactic should be applied to
    1.26 +*****************************************************************************)
    1.27 +
    1.28 +fun split_prem_tac []     = K no_tac
    1.29 +  | split_prem_tac splits = 
    1.30 +  let fun const thm =
    1.31 +            (case concl_of thm of Const ("Trueprop",_)$
    1.32 +				 (Const ("op =", _)$(Var _$t)$_) =>
    1.33 +               (case strip_comb t of (Const(a,_),_) => a
    1.34 +                | _ => error("Wrong format for split rule"))
    1.35 +             | _ =>    error("Wrong format for split rule"))
    1.36 +      val cname_list = map const splits;
    1.37 +      fun is_case (a,_) = a mem cname_list;
    1.38 +      fun tac (t,i) = 
    1.39 +	  let val n = find_index (exists_Const is_case) 
    1.40 +				 (Logic.strip_assums_hyp t);
    1.41 +	      fun first_prem_is_disj (Const ("==>", _) $ (Const ("Trueprop", _)
    1.42 +				 $ (Const ("op |", _) $ _ $ _ )) $ _ ) = true
    1.43 +	      |   first_prem_is_disj _ = false;
    1.44 +	      fun flat_prems_tac j = SUBGOAL (fn (t,i) => 
    1.45 +				   (if first_prem_is_disj t
    1.46 +				    then EVERY[etac disjE i, rotate_tac ~1 i,
    1.47 +					       rotate_tac ~1  (i+1),
    1.48 +					       flat_prems_tac (i+1)]
    1.49 +				    else all_tac) 
    1.50 +				   THEN REPEAT (eresolve_tac [conjE,exE] i)
    1.51 +				   THEN REPEAT (dresolve_tac [notnotD]   i)) j;
    1.52 +	  in if n<0 then no_tac else DETERM (EVERY'
    1.53 +		[rotate_tac n, etac contrapos2,
    1.54 +		 split_tac splits, 
    1.55 +		 rotate_tac ~1, etac contrapos, rotate_tac ~1, 
    1.56 +		 SELECT_GOAL (flat_prems_tac 1)] i)
    1.57 +	  end;
    1.58 +  in SUBGOAL tac
    1.59 +  end;
    1.60 +
    1.61 +in split_prem_tac end;
    1.62 +
    1.63 +
    1.64  in
    1.65  
    1.66  fun mk_case_split_tac iffD = mk_case_split_tac_2 iffD (op <=) ;
    1.67  
    1.68  fun mk_case_split_inside_tac iffD = mk_case_split_tac_2 iffD (op >=) ;
    1.69  
    1.70 +val mk_case_split_prem_tac = mk_case_split_prem_tac;
    1.71 +
    1.72  end;