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