396 | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t) |
396 | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t) |
397 | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2) |
397 | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2) |
398 | vperm (t, u) = (t = u); |
398 | vperm (t, u) = (t = u); |
399 |
399 |
400 fun var_perm (t, u) = |
400 fun var_perm (t, u) = |
401 vperm (t, u) andalso gen_eq_set (op =) (Term.add_vars t [], Term.add_vars u []); |
401 vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []); |
402 |
402 |
403 (*simple test for looping rewrite rules and stupid orientations*) |
403 (*simple test for looping rewrite rules and stupid orientations*) |
404 fun default_reorient thy prems lhs rhs = |
404 fun default_reorient thy prems lhs rhs = |
405 rewrite_rule_extra_vars prems lhs rhs |
405 rewrite_rule_extra_vars prems lhs rhs |
406 orelse |
406 orelse |
862 (*Behaves like unconditional rule if rhs does not contain vars not in the lhs. |
862 (*Behaves like unconditional rule if rhs does not contain vars not in the lhs. |
863 Otherwise those vars may become instantiated with unnormalized terms |
863 Otherwise those vars may become instantiated with unnormalized terms |
864 while the premises are solved.*) |
864 while the premises are solved.*) |
865 |
865 |
866 fun cond_skel (args as (_, (lhs, rhs))) = |
866 fun cond_skel (args as (_, (lhs, rhs))) = |
867 if gen_subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args |
867 if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args |
868 else skel0; |
868 else skel0; |
869 |
869 |
870 (* |
870 (* |
871 Rewriting -- we try in order: |
871 Rewriting -- we try in order: |
872 (1) beta reduction |
872 (1) beta reduction |