--- a/Quot/Examples/AbsRepTest.thy	Thu Jan 07 15:50:22 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Thu Jan 07 16:06:13 2010 +0100
@@ -119,114 +119,100 @@
       @{typ "('a fset) fset \<Rightarrow> 'a fset"})
 *}
 
-lemma
+lemma OO_sym_inv:
   assumes sr: "symp r"
   and     ss: "symp s"
   shows "(r OO s) x y = (s OO r) y x"
-using sr ss
-unfolding symp_def
-apply (metis pred_comp.intros pred_compE ss symp_def)
-done
+  using sr ss
+  unfolding symp_def
+  apply (metis pred_comp.intros pred_compE ss symp_def)
+  done
 
 lemma abs_o_rep:
   assumes a: "Quotient r absf repf"
   shows "absf o repf = id"
   apply(rule ext)
   apply(simp add: Quotient_abs_rep[OF a])
-done
+  done
 
 lemma set_in_eq: "(\<forall>e. ((e \<in> A) = (e \<in> B))) \<equiv> A = B"
-apply (rule eq_reflection)
-apply auto
-done
-
-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
+  apply (rule eq_reflection)
+  apply auto
+  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 map_rel_cong: "b \<approx>1 ba \<Longrightarrow> map f b \<approx>1 map f 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>
-        (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 rule
-apply rule
-apply rule
-apply (rule list_rel_refl)
-apply (metis equivp_def fset_equivp)
-apply rule
-apply (rule equivp_reflp[OF fset_equivp])
-apply (rule list_rel_refl)
-apply (metis equivp_def fset_equivp)
-apply(rule)
-apply rule
-apply (rule list_rel_refl)
-apply (metis equivp_def fset_equivp)
-apply rule
-apply (rule equivp_reflp[OF fset_equivp])
-apply (rule list_rel_refl)
-apply (metis equivp_def fset_equivp)
-apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s")
-apply (metis Quotient_rel[OF Quotient_fset])
-apply (auto)[1]
-apply (subgoal_tac "map abs_fset r = map abs_fset b")
-prefer 2
-apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
-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 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 *})
-apply (rule list_rel_refl)
-apply (metis equivp_def fset_equivp)
-apply rule
-prefer 2
-apply (rule rep_abs_rsp_left[of "list_rel op \<approx>1" "map abs_fset"])
-apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
-apply (rule list_rel_refl)
-apply (metis equivp_def fset_equivp)
-apply (erule conjE)+
-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)
-apply (rule map_rep_ok)
-apply (assumption)
-done
+        (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 rule
+  apply rule
+  apply rule
+  apply (rule list_rel_refl)
+  apply (metis equivp_def fset_equivp)
+  apply rule
+  apply (rule equivp_reflp[OF fset_equivp])
+  apply (rule list_rel_refl)
+  apply (metis equivp_def fset_equivp)
+  apply(rule)
+  apply rule
+  apply (rule list_rel_refl)
+  apply (metis equivp_def fset_equivp)
+  apply rule
+  apply (rule equivp_reflp[OF fset_equivp])
+  apply (rule list_rel_refl)
+  apply (metis equivp_def fset_equivp)
+  apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s")
+  apply (metis Quotient_rel[OF Quotient_fset])
+  apply (auto)[1]
+  apply (subgoal_tac "map abs_fset r = map abs_fset b")
+  prefer 2
+  apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])
+  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 add: map_rel_cong)
+  apply rule
+  apply (rule rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"])
+  apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
+  apply (rule list_rel_refl)
+  apply (metis equivp_def fset_equivp)
+  apply rule
+  prefer 2
+  apply (rule rep_abs_rsp_left[of "list_rel op \<approx>1" "map abs_fset"])
+  apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
+  apply (rule list_rel_refl)
+  apply (metis equivp_def fset_equivp)
+  apply (erule conjE)+
+  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)
+  apply (rule map_rel_cong)
+  apply (assumption)
+  done
 
 lemma quotient_compose_list:
   shows  "Quotient ((list_rel op \<approx>1) OO (op \<approx>1) OO (list_rel op \<approx>1))
-               (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
+  (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
   unfolding Quotient_def comp_def
-apply (rule)+
-apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset])
-apply (rule)
-apply (rule)
-apply (rule)
-apply (rule list_rel_refl)
-apply (metis equivp_def fset_equivp)
-apply (rule)
-apply (rule equivp_reflp[OF fset_equivp])
-apply (rule list_rel_refl)
-apply (metis equivp_def fset_equivp)
-apply rule
-apply rule
+  apply (rule)+
+  apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset])
+  apply (rule)
+  apply (rule)
+  apply (rule)
+  apply (rule list_rel_refl)
+  apply (metis equivp_def fset_equivp)
+  apply (rule)
+  apply (rule equivp_reflp[OF fset_equivp])
+  apply (rule list_rel_refl)
+  apply (metis equivp_def fset_equivp)
+  apply rule
+  apply rule
 apply(rule quotient_compose_list_pre)
 done
 
@@ -237,52 +223,52 @@
           ((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
+  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_rel_cong)
+  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_rel_cong)
+  apply (assumption)
+  apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp a b)
+  done
 
 lemma quotient_compose_list_gen:
   assumes a: "Quotient r2 abs2 rep2"
@@ -290,25 +276,24 @@
   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 a] id_simps Quotient_abs_rep[OF Quotient_fset])
-apply (rule)
-apply (rule)
-apply (rule)
-apply (rule list_rel_refl)
-apply (metis b equivp_def)
-apply (rule)
-apply (rule equivp_reflp[OF fset_equivp])
-apply (rule list_rel_refl)
-apply (metis b equivp_def)
-apply rule
-apply rule
-apply(rule quotient_compose_list_gen_pre[OF b a])
-done
+  apply (rule)+
+  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 b equivp_def)
+  apply (rule)
+  apply (rule equivp_reflp[OF fset_equivp])
+  apply (rule list_rel_refl)
+  apply (metis b equivp_def)
+  apply rule
+  apply rule
+  apply(rule quotient_compose_list_gen_pre[OF b a])
+  done
 
 (* 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 rep1"
   and         "Quotient r2 abs2 rep2"
@@ -316,10 +301,8 @@
                (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep1)"
 sorry
 
-thm quotient_compose_ok     [OF Quotient_fset]
+thm quotient_compose_list_gen[OF Quotient_fset fset_equivp]
 thm quotient_compose_general[OF Quotient_fset]
-
-thm quotient_compose_ok     [OF Quotient_fset Quotient_fset]
 (* Doesn't work: *)
 (* thm quotient_compose_general[OF Quotient_fset Quotient_fset] *)