src/Pure/Pure.thy
author haftmann
Tue Sep 19 15:22:03 2006 +0200 (2006-09-19 ago)
changeset 20596 3950e65f48f8
parent 19800 5f764272183e
child 20627 30da2841553e
permissions -rw-r--r--
(void)
     1 (*  Title:      Pure/Pure.thy
     2     ID:         $Id$
     3 *)
     4 
     5 header {* The Pure theory *}
     6 
     7 theory Pure
     8 imports ProtoPure
     9 begin
    10 
    11 setup  -- {* Common setup of internal components *}
    12 
    13 subsection {* Meta-level connectives in assumptions *}
    14 
    15 lemma meta_mp:
    16   assumes "PROP P ==> PROP Q" and "PROP P"
    17   shows "PROP Q"
    18     by (rule `PROP P ==> PROP Q` [OF `PROP P`])
    19 
    20 lemma meta_spec:
    21   assumes "!!x. PROP P(x)"
    22   shows "PROP P(x)"
    23     by (rule `!!x. PROP P(x)`)
    24 
    25 lemmas meta_allE = meta_spec [elim_format]
    26 
    27 
    28 subsection {* Meta-level conjunction *}
    29 
    30 locale (open) meta_conjunction_syntax =
    31   fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    32 
    33 parse_translation {*
    34   [("\<^fixed>meta_conjunction", fn [t, u] => Logic.mk_conjunction (t, u))]
    35 *}
    36 
    37 lemma all_conjunction:
    38   includes meta_conjunction_syntax
    39   shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
    40 proof
    41   assume conj: "!!x. PROP A(x) && PROP B(x)"
    42   show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))"
    43   proof -
    44     fix x
    45     from conj show "PROP A(x)" by (rule conjunctionD1)
    46     from conj show "PROP B(x)" by (rule conjunctionD2)
    47   qed
    48 next
    49   assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
    50   fix x
    51   show "PROP A(x) && PROP B(x)"
    52   proof -
    53     show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
    54     show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
    55   qed
    56 qed
    57 
    58 lemma imp_conjunction:
    59   includes meta_conjunction_syntax
    60   shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
    61 proof
    62   assume conj: "PROP A ==> PROP B && PROP C"
    63   show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    64   proof -
    65     assume "PROP A"
    66     from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
    67     from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
    68   qed
    69 next
    70   assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    71   assume "PROP A"
    72   show "PROP B && PROP C"
    73   proof -
    74     from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
    75     from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
    76   qed
    77 qed
    78 
    79 lemma conjunction_imp:
    80   includes meta_conjunction_syntax
    81   shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
    82 proof
    83   assume r: "PROP A && PROP B ==> PROP C"
    84   assume "PROP A" and "PROP B"
    85   show "PROP C" by (rule r) -
    86 next
    87   assume r: "PROP A ==> PROP B ==> PROP C"
    88   assume conj: "PROP A && PROP B"
    89   show "PROP C"
    90   proof (rule r)
    91     from conj show "PROP A" by (rule conjunctionD1)
    92     from conj show "PROP B" by (rule conjunctionD2)
    93   qed
    94 qed
    95 
    96 end