# HG changeset patch
# User wenzelm
# Date 1140643119 -3600
# Node ID 59b26248547b80cb46bc66cf5e3dab32731eba35
# Parent  d9ac560a7bc80032ff49353dbfa864e6f84e3553
simplified Pure conjunction, based on actual const;

diff -r d9ac560a7bc8 -r 59b26248547b src/Pure/logic.ML
--- a/src/Pure/logic.ML	Wed Feb 22 22:18:38 2006 +0100
+++ b/src/Pure/logic.ML	Wed Feb 22 22:18:39 2006 +0100
@@ -22,6 +22,7 @@
   val strip_prems: int * term list * term -> term list * term
   val count_prems: term * int -> int
   val nth_prem: int * term -> term
+  val conjunction: term
   val mk_conjunction: term * term -> term
   val mk_conjunction_list: term list -> term
   val mk_conjunction_list2: term list list -> term
@@ -144,10 +145,10 @@
 
 (** conjunction **)
 
+val conjunction = Const ("ProtoPure.conjunction", propT --> propT --> propT);
+
 (*A && B*)
-fun mk_conjunction (t, u) =
-  Term.list_all ([("X", propT)],
-    mk_implies (list_implies (map (Term.incr_boundvars 1) [t, u], Bound 0), Bound 0));
+fun mk_conjunction (A, B) = conjunction $ A $ B;
 
 (*A && B && C -- improper*)
 fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0))
@@ -158,12 +159,7 @@
   mk_conjunction_list (map mk_conjunction_list (filter_out null tss));
 
 (*A && B*)
-fun dest_conjunction
-      (t as Const ("all", _) $ Abs (_, _,
-        Const ("==>", _) $ (Const ("==>", _) $ A $ (Const ("==>", _) $ B $ Bound 0)) $ Bound 0)) =
-      if Term.loose_bvar1 (A, 0) orelse Term.loose_bvar1 (B, 0)
-      then raise TERM ("dest_conjunction", [t])
-      else (Term.incr_boundvars ~1 A, Term.incr_boundvars ~1 B)
+fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B)
   | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
 
 (*((A && B) && C) && D && E -- flat*)
diff -r d9ac560a7bc8 -r 59b26248547b src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Feb 22 22:18:38 2006 +0100
+++ b/src/Pure/pure_thy.ML	Wed Feb 22 22:18:39 2006 +0100
@@ -23,6 +23,7 @@
     sig
       val thy: theory
       val prop_def: thm
+      val conjunction_def: thm
     end
 end;
 
@@ -609,7 +610,7 @@
     ("_DDDOT",   "logic",                 Delimfix "\\<dots>")]
   |> Theory.add_modesyntax ("", false)
    [("prop", "prop => prop", Mixfix ("_", [0], 0)),
-    ("_meta_conjunction", "prop => prop => prop", InfixrName ("&&", 2))]
+    ("ProtoPure.conjunction", "prop => prop => prop", InfixrName ("&&", 2))]
   |> Theory.add_modesyntax ("HTML", false)
    [("_lambda",  "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
   |> Theory.add_consts
@@ -628,8 +629,13 @@
   |> Theory.add_trfuns Syntax.pure_trfuns
   |> Theory.add_trfunsT Syntax.pure_trfunsT
   |> Sign.local_path
-  |> (add_defs_i false o map Thm.no_attributes)
-       [("prop_def", Logic.mk_equals (Logic.protect A, A))] |> snd
+  |> Theory.add_consts
+   [("conjunction", "prop => prop => prop", NoSyn)]
+  |> (add_defs false o map Thm.no_attributes)
+   [("prop_def", "prop(A) == A"),
+    ("conjunction_def",
+      "conjunction(A, B) == (!!C. (PROP A ==> PROP B ==> PROP C) ==> PROP C)")] |> snd
+  |> Sign.hide_consts false ["conjunction"]
   |> add_thmss [(("nothing", []), [])] |> snd
   |> Theory.add_axioms_i Proofterm.equality_axms
   |> Theory.end_theory;
@@ -638,6 +644,7 @@
 struct
   val thy = proto_pure;
   val prop_def = get_axiom thy "prop_def";
+  val conjunction_def = get_axiom thy "conjunction_def";
 end;
 
 end;
diff -r d9ac560a7bc8 -r 59b26248547b src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed Feb 22 22:18:38 2006 +0100
+++ b/src/Pure/tactic.ML	Wed Feb 22 22:18:39 2006 +0100
@@ -642,8 +642,7 @@
 (* meta-level conjunction *)
 
 val conj_tac = SUBGOAL (fn (goal, i) =>
-  if can Logic.dest_conjunction goal then
-    (fn st => compose_tac (false, Drule.incr_indexes st Drule.conj_intr_thm, 2) i st)
+  if can Logic.dest_conjunction goal then rtac Drule.conjunctionI i
   else no_tac);
 
 val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac;