# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1262941681 -3600
# Node ID cedfe2a712985303e8ad176d0bd93d2a94fcd69f
# Parent  ae3ed7a68e8031b825e1ba537acdc73a2297882a
Proved concat_empty.

diff -r ae3ed7a68e80 -r cedfe2a71298 Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Thu Jan 07 16:51:38 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Fri Jan 08 10:08:01 2010 +0100
@@ -135,7 +135,7 @@
   apply(simp add: Quotient_abs_rep[OF a])
   done
 
-lemma set_in_eq: "(\<forall>e. ((e \<in> A) = (e \<in> B))) \<equiv> A = B"
+lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
   apply (rule eq_reflection)
   apply auto
   done
@@ -145,77 +145,6 @@
   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_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)"
-  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 quotient_compose_list_pre)
-done
-
 lemma quotient_compose_list_gen_pre:
   assumes a: "equivp r2"
   and b: "Quotient r2 abs2 rep2"
diff -r ae3ed7a68e80 -r cedfe2a71298 Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Thu Jan 07 16:51:38 2010 +0100
+++ b/Quot/Examples/FSet3.thy	Fri Jan 08 10:08:01 2010 +0100
@@ -260,36 +260,95 @@
 apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)
 done
 
+lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
+  apply (rule eq_reflection)
+  apply auto
+  done
+
+lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
+  unfolding list_eq.simps
+  apply(simp only: set_map set_in_eq)
+  done
+
+lemma quotient_compose_list_pre:
+  "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) r s =
+  ((list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) r r \<and>
+  (list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) 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> map abs_fset s")
+  apply (metis Quotient_rel[OF Quotient_fset])
+  apply (auto simp only:)[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 only: map_rel_cong)
+  apply rule
+  apply (rule rep_abs_rsp[of "list_rel op \<approx>" "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>" "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> 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[quot_thm]:
+  shows  "Quotient ((list_rel op \<approx>) OO (op \<approx>) OO (list_rel op \<approx>))
+  (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 quotient_compose_list_pre)
+  done
+
 lemma fconcat_empty:
   shows "fconcat {||} = {||}"
-apply(lifting_setup concat1)
-apply(regularize)
-defer
+apply(lifting concat1)
 apply(cleaning)
 apply(simp add: comp_def)
-apply(cleaning)
 apply(fold fempty_def[simplified id_simps])
 apply(rule refl)
-apply(injection)
-apply(rule apply_rsp[of "(list_rel (op \<approx>)) OO (op \<approx>) OO (list_rel (op \<approx>))" _ _ "op \<approx>" "concat" _ "[]" "((map rep_fset \<circ> rep_fset) ((abs_fset \<circ> map abs_fset) []))"])
-prefer 2
-ML_prf {* fun dest_comb (f $ a) = (f, a) *}
-apply(tactic {* Quotient_Tacs.quot_true_tac @{context} (fst o dest_comb) 1 *})
-prefer 3
-apply(tactic {* Quotient_Tacs.quot_true_tac @{context} (snd o dest_comb) 1 *})
-apply(rule rep_abs_rsp[of _ "(abs_fset \<circ> map abs_fset)" "(map rep_fset \<circ> rep_fset)"])
-prefer 3
-apply(rule rep_abs_rsp[of _ "((map rep_fset \<circ> rep_fset) ---> abs_fset)" "(abs_fset \<circ> map abs_fset) ---> rep_fset"])
-prefer 2
-apply(rule concat_rsp)
-prefer 3
-apply(injection)
-prefer 2
-apply(thin_tac "Quot_True {||}")
-apply(unfold Quotient_def)
-
-apply(auto)
-sorry
+done
 
 lemma fconcat_insert:
   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
diff -r ae3ed7a68e80 -r cedfe2a71298 Quot/QuotScript.thy
--- a/Quot/QuotScript.thy	Thu Jan 07 16:51:38 2010 +0100
+++ b/Quot/QuotScript.thy	Fri Jan 08 10:08:01 2010 +0100
@@ -502,6 +502,13 @@
   using a b unfolding Respects_def
   by simp
 
+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
+
 lemma fun_rel_eq_rel:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"