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