renamed split_prem_tac to split_asm_tac
authoroheimb
Wed Nov 12 12:22:56 1997 +0100 (1997-11-12)
changeset 420296876d71eef5
parent 4201 858b3ec2c9db
child 4203 ca73de799b73
renamed split_prem_tac to split_asm_tac
split_asm_tac: simplification, debugged first_prem_is_disj
src/Provers/splitter.ML
     1.1 --- a/src/Provers/splitter.ML	Tue Nov 11 16:04:14 1997 +0100
     1.2 +++ b/src/Provers/splitter.ML	Wed Nov 12 12:22:56 1997 +0100
     1.3 @@ -284,8 +284,8 @@
     1.4  in split_tac end;
     1.5  
     1.6  
     1.7 -fun mk_case_split_prem_tac split_tac disjE conjE exE contrapos 
     1.8 -			   contrapos2 notnotD = 
     1.9 +fun mk_case_split_asm_tac split_tac 
    1.10 +			  (disjE,conjE,exE,contrapos,contrapos2,notnotD) = 
    1.11  let
    1.12  
    1.13  (*****************************************************************************
    1.14 @@ -295,8 +295,8 @@
    1.15     i      : number of subgoal the tactic should be applied to
    1.16  *****************************************************************************)
    1.17  
    1.18 -fun split_prem_tac []     = K no_tac
    1.19 -  | split_prem_tac splits = 
    1.20 +fun split_asm_tac []     = K no_tac
    1.21 +  | split_asm_tac splits = 
    1.22    let fun const thm =
    1.23              (case concl_of thm of Const ("Trueprop",_)$
    1.24  				 (Const ("op =", _)$(Var _$t)$_) =>
    1.25 @@ -310,25 +310,27 @@
    1.26  				 (Logic.strip_assums_hyp t);
    1.27  	      fun first_prem_is_disj (Const ("==>", _) $ (Const ("Trueprop", _)
    1.28  				 $ (Const ("op |", _) $ _ $ _ )) $ _ ) = true
    1.29 +	      |   first_prem_is_disj (Const("all",_)$Abs(_,_,t)) = 
    1.30 +					first_prem_is_disj t
    1.31  	      |   first_prem_is_disj _ = false;
    1.32 -	      fun flat_prems_tac j = SUBGOAL (fn (t,i) => 
    1.33 +	      fun flat_prems_tac i = SUBGOAL (fn (t,i) => 
    1.34  				   (if first_prem_is_disj t
    1.35  				    then EVERY[etac disjE i, rotate_tac ~1 i,
    1.36  					       rotate_tac ~1  (i+1),
    1.37  					       flat_prems_tac (i+1)]
    1.38  				    else all_tac) 
    1.39  				   THEN REPEAT (eresolve_tac [conjE,exE] i)
    1.40 -				   THEN REPEAT (dresolve_tac [notnotD]   i)) j;
    1.41 +				   THEN REPEAT (dresolve_tac [notnotD]   i)) i;
    1.42  	  in if n<0 then no_tac else DETERM (EVERY'
    1.43  		[rotate_tac n, etac contrapos2,
    1.44  		 split_tac splits, 
    1.45  		 rotate_tac ~1, etac contrapos, rotate_tac ~1, 
    1.46 -		 SELECT_GOAL (flat_prems_tac 1)] i)
    1.47 +		 flat_prems_tac] i)
    1.48  	  end;
    1.49    in SUBGOAL tac
    1.50    end;
    1.51  
    1.52 -in split_prem_tac end;
    1.53 +in split_asm_tac end;
    1.54  
    1.55  
    1.56  in
    1.57 @@ -337,6 +339,6 @@
    1.58  
    1.59  fun mk_case_split_inside_tac iffD = mk_case_split_tac_2 iffD (op >=) ;
    1.60  
    1.61 -val mk_case_split_prem_tac = mk_case_split_prem_tac;
    1.62 +val mk_case_split_asm_tac = mk_case_split_asm_tac;
    1.63  
    1.64  end;