src/Pure/Pure.thy
author wenzelm
Tue, 06 Jun 2006 20:47:12 +0200
changeset 19800 5f764272183e
parent 19783 82f365a14960
child 20596 3950e65f48f8
permissions -rw-r--r--
removed Toplevel.debug;
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$
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
     3
*)
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     4
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
     5
header {* The Pure theory *}
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     6
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     7
theory Pure
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     8
imports ProtoPure
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     9
begin
19800
5f764272183e removed Toplevel.debug;
wenzelm
parents: 19783
diff changeset
    10
19048
2b875dd5eb4c cannot use section before setup;
wenzelm
parents: 18836
diff changeset
    11
setup  -- {* Common setup of internal components *}
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    12
18710
527aa560a9e0 tuned comments;
wenzelm
parents: 18663
diff changeset
    13
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    14
subsection {* Meta-level connectives in assumptions *}
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    15
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    16
lemma meta_mp:
18019
wenzelm
parents: 15824
diff changeset
    17
  assumes "PROP P ==> PROP Q" and "PROP P"
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    18
  shows "PROP Q"
18019
wenzelm
parents: 15824
diff changeset
    19
    by (rule `PROP P ==> PROP Q` [OF `PROP P`])
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    20
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    21
lemma meta_spec:
18019
wenzelm
parents: 15824
diff changeset
    22
  assumes "!!x. PROP P(x)"
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    23
  shows "PROP P(x)"
18019
wenzelm
parents: 15824
diff changeset
    24
    by (rule `!!x. PROP P(x)`)
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    25
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    26
lemmas meta_allE = meta_spec [elim_format]
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    27
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    28
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    29
subsection {* Meta-level conjunction *}
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    30
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    31
locale (open) meta_conjunction_syntax =
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    32
  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    33
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    34
parse_translation {*
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    35
  [("\<^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
    36
*}
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
lemma all_conjunction:
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    39
  includes meta_conjunction_syntax
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    40
  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
    41
proof
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    42
  assume conj: "!!x. PROP A(x) && PROP B(x)"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    43
  show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))"
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    44
  proof -
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    45
    fix x
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    46
    from conj show "PROP A(x)" by (rule conjunctionD1)
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    47
    from conj show "PROP B(x)" by (rule conjunctionD2)
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    48
  qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    49
next
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    50
  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
    51
  fix x
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    52
  show "PROP A(x) && PROP B(x)"
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    53
  proof -
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    54
    show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    55
    show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    56
  qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    57
qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    58
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    59
lemma imp_conjunction:
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    60
  includes meta_conjunction_syntax
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    61
  shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
18836
3a1e4ee72075 tuned proofs;
wenzelm
parents: 18710
diff changeset
    62
proof
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    63
  assume conj: "PROP A ==> PROP B && PROP C"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    64
  show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    65
  proof -
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    66
    assume "PROP A"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    67
    from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    68
    from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
18466
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
next
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    71
  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
    72
  assume "PROP A"
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    73
  show "PROP B && PROP C"
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    74
  proof -
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    75
    from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    76
    from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    77
  qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    78
qed
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    79
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    80
lemma conjunction_imp:
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    81
  includes meta_conjunction_syntax
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    82
  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
    83
proof
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    84
  assume r: "PROP A && PROP B ==> PROP C"
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    85
  assume "PROP A" and "PROP B"
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    86
  show "PROP C" by (rule r) -
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    87
next
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    88
  assume r: "PROP A ==> PROP B ==> PROP C"
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    89
  assume conj: "PROP A && PROP B"
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    90
  show "PROP C"
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    91
  proof (rule r)
19121
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    92
    from conj show "PROP A" by (rule conjunctionD1)
d7fd5415a781 simplified Pure conjunction;
wenzelm
parents: 19048
diff changeset
    93
    from conj show "PROP B" by (rule conjunctionD2)
18466
389a6f9c31f4 added locale meta_conjunction_syntax and various conjunction rules;
wenzelm
parents: 18019
diff changeset
    94
  qed
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
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    97
end