# HG changeset patch
# User wenzelm
# Date 1132406463 -3600
# Node ID faaaa458198df12c632243d9d34e4e387758c649
# Parent  744803a2d5a530f8c064b669390b9282ef0415ed
removed conj_mono;
added conj_curry;
tuned;

diff -r 744803a2d5a5 -r faaaa458198d src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat Nov 19 14:21:02 2005 +0100
+++ b/src/Pure/drule.ML	Sat Nov 19 14:21:03 2005 +0100
@@ -19,11 +19,9 @@
   val cprems_of: thm -> cterm list
   val cterm_fun: (term -> term) -> (cterm -> cterm)
   val ctyp_fun: (typ -> typ) -> (ctyp -> ctyp)
-  val read_insts:
-          theory -> (indexname -> typ option) * (indexname -> sort option)
-                  -> (indexname -> typ option) * (indexname -> sort option)
-                  -> string list -> (indexname * string) list
-                  -> (ctyp * ctyp) list * (cterm * cterm) list
+  val read_insts: theory -> (indexname -> typ option) * (indexname -> sort option) ->
+    (indexname -> typ option) * (indexname -> sort option) -> string list ->
+    (indexname * string) list -> (ctyp * ctyp) list * (cterm * cterm) list
   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
   val strip_shyps_warning: thm -> thm
   val forall_intr_list: cterm list -> thm -> thm
@@ -38,8 +36,7 @@
   val freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
   val implies_elim_list: thm -> thm list -> thm
   val implies_intr_list: cterm list -> thm -> thm
-  val instantiate:
-    (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
+  val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
   val zero_var_indexes: thm -> thm
   val implies_intr_hyps: thm -> thm
   val standard: thm -> thm
@@ -151,7 +148,7 @@
   val conj_elim_list: thm -> thm list
   val conj_elim_precise: int -> thm -> thm list
   val conj_intr_thm: thm
-  val conj_mono_thm: thm
+  val conj_curry: thm -> thm
   val abs_def: thm -> thm
   val read_instantiate_sg': theory -> (indexname * string) list -> thm -> thm
   val read_instantiate': (indexname * string) list -> thm -> thm
@@ -163,8 +160,6 @@
 
 (** some cterm->cterm operations: faster than calling cterm_of! **)
 
-(* FIXME exception CTERM (!?) *)
-
 fun dest_implies ct =
   (case Thm.term_of ct of
     (Const ("==>", _) $ _ $ _) =>
@@ -1127,11 +1122,7 @@
   val A = read_prop "PROP A";
   val B = read_prop "PROP B";
   val C = read_prop "PROP C";
-  val D = read_prop "PROP D";
-  val AC = read_prop "PROP A ==> PROP C";
-  val BD = read_prop "PROP B ==> PROP D";
   val ABC = read_prop "PROP A ==> PROP B ==> PROP C";
-  val A_B = read_prop "!!X. (PROP A ==> PROP B ==> PROP X) ==> PROP X";
 
   val proj1 =
     forall_intr_list [A, B] (implies_intr_list [A, B] (Thm.assume A))
@@ -1170,14 +1161,28 @@
 val conj_intr_thm = store_standard_thm_open "conjunctionI"
   (implies_intr_list [A, B] (conj_intr (Thm.assume A) (Thm.assume B)));
 
-val conj_mono_thm = store_standard_thm_open "conjunction_mono"
-  (Thm.assume A_B |> conj_elim |> (fn (a, b) =>
-    conj_intr
-      (Thm.implies_elim (Thm.assume AC) a)
-      (Thm.implies_elim (Thm.assume BD) b))
-  |> implies_intr_list [AC, BD, A_B]);
+end;
 
-end;
+fun conj_curry th =
+  let
+    val {thy, maxidx, ...} = Thm.rep_thm th;
+    val n = Thm.nprems_of th;
+  in
+    if n < 2 then th
+    else
+      let
+        val cert = Thm.cterm_of thy;
+        val As = map (fn i => Free ("A" ^ string_of_int i, propT)) (1 upto n);
+        val B = Free ("B", propT);
+        val C = cert (Logic.mk_conjunction_list As);
+        val D = cert (Logic.list_implies (As, B));
+        val rule =
+          implies_elim_list (Thm.assume D) (conj_elim_list (Thm.assume C))
+          |> implies_intr_list [D, C]
+          |> forall_intr_frees
+          |> forall_elim_vars (maxidx + 1)
+      in Thm.adjust_maxidx_thm (th COMP rule) end
+  end;
 
 end;