src/Pure/raw_simplifier.ML
changeset 74227 fdcc7e8f95ea
parent 71403 43c2355648d2
child 74232 1091880266e5
equal deleted inserted replaced
74222:bf595bfbdc98 74227:fdcc7e8f95ea
   159 all its Vars? Better: a dynamic check each time a rule is applied.
   159 all its Vars? Better: a dynamic check each time a rule is applied.
   160 *)
   160 *)
   161 fun rewrite_rule_extra_vars prems elhs erhs =
   161 fun rewrite_rule_extra_vars prems elhs erhs =
   162   let
   162   let
   163     val elhss = elhs :: prems;
   163     val elhss = elhs :: prems;
   164     val tvars = fold Term.add_tvars elhss [];
   164     val tvars = fold Term_Subst.add_tvars elhss Term_Subst.TVars.empty;
   165     val vars = fold Term.add_vars elhss [];
   165     val vars = fold Term_Subst.add_vars elhss Term_Subst.Vars.empty;
   166   in
   166   in
   167     erhs |> Term.exists_type (Term.exists_subtype
   167     erhs |> Term.exists_type (Term.exists_subtype
   168       (fn TVar v => not (member (op =) tvars v) | _ => false)) orelse
   168       (fn TVar v => not (Term_Subst.TVars.defined tvars v) | _ => false)) orelse
   169     erhs |> Term.exists_subterm
   169     erhs |> Term.exists_subterm
   170       (fn Var v => not (member (op =) vars v) | _ => false)
   170       (fn Var v => not (Term_Subst.Vars.defined vars v) | _ => false)
   171   end;
   171   end;
   172 
   172 
   173 fun rrule_extra_vars elhs thm =
   173 fun rrule_extra_vars elhs thm =
   174   rewrite_rule_extra_vars [] (Thm.term_of elhs) (Thm.full_prop_of thm);
   174   rewrite_rule_extra_vars [] (Thm.term_of elhs) (Thm.full_prop_of thm);
   175 
   175 
   472     in (rules', prems, depth) end)
   472     in (rules', prems, depth) end)
   473   handle Net.INSERT =>
   473   handle Net.INSERT =>
   474     (cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm));
   474     (cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm));
   475       ctxt));
   475       ctxt));
   476 
   476 
       
   477 fun vars_set t = Term_Subst.add_vars t Term_Subst.Vars.empty;
       
   478 
   477 local
   479 local
   478 
   480 
   479 fun vperm (Var _, Var _) = true
   481 fun vperm (Var _, Var _) = true
   480   | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
   482   | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
   481   | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
   483   | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
   482   | vperm (t, u) = (t = u);
   484   | vperm (t, u) = (t = u);
   483 
   485 
   484 fun var_perm (t, u) =
   486 fun var_perm (t, u) = vperm (t, u) andalso Term_Subst.Vars.eq_set (apply2 vars_set (t, u));
   485   vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
       
   486 
   487 
   487 in
   488 in
   488 
   489 
   489 fun decomp_simp thm =
   490 fun decomp_simp thm =
   490   let
   491   let
   943 (*Behaves like unconditional rule if rhs does not contain vars not in the lhs.
   944 (*Behaves like unconditional rule if rhs does not contain vars not in the lhs.
   944   Otherwise those vars may become instantiated with unnormalized terms
   945   Otherwise those vars may become instantiated with unnormalized terms
   945   while the premises are solved.*)
   946   while the premises are solved.*)
   946 
   947 
   947 fun cond_skel (args as (_, (lhs, rhs))) =
   948 fun cond_skel (args as (_, (lhs, rhs))) =
   948   if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args
   949   if Term_Subst.Vars.subset (vars_set rhs, vars_set lhs) then uncond_skel args
   949   else skel0;
   950   else skel0;
   950 
   951 
   951 (*
   952 (*
   952   Rewriting -- we try in order:
   953   Rewriting -- we try in order:
   953     (1) beta reduction
   954     (1) beta reduction