src/Pure/Pure.thy
author wenzelm
Sun Jan 29 19:23:43 2006 +0100 (2006-01-29)
changeset 18836 3a1e4ee72075
parent 18710 527aa560a9e0
child 19048 2b875dd5eb4c
permissions -rw-r--r--
tuned proofs;
wenzelm@15803
     1
(*  Title:      Pure/Pure.thy
wenzelm@15803
     2
    ID:         $Id$
wenzelm@18710
     3
wenzelm@18710
     4
The actual Pure theory.
wenzelm@18466
     5
*)
wenzelm@15803
     6
wenzelm@18466
     7
header {* The Pure theory *}
wenzelm@15803
     8
wenzelm@15803
     9
theory Pure
wenzelm@15803
    10
imports ProtoPure
wenzelm@15803
    11
begin
wenzelm@15803
    12
wenzelm@18710
    13
subsection {* Common setup of internal components *}
wenzelm@18710
    14
wenzelm@18663
    15
setup
wenzelm@15803
    16
wenzelm@18710
    17
wenzelm@18466
    18
subsection {* Meta-level connectives in assumptions *}
wenzelm@15803
    19
wenzelm@15803
    20
lemma meta_mp:
wenzelm@18019
    21
  assumes "PROP P ==> PROP Q" and "PROP P"
wenzelm@15803
    22
  shows "PROP Q"
wenzelm@18019
    23
    by (rule `PROP P ==> PROP Q` [OF `PROP P`])
wenzelm@15803
    24
wenzelm@15803
    25
lemma meta_spec:
wenzelm@18019
    26
  assumes "!!x. PROP P(x)"
wenzelm@15803
    27
  shows "PROP P(x)"
wenzelm@18019
    28
    by (rule `!!x. PROP P(x)`)
wenzelm@15803
    29
wenzelm@15803
    30
lemmas meta_allE = meta_spec [elim_format]
wenzelm@15803
    31
wenzelm@18466
    32
wenzelm@18466
    33
subsection {* Meta-level conjunction *}
wenzelm@18466
    34
wenzelm@18466
    35
locale (open) meta_conjunction_syntax =
wenzelm@18466
    36
  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
wenzelm@18466
    37
wenzelm@18466
    38
parse_translation {*
wenzelm@18466
    39
  [("\<^fixed>meta_conjunction", fn [t, u] => Logic.mk_conjunction (t, u))]
wenzelm@18466
    40
*}
wenzelm@18466
    41
wenzelm@18466
    42
lemma all_conjunction:
wenzelm@18466
    43
  includes meta_conjunction_syntax
wenzelm@18466
    44
  shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
wenzelm@18466
    45
proof
wenzelm@18466
    46
  assume conj: "!!x. PROP A(x) && PROP B(x)"
wenzelm@18466
    47
  fix X assume r: "(!!x. PROP A(x)) ==> (!!x. PROP B(x)) ==> PROP X"
wenzelm@18466
    48
  show "PROP X"
wenzelm@18466
    49
  proof (rule r)
wenzelm@18466
    50
    fix x
wenzelm@18466
    51
    from conj show "PROP A(x)" .
wenzelm@18466
    52
    from conj show "PROP B(x)" .
wenzelm@18466
    53
  qed
wenzelm@18466
    54
next
wenzelm@18466
    55
  assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
wenzelm@18466
    56
  fix x
wenzelm@18466
    57
  fix X assume r: "PROP A(x) ==> PROP B(x) ==> PROP X"
wenzelm@18466
    58
  show "PROP X"
wenzelm@18466
    59
  proof (rule r)
wenzelm@18466
    60
    show "PROP A(x)"
wenzelm@18466
    61
    proof (rule conj)
wenzelm@18466
    62
      assume "!!x. PROP A(x)"
wenzelm@18466
    63
      then show "PROP A(x)" .
wenzelm@18466
    64
    qed
wenzelm@18466
    65
    show "PROP B(x)"
wenzelm@18466
    66
    proof (rule conj)
wenzelm@18466
    67
      assume "!!x. PROP B(x)"
wenzelm@18466
    68
      then show "PROP B(x)" .
wenzelm@18466
    69
    qed
wenzelm@18466
    70
  qed
wenzelm@18466
    71
qed
wenzelm@18466
    72
wenzelm@18466
    73
lemma imp_conjunction [unfolded prop_def]:
wenzelm@18466
    74
  includes meta_conjunction_syntax
wenzelm@18466
    75
  shows "(PROP A ==> PROP prop (PROP B && PROP C)) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
wenzelm@18836
    76
  unfolding prop_def
wenzelm@18836
    77
proof
wenzelm@18466
    78
  assume conj: "PROP A ==> PROP B && PROP C"
wenzelm@18466
    79
  fix X assume r: "(PROP A ==> PROP B) ==> (PROP A ==> PROP C) ==> PROP X"
wenzelm@18466
    80
  show "PROP X"
wenzelm@18466
    81
  proof (rule r)
wenzelm@18466
    82
    assume "PROP A"
wenzelm@18466
    83
    from conj [OF `PROP A`] show "PROP B" .
wenzelm@18466
    84
    from conj [OF `PROP A`] show "PROP C" .
wenzelm@18466
    85
  qed
wenzelm@18466
    86
next
wenzelm@18466
    87
  assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
wenzelm@18466
    88
  assume "PROP A"
wenzelm@18466
    89
  fix X assume r: "PROP B ==> PROP C ==> PROP X"
wenzelm@18466
    90
  show "PROP X"
wenzelm@18466
    91
  proof (rule r)
wenzelm@18466
    92
    show "PROP B"
wenzelm@18466
    93
    proof (rule conj)
wenzelm@18466
    94
      assume "PROP A ==> PROP B"
wenzelm@18466
    95
      from this [OF `PROP A`] show "PROP B" .
wenzelm@18466
    96
    qed
wenzelm@18466
    97
    show "PROP C"
wenzelm@18466
    98
    proof (rule conj)
wenzelm@18466
    99
      assume "PROP A ==> PROP C"
wenzelm@18466
   100
      from this [OF `PROP A`] show "PROP C" .
wenzelm@18466
   101
    qed
wenzelm@18466
   102
  qed
wenzelm@18466
   103
qed
wenzelm@18466
   104
wenzelm@18466
   105
lemma conjunction_imp:
wenzelm@18466
   106
  includes meta_conjunction_syntax
wenzelm@18466
   107
  shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
wenzelm@18466
   108
proof
wenzelm@18466
   109
  assume r: "PROP A && PROP B ==> PROP C"
wenzelm@18466
   110
  assume "PROP A" and "PROP B"
wenzelm@18466
   111
  show "PROP C" by (rule r) -
wenzelm@18466
   112
next
wenzelm@18466
   113
  assume r: "PROP A ==> PROP B ==> PROP C"
wenzelm@18466
   114
  assume conj: "PROP A && PROP B"
wenzelm@18466
   115
  show "PROP C"
wenzelm@18466
   116
  proof (rule r)
wenzelm@18466
   117
    from conj show "PROP A" .
wenzelm@18466
   118
    from conj show "PROP B" .
wenzelm@18466
   119
  qed
wenzelm@18466
   120
qed
wenzelm@18466
   121
wenzelm@18466
   122
lemma conjunction_assoc:
wenzelm@18466
   123
  includes meta_conjunction_syntax
wenzelm@18466
   124
  shows "((PROP A && PROP B) && PROP C) == (PROP A && (PROP B && PROP C))"
wenzelm@18836
   125
  unfolding conjunction_imp .
wenzelm@18466
   126
wenzelm@15803
   127
end