src/Pure/thm.ML
changeset 3994 0343230ec85c
parent 3971 b19d38604042
child 4018 09b77900af0f
     1.1 --- a/src/Pure/thm.ML	Fri Oct 24 17:14:41 1997 +0200
     1.2 +++ b/src/Pure/thm.ML	Fri Oct 24 17:15:59 1997 +0200
     1.3 @@ -86,6 +86,7 @@
     1.4    val crep_thm          : thm -> {sign: Sign.sg, der: deriv, maxidx: int,
     1.5                                    shyps: sort list, hyps: cterm list, 
     1.6                                    prop: cterm}
     1.7 +  val eq_thm		: thm * thm -> bool
     1.8    val sign_of_thm       : thm -> Sign.sg
     1.9    val transfer		: theory -> thm -> thm
    1.10    val tpairs_of         : thm -> (term * term) list
    1.11 @@ -108,7 +109,6 @@
    1.12    val implies_elim      : thm -> thm -> thm
    1.13    val forall_intr       : cterm -> thm -> thm
    1.14    val forall_elim       : cterm -> thm -> thm
    1.15 -  val flexpair_def      : thm
    1.16    val reflexive         : cterm -> thm
    1.17    val symmetric         : thm -> thm
    1.18    val transitive        : thm -> thm -> thm
    1.19 @@ -408,6 +408,18 @@
    1.20  (*errors involving theorems*)
    1.21  exception THM of string * int * thm list;
    1.22  
    1.23 +(*equality of theorems uses equality of signatures and the
    1.24 +  a-convertible test for terms*)
    1.25 +fun eq_thm (th1, th2) =
    1.26 +  let
    1.27 +    val {sign = sg1, shyps = shyps1, hyps = hyps1, prop = prop1, ...} = rep_thm th1;
    1.28 +    val {sign = sg2, shyps = shyps2, hyps = hyps2, prop = prop2, ...} = rep_thm th2;
    1.29 +  in
    1.30 +    Sign.eq_sg (sg1, sg2) andalso
    1.31 +    eq_set_sort (shyps1, shyps2) andalso
    1.32 +    aconvs (hyps1, hyps2) andalso
    1.33 +    prop1 aconv prop2
    1.34 +  end;
    1.35  
    1.36  fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref;
    1.37  
    1.38 @@ -565,11 +577,11 @@
    1.39  (*look up the named axiom in the theory*)
    1.40  fun get_axiom theory raw_name =
    1.41    let
    1.42 -    val name = Sign.intern (sign_of theory) Theory.thmK raw_name;
    1.43 +    val name = Sign.intern (sign_of theory) Theory.axiomK raw_name;
    1.44      fun get_ax [] = raise Match
    1.45        | get_ax (thy :: thys) =
    1.46 -          let val {sign, new_axioms, parents, ...} = rep_theory thy
    1.47 -          in case Symtab.lookup (new_axioms, name) of
    1.48 +          let val {sign, axioms, parents, ...} = rep_theory thy
    1.49 +          in case Symtab.lookup (axioms, name) of
    1.50                  Some t => fix_shyps [] []
    1.51                             (Thm {sign_ref = Sign.self_ref sign,
    1.52                                   der = infer_derivs (Axiom(theory,name), []),
    1.53 @@ -581,14 +593,14 @@
    1.54            end;
    1.55    in
    1.56      get_ax [theory] handle Match
    1.57 -      => raise THEORY ("get_axiom: no axiom " ^ quote name, [theory])
    1.58 +      => raise THEORY ("No axiom " ^ quote name, [theory])
    1.59    end;
    1.60  
    1.61  
    1.62  (*return additional axioms of this theory node*)
    1.63  fun axioms_of thy =
    1.64    map (fn (s, _) => (s, get_axiom thy s))
    1.65 -    (Symtab.dest (#new_axioms (rep_theory thy)));
    1.66 +    (Symtab.dest (#axioms (rep_theory thy)));
    1.67  
    1.68  (*Attach a label to a theorem to make proof objects more readable*)
    1.69  fun name_thm (name, th as Thm {sign_ref, der, maxidx, shyps, hyps, prop}) = 
    1.70 @@ -747,16 +759,6 @@
    1.71  
    1.72  (* Equality *)
    1.73  
    1.74 -(* Definition of the relation =?= *)
    1.75 -val flexpair_def = fix_shyps [] []
    1.76 -  (Thm{sign_ref= Sign.self_ref Sign.proto_pure, 
    1.77 -       der = Join(Axiom(Theory.proto_pure, "flexpair_def"), []),
    1.78 -       shyps = [], 
    1.79 -       hyps = [], 
    1.80 -       maxidx = 0,
    1.81 -       prop = term_of (read_cterm Sign.proto_pure
    1.82 -                       ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))});
    1.83 -
    1.84  (*The reflexivity rule: maps  t   to the theorem   t==t   *)
    1.85  fun reflexive ct =
    1.86    let val Cterm {sign_ref, t, T, maxidx} = ct