--- a/src/HOL/Import/MakeEqual.thy Sun Mar 04 00:03:21 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-(* Title: HOL/Import/MakeEqual.thy
- Author: Sebastian Skalberg, TU Muenchen
-*)
-
-theory MakeEqual imports Main
- uses "shuffler.ML" begin
-
-setup Shuffler.setup
-
-lemma conj_norm [shuffle_rule]: "(A & B ==> PROP C) == ([| A ; B |] ==> PROP C)"
-proof
- assume "A & B ==> PROP C" A B
- thus "PROP C"
- by auto
-next
- assume "[| A; B |] ==> PROP C" "A & B"
- thus "PROP C"
- by auto
-qed
-
-lemma imp_norm [shuffle_rule]: "(Trueprop (A --> B)) == (A ==> B)"
-proof
- assume "A --> B" A
- thus B ..
-next
- assume "A ==> B"
- thus "A --> B"
- by auto
-qed
-
-lemma all_norm [shuffle_rule]: "(Trueprop (ALL x. P x)) == (!!x. P x)"
-proof
- fix x
- assume "ALL x. P x"
- thus "P x" ..
-next
- assume "!!x. P x"
- thus "ALL x. P x"
- ..
-qed
-
-lemma ex_norm [shuffle_rule]: "(EX x. P x ==> PROP Q) == (!!x. P x ==> PROP Q)"
-proof
- fix x
- assume ex: "EX x. P x ==> PROP Q"
- assume "P x"
- hence "EX x. P x" ..
- with ex show "PROP Q" .
-next
- assume allx: "!!x. P x ==> PROP Q"
- assume "EX x. P x"
- hence p: "P (SOME x. P x)"
- ..
- from allx
- have "P (SOME x. P x) ==> PROP Q"
- .
- with p
- show "PROP Q"
- by auto
-qed
-
-lemma eq_norm [shuffle_rule]: "Trueprop (t = u) == (t == u)"
-proof
- assume "t = u"
- thus "t == u" by simp
-next
- assume "t == u"
- thus "t = u"
- by simp
-qed
-
-end