138 lemma help1: "list_rel op \<approx>1 ba [] \<equiv> ba = []"

   139 apply(induct ba)

   140 apply (auto)

   141 done

   142 

   143 lemma help2: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) (x # xs) [] \<equiv> False"

   144 sorry

   145 lemma help2a: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) [] (x # xs) \<equiv> False"

   146 sorry

   147 

   148 (* not used anymore *)

   149 lemma help3: "list_rel op \<approx>1 [] b \<equiv> b = []"

   150 apply (induct b)

   151 apply auto

   152 done

   153 

   154 lemma help4: "abs_fset (a # b) = abs_fset [] \<equiv> False"

   155 sorry

   156 lemma help4a: "abs_fset [] = abs_fset (a # b) \<equiv> False"

   157 sorry

   158 

   159 lemma help5: "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) x x"

   160 sorry

   161 

   162 lemma bla0pre:

   163  "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s =

   164        ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and>

   165         (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))"

   166 apply(induct r s rule: list_induct2')

   167   apply(simp)

   168   apply(simp add: help2 help4 help5)

   169   apply(simp add: help2a help4a help5)

   170   apply(simp add: help5)

   171   apply rule

   172 apply (auto simp add: help2a help4a help5 help1 help2 help4 )

   173 sorry

   174 

   175 lemma bla0:

   176   shows  "Quotient ((list_rel op \<approx>1) OO (op \<approx>1) OO (list_rel op \<approx>1)) 

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

   178   unfolding Quotient_def comp_def

   179 apply (rule)+

   180 apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset])

   181 apply (rule)

   182 apply (rule)

   183 apply (rule)

   184 apply (rule list_rel_refl)

   185 apply (metis equivp_def fset_equivp)

   186 apply (rule)

   187 apply (rule equivp_reflp[OF fset_equivp])

   188 apply (rule list_rel_refl)

   189 apply (metis equivp_def fset_equivp)

   190 apply rule

   191 apply rule

   192 apply(rule bla0pre)

   193 done

   194 

   195 lemma bla0pre2:

   196  "(list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r s =

   197        ((list_rel op \<approx>1 OO op \<approx>1 OO list_rel op \<approx>1) r r \<and>

   198         (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))"

   199 apply rule

   200 apply rule

   201 apply rule

   202 apply (rule list_rel_refl)

   203 apply (metis equivp_def fset_equivp)

   204 apply rule

   205 apply (rule equivp_reflp[OF fset_equivp])

   206 apply (rule list_rel_refl)

   207 apply (metis equivp_def fset_equivp)

   208 apply(rule)

   209 apply rule

   210 apply (rule list_rel_refl)

   211 apply (metis equivp_def fset_equivp)

   212 apply rule

   213 apply (rule equivp_reflp[OF fset_equivp])

   214 apply (rule list_rel_refl)

   215 apply (metis equivp_def fset_equivp)

   216 apply (subgoal_tac "map abs_fset r \<approx>1 map abs_fset s")

   217 apply (metis Quotient_rel[OF Quotient_fset])

   218 prefer 2

   219 apply rule

   220 thm rep_abs_rsp

   221 thm rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"]

   222 apply (rule rep_abs_rsp[of "list_rel op \<approx>1" "map abs_fset"])

   223 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})

   224 apply (rule list_rel_refl)

   225 apply (metis equivp_def fset_equivp)

   226 apply rule

   227 prefer 2

   228 apply (rule rep_abs_rsp_left[of "list_rel op \<approx>1" "map abs_fset"])

   229 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})

   230 apply (rule list_rel_refl)

   231 apply (metis equivp_def fset_equivp)

   232 apply auto

   233 sorry

   234