moved norm_hhf_rule, prove etc. to goal.ML;
authorwenzelm
Fri Oct 21 18:14:48 2005 +0200 (2005-10-21)
changeset 17968d50f08d9aabb
parent 17967 7a733b7438e1
child 17969 7262f4a45190
moved norm_hhf_rule, prove etc. to goal.ML;
moved asm_rewrite_goal_tac to simplifier.ML;
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Fri Oct 21 18:14:47 2005 +0200
     1.2 +++ b/src/Pure/tactic.ML	Fri Oct 21 18:14:48 2005 +0200
     1.3 @@ -70,8 +70,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_plain    : thm -> thm
     1.8 -  val norm_hhf_rule     : thm -> thm
     1.9    val norm_hhf_tac      : int -> tactic
    1.10    val prune_params_tac  : tactic
    1.11    val rename_params_tac : string list -> int -> tactic
    1.12 @@ -85,6 +83,7 @@
    1.13    val rewrite_rule      : thm list -> thm -> thm
    1.14    val rewrite_goals_tac : thm list -> tactic
    1.15    val rewrite_tac       : thm list -> tactic
    1.16 +  val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic
    1.17    val rewtac            : thm -> tactic
    1.18    val rotate_tac        : int -> int -> tactic
    1.19    val rtac              : thm -> int -> tactic
    1.20 @@ -112,12 +111,6 @@
    1.21    val simplify: bool -> thm list -> thm -> thm
    1.22    val conjunction_tac: tactic
    1.23    val smart_conjunction_tac: int -> tactic
    1.24 -  val prove_multi_plain: theory -> string list -> term list -> term list ->
    1.25 -    (thm list -> tactic) -> thm list
    1.26 -  val prove_multi: theory -> string list -> term list -> term list ->
    1.27 -    (thm list -> tactic) -> thm list
    1.28 -  val prove_plain: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.29 -  val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    1.30    val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
    1.31                            int -> tactic
    1.32    val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
    1.33 @@ -534,9 +527,14 @@
    1.34  val rewrite_rule = simplify true;
    1.35  val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
    1.36  
    1.37 +(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
    1.38 +fun asm_rewrite_goal_tac mode prover_tac ss =
    1.39 +  SELECT_GOAL
    1.40 +    (PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (SINGLE o prover_tac) ss 1));
    1.41 +
    1.42  fun rewrite_goal_tac rews =
    1.43    let val ss = MetaSimplifier.empty_ss addsimps rews in
    1.44 -    fn i => fn st => MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac)
    1.45 +    fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
    1.46        (MetaSimplifier.theory_context (Thm.theory_of_thm st) ss) i st
    1.47    end;
    1.48  
    1.49 @@ -547,15 +545,6 @@
    1.50  fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
    1.51  fun rewtac def = rewrite_goals_tac [def];
    1.52  
    1.53 -fun norm_hhf_plain th =
    1.54 -  if Drule.is_norm_hhf (Thm.prop_of th) then th
    1.55 -  else rewrite_rule [Drule.norm_hhf_eq] th;
    1.56 -
    1.57 -val norm_hhf_rule =
    1.58 -  norm_hhf_plain
    1.59 -  #> Thm.adjust_maxidx_thm
    1.60 -  #> Drule.gen_all;
    1.61 -
    1.62  val norm_hhf_tac =
    1.63    rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
    1.64    THEN' SUBGOAL (fn (t, i) =>
    1.65 @@ -655,64 +644,6 @@
    1.66  fun smart_conjunction_tac 0 = assume_tac 1
    1.67    | smart_conjunction_tac _ = TRY conjunction_tac;
    1.68  
    1.69 -
    1.70 -
    1.71 -(** minimal goal interface for programmed proofs *)
    1.72 -
    1.73 -fun gen_prove_multi finish_thm thy xs asms props tac =
    1.74 -  let
    1.75 -    val prop = Logic.mk_conjunction_list props;
    1.76 -    val statement = Logic.list_implies (asms, prop);
    1.77 -    val frees = map Term.dest_Free (Term.term_frees statement);
    1.78 -    val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees;
    1.79 -    val fixed_tfrees = foldr Term.add_typ_tfrees [] (map #2 fixed_frees);
    1.80 -    val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
    1.81 -
    1.82 -    fun err msg = raise ERROR_MESSAGE
    1.83 -      (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^
    1.84 -        Sign.string_of_term thy (Term.list_all_free (params, statement)));
    1.85 -
    1.86 -    fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm t)
    1.87 -      handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
    1.88 -
    1.89 -    val _ = cert_safe statement;
    1.90 -    val _ = Term.no_dummy_patterns statement handle TERM (msg, _) => err msg;
    1.91 -
    1.92 -    val cparams = map (cert_safe o Free) params;
    1.93 -    val casms = map cert_safe asms;
    1.94 -    val prems = map (norm_hhf_rule o Thm.assume) casms;
    1.95 -    val goal = Drule.mk_triv_goal (cert_safe prop);
    1.96 -
    1.97 -    val goal' =
    1.98 -      (case Seq.pull (tac prems goal) of SOME (goal', _) => goal' | _ => err "Tactic failed.");
    1.99 -    val ngoals = Thm.nprems_of goal';
   1.100 -    val _ = conditional (ngoals <> 0) (fn () =>
   1.101 -      err ("Proof failed.\n" ^
   1.102 -        Pretty.string_of (Pretty.chunks (Display.pretty_goals ngoals goal')) ^
   1.103 -        ("\n" ^ string_of_int ngoals ^ " unsolved goal(s)!")));
   1.104 -
   1.105 -    val raw_result = goal' RS Drule.rev_triv_goal;
   1.106 -    val prop' = prop_of raw_result;
   1.107 -    val _ = conditional (not (Pattern.matches thy (prop, prop'))) (fn () =>
   1.108 -      err ("Proved a different theorem: " ^ Sign.string_of_term thy prop'));
   1.109 -  in
   1.110 -    Drule.conj_elim_precise (length props) raw_result
   1.111 -    |> map (fn res => res
   1.112 -      |> Drule.implies_intr_list casms
   1.113 -      |> Drule.forall_intr_list cparams
   1.114 -      |> finish_thm fixed_tfrees)
   1.115 -  end;
   1.116 -
   1.117 -fun prove_multi_plain thy xs asms prop tac =
   1.118 -  gen_prove_multi (K norm_hhf_plain) thy xs asms prop tac;
   1.119 -fun prove_multi thy xs asms prop tac =
   1.120 -  gen_prove_multi (fn fixed_tfrees => Drule.zero_var_indexes o
   1.121 -      (#1 o Thm.varifyT' fixed_tfrees) o norm_hhf_rule)
   1.122 -    thy xs asms prop tac;
   1.123 -
   1.124 -fun prove_plain thy xs asms prop tac = hd (prove_multi_plain thy xs asms [prop] tac);
   1.125 -fun prove thy xs asms prop tac = hd (prove_multi thy xs asms [prop] tac);
   1.126 -
   1.127  end;
   1.128  
   1.129  structure BasicTactic: BASIC_TACTIC = Tactic;