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