diff -r 000000000000 -r ebe0ea8fe247 Quotients.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quotients.thy	Tue Aug 11 12:29:15 2009 +0200
@@ -0,0 +1,412 @@
+theory Quotients
+imports Main
+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
+  "OPTION_REL R None None = True"
+| "OPTION_REL R (Some x) None = False"
+| "OPTION_REL R None (Some x) = False"
+| "OPTION_REL R (Some x) (Some y) = R x y"
+
+fun
+  option_map
+where
+  "option_map f None = None"
+| "option_map f (Some x) = Some (f x)"
+
+fun 
+  PROD_REL
+where
+  "PROD_REL R1 R2 (a1,a2) (b1,b2) = (R1 a1 b1 \<and> R2 a2 b2)"
+
+fun
+  prod_map
+where
+  "prod_map f1 f2 (a,b) = (f1 a, f2 b)"
+
+fun
+  SUM_REL  
+where
+  "SUM_REL R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
+| "SUM_REL R1 R2 (Inl a1) (Inr b2) = False"
+| "SUM_REL R1 R2 (Inr a2) (Inl b1) = False"
+| "SUM_REL R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
+
+fun
+  sum_map
+where
+  "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"
+  shows "QUOTIENT (PROD_REL E1 e2) (prod_map Abs1 Abs2) (prod_map Rep1 rep2)"
+using a b unfolding QUOTIENT_def
+oops
+
+lemma QUOTIENT_ABS_REP_LIST:
+  assumes a: "QUOTIENT_ABS_REP Abs Rep"
+  shows "QUOTIENT_ABS_REP (map Abs) (map Rep)"
+using a
+unfolding QUOTIENT_ABS_REP_def
+apply(rule_tac allI)
+apply(induct_tac a rule: list.induct)
+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))"
+
+
+ 
+  
+
+