src/Pure/Pure.thy
author ballarin
Tue Jun 06 10:05:57 2006 +0200 (2006-06-06)
changeset 19783 82f365a14960
parent 19121 d7fd5415a781
child 19800 5f764272183e
permissions -rw-r--r--
Improved parameter management of locales.
     1 (*  Title:      Pure/Pure.thy
     2     ID:         $Id$
     3 
     4 The Pure theory.
     5 *)
     6 
     7 header {* The Pure theory *}
     8 
     9 theory Pure
    10 imports ProtoPure
    11 begin
    12 ML{*set Toplevel.debug*}
    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