--- a/Prove.thy	Mon Oct 12 22:44:16 2009 +0200
+++ b/Prove.thy	Mon Oct 12 23:06:14 2009 +0200
@@ -1,7 +1,148 @@
 theory Prove
-imports Main
+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)"
 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)
 *}