src/Pure/Pure.thy
author wenzelm
Mon Apr 07 21:25:21 2008 +0200 (2008-04-07)
changeset 26570 dbc458262f4c
parent 26435 bdce320cd426
child 26572 9178a7f4c4c8
permissions -rw-r--r--
added swap_params;
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@18019
    17
  assumes "!!x. PROP P(x)"
wenzelm@15803
    18
  shows "PROP P(x)"
wenzelm@18019
    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@26570
    24
  "(\<And>x y. PROP P(x, y)) == (\<And>y x. PROP P(x, y))" ..
wenzelm@26570
    25
wenzelm@18466
    26
wenzelm@21625
    27
subsection {* Embedded terms *}
wenzelm@21625
    28
wenzelm@21625
    29
locale (open) meta_term_syntax =
wenzelm@21625
    30
  fixes meta_term :: "'a => prop"  ("TERM _")
wenzelm@21625
    31
wenzelm@21625
    32
lemmas [intro?] = termI
wenzelm@21625
    33
wenzelm@21625
    34
wenzelm@18466
    35
subsection {* Meta-level conjunction *}
wenzelm@18466
    36
wenzelm@18466
    37
locale (open) meta_conjunction_syntax =
wenzelm@18466
    38
  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
wenzelm@18466
    39
wenzelm@18466
    40
lemma all_conjunction:
wenzelm@18466
    41
  includes meta_conjunction_syntax
wenzelm@18466
    42
  shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
wenzelm@18466
    43
proof
wenzelm@18466
    44
  assume conj: "!!x. PROP A(x) && PROP B(x)"
wenzelm@19121
    45
  show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))"
wenzelm@19121
    46
  proof -
wenzelm@18466
    47
    fix x
wenzelm@19121
    48
    from conj show "PROP A(x)" by (rule conjunctionD1)
wenzelm@19121
    49
    from conj show "PROP B(x)" by (rule conjunctionD2)
wenzelm@18466
    50
  qed
wenzelm@18466
    51
next
wenzelm@18466
    52
  assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
wenzelm@18466
    53
  fix x
wenzelm@19121
    54
  show "PROP A(x) && PROP B(x)"
wenzelm@19121
    55
  proof -
wenzelm@19121
    56
    show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
wenzelm@19121
    57
    show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
wenzelm@18466
    58
  qed
wenzelm@18466
    59
qed
wenzelm@18466
    60
wenzelm@19121
    61
lemma imp_conjunction:
wenzelm@18466
    62
  includes meta_conjunction_syntax
wenzelm@19121
    63
  shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
wenzelm@18836
    64
proof
wenzelm@18466
    65
  assume conj: "PROP A ==> PROP B && PROP C"
wenzelm@19121
    66
  show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
wenzelm@19121
    67
  proof -
wenzelm@18466
    68
    assume "PROP A"
wenzelm@19121
    69
    from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
wenzelm@19121
    70
    from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
wenzelm@18466
    71
  qed
wenzelm@18466
    72
next
wenzelm@18466
    73
  assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
wenzelm@18466
    74
  assume "PROP A"
wenzelm@19121
    75
  show "PROP B && PROP C"
wenzelm@19121
    76
  proof -
wenzelm@19121
    77
    from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
wenzelm@19121
    78
    from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
wenzelm@18466
    79
  qed
wenzelm@18466
    80
qed
wenzelm@18466
    81
wenzelm@18466
    82
lemma conjunction_imp:
wenzelm@18466
    83
  includes meta_conjunction_syntax
wenzelm@18466
    84
  shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
wenzelm@18466
    85
proof
wenzelm@18466
    86
  assume r: "PROP A && PROP B ==> PROP C"
wenzelm@22933
    87
  assume ab: "PROP A" "PROP B"
wenzelm@22933
    88
  show "PROP C"
wenzelm@22933
    89
  proof (rule r)
wenzelm@22933
    90
    from ab show "PROP A && PROP B" .
wenzelm@22933
    91
  qed
wenzelm@18466
    92
next
wenzelm@18466
    93
  assume r: "PROP A ==> PROP B ==> PROP C"
wenzelm@18466
    94
  assume conj: "PROP A && PROP B"
wenzelm@18466
    95
  show "PROP C"
wenzelm@18466
    96
  proof (rule r)
wenzelm@19121
    97
    from conj show "PROP A" by (rule conjunctionD1)
wenzelm@19121
    98
    from conj show "PROP B" by (rule conjunctionD2)
wenzelm@18466
    99
  qed
wenzelm@18466
   100
qed
wenzelm@18466
   101