src/Pure/Pure.thy
author wenzelm
Sat Dec 13 15:00:39 2008 +0100 (2008-12-13)
changeset 29091 b81fe045e799
parent 28856 5e009a80fe6d
child 29606 fedb8be05f24
permissions -rw-r--r--
Context.display_names;
     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 {* Meta-level conjunction *}
    28 
    29 lemma all_conjunction:
    30   "(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))"
    31 proof
    32   assume conj: "!!x. PROP A x &&& PROP B x"
    33   show "(!!x. PROP A x) &&& (!!x. PROP B x)"
    34   proof -
    35     fix x
    36     from conj show "PROP A x" by (rule conjunctionD1)
    37     from conj show "PROP B x" by (rule conjunctionD2)
    38   qed
    39 next
    40   assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)"
    41   fix x
    42   show "PROP A x &&& PROP B x"
    43   proof -
    44     show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
    45     show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
    46   qed
    47 qed
    48 
    49 lemma imp_conjunction:
    50   "(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
    51 proof
    52   assume conj: "PROP A ==> PROP B &&& PROP C"
    53   show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
    54   proof -
    55     assume "PROP A"
    56     from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
    57     from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
    58   qed
    59 next
    60   assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
    61   assume "PROP A"
    62   show "PROP B &&& PROP C"
    63   proof -
    64     from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
    65     from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
    66   qed
    67 qed
    68 
    69 lemma conjunction_imp:
    70   "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
    71 proof
    72   assume r: "PROP A &&& PROP B ==> PROP C"
    73   assume ab: "PROP A" "PROP B"
    74   show "PROP C"
    75   proof (rule r)
    76     from ab show "PROP A &&& PROP B" .
    77   qed
    78 next
    79   assume r: "PROP A ==> PROP B ==> PROP C"
    80   assume conj: "PROP A &&& PROP B"
    81   show "PROP C"
    82   proof (rule r)
    83     from conj show "PROP A" by (rule conjunctionD1)
    84     from conj show "PROP B" by (rule conjunctionD2)
    85   qed
    86 qed
    87