# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1262875822 -3600
# Node ID c2ebb7fcf9d062264b29c83260305f81427833ab
# Parent  162e38c14f24f7f5bbec30174e111423fb2a4bf1
First generalization.

diff -r 162e38c14f24 -r c2ebb7fcf9d0 Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Thu Jan 07 14:14:17 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Thu Jan 07 15:50:22 2010 +0100
@@ -145,11 +145,21 @@
 apply(simp only: set_map set_in_eq)
 done
 
+lemma map_rep_ok_gen: "b \<approx>1 ba \<Longrightarrow> map rep2 b \<approx>1 map rep2 ba"
+unfolding erel1_def
+apply(simp only: set_map set_in_eq)
+done
+
 lemma map_abs_ok: "b \<approx>1 ba \<Longrightarrow> map abs_fset b \<approx>1 map abs_fset ba"
 unfolding erel1_def
 apply(simp only: set_map set_in_eq)
 done
 
+lemma map_abs_ok_gen: "b \<approx>1 ba \<Longrightarrow> map abs2 b \<approx>1 map abs2 ba"
+unfolding erel1_def
+apply(simp only: set_map set_in_eq)
+done
+
 lemma quotient_compose_list_pre:
  "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s =
        ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and>
@@ -220,34 +230,90 @@
 apply(rule quotient_compose_list_pre)
 done
 
+lemma quotient_compose_list_gen_pre:
+  assumes a: "equivp r2"
+  and b: "Quotient r2 abs2 rep2"
+  shows  "(list_rel r2 OO op \<approx>1 OO list_rel r2) r s =
+          ((list_rel r2 OO op \<approx>1 OO list_rel r2) r r \<and>
+           (list_rel r2 OO op \<approx>1 OO list_rel r2) s s \<and>
+           abs_fset (map abs2 r) = abs_fset (map abs2 s))"
+apply rule
+apply rule
+apply rule
+apply (rule list_rel_refl)
+apply (metis equivp_def a)
+apply rule
+apply (rule equivp_reflp[OF fset_equivp])
+apply (rule list_rel_refl)
+apply (metis equivp_def a)
+apply(rule)
+apply rule
+apply (rule list_rel_refl)
+apply (metis equivp_def a)
+apply rule
+apply (rule equivp_reflp[OF fset_equivp])
+apply (rule list_rel_refl)
+apply (metis equivp_def a)
+apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s")
+apply (metis Quotient_rel[OF Quotient_fset])
+apply (auto)[1]
+apply (subgoal_tac "map abs2 r = map abs2 b")
+prefer 2
+apply (metis Quotient_rel[OF list_quotient[OF b]])
+apply (subgoal_tac "map abs2 s = map abs2 ba")
+prefer 2
+apply (metis Quotient_rel[OF list_quotient[OF b]])
+apply (simp add: map_abs_ok_gen)
+apply rule
+apply (rule rep_abs_rsp[of "list_rel r2" "map abs2"])
+apply (rule list_quotient)
+apply (rule b)
+apply (rule list_rel_refl)
+apply (metis equivp_def a)
+apply rule
+prefer 2
+apply (rule rep_abs_rsp_left[of "list_rel r2" "map abs2"])
+apply (rule list_quotient)
+apply (rule b)
+apply (rule list_rel_refl)
+apply (metis equivp_def a)
+apply (erule conjE)+
+apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s")
+apply (rule map_rep_ok_gen)
+apply (assumption)
+apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp a b)
+done
+
 lemma quotient_compose_list_gen:
-  assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset"
-  and     a2:  "Quotient r2 abs2 rep2" "equivp r2"
+  assumes a: "Quotient r2 abs2 rep2"
+  and     b: "equivp r2" (* reflp should be enough... *)
   shows  "Quotient ((list_rel r2) OO (op \<approx>1) OO (list_rel r2))
                (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)"
   unfolding Quotient_def comp_def
 apply (rule)+
-apply (simp add: abs_o_rep[OF a2(1)] id_simps Quotient_abs_rep[OF Quotient_fset])
+apply (simp add: abs_o_rep[OF a] id_simps Quotient_abs_rep[OF Quotient_fset])
 apply (rule)
 apply (rule)
 apply (rule)
 apply (rule list_rel_refl)
-apply (metis a2(2) equivp_def)
+apply (metis b equivp_def)
 apply (rule)
 apply (rule equivp_reflp[OF fset_equivp])
 apply (rule list_rel_refl)
-apply (metis a2(2) equivp_def)
+apply (metis b equivp_def)
 apply rule
 apply rule
-apply(rule quotient_compose_list_gen_pre)
+apply(rule quotient_compose_list_gen_pre[OF b a])
 done
 
-(* This is the general statement but the types are wrong as in following exanples *)
+(* This is the general statement but the types of abs2 and rep2
+   are wrong as can be seen in following exanples *)
+
 lemma quotient_compose_general:
-  assumes a2: "Quotient r1 abs1 rep_fset"
+  assumes a2: "Quotient r1 abs1 rep1"
   and         "Quotient r2 abs2 rep2"
   shows  "Quotient ((list_rel r2) OO r1 OO (list_rel r2))
-               (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)"
+               (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep1)"
 sorry
 
 thm quotient_compose_ok     [OF Quotient_fset]