src/Pure/Pure.thy
changeset 18466 389a6f9c31f4
parent 18019 d1ff9ebb8bcb
child 18663 8474756e4cbf
     1.1 --- a/src/Pure/Pure.thy	Thu Dec 22 00:28:51 2005 +0100
     1.2 +++ b/src/Pure/Pure.thy	Thu Dec 22 00:28:52 2005 +0100
     1.3 @@ -1,8 +1,8 @@
     1.4  (*  Title:      Pure/Pure.thy
     1.5      ID:         $Id$
     1.6 +*)
     1.7  
     1.8 -The Pure theory.
     1.9 -*)
    1.10 +header {* The Pure theory *}
    1.11  
    1.12  theory Pure
    1.13  imports ProtoPure
    1.14 @@ -11,8 +11,7 @@
    1.15  setup "Context.setup ()"
    1.16  
    1.17  
    1.18 -text{* These meta-level elimination rules facilitate the use of assumptions
    1.19 -  that contain !! and ==>, especially in linear scripts. *}
    1.20 +subsection {* Meta-level connectives in assumptions *}
    1.21  
    1.22  lemma meta_mp:
    1.23    assumes "PROP P ==> PROP Q" and "PROP P"
    1.24 @@ -26,4 +25,98 @@
    1.25  
    1.26  lemmas meta_allE = meta_spec [elim_format]
    1.27  
    1.28 +
    1.29 +subsection {* Meta-level conjunction *}
    1.30 +
    1.31 +locale (open) meta_conjunction_syntax =
    1.32 +  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    1.33 +
    1.34 +parse_translation {*
    1.35 +  [("\<^fixed>meta_conjunction", fn [t, u] => Logic.mk_conjunction (t, u))]
    1.36 +*}
    1.37 +
    1.38 +lemma all_conjunction:
    1.39 +  includes meta_conjunction_syntax
    1.40 +  shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
    1.41 +proof
    1.42 +  assume conj: "!!x. PROP A(x) && PROP B(x)"
    1.43 +  fix X assume r: "(!!x. PROP A(x)) ==> (!!x. PROP B(x)) ==> PROP X"
    1.44 +  show "PROP X"
    1.45 +  proof (rule r)
    1.46 +    fix x
    1.47 +    from conj show "PROP A(x)" .
    1.48 +    from conj show "PROP B(x)" .
    1.49 +  qed
    1.50 +next
    1.51 +  assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
    1.52 +  fix x
    1.53 +  fix X assume r: "PROP A(x) ==> PROP B(x) ==> PROP X"
    1.54 +  show "PROP X"
    1.55 +  proof (rule r)
    1.56 +    show "PROP A(x)"
    1.57 +    proof (rule conj)
    1.58 +      assume "!!x. PROP A(x)"
    1.59 +      then show "PROP A(x)" .
    1.60 +    qed
    1.61 +    show "PROP B(x)"
    1.62 +    proof (rule conj)
    1.63 +      assume "!!x. PROP B(x)"
    1.64 +      then show "PROP B(x)" .
    1.65 +    qed
    1.66 +  qed
    1.67 +qed
    1.68 +
    1.69 +lemma imp_conjunction [unfolded prop_def]:
    1.70 +  includes meta_conjunction_syntax
    1.71 +  shows "(PROP A ==> PROP prop (PROP B && PROP C)) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
    1.72 +proof (unfold prop_def, rule)
    1.73 +  assume conj: "PROP A ==> PROP B && PROP C"
    1.74 +  fix X assume r: "(PROP A ==> PROP B) ==> (PROP A ==> PROP C) ==> PROP X"
    1.75 +  show "PROP X"
    1.76 +  proof (rule r)
    1.77 +    assume "PROP A"
    1.78 +    from conj [OF `PROP A`] show "PROP B" .
    1.79 +    from conj [OF `PROP A`] show "PROP C" .
    1.80 +  qed
    1.81 +next
    1.82 +  assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    1.83 +  assume "PROP A"
    1.84 +  fix X assume r: "PROP B ==> PROP C ==> PROP X"
    1.85 +  show "PROP X"
    1.86 +  proof (rule r)
    1.87 +    show "PROP B"
    1.88 +    proof (rule conj)
    1.89 +      assume "PROP A ==> PROP B"
    1.90 +      from this [OF `PROP A`] show "PROP B" .
    1.91 +    qed
    1.92 +    show "PROP C"
    1.93 +    proof (rule conj)
    1.94 +      assume "PROP A ==> PROP C"
    1.95 +      from this [OF `PROP A`] show "PROP C" .
    1.96 +    qed
    1.97 +  qed
    1.98 +qed
    1.99 +
   1.100 +lemma conjunction_imp:
   1.101 +  includes meta_conjunction_syntax
   1.102 +  shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
   1.103 +proof
   1.104 +  assume r: "PROP A && PROP B ==> PROP C"
   1.105 +  assume "PROP A" and "PROP B"
   1.106 +  show "PROP C" by (rule r) -
   1.107 +next
   1.108 +  assume r: "PROP A ==> PROP B ==> PROP C"
   1.109 +  assume conj: "PROP A && PROP B"
   1.110 +  show "PROP C"
   1.111 +  proof (rule r)
   1.112 +    from conj show "PROP A" .
   1.113 +    from conj show "PROP B" .
   1.114 +  qed
   1.115 +qed
   1.116 +
   1.117 +lemma conjunction_assoc:
   1.118 +  includes meta_conjunction_syntax
   1.119 +  shows "((PROP A && PROP B) && PROP C) == (PROP A && (PROP B && PROP C))"
   1.120 +  by (rule equal_intr_rule) (unfold imp_conjunction conjunction_imp)
   1.121 +
   1.122  end