simplified Pure conjunction;

--- a/src/HOL/HOL.thy	Wed Feb 22 22:18:31 2006 +0100
+++ b/src/HOL/HOL.thy	Wed Feb 22 22:18:32 2006 +0100
@@ -888,18 +888,21 @@
 qed
 
 lemma atomize_conj [atomize]:
-  "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
+  includes meta_conjunction_syntax
+  shows "(A && B) == Trueprop (A & B)"
 proof
-  assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
-  show "A & B" by (rule conjI)
+  assume conj: "A && B"
+  show "A & B"
+  proof (rule conjI)
+    from conj show A by (rule conjunctionD1)
+    from conj show B by (rule conjunctionD2)
+  qed
 next
-  fix C
-  assume "A & B"
-  assume "A ==> B ==> PROP C"
-  thus "PROP C"
-  proof this
-    show A by (rule conjunct1)
-    show B by (rule conjunct2)
+  assume conj: "A & B"
+  show "A && B"
+  proof -
+    from conj show A ..
+    from conj show B ..
   qed
 qed
 

--- a/src/Provers/induct_method.ML	Wed Feb 22 22:18:31 2006 +0100
+++ b/src/Provers/induct_method.ML	Wed Feb 22 22:18:32 2006 +0100
@@ -42,7 +42,6 @@
 val all_conjunction = thm "Pure.all_conjunction";
 val imp_conjunction = thm "Pure.imp_conjunction";
 val conjunction_imp = thm "Pure.conjunction_imp";
-val conjunction_assoc = thm "Pure.conjunction_assoc";
 val conjunction_congs = [all_conjunction, imp_conjunction];
 
 
@@ -182,23 +181,11 @@
     val (As, B) = Logic.strip_horn (Thm.prop_of thm);
   in (thy, Logic.list_implies (map rulify As, rulify B)) end;
 
-val curry_prems_tac =
-  let
-    val rule = conjunction_imp;
-    val thy = Thm.theory_of_thm rule;
-    val proc = Simplifier.simproc_i thy "curry_prems"
-      [#1 (Logic.dest_equals (Thm.prop_of rule))]
-      (fn _ => fn ss => fn _ =>  (*WORKAROUND: prevent descending into meta conjunctions*)
-        if exists (equal propT o #2 o #1) (#2 (#bounds (#1 (Simplifier.rep_ss ss))))
-        then NONE else SOME rule);
-    val ss = MetaSimplifier.theory_context thy Simplifier.empty_ss addsimprocs [proc];
-  in Simplifier.full_simp_tac ss end;
-
 val rulify_tac =
   Tactic.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
   Tactic.rewrite_goal_tac Data.rulify_fallback THEN'
   Tactic.conjunction_tac THEN_ALL_NEW
-  (curry_prems_tac THEN' Tactic.norm_hhf_tac);
+  (Tactic.rewrite_goal_tac [conjunction_imp] THEN' Tactic.norm_hhf_tac);
 
 
 (* prepare rule *)

--- a/src/Pure/Pure.thy	Wed Feb 22 22:18:31 2006 +0100
+++ b/src/Pure/Pure.thy	Wed Feb 22 22:18:32 2006 +0100
@@ -42,61 +42,40 @@
   shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
 proof
   assume conj: "!!x. PROP A(x) && PROP B(x)"
-  fix X assume r: "(!!x. PROP A(x)) ==> (!!x. PROP B(x)) ==> PROP X"
-  show "PROP X"
-  proof (rule r)
+  show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))"
+  proof -
     fix x
-    from conj show "PROP A(x)" .
-    from conj show "PROP B(x)" .
+    from conj show "PROP A(x)" by (rule conjunctionD1)
+    from conj show "PROP B(x)" by (rule conjunctionD2)
   qed
 next
   assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
   fix x
-  fix X assume r: "PROP A(x) ==> PROP B(x) ==> PROP X"
-  show "PROP X"
-  proof (rule r)
-    show "PROP A(x)"
-    proof (rule conj)
-      assume "!!x. PROP A(x)"
-      then show "PROP A(x)" .
-    qed
-    show "PROP B(x)"
-    proof (rule conj)
-      assume "!!x. PROP B(x)"
-      then show "PROP B(x)" .
-    qed
+  show "PROP A(x) && PROP B(x)"
+  proof -
+    show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
+    show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
   qed
 qed
 
-lemma imp_conjunction [unfolded prop_def]:
+lemma imp_conjunction:
   includes meta_conjunction_syntax
-  shows "(PROP A ==> PROP prop (PROP B && PROP C)) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
-  unfolding prop_def
+  shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
 proof
   assume conj: "PROP A ==> PROP B && PROP C"
-  fix X assume r: "(PROP A ==> PROP B) ==> (PROP A ==> PROP C) ==> PROP X"
-  show "PROP X"
-  proof (rule r)
+  show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
+  proof -
     assume "PROP A"
-    from conj [OF `PROP A`] show "PROP B" .
-    from conj [OF `PROP A`] show "PROP C" .
+    from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
+    from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
   qed
 next
   assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
   assume "PROP A"
-  fix X assume r: "PROP B ==> PROP C ==> PROP X"
-  show "PROP X"
-  proof (rule r)
-    show "PROP B"
-    proof (rule conj)
-      assume "PROP A ==> PROP B"
-      from this [OF `PROP A`] show "PROP B" .
-    qed
-    show "PROP C"
-    proof (rule conj)
-      assume "PROP A ==> PROP C"
-      from this [OF `PROP A`] show "PROP C" .
-    qed
+  show "PROP B && PROP C"
+  proof -
+    from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
+    from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
   qed
 qed
 
@@ -112,14 +91,9 @@
   assume conj: "PROP A && PROP B"
   show "PROP C"
   proof (rule r)
-    from conj show "PROP A" .
-    from conj show "PROP B" .
+    from conj show "PROP A" by (rule conjunctionD1)
+    from conj show "PROP B" by (rule conjunctionD2)
   qed
 qed
 
-lemma conjunction_assoc:
-  includes meta_conjunction_syntax
-  shows "((PROP A && PROP B) && PROP C) == (PROP A && (PROP B && PROP C))"
-  unfolding conjunction_imp .
-
 end