src/HOL/Import/MakeEqual.thy
 author nipkow Wed Aug 18 11:09:40 2004 +0200 (2004-08-18) changeset 15140 322485b816ac parent 14620 1be590fd2422 child 16417 9bc16273c2d4 permissions -rw-r--r--
import -> imports
1 (*  Title:      HOL/Import/MakeEqual.thy
2     ID:         \$Id\$
3     Author:     Sebastian Skalberg (TU Muenchen)
4 *)
6 theory MakeEqual = Main
7   files "shuffler.ML":
9 setup Shuffler.setup
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
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
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
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
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
73 end