src/Pure/Pure.thy
author wenzelm
Sat, 23 Apr 2005 19:49:39 +0200
changeset 15824 222eeb9655f3
parent 15803 42c75e0c9140
child 18019 d1ff9ebb8bcb
permissions -rw-r--r--
tuned proofs;
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$
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     3
    Author:     Larry Paulson and Makarius
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     4
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     5
The Pure theory.
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     6
*)
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     7
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     8
theory Pure
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
     9
imports ProtoPure
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    10
begin
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    11
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    12
setup "Context.setup ()"
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    13
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    14
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    15
text{*These meta-level elimination rules facilitate the use of assumptions
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    16
that contain !! and ==>, especially in linear scripts. *}
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    17
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    18
lemma meta_mp:
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    19
  assumes major: "PROP P ==> PROP Q" and minor: "PROP P"
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    20
  shows "PROP Q"
15824
222eeb9655f3 tuned proofs;
wenzelm
parents: 15803
diff changeset
    21
    by (rule major [OF minor])
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    22
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    23
lemma meta_spec:
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    24
  assumes major: "!!x. PROP P(x)"
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    25
  shows "PROP P(x)"
15824
222eeb9655f3 tuned proofs;
wenzelm
parents: 15803
diff changeset
    26
    by (rule major)
15803
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    27
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    28
lemmas meta_allE = meta_spec [elim_format]
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    29
42c75e0c9140 The Pure theory.
wenzelm
parents:
diff changeset
    30
end