src/Pure/meta_simplifier.ML
author wenzelm
Thu Feb 28 19:22:56 2002 +0100 (2002-02-28)
changeset 12979 4c76bce4ce39
parent 12783 36ca5ea8092c
child 13196 08c42252346f
permissions -rw-r--r--
decomp_simp': use lhs instead of elhs (preserves more bound variable names);
     1 (*  Title:      Pure/meta_simplifier.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Stefan Berghofer
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Meta-level Simplification.
     7 *)
     8 
     9 signature BASIC_META_SIMPLIFIER =
    10 sig
    11   val trace_simp: bool ref
    12   val debug_simp: bool ref
    13 end;
    14 
    15 signature META_SIMPLIFIER =
    16 sig
    17   include BASIC_META_SIMPLIFIER
    18   exception SIMPLIFIER of string * thm
    19   type meta_simpset
    20   val dest_mss          : meta_simpset ->
    21     {simps: thm list, congs: thm list, procs: (string * cterm list) list}
    22   val empty_mss         : meta_simpset
    23   val clear_mss         : meta_simpset -> meta_simpset
    24   val merge_mss         : meta_simpset * meta_simpset -> meta_simpset
    25   val add_simps         : meta_simpset * thm list -> meta_simpset
    26   val del_simps         : meta_simpset * thm list -> meta_simpset
    27   val mss_of            : thm list -> meta_simpset
    28   val add_congs         : meta_simpset * thm list -> meta_simpset
    29   val del_congs         : meta_simpset * thm list -> meta_simpset
    30   val add_simprocs      : meta_simpset *
    31     (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
    32       -> meta_simpset
    33   val del_simprocs      : meta_simpset *
    34     (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
    35       -> meta_simpset
    36   val add_prems         : meta_simpset * thm list -> meta_simpset
    37   val prems_of_mss      : meta_simpset -> thm list
    38   val set_mk_rews       : meta_simpset * (thm -> thm list) -> meta_simpset
    39   val set_mk_sym        : meta_simpset * (thm -> thm option) -> meta_simpset
    40   val set_mk_eq_True    : meta_simpset * (thm -> thm option) -> meta_simpset
    41   val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
    42   val beta_eta_conversion: cterm -> thm
    43   val rewrite_cterm: bool * bool * bool ->
    44     (meta_simpset -> thm -> thm option) -> meta_simpset -> cterm -> thm
    45   val goals_conv        : (int -> bool) -> (cterm -> thm) -> cterm -> thm
    46   val forall_conv       : (cterm -> thm) -> cterm -> thm
    47   val fconv_rule        : (cterm -> thm) -> thm -> thm
    48   val rewrite_aux       : (meta_simpset -> thm -> thm option) -> bool -> thm list -> cterm -> thm
    49   val simplify_aux      : (meta_simpset -> thm -> thm option) -> bool -> thm list -> thm -> thm
    50   val rewrite_thm       : bool * bool * bool
    51                           -> (meta_simpset -> thm -> thm option)
    52                           -> meta_simpset -> thm -> thm
    53   val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    54   val rewrite_goal_rule : bool* bool * bool
    55                           -> (meta_simpset -> thm -> thm option)
    56                           -> meta_simpset -> int -> thm -> thm
    57   val rewrite_term: Sign.sg -> thm list -> term -> term
    58 end;
    59 
    60 structure MetaSimplifier : META_SIMPLIFIER =
    61 struct
    62 
    63 (** diagnostics **)
    64 
    65 exception SIMPLIFIER of string * thm;
    66 
    67 val simp_depth = ref 0;
    68 
    69 local
    70 
    71 fun println a =
    72   tracing ((case ! simp_depth of 0 => "" | n => "[" ^ string_of_int n ^ "]") ^ a);
    73 
    74 fun prnt warn a = if warn then warning a else println a;
    75 fun prtm warn a sign t = prnt warn (a ^ "\n" ^ Sign.string_of_term sign t);
    76 fun prctm warn a t = prnt warn (a ^ "\n" ^ Display.string_of_cterm t);
    77 
    78 in
    79 
    80 fun prthm warn a = prctm warn a o Thm.cprop_of;
    81 
    82 val trace_simp = ref false;
    83 val debug_simp = ref false;
    84 
    85 fun trace warn a = if !trace_simp then prnt warn a else ();
    86 fun debug warn a = if !debug_simp then prnt warn a else ();
    87 
    88 fun trace_term warn a sign t = if !trace_simp then prtm warn a sign t else ();
    89 fun trace_cterm warn a t = if !trace_simp then prctm warn a t else ();
    90 fun debug_term warn a sign t = if !debug_simp then prtm warn a sign t else ();
    91 
    92 fun trace_thm warn a thm =
    93   let val {sign, prop, ...} = rep_thm thm
    94   in trace_term warn a sign prop end;
    95 
    96 end;
    97 
    98 
    99 (** meta simp sets **)
   100 
   101 (* basic components *)
   102 
   103 type rrule = {thm: thm, lhs: term, elhs: cterm, fo: bool, perm: bool};
   104 (* thm: the rewrite rule
   105    lhs: the left-hand side
   106    elhs: the etac-contracted lhs.
   107    fo:  use first-order matching
   108    perm: the rewrite rule is permutative
   109 Remarks:
   110   - elhs is used for matching,
   111     lhs only for preservation of bound variable names.
   112   - fo is set iff
   113     either elhs is first-order (no Var is applied),
   114            in which case fo-matching is complete,
   115     or elhs is not a pattern,
   116        in which case there is nothing better to do.
   117 *)
   118 type cong = {thm: thm, lhs: cterm};
   119 type simproc =
   120  {name: string, proc: Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
   121 
   122 fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
   123   #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
   124 
   125 fun eq_cong ({thm = thm1, ...}: cong, {thm = thm2, ...}: cong) =
   126   #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
   127 
   128 fun eq_prem (thm1, thm2) =
   129   #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
   130 
   131 fun eq_simproc ({id = s1, ...}:simproc, {id = s2, ...}:simproc) = (s1 = s2);
   132 
   133 fun mk_simproc (name, proc, lhs, id) =
   134   {name = name, proc = proc, lhs = lhs, id = id};
   135 
   136 
   137 (* datatype mss *)
   138 
   139 (*
   140   A "mss" contains data needed during conversion:
   141     rules: discrimination net of rewrite rules;
   142     congs: association list of congruence rules and
   143            a list of `weak' congruence constants.
   144            A congruence is `weak' if it avoids normalization of some argument.
   145     procs: discrimination net of simplification procedures
   146       (functions that prove rewrite rules on the fly);
   147     bounds: names of bound variables already used
   148       (for generating new names when rewriting under lambda abstractions);
   149     prems: current premises;
   150     mk_rews: mk: turns simplification thms into rewrite rules;
   151              mk_sym: turns == around; (needs Drule!)
   152              mk_eq_True: turns P into P == True - logic specific;
   153     termless: relation for ordered rewriting;
   154     depth: depth of conditional rewriting;
   155 *)
   156 
   157 datatype meta_simpset =
   158   Mss of {
   159     rules: rrule Net.net,
   160     congs: (string * cong) list * string list,
   161     procs: simproc Net.net,
   162     bounds: string list,
   163     prems: thm list,
   164     mk_rews: {mk: thm -> thm list,
   165               mk_sym: thm -> thm option,
   166               mk_eq_True: thm -> thm option},
   167     termless: term * term -> bool,
   168     depth: int};
   169 
   170 fun mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless, depth) =
   171   Mss {rules = rules, congs = congs, procs = procs, bounds = bounds,
   172        prems=prems, mk_rews=mk_rews, termless=termless, depth=depth};
   173 
   174 fun upd_rules(Mss{rules,congs,procs,bounds,prems,mk_rews,termless,depth}, rules') =
   175   mk_mss(rules',congs,procs,bounds,prems,mk_rews,termless,depth);
   176 
   177 val empty_mss =
   178   let val mk_rews = {mk = K [], mk_sym = K None, mk_eq_True = K None}
   179   in mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, Term.termless, 0) end;
   180 
   181 fun clear_mss (Mss {mk_rews, termless, ...}) =
   182   mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, termless,0);
   183 
   184 fun incr_depth(Mss{rules,congs,procs,bounds,prems,mk_rews,termless,depth}) =
   185   mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless, depth+1)
   186 
   187 
   188 
   189 (** simpset operations **)
   190 
   191 (* term variables *)
   192 
   193 val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
   194 fun term_varnames t = add_term_varnames ([], t);
   195 
   196 
   197 (* dest_mss *)
   198 
   199 fun dest_mss (Mss {rules, congs, procs, ...}) =
   200   {simps = map (fn (_, {thm, ...}) => thm) (Net.dest rules),
   201    congs = map (fn (_, {thm, ...}) => thm) (fst congs),
   202    procs =
   203      map (fn (_, {name, lhs, id, ...}) => ((name, lhs), id)) (Net.dest procs)
   204      |> partition_eq eq_snd
   205      |> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))
   206      |> Library.sort_wrt #1};
   207 
   208 
   209 (* merge_mss *)       (*NOTE: ignores mk_rews, termless and depth of 2nd mss*)
   210 
   211 fun merge_mss
   212  (Mss {rules = rules1, congs = (congs1,weak1), procs = procs1,
   213        bounds = bounds1, prems = prems1, mk_rews, termless, depth},
   214   Mss {rules = rules2, congs = (congs2,weak2), procs = procs2,
   215        bounds = bounds2, prems = prems2, ...}) =
   216       mk_mss
   217        (Net.merge (rules1, rules2, eq_rrule),
   218         (gen_merge_lists (eq_cong o pairself snd) congs1 congs2,
   219         merge_lists weak1 weak2),
   220         Net.merge (procs1, procs2, eq_simproc),
   221         merge_lists bounds1 bounds2,
   222         gen_merge_lists eq_prem prems1 prems2,
   223         mk_rews, termless, depth);
   224 
   225 
   226 (* add_simps *)
   227 
   228 fun mk_rrule2{thm,lhs,elhs,perm} =
   229   let val fo = Pattern.first_order (term_of elhs) orelse not(Pattern.pattern (term_of elhs))
   230   in {thm=thm,lhs=lhs,elhs=elhs,fo=fo,perm=perm} end
   231 
   232 fun insert_rrule(mss as Mss {rules,...},
   233                  rrule as {thm,lhs,elhs,perm}) =
   234   (trace_thm false "Adding rewrite rule:" thm;
   235    let val rrule2 as {elhs,...} = mk_rrule2 rrule
   236        val rules' = Net.insert_term ((term_of elhs, rrule2), rules, eq_rrule)
   237    in upd_rules(mss,rules') end
   238    handle Net.INSERT =>
   239      (prthm true "Ignoring duplicate rewrite rule:" thm; mss));
   240 
   241 fun vperm (Var _, Var _) = true
   242   | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
   243   | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
   244   | vperm (t, u) = (t = u);
   245 
   246 fun var_perm (t, u) =
   247   vperm (t, u) andalso eq_set (term_varnames t, term_varnames u);
   248 
   249 (* FIXME: it seems that the conditions on extra variables are too liberal if
   250 prems are nonempty: does solving the prems really guarantee instantiation of
   251 all its Vars? Better: a dynamic check each time a rule is applied.
   252 *)
   253 fun rewrite_rule_extra_vars prems elhs erhs =
   254   not (term_varnames erhs subset foldl add_term_varnames (term_varnames elhs, prems))
   255   orelse
   256   not ((term_tvars erhs) subset
   257        (term_tvars elhs  union  List.concat(map term_tvars prems)));
   258 
   259 (*Simple test for looping rewrite rules and stupid orientations*)
   260 fun reorient sign prems lhs rhs =
   261    rewrite_rule_extra_vars prems lhs rhs
   262   orelse
   263    is_Var (head_of lhs)
   264   orelse
   265    (exists (apl (lhs, Logic.occs)) (rhs :: prems))
   266   orelse
   267    (null prems andalso
   268     Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
   269     (*the condition "null prems" is necessary because conditional rewrites
   270       with extra variables in the conditions may terminate although
   271       the rhs is an instance of the lhs. Example: ?m < ?n ==> f(?n) == f(?m)*)
   272   orelse
   273    (is_Const lhs andalso not(is_Const rhs))
   274 
   275 fun decomp_simp thm =
   276   let val {sign, prop, ...} = rep_thm thm;
   277       val prems = Logic.strip_imp_prems prop;
   278       val concl = Drule.strip_imp_concl (cprop_of thm);
   279       val (lhs, rhs) = Drule.dest_equals concl handle TERM _ =>
   280         raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm)
   281       val elhs = snd (Drule.dest_equals (cprop_of (Thm.eta_conversion lhs)));
   282       val elhs = if elhs=lhs then lhs else elhs (* try to share *)
   283       val erhs = Pattern.eta_contract (term_of rhs);
   284       val perm = var_perm (term_of elhs, erhs) andalso not (term_of elhs aconv erhs)
   285                  andalso not (is_Var (term_of elhs))
   286   in (sign, prems, term_of lhs, elhs, term_of rhs, perm) end;
   287 
   288 fun decomp_simp' thm =
   289   let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
   290     if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
   291     else (lhs, rhs)
   292   end;
   293 
   294 fun mk_eq_True (Mss{mk_rews={mk_eq_True,...},...}) thm =
   295   case mk_eq_True thm of
   296     None => []
   297   | Some eq_True => let val (_,_,lhs,elhs,_,_) = decomp_simp eq_True
   298                     in [{thm=eq_True, lhs=lhs, elhs=elhs, perm=false}] end;
   299 
   300 (* create the rewrite rule and possibly also the ==True variant,
   301    in case there are extra vars on the rhs *)
   302 fun rrule_eq_True(thm,lhs,elhs,rhs,mss,thm2) =
   303   let val rrule = {thm=thm, lhs=lhs, elhs=elhs, perm=false}
   304   in if (term_varnames rhs)  subset (term_varnames lhs) andalso
   305         (term_tvars rhs) subset (term_tvars lhs)
   306      then [rrule]
   307      else mk_eq_True mss thm2 @ [rrule]
   308   end;
   309 
   310 fun mk_rrule mss thm =
   311   let val (_,prems,lhs,elhs,rhs,perm) = decomp_simp thm
   312   in if perm then [{thm=thm, lhs=lhs, elhs=elhs, perm=true}] else
   313      (* weak test for loops: *)
   314      if rewrite_rule_extra_vars prems lhs rhs orelse
   315         is_Var (term_of elhs)
   316      then mk_eq_True mss thm
   317      else rrule_eq_True(thm,lhs,elhs,rhs,mss,thm)
   318   end;
   319 
   320 fun orient_rrule mss thm =
   321   let val (sign,prems,lhs,elhs,rhs,perm) = decomp_simp thm
   322   in if perm then [{thm=thm,lhs=lhs,elhs=elhs,perm=true}]
   323      else if reorient sign prems lhs rhs
   324           then if reorient sign prems rhs lhs
   325                then mk_eq_True mss thm
   326                else let val Mss{mk_rews={mk_sym,...},...} = mss
   327                     in case mk_sym thm of
   328                          None => []
   329                        | Some thm' =>
   330                            let val (_,_,lhs',elhs',rhs',_) = decomp_simp thm'
   331                            in rrule_eq_True(thm',lhs',elhs',rhs',mss,thm) end
   332                     end
   333           else rrule_eq_True(thm,lhs,elhs,rhs,mss,thm)
   334   end;
   335 
   336 fun extract_rews(Mss{mk_rews = {mk,...},...},thms) = flat(map mk thms);
   337 
   338 fun orient_comb_simps comb mk_rrule (mss,thms) =
   339   let val rews = extract_rews(mss,thms)
   340       val rrules = flat (map mk_rrule rews)
   341   in foldl comb (mss,rrules) end
   342 
   343 (* Add rewrite rules explicitly; do not reorient! *)
   344 fun add_simps(mss,thms) =
   345   orient_comb_simps insert_rrule (mk_rrule mss) (mss,thms);
   346 
   347 fun mss_of thms =
   348   foldl insert_rrule (empty_mss, flat(map (mk_rrule empty_mss) thms));
   349 
   350 fun extract_safe_rrules(mss,thm) =
   351   flat (map (orient_rrule mss) (extract_rews(mss,[thm])));
   352 
   353 fun add_safe_simp(mss,thm) =
   354   foldl insert_rrule (mss, extract_safe_rrules(mss,thm))
   355 
   356 (* del_simps *)
   357 
   358 fun del_rrule(mss as Mss {rules,...},
   359               rrule as {thm, elhs, ...}) =
   360   (upd_rules(mss, Net.delete_term ((term_of elhs, rrule), rules, eq_rrule))
   361    handle Net.DELETE =>
   362      (prthm true "Rewrite rule not in simpset:" thm; mss));
   363 
   364 fun del_simps(mss,thms) =
   365   orient_comb_simps del_rrule (map mk_rrule2 o mk_rrule mss) (mss,thms);
   366 
   367 
   368 (* add_congs *)
   369 
   370 fun is_full_cong_prems [] varpairs = null varpairs
   371   | is_full_cong_prems (p::prems) varpairs =
   372     (case Logic.strip_assums_concl p of
   373        Const("==",_) $ lhs $ rhs =>
   374          let val (x,xs) = strip_comb lhs and (y,ys) = strip_comb rhs
   375          in is_Var x  andalso  forall is_Bound xs  andalso
   376             null(findrep(xs))  andalso xs=ys andalso
   377             (x,y) mem varpairs andalso
   378             is_full_cong_prems prems (varpairs\(x,y))
   379          end
   380      | _ => false);
   381 
   382 fun is_full_cong thm =
   383 let val prems = prems_of thm
   384     and concl = concl_of thm
   385     val (lhs,rhs) = Logic.dest_equals concl
   386     val (f,xs) = strip_comb lhs
   387     and (g,ys) = strip_comb rhs
   388 in
   389   f=g andalso null(findrep(xs@ys)) andalso length xs = length ys andalso
   390   is_full_cong_prems prems (xs ~~ ys)
   391 end
   392 
   393 fun add_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth}, thm) =
   394   let
   395     val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (cprop_of thm)) handle TERM _ =>
   396       raise SIMPLIFIER ("Congruence not a meta-equality", thm);
   397 (*   val lhs = Pattern.eta_contract lhs; *)
   398     val (a, _) = dest_Const (head_of (term_of lhs)) handle TERM _ =>
   399       raise SIMPLIFIER ("Congruence must start with a constant", thm);
   400     val (alist,weak) = congs
   401     val alist2 = overwrite_warn (alist, (a,{lhs=lhs, thm=thm}))
   402            ("Overwriting congruence rule for " ^ quote a);
   403     val weak2 = if is_full_cong thm then weak else a::weak
   404   in
   405     mk_mss (rules,(alist2,weak2),procs,bounds,prems,mk_rews,termless,depth)
   406   end;
   407 
   408 val (op add_congs) = foldl add_cong;
   409 
   410 
   411 (* del_congs *)
   412 
   413 fun del_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth}, thm) =
   414   let
   415     val (lhs, _) = Logic.dest_equals (concl_of thm) handle TERM _ =>
   416       raise SIMPLIFIER ("Congruence not a meta-equality", thm);
   417 (*   val lhs = Pattern.eta_contract lhs; *)
   418     val (a, _) = dest_Const (head_of lhs) handle TERM _ =>
   419       raise SIMPLIFIER ("Congruence must start with a constant", thm);
   420     val (alist,_) = congs
   421     val alist2 = filter (fn (x,_)=> x<>a) alist
   422     val weak2 = mapfilter (fn(a,{thm,...}) => if is_full_cong thm then None
   423                                               else Some a)
   424                    alist2
   425   in
   426     mk_mss (rules,(alist2,weak2),procs,bounds,prems,mk_rews,termless,depth)
   427   end;
   428 
   429 val (op del_congs) = foldl del_cong;
   430 
   431 
   432 (* add_simprocs *)
   433 
   434 fun add_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth},
   435     (name, lhs, proc, id)) =
   436   let val {sign, t, ...} = rep_cterm lhs
   437   in (trace_term false ("Adding simplification procedure " ^ quote name ^ " for")
   438       sign t;
   439     mk_mss (rules, congs,
   440       Net.insert_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
   441         handle Net.INSERT =>
   442             (warning ("Ignoring duplicate simplification procedure \""
   443                       ^ name ^ "\"");
   444              procs),
   445         bounds, prems, mk_rews, termless,depth))
   446   end;
   447 
   448 fun add_simproc (mss, (name, lhss, proc, id)) =
   449   foldl add_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);
   450 
   451 val add_simprocs = foldl add_simproc;
   452 
   453 
   454 (* del_simprocs *)
   455 
   456 fun del_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth},
   457     (name, lhs, proc, id)) =
   458   mk_mss (rules, congs,
   459     Net.delete_term ((term_of lhs, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
   460       handle Net.DELETE =>
   461           (warning ("Simplification procedure \"" ^ name ^
   462                        "\" not in simpset"); procs),
   463       bounds, prems, mk_rews, termless, depth);
   464 
   465 fun del_simproc (mss, (name, lhss, proc, id)) =
   466   foldl del_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);
   467 
   468 val del_simprocs = foldl del_simproc;
   469 
   470 
   471 (* prems *)
   472 
   473 fun add_prems (Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth}, thms) =
   474   mk_mss (rules, congs, procs, bounds, thms @ prems, mk_rews, termless, depth);
   475 
   476 fun prems_of_mss (Mss {prems, ...}) = prems;
   477 
   478 
   479 (* mk_rews *)
   480 
   481 fun set_mk_rews
   482   (Mss {rules, congs, procs, bounds, prems, mk_rews, termless, depth}, mk) =
   483     mk_mss (rules, congs, procs, bounds, prems,
   484             {mk=mk, mk_sym= #mk_sym mk_rews, mk_eq_True= #mk_eq_True mk_rews},
   485             termless, depth);
   486 
   487 fun set_mk_sym
   488   (Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth}, mk_sym) =
   489     mk_mss (rules, congs, procs, bounds, prems,
   490             {mk= #mk mk_rews, mk_sym= mk_sym, mk_eq_True= #mk_eq_True mk_rews},
   491             termless,depth);
   492 
   493 fun set_mk_eq_True
   494   (Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth}, mk_eq_True) =
   495     mk_mss (rules, congs, procs, bounds, prems,
   496             {mk= #mk mk_rews, mk_sym= #mk_sym mk_rews, mk_eq_True= mk_eq_True},
   497             termless,depth);
   498 
   499 (* termless *)
   500 
   501 fun set_termless
   502   (Mss {rules, congs, procs, bounds, prems, mk_rews, depth, ...}, termless) =
   503     mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless, depth);
   504 
   505 
   506 
   507 (** rewriting **)
   508 
   509 (*
   510   Uses conversions, see:
   511     L C Paulson, A higher-order implementation of rewriting,
   512     Science of Computer Programming 3 (1983), pages 119-149.
   513 *)
   514 
   515 type prover = meta_simpset -> thm -> thm option;
   516 type termrec = (Sign.sg_ref * term list) * term;
   517 type conv = meta_simpset -> termrec -> termrec;
   518 
   519 val dest_eq = Drule.dest_equals o cprop_of;
   520 val lhs_of = fst o dest_eq;
   521 val rhs_of = snd o dest_eq;
   522 
   523 fun beta_eta_conversion t =
   524   let val thm = beta_conversion true t;
   525   in transitive thm (eta_conversion (rhs_of thm)) end;
   526 
   527 fun check_conv msg thm thm' =
   528   let
   529     val thm'' = transitive thm (transitive
   530       (symmetric (beta_eta_conversion (lhs_of thm'))) thm')
   531   in (if msg then trace_thm false "SUCCEEDED" thm' else (); Some thm'') end
   532   handle THM _ =>
   533     let val {sign, prop = _ $ _ $ prop0, ...} = rep_thm thm;
   534     in
   535       (trace_thm false "Proved wrong thm (Check subgoaler?)" thm';
   536        trace_term false "Should have proved:" sign prop0;
   537        None)
   538     end;
   539 
   540 
   541 (* mk_procrule *)
   542 
   543 fun mk_procrule thm =
   544   let val (_,prems,lhs,elhs,rhs,_) = decomp_simp thm
   545   in if rewrite_rule_extra_vars prems lhs rhs
   546      then (prthm true "Extra vars on rhs:" thm; [])
   547      else [mk_rrule2{thm=thm, lhs=lhs, elhs=elhs, perm=false}]
   548   end;
   549 
   550 
   551 (* conversion to apply the meta simpset to a term *)
   552 
   553 (* Since the rewriting strategy is bottom-up, we avoid re-normalizing already
   554    normalized terms by carrying around the rhs of the rewrite rule just
   555    applied. This is called the `skeleton'. It is decomposed in parallel
   556    with the term. Once a Var is encountered, the corresponding term is
   557    already in normal form.
   558    skel0 is a dummy skeleton that is to enforce complete normalization.
   559 *)
   560 val skel0 = Bound 0;
   561 
   562 (* Use rhs as skeleton only if the lhs does not contain unnormalized bits.
   563    The latter may happen iff there are weak congruence rules for constants
   564    in the lhs.
   565 *)
   566 fun uncond_skel((_,weak),(lhs,rhs)) =
   567   if null weak then rhs (* optimization *)
   568   else if exists_Const (fn (c,_) => c mem weak) lhs then skel0
   569        else rhs;
   570 
   571 (* Behaves like unconditional rule if rhs does not contain vars not in the lhs.
   572    Otherwise those vars may become instantiated with unnormalized terms
   573    while the premises are solved.
   574 *)
   575 fun cond_skel(args as (congs,(lhs,rhs))) =
   576   if term_varnames rhs subset term_varnames lhs then uncond_skel(args)
   577   else skel0;
   578 
   579 (*
   580   we try in order:
   581     (1) beta reduction
   582     (2) unconditional rewrite rules
   583     (3) conditional rewrite rules
   584     (4) simplification procedures
   585 
   586   IMPORTANT: rewrite rules must not introduce new Vars or TVars!
   587 
   588 *)
   589 
   590 fun rewritec (prover, signt, maxt)
   591              (mss as Mss{rules, procs, termless, prems, congs, depth,...}) t =
   592   let
   593     val eta_thm = Thm.eta_conversion t;
   594     val eta_t' = rhs_of eta_thm;
   595     val eta_t = term_of eta_t';
   596     val tsigt = Sign.tsig_of signt;
   597     fun rew {thm, lhs, elhs, fo, perm} =
   598       let
   599         val {sign, prop, maxidx, ...} = rep_thm thm;
   600         val _ = if Sign.subsig (sign, signt) then ()
   601                 else (prthm true "Ignoring rewrite rule from different theory:" thm;
   602                       raise Pattern.MATCH);
   603         val (rthm, elhs') = if maxt = ~1 then (thm, elhs)
   604           else (Thm.incr_indexes (maxt+1) thm, Thm.cterm_incr_indexes (maxt+1) elhs);
   605         val insts = if fo then Thm.cterm_first_order_match (elhs', eta_t')
   606                           else Thm.cterm_match (elhs', eta_t');
   607         val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
   608         val prop' = #prop (rep_thm thm');
   609         val unconditional = (Logic.count_prems (prop',0) = 0);
   610         val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
   611       in
   612         if perm andalso not (termless (rhs', lhs'))
   613         then (trace_thm false "Cannot apply permutative rewrite rule:" thm;
   614               trace_thm false "Term does not become smaller:" thm'; None)
   615         else (trace_thm false "Applying instance of rewrite rule:" thm;
   616            if unconditional
   617            then
   618              (trace_thm false "Rewriting:" thm';
   619               let val lr = Logic.dest_equals prop;
   620                   val Some thm'' = check_conv false eta_thm thm'
   621               in Some (thm'', uncond_skel (congs, lr)) end)
   622            else
   623              (trace_thm false "Trying to rewrite:" thm';
   624               case prover (incr_depth mss) thm' of
   625                 None       => (trace_thm false "FAILED" thm'; None)
   626               | Some thm2 =>
   627                   (case check_conv true eta_thm thm2 of
   628                      None => None |
   629                      Some thm2' =>
   630                        let val concl = Logic.strip_imp_concl prop
   631                            val lr = Logic.dest_equals concl
   632                        in Some (thm2', cond_skel (congs, lr)) end)))
   633       end
   634 
   635     fun rews [] = None
   636       | rews (rrule :: rrules) =
   637           let val opt = rew rrule handle Pattern.MATCH => None
   638           in case opt of None => rews rrules | some => some end;
   639 
   640     fun sort_rrules rrs = let
   641       fun is_simple({thm, ...}:rrule) = case #prop (rep_thm thm) of
   642                                       Const("==",_) $ _ $ _ => true
   643                                       | _                   => false
   644       fun sort []        (re1,re2) = re1 @ re2
   645         | sort (rr::rrs) (re1,re2) = if is_simple rr
   646                                      then sort rrs (rr::re1,re2)
   647                                      else sort rrs (re1,rr::re2)
   648     in sort rrs ([],[]) end
   649 
   650     fun proc_rews ([]:simproc list) = None
   651       | proc_rews ({name, proc, lhs, ...} :: ps) =
   652           if Pattern.matches tsigt (term_of lhs, term_of t) then
   653             (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
   654              case proc signt prems eta_t of
   655                None => (debug false "FAILED"; proc_rews ps)
   656              | Some raw_thm =>
   657                  (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
   658                   (case rews (mk_procrule raw_thm) of
   659                     None => (trace_cterm false "IGNORED - does not match" t; proc_rews ps)
   660                   | some => some)))
   661           else proc_rews ps;
   662   in case eta_t of
   663        Abs _ $ _ => Some (transitive eta_thm
   664          (beta_conversion false eta_t'), skel0)
   665      | _ => (case rews (sort_rrules (Net.match_term rules eta_t)) of
   666                None => proc_rews (Net.match_term procs eta_t)
   667              | some => some)
   668   end;
   669 
   670 
   671 (* conversion to apply a congruence rule to a term *)
   672 
   673 fun congc (prover,signt,maxt) {thm=cong,lhs=lhs} t =
   674   let val {sign, ...} = rep_thm cong
   675       val _ = if Sign.subsig (sign, signt) then ()
   676                  else error("Congruence rule from different theory")
   677       val rthm = if maxt = ~1 then cong else Thm.incr_indexes (maxt+1) cong;
   678       val rlhs = fst (Drule.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
   679       val insts = Thm.cterm_match (rlhs, t)
   680       (* Pattern.match can raise Pattern.MATCH;
   681          is handled when congc is called *)
   682       val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
   683       val unit = trace_thm false "Applying congruence rule:" thm';
   684       fun err (msg, thm) = (prthm false msg thm; error "Failed congruence proof!")
   685   in case prover thm' of
   686        None => err ("Could not prove", thm')
   687      | Some thm2 => (case check_conv true (beta_eta_conversion t) thm2 of
   688           None => err ("Should not have proved", thm2)
   689         | Some thm2' =>
   690             if op aconv (pairself term_of (dest_equals (cprop_of thm2')))
   691             then None else Some thm2')
   692   end;
   693 
   694 val (cA, (cB, cC)) =
   695   apsnd dest_equals (dest_implies (hd (cprems_of Drule.imp_cong)));
   696 
   697 fun transitive' thm1 None = Some thm1
   698   | transitive' thm1 (Some thm2) = Some (transitive thm1 thm2);
   699 
   700 fun transitive'' None thm2 = Some thm2
   701   | transitive'' (Some thm1) thm2 = Some (transitive thm1 thm2);
   702 
   703 fun bottomc ((simprem,useprem,mutsimp), prover, sign, maxidx) =
   704   let
   705     fun botc skel mss t =
   706           if is_Var skel then None
   707           else
   708           (case subc skel mss t of
   709              some as Some thm1 =>
   710                (case rewritec (prover, sign, maxidx) mss (rhs_of thm1) of
   711                   Some (thm2, skel2) =>
   712                     transitive' (transitive thm1 thm2)
   713                       (botc skel2 mss (rhs_of thm2))
   714                 | None => some)
   715            | None =>
   716                (case rewritec (prover, sign, maxidx) mss t of
   717                   Some (thm2, skel2) => transitive' thm2
   718                     (botc skel2 mss (rhs_of thm2))
   719                 | None => None))
   720 
   721     and try_botc mss t =
   722           (case botc skel0 mss t of
   723              Some trec1 => trec1 | None => (reflexive t))
   724 
   725     and subc skel
   726           (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless,depth}) t0 =
   727        (case term_of t0 of
   728            Abs (a, T, t) =>
   729              let val b = variant bounds a
   730                  val (v, t') = Thm.dest_abs (Some ("." ^ b)) t0
   731                  val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless,depth)
   732                  val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0
   733              in case botc skel' mss' t' of
   734                   Some thm => Some (abstract_rule a v thm)
   735                 | None => None
   736              end
   737          | t $ _ => (case t of
   738              Const ("==>", _) $ _  =>
   739                let val (s, u) = Drule.dest_implies t0
   740                in impc (s, u, mss) end
   741            | Abs _ =>
   742                let val thm = beta_conversion false t0
   743                in case subc skel0 mss (rhs_of thm) of
   744                     None => Some thm
   745                   | Some thm' => Some (transitive thm thm')
   746                end
   747            | _  =>
   748                let fun appc () =
   749                      let
   750                        val (tskel, uskel) = case skel of
   751                            tskel $ uskel => (tskel, uskel)
   752                          | _ => (skel0, skel0);
   753                        val (ct, cu) = Thm.dest_comb t0
   754                      in
   755                      (case botc tskel mss ct of
   756                         Some thm1 =>
   757                           (case botc uskel mss cu of
   758                              Some thm2 => Some (combination thm1 thm2)
   759                            | None => Some (combination thm1 (reflexive cu)))
   760                       | None =>
   761                           (case botc uskel mss cu of
   762                              Some thm1 => Some (combination (reflexive ct) thm1)
   763                            | None => None))
   764                      end
   765                    val (h, ts) = strip_comb t
   766                in case h of
   767                     Const(a, _) =>
   768                       (case assoc_string (fst congs, a) of
   769                          None => appc ()
   770                        | Some cong =>
   771 (* post processing: some partial applications h t1 ... tj, j <= length ts,
   772    may be a redex. Example: map (%x.x) = (%xs.xs) wrt map_cong *)
   773                           (let
   774                              val thm = congc (prover mss, sign, maxidx) cong t0;
   775                              val t = if_none (apsome rhs_of thm) t0;
   776                              val (cl, cr) = Thm.dest_comb t
   777                              val dVar = Var(("", 0), dummyT)
   778                              val skel =
   779                                list_comb (h, replicate (length ts) dVar)
   780                            in case botc skel mss cl of
   781                                 None => thm
   782                               | Some thm' => transitive'' thm
   783                                   (combination thm' (reflexive cr))
   784                            end handle TERM _ => error "congc result"
   785                                     | Pattern.MATCH => appc ()))
   786                   | _ => appc ()
   787                end)
   788          | _ => None)
   789 
   790     and impc args =
   791       if mutsimp
   792       then let val (prem, conc, mss) = args
   793            in apsome snd (mut_impc ([], prem, conc, mss)) end
   794       else nonmut_impc args
   795 
   796     and mut_impc (prems, prem, conc, mss) = (case botc skel0 mss prem of
   797         None => mut_impc1 (prems, prem, conc, mss)
   798       | Some thm1 =>
   799           let val prem1 = rhs_of thm1
   800           in (case mut_impc1 (prems, prem1, conc, mss) of
   801               None => Some (None,
   802                 combination (combination refl_implies thm1) (reflexive conc))
   803             | Some (x, thm2) => Some (x, transitive (combination (combination
   804                 refl_implies thm1) (reflexive conc)) thm2))
   805           end)
   806 
   807     and mut_impc1 (prems, prem1, conc, mss) =
   808       let
   809         fun uncond ({thm, lhs, elhs, perm}) =
   810           if Thm.no_prems thm then Some lhs else None
   811 
   812         val (lhss1, mss1) =
   813           if maxidx_of_term (term_of prem1) <> ~1
   814           then (trace_cterm true
   815             "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem1;
   816                 ([],mss))
   817           else let val thm = assume prem1
   818                    val rrules1 = extract_safe_rrules (mss, thm)
   819                    val lhss1 = mapfilter uncond rrules1
   820                    val mss1 = foldl insert_rrule (add_prems (mss, [thm]), rrules1)
   821                in (lhss1, mss1) end
   822 
   823         fun disch1 thm =
   824           let val (cB', cC') = dest_eq thm
   825           in
   826             implies_elim (Thm.instantiate
   827               ([], [(cA, prem1), (cB, cB'), (cC, cC')]) Drule.imp_cong)
   828               (implies_intr prem1 thm)
   829           end
   830 
   831         fun rebuild None = (case rewritec (prover, sign, maxidx) mss
   832             (mk_implies (prem1, conc)) of
   833               None => None
   834             | Some (thm, _) =>
   835                 let val (prem, conc) = Drule.dest_implies (rhs_of thm)
   836                 in (case mut_impc (prems, prem, conc, mss) of
   837                     None => Some (None, thm)
   838                   | Some (x, thm') => Some (x, transitive thm thm'))
   839                 end handle TERM _ => Some (None, thm))
   840           | rebuild (Some thm2) =
   841             let val thm = disch1 thm2
   842             in (case rewritec (prover, sign, maxidx) mss (rhs_of thm) of
   843                  None => Some (None, thm)
   844                | Some (thm', _) =>
   845                    let val (prem, conc) = Drule.dest_implies (rhs_of thm')
   846                    in (case mut_impc (prems, prem, conc, mss) of
   847                        None => Some (None, transitive thm thm')
   848                      | Some (x, thm'') =>
   849                          Some (x, transitive (transitive thm thm') thm''))
   850                    end handle TERM _ => Some (None, transitive thm thm'))
   851             end
   852 
   853         fun simpconc () =
   854           let val (s, t) = Drule.dest_implies conc
   855           in case mut_impc (prems @ [prem1], s, t, mss1) of
   856                None => rebuild None
   857              | Some (Some i, thm2) =>
   858                   let
   859                     val (prem, cC') = Drule.dest_implies (rhs_of thm2);
   860                     val thm2' = transitive (disch1 thm2) (Thm.instantiate
   861                       ([], [(cA, prem1), (cB, prem), (cC, cC')])
   862                       Drule.swap_prems_eq)
   863                   in if i=0 then apsome (apsnd (transitive thm2'))
   864                        (mut_impc1 (prems, prem, mk_implies (prem1, cC'), mss))
   865                      else Some (Some (i-1), thm2')
   866                   end
   867              | Some (None, thm) => rebuild (Some thm)
   868           end handle TERM _ => rebuild (botc skel0 mss1 conc)
   869 
   870       in
   871         let
   872           val tsig = Sign.tsig_of sign
   873           fun reducible t =
   874             exists (fn lhs => Pattern.matches_subterm tsig (lhs, term_of t)) lhss1;
   875         in case dropwhile (not o reducible) prems of
   876             [] => simpconc ()
   877           | red::rest => (trace_cterm false "Can now reduce premise:" red;
   878               Some (Some (length rest), reflexive (mk_implies (prem1, conc))))
   879         end
   880       end
   881 
   882      (* legacy code - only for backwards compatibility *)
   883      and nonmut_impc (prem, conc, mss) =
   884        let val thm1 = if simprem then botc skel0 mss prem else None;
   885            val prem1 = if_none (apsome rhs_of thm1) prem;
   886            val maxidx1 = maxidx_of_term (term_of prem1)
   887            val mss1 =
   888              if not useprem then mss else
   889              if maxidx1 <> ~1
   890              then (trace_cterm true
   891                "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem1;
   892                    mss)
   893              else let val thm = assume prem1
   894                   in add_safe_simp (add_prems (mss, [thm]), thm) end
   895        in (case botc skel0 mss1 conc of
   896            None => (case thm1 of
   897                None => None
   898              | Some thm1' => Some (combination
   899                  (combination refl_implies thm1') (reflexive conc)))
   900          | Some thm2 =>
   901            let
   902              val conc2 = rhs_of thm2;
   903              val thm2' = implies_elim (Thm.instantiate
   904                ([], [(cA, prem1), (cB, conc), (cC, conc2)]) Drule.imp_cong)
   905                (implies_intr prem1 thm2)
   906            in (case thm1 of
   907                None => Some thm2'
   908              | Some thm1' => Some (transitive (combination
   909                  (combination refl_implies thm1') (reflexive conc)) thm2'))
   910            end)
   911        end
   912 
   913  in try_botc end;
   914 
   915 
   916 (*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***)
   917 
   918 (*
   919   Parameters:
   920     mode = (simplify A,
   921             use A in simplifying B,
   922             use prems of B (if B is again a meta-impl.) to simplify A)
   923            when simplifying A ==> B
   924     mss: contains equality theorems of the form [|p1,...|] ==> t==u
   925     prover: how to solve premises in conditional rewrites and congruences
   926 *)
   927 
   928 fun rewrite_cterm mode prover mss ct =
   929   let val {sign, t, maxidx, ...} = rep_cterm ct
   930       val Mss{depth, ...} = mss
   931   in simp_depth := depth;
   932      bottomc (mode, prover, sign, maxidx) mss ct
   933   end
   934   handle THM (s, _, thms) =>
   935     error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
   936       Pretty.string_of (Display.pretty_thms thms));
   937 
   938 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
   939 (*Do not rewrite flex-flex pairs*)
   940 fun goals_conv pred cv =
   941   let fun gconv i ct =
   942         let val (A,B) = Drule.dest_implies ct
   943             val (thA,j) = case term_of A of
   944                   Const("=?=",_)$_$_ => (reflexive A, i)
   945                 | _ => (if pred i then cv A else reflexive A, i+1)
   946         in  combination (combination refl_implies thA) (gconv j B) end
   947         handle TERM _ => reflexive ct
   948   in gconv 1 end;
   949 
   950 (* Rewrite A in !!x1,...,xn. A *)
   951 fun forall_conv cv ct =
   952   let val p as (ct1, ct2) = Thm.dest_comb ct
   953   in (case pairself term_of p of
   954       (Const ("all", _), Abs (s, _, _)) =>
   955          let val (v, ct') = Thm.dest_abs (Some "@") ct2;
   956          in Thm.combination (Thm.reflexive ct1)
   957            (Thm.abstract_rule s v (forall_conv cv ct'))
   958          end
   959     | _ => cv ct)
   960   end handle TERM _ => cv ct;
   961 
   962 (*Use a conversion to transform a theorem*)
   963 fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
   964 
   965 (*Rewrite a cterm*)
   966 fun rewrite_aux _ _ [] = (fn ct => Thm.reflexive ct)
   967   | rewrite_aux prover full thms = rewrite_cterm (full, false, false) prover (mss_of thms);
   968 
   969 (*Rewrite a theorem*)
   970 fun simplify_aux _ _ [] = (fn th => th)
   971   | simplify_aux prover full thms =
   972       fconv_rule (rewrite_cterm (full, false, false) prover (mss_of thms));
   973 
   974 fun rewrite_thm mode prover mss = fconv_rule (rewrite_cterm mode prover mss);
   975 
   976 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
   977 fun rewrite_goals_rule_aux _ []   th = th
   978   | rewrite_goals_rule_aux prover thms th =
   979       fconv_rule (goals_conv (K true) (rewrite_cterm (true, true, false) prover
   980         (mss_of thms))) th;
   981 
   982 (*Rewrite the subgoal of a proof state (represented by a theorem) *)
   983 fun rewrite_goal_rule mode prover mss i thm =
   984   if 0 < i  andalso  i <= nprems_of thm
   985   then fconv_rule (goals_conv (fn j => j=i) (rewrite_cterm mode prover mss)) thm
   986   else raise THM("rewrite_goal_rule",i,[thm]);
   987 
   988 
   989 (*simple term rewriting -- without proofs*)
   990 fun rewrite_term sg rules = Pattern.rewrite_term (Sign.tsig_of sg) (map decomp_simp' rules);
   991 
   992 end;
   993 
   994 structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
   995 open BasicMetaSimplifier;