added conj_elim_precise, conj_intr_thm;
authorwenzelm
Sun Nov 11 21:30:10 2001 +0100 (2001-11-11)
changeset 12135e370e5d469c2
parent 12134 7049eead7a50
child 12136 74156e7bb22e
added conj_elim_precise, conj_intr_thm;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Sat Nov 10 16:25:17 2001 +0100
     1.2 +++ b/src/Pure/drule.ML	Sun Nov 11 21:30:10 2001 +0100
     1.3 @@ -125,6 +125,8 @@
     1.4    val conj_intr_list: thm list -> thm
     1.5    val conj_elim: thm -> thm * thm
     1.6    val conj_elim_list: thm -> thm list
     1.7 +  val conj_elim_precise: int -> thm -> thm list
     1.8 +  val conj_intr_thm: thm
     1.9  end;
    1.10  
    1.11  structure Drule: DRULE =
    1.12 @@ -517,22 +519,22 @@
    1.13  
    1.14  fun store_thm name thm = hd (PureThy.smart_store_thms (name, [thm]));
    1.15  fun store_standard_thm name thm = store_thm name (standard thm);
    1.16 -fun open_store_thm name thm = hd (PureThy.open_smart_store_thms (name, [thm]));
    1.17 -fun open_store_standard_thm name thm = open_store_thm name (standard' thm);
    1.18 +fun store_thm_open name thm = hd (PureThy.smart_store_thms_open (name, [thm]));
    1.19 +fun store_standard_thm_open name thm = store_thm_open name (standard' thm);
    1.20  
    1.21  val reflexive_thm =
    1.22    let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),logicS)))
    1.23 -  in open_store_standard_thm "reflexive" (Thm.reflexive cx) end;
    1.24 +  in store_standard_thm_open "reflexive" (Thm.reflexive cx) end;
    1.25  
    1.26  val symmetric_thm =
    1.27    let val xy = read_prop "x::'a::logic == y"
    1.28 -  in open_store_standard_thm "symmetric" (Thm.implies_intr_hyps (Thm.symmetric (Thm.assume xy))) end;
    1.29 +  in store_standard_thm_open "symmetric" (Thm.implies_intr_hyps (Thm.symmetric (Thm.assume xy))) end;
    1.30  
    1.31  val transitive_thm =
    1.32    let val xy = read_prop "x::'a::logic == y"
    1.33        val yz = read_prop "y::'a::logic == z"
    1.34        val xythm = Thm.assume xy and yzthm = Thm.assume yz
    1.35 -  in open_store_standard_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
    1.36 +  in store_standard_thm_open "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
    1.37  
    1.38  fun symmetric_fun thm = thm RS symmetric_thm;
    1.39  
    1.40 @@ -548,7 +550,7 @@
    1.41      val AC = read_prop "PROP A ==> PROP C"
    1.42      val A = read_prop "PROP A"
    1.43    in
    1.44 -    open_store_standard_thm "imp_cong" (implies_intr ABC (equal_intr
    1.45 +    store_standard_thm_open "imp_cong" (implies_intr ABC (equal_intr
    1.46        (implies_intr AB (implies_intr A
    1.47          (equal_elim (implies_elim (assume ABC) (assume A))
    1.48            (implies_elim (assume AB) (assume A)))))
    1.49 @@ -564,7 +566,7 @@
    1.50      val A = read_prop "PROP A"
    1.51      val B = read_prop "PROP B"
    1.52    in
    1.53 -    open_store_standard_thm "swap_prems_eq" (equal_intr
    1.54 +    store_standard_thm_open "swap_prems_eq" (equal_intr
    1.55        (implies_intr ABC (implies_intr B (implies_intr A
    1.56          (implies_elim (implies_elim (assume ABC) (assume A)) (assume B)))))
    1.57        (implies_intr BAC (implies_intr A (implies_intr B
    1.58 @@ -577,12 +579,12 @@
    1.59  (*** Some useful meta-theorems ***)
    1.60  
    1.61  (*The rule V/V, obtains assumption solving for eresolve_tac*)
    1.62 -val asm_rl = open_store_standard_thm "asm_rl" (Thm.trivial (read_prop "PROP ?psi"));
    1.63 +val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "PROP ?psi"));
    1.64  val _ = store_thm "_" asm_rl;
    1.65  
    1.66  (*Meta-level cut rule: [| V==>W; V |] ==> W *)
    1.67  val cut_rl =
    1.68 -  open_store_standard_thm "cut_rl"
    1.69 +  store_standard_thm_open "cut_rl"
    1.70      (Thm.trivial (read_prop "PROP ?psi ==> PROP ?theta"));
    1.71  
    1.72  (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
    1.73 @@ -591,7 +593,7 @@
    1.74    let val V = read_prop "PROP V"
    1.75        and VW = read_prop "PROP V ==> PROP W";
    1.76    in
    1.77 -    open_store_standard_thm "revcut_rl"
    1.78 +    store_standard_thm_open "revcut_rl"
    1.79        (implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V))))
    1.80    end;
    1.81  
    1.82 @@ -599,8 +601,7 @@
    1.83  val thin_rl =
    1.84    let val V = read_prop "PROP V"
    1.85        and W = read_prop "PROP W";
    1.86 -  in  open_store_standard_thm "thin_rl" (implies_intr V (implies_intr W (assume W)))
    1.87 -  end;
    1.88 +  in store_standard_thm_open "thin_rl" (implies_intr V (implies_intr W (assume W))) end;
    1.89  
    1.90  (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
    1.91  val triv_forall_equality =
    1.92 @@ -608,7 +609,7 @@
    1.93        and QV = read_prop "!!x::'a. PROP V"
    1.94        and x  = read_cterm proto_sign ("x", TypeInfer.logicT);
    1.95    in
    1.96 -    open_store_standard_thm "triv_forall_equality"
    1.97 +    store_standard_thm_open "triv_forall_equality"
    1.98        (equal_intr (implies_intr QV (forall_elim x (assume QV)))
    1.99          (implies_intr V  (forall_intr x (assume V))))
   1.100    end;
   1.101 @@ -624,7 +625,7 @@
   1.102        val minor1 = assume cminor1;
   1.103        val cminor2 = read_prop "PROP PhiB";
   1.104        val minor2 = assume cminor2;
   1.105 -  in open_store_standard_thm "swap_prems_rl"
   1.106 +  in store_standard_thm_open "swap_prems_rl"
   1.107         (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
   1.108           (implies_elim (implies_elim major minor1) minor2))))
   1.109    end;
   1.110 @@ -637,7 +638,7 @@
   1.111    let val PQ = read_prop "PROP phi ==> PROP psi"
   1.112        and QP = read_prop "PROP psi ==> PROP phi"
   1.113    in
   1.114 -    open_store_standard_thm "equal_intr_rule"
   1.115 +    store_standard_thm_open "equal_intr_rule"
   1.116        (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
   1.117    end;
   1.118  
   1.119 @@ -671,7 +672,7 @@
   1.120          |> Thm.forall_intr cx
   1.121          |> Thm.implies_intr cphi
   1.122          |> Thm.implies_intr rhs)
   1.123 -    |> open_store_standard_thm "norm_hhf_eq"
   1.124 +    |> store_standard_thm_open "norm_hhf_eq"
   1.125    end;
   1.126  
   1.127  
   1.128 @@ -928,6 +929,14 @@
   1.129    let val (th1, th2) = conj_elim th
   1.130    in conj_elim_list th1 @ conj_elim_list th2 end handle THM _ => [th];
   1.131  
   1.132 +fun conj_elim_precise 1 th = [th]
   1.133 +  | conj_elim_precise n th =
   1.134 +      let val (th1, th2) = conj_elim th
   1.135 +      in th1 :: conj_elim_precise (n - 1) th2 end;
   1.136 +
   1.137 +val conj_intr_thm = store_standard_thm_open "conjunctionI"
   1.138 +  (implies_intr_list [A, B] (conj_intr (Thm.assume A) (Thm.assume B)));
   1.139 +
   1.140  end;
   1.141  
   1.142  end;