src/Pure/meta_simplifier.ML

 
 (** datatype simpset **)
 
 (* rewrite rules *)
 
-type rrule = {thm: thm, name: string, lhs: term, elhs: cterm, fo: bool, perm: bool};
-
-(*thm: the rewrite rule;
-  name: name of theorem from which rewrite rule was extracted;
-  lhs: the left-hand side;
-  elhs: the etac-contracted lhs;
-  fo: use first-order matching;
-  perm: the rewrite rule is permutative;
-
+type rrule =
+ {thm: thm,         (*the rewrite rule*)
+  name: string,     (*name of theorem from which rewrite rule was extracted*)
+  lhs: term,        (*the left-hand side*)
+  elhs: cterm,      (*the etac-contracted lhs*)
+  extra: bool,      (*extra variables outside of elhs*)
+  fo: bool,         (*use first-order matching*)
+  perm: bool};      (*the rewrite rule is permutative*)
+
+(*
 Remarks:
   - elhs is used for matching,
     lhs only for preservation of bound variable names;
   - fo is set iff
     either elhs is first-order (no Var is applied),
       in which case fo-matching is complete,
     or elhs is not a pattern,
-      in which case there is nothing better to do;*)
+      in which case there is nothing better to do;
+*)
 
 fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
   Drule.eq_thm_prop (thm1, thm2);
 
 

   else ();
 
 fun warn_thm a ss th = print_term true a ss (Thm.theory_of_thm th) (Thm.full_prop_of th);
 
 fun cond_warn_thm a (ss as Simpset ({context, ...}, _)) th =
-  if is_some context then () else warn_thm a ss th; 
+  if is_some context then () else warn_thm a ss th;
 
 end;
 
 
 (* print simpsets *)

       theory_context thy ss);
 
 
 (* maintain simp rules *)
 
+(* FIXME: it seems that the conditions on extra variables are too liberal if
+prems are nonempty: does solving the prems really guarantee instantiation of
+all its Vars? Better: a dynamic check each time a rule is applied.
+*)
+fun rewrite_rule_extra_vars prems elhs erhs =
+  let
+    val elhss = elhs :: prems;
+    val tvars = fold Term.add_tvars elhss [];
+    val vars = fold Term.add_vars elhss [];
+  in
+    erhs |> Term.exists_type (Term.exists_subtype
+      (fn TVar v => not (member (op =) tvars v) | _ => false)) orelse
+    erhs |> Term.exists_subterm
+      (fn Var v => not (member (op =) vars v) | _ => false)
+  end;
+
+fun rrule_extra_vars elhs thm =
+  rewrite_rule_extra_vars [] (term_of elhs) (Thm.full_prop_of thm);
+
 fun mk_rrule2 {thm, name, lhs, elhs, perm} =
   let
-    val fo = Pattern.first_order (term_of elhs) orelse not (Pattern.pattern (term_of elhs))
-  in {thm = thm, name = name, lhs = lhs, elhs = elhs, fo = fo, perm = perm} end;
+    val t = term_of elhs;
+    val fo = Pattern.first_order t orelse not (Pattern.pattern t);
+    val extra = rrule_extra_vars elhs thm;
+  in {thm = thm, name = name, lhs = lhs, elhs = elhs, extra = extra, fo = fo, perm = perm} end;
 
 fun del_rrule (rrule as {thm, elhs, ...}) ss =
   ss |> map_simpset1 (fn (rules, prems, bounds, context) =>
     (Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, bounds, context))
   handle Net.DELETE => (cond_warn_thm "Rewrite rule not in simpset:" ss thm; ss);
 
-fun insert_rrule (rrule as {thm, name, lhs, elhs, perm}) ss =
+fun insert_rrule (rrule as {thm, name, elhs, ...}) ss =
  (trace_named_thm "Adding rewrite rule" ss (thm, name);
   ss |> map_simpset1 (fn (rules, prems, bounds, context) =>
     let
       val rrule2 as {elhs, ...} = mk_rrule2 rrule;
       val rules' = Net.insert_term eq_rrule (term_of elhs, rrule2) rules;

   | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
   | vperm (t, u) = (t = u);
 
 fun var_perm (t, u) =
   vperm (t, u) andalso gen_eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
-
-(* FIXME: it seems that the conditions on extra variables are too liberal if
-prems are nonempty: does solving the prems really guarantee instantiation of
-all its Vars? Better: a dynamic check each time a rule is applied.
-*)
-fun rewrite_rule_extra_vars prems elhs erhs =
-  not (Term.add_vars erhs [] subset fold Term.add_vars (elhs :: prems) [])
-  orelse
-  not (Term.add_tvars erhs [] subset (fold Term.add_tvars (elhs :: prems) []));
 
 (*simple test for looping rewrite rules and stupid orientations*)
 fun default_reorient thy prems lhs rhs =
   rewrite_rule_extra_vars prems lhs rhs
     orelse

 
 fun mk_eq_True (Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
   (case mk_eq_True thm of
     NONE => []
   | SOME eq_True =>
-      let val (_, _, lhs, elhs, _, _) = decomp_simp eq_True
+      let
+        val (_, _, lhs, elhs, _, _) = decomp_simp eq_True;
+        val extra = rrule_extra_vars elhs eq_True;
       in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end);
 
 (*create the rewrite rule and possibly also the eq_True variant,
   in case there are extra vars on the rhs*)
 fun rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm2) =
   let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in
-    if Term.add_vars rhs [] subset Term.add_vars lhs [] andalso
-      Term.add_tvars rhs [] subset Term.add_tvars lhs [] then [rrule]
-    else mk_eq_True ss (thm2, name) @ [rrule]
+    if rewrite_rule_extra_vars [] lhs rhs then
+      mk_eq_True ss (thm2, name) @ [rrule]
+    else [rrule]
   end;
 
 fun mk_rrule ss (thm, name) =
   let val (_, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
     if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]

   let
     val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss;
     val eta_thm = Thm.eta_conversion t;
     val eta_t' = rhs_of eta_thm;
     val eta_t = term_of eta_t';
-    fun rew {thm, name, lhs, elhs, fo, perm} =
+    fun rew {thm, name, lhs, elhs, extra, fo, perm} =
       let
         val {thy, prop, maxidx, ...} = rep_thm thm;
-        val (rthm, elhs') = if maxt = ~1 then (thm, elhs)
+        val (rthm, elhs') =
+          if maxt = ~1 orelse not extra then (thm, elhs)
           else (Thm.incr_indexes (maxt+1) thm, Thm.cterm_incr_indexes (maxt+1) elhs);
         val insts = if fo then Thm.cterm_first_order_match (elhs', eta_t')
                           else Thm.cterm_match (elhs', eta_t');
         val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
         val prop' = Thm.prop_of thm';