src/Pure/Pure.thy
author haftmann
Fri Jul 25 12:03:32 2008 +0200 (2008-07-25)
changeset 27681 8cedebf55539
parent 26958 ed3a58a9eae1
child 28699 32b6a8f12c1c
permissions -rw-r--r--
dropped locale (open)
     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 lemma swap_params:
    24   "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
    25 
    26 
    27 subsection {* Embedded terms *}
    28 
    29 locale meta_term_syntax =
    30   fixes meta_term :: "'a => prop"  ("TERM _")
    31 
    32 lemmas [intro?] = termI
    33 
    34 
    35 subsection {* Meta-level conjunction *}
    36 
    37 locale meta_conjunction_syntax =
    38   fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
    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 "(!!x. PROP A x) && (!!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 ab: "PROP A" "PROP B"
    88   show "PROP C"
    89   proof (rule r)
    90     from ab show "PROP A && PROP B" .
    91   qed
    92 next
    93   assume r: "PROP A ==> PROP B ==> PROP C"
    94   assume conj: "PROP A && PROP B"
    95   show "PROP C"
    96   proof (rule r)
    97     from conj show "PROP A" by (rule conjunctionD1)
    98     from conj show "PROP B" by (rule conjunctionD2)
    99   qed
   100 qed
   101