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