src/Pure/meta_simplifier.ML
changeset 10413 0e015d9bea4e
child 10767 8fa4aafa7314
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/meta_simplifier.ML	Tue Nov 07 17:44:48 2000 +0100
     1.3 @@ -0,0 +1,937 @@
     1.4 +(*  Title:      Pure/meta_simplifier.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Copyright   1994  University of Cambridge
     1.8 +
     1.9 +Meta Simplification
    1.10 +*)
    1.11 +
    1.12 +signature META_SIMPLIFIER =
    1.13 +sig
    1.14 +  exception SIMPLIFIER of string * thm
    1.15 +  type meta_simpset
    1.16 +  val dest_mss		: meta_simpset ->
    1.17 +    {simps: thm list, congs: thm list, procs: (string * cterm list) list}
    1.18 +  val empty_mss         : meta_simpset
    1.19 +  val clear_mss		: meta_simpset -> meta_simpset
    1.20 +  val merge_mss		: meta_simpset * meta_simpset -> meta_simpset
    1.21 +  val add_simps         : meta_simpset * thm list -> meta_simpset
    1.22 +  val del_simps         : meta_simpset * thm list -> meta_simpset
    1.23 +  val mss_of            : thm list -> meta_simpset
    1.24 +  val add_congs         : meta_simpset * thm list -> meta_simpset
    1.25 +  val del_congs         : meta_simpset * thm list -> meta_simpset
    1.26 +  val add_simprocs	: meta_simpset *
    1.27 +    (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
    1.28 +      -> meta_simpset
    1.29 +  val del_simprocs	: meta_simpset *
    1.30 +    (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
    1.31 +      -> meta_simpset
    1.32 +  val add_prems         : meta_simpset * thm list -> meta_simpset
    1.33 +  val prems_of_mss      : meta_simpset -> thm list
    1.34 +  val set_mk_rews       : meta_simpset * (thm -> thm list) -> meta_simpset
    1.35 +  val set_mk_sym        : meta_simpset * (thm -> thm option) -> meta_simpset
    1.36 +  val set_mk_eq_True    : meta_simpset * (thm -> thm option) -> meta_simpset
    1.37 +  val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
    1.38 +  val trace_simp        : bool ref
    1.39 +  val debug_simp        : bool ref
    1.40 +  val rewrite_cterm     : bool * bool * bool
    1.41 +                          -> (meta_simpset -> thm -> thm option)
    1.42 +                          -> meta_simpset -> cterm -> thm
    1.43 +  val rewrite_rule_aux  : (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    1.44 +  val rewrite_thm       : bool * bool * bool
    1.45 +                          -> (meta_simpset -> thm -> thm option)
    1.46 +                          -> meta_simpset -> thm -> thm
    1.47 +  val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    1.48 +  val rewrite_goal_rule : bool* bool * bool
    1.49 +                          -> (meta_simpset -> thm -> thm option)
    1.50 +                          -> meta_simpset -> int -> thm -> thm
    1.51 +end;
    1.52 +
    1.53 +structure MetaSimplifier : META_SIMPLIFIER =
    1.54 +struct
    1.55 +
    1.56 +(** diagnostics **)
    1.57 +
    1.58 +exception SIMPLIFIER of string * thm;
    1.59 +
    1.60 +fun prnt warn a = if warn then warning a else writeln a;
    1.61 +
    1.62 +fun prtm warn a sign t =
    1.63 +  (prnt warn a; prnt warn (Sign.string_of_term sign t));
    1.64 +
    1.65 +fun prctm warn a t =
    1.66 +  (prnt warn a; prnt warn (Display.string_of_cterm t));
    1.67 +
    1.68 +fun prthm warn a thm =
    1.69 +  let val {sign, prop, ...} = rep_thm thm
    1.70 +  in prtm warn a sign prop end;
    1.71 +
    1.72 +val trace_simp = ref false;
    1.73 +val debug_simp = ref false;
    1.74 +
    1.75 +fun trace warn a = if !trace_simp then prnt warn a else ();
    1.76 +fun debug warn a = if !debug_simp then prnt warn a else ();
    1.77 +
    1.78 +fun trace_term warn a sign t = if !trace_simp then prtm warn a sign t else ();
    1.79 +fun trace_cterm warn a t = if !trace_simp then prctm warn a t else ();
    1.80 +fun debug_term warn a sign t = if !debug_simp then prtm warn a sign t else ();
    1.81 +
    1.82 +fun trace_thm warn a thm =
    1.83 +  let val {sign, prop, ...} = rep_thm thm
    1.84 +  in trace_term warn a sign prop end;
    1.85 +
    1.86 +
    1.87 +
    1.88 +(** meta simp sets **)
    1.89 +
    1.90 +(* basic components *)
    1.91 +
    1.92 +type rrule = {thm: thm, lhs: term, elhs: cterm, fo: bool, perm: bool};
    1.93 +(* thm: the rewrite rule
    1.94 +   lhs: the left-hand side
    1.95 +   elhs: the etac-contracted lhs.
    1.96 +   fo:  use first-order matching
    1.97 +   perm: the rewrite rule is permutative
    1.98 +Reamrks:
    1.99 +  - elhs is used for matching,
   1.100 +    lhs only for preservation of bound variable names.
   1.101 +  - fo is set iff
   1.102 +    either elhs is first-order (no Var is applied),
   1.103 +           in which case fo-matching is complete,
   1.104 +    or elhs is not a pattern,
   1.105 +       in which case there is nothing better to do.
   1.106 +*)
   1.107 +type cong = {thm: thm, lhs: cterm};
   1.108 +type simproc =
   1.109 + {name: string, proc: Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
   1.110 +
   1.111 +fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
   1.112 +  #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
   1.113 +
   1.114 +fun eq_cong ({thm = thm1, ...}: cong, {thm = thm2, ...}: cong) = 
   1.115 +  #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
   1.116 +
   1.117 +fun eq_prem (thm1, thm2) =
   1.118 +  #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
   1.119 +
   1.120 +fun eq_simproc ({id = s1, ...}:simproc, {id = s2, ...}:simproc) = (s1 = s2);
   1.121 +
   1.122 +fun mk_simproc (name, proc, lhs, id) =
   1.123 +  {name = name, proc = proc, lhs = lhs, id = id};
   1.124 +
   1.125 +
   1.126 +(* datatype mss *)
   1.127 +
   1.128 +(*
   1.129 +  A "mss" contains data needed during conversion:
   1.130 +    rules: discrimination net of rewrite rules;
   1.131 +    congs: association list of congruence rules and
   1.132 +           a list of `weak' congruence constants.
   1.133 +           A congruence is `weak' if it avoids normalization of some argument.
   1.134 +    procs: discrimination net of simplification procedures
   1.135 +      (functions that prove rewrite rules on the fly);
   1.136 +    bounds: names of bound variables already used
   1.137 +      (for generating new names when rewriting under lambda abstractions);
   1.138 +    prems: current premises;
   1.139 +    mk_rews: mk: turns simplification thms into rewrite rules;
   1.140 +             mk_sym: turns == around; (needs Drule!)
   1.141 +             mk_eq_True: turns P into P == True - logic specific;
   1.142 +    termless: relation for ordered rewriting;
   1.143 +*)
   1.144 +
   1.145 +datatype meta_simpset =
   1.146 +  Mss of {
   1.147 +    rules: rrule Net.net,
   1.148 +    congs: (string * cong) list * string list,
   1.149 +    procs: simproc Net.net,
   1.150 +    bounds: string list,
   1.151 +    prems: thm list,
   1.152 +    mk_rews: {mk: thm -> thm list,
   1.153 +              mk_sym: thm -> thm option,
   1.154 +              mk_eq_True: thm -> thm option},
   1.155 +    termless: term * term -> bool};
   1.156 +
   1.157 +fun mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless) =
   1.158 +  Mss {rules = rules, congs = congs, procs = procs, bounds = bounds,
   1.159 +       prems=prems, mk_rews=mk_rews, termless=termless};
   1.160 +
   1.161 +fun upd_rules(Mss{rules,congs,procs,bounds,prems,mk_rews,termless}, rules') =
   1.162 +  mk_mss(rules',congs,procs,bounds,prems,mk_rews,termless);
   1.163 +
   1.164 +val empty_mss =
   1.165 +  let val mk_rews = {mk = K [], mk_sym = K None, mk_eq_True = K None}
   1.166 +  in mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, Term.termless) end;
   1.167 +
   1.168 +fun clear_mss (Mss {mk_rews, termless, ...}) =
   1.169 +  mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, termless);
   1.170 +
   1.171 +
   1.172 +
   1.173 +(** simpset operations **)
   1.174 +
   1.175 +(* term variables *)
   1.176 +
   1.177 +val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
   1.178 +fun term_varnames t = add_term_varnames ([], t);
   1.179 +
   1.180 +
   1.181 +(* dest_mss *)
   1.182 +
   1.183 +fun dest_mss (Mss {rules, congs, procs, ...}) =
   1.184 +  {simps = map (fn (_, {thm, ...}) => thm) (Net.dest rules),
   1.185 +   congs = map (fn (_, {thm, ...}) => thm) (fst congs),
   1.186 +   procs =
   1.187 +     map (fn (_, {name, lhs, id, ...}) => ((name, lhs), id)) (Net.dest procs)
   1.188 +     |> partition_eq eq_snd
   1.189 +     |> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))
   1.190 +     |> Library.sort_wrt #1};
   1.191 +
   1.192 +
   1.193 +(* merge_mss *)		(*NOTE: ignores mk_rews and termless of 2nd mss*)
   1.194 +
   1.195 +fun merge_mss
   1.196 + (Mss {rules = rules1, congs = (congs1,weak1), procs = procs1,
   1.197 +       bounds = bounds1, prems = prems1, mk_rews, termless},
   1.198 +  Mss {rules = rules2, congs = (congs2,weak2), procs = procs2,
   1.199 +       bounds = bounds2, prems = prems2, ...}) =
   1.200 +      mk_mss
   1.201 +       (Net.merge (rules1, rules2, eq_rrule),
   1.202 +        (generic_merge (eq_cong o pairself snd) I I congs1 congs2,
   1.203 +        merge_lists weak1 weak2),
   1.204 +        Net.merge (procs1, procs2, eq_simproc),
   1.205 +        merge_lists bounds1 bounds2,
   1.206 +        generic_merge eq_prem I I prems1 prems2,
   1.207 +        mk_rews, termless);
   1.208 +
   1.209 +
   1.210 +(* add_simps *)
   1.211 +
   1.212 +fun mk_rrule2{thm,lhs,elhs,perm} =
   1.213 +  let val fo = Pattern.first_order (term_of elhs) orelse not(Pattern.pattern (term_of elhs))
   1.214 +  in {thm=thm,lhs=lhs,elhs=elhs,fo=fo,perm=perm} end
   1.215 +
   1.216 +fun insert_rrule(mss as Mss {rules,...},
   1.217 +                 rrule as {thm,lhs,elhs,perm}) =
   1.218 +  (trace_thm false "Adding rewrite rule:" thm;
   1.219 +   let val rrule2 as {elhs,...} = mk_rrule2 rrule
   1.220 +       val rules' = Net.insert_term ((term_of elhs, rrule2), rules, eq_rrule)
   1.221 +   in upd_rules(mss,rules') end
   1.222 +   handle Net.INSERT =>
   1.223 +     (prthm true "Ignoring duplicate rewrite rule:" thm; mss));
   1.224 +
   1.225 +fun vperm (Var _, Var _) = true
   1.226 +  | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
   1.227 +  | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
   1.228 +  | vperm (t, u) = (t = u);
   1.229 +
   1.230 +fun var_perm (t, u) =
   1.231 +  vperm (t, u) andalso eq_set (term_varnames t, term_varnames u);
   1.232 +
   1.233 +(* FIXME: it seems that the conditions on extra variables are too liberal if
   1.234 +prems are nonempty: does solving the prems really guarantee instantiation of
   1.235 +all its Vars? Better: a dynamic check each time a rule is applied.
   1.236 +*)
   1.237 +fun rewrite_rule_extra_vars prems elhs erhs =
   1.238 +  not (term_varnames erhs subset foldl add_term_varnames (term_varnames elhs, prems))
   1.239 +  orelse
   1.240 +  not ((term_tvars erhs) subset
   1.241 +       (term_tvars elhs  union  List.concat(map term_tvars prems)));
   1.242 +
   1.243 +(*Simple test for looping rewrite rules and stupid orientations*)
   1.244 +fun reorient sign prems lhs rhs =
   1.245 +   rewrite_rule_extra_vars prems lhs rhs
   1.246 +  orelse
   1.247 +   is_Var (head_of lhs)
   1.248 +  orelse
   1.249 +   (exists (apl (lhs, Logic.occs)) (rhs :: prems))
   1.250 +  orelse
   1.251 +   (null prems andalso
   1.252 +    Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
   1.253 +    (*the condition "null prems" is necessary because conditional rewrites
   1.254 +      with extra variables in the conditions may terminate although
   1.255 +      the rhs is an instance of the lhs. Example: ?m < ?n ==> f(?n) == f(?m)*)
   1.256 +  orelse
   1.257 +   (is_Const lhs andalso not(is_Const rhs))
   1.258 +
   1.259 +fun decomp_simp thm =
   1.260 +  let val {sign, prop, ...} = rep_thm thm;
   1.261 +      val prems = Logic.strip_imp_prems prop;
   1.262 +      val concl = Drule.strip_imp_concl (cprop_of thm);
   1.263 +      val (lhs, rhs) = Drule.dest_equals concl handle TERM _ =>
   1.264 +        raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm)
   1.265 +      val elhs = snd (Drule.dest_equals (cprop_of (Thm.eta_conversion lhs)));
   1.266 +      val elhs = if elhs=lhs then lhs else elhs (* try to share *)
   1.267 +      val erhs = Pattern.eta_contract (term_of rhs);
   1.268 +      val perm = var_perm (term_of elhs, erhs) andalso not (term_of elhs aconv erhs)
   1.269 +                 andalso not (is_Var (term_of elhs))
   1.270 +  in (sign, prems, term_of lhs, elhs, term_of rhs, perm) end;
   1.271 +
   1.272 +fun mk_eq_True (Mss{mk_rews={mk_eq_True,...},...}) thm =
   1.273 +  case mk_eq_True thm of
   1.274 +    None => []
   1.275 +  | Some eq_True => let val (_,_,lhs,elhs,_,_) = decomp_simp eq_True
   1.276 +                    in [{thm=eq_True, lhs=lhs, elhs=elhs, perm=false}] end;
   1.277 +
   1.278 +(* create the rewrite rule and possibly also the ==True variant,
   1.279 +   in case there are extra vars on the rhs *)
   1.280 +fun rrule_eq_True(thm,lhs,elhs,rhs,mss,thm2) =
   1.281 +  let val rrule = {thm=thm, lhs=lhs, elhs=elhs, perm=false}
   1.282 +  in if (term_varnames rhs)  subset (term_varnames lhs) andalso
   1.283 +        (term_tvars rhs) subset (term_tvars lhs)
   1.284 +     then [rrule]
   1.285 +     else mk_eq_True mss thm2 @ [rrule]
   1.286 +  end;
   1.287 +
   1.288 +fun mk_rrule mss thm =
   1.289 +  let val (_,prems,lhs,elhs,rhs,perm) = decomp_simp thm
   1.290 +  in if perm then [{thm=thm, lhs=lhs, elhs=elhs, perm=true}] else
   1.291 +     (* weak test for loops: *)
   1.292 +     if rewrite_rule_extra_vars prems lhs rhs orelse
   1.293 +        is_Var (term_of elhs)
   1.294 +     then mk_eq_True mss thm
   1.295 +     else rrule_eq_True(thm,lhs,elhs,rhs,mss,thm)
   1.296 +  end;
   1.297 +
   1.298 +fun orient_rrule mss thm =
   1.299 +  let val (sign,prems,lhs,elhs,rhs,perm) = decomp_simp thm
   1.300 +  in if perm then [{thm=thm,lhs=lhs,elhs=elhs,perm=true}]
   1.301 +     else if reorient sign prems lhs rhs
   1.302 +          then if reorient sign prems rhs lhs
   1.303 +               then mk_eq_True mss thm
   1.304 +               else let val Mss{mk_rews={mk_sym,...},...} = mss
   1.305 +                    in case mk_sym thm of
   1.306 +                         None => []
   1.307 +                       | Some thm' =>
   1.308 +                           let val (_,_,lhs',elhs',rhs',_) = decomp_simp thm'
   1.309 +                           in rrule_eq_True(thm',lhs',elhs',rhs',mss,thm) end
   1.310 +                    end
   1.311 +          else rrule_eq_True(thm,lhs,elhs,rhs,mss,thm)
   1.312 +  end;
   1.313 +
   1.314 +fun extract_rews(Mss{mk_rews = {mk,...},...},thms) = flat(map mk thms);
   1.315 +
   1.316 +fun orient_comb_simps comb mk_rrule (mss,thms) =
   1.317 +  let val rews = extract_rews(mss,thms)
   1.318 +      val rrules = flat (map mk_rrule rews)
   1.319 +  in foldl comb (mss,rrules) end
   1.320 +
   1.321 +(* Add rewrite rules explicitly; do not reorient! *)
   1.322 +fun add_simps(mss,thms) =
   1.323 +  orient_comb_simps insert_rrule (mk_rrule mss) (mss,thms);
   1.324 +
   1.325 +fun mss_of thms =
   1.326 +  foldl insert_rrule (empty_mss, flat(map (mk_rrule empty_mss) thms));
   1.327 +
   1.328 +fun extract_safe_rrules(mss,thm) =
   1.329 +  flat (map (orient_rrule mss) (extract_rews(mss,[thm])));
   1.330 +
   1.331 +fun add_safe_simp(mss,thm) =
   1.332 +  foldl insert_rrule (mss, extract_safe_rrules(mss,thm))
   1.333 +
   1.334 +(* del_simps *)
   1.335 +
   1.336 +fun del_rrule(mss as Mss {rules,...},
   1.337 +              rrule as {thm, elhs, ...}) =
   1.338 +  (upd_rules(mss, Net.delete_term ((term_of elhs, rrule), rules, eq_rrule))
   1.339 +   handle Net.DELETE =>
   1.340 +     (prthm true "Rewrite rule not in simpset:" thm; mss));
   1.341 +
   1.342 +fun del_simps(mss,thms) =
   1.343 +  orient_comb_simps del_rrule (map mk_rrule2 o mk_rrule mss) (mss,thms);
   1.344 +
   1.345 +
   1.346 +(* add_congs *)
   1.347 +
   1.348 +fun is_full_cong_prems [] varpairs = null varpairs
   1.349 +  | is_full_cong_prems (p::prems) varpairs =
   1.350 +    (case Logic.strip_assums_concl p of
   1.351 +       Const("==",_) $ lhs $ rhs =>
   1.352 +         let val (x,xs) = strip_comb lhs and (y,ys) = strip_comb rhs
   1.353 +         in is_Var x  andalso  forall is_Bound xs  andalso
   1.354 +            null(findrep(xs))  andalso xs=ys andalso
   1.355 +            (x,y) mem varpairs andalso
   1.356 +            is_full_cong_prems prems (varpairs\(x,y))
   1.357 +         end
   1.358 +     | _ => false);
   1.359 +
   1.360 +fun is_full_cong thm =
   1.361 +let val prems = prems_of thm
   1.362 +    and concl = concl_of thm
   1.363 +    val (lhs,rhs) = Logic.dest_equals concl
   1.364 +    val (f,xs) = strip_comb lhs
   1.365 +    and (g,ys) = strip_comb rhs
   1.366 +in
   1.367 +  f=g andalso null(findrep(xs@ys)) andalso length xs = length ys andalso
   1.368 +  is_full_cong_prems prems (xs ~~ ys)
   1.369 +end
   1.370 +
   1.371 +fun add_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thm) =
   1.372 +  let
   1.373 +    val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (cprop_of thm)) handle TERM _ =>
   1.374 +      raise SIMPLIFIER ("Congruence not a meta-equality", thm);
   1.375 +(*   val lhs = Pattern.eta_contract lhs; *)
   1.376 +    val (a, _) = dest_Const (head_of (term_of lhs)) handle TERM _ =>
   1.377 +      raise SIMPLIFIER ("Congruence must start with a constant", thm);
   1.378 +    val (alist,weak) = congs
   1.379 +    val alist2 = overwrite_warn (alist, (a,{lhs=lhs, thm=thm}))
   1.380 +           ("Overwriting congruence rule for " ^ quote a);
   1.381 +    val weak2 = if is_full_cong thm then weak else a::weak
   1.382 +  in
   1.383 +    mk_mss (rules, (alist2,weak2), procs, bounds, prems, mk_rews, termless)
   1.384 +  end;
   1.385 +
   1.386 +val (op add_congs) = foldl add_cong;
   1.387 +
   1.388 +
   1.389 +(* del_congs *)
   1.390 +
   1.391 +fun del_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thm) =
   1.392 +  let
   1.393 +    val (lhs, _) = Logic.dest_equals (concl_of thm) handle TERM _ =>
   1.394 +      raise SIMPLIFIER ("Congruence not a meta-equality", thm);
   1.395 +(*   val lhs = Pattern.eta_contract lhs; *)
   1.396 +    val (a, _) = dest_Const (head_of lhs) handle TERM _ =>
   1.397 +      raise SIMPLIFIER ("Congruence must start with a constant", thm);
   1.398 +    val (alist,_) = congs
   1.399 +    val alist2 = filter (fn (x,_)=> x<>a) alist
   1.400 +    val weak2 = mapfilter (fn(a,{thm,...}) => if is_full_cong thm then None
   1.401 +                                              else Some a)
   1.402 +                   alist2
   1.403 +  in
   1.404 +    mk_mss (rules, (alist2,weak2), procs, bounds, prems, mk_rews, termless)
   1.405 +  end;
   1.406 +
   1.407 +val (op del_congs) = foldl del_cong;
   1.408 +
   1.409 +
   1.410 +(* add_simprocs *)
   1.411 +
   1.412 +fun add_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
   1.413 +    (name, lhs, proc, id)) =
   1.414 +  let val {sign, t, ...} = rep_cterm lhs
   1.415 +  in (trace_term false ("Adding simplification procedure " ^ quote name ^ " for")
   1.416 +      sign t;
   1.417 +    mk_mss (rules, congs,
   1.418 +      Net.insert_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
   1.419 +        handle Net.INSERT => 
   1.420 +	    (warning ("Ignoring duplicate simplification procedure \"" 
   1.421 +	              ^ name ^ "\""); 
   1.422 +	     procs),
   1.423 +        bounds, prems, mk_rews, termless))
   1.424 +  end;
   1.425 +
   1.426 +fun add_simproc (mss, (name, lhss, proc, id)) =
   1.427 +  foldl add_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);
   1.428 +
   1.429 +val add_simprocs = foldl add_simproc;
   1.430 +
   1.431 +
   1.432 +(* del_simprocs *)
   1.433 +
   1.434 +fun del_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
   1.435 +    (name, lhs, proc, id)) =
   1.436 +  mk_mss (rules, congs,
   1.437 +    Net.delete_term ((term_of lhs, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
   1.438 +      handle Net.DELETE => 
   1.439 +	  (warning ("Simplification procedure \"" ^ name ^
   1.440 +		       "\" not in simpset"); procs),
   1.441 +      bounds, prems, mk_rews, termless);
   1.442 +
   1.443 +fun del_simproc (mss, (name, lhss, proc, id)) =
   1.444 +  foldl del_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);
   1.445 +
   1.446 +val del_simprocs = foldl del_simproc;
   1.447 +
   1.448 +
   1.449 +(* prems *)
   1.450 +
   1.451 +fun add_prems (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thms) =
   1.452 +  mk_mss (rules, congs, procs, bounds, thms @ prems, mk_rews, termless);
   1.453 +
   1.454 +fun prems_of_mss (Mss {prems, ...}) = prems;
   1.455 +
   1.456 +
   1.457 +(* mk_rews *)
   1.458 +
   1.459 +fun set_mk_rews
   1.460 +  (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, mk) =
   1.461 +    mk_mss (rules, congs, procs, bounds, prems,
   1.462 +            {mk=mk, mk_sym= #mk_sym mk_rews, mk_eq_True= #mk_eq_True mk_rews},
   1.463 +            termless);
   1.464 +
   1.465 +fun set_mk_sym
   1.466 +  (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, mk_sym) =
   1.467 +    mk_mss (rules, congs, procs, bounds, prems,
   1.468 +            {mk= #mk mk_rews, mk_sym= mk_sym, mk_eq_True= #mk_eq_True mk_rews},
   1.469 +            termless);
   1.470 +
   1.471 +fun set_mk_eq_True
   1.472 +  (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, mk_eq_True) =
   1.473 +    mk_mss (rules, congs, procs, bounds, prems,
   1.474 +            {mk= #mk mk_rews, mk_sym= #mk_sym mk_rews, mk_eq_True= mk_eq_True},
   1.475 +            termless);
   1.476 +
   1.477 +(* termless *)
   1.478 +
   1.479 +fun set_termless
   1.480 +  (Mss {rules, congs, procs, bounds, prems, mk_rews, termless = _}, termless) =
   1.481 +    mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless);
   1.482 +
   1.483 +
   1.484 +
   1.485 +(** rewriting **)
   1.486 +
   1.487 +(*
   1.488 +  Uses conversions, see:
   1.489 +    L C Paulson, A higher-order implementation of rewriting,
   1.490 +    Science of Computer Programming 3 (1983), pages 119-149.
   1.491 +*)
   1.492 +
   1.493 +type prover = meta_simpset -> thm -> thm option;
   1.494 +type termrec = (Sign.sg_ref * term list) * term;
   1.495 +type conv = meta_simpset -> termrec -> termrec;
   1.496 +
   1.497 +val dest_eq = Drule.dest_equals o cprop_of;
   1.498 +val lhs_of = fst o dest_eq;
   1.499 +val rhs_of = snd o dest_eq;
   1.500 +
   1.501 +fun beta_eta_conversion t =
   1.502 +  let val thm = beta_conversion true t;
   1.503 +  in transitive thm (eta_conversion (rhs_of thm)) end;
   1.504 +
   1.505 +fun check_conv msg thm thm' =
   1.506 +  let
   1.507 +    val thm'' = transitive thm (transitive
   1.508 +      (symmetric (beta_eta_conversion (lhs_of thm'))) thm')
   1.509 +  in (if msg then trace_thm false "SUCCEEDED" thm' else (); Some thm'') end
   1.510 +  handle THM _ =>
   1.511 +    let val {sign, prop = _ $ _ $ prop0, ...} = rep_thm thm;
   1.512 +    in
   1.513 +      (trace_thm false "Proved wrong thm (Check subgoaler?)" thm';
   1.514 +       trace_term false "Should have proved:" sign prop0;
   1.515 +       None)
   1.516 +    end;
   1.517 +
   1.518 +
   1.519 +(* mk_procrule *)
   1.520 +
   1.521 +fun mk_procrule thm =
   1.522 +  let val (_,prems,lhs,elhs,rhs,_) = decomp_simp thm
   1.523 +  in if rewrite_rule_extra_vars prems lhs rhs
   1.524 +     then (prthm true "Extra vars on rhs:" thm; [])
   1.525 +     else [mk_rrule2{thm=thm, lhs=lhs, elhs=elhs, perm=false}]
   1.526 +  end;
   1.527 +
   1.528 +
   1.529 +(* conversion to apply the meta simpset to a term *)
   1.530 +
   1.531 +(* Since the rewriting strategy is bottom-up, we avoid re-normalizing already
   1.532 +   normalized terms by carrying around the rhs of the rewrite rule just
   1.533 +   applied. This is called the `skeleton'. It is decomposed in parallel
   1.534 +   with the term. Once a Var is encountered, the corresponding term is
   1.535 +   already in normal form.
   1.536 +   skel0 is a dummy skeleton that is to enforce complete normalization.
   1.537 +*)
   1.538 +val skel0 = Bound 0;
   1.539 +
   1.540 +(* Use rhs as skeleton only if the lhs does not contain unnormalized bits.
   1.541 +   The latter may happen iff there are weak congruence rules for constants
   1.542 +   in the lhs.
   1.543 +*)
   1.544 +fun uncond_skel((_,weak),(lhs,rhs)) =
   1.545 +  if null weak then rhs (* optimization *)
   1.546 +  else if exists_Const (fn (c,_) => c mem weak) lhs then skel0
   1.547 +       else rhs;
   1.548 +
   1.549 +(* Behaves like unconditional rule if rhs does not contain vars not in the lhs.
   1.550 +   Otherwise those vars may become instantiated with unnormalized terms
   1.551 +   while the premises are solved.
   1.552 +*)
   1.553 +fun cond_skel(args as (congs,(lhs,rhs))) =
   1.554 +  if term_varnames rhs subset term_varnames lhs then uncond_skel(args)
   1.555 +  else skel0;
   1.556 +
   1.557 +(*
   1.558 +  we try in order:
   1.559 +    (1) beta reduction
   1.560 +    (2) unconditional rewrite rules
   1.561 +    (3) conditional rewrite rules
   1.562 +    (4) simplification procedures
   1.563 +
   1.564 +  IMPORTANT: rewrite rules must not introduce new Vars or TVars!
   1.565 +
   1.566 +*)
   1.567 +
   1.568 +fun rewritec (prover, signt, maxt)
   1.569 +             (mss as Mss{rules, procs, termless, prems, congs, ...}) t =
   1.570 +  let
   1.571 +    val eta_thm = Thm.eta_conversion t;
   1.572 +    val eta_t' = rhs_of eta_thm;
   1.573 +    val eta_t = term_of eta_t';
   1.574 +    val tsigt = Sign.tsig_of signt;
   1.575 +    fun rew {thm, lhs, elhs, fo, perm} =
   1.576 +      let
   1.577 +        val {sign, prop, maxidx, ...} = rep_thm thm;
   1.578 +        val _ = if Sign.subsig (sign, signt) then ()
   1.579 +                else (prthm true "Ignoring rewrite rule from different theory:" thm;
   1.580 +                      raise Pattern.MATCH);
   1.581 +        val (rthm, elhs') = if maxt = ~1 then (thm, elhs)
   1.582 +          else (Thm.incr_indexes (maxt+1) thm, Thm.cterm_incr_indexes (maxt+1) elhs);
   1.583 +        val insts = if fo then Thm.cterm_first_order_match (elhs', eta_t')
   1.584 +                          else Thm.cterm_match (elhs', eta_t');
   1.585 +        val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
   1.586 +        val prop' = #prop (rep_thm thm');
   1.587 +        val unconditional = (Logic.count_prems (prop',0) = 0);
   1.588 +        val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
   1.589 +      in
   1.590 +        if perm andalso not (termless (rhs', lhs')) then None
   1.591 +        else
   1.592 +          (trace_thm false "Applying instance of rewrite rule:" thm;
   1.593 +           if unconditional
   1.594 +           then
   1.595 +             (trace_thm false "Rewriting:" thm';
   1.596 +              let val lr = Logic.dest_equals prop;
   1.597 +                  val Some thm'' = check_conv false eta_thm thm'
   1.598 +              in Some (thm'', uncond_skel (congs, lr)) end)
   1.599 +           else
   1.600 +             (trace_thm false "Trying to rewrite:" thm';
   1.601 +              case prover mss thm' of
   1.602 +                None       => (trace_thm false "FAILED" thm'; None)
   1.603 +              | Some thm2 =>
   1.604 +                  (case check_conv true eta_thm thm2 of
   1.605 +                     None => None |
   1.606 +                     Some thm2' =>
   1.607 +                       let val concl = Logic.strip_imp_concl prop
   1.608 +                           val lr = Logic.dest_equals concl
   1.609 +                       in Some (thm2', cond_skel (congs, lr)) end)))
   1.610 +      end
   1.611 +
   1.612 +    fun rews [] = None
   1.613 +      | rews (rrule :: rrules) =
   1.614 +          let val opt = rew rrule handle Pattern.MATCH => None
   1.615 +          in case opt of None => rews rrules | some => some end;
   1.616 +
   1.617 +    fun sort_rrules rrs = let
   1.618 +      fun is_simple({thm, ...}:rrule) = case #prop (rep_thm thm) of 
   1.619 +                                      Const("==",_) $ _ $ _ => true
   1.620 +                                      | _                   => false 
   1.621 +      fun sort []        (re1,re2) = re1 @ re2
   1.622 +        | sort (rr::rrs) (re1,re2) = if is_simple rr 
   1.623 +                                     then sort rrs (rr::re1,re2)
   1.624 +                                     else sort rrs (re1,rr::re2)
   1.625 +    in sort rrs ([],[]) end
   1.626 +
   1.627 +    fun proc_rews ([]:simproc list) = None
   1.628 +      | proc_rews ({name, proc, lhs, ...} :: ps) =
   1.629 +          if Pattern.matches tsigt (term_of lhs, term_of t) then
   1.630 +            (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
   1.631 +             case proc signt prems eta_t of
   1.632 +               None => (debug false "FAILED"; proc_rews ps)
   1.633 +             | Some raw_thm =>
   1.634 +                 (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
   1.635 +                  (case rews (mk_procrule raw_thm) of
   1.636 +                    None => (trace false "IGNORED"; proc_rews ps)
   1.637 +                  | some => some)))
   1.638 +          else proc_rews ps;
   1.639 +  in case eta_t of
   1.640 +       Abs _ $ _ => Some (transitive eta_thm
   1.641 +         (beta_conversion false (rhs_of eta_thm)), skel0)
   1.642 +     | _ => (case rews (sort_rrules (Net.match_term rules eta_t)) of
   1.643 +               None => proc_rews (Net.match_term procs eta_t)
   1.644 +             | some => some)
   1.645 +  end;
   1.646 +
   1.647 +
   1.648 +(* conversion to apply a congruence rule to a term *)
   1.649 +
   1.650 +fun congc (prover,signt,maxt) {thm=cong,lhs=lhs} t =
   1.651 +  let val {sign, ...} = rep_thm cong
   1.652 +      val _ = if Sign.subsig (sign, signt) then ()
   1.653 +                 else error("Congruence rule from different theory")
   1.654 +      val rthm = if maxt = ~1 then cong else Thm.incr_indexes (maxt+1) cong;
   1.655 +      val rlhs = fst (Drule.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
   1.656 +      val insts = Thm.cterm_match (rlhs, t)
   1.657 +      (* Pattern.match can raise Pattern.MATCH;
   1.658 +         is handled when congc is called *)
   1.659 +      val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
   1.660 +      val unit = trace_thm false "Applying congruence rule:" thm';
   1.661 +      fun err (msg, thm) = (prthm false msg thm; error "Failed congruence proof!")
   1.662 +  in case prover thm' of
   1.663 +       None => err ("Could not prove", thm')
   1.664 +     | Some thm2 => (case check_conv true (beta_eta_conversion t) thm2 of
   1.665 +          None => err ("Should not have proved", thm2)
   1.666 +        | Some thm2' => thm2')
   1.667 +  end;
   1.668 +
   1.669 +val (cA, (cB, cC)) =
   1.670 +  apsnd dest_equals (dest_implies (hd (cprems_of Drule.imp_cong)));
   1.671 +
   1.672 +fun transitive' thm1 None = Some thm1
   1.673 +  | transitive' thm1 (Some thm2) = Some (transitive thm1 thm2);
   1.674 +
   1.675 +fun bottomc ((simprem,useprem,mutsimp), prover, sign, maxidx) =
   1.676 +  let
   1.677 +    fun botc skel mss t =
   1.678 +          if is_Var skel then None
   1.679 +          else
   1.680 +          (case subc skel mss t of
   1.681 +             some as Some thm1 =>
   1.682 +               (case rewritec (prover, sign, maxidx) mss (rhs_of thm1) of
   1.683 +                  Some (thm2, skel2) =>
   1.684 +                    transitive' (transitive thm1 thm2)
   1.685 +                      (botc skel2 mss (rhs_of thm2))
   1.686 +                | None => some)
   1.687 +           | None =>
   1.688 +               (case rewritec (prover, sign, maxidx) mss t of
   1.689 +                  Some (thm2, skel2) => transitive' thm2
   1.690 +                    (botc skel2 mss (rhs_of thm2))
   1.691 +                | None => None))
   1.692 +
   1.693 +    and try_botc mss t =
   1.694 +          (case botc skel0 mss t of
   1.695 +             Some trec1 => trec1 | None => (reflexive t))
   1.696 +
   1.697 +    and subc skel
   1.698 +          (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless}) t0 =
   1.699 +       (case term_of t0 of
   1.700 +           Abs (a, T, t) =>
   1.701 +             let val b = variant bounds a
   1.702 +                 val (v, t') = dest_abs (Some ("." ^ b)) t0
   1.703 +                 val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless)
   1.704 +                 val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0
   1.705 +             in case botc skel' mss' t' of
   1.706 +                  Some thm => Some (abstract_rule a v thm)
   1.707 +                | None => None
   1.708 +             end
   1.709 +         | t $ _ => (case t of
   1.710 +             Const ("==>", _) $ _  =>
   1.711 +               let val (s, u) = Drule.dest_implies t0
   1.712 +               in impc (s, u, mss) end
   1.713 +           | Abs _ =>
   1.714 +               let val thm = beta_conversion false t0
   1.715 +               in case subc skel0 mss (rhs_of thm) of
   1.716 +                    None => Some thm
   1.717 +                  | Some thm' => Some (transitive thm thm')
   1.718 +               end
   1.719 +           | _  =>
   1.720 +               let fun appc () =
   1.721 +                     let
   1.722 +                       val (tskel, uskel) = case skel of
   1.723 +                           tskel $ uskel => (tskel, uskel)
   1.724 +                         | _ => (skel0, skel0);
   1.725 +                       val (ct, cu) = dest_comb t0
   1.726 +                     in
   1.727 +                     (case botc tskel mss ct of
   1.728 +                        Some thm1 =>
   1.729 +                          (case botc uskel mss cu of
   1.730 +                             Some thm2 => Some (combination thm1 thm2)
   1.731 +                           | None => Some (combination thm1 (reflexive cu)))
   1.732 +                      | None =>
   1.733 +                          (case botc uskel mss cu of
   1.734 +                             Some thm1 => Some (combination (reflexive ct) thm1)
   1.735 +                           | None => None))
   1.736 +                     end
   1.737 +                   val (h, ts) = strip_comb t
   1.738 +               in case h of
   1.739 +                    Const(a, _) =>
   1.740 +                      (case assoc_string (fst congs, a) of
   1.741 +                         None => appc ()
   1.742 +                       | Some cong =>
   1.743 +(* post processing: some partial applications h t1 ... tj, j <= length ts,
   1.744 +   may be a redex. Example: map (%x.x) = (%xs.xs) wrt map_cong *)
   1.745 +                          (let
   1.746 +                             val thm = congc (prover mss, sign, maxidx) cong t0;
   1.747 +                             val t = rhs_of thm;
   1.748 +                             val (cl, cr) = dest_comb t
   1.749 +                             val dVar = Var(("", 0), dummyT)
   1.750 +                             val skel =
   1.751 +                               list_comb (h, replicate (length ts) dVar)
   1.752 +                           in case botc skel mss cl of
   1.753 +                                None => Some thm
   1.754 +                              | Some thm' => Some (transitive thm
   1.755 +                                  (combination thm' (reflexive cr)))
   1.756 +                           end handle TERM _ => error "congc result"
   1.757 +                                    | Pattern.MATCH => appc ()))
   1.758 +                  | _ => appc ()
   1.759 +               end)
   1.760 +         | _ => None)
   1.761 +
   1.762 +    and impc args =
   1.763 +      if mutsimp
   1.764 +      then let val (prem, conc, mss) = args
   1.765 +           in apsome snd (mut_impc ([], prem, conc, mss)) end
   1.766 +      else nonmut_impc args
   1.767 +
   1.768 +    and mut_impc (prems, prem, conc, mss) = (case botc skel0 mss prem of
   1.769 +        None => mut_impc1 (prems, prem, conc, mss)
   1.770 +      | Some thm1 =>
   1.771 +          let val prem1 = rhs_of thm1
   1.772 +          in (case mut_impc1 (prems, prem1, conc, mss) of
   1.773 +              None => Some (None,
   1.774 +                combination (combination refl_implies thm1) (reflexive conc))
   1.775 +            | Some (x, thm2) => Some (x, transitive (combination (combination
   1.776 +                refl_implies thm1) (reflexive conc)) thm2))
   1.777 +          end)
   1.778 +
   1.779 +    and mut_impc1 (prems, prem1, conc, mss) =
   1.780 +      let
   1.781 +        fun uncond ({thm, lhs, elhs, perm}) =
   1.782 +          if Thm.no_prems thm then Some lhs else None
   1.783 +
   1.784 +        val (lhss1, mss1) =
   1.785 +          if maxidx_of_term (term_of prem1) <> ~1
   1.786 +          then (trace_cterm true
   1.787 +            "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem1;
   1.788 +                ([],mss))
   1.789 +          else let val thm = assume prem1
   1.790 +                   val rrules1 = extract_safe_rrules (mss, thm)
   1.791 +                   val lhss1 = mapfilter uncond rrules1
   1.792 +                   val mss1 = foldl insert_rrule (add_prems (mss, [thm]), rrules1)
   1.793 +               in (lhss1, mss1) end
   1.794 +
   1.795 +        fun disch1 thm =
   1.796 +          let val (cB', cC') = dest_eq thm
   1.797 +          in
   1.798 +            implies_elim (Thm.instantiate
   1.799 +              ([], [(cA, prem1), (cB, cB'), (cC, cC')]) Drule.imp_cong)
   1.800 +              (implies_intr prem1 thm)
   1.801 +          end
   1.802 +
   1.803 +        fun rebuild None = (case rewritec (prover, sign, maxidx) mss
   1.804 +            (mk_implies (prem1, conc)) of
   1.805 +              None => None
   1.806 +            | Some (thm, _) => Some (None, thm))
   1.807 +          | rebuild (Some thm2) =
   1.808 +            let val thm = disch1 thm2
   1.809 +            in (case rewritec (prover, sign, maxidx) mss (rhs_of thm) of
   1.810 +                 None => Some (None, thm)
   1.811 +               | Some (thm', _) =>
   1.812 +                   let val (prem, conc) = Drule.dest_implies (rhs_of thm')
   1.813 +                   in (case mut_impc (prems, prem, conc, mss) of
   1.814 +                       None => Some (None, transitive thm thm')
   1.815 +                     | Some (x, thm'') =>
   1.816 +                         Some (x, transitive (transitive thm thm') thm''))
   1.817 +                   end handle TERM _ => Some (None, transitive thm thm'))
   1.818 +            end
   1.819 +
   1.820 +        fun simpconc () =
   1.821 +          let val (s, t) = Drule.dest_implies conc
   1.822 +          in case mut_impc (prems @ [prem1], s, t, mss1) of
   1.823 +               None => rebuild None
   1.824 +             | Some (Some i, thm2) =>
   1.825 +                  let
   1.826 +                    val (prem, cC') = Drule.dest_implies (rhs_of thm2);
   1.827 +                    val thm2' = transitive (disch1 thm2) (Thm.instantiate
   1.828 +                      ([], [(cA, prem1), (cB, prem), (cC, cC')])
   1.829 +                      Drule.swap_prems_eq)
   1.830 +                  in if i=0 then apsome (apsnd (transitive thm2'))
   1.831 +                       (mut_impc1 (prems, prem, mk_implies (prem1, cC'), mss))
   1.832 +                     else Some (Some (i-1), thm2')
   1.833 +                  end
   1.834 +             | Some (None, thm) => rebuild (Some thm)
   1.835 +          end handle TERM _ => rebuild (botc skel0 mss1 conc)
   1.836 +
   1.837 +      in
   1.838 +        let
   1.839 +          val tsig = Sign.tsig_of sign
   1.840 +          fun reducible t =
   1.841 +            exists (fn lhs => Pattern.matches_subterm tsig (lhs, term_of t)) lhss1;
   1.842 +        in case dropwhile (not o reducible) prems of
   1.843 +            [] => simpconc ()
   1.844 +          | red::rest => (trace_cterm false "Can now reduce premise:" red;
   1.845 +              Some (Some (length rest), reflexive (mk_implies (prem1, conc))))
   1.846 +        end
   1.847 +      end
   1.848 +
   1.849 +     (* legacy code - only for backwards compatibility *)
   1.850 +     and nonmut_impc (prem, conc, mss) =
   1.851 +       let val thm1 = if simprem then botc skel0 mss prem else None;
   1.852 +           val prem1 = if_none (apsome rhs_of thm1) prem;
   1.853 +           val maxidx1 = maxidx_of_term (term_of prem1)
   1.854 +           val mss1 =
   1.855 +             if not useprem then mss else
   1.856 +             if maxidx1 <> ~1
   1.857 +             then (trace_cterm true
   1.858 +               "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem1;
   1.859 +                   mss)
   1.860 +             else let val thm = assume prem1
   1.861 +                  in add_safe_simp (add_prems (mss, [thm]), thm) end
   1.862 +       in (case botc skel0 mss1 conc of
   1.863 +           None => (case thm1 of
   1.864 +               None => None
   1.865 +             | Some thm1' => Some (combination
   1.866 +                 (combination refl_implies thm1') (reflexive conc)))
   1.867 +         | Some thm2 =>
   1.868 +           let
   1.869 +             val conc2 = rhs_of thm2;
   1.870 +             val thm2' = implies_elim (Thm.instantiate
   1.871 +               ([], [(cA, prem1), (cB, conc), (cC, conc2)]) Drule.imp_cong)
   1.872 +               (implies_intr prem1 thm2)
   1.873 +           in (case thm1 of
   1.874 +               None => Some thm2'
   1.875 +             | Some thm1' => Some (transitive (combination
   1.876 +                 (combination refl_implies thm1') (reflexive conc)) thm2'))
   1.877 +           end)
   1.878 +       end
   1.879 +
   1.880 + in try_botc end;
   1.881 +
   1.882 +
   1.883 +(*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***)
   1.884 +
   1.885 +(*
   1.886 +  Parameters:
   1.887 +    mode = (simplify A,
   1.888 +            use A in simplifying B,
   1.889 +            use prems of B (if B is again a meta-impl.) to simplify A)
   1.890 +           when simplifying A ==> B
   1.891 +    mss: contains equality theorems of the form [|p1,...|] ==> t==u
   1.892 +    prover: how to solve premises in conditional rewrites and congruences
   1.893 +*)
   1.894 +
   1.895 +(* FIXME: check that #bounds(mss) does not "occur" in ct already *)
   1.896 +
   1.897 +fun rewrite_cterm mode prover mss ct =
   1.898 +  let val {sign, t, maxidx, ...} = rep_cterm ct
   1.899 +  in bottomc (mode, prover, sign, maxidx) mss ct end
   1.900 +  handle THM (s, _, thms) =>
   1.901 +    error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
   1.902 +      Pretty.string_of (pretty_thms thms));
   1.903 +
   1.904 +(*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*)
   1.905 +(*Do not rewrite flex-flex pairs*)
   1.906 +fun goals_conv pred cv =
   1.907 +  let fun gconv i ct =
   1.908 +        let val (A,B) = Drule.dest_implies ct
   1.909 +            val (thA,j) = case term_of A of
   1.910 +                  Const("=?=",_)$_$_ => (reflexive A, i)
   1.911 +                | _ => (if pred i then cv A else reflexive A, i+1)
   1.912 +        in  combination (combination refl_implies thA) (gconv j B) end
   1.913 +        handle TERM _ => reflexive ct
   1.914 +  in gconv 1 end;
   1.915 +
   1.916 +(*Use a conversion to transform a theorem*)
   1.917 +fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
   1.918 +
   1.919 +(*Rewrite a theorem*)
   1.920 +fun rewrite_rule_aux _ [] = (fn th => th)
   1.921 +  | rewrite_rule_aux prover thms =
   1.922 +      fconv_rule (rewrite_cterm (true,false,false) prover (mss_of thms));
   1.923 +
   1.924 +fun rewrite_thm mode prover mss = fconv_rule (rewrite_cterm mode prover mss);
   1.925 +
   1.926 +(*Rewrite the subgoals of a proof state (represented by a theorem) *)
   1.927 +fun rewrite_goals_rule_aux _ []   th = th
   1.928 +  | rewrite_goals_rule_aux prover thms th =
   1.929 +      fconv_rule (goals_conv (K true) (rewrite_cterm (true, true, false) prover
   1.930 +        (mss_of thms))) th;
   1.931 +
   1.932 +(*Rewrite the subgoal of a proof state (represented by a theorem) *)
   1.933 +fun rewrite_goal_rule mode prover mss i thm =
   1.934 +  if 0 < i  andalso  i <= nprems_of thm
   1.935 +  then fconv_rule (goals_conv (fn j => j=i) (rewrite_cterm mode prover mss)) thm
   1.936 +  else raise THM("rewrite_goal_rule",i,[thm]);
   1.937 +
   1.938 +end;
   1.939 +
   1.940 +open MetaSimplifier;