4 

     5 notation

     6   list_eq (infix "\<approx>" 50)

     7 

     8 lemma fset_exhaust[case_names fempty finsert, cases type: fset]:

     9   shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"

    10 by (lifting list.exhaust)

    11 

    12 (* PROBLEM: these lemmas needs to be restated, since  *)

    13 (* concat.simps(1) and concat.simps(2) contain the    *)

    14 (* type variables ?'a1.0 (which are turned into frees *)

    15 (* 'a_1                                               *)

    16 

    17 lemma concat1:

    18   shows "concat [] \<approx> []"

    19 by (simp)

    20 

    21 lemma concat2:

    22   shows "concat (x # xs) \<approx> x @ concat xs"

    23 by (simp)

    24 

    25 lemma concat_rsp:

    26   "\<lbrakk>list_rel op \<approx> x x'; x' \<approx> y'; list_rel op \<approx> y' y\<rbrakk> \<Longrightarrow> concat x \<approx> concat y"

    27   apply (induct x y arbitrary: x' y' rule: list_induct2')

    28   apply simp

    29   defer defer

    30   apply (simp only: concat.simps)

    31   sorry

    32 

    33 lemma [quot_respect]:

    34   shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"

    35   apply (simp only: fun_rel_def)

    36   apply clarify

    37   apply (rule concat_rsp)

    38   apply assumption+

    39   done

    40 

    41 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []"

    42   by (metis nil_rsp list_rel.simps(1) pred_compI)

    43 

    44 lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"

    45   apply (rule eq_reflection)

    46   apply auto

    47   done

    48 

    49 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"

    50   unfolding list_eq.simps

    51   apply(simp only: set_map set_in_eq)

    52   done

    53 

    54 lemma quotient_compose_list_pre:

    55   "(list_rel op \<approx> OOO op \<approx>) r s =

    56   ((list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s \<and>

    57   abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"

    58   apply rule

    59   apply rule

    60   apply rule

    61   apply (rule list_rel_refl)

    62   apply (metis equivp_def fset_equivp)

    63   apply rule

    64   apply (rule equivp_reflp[OF fset_equivp])

    65   apply (rule list_rel_refl)

    66   apply (metis equivp_def fset_equivp)

    67   apply(rule)

    68   apply rule

    69   apply (rule list_rel_refl)

    70   apply (metis equivp_def fset_equivp)

    71   apply rule

    72   apply (rule equivp_reflp[OF fset_equivp])

    73   apply (rule list_rel_refl)

    74   apply (metis equivp_def fset_equivp)

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

    76   apply (metis Quotient_rel[OF Quotient_fset])

    77   apply (auto simp only:)[1]

    78   apply (subgoal_tac "map abs_fset r = map abs_fset b")

    79   prefer 2

    80   apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])

    81   apply (subgoal_tac "map abs_fset s = map abs_fset ba")

    82   prefer 2

    83   apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]])

    84   apply (simp only: map_rel_cong)

    85   apply rule

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

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

    88   apply (rule list_rel_refl)

    89   apply (metis equivp_def fset_equivp)

    90   apply rule

    91   prefer 2

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

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

    94   apply (rule list_rel_refl)

    95   apply (metis equivp_def fset_equivp)

    96   apply (erule conjE)+

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

    98   prefer 2

    99   apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp)

   100   apply (rule map_rel_cong)

   101   apply (assumption)

   102   done

   103 

   104 lemma quotient_compose_list[quot_thm]:

   105   shows  "Quotient ((list_rel op \<approx>) OOO (op \<approx>))

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

   107   unfolding Quotient_def comp_def

   108   apply (rule)+

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

   110   apply (rule)

   111   apply (rule)

   112   apply (rule)

   113   apply (rule list_rel_refl)

   114   apply (metis equivp_def fset_equivp)

   115   apply (rule)

   116   apply (rule equivp_reflp[OF fset_equivp])

   117   apply (rule list_rel_refl)

   118   apply (metis equivp_def fset_equivp)

   119   apply rule

   120   apply rule

   121   apply (rule quotient_compose_list_pre)

   122   done

   123 

   124 lemma fconcat_empty:

   125   shows "fconcat {||} = {||}"

   126   apply(lifting concat1)

   127   apply(cleaning)

   128   apply(simp add: comp_def bot_fset_def)

   129   done

   130 

   131 lemma insert_rsp2[quot_respect]:

   132   "(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #"

   133   apply auto

   134   apply (simp add: set_in_eq)

   135   apply (rule_tac b="x # b" in pred_compI)

   136   apply auto

   137   apply (rule_tac b="x # ba" in pred_compI)

   138   apply auto

   139   done

   140 

   141 lemma append_rsp[quot_respect]:

   142   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"

   143   by (auto)

   144 

   145 lemma fconcat_insert:

   146   shows "fconcat (finsert x S) = x |\<union>| fconcat S"

   147   apply(lifting concat2)

   148   apply(cleaning)

   149   apply (simp add: finsert_def fconcat_def comp_def)

   150   apply cleaning

   151   done