reorganized structure Tactic vs. MetaSimplifier;
authorwenzelm
Thu Dec 07 23:16:55 2006 +0100 (2006-12-07)
changeset 2170845e7491bea47
parent 21707 dfc7b21d0ee9
child 21709 9cfd9eb9faec
reorganized structure Tactic vs. MetaSimplifier;
TFL/casesplit.ML
src/HOL/Hyperreal/transfer.ML
src/HOL/Integ/presburger.ML
src/HOL/Real/ferrante_rackoff.ML
src/HOL/Tools/Presburger/presburger.ML
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/typecopy_package.ML
src/Provers/eqsubst.ML
src/Provers/induct_method.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Isar/theory_target.ML
src/Pure/ROOT.ML
src/Pure/Tools/class_package.ML
src/Pure/Tools/codegen_data.ML
src/Pure/Tools/nbe.ML
src/Pure/meta_simplifier.ML
src/Pure/simplifier.ML
src/Pure/tactic.ML
     1.1 --- a/TFL/casesplit.ML	Thu Dec 07 21:44:13 2006 +0100
     1.2 +++ b/TFL/casesplit.ML	Thu Dec 07 23:16:55 2006 +0100
     1.3 @@ -80,8 +80,8 @@
     1.4  functor CaseSplitFUN(Data : CASE_SPLIT_DATA) =
     1.5  struct
     1.6  
     1.7 -val rulify_goals = Tactic.rewrite_goals_rule Data.rulify;
     1.8 -val atomize_goals = Tactic.rewrite_goals_rule Data.atomize;
     1.9 +val rulify_goals = MetaSimplifier.rewrite_goals_rule Data.rulify;
    1.10 +val atomize_goals = MetaSimplifier.rewrite_goals_rule Data.atomize;
    1.11  
    1.12  (* beta-eta contract the theorem *)
    1.13  fun beta_eta_contract thm =
     2.1 --- a/src/HOL/Hyperreal/transfer.ML	Thu Dec 07 21:44:13 2006 +0100
     2.2 +++ b/src/HOL/Hyperreal/transfer.ML	Thu Dec 07 23:16:55 2006 +0100
     2.3 @@ -62,7 +62,7 @@
     2.4      val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt)
     2.5      val meta = LocalDefs.meta_rewrite_rule ctxt
     2.6      val unfolds' = map meta unfolds and refolds' = map meta refolds;
     2.7 -    val (_$_$t') = concl_of (Tactic.rewrite true unfolds' (cterm_of thy t))
     2.8 +    val (_$_$t') = concl_of (MetaSimplifier.rewrite true unfolds' (cterm_of thy t))
     2.9      val u = unstar_term consts t'
    2.10      val tac =
    2.11        rewrite_goals_tac (ths @ refolds' @ unfolds') THEN
     3.1 --- a/src/HOL/Integ/presburger.ML	Thu Dec 07 21:44:13 2006 +0100
     3.2 +++ b/src/HOL/Integ/presburger.ML	Thu Dec 07 23:16:55 2006 +0100
     3.3 @@ -56,7 +56,7 @@
     3.4  val powerarith =
     3.5      (map thm ["nat_number_of", "zpower_number_of_even",
     3.6                "zpower_Pls", "zpower_Min"]) @
     3.7 -    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring",
     3.8 +    [(MetaSimplifier.simplify true [thm "zero_eq_Numeral0_nring",
     3.9                             thm "one_eq_Numeral1_nring"]
    3.10    (thm "zpower_number_of_odd"))]
    3.11  
     4.1 --- a/src/HOL/Real/ferrante_rackoff.ML	Thu Dec 07 21:44:13 2006 +0100
     4.2 +++ b/src/HOL/Real/ferrante_rackoff.ML	Thu Dec 07 23:16:55 2006 +0100
     4.3 @@ -42,7 +42,7 @@
     4.4  val powerarith =
     4.5    map thm ["nat_number_of", "zpower_number_of_even",
     4.6    "zpower_Pls", "zpower_Min"]
     4.7 -  @ [Tactic.simplify true [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"]
     4.8 +  @ [MetaSimplifier.simplify true [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"]
     4.9      (thm "zpower_number_of_odd")]
    4.10  
    4.11  val comp_arith = binarith @ intarith @ intarithrel @ natarith 
     5.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Thu Dec 07 21:44:13 2006 +0100
     5.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Thu Dec 07 23:16:55 2006 +0100
     5.3 @@ -56,7 +56,7 @@
     5.4  val powerarith =
     5.5      (map thm ["nat_number_of", "zpower_number_of_even",
     5.6                "zpower_Pls", "zpower_Min"]) @
     5.7 -    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring",
     5.8 +    [(MetaSimplifier.simplify true [thm "zero_eq_Numeral0_nring",
     5.9                             thm "one_eq_Numeral1_nring"]
    5.10    (thm "zpower_number_of_odd"))]
    5.11  
     6.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu Dec 07 21:44:13 2006 +0100
     6.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Dec 07 23:16:55 2006 +0100
     6.3 @@ -375,7 +375,7 @@
     6.4    in map mk_dist (sym_product cos) end;
     6.5  
     6.6  local
     6.7 -  val bool_eq_implies = thm "iffD1";
     6.8 +  val bool_eq_implies = iffD1;
     6.9    val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
    6.10    val rew_conj = thm "HOL.atomize_conj" |> Thm.symmetric;
    6.11    val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
    6.12 @@ -387,7 +387,7 @@
    6.13      val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
    6.14      val inject = (#inject o DatatypePackage.the_datatype thy) dtco
    6.15        |> map (fn thm => bool_eq_implies OF [thm] )
    6.16 -      |> map (Tactic.rewrite_rule [rew_eq, rew_conj]);
    6.17 +      |> map (MetaSimplifier.rewrite_rule [rew_eq, rew_conj]);
    6.18      val ctxt = ProofContext.init thy;
    6.19      val simpset = Simplifier.context ctxt
    6.20        (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
     7.1 --- a/src/HOL/Tools/record_package.ML	Thu Dec 07 21:44:13 2006 +0100
     7.2 +++ b/src/HOL/Tools/record_package.ML	Thu Dec 07 23:16:55 2006 +0100
     7.3 @@ -1428,7 +1428,7 @@
     7.4        let
     7.5          val SOME { Abs_induct = abs_induct,
     7.6            Abs_inject=abs_inject, Abs_inverse = abs_inverse, ...} = TypedefPackage.get_info thy name;
     7.7 -        val rewrite_rule = Tactic.rewrite_rule [rec_UNIV_I, rec_True_simp];
     7.8 +        val rewrite_rule = MetaSimplifier.rewrite_rule [rec_UNIV_I, rec_True_simp];
     7.9        in map rewrite_rule [abs_inject, abs_inverse, abs_induct] end;
    7.10    in
    7.11      thy
     8.1 --- a/src/HOL/Tools/typecopy_package.ML	Thu Dec 07 21:44:13 2006 +0100
     8.2 +++ b/src/HOL/Tools/typecopy_package.ML	Thu Dec 07 23:16:55 2006 +0100
     8.3 @@ -96,7 +96,7 @@
     8.4      val tac = Tactic.rtac UNIV_witness 1;
     8.5      fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
     8.6        Rep_name = c_rep, Abs_inject = inject,
     8.7 -      Abs_inverse = inverse, ... } : TypedefPackage.info ) thy = 
     8.8 +      Abs_inverse = inverse, ... } : TypedefPackage.info ) thy =
     8.9          let
    8.10            val exists_thm =
    8.11              UNIV_I
    8.12 @@ -146,16 +146,16 @@
    8.13    in (vs, [(constr, [typ])]) end;
    8.14  
    8.15  local
    8.16 -  val bool_eq_implies = thm "iffD1";
    8.17 +  val bool_eq_implies = iffD1;
    8.18    val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
    8.19  in fun get_cert thy tyco =
    8.20 -  Tactic.rewrite_rule [rew_eq] (bool_eq_implies OF [get_eq thy tyco])
    8.21 +  MetaSimplifier.rewrite_rule [rew_eq] (bool_eq_implies OF [get_eq thy tyco])
    8.22  end; (*local*)
    8.23  
    8.24  
    8.25  (* hook for projection function code *)
    8.26  
    8.27 -fun add_project (_ , { proj_def, ...} : info) =
    8.28 +fun add_project (_ , {proj_def, ...} : info) =
    8.29    CodegenData.add_func proj_def;
    8.30  
    8.31  val setup =
     9.1 --- a/src/Provers/eqsubst.ML	Thu Dec 07 21:44:13 2006 +0100
     9.2 +++ b/src/Provers/eqsubst.ML	Thu Dec 07 23:16:55 2006 +0100
     9.3 @@ -415,7 +415,7 @@
     9.4        val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
     9.5        val preelimrule =
     9.6            (RWInst.rw m rule pth)
     9.7 -            |> (Seq.hd o Tactic.prune_params_tac)
     9.8 +            |> (Seq.hd o prune_params_tac)
     9.9              |> Thm.permute_prems 0 ~1 (* put old asm first *)
    9.10              |> IsaND.unfix_frees cfvs (* unfix any global params *)
    9.11              |> RWInst.beta_eta_contract; (* normal form *)
    10.1 --- a/src/Provers/induct_method.ML	Thu Dec 07 21:44:13 2006 +0100
    10.2 +++ b/src/Provers/induct_method.ML	Thu Dec 07 23:16:55 2006 +0100
    10.3 @@ -160,7 +160,7 @@
    10.4    MetaSimplifier.rewrite_term thy Data.atomize []
    10.5    #> ObjectLogic.drop_judgment thy;
    10.6  
    10.7 -val atomize_cterm = Tactic.rewrite true Data.atomize;
    10.8 +val atomize_cterm = MetaSimplifier.rewrite true Data.atomize;
    10.9  
   10.10  val atomize_tac = Goal.rewrite_goal_tac Data.atomize;
   10.11  
   10.12 @@ -312,7 +312,7 @@
   10.13  
   10.14  fun miniscope_tac p i = PRIMITIVE (Drule.fconv_rule
   10.15    (Drule.goals_conv (Library.equal i)
   10.16 -    (Drule.forall_conv p (Tactic.rewrite true [Thm.symmetric Drule.norm_hhf_eq]))));
   10.17 +    (Drule.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]))));
   10.18  
   10.19  in
   10.20  
    11.1 --- a/src/Pure/Isar/local_defs.ML	Thu Dec 07 21:44:13 2006 +0100
    11.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Dec 07 23:16:55 2006 +0100
    11.3 @@ -161,11 +161,11 @@
    11.4  
    11.5  fun meta f ctxt = f o map (meta_rewrite_rule ctxt);
    11.6  
    11.7 -val unfold       = meta Tactic.rewrite_rule;
    11.8 -val unfold_goals = meta Tactic.rewrite_goals_rule;
    11.9 -val unfold_tac   = meta Tactic.rewrite_goals_tac;
   11.10 -val fold         = meta Tactic.fold_rule;
   11.11 -val fold_tac     = meta Tactic.fold_goals_tac;
   11.12 +val unfold       = meta MetaSimplifier.rewrite_rule;
   11.13 +val unfold_goals = meta MetaSimplifier.rewrite_goals_rule;
   11.14 +val unfold_tac   = meta MetaSimplifier.rewrite_goals_tac;
   11.15 +val fold         = meta MetaSimplifier.fold_rule;
   11.16 +val fold_tac     = meta MetaSimplifier.fold_goals_tac;
   11.17  
   11.18  
   11.19  (* derived defs -- potentially within the object-logic *)
   11.20 @@ -186,7 +186,7 @@
   11.21          Goal.prove ctxt' frees [] prop (K (ALLGOALS
   11.22            (meta_rewrite_tac ctxt' THEN'
   11.23              Goal.rewrite_goal_tac [def] THEN'
   11.24 -            Tactic.resolve_tac [Drule.reflexive_thm])))
   11.25 +            resolve_tac [Drule.reflexive_thm])))
   11.26          handle ERROR msg => cat_error msg "Failed to prove definitional specification."
   11.27        end;
   11.28    in (((c, T), rhs), prove) end;
    12.1 --- a/src/Pure/Isar/locale.ML	Thu Dec 07 21:44:13 2006 +0100
    12.2 +++ b/src/Pure/Isar/locale.ML	Thu Dec 07 23:16:55 2006 +0100
    12.3 @@ -1648,17 +1648,17 @@
    12.4      val cert = Thm.cterm_of defs_thy;
    12.5  
    12.6      val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
    12.7 -      Tactic.rewrite_goals_tac [pred_def] THEN
    12.8 +      MetaSimplifier.rewrite_goals_tac [pred_def] THEN
    12.9        Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
   12.10        Tactic.compose_tac (false, Conjunction.intr_list (map (Thm.assume o cert) norm_ts), 0) 1);
   12.11  
   12.12      val conjuncts =
   12.13        (Drule.equal_elim_rule2 OF [body_eq,
   12.14 -        Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))])
   12.15 +        MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
   12.16        |> Conjunction.elim_precise [length ts] |> hd;
   12.17      val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
   12.18        Element.prove_witness defs_ctxt t
   12.19 -       (Tactic.rewrite_goals_tac defs THEN
   12.20 +       (MetaSimplifier.rewrite_goals_tac defs THEN
   12.21          Tactic.compose_tac (false, ax, 0) 1));
   12.22    in ((statement, intro, axioms), defs_thy) end;
   12.23  
    13.1 --- a/src/Pure/Isar/object_logic.ML	Thu Dec 07 21:44:13 2006 +0100
    13.2 +++ b/src/Pure/Isar/object_logic.ML	Thu Dec 07 23:16:55 2006 +0100
    13.3 @@ -148,12 +148,12 @@
    13.4  fun rewrite_prems_tac rews i = PRIMITIVE (Drule.fconv_rule
    13.5    (Drule.goals_conv (Library.equal i)
    13.6      (Drule.forall_conv ~1
    13.7 -      (Drule.goals_conv (K true) (Tactic.rewrite true rews)))));
    13.8 +      (Drule.goals_conv (K true) (MetaSimplifier.rewrite true rews)))));
    13.9  
   13.10  fun atomize_term thy =
   13.11    drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) [];
   13.12  
   13.13 -fun atomize_cterm ct = Tactic.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
   13.14 +fun atomize_cterm ct = MetaSimplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
   13.15  fun atomize_thm th = rewrite_rule (get_atomize (Thm.theory_of_thm th)) th;
   13.16  
   13.17  fun atomize_tac i st =
   13.18 @@ -174,7 +174,7 @@
   13.19  fun rulify_tac i st = Goal.rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
   13.20  
   13.21  fun gen_rulify full thm =
   13.22 -  Tactic.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
   13.23 +  MetaSimplifier.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
   13.24    |> Drule.gen_all |> Thm.strip_shyps |> Drule.zero_var_indexes;
   13.25  
   13.26  val rulify = gen_rulify true;
    14.1 --- a/src/Pure/Isar/rule_cases.ML	Thu Dec 07 21:44:13 2006 +0100
    14.2 +++ b/src/Pure/Isar/rule_cases.ML	Thu Dec 07 23:16:55 2006 +0100
    14.3 @@ -189,14 +189,14 @@
    14.4  
    14.5  fun unfold_prems n defs th =
    14.6    if null defs then th
    14.7 -  else Drule.fconv_rule (Drule.goals_conv (fn i => i <= n) (Tactic.rewrite true defs)) th;
    14.8 +  else Drule.fconv_rule (Drule.goals_conv (fn i => i <= n) (MetaSimplifier.rewrite true defs)) th;
    14.9  
   14.10  fun unfold_prems_concls defs th =
   14.11    if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
   14.12    else
   14.13      Drule.fconv_rule
   14.14        (Drule.concl_conv ~1 (Conjunction.conv ~1
   14.15 -        (K (Drule.prems_conv ~1 (K (Tactic.rewrite true defs)))))) th;
   14.16 +        (K (Drule.prems_conv ~1 (K (MetaSimplifier.rewrite true defs)))))) th;
   14.17  
   14.18  in
   14.19  
    15.1 --- a/src/Pure/Isar/theory_target.ML	Thu Dec 07 21:44:13 2006 +0100
    15.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Dec 07 23:16:55 2006 +0100
    15.3 @@ -92,7 +92,7 @@
    15.4      val thy_ctxt = ProofContext.init thy;
    15.5      val ct = Thm.cterm_of thy t;
    15.6      val (defs, ct') = LocalDefs.export ctxt thy_ctxt (Drule.mk_term ct) ||> Drule.dest_term;
    15.7 -  in (Thm.term_of ct', Tactic.rewrite true defs ct) end;
    15.8 +  in (Thm.term_of ct', MetaSimplifier.rewrite true defs ct) end;
    15.9  
   15.10  fun add_def (name, prop) =
   15.11    Theory.add_defs_i false false [(name, prop)] #>
   15.12 @@ -171,8 +171,8 @@
   15.13      (*export assumes/defines*)
   15.14      val th = Goal.norm_result raw_th;
   15.15      val (defs, th') = LocalDefs.export ctxt thy_ctxt th;
   15.16 -    val concl_conv = Tactic.rewrite true defs (Thm.cprop_of th);
   15.17 -    val assms = map (Tactic.rewrite_rule defs o Thm.assume) (Assumption.assms_of ctxt);
   15.18 +    val concl_conv = MetaSimplifier.rewrite true defs (Thm.cprop_of th);
   15.19 +    val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.assms_of ctxt);
   15.20      val nprems = Thm.nprems_of th' - Thm.nprems_of th;
   15.21  
   15.22      (*export fixes*)
    16.1 --- a/src/Pure/ROOT.ML	Thu Dec 07 21:44:13 2006 +0100
    16.2 +++ b/src/Pure/ROOT.ML	Thu Dec 07 23:16:55 2006 +0100
    16.3 @@ -55,8 +55,8 @@
    16.4  use "variable.ML";
    16.5  use "tctical.ML";
    16.6  use "search.ML";
    16.7 +use "tactic.ML";
    16.8  use "meta_simplifier.ML";
    16.9 -use "tactic.ML";
   16.10  use "conjunction.ML";
   16.11  use "assumption.ML";
   16.12  use "goal.ML";
    17.1 --- a/src/Pure/Tools/class_package.ML	Thu Dec 07 21:44:13 2006 +0100
    17.2 +++ b/src/Pure/Tools/class_package.ML	Thu Dec 07 23:16:55 2006 +0100
    17.3 @@ -185,7 +185,7 @@
    17.4      val class = loc (*FIXME*);
    17.5      val thms = (#defs o fst o the_class_data thy) class;
    17.6    in
    17.7 -    Tactic.rewrite_rule thms
    17.8 +    MetaSimplifier.rewrite_rule thms
    17.9    end;
   17.10  
   17.11  
    18.1 --- a/src/Pure/Tools/codegen_data.ML	Thu Dec 07 21:44:13 2006 +0100
    18.2 +++ b/src/Pure/Tools/codegen_data.ML	Thu Dec 07 23:16:55 2006 +0100
    18.3 @@ -524,7 +524,7 @@
    18.4  
    18.5  fun rewrite_func rewrites thm =
    18.6    let
    18.7 -    val rewrite = Tactic.rewrite false rewrites;
    18.8 +    val rewrite = MetaSimplifier.rewrite false rewrites;
    18.9      val (ct_eq, [ct_lhs, ct_rhs]) = (Drule.strip_comb o Thm.cprop_of) thm;
   18.10      val Const ("==", _) = Thm.term_of ct_eq;
   18.11      val (ct_f, ct_args) = Drule.strip_comb ct_lhs;
   18.12 @@ -715,7 +715,7 @@
   18.13    ((fn [args, rhs] => rhs :: (snd o Drule.strip_comb) args) o snd o Drule.strip_comb o Thm.cprop_of))
   18.14    (fn rews => map (rewrite_func rews));
   18.15  val apply_inline_proc_cterm = gen_apply_inline_proc single
   18.16 -  (Tactic.rewrite false);
   18.17 +  (MetaSimplifier.rewrite false);
   18.18  
   18.19  fun apply_preproc thy f [] = []
   18.20    | apply_preproc thy f (thms as (thm :: _)) =
   18.21 @@ -746,8 +746,10 @@
   18.22  fun preprocess_cterm thy ct =
   18.23    ct
   18.24    |> Thm.reflexive
   18.25 -  |> fold (rhs_conv o Tactic.rewrite false o single) ((#inlines o the_preproc o get_exec) thy)
   18.26 -  |> fold (fn (_, f) => rhs_conv (apply_inline_proc_cterm thy f)) ((#inline_procs o the_preproc o get_exec) thy)
   18.27 +  |> fold (rhs_conv o MetaSimplifier.rewrite false o single)
   18.28 +    ((#inlines o the_preproc o get_exec) thy)
   18.29 +  |> fold (fn (_, f) => rhs_conv (apply_inline_proc_cterm thy f))
   18.30 +    ((#inline_procs o the_preproc o get_exec) thy)
   18.31  
   18.32  end; (*local*)
   18.33  
    19.1 --- a/src/Pure/Tools/nbe.ML	Thu Dec 07 21:44:13 2006 +0100
    19.2 +++ b/src/Pure/Tools/nbe.ML	Thu Dec 07 23:16:55 2006 +0100
    19.3 @@ -78,7 +78,7 @@
    19.4    let
    19.5      val ctxt = ProofContext.init thy;
    19.6      val posts = (map (LocalDefs.meta_rewrite_rule ctxt) o snd) (NBE_Rewrite.get thy)
    19.7 -  in Tactic.rewrite false posts end
    19.8 +  in MetaSimplifier.rewrite false posts end
    19.9  
   19.10  
   19.11  (* code store *)
    20.1 --- a/src/Pure/meta_simplifier.ML	Thu Dec 07 21:44:13 2006 +0100
    20.2 +++ b/src/Pure/meta_simplifier.ML	Thu Dec 07 23:16:55 2006 +0100
    20.3 @@ -72,6 +72,16 @@
    20.4    val addSSolver: simpset * solver -> simpset
    20.5    val setSolver: simpset * solver -> simpset
    20.6    val addSolver: simpset * solver -> simpset
    20.7 +
    20.8 +  val rewrite_rule: thm list -> thm -> thm
    20.9 +  val rewrite_goals_rule: thm list -> thm -> thm
   20.10 +  val rewrite_goals_tac: thm list -> tactic
   20.11 +  val rewrite_tac: thm list -> tactic
   20.12 +  val rewtac: thm -> tactic
   20.13 +  val prune_params_tac: tactic
   20.14 +  val fold_rule: thm list -> thm -> thm
   20.15 +  val fold_tac: thm list -> tactic
   20.16 +  val fold_goals_tac: thm list -> tactic
   20.17  end;
   20.18  
   20.19  signature META_SIMPLIFIER =
   20.20 @@ -94,16 +104,15 @@
   20.21    val set_solvers: solver list -> simpset -> simpset
   20.22    val rewrite_cterm: bool * bool * bool ->
   20.23      (simpset -> thm -> thm option) -> simpset -> cterm -> thm
   20.24 -  val rewrite_aux: (simpset -> thm -> thm option) -> bool -> thm list -> cterm -> thm
   20.25 -  val simplify_aux: (simpset -> thm -> thm option) -> bool -> thm list -> thm -> thm
   20.26    val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
   20.27    val rewrite_thm: bool * bool * bool ->
   20.28      (simpset -> thm -> thm option) -> simpset -> thm -> thm
   20.29 -  val rewrite_goals_rule_aux: (simpset -> thm -> thm option) -> thm list -> thm -> thm
   20.30    val rewrite_goal_rule: bool * bool * bool ->
   20.31      (simpset -> thm -> thm option) -> simpset -> int -> thm -> thm
   20.32    val norm_hhf: thm -> thm
   20.33    val norm_hhf_protect: thm -> thm
   20.34 +  val rewrite: bool -> thm list -> cterm -> thm
   20.35 +  val simplify: bool -> thm list -> thm -> thm
   20.36  end;
   20.37  
   20.38  structure MetaSimplifier: META_SIMPLIFIER =
   20.39 @@ -1189,18 +1198,23 @@
   20.40    in dec simp_depth; res end
   20.41    handle exn => (dec simp_depth; raise exn);  (* FIXME avoid handling of generic exceptions *)
   20.42  
   20.43 +val simple_prover =
   20.44 +  SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss)));
   20.45 +
   20.46  (*Rewrite a cterm*)
   20.47 -fun rewrite_aux _ _ [] ct = Thm.reflexive ct
   20.48 -  | rewrite_aux prover full thms ct =
   20.49 -      rewrite_cterm (full, false, false) prover
   20.50 -      (theory_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
   20.51 +fun rewrite _ [] ct = Thm.reflexive ct
   20.52 +  | rewrite full thms ct =
   20.53 +      rewrite_cterm (full, false, false) simple_prover
   20.54 +        (theory_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
   20.55  
   20.56  (*Rewrite a theorem*)
   20.57 -fun simplify_aux _ _ [] th = th
   20.58 -  | simplify_aux prover full thms th =
   20.59 -      Drule.fconv_rule (rewrite_cterm (full, false, false) prover
   20.60 +fun simplify _ [] th = th
   20.61 +  | simplify full thms th =
   20.62 +      Drule.fconv_rule (rewrite_cterm (full, false, false) simple_prover
   20.63          (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms)) th;
   20.64  
   20.65 +val rewrite_rule = simplify true;
   20.66 +
   20.67  (*simple term rewriting -- no proof*)
   20.68  fun rewrite_term thy rules procs =
   20.69    Pattern.rewrite_term thy (map decomp_simp' rules) procs;
   20.70 @@ -1208,8 +1222,8 @@
   20.71  fun rewrite_thm mode prover ss = Drule.fconv_rule (rewrite_cterm mode prover ss);
   20.72  
   20.73  (*Rewrite the subgoals of a proof state (represented by a theorem) *)
   20.74 -fun rewrite_goals_rule_aux prover thms th =
   20.75 -  Drule.fconv_rule (Drule.goals_conv (K true) (rewrite_cterm (true, true, true) prover
   20.76 +fun rewrite_goals_rule thms th =
   20.77 +  Drule.fconv_rule (Drule.goals_conv (K true) (rewrite_cterm (true, true, true) simple_prover
   20.78      (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
   20.79  
   20.80  (*Rewrite the subgoal of a proof state (represented by a theorem)*)
   20.81 @@ -1219,6 +1233,44 @@
   20.82    else raise THM("rewrite_goal_rule",i,[thm]);
   20.83  
   20.84  
   20.85 +(** meta-rewriting tactics **)
   20.86 +
   20.87 +(*Rewrite throughout proof state. *)
   20.88 +fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
   20.89 +
   20.90 +(*Rewrite subgoals only, not main goal. *)
   20.91 +fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
   20.92 +fun rewtac def = rewrite_goals_tac [def];
   20.93 +
   20.94 +(*Prunes all redundant parameters from the proof state by rewriting.
   20.95 +  DOES NOT rewrite main goal, where quantification over an unused bound
   20.96 +    variable is sometimes done to avoid the need for cut_facts_tac.*)
   20.97 +val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
   20.98 +
   20.99 +
  20.100 +(* for folding definitions, handling critical pairs *)
  20.101 +
  20.102 +(*The depth of nesting in a term*)
  20.103 +fun term_depth (Abs(a,T,t)) = 1 + term_depth t
  20.104 +  | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
  20.105 +  | term_depth _ = 0;
  20.106 +
  20.107 +val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
  20.108 +
  20.109 +(*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
  20.110 +  Returns longest lhs first to avoid folding its subexpressions.*)
  20.111 +fun sort_lhs_depths defs =
  20.112 +  let val keylist = AList.make (term_depth o lhs_of_thm) defs
  20.113 +      val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
  20.114 +  in map (AList.find (op =) keylist) keys end;
  20.115 +
  20.116 +val rev_defs = sort_lhs_depths o map symmetric;
  20.117 +
  20.118 +fun fold_rule defs = fold rewrite_rule (rev_defs defs);
  20.119 +fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
  20.120 +fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
  20.121 +
  20.122 +
  20.123  (* HHF normal form: !! before ==>, outermost !! generalized *)
  20.124  
  20.125  local
    21.1 --- a/src/Pure/simplifier.ML	Thu Dec 07 21:44:13 2006 +0100
    21.2 +++ b/src/Pure/simplifier.ML	Thu Dec 07 23:16:55 2006 +0100
    21.3 @@ -80,6 +80,9 @@
    21.4  structure Simplifier: SIMPLIFIER =
    21.5  struct
    21.6  
    21.7 +open MetaSimplifier;
    21.8 +
    21.9 +
   21.10  (** simpset data **)
   21.11  
   21.12  (* global simpsets *)
   21.13 @@ -348,9 +351,6 @@
   21.14      thy
   21.15    end);
   21.16  
   21.17 -
   21.18 -open MetaSimplifier;
   21.19 -
   21.20  end;
   21.21  
   21.22  structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;
    22.1 --- a/src/Pure/tactic.ML	Thu Dec 07 21:44:13 2006 +0100
    22.2 +++ b/src/Pure/tactic.ML	Thu Dec 07 23:16:55 2006 +0100
    22.3 @@ -47,9 +47,6 @@
    22.4    val filter_thms       : (term*term->bool) -> int*term*thm list -> thm list
    22.5    val filt_resolve_tac  : thm list -> int -> int -> tactic
    22.6    val flexflex_tac      : tactic
    22.7 -  val fold_goals_tac    : thm list -> tactic
    22.8 -  val fold_rule         : thm list -> thm -> thm
    22.9 -  val fold_tac          : thm list -> tactic
   22.10    val forward_tac       : thm list -> int -> tactic
   22.11    val forw_inst_tac     : (string*string)list -> thm -> int -> tactic
   22.12    val ftac              : thm -> int ->tactic
   22.13 @@ -69,18 +66,12 @@
   22.14    val net_biresolve_tac : (bool*thm) list -> int -> tactic
   22.15    val net_match_tac     : thm list -> int -> tactic
   22.16    val net_resolve_tac   : thm list -> int -> tactic
   22.17 -  val prune_params_tac  : tactic
   22.18    val rename_params_tac : string list -> int -> tactic
   22.19    val rename_tac        : string -> int -> tactic
   22.20    val rename_last_tac   : string -> string list -> int -> tactic
   22.21    val resolve_from_net_tac      : (int*thm) Net.net -> int -> tactic
   22.22    val resolve_tac       : thm list -> int -> tactic
   22.23    val res_inst_tac      : (string*string)list -> thm -> int -> tactic
   22.24 -  val rewrite_goals_rule: thm list -> thm -> thm
   22.25 -  val rewrite_rule      : thm list -> thm -> thm
   22.26 -  val rewrite_goals_tac : thm list -> tactic
   22.27 -  val rewrite_tac       : thm list -> tactic
   22.28 -  val rewtac            : thm -> tactic
   22.29    val rotate_tac        : int -> int -> tactic
   22.30    val rtac              : thm -> int -> tactic
   22.31    val rule_by_tactic    : tactic -> thm -> thm
   22.32 @@ -103,8 +94,6 @@
   22.33    val untaglist: (int * 'a) list -> 'a list
   22.34    val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool
   22.35    val orderlist: (int * 'a) list -> 'a list
   22.36 -  val rewrite: bool -> thm list -> cterm -> thm
   22.37 -  val simplify: bool -> thm list -> thm -> thm
   22.38    val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
   22.39                            int -> tactic
   22.40    val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
   22.41 @@ -512,47 +501,6 @@
   22.42  fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2;
   22.43  
   22.44  
   22.45 -(*** Meta-Rewriting Tactics ***)
   22.46 -
   22.47 -val simple_prover =
   22.48 -  SINGLE o (fn ss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_ss ss)));
   22.49 -
   22.50 -val rewrite = MetaSimplifier.rewrite_aux simple_prover;
   22.51 -val simplify = MetaSimplifier.simplify_aux simple_prover;
   22.52 -val rewrite_rule = simplify true;
   22.53 -val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
   22.54 -
   22.55 -(*Rewrite throughout proof state. *)
   22.56 -fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
   22.57 -
   22.58 -(*Rewrite subgoals only, not main goal. *)
   22.59 -fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
   22.60 -fun rewtac def = rewrite_goals_tac [def];
   22.61 -
   22.62 -
   22.63 -(*** for folding definitions, handling critical pairs ***)
   22.64 -
   22.65 -(*The depth of nesting in a term*)
   22.66 -fun term_depth (Abs(a,T,t)) = 1 + term_depth t
   22.67 -  | term_depth (f$t) = 1 + Int.max(term_depth f, term_depth t)
   22.68 -  | term_depth _ = 0;
   22.69 -
   22.70 -val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
   22.71 -
   22.72 -(*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
   22.73 -  Returns longest lhs first to avoid folding its subexpressions.*)
   22.74 -fun sort_lhs_depths defs =
   22.75 -  let val keylist = AList.make (term_depth o lhs_of_thm) defs
   22.76 -      val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
   22.77 -  in map (AList.find (op =) keylist) keys end;
   22.78 -
   22.79 -val rev_defs = sort_lhs_depths o map symmetric;
   22.80 -
   22.81 -fun fold_rule defs = fold rewrite_rule (rev_defs defs);
   22.82 -fun fold_tac defs = EVERY (map rewrite_tac (rev_defs defs));
   22.83 -fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
   22.84 -
   22.85 -
   22.86  (*** Renaming of parameters in a subgoal
   22.87       Names may contain letters, digits or primes and must be
   22.88       separated by blanks ***)
   22.89 @@ -582,11 +530,6 @@
   22.90        else all_tac
   22.91    end;
   22.92  
   22.93 -(*Prunes all redundant parameters from the proof state by rewriting.
   22.94 -  DOES NOT rewrite main goal, where quantification over an unused bound
   22.95 -    variable is sometimes done to avoid the need for cut_facts_tac.*)
   22.96 -val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
   22.97 -
   22.98  (*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
   22.99    right to left if n is positive, and from left to right if n is negative.*)
  22.100  fun rotate_tac 0 i = all_tac