src/Pure/meta_simplifier.ML
changeset 15011 35be762f58f9
parent 15006 107e4dfd3b96
child 15023 0e4689f411d5
     1.1 --- a/src/Pure/meta_simplifier.ML	Tue Jun 29 11:18:34 2004 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Wed Jun 30 00:42:59 2004 +0200
     1.3 @@ -20,12 +20,14 @@
     1.4  signature AUX_SIMPLIFIER =
     1.5  sig
     1.6    type meta_simpset
     1.7 +  type simpset
     1.8    type simproc
     1.9 +  val full_mk_simproc: string -> cterm list
    1.10 +    -> (simpset -> Sign.sg -> thm list -> term -> thm option) -> simproc
    1.11    val mk_simproc: string -> cterm list
    1.12      -> (Sign.sg -> thm list -> term -> thm option) -> simproc
    1.13    type solver
    1.14    val mk_solver: string -> (thm list -> int -> tactic) -> solver
    1.15 -  type simpset
    1.16    val empty_ss: simpset
    1.17    val rep_ss: simpset ->
    1.18     {mss: meta_simpset,
    1.19 @@ -33,7 +35,9 @@
    1.20      subgoal_tac: simpset -> int -> tactic,
    1.21      loop_tacs: (string * (int -> tactic)) list,
    1.22      unsafe_solvers: solver list,
    1.23 -    solvers: solver list};
    1.24 +    solvers: solver list}
    1.25 +  val from_mss: meta_simpset -> simpset
    1.26 +  val ss_of            : thm list -> simpset
    1.27    val print_ss: simpset -> unit
    1.28    val setsubgoaler: simpset *  (simpset -> int -> tactic) -> simpset
    1.29    val setloop:      simpset *             (int -> tactic) -> simpset
    1.30 @@ -63,6 +67,10 @@
    1.31      -> (Sign.sg -> thm list -> term -> thm option) -> simproc
    1.32    val simproc_i: Sign.sg -> string -> term list
    1.33      -> (Sign.sg -> thm list -> term -> thm option) -> simproc
    1.34 +  val full_simproc: Sign.sg -> string -> string list
    1.35 +    -> (simpset -> Sign.sg -> thm list -> term -> thm option) -> simproc
    1.36 +  val full_simproc_i: Sign.sg -> string -> term list
    1.37 +    -> (simpset -> Sign.sg -> thm list -> term -> thm option) -> simproc
    1.38    val clear_ss  : simpset -> simpset
    1.39    val simp_thm  : bool * bool * bool -> simpset -> thm -> thm
    1.40    val simp_cterm: bool * bool * bool -> simpset -> cterm -> thm
    1.41 @@ -85,10 +93,10 @@
    1.42    val add_congs         : meta_simpset * thm list -> meta_simpset
    1.43    val del_congs         : meta_simpset * thm list -> meta_simpset
    1.44    val add_simprocs      : meta_simpset *
    1.45 -    (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
    1.46 +    (string * cterm list * (simpset -> Sign.sg -> thm list -> term -> thm option) * stamp) list
    1.47        -> meta_simpset
    1.48    val del_simprocs      : meta_simpset *
    1.49 -    (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
    1.50 +    (string * cterm list * (simpset -> Sign.sg -> thm list -> term -> thm option) * stamp) list
    1.51        -> meta_simpset
    1.52    val add_prems         : meta_simpset * thm list -> meta_simpset
    1.53    val prems_of_mss      : meta_simpset -> thm list
    1.54 @@ -100,19 +108,19 @@
    1.55    val get_mk_eq_True    : meta_simpset -> thm -> thm option
    1.56    val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
    1.57    val rewrite_cterm: bool * bool * bool ->
    1.58 -    (meta_simpset -> thm -> thm option) -> meta_simpset -> cterm -> thm
    1.59 +    (meta_simpset -> thm -> thm option) -> simpset -> cterm -> thm
    1.60    val rewrite_aux       : (meta_simpset -> thm -> thm option) -> bool -> thm list -> cterm -> thm
    1.61    val simplify_aux      : (meta_simpset -> thm -> thm option) -> bool -> thm list -> thm -> thm
    1.62    val rewrite_thm       : bool * bool * bool
    1.63                            -> (meta_simpset -> thm -> thm option)
    1.64 -                          -> meta_simpset -> thm -> thm
    1.65 +                          -> simpset -> thm -> thm
    1.66    val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    1.67    val rewrite_goal_rule : bool* bool * bool
    1.68                            -> (meta_simpset -> thm -> thm option)
    1.69 -                          -> meta_simpset -> int -> thm -> thm
    1.70 +                          -> simpset -> int -> thm -> thm
    1.71    val rewrite_term: Sign.sg -> thm list -> (term -> term option) list -> term -> term
    1.72    val asm_rewrite_goal_tac: bool*bool*bool ->
    1.73 -    (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
    1.74 +    (meta_simpset -> tactic) -> simpset -> int -> tactic
    1.75  
    1.76  end;
    1.77  
    1.78 @@ -181,8 +189,6 @@
    1.79         in which case there is nothing better to do.
    1.80  *)
    1.81  type cong = {thm: thm, lhs: cterm};
    1.82 -type meta_simproc =
    1.83 - {name: string, proc: Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
    1.84  
    1.85  fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
    1.86    #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
    1.87 @@ -193,11 +199,6 @@
    1.88  fun eq_prem (thm1, thm2) =
    1.89    #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
    1.90  
    1.91 -fun eq_simproc ({id = s1, ...}:meta_simproc, {id = s2, ...}:meta_simproc) = (s1 = s2);
    1.92 -
    1.93 -fun mk_simproc (name, proc, lhs, id) =
    1.94 -  {name = name, proc = proc, lhs = lhs, id = id};
    1.95 -
    1.96  
    1.97  (* datatype mss *)
    1.98  
    1.99 @@ -219,6 +220,8 @@
   1.100      depth: depth of conditional rewriting;
   1.101  *)
   1.102  
   1.103 +datatype solver = Solver of string * (thm list -> int -> tactic) * stamp;
   1.104 +
   1.105  datatype meta_simpset =
   1.106    Mss of {
   1.107      rules: rrule Net.net,
   1.108 @@ -230,7 +233,17 @@
   1.109                mk_sym: thm -> thm option,
   1.110                mk_eq_True: thm -> thm option},
   1.111      termless: term * term -> bool,
   1.112 -    depth: int};
   1.113 +    depth: int}
   1.114 +and simpset =
   1.115 +  Simpset of {
   1.116 +    mss: meta_simpset,
   1.117 +    mk_cong: thm -> thm,
   1.118 +    subgoal_tac: simpset -> int -> tactic,
   1.119 +    loop_tacs: (string * (int -> tactic)) list,
   1.120 +    unsafe_solvers: solver list,
   1.121 +    solvers: solver list}
   1.122 +withtype meta_simproc =
   1.123 + {name: string, proc: simpset -> Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
   1.124  
   1.125  fun mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless, depth) =
   1.126    Mss {rules = rules, congs = congs, procs = procs, bounds = bounds,
   1.127 @@ -257,6 +270,14 @@
   1.128            )
   1.129    end;
   1.130  
   1.131 +datatype simproc =
   1.132 +  Simproc of string * cterm list * (simpset -> Sign.sg -> thm list -> term -> thm option) * stamp
   1.133 +
   1.134 +fun eq_simproc ({id = s1, ...}:meta_simproc, {id = s2, ...}:meta_simproc) = (s1 = s2);
   1.135 +
   1.136 +fun mk_simproc (name, proc, lhs, id) =
   1.137 +  {name = name, proc = proc, lhs = lhs, id = id};
   1.138 +
   1.139  
   1.140  (** simpset operations **)
   1.141  
   1.142 @@ -591,11 +612,15 @@
   1.143  
   1.144  (* datatype simproc *)
   1.145  
   1.146 -datatype simproc =
   1.147 -  Simproc of string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp;
   1.148 +fun full_mk_simproc name lhss proc =
   1.149 +  Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ());
   1.150 +
   1.151 +fun full_simproc sg name ss =
   1.152 +  full_mk_simproc name (map (fn s => Thm.read_cterm sg (s, TypeInfer.logicT)) ss);
   1.153 +fun full_simproc_i sg name = full_mk_simproc name o map (Thm.cterm_of sg);
   1.154  
   1.155  fun mk_simproc name lhss proc =
   1.156 -  Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ());
   1.157 +  Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, K proc, stamp ());
   1.158  
   1.159  fun simproc sg name ss =
   1.160    mk_simproc name (map (fn s => Thm.read_cterm sg (s, TypeInfer.logicT)) ss);
   1.161 @@ -607,8 +632,6 @@
   1.162  
   1.163  (** solvers **)
   1.164  
   1.165 -datatype solver = Solver of string * (thm list -> int -> tactic) * stamp;
   1.166 -
   1.167  fun mk_solver name solver = Solver (name, solver, stamp());
   1.168  fun eq_solver (Solver (_, _, s1), Solver(_, _, s2)) = s1 = s2;
   1.169  
   1.170 @@ -624,22 +647,13 @@
   1.171  
   1.172  (* type simpset *)
   1.173  
   1.174 -datatype simpset =
   1.175 -  Simpset of {
   1.176 -    mss: meta_simpset,
   1.177 -    mk_cong: thm -> thm,
   1.178 -    subgoal_tac: simpset -> int -> tactic,
   1.179 -    loop_tacs: (string * (int -> tactic)) list,
   1.180 -    unsafe_solvers: solver list,
   1.181 -    solvers: solver list};
   1.182 -
   1.183  fun make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers =
   1.184    Simpset {mss = mss, mk_cong = mk_cong, subgoal_tac = subgoal_tac,
   1.185      loop_tacs = loop_tacs, unsafe_solvers = unsafe_solvers, solvers = solvers};
   1.186  
   1.187 -val empty_ss =
   1.188 -  let val mss = set_mk_sym (empty_mss, Some o symmetric_fun)
   1.189 -  in make_ss mss I (K (K no_tac)) [] [] [] end;
   1.190 +fun from_mss mss = make_ss mss I (K (K no_tac)) [] [] [];
   1.191 +
   1.192 +val empty_ss = from_mss (set_mk_sym (empty_mss, Some o symmetric_fun));
   1.193  
   1.194  fun rep_ss (Simpset args) = args;
   1.195  fun prems_of_ss (Simpset {mss, ...}) = prems_of_mss mss;
   1.196 @@ -850,7 +864,7 @@
   1.197  *)
   1.198  
   1.199  fun rewritec (prover, signt, maxt)
   1.200 -             (mss as Mss{rules, procs, termless, prems, congs, depth,...}) t =
   1.201 +             (ss as Simpset{mss=mss as Mss{rules, procs, termless, prems, congs, depth,...},...}) t =
   1.202    let
   1.203      val eta_thm = Thm.eta_conversion t;
   1.204      val eta_t' = rhs_of eta_thm;
   1.205 @@ -917,7 +931,7 @@
   1.206            if Pattern.matches tsigt (term_of lhs, term_of t) then
   1.207              (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
   1.208               case transform_failure (curry SIMPROC_FAIL name)
   1.209 -                 (fn () => proc signt prems eta_t) () of
   1.210 +                 (fn () => proc ss signt prems eta_t) () of
   1.211                 None => (debug false "FAILED"; proc_rews ps)
   1.212               | Some raw_thm =>
   1.213                   (trace_thm ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
   1.214 @@ -969,20 +983,24 @@
   1.215  fun transitive2 thm = transitive1 (Some thm);
   1.216  fun transitive3 thm = transitive1 thm o Some;
   1.217  
   1.218 -fun bottomc ((simprem,useprem,mutsimp), prover, sign, maxidx) =
   1.219 +fun replace_mss (Simpset{mss=_,mk_cong,subgoal_tac,loop_tacs,unsafe_solvers,solvers}) mss_new =
   1.220 +    Simpset{mss=mss_new,mk_cong=mk_cong,subgoal_tac=subgoal_tac,loop_tacs=loop_tacs,
   1.221 +	    unsafe_solvers=unsafe_solvers,solvers=solvers};
   1.222 +
   1.223 +fun bottomc ((simprem,useprem,mutsimp), prover, sign, maxidx) (ss as Simpset{mss,...}) =
   1.224    let
   1.225      fun botc skel mss t =
   1.226            if is_Var skel then None
   1.227            else
   1.228            (case subc skel mss t of
   1.229               some as Some thm1 =>
   1.230 -               (case rewritec (prover, sign, maxidx) mss (rhs_of thm1) of
   1.231 +               (case rewritec (prover, sign, maxidx) (replace_mss ss mss) (rhs_of thm1) of
   1.232                    Some (thm2, skel2) =>
   1.233                      transitive2 (transitive thm1 thm2)
   1.234                        (botc skel2 mss (rhs_of thm2))
   1.235                  | None => some)
   1.236             | None =>
   1.237 -               (case rewritec (prover, sign, maxidx) mss t of
   1.238 +               (case rewritec (prover, sign, maxidx) (replace_mss ss mss) t of
   1.239                    Some (thm2, skel2) => transitive2 thm2
   1.240                      (botc skel2 mss (rhs_of thm2))
   1.241                  | None => None))
   1.242 @@ -1093,7 +1111,7 @@
   1.243              val concl' =
   1.244                Drule.mk_implies (prem, if_none (apsome rhs_of eq) concl);
   1.245              val dprem = apsome (curry (disch false) prem)
   1.246 -          in case rewritec (prover, sign, maxidx) mss' concl' of
   1.247 +          in case rewritec (prover, sign, maxidx) (replace_mss ss mss') concl' of
   1.248                None => rebuild prems concl' rrss asms mss (dprem eq)
   1.249              | Some (eq', _) => transitive2 (foldl (disch false o swap)
   1.250                    (the (transitive3 (dprem eq) eq'), prems))
   1.251 @@ -1157,7 +1175,7 @@
   1.252             end)
   1.253         end
   1.254  
   1.255 - in try_botc end;
   1.256 + in try_botc mss end;
   1.257  
   1.258  
   1.259  (*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***)
   1.260 @@ -1172,25 +1190,27 @@
   1.261      prover: how to solve premises in conditional rewrites and congruences
   1.262  *)
   1.263  
   1.264 -fun rewrite_cterm mode prover mss ct =
   1.265 +fun rewrite_cterm mode prover (ss as Simpset{mss,...}) ct =
   1.266    let val {sign, t, maxidx, ...} = rep_cterm ct
   1.267        val Mss{depth, ...} = mss
   1.268    in trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ct;
   1.269       simp_depth := depth;
   1.270 -     bottomc (mode, prover, sign, maxidx) mss ct
   1.271 +     bottomc (mode, prover, sign, maxidx) ss ct
   1.272    end
   1.273    handle THM (s, _, thms) =>
   1.274      error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
   1.275        Pretty.string_of (Display.pretty_thms thms));
   1.276  
   1.277 +val ss_of = from_mss o mss_of
   1.278 +
   1.279  (*Rewrite a cterm*)
   1.280  fun rewrite_aux _ _ [] = (fn ct => Thm.reflexive ct)
   1.281 -  | rewrite_aux prover full thms = rewrite_cterm (full, false, false) prover (mss_of thms);
   1.282 +  | rewrite_aux prover full thms = rewrite_cterm (full, false, false) prover (ss_of thms);
   1.283  
   1.284  (*Rewrite a theorem*)
   1.285  fun simplify_aux _ _ [] = (fn th => th)
   1.286    | simplify_aux prover full thms =
   1.287 -      Drule.fconv_rule (rewrite_cterm (full, false, false) prover (mss_of thms));
   1.288 +      Drule.fconv_rule (rewrite_cterm (full, false, false) prover (ss_of thms));
   1.289  
   1.290  fun rewrite_thm mode prover mss = Drule.fconv_rule (rewrite_cterm mode prover mss);
   1.291  
   1.292 @@ -1198,12 +1218,12 @@
   1.293  fun rewrite_goals_rule_aux _ []   th = th
   1.294    | rewrite_goals_rule_aux prover thms th =
   1.295        Drule.fconv_rule (Drule.goals_conv (K true) (rewrite_cterm (true, true, false) prover
   1.296 -        (mss_of thms))) th;
   1.297 +        (ss_of thms))) th;
   1.298  
   1.299  (*Rewrite the subgoal of a proof state (represented by a theorem) *)
   1.300 -fun rewrite_goal_rule mode prover mss i thm =
   1.301 +fun rewrite_goal_rule mode prover ss i thm =
   1.302    if 0 < i  andalso  i <= nprems_of thm
   1.303 -  then Drule.fconv_rule (Drule.goals_conv (fn j => j=i) (rewrite_cterm mode prover mss)) thm
   1.304 +  then Drule.fconv_rule (Drule.goals_conv (fn j => j=i) (rewrite_cterm mode prover ss)) thm
   1.305    else raise THM("rewrite_goal_rule",i,[thm]);
   1.306  
   1.307  
   1.308 @@ -1229,25 +1249,25 @@
   1.309  
   1.310  (*note: may instantiate unknowns that appear also in other subgoals*)
   1.311  fun generic_simp_tac safe mode =
   1.312 -  fn (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers, ...}) =>
   1.313 +  fn (ss as Simpset {mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers, ...}) =>
   1.314      let
   1.315        val solvs = app_sols (if safe then solvers else unsafe_solvers);
   1.316        fun simp_loop_tac i =
   1.317          asm_rewrite_goal_tac mode
   1.318            (solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers))
   1.319 -          mss i
   1.320 -        THEN (solvs (prems_of_mss mss) i ORELSE
   1.321 +          ss i
   1.322 +        THEN (solvs (prems_of_ss ss) i ORELSE
   1.323                TRY ((loop_tac loop_tacs THEN_ALL_NEW simp_loop_tac) i))
   1.324      in simp_loop_tac end;
   1.325  
   1.326  (** simplification rules and conversions **)
   1.327  
   1.328  fun simp rew mode
   1.329 -     (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, ...}) thm =
   1.330 +     (ss as Simpset {mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, ...}) thm =
   1.331    let
   1.332      val tacf = solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers);
   1.333      fun prover m th = apsome fst (Seq.pull (tacf m th));
   1.334 -  in rew mode prover mss thm end;
   1.335 +  in rew mode prover ss thm end;
   1.336  
   1.337  val simp_thm = simp rewrite_thm;
   1.338  val simp_cterm = simp rewrite_cterm;