# HG changeset patch
# User wenzelm
# Date 1183494431 -7200
# Node ID 16e5fd18905c61684be3309f351dddbfbd21d196
# Parent  151d60fbfffe26fae63bf4d3002ca9f28908d6db
assume basic HOL context for compilation (antiquotations);
added dest_cTrueprop;
tuned Trueprop_conv;
added low-level conj_intr/elim/elis (dire need for @{rule} antiquotation!);

diff -r 151d60fbfffe -r 16e5fd18905c src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Tue Jul 03 22:27:08 2007 +0200
+++ b/src/HOL/hologic.ML	Tue Jul 03 22:27:11 2007 +0200
@@ -18,7 +18,11 @@
   val Trueprop: term
   val mk_Trueprop: term -> term
   val dest_Trueprop: term -> term
-  val Trueprop_conv: (cterm -> thm) -> cterm -> thm
+  val dest_cTrueprop: cterm -> cterm
+  val Trueprop_conv: conv -> conv
+  val conj_intr: thm -> thm -> thm
+  val conj_elim: thm -> thm * thm
+  val conj_elims: thm -> thm list
   val conj: term
   val disj: term
   val imp: term
@@ -137,16 +141,38 @@
 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
   | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
 
-fun Trueprop_conv conv ct = (case term_of ct of
-    Const ("Trueprop", _) $ _ =>
-      let val (ct1, ct2) = Thm.dest_comb ct
-      in Thm.combination (Thm.reflexive ct1) (conv ct2) end
-  | _ => raise TERM ("Trueprop_conv", []));
+fun dest_cTrueprop ct =
+  if can dest_Trueprop (Thm.term_of ct) then Thm.dest_arg ct
+  else raise CTERM ("cdest_Trueprop", [ct]);
+
+fun Trueprop_conv conv ct =
+  if can dest_Trueprop (Thm.term_of ct) then Conv.arg_conv conv ct
+  else raise CTERM ("Trueprop_conv", [ct]);
+
+fun conj_intr thP thQ =
+  let
+    val (P, Q) = pairself (dest_cTrueprop o Thm.cprop_of) (thP, thQ)
+      handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
+    val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
+  in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end;
 
-val conj = Const ("op &", [boolT, boolT] ---> boolT)
-and disj = Const ("op |", [boolT, boolT] ---> boolT)
-and imp = Const ("op -->", [boolT, boolT] ---> boolT)
-and Not = Const ("Not", boolT --> boolT);
+fun conj_elim thPQ =
+  let
+    val (P, Q) = Thm.dest_binop (dest_cTrueprop (Thm.cprop_of thPQ))
+      handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
+    val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
+    val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ;
+    val thQ = Thm.implies_elim (inst @{thm conjunct2}) thPQ;
+  in (thP, thQ) end;
+
+fun conj_elims th =
+  let val (th1, th2) = conj_elim th
+  in conj_elims th1 @ conj_elims th2 end handle THM _ => [th];
+
+val conj = @{term "op &"}
+and disj = @{term "op |"}
+and imp = @{term "op -->"}
+and Not = @{term "Not"};
 
 fun mk_conj (t1, t2) = conj $ t1 $ t2
 and mk_disj (t1, t2) = disj $ t1 $ t2