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