| author | wenzelm |
| Fri, 03 Dec 2010 20:38:58 +0100 | |
| changeset 40945 | b8703f63bfb2 |
| parent 16417 | 9bc16273c2d4 |
| child 41589 | bbd861837ebc |
| permissions | -rw-r--r-- |
|
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
1 |
(* Title: HOL/Import/MakeEqual.thy |
|
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
2 |
ID: $Id$ |
|
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
3 |
Author: Sebastian Skalberg (TU Muenchen) |
|
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
4 |
*) |
|
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14516
diff
changeset
|
5 |
|
| 16417 | 6 |
theory MakeEqual imports Main |
7 |
uses "shuffler.ML" begin |
|
| 14516 | 8 |
|
9 |
setup Shuffler.setup |
|
10 |
||
11 |
lemma conj_norm [shuffle_rule]: "(A & B ==> PROP C) == ([| A ; B |] ==> PROP C)" |
|
12 |
proof |
|
13 |
assume "A & B ==> PROP C" A B |
|
14 |
thus "PROP C" |
|
15 |
by auto |
|
16 |
next |
|
17 |
assume "[| A; B |] ==> PROP C" "A & B" |
|
18 |
thus "PROP C" |
|
19 |
by auto |
|
20 |
qed |
|
21 |
||
22 |
lemma imp_norm [shuffle_rule]: "(Trueprop (A --> B)) == (A ==> B)" |
|
23 |
proof |
|
24 |
assume "A --> B" A |
|
25 |
thus B .. |
|
26 |
next |
|
27 |
assume "A ==> B" |
|
28 |
thus "A --> B" |
|
29 |
by auto |
|
30 |
qed |
|
31 |
||
32 |
lemma all_norm [shuffle_rule]: "(Trueprop (ALL x. P x)) == (!!x. P x)" |
|
33 |
proof |
|
34 |
fix x |
|
35 |
assume "ALL x. P x" |
|
36 |
thus "P x" .. |
|
37 |
next |
|
38 |
assume "!!x. P x" |
|
39 |
thus "ALL x. P x" |
|
40 |
.. |
|
41 |
qed |
|
42 |
||
43 |
lemma ex_norm [shuffle_rule]: "(EX x. P x ==> PROP Q) == (!!x. P x ==> PROP Q)" |
|
44 |
proof |
|
45 |
fix x |
|
46 |
assume ex: "EX x. P x ==> PROP Q" |
|
47 |
assume "P x" |
|
48 |
hence "EX x. P x" .. |
|
49 |
with ex show "PROP Q" . |
|
50 |
next |
|
51 |
assume allx: "!!x. P x ==> PROP Q" |
|
52 |
assume "EX x. P x" |
|
53 |
hence p: "P (SOME x. P x)" |
|
54 |
.. |
|
55 |
from allx |
|
56 |
have "P (SOME x. P x) ==> PROP Q" |
|
57 |
. |
|
58 |
with p |
|
59 |
show "PROP Q" |
|
60 |
by auto |
|
61 |
qed |
|
62 |
||
63 |
lemma eq_norm [shuffle_rule]: "Trueprop (t = u) == (t == u)" |
|
64 |
proof |
|
65 |
assume "t = u" |
|
66 |
thus "t == u" by simp |
|
67 |
next |
|
68 |
assume "t == u" |
|
69 |
thus "t = u" |
|
70 |
by simp |
|
71 |
qed |
|
72 |
||
73 |
end |