src/Pure/meta_simplifier.ML
author wenzelm
Mon Aug 05 21:17:45 2002 +0200 (2002-08-05)
changeset 13458 a73823f70159
parent 13196 08c42252346f
child 13486 54464ea94d6f
permissions -rw-r--r--
protect simplifier operation against spurious exceptions from simprocs;
     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 option) 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 try (fn () => proc signt prems eta_t) () of
   655                None => (debug true "EXCEPTION in simproc"; proc_rews ps)
   656              | Some None => (debug false "FAILED"; proc_rews ps)
   657              | Some (Some raw_thm) =>
   658                  (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
   659                   (case rews (mk_procrule raw_thm) of
   660                     None => (trace_cterm false "IGNORED - does not match" t; proc_rews ps)
   661                   | some => some)))
   662           else proc_rews ps;
   663   in case eta_t of
   664        Abs _ $ _ => Some (transitive eta_thm
   665          (beta_conversion false eta_t'), skel0)
   666      | _ => (case rews (sort_rrules (Net.match_term rules eta_t)) of
   667                None => proc_rews (Net.match_term procs eta_t)
   668              | some => some)
   669   end;
   670 
   671 
   672 (* conversion to apply a congruence rule to a term *)
   673 
   674 fun congc (prover,signt,maxt) {thm=cong,lhs=lhs} t =
   675   let val {sign, ...} = rep_thm cong
   676       val _ = if Sign.subsig (sign, signt) then ()
   677                  else error("Congruence rule from different theory")
   678       val rthm = if maxt = ~1 then cong else Thm.incr_indexes (maxt+1) cong;
   679       val rlhs = fst (Drule.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
   680       val insts = Thm.cterm_match (rlhs, t)
   681       (* Pattern.match can raise Pattern.MATCH;
   682          is handled when congc is called *)
   683       val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
   684       val unit = trace_thm false "Applying congruence rule:" thm';
   685       fun err (msg, thm) = (prthm false msg thm; error "Failed congruence proof!")
   686   in case prover thm' of
   687        None => err ("Could not prove", thm')
   688      | Some thm2 => (case check_conv true (beta_eta_conversion t) thm2 of
   689           None => err ("Should not have proved", thm2)
   690         | Some thm2' =>
   691             if op aconv (pairself term_of (dest_equals (cprop_of thm2')))
   692             then None else Some thm2')
   693   end;
   694 
   695 val (cA, (cB, cC)) =
   696   apsnd dest_equals (dest_implies (hd (cprems_of Drule.imp_cong)));
   697 
   698 fun transitive' thm1 None = Some thm1
   699   | transitive' thm1 (Some thm2) = Some (transitive thm1 thm2);
   700 
   701 fun transitive'' None thm2 = Some thm2
   702   | transitive'' (Some thm1) thm2 = Some (transitive thm1 thm2);
   703 
   704 fun bottomc ((simprem,useprem,mutsimp), prover, sign, maxidx) =
   705   let
   706     fun botc skel mss t =
   707           if is_Var skel then None
   708           else
   709           (case subc skel mss t of
   710              some as Some thm1 =>
   711                (case rewritec (prover, sign, maxidx) mss (rhs_of thm1) of
   712                   Some (thm2, skel2) =>
   713                     transitive' (transitive thm1 thm2)
   714                       (botc skel2 mss (rhs_of thm2))
   715                 | None => some)
   716            | None =>
   717                (case rewritec (prover, sign, maxidx) mss t of
   718                   Some (thm2, skel2) => transitive' thm2
   719                     (botc skel2 mss (rhs_of thm2))
   720                 | None => None))
   721 
   722     and try_botc mss t =
   723           (case botc skel0 mss t of
   724              Some trec1 => trec1 | None => (reflexive t))
   725 
   726     and subc skel
   727           (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless,depth}) t0 =
   728        (case term_of t0 of
   729            Abs (a, T, t) =>
   730              let val b = variant bounds a
   731                  val (v, t') = Thm.dest_abs (Some ("." ^ b)) t0
   732                  val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless,depth)
   733                  val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0
   734              in case botc skel' mss' t' of
   735                   Some thm => Some (abstract_rule a v thm)
   736                 | None => None
   737              end
   738          | t $ _ => (case t of
   739              Const ("==>", _) $ _  =>
   740                let val (s, u) = Drule.dest_implies t0
   741                in impc (s, u, mss) end
   742            | Abs _ =>
   743                let val thm = beta_conversion false t0
   744                in case subc skel0 mss (rhs_of thm) of
   745                     None => Some thm
   746                   | Some thm' => Some (transitive thm thm')
   747                end
   748            | _  =>
   749                let fun appc () =
   750                      let
   751                        val (tskel, uskel) = case skel of
   752                            tskel $ uskel => (tskel, uskel)
   753                          | _ => (skel0, skel0);
   754                        val (ct, cu) = Thm.dest_comb t0
   755                      in
   756                      (case botc tskel mss ct of
   757                         Some thm1 =>
   758                           (case botc uskel mss cu of
   759                              Some thm2 => Some (combination thm1 thm2)
   760                            | None => Some (combination thm1 (reflexive cu)))
   761                       | None =>
   762                           (case botc uskel mss cu of
   763                              Some thm1 => Some (combination (reflexive ct) thm1)
   764                            | None => None))
   765                      end
   766                    val (h, ts) = strip_comb t
   767                in case h of
   768                     Const(a, _) =>
   769                       (case assoc_string (fst congs, a) of
   770                          None => appc ()
   771                        | Some cong =>
   772 (* post processing: some partial applications h t1 ... tj, j <= length ts,
   773    may be a redex. Example: map (%x.x) = (%xs.xs) wrt map_cong *)
   774                           (let
   775                              val thm = congc (prover mss, sign, maxidx) cong t0;
   776                              val t = if_none (apsome rhs_of thm) t0;
   777                              val (cl, cr) = Thm.dest_comb t
   778                              val dVar = Var(("", 0), dummyT)
   779                              val skel =
   780                                list_comb (h, replicate (length ts) dVar)
   781                            in case botc skel mss cl of
   782                                 None => thm
   783                               | Some thm' => transitive'' thm
   784                                   (combination thm' (reflexive cr))
   785                            end handle TERM _ => error "congc result"
   786                                     | Pattern.MATCH => appc ()))
   787                   | _ => appc ()
   788                end)
   789          | _ => None)
   790 
   791     and impc args =
   792       if mutsimp
   793       then let val (prem, conc, mss) = args
   794            in apsome snd (mut_impc ([], prem, conc, mss)) end
   795       else nonmut_impc args
   796 
   797     and mut_impc (prems, prem, conc, mss) = (case botc skel0 mss prem of
   798         None => mut_impc1 (prems, prem, conc, mss)
   799       | Some thm1 =>
   800           let val prem1 = rhs_of thm1
   801           in (case mut_impc1 (prems, prem1, conc, mss) of
   802               None => Some (None,
   803                 combination (combination refl_implies thm1) (reflexive conc))
   804             | Some (x, thm2) => Some (x, transitive (combination (combination
   805                 refl_implies thm1) (reflexive conc)) thm2))
   806           end)
   807 
   808     and mut_impc1 (prems, prem1, conc, mss) =
   809       let
   810         fun uncond ({thm, lhs, elhs, perm}) =
   811           if Thm.no_prems thm then Some lhs else None
   812 
   813         val (lhss1, mss1) =
   814           if maxidx_of_term (term_of prem1) <> ~1
   815           then (trace_cterm true
   816             "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem1;
   817                 ([],mss))
   818           else let val thm = assume prem1
   819                    val rrules1 = extract_safe_rrules (mss, thm)
   820                    val lhss1 = mapfilter uncond rrules1
   821                    val mss1 = foldl insert_rrule (add_prems (mss, [thm]), rrules1)
   822                in (lhss1, mss1) end
   823 
   824         fun disch1 thm =
   825           let val (cB', cC') = dest_eq thm
   826           in
   827             implies_elim (Thm.instantiate
   828               ([], [(cA, prem1), (cB, cB'), (cC, cC')]) Drule.imp_cong)
   829               (implies_intr prem1 thm)
   830           end
   831 
   832         fun rebuild None = (case rewritec (prover, sign, maxidx) mss
   833             (mk_implies (prem1, conc)) of
   834               None => None
   835             | Some (thm, _) =>
   836                 let val (prem, conc) = Drule.dest_implies (rhs_of thm)
   837                 in (case mut_impc (prems, prem, conc, mss) of
   838                     None => Some (None, thm)
   839                   | Some (x, thm') => Some (x, transitive thm thm'))
   840                 end handle TERM _ => Some (None, thm))
   841           | rebuild (Some thm2) =
   842             let val thm = disch1 thm2
   843             in (case rewritec (prover, sign, maxidx) mss (rhs_of thm) of
   844                  None => Some (None, thm)
   845                | Some (thm', _) =>
   846                    let val (prem, conc) = Drule.dest_implies (rhs_of thm')
   847                    in (case mut_impc (prems, prem, conc, mss) of
   848                        None => Some (None, transitive thm thm')
   849                      | Some (x, thm'') =>
   850                          Some (x, transitive (transitive thm thm') thm''))
   851                    end handle TERM _ => Some (None, transitive thm thm'))
   852             end
   853 
   854         fun simpconc () =
   855           let val (s, t) = Drule.dest_implies conc
   856           in case mut_impc (prems @ [prem1], s, t, mss1) of
   857                None => rebuild None
   858              | Some (Some i, thm2) =>
   859                   let
   860                     val (prem, cC') = Drule.dest_implies (rhs_of thm2);
   861                     val thm2' = transitive (disch1 thm2) (Thm.instantiate
   862                       ([], [(cA, prem1), (cB, prem), (cC, cC')])
   863                       Drule.swap_prems_eq)
   864                   in if i=0 then apsome (apsnd (transitive thm2'))
   865                        (mut_impc1 (prems, prem, mk_implies (prem1, cC'), mss))
   866                      else Some (Some (i-1), thm2')
   867                   end
   868              | Some (None, thm) => rebuild (Some thm)
   869           end handle TERM _ => rebuild (botc skel0 mss1 conc)
   870 
   871       in
   872         let
   873           val tsig = Sign.tsig_of sign
   874           fun reducible t =
   875             exists (fn lhs => Pattern.matches_subterm tsig (lhs, term_of t)) lhss1;
   876         in case dropwhile (not o reducible) prems of
   877             [] => simpconc ()
   878           | red::rest => (trace_cterm false "Can now reduce premise:" red;
   879               Some (Some (length rest), reflexive (mk_implies (prem1, conc))))
   880         end
   881       end
   882 
   883      (* legacy code - only for backwards compatibility *)
   884      and nonmut_impc (prem, conc, mss) =
   885        let val thm1 = if simprem then botc skel0 mss prem else None;
   886            val prem1 = if_none (apsome rhs_of thm1) prem;
   887            val maxidx1 = maxidx_of_term (term_of prem1)
   888            val mss1 =
   889              if not useprem then mss else
   890              if maxidx1 <> ~1
   891              then (trace_cterm true
   892                "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem1;
   893                    mss)
   894              else let val thm = assume prem1
   895                   in add_safe_simp (add_prems (mss, [thm]), thm) end
   896        in (case botc skel0 mss1 conc of
   897            None => (case thm1 of
   898                None => None
   899              | Some thm1' => Some (combination
   900                  (combination refl_implies thm1') (reflexive conc)))
   901          | Some thm2 =>
   902            let
   903              val conc2 = rhs_of thm2;
   904              val thm2' = implies_elim (Thm.instantiate
   905                ([], [(cA, prem1), (cB, conc), (cC, conc2)]) Drule.imp_cong)
   906                (implies_intr prem1 thm2)
   907            in (case thm1 of
   908                None => Some thm2'
   909              | Some thm1' => Some (transitive (combination
   910                  (combination refl_implies thm1') (reflexive conc)) thm2'))
   911            end)
   912        end
   913 
   914  in try_botc end;
   915 
   916 
   917 (*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***)
   918 
   919 (*
   920   Parameters:
   921     mode = (simplify A,
   922             use A in simplifying B,
   923             use prems of B (if B is again a meta-impl.) to simplify A)
   924            when simplifying A ==> B
   925     mss: contains equality theorems of the form [|p1,...|] ==> t==u
   926     prover: how to solve premises in conditional rewrites and congruences
   927 *)
   928 
   929 fun rewrite_cterm mode prover mss ct =
   930   let val {sign, t, maxidx, ...} = rep_cterm ct
   931       val Mss{depth, ...} = mss
   932   in simp_depth := depth;
   933      bottomc (mode, prover, sign, maxidx) mss ct
   934   end
   935   handle THM (s, _, thms) =>
   936     error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
   937       Pretty.string_of (Display.pretty_thms thms));
   938 
   939 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
   940 (*Do not rewrite flex-flex pairs*)
   941 fun goals_conv pred cv =
   942   let fun gconv i ct =
   943         let val (A,B) = Drule.dest_implies ct
   944             val (thA,j) = case term_of A of
   945                   Const("=?=",_)$_$_ => (reflexive A, i)
   946                 | _ => (if pred i then cv A else reflexive A, i+1)
   947         in  combination (combination refl_implies thA) (gconv j B) end
   948         handle TERM _ => reflexive ct
   949   in gconv 1 end;
   950 
   951 (* Rewrite A in !!x1,...,xn. A *)
   952 fun forall_conv cv ct =
   953   let val p as (ct1, ct2) = Thm.dest_comb ct
   954   in (case pairself term_of p of
   955       (Const ("all", _), Abs (s, _, _)) =>
   956          let val (v, ct') = Thm.dest_abs (Some "@") ct2;
   957          in Thm.combination (Thm.reflexive ct1)
   958            (Thm.abstract_rule s v (forall_conv cv ct'))
   959          end
   960     | _ => cv ct)
   961   end handle TERM _ => cv ct;
   962 
   963 (*Use a conversion to transform a theorem*)
   964 fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
   965 
   966 (*Rewrite a cterm*)
   967 fun rewrite_aux _ _ [] = (fn ct => Thm.reflexive ct)
   968   | rewrite_aux prover full thms = rewrite_cterm (full, false, false) prover (mss_of thms);
   969 
   970 (*Rewrite a theorem*)
   971 fun simplify_aux _ _ [] = (fn th => th)
   972   | simplify_aux prover full thms =
   973       fconv_rule (rewrite_cterm (full, false, false) prover (mss_of thms));
   974 
   975 fun rewrite_thm mode prover mss = fconv_rule (rewrite_cterm mode prover mss);
   976 
   977 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
   978 fun rewrite_goals_rule_aux _ []   th = th
   979   | rewrite_goals_rule_aux prover thms th =
   980       fconv_rule (goals_conv (K true) (rewrite_cterm (true, true, false) prover
   981         (mss_of thms))) th;
   982 
   983 (*Rewrite the subgoal of a proof state (represented by a theorem) *)
   984 fun rewrite_goal_rule mode prover mss i thm =
   985   if 0 < i  andalso  i <= nprems_of thm
   986   then fconv_rule (goals_conv (fn j => j=i) (rewrite_cterm mode prover mss)) thm
   987   else raise THM("rewrite_goal_rule",i,[thm]);
   988 
   989 
   990 (*simple term rewriting -- without proofs*)
   991 fun rewrite_term sg rules procs =
   992   Pattern.rewrite_term (Sign.tsig_of sg) (map decomp_simp' rules) procs;
   993 
   994 end;
   995 
   996 structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
   997 open BasicMetaSimplifier;