src/Pure/Pure.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 23824 8ad7131dbfcf
child 26426 ddac7ef1e991
permissions -rw-r--r--
Name.uu, Name.aT;
     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 lemmas [intro?] = termI
    37 
    38 
    39 subsection {* Meta-level conjunction *}
    40 
    41 locale (open) meta_conjunction_syntax =
    42   fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    43 
    44 lemma all_conjunction:
    45   includes meta_conjunction_syntax
    46   shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
    47 proof
    48   assume conj: "!!x. PROP A(x) && PROP B(x)"
    49   show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))"
    50   proof -
    51     fix x
    52     from conj show "PROP A(x)" by (rule conjunctionD1)
    53     from conj show "PROP B(x)" by (rule conjunctionD2)
    54   qed
    55 next
    56   assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
    57   fix x
    58   show "PROP A(x) && PROP B(x)"
    59   proof -
    60     show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
    61     show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
    62   qed
    63 qed
    64 
    65 lemma imp_conjunction:
    66   includes meta_conjunction_syntax
    67   shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
    68 proof
    69   assume conj: "PROP A ==> PROP B && PROP C"
    70   show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    71   proof -
    72     assume "PROP A"
    73     from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
    74     from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
    75   qed
    76 next
    77   assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    78   assume "PROP A"
    79   show "PROP B && PROP C"
    80   proof -
    81     from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
    82     from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
    83   qed
    84 qed
    85 
    86 lemma conjunction_imp:
    87   includes meta_conjunction_syntax
    88   shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
    89 proof
    90   assume r: "PROP A && PROP B ==> PROP C"
    91   assume ab: "PROP A" "PROP B"
    92   show "PROP C"
    93   proof (rule r)
    94     from ab show "PROP A && PROP B" .
    95   qed
    96 next
    97   assume r: "PROP A ==> PROP B ==> PROP C"
    98   assume conj: "PROP A && PROP B"
    99   show "PROP C"
   100   proof (rule r)
   101     from conj show "PROP A" by (rule conjunctionD1)
   102     from conj show "PROP B" by (rule conjunctionD2)
   103   qed
   104 qed
   105 
   106 end