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