src/Pure/tactic.ML
changeset 21708 45e7491bea47
parent 21687 f689f729afab
child 22360 26ead7ed4f4b
     1.1 --- a/src/Pure/tactic.ML	Thu Dec 07 21:44:13 2006 +0100
     1.2 +++ b/src/Pure/tactic.ML	Thu Dec 07 23:16:55 2006 +0100
     1.3 @@ -47,9 +47,6 @@
     1.4    val filter_thms       : (term*term->bool) -> int*term*thm list -> thm list
     1.5    val filt_resolve_tac  : thm list -> int -> int -> tactic
     1.6    val flexflex_tac      : tactic
     1.7 -  val fold_goals_tac    : thm list -> tactic
     1.8 -  val fold_rule         : thm list -> thm -> thm
     1.9 -  val fold_tac          : thm list -> tactic
    1.10    val forward_tac       : thm list -> int -> tactic
    1.11    val forw_inst_tac     : (string*string)list -> thm -> int -> tactic
    1.12    val ftac              : thm -> int ->tactic
    1.13 @@ -69,18 +66,12 @@
    1.14    val net_biresolve_tac : (bool*thm) list -> int -> tactic
    1.15    val net_match_tac     : thm list -> int -> tactic
    1.16    val net_resolve_tac   : thm list -> int -> tactic
    1.17 -  val prune_params_tac  : tactic
    1.18    val rename_params_tac : string list -> int -> tactic
    1.19    val rename_tac        : string -> int -> tactic
    1.20    val rename_last_tac   : string -> string list -> int -> tactic
    1.21    val resolve_from_net_tac      : (int*thm) Net.net -> int -> tactic
    1.22    val resolve_tac       : thm list -> int -> tactic
    1.23    val res_inst_tac      : (string*string)list -> thm -> int -> tactic
    1.24 -  val rewrite_goals_rule: thm list -> thm -> thm
    1.25 -  val rewrite_rule      : thm list -> thm -> thm
    1.26 -  val rewrite_goals_tac : thm list -> tactic
    1.27 -  val rewrite_tac       : thm list -> tactic
    1.28 -  val rewtac            : thm -> tactic
    1.29    val rotate_tac        : int -> int -> tactic
    1.30    val rtac              : thm -> int -> tactic
    1.31    val rule_by_tactic    : tactic -> thm -> thm
    1.32 @@ -103,8 +94,6 @@
    1.33    val untaglist: (int * 'a) list -> 'a list
    1.34    val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool
    1.35    val orderlist: (int * 'a) list -> 'a list
    1.36 -  val rewrite: bool -> thm list -> cterm -> thm
    1.37 -  val simplify: bool -> thm list -> thm -> thm
    1.38    val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
    1.39                            int -> tactic
    1.40    val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
    1.41 @@ -512,47 +501,6 @@
    1.42  fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
    1.43  
    1.44  
    1.45 -(*** Meta-Rewriting Tactics ***)
    1.46 -
    1.47 -val simple_prover =
    1.48 -  SINGLE o (fn ss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_ss ss)));
    1.49 -
    1.50 -val rewrite = MetaSimplifier.rewrite_aux simple_prover;
    1.51 -val simplify = MetaSimplifier.simplify_aux simple_prover;
    1.52 -val rewrite_rule = simplify true;
    1.53 -val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
    1.54 -
    1.55 -(*Rewrite throughout proof state. *)
    1.56 -fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
    1.57 -
    1.58 -(*Rewrite subgoals only, not main goal. *)
    1.59 -fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
    1.60 -fun rewtac def = rewrite_goals_tac [def];
    1.61 -
    1.62 -
    1.63 -(*** for folding definitions, handling critical pairs ***)
    1.64 -
    1.65 -(*The depth of nesting in a term*)
    1.66 -fun term_depth (Abs(a,T,t)) = 1 + term_depth t
    1.67 -  | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
    1.68 -  | term_depth _ = 0;
    1.69 -
    1.70 -val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
    1.71 -
    1.72 -(*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
    1.73 -  Returns longest lhs first to avoid folding its subexpressions.*)
    1.74 -fun sort_lhs_depths defs =
    1.75 -  let val keylist = AList.make (term_depth o lhs_of_thm) defs
    1.76 -      val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
    1.77 -  in map (AList.find (op =) keylist) keys end;
    1.78 -
    1.79 -val rev_defs = sort_lhs_depths o map symmetric;
    1.80 -
    1.81 -fun fold_rule defs = fold rewrite_rule (rev_defs defs);
    1.82 -fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
    1.83 -fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
    1.84 -
    1.85 -
    1.86  (*** Renaming of parameters in a subgoal
    1.87       Names may contain letters, digits or primes and must be
    1.88       separated by blanks ***)
    1.89 @@ -582,11 +530,6 @@
    1.90        else all_tac
    1.91    end;
    1.92  
    1.93 -(*Prunes all redundant parameters from the proof state by rewriting.
    1.94 -  DOES NOT rewrite main goal, where quantification over an unused bound
    1.95 -    variable is sometimes done to avoid the need for cut_facts_tac.*)
    1.96 -val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
    1.97 -
    1.98  (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
    1.99    right to left if n is positive, and from left to right if n is negative.*)
   1.100  fun rotate_tac 0 i = all_tac