src/Pure/Pure.thy

--- a/src/Pure/Pure.thy	Thu Dec 22 00:28:51 2005 +0100
+++ b/src/Pure/Pure.thy	Thu Dec 22 00:28:52 2005 +0100
@@ -1,8 +1,8 @@
 (*  Title:      Pure/Pure.thy
     ID:         $Id$
+*)
 
-The Pure theory.
-*)
+header {* The Pure theory *}
 
 theory Pure
 imports ProtoPure
@@ -11,8 +11,7 @@
 setup "Context.setup ()"
 
 
-text{* These meta-level elimination rules facilitate the use of assumptions
-  that contain !! and ==>, especially in linear scripts. *}
+subsection {* Meta-level connectives in assumptions *}
 
 lemma meta_mp:
   assumes "PROP P ==> PROP Q" and "PROP P"
@@ -26,4 +25,98 @@
 
 lemmas meta_allE = meta_spec [elim_format]
 
+
+subsection {* Meta-level conjunction *}
+
+locale (open) meta_conjunction_syntax =
+  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
+
+parse_translation {*
+  [("\<^fixed>meta_conjunction", fn [t, u] => Logic.mk_conjunction (t, u))]
+*}
+
+lemma all_conjunction:
+  includes meta_conjunction_syntax
+  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)
+    fix x
+    from conj show "PROP A(x)" .
+    from conj show "PROP B(x)" .
+  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
+  qed
+qed
+
+lemma imp_conjunction [unfolded prop_def]:
+  includes meta_conjunction_syntax
+  shows "(PROP A ==> PROP prop (PROP B && PROP C)) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
+proof (unfold prop_def, rule)
+  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)
+    assume "PROP A"
+    from conj [OF `PROP A`] show "PROP B" .
+    from conj [OF `PROP A`] show "PROP C" .
+  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
+  qed
+qed
+
+lemma conjunction_imp:
+  includes meta_conjunction_syntax
+  shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
+proof
+  assume r: "PROP A && PROP B ==> PROP C"
+  assume "PROP A" and "PROP B"
+  show "PROP C" by (rule r) -
+next
+  assume r: "PROP A ==> PROP B ==> PROP C"
+  assume conj: "PROP A && PROP B"
+  show "PROP C"
+  proof (rule r)
+    from conj show "PROP A" .
+    from conj show "PROP B" .
+  qed
+qed
+
+lemma conjunction_assoc:
+  includes meta_conjunction_syntax
+  shows "((PROP A && PROP B) && PROP C) == (PROP A && (PROP B && PROP C))"
+  by (rule equal_intr_rule) (unfold imp_conjunction conjunction_imp)
+
 end