src/Pure/Pure.thy
author bulwahn
Tue Aug 31 08:00:53 2010 +0200 (2010-08-31)
changeset 38950 62578950e748
parent 29606 fedb8be05f24
child 48638 22d65e375c01
permissions -rw-r--r--
storing options for prolog code generation in the theory
     1 
     2 section {* Further content for the Pure theory *}
     3 
     4 subsection {* Meta-level connectives in assumptions *}
     5 
     6 lemma meta_mp:
     7   assumes "PROP P ==> PROP Q" and "PROP P"
     8   shows "PROP Q"
     9     by (rule `PROP P ==> PROP Q` [OF `PROP P`])
    10 
    11 lemmas meta_impE = meta_mp [elim_format]
    12 
    13 lemma meta_spec:
    14   assumes "!!x. PROP P x"
    15   shows "PROP P x"
    16     by (rule `!!x. PROP P x`)
    17 
    18 lemmas meta_allE = meta_spec [elim_format]
    19 
    20 lemma swap_params:
    21   "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
    22 
    23 
    24 subsection {* Meta-level conjunction *}
    25 
    26 lemma all_conjunction:
    27   "(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))"
    28 proof
    29   assume conj: "!!x. PROP A x &&& PROP B x"
    30   show "(!!x. PROP A x) &&& (!!x. PROP B x)"
    31   proof -
    32     fix x
    33     from conj show "PROP A x" by (rule conjunctionD1)
    34     from conj show "PROP B x" by (rule conjunctionD2)
    35   qed
    36 next
    37   assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)"
    38   fix x
    39   show "PROP A x &&& PROP B x"
    40   proof -
    41     show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
    42     show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
    43   qed
    44 qed
    45 
    46 lemma imp_conjunction:
    47   "(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
    48 proof
    49   assume conj: "PROP A ==> PROP B &&& PROP C"
    50   show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
    51   proof -
    52     assume "PROP A"
    53     from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
    54     from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
    55   qed
    56 next
    57   assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
    58   assume "PROP A"
    59   show "PROP B &&& PROP C"
    60   proof -
    61     from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
    62     from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
    63   qed
    64 qed
    65 
    66 lemma conjunction_imp:
    67   "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
    68 proof
    69   assume r: "PROP A &&& PROP B ==> PROP C"
    70   assume ab: "PROP A" "PROP B"
    71   show "PROP C"
    72   proof (rule r)
    73     from ab show "PROP A &&& PROP B" .
    74   qed
    75 next
    76   assume r: "PROP A ==> PROP B ==> PROP C"
    77   assume conj: "PROP A &&& PROP B"
    78   show "PROP C"
    79   proof (rule r)
    80     from conj show "PROP A" by (rule conjunctionD1)
    81     from conj show "PROP B" by (rule conjunctionD2)
    82   qed
    83 qed
    84