# HG changeset patch
# User wenzelm
# Date 978812832 -3600
# Node ID 89a29437cebcb334b78e3b27190d24d3a0681966
# Parent  306aee77eaddf4238dfdcd2d96bcb668a0814a39
added norm_hhf(_tac);

diff -r 306aee77eadd -r 89a29437cebc src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Sat Jan 06 21:26:27 2001 +0100
+++ b/src/Pure/tactic.ML	Sat Jan 06 21:27:12 2001 +0100
@@ -1,105 +1,107 @@
-(*  Title: 	Pure/tactic.ML
+(*  Title:      Pure/tactic.ML
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-Tactics 
+Tactics.
 *)
 
 signature TACTIC =
   sig
-  val ares_tac		: thm list -> int -> tactic
+  val ares_tac          : thm list -> int -> tactic
   val asm_rewrite_goal_tac:
     bool*bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
-  val assume_tac	: int -> tactic
-  val atac	: int ->tactic
+  val assume_tac        : int -> tactic
+  val atac      : int ->tactic
   val bimatch_from_nets_tac: 
       (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
-  val bimatch_tac	: (bool*thm)list -> int -> tactic
+  val bimatch_tac       : (bool*thm)list -> int -> tactic
   val biresolution_from_nets_tac: 
-	('a list -> (bool * thm) list) ->
-	bool -> 'a Net.net * 'a Net.net -> int -> tactic
+        ('a list -> (bool * thm) list) ->
+        bool -> 'a Net.net * 'a Net.net -> int -> tactic
   val biresolve_from_nets_tac: 
       (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
-  val biresolve_tac	: (bool*thm)list -> int -> tactic
-  val build_net	: thm list -> (int*thm) Net.net
+  val biresolve_tac     : (bool*thm)list -> int -> tactic
+  val build_net : thm list -> (int*thm) Net.net
   val build_netpair:    (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net ->
       (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net
-  val compose_inst_tac	: (string*string)list -> (bool*thm*int) -> 
+  val compose_inst_tac  : (string*string)list -> (bool*thm*int) -> 
                           int -> tactic
-  val compose_tac	: (bool * thm * int) -> int -> tactic 
-  val cut_facts_tac	: thm list -> int -> tactic
-  val cut_inst_tac	: (string*string)list -> thm -> int -> tactic   
+  val compose_tac       : (bool * thm * int) -> int -> tactic 
+  val cut_facts_tac     : thm list -> int -> tactic
+  val cut_inst_tac      : (string*string)list -> thm -> int -> tactic   
   val datac             : thm -> int -> int -> tactic
-  val defer_tac 	: int -> tactic
-  val distinct_subgoals_tac	: tactic
-  val dmatch_tac	: thm list -> int -> tactic
-  val dresolve_tac	: thm list -> int -> tactic
-  val dres_inst_tac	: (string*string)list -> thm -> int -> tactic   
-  val dtac		: thm -> int ->tactic
+  val defer_tac         : int -> tactic
+  val distinct_subgoals_tac     : tactic
+  val dmatch_tac        : thm list -> int -> tactic
+  val dresolve_tac      : thm list -> int -> tactic
+  val dres_inst_tac     : (string*string)list -> thm -> int -> tactic   
+  val dtac              : thm -> int ->tactic
   val eatac             : thm -> int -> int -> tactic
-  val etac		: thm -> int ->tactic
-  val eq_assume_tac	: int -> tactic   
-  val ematch_tac	: thm list -> int -> tactic
-  val eresolve_tac	: thm list -> int -> tactic
-  val eres_inst_tac	: (string*string)list -> thm -> int -> tactic
+  val etac              : thm -> int ->tactic
+  val eq_assume_tac     : int -> tactic   
+  val ematch_tac        : thm list -> int -> tactic
+  val eresolve_tac      : thm list -> int -> tactic
+  val eres_inst_tac     : (string*string)list -> thm -> int -> tactic
   val fatac             : thm -> int -> int -> tactic
   val filter_prems_tac  : (term -> bool) -> int -> tactic  
-  val filter_thms	: (term*term->bool) -> int*term*thm list -> thm list
-  val filt_resolve_tac	: thm list -> int -> int -> tactic
-  val flexflex_tac	: tactic
-  val fold_goals_tac	: thm list -> tactic
-  val fold_rule		: thm list -> thm -> thm
-  val fold_tac		: thm list -> tactic
-  val forward_tac	: thm list -> int -> tactic   
-  val forw_inst_tac	: (string*string)list -> thm -> int -> tactic
-  val ftac		: thm -> int ->tactic
+  val filter_thms       : (term*term->bool) -> int*term*thm list -> thm list
+  val filt_resolve_tac  : thm list -> int -> int -> tactic
+  val flexflex_tac      : tactic
+  val fold_goals_tac    : thm list -> tactic
+  val fold_rule         : thm list -> thm -> thm
+  val fold_tac          : thm list -> tactic
+  val forward_tac       : thm list -> int -> tactic   
+  val forw_inst_tac     : (string*string)list -> thm -> int -> tactic
+  val ftac              : thm -> int ->tactic
   val insert_tagged_brl : ('a*(bool*thm)) * 
                           (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
                           ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
-  val delete_tagged_brl	: (bool*thm) * 
+  val delete_tagged_brl : (bool*thm) * 
                          ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) ->
                     (int*(bool*thm))Net.net * (int*(bool*thm))Net.net
-  val is_fact		: thm -> bool
-  val lessb		: (bool * thm) * (bool * thm) -> bool
-  val lift_inst_rule	: thm * int * (string*string)list * thm -> thm
-  val make_elim		: thm -> thm
-  val match_from_net_tac	: (int*thm) Net.net -> int -> tactic
-  val match_tac	: thm list -> int -> tactic
-  val metacut_tac	: thm -> int -> tactic
-  val net_bimatch_tac	: (bool*thm) list -> int -> tactic
-  val net_biresolve_tac	: (bool*thm) list -> int -> tactic
-  val net_match_tac	: thm list -> int -> tactic
-  val net_resolve_tac	: thm list -> int -> tactic
-  val orderlist		: (int * 'a) list -> 'a list
-  val PRIMITIVE		: (thm -> thm) -> tactic  
-  val PRIMSEQ		: (thm -> thm Seq.seq) -> tactic  
-  val prune_params_tac	: tactic
-  val rename_params_tac	: string list -> int -> tactic
-  val rename_tac	: string -> int -> tactic
-  val rename_last_tac	: string -> string list -> int -> tactic
-  val resolve_from_net_tac	: (int*thm) Net.net -> int -> tactic
-  val resolve_tac	: thm list -> int -> tactic
-  val res_inst_tac	: (string*string)list -> thm -> int -> tactic   
+  val is_fact           : thm -> bool
+  val lessb             : (bool * thm) * (bool * thm) -> bool
+  val lift_inst_rule    : thm * int * (string*string)list * thm -> thm
+  val make_elim         : thm -> thm
+  val match_from_net_tac        : (int*thm) Net.net -> int -> tactic
+  val match_tac : thm list -> int -> tactic
+  val metacut_tac       : thm -> int -> tactic
+  val net_bimatch_tac   : (bool*thm) list -> int -> tactic
+  val net_biresolve_tac : (bool*thm) list -> int -> tactic
+  val net_match_tac     : thm list -> int -> tactic
+  val net_resolve_tac   : thm list -> int -> tactic
+  val norm_hhf          : thm -> thm
+  val norm_hhf_tac      : int -> tactic
+  val orderlist         : (int * 'a) list -> 'a list
+  val PRIMITIVE         : (thm -> thm) -> tactic  
+  val PRIMSEQ           : (thm -> thm Seq.seq) -> tactic  
+  val prune_params_tac  : tactic
+  val rename_params_tac : string list -> int -> tactic
+  val rename_tac        : string -> int -> tactic
+  val rename_last_tac   : string -> string list -> int -> tactic
+  val resolve_from_net_tac      : (int*thm) Net.net -> int -> tactic
+  val resolve_tac       : thm list -> int -> tactic
+  val res_inst_tac      : (string*string)list -> thm -> int -> tactic   
   val rewrite_goal_tac  : thm list -> int -> tactic
   val rewrite_goals_rule: thm list -> thm -> thm
-  val rewrite_rule	: thm list -> thm -> thm
-  val rewrite_goals_tac	: thm list -> tactic
-  val rewrite_tac	: thm list -> tactic
-  val rewtac		: thm -> tactic
-  val rotate_tac	: int -> int -> tactic
-  val rtac		: thm -> int -> tactic
-  val rule_by_tactic	: tactic -> thm -> thm
-  val solve_tac		: thm list -> int -> tactic
-  val subgoal_tac	: string -> int -> tactic
-  val subgoals_tac	: string list -> int -> tactic
-  val subgoals_of_brl	: bool * thm -> int
-  val term_lift_inst_rule	:
+  val rewrite_rule      : thm list -> thm -> thm
+  val rewrite_goals_tac : thm list -> tactic
+  val rewrite_tac       : thm list -> tactic
+  val rewtac            : thm -> tactic
+  val rotate_tac        : int -> int -> tactic
+  val rtac              : thm -> int -> tactic
+  val rule_by_tactic    : tactic -> thm -> thm
+  val solve_tac         : thm list -> int -> tactic
+  val subgoal_tac       : string -> int -> tactic
+  val subgoals_tac      : string list -> int -> tactic
+  val subgoals_of_brl   : bool * thm -> int
+  val term_lift_inst_rule       :
       thm * int * (indexname*typ)list * ((indexname*typ)*term)list  * thm
       -> thm
   val instantiate_tac   : (string * string) list -> tactic
-  val thin_tac		: string -> int -> tactic
-  val trace_goalno_tac	: (int -> tactic) -> int -> tactic
+  val thin_tac          : string -> int -> tactic
+  val trace_goalno_tac  : (int -> tactic) -> int -> tactic
   end;
 
 
@@ -109,15 +111,15 @@
 (*Discover which goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
 fun trace_goalno_tac tac i st =  
     case Seq.pull(tac i st) of
-	None    => Seq.empty
+        None    => Seq.empty
       | seqcell => (writeln ("Subgoal " ^ string_of_int i ^ " selected"); 
-    			 Seq.make(fn()=> seqcell));
+                         Seq.make(fn()=> seqcell));
 
 (*Makes a rule by applying a tactic to an existing rule*)
 fun rule_by_tactic tac rl =
   let val (st, thaw) = freeze_thaw (zero_var_indexes rl)
   in case Seq.pull (tac st)  of
-	None        => raise THM("rule_by_tactic", 0, [rl])
+        None        => raise THM("rule_by_tactic", 0, [rl])
       | Some(st',_) => Thm.varifyT (thaw st')
   end;
  
@@ -194,10 +196,10 @@
 in
 fun distinct_subgoals_tac state = 
     let val (frozth,thawfn) = freeze_thaw state
-	val froz_prems = cprems_of frozth
-	val assumed = implies_elim_list frozth (map assume froz_prems)
-	val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems)
-					assumed;
+        val froz_prems = cprems_of frozth
+        val assumed = implies_elim_list frozth (map assume froz_prems)
+        val implied = implies_intr_list (gen_distinct cterm_aconv froz_prems)
+                                        assumed;
     in  Seq.single (thawfn implied)  end
 end; 
 
@@ -206,19 +208,19 @@
 fun lift_inst_rule (st, i, sinsts, rule) =
 let val {maxidx,sign,...} = rep_thm st
     val (_, _, Bi, _) = dest_state(st,i)
-    val params = Logic.strip_params Bi	        (*params of subgoal i*)
+    val params = Logic.strip_params Bi          (*params of subgoal i*)
     val params = rev(rename_wrt_term Bi params) (*as they are printed*)
     val paramTs = map #2 params
     and inc = maxidx+1
     fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T)
       | liftvar t = raise TERM("Variable expected", [t]);
     fun liftterm t = list_abs_free (params, 
-				    Logic.incr_indexes(paramTs,inc) t)
+                                    Logic.incr_indexes(paramTs,inc) t)
     (*Lifts instantiation pair over params*)
     fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
     fun lifttvar((a,i),ctyp) =
-	let val {T,sign} = rep_ctyp ctyp
-	in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
+        let val {T,sign} = rep_ctyp ctyp
+        in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
     val rts = types_sorts rule and (types,sorts) = types_sorts st
     fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
       | types'(ixn) = types ixn;
@@ -267,7 +269,7 @@
   else st |>
     (compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule), nsubgoal) i
      handle TERM (msg,_)   => (writeln msg;  no_tac)
-	  | THM  (msg,_,_) => (writeln msg;  no_tac));
+          | THM  (msg,_,_) => (writeln msg;  no_tac));
 
 (*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
   terms that are substituted contain (term or type) unknowns from the
@@ -291,8 +293,8 @@
   let val {maxidx,...} = rep_thm rl
       fun cvar ixn = cterm_of (Theory.sign_of ProtoPure.thy) (Var(ixn,propT));
       val revcut_rl' = 
-	  instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
-			     (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
+          instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
+                             (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
       val arg = (false, rl, nprems_of rl)
       val [th] = Seq.list_of (bicompose false arg 1 revcut_rl')
   in  th  end
@@ -326,7 +328,7 @@
 (*Recognizes theorems that are not rules, but simple propositions*)
 fun is_fact rl =
     case prems_of rl of
-	[] => true  |  _::_ => false;
+        [] => true  |  _::_ => false;
 
 (*"Cut" all facts from theorem list into the goal as assumptions. *)
 fun cut_facts_tac ths i =
@@ -349,15 +351,15 @@
 (**** Indexing and filtering of theorems ****)
 
 (*Returns the list of potentially resolvable theorems for the goal "prem",
-	using the predicate  could(subgoal,concl).
+        using the predicate  could(subgoal,concl).
   Resulting list is no longer than "limit"*)
 fun filter_thms could (limit, prem, ths) =
   let val pb = Logic.strip_assums_concl prem;   (*delete assumptions*)
       fun filtr (limit, []) = []
-	| filtr (limit, th::ths) =
-	    if limit=0 then  []
-	    else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
-	    else filtr(limit,ths)
+        | filtr (limit, th::ths) =
+            if limit=0 then  []
+            else if could(pb, concl_of th)  then th :: filtr(limit-1, ths)
+            else filtr(limit,ths)
   in  filtr(limit,ths)  end;
 
 
@@ -382,9 +384,9 @@
 (*insert one tagged brl into the pair of nets*)
 fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) =
     if eres then 
-	case prems_of th of
-	    prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false))
-	  | [] => error"insert_tagged_brl: elimination rule with no premises"
+        case prems_of th of
+            prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false))
+          | [] => error"insert_tagged_brl: elimination rule with no premises"
     else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet);
 
 (*build a pair of nets for biresolution*)
@@ -398,9 +400,9 @@
 in
 fun delete_tagged_brl (brl as (eres,th), (inet,enet)) =
     if eres then 
-	case prems_of th of
-	    prem::_ => (inet, Net.delete_term ((prem, (0,brl)), enet, eq_kbrl))
-	  | []      => (inet,enet)     (*no major premise: ignore*)
+        case prems_of th of
+            prem::_ => (inet, Net.delete_term ((prem, (0,brl)), enet, eq_kbrl))
+          | []      => (inet,enet)     (*no major premise: ignore*)
     else (Net.delete_term ((concl_of th, (0,brl)), inet, eq_kbrl), enet);
 end;
 
@@ -444,9 +446,9 @@
     (fn (prem,i) =>
       let val krls = Net.unify_term net (Logic.strip_assums_concl prem)
       in 
-	 if pred krls  
+         if pred krls  
          then PRIMSEQ
-		(biresolution match (map (pair false) (orderlist krls)) i)
+                (biresolution match (map (pair false) (orderlist krls)) i)
          else no_tac
       end);
 
@@ -491,7 +493,7 @@
 fun asm_rewrite_goal_tac mode prover_tac mss =
       SELECT_GOAL 
         (PRIMITIVE
-	   (rewrite_goal_rule mode (result1 prover_tac) mss 1));
+           (rewrite_goal_rule mode (result1 prover_tac) mss 1));
 
 fun rewrite_goal_tac rews =
   asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.mss_of rews);
@@ -503,6 +505,9 @@
 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
 fun rewtac def = rewrite_goals_tac [def];
 
+val norm_hhf = Drule.forall_elim_vars_safe o rewrite_rule [Drule.norm_hhf_eq];
+val norm_hhf_tac = rewrite_goal_tac [Drule.norm_hhf_eq];
+
 
 (*** for folding definitions, handling critical pairs ***)
 
@@ -536,7 +541,7 @@
 fun rename_params_tac xs i =
   (if !Logic.auto_rename
     then (warning "Resetting Logic.auto_rename"; 
-	Logic.auto_rename := false)
+        Logic.auto_rename := false)
    else (); PRIMITIVE (rename_params_rule (xs, i)));
 
 fun rename_tac str i =