Added Larry's equal_intr_rule
authornipkow
Tue Sep 02 16:10:26 1997 +0200 (1997-09-02)
changeset 36536d5b3d5ff132
parent 3652 4c484f03079c
child 3654 ebad042c0bba
Added Larry's equal_intr_rule
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Tue Sep 02 11:25:32 1997 +0200
     1.2 +++ b/src/Pure/drule.ML	Tue Sep 02 16:10:26 1997 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    val cut_rl		: thm
     1.5    val equal_abs_elim	: cterm  -> thm -> thm
     1.6    val equal_abs_elim_list: cterm list -> thm -> thm
     1.7 +  val equal_intr_rule   : thm
     1.8    val eq_thm		: thm * thm -> bool
     1.9    val same_thm		: thm * thm -> bool
    1.10    val eq_thm_sg		: thm * thm -> bool
    1.11 @@ -658,6 +659,19 @@
    1.12           (implies_elim (implies_elim major minor1) minor2))))
    1.13    end;
    1.14  
    1.15 +(* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
    1.16 +   ==> PROP ?phi == PROP ?psi
    1.17 +   Introduction rule for == using ==> not meta-hyps.
    1.18 +*)
    1.19 +val equal_intr_rule =
    1.20 +  let val PQ = read_cterm Sign.proto_pure ("PROP phi ==> PROP psi", propT)
    1.21 +      and QP = read_cterm Sign.proto_pure ("PROP psi ==> PROP phi", propT)
    1.22 +  in  equal_intr (assume PQ) (assume QP)
    1.23 +      |> implies_intr QP
    1.24 +      |> implies_intr PQ
    1.25 +      |> standard
    1.26 +  end;
    1.27 +
    1.28  end;
    1.29  
    1.30  open Drule;