src/Pure/logic.ML
changeset 4679 24917efb31b5
parent 4667 6328d427a339
child 4693 2e47ea2c6109
     1.1 --- a/src/Pure/logic.ML	Wed Mar 04 13:15:05 1998 +0100
     1.2 +++ b/src/Pure/logic.ML	Wed Mar 04 13:16:05 1998 +0100
     1.3 @@ -26,9 +26,6 @@
     1.4    val list_flexpairs	: (term*term)list * term -> term
     1.5    val list_implies	: term list * term -> term
     1.6    val list_rename_params: string list * term -> term
     1.7 -  val rewrite_rule_extra_vars: term list -> term -> term -> string option
     1.8 -  val rewrite_rule_ok   : Sign.sg -> term list -> term -> term
     1.9 -                          -> string option * bool
    1.10    val mk_equals		: term * term -> term
    1.11    val mk_flexpair	: term * term -> term
    1.12    val mk_implies	: term * term -> term
    1.13 @@ -304,59 +301,4 @@
    1.14    | unvarify (f$t) = unvarify f $ unvarify t
    1.15    | unvarify t = t;
    1.16  
    1.17 -
    1.18 -
    1.19 -(** Test wellformedness of rewrite rules **)
    1.20 -
    1.21 -fun vperm (Var _, Var _) = true
    1.22 -  | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
    1.23 -  | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
    1.24 -  | vperm (t, u) = (t = u);
    1.25 -
    1.26 -fun var_perm (t, u) =
    1.27 -  vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
    1.28 -
    1.29 -(*simple test for looping rewrite*)
    1.30 -fun looptest sign prems lhs rhs =
    1.31 -   is_Var (head_of lhs)
    1.32 -  orelse
    1.33 -   (exists (apl (lhs, op occs)) (rhs :: prems))
    1.34 -  orelse
    1.35 -   (null prems andalso
    1.36 -    Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
    1.37 -(*  orelse
    1.38 -   (case lhs of
    1.39 -      (f as Free _) $ (Var _) => exists (fn p => f occs p) prems orelse
    1.40 -                                 (null prems andalso f occs rhs)
    1.41 -    | _ => false)*);
    1.42 -(*the condition "null prems" in the last cases is necessary because
    1.43 -  conditional rewrites with extra variables in the conditions may terminate
    1.44 -  although the rhs is an instance of the lhs. Example:
    1.45 -  ?m < ?n ==> f(?n) == f(?m)*)
    1.46 -(*FIXME: proper test: lhs does not match a subterm of a premise
    1.47 -                      and does not match a subterm of the rhs if null prems *)
    1.48 -
    1.49 -fun rewrite_rule_extra_vars prems elhs erhs =
    1.50 -  if not ((term_vars erhs) subset
    1.51 -          (union_term (term_vars elhs, List.concat(map term_vars prems))))
    1.52 -  then Some("extra Var(s) on rhs") else
    1.53 -  if not ((term_tvars erhs) subset
    1.54 -          (term_tvars elhs  union  List.concat(map term_tvars prems)))
    1.55 -  then Some("extra TVar(s) on rhs")
    1.56 -  else None;
    1.57 -
    1.58 -fun rewrite_rule_ok sign prems lhs rhs =
    1.59 -  let
    1.60 -    val elhs = Pattern.eta_contract lhs;
    1.61 -    val erhs = Pattern.eta_contract rhs;
    1.62 -    val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs)
    1.63 -               andalso not (is_Var elhs)
    1.64 -  in (case rewrite_rule_extra_vars prems elhs erhs of
    1.65 -        None => if not perm andalso looptest sign prems elhs erhs
    1.66 -                then Some("loops")
    1.67 -                else None
    1.68 -      | some => some
    1.69 -      ,perm)
    1.70 -  end;
    1.71 -
    1.72  end;