Added functions to test equivalence between clauses.
authormengj
Thu Dec 15 05:47:26 2005 +0100 (2005-12-15)
changeset 18409080094128a09
parent 18408 07da804d1119
child 18410 73bb08d2823c
Added functions to test equivalence between clauses.
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_clause.ML	Wed Dec 14 22:05:22 2005 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Thu Dec 15 05:47:26 2005 +0100
     1.3 @@ -537,6 +537,107 @@
     1.4  
     1.5  fun sort_lits lits = sort literal_ord lits;
     1.6  
     1.7 +(********** clause equivalence ******************)
     1.8 +
     1.9 +fun check_var_pairs (x,y) [] = 0 
    1.10 +  | check_var_pairs (x,y) ((u,v)::w) =
    1.11 +    if (x,y) = (u,v) then 1 
    1.12 +    else
    1.13 +	if (x = u) orelse (y = v) then 2 (*conflict*)
    1.14 +	else check_var_pairs (x,y) w;
    1.15 +
    1.16 +
    1.17 +fun type_eq (AtomV(v1),AtomV(v2)) (vars,tvars) =
    1.18 +    (case check_var_pairs (v1,v2) tvars of 0 => (true,(vars,(v1,v2)::tvars))
    1.19 +					 | 1 => (true,(vars,tvars))
    1.20 +					 | 2 => (false,(vars,tvars)))
    1.21 +  | type_eq (AtomV(_),_) vtvars = (false,vtvars)
    1.22 +  | type_eq (AtomF(f1),AtomF(f2)) vtvars = (f1=f2,vtvars)
    1.23 +  | type_eq (AtomF(_),_) vtvars = (false,vtvars)
    1.24 +  | type_eq (Comp(con1,args1),Comp(con2,args2)) vtvars =
    1.25 +    let val (eq1,vtvars1) = 
    1.26 +	    if (con1 = con2) then types_eq (args1,args2) vtvars
    1.27 +	    else (false,vtvars)
    1.28 +    in
    1.29 +	(eq1,vtvars1)
    1.30 +    end
    1.31 +  | type_eq (Comp(_,_),_) vtvars = (false,vtvars)
    1.32 +
    1.33 +and
    1.34 +
    1.35 +types_eq ([],[]) vtvars = (true,vtvars)
    1.36 +| types_eq (tp1::tps1,tp2::tps2) vtvars =
    1.37 +  let val (eq1,vtvars1) = type_eq (tp1,tp2) vtvars
    1.38 +      val (eq2,vtvars2) = if eq1 then types_eq (tps1,tps2) vtvars1
    1.39 +			  else (eq1,vtvars1)
    1.40 +  in
    1.41 +      (eq2,vtvars2)
    1.42 +  end;
    1.43 +
    1.44 +
    1.45 +fun term_eq (UVar(v1,tp1),UVar(v2,tp2)) (vars,tvars) =
    1.46 +    (case check_var_pairs (v1,v2) vars of 0 => type_eq (tp1,tp2) (((v1,v2)::vars),tvars)
    1.47 +					| 1 => type_eq (tp1,tp2) (vars,tvars)
    1.48 +					| 2 => (false,(vars,tvars)))
    1.49 +  | term_eq (UVar(_,_),_) vtvars = (false,vtvars)
    1.50 +  | term_eq (Fun(f1,tps1,tms1),Fun(f2,tps2,tms2)) vtvars =
    1.51 +    let val (eq1,vtvars1) = 
    1.52 +	    if (f1 = f2) then terms_eq (tms1,tms2) vtvars
    1.53 +	    else (false,vtvars)
    1.54 +	val (eq2,vtvars2) =
    1.55 +	    if eq1 then types_eq (tps1,tps2) vtvars1
    1.56 +	    else (eq1,vtvars1)
    1.57 +    in
    1.58 +	(eq2,vtvars2)
    1.59 +    end
    1.60 +  | term_eq (Fun(_,_,_),_) vtvars = (false,vtvars)
    1.61 +
    1.62 +and
    1.63 +
    1.64 +terms_eq ([],[]) vtvars = (true,vtvars)
    1.65 +| terms_eq (tm1::tms1,tm2::tms2) vtvars =
    1.66 +  let val (eq1,vtvars1) = term_eq (tm1,tm2) vtvars
    1.67 +      val (eq2,vtvars2) = if eq1 then terms_eq (tms1,tms2) vtvars1
    1.68 +				 else (eq1,vtvars1)
    1.69 +  in
    1.70 +      (eq2,vtvars2)
    1.71 +  end;
    1.72 +					     
    1.73 +
    1.74 +fun pred_eq (Predicate(predname1,tps1,tms1),Predicate(predname2,tps2,tms2)) vtvars =
    1.75 +    let val (eq1,vtvars1) = 
    1.76 +	    if (predname1 = predname2) then terms_eq (tms1,tms2) vtvars
    1.77 +	    else (false,vtvars)
    1.78 +	val (eq2,vtvars2) = 
    1.79 +	    if eq1 then types_eq (tps1,tps2) vtvars1
    1.80 +	    else (eq1,vtvars1)
    1.81 +    in
    1.82 +	(eq2,vtvars2)
    1.83 +    end;
    1.84 +					      
    1.85 +
    1.86 +fun lit_eq (Literal(pol1,pred1,_),Literal(pol2,pred2,_)) vtvars =
    1.87 +    if (pol1 = pol2) then pred_eq (pred1,pred2) vtvars
    1.88 +    else (false,vtvars);
    1.89 +
    1.90 +(*must have the same number of literals*)
    1.91 +fun lits_eq ([],[]) vtvars = (true,vtvars)
    1.92 +  | lits_eq (l1::ls1,l2::ls2) vtvars = 
    1.93 +    let val (eq1,vtvars1) = lit_eq (l1,l2) vtvars
    1.94 +    in
    1.95 +	if eq1 then lits_eq (ls1,ls2) vtvars1
    1.96 +	else (false,vtvars1)
    1.97 +    end;
    1.98 +
    1.99 +
   1.100 +fun cls_eq (cls1,cls2) =
   1.101 +    let val lits1 = get_literals cls1
   1.102 +	val lits2 = get_literals cls2
   1.103 +    in
   1.104 +	(length lits1 = length lits2) andalso (fst (lits_eq (lits1,lits2) ([],[])))
   1.105 +    end;
   1.106 +
   1.107 +
   1.108  
   1.109  
   1.110  (* FIX: not sure what to do with these funcs *)