renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
authorwenzelm
Fri Dec 17 17:08:56 2010 +0100 (2010-12-17 ago)
changeset 41228e1fce873b814
parent 41227 11e7ee2ca77f
child 41229 d797baa3d57c
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
NEWS
src/HOL/HOLCF/Tools/domaindef.ML
src/HOL/NSA/transfer.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Predicate_Compile/core_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/TFL/casesplit.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/inductive.ML
src/HOL/ex/Numeral.thy
src/Pure/IsaMakefile
src/Pure/Isar/attrib.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/rule_cases.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/ROOT.ML
src/Pure/assumption.ML
src/Pure/axclass.ML
src/Pure/goal.ML
src/Pure/meta_simplifier.ML
src/Pure/raw_simplifier.ML
src/Pure/simplifier.ML
src/Tools/atomize_elim.ML
src/Tools/coherent.ML
src/Tools/induct.ML
     1.1 --- a/NEWS	Fri Dec 17 16:25:21 2010 +0100
     1.2 +++ b/NEWS	Fri Dec 17 17:08:56 2010 +0100
     1.3 @@ -599,6 +599,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Renamed structure MetaSimplifier to Raw_Simplifier.  Note that the
     1.8 +main functionality is provided by structure Simplifier.
     1.9 +
    1.10  * Syntax.pretty_priority (default 0) configures the required priority
    1.11  of pretty-printed output and thus affects insertion of parentheses.
    1.12  
     2.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Fri Dec 17 16:25:21 2010 +0100
     2.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Fri Dec 17 17:08:56 2010 +0100
     2.3 @@ -170,7 +170,7 @@
     2.4      val liftprj_def = singleton (ProofContext.export lthy ctxt_thy) liftprj_ldef
     2.5      val liftdefl_def = singleton (ProofContext.export lthy ctxt_thy) liftdefl_ldef
     2.6      val type_definition_thm =
     2.7 -      MetaSimplifier.rewrite_rule
     2.8 +      Raw_Simplifier.rewrite_rule
     2.9          (the_list (#set_def (#2 info)))
    2.10          (#type_definition (#2 info))
    2.11      val typedef_thms =
     3.1 --- a/src/HOL/NSA/transfer.ML	Fri Dec 17 16:25:21 2010 +0100
     3.2 +++ b/src/HOL/NSA/transfer.ML	Fri Dec 17 17:08:56 2010 +0100
     3.3 @@ -58,7 +58,7 @@
     3.4      val meta = Local_Defs.meta_rewrite_rule ctxt;
     3.5      val ths' = map meta ths;
     3.6      val unfolds' = map meta unfolds and refolds' = map meta refolds;
     3.7 -    val (_$_$t') = concl_of (MetaSimplifier.rewrite true unfolds' (cterm_of thy t))
     3.8 +    val (_$_$t') = concl_of (Raw_Simplifier.rewrite true unfolds' (cterm_of thy t))
     3.9      val u = unstar_term consts t'
    3.10      val tac =
    3.11        rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN
     4.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Fri Dec 17 16:25:21 2010 +0100
     4.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Dec 17 17:08:56 2010 +0100
     4.3 @@ -19,10 +19,10 @@
     4.4  val inductive_atomize = @{thms induct_atomize};
     4.5  val inductive_rulify = @{thms induct_rulify};
     4.6  
     4.7 -fun rulify_term thy = MetaSimplifier.rewrite_term thy inductive_rulify [];
     4.8 +fun rulify_term thy = Raw_Simplifier.rewrite_term thy inductive_rulify [];
     4.9  
    4.10  val atomize_conv =
    4.11 -  MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE))
    4.12 +  Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
    4.13      (HOL_basic_ss addsimps inductive_atomize);
    4.14  val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);
    4.15  fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
     5.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Dec 17 16:25:21 2010 +0100
     5.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Dec 17 17:08:56 2010 +0100
     5.3 @@ -20,10 +20,10 @@
     5.4  val inductive_atomize = @{thms induct_atomize};
     5.5  val inductive_rulify = @{thms induct_rulify};
     5.6  
     5.7 -fun rulify_term thy = MetaSimplifier.rewrite_term thy inductive_rulify [];
     5.8 +fun rulify_term thy = Raw_Simplifier.rewrite_term thy inductive_rulify [];
     5.9  
    5.10  val atomize_conv =
    5.11 -  MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE))
    5.12 +  Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
    5.13      (HOL_basic_ss addsimps inductive_atomize);
    5.14  val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);
    5.15  fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
     6.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Fri Dec 17 16:25:21 2010 +0100
     6.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Fri Dec 17 17:08:56 2010 +0100
     6.3 @@ -52,7 +52,7 @@
     6.4    in
     6.5      thms
     6.6      |> Conjunction.intr_balanced
     6.7 -    |> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
     6.8 +    |> Raw_Simplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
     6.9      |> Thm.implies_intr asm
    6.10      |> Thm.generalize ([], params) 0
    6.11      |> AxClass.unoverload thy
     7.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Fri Dec 17 16:25:21 2010 +0100
     7.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Fri Dec 17 17:08:56 2010 +0100
     7.3 @@ -39,12 +39,12 @@
     7.4    branches: scheme_branch list,
     7.5    cases: scheme_case list}
     7.6  
     7.7 -val ind_atomize = MetaSimplifier.rewrite true @{thms induct_atomize}
     7.8 -val ind_rulify = MetaSimplifier.rewrite true @{thms induct_rulify}
     7.9 +val ind_atomize = Raw_Simplifier.rewrite true @{thms induct_atomize}
    7.10 +val ind_rulify = Raw_Simplifier.rewrite true @{thms induct_rulify}
    7.11  
    7.12  fun meta thm = thm RS eq_reflection
    7.13  
    7.14 -val sum_prod_conv = MetaSimplifier.rewrite true
    7.15 +val sum_prod_conv = Raw_Simplifier.rewrite true
    7.16    (map meta (@{thm split_conv} :: @{thms sum.cases}))
    7.17  
    7.18  fun term_conv thy cv t =
     8.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Dec 17 16:25:21 2010 +0100
     8.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Dec 17 17:08:56 2010 +0100
     8.3 @@ -219,9 +219,9 @@
     8.4          fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
     8.5            |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)
     8.6          val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
     8.7 -        val case_th = MetaSimplifier.simplify true
     8.8 +        val case_th = Raw_Simplifier.simplify true
     8.9            (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
    8.10 -        val prems' = maps (dest_conjunct_prem o MetaSimplifier.simplify true tuple_rew_rules) prems
    8.11 +        val prems' = maps (dest_conjunct_prem o Raw_Simplifier.simplify true tuple_rew_rules) prems
    8.12          val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
    8.13          val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
    8.14            OF (replicate nargs @{thm refl})
     9.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Dec 17 16:25:21 2010 +0100
     9.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Dec 17 17:08:56 2010 +0100
     9.3 @@ -969,7 +969,7 @@
     9.4      val Tcons = datatype_names_of_case_name thy case_name
     9.5      val ths = maps (instantiated_case_rewrites thy) Tcons
     9.6    in
     9.7 -    MetaSimplifier.rewrite_term thy
     9.8 +    Raw_Simplifier.rewrite_term thy
     9.9        (map (fn th => th RS @{thm eq_reflection}) ths) [] t
    9.10    end
    9.11  
    9.12 @@ -1044,7 +1044,7 @@
    9.13  fun peephole_optimisation thy intro =
    9.14    let
    9.15      val process =
    9.16 -      MetaSimplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init_global thy))
    9.17 +      Raw_Simplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init_global thy))
    9.18      fun process_False intro_t =
    9.19        if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
    9.20      fun process_True intro_t =
    10.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Dec 17 16:25:21 2010 +0100
    10.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Dec 17 17:08:56 2010 +0100
    10.3 @@ -96,7 +96,7 @@
    10.4        (Const (@{const_name If}, _)) =>
    10.5          let
    10.6            val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
    10.7 -          val atom' = MetaSimplifier.rewrite_term thy
    10.8 +          val atom' = Raw_Simplifier.rewrite_term thy
    10.9              (map (fn th => th RS @{thm eq_reflection}) [@{thm if_bool_eq_disj}, if_beta]) [] atom
   10.10            val _ = assert (not (atom = atom'))
   10.11          in
   10.12 @@ -212,7 +212,7 @@
   10.13            error ("unexpected specification for constant " ^ quote constname ^ ":\n"
   10.14              ^ commas (map (quote o Display.string_of_thm_global thy) specs))
   10.15        val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
   10.16 -      val intros = map (MetaSimplifier.rewrite_rule
   10.17 +      val intros = map (Raw_Simplifier.rewrite_rule
   10.18            [if_beta RS @{thm eq_reflection}]) intros
   10.19        val _ = print_specs options thy "normalized intros" intros
   10.20        (*val intros = maps (split_cases thy) intros*)
    11.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Dec 17 16:25:21 2010 +0100
    11.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Dec 17 17:08:56 2010 +0100
    11.3 @@ -127,7 +127,7 @@
    11.4            fun param_rewrite prem =
    11.5              param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem)))
    11.6            val SOME rew_eq = find_first param_rewrite prems'
    11.7 -          val param_prem' = MetaSimplifier.rewrite_rule
    11.8 +          val param_prem' = Raw_Simplifier.rewrite_rule
    11.9              (map (fn th => th RS @{thm eq_reflection})
   11.10                [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
   11.11              param_prem
    12.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Dec 17 16:25:21 2010 +0100
    12.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Dec 17 17:08:56 2010 +0100
    12.3 @@ -486,7 +486,7 @@
    12.4          val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
    12.5          val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
    12.6          val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
    12.7 -        val thm3 = MetaSimplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
    12.8 +        val thm3 = Raw_Simplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
    12.9          val (insp, inst) =
   12.10            if ty_c = ty_d
   12.11            then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
    13.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Fri Dec 17 16:25:21 2010 +0100
    13.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Fri Dec 17 17:08:56 2010 +0100
    13.3 @@ -73,8 +73,8 @@
    13.4  functor CaseSplitFUN(Data : CASE_SPLIT_DATA) =
    13.5  struct
    13.6  
    13.7 -val rulify_goals = MetaSimplifier.rewrite_goals_rule Data.rulify;
    13.8 -val atomize_goals = MetaSimplifier.rewrite_goals_rule Data.atomize;
    13.9 +val rulify_goals = Raw_Simplifier.rewrite_goals_rule Data.rulify;
   13.10 +val atomize_goals = Raw_Simplifier.rewrite_goals_rule Data.atomize;
   13.11  
   13.12  (* beta-eta contract the theorem *)
   13.13  fun beta_eta_contract thm =
    14.1 --- a/src/HOL/Tools/TFL/rules.ML	Fri Dec 17 16:25:21 2010 +0100
    14.2 +++ b/src/HOL/Tools/TFL/rules.ML	Fri Dec 17 17:08:56 2010 +0100
    14.3 @@ -422,7 +422,7 @@
    14.4  fun SUBS thl =
    14.5    rewrite_rule (map (fn th => th RS eq_reflection handle THM _ => th) thl);
    14.6  
    14.7 -val rew_conv = MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE));
    14.8 +val rew_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE));
    14.9  
   14.10  fun simpl_conv ss thl ctm =
   14.11   rew_conv (ss addsimps thl) ctm RS meta_eq_to_obj_eq;
   14.12 @@ -669,7 +669,7 @@
   14.13                       val eq = Logic.strip_imp_concl imp
   14.14                       val lhs = tych(get_lhs eq)
   14.15                       val ss' = Simplifier.add_prems (map ASSUME ants) ss
   14.16 -                     val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs
   14.17 +                     val lhs_eq_lhs1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs
   14.18                         handle Utils.ERR _ => Thm.reflexive lhs
   14.19                       val dummy = print_thms "proven:" [lhs_eq_lhs1]
   14.20                       val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
   14.21 @@ -690,7 +690,7 @@
   14.22                    val QeqQ1 = pbeta_reduce (tych Q)
   14.23                    val Q1 = #2(Dcterm.dest_eq(cconcl QeqQ1))
   14.24                    val ss' = Simplifier.add_prems (map ASSUME ants1) ss
   14.25 -                  val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1
   14.26 +                  val Q1eeqQ2 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1
   14.27                                  handle Utils.ERR _ => Thm.reflexive Q1
   14.28                    val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
   14.29                    val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
   14.30 @@ -715,7 +715,7 @@
   14.31                   let val tych = cterm_of thy
   14.32                       val ants1 = map tych ants
   14.33                       val ss' = Simplifier.add_prems (map ASSUME ants1) ss
   14.34 -                     val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
   14.35 +                     val Q_eeq_Q1 = Raw_Simplifier.rewrite_cterm
   14.36                          (false,true,false) (prover used') ss' (tych Q)
   14.37                        handle Utils.ERR _ => Thm.reflexive (tych Q)
   14.38                       val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
   14.39 @@ -783,7 +783,7 @@
   14.40      end
   14.41      val ctm = cprop_of th
   14.42      val names = OldTerm.add_term_names (term_of ctm, [])
   14.43 -    val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
   14.44 +    val th1 = Raw_Simplifier.rewrite_cterm (false,true,false)
   14.45        (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm
   14.46      val th2 = Thm.equal_elim th1 th
   14.47   in
    15.1 --- a/src/HOL/Tools/inductive.ML	Fri Dec 17 16:25:21 2010 +0100
    15.2 +++ b/src/HOL/Tools/inductive.ML	Fri Dec 17 17:08:56 2010 +0100
    15.3 @@ -282,7 +282,7 @@
    15.4  
    15.5  val bad_app = "Inductive predicate must be applied to parameter(s) ";
    15.6  
    15.7 -fun atomize_term thy = MetaSimplifier.rewrite_term thy inductive_atomize [];
    15.8 +fun atomize_term thy = Raw_Simplifier.rewrite_term thy inductive_atomize [];
    15.9  
   15.10  in
   15.11  
    16.1 --- a/src/HOL/ex/Numeral.thy	Fri Dec 17 16:25:21 2010 +0100
    16.2 +++ b/src/HOL/ex/Numeral.thy	Fri Dec 17 17:08:56 2010 +0100
    16.3 @@ -592,14 +592,14 @@
    16.4      fun cdest_minus ct = case (rev o snd o Drule.strip_comb) ct of [n, m] => (m, n);
    16.5      fun attach_num ct = (dest_num (Thm.term_of ct), ct);
    16.6      fun cdifference t = (pairself (attach_num o cdest_of_num) o cdest_minus) t;
    16.7 -    val simplify = MetaSimplifier.rewrite false (map mk_meta_eq @{thms Dig_plus_eval});
    16.8 +    val simplify = Raw_Simplifier.rewrite false (map mk_meta_eq @{thms Dig_plus_eval});
    16.9      fun cert ck cl cj = @{thm eqTrueE} OF [@{thm meta_eq_to_obj_eq}
   16.10        OF [simplify (Drule.list_comb (@{cterm "op = :: num \<Rightarrow> _"},
   16.11          [Drule.list_comb (@{cterm "op + :: num \<Rightarrow> _"}, [ck, cl]), cj]))]];
   16.12    in fn phi => fn _ => fn ct => case try cdifference ct
   16.13     of NONE => (NONE)
   16.14      | SOME ((k, ck), (l, cl)) => SOME (let val j = k - l in if j = 0
   16.15 -        then MetaSimplifier.rewrite false [mk_meta_eq (Morphism.thm phi @{thm Dig_of_num_zero})] ct
   16.16 +        then Raw_Simplifier.rewrite false [mk_meta_eq (Morphism.thm phi @{thm Dig_of_num_zero})] ct
   16.17          else mk_meta_eq (let
   16.18            val cj = Thm.cterm_of (Thm.theory_of_cterm ct) (mk_num (abs j));
   16.19          in
    17.1 --- a/src/Pure/IsaMakefile	Fri Dec 17 16:25:21 2010 +0100
    17.2 +++ b/src/Pure/IsaMakefile	Fri Dec 17 17:08:56 2010 +0100
    17.3 @@ -227,7 +227,6 @@
    17.4    item_net.ML						\
    17.5    library.ML						\
    17.6    logic.ML						\
    17.7 -  meta_simplifier.ML					\
    17.8    more_thm.ML						\
    17.9    morphism.ML						\
   17.10    name.ML						\
   17.11 @@ -238,6 +237,7 @@
   17.12    proofterm.ML						\
   17.13    pure_setup.ML						\
   17.14    pure_thy.ML						\
   17.15 +  raw_simplifier.ML					\
   17.16    search.ML						\
   17.17    sign.ML						\
   17.18    simplifier.ML						\
    18.1 --- a/src/Pure/Isar/attrib.ML	Fri Dec 17 16:25:21 2010 +0100
    18.2 +++ b/src/Pure/Isar/attrib.ML	Fri Dec 17 17:08:56 2010 +0100
    18.3 @@ -415,9 +415,9 @@
    18.4    register_config Unify.search_bound_raw #>
    18.5    register_config Unify.trace_simp_raw #>
    18.6    register_config Unify.trace_types_raw #>
    18.7 -  register_config MetaSimplifier.simp_depth_limit_raw #>
    18.8 -  register_config MetaSimplifier.simp_trace_depth_limit_raw #>
    18.9 -  register_config MetaSimplifier.simp_debug_raw #>
   18.10 -  register_config MetaSimplifier.simp_trace_raw));
   18.11 +  register_config Raw_Simplifier.simp_depth_limit_raw #>
   18.12 +  register_config Raw_Simplifier.simp_trace_depth_limit_raw #>
   18.13 +  register_config Raw_Simplifier.simp_debug_raw #>
   18.14 +  register_config Raw_Simplifier.simp_trace_raw));
   18.15  
   18.16  end;
    19.1 --- a/src/Pure/Isar/element.ML	Fri Dec 17 16:25:21 2010 +0100
    19.2 +++ b/src/Pure/Isar/element.ML	Fri Dec 17 17:08:56 2010 +0100
    19.3 @@ -224,7 +224,7 @@
    19.4      val thy = ProofContext.theory_of ctxt;
    19.5      val cert = Thm.cterm_of thy;
    19.6  
    19.7 -    val th = MetaSimplifier.norm_hhf raw_th;
    19.8 +    val th = Raw_Simplifier.norm_hhf raw_th;
    19.9      val is_elim = Object_Logic.is_elim th;
   19.10  
   19.11      val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body false ctxt);
   19.12 @@ -318,7 +318,7 @@
   19.13    end;
   19.14  
   19.15  fun conclude_witness (Witness (_, th)) =
   19.16 -  Thm.close_derivation (MetaSimplifier.norm_hhf_protect (Goal.conclude th));
   19.17 +  Thm.close_derivation (Raw_Simplifier.norm_hhf_protect (Goal.conclude th));
   19.18  
   19.19  fun pretty_witness ctxt witn =
   19.20    let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in
   19.21 @@ -459,8 +459,8 @@
   19.22  fun eq_morphism thy thms = if null thms then NONE else SOME (Morphism.morphism
   19.23   {binding = I,
   19.24    typ = I,
   19.25 -  term = MetaSimplifier.rewrite_term thy thms [],
   19.26 -  fact = map (MetaSimplifier.rewrite_rule thms)});
   19.27 +  term = Raw_Simplifier.rewrite_term thy thms [],
   19.28 +  fact = map (Raw_Simplifier.rewrite_rule thms)});
   19.29  
   19.30  
   19.31  (* transfer to theory using closure *)
    20.1 --- a/src/Pure/Isar/expression.ML	Fri Dec 17 16:25:21 2010 +0100
    20.2 +++ b/src/Pure/Isar/expression.ML	Fri Dec 17 17:08:56 2010 +0100
    20.3 @@ -647,18 +647,18 @@
    20.4      val cert = Thm.cterm_of defs_thy;
    20.5  
    20.6      val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
    20.7 -      MetaSimplifier.rewrite_goals_tac [pred_def] THEN
    20.8 +      rewrite_goals_tac [pred_def] THEN
    20.9        Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
   20.10        Tactic.compose_tac (false,
   20.11          Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
   20.12  
   20.13      val conjuncts =
   20.14        (Drule.equal_elim_rule2 OF [body_eq,
   20.15 -        MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
   20.16 +        Raw_Simplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
   20.17        |> Conjunction.elim_balanced (length ts);
   20.18      val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
   20.19        Element.prove_witness defs_ctxt t
   20.20 -       (MetaSimplifier.rewrite_goals_tac defs THEN
   20.21 +       (rewrite_goals_tac defs THEN
   20.22          Tactic.compose_tac (false, ax, 0) 1));
   20.23    in ((statement, intro, axioms), defs_thy) end;
   20.24  
    21.1 --- a/src/Pure/Isar/generic_target.ML	Fri Dec 17 16:25:21 2010 +0100
    21.2 +++ b/src/Pure/Isar/generic_target.ML	Fri Dec 17 17:08:56 2010 +0100
    21.3 @@ -58,7 +58,7 @@
    21.4      (*term and type parameters*)
    21.5      val crhs = Thm.cterm_of thy rhs;
    21.6      val (defs, rhs') = Local_Defs.export_cterm lthy thy_ctxt crhs ||> Thm.term_of;
    21.7 -    val rhs_conv = MetaSimplifier.rewrite true defs crhs;
    21.8 +    val rhs_conv = Raw_Simplifier.rewrite true defs crhs;
    21.9  
   21.10      val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' [];
   21.11      val T = Term.fastype_of rhs;
   21.12 @@ -107,7 +107,7 @@
   21.13      (*export assumes/defines*)
   21.14      val th = Goal.norm_result raw_th;
   21.15      val (defs, th') = Local_Defs.export ctxt thy_ctxt th;
   21.16 -    val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume)
   21.17 +    val assms = map (Raw_Simplifier.rewrite_rule defs o Thm.assume)
   21.18        (Assumption.all_assms_of ctxt);
   21.19      val nprems = Thm.nprems_of th' - Thm.nprems_of th;
   21.20  
    22.1 --- a/src/Pure/Isar/local_defs.ML	Fri Dec 17 16:25:21 2010 +0100
    22.2 +++ b/src/Pure/Isar/local_defs.ML	Fri Dec 17 17:08:56 2010 +0100
    22.3 @@ -182,7 +182,7 @@
    22.4  end;
    22.5  
    22.6  fun contract ctxt defs ct th =
    22.7 -  trans_props ctxt [th, Thm.symmetric (MetaSimplifier.rewrite true defs ct)];
    22.8 +  trans_props ctxt [th, Thm.symmetric (Raw_Simplifier.rewrite true defs ct)];
    22.9  
   22.10  
   22.11  (** defived definitions **)
   22.12 @@ -208,8 +208,8 @@
   22.13  (* meta rewrite rules *)
   22.14  
   22.15  fun meta_rewrite_conv ctxt =
   22.16 -  MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE))
   22.17 -    (MetaSimplifier.context ctxt MetaSimplifier.empty_ss
   22.18 +  Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
   22.19 +    (Raw_Simplifier.context ctxt empty_ss
   22.20        addeqcongs [Drule.equals_cong]    (*protect meta-level equality*)
   22.21        addsimps (Rules.get (Context.Proof ctxt)));
   22.22  
   22.23 @@ -220,11 +220,11 @@
   22.24  
   22.25  fun meta f ctxt = f o map (meta_rewrite_rule ctxt);
   22.26  
   22.27 -val unfold       = meta MetaSimplifier.rewrite_rule;
   22.28 -val unfold_goals = meta MetaSimplifier.rewrite_goals_rule;
   22.29 -val unfold_tac   = meta MetaSimplifier.rewrite_goals_tac;
   22.30 -val fold         = meta MetaSimplifier.fold_rule;
   22.31 -val fold_tac     = meta MetaSimplifier.fold_goals_tac;
   22.32 +val unfold       = meta Raw_Simplifier.rewrite_rule;
   22.33 +val unfold_goals = meta Raw_Simplifier.rewrite_goals_rule;
   22.34 +val unfold_tac   = meta Raw_Simplifier.rewrite_goals_tac;
   22.35 +val fold         = meta Raw_Simplifier.fold_rule;
   22.36 +val fold_tac     = meta Raw_Simplifier.fold_goals_tac;
   22.37  
   22.38  
   22.39  (* derived defs -- potentially within the object-logic *)
   22.40 @@ -244,7 +244,7 @@
   22.41        in
   22.42          Goal.prove ctxt' frees [] prop (K (ALLGOALS
   22.43            (CONVERSION (meta_rewrite_conv ctxt') THEN'
   22.44 -            MetaSimplifier.rewrite_goal_tac [def] THEN'
   22.45 +            rewrite_goal_tac [def] THEN'
   22.46              resolve_tac [Drule.reflexive_thm])))
   22.47          handle ERROR msg => cat_error msg "Failed to prove definitional specification"
   22.48        end;
    23.1 --- a/src/Pure/Isar/object_logic.ML	Fri Dec 17 16:25:21 2010 +0100
    23.2 +++ b/src/Pure/Isar/object_logic.ML	Fri Dec 17 17:08:56 2010 +0100
    23.3 @@ -178,10 +178,10 @@
    23.4  (* atomize *)
    23.5  
    23.6  fun atomize_term thy =
    23.7 -  drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) [];
    23.8 +  drop_judgment thy o Raw_Simplifier.rewrite_term thy (get_atomize thy) [];
    23.9  
   23.10  fun atomize ct =
   23.11 -  MetaSimplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
   23.12 +  Raw_Simplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct;
   23.13  
   23.14  fun atomize_prems ct =
   23.15    if Logic.has_meta_prems (Thm.term_of ct) then
   23.16 @@ -195,11 +195,11 @@
   23.17  
   23.18  (* rulify *)
   23.19  
   23.20 -fun rulify_term thy = MetaSimplifier.rewrite_term thy (get_rulify thy) [];
   23.21 -fun rulify_tac i st = MetaSimplifier.rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
   23.22 +fun rulify_term thy = Raw_Simplifier.rewrite_term thy (get_rulify thy) [];
   23.23 +fun rulify_tac i st = rewrite_goal_tac (get_rulify (Thm.theory_of_thm st)) i st;
   23.24  
   23.25  fun gen_rulify full thm =
   23.26 -  MetaSimplifier.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
   23.27 +  Raw_Simplifier.simplify full (get_rulify (Thm.theory_of_thm thm)) thm
   23.28    |> Drule.gen_all |> Thm.strip_shyps |> Drule.zero_var_indexes;
   23.29  
   23.30  val rulify = gen_rulify true;
    24.1 --- a/src/Pure/Isar/obtain.ML	Fri Dec 17 16:25:21 2010 +0100
    24.2 +++ b/src/Pure/Isar/obtain.ML	Fri Dec 17 17:08:56 2010 +0100
    24.3 @@ -193,7 +193,7 @@
    24.4      val rule =
    24.5        (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) (Goal.init (cert thesis)) of
    24.6          NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
    24.7 -      | SOME th => check_result ctxt thesis (MetaSimplifier.norm_hhf (Goal.conclude th)));
    24.8 +      | SOME th => check_result ctxt thesis (Raw_Simplifier.norm_hhf (Goal.conclude th)));
    24.9  
   24.10      val closed_rule = Thm.forall_intr (cert (Free thesis_var)) rule;
   24.11      val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
   24.12 @@ -299,7 +299,7 @@
   24.13      val goal = Var (("guess", 0), propT);
   24.14      fun print_result ctxt' (k, [(s, [_, th])]) =
   24.15        Proof_Display.print_results int ctxt' (k, [(s, [th])]);
   24.16 -    val before_qed = SOME (Method.primitive_text (Goal.conclude #> MetaSimplifier.norm_hhf #>
   24.17 +    val before_qed = SOME (Method.primitive_text (Goal.conclude #> Raw_Simplifier.norm_hhf #>
   24.18          (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
   24.19      fun after_qed [[_, res]] =
   24.20        Proof.end_block #> guess_context (check_result ctxt thesis res);
    25.1 --- a/src/Pure/Isar/rule_cases.ML	Fri Dec 17 16:25:21 2010 +0100
    25.2 +++ b/src/Pure/Isar/rule_cases.ML	Fri Dec 17 17:08:56 2010 +0100
    25.3 @@ -189,14 +189,14 @@
    25.4  
    25.5  fun unfold_prems n defs th =
    25.6    if null defs then th
    25.7 -  else Conv.fconv_rule (Conv.prems_conv n (MetaSimplifier.rewrite true defs)) th;
    25.8 +  else Conv.fconv_rule (Conv.prems_conv n (Raw_Simplifier.rewrite true defs)) th;
    25.9  
   25.10  fun unfold_prems_concls defs th =
   25.11    if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
   25.12    else
   25.13      Conv.fconv_rule
   25.14        (Conv.concl_conv ~1 (Conjunction.convs
   25.15 -        (Conv.prems_conv ~1 (MetaSimplifier.rewrite true defs)))) th;
   25.16 +        (Conv.prems_conv ~1 (Raw_Simplifier.rewrite true defs)))) th;
   25.17  
   25.18  in
   25.19  
    26.1 --- a/src/Pure/ProofGeneral/preferences.ML	Fri Dec 17 16:25:21 2010 +0100
    26.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Fri Dec 17 17:08:56 2010 +0100
    26.3 @@ -147,10 +147,10 @@
    26.4      "Show leading question mark of variable name"];
    26.5  
    26.6  val tracing_preferences =
    26.7 - [bool_pref MetaSimplifier.simp_trace_default
    26.8 + [bool_pref Raw_Simplifier.simp_trace_default
    26.9      "trace-simplifier"
   26.10      "Trace simplification rules.",
   26.11 -  nat_pref MetaSimplifier.simp_trace_depth_limit_default
   26.12 +  nat_pref Raw_Simplifier.simp_trace_depth_limit_default
   26.13      "trace-simplifier-depth"
   26.14      "Trace simplifier depth limit.",
   26.15    bool_pref trace_rules
    27.1 --- a/src/Pure/ROOT.ML	Fri Dec 17 16:25:21 2010 +0100
    27.2 +++ b/src/Pure/ROOT.ML	Fri Dec 17 17:08:56 2010 +0100
    27.3 @@ -153,7 +153,7 @@
    27.4  use "tactical.ML";
    27.5  use "search.ML";
    27.6  use "tactic.ML";
    27.7 -use "meta_simplifier.ML";
    27.8 +use "raw_simplifier.ML";
    27.9  use "conjunction.ML";
   27.10  use "assumption.ML";
   27.11  use "display.ML";
    28.1 --- a/src/Pure/assumption.ML	Fri Dec 17 16:25:21 2010 +0100
    28.2 +++ b/src/Pure/assumption.ML	Fri Dec 17 17:08:56 2010 +0100
    28.3 @@ -48,7 +48,7 @@
    28.4  *)
    28.5  fun presume_export _ = assume_export false;
    28.6  
    28.7 -val assume = MetaSimplifier.norm_hhf o Thm.assume;
    28.8 +val assume = Raw_Simplifier.norm_hhf o Thm.assume;
    28.9  
   28.10  
   28.11  
   28.12 @@ -110,9 +110,9 @@
   28.13  (* export *)
   28.14  
   28.15  fun export is_goal inner outer =
   28.16 -  MetaSimplifier.norm_hhf_protect #>
   28.17 +  Raw_Simplifier.norm_hhf_protect #>
   28.18    fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
   28.19 -  MetaSimplifier.norm_hhf_protect;
   28.20 +  Raw_Simplifier.norm_hhf_protect;
   28.21  
   28.22  fun export_term inner outer =
   28.23    fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
    29.1 --- a/src/Pure/axclass.ML	Fri Dec 17 16:25:21 2010 +0100
    29.2 +++ b/src/Pure/axclass.ML	Fri Dec 17 17:08:56 2010 +0100
    29.3 @@ -322,11 +322,11 @@
    29.4  
    29.5  fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts);
    29.6  
    29.7 -fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
    29.8 -fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
    29.9 +fun unoverload thy = Raw_Simplifier.simplify true (inst_thms thy);
   29.10 +fun overload thy = Raw_Simplifier.simplify true (map Thm.symmetric (inst_thms thy));
   29.11  
   29.12 -fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
   29.13 -fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
   29.14 +fun unoverload_conv thy = Raw_Simplifier.rewrite true (inst_thms thy);
   29.15 +fun overload_conv thy = Raw_Simplifier.rewrite true (map Thm.symmetric (inst_thms thy));
   29.16  
   29.17  fun lookup_inst_param consts params (c, T) =
   29.18    (case get_inst_tyco consts (c, T) of
    30.1 --- a/src/Pure/goal.ML	Fri Dec 17 16:25:21 2010 +0100
    30.2 +++ b/src/Pure/goal.ML	Fri Dec 17 17:08:56 2010 +0100
    30.3 @@ -99,7 +99,7 @@
    30.4  
    30.5  val norm_result =
    30.6    Drule.flexflex_unique
    30.7 -  #> MetaSimplifier.norm_hhf_protect
    30.8 +  #> Raw_Simplifier.norm_hhf_protect
    30.9    #> Thm.strip_shyps
   30.10    #> Drule.zero_var_indexes;
   30.11  
   30.12 @@ -278,7 +278,7 @@
   30.13    rtac Drule.asm_rl  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
   30.14    THEN' SUBGOAL (fn (t, i) =>
   30.15      if Drule.is_norm_hhf t then all_tac
   30.16 -    else MetaSimplifier.rewrite_goal_tac Drule.norm_hhf_eqs i);
   30.17 +    else rewrite_goal_tac Drule.norm_hhf_eqs i);
   30.18  
   30.19  fun compose_hhf_tac th i st =
   30.20    PRIMSEQ (Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
   30.21 @@ -296,7 +296,7 @@
   30.22      val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
   30.23      val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
   30.24      val tacs = Rs |> map (fn R =>
   30.25 -      Tactic.etac (MetaSimplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
   30.26 +      Tactic.etac (Raw_Simplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
   30.27    in fold_rev (curry op APPEND') tacs (K no_tac) i end);
   30.28  
   30.29  
    31.1 --- a/src/Pure/meta_simplifier.ML	Fri Dec 17 16:25:21 2010 +0100
    31.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    31.3 @@ -1,1379 +0,0 @@
    31.4 -(*  Title:      Pure/meta_simplifier.ML
    31.5 -    Author:     Tobias Nipkow and Stefan Berghofer, TU Muenchen
    31.6 -
    31.7 -Meta-level Simplification.
    31.8 -*)
    31.9 -
   31.10 -infix 4
   31.11 -  addsimps delsimps addeqcongs deleqcongs addcongs delcongs addsimprocs delsimprocs
   31.12 -  setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler
   31.13 -  setloop' setloop addloop addloop' delloop setSSolver addSSolver setSolver addSolver;
   31.14 -
   31.15 -signature BASIC_META_SIMPLIFIER =
   31.16 -sig
   31.17 -  val simp_depth_limit: int Config.T
   31.18 -  val simp_trace_depth_limit: int Config.T
   31.19 -  val simp_debug: bool Config.T
   31.20 -  val simp_trace: bool Config.T
   31.21 -  type rrule
   31.22 -  val eq_rrule: rrule * rrule -> bool
   31.23 -  type simpset
   31.24 -  type proc
   31.25 -  type solver
   31.26 -  val mk_solver': string -> (simpset -> int -> tactic) -> solver
   31.27 -  val mk_solver: string -> (thm list -> int -> tactic) -> solver
   31.28 -  val empty_ss: simpset
   31.29 -  val merge_ss: simpset * simpset -> simpset
   31.30 -  val dest_ss: simpset ->
   31.31 -   {simps: (string * thm) list,
   31.32 -    procs: (string * cterm list) list,
   31.33 -    congs: (string * thm) list,
   31.34 -    weak_congs: string list,
   31.35 -    loopers: string list,
   31.36 -    unsafe_solvers: string list,
   31.37 -    safe_solvers: string list}
   31.38 -  type simproc
   31.39 -  val eq_simproc: simproc * simproc -> bool
   31.40 -  val morph_simproc: morphism -> simproc -> simproc
   31.41 -  val make_simproc: {name: string, lhss: cterm list,
   31.42 -    proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc
   31.43 -  val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc
   31.44 -  val prems_of_ss: simpset -> thm list
   31.45 -  val addsimps: simpset * thm list -> simpset
   31.46 -  val delsimps: simpset * thm list -> simpset
   31.47 -  val addeqcongs: simpset * thm list -> simpset
   31.48 -  val deleqcongs: simpset * thm list -> simpset
   31.49 -  val addcongs: simpset * thm list -> simpset
   31.50 -  val delcongs: simpset * thm list -> simpset
   31.51 -  val addsimprocs: simpset * simproc list -> simpset
   31.52 -  val delsimprocs: simpset * simproc list -> simpset
   31.53 -  val mksimps: simpset -> thm -> thm list
   31.54 -  val setmksimps: simpset * (simpset -> thm -> thm list) -> simpset
   31.55 -  val setmkcong: simpset * (simpset -> thm -> thm) -> simpset
   31.56 -  val setmksym: simpset * (simpset -> thm -> thm option) -> simpset
   31.57 -  val setmkeqTrue: simpset * (simpset -> thm -> thm option) -> simpset
   31.58 -  val settermless: simpset * (term * term -> bool) -> simpset
   31.59 -  val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
   31.60 -  val setloop': simpset * (simpset -> int -> tactic) -> simpset
   31.61 -  val setloop: simpset * (int -> tactic) -> simpset
   31.62 -  val addloop': simpset * (string * (simpset -> int -> tactic)) -> simpset
   31.63 -  val addloop: simpset * (string * (int -> tactic)) -> simpset
   31.64 -  val delloop: simpset * string -> simpset
   31.65 -  val setSSolver: simpset * solver -> simpset
   31.66 -  val addSSolver: simpset * solver -> simpset
   31.67 -  val setSolver: simpset * solver -> simpset
   31.68 -  val addSolver: simpset * solver -> simpset
   31.69 -
   31.70 -  val rewrite_rule: thm list -> thm -> thm
   31.71 -  val rewrite_goals_rule: thm list -> thm -> thm
   31.72 -  val rewrite_goals_tac: thm list -> tactic
   31.73 -  val rewrite_goal_tac: thm list -> int -> tactic
   31.74 -  val rewtac: thm -> tactic
   31.75 -  val prune_params_tac: tactic
   31.76 -  val fold_rule: thm list -> thm -> thm
   31.77 -  val fold_goals_tac: thm list -> tactic
   31.78 -  val norm_hhf: thm -> thm
   31.79 -  val norm_hhf_protect: thm -> thm
   31.80 -end;
   31.81 -
   31.82 -signature META_SIMPLIFIER =
   31.83 -sig
   31.84 -  include BASIC_META_SIMPLIFIER
   31.85 -  exception SIMPLIFIER of string * thm
   31.86 -  val internal_ss: simpset ->
   31.87 -   {rules: rrule Net.net,
   31.88 -    prems: thm list,
   31.89 -    bounds: int * ((string * typ) * string) list,
   31.90 -    depth: int * bool Unsynchronized.ref,
   31.91 -    context: Proof.context option} *
   31.92 -   {congs: (string * thm) list * string list,
   31.93 -    procs: proc Net.net,
   31.94 -    mk_rews:
   31.95 -     {mk: simpset -> thm -> thm list,
   31.96 -      mk_cong: simpset -> thm -> thm,
   31.97 -      mk_sym: simpset -> thm -> thm option,
   31.98 -      mk_eq_True: simpset -> thm -> thm option,
   31.99 -      reorient: theory -> term list -> term -> term -> bool},
  31.100 -    termless: term * term -> bool,
  31.101 -    subgoal_tac: simpset -> int -> tactic,
  31.102 -    loop_tacs: (string * (simpset -> int -> tactic)) list,
  31.103 -    solvers: solver list * solver list}
  31.104 -  val add_simp: thm -> simpset -> simpset
  31.105 -  val del_simp: thm -> simpset -> simpset
  31.106 -  val solver: simpset -> solver -> int -> tactic
  31.107 -  val simp_depth_limit_raw: Config.raw
  31.108 -  val clear_ss: simpset -> simpset
  31.109 -  val simproc_global_i: theory -> string -> term list
  31.110 -    -> (theory -> simpset -> term -> thm option) -> simproc
  31.111 -  val simproc_global: theory -> string -> string list
  31.112 -    -> (theory -> simpset -> term -> thm option) -> simproc
  31.113 -  val simp_trace_depth_limit_raw: Config.raw
  31.114 -  val simp_trace_depth_limit_default: int Unsynchronized.ref
  31.115 -  val simp_trace_default: bool Unsynchronized.ref
  31.116 -  val simp_trace_raw: Config.raw
  31.117 -  val simp_debug_raw: Config.raw
  31.118 -  val add_prems: thm list -> simpset -> simpset
  31.119 -  val inherit_context: simpset -> simpset -> simpset
  31.120 -  val the_context: simpset -> Proof.context
  31.121 -  val context: Proof.context -> simpset -> simpset
  31.122 -  val global_context: theory  -> simpset -> simpset
  31.123 -  val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
  31.124 -  val debug_bounds: bool Unsynchronized.ref
  31.125 -  val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
  31.126 -  val set_solvers: solver list -> simpset -> simpset
  31.127 -  val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> conv
  31.128 -  val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
  31.129 -  val rewrite_thm: bool * bool * bool ->
  31.130 -    (simpset -> thm -> thm option) -> simpset -> thm -> thm
  31.131 -  val rewrite_goal_rule: bool * bool * bool ->
  31.132 -    (simpset -> thm -> thm option) -> simpset -> int -> thm -> thm
  31.133 -  val asm_rewrite_goal_tac: bool * bool * bool ->
  31.134 -    (simpset -> tactic) -> simpset -> int -> tactic
  31.135 -  val rewrite: bool -> thm list -> conv
  31.136 -  val simplify: bool -> thm list -> thm -> thm
  31.137 -end;
  31.138 -
  31.139 -structure MetaSimplifier: META_SIMPLIFIER =
  31.140 -struct
  31.141 -
  31.142 -(** datatype simpset **)
  31.143 -
  31.144 -(* rewrite rules *)
  31.145 -
  31.146 -type rrule =
  31.147 - {thm: thm,         (*the rewrite rule*)
  31.148 -  name: string,     (*name of theorem from which rewrite rule was extracted*)
  31.149 -  lhs: term,        (*the left-hand side*)
  31.150 -  elhs: cterm,      (*the etac-contracted lhs*)
  31.151 -  extra: bool,      (*extra variables outside of elhs*)
  31.152 -  fo: bool,         (*use first-order matching*)
  31.153 -  perm: bool};      (*the rewrite rule is permutative*)
  31.154 -
  31.155 -(*
  31.156 -Remarks:
  31.157 -  - elhs is used for matching,
  31.158 -    lhs only for preservation of bound variable names;
  31.159 -  - fo is set iff
  31.160 -    either elhs is first-order (no Var is applied),
  31.161 -      in which case fo-matching is complete,
  31.162 -    or elhs is not a pattern,
  31.163 -      in which case there is nothing better to do;
  31.164 -*)
  31.165 -
  31.166 -fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
  31.167 -  Thm.eq_thm_prop (thm1, thm2);
  31.168 -
  31.169 -
  31.170 -(* simplification sets, procedures, and solvers *)
  31.171 -
  31.172 -(*A simpset contains data required during conversion:
  31.173 -    rules: discrimination net of rewrite rules;
  31.174 -    prems: current premises;
  31.175 -    bounds: maximal index of bound variables already used
  31.176 -      (for generating new names when rewriting under lambda abstractions);
  31.177 -    depth: simp_depth and exceeded flag;
  31.178 -    congs: association list of congruence rules and
  31.179 -           a list of `weak' congruence constants.
  31.180 -           A congruence is `weak' if it avoids normalization of some argument.
  31.181 -    procs: discrimination net of simplification procedures
  31.182 -      (functions that prove rewrite rules on the fly);
  31.183 -    mk_rews:
  31.184 -      mk: turn simplification thms into rewrite rules;
  31.185 -      mk_cong: prepare congruence rules;
  31.186 -      mk_sym: turn == around;
  31.187 -      mk_eq_True: turn P into P == True;
  31.188 -    termless: relation for ordered rewriting;*)
  31.189 -
  31.190 -datatype simpset =
  31.191 -  Simpset of
  31.192 -   {rules: rrule Net.net,
  31.193 -    prems: thm list,
  31.194 -    bounds: int * ((string * typ) * string) list,
  31.195 -    depth: int * bool Unsynchronized.ref,
  31.196 -    context: Proof.context option} *
  31.197 -   {congs: (string * thm) list * string list,
  31.198 -    procs: proc Net.net,
  31.199 -    mk_rews:
  31.200 -     {mk: simpset -> thm -> thm list,
  31.201 -      mk_cong: simpset -> thm -> thm,
  31.202 -      mk_sym: simpset -> thm -> thm option,
  31.203 -      mk_eq_True: simpset -> thm -> thm option,
  31.204 -      reorient: theory -> term list -> term -> term -> bool},
  31.205 -    termless: term * term -> bool,
  31.206 -    subgoal_tac: simpset -> int -> tactic,
  31.207 -    loop_tacs: (string * (simpset -> int -> tactic)) list,
  31.208 -    solvers: solver list * solver list}
  31.209 -and proc =
  31.210 -  Proc of
  31.211 -   {name: string,
  31.212 -    lhs: cterm,
  31.213 -    proc: simpset -> cterm -> thm option,
  31.214 -    id: stamp * thm list}
  31.215 -and solver =
  31.216 -  Solver of
  31.217 -   {name: string,
  31.218 -    solver: simpset -> int -> tactic,
  31.219 -    id: stamp};
  31.220 -
  31.221 -
  31.222 -fun internal_ss (Simpset args) = args;
  31.223 -
  31.224 -fun make_ss1 (rules, prems, bounds, depth, context) =
  31.225 -  {rules = rules, prems = prems, bounds = bounds, depth = depth, context = context};
  31.226 -
  31.227 -fun map_ss1 f {rules, prems, bounds, depth, context} =
  31.228 -  make_ss1 (f (rules, prems, bounds, depth, context));
  31.229 -
  31.230 -fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =
  31.231 -  {congs = congs, procs = procs, mk_rews = mk_rews, termless = termless,
  31.232 -    subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers};
  31.233 -
  31.234 -fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers} =
  31.235 -  make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
  31.236 -
  31.237 -fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
  31.238 -
  31.239 -fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2);
  31.240 -fun map_simpset2 f (Simpset (r1, r2)) = Simpset (r1, map_ss2 f r2);
  31.241 -
  31.242 -fun prems_of_ss (Simpset ({prems, ...}, _)) = prems;
  31.243 -
  31.244 -fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) =
  31.245 -  s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
  31.246 -fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2);
  31.247 -
  31.248 -fun mk_solver' name solver = Solver {name = name, solver = solver, id = stamp ()};
  31.249 -fun mk_solver name solver = mk_solver' name (solver o prems_of_ss);
  31.250 -
  31.251 -fun solver_name (Solver {name, ...}) = name;
  31.252 -fun solver ss (Solver {solver = tac, ...}) = tac ss;
  31.253 -fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2);
  31.254 -
  31.255 -
  31.256 -(* simp depth *)
  31.257 -
  31.258 -val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100));
  31.259 -val simp_depth_limit = Config.int simp_depth_limit_raw;
  31.260 -
  31.261 -val simp_trace_depth_limit_default = Unsynchronized.ref 1;
  31.262 -val simp_trace_depth_limit_raw = Config.declare "simp_trace_depth_limit"
  31.263 -  (fn _ => Config.Int (! simp_trace_depth_limit_default));
  31.264 -val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw;
  31.265 -
  31.266 -fun simp_trace_depth_limit_of NONE = ! simp_trace_depth_limit_default
  31.267 -  | simp_trace_depth_limit_of (SOME ctxt) = Config.get ctxt simp_trace_depth_limit;
  31.268 -
  31.269 -fun trace_depth (Simpset ({depth = (depth, exceeded), context, ...}, _)) msg =
  31.270 -  if depth > simp_trace_depth_limit_of context then
  31.271 -    if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true)
  31.272 -  else
  31.273 -    (tracing (enclose "[" "]" (string_of_int depth) ^ msg); exceeded := false);
  31.274 -
  31.275 -val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
  31.276 -  (rules, prems, bounds,
  31.277 -    (depth + 1,
  31.278 -      if depth = simp_trace_depth_limit_of context then Unsynchronized.ref false else exceeded), context));
  31.279 -
  31.280 -fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
  31.281 -
  31.282 -
  31.283 -(* diagnostics *)
  31.284 -
  31.285 -exception SIMPLIFIER of string * thm;
  31.286 -
  31.287 -val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false));
  31.288 -val simp_debug = Config.bool simp_debug_raw;
  31.289 -
  31.290 -val simp_trace_default = Unsynchronized.ref false;
  31.291 -val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default));
  31.292 -val simp_trace = Config.bool simp_trace_raw;
  31.293 -
  31.294 -fun if_enabled (Simpset ({context, ...}, _)) flag f =
  31.295 -  (case context of
  31.296 -    SOME ctxt => if Config.get ctxt flag then f ctxt else ()
  31.297 -  | NONE => ())
  31.298 -
  31.299 -fun if_visible (Simpset ({context, ...}, _)) f x =
  31.300 -  (case context of
  31.301 -    SOME ctxt => if Context_Position.is_visible ctxt then f x else ()
  31.302 -  | NONE => ());
  31.303 -
  31.304 -local
  31.305 -
  31.306 -fun prnt ss warn a = if warn then warning a else trace_depth ss a;
  31.307 -
  31.308 -fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t =
  31.309 -  let
  31.310 -    val names = Term.declare_term_names t Name.context;
  31.311 -    val xs = rev (#1 (Name.variants (rev (map #2 bs)) names));
  31.312 -    fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T));
  31.313 -  in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
  31.314 -
  31.315 -fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^
  31.316 -  Syntax.string_of_term ctxt
  31.317 -    (if Config.get ctxt simp_debug then t else show_bounds ss t));
  31.318 -
  31.319 -in
  31.320 -
  31.321 -fun print_term_global ss warn a thy t =
  31.322 -  print_term ss warn (K a) t (ProofContext.init_global thy);
  31.323 -
  31.324 -fun debug warn a ss = if_enabled ss simp_debug (fn _ => prnt ss warn (a ()));
  31.325 -fun trace warn a ss = if_enabled ss simp_trace (fn _ => prnt ss warn (a ()));
  31.326 -
  31.327 -fun debug_term warn a ss t = if_enabled ss simp_debug (print_term ss warn a t);
  31.328 -fun trace_term warn a ss t = if_enabled ss simp_trace (print_term ss warn a t);
  31.329 -
  31.330 -fun trace_cterm warn a ss ct =
  31.331 -  if_enabled ss simp_trace (print_term ss warn a (Thm.term_of ct));
  31.332 -
  31.333 -fun trace_thm a ss th =
  31.334 -  if_enabled ss simp_trace (print_term ss false a (Thm.full_prop_of th));
  31.335 -
  31.336 -fun trace_named_thm a ss (th, name) =
  31.337 -  if_enabled ss simp_trace (print_term ss false
  31.338 -    (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
  31.339 -    (Thm.full_prop_of th));
  31.340 -
  31.341 -fun warn_thm a ss th =
  31.342 -  print_term_global ss true a (Thm.theory_of_thm th) (Thm.full_prop_of th);
  31.343 -
  31.344 -fun cond_warn_thm a ss th = if_visible ss (fn () => warn_thm a ss th) ();
  31.345 -
  31.346 -end;
  31.347 -
  31.348 -
  31.349 -
  31.350 -(** simpset operations **)
  31.351 -
  31.352 -(* context *)
  31.353 -
  31.354 -fun eq_bound (x: string, (y, _)) = x = y;
  31.355 -
  31.356 -fun add_bound bound = map_simpset1 (fn (rules, prems, (count, bounds), depth, context) =>
  31.357 -  (rules, prems, (count + 1, bound :: bounds), depth, context));
  31.358 -
  31.359 -fun add_prems ths = map_simpset1 (fn (rules, prems, bounds, depth, context) =>
  31.360 -  (rules, ths @ prems, bounds, depth, context));
  31.361 -
  31.362 -fun inherit_context (Simpset ({bounds, depth, context, ...}, _)) =
  31.363 -  map_simpset1 (fn (rules, prems, _, _, _) => (rules, prems, bounds, depth, context));
  31.364 -
  31.365 -fun the_context (Simpset ({context = SOME ctxt, ...}, _)) = ctxt
  31.366 -  | the_context _ = raise Fail "Simplifier: no proof context in simpset";
  31.367 -
  31.368 -fun context ctxt =
  31.369 -  map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt));
  31.370 -
  31.371 -val global_context = context o ProofContext.init_global;
  31.372 -
  31.373 -fun activate_context thy ss =
  31.374 -  let
  31.375 -    val ctxt = the_context ss;
  31.376 -    val ctxt' = ctxt
  31.377 -      |> Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt))
  31.378 -      |> Context_Position.set_visible false;
  31.379 -  in context ctxt' ss end;
  31.380 -
  31.381 -fun with_context ctxt f ss = inherit_context ss (f (context ctxt ss));
  31.382 -
  31.383 -
  31.384 -(* maintain simp rules *)
  31.385 -
  31.386 -(* FIXME: it seems that the conditions on extra variables are too liberal if
  31.387 -prems are nonempty: does solving the prems really guarantee instantiation of
  31.388 -all its Vars? Better: a dynamic check each time a rule is applied.
  31.389 -*)
  31.390 -fun rewrite_rule_extra_vars prems elhs erhs =
  31.391 -  let
  31.392 -    val elhss = elhs :: prems;
  31.393 -    val tvars = fold Term.add_tvars elhss [];
  31.394 -    val vars = fold Term.add_vars elhss [];
  31.395 -  in
  31.396 -    erhs |> Term.exists_type (Term.exists_subtype
  31.397 -      (fn TVar v => not (member (op =) tvars v) | _ => false)) orelse
  31.398 -    erhs |> Term.exists_subterm
  31.399 -      (fn Var v => not (member (op =) vars v) | _ => false)
  31.400 -  end;
  31.401 -
  31.402 -fun rrule_extra_vars elhs thm =
  31.403 -  rewrite_rule_extra_vars [] (term_of elhs) (Thm.full_prop_of thm);
  31.404 -
  31.405 -fun mk_rrule2 {thm, name, lhs, elhs, perm} =
  31.406 -  let
  31.407 -    val t = term_of elhs;
  31.408 -    val fo = Pattern.first_order t orelse not (Pattern.pattern t);
  31.409 -    val extra = rrule_extra_vars elhs thm;
  31.410 -  in {thm = thm, name = name, lhs = lhs, elhs = elhs, extra = extra, fo = fo, perm = perm} end;
  31.411 -
  31.412 -fun del_rrule (rrule as {thm, elhs, ...}) ss =
  31.413 -  ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) =>
  31.414 -    (Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, bounds, depth, context))
  31.415 -  handle Net.DELETE => (cond_warn_thm "Rewrite rule not in simpset:" ss thm; ss);
  31.416 -
  31.417 -fun insert_rrule (rrule as {thm, name, ...}) ss =
  31.418 - (trace_named_thm (fn () => "Adding rewrite rule") ss (thm, name);
  31.419 -  ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) =>
  31.420 -    let
  31.421 -      val rrule2 as {elhs, ...} = mk_rrule2 rrule;
  31.422 -      val rules' = Net.insert_term eq_rrule (term_of elhs, rrule2) rules;
  31.423 -    in (rules', prems, bounds, depth, context) end)
  31.424 -  handle Net.INSERT => (cond_warn_thm "Ignoring duplicate rewrite rule:" ss thm; ss));
  31.425 -
  31.426 -fun vperm (Var _, Var _) = true
  31.427 -  | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
  31.428 -  | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
  31.429 -  | vperm (t, u) = (t = u);
  31.430 -
  31.431 -fun var_perm (t, u) =
  31.432 -  vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
  31.433 -
  31.434 -(*simple test for looping rewrite rules and stupid orientations*)
  31.435 -fun default_reorient thy prems lhs rhs =
  31.436 -  rewrite_rule_extra_vars prems lhs rhs
  31.437 -    orelse
  31.438 -  is_Var (head_of lhs)
  31.439 -    orelse
  31.440 -(* turns t = x around, which causes a headache if x is a local variable -
  31.441 -   usually it is very useful :-(
  31.442 -  is_Free rhs andalso not(is_Free lhs) andalso not(Logic.occs(rhs,lhs))
  31.443 -  andalso not(exists_subterm is_Var lhs)
  31.444 -    orelse
  31.445 -*)
  31.446 -  exists (fn t => Logic.occs (lhs, t)) (rhs :: prems)
  31.447 -    orelse
  31.448 -  null prems andalso Pattern.matches thy (lhs, rhs)
  31.449 -    (*the condition "null prems" is necessary because conditional rewrites
  31.450 -      with extra variables in the conditions may terminate although
  31.451 -      the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*)
  31.452 -    orelse
  31.453 -  is_Const lhs andalso not (is_Const rhs);
  31.454 -
  31.455 -fun decomp_simp thm =
  31.456 -  let
  31.457 -    val thy = Thm.theory_of_thm thm;
  31.458 -    val prop = Thm.prop_of thm;
  31.459 -    val prems = Logic.strip_imp_prems prop;
  31.460 -    val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
  31.461 -    val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
  31.462 -      raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
  31.463 -    val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
  31.464 -    val elhs = if term_of elhs aconv term_of lhs then lhs else elhs;  (*share identical copies*)
  31.465 -    val erhs = Envir.eta_contract (term_of rhs);
  31.466 -    val perm =
  31.467 -      var_perm (term_of elhs, erhs) andalso
  31.468 -      not (term_of elhs aconv erhs) andalso
  31.469 -      not (is_Var (term_of elhs));
  31.470 -  in (thy, prems, term_of lhs, elhs, term_of rhs, perm) end;
  31.471 -
  31.472 -fun decomp_simp' thm =
  31.473 -  let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
  31.474 -    if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
  31.475 -    else (lhs, rhs)
  31.476 -  end;
  31.477 -
  31.478 -fun mk_eq_True (ss as Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
  31.479 -  (case mk_eq_True ss thm of
  31.480 -    NONE => []
  31.481 -  | SOME eq_True =>
  31.482 -      let
  31.483 -        val (_, _, lhs, elhs, _, _) = decomp_simp eq_True;
  31.484 -      in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end);
  31.485 -
  31.486 -(*create the rewrite rule and possibly also the eq_True variant,
  31.487 -  in case there are extra vars on the rhs*)
  31.488 -fun rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm2) =
  31.489 -  let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in
  31.490 -    if rewrite_rule_extra_vars [] lhs rhs then
  31.491 -      mk_eq_True ss (thm2, name) @ [rrule]
  31.492 -    else [rrule]
  31.493 -  end;
  31.494 -
  31.495 -fun mk_rrule ss (thm, name) =
  31.496 -  let val (_, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
  31.497 -    if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
  31.498 -    else
  31.499 -      (*weak test for loops*)
  31.500 -      if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (term_of elhs)
  31.501 -      then mk_eq_True ss (thm, name)
  31.502 -      else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
  31.503 -  end;
  31.504 -
  31.505 -fun orient_rrule ss (thm, name) =
  31.506 -  let
  31.507 -    val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm;
  31.508 -    val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = ss;
  31.509 -  in
  31.510 -    if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
  31.511 -    else if reorient thy prems lhs rhs then
  31.512 -      if reorient thy prems rhs lhs
  31.513 -      then mk_eq_True ss (thm, name)
  31.514 -      else
  31.515 -        (case mk_sym ss thm of
  31.516 -          NONE => []
  31.517 -        | SOME thm' =>
  31.518 -            let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm'
  31.519 -            in rrule_eq_True (thm', name, lhs', elhs', rhs', ss, thm) end)
  31.520 -    else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
  31.521 -  end;
  31.522 -
  31.523 -fun extract_rews (ss as Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
  31.524 -  maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ss thm)) thms;
  31.525 -
  31.526 -fun extract_safe_rrules (ss, thm) =
  31.527 -  maps (orient_rrule ss) (extract_rews (ss, [thm]));
  31.528 -
  31.529 -
  31.530 -(* add/del rules explicitly *)
  31.531 -
  31.532 -fun comb_simps comb mk_rrule (ss, thms) =
  31.533 -  let
  31.534 -    val rews = extract_rews (ss, thms);
  31.535 -  in fold (fold comb o mk_rrule) rews ss end;
  31.536 -
  31.537 -fun ss addsimps thms =
  31.538 -  comb_simps insert_rrule (mk_rrule ss) (ss, thms);
  31.539 -
  31.540 -fun ss delsimps thms =
  31.541 -  comb_simps del_rrule (map mk_rrule2 o mk_rrule ss) (ss, thms);
  31.542 -
  31.543 -fun add_simp thm ss = ss addsimps [thm];
  31.544 -fun del_simp thm ss = ss delsimps [thm];
  31.545 -
  31.546 -
  31.547 -(* congs *)
  31.548 -
  31.549 -fun cong_name (Const (a, _)) = SOME a
  31.550 -  | cong_name (Free (a, _)) = SOME ("Free: " ^ a)
  31.551 -  | cong_name _ = NONE;
  31.552 -
  31.553 -local
  31.554 -
  31.555 -fun is_full_cong_prems [] [] = true
  31.556 -  | is_full_cong_prems [] _ = false
  31.557 -  | is_full_cong_prems (p :: prems) varpairs =
  31.558 -      (case Logic.strip_assums_concl p of
  31.559 -        Const ("==", _) $ lhs $ rhs =>
  31.560 -          let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in
  31.561 -            is_Var x andalso forall is_Bound xs andalso
  31.562 -            not (has_duplicates (op =) xs) andalso xs = ys andalso
  31.563 -            member (op =) varpairs (x, y) andalso
  31.564 -            is_full_cong_prems prems (remove (op =) (x, y) varpairs)
  31.565 -          end
  31.566 -      | _ => false);
  31.567 -
  31.568 -fun is_full_cong thm =
  31.569 -  let
  31.570 -    val prems = prems_of thm and concl = concl_of thm;
  31.571 -    val (lhs, rhs) = Logic.dest_equals concl;
  31.572 -    val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs;
  31.573 -  in
  31.574 -    f = g andalso not (has_duplicates (op =) (xs @ ys)) andalso length xs = length ys andalso
  31.575 -    is_full_cong_prems prems (xs ~~ ys)
  31.576 -  end;
  31.577 -
  31.578 -fun add_cong (ss, thm) = ss |>
  31.579 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  31.580 -    let
  31.581 -      val (lhs, _) = Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
  31.582 -        handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
  31.583 -    (*val lhs = Envir.eta_contract lhs;*)
  31.584 -      val a = the (cong_name (head_of (term_of lhs))) handle Option.Option =>
  31.585 -        raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
  31.586 -      val (xs, weak) = congs;
  31.587 -      val _ =
  31.588 -        if AList.defined (op =) xs a
  31.589 -        then if_visible ss warning ("Overwriting congruence rule for " ^ quote a)
  31.590 -        else ();
  31.591 -      val xs' = AList.update (op =) (a, thm) xs;
  31.592 -      val weak' = if is_full_cong thm then weak else a :: weak;
  31.593 -    in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
  31.594 -
  31.595 -fun del_cong (ss, thm) = ss |>
  31.596 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  31.597 -    let
  31.598 -      val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
  31.599 -        raise SIMPLIFIER ("Congruence not a meta-equality", thm);
  31.600 -    (*val lhs = Envir.eta_contract lhs;*)
  31.601 -      val a = the (cong_name (head_of lhs)) handle Option.Option =>
  31.602 -        raise SIMPLIFIER ("Congruence must start with a constant", thm);
  31.603 -      val (xs, _) = congs;
  31.604 -      val xs' = filter_out (fn (x : string, _) => x = a) xs;
  31.605 -      val weak' = xs' |> map_filter (fn (a, thm) =>
  31.606 -        if is_full_cong thm then NONE else SOME a);
  31.607 -    in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
  31.608 -
  31.609 -fun mk_cong (ss as Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f ss;
  31.610 -
  31.611 -in
  31.612 -
  31.613 -val (op addeqcongs) = Library.foldl add_cong;
  31.614 -val (op deleqcongs) = Library.foldl del_cong;
  31.615 -
  31.616 -fun ss addcongs congs = ss addeqcongs map (mk_cong ss) congs;
  31.617 -fun ss delcongs congs = ss deleqcongs map (mk_cong ss) congs;
  31.618 -
  31.619 -end;
  31.620 -
  31.621 -
  31.622 -(* simprocs *)
  31.623 -
  31.624 -datatype simproc =
  31.625 -  Simproc of
  31.626 -    {name: string,
  31.627 -     lhss: cterm list,
  31.628 -     proc: morphism -> simpset -> cterm -> thm option,
  31.629 -     id: stamp * thm list};
  31.630 -
  31.631 -fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2);
  31.632 -
  31.633 -fun morph_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
  31.634 -  Simproc
  31.635 -   {name = name,
  31.636 -    lhss = map (Morphism.cterm phi) lhss,
  31.637 -    proc = Morphism.transform phi proc,
  31.638 -    id = (s, Morphism.fact phi ths)};
  31.639 -
  31.640 -fun make_simproc {name, lhss, proc, identifier} =
  31.641 -  Simproc {name = name, lhss = lhss, proc = proc, id = (stamp (), identifier)};
  31.642 -
  31.643 -fun mk_simproc name lhss proc =
  31.644 -  make_simproc {name = name, lhss = lhss, proc = fn _ => fn ss => fn ct =>
  31.645 -    proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []};
  31.646 -
  31.647 -(* FIXME avoid global thy and Logic.varify_global *)
  31.648 -fun simproc_global_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global);
  31.649 -fun simproc_global thy name = simproc_global_i thy name o map (Syntax.read_term_global thy);
  31.650 -
  31.651 -
  31.652 -local
  31.653 -
  31.654 -fun add_proc (proc as Proc {name, lhs, ...}) ss =
  31.655 - (trace_cterm false (fn () => "Adding simplification procedure " ^ quote name ^ " for") ss lhs;
  31.656 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  31.657 -    (congs, Net.insert_term eq_proc (term_of lhs, proc) procs,
  31.658 -      mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
  31.659 -  handle Net.INSERT =>
  31.660 -    (if_visible ss warning ("Ignoring duplicate simplification procedure " ^ quote name); ss));
  31.661 -
  31.662 -fun del_proc (proc as Proc {name, lhs, ...}) ss =
  31.663 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  31.664 -    (congs, Net.delete_term eq_proc (term_of lhs, proc) procs,
  31.665 -      mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
  31.666 -  handle Net.DELETE =>
  31.667 -    (if_visible ss warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ss);
  31.668 -
  31.669 -fun prep_procs (Simproc {name, lhss, proc, id}) =
  31.670 -  lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id});
  31.671 -
  31.672 -in
  31.673 -
  31.674 -fun ss addsimprocs ps = fold (fold add_proc o prep_procs) ps ss;
  31.675 -fun ss delsimprocs ps = fold (fold del_proc o prep_procs) ps ss;
  31.676 -
  31.677 -end;
  31.678 -
  31.679 -
  31.680 -(* mk_rews *)
  31.681 -
  31.682 -local
  31.683 -
  31.684 -fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True, reorient},
  31.685 -      termless, subgoal_tac, loop_tacs, solvers) =>
  31.686 -  let
  31.687 -    val (mk', mk_cong', mk_sym', mk_eq_True', reorient') =
  31.688 -      f (mk, mk_cong, mk_sym, mk_eq_True, reorient);
  31.689 -    val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True',
  31.690 -      reorient = reorient'};
  31.691 -  in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end);
  31.692 -
  31.693 -in
  31.694 -
  31.695 -fun mksimps (ss as Simpset (_, {mk_rews = {mk, ...}, ...})) = mk ss;
  31.696 -
  31.697 -fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
  31.698 -  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  31.699 -
  31.700 -fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) =>
  31.701 -  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  31.702 -
  31.703 -fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) =>
  31.704 -  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  31.705 -
  31.706 -fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) =>
  31.707 -  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  31.708 -
  31.709 -fun set_reorient reorient = map_mk_rews (fn (mk, mk_cong, mk_sym, mk_eq_True, _) =>
  31.710 -  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  31.711 -
  31.712 -end;
  31.713 -
  31.714 -
  31.715 -(* termless *)
  31.716 -
  31.717 -fun ss settermless termless = ss |>
  31.718 -  map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) =>
  31.719 -   (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
  31.720 -
  31.721 -
  31.722 -(* tactics *)
  31.723 -
  31.724 -fun ss setsubgoaler subgoal_tac = ss |>
  31.725 -  map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) =>
  31.726 -   (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
  31.727 -
  31.728 -fun ss setloop' tac = ss |>
  31.729 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) =>
  31.730 -   (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers));
  31.731 -
  31.732 -fun ss setloop tac = ss setloop' (K tac);
  31.733 -
  31.734 -fun ss addloop' (name, tac) = ss |>
  31.735 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  31.736 -    (congs, procs, mk_rews, termless, subgoal_tac,
  31.737 -     (if AList.defined (op =) loop_tacs name
  31.738 -      then if_visible ss warning ("Overwriting looper " ^ quote name)
  31.739 -      else (); AList.update (op =) (name, tac) loop_tacs), solvers));
  31.740 -
  31.741 -fun ss addloop (name, tac) = ss addloop' (name, K tac);
  31.742 -
  31.743 -fun ss delloop name = ss |>
  31.744 -  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  31.745 -    (congs, procs, mk_rews, termless, subgoal_tac,
  31.746 -     (if AList.defined (op =) loop_tacs name then ()
  31.747 -      else if_visible ss warning ("No such looper in simpset: " ^ quote name);
  31.748 -      AList.delete (op =) name loop_tacs), solvers));
  31.749 -
  31.750 -fun ss setSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  31.751 -  subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
  31.752 -    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));
  31.753 -
  31.754 -fun ss addSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  31.755 -  subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
  31.756 -    subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers)));
  31.757 -
  31.758 -fun ss setSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  31.759 -  subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless,
  31.760 -    subgoal_tac, loop_tacs, ([solver], solvers)));
  31.761 -
  31.762 -fun ss addSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  31.763 -  subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
  31.764 -    subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers)));
  31.765 -
  31.766 -fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless,
  31.767 -  subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless,
  31.768 -  subgoal_tac, loop_tacs, (solvers, solvers)));
  31.769 -
  31.770 -
  31.771 -(* empty *)
  31.772 -
  31.773 -fun init_ss mk_rews termless subgoal_tac solvers =
  31.774 -  make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false), NONE),
  31.775 -    (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
  31.776 -
  31.777 -fun clear_ss (ss as Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) =
  31.778 -  init_ss mk_rews termless subgoal_tac solvers
  31.779 -  |> inherit_context ss;
  31.780 -
  31.781 -val empty_ss =
  31.782 -  init_ss
  31.783 -    {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
  31.784 -      mk_cong = K I,
  31.785 -      mk_sym = K (SOME o Drule.symmetric_fun),
  31.786 -      mk_eq_True = K (K NONE),
  31.787 -      reorient = default_reorient}
  31.788 -    Term_Ord.termless (K (K no_tac)) ([], []);
  31.789 -
  31.790 -
  31.791 -(* merge *)  (*NOTE: ignores some fields of 2nd simpset*)
  31.792 -
  31.793 -fun merge_ss (ss1, ss2) =
  31.794 -  if pointer_eq (ss1, ss2) then ss1
  31.795 -  else
  31.796 -    let
  31.797 -      val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1, context = _},
  31.798 -       {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac,
  31.799 -        loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
  31.800 -      val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _},
  31.801 -       {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
  31.802 -        loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
  31.803 -
  31.804 -      val rules' = Net.merge eq_rrule (rules1, rules2);
  31.805 -      val prems' = Thm.merge_thms (prems1, prems2);
  31.806 -      val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
  31.807 -      val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
  31.808 -      val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2);
  31.809 -      val weak' = merge (op =) (weak1, weak2);
  31.810 -      val procs' = Net.merge eq_proc (procs1, procs2);
  31.811 -      val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
  31.812 -      val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
  31.813 -      val solvers' = merge eq_solver (solvers1, solvers2);
  31.814 -    in
  31.815 -      make_simpset ((rules', prems', bounds', depth', NONE), ((congs', weak'), procs',
  31.816 -        mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
  31.817 -    end;
  31.818 -
  31.819 -
  31.820 -(* dest_ss *)
  31.821 -
  31.822 -fun dest_ss (Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...})) =
  31.823 - {simps = Net.entries rules
  31.824 -    |> map (fn {name, thm, ...} => (name, thm)),
  31.825 -  procs = Net.entries procs
  31.826 -    |> map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
  31.827 -    |> partition_eq (eq_snd eq_procid)
  31.828 -    |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)),
  31.829 -  congs = #1 congs,
  31.830 -  weak_congs = #2 congs,
  31.831 -  loopers = map fst loop_tacs,
  31.832 -  unsafe_solvers = map solver_name (#1 solvers),
  31.833 -  safe_solvers = map solver_name (#2 solvers)};
  31.834 -
  31.835 -
  31.836 -
  31.837 -(** rewriting **)
  31.838 -
  31.839 -(*
  31.840 -  Uses conversions, see:
  31.841 -    L C Paulson, A higher-order implementation of rewriting,
  31.842 -    Science of Computer Programming 3 (1983), pages 119-149.
  31.843 -*)
  31.844 -
  31.845 -fun check_conv msg ss thm thm' =
  31.846 -  let
  31.847 -    val thm'' = Thm.transitive thm thm' handle THM _ =>
  31.848 -     Thm.transitive thm (Thm.transitive
  31.849 -       (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
  31.850 -  in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
  31.851 -  handle THM _ =>
  31.852 -    let
  31.853 -      val _ $ _ $ prop0 = Thm.prop_of thm;
  31.854 -    in
  31.855 -      trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';
  31.856 -      trace_term false (fn () => "Should have proved:") ss prop0;
  31.857 -      NONE
  31.858 -    end;
  31.859 -
  31.860 -
  31.861 -(* mk_procrule *)
  31.862 -
  31.863 -fun mk_procrule ss thm =
  31.864 -  let val (_, prems, lhs, elhs, rhs, _) = decomp_simp thm in
  31.865 -    if rewrite_rule_extra_vars prems lhs rhs
  31.866 -    then (cond_warn_thm "Extra vars on rhs:" ss thm; [])
  31.867 -    else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}]
  31.868 -  end;
  31.869 -
  31.870 -
  31.871 -(* rewritec: conversion to apply the meta simpset to a term *)
  31.872 -
  31.873 -(*Since the rewriting strategy is bottom-up, we avoid re-normalizing already
  31.874 -  normalized terms by carrying around the rhs of the rewrite rule just
  31.875 -  applied. This is called the `skeleton'. It is decomposed in parallel
  31.876 -  with the term. Once a Var is encountered, the corresponding term is
  31.877 -  already in normal form.
  31.878 -  skel0 is a dummy skeleton that is to enforce complete normalization.*)
  31.879 -
  31.880 -val skel0 = Bound 0;
  31.881 -
  31.882 -(*Use rhs as skeleton only if the lhs does not contain unnormalized bits.
  31.883 -  The latter may happen iff there are weak congruence rules for constants
  31.884 -  in the lhs.*)
  31.885 -
  31.886 -fun uncond_skel ((_, weak), (lhs, rhs)) =
  31.887 -  if null weak then rhs  (*optimization*)
  31.888 -  else if exists_Const (member (op =) weak o #1) lhs then skel0
  31.889 -  else rhs;
  31.890 -
  31.891 -(*Behaves like unconditional rule if rhs does not contain vars not in the lhs.
  31.892 -  Otherwise those vars may become instantiated with unnormalized terms
  31.893 -  while the premises are solved.*)
  31.894 -
  31.895 -fun cond_skel (args as (_, (lhs, rhs))) =
  31.896 -  if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args
  31.897 -  else skel0;
  31.898 -
  31.899 -(*
  31.900 -  Rewriting -- we try in order:
  31.901 -    (1) beta reduction
  31.902 -    (2) unconditional rewrite rules
  31.903 -    (3) conditional rewrite rules
  31.904 -    (4) simplification procedures
  31.905 -
  31.906 -  IMPORTANT: rewrite rules must not introduce new Vars or TVars!
  31.907 -*)
  31.908 -
  31.909 -fun rewritec (prover, thyt, maxt) ss t =
  31.910 -  let
  31.911 -    val ctxt = the_context ss;
  31.912 -    val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss;
  31.913 -    val eta_thm = Thm.eta_conversion t;
  31.914 -    val eta_t' = Thm.rhs_of eta_thm;
  31.915 -    val eta_t = term_of eta_t';
  31.916 -    fun rew {thm, name, lhs, elhs, extra, fo, perm} =
  31.917 -      let
  31.918 -        val prop = Thm.prop_of thm;
  31.919 -        val (rthm, elhs') =
  31.920 -          if maxt = ~1 orelse not extra then (thm, elhs)
  31.921 -          else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs);
  31.922 -        val insts =
  31.923 -          if fo then Thm.first_order_match (elhs', eta_t')
  31.924 -          else Thm.match (elhs', eta_t');
  31.925 -        val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
  31.926 -        val prop' = Thm.prop_of thm';
  31.927 -        val unconditional = (Logic.count_prems prop' = 0);
  31.928 -        val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
  31.929 -      in
  31.930 -        if perm andalso not (termless (rhs', lhs'))
  31.931 -        then (trace_named_thm (fn () => "Cannot apply permutative rewrite rule") ss (thm, name);
  31.932 -              trace_thm (fn () => "Term does not become smaller:") ss thm'; NONE)
  31.933 -        else (trace_named_thm (fn () => "Applying instance of rewrite rule") ss (thm, name);
  31.934 -           if unconditional
  31.935 -           then
  31.936 -             (trace_thm (fn () => "Rewriting:") ss thm';
  31.937 -              let
  31.938 -                val lr = Logic.dest_equals prop;
  31.939 -                val SOME thm'' = check_conv false ss eta_thm thm';
  31.940 -              in SOME (thm'', uncond_skel (congs, lr)) end)
  31.941 -           else
  31.942 -             (trace_thm (fn () => "Trying to rewrite:") ss thm';
  31.943 -              if simp_depth ss > Config.get ctxt simp_depth_limit
  31.944 -              then
  31.945 -                let
  31.946 -                  val s = "simp_depth_limit exceeded - giving up";
  31.947 -                  val _ = trace false (fn () => s) ss;
  31.948 -                  val _ = if_visible ss warning s;
  31.949 -                in NONE end
  31.950 -              else
  31.951 -              case prover ss thm' of
  31.952 -                NONE => (trace_thm (fn () => "FAILED") ss thm'; NONE)
  31.953 -              | SOME thm2 =>
  31.954 -                  (case check_conv true ss eta_thm thm2 of
  31.955 -                     NONE => NONE |
  31.956 -                     SOME thm2' =>
  31.957 -                       let val concl = Logic.strip_imp_concl prop
  31.958 -                           val lr = Logic.dest_equals concl
  31.959 -                       in SOME (thm2', cond_skel (congs, lr)) end)))
  31.960 -      end
  31.961 -
  31.962 -    fun rews [] = NONE
  31.963 -      | rews (rrule :: rrules) =
  31.964 -          let val opt = rew rrule handle Pattern.MATCH => NONE
  31.965 -          in case opt of NONE => rews rrules | some => some end;
  31.966 -
  31.967 -    fun sort_rrules rrs =
  31.968 -      let
  31.969 -        fun is_simple ({thm, ...}: rrule) =
  31.970 -          (case Thm.prop_of thm of
  31.971 -            Const ("==", _) $ _ $ _ => true
  31.972 -          | _ => false);
  31.973 -        fun sort [] (re1, re2) = re1 @ re2
  31.974 -          | sort (rr :: rrs) (re1, re2) =
  31.975 -              if is_simple rr
  31.976 -              then sort rrs (rr :: re1, re2)
  31.977 -              else sort rrs (re1, rr :: re2);
  31.978 -      in sort rrs ([], []) end;
  31.979 -
  31.980 -    fun proc_rews [] = NONE
  31.981 -      | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
  31.982 -          if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then
  31.983 -            (debug_term false (fn () => "Trying procedure " ^ quote name ^ " on:") ss eta_t;
  31.984 -             case proc ss eta_t' of
  31.985 -               NONE => (debug false (fn () => "FAILED") ss; proc_rews ps)
  31.986 -             | SOME raw_thm =>
  31.987 -                 (trace_thm (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:")
  31.988 -                   ss raw_thm;
  31.989 -                  (case rews (mk_procrule ss raw_thm) of
  31.990 -                    NONE => (trace_cterm true (fn () => "IGNORED result of simproc " ^ quote name ^
  31.991 -                      " -- does not match") ss t; proc_rews ps)
  31.992 -                  | some => some)))
  31.993 -          else proc_rews ps;
  31.994 -  in
  31.995 -    (case eta_t of
  31.996 -      Abs _ $ _ => SOME (Thm.transitive eta_thm (Thm.beta_conversion false eta_t'), skel0)
  31.997 -    | _ =>
  31.998 -      (case rews (sort_rrules (Net.match_term rules eta_t)) of
  31.999 -        NONE => proc_rews (Net.match_term procs eta_t)
 31.1000 -      | some => some))
 31.1001 -  end;
 31.1002 -
 31.1003 -
 31.1004 -(* conversion to apply a congruence rule to a term *)
 31.1005 -
 31.1006 -fun congc prover ss maxt cong t =
 31.1007 -  let val rthm = Thm.incr_indexes (maxt + 1) cong;
 31.1008 -      val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
 31.1009 -      val insts = Thm.match (rlhs, t)
 31.1010 -      (* Thm.match can raise Pattern.MATCH;
 31.1011 -         is handled when congc is called *)
 31.1012 -      val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
 31.1013 -      val _ = trace_thm (fn () => "Applying congruence rule:") ss thm';
 31.1014 -      fun err (msg, thm) = (trace_thm (fn () => msg) ss thm; NONE)
 31.1015 -  in
 31.1016 -    (case prover thm' of
 31.1017 -      NONE => err ("Congruence proof failed.  Could not prove", thm')
 31.1018 -    | SOME thm2 =>
 31.1019 -        (case check_conv true ss (Drule.beta_eta_conversion t) thm2 of
 31.1020 -          NONE => err ("Congruence proof failed.  Should not have proved", thm2)
 31.1021 -        | SOME thm2' =>
 31.1022 -            if op aconv (pairself term_of (Thm.dest_equals (cprop_of thm2')))
 31.1023 -            then NONE else SOME thm2'))
 31.1024 -  end;
 31.1025 -
 31.1026 -val (cA, (cB, cC)) =
 31.1027 -  apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong)));
 31.1028 -
 31.1029 -fun transitive1 NONE NONE = NONE
 31.1030 -  | transitive1 (SOME thm1) NONE = SOME thm1
 31.1031 -  | transitive1 NONE (SOME thm2) = SOME thm2
 31.1032 -  | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2)
 31.1033 -
 31.1034 -fun transitive2 thm = transitive1 (SOME thm);
 31.1035 -fun transitive3 thm = transitive1 thm o SOME;
 31.1036 -
 31.1037 -fun bottomc ((simprem, useprem, mutsimp), prover, thy, maxidx) =
 31.1038 -  let
 31.1039 -    fun botc skel ss t =
 31.1040 -          if is_Var skel then NONE
 31.1041 -          else
 31.1042 -          (case subc skel ss t of
 31.1043 -             some as SOME thm1 =>
 31.1044 -               (case rewritec (prover, thy, maxidx) ss (Thm.rhs_of thm1) of
 31.1045 -                  SOME (thm2, skel2) =>
 31.1046 -                    transitive2 (Thm.transitive thm1 thm2)
 31.1047 -                      (botc skel2 ss (Thm.rhs_of thm2))
 31.1048 -                | NONE => some)
 31.1049 -           | NONE =>
 31.1050 -               (case rewritec (prover, thy, maxidx) ss t of
 31.1051 -                  SOME (thm2, skel2) => transitive2 thm2
 31.1052 -                    (botc skel2 ss (Thm.rhs_of thm2))
 31.1053 -                | NONE => NONE))
 31.1054 -
 31.1055 -    and try_botc ss t =
 31.1056 -          (case botc skel0 ss t of
 31.1057 -             SOME trec1 => trec1 | NONE => (Thm.reflexive t))
 31.1058 -
 31.1059 -    and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 =
 31.1060 -       (case term_of t0 of
 31.1061 -           Abs (a, T, _) =>
 31.1062 -             let
 31.1063 -                 val b = Name.bound (#1 bounds);
 31.1064 -                 val (v, t') = Thm.dest_abs (SOME b) t0;
 31.1065 -                 val b' = #1 (Term.dest_Free (Thm.term_of v));
 31.1066 -                 val _ =
 31.1067 -                   if b <> b' then
 31.1068 -                     warning ("Simplifier: renamed bound variable " ^
 31.1069 -                       quote b ^ " to " ^ quote b' ^ Position.str_of (Position.thread_data ()))
 31.1070 -                   else ();
 31.1071 -                 val ss' = add_bound ((b', T), a) ss;
 31.1072 -                 val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
 31.1073 -             in case botc skel' ss' t' of
 31.1074 -                  SOME thm => SOME (Thm.abstract_rule a v thm)
 31.1075 -                | NONE => NONE
 31.1076 -             end
 31.1077 -         | t $ _ => (case t of
 31.1078 -             Const ("==>", _) $ _  => impc t0 ss
 31.1079 -           | Abs _ =>
 31.1080 -               let val thm = Thm.beta_conversion false t0
 31.1081 -               in case subc skel0 ss (Thm.rhs_of thm) of
 31.1082 -                    NONE => SOME thm
 31.1083 -                  | SOME thm' => SOME (Thm.transitive thm thm')
 31.1084 -               end
 31.1085 -           | _  =>
 31.1086 -               let fun appc () =
 31.1087 -                     let
 31.1088 -                       val (tskel, uskel) = case skel of
 31.1089 -                           tskel $ uskel => (tskel, uskel)
 31.1090 -                         | _ => (skel0, skel0);
 31.1091 -                       val (ct, cu) = Thm.dest_comb t0
 31.1092 -                     in
 31.1093 -                     (case botc tskel ss ct of
 31.1094 -                        SOME thm1 =>
 31.1095 -                          (case botc uskel ss cu of
 31.1096 -                             SOME thm2 => SOME (Thm.combination thm1 thm2)
 31.1097 -                           | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu)))
 31.1098 -                      | NONE =>
 31.1099 -                          (case botc uskel ss cu of
 31.1100 -                             SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1)
 31.1101 -                           | NONE => NONE))
 31.1102 -                     end
 31.1103 -                   val (h, ts) = strip_comb t
 31.1104 -               in case cong_name h of
 31.1105 -                    SOME a =>
 31.1106 -                      (case AList.lookup (op =) (fst congs) a of
 31.1107 -                         NONE => appc ()
 31.1108 -                       | SOME cong =>
 31.1109 -  (*post processing: some partial applications h t1 ... tj, j <= length ts,
 31.1110 -    may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
 31.1111 -                          (let
 31.1112 -                             val thm = congc (prover ss) ss maxidx cong t0;
 31.1113 -                             val t = the_default t0 (Option.map Thm.rhs_of thm);
 31.1114 -                             val (cl, cr) = Thm.dest_comb t
 31.1115 -                             val dVar = Var(("", 0), dummyT)
 31.1116 -                             val skel =
 31.1117 -                               list_comb (h, replicate (length ts) dVar)
 31.1118 -                           in case botc skel ss cl of
 31.1119 -                                NONE => thm
 31.1120 -                              | SOME thm' => transitive3 thm
 31.1121 -                                  (Thm.combination thm' (Thm.reflexive cr))
 31.1122 -                           end handle Pattern.MATCH => appc ()))
 31.1123 -                  | _ => appc ()
 31.1124 -               end)
 31.1125 -         | _ => NONE)
 31.1126 -
 31.1127 -    and impc ct ss =
 31.1128 -      if mutsimp then mut_impc0 [] ct [] [] ss else nonmut_impc ct ss
 31.1129 -
 31.1130 -    and rules_of_prem ss prem =
 31.1131 -      if maxidx_of_term (term_of prem) <> ~1
 31.1132 -      then (trace_cterm true
 31.1133 -        (fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:")
 31.1134 -          ss prem; ([], NONE))
 31.1135 -      else
 31.1136 -        let val asm = Thm.assume prem
 31.1137 -        in (extract_safe_rrules (ss, asm), SOME asm) end
 31.1138 -
 31.1139 -    and add_rrules (rrss, asms) ss =
 31.1140 -      (fold o fold) insert_rrule rrss ss |> add_prems (map_filter I asms)
 31.1141 -
 31.1142 -    and disch r prem eq =
 31.1143 -      let
 31.1144 -        val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
 31.1145 -        val eq' = Thm.implies_elim (Thm.instantiate
 31.1146 -          ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
 31.1147 -          (Thm.implies_intr prem eq)
 31.1148 -      in if not r then eq' else
 31.1149 -        let
 31.1150 -          val (prem', concl) = Thm.dest_implies lhs;
 31.1151 -          val (prem'', _) = Thm.dest_implies rhs
 31.1152 -        in Thm.transitive (Thm.transitive
 31.1153 -          (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)])
 31.1154 -             Drule.swap_prems_eq) eq')
 31.1155 -          (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)])
 31.1156 -             Drule.swap_prems_eq)
 31.1157 -        end
 31.1158 -      end
 31.1159 -
 31.1160 -    and rebuild [] _ _ _ _ eq = eq
 31.1161 -      | rebuild (prem :: prems) concl (_ :: rrss) (_ :: asms) ss eq =
 31.1162 -          let
 31.1163 -            val ss' = add_rrules (rev rrss, rev asms) ss;
 31.1164 -            val concl' =
 31.1165 -              Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq));
 31.1166 -            val dprem = Option.map (disch false prem)
 31.1167 -          in
 31.1168 -            (case rewritec (prover, thy, maxidx) ss' concl' of
 31.1169 -              NONE => rebuild prems concl' rrss asms ss (dprem eq)
 31.1170 -            | SOME (eq', _) => transitive2 (fold (disch false)
 31.1171 -                  prems (the (transitive3 (dprem eq) eq')))
 31.1172 -                (mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ss))
 31.1173 -          end
 31.1174 -
 31.1175 -    and mut_impc0 prems concl rrss asms ss =
 31.1176 -      let
 31.1177 -        val prems' = strip_imp_prems concl;
 31.1178 -        val (rrss', asms') = split_list (map (rules_of_prem ss) prems')
 31.1179 -      in
 31.1180 -        mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss')
 31.1181 -          (asms @ asms') [] [] [] [] ss ~1 ~1
 31.1182 -      end
 31.1183 -
 31.1184 -    and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k =
 31.1185 -        transitive1 (fold (fn (eq1, prem) => fn eq2 => transitive1 eq1
 31.1186 -            (Option.map (disch false prem) eq2)) (eqns ~~ prems') NONE)
 31.1187 -          (if changed > 0 then
 31.1188 -             mut_impc (rev prems') concl (rev rrss') (rev asms')
 31.1189 -               [] [] [] [] ss ~1 changed
 31.1190 -           else rebuild prems' concl rrss' asms' ss
 31.1191 -             (botc skel0 (add_rrules (rev rrss', rev asms') ss) concl))
 31.1192 -
 31.1193 -      | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms)
 31.1194 -          prems' rrss' asms' eqns ss changed k =
 31.1195 -        case (if k = 0 then NONE else botc skel0 (add_rrules
 31.1196 -          (rev rrss' @ rrss, rev asms' @ asms) ss) prem) of
 31.1197 -            NONE => mut_impc prems concl rrss asms (prem :: prems')
 31.1198 -              (rrs :: rrss') (asm :: asms') (NONE :: eqns) ss changed
 31.1199 -              (if k = 0 then 0 else k - 1)
 31.1200 -          | SOME eqn =>
 31.1201 -            let
 31.1202 -              val prem' = Thm.rhs_of eqn;
 31.1203 -              val tprems = map term_of prems;
 31.1204 -              val i = 1 + fold Integer.max (map (fn p =>
 31.1205 -                find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1;
 31.1206 -              val (rrs', asm') = rules_of_prem ss prem'
 31.1207 -            in mut_impc prems concl rrss asms (prem' :: prems')
 31.1208 -              (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
 31.1209 -                (take i prems)
 31.1210 -                (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies
 31.1211 -                  (drop i prems, concl))))) :: eqns)
 31.1212 -                  ss (length prems') ~1
 31.1213 -            end
 31.1214 -
 31.1215 -     (*legacy code - only for backwards compatibility*)
 31.1216 -    and nonmut_impc ct ss =
 31.1217 -      let
 31.1218 -        val (prem, conc) = Thm.dest_implies ct;
 31.1219 -        val thm1 = if simprem then botc skel0 ss prem else NONE;
 31.1220 -        val prem1 = the_default prem (Option.map Thm.rhs_of thm1);
 31.1221 -        val ss1 =
 31.1222 -          if not useprem then ss
 31.1223 -          else add_rrules (apsnd single (apfst single (rules_of_prem ss prem1))) ss
 31.1224 -      in
 31.1225 -        (case botc skel0 ss1 conc of
 31.1226 -          NONE =>
 31.1227 -            (case thm1 of
 31.1228 -              NONE => NONE
 31.1229 -            | SOME thm1' => SOME (Drule.imp_cong_rule thm1' (Thm.reflexive conc)))
 31.1230 -        | SOME thm2 =>
 31.1231 -            let val thm2' = disch false prem1 thm2 in
 31.1232 -              (case thm1 of
 31.1233 -                NONE => SOME thm2'
 31.1234 -              | SOME thm1' =>
 31.1235 -                 SOME (Thm.transitive (Drule.imp_cong_rule thm1' (Thm.reflexive conc)) thm2'))
 31.1236 -            end)
 31.1237 -      end
 31.1238 -
 31.1239 - in try_botc end;
 31.1240 -
 31.1241 -
 31.1242 -(* Meta-rewriting: rewrites t to u and returns the theorem t==u *)
 31.1243 -
 31.1244 -(*
 31.1245 -  Parameters:
 31.1246 -    mode = (simplify A,
 31.1247 -            use A in simplifying B,
 31.1248 -            use prems of B (if B is again a meta-impl.) to simplify A)
 31.1249 -           when simplifying A ==> B
 31.1250 -    prover: how to solve premises in conditional rewrites and congruences
 31.1251 -*)
 31.1252 -
 31.1253 -val debug_bounds = Unsynchronized.ref false;
 31.1254 -
 31.1255 -fun check_bounds ss ct =
 31.1256 -  if ! debug_bounds then
 31.1257 -    let
 31.1258 -      val Simpset ({bounds = (_, bounds), ...}, _) = ss;
 31.1259 -      val bs = fold_aterms (fn Free (x, _) =>
 31.1260 -          if Name.is_bound x andalso not (AList.defined eq_bound bounds x)
 31.1261 -          then insert (op =) x else I
 31.1262 -        | _ => I) (term_of ct) [];
 31.1263 -    in
 31.1264 -      if null bs then ()
 31.1265 -      else print_term_global ss true ("Simplifier: term contains loose bounds: " ^ commas_quote bs)
 31.1266 -        (Thm.theory_of_cterm ct) (Thm.term_of ct)
 31.1267 -    end
 31.1268 -  else ();
 31.1269 -
 31.1270 -fun rewrite_cterm mode prover raw_ss raw_ct =
 31.1271 -  let
 31.1272 -    val thy = Thm.theory_of_cterm raw_ct;
 31.1273 -    val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
 31.1274 -    val {maxidx, ...} = Thm.rep_cterm ct;
 31.1275 -    val ss = inc_simp_depth (activate_context thy raw_ss);
 31.1276 -    val depth = simp_depth ss;
 31.1277 -    val _ =
 31.1278 -      if depth mod 20 = 0 then
 31.1279 -        if_visible ss warning ("Simplification depth " ^ string_of_int depth)
 31.1280 -      else ();
 31.1281 -    val _ = trace_cterm false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ss ct;
 31.1282 -    val _ = check_bounds ss ct;
 31.1283 -  in bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct end;
 31.1284 -
 31.1285 -val simple_prover =
 31.1286 -  SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss)));
 31.1287 -
 31.1288 -fun rewrite _ [] ct = Thm.reflexive ct
 31.1289 -  | rewrite full thms ct = rewrite_cterm (full, false, false) simple_prover
 31.1290 -      (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
 31.1291 -
 31.1292 -fun simplify full thms = Conv.fconv_rule (rewrite full thms);
 31.1293 -val rewrite_rule = simplify true;
 31.1294 -
 31.1295 -(*simple term rewriting -- no proof*)
 31.1296 -fun rewrite_term thy rules procs =
 31.1297 -  Pattern.rewrite_term thy (map decomp_simp' rules) procs;
 31.1298 -
 31.1299 -fun rewrite_thm mode prover ss = Conv.fconv_rule (rewrite_cterm mode prover ss);
 31.1300 -
 31.1301 -(*Rewrite the subgoals of a proof state (represented by a theorem)*)
 31.1302 -fun rewrite_goals_rule thms th =
 31.1303 -  Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
 31.1304 -    (global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
 31.1305 -
 31.1306 -(*Rewrite the subgoal of a proof state (represented by a theorem)*)
 31.1307 -fun rewrite_goal_rule mode prover ss i thm =
 31.1308 -  if 0 < i andalso i <= Thm.nprems_of thm
 31.1309 -  then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm
 31.1310 -  else raise THM ("rewrite_goal_rule", i, [thm]);
 31.1311 -
 31.1312 -
 31.1313 -(** meta-rewriting tactics **)
 31.1314 -
 31.1315 -(*Rewrite all subgoals*)
 31.1316 -fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
 31.1317 -fun rewtac def = rewrite_goals_tac [def];
 31.1318 -
 31.1319 -(*Rewrite one subgoal*)
 31.1320 -fun asm_rewrite_goal_tac mode prover_tac ss i thm =
 31.1321 -  if 0 < i andalso i <= Thm.nprems_of thm then
 31.1322 -    Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm)
 31.1323 -  else Seq.empty;
 31.1324 -
 31.1325 -fun rewrite_goal_tac rews =
 31.1326 -  let val ss = empty_ss addsimps rews in
 31.1327 -    fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
 31.1328 -      (global_context (Thm.theory_of_thm st) ss) i st
 31.1329 -  end;
 31.1330 -
 31.1331 -(*Prunes all redundant parameters from the proof state by rewriting.
 31.1332 -  DOES NOT rewrite main goal, where quantification over an unused bound
 31.1333 -    variable is sometimes done to avoid the need for cut_facts_tac.*)
 31.1334 -val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
 31.1335 -
 31.1336 -
 31.1337 -(* for folding definitions, handling critical pairs *)
 31.1338 -
 31.1339 -(*The depth of nesting in a term*)
 31.1340 -fun term_depth (Abs (_, _, t)) = 1 + term_depth t
 31.1341 -  | term_depth (f $ t) = 1 + Int.max (term_depth f, term_depth t)
 31.1342 -  | term_depth _ = 0;
 31.1343 -
 31.1344 -val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
 31.1345 -
 31.1346 -(*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
 31.1347 -  Returns longest lhs first to avoid folding its subexpressions.*)
 31.1348 -fun sort_lhs_depths defs =
 31.1349 -  let val keylist = AList.make (term_depth o lhs_of_thm) defs
 31.1350 -      val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
 31.1351 -  in map (AList.find (op =) keylist) keys end;
 31.1352 -
 31.1353 -val rev_defs = sort_lhs_depths o map Thm.symmetric;
 31.1354 -
 31.1355 -fun fold_rule defs = fold rewrite_rule (rev_defs defs);
 31.1356 -fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
 31.1357 -
 31.1358 -
 31.1359 -(* HHF normal form: !! before ==>, outermost !! generalized *)
 31.1360 -
 31.1361 -local
 31.1362 -
 31.1363 -fun gen_norm_hhf ss th =
 31.1364 -  (if Drule.is_norm_hhf (Thm.prop_of th) then th
 31.1365 -   else Conv.fconv_rule
 31.1366 -    (rewrite_cterm (true, false, false) (K (K NONE)) (global_context (Thm.theory_of_thm th) ss)) th)
 31.1367 -  |> Thm.adjust_maxidx_thm ~1
 31.1368 -  |> Drule.gen_all;
 31.1369 -
 31.1370 -val hhf_ss = empty_ss addsimps Drule.norm_hhf_eqs;
 31.1371 -
 31.1372 -in
 31.1373 -
 31.1374 -val norm_hhf = gen_norm_hhf hhf_ss;
 31.1375 -val norm_hhf_protect = gen_norm_hhf (hhf_ss addeqcongs [Drule.protect_cong]);
 31.1376 -
 31.1377 -end;
 31.1378 -
 31.1379 -end;
 31.1380 -
 31.1381 -structure Basic_Meta_Simplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
 31.1382 -open Basic_Meta_Simplifier;
    32.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    32.2 +++ b/src/Pure/raw_simplifier.ML	Fri Dec 17 17:08:56 2010 +0100
    32.3 @@ -0,0 +1,1379 @@
    32.4 +(*  Title:      Pure/raw_simplifier.ML
    32.5 +    Author:     Tobias Nipkow and Stefan Berghofer, TU Muenchen
    32.6 +
    32.7 +Higher-order Simplification.
    32.8 +*)
    32.9 +
   32.10 +infix 4
   32.11 +  addsimps delsimps addeqcongs deleqcongs addcongs delcongs addsimprocs delsimprocs
   32.12 +  setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler
   32.13 +  setloop' setloop addloop addloop' delloop setSSolver addSSolver setSolver addSolver;
   32.14 +
   32.15 +signature BASIC_RAW_SIMPLIFIER =
   32.16 +sig
   32.17 +  val simp_depth_limit: int Config.T
   32.18 +  val simp_trace_depth_limit: int Config.T
   32.19 +  val simp_debug: bool Config.T
   32.20 +  val simp_trace: bool Config.T
   32.21 +  type rrule
   32.22 +  val eq_rrule: rrule * rrule -> bool
   32.23 +  type simpset
   32.24 +  type proc
   32.25 +  type solver
   32.26 +  val mk_solver': string -> (simpset -> int -> tactic) -> solver
   32.27 +  val mk_solver: string -> (thm list -> int -> tactic) -> solver
   32.28 +  val empty_ss: simpset
   32.29 +  val merge_ss: simpset * simpset -> simpset
   32.30 +  val dest_ss: simpset ->
   32.31 +   {simps: (string * thm) list,
   32.32 +    procs: (string * cterm list) list,
   32.33 +    congs: (string * thm) list,
   32.34 +    weak_congs: string list,
   32.35 +    loopers: string list,
   32.36 +    unsafe_solvers: string list,
   32.37 +    safe_solvers: string list}
   32.38 +  type simproc
   32.39 +  val eq_simproc: simproc * simproc -> bool
   32.40 +  val morph_simproc: morphism -> simproc -> simproc
   32.41 +  val make_simproc: {name: string, lhss: cterm list,
   32.42 +    proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc
   32.43 +  val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc
   32.44 +  val prems_of_ss: simpset -> thm list
   32.45 +  val addsimps: simpset * thm list -> simpset
   32.46 +  val delsimps: simpset * thm list -> simpset
   32.47 +  val addeqcongs: simpset * thm list -> simpset
   32.48 +  val deleqcongs: simpset * thm list -> simpset
   32.49 +  val addcongs: simpset * thm list -> simpset
   32.50 +  val delcongs: simpset * thm list -> simpset
   32.51 +  val addsimprocs: simpset * simproc list -> simpset
   32.52 +  val delsimprocs: simpset * simproc list -> simpset
   32.53 +  val mksimps: simpset -> thm -> thm list
   32.54 +  val setmksimps: simpset * (simpset -> thm -> thm list) -> simpset
   32.55 +  val setmkcong: simpset * (simpset -> thm -> thm) -> simpset
   32.56 +  val setmksym: simpset * (simpset -> thm -> thm option) -> simpset
   32.57 +  val setmkeqTrue: simpset * (simpset -> thm -> thm option) -> simpset
   32.58 +  val settermless: simpset * (term * term -> bool) -> simpset
   32.59 +  val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
   32.60 +  val setloop': simpset * (simpset -> int -> tactic) -> simpset
   32.61 +  val setloop: simpset * (int -> tactic) -> simpset
   32.62 +  val addloop': simpset * (string * (simpset -> int -> tactic)) -> simpset
   32.63 +  val addloop: simpset * (string * (int -> tactic)) -> simpset
   32.64 +  val delloop: simpset * string -> simpset
   32.65 +  val setSSolver: simpset * solver -> simpset
   32.66 +  val addSSolver: simpset * solver -> simpset
   32.67 +  val setSolver: simpset * solver -> simpset
   32.68 +  val addSolver: simpset * solver -> simpset
   32.69 +
   32.70 +  val rewrite_rule: thm list -> thm -> thm
   32.71 +  val rewrite_goals_rule: thm list -> thm -> thm
   32.72 +  val rewrite_goals_tac: thm list -> tactic
   32.73 +  val rewrite_goal_tac: thm list -> int -> tactic
   32.74 +  val rewtac: thm -> tactic
   32.75 +  val prune_params_tac: tactic
   32.76 +  val fold_rule: thm list -> thm -> thm
   32.77 +  val fold_goals_tac: thm list -> tactic
   32.78 +  val norm_hhf: thm -> thm
   32.79 +  val norm_hhf_protect: thm -> thm
   32.80 +end;
   32.81 +
   32.82 +signature RAW_SIMPLIFIER =
   32.83 +sig
   32.84 +  include BASIC_RAW_SIMPLIFIER
   32.85 +  exception SIMPLIFIER of string * thm
   32.86 +  val internal_ss: simpset ->
   32.87 +   {rules: rrule Net.net,
   32.88 +    prems: thm list,
   32.89 +    bounds: int * ((string * typ) * string) list,
   32.90 +    depth: int * bool Unsynchronized.ref,
   32.91 +    context: Proof.context option} *
   32.92 +   {congs: (string * thm) list * string list,
   32.93 +    procs: proc Net.net,
   32.94 +    mk_rews:
   32.95 +     {mk: simpset -> thm -> thm list,
   32.96 +      mk_cong: simpset -> thm -> thm,
   32.97 +      mk_sym: simpset -> thm -> thm option,
   32.98 +      mk_eq_True: simpset -> thm -> thm option,
   32.99 +      reorient: theory -> term list -> term -> term -> bool},
  32.100 +    termless: term * term -> bool,
  32.101 +    subgoal_tac: simpset -> int -> tactic,
  32.102 +    loop_tacs: (string * (simpset -> int -> tactic)) list,
  32.103 +    solvers: solver list * solver list}
  32.104 +  val add_simp: thm -> simpset -> simpset
  32.105 +  val del_simp: thm -> simpset -> simpset
  32.106 +  val solver: simpset -> solver -> int -> tactic
  32.107 +  val simp_depth_limit_raw: Config.raw
  32.108 +  val clear_ss: simpset -> simpset
  32.109 +  val simproc_global_i: theory -> string -> term list
  32.110 +    -> (theory -> simpset -> term -> thm option) -> simproc
  32.111 +  val simproc_global: theory -> string -> string list
  32.112 +    -> (theory -> simpset -> term -> thm option) -> simproc
  32.113 +  val simp_trace_depth_limit_raw: Config.raw
  32.114 +  val simp_trace_depth_limit_default: int Unsynchronized.ref
  32.115 +  val simp_trace_default: bool Unsynchronized.ref
  32.116 +  val simp_trace_raw: Config.raw
  32.117 +  val simp_debug_raw: Config.raw
  32.118 +  val add_prems: thm list -> simpset -> simpset
  32.119 +  val inherit_context: simpset -> simpset -> simpset
  32.120 +  val the_context: simpset -> Proof.context
  32.121 +  val context: Proof.context -> simpset -> simpset
  32.122 +  val global_context: theory  -> simpset -> simpset
  32.123 +  val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
  32.124 +  val debug_bounds: bool Unsynchronized.ref
  32.125 +  val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
  32.126 +  val set_solvers: solver list -> simpset -> simpset
  32.127 +  val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> conv
  32.128 +  val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
  32.129 +  val rewrite_thm: bool * bool * bool ->
  32.130 +    (simpset -> thm -> thm option) -> simpset -> thm -> thm
  32.131 +  val rewrite_goal_rule: bool * bool * bool ->
  32.132 +    (simpset -> thm -> thm option) -> simpset -> int -> thm -> thm
  32.133 +  val asm_rewrite_goal_tac: bool * bool * bool ->
  32.134 +    (simpset -> tactic) -> simpset -> int -> tactic
  32.135 +  val rewrite: bool -> thm list -> conv
  32.136 +  val simplify: bool -> thm list -> thm -> thm
  32.137 +end;
  32.138 +
  32.139 +structure Raw_Simplifier: RAW_SIMPLIFIER =
  32.140 +struct
  32.141 +
  32.142 +(** datatype simpset **)
  32.143 +
  32.144 +(* rewrite rules *)
  32.145 +
  32.146 +type rrule =
  32.147 + {thm: thm,         (*the rewrite rule*)
  32.148 +  name: string,     (*name of theorem from which rewrite rule was extracted*)
  32.149 +  lhs: term,        (*the left-hand side*)
  32.150 +  elhs: cterm,      (*the etac-contracted lhs*)
  32.151 +  extra: bool,      (*extra variables outside of elhs*)
  32.152 +  fo: bool,         (*use first-order matching*)
  32.153 +  perm: bool};      (*the rewrite rule is permutative*)
  32.154 +
  32.155 +(*
  32.156 +Remarks:
  32.157 +  - elhs is used for matching,
  32.158 +    lhs only for preservation of bound variable names;
  32.159 +  - fo is set iff
  32.160 +    either elhs is first-order (no Var is applied),
  32.161 +      in which case fo-matching is complete,
  32.162 +    or elhs is not a pattern,
  32.163 +      in which case there is nothing better to do;
  32.164 +*)
  32.165 +
  32.166 +fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
  32.167 +  Thm.eq_thm_prop (thm1, thm2);
  32.168 +
  32.169 +
  32.170 +(* simplification sets, procedures, and solvers *)
  32.171 +
  32.172 +(*A simpset contains data required during conversion:
  32.173 +    rules: discrimination net of rewrite rules;
  32.174 +    prems: current premises;
  32.175 +    bounds: maximal index of bound variables already used
  32.176 +      (for generating new names when rewriting under lambda abstractions);
  32.177 +    depth: simp_depth and exceeded flag;
  32.178 +    congs: association list of congruence rules and
  32.179 +           a list of `weak' congruence constants.
  32.180 +           A congruence is `weak' if it avoids normalization of some argument.
  32.181 +    procs: discrimination net of simplification procedures
  32.182 +      (functions that prove rewrite rules on the fly);
  32.183 +    mk_rews:
  32.184 +      mk: turn simplification thms into rewrite rules;
  32.185 +      mk_cong: prepare congruence rules;
  32.186 +      mk_sym: turn == around;
  32.187 +      mk_eq_True: turn P into P == True;
  32.188 +    termless: relation for ordered rewriting;*)
  32.189 +
  32.190 +datatype simpset =
  32.191 +  Simpset of
  32.192 +   {rules: rrule Net.net,
  32.193 +    prems: thm list,
  32.194 +    bounds: int * ((string * typ) * string) list,
  32.195 +    depth: int * bool Unsynchronized.ref,
  32.196 +    context: Proof.context option} *
  32.197 +   {congs: (string * thm) list * string list,
  32.198 +    procs: proc Net.net,
  32.199 +    mk_rews:
  32.200 +     {mk: simpset -> thm -> thm list,
  32.201 +      mk_cong: simpset -> thm -> thm,
  32.202 +      mk_sym: simpset -> thm -> thm option,
  32.203 +      mk_eq_True: simpset -> thm -> thm option,
  32.204 +      reorient: theory -> term list -> term -> term -> bool},
  32.205 +    termless: term * term -> bool,
  32.206 +    subgoal_tac: simpset -> int -> tactic,
  32.207 +    loop_tacs: (string * (simpset -> int -> tactic)) list,
  32.208 +    solvers: solver list * solver list}
  32.209 +and proc =
  32.210 +  Proc of
  32.211 +   {name: string,
  32.212 +    lhs: cterm,
  32.213 +    proc: simpset -> cterm -> thm option,
  32.214 +    id: stamp * thm list}
  32.215 +and solver =
  32.216 +  Solver of
  32.217 +   {name: string,
  32.218 +    solver: simpset -> int -> tactic,
  32.219 +    id: stamp};
  32.220 +
  32.221 +
  32.222 +fun internal_ss (Simpset args) = args;
  32.223 +
  32.224 +fun make_ss1 (rules, prems, bounds, depth, context) =
  32.225 +  {rules = rules, prems = prems, bounds = bounds, depth = depth, context = context};
  32.226 +
  32.227 +fun map_ss1 f {rules, prems, bounds, depth, context} =
  32.228 +  make_ss1 (f (rules, prems, bounds, depth, context));
  32.229 +
  32.230 +fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =
  32.231 +  {congs = congs, procs = procs, mk_rews = mk_rews, termless = termless,
  32.232 +    subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers};
  32.233 +
  32.234 +fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers} =
  32.235 +  make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
  32.236 +
  32.237 +fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
  32.238 +
  32.239 +fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2);
  32.240 +fun map_simpset2 f (Simpset (r1, r2)) = Simpset (r1, map_ss2 f r2);
  32.241 +
  32.242 +fun prems_of_ss (Simpset ({prems, ...}, _)) = prems;
  32.243 +
  32.244 +fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) =
  32.245 +  s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
  32.246 +fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2);
  32.247 +
  32.248 +fun mk_solver' name solver = Solver {name = name, solver = solver, id = stamp ()};
  32.249 +fun mk_solver name solver = mk_solver' name (solver o prems_of_ss);
  32.250 +
  32.251 +fun solver_name (Solver {name, ...}) = name;
  32.252 +fun solver ss (Solver {solver = tac, ...}) = tac ss;
  32.253 +fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2);
  32.254 +
  32.255 +
  32.256 +(* simp depth *)
  32.257 +
  32.258 +val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100));
  32.259 +val simp_depth_limit = Config.int simp_depth_limit_raw;
  32.260 +
  32.261 +val simp_trace_depth_limit_default = Unsynchronized.ref 1;
  32.262 +val simp_trace_depth_limit_raw = Config.declare "simp_trace_depth_limit"
  32.263 +  (fn _ => Config.Int (! simp_trace_depth_limit_default));
  32.264 +val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw;
  32.265 +
  32.266 +fun simp_trace_depth_limit_of NONE = ! simp_trace_depth_limit_default
  32.267 +  | simp_trace_depth_limit_of (SOME ctxt) = Config.get ctxt simp_trace_depth_limit;
  32.268 +
  32.269 +fun trace_depth (Simpset ({depth = (depth, exceeded), context, ...}, _)) msg =
  32.270 +  if depth > simp_trace_depth_limit_of context then
  32.271 +    if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true)
  32.272 +  else
  32.273 +    (tracing (enclose "[" "]" (string_of_int depth) ^ msg); exceeded := false);
  32.274 +
  32.275 +val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
  32.276 +  (rules, prems, bounds,
  32.277 +    (depth + 1,
  32.278 +      if depth = simp_trace_depth_limit_of context then Unsynchronized.ref false else exceeded), context));
  32.279 +
  32.280 +fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
  32.281 +
  32.282 +
  32.283 +(* diagnostics *)
  32.284 +
  32.285 +exception SIMPLIFIER of string * thm;
  32.286 +
  32.287 +val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false));
  32.288 +val simp_debug = Config.bool simp_debug_raw;
  32.289 +
  32.290 +val simp_trace_default = Unsynchronized.ref false;
  32.291 +val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default));
  32.292 +val simp_trace = Config.bool simp_trace_raw;
  32.293 +
  32.294 +fun if_enabled (Simpset ({context, ...}, _)) flag f =
  32.295 +  (case context of
  32.296 +    SOME ctxt => if Config.get ctxt flag then f ctxt else ()
  32.297 +  | NONE => ())
  32.298 +
  32.299 +fun if_visible (Simpset ({context, ...}, _)) f x =
  32.300 +  (case context of
  32.301 +    SOME ctxt => if Context_Position.is_visible ctxt then f x else ()
  32.302 +  | NONE => ());
  32.303 +
  32.304 +local
  32.305 +
  32.306 +fun prnt ss warn a = if warn then warning a else trace_depth ss a;
  32.307 +
  32.308 +fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t =
  32.309 +  let
  32.310 +    val names = Term.declare_term_names t Name.context;
  32.311 +    val xs = rev (#1 (Name.variants (rev (map #2 bs)) names));
  32.312 +    fun subst (((b, T), _), x') = (Free (b, T), Syntax.mark_boundT (x', T));
  32.313 +  in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
  32.314 +
  32.315 +fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^
  32.316 +  Syntax.string_of_term ctxt
  32.317 +    (if Config.get ctxt simp_debug then t else show_bounds ss t));
  32.318 +
  32.319 +in
  32.320 +
  32.321 +fun print_term_global ss warn a thy t =
  32.322 +  print_term ss warn (K a) t (ProofContext.init_global thy);
  32.323 +
  32.324 +fun debug warn a ss = if_enabled ss simp_debug (fn _ => prnt ss warn (a ()));
  32.325 +fun trace warn a ss = if_enabled ss simp_trace (fn _ => prnt ss warn (a ()));
  32.326 +
  32.327 +fun debug_term warn a ss t = if_enabled ss simp_debug (print_term ss warn a t);
  32.328 +fun trace_term warn a ss t = if_enabled ss simp_trace (print_term ss warn a t);
  32.329 +
  32.330 +fun trace_cterm warn a ss ct =
  32.331 +  if_enabled ss simp_trace (print_term ss warn a (Thm.term_of ct));
  32.332 +
  32.333 +fun trace_thm a ss th =
  32.334 +  if_enabled ss simp_trace (print_term ss false a (Thm.full_prop_of th));
  32.335 +
  32.336 +fun trace_named_thm a ss (th, name) =
  32.337 +  if_enabled ss simp_trace (print_term ss false
  32.338 +    (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
  32.339 +    (Thm.full_prop_of th));
  32.340 +
  32.341 +fun warn_thm a ss th =
  32.342 +  print_term_global ss true a (Thm.theory_of_thm th) (Thm.full_prop_of th);
  32.343 +
  32.344 +fun cond_warn_thm a ss th = if_visible ss (fn () => warn_thm a ss th) ();
  32.345 +
  32.346 +end;
  32.347 +
  32.348 +
  32.349 +
  32.350 +(** simpset operations **)
  32.351 +
  32.352 +(* context *)
  32.353 +
  32.354 +fun eq_bound (x: string, (y, _)) = x = y;
  32.355 +
  32.356 +fun add_bound bound = map_simpset1 (fn (rules, prems, (count, bounds), depth, context) =>
  32.357 +  (rules, prems, (count + 1, bound :: bounds), depth, context));
  32.358 +
  32.359 +fun add_prems ths = map_simpset1 (fn (rules, prems, bounds, depth, context) =>
  32.360 +  (rules, ths @ prems, bounds, depth, context));
  32.361 +
  32.362 +fun inherit_context (Simpset ({bounds, depth, context, ...}, _)) =
  32.363 +  map_simpset1 (fn (rules, prems, _, _, _) => (rules, prems, bounds, depth, context));
  32.364 +
  32.365 +fun the_context (Simpset ({context = SOME ctxt, ...}, _)) = ctxt
  32.366 +  | the_context _ = raise Fail "Simplifier: no proof context in simpset";
  32.367 +
  32.368 +fun context ctxt =
  32.369 +  map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt));
  32.370 +
  32.371 +val global_context = context o ProofContext.init_global;
  32.372 +
  32.373 +fun activate_context thy ss =
  32.374 +  let
  32.375 +    val ctxt = the_context ss;
  32.376 +    val ctxt' = ctxt
  32.377 +      |> Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt))
  32.378 +      |> Context_Position.set_visible false;
  32.379 +  in context ctxt' ss end;
  32.380 +
  32.381 +fun with_context ctxt f ss = inherit_context ss (f (context ctxt ss));
  32.382 +
  32.383 +
  32.384 +(* maintain simp rules *)
  32.385 +
  32.386 +(* FIXME: it seems that the conditions on extra variables are too liberal if
  32.387 +prems are nonempty: does solving the prems really guarantee instantiation of
  32.388 +all its Vars? Better: a dynamic check each time a rule is applied.
  32.389 +*)
  32.390 +fun rewrite_rule_extra_vars prems elhs erhs =
  32.391 +  let
  32.392 +    val elhss = elhs :: prems;
  32.393 +    val tvars = fold Term.add_tvars elhss [];
  32.394 +    val vars = fold Term.add_vars elhss [];
  32.395 +  in
  32.396 +    erhs |> Term.exists_type (Term.exists_subtype
  32.397 +      (fn TVar v => not (member (op =) tvars v) | _ => false)) orelse
  32.398 +    erhs |> Term.exists_subterm
  32.399 +      (fn Var v => not (member (op =) vars v) | _ => false)
  32.400 +  end;
  32.401 +
  32.402 +fun rrule_extra_vars elhs thm =
  32.403 +  rewrite_rule_extra_vars [] (term_of elhs) (Thm.full_prop_of thm);
  32.404 +
  32.405 +fun mk_rrule2 {thm, name, lhs, elhs, perm} =
  32.406 +  let
  32.407 +    val t = term_of elhs;
  32.408 +    val fo = Pattern.first_order t orelse not (Pattern.pattern t);
  32.409 +    val extra = rrule_extra_vars elhs thm;
  32.410 +  in {thm = thm, name = name, lhs = lhs, elhs = elhs, extra = extra, fo = fo, perm = perm} end;
  32.411 +
  32.412 +fun del_rrule (rrule as {thm, elhs, ...}) ss =
  32.413 +  ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) =>
  32.414 +    (Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, bounds, depth, context))
  32.415 +  handle Net.DELETE => (cond_warn_thm "Rewrite rule not in simpset:" ss thm; ss);
  32.416 +
  32.417 +fun insert_rrule (rrule as {thm, name, ...}) ss =
  32.418 + (trace_named_thm (fn () => "Adding rewrite rule") ss (thm, name);
  32.419 +  ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) =>
  32.420 +    let
  32.421 +      val rrule2 as {elhs, ...} = mk_rrule2 rrule;
  32.422 +      val rules' = Net.insert_term eq_rrule (term_of elhs, rrule2) rules;
  32.423 +    in (rules', prems, bounds, depth, context) end)
  32.424 +  handle Net.INSERT => (cond_warn_thm "Ignoring duplicate rewrite rule:" ss thm; ss));
  32.425 +
  32.426 +fun vperm (Var _, Var _) = true
  32.427 +  | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
  32.428 +  | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
  32.429 +  | vperm (t, u) = (t = u);
  32.430 +
  32.431 +fun var_perm (t, u) =
  32.432 +  vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
  32.433 +
  32.434 +(*simple test for looping rewrite rules and stupid orientations*)
  32.435 +fun default_reorient thy prems lhs rhs =
  32.436 +  rewrite_rule_extra_vars prems lhs rhs
  32.437 +    orelse
  32.438 +  is_Var (head_of lhs)
  32.439 +    orelse
  32.440 +(* turns t = x around, which causes a headache if x is a local variable -
  32.441 +   usually it is very useful :-(
  32.442 +  is_Free rhs andalso not(is_Free lhs) andalso not(Logic.occs(rhs,lhs))
  32.443 +  andalso not(exists_subterm is_Var lhs)
  32.444 +    orelse
  32.445 +*)
  32.446 +  exists (fn t => Logic.occs (lhs, t)) (rhs :: prems)
  32.447 +    orelse
  32.448 +  null prems andalso Pattern.matches thy (lhs, rhs)
  32.449 +    (*the condition "null prems" is necessary because conditional rewrites
  32.450 +      with extra variables in the conditions may terminate although
  32.451 +      the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*)
  32.452 +    orelse
  32.453 +  is_Const lhs andalso not (is_Const rhs);
  32.454 +
  32.455 +fun decomp_simp thm =
  32.456 +  let
  32.457 +    val thy = Thm.theory_of_thm thm;
  32.458 +    val prop = Thm.prop_of thm;
  32.459 +    val prems = Logic.strip_imp_prems prop;
  32.460 +    val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
  32.461 +    val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
  32.462 +      raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
  32.463 +    val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
  32.464 +    val elhs = if term_of elhs aconv term_of lhs then lhs else elhs;  (*share identical copies*)
  32.465 +    val erhs = Envir.eta_contract (term_of rhs);
  32.466 +    val perm =
  32.467 +      var_perm (term_of elhs, erhs) andalso
  32.468 +      not (term_of elhs aconv erhs) andalso
  32.469 +      not (is_Var (term_of elhs));
  32.470 +  in (thy, prems, term_of lhs, elhs, term_of rhs, perm) end;
  32.471 +
  32.472 +fun decomp_simp' thm =
  32.473 +  let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
  32.474 +    if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
  32.475 +    else (lhs, rhs)
  32.476 +  end;
  32.477 +
  32.478 +fun mk_eq_True (ss as Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
  32.479 +  (case mk_eq_True ss thm of
  32.480 +    NONE => []
  32.481 +  | SOME eq_True =>
  32.482 +      let
  32.483 +        val (_, _, lhs, elhs, _, _) = decomp_simp eq_True;
  32.484 +      in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end);
  32.485 +
  32.486 +(*create the rewrite rule and possibly also the eq_True variant,
  32.487 +  in case there are extra vars on the rhs*)
  32.488 +fun rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm2) =
  32.489 +  let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in
  32.490 +    if rewrite_rule_extra_vars [] lhs rhs then
  32.491 +      mk_eq_True ss (thm2, name) @ [rrule]
  32.492 +    else [rrule]
  32.493 +  end;
  32.494 +
  32.495 +fun mk_rrule ss (thm, name) =
  32.496 +  let val (_, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
  32.497 +    if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
  32.498 +    else
  32.499 +      (*weak test for loops*)
  32.500 +      if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (term_of elhs)
  32.501 +      then mk_eq_True ss (thm, name)
  32.502 +      else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
  32.503 +  end;
  32.504 +
  32.505 +fun orient_rrule ss (thm, name) =
  32.506 +  let
  32.507 +    val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm;
  32.508 +    val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = ss;
  32.509 +  in
  32.510 +    if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
  32.511 +    else if reorient thy prems lhs rhs then
  32.512 +      if reorient thy prems rhs lhs
  32.513 +      then mk_eq_True ss (thm, name)
  32.514 +      else
  32.515 +        (case mk_sym ss thm of
  32.516 +          NONE => []
  32.517 +        | SOME thm' =>
  32.518 +            let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm'
  32.519 +            in rrule_eq_True (thm', name, lhs', elhs', rhs', ss, thm) end)
  32.520 +    else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
  32.521 +  end;
  32.522 +
  32.523 +fun extract_rews (ss as Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
  32.524 +  maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ss thm)) thms;
  32.525 +
  32.526 +fun extract_safe_rrules (ss, thm) =
  32.527 +  maps (orient_rrule ss) (extract_rews (ss, [thm]));
  32.528 +
  32.529 +
  32.530 +(* add/del rules explicitly *)
  32.531 +
  32.532 +fun comb_simps comb mk_rrule (ss, thms) =
  32.533 +  let
  32.534 +    val rews = extract_rews (ss, thms);
  32.535 +  in fold (fold comb o mk_rrule) rews ss end;
  32.536 +
  32.537 +fun ss addsimps thms =
  32.538 +  comb_simps insert_rrule (mk_rrule ss) (ss, thms);
  32.539 +
  32.540 +fun ss delsimps thms =
  32.541 +  comb_simps del_rrule (map mk_rrule2 o mk_rrule ss) (ss, thms);
  32.542 +
  32.543 +fun add_simp thm ss = ss addsimps [thm];
  32.544 +fun del_simp thm ss = ss delsimps [thm];
  32.545 +
  32.546 +
  32.547 +(* congs *)
  32.548 +
  32.549 +fun cong_name (Const (a, _)) = SOME a
  32.550 +  | cong_name (Free (a, _)) = SOME ("Free: " ^ a)
  32.551 +  | cong_name _ = NONE;
  32.552 +
  32.553 +local
  32.554 +
  32.555 +fun is_full_cong_prems [] [] = true
  32.556 +  | is_full_cong_prems [] _ = false
  32.557 +  | is_full_cong_prems (p :: prems) varpairs =
  32.558 +      (case Logic.strip_assums_concl p of
  32.559 +        Const ("==", _) $ lhs $ rhs =>
  32.560 +          let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in
  32.561 +            is_Var x andalso forall is_Bound xs andalso
  32.562 +            not (has_duplicates (op =) xs) andalso xs = ys andalso
  32.563 +            member (op =) varpairs (x, y) andalso
  32.564 +            is_full_cong_prems prems (remove (op =) (x, y) varpairs)
  32.565 +          end
  32.566 +      | _ => false);
  32.567 +
  32.568 +fun is_full_cong thm =
  32.569 +  let
  32.570 +    val prems = prems_of thm and concl = concl_of thm;
  32.571 +    val (lhs, rhs) = Logic.dest_equals concl;
  32.572 +    val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs;
  32.573 +  in
  32.574 +    f = g andalso not (has_duplicates (op =) (xs @ ys)) andalso length xs = length ys andalso
  32.575 +    is_full_cong_prems prems (xs ~~ ys)
  32.576 +  end;
  32.577 +
  32.578 +fun add_cong (ss, thm) = ss |>
  32.579 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  32.580 +    let
  32.581 +      val (lhs, _) = Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
  32.582 +        handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
  32.583 +    (*val lhs = Envir.eta_contract lhs;*)
  32.584 +      val a = the (cong_name (head_of (term_of lhs))) handle Option.Option =>
  32.585 +        raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
  32.586 +      val (xs, weak) = congs;
  32.587 +      val _ =
  32.588 +        if AList.defined (op =) xs a
  32.589 +        then if_visible ss warning ("Overwriting congruence rule for " ^ quote a)
  32.590 +        else ();
  32.591 +      val xs' = AList.update (op =) (a, thm) xs;
  32.592 +      val weak' = if is_full_cong thm then weak else a :: weak;
  32.593 +    in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
  32.594 +
  32.595 +fun del_cong (ss, thm) = ss |>
  32.596 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  32.597 +    let
  32.598 +      val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
  32.599 +        raise SIMPLIFIER ("Congruence not a meta-equality", thm);
  32.600 +    (*val lhs = Envir.eta_contract lhs;*)
  32.601 +      val a = the (cong_name (head_of lhs)) handle Option.Option =>
  32.602 +        raise SIMPLIFIER ("Congruence must start with a constant", thm);
  32.603 +      val (xs, _) = congs;
  32.604 +      val xs' = filter_out (fn (x : string, _) => x = a) xs;
  32.605 +      val weak' = xs' |> map_filter (fn (a, thm) =>
  32.606 +        if is_full_cong thm then NONE else SOME a);
  32.607 +    in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
  32.608 +
  32.609 +fun mk_cong (ss as Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f ss;
  32.610 +
  32.611 +in
  32.612 +
  32.613 +val (op addeqcongs) = Library.foldl add_cong;
  32.614 +val (op deleqcongs) = Library.foldl del_cong;
  32.615 +
  32.616 +fun ss addcongs congs = ss addeqcongs map (mk_cong ss) congs;
  32.617 +fun ss delcongs congs = ss deleqcongs map (mk_cong ss) congs;
  32.618 +
  32.619 +end;
  32.620 +
  32.621 +
  32.622 +(* simprocs *)
  32.623 +
  32.624 +datatype simproc =
  32.625 +  Simproc of
  32.626 +    {name: string,
  32.627 +     lhss: cterm list,
  32.628 +     proc: morphism -> simpset -> cterm -> thm option,
  32.629 +     id: stamp * thm list};
  32.630 +
  32.631 +fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2);
  32.632 +
  32.633 +fun morph_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
  32.634 +  Simproc
  32.635 +   {name = name,
  32.636 +    lhss = map (Morphism.cterm phi) lhss,
  32.637 +    proc = Morphism.transform phi proc,
  32.638 +    id = (s, Morphism.fact phi ths)};
  32.639 +
  32.640 +fun make_simproc {name, lhss, proc, identifier} =
  32.641 +  Simproc {name = name, lhss = lhss, proc = proc, id = (stamp (), identifier)};
  32.642 +
  32.643 +fun mk_simproc name lhss proc =
  32.644 +  make_simproc {name = name, lhss = lhss, proc = fn _ => fn ss => fn ct =>
  32.645 +    proc (ProofContext.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []};
  32.646 +
  32.647 +(* FIXME avoid global thy and Logic.varify_global *)
  32.648 +fun simproc_global_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global);
  32.649 +fun simproc_global thy name = simproc_global_i thy name o map (Syntax.read_term_global thy);
  32.650 +
  32.651 +
  32.652 +local
  32.653 +
  32.654 +fun add_proc (proc as Proc {name, lhs, ...}) ss =
  32.655 + (trace_cterm false (fn () => "Adding simplification procedure " ^ quote name ^ " for") ss lhs;
  32.656 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  32.657 +    (congs, Net.insert_term eq_proc (term_of lhs, proc) procs,
  32.658 +      mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
  32.659 +  handle Net.INSERT =>
  32.660 +    (if_visible ss warning ("Ignoring duplicate simplification procedure " ^ quote name); ss));
  32.661 +
  32.662 +fun del_proc (proc as Proc {name, lhs, ...}) ss =
  32.663 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  32.664 +    (congs, Net.delete_term eq_proc (term_of lhs, proc) procs,
  32.665 +      mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
  32.666 +  handle Net.DELETE =>
  32.667 +    (if_visible ss warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ss);
  32.668 +
  32.669 +fun prep_procs (Simproc {name, lhss, proc, id}) =
  32.670 +  lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id});
  32.671 +
  32.672 +in
  32.673 +
  32.674 +fun ss addsimprocs ps = fold (fold add_proc o prep_procs) ps ss;
  32.675 +fun ss delsimprocs ps = fold (fold del_proc o prep_procs) ps ss;
  32.676 +
  32.677 +end;
  32.678 +
  32.679 +
  32.680 +(* mk_rews *)
  32.681 +
  32.682 +local
  32.683 +
  32.684 +fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True, reorient},
  32.685 +      termless, subgoal_tac, loop_tacs, solvers) =>
  32.686 +  let
  32.687 +    val (mk', mk_cong', mk_sym', mk_eq_True', reorient') =
  32.688 +      f (mk, mk_cong, mk_sym, mk_eq_True, reorient);
  32.689 +    val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True',
  32.690 +      reorient = reorient'};
  32.691 +  in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end);
  32.692 +
  32.693 +in
  32.694 +
  32.695 +fun mksimps (ss as Simpset (_, {mk_rews = {mk, ...}, ...})) = mk ss;
  32.696 +
  32.697 +fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
  32.698 +  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  32.699 +
  32.700 +fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) =>
  32.701 +  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  32.702 +
  32.703 +fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) =>
  32.704 +  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  32.705 +
  32.706 +fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) =>
  32.707 +  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  32.708 +
  32.709 +fun set_reorient reorient = map_mk_rews (fn (mk, mk_cong, mk_sym, mk_eq_True, _) =>
  32.710 +  (mk, mk_cong, mk_sym, mk_eq_True, reorient));
  32.711 +
  32.712 +end;
  32.713 +
  32.714 +
  32.715 +(* termless *)
  32.716 +
  32.717 +fun ss settermless termless = ss |>
  32.718 +  map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) =>
  32.719 +   (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
  32.720 +
  32.721 +
  32.722 +(* tactics *)
  32.723 +
  32.724 +fun ss setsubgoaler subgoal_tac = ss |>
  32.725 +  map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) =>
  32.726 +   (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
  32.727 +
  32.728 +fun ss setloop' tac = ss |>
  32.729 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) =>
  32.730 +   (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers));
  32.731 +
  32.732 +fun ss setloop tac = ss setloop' (K tac);
  32.733 +
  32.734 +fun ss addloop' (name, tac) = ss |>
  32.735 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  32.736 +    (congs, procs, mk_rews, termless, subgoal_tac,
  32.737 +     (if AList.defined (op =) loop_tacs name
  32.738 +      then if_visible ss warning ("Overwriting looper " ^ quote name)
  32.739 +      else (); AList.update (op =) (name, tac) loop_tacs), solvers));
  32.740 +
  32.741 +fun ss addloop (name, tac) = ss addloop' (name, K tac);
  32.742 +
  32.743 +fun ss delloop name = ss |>
  32.744 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  32.745 +    (congs, procs, mk_rews, termless, subgoal_tac,
  32.746 +     (if AList.defined (op =) loop_tacs name then ()
  32.747 +      else if_visible ss warning ("No such looper in simpset: " ^ quote name);
  32.748 +      AList.delete (op =) name loop_tacs), solvers));
  32.749 +
  32.750 +fun ss setSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  32.751 +  subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
  32.752 +    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));
  32.753 +
  32.754 +fun ss addSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  32.755 +  subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
  32.756 +    subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers)));
  32.757 +
  32.758 +fun ss setSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  32.759 +  subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless,
  32.760 +    subgoal_tac, loop_tacs, ([solver], solvers)));
  32.761 +
  32.762 +fun ss addSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  32.763 +  subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
  32.764 +    subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers)));
  32.765 +
  32.766 +fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless,
  32.767 +  subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless,
  32.768 +  subgoal_tac, loop_tacs, (solvers, solvers)));
  32.769 +
  32.770 +
  32.771 +(* empty *)
  32.772 +
  32.773 +fun init_ss mk_rews termless subgoal_tac solvers =
  32.774 +  make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false), NONE),
  32.775 +    (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
  32.776 +
  32.777 +fun clear_ss (ss as Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) =
  32.778 +  init_ss mk_rews termless subgoal_tac solvers
  32.779 +  |> inherit_context ss;
  32.780 +
  32.781 +val empty_ss =
  32.782 +  init_ss
  32.783 +    {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
  32.784 +      mk_cong = K I,
  32.785 +      mk_sym = K (SOME o Drule.symmetric_fun),
  32.786 +      mk_eq_True = K (K NONE),
  32.787 +      reorient = default_reorient}
  32.788 +    Term_Ord.termless (K (K no_tac)) ([], []);
  32.789 +
  32.790 +
  32.791 +(* merge *)  (*NOTE: ignores some fields of 2nd simpset*)
  32.792 +
  32.793 +fun merge_ss (ss1, ss2) =
  32.794 +  if pointer_eq (ss1, ss2) then ss1
  32.795 +  else
  32.796 +    let
  32.797 +      val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1, context = _},
  32.798 +       {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac,
  32.799 +        loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
  32.800 +      val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _},
  32.801 +       {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
  32.802 +        loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
  32.803 +
  32.804 +      val rules' = Net.merge eq_rrule (rules1, rules2);
  32.805 +      val prems' = Thm.merge_thms (prems1, prems2);
  32.806 +      val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
  32.807 +      val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
  32.808 +      val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2);
  32.809 +      val weak' = merge (op =) (weak1, weak2);
  32.810 +      val procs' = Net.merge eq_proc (procs1, procs2);
  32.811 +      val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
  32.812 +      val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
  32.813 +      val solvers' = merge eq_solver (solvers1, solvers2);
  32.814 +    in
  32.815 +      make_simpset ((rules', prems', bounds', depth', NONE), ((congs', weak'), procs',
  32.816 +        mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
  32.817 +    end;
  32.818 +
  32.819 +
  32.820 +(* dest_ss *)
  32.821 +
  32.822 +fun dest_ss (Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...})) =
  32.823 + {simps = Net.entries rules
  32.824 +    |> map (fn {name, thm, ...} => (name, thm)),
  32.825 +  procs = Net.entries procs
  32.826 +    |> map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
  32.827 +    |> partition_eq (eq_snd eq_procid)
  32.828 +    |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)),
  32.829 +  congs = #1 congs,
  32.830 +  weak_congs = #2 congs,
  32.831 +  loopers = map fst loop_tacs,
  32.832 +  unsafe_solvers = map solver_name (#1 solvers),
  32.833 +  safe_solvers = map solver_name (#2 solvers)};
  32.834 +
  32.835 +
  32.836 +
  32.837 +(** rewriting **)
  32.838 +
  32.839 +(*
  32.840 +  Uses conversions, see:
  32.841 +    L C Paulson, A higher-order implementation of rewriting,
  32.842 +    Science of Computer Programming 3 (1983), pages 119-149.
  32.843 +*)
  32.844 +
  32.845 +fun check_conv msg ss thm thm' =
  32.846 +  let
  32.847 +    val thm'' = Thm.transitive thm thm' handle THM _ =>
  32.848 +     Thm.transitive thm (Thm.transitive
  32.849 +       (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
  32.850 +  in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
  32.851 +  handle THM _ =>
  32.852 +    let
  32.853 +      val _ $ _ $ prop0 = Thm.prop_of thm;
  32.854 +    in
  32.855 +      trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';
  32.856 +      trace_term false (fn () => "Should have proved:") ss prop0;
  32.857 +      NONE
  32.858 +    end;
  32.859 +
  32.860 +
  32.861 +(* mk_procrule *)
  32.862 +
  32.863 +fun mk_procrule ss thm =
  32.864 +  let val (_, prems, lhs, elhs, rhs, _) = decomp_simp thm in
  32.865 +    if rewrite_rule_extra_vars prems lhs rhs
  32.866 +    then (cond_warn_thm "Extra vars on rhs:" ss thm; [])
  32.867 +    else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}]
  32.868 +  end;
  32.869 +
  32.870 +
  32.871 +(* rewritec: conversion to apply the meta simpset to a term *)
  32.872 +
  32.873 +(*Since the rewriting strategy is bottom-up, we avoid re-normalizing already
  32.874 +  normalized terms by carrying around the rhs of the rewrite rule just
  32.875 +  applied. This is called the `skeleton'. It is decomposed in parallel
  32.876 +  with the term. Once a Var is encountered, the corresponding term is
  32.877 +  already in normal form.
  32.878 +  skel0 is a dummy skeleton that is to enforce complete normalization.*)
  32.879 +
  32.880 +val skel0 = Bound 0;
  32.881 +
  32.882 +(*Use rhs as skeleton only if the lhs does not contain unnormalized bits.
  32.883 +  The latter may happen iff there are weak congruence rules for constants
  32.884 +  in the lhs.*)
  32.885 +
  32.886 +fun uncond_skel ((_, weak), (lhs, rhs)) =
  32.887 +  if null weak then rhs  (*optimization*)
  32.888 +  else if exists_Const (member (op =) weak o #1) lhs then skel0
  32.889 +  else rhs;
  32.890 +
  32.891 +(*Behaves like unconditional rule if rhs does not contain vars not in the lhs.
  32.892 +  Otherwise those vars may become instantiated with unnormalized terms
  32.893 +  while the premises are solved.*)
  32.894 +
  32.895 +fun cond_skel (args as (_, (lhs, rhs))) =
  32.896 +  if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args
  32.897 +  else skel0;
  32.898 +
  32.899 +(*
  32.900 +  Rewriting -- we try in order:
  32.901 +    (1) beta reduction
  32.902 +    (2) unconditional rewrite rules
  32.903 +    (3) conditional rewrite rules
  32.904 +    (4) simplification procedures
  32.905 +
  32.906 +  IMPORTANT: rewrite rules must not introduce new Vars or TVars!
  32.907 +*)
  32.908 +
  32.909 +fun rewritec (prover, thyt, maxt) ss t =
  32.910 +  let
  32.911 +    val ctxt = the_context ss;
  32.912 +    val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss;
  32.913 +    val eta_thm = Thm.eta_conversion t;
  32.914 +    val eta_t' = Thm.rhs_of eta_thm;
  32.915 +    val eta_t = term_of eta_t';
  32.916 +    fun rew {thm, name, lhs, elhs, extra, fo, perm} =
  32.917 +      let
  32.918 +        val prop = Thm.prop_of thm;
  32.919 +        val (rthm, elhs') =
  32.920 +          if maxt = ~1 orelse not extra then (thm, elhs)
  32.921 +          else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs);
  32.922 +        val insts =
  32.923 +          if fo then Thm.first_order_match (elhs', eta_t')
  32.924 +          else Thm.match (elhs', eta_t');
  32.925 +        val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
  32.926 +        val prop' = Thm.prop_of thm';
  32.927 +        val unconditional = (Logic.count_prems prop' = 0);
  32.928 +        val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
  32.929 +      in
  32.930 +        if perm andalso not (termless (rhs', lhs'))
  32.931 +        then (trace_named_thm (fn () => "Cannot apply permutative rewrite rule") ss (thm, name);
  32.932 +              trace_thm (fn () => "Term does not become smaller:") ss thm'; NONE)
  32.933 +        else (trace_named_thm (fn () => "Applying instance of rewrite rule") ss (thm, name);
  32.934 +           if unconditional
  32.935 +           then
  32.936 +             (trace_thm (fn () => "Rewriting:") ss thm';
  32.937 +              let
  32.938 +                val lr = Logic.dest_equals prop;
  32.939 +                val SOME thm'' = check_conv false ss eta_thm thm';
  32.940 +              in SOME (thm'', uncond_skel (congs, lr)) end)
  32.941 +           else
  32.942 +             (trace_thm (fn () => "Trying to rewrite:") ss thm';
  32.943 +              if simp_depth ss > Config.get ctxt simp_depth_limit
  32.944 +              then
  32.945 +                let
  32.946 +                  val s = "simp_depth_limit exceeded - giving up";
  32.947 +                  val _ = trace false (fn () => s) ss;
  32.948 +                  val _ = if_visible ss warning s;
  32.949 +                in NONE end
  32.950 +              else
  32.951 +              case prover ss thm' of
  32.952 +                NONE => (trace_thm (fn () => "FAILED") ss thm'; NONE)
  32.953 +              | SOME thm2 =>
  32.954 +                  (case check_conv true ss eta_thm thm2 of
  32.955 +                     NONE => NONE |
  32.956 +                     SOME thm2' =>
  32.957 +                       let val concl = Logic.strip_imp_concl prop
  32.958 +                           val lr = Logic.dest_equals concl
  32.959 +                       in SOME (thm2', cond_skel (congs, lr)) end)))
  32.960 +      end
  32.961 +
  32.962 +    fun rews [] = NONE
  32.963 +      | rews (rrule :: rrules) =
  32.964 +          let val opt = rew rrule handle Pattern.MATCH => NONE
  32.965 +          in case opt of NONE => rews rrules | some => some end;
  32.966 +
  32.967 +    fun sort_rrules rrs =
  32.968 +      let
  32.969 +        fun is_simple ({thm, ...}: rrule) =
  32.970 +          (case Thm.prop_of thm of
  32.971 +            Const ("==", _) $ _ $ _ => true
  32.972 +          | _ => false);
  32.973 +        fun sort [] (re1, re2) = re1 @ re2
  32.974 +          | sort (rr :: rrs) (re1, re2) =
  32.975 +              if is_simple rr
  32.976 +              then sort rrs (rr :: re1, re2)
  32.977 +              else sort rrs (re1, rr :: re2);
  32.978 +      in sort rrs ([], []) end;
  32.979 +
  32.980 +    fun proc_rews [] = NONE
  32.981 +      | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
  32.982 +          if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then
  32.983 +            (debug_term false (fn () => "Trying procedure " ^ quote name ^ " on:") ss eta_t;
  32.984 +             case proc ss eta_t' of
  32.985 +               NONE => (debug false (fn () => "FAILED") ss; proc_rews ps)
  32.986 +             | SOME raw_thm =>
  32.987 +                 (trace_thm (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:")
  32.988 +                   ss raw_thm;
  32.989 +                  (case rews (mk_procrule ss raw_thm) of
  32.990 +                    NONE => (trace_cterm true (fn () => "IGNORED result of simproc " ^ quote name ^
  32.991 +                      " -- does not match") ss t; proc_rews ps)
  32.992 +                  | some => some)))
  32.993 +          else proc_rews ps;
  32.994 +  in
  32.995 +    (case eta_t of
  32.996 +      Abs _ $ _ => SOME (Thm.transitive eta_thm (Thm.beta_conversion false eta_t'), skel0)
  32.997 +    | _ =>
  32.998 +      (case rews (sort_rrules (Net.match_term rules eta_t)) of
  32.999 +        NONE => proc_rews (Net.match_term procs eta_t)
 32.1000 +      | some => some))
 32.1001 +  end;
 32.1002 +
 32.1003 +
 32.1004 +(* conversion to apply a congruence rule to a term *)
 32.1005 +
 32.1006 +fun congc prover ss maxt cong t =
 32.1007 +  let val rthm = Thm.incr_indexes (maxt + 1) cong;
 32.1008 +      val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
 32.1009 +      val insts = Thm.match (rlhs, t)
 32.1010 +      (* Thm.match can raise Pattern.MATCH;
 32.1011 +         is handled when congc is called *)
 32.1012 +      val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
 32.1013 +      val _ = trace_thm (fn () => "Applying congruence rule:") ss thm';
 32.1014 +      fun err (msg, thm) = (trace_thm (fn () => msg) ss thm; NONE)
 32.1015 +  in
 32.1016 +    (case prover thm' of
 32.1017 +      NONE => err ("Congruence proof failed.  Could not prove", thm')
 32.1018 +    | SOME thm2 =>
 32.1019 +        (case check_conv true ss (Drule.beta_eta_conversion t) thm2 of
 32.1020 +          NONE => err ("Congruence proof failed.  Should not have proved", thm2)
 32.1021 +        | SOME thm2' =>
 32.1022 +            if op aconv (pairself term_of (Thm.dest_equals (cprop_of thm2')))
 32.1023 +            then NONE else SOME thm2'))
 32.1024 +  end;
 32.1025 +
 32.1026 +val (cA, (cB, cC)) =
 32.1027 +  apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong)));
 32.1028 +
 32.1029 +fun transitive1 NONE NONE = NONE
 32.1030 +  | transitive1 (SOME thm1) NONE = SOME thm1
 32.1031 +  | transitive1 NONE (SOME thm2) = SOME thm2
 32.1032 +  | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2)
 32.1033 +
 32.1034 +fun transitive2 thm = transitive1 (SOME thm);
 32.1035 +fun transitive3 thm = transitive1 thm o SOME;
 32.1036 +
 32.1037 +fun bottomc ((simprem, useprem, mutsimp), prover, thy, maxidx) =
 32.1038 +  let
 32.1039 +    fun botc skel ss t =
 32.1040 +          if is_Var skel then NONE
 32.1041 +          else
 32.1042 +          (case subc skel ss t of
 32.1043 +             some as SOME thm1 =>
 32.1044 +               (case rewritec (prover, thy, maxidx) ss (Thm.rhs_of thm1) of
 32.1045 +                  SOME (thm2, skel2) =>
 32.1046 +                    transitive2 (Thm.transitive thm1 thm2)
 32.1047 +                      (botc skel2 ss (Thm.rhs_of thm2))
 32.1048 +                | NONE => some)
 32.1049 +           | NONE =>
 32.1050 +               (case rewritec (prover, thy, maxidx) ss t of
 32.1051 +                  SOME (thm2, skel2) => transitive2 thm2
 32.1052 +                    (botc skel2 ss (Thm.rhs_of thm2))
 32.1053 +                | NONE => NONE))
 32.1054 +
 32.1055 +    and try_botc ss t =
 32.1056 +          (case botc skel0 ss t of
 32.1057 +             SOME trec1 => trec1 | NONE => (Thm.reflexive t))
 32.1058 +
 32.1059 +    and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 =
 32.1060 +       (case term_of t0 of
 32.1061 +           Abs (a, T, _) =>
 32.1062 +             let
 32.1063 +                 val b = Name.bound (#1 bounds);
 32.1064 +                 val (v, t') = Thm.dest_abs (SOME b) t0;
 32.1065 +                 val b' = #1 (Term.dest_Free (Thm.term_of v));
 32.1066 +                 val _ =
 32.1067 +                   if b <> b' then
 32.1068 +                     warning ("Simplifier: renamed bound variable " ^
 32.1069 +                       quote b ^ " to " ^ quote b' ^ Position.str_of (Position.thread_data ()))
 32.1070 +                   else ();
 32.1071 +                 val ss' = add_bound ((b', T), a) ss;
 32.1072 +                 val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
 32.1073 +             in case botc skel' ss' t' of
 32.1074 +                  SOME thm => SOME (Thm.abstract_rule a v thm)
 32.1075 +                | NONE => NONE
 32.1076 +             end
 32.1077 +         | t $ _ => (case t of
 32.1078 +             Const ("==>", _) $ _  => impc t0 ss
 32.1079 +           | Abs _ =>
 32.1080 +               let val thm = Thm.beta_conversion false t0
 32.1081 +               in case subc skel0 ss (Thm.rhs_of thm) of
 32.1082 +                    NONE => SOME thm
 32.1083 +                  | SOME thm' => SOME (Thm.transitive thm thm')
 32.1084 +               end
 32.1085 +           | _  =>
 32.1086 +               let fun appc () =
 32.1087 +                     let
 32.1088 +                       val (tskel, uskel) = case skel of
 32.1089 +                           tskel $ uskel => (tskel, uskel)
 32.1090 +                         | _ => (skel0, skel0);
 32.1091 +                       val (ct, cu) = Thm.dest_comb t0
 32.1092 +                     in
 32.1093 +                     (case botc tskel ss ct of
 32.1094 +                        SOME thm1 =>
 32.1095 +                          (case botc uskel ss cu of
 32.1096 +                             SOME thm2 => SOME (Thm.combination thm1 thm2)
 32.1097 +                           | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu)))
 32.1098 +                      | NONE =>
 32.1099 +                          (case botc uskel ss cu of
 32.1100 +                             SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1)
 32.1101 +                           | NONE => NONE))
 32.1102 +                     end
 32.1103 +                   val (h, ts) = strip_comb t
 32.1104 +               in case cong_name h of
 32.1105 +                    SOME a =>
 32.1106 +                      (case AList.lookup (op =) (fst congs) a of
 32.1107 +                         NONE => appc ()
 32.1108 +                       | SOME cong =>
 32.1109 +  (*post processing: some partial applications h t1 ... tj, j <= length ts,
 32.1110 +    may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
 32.1111 +                          (let
 32.1112 +                             val thm = congc (prover ss) ss maxidx cong t0;
 32.1113 +                             val t = the_default t0 (Option.map Thm.rhs_of thm);
 32.1114 +                             val (cl, cr) = Thm.dest_comb t
 32.1115 +                             val dVar = Var(("", 0), dummyT)
 32.1116 +                             val skel =
 32.1117 +                               list_comb (h, replicate (length ts) dVar)
 32.1118 +                           in case botc skel ss cl of
 32.1119 +                                NONE => thm
 32.1120 +                              | SOME thm' => transitive3 thm
 32.1121 +                                  (Thm.combination thm' (Thm.reflexive cr))
 32.1122 +                           end handle Pattern.MATCH => appc ()))
 32.1123 +                  | _ => appc ()
 32.1124 +               end)
 32.1125 +         | _ => NONE)
 32.1126 +
 32.1127 +    and impc ct ss =
 32.1128 +      if mutsimp then mut_impc0 [] ct [] [] ss else nonmut_impc ct ss
 32.1129 +
 32.1130 +    and rules_of_prem ss prem =
 32.1131 +      if maxidx_of_term (term_of prem) <> ~1
 32.1132 +      then (trace_cterm true
 32.1133 +        (fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:")
 32.1134 +          ss prem; ([], NONE))
 32.1135 +      else
 32.1136 +        let val asm = Thm.assume prem
 32.1137 +        in (extract_safe_rrules (ss, asm), SOME asm) end
 32.1138 +
 32.1139 +    and add_rrules (rrss, asms) ss =
 32.1140 +      (fold o fold) insert_rrule rrss ss |> add_prems (map_filter I asms)
 32.1141 +
 32.1142 +    and disch r prem eq =
 32.1143 +      let
 32.1144 +        val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
 32.1145 +        val eq' = Thm.implies_elim (Thm.instantiate
 32.1146 +          ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
 32.1147 +          (Thm.implies_intr prem eq)
 32.1148 +      in if not r then eq' else
 32.1149 +        let
 32.1150 +          val (prem', concl) = Thm.dest_implies lhs;
 32.1151 +          val (prem'', _) = Thm.dest_implies rhs
 32.1152 +        in Thm.transitive (Thm.transitive
 32.1153 +          (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)])
 32.1154 +             Drule.swap_prems_eq) eq')
 32.1155 +          (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)])
 32.1156 +             Drule.swap_prems_eq)
 32.1157 +        end
 32.1158 +      end
 32.1159 +
 32.1160 +    and rebuild [] _ _ _ _ eq = eq
 32.1161 +      | rebuild (prem :: prems) concl (_ :: rrss) (_ :: asms) ss eq =
 32.1162 +          let
 32.1163 +            val ss' = add_rrules (rev rrss, rev asms) ss;
 32.1164 +            val concl' =
 32.1165 +              Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq));
 32.1166 +            val dprem = Option.map (disch false prem)
 32.1167 +          in
 32.1168 +            (case rewritec (prover, thy, maxidx) ss' concl' of
 32.1169 +              NONE => rebuild prems concl' rrss asms ss (dprem eq)
 32.1170 +            | SOME (eq', _) => transitive2 (fold (disch false)
 32.1171 +                  prems (the (transitive3 (dprem eq) eq')))
 32.1172 +                (mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ss))
 32.1173 +          end
 32.1174 +
 32.1175 +    and mut_impc0 prems concl rrss asms ss =
 32.1176 +      let
 32.1177 +        val prems' = strip_imp_prems concl;
 32.1178 +        val (rrss', asms') = split_list (map (rules_of_prem ss) prems')
 32.1179 +      in
 32.1180 +        mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss')
 32.1181 +          (asms @ asms') [] [] [] [] ss ~1 ~1
 32.1182 +      end
 32.1183 +
 32.1184 +    and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k =
 32.1185 +        transitive1 (fold (fn (eq1, prem) => fn eq2 => transitive1 eq1
 32.1186 +            (Option.map (disch false prem) eq2)) (eqns ~~ prems') NONE)
 32.1187 +          (if changed > 0 then
 32.1188 +             mut_impc (rev prems') concl (rev rrss') (rev asms')
 32.1189 +               [] [] [] [] ss ~1 changed
 32.1190 +           else rebuild prems' concl rrss' asms' ss
 32.1191 +             (botc skel0 (add_rrules (rev rrss', rev asms') ss) concl))
 32.1192 +
 32.1193 +      | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms)
 32.1194 +          prems' rrss' asms' eqns ss changed k =
 32.1195 +        case (if k = 0 then NONE else botc skel0 (add_rrules
 32.1196 +          (rev rrss' @ rrss, rev asms' @ asms) ss) prem) of
 32.1197 +            NONE => mut_impc prems concl rrss asms (prem :: prems')
 32.1198 +              (rrs :: rrss') (asm :: asms') (NONE :: eqns) ss changed
 32.1199 +              (if k = 0 then 0 else k - 1)
 32.1200 +          | SOME eqn =>
 32.1201 +            let
 32.1202 +              val prem' = Thm.rhs_of eqn;
 32.1203 +              val tprems = map term_of prems;
 32.1204 +              val i = 1 + fold Integer.max (map (fn p =>
 32.1205 +                find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1;
 32.1206 +              val (rrs', asm') = rules_of_prem ss prem'
 32.1207 +            in mut_impc prems concl rrss asms (prem' :: prems')
 32.1208 +              (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
 32.1209 +                (take i prems)
 32.1210 +                (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies
 32.1211 +                  (drop i prems, concl))))) :: eqns)
 32.1212 +                  ss (length prems') ~1
 32.1213 +            end
 32.1214 +
 32.1215 +     (*legacy code - only for backwards compatibility*)
 32.1216 +    and nonmut_impc ct ss =
 32.1217 +      let
 32.1218 +        val (prem, conc) = Thm.dest_implies ct;
 32.1219 +        val thm1 = if simprem then botc skel0 ss prem else NONE;
 32.1220 +        val prem1 = the_default prem (Option.map Thm.rhs_of thm1);
 32.1221 +        val ss1 =
 32.1222 +          if not useprem then ss
 32.1223 +          else add_rrules (apsnd single (apfst single (rules_of_prem ss prem1))) ss
 32.1224 +      in
 32.1225 +        (case botc skel0 ss1 conc of
 32.1226 +          NONE =>
 32.1227 +            (case thm1 of
 32.1228 +              NONE => NONE
 32.1229 +            | SOME thm1' => SOME (Drule.imp_cong_rule thm1' (Thm.reflexive conc)))
 32.1230 +        | SOME thm2 =>
 32.1231 +            let val thm2' = disch false prem1 thm2 in
 32.1232 +              (case thm1 of
 32.1233 +                NONE => SOME thm2'
 32.1234 +              | SOME thm1' =>
 32.1235 +                 SOME (Thm.transitive (Drule.imp_cong_rule thm1' (Thm.reflexive conc)) thm2'))
 32.1236 +            end)
 32.1237 +      end
 32.1238 +
 32.1239 + in try_botc end;
 32.1240 +
 32.1241 +
 32.1242 +(* Meta-rewriting: rewrites t to u and returns the theorem t==u *)
 32.1243 +
 32.1244 +(*
 32.1245 +  Parameters:
 32.1246 +    mode = (simplify A,
 32.1247 +            use A in simplifying B,
 32.1248 +            use prems of B (if B is again a meta-impl.) to simplify A)
 32.1249 +           when simplifying A ==> B
 32.1250 +    prover: how to solve premises in conditional rewrites and congruences
 32.1251 +*)
 32.1252 +
 32.1253 +val debug_bounds = Unsynchronized.ref false;
 32.1254 +
 32.1255 +fun check_bounds ss ct =
 32.1256 +  if ! debug_bounds then
 32.1257 +    let
 32.1258 +      val Simpset ({bounds = (_, bounds), ...}, _) = ss;
 32.1259 +      val bs = fold_aterms (fn Free (x, _) =>
 32.1260 +          if Name.is_bound x andalso not (AList.defined eq_bound bounds x)
 32.1261 +          then insert (op =) x else I
 32.1262 +        | _ => I) (term_of ct) [];
 32.1263 +    in
 32.1264 +      if null bs then ()
 32.1265 +      else print_term_global ss true ("Simplifier: term contains loose bounds: " ^ commas_quote bs)
 32.1266 +        (Thm.theory_of_cterm ct) (Thm.term_of ct)
 32.1267 +    end
 32.1268 +  else ();
 32.1269 +
 32.1270 +fun rewrite_cterm mode prover raw_ss raw_ct =
 32.1271 +  let
 32.1272 +    val thy = Thm.theory_of_cterm raw_ct;
 32.1273 +    val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
 32.1274 +    val {maxidx, ...} = Thm.rep_cterm ct;
 32.1275 +    val ss = inc_simp_depth (activate_context thy raw_ss);
 32.1276 +    val depth = simp_depth ss;
 32.1277 +    val _ =
 32.1278 +      if depth mod 20 = 0 then
 32.1279 +        if_visible ss warning ("Simplification depth " ^ string_of_int depth)
 32.1280 +      else ();
 32.1281 +    val _ = trace_cterm false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ss ct;
 32.1282 +    val _ = check_bounds ss ct;
 32.1283 +  in bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct end;
 32.1284 +
 32.1285 +val simple_prover =
 32.1286 +  SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss)));
 32.1287 +
 32.1288 +fun rewrite _ [] ct = Thm.reflexive ct
 32.1289 +  | rewrite full thms ct = rewrite_cterm (full, false, false) simple_prover
 32.1290 +      (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
 32.1291 +
 32.1292 +fun simplify full thms = Conv.fconv_rule (rewrite full thms);
 32.1293 +val rewrite_rule = simplify true;
 32.1294 +
 32.1295 +(*simple term rewriting -- no proof*)
 32.1296 +fun rewrite_term thy rules procs =
 32.1297 +  Pattern.rewrite_term thy (map decomp_simp' rules) procs;
 32.1298 +
 32.1299 +fun rewrite_thm mode prover ss = Conv.fconv_rule (rewrite_cterm mode prover ss);
 32.1300 +
 32.1301 +(*Rewrite the subgoals of a proof state (represented by a theorem)*)
 32.1302 +fun rewrite_goals_rule thms th =
 32.1303 +  Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
 32.1304 +    (global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
 32.1305 +
 32.1306 +(*Rewrite the subgoal of a proof state (represented by a theorem)*)
 32.1307 +fun rewrite_goal_rule mode prover ss i thm =
 32.1308 +  if 0 < i andalso i <= Thm.nprems_of thm
 32.1309 +  then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm
 32.1310 +  else raise THM ("rewrite_goal_rule", i, [thm]);
 32.1311 +
 32.1312 +
 32.1313 +(** meta-rewriting tactics **)
 32.1314 +
 32.1315 +(*Rewrite all subgoals*)
 32.1316 +fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
 32.1317 +fun rewtac def = rewrite_goals_tac [def];
 32.1318 +
 32.1319 +(*Rewrite one subgoal*)
 32.1320 +fun asm_rewrite_goal_tac mode prover_tac ss i thm =
 32.1321 +  if 0 < i andalso i <= Thm.nprems_of thm then
 32.1322 +    Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm)
 32.1323 +  else Seq.empty;
 32.1324 +
 32.1325 +fun rewrite_goal_tac rews =
 32.1326 +  let val ss = empty_ss addsimps rews in
 32.1327 +    fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
 32.1328 +      (global_context (Thm.theory_of_thm st) ss) i st
 32.1329 +  end;
 32.1330 +
 32.1331 +(*Prunes all redundant parameters from the proof state by rewriting.
 32.1332 +  DOES NOT rewrite main goal, where quantification over an unused bound
 32.1333 +    variable is sometimes done to avoid the need for cut_facts_tac.*)
 32.1334 +val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
 32.1335 +
 32.1336 +
 32.1337 +(* for folding definitions, handling critical pairs *)
 32.1338 +
 32.1339 +(*The depth of nesting in a term*)
 32.1340 +fun term_depth (Abs (_, _, t)) = 1 + term_depth t
 32.1341 +  | term_depth (f $ t) = 1 + Int.max (term_depth f, term_depth t)
 32.1342 +  | term_depth _ = 0;
 32.1343 +
 32.1344 +val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
 32.1345 +
 32.1346 +(*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
 32.1347 +  Returns longest lhs first to avoid folding its subexpressions.*)
 32.1348 +fun sort_lhs_depths defs =
 32.1349 +  let val keylist = AList.make (term_depth o lhs_of_thm) defs
 32.1350 +      val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
 32.1351 +  in map (AList.find (op =) keylist) keys end;
 32.1352 +
 32.1353 +val rev_defs = sort_lhs_depths o map Thm.symmetric;
 32.1354 +
 32.1355 +fun fold_rule defs = fold rewrite_rule (rev_defs defs);
 32.1356 +fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
 32.1357 +
 32.1358 +
 32.1359 +(* HHF normal form: !! before ==>, outermost !! generalized *)
 32.1360 +
 32.1361 +local
 32.1362 +
 32.1363 +fun gen_norm_hhf ss th =
 32.1364 +  (if Drule.is_norm_hhf (Thm.prop_of th) then th
 32.1365 +   else Conv.fconv_rule
 32.1366 +    (rewrite_cterm (true, false, false) (K (K NONE)) (global_context (Thm.theory_of_thm th) ss)) th)
 32.1367 +  |> Thm.adjust_maxidx_thm ~1
 32.1368 +  |> Drule.gen_all;
 32.1369 +
 32.1370 +val hhf_ss = empty_ss addsimps Drule.norm_hhf_eqs;
 32.1371 +
 32.1372 +in
 32.1373 +
 32.1374 +val norm_hhf = gen_norm_hhf hhf_ss;
 32.1375 +val norm_hhf_protect = gen_norm_hhf (hhf_ss addeqcongs [Drule.protect_cong]);
 32.1376 +
 32.1377 +end;
 32.1378 +
 32.1379 +end;
 32.1380 +
 32.1381 +structure Basic_Meta_Simplifier: BASIC_RAW_SIMPLIFIER = Raw_Simplifier;
 32.1382 +open Basic_Meta_Simplifier;
    33.1 --- a/src/Pure/simplifier.ML	Fri Dec 17 16:25:21 2010 +0100
    33.2 +++ b/src/Pure/simplifier.ML	Fri Dec 17 17:08:56 2010 +0100
    33.3 @@ -7,7 +7,7 @@
    33.4  
    33.5  signature BASIC_SIMPLIFIER =
    33.6  sig
    33.7 -  include BASIC_META_SIMPLIFIER
    33.8 +  include BASIC_RAW_SIMPLIFIER
    33.9    val change_simpset: (simpset -> simpset) -> unit
   33.10    val global_simpset_of: theory -> simpset
   33.11    val Addsimprocs: simproc list -> unit
   33.12 @@ -75,7 +75,7 @@
   33.13  structure Simplifier: SIMPLIFIER =
   33.14  struct
   33.15  
   33.16 -open MetaSimplifier;
   33.17 +open Raw_Simplifier;
   33.18  
   33.19  
   33.20  (** pretty printing **)
   33.21 @@ -107,7 +107,7 @@
   33.22  (
   33.23    type T = simpset;
   33.24    val empty = empty_ss;
   33.25 -  fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
   33.26 +  fun extend ss = Raw_Simplifier.inherit_context empty_ss ss;
   33.27    val merge = merge_ss;
   33.28  );
   33.29  
   33.30 @@ -130,7 +130,7 @@
   33.31  fun map_simpset f = Context.theory_map (map_ss f);
   33.32  fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
   33.33  fun global_simpset_of thy =
   33.34 -  MetaSimplifier.context (ProofContext.init_global thy) (get_ss (Context.Theory thy));
   33.35 +  Raw_Simplifier.context (ProofContext.init_global thy) (get_ss (Context.Theory thy));
   33.36  
   33.37  fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
   33.38  fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
   33.39 @@ -138,7 +138,7 @@
   33.40  
   33.41  (* local simpset *)
   33.42  
   33.43 -fun simpset_of ctxt = MetaSimplifier.context ctxt (get_ss (Context.Proof ctxt));
   33.44 +fun simpset_of ctxt = Raw_Simplifier.context ctxt (get_ss (Context.Proof ctxt));
   33.45  
   33.46  val _ = ML_Antiquote.value "simpset"
   33.47    (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())");
   33.48 @@ -218,16 +218,16 @@
   33.49  
   33.50  fun solve_all_tac solvers ss =
   33.51    let
   33.52 -    val (_, {subgoal_tac, ...}) = MetaSimplifier.internal_ss ss;
   33.53 -    val solve_tac = subgoal_tac (MetaSimplifier.set_solvers solvers ss) THEN_ALL_NEW (K no_tac);
   33.54 +    val (_, {subgoal_tac, ...}) = Raw_Simplifier.internal_ss ss;
   33.55 +    val solve_tac = subgoal_tac (Raw_Simplifier.set_solvers solvers ss) THEN_ALL_NEW (K no_tac);
   33.56    in DEPTH_SOLVE (solve_tac 1) end;
   33.57  
   33.58  (*NOTE: may instantiate unknowns that appear also in other subgoals*)
   33.59  fun generic_simp_tac safe mode ss =
   33.60    let
   33.61 -    val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.internal_ss ss;
   33.62 +    val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = Raw_Simplifier.internal_ss ss;
   33.63      val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs));
   33.64 -    val solve_tac = FIRST' (map (MetaSimplifier.solver ss)
   33.65 +    val solve_tac = FIRST' (map (Raw_Simplifier.solver ss)
   33.66        (rev (if safe then solvers else unsafe_solvers)));
   33.67  
   33.68      fun simp_loop_tac i =
   33.69 @@ -239,15 +239,15 @@
   33.70  
   33.71  fun simp rew mode ss thm =
   33.72    let
   33.73 -    val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.internal_ss ss;
   33.74 +    val (_, {solvers = (unsafe_solvers, _), ...}) = Raw_Simplifier.internal_ss ss;
   33.75      val tacf = solve_all_tac (rev unsafe_solvers);
   33.76      fun prover s th = Option.map #1 (Seq.pull (tacf s th));
   33.77    in rew mode prover ss thm end;
   33.78  
   33.79  in
   33.80  
   33.81 -val simp_thm = simp MetaSimplifier.rewrite_thm;
   33.82 -val simp_cterm = simp MetaSimplifier.rewrite_cterm;
   33.83 +val simp_thm = simp Raw_Simplifier.rewrite_thm;
   33.84 +val simp_cterm = simp Raw_Simplifier.rewrite_cterm;
   33.85  
   33.86  end;
   33.87  
   33.88 @@ -326,7 +326,7 @@
   33.89  
   33.90  val simplified = conv_mode -- Attrib.thms >>
   33.91    (fn (f, ths) => Thm.rule_attribute (fn context =>
   33.92 -    f ((if null ths then I else MetaSimplifier.clear_ss)
   33.93 +    f ((if null ths then I else Raw_Simplifier.clear_ss)
   33.94          (simpset_of (Context.proof_of context)) addsimps ths)));
   33.95  
   33.96  end;
   33.97 @@ -357,14 +357,14 @@
   33.98    Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add),
   33.99    Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del),
  33.100    Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon
  33.101 -    >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)]
  33.102 +    >> K (Context.proof_map (map_ss Raw_Simplifier.clear_ss), simp_add)]
  33.103     @ cong_modifiers;
  33.104  
  33.105  val simp_modifiers' =
  33.106   [Args.add -- Args.colon >> K (I, simp_add),
  33.107    Args.del -- Args.colon >> K (I, simp_del),
  33.108    Args.$$$ onlyN -- Args.colon
  33.109 -    >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)]
  33.110 +    >> K (Context.proof_map (map_ss Raw_Simplifier.clear_ss), simp_add)]
  33.111     @ cong_modifiers;
  33.112  
  33.113  val simp_options =
    34.1 --- a/src/Tools/atomize_elim.ML	Fri Dec 17 16:25:21 2010 +0100
    34.2 +++ b/src/Tools/atomize_elim.ML	Fri Dec 17 17:08:56 2010 +0100
    34.3 @@ -60,7 +60,7 @@
    34.4  *)
    34.5  fun atomize_elim_conv ctxt ct =
    34.6      (forall_conv (K (prems_conv ~1 Object_Logic.atomize_prems)) ctxt
    34.7 -    then_conv MetaSimplifier.rewrite true (AtomizeElimData.get ctxt)
    34.8 +    then_conv Raw_Simplifier.rewrite true (AtomizeElimData.get ctxt)
    34.9      then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
   34.10                           then all_conv ct'
   34.11                           else raise CTERM ("atomize_elim", [ct', ct])))
    35.1 --- a/src/Tools/coherent.ML	Fri Dec 17 16:25:21 2010 +0100
    35.2 +++ b/src/Tools/coherent.ML	Fri Dec 17 17:08:56 2010 +0100
    35.3 @@ -45,7 +45,7 @@
    35.4    if is_atomic (Logic.strip_imp_concl (term_of ct)) then Conv.all_conv ct
    35.5    else Conv.concl_conv (length (Logic.strip_imp_prems (term_of ct)))
    35.6      (Conv.rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv
    35.7 -     MetaSimplifier.rewrite true (map Thm.symmetric
    35.8 +     Raw_Simplifier.rewrite true (map Thm.symmetric
    35.9         [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
   35.10  
   35.11  fun rulify_elim th = Simplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th);
    36.1 --- a/src/Tools/induct.ML	Fri Dec 17 16:25:21 2010 +0100
    36.2 +++ b/src/Tools/induct.ML	Fri Dec 17 17:08:56 2010 +0100
    36.3 @@ -420,10 +420,10 @@
    36.4  
    36.5  fun mark_constraints n ctxt = Conv.fconv_rule
    36.6    (Conv.prems_conv (~1) (Conv.params_conv ~1 (K (Conv.prems_conv n
    36.7 -     (MetaSimplifier.rewrite false [equal_def']))) ctxt));
    36.8 +     (Raw_Simplifier.rewrite false [equal_def']))) ctxt));
    36.9  
   36.10  val unmark_constraints = Conv.fconv_rule
   36.11 -  (MetaSimplifier.rewrite true [Induct_Args.equal_def]);
   36.12 +  (Raw_Simplifier.rewrite true [Induct_Args.equal_def]);
   36.13  
   36.14  
   36.15  (* simplify *)
   36.16 @@ -514,10 +514,10 @@
   36.17  (* atomize *)
   36.18  
   36.19  fun atomize_term thy =
   36.20 -  MetaSimplifier.rewrite_term thy Induct_Args.atomize []
   36.21 +  Raw_Simplifier.rewrite_term thy Induct_Args.atomize []
   36.22    #> Object_Logic.drop_judgment thy;
   36.23  
   36.24 -val atomize_cterm = MetaSimplifier.rewrite true Induct_Args.atomize;
   36.25 +val atomize_cterm = Raw_Simplifier.rewrite true Induct_Args.atomize;
   36.26  
   36.27  val atomize_tac = Simplifier.rewrite_goal_tac Induct_Args.atomize;
   36.28  
   36.29 @@ -528,8 +528,8 @@
   36.30  (* rulify *)
   36.31  
   36.32  fun rulify_term thy =
   36.33 -  MetaSimplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #>
   36.34 -  MetaSimplifier.rewrite_term thy Induct_Args.rulify_fallback [];
   36.35 +  Raw_Simplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #>
   36.36 +  Raw_Simplifier.rewrite_term thy Induct_Args.rulify_fallback [];
   36.37  
   36.38  fun rulified_term thm =
   36.39    let
   36.40 @@ -668,7 +668,7 @@
   36.41    end);
   36.42  
   36.43  fun miniscope_tac p = CONVERSION o
   36.44 -  Conv.params_conv p (K (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
   36.45 +  Conv.params_conv p (K (Raw_Simplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
   36.46  
   36.47  in
   36.48