Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/FSet.thy
changeset 1909 9972dc5bd7ad
parent 1907 7b74cf843942
child 1913 39951d71bfce
equal deleted inserted replaced
1908:880fe1d2234e 1909:9972dc5bd7ad 
     6 *)
 
     6 *)
 
     7 theory FSet
 
     7 theory FSet
 
     8 imports Quotient Quotient_List List
 
     8 imports Quotient Quotient_List List
 
     9 begin
 
     9 begin
 
    10 
    10 
       
    11 text {* Definiton of List relation and the quotient type *}
 
       
    12 
    11 fun
 
    13 fun
 
    12   list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
 
    14   list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
 
    13 where
 
    15 where
 
    14   "list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)"
 
    16   "list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)"
 
    15 
    17 
    16 lemma list_eq_equivp:
 
    18 lemma list_eq_equivp:
 
    17   shows "equivp list_eq"
 
    19   shows "equivp list_eq"
 
    18   unfolding equivp_reflp_symp_transp 
    20   unfolding equivp_reflp_symp_transp
 
    19   unfolding reflp_def symp_def transp_def
 
    21   unfolding reflp_def symp_def transp_def
 
    20   by auto
 
    22   by auto
 
    21 
    23 
       
    24 quotient_type
 
       
    25   'a fset = "'a list" / "list_eq"
 
       
    26   by (rule list_eq_equivp)
 
       
    27 
       
    28 text {* Raw definitions *}
 
       
    29 
    22 definition
 
    30 definition
 
    23   memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
 
    31   memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
 
    24 where
 
    32 where
 
    25   "memb x xs \<equiv> x \<in> set xs"
 
    33   "memb x xs \<equiv> x \<in> set xs"
 
    26 
    34 
    27 definition
 
    35 definition
 
    28   sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
 
    36   sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
 
    29 where
 
    37 where
 
    30   "sub_list xs ys \<equiv> (\<forall>x. x \<in> set xs \<longrightarrow> x \<in> set ys)"
 
    38   "sub_list xs ys \<equiv> (\<forall>x. x \<in> set xs \<longrightarrow> x \<in> set ys)"
 
    31 
    39 
    32 quotient_type
 
    40 fun
 
    33   'a fset = "'a list" / "list_eq"
 
    41   fcard_raw :: "'a list \<Rightarrow> nat"
 
    34 by (rule list_eq_equivp)
 
    42 where
 
    35 
    43   fcard_raw_nil:  "fcard_raw [] = 0"
 
    36 lemma sub_list_rsp1: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list xs zs = sub_list ys zs"
 
    44 | fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))"
 
    37   by (simp add: sub_list_def)
 
    45 
    38 
    46 primrec
 
    39 lemma sub_list_rsp2: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list zs xs = sub_list zs ys"
 
    47   finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
    40   by (simp add: sub_list_def)
 
    48 where
 
    41 
    49   "finter_raw [] l = []"
 
    42 lemma [quot_respect]:
 
    50 | "finter_raw (h # t) l =
 
    43   shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
 
    51      (if memb h l then h # (finter_raw t l) else finter_raw t l)"
 
    44   by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2)
 
    52 
       
    53 fun
 
       
    54   delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
 
       
    55 where
 
       
    56   "delete_raw [] x = []"
 
       
    57 | "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
 
       
    58 
       
    59 definition
 
       
    60   rsp_fold
 
       
    61 where
 
       
    62   "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
 
       
    63 
       
    64 primrec
 
       
    65   ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
 
       
    66 where
 
       
    67   "ffold_raw f z [] = z"
 
       
    68 | "ffold_raw f z (a # A) =
 
       
    69      (if (rsp_fold f) then
 
       
    70        if memb a A then ffold_raw f z A
 
       
    71        else f a (ffold_raw f z A)
 
       
    72      else z)"
 
       
    73 
       
    74 text {* Respectfullness *}
 
    45 
    75 
    46 lemma [quot_respect]:
 
    76 lemma [quot_respect]:
 
    47   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
 
    77   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
 
    48   by auto
 
    78   by auto
 
    49 
    79 
       
    80 lemma [quot_respect]:
 
       
    81   shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
 
       
    82   by (auto simp add: sub_list_def)
 
       
    83 
       
    84 lemma memb_rsp[quot_respect]:
 
       
    85   shows "(op = ===> op \<approx> ===> op =) memb memb"
 
       
    86   by (auto simp add: memb_def)
 
       
    87 
       
    88 lemma nil_rsp[quot_respect]:
 
       
    89   shows "[] \<approx> []"
 
       
    90   by simp
 
       
    91 
       
    92 lemma cons_rsp[quot_respect]:
 
       
    93   shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
 
       
    94   by simp
 
       
    95 
       
    96 lemma map_rsp[quot_respect]:
 
       
    97   shows "(op = ===> op \<approx> ===> op \<approx>) map map"
 
       
    98   by auto
 
       
    99 
       
   100 lemma set_rsp[quot_respect]:
 
       
   101   "(op \<approx> ===> op =) set set"
 
       
   102   by auto
 
       
   103 
       
   104 lemma list_equiv_rsp[quot_respect]:
 
       
   105   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
 
       
   106   by auto
 
       
   107 
       
   108 lemma not_memb_nil:
 
       
   109   shows "\<not> memb x []"
 
       
   110   by (simp add: memb_def)
 
       
   111 
       
   112 lemma memb_cons_iff:
 
       
   113   shows "memb x (y # xs) = (x = y \<or> memb x xs)"
 
       
   114   by (induct xs) (auto simp add: memb_def)
 
       
   115 
       
   116 lemma memb_finter_raw:
 
       
   117   "memb x (finter_raw xs ys) \<longleftrightarrow> memb x xs \<and> memb x ys"
 
       
   118   by (induct xs) (auto simp add: not_memb_nil memb_cons_iff)
 
       
   119 
       
   120 lemma [quot_respect]:
 
       
   121   "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
 
       
   122   by (simp add: memb_def[symmetric] memb_finter_raw)
 
       
   123 
       
   124 lemma memb_delete_raw:
 
       
   125   "memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)"
 
       
   126   by (induct xs arbitrary: x y) (auto simp add: memb_def)
 
       
   127 
       
   128 lemma [quot_respect]:
 
       
   129   "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
 
       
   130   by (simp add: memb_def[symmetric] memb_delete_raw)
 
       
   131 
       
   132 lemma fcard_raw_gt_0:
 
       
   133   assumes a: "x \<in> set xs"
 
       
   134   shows "0 < fcard_raw xs"
 
       
   135   using a by (induct xs) (auto simp add: memb_def)
 
       
   136 
       
   137 lemma fcard_raw_delete_one:
 
       
   138   shows "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
 
       
   139   by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)
 
       
   140 
       
   141 lemma fcard_raw_rsp_aux:
 
       
   142   assumes a: "xs \<approx> ys"
 
       
   143   shows "fcard_raw xs = fcard_raw ys"
 
       
   144   using a
 
       
   145   apply (induct xs arbitrary: ys)
 
       
   146   apply (auto simp add: memb_def)
 
       
   147   apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys)")
 
       
   148   apply (auto)
 
       
   149   apply (drule_tac x="x" in spec)
 
       
   150   apply (blast)
 
       
   151   apply (drule_tac x="[x \<leftarrow> ys. x \<noteq> a]" in meta_spec)
 
       
   152   apply (simp add: fcard_raw_delete_one memb_def)
 
       
   153   apply (case_tac "a \<in> set ys")
 
       
   154   apply (simp only: if_True)
 
       
   155   apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)")
 
       
   156   apply (drule Suc_pred'[OF fcard_raw_gt_0])
 
       
   157   apply (auto)
 
       
   158   done
 
       
   159 
       
   160 lemma fcard_raw_rsp[quot_respect]:
 
       
   161   shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
 
       
   162   by (simp add: fcard_raw_rsp_aux)
 
       
   163 
       
   164 lemma memb_absorb:
 
       
   165   shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
 
       
   166   by (induct xs) (auto simp add: memb_def)
 
       
   167 
       
   168 lemma none_memb_nil:
 
       
   169   "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
 
       
   170   by (simp add: memb_def)
 
       
   171 
       
   172 lemma not_memb_delete_raw_ident:
 
       
   173   shows "\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"
 
       
   174   by (induct xs) (auto simp add: memb_def)
 
       
   175 
       
   176 lemma memb_commute_ffold_raw:
 
       
   177   "rsp_fold f \<Longrightarrow> memb h b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (delete_raw b h))"
 
       
   178   apply (induct b)
 
       
   179   apply (simp_all add: not_memb_nil)
 
       
   180   apply (auto)
 
       
   181   apply (simp_all add: memb_delete_raw not_memb_delete_raw_ident  rsp_fold_def  memb_cons_iff)
 
       
   182   done
 
       
   183 
       
   184 lemma ffold_raw_rsp_pre:
 
       
   185   "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
 
       
   186   apply (induct a arbitrary: b)
 
       
   187   apply (simp add: memb_absorb memb_def none_memb_nil)
 
       
   188   apply (simp)
 
       
   189   apply (rule conjI)
 
       
   190   apply (rule_tac [!] impI)
 
       
   191   apply (rule_tac [!] conjI)
 
       
   192   apply (rule_tac [!] impI)
 
       
   193   apply (subgoal_tac "\<forall>e. memb e a2 = memb e b")
 
       
   194   apply (simp)
 
       
   195   apply (simp add: memb_cons_iff memb_def)
 
       
   196   apply (auto)[1]
 
       
   197   apply (drule_tac x="e" in spec)
 
       
   198   apply (blast)
 
       
   199   apply (case_tac b)
 
       
   200   apply (simp_all)
 
       
   201   apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))")
 
       
   202   apply (simp only:)
 
       
   203   apply (rule_tac f="f a1" in arg_cong)
 
       
   204   apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)")
 
       
   205   apply (simp)
 
       
   206   apply (simp add: memb_delete_raw)
 
       
   207   apply (auto simp add: memb_cons_iff)[1]
 
       
   208   apply (erule memb_commute_ffold_raw)
 
       
   209   apply (drule_tac x="a1" in spec)
 
       
   210   apply (simp add: memb_cons_iff)
 
       
   211   apply (simp add: memb_cons_iff)
 
       
   212   apply (case_tac b)
 
       
   213   apply (simp_all)
 
       
   214   done
 
       
   215 
       
   216 lemma [quot_respect]:
 
       
   217   "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
 
       
   218   by (simp add: memb_def[symmetric] ffold_raw_rsp_pre)
 
       
   219 
       
   220 text {* Distributive lattice with bot *}
 
       
   221 
    50 lemma sub_list_not_eq:
 
   222 lemma sub_list_not_eq:
 
    51   "(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)"
 
   223   "(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)"
 
    52   by (auto simp add: sub_list_def)
 
   224   by (auto simp add: sub_list_def)
 
    53 
   225 
    54 lemma sub_list_refl:
 
   226 lemma sub_list_refl:
 
    61 
   233 
    62 lemma sub_list_empty:
 
   234 lemma sub_list_empty:
 
    63   "sub_list [] x"
 
   235   "sub_list [] x"
 
    64   by (simp add: sub_list_def)
 
   236   by (simp add: sub_list_def)
 
    65 
   237 
    66 primrec
 
       
    67   finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
       
    68 where
 
       
    69   "finter_raw [] l = []"
 
       
    70 | "finter_raw (h # t) l =
 
       
    71      (if memb h l then h # (finter_raw t l) else finter_raw t l)"
 
       
    72 
       
    73 lemma not_memb_nil:
 
       
    74   shows "\<not> memb x []"
 
       
    75   by (simp add: memb_def)
 
       
    76 
       
    77 lemma memb_cons_iff:
 
       
    78   shows "memb x (y # xs) = (x = y \<or> memb x xs)"
 
       
    79   by (induct xs) (auto simp add: memb_def)
 
       
    80 
       
    81 lemma memb_finter_raw:
 
       
    82   "memb x (finter_raw xs ys) \<longleftrightarrow> memb x xs \<and> memb x ys"
 
       
    83   apply (induct xs)
 
       
    84   apply (simp add: not_memb_nil)
 
       
    85   apply (simp add: finter_raw.simps)
 
       
    86   apply (simp add: memb_cons_iff)
 
       
    87   apply auto
 
       
    88   done
 
       
    89 
       
    90 lemma [quot_respect]:
 
       
    91   "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
 
       
    92   by (simp add: memb_def[symmetric] memb_finter_raw)
 
       
    93 
       
    94 
       
    95 lemma sub_list_append_left:
 
   238 lemma sub_list_append_left:
 
    96   "sub_list x (x @ y)"
 
   239   "sub_list x (x @ y)"
 
    97   by (simp add: sub_list_def)
 
   240   by (simp add: sub_list_def)
 
    98 
   241 
    99 lemma sub_list_append_right:
 
   242 lemma sub_list_append_right:
 
   121   by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
 
   264   by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
 
   122 
   265 
   123 lemma append_inter_distrib:
 
   266 lemma append_inter_distrib:
 
   124   "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
 
   267   "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
 
   125   apply (induct x)
 
   268   apply (induct x)
 
   126   apply simp
 
       
   127   apply simp
 
       
   128   apply (rule conjI)
 
       
   129   apply (simp_all add: memb_def)
 
   269   apply (simp_all add: memb_def)
 
   130   apply (simp add: memb_def[symmetric] memb_finter_raw)
 
   270   apply (simp add: memb_def[symmetric] memb_finter_raw)
 
   131   apply (simp add: memb_def)
 
   271   by (auto simp add: memb_def)
 
   132   apply auto
 
       
   133   done
 
       
   134 
   272 
   135 instantiation fset :: (type) "{bot,distrib_lattice}"
 
   273 instantiation fset :: (type) "{bot,distrib_lattice}"
 
   136 begin
 
   274 begin
 
   137 
   275 
   138 quotient_definition
 
   276 quotient_definition
 
   216   show "x |\<subseteq>| y |\<inter>| z" using a b by (lifting sub_list_inter)
 
   354   show "x |\<subseteq>| y |\<inter>| z" using a b by (lifting sub_list_inter)
 
   217 qed
 
   355 qed
 
   218 
   356 
   219 end
 
   357 end
 
   220 
   358 
   221 section {* Empty fset, Finsert and Membership *}
 
   359 section {* Finsert and Membership *}
 
   222 
   360 
   223 quotient_definition
 
   361 quotient_definition
 
   224   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 
   362   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 
   225 is "op #"
 
   363 is "op #"
 
   226 
   364 
   238 
   376 
   239 abbreviation
 
   377 abbreviation
 
   240   fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)
 
   378   fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)
 
   241 where
 
   379 where
 
   242   "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
 
   380   "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
 
   243 
       
   244 lemma memb_rsp[quot_respect]:
 
       
   245   shows "(op = ===> op \<approx> ===> op =) memb memb"
 
       
   246 by (auto simp add: memb_def)
 
       
   247 
       
   248 lemma nil_rsp[quot_respect]:
 
       
   249   shows "[] \<approx> []"
 
       
   250 by simp
 
       
   251 
       
   252 lemma cons_rsp[quot_respect]:
 
       
   253   shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
 
       
   254 by simp
 
       
   255 
   381 
   256 section {* Augmenting an fset -- @{const finsert} *}
 
   382 section {* Augmenting an fset -- @{const finsert} *}
 
   257 
   383 
   258 lemma nil_not_cons:
 
   384 lemma nil_not_cons:
 
   259   shows "\<not> ([] \<approx> x # xs)"
 
   385   shows "\<not> ([] \<approx> x # xs)"
 
   262 
   388 
   263 lemma no_memb_nil:
 
   389 lemma no_memb_nil:
 
   264   "(\<forall>x. \<not> memb x xs) = (xs = [])"
 
   390   "(\<forall>x. \<not> memb x xs) = (xs = [])"
 
   265   by (simp add: memb_def)
 
   391   by (simp add: memb_def)
 
   266 
   392 
   267 lemma none_memb_nil:
 
       
   268   "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
 
       
   269   by (simp add: memb_def)
 
       
   270 
       
   271 lemma memb_consI1:
 
   393 lemma memb_consI1:
 
   272   shows "memb x (x # xs)"
 
   394   shows "memb x (x # xs)"
 
   273   by (simp add: memb_def)
 
   395   by (simp add: memb_def)
 
   274 
   396 
   275 lemma memb_consI2:
 
   397 lemma memb_consI2:
 
   276   shows "memb x xs \<Longrightarrow> memb x (y # xs)"
 
   398   shows "memb x xs \<Longrightarrow> memb x (y # xs)"
 
   277   by (simp add: memb_def)
 
   399   by (simp add: memb_def)
 
   278 
   400 
   279 lemma memb_absorb:
 
       
   280   shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
 
       
   281   by (induct xs) (auto simp add: memb_def id_simps)
 
       
   282 
       
   283 section {* Singletons *}
 
   401 section {* Singletons *}
 
   284 
   402 
   285 lemma singleton_list_eq:
 
   403 lemma singleton_list_eq:
 
   286   shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
 
   404   shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
 
   287   by (simp add: id_simps) auto
 
   405   by (simp add: id_simps) auto
 
   292   "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
 
   410   "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
 
   293   by (auto simp add: memb_def sub_list_def)
 
   411   by (auto simp add: memb_def sub_list_def)
 
   294 
   412 
   295 section {* Cardinality of finite sets *}
 
   413 section {* Cardinality of finite sets *}
 
   296 
   414 
   297 fun
 
       
   298   fcard_raw :: "'a list \<Rightarrow> nat"
 
       
   299 where
 
       
   300   fcard_raw_nil:  "fcard_raw [] = 0"
 
       
   301 | fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))"
 
       
   302 
       
   303 quotient_definition
 
   415 quotient_definition
 
   304   "fcard :: 'a fset \<Rightarrow> nat" 
   416   "fcard :: 'a fset \<Rightarrow> nat" 
   305 is
 
   417 is
 
   306   "fcard_raw"
 
   418   "fcard_raw"
 
   307 
   419 
   308 lemma fcard_raw_0:
 
   420 lemma fcard_raw_0:
 
   309   shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
 
   421   shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
 
   310   by (induct xs) (auto simp add: memb_def)
 
   422   by (induct xs) (auto simp add: memb_def)
 
   311 
   423 
   312 lemma fcard_raw_gt_0:
 
       
   313   assumes a: "x \<in> set xs"
 
       
   314   shows "0 < fcard_raw xs"
 
       
   315   using a by (induct xs) (auto simp add: memb_def)
 
       
   316 
   424 
   317 lemma fcard_raw_not_memb:
 
   425 lemma fcard_raw_not_memb:
 
   318   shows "\<not> memb x xs \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)"
 
   426   shows "\<not> memb x xs \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)"
 
   319   by auto
 
   427   by auto
 
   320 
   428 
   337   apply (subgoal_tac "set xs = {x}")
 
   445   apply (subgoal_tac "set xs = {x}")
 
   338   apply (drule singleton_fcard_1)
 
   446   apply (drule singleton_fcard_1)
 
   339   apply auto
 
   447   apply auto
 
   340   done
 
   448   done
 
   341 
   449 
   342 lemma fcard_raw_delete_one:
 
       
   343   shows "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
 
       
   344   by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)
 
       
   345 
       
   346 lemma fcard_raw_suc_memb:
 
   450 lemma fcard_raw_suc_memb:
 
   347   assumes a: "fcard_raw A = Suc n"
 
   451   assumes a: "fcard_raw A = Suc n"
 
   348   shows "\<exists>a. memb a A"
 
   452   shows "\<exists>a. memb a A"
 
   349   using a
 
   453   using a
 
   350   apply (induct A)
 
   454   apply (induct A)
 
   360   have "\<not>(\<forall>x. \<not> memb x A)" using a by auto
 
   464   have "\<not>(\<forall>x. \<not> memb x A)" using a by auto
 
   361   then have "\<not>A \<approx> []" using none_memb_nil[of A] by simp
 
   465   then have "\<not>A \<approx> []" using none_memb_nil[of A] by simp
 
   362   then show ?thesis using fcard_raw_0[of A] by simp
 
   466   then show ?thesis using fcard_raw_0[of A] by simp
 
   363 qed
 
   467 qed
 
   364 
   468 
   365 lemma fcard_raw_rsp_aux:
 
   469 section {* fmap *}
 
   366   assumes a: "xs \<approx> ys"
 
       
   367   shows "fcard_raw xs = fcard_raw ys"
 
       
   368   using a
 
       
   369   apply(induct xs arbitrary: ys)
 
       
   370   apply(auto simp add: memb_def)
 
       
   371   apply(subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys)")
 
       
   372   apply simp
 
       
   373   apply auto
 
       
   374   apply (drule_tac x="x" in spec)
 
       
   375   apply blast
 
       
   376   apply(drule_tac x="[x \<leftarrow> ys. x \<noteq> a]" in meta_spec)
 
       
   377   apply(simp add: fcard_raw_delete_one memb_def)
 
       
   378   apply (case_tac "a \<in> set ys")
 
       
   379   apply (simp only: if_True)
 
       
   380   apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)")
 
       
   381   apply (drule Suc_pred'[OF fcard_raw_gt_0])
 
       
   382   apply auto
 
       
   383   done
 
       
   384 
       
   385 lemma fcard_raw_rsp[quot_respect]:
 
       
   386   shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
 
       
   387   by (simp add: fcard_raw_rsp_aux)
 
       
   388 
       
   389 
       
   390 section {* fmap and fset comprehension *}
 
       
   391 
   470 
   392 quotient_definition
 
   471 quotient_definition
 
   393   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 
   472   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 
   394 is
 
   473 is
 
   395  "map"
 
   474  "map"
 
   399   by simp
 
   478   by simp
 
   400 
   479 
   401 lemma memb_append:
 
   480 lemma memb_append:
 
   402   "memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys"
 
   481   "memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys"
 
   403   by (induct xs) (simp_all add: not_memb_nil memb_cons_iff)
 
   482   by (induct xs) (simp_all add: not_memb_nil memb_cons_iff)
 
   404 
       
   405 text {* raw section *}
 
       
   406 
       
   407 lemma map_rsp[quot_respect]:
 
       
   408   shows "(op = ===> op \<approx> ===> op \<approx>) map map"
 
       
   409   by auto
 
       
   410 
   483 
   411 lemma cons_left_comm:
 
   484 lemma cons_left_comm:
 
   412   "x # y # xs \<approx> y # x # xs"
 
   485   "x # y # xs \<approx> y # x # xs"
 
   413   by auto
 
   486   by auto
 
   414 
   487 
   435   apply (auto simp add: memb_def)
 
   508   apply (auto simp add: memb_def)
 
   436   done
 
   509   done
 
   437 
   510 
   438 section {* deletion *}
 
   511 section {* deletion *}
 
   439 
   512 
   440 fun
 
       
   441   delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
 
       
   442 where
 
       
   443   "delete_raw [] x = []"
 
       
   444 | "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
 
       
   445 
       
   446 lemma memb_delete_raw:
 
       
   447   "memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)"
 
       
   448   by (induct xs arbitrary: x y) (auto simp add: memb_def)
 
       
   449 
       
   450 lemma delete_raw_rsp:
 
       
   451   "xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x"
 
       
   452   by (simp add: memb_def[symmetric] memb_delete_raw)
 
       
   453 
       
   454 lemma [quot_respect]:
 
       
   455   "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
 
       
   456   by (simp add: memb_def[symmetric] memb_delete_raw)
 
       
   457 
       
   458 lemma memb_delete_raw_ident:
 
   513 lemma memb_delete_raw_ident:
 
   459   shows "\<not> memb x (delete_raw xs x)"
 
   514   shows "\<not> memb x (delete_raw xs x)"
 
   460   by (induct xs) (auto simp add: memb_def)
 
   515   by (induct xs) (auto simp add: memb_def)
 
   461 
   516 
   462 lemma not_memb_delete_raw_ident:
 
       
   463   shows "\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"
 
       
   464   by (induct xs) (auto simp add: memb_def)
 
       
   465 
       
   466 lemma fset_raw_delete_raw_cases:
 
   517 lemma fset_raw_delete_raw_cases:
 
   467   "xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # delete_raw xs x)"
 
   518   "xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # delete_raw xs x)"
 
   468   by (induct xs) (auto simp add: memb_def)
 
   519   by (induct xs) (auto simp add: memb_def)
 
   469 
   520 
   470 lemma fdelete_raw_filter:
 
   521 lemma fdelete_raw_filter:
 
   473 
   524 
   474 lemma fcard_raw_delete:
 
   525 lemma fcard_raw_delete:
 
   475   "fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
 
   526   "fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
 
   476   by (simp add: fdelete_raw_filter fcard_raw_delete_one)
 
   527   by (simp add: fdelete_raw_filter fcard_raw_delete_one)
 
   477 
   528 
   478 lemma set_rsp[quot_respect]:
 
   529 
   479   "(op \<approx> ===> op =) set set"
 
   530 
   480   by auto
 
   531 
   481 
       
   482 definition
 
       
   483   rsp_fold
 
       
   484 where
 
       
   485   "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
 
       
   486 
       
   487 primrec
 
       
   488   ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
 
       
   489 where
 
       
   490   "ffold_raw f z [] = z"
 
       
   491 | "ffold_raw f z (a # A) =
 
       
   492      (if (rsp_fold f) then
 
       
   493        if memb a A then ffold_raw f z A
 
       
   494        else f a (ffold_raw f z A)
 
       
   495      else z)"
 
       
   496 
       
   497 lemma memb_commute_ffold_raw:
 
       
   498   "rsp_fold f \<Longrightarrow> memb h b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (delete_raw b h))"
 
       
   499   apply (induct b)
 
       
   500   apply (simp add: not_memb_nil)
 
       
   501   apply (simp add: ffold_raw.simps)
 
       
   502   apply (rule conjI)
 
       
   503   apply (rule_tac [!] impI)
 
       
   504   apply (rule_tac [!] conjI)
 
       
   505   apply (rule_tac [!] impI)
 
       
   506   apply (simp_all add: memb_delete_raw)
 
       
   507   apply (simp add: memb_cons_iff)
 
       
   508   apply (simp add: not_memb_delete_raw_ident)
 
       
   509   apply (simp add: memb_cons_iff rsp_fold_def)
 
       
   510   done
 
       
   511 
       
   512 lemma ffold_raw_rsp_pre:
 
       
   513   "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
 
       
   514   apply (induct a arbitrary: b)
 
       
   515   apply (simp add: hd_in_set memb_absorb memb_def none_memb_nil)
 
       
   516   apply (simp add: ffold_raw.simps)
 
       
   517   apply (rule conjI)
 
       
   518   apply (rule_tac [!] impI)
 
       
   519   apply (rule_tac [!] conjI)
 
       
   520   apply (rule_tac [!] impI)
 
       
   521   apply (subgoal_tac "\<forall>e. memb e a2 = memb e b")
 
       
   522   apply (simp)
 
       
   523   apply (simp add: memb_cons_iff memb_def)
 
       
   524   apply auto
 
       
   525   apply (drule_tac x="e" in spec)
 
       
   526   apply blast
 
       
   527   apply (case_tac b)
 
       
   528   apply simp_all
 
       
   529   apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))")
 
       
   530   apply (simp only:)
 
       
   531   apply (rule_tac f="f a1" in arg_cong)
 
       
   532   apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)")
 
       
   533   apply simp
 
       
   534   apply (simp add: memb_delete_raw)
 
       
   535   apply (auto simp add: memb_cons_iff)[1]
 
       
   536   apply (erule memb_commute_ffold_raw)
 
       
   537   apply (drule_tac x="a1" in spec)
 
       
   538   apply (simp add: memb_cons_iff)
 
       
   539   apply (simp add: memb_cons_iff)
 
       
   540   apply (case_tac b)
 
       
   541   apply simp_all
 
       
   542   done
 
       
   543 
       
   544 lemma [quot_respect]:
 
       
   545   "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
 
       
   546   by (simp add: memb_def[symmetric] ffold_raw_rsp_pre)
 
       
   547 
   532 
   548 lemma finter_raw_empty:
 
   533 lemma finter_raw_empty:
 
   549   "finter_raw l [] = []"
 
   534   "finter_raw l [] = []"
 
   550   by (induct l) (simp_all add: not_memb_nil)
 
   535   by (induct l) (simp_all add: not_memb_nil)
 
   551 
   536 
   574 quotient_definition
 
   559 quotient_definition
 
   575   "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
 
   560   "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
 
   576 is
 
   561 is
 
   577   "concat"
 
   562   "concat"
 
   578 
   563 
   579 lemma list_equiv_rsp[quot_respect]:
 
       
   580   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
 
       
   581   by auto
 
       
   582 
   564 
   583 text {* alternate formulation with a different decomposition principle
 
   565 text {* alternate formulation with a different decomposition principle
 
   584   and a proof of equivalence *}
 
   566   and a proof of equivalence *}
 
   585 
   567 
   586 inductive
 
   568 inductive
 
   602   apply (induct A)
 
   584   apply (induct A)
 
   603   apply (simp add: memb_def list_eq2_refl)
 
   585   apply (simp add: memb_def list_eq2_refl)
 
   604   apply (case_tac "memb a (aa # A)")
 
   586   apply (case_tac "memb a (aa # A)")
 
   605   apply (simp_all only: memb_cons_iff)
 
   587   apply (simp_all only: memb_cons_iff)
 
   606   apply (case_tac [!] "a = aa")
 
   588   apply (case_tac [!] "a = aa")
 
   607   apply (simp_all add: delete_raw.simps)
 
   589   apply (simp_all)
 
   608   apply (case_tac "memb a A")
 
   590   apply (case_tac "memb a A")
 
   609   apply (auto simp add: memb_def)[2]
 
   591   apply (auto simp add: memb_def)[2]
 
   610   apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
 
   592   apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
 
   611   apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
 
   593   apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
 
   612   apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident)
 
   594   apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident)
 
   615 lemma memb_delete_list_eq2:
 
   597 lemma memb_delete_list_eq2:
 
   616   assumes a: "memb e r"
 
   598   assumes a: "memb e r"
 
   617   shows "list_eq2 (e # delete_raw r e) r"
 
   599   shows "list_eq2 (e # delete_raw r e) r"
 
   618   using a cons_delete_list_eq2[of e r]
 
   600   using a cons_delete_list_eq2[of e r]
 
   619   by simp
 
   601   by simp
 
       
   602 
       
   603 lemma delete_raw_rsp:
 
       
   604   "xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x"
 
       
   605   by (simp add: memb_def[symmetric] memb_delete_raw)
 
   620 
   606 
   621 lemma list_eq2_equiv_aux:
 
   607 lemma list_eq2_equiv_aux:
 
   622   assumes a: "fcard_raw l = n"
 
   608   assumes a: "fcard_raw l = n"
 
   623   and b: "l \<approx> r"
 
   609   and b: "l \<approx> r"
 
   624   shows "list_eq2 l r"
 
   610   shows "list_eq2 l r"
nominal2