src/Pure/Pure.thy
author wenzelm
Wed Feb 22 22:18:32 2006 +0100 (2006-02-22)
changeset 19121 d7fd5415a781
parent 19048 2b875dd5eb4c
child 19783 82f365a14960
permissions -rw-r--r--
simplified Pure conjunction;
     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   show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))"
    46   proof -
    47     fix x
    48     from conj show "PROP A(x)" by (rule conjunctionD1)
    49     from conj show "PROP B(x)" by (rule conjunctionD2)
    50   qed
    51 next
    52   assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
    53   fix x
    54   show "PROP A(x) && PROP B(x)"
    55   proof -
    56     show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
    57     show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
    58   qed
    59 qed
    60 
    61 lemma imp_conjunction:
    62   includes meta_conjunction_syntax
    63   shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
    64 proof
    65   assume conj: "PROP A ==> PROP B && PROP C"
    66   show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    67   proof -
    68     assume "PROP A"
    69     from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
    70     from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
    71   qed
    72 next
    73   assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    74   assume "PROP A"
    75   show "PROP B && PROP C"
    76   proof -
    77     from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
    78     from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
    79   qed
    80 qed
    81 
    82 lemma conjunction_imp:
    83   includes meta_conjunction_syntax
    84   shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
    85 proof
    86   assume r: "PROP A && PROP B ==> PROP C"
    87   assume "PROP A" and "PROP B"
    88   show "PROP C" by (rule r) -
    89 next
    90   assume r: "PROP A ==> PROP B ==> PROP C"
    91   assume conj: "PROP A && PROP B"
    92   show "PROP C"
    93   proof (rule r)
    94     from conj show "PROP A" by (rule conjunctionD1)
    95     from conj show "PROP B" by (rule conjunctionD2)
    96   qed
    97 qed
    98 
    99 end