586 lemma helper:

   587   assumes a : "list_eq l1 r1"

   588   shows "list_eq (l1 @ l) (r1 @ l)"

   589   using a

   590   apply(induct)

   591   apply(simp add:list_eq.intros)

   592   apply(simp add:list_eq_sym)

   593   apply(simp add:list_eq.intros(3))

   594   apply(simp add:list_eq.intros(4))

   595   apply(simp add:list_eq.intros(5))

   596   apply(rule_tac list_eq.intros(6))

   597   apply(assumption)

   598   apply(assumption)

   599 done

   600 

   601 lemma yyy :

   602   shows "

   603     (

   604      (UNION EMPTY s = s) &

   605      ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))

   606     ) = (

   607      ((ABS_fset ([] @ REP_fset s)) = s) &

   608      ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2)))

   609     )"

   610   unfolding UNION_def EMPTY_def INSERT_def

   611   apply(rule_tac f="(op &)" in arg_cong2)

   612   apply(rule_tac f="(op =)" in arg_cong2)

   613   apply (unfold REP_fset_def ABS_fset_def)

   614   apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset,symmetric])

   615   apply(rule helper)

   616   apply(rule list_eq.intros(3))

   617   apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])

   618   apply(rule list_eq_sym)

   619   apply(simp)

   620   apply(rule_tac f="(op =)" in arg_cong2)

   621   apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset,symmetric])

   622   apply(rule helper)

   623   apply(rule list_eq.intros(3))

   624   apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])

   625   apply(rule list_eq_sym)

   626   apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset,symmetric])

   627   apply(fold REP_fset_def ABS_fset_def)

   628   apply(rule list_eq.intros(5))

   629   apply(rule list_eq.intros(3))

   630   apply (unfold REP_fset_def ABS_fset_def)

   631   apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])

   632   apply(rule list_eq_sym)

   633 done

   634 

   635 lemma

   636   shows "

   637     (

   638      (UNION EMPTY s = s) &

   639      ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))

   640     )"

   641   apply(simp add:yyy)

   642   apply (unfold REP_fset_def ABS_fset_def)

   643   apply (rule QUOT_TYPE.thm10[OF QUOT_TYPE_fset])

   644 done

   645