# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1262870057 -3600
# Node ID 162e38c14f24f7f5bbec30174e111423fb2a4bf1
# Parent  f5c9ddc18246ff902350f463a8de012f35bd3a9d
The working proof of the special case.

diff -r f5c9ddc18246 -r 162e38c14f24 Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Thu Jan 07 10:55:20 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Thu Jan 07 14:14:17 2010 +0100
@@ -135,37 +135,20 @@
   apply(simp add: Quotient_abs_rep[OF a])
 done
 
-(* Trying to use induction: *)
-lemma help1: "list_rel op \<approx>1 ba [] \<equiv> ba = []"
-apply(induct ba)
-apply (auto)
+lemma set_in_eq: "(\<forall>e. ((e \<in> A) = (e \<in> B))) \<equiv> A = B"
+apply (rule eq_reflection)
+apply auto
 done
-lemma help2: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) (x # xs) [] \<equiv> False"
-sorry
-lemma help2a: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) [] (x # xs) \<equiv> False"
-sorry
-lemma help4: "abs_fset (a # b) = abs_fset [] \<equiv> False"
-sorry
-lemma help4a: "abs_fset [] = abs_fset (a # b) \<equiv> False"
-sorry
 
-lemma help5: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) x x"
-sorry
+lemma map_rep_ok: "b \<approx>1 ba \<Longrightarrow> map rep_fset b \<approx>1 map rep_fset ba"
+unfolding erel1_def
+apply(simp only: set_map set_in_eq)
+done
 
-lemma quotient_compose_list_pre_ind:
- "(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>
-        (list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
-apply(induct r s rule: list_induct2')
-  apply(simp)
-  apply(simp add: help2 help4 help5)
-  apply(simp add: help2a help4a help5)
-  apply(simp add: help5)
-  apply rule
-apply (auto simp add: help2a help4a help5 help1 help2 help4 )
-sorry
-
-(* Trying to solve it directly: *)
+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 quotient_compose_list_pre:
  "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s =
@@ -197,10 +180,7 @@
 apply (subgoal_tac "map abs_fset s = map abs_fset ba")
 prefer 2
 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
-apply simp
-(* To solve first subgoal we just need: *)
-(* b \<approx> ba \<Longrightarrow> mapabs b \<approx> mapabs ba *)
-prefer 2
+apply (simp add: map_abs_ok)
 apply rule
 apply (rule rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"])
 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
@@ -216,9 +196,9 @@
 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s")
 prefer 2
 apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp)
-(* To solve this subgoal we just need: *)
-(* x \<approx> y \<Longrightarrow> maprep x \<approx> maprep y *)
-sorry
+apply (rule map_rep_ok)
+apply (assumption)
+done
 
 lemma quotient_compose_list:
   shows  "Quotient ((list_rel op \<approx>1) OO (op \<approx>1) OO (list_rel op \<approx>1))
@@ -240,19 +220,27 @@
 apply(rule quotient_compose_list_pre)
 done
 
-lemma quotient_compose_ok:
+lemma quotient_compose_list_gen:
   assumes a1: "Quotient (op \<approx>1) abs_fset rep_fset"
-  and     a2:  "Quotient r2 abs2 rep2"
+  and     a2:  "Quotient r2 abs2 rep2" "equivp r2"
   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] id_simps Quotient_abs_rep[OF Quotient_fset])
+apply (simp add: abs_o_rep[OF a2(1)] id_simps Quotient_abs_rep[OF Quotient_fset])
+apply (rule)
 apply (rule)
 apply (rule)
-using a1
-apply -
-sorry
+apply (rule list_rel_refl)
+apply (metis a2(2) equivp_def)
+apply (rule)
+apply (rule equivp_reflp[OF fset_equivp])
+apply (rule list_rel_refl)
+apply (metis a2(2) equivp_def)
+apply rule
+apply rule
+apply(rule quotient_compose_list_gen_pre)
+done
 
 (* This is the general statement but the types are wrong as in following exanples *)
 lemma quotient_compose_general: