src/Pure/Pure.thy
author nipkow
Wed Jun 20 08:09:56 2007 +0200 (2007-06-20)
changeset 23432 cec811764a38
parent 22933 338c7890c96f
child 23824 8ad7131dbfcf
permissions -rw-r--r--
added meta_impE
     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 lemmas meta_impE = meta_mp [elim_format]
    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 {* Embedded terms *}
    32 
    33 locale (open) meta_term_syntax =
    34   fixes meta_term :: "'a => prop"  ("TERM _")
    35 
    36 parse_translation {*
    37   [("\<^fixed>meta_term", fn [t] => Const ("ProtoPure.term", dummyT --> propT) $ t)]
    38 *}
    39 
    40 lemmas [intro?] = termI
    41 
    42 
    43 subsection {* Meta-level conjunction *}
    44 
    45 locale (open) meta_conjunction_syntax =
    46   fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    47 
    48 parse_translation {*
    49   [("\<^fixed>meta_conjunction", fn [t, u] => Logic.mk_conjunction (t, u))]
    50 *}
    51 
    52 lemma all_conjunction:
    53   includes meta_conjunction_syntax
    54   shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
    55 proof
    56   assume conj: "!!x. PROP A(x) && PROP B(x)"
    57   show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))"
    58   proof -
    59     fix x
    60     from conj show "PROP A(x)" by (rule conjunctionD1)
    61     from conj show "PROP B(x)" by (rule conjunctionD2)
    62   qed
    63 next
    64   assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
    65   fix x
    66   show "PROP A(x) && PROP B(x)"
    67   proof -
    68     show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
    69     show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
    70   qed
    71 qed
    72 
    73 lemma imp_conjunction:
    74   includes meta_conjunction_syntax
    75   shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
    76 proof
    77   assume conj: "PROP A ==> PROP B && PROP C"
    78   show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    79   proof -
    80     assume "PROP A"
    81     from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
    82     from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
    83   qed
    84 next
    85   assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    86   assume "PROP A"
    87   show "PROP B && PROP C"
    88   proof -
    89     from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
    90     from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
    91   qed
    92 qed
    93 
    94 lemma conjunction_imp:
    95   includes meta_conjunction_syntax
    96   shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
    97 proof
    98   assume r: "PROP A && PROP B ==> PROP C"
    99   assume ab: "PROP A" "PROP B"
   100   show "PROP C"
   101   proof (rule r)
   102     from ab show "PROP A && PROP B" .
   103   qed
   104 next
   105   assume r: "PROP A ==> PROP B ==> PROP C"
   106   assume conj: "PROP A && PROP B"
   107   show "PROP C"
   108   proof (rule r)
   109     from conj show "PROP A" by (rule conjunctionD1)
   110     from conj show "PROP B" by (rule conjunctionD2)
   111   qed
   112 qed
   113 
   114 end