# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259938883 -3600
# Node ID bce41bea3de26b1f3fc5ef957cb5133f624e75df
# Parent  57073b0b8fac7bf55b6e29498147ea41f2ce66d9
Cleaning in Quotients

diff -r 57073b0b8fac -r bce41bea3de2 Quotients.thy
--- a/Quotients.thy	Fri Dec 04 15:50:57 2009 +0100
+++ b/Quotients.thy	Fri Dec 04 16:01:23 2009 +0100
@@ -3,75 +3,8 @@
 begin
 
 definition
-  "REFL E \<equiv> \<forall>x. E x x"
-
-definition 
-  "SYM E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
-
-definition
-  "TRANS E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
-
-definition
   "NONEMPTY E \<equiv> \<exists>x. E x x"
 
-definition 
-  "EQUIV E \<equiv> REFL E \<and> SYM E \<and> TRANS E" 
-
-definition 
-  "EQUIV_PROP E \<equiv> (\<forall>x y. E x y = (E x = E y))"
-
-lemma EQUIV_PROP_EQUALITY:
-  shows "EQUIV_PROP (op =)"
-unfolding EQUIV_PROP_def expand_fun_eq
-by (blast)
-
-lemma EQUIV_implies_EQUIV_PROP:
-  assumes a: "REFL E"
-  and     b: "SYM E"
-  and     c: "TRANS E"
-  shows "EQUIV_PROP E"
-using a b c
-unfolding EQUIV_PROP_def REFL_def SYM_def TRANS_def expand_fun_eq
-by (metis)
-
-lemma EQUIV_PROP_implies_REFL:
-  assumes a: "EQUIV_PROP E"
-  shows "REFL E"
-using a
-unfolding EQUIV_PROP_def REFL_def expand_fun_eq
-by (metis)
-
-lemma EQUIV_PROP_implies_SYM:
-  assumes a: "EQUIV_PROP E"
-  shows "SYM E"
-using a
-unfolding EQUIV_PROP_def SYM_def expand_fun_eq
-by (metis)
-
-lemma EQUIV_PROP_implies_TRANS:
-  assumes a: "EQUIV_PROP E"
-  shows "TRANS E"
-using a
-unfolding EQUIV_PROP_def TRANS_def expand_fun_eq
-by (blast)
-
-ML {* 
-fun equiv_refl thm = thm RS @{thm EQUIV_PROP_implies_REFL} 
-fun equiv_sym thm = thm RS @{thm EQUIV_PROP_implies_SYM} 
-fun equiv_trans thm = thm RS @{thm EQUIV_PROP_implies_TRANS} 
-
-fun refl_sym_trans_equiv thm1 thm2 thm3 = [thm1,thm2,thm3] MRS @{thm EQUIV_implies_EQUIV_PROP} 
-*}
-
-
-fun
-  LIST_REL
-where
-  "LIST_REL R [] [] = True"
-| "LIST_REL R (x#xs) [] = False"
-| "LIST_REL R [] (x#xs) = False"
-| "LIST_REL R (x#xs) (y#ys) = (R x y \<and> LIST_REL R xs ys)"
-
 fun 
   OPTION_REL 
 where
@@ -97,7 +30,7 @@
   "prod_map f1 f2 (a,b) = (f1 a, f2 b)"
 
 fun
-  SUM_REL  
+  SUM_REL
 where
   "SUM_REL R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
 | "SUM_REL R1 R2 (Inl a1) (Inr b2) = False"
@@ -110,31 +43,11 @@
   "sum_map f1 f2 (Inl a) = Inl (f1 a)"
 | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
 
-fun
-  FUN_REL 
-where
-  "FUN_REL R1 R2 f g = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
-
-fun
-  fun_map
-where
-  "fun_map f g h x = g (h (f x))" 
-
-definition 
-  "QUOTIENT_ABS_REP Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a)"
-
-
-
 definition
   "QUOTIENT R Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and> 
                         (\<forall>a. R (Rep a) (Rep a)) \<and> 
                         (\<forall>r s. R r s = (R r r \<and> R s s \<and> (Abs r = Abs s)))"
 
-lemma QUOTIENT_ID:
-  shows "QUOTIENT (op =) id id"
-unfolding QUOTIENT_def id_def
-by (blast)
-
 lemma QUOTIENT_PROD:
   assumes a: "QUOTIENT E1 Abs1 Rep1"
   and     b: "QUOTIENT E2 Abs2 Rep2"
@@ -152,261 +65,3 @@
 apply(auto)
 done
 
-definition
-  eqclass ("[_]_")
-where
-  "[x]E \<equiv> E x"
-
-definition
- QUOTIENT_SET :: "'a set \<Rightarrow> ('a \<Rightarrow>'a\<Rightarrow>bool) \<Rightarrow> ('a set) set" ("_'/#'/_")
-where
- "S/#/E = {[x]E | x. x\<in>S}"
-
-definition
- QUOTIENT_UNIV
-where
- "QUOTIENT_UNIV TYPE('a) E \<equiv> (UNIV::'a set)/#/E"
-
-consts MY::"'a\<Rightarrow>'a\<Rightarrow>bool"
-axioms my1: "REFL MY"
-axioms my2: "SYM MY"
-axioms my3: "TRANS MY"
-
-term "QUOTIENT_UNIV TYPE('a) MY"
-term "\<lambda>f. \<exists>x. f = [x]MY"
-
-typedef 'a quot = "\<lambda>f::'a\<Rightarrow>bool. \<exists>x. f = [x]MY"
-by (auto simp add: mem_def)
-
-thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quot
-thm Abs_quot_cases Rep_quot_cases Abs_quot_induct Rep_quot_induct
-
-lemma lem2:
-  shows "([x]MY = [y]MY) = MY x y"
-apply(rule iffI)
-apply(simp add: eqclass_def)
-using my1
-apply(auto simp add: REFL_def)[1]
-apply(simp add: eqclass_def expand_fun_eq)
-apply(rule allI)
-apply(rule iffI)
-apply(subgoal_tac "MY y x")
-using my3
-apply(simp add: TRANS_def)[1]
-apply(drule_tac x="y" in spec)
-apply(drule_tac x="x" in spec)
-apply(drule_tac x="xa" in spec)
-apply(simp)
-using my2
-apply(simp add: SYM_def)[1]
-oops
-
-lemma lem6:
-  "\<forall>a. \<exists>r. Rep_quot a = [r]MY"
-apply(rule allI)
-apply(subgoal_tac "Rep_quot a \<in> quot")
-apply(simp add: quot_def mem_def)
-apply(rule Rep_quot)
-done
-
-lemma lem7:
-  "\<forall>x y. (Abs_quot ([x]MY) = Abs_quot ([y]MY)) = ([x]MY = [y]MY)"
-apply(subst Abs_quot_inject)
-apply(unfold quot_def mem_def)
-apply(auto)
-done
-
-definition
-  "Abs x = Abs_quot ([x]MY)"
-
-definition
-  "Rep a = Eps (Rep_quot a)"
-
-lemma lem9:
-  "\<forall>r. [(Eps [r]MY)]MY = [r]MY"
-apply(rule allI)
-apply(subgoal_tac "MY r r \<Longrightarrow> MY r (Eps (MY r))")
-apply(drule meta_mp)
-apply(rule eq1[THEN spec])
-
-
-apply(rule_tac x="MY r" in someI)
-
-lemma 
-  "(f \<in> UNIV/#/MY) = (Rep_quot (Abs_quot f) = f)"
-apply(simp add: QUOTIENT_SET_def)
-apply(auto)
-apply(subgoal_tac "[x]MY \<in> quot")
-apply(simp add: Abs_quot_inverse)
-apply(simp add: quot_def)
-apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)
-apply(auto)[1]
-apply(subgoal_tac "[x]MY \<in> quot")
-apply(simp add: Abs_quot_inverse)
-apply(simp add: quot_def)
-apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)
-apply(auto)[1]
-apply(subst expand_set_eq)
-thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quot
-
-lemma
-  "\<forall>a. \<exists>r. Rep_quot a = [r]MY"
-apply(rule allI)
-apply(subst Abs_quot_inject[symmetric])
-apply(rule Rep_quot)
-apply(simp add: quot_def)
-apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)
-apply(auto)[1]
-apply(simp add: Rep_quot_inverse)
-thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quot
-apply(subst Abs_quot_inject[symmetric])
-proof -
-  have "[r]MY \<in> quot"
-    apply(simp add: quot_def)
-    apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)
-    apply(auto)
-
-thm Abs_quot_inverse
-
-
-thm Abs_quot_inverse
-apply(simp add: Rep_quot_inverse)
-
-
-thm Rep_quot_inverse
-
-term ""
-
-lemma
-  assumes a: "EQUIV2 E"
-  shows "([x]E = [y]E) = E x y"
-using a
-by (simp add: eqclass_def EQUIV2_def)
-
-
-
-
-
-lemma 
-  shows "QUOTIENT (op =) (\<lambda>x. x) (\<lambda>x. x)"
-apply(unfold QUOTIENT_def)
-apply(blast)
-done
-
-definition
-  fun_app ("_ ---> _")
-where
-  "f ---> g \<equiv> \<lambda>h x. g (h (f x))"
-
-lemma helper:
-  assumes q: "QUOTIENT R ab re"
-  and     a: "R z z"
-  shows "R (re (ab z)) z"
-using q a
-apply(unfold QUOTIENT_def)[1]
-apply(blast)
-done
-
-
-lemma
-  assumes q1: "QUOTIENT R1 abs1 rep1"
-  and     q2: "QUOTIENT R2 abs2 rep2"
-  shows "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
-proof -
-  have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
-    apply(simp add: expand_fun_eq)
-    apply(simp add: fun_app_def)
-    using q1 q2
-    apply(simp add: QUOTIENT_def)
-    done
-  moreover
-  have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
-    apply(simp add: FUN_REL_def)
-    apply(auto)
-    apply(simp add: fun_app_def)
-    using q1 q2
-    apply(unfold QUOTIENT_def)
-    apply(metis)
-    done
-  moreover
-  have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and> 
-        (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
-    apply(simp add: expand_fun_eq)
-    apply(rule allI)+
-    apply(rule iffI)
-    using q1 q2
-    apply(unfold QUOTIENT_def)[1]
-    apply(unfold fun_app_def)[1]
-    apply(unfold FUN_REL_def)[1]
-    apply(rule conjI)
-    apply(metis)
-    apply(rule conjI)
-    apply(metis)
-    apply(metis)
-    apply(erule conjE)
-    apply(simp (no_asm) add: FUN_REL_def)
-    apply(rule allI impI)+
-    apply(subgoal_tac "R1 x x \<and> R1 y y \<and> abs1 x = abs1 y")(*A*)
-    using q2
-    apply(unfold QUOTIENT_def)[1]
-    apply(unfold fun_app_def)[1]
-    apply(unfold FUN_REL_def)[1]
-    apply(subgoal_tac "R2 (r x) (r x)")(*B*)
-    apply(subgoal_tac "R2 (s y) (s y)")(*C*)
-    apply(subgoal_tac "abs2 (r x) = abs2 (s y)")(*D*)
-    apply(blast)
-    (*D*)
-    apply(metis helper q1)
-    (*C*)
-    apply(blast)
-    (*B*)
-    apply(blast)
-    (*A*)
-    using q1
-    apply(unfold QUOTIENT_def)[1]
-    apply(unfold fun_app_def)[1]
-    apply(unfold FUN_REL_def)[1]
-    apply(metis)
-    done
-  ultimately
-  show "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
-    apply(unfold QUOTIENT_def)[1]
-    apply(blast)
-    done
-qed
-    
-    
-    
-    
-
-
-
-definition 
-  "USER R \<equiv> NONEMPTY R \<and> 
-
-
-
-typedecl tau
-consts R::"tau \<Rightarrow> tau \<Rightarrow> bool"
-
-
-
-definition
-  FACTOR :: "'a set \<Rightarrow> ('a \<times>'a \<Rightarrow> bool) \<Rightarrow> ('a set) set" ("_ '/'/'/ _")
-where
-  "A /// r \<equiv> \<Union>x\<in>A. {r``{x}}"
-
-typedef qtau = "\<lambda>c::tau\<Rightarrow>bool. (\<exists>x. R x x \<and> (c = R x))"
-apply(rule exI)
-
-apply(rule_tac x="R x" in exI)
-apply(auto)
-
-definition  
- "QUOT TYPE('a) R \<equiv> \<lambda>c::'a\<Rightarrow>bool. (\<exists>x. R x x \<and> (c = R x))"
-
-
- 
-  
-
-