src/Pure/Pure.thy
author wenzelm
Wed Jan 21 22:26:49 2009 +0100 (2009-01-21)
changeset 29605 f2924219125e
parent 28856 5e009a80fe6d
child 29606 fedb8be05f24
permissions -rw-r--r--
eliminated obsolete var morphism;
wenzelm@15803
     1
(*  Title:      Pure/Pure.thy
wenzelm@15803
     2
    ID:         $Id$
wenzelm@18466
     3
*)
wenzelm@15803
     4
wenzelm@26435
     5
section {* Further content for the Pure theory *}
wenzelm@20627
     6
wenzelm@18466
     7
subsection {* Meta-level connectives in assumptions *}
wenzelm@15803
     8
wenzelm@15803
     9
lemma meta_mp:
wenzelm@18019
    10
  assumes "PROP P ==> PROP Q" and "PROP P"
wenzelm@15803
    11
  shows "PROP Q"
wenzelm@18019
    12
    by (rule `PROP P ==> PROP Q` [OF `PROP P`])
wenzelm@15803
    13
nipkow@23432
    14
lemmas meta_impE = meta_mp [elim_format]
nipkow@23432
    15
wenzelm@15803
    16
lemma meta_spec:
wenzelm@26958
    17
  assumes "!!x. PROP P x"
wenzelm@26958
    18
  shows "PROP P x"
wenzelm@26958
    19
    by (rule `!!x. PROP P x`)
wenzelm@15803
    20
wenzelm@15803
    21
lemmas meta_allE = meta_spec [elim_format]
wenzelm@15803
    22
wenzelm@26570
    23
lemma swap_params:
wenzelm@26958
    24
  "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
wenzelm@26570
    25
wenzelm@18466
    26
wenzelm@18466
    27
subsection {* Meta-level conjunction *}
wenzelm@18466
    28
wenzelm@18466
    29
lemma all_conjunction:
wenzelm@28856
    30
  "(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))"
wenzelm@18466
    31
proof
wenzelm@28856
    32
  assume conj: "!!x. PROP A x &&& PROP B x"
wenzelm@28856
    33
  show "(!!x. PROP A x) &&& (!!x. PROP B x)"
wenzelm@19121
    34
  proof -
wenzelm@18466
    35
    fix x
wenzelm@26958
    36
    from conj show "PROP A x" by (rule conjunctionD1)
wenzelm@26958
    37
    from conj show "PROP B x" by (rule conjunctionD2)
wenzelm@18466
    38
  qed
wenzelm@18466
    39
next
wenzelm@28856
    40
  assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)"
wenzelm@18466
    41
  fix x
wenzelm@28856
    42
  show "PROP A x &&& PROP B x"
wenzelm@19121
    43
  proof -
wenzelm@26958
    44
    show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
wenzelm@26958
    45
    show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
wenzelm@18466
    46
  qed
wenzelm@18466
    47
qed
wenzelm@18466
    48
wenzelm@19121
    49
lemma imp_conjunction:
wenzelm@28856
    50
  "(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
wenzelm@18836
    51
proof
wenzelm@28856
    52
  assume conj: "PROP A ==> PROP B &&& PROP C"
wenzelm@28856
    53
  show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
wenzelm@19121
    54
  proof -
wenzelm@18466
    55
    assume "PROP A"
wenzelm@19121
    56
    from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
wenzelm@19121
    57
    from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
wenzelm@18466
    58
  qed
wenzelm@18466
    59
next
wenzelm@28856
    60
  assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
wenzelm@18466
    61
  assume "PROP A"
wenzelm@28856
    62
  show "PROP B &&& PROP C"
wenzelm@19121
    63
  proof -
wenzelm@19121
    64
    from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
wenzelm@19121
    65
    from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
wenzelm@18466
    66
  qed
wenzelm@18466
    67
qed
wenzelm@18466
    68
wenzelm@18466
    69
lemma conjunction_imp:
wenzelm@28856
    70
  "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
wenzelm@18466
    71
proof
wenzelm@28856
    72
  assume r: "PROP A &&& PROP B ==> PROP C"
wenzelm@22933
    73
  assume ab: "PROP A" "PROP B"
wenzelm@22933
    74
  show "PROP C"
wenzelm@22933
    75
  proof (rule r)
wenzelm@28856
    76
    from ab show "PROP A &&& PROP B" .
wenzelm@22933
    77
  qed
wenzelm@18466
    78
next
wenzelm@18466
    79
  assume r: "PROP A ==> PROP B ==> PROP C"
wenzelm@28856
    80
  assume conj: "PROP A &&& PROP B"
wenzelm@18466
    81
  show "PROP C"
wenzelm@18466
    82
  proof (rule r)
wenzelm@19121
    83
    from conj show "PROP A" by (rule conjunctionD1)
wenzelm@19121
    84
    from conj show "PROP B" by (rule conjunctionD2)
wenzelm@18466
    85
  qed
wenzelm@18466
    86
qed
wenzelm@18466
    87