| author | skalberg |
| Fri, 02 Apr 2004 17:37:45 +0200 | |
| changeset 14516 | a183dec876ab |
| child 14620 | 1be590fd2422 |
| permissions | -rw-r--r-- |
1 theory MakeEqual = Main
2 files "shuffler.ML":
4 setup Shuffler.setup
6 lemma conj_norm [shuffle_rule]: "(A & B ==> PROP C) == ([| A ; B |] ==> PROP C)"
7 proof
8 assume "A & B ==> PROP C" A B
9 thus "PROP C"
10 by auto
11 next
12 assume "[| A; B |] ==> PROP C" "A & B"
13 thus "PROP C"
14 by auto
15 qed
17 lemma imp_norm [shuffle_rule]: "(Trueprop (A --> B)) == (A ==> B)"
18 proof
19 assume "A --> B" A
20 thus B ..
21 next
22 assume "A ==> B"
23 thus "A --> B"
24 by auto
25 qed
27 lemma all_norm [shuffle_rule]: "(Trueprop (ALL x. P x)) == (!!x. P x)"
28 proof
29 fix x
30 assume "ALL x. P x"
31 thus "P x" ..
32 next
33 assume "!!x. P x"
34 thus "ALL x. P x"
35 ..
36 qed
38 lemma ex_norm [shuffle_rule]: "(EX x. P x ==> PROP Q) == (!!x. P x ==> PROP Q)"
39 proof
40 fix x
41 assume ex: "EX x. P x ==> PROP Q"
42 assume "P x"
43 hence "EX x. P x" ..
44 with ex show "PROP Q" .
45 next
46 assume allx: "!!x. P x ==> PROP Q"
47 assume "EX x. P x"
48 hence p: "P (SOME x. P x)"
49 ..
50 from allx
51 have "P (SOME x. P x) ==> PROP Q"
52 .
53 with p
54 show "PROP Q"
55 by auto
56 qed
58 lemma eq_norm [shuffle_rule]: "Trueprop (t = u) == (t == u)"
59 proof
60 assume "t = u"
61 thus "t == u" by simp
62 next
63 assume "t == u"
64 thus "t = u"
65 by simp
66 qed
68 end