src/Pure/meta_simplifier.ML
author nipkow
Wed May 09 23:09:26 2001 +0200 (2001-05-09)
changeset 11291 02db0084a695
parent 10767 8fa4aafa7314
child 11295 66925f23ac7f
permissions -rw-r--r--
improved simproc trace IGNORED
     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')) then None
   588         else
   589           (trace_thm false "Applying instance of rewrite rule:" thm;
   590            if unconditional
   591            then
   592              (trace_thm false "Rewriting:" thm';
   593               let val lr = Logic.dest_equals prop;
   594                   val Some thm'' = check_conv false eta_thm thm'
   595               in Some (thm'', uncond_skel (congs, lr)) end)
   596            else
   597              (trace_thm false "Trying to rewrite:" thm';
   598               case prover mss thm' of
   599                 None       => (trace_thm false "FAILED" thm'; None)
   600               | Some thm2 =>
   601                   (case check_conv true eta_thm thm2 of
   602                      None => None |
   603                      Some thm2' =>
   604                        let val concl = Logic.strip_imp_concl prop
   605                            val lr = Logic.dest_equals concl
   606                        in Some (thm2', cond_skel (congs, lr)) end)))
   607       end
   608 
   609     fun rews [] = None
   610       | rews (rrule :: rrules) =
   611           let val opt = rew rrule handle Pattern.MATCH => None
   612           in case opt of None => rews rrules | some => some end;
   613 
   614     fun sort_rrules rrs = let
   615       fun is_simple({thm, ...}:rrule) = case #prop (rep_thm thm) of 
   616                                       Const("==",_) $ _ $ _ => true
   617                                       | _                   => false 
   618       fun sort []        (re1,re2) = re1 @ re2
   619         | sort (rr::rrs) (re1,re2) = if is_simple rr 
   620                                      then sort rrs (rr::re1,re2)
   621                                      else sort rrs (re1,rr::re2)
   622     in sort rrs ([],[]) end
   623 
   624     fun proc_rews ([]:simproc list) = None
   625       | proc_rews ({name, proc, lhs, ...} :: ps) =
   626           if Pattern.matches tsigt (term_of lhs, term_of t) then
   627             (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
   628              case proc signt prems eta_t of
   629                None => (debug false "FAILED"; proc_rews ps)
   630              | Some raw_thm =>
   631                  (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
   632                   (case rews (mk_procrule raw_thm) of
   633                     None => (trace_cterm false "IGNORED - does not match" t; proc_rews ps)
   634                   | some => some)))
   635           else proc_rews ps;
   636   in case eta_t of
   637        Abs _ $ _ => Some (transitive eta_thm
   638          (beta_conversion false (rhs_of eta_thm)), skel0)
   639      | _ => (case rews (sort_rrules (Net.match_term rules eta_t)) of
   640                None => proc_rews (Net.match_term procs eta_t)
   641              | some => some)
   642   end;
   643 
   644 
   645 (* conversion to apply a congruence rule to a term *)
   646 
   647 fun congc (prover,signt,maxt) {thm=cong,lhs=lhs} t =
   648   let val {sign, ...} = rep_thm cong
   649       val _ = if Sign.subsig (sign, signt) then ()
   650                  else error("Congruence rule from different theory")
   651       val rthm = if maxt = ~1 then cong else Thm.incr_indexes (maxt+1) cong;
   652       val rlhs = fst (Drule.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
   653       val insts = Thm.cterm_match (rlhs, t)
   654       (* Pattern.match can raise Pattern.MATCH;
   655          is handled when congc is called *)
   656       val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
   657       val unit = trace_thm false "Applying congruence rule:" thm';
   658       fun err (msg, thm) = (prthm false msg thm; error "Failed congruence proof!")
   659   in case prover thm' of
   660        None => err ("Could not prove", thm')
   661      | Some thm2 => (case check_conv true (beta_eta_conversion t) thm2 of
   662           None => err ("Should not have proved", thm2)
   663         | Some thm2' => thm2')
   664   end;
   665 
   666 val (cA, (cB, cC)) =
   667   apsnd dest_equals (dest_implies (hd (cprems_of Drule.imp_cong)));
   668 
   669 fun transitive' thm1 None = Some thm1
   670   | transitive' thm1 (Some thm2) = Some (transitive thm1 thm2);
   671 
   672 fun bottomc ((simprem,useprem,mutsimp), prover, sign, maxidx) =
   673   let
   674     fun botc skel mss t =
   675           if is_Var skel then None
   676           else
   677           (case subc skel mss t of
   678              some as Some thm1 =>
   679                (case rewritec (prover, sign, maxidx) mss (rhs_of thm1) of
   680                   Some (thm2, skel2) =>
   681                     transitive' (transitive thm1 thm2)
   682                       (botc skel2 mss (rhs_of thm2))
   683                 | None => some)
   684            | None =>
   685                (case rewritec (prover, sign, maxidx) mss t of
   686                   Some (thm2, skel2) => transitive' thm2
   687                     (botc skel2 mss (rhs_of thm2))
   688                 | None => None))
   689 
   690     and try_botc mss t =
   691           (case botc skel0 mss t of
   692              Some trec1 => trec1 | None => (reflexive t))
   693 
   694     and subc skel
   695           (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless}) t0 =
   696        (case term_of t0 of
   697            Abs (a, T, t) =>
   698              let val b = variant bounds a
   699                  val (v, t') = Thm.dest_abs (Some ("." ^ b)) t0
   700                  val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless)
   701                  val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0
   702              in case botc skel' mss' t' of
   703                   Some thm => Some (abstract_rule a v thm)
   704                 | None => None
   705              end
   706          | t $ _ => (case t of
   707              Const ("==>", _) $ _  =>
   708                let val (s, u) = Drule.dest_implies t0
   709                in impc (s, u, mss) end
   710            | Abs _ =>
   711                let val thm = beta_conversion false t0
   712                in case subc skel0 mss (rhs_of thm) of
   713                     None => Some thm
   714                   | Some thm' => Some (transitive thm thm')
   715                end
   716            | _  =>
   717                let fun appc () =
   718                      let
   719                        val (tskel, uskel) = case skel of
   720                            tskel $ uskel => (tskel, uskel)
   721                          | _ => (skel0, skel0);
   722                        val (ct, cu) = Thm.dest_comb t0
   723                      in
   724                      (case botc tskel mss ct of
   725                         Some thm1 =>
   726                           (case botc uskel mss cu of
   727                              Some thm2 => Some (combination thm1 thm2)
   728                            | None => Some (combination thm1 (reflexive cu)))
   729                       | None =>
   730                           (case botc uskel mss cu of
   731                              Some thm1 => Some (combination (reflexive ct) thm1)
   732                            | None => None))
   733                      end
   734                    val (h, ts) = strip_comb t
   735                in case h of
   736                     Const(a, _) =>
   737                       (case assoc_string (fst congs, a) of
   738                          None => appc ()
   739                        | Some cong =>
   740 (* post processing: some partial applications h t1 ... tj, j <= length ts,
   741    may be a redex. Example: map (%x.x) = (%xs.xs) wrt map_cong *)
   742                           (let
   743                              val thm = congc (prover mss, sign, maxidx) cong t0;
   744                              val t = rhs_of thm;
   745                              val (cl, cr) = Thm.dest_comb t
   746                              val dVar = Var(("", 0), dummyT)
   747                              val skel =
   748                                list_comb (h, replicate (length ts) dVar)
   749                            in case botc skel mss cl of
   750                                 None => Some thm
   751                               | Some thm' => Some (transitive thm
   752                                   (combination thm' (reflexive cr)))
   753                            end handle TERM _ => error "congc result"
   754                                     | Pattern.MATCH => appc ()))
   755                   | _ => appc ()
   756                end)
   757          | _ => None)
   758 
   759     and impc args =
   760       if mutsimp
   761       then let val (prem, conc, mss) = args
   762            in apsome snd (mut_impc ([], prem, conc, mss)) end
   763       else nonmut_impc args
   764 
   765     and mut_impc (prems, prem, conc, mss) = (case botc skel0 mss prem of
   766         None => mut_impc1 (prems, prem, conc, mss)
   767       | Some thm1 =>
   768           let val prem1 = rhs_of thm1
   769           in (case mut_impc1 (prems, prem1, conc, mss) of
   770               None => Some (None,
   771                 combination (combination refl_implies thm1) (reflexive conc))
   772             | Some (x, thm2) => Some (x, transitive (combination (combination
   773                 refl_implies thm1) (reflexive conc)) thm2))
   774           end)
   775 
   776     and mut_impc1 (prems, prem1, conc, mss) =
   777       let
   778         fun uncond ({thm, lhs, elhs, perm}) =
   779           if Thm.no_prems thm then Some lhs else None
   780 
   781         val (lhss1, mss1) =
   782           if maxidx_of_term (term_of prem1) <> ~1
   783           then (trace_cterm true
   784             "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem1;
   785                 ([],mss))
   786           else let val thm = assume prem1
   787                    val rrules1 = extract_safe_rrules (mss, thm)
   788                    val lhss1 = mapfilter uncond rrules1
   789                    val mss1 = foldl insert_rrule (add_prems (mss, [thm]), rrules1)
   790                in (lhss1, mss1) end
   791 
   792         fun disch1 thm =
   793           let val (cB', cC') = dest_eq thm
   794           in
   795             implies_elim (Thm.instantiate
   796               ([], [(cA, prem1), (cB, cB'), (cC, cC')]) Drule.imp_cong)
   797               (implies_intr prem1 thm)
   798           end
   799 
   800         fun rebuild None = (case rewritec (prover, sign, maxidx) mss
   801             (mk_implies (prem1, conc)) of
   802               None => None
   803             | Some (thm, _) => Some (None, thm))
   804           | rebuild (Some thm2) =
   805             let val thm = disch1 thm2
   806             in (case rewritec (prover, sign, maxidx) mss (rhs_of thm) of
   807                  None => Some (None, thm)
   808                | Some (thm', _) =>
   809                    let val (prem, conc) = Drule.dest_implies (rhs_of thm')
   810                    in (case mut_impc (prems, prem, conc, mss) of
   811                        None => Some (None, transitive thm thm')
   812                      | Some (x, thm'') =>
   813                          Some (x, transitive (transitive thm thm') thm''))
   814                    end handle TERM _ => Some (None, transitive thm thm'))
   815             end
   816 
   817         fun simpconc () =
   818           let val (s, t) = Drule.dest_implies conc
   819           in case mut_impc (prems @ [prem1], s, t, mss1) of
   820                None => rebuild None
   821              | Some (Some i, thm2) =>
   822                   let
   823                     val (prem, cC') = Drule.dest_implies (rhs_of thm2);
   824                     val thm2' = transitive (disch1 thm2) (Thm.instantiate
   825                       ([], [(cA, prem1), (cB, prem), (cC, cC')])
   826                       Drule.swap_prems_eq)
   827                   in if i=0 then apsome (apsnd (transitive thm2'))
   828                        (mut_impc1 (prems, prem, mk_implies (prem1, cC'), mss))
   829                      else Some (Some (i-1), thm2')
   830                   end
   831              | Some (None, thm) => rebuild (Some thm)
   832           end handle TERM _ => rebuild (botc skel0 mss1 conc)
   833 
   834       in
   835         let
   836           val tsig = Sign.tsig_of sign
   837           fun reducible t =
   838             exists (fn lhs => Pattern.matches_subterm tsig (lhs, term_of t)) lhss1;
   839         in case dropwhile (not o reducible) prems of
   840             [] => simpconc ()
   841           | red::rest => (trace_cterm false "Can now reduce premise:" red;
   842               Some (Some (length rest), reflexive (mk_implies (prem1, conc))))
   843         end
   844       end
   845 
   846      (* legacy code - only for backwards compatibility *)
   847      and nonmut_impc (prem, conc, mss) =
   848        let val thm1 = if simprem then botc skel0 mss prem else None;
   849            val prem1 = if_none (apsome rhs_of thm1) prem;
   850            val maxidx1 = maxidx_of_term (term_of prem1)
   851            val mss1 =
   852              if not useprem then mss else
   853              if maxidx1 <> ~1
   854              then (trace_cterm true
   855                "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem1;
   856                    mss)
   857              else let val thm = assume prem1
   858                   in add_safe_simp (add_prems (mss, [thm]), thm) end
   859        in (case botc skel0 mss1 conc of
   860            None => (case thm1 of
   861                None => None
   862              | Some thm1' => Some (combination
   863                  (combination refl_implies thm1') (reflexive conc)))
   864          | Some thm2 =>
   865            let
   866              val conc2 = rhs_of thm2;
   867              val thm2' = implies_elim (Thm.instantiate
   868                ([], [(cA, prem1), (cB, conc), (cC, conc2)]) Drule.imp_cong)
   869                (implies_intr prem1 thm2)
   870            in (case thm1 of
   871                None => Some thm2'
   872              | Some thm1' => Some (transitive (combination
   873                  (combination refl_implies thm1') (reflexive conc)) thm2'))
   874            end)
   875        end
   876 
   877  in try_botc end;
   878 
   879 
   880 (*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***)
   881 
   882 (*
   883   Parameters:
   884     mode = (simplify A,
   885             use A in simplifying B,
   886             use prems of B (if B is again a meta-impl.) to simplify A)
   887            when simplifying A ==> B
   888     mss: contains equality theorems of the form [|p1,...|] ==> t==u
   889     prover: how to solve premises in conditional rewrites and congruences
   890 *)
   891 
   892 (* FIXME: check that #bounds(mss) does not "occur" in ct already *)
   893 
   894 fun rewrite_cterm mode prover mss ct =
   895   let val {sign, t, maxidx, ...} = rep_cterm ct
   896   in bottomc (mode, prover, sign, maxidx) mss ct end
   897   handle THM (s, _, thms) =>
   898     error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
   899       Pretty.string_of (pretty_thms thms));
   900 
   901 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
   902 (*Do not rewrite flex-flex pairs*)
   903 fun goals_conv pred cv =
   904   let fun gconv i ct =
   905         let val (A,B) = Drule.dest_implies ct
   906             val (thA,j) = case term_of A of
   907                   Const("=?=",_)$_$_ => (reflexive A, i)
   908                 | _ => (if pred i then cv A else reflexive A, i+1)
   909         in  combination (combination refl_implies thA) (gconv j B) end
   910         handle TERM _ => reflexive ct
   911   in gconv 1 end;
   912 
   913 (*Use a conversion to transform a theorem*)
   914 fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
   915 
   916 (*Rewrite a theorem*)
   917 fun rewrite_rule_aux _ [] = (fn th => th)
   918   | rewrite_rule_aux prover thms =
   919       fconv_rule (rewrite_cterm (true,false,false) prover (mss_of thms));
   920 
   921 fun rewrite_thm mode prover mss = fconv_rule (rewrite_cterm mode prover mss);
   922 
   923 (*Rewrite the subgoals of a proof state (represented by a theorem) *)
   924 fun rewrite_goals_rule_aux _ []   th = th
   925   | rewrite_goals_rule_aux prover thms th =
   926       fconv_rule (goals_conv (K true) (rewrite_cterm (true, true, false) prover
   927         (mss_of thms))) th;
   928 
   929 (*Rewrite the subgoal of a proof state (represented by a theorem) *)
   930 fun rewrite_goal_rule mode prover mss i thm =
   931   if 0 < i  andalso  i <= nprems_of thm
   932   then fconv_rule (goals_conv (fn j => j=i) (rewrite_cterm mode prover mss)) thm
   933   else raise THM("rewrite_goal_rule",i,[thm]);
   934 
   935 end;
   936 
   937 open MetaSimplifier;