159 lemma quotient_compose_list[quot_thm]:

   159 lemma quotient_compose_list[quot_thm]:

   160   shows  "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))

   160   shows  "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))

   161     (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"

   161     (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"

   162   by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp)

   162   by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp)

   163 

   163 

   164 subsection {* Respectfulness lemmas for list operations *}

   166 subsection {* Respectfulness lemmas for list operations *}

   165 

   167 

   166 lemma list_equiv_rsp [quot_respect]:

   168 lemma list_equiv_rsp [quot_respect]:

   167   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"

   169   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"

   168   by auto

   170   by auto

   506   apply simp_all

   508   apply simp_all

   507   apply (rule append_rsp2_pre1)

   509   apply (rule append_rsp2_pre1)

   508   apply simp

   510   apply simp

   509   done

   511   done

   510 

   512 

   512   "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"

   514   "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"

   513 proof (intro fun_relI, elim pred_compE)

   515 proof (intro fun_relI, elim pred_compE)

   514   fix x y z w x' z' y' w' :: "'a list list"

   516   fix x y z w x' z' y' w' :: "'a list list"

   515   assume a:"list_all2 op \<approx> x x'"

   517   assume a:"list_all2 op \<approx> x x'"

   516   and b:    "x' \<approx> y'"

   518   and b:    "x' \<approx> y'"

   620 

   622 

   621 lemma singleton_fset_eq[simp]:

   623 lemma singleton_fset_eq[simp]:

   622   shows "{|x|} = {|y|} \<longleftrightarrow> x = y"

   624   shows "{|x|} = {|y|} \<longleftrightarrow> x = y"

   623   by (descending) (auto)

   625   by (descending) (auto)

   624 

   626 

   627 lemma in_fset_mdef:

   627 lemma in_fset_mdef:

   628   shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = insert_fset x (F - {|x|})"

   628   shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = insert_fset x (F - {|x|})"

   629   by (descending) (auto)

   629   by (descending) (auto)

   630 

   630 

   631 

   631