eq_thm moved to thm.ML;
authorwenzelm
Tue Oct 28 17:28:11 1997 +0100 (1997-10-28)
changeset 401690aebb69c04e
parent 4015 92874142156b
child 4017 63878e2587a7
eq_thm moved to thm.ML;
store ProtoPure lemmas;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Tue Oct 28 17:27:10 1997 +0100
     1.2 +++ b/src/Pure/drule.ML	Tue Oct 28 17:28:11 1997 +0100
     1.3 @@ -333,18 +333,9 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -(** theorem equality test is exported and used by BEST_FIRST **)
     1.8 +(** theorem equality **)
     1.9  
    1.10 -(*equality of theorems uses equality of signatures and
    1.11 -  the a-convertible test for terms*)
    1.12 -fun eq_thm (th1,th2) =
    1.13 -    let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
    1.14 -        and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
    1.15 -    in  Sign.eq_sg (sg1,sg2) andalso
    1.16 -        eq_set_sort (shyps1, shyps2) andalso
    1.17 -        aconvs(hyps1,hyps2) andalso
    1.18 -        prop1 aconv prop2
    1.19 -    end;
    1.20 +val eq_thm = Thm.eq_thm;
    1.21  
    1.22  (*equality of theorems using similarity of signatures,
    1.23    i.e. the theorems belong to the same theory but not necessarily to the same
    1.24 @@ -388,19 +379,21 @@
    1.25  
    1.26  (*** Meta-Rewriting Rules ***)
    1.27  
    1.28 +fun store_thm name thm = PureThy.smart_store_thm (name, standard thm);
    1.29 +
    1.30  val reflexive_thm =
    1.31    let val cx = cterm_of (sign_of ProtoPure.thy) (Var(("x",0),TVar(("'a",0),logicS)))
    1.32 -  in Thm.reflexive cx end;
    1.33 +  in store_thm "reflexive" (Thm.reflexive cx) end;
    1.34  
    1.35  val symmetric_thm =
    1.36    let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
    1.37 -  in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
    1.38 +  in store_thm "symmetric" (Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
    1.39  
    1.40  val transitive_thm =
    1.41    let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
    1.42        val yz = read_cterm (sign_of ProtoPure.thy) ("y::'a::logic == z",propT)
    1.43        val xythm = Thm.assume xy and yzthm = Thm.assume yz
    1.44 -  in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
    1.45 +  in store_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
    1.46  
    1.47  (** Below, a "conversion" has type cterm -> thm **)
    1.48  
    1.49 @@ -486,27 +479,29 @@
    1.50  (*** Some useful meta-theorems ***)
    1.51  
    1.52  (*The rule V/V, obtains assumption solving for eresolve_tac*)
    1.53 -val asm_rl = trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi",propT));
    1.54 +val asm_rl =
    1.55 +  store_thm "asm_rl" (trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi",propT)));
    1.56  
    1.57  (*Meta-level cut rule: [| V==>W; V |] ==> W *)
    1.58 -val cut_rl = trivial(read_cterm (sign_of ProtoPure.thy)
    1.59 -        ("PROP ?psi ==> PROP ?theta", propT));
    1.60 +val cut_rl =
    1.61 +  store_thm "cut_rl"
    1.62 +    (trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi ==> PROP ?theta", propT)));
    1.63  
    1.64  (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
    1.65       [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
    1.66  val revcut_rl =
    1.67    let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
    1.68        and VW = read_cterm (sign_of ProtoPure.thy) ("PROP V ==> PROP W", propT);
    1.69 -  in  standard (implies_intr V
    1.70 -                (implies_intr VW
    1.71 -                 (implies_elim (assume VW) (assume V))))
    1.72 +  in
    1.73 +    store_thm "revcut_rl"
    1.74 +      (implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V))))
    1.75    end;
    1.76  
    1.77  (*for deleting an unwanted assumption*)
    1.78  val thin_rl =
    1.79    let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
    1.80        and W = read_cterm (sign_of ProtoPure.thy) ("PROP W", propT);
    1.81 -  in  standard (implies_intr V (implies_intr W (assume W)))
    1.82 +  in  store_thm "thin_rl" (implies_intr V (implies_intr W (assume W)))
    1.83    end;
    1.84  
    1.85  (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
    1.86 @@ -514,8 +509,10 @@
    1.87    let val V  = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
    1.88        and QV = read_cterm (sign_of ProtoPure.thy) ("!!x::'a. PROP V", propT)
    1.89        and x  = read_cterm (sign_of ProtoPure.thy) ("x", TFree("'a",logicS));
    1.90 -  in  standard (equal_intr (implies_intr QV (forall_elim x (assume QV)))
    1.91 -                           (implies_intr V  (forall_intr x (assume V))))
    1.92 +  in
    1.93 +    store_thm "triv_forall_equality"
    1.94 +      (equal_intr (implies_intr QV (forall_elim x (assume QV)))
    1.95 +        (implies_intr V  (forall_intr x (assume V))))
    1.96    end;
    1.97  
    1.98  (* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==>
    1.99 @@ -530,7 +527,7 @@
   1.100        val minor1 = assume cminor1;
   1.101        val cminor2 = read_cterm (sign_of ProtoPure.thy)  ("PROP PhiB", propT);
   1.102        val minor2 = assume cminor2;
   1.103 -  in standard
   1.104 +  in store_thm "swap_prems_rl"
   1.105         (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
   1.106           (implies_elim (implies_elim major minor1) minor2))))
   1.107    end;
   1.108 @@ -542,10 +539,9 @@
   1.109  val equal_intr_rule =
   1.110    let val PQ = read_cterm (sign_of ProtoPure.thy) ("PROP phi ==> PROP psi", propT)
   1.111        and QP = read_cterm (sign_of ProtoPure.thy) ("PROP psi ==> PROP phi", propT)
   1.112 -  in  equal_intr (assume PQ) (assume QP)
   1.113 -      |> implies_intr QP
   1.114 -      |> implies_intr PQ
   1.115 -      |> standard
   1.116 +  in
   1.117 +    store_thm "equal_intr_rule"
   1.118 +      (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
   1.119    end;
   1.120  
   1.121  end;