src/Pure/Pure.thy
author wenzelm
Thu Mar 27 15:32:15 2008 +0100 (2008-03-27)
changeset 26435 bdce320cd426
parent 26426 ddac7ef1e991
child 26570 dbc458262f4c
permissions -rw-r--r--
eliminated delayed theory setup
     1 (*  Title:      Pure/Pure.thy
     2     ID:         $Id$
     3 *)
     4 
     5 section {* Further content for the Pure theory *}
     6 
     7 subsection {* Meta-level connectives in assumptions *}
     8 
     9 lemma meta_mp:
    10   assumes "PROP P ==> PROP Q" and "PROP P"
    11   shows "PROP Q"
    12     by (rule `PROP P ==> PROP Q` [OF `PROP P`])
    13 
    14 lemmas meta_impE = meta_mp [elim_format]
    15 
    16 lemma meta_spec:
    17   assumes "!!x. PROP P(x)"
    18   shows "PROP P(x)"
    19     by (rule `!!x. PROP P(x)`)
    20 
    21 lemmas meta_allE = meta_spec [elim_format]
    22 
    23 
    24 subsection {* Embedded terms *}
    25 
    26 locale (open) meta_term_syntax =
    27   fixes meta_term :: "'a => prop"  ("TERM _")
    28 
    29 lemmas [intro?] = termI
    30 
    31 
    32 subsection {* Meta-level conjunction *}
    33 
    34 locale (open) meta_conjunction_syntax =
    35   fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    36 
    37 lemma all_conjunction:
    38   includes meta_conjunction_syntax
    39   shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
    40 proof
    41   assume conj: "!!x. PROP A(x) && PROP B(x)"
    42   show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))"
    43   proof -
    44     fix x
    45     from conj show "PROP A(x)" by (rule conjunctionD1)
    46     from conj show "PROP B(x)" by (rule conjunctionD2)
    47   qed
    48 next
    49   assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
    50   fix x
    51   show "PROP A(x) && PROP B(x)"
    52   proof -
    53     show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
    54     show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
    55   qed
    56 qed
    57 
    58 lemma imp_conjunction:
    59   includes meta_conjunction_syntax
    60   shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
    61 proof
    62   assume conj: "PROP A ==> PROP B && PROP C"
    63   show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    64   proof -
    65     assume "PROP A"
    66     from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
    67     from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
    68   qed
    69 next
    70   assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
    71   assume "PROP A"
    72   show "PROP B && PROP C"
    73   proof -
    74     from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
    75     from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
    76   qed
    77 qed
    78 
    79 lemma conjunction_imp:
    80   includes meta_conjunction_syntax
    81   shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
    82 proof
    83   assume r: "PROP A && PROP B ==> PROP C"
    84   assume ab: "PROP A" "PROP B"
    85   show "PROP C"
    86   proof (rule r)
    87     from ab show "PROP A && PROP B" .
    88   qed
    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