src/Pure/tactic.ML
changeset 21687 f689f729afab
parent 20302 265b2342cf21
child 21708 45e7491bea47
     1.1 --- a/src/Pure/tactic.ML	Wed Dec 06 21:19:03 2006 +0100
     1.2 +++ b/src/Pure/tactic.ML	Thu Dec 07 00:42:04 2006 +0100
     1.3 @@ -69,7 +69,6 @@
     1.4    val net_biresolve_tac : (bool*thm) list -> int -> tactic
     1.5    val net_match_tac     : thm list -> int -> tactic
     1.6    val net_resolve_tac   : thm list -> int -> tactic
     1.7 -  val norm_hhf_tac      : int -> tactic
     1.8    val prune_params_tac  : tactic
     1.9    val rename_params_tac : string list -> int -> tactic
    1.10    val rename_tac        : string -> int -> tactic
    1.11 @@ -77,12 +76,10 @@
    1.12    val resolve_from_net_tac      : (int*thm) Net.net -> int -> tactic
    1.13    val resolve_tac       : thm list -> int -> tactic
    1.14    val res_inst_tac      : (string*string)list -> thm -> int -> tactic
    1.15 -  val rewrite_goal_tac  : thm list -> int -> tactic
    1.16    val rewrite_goals_rule: thm list -> thm -> thm
    1.17    val rewrite_rule      : thm list -> thm -> thm
    1.18    val rewrite_goals_tac : thm list -> tactic
    1.19    val rewrite_tac       : thm list -> tactic
    1.20 -  val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic
    1.21    val rewtac            : thm -> tactic
    1.22    val rotate_tac        : int -> int -> tactic
    1.23    val rtac              : thm -> int -> tactic
    1.24 @@ -97,8 +94,6 @@
    1.25    val instantiate_tac   : (string * string) list -> tactic
    1.26    val thin_tac          : string -> int -> tactic
    1.27    val trace_goalno_tac  : (int -> tactic) -> int -> tactic
    1.28 -  val CONJUNCTS: tactic -> int -> tactic
    1.29 -  val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
    1.30  end;
    1.31  
    1.32  signature TACTIC =
    1.33 @@ -110,8 +105,6 @@
    1.34    val orderlist: (int * 'a) list -> 'a list
    1.35    val rewrite: bool -> thm list -> cterm -> thm
    1.36    val simplify: bool -> thm list -> thm -> thm
    1.37 -  val conjunction_tac: int -> tactic
    1.38 -  val precise_conjunction_tac: int -> int -> tactic
    1.39    val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
    1.40                            int -> tactic
    1.41    val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
    1.42 @@ -529,17 +522,6 @@
    1.43  val rewrite_rule = simplify true;
    1.44  val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
    1.45  
    1.46 -(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
    1.47 -fun asm_rewrite_goal_tac mode prover_tac ss =
    1.48 -  SELECT_GOAL
    1.49 -    (PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (SINGLE o prover_tac) ss 1));
    1.50 -
    1.51 -fun rewrite_goal_tac rews =
    1.52 -  let val ss = MetaSimplifier.empty_ss addsimps rews in
    1.53 -    fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
    1.54 -      (MetaSimplifier.theory_context (Thm.theory_of_thm st) ss) i st
    1.55 -  end;
    1.56 -
    1.57  (*Rewrite throughout proof state. *)
    1.58  fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
    1.59  
    1.60 @@ -547,12 +529,6 @@
    1.61  fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
    1.62  fun rewtac def = rewrite_goals_tac [def];
    1.63  
    1.64 -val norm_hhf_tac =
    1.65 -  rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
    1.66 -  THEN' SUBGOAL (fn (t, i) =>
    1.67 -    if Drule.is_norm_hhf t then all_tac
    1.68 -    else rewrite_goal_tac [Drule.norm_hhf_eq] i);
    1.69 -
    1.70  
    1.71  (*** for folding definitions, handling critical pairs ***)
    1.72  
    1.73 @@ -633,32 +609,6 @@
    1.74         end)
    1.75    end;
    1.76  
    1.77 -
    1.78 -(* meta-level conjunction *)
    1.79 -
    1.80 -val conj_tac = SUBGOAL (fn (goal, i) =>
    1.81 -  if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
    1.82 -  else no_tac);
    1.83 -
    1.84 -val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac;
    1.85 -
    1.86 -val precise_conjunction_tac =
    1.87 -  let
    1.88 -    fun tac 0 i = eq_assume_tac i
    1.89 -      | tac 1 i = SUBGOAL (K all_tac) i
    1.90 -      | tac n i = conj_tac i THEN TRY (fn st => tac (n - 1) (i + 1) st);
    1.91 -  in TRY oo tac end;
    1.92 -
    1.93 -fun CONJUNCTS tac =
    1.94 -  SELECT_GOAL (conjunction_tac 1
    1.95 -    THEN tac
    1.96 -    THEN PRIMITIVE (Conjunction.uncurry ~1));
    1.97 -
    1.98 -fun PRECISE_CONJUNCTS n tac =
    1.99 -  SELECT_GOAL (precise_conjunction_tac n 1
   1.100 -    THEN tac
   1.101 -    THEN PRIMITIVE (Conjunction.uncurry ~1));
   1.102 -
   1.103  end;
   1.104  
   1.105  structure BasicTactic: BASIC_TACTIC = Tactic;