src/Pure/Pure.thy
author wenzelm
Wed Feb 15 21:34:59 2006 +0100 (2006-02-15 ago)
changeset 19048 2b875dd5eb4c
parent 18836 3a1e4ee72075
child 19121 d7fd5415a781
permissions -rw-r--r--
cannot use section before setup;
     1 (*  Title:      Pure/Pure.thy
     2     ID:         $Id$
     3 
     4 The actual Pure theory.
     5 *)
     6 
     7 header {* The Pure theory *}
     8 
     9 theory Pure
    10 imports ProtoPure
    11 begin
    12 
    13 setup  -- {* Common setup of internal components *}
    14 
    15 
    16 subsection {* Meta-level connectives in assumptions *}
    17 
    18 lemma meta_mp:
    19   assumes "PROP P ==> PROP Q" and "PROP P"
    20   shows "PROP Q"
    21     by (rule `PROP P ==> PROP Q` [OF `PROP P`])
    22 
    23 lemma meta_spec:
    24   assumes "!!x. PROP P(x)"
    25   shows "PROP P(x)"
    26     by (rule `!!x. PROP P(x)`)
    27 
    28 lemmas meta_allE = meta_spec [elim_format]
    29 
    30 
    31 subsection {* Meta-level conjunction *}
    32 
    33 locale (open) meta_conjunction_syntax =
    34   fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    35 
    36 parse_translation {*
    37   [("\<^fixed>meta_conjunction", fn [t, u] => Logic.mk_conjunction (t, u))]
    38 *}
    39 
    40 lemma all_conjunction:
    41   includes meta_conjunction_syntax
    42   shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
    43 proof
    44   assume conj: "!!x. PROP A(x) && PROP B(x)"
    45   fix X assume r: "(!!x. PROP A(x)) ==> (!!x. PROP B(x)) ==> PROP X"
    46   show "PROP X"
    47   proof (rule r)
    48     fix x
    49     from conj show "PROP A(x)" .
    50     from conj show "PROP B(x)" .
    51   qed
    52 next
    53   assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
    54   fix x
    55   fix X assume r: "PROP A(x) ==> PROP B(x) ==> PROP X"
    56   show "PROP X"
    57   proof (rule r)
    58     show "PROP A(x)"
    59     proof (rule conj)
    60       assume "!!x. PROP A(x)"
    61       then show "PROP A(x)" .
    62     qed
    63     show "PROP B(x)"
    64     proof (rule conj)
    65       assume "!!x. PROP B(x)"
    66       then show "PROP B(x)" .
    67     qed
    68   qed
    69 qed
    70 
    71 lemma imp_conjunction [unfolded prop_def]:
    72   includes meta_conjunction_syntax
    73   shows "(PROP A ==> PROP prop (PROP B && PROP C)) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
    74   unfolding prop_def
    75 proof
    76   assume conj: "PROP A ==> PROP B && PROP C"
    77   fix X assume r: "(PROP A ==> PROP B) ==> (PROP A ==> PROP C) ==> PROP X"
    78   show "PROP X"
    79   proof (rule r)
    80     assume "PROP A"
    81     from conj [OF `PROP A`] show "PROP B" .
    82     from conj [OF `PROP A`] show "PROP C" .
    83   qed
    84 next
    85   assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    86   assume "PROP A"
    87   fix X assume r: "PROP B ==> PROP C ==> PROP X"
    88   show "PROP X"
    89   proof (rule r)
    90     show "PROP B"
    91     proof (rule conj)
    92       assume "PROP A ==> PROP B"
    93       from this [OF `PROP A`] show "PROP B" .
    94     qed
    95     show "PROP C"
    96     proof (rule conj)
    97       assume "PROP A ==> PROP C"
    98       from this [OF `PROP A`] show "PROP C" .
    99     qed
   100   qed
   101 qed
   102 
   103 lemma conjunction_imp:
   104   includes meta_conjunction_syntax
   105   shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
   106 proof
   107   assume r: "PROP A && PROP B ==> PROP C"
   108   assume "PROP A" and "PROP B"
   109   show "PROP C" by (rule r) -
   110 next
   111   assume r: "PROP A ==> PROP B ==> PROP C"
   112   assume conj: "PROP A && PROP B"
   113   show "PROP C"
   114   proof (rule r)
   115     from conj show "PROP A" .
   116     from conj show "PROP B" .
   117   qed
   118 qed
   119 
   120 lemma conjunction_assoc:
   121   includes meta_conjunction_syntax
   122   shows "((PROP A && PROP B) && PROP C) == (PROP A && (PROP B && PROP C))"
   123   unfolding conjunction_imp .
   124 
   125 end