src/Pure/conjunction.ML
changeset 20508 8182d961c7cc
parent 20260 990dbc007ca6
child 20666 82638257d372
     1.1 --- a/src/Pure/conjunction.ML	Tue Sep 12 12:12:33 2006 +0200
     1.2 +++ b/src/Pure/conjunction.ML	Tue Sep 12 12:12:39 2006 +0200
     1.3 @@ -74,8 +74,8 @@
     1.4  
     1.5  local
     1.6  
     1.7 -val A = read "PROP A";
     1.8 -val B = read "PROP B";
     1.9 +val A = read "PROP A" and vA = read "PROP ?A";
    1.10 +val B = read "PROP B" and vB = read "PROP ?B";
    1.11  val C = read "PROP C";
    1.12  val ABC = read "PROP A ==> PROP B ==> PROP C";
    1.13  val A_B = read "PROP ProtoPure.conjunction(A, B)"
    1.14 @@ -98,14 +98,25 @@
    1.15        (Thm.forall_intr C (Thm.implies_intr ABC
    1.16          (Drule.implies_elim_list (Thm.assume ABC) [Thm.assume A, Thm.assume B])))));
    1.17  
    1.18 -fun intr tha thb = thb COMP (tha COMP Drule.incr_indexes2 tha thb conjunctionI);
    1.19 +fun intr tha thb =
    1.20 +  Thm.implies_elim
    1.21 +    (Thm.implies_elim
    1.22 +      (Thm.instantiate ([], [(vA, Thm.cprop_of tha), (vB, Thm.cprop_of thb)]) conjunctionI)
    1.23 +    tha)
    1.24 +  thb;
    1.25  
    1.26  fun intr_list [] = asm_rl
    1.27    | intr_list ths = foldr1 (uncurry intr) ths;
    1.28  
    1.29  fun elim th =
    1.30 - (th COMP Drule.incr_indexes th conjunctionD1,
    1.31 -  th COMP Drule.incr_indexes th conjunctionD2);
    1.32 +  let
    1.33 +    val (A, B) = dest_conjunction (Thm.cprop_of th)
    1.34 +      handle TERM (msg, _) => raise THM (msg, 0, [th]);
    1.35 +    val inst = Thm.instantiate ([], [(vA, A), (vB, B)]);
    1.36 +  in
    1.37 +   (Thm.implies_elim (inst conjunctionD1) th,
    1.38 +    Thm.implies_elim (inst conjunctionD2) th)
    1.39 +  end;
    1.40  
    1.41  (*((A && B) && C) && D && E -- flat*)
    1.42  fun elim_list th =