src/Pure/tactic.ML
changeset 1458 fd510875fb71
parent 1209 03dc596b3a18
child 1460 5a6f2aabd538
     1.1 --- a/src/Pure/tactic.ML	Mon Jan 29 13:50:10 1996 +0100
     1.2 +++ b/src/Pure/tactic.ML	Mon Jan 29 13:56:41 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	tactic
     1.5 +(*  Title:      tactic
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1991  University of Cambridge
    1.10  
    1.11  Tactics 
    1.12 @@ -83,8 +83,8 @@
    1.13  
    1.14  
    1.15  functor TacticFun (structure Logic: LOGIC and Drule: DRULE and 
    1.16 -		   Tactical: TACTICAL and Net: NET
    1.17 -	  sharing Drule.Thm = Tactical.Thm) : TACTIC = 
    1.18 +                   Tactical: TACTICAL and Net: NET
    1.19 +          sharing Drule.Thm = Tactical.Thm) : TACTIC = 
    1.20  struct
    1.21  structure Tactical = Tactical;
    1.22  structure Thm = Tactical.Thm;
    1.23 @@ -97,9 +97,9 @@
    1.24  (*Discover what goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
    1.25  fun trace_goalno_tac tf i = Tactic (fn state => 
    1.26      case Sequence.pull(tapply(tf i, state)) of
    1.27 -	None    => Sequence.null
    1.28 +        None    => Sequence.null
    1.29        | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 
    1.30 -    			 Sequence.seqof(fn()=> seqcell)));
    1.31 +                         Sequence.seqof(fn()=> seqcell)));
    1.32  
    1.33  fun string_of (a,0) = a
    1.34    | string_of (a,i) = a ^ "_" ^ string_of_int i;
    1.35 @@ -109,22 +109,22 @@
    1.36    let val fth = freezeT th
    1.37        val {prop,sign,...} = rep_thm fth
    1.38        fun mk_inst (Var(v,T)) = 
    1.39 -	  (cterm_of sign (Var(v,T)),
    1.40 -	   cterm_of sign (Free(string_of v, T)))
    1.41 +          (cterm_of sign (Var(v,T)),
    1.42 +           cterm_of sign (Free(string_of v, T)))
    1.43        val insts = map mk_inst (term_vars prop)
    1.44    in  instantiate ([],insts) fth  end;
    1.45  
    1.46  (*Makes a rule by applying a tactic to an existing rule*)
    1.47  fun rule_by_tactic (Tactic tf) rl =
    1.48      case Sequence.pull(tf (freeze (standard rl))) of
    1.49 -	None        => raise THM("rule_by_tactic", 0, [rl])
    1.50 +        None        => raise THM("rule_by_tactic", 0, [rl])
    1.51        | Some(rl',_) => standard rl';
    1.52   
    1.53  (*** Basic tactics ***)
    1.54  
    1.55  (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
    1.56  fun PRIMSEQ thmfun = Tactic (fn state => thmfun state
    1.57 -			                 handle THM _ => Sequence.null);
    1.58 +                                         handle THM _ => Sequence.null);
    1.59  
    1.60  (*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
    1.61  fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun);
    1.62 @@ -164,9 +164,9 @@
    1.63  fun dresolve_tac rls = eresolve_tac (map make_elim rls);
    1.64  
    1.65  (*Shorthand versions: for resolution with a single theorem*)
    1.66 -fun rtac rl = resolve_tac [rl];
    1.67 -fun etac rl = eresolve_tac [rl];
    1.68 -fun dtac rl = dresolve_tac [rl];
    1.69 +fun rtac rl = rtac rl ;
    1.70 +fun etac rl = etac rl ;
    1.71 +fun dtac rl = dtac rl ;
    1.72  val atac = assume_tac;
    1.73  
    1.74  (*Use an assumption or some rules ... A popular combination!*)
    1.75 @@ -185,19 +185,19 @@
    1.76  fun lift_inst_rule (state, i, sinsts, rule) =
    1.77  let val {maxidx,sign,...} = rep_thm state
    1.78      val (_, _, Bi, _) = dest_state(state,i)
    1.79 -    val params = Logic.strip_params Bi	        (*params of subgoal i*)
    1.80 +    val params = Logic.strip_params Bi          (*params of subgoal i*)
    1.81      val params = rev(rename_wrt_term Bi params) (*as they are printed*)
    1.82      val paramTs = map #2 params
    1.83      and inc = maxidx+1
    1.84      fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T)
    1.85        | liftvar t = raise TERM("Variable expected", [t]);
    1.86      fun liftterm t = list_abs_free (params, 
    1.87 -				    Logic.incr_indexes(paramTs,inc) t)
    1.88 +                                    Logic.incr_indexes(paramTs,inc) t)
    1.89      (*Lifts instantiation pair over params*)
    1.90      fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
    1.91      fun lifttvar((a,i),ctyp) =
    1.92 -	let val {T,sign} = rep_ctyp ctyp
    1.93 -	in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
    1.94 +        let val {T,sign} = rep_ctyp ctyp
    1.95 +        in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
    1.96      val rts = types_sorts rule and (types,sorts) = types_sorts state
    1.97      fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
    1.98        | types'(ixn) = types ixn;
    1.99 @@ -215,10 +215,10 @@
   1.100  (*compose version: arguments are as for bicompose.*)
   1.101  fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i =
   1.102    STATE ( fn state => 
   1.103 -	   compose_tac (bires_flg, lift_inst_rule (state, i, sinsts, rule),
   1.104 -			nsubgoal) i
   1.105 -	   handle TERM (msg,_) => (writeln msg;  no_tac)
   1.106 -		| THM  (msg,_,_) => (writeln msg;  no_tac) );
   1.107 +           compose_tac (bires_flg, lift_inst_rule (state, i, sinsts, rule),
   1.108 +                        nsubgoal) i
   1.109 +           handle TERM (msg,_) => (writeln msg;  no_tac)
   1.110 +                | THM  (msg,_,_) => (writeln msg;  no_tac) );
   1.111  
   1.112  (*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
   1.113    terms that are substituted contain (term or type) unknowns from the
   1.114 @@ -242,8 +242,8 @@
   1.115    let val {maxidx,...} = rep_thm rl
   1.116        fun cvar ixn = cterm_of Sign.proto_pure (Var(ixn,propT));
   1.117        val revcut_rl' = 
   1.118 -	  instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
   1.119 -			     (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
   1.120 +          instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
   1.121 +                             (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
   1.122        val arg = (false, rl, nprems_of rl)
   1.123        val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl')
   1.124    in  th  end
   1.125 @@ -262,7 +262,7 @@
   1.126  
   1.127  (*Used by metacut_tac*)
   1.128  fun bires_cut_tac arg i =
   1.129 -    resolve_tac [cut_rl] i  THEN  biresolve_tac arg (i+1) ;
   1.130 +    rtac cut_rl i  THEN  biresolve_tac arg (i+1) ;
   1.131  
   1.132  (*The conclusion of the rule gets assumed in subgoal i,
   1.133    while subgoal i+1,... are the premises of the rule.*)
   1.134 @@ -271,7 +271,7 @@
   1.135  (*Recognizes theorems that are not rules, but simple propositions*)
   1.136  fun is_fact rl =
   1.137      case prems_of rl of
   1.138 -	[] => true  |  _::_ => false;
   1.139 +        [] => true  |  _::_ => false;
   1.140  
   1.141  (*"Cut" all facts from theorem list into the goal as assumptions. *)
   1.142  fun cut_facts_tac ths i =
   1.143 @@ -287,15 +287,15 @@
   1.144  (**** Indexing and filtering of theorems ****)
   1.145  
   1.146  (*Returns the list of potentially resolvable theorems for the goal "prem",
   1.147 -	using the predicate  could(subgoal,concl).
   1.148 +        using the predicate  could(subgoal,concl).
   1.149    Resulting list is no longer than "limit"*)
   1.150  fun filter_thms could (limit, prem, ths) =
   1.151    let val pb = Logic.strip_assums_concl prem;   (*delete assumptions*)
   1.152        fun filtr (limit, []) = []
   1.153 -	| filtr (limit, th::ths) =
   1.154 -	    if limit=0 then  []
   1.155 -	    else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
   1.156 -	    else filtr(limit,ths)
   1.157 +        | filtr (limit, th::ths) =
   1.158 +            if limit=0 then  []
   1.159 +            else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
   1.160 +            else filtr(limit,ths)
   1.161    in  filtr(limit,ths)  end;
   1.162  
   1.163  
   1.164 @@ -320,9 +320,9 @@
   1.165  (*insert one tagged brl into the pair of nets*)
   1.166  fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) =
   1.167      if eres then 
   1.168 -	case prems_of th of
   1.169 -	    prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false))
   1.170 -	  | [] => error"insert_tagged_brl: elimination rule with no premises"
   1.171 +        case prems_of th of
   1.172 +            prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false))
   1.173 +          | [] => error"insert_tagged_brl: elimination rule with no premises"
   1.174      else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet);
   1.175  
   1.176  (*build a pair of nets for biresolution*)
   1.177 @@ -366,9 +366,9 @@
   1.178      (fn (prem,i) =>
   1.179        let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
   1.180        in 
   1.181 -	 if pred krls  
   1.182 +         if pred krls  
   1.183           then PRIMSEQ
   1.184 -		(biresolution match (map (pair false) (orderlist krls)) i)
   1.185 +                (biresolution match (map (pair false) (orderlist krls)) i)
   1.186           else no_tac
   1.187        end);
   1.188  
   1.189 @@ -414,7 +414,7 @@
   1.190  (*Rewrite subgoals only, not main goal. *)
   1.191  fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
   1.192  
   1.193 -fun rewtac def = rewrite_goals_tac [def];
   1.194 +fun rewtac def = rewtac def;
   1.195  
   1.196  
   1.197  (*** Tactic for folding definitions, handling critical pairs ***)
   1.198 @@ -451,7 +451,7 @@
   1.199    in  
   1.200    if !Logic.auto_rename 
   1.201    then (writeln"Note: setting Logic.auto_rename := false"; 
   1.202 -	Logic.auto_rename := false)
   1.203 +        Logic.auto_rename := false)
   1.204    else ();
   1.205    case #2 (take_prefix (is_letdig orf is_blank) cs) of
   1.206        [] => PRIMITIVE (rename_params_rule (scanwords is_letdig cs, i))