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