added same_sg and same_thm
authorclasohm
Fri Sep 01 13:27:48 1995 +0200 (1995-09-01)
changeset 1241bfc93c86f0a1
parent 1240 0901441a7ebf
child 1242 b3f68a644380
added same_sg and same_thm
src/Pure/drule.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/drule.ML	Fri Sep 01 13:16:24 1995 +0200
     1.2 +++ b/src/Pure/drule.ML	Fri Sep 01 13:27:48 1995 +0200
     1.3 @@ -26,6 +26,7 @@
     1.4    val equal_abs_elim	: cterm  -> thm -> thm
     1.5    val equal_abs_elim_list: cterm list -> thm -> thm
     1.6    val eq_thm		: thm * thm -> bool
     1.7 +  val same_thm		: thm * thm -> bool
     1.8    val eq_thm_sg		: thm * thm -> bool
     1.9    val flexpair_abs_elim_list: cterm list -> thm -> thm
    1.10    val forall_intr_list	: cterm list -> thm -> thm
    1.11 @@ -648,6 +649,18 @@
    1.12          prop1 aconv prop2
    1.13      end;
    1.14  
    1.15 +(*equality of theorems using similarity of signatures,
    1.16 +  i.e. the theorems belong to the same theory but not necessarily to the same
    1.17 +  version of this theory*)
    1.18 +fun same_thm (th1,th2) =
    1.19 +    let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
    1.20 +        and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
    1.21 +    in  Sign.same_sg (sg1,sg2) andalso
    1.22 +        eq_set (shyps1, shyps2) andalso
    1.23 +        aconvs(hyps1,hyps2) andalso
    1.24 +        prop1 aconv prop2
    1.25 +    end;
    1.26 +
    1.27  (*Do the two theorems have the same signature?*)
    1.28  fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2));
    1.29  
     2.1 --- a/src/Pure/sign.ML	Fri Sep 01 13:16:24 1995 +0200
     2.2 +++ b/src/Pure/sign.ML	Fri Sep 01 13:27:48 1995 +0200
     2.3 @@ -20,6 +20,7 @@
     2.4         stamps: string ref list}
     2.5      val subsig: sg * sg -> bool
     2.6      val eq_sg: sg * sg -> bool
     2.7 +    val same_sg: sg * sg -> bool
     2.8      val is_draft: sg -> bool
     2.9      val const_type: sg -> string -> typ option
    2.10      val classes: sg -> class list
    2.11 @@ -107,6 +108,12 @@
    2.12  
    2.13  fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = eq_set (s1, s2);
    2.14  
    2.15 +(* test if same theory names are contained in signatures' stamps,
    2.16 +   i.e. if signatures belong to same theory but not necessarily to the same
    2.17 +   version of it*)
    2.18 +fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
    2.19 +  eq_set (pairself (map (op !)) (s1, s2));
    2.20 +
    2.21  
    2.22  (* consts *)
    2.23