--- a/Prove.thy	Tue Oct 13 00:02:22 2009 +0200
+++ b/Prove.thy	Tue Oct 13 09:26:19 2009 +0200
@@ -1,148 +1,7 @@
 theory Prove
-imports Main QuotScript QuotList
-uses ("quotient.ML")
-begin
-
-locale QUOT_TYPE =
-  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-  and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
-  and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
-  assumes equiv: "EQUIV R"
-  and     rep_prop: "\<And>y. \<exists>x. Rep y = R x"
-  and     rep_inverse: "\<And>x. Abs (Rep x) = x"
-  and     abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
-  and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
+imports Main 
 begin
 
-definition
-  "ABS x \<equiv> Abs (R x)"
-
-definition
-  "REP a = Eps (Rep a)"
-
-lemma lem9:
-  shows "R (Eps (R x)) = R x"
-proof -
-  have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
-  then have "R x (Eps (R x))" by (rule someI)
-  then show "R (Eps (R x)) = R x"
-    using equiv unfolding EQUIV_def by simp
-qed
-
-theorem thm10:
-  shows "ABS (REP a) \<equiv> a"
-  apply  (rule eq_reflection)
-  unfolding ABS_def REP_def
-proof -
-  from rep_prop
-  obtain x where eq: "Rep a = R x" by auto
-  have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
-  also have "\<dots> = Abs (R x)" using lem9 by simp
-  also have "\<dots> = Abs (Rep a)" using eq by simp
-  also have "\<dots> = a" using rep_inverse by simp
-  finally
-  show "Abs (R (Eps (Rep a))) = a" by simp
-qed
-
-lemma REP_refl:
-  shows "R (REP a) (REP a)"
-unfolding REP_def
-by (simp add: equiv[simplified EQUIV_def])
-
-lemma lem7:
-  shows "(R x = R y) = (Abs (R x) = Abs (R y))"
-apply(rule iffI)
-apply(simp)
-apply(drule rep_inject[THEN iffD2])
-apply(simp add: abs_inverse)
-done
-
-theorem thm11:
-  shows "R r r' = (ABS r = ABS r')"
-unfolding ABS_def
-by (simp only: equiv[simplified EQUIV_def] lem7)
-
-
-lemma REP_ABS_rsp:
-  shows "R f (REP (ABS g)) = R f g"
-  and   "R (REP (ABS g)) f = R g f"
-by (simp_all add: thm10 thm11)
-
-lemma QUOTIENT:
-  "QUOTIENT R ABS REP"
-apply(unfold QUOTIENT_def)
-apply(simp add: thm10)
-apply(simp add: REP_refl)
-apply(subst thm11[symmetric])
-apply(simp add: equiv[simplified EQUIV_def])
-done
-
-lemma R_trans:
-  assumes ab: "R a b"
-  and     bc: "R b c"
-  shows "R a c"
-proof -
-  have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
-  moreover have ab: "R a b" by fact
-  moreover have bc: "R b c" by fact
-  ultimately show "R a c" unfolding TRANS_def by blast
-qed
-
-lemma R_sym:
-  assumes ab: "R a b"
-  shows "R b a"
-proof -
-  have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
-  then show "R b a" using ab unfolding SYM_def by blast
-qed
-
-lemma R_trans2:
-  assumes ac: "R a c"
-  and     bd: "R b d"
-  shows "R a b = R c d"
-proof
-  assume "R a b"
-  then have "R b a" using R_sym by blast
-  then have "R b c" using ac R_trans by blast
-  then have "R c b" using R_sym by blast
-  then show "R c d" using bd R_trans by blast
-next
-  assume "R c d"
-  then have "R a d" using ac R_trans by blast
-  then have "R d a" using R_sym by blast
-  then have "R b a" using bd R_trans by blast
-  then show "R a b" using R_sym by blast
-qed
-
-lemma REPS_same:
-  shows "R (REP a) (REP b) \<equiv> (a = b)"
-proof -
-  have "R (REP a) (REP b) = (a = b)"
-  proof
-    assume as: "R (REP a) (REP b)"
-    from rep_prop
-    obtain x y
-      where eqs: "Rep a = R x" "Rep b = R y" by blast
-    from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
-    then have "R x (Eps (R y))" using lem9 by simp
-    then have "R (Eps (R y)) x" using R_sym by blast
-    then have "R y x" using lem9 by simp
-    then have "R x y" using R_sym by blast
-    then have "ABS x = ABS y" using thm11 by simp
-    then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
-    then show "a = b" using rep_inverse by simp
-  next
-    assume ab: "a = b"
-    have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
-    then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto
-  qed
-  then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
-qed
-
-end
-
-use "quotient.ML"
-
 ML {*
 val r = ref (NONE:(unit -> term) option)
 *}