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 1913 39951d71bfce
parent 1912 0a857f662e4c
parent 1909 9972dc5bd7ad
child 1927 6c5e3ac737d9
child 1951 a0c7290a4e27
equal deleted inserted replaced
1912:0a857f662e4c 1913:39951d71bfce 
     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 instantiation fset :: (type) bot
 
   238 lemma sub_list_append_left:
 
       
   239   "sub_list x (x @ y)"
 
       
   240   by (simp add: sub_list_def)
 
       
   241 
       
   242 lemma sub_list_append_right:
 
       
   243   "sub_list y (x @ y)"
 
       
   244   by (simp add: sub_list_def)
 
       
   245 
       
   246 lemma sub_list_inter_left:
 
       
   247   shows "sub_list (finter_raw x y) x"
 
       
   248   by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
 
       
   249 
       
   250 lemma sub_list_inter_right:
 
       
   251   shows "sub_list (finter_raw x y) y"
 
       
   252   by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
 
       
   253 
       
   254 lemma sub_list_list_eq:
 
       
   255   "sub_list x y \<Longrightarrow> sub_list y x \<Longrightarrow> list_eq x y"
 
       
   256   unfolding sub_list_def list_eq.simps by blast
 
       
   257 
       
   258 lemma sub_list_append:
 
       
   259   "sub_list y x \<Longrightarrow> sub_list z x \<Longrightarrow> sub_list (y @ z) x"
 
       
   260   unfolding sub_list_def by auto
 
       
   261 
       
   262 lemma sub_list_inter:
 
       
   263   "sub_list x y \<Longrightarrow> sub_list x z \<Longrightarrow> sub_list x (finter_raw y z)"
 
       
   264   by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
 
       
   265 
       
   266 lemma append_inter_distrib:
 
       
   267   "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
 
       
   268   apply (induct x)
 
       
   269   apply (simp_all add: memb_def)
 
       
   270   apply (simp add: memb_def[symmetric] memb_finter_raw)
 
       
   271   by (auto simp add: memb_def)
 
       
   272 
       
   273 instantiation fset :: (type) "{bot,distrib_lattice}"
 
    67 begin
 
   274 begin
 
    68 
   275 
    69 quotient_definition
 
   276 quotient_definition
 
    70   "bot :: 'a fset" is "[] :: 'a list"
 
   277   "bot :: 'a fset" is "[] :: 'a list"
 
    71 
   278 
    90 
   297 
    91 abbreviation
 
   298 abbreviation
 
    92   f_subset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50)
 
   299   f_subset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50)
 
    93 where
 
   300 where
 
    94   "xs |\<subset>| ys \<equiv> xs < ys"
 
   301   "xs |\<subset>| ys \<equiv> xs < ys"
 
       
   302 
       
   303 quotient_definition
 
       
   304   "sup  \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
 
       
   305 is
 
       
   306   "(op @) \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
 
       
   307 
       
   308 abbreviation
 
       
   309   funion  (infixl "|\<union>|" 65)
 
       
   310 where
 
       
   311   "xs |\<union>| ys \<equiv> sup (xs :: 'a fset) ys"
 
       
   312 
       
   313 quotient_definition
 
       
   314   "inf  \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
 
       
   315 is
 
       
   316   "finter_raw \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
 
       
   317 
       
   318 abbreviation
 
       
   319   finter (infixl "|\<inter>|" 65)
 
       
   320 where
 
       
   321   "xs |\<inter>| ys \<equiv> inf (xs :: 'a fset) ys"
 
    95 
   322 
    96 instance
 
   323 instance
 
    97 proof
 
   324 proof
 
    98   fix x y z :: "'a fset"
 
   325   fix x y z :: "'a fset"
 
    99   show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)"
 
   326   show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)"
 
   100     unfolding less_fset by (lifting sub_list_not_eq)
 
   327     unfolding less_fset by (lifting sub_list_not_eq)
 
   101   show "x |\<subseteq>| x" by (lifting sub_list_refl)
 
   328   show "x |\<subseteq>| x" by (lifting sub_list_refl)
 
   102   show "{||} |\<subseteq>| x" by (lifting sub_list_empty)
 
   329   show "{||} |\<subseteq>| x" by (lifting sub_list_empty)
 
       
   330   show "x |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_left)
 
       
   331   show "y |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_right)
 
       
   332   show "x |\<inter>| y |\<subseteq>| x" by (lifting sub_list_inter_left)
 
       
   333   show "x |\<inter>| y |\<subseteq>| y" by (lifting sub_list_inter_right)
 
       
   334   show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" by (lifting append_inter_distrib)
 
   103 next
 
   335 next
 
   104   fix x y z :: "'a fset"
 
   336   fix x y z :: "'a fset"
 
   105   assume a: "x |\<subseteq>| y"
 
   337   assume a: "x |\<subseteq>| y"
 
   106   assume b: "y |\<subseteq>| z"
 
   338   assume b: "y |\<subseteq>| z"
 
   107   show "x |\<subseteq>| z" using a b by (lifting sub_list_trans)
 
   339   show "x |\<subseteq>| z" using a b by (lifting sub_list_trans)
 
   108 qed
 
       
   109 end
 
       
   110 
       
   111 lemma sub_list_append_left:
 
       
   112   "sub_list x (x @ y)"
 
       
   113   by (simp add: sub_list_def)
 
       
   114 
       
   115 lemma sub_list_append_right:
 
       
   116   "sub_list y (x @ y)"
 
       
   117   by (simp add: sub_list_def)
 
       
   118 
       
   119 lemma sub_list_list_eq:
 
       
   120   "sub_list x y \<Longrightarrow> sub_list y x \<Longrightarrow> list_eq x y"
 
       
   121   unfolding sub_list_def list_eq.simps by blast
 
       
   122 
       
   123 lemma sub_list_append:
 
       
   124   "sub_list y x \<Longrightarrow> sub_list z x \<Longrightarrow> sub_list (y @ z) x"
 
       
   125   unfolding sub_list_def by auto
 
       
   126 
       
   127 instantiation fset :: (type) "semilattice_sup"
 
       
   128 begin
 
       
   129 
       
   130 quotient_definition
 
       
   131   "sup  \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
 
       
   132 is
 
       
   133   "(op @) \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
 
       
   134 
       
   135 abbreviation
 
       
   136   funion  (infixl "|\<union>|" 65)
 
       
   137 where
 
       
   138   "xs |\<union>| ys \<equiv> sup (xs :: 'a fset) ys"
 
       
   139 
       
   140 instance
 
       
   141 proof
 
       
   142   fix x y :: "'a fset"
 
       
   143   show "x |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_left)
 
       
   144   show "y |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_right)
 
       
   145 next
 
   340 next
 
   146   fix x y :: "'a fset"
 
   341   fix x y :: "'a fset"
 
   147   assume a: "x |\<subseteq>| y"
 
   342   assume a: "x |\<subseteq>| y"
 
   148   assume b: "y |\<subseteq>| x"
 
   343   assume b: "y |\<subseteq>| x"
 
   149   show "x = y" using a b by (lifting sub_list_list_eq)
 
   344   show "x = y" using a b by (lifting sub_list_list_eq)
 
   150 next
 
   345 next
 
   151   fix x y z :: "'a fset"
 
   346   fix x y z :: "'a fset"
 
   152   assume a: "y |\<subseteq>| x"
 
   347   assume a: "y |\<subseteq>| x"
 
   153   assume b: "z |\<subseteq>| x"
 
   348   assume b: "z |\<subseteq>| x"
 
   154   show "y |\<union>| z |\<subseteq>| x" using a b by (lifting sub_list_append)
 
   349   show "y |\<union>| z |\<subseteq>| x" using a b by (lifting sub_list_append)
 
       
   350 next
 
       
   351   fix x y z :: "'a fset"
 
       
   352   assume a: "x |\<subseteq>| y"
 
       
   353   assume b: "x |\<subseteq>| z"
 
       
   354   show "x |\<subseteq>| y |\<inter>| z" using a b by (lifting sub_list_inter)
 
   155 qed
 
   355 qed
 
       
   356 
   156 end
 
   357 end
 
   157 
   358 
   158 section {* Empty fset, Finsert and Membership *}
 
   359 section {* Finsert and Membership *}
 
   159 
   360 
   160 quotient_definition
 
   361 quotient_definition
 
   161   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 
   362   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 
   162 is "op #"
 
   363 is "op #"
 
   163 
   364 
   175 
   376 
   176 abbreviation
 
   377 abbreviation
 
   177   fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)
 
   378   fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)
 
   178 where
 
   379 where
 
   179   "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
 
   380   "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
 
   180 
       
   181 lemma memb_rsp[quot_respect]:
 
       
   182   shows "(op = ===> op \<approx> ===> op =) memb memb"
 
       
   183 by (auto simp add: memb_def)
 
       
   184 
       
   185 lemma nil_rsp[quot_respect]:
 
       
   186   shows "[] \<approx> []"
 
       
   187 by simp
 
       
   188 
       
   189 lemma cons_rsp[quot_respect]:
 
       
   190   shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
 
       
   191 by simp
 
       
   192 
   381 
   193 section {* Augmenting an fset -- @{const finsert} *}
 
   382 section {* Augmenting an fset -- @{const finsert} *}
 
   194 
   383 
   195 lemma nil_not_cons:
 
   384 lemma nil_not_cons:
 
   196   shows "\<not> ([] \<approx> x # xs)"
 
   385   shows "\<not> ([] \<approx> x # xs)"
 
   197   and   "\<not> (x # xs \<approx> [])"
 
   386   and   "\<not> (x # xs \<approx> [])"
 
   198   by auto
 
   387   by auto
 
   199 
   388 
   200 lemma not_memb_nil:
 
       
   201   shows "\<not> memb x []"
 
       
   202   by (simp add: memb_def)
 
       
   203 
       
   204 lemma no_memb_nil:
 
   389 lemma no_memb_nil:
 
   205   "(\<forall>x. \<not> memb x xs) = (xs = [])"
 
   390   "(\<forall>x. \<not> memb x xs) = (xs = [])"
 
   206   by (simp add: memb_def)
 
   391   by (simp add: memb_def)
 
   207 
   392 
   208 lemma none_memb_nil:
 
       
   209   "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
 
       
   210   by (simp add: memb_def)
 
       
   211 
       
   212 lemma memb_cons_iff:
 
       
   213   shows "memb x (y # xs) = (x = y \<or> memb x xs)"
 
       
   214   by (induct xs) (auto simp add: memb_def)
 
       
   215 
       
   216 lemma memb_consI1:
 
   393 lemma memb_consI1:
 
   217   shows "memb x (x # xs)"
 
   394   shows "memb x (x # xs)"
 
   218   by (simp add: memb_def)
 
   395   by (simp add: memb_def)
 
   219 
   396 
   220 lemma memb_consI2:
 
   397 lemma memb_consI2:
 
   221   shows "memb x xs \<Longrightarrow> memb x (y # xs)"
 
   398   shows "memb x xs \<Longrightarrow> memb x (y # xs)"
 
   222   by (simp add: memb_def)
 
   399   by (simp add: memb_def)
 
   223 
   400 
   224 lemma memb_absorb:
 
       
   225   shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
 
       
   226   by (induct xs) (auto simp add: memb_def id_simps)
 
       
   227 
       
   228 section {* Singletons *}
 
   401 section {* Singletons *}
 
   229 
   402 
   230 lemma singleton_list_eq:
 
   403 lemma singleton_list_eq:
 
   231   shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
 
   404   shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
 
   232   by (simp add: id_simps) auto
 
   405   by (simp add: id_simps) auto
 
   237   "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)"
 
   238   by (auto simp add: memb_def sub_list_def)
 
   411   by (auto simp add: memb_def sub_list_def)
 
   239 
   412 
   240 section {* Cardinality of finite sets *}
 
   413 section {* Cardinality of finite sets *}
 
   241 
   414 
   242 fun
 
       
   243   fcard_raw :: "'a list \<Rightarrow> nat"
 
       
   244 where
 
       
   245   fcard_raw_nil:  "fcard_raw [] = 0"
 
       
   246 | fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))"
 
       
   247 
       
   248 quotient_definition
 
   415 quotient_definition
 
   249   "fcard :: 'a fset \<Rightarrow> nat" 
   416   "fcard :: 'a fset \<Rightarrow> nat" 
   250 is
 
   417 is
 
   251   "fcard_raw"
 
   418   "fcard_raw"
 
   252 
   419 
   253 lemma fcard_raw_0:
 
   420 lemma fcard_raw_0:
 
   254   shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
 
   421   shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
 
   255   by (induct xs) (auto simp add: memb_def)
 
   422   by (induct xs) (auto simp add: memb_def)
 
   256 
   423 
   257 lemma fcard_raw_gt_0:
 
       
   258   assumes a: "x \<in> set xs"
 
       
   259   shows "0 < fcard_raw xs"
 
       
   260   using a by (induct xs) (auto simp add: memb_def)
 
       
   261 
   424 
   262 lemma fcard_raw_not_memb:
 
   425 lemma fcard_raw_not_memb:
 
   263   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)"
 
   264   by auto
 
   427   by auto
 
   265 
   428 
   282   apply (subgoal_tac "set xs = {x}")
 
   445   apply (subgoal_tac "set xs = {x}")
 
   283   apply (drule singleton_fcard_1)
 
   446   apply (drule singleton_fcard_1)
 
   284   apply auto
 
   447   apply auto
 
   285   done
 
   448   done
 
   286 
   449 
   287 lemma fcard_raw_delete_one:
 
       
   288   shows "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
 
       
   289   by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)
 
       
   290 
       
   291 lemma fcard_raw_suc_memb:
 
   450 lemma fcard_raw_suc_memb:
 
   292   assumes a: "fcard_raw A = Suc n"
 
   451   assumes a: "fcard_raw A = Suc n"
 
   293   shows "\<exists>a. memb a A"
 
   452   shows "\<exists>a. memb a A"
 
   294   using a
 
   453   using a
 
   295   apply (induct A)
 
   454   apply (induct A)
 
   305   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
 
   306   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
 
   307   then show ?thesis using fcard_raw_0[of A] by simp
 
   466   then show ?thesis using fcard_raw_0[of A] by simp
 
   308 qed
 
   467 qed
 
   309 
   468 
   310 lemma fcard_raw_rsp_aux:
 
   469 section {* fmap *}
 
   311   assumes a: "xs \<approx> ys"
 
       
   312   shows "fcard_raw xs = fcard_raw ys"
 
       
   313   using a
 
       
   314   apply(induct xs arbitrary: ys)
 
       
   315   apply(auto simp add: memb_def)
 
       
   316   apply(subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys)")
 
       
   317   apply simp
 
       
   318   apply auto
 
       
   319   apply (drule_tac x="x" in spec)
 
       
   320   apply blast
 
       
   321   apply(drule_tac x="[x \<leftarrow> ys. x \<noteq> a]" in meta_spec)
 
       
   322   apply(simp add: fcard_raw_delete_one memb_def)
 
       
   323   apply (case_tac "a \<in> set ys")
 
       
   324   apply (simp only: if_True)
 
       
   325   apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)")
 
       
   326   apply (drule Suc_pred'[OF fcard_raw_gt_0])
 
       
   327   apply auto
 
       
   328   done
 
       
   329 
       
   330 lemma fcard_raw_rsp[quot_respect]:
 
       
   331   shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
 
       
   332   by (simp add: fcard_raw_rsp_aux)
 
       
   333 
       
   334 
       
   335 section {* fmap and fset comprehension *}
 
       
   336 
   470 
   337 quotient_definition
 
   471 quotient_definition
 
   338   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 
   472   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 
   339 is
 
   473 is
 
   340  "map"
 
   474  "map"
 
   344   by simp
 
   478   by simp
 
   345 
   479 
   346 lemma memb_append:
 
   480 lemma memb_append:
 
   347   "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"
 
   348   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)
 
   349 
       
   350 text {* raw section *}
 
       
   351 
       
   352 lemma map_rsp[quot_respect]:
 
       
   353   shows "(op = ===> op \<approx> ===> op \<approx>) map map"
 
       
   354   by auto
 
       
   355 
   483 
   356 lemma cons_left_comm:
 
   484 lemma cons_left_comm:
 
   357   "x # y # xs \<approx> y # x # xs"
 
   485   "x # y # xs \<approx> y # x # xs"
 
   358   by auto
 
   486   by auto
 
   359 
   487 
   380   apply (auto simp add: memb_def)
 
   508   apply (auto simp add: memb_def)
 
   381   done
 
   509   done
 
   382 
   510 
   383 section {* deletion *}
 
   511 section {* deletion *}
 
   384 
   512 
   385 fun
 
       
   386   delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
 
       
   387 where
 
       
   388   "delete_raw [] x = []"
 
       
   389 | "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
 
       
   390 
       
   391 lemma memb_delete_raw:
 
       
   392   "memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)"
 
       
   393   by (induct xs arbitrary: x y) (auto simp add: memb_def)
 
       
   394 
       
   395 lemma delete_raw_rsp:
 
       
   396   "xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x"
 
       
   397   by (simp add: memb_def[symmetric] memb_delete_raw)
 
       
   398 
       
   399 lemma [quot_respect]:
 
       
   400   "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
 
       
   401   by (simp add: memb_def[symmetric] memb_delete_raw)
 
       
   402 
       
   403 lemma memb_delete_raw_ident:
 
   513 lemma memb_delete_raw_ident:
 
   404   shows "\<not> memb x (delete_raw xs x)"
 
   514   shows "\<not> memb x (delete_raw xs x)"
 
   405   by (induct xs) (auto simp add: memb_def)
 
   515   by (induct xs) (auto simp add: memb_def)
 
   406 
   516 
   407 lemma not_memb_delete_raw_ident:
 
       
   408   shows "\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"
 
       
   409   by (induct xs) (auto simp add: memb_def)
 
       
   410 
       
   411 lemma fset_raw_delete_raw_cases:
 
   517 lemma fset_raw_delete_raw_cases:
 
   412   "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)"
 
   413   by (induct xs) (auto simp add: memb_def)
 
   519   by (induct xs) (auto simp add: memb_def)
 
   414 
   520 
   415 lemma fdelete_raw_filter:
 
   521 lemma fdelete_raw_filter:
 
   418 
   524 
   419 lemma fcard_raw_delete:
 
   525 lemma fcard_raw_delete:
 
   420   "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)"
 
   421   by (simp add: fdelete_raw_filter fcard_raw_delete_one)
 
   527   by (simp add: fdelete_raw_filter fcard_raw_delete_one)
 
   422 
   528 
   423 lemma set_rsp[quot_respect]:
 
   529 
   424   "(op \<approx> ===> op =) set set"
 
   530 
   425   by auto
 
   531 
   426 
       
   427 definition
 
       
   428   rsp_fold
 
       
   429 where
 
       
   430   "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
 
       
   431 
       
   432 primrec
 
       
   433   ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
 
       
   434 where
 
       
   435   "ffold_raw f z [] = z"
 
       
   436 | "ffold_raw f z (a # A) =
 
       
   437      (if (rsp_fold f) then
 
       
   438        if memb a A then ffold_raw f z A
 
       
   439        else f a (ffold_raw f z A)
 
       
   440      else z)"
 
       
   441 
       
   442 lemma memb_commute_ffold_raw:
 
       
   443   "rsp_fold f \<Longrightarrow> memb h b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (delete_raw b h))"
 
       
   444   apply (induct b)
 
       
   445   apply (simp add: not_memb_nil)
 
       
   446   apply (simp add: ffold_raw.simps)
 
       
   447   apply (rule conjI)
 
       
   448   apply (rule_tac [!] impI)
 
       
   449   apply (rule_tac [!] conjI)
 
       
   450   apply (rule_tac [!] impI)
 
       
   451   apply (simp_all add: memb_delete_raw)
 
       
   452   apply (simp add: memb_cons_iff)
 
       
   453   apply (simp add: not_memb_delete_raw_ident)
 
       
   454   apply (simp add: memb_cons_iff rsp_fold_def)
 
       
   455   done
 
       
   456 
       
   457 lemma ffold_raw_rsp_pre:
 
       
   458   "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
 
       
   459   apply (induct a arbitrary: b)
 
       
   460   apply (simp add: hd_in_set memb_absorb memb_def none_memb_nil)
 
       
   461   apply (simp add: ffold_raw.simps)
 
       
   462   apply (rule conjI)
 
       
   463   apply (rule_tac [!] impI)
 
       
   464   apply (rule_tac [!] conjI)
 
       
   465   apply (rule_tac [!] impI)
 
       
   466   apply (subgoal_tac "\<forall>e. memb e a2 = memb e b")
 
       
   467   apply (simp)
 
       
   468   apply (simp add: memb_cons_iff memb_def)
 
       
   469   apply auto
 
       
   470   apply (drule_tac x="e" in spec)
 
       
   471   apply blast
 
       
   472   apply (case_tac b)
 
       
   473   apply simp_all
 
       
   474   apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))")
 
       
   475   apply (simp only:)
 
       
   476   apply (rule_tac f="f a1" in arg_cong)
 
       
   477   apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)")
 
       
   478   apply simp
 
       
   479   apply (simp add: memb_delete_raw)
 
       
   480   apply (auto simp add: memb_cons_iff)[1]
 
       
   481   apply (erule memb_commute_ffold_raw)
 
       
   482   apply (drule_tac x="a1" in spec)
 
       
   483   apply (simp add: memb_cons_iff)
 
       
   484   apply (simp add: memb_cons_iff)
 
       
   485   apply (case_tac b)
 
       
   486   apply simp_all
 
       
   487   done
 
       
   488 
       
   489 lemma [quot_respect]:
 
       
   490   "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
 
       
   491   by (simp add: memb_def[symmetric] ffold_raw_rsp_pre)
 
       
   492 
       
   493 primrec
 
       
   494   finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
       
   495 where
 
       
   496   "finter_raw [] l = []"
 
       
   497 | "finter_raw (h # t) l =
 
       
   498      (if memb h l then h # (finter_raw t l) else finter_raw t l)"
 
       
   499 
   532 
   500 lemma finter_raw_empty:
 
   533 lemma finter_raw_empty:
 
   501   "finter_raw l [] = []"
 
   534   "finter_raw l [] = []"
 
   502   by (induct l) (simp_all add: not_memb_nil)
 
   535   by (induct l) (simp_all add: not_memb_nil)
 
   503 
   536 
   504 lemma memb_finter_raw:
 
       
   505   "memb x (finter_raw xs ys) \<longleftrightarrow> memb x xs \<and> memb x ys"
 
       
   506   apply (induct xs)
 
       
   507   apply (simp add: not_memb_nil)
 
       
   508   apply (simp add: finter_raw.simps)
 
       
   509   apply (simp add: memb_cons_iff)
 
       
   510   apply auto
 
       
   511   done
 
       
   512 
       
   513 lemma [quot_respect]:
 
       
   514   "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
 
       
   515   by (simp add: memb_def[symmetric] memb_finter_raw)
 
       
   516 
       
   517 section {* Constants on the Quotient Type *} 
   537 section {* Constants on the Quotient Type *} 
   518 
   538 
   519 quotient_definition
 
   539 quotient_definition
 
   520   "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" 
   540   "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" 
   521   is "delete_raw"
 
   541   is "delete_raw"
 
   525   is "set"
 
   545   is "set"
 
   526 
   546 
   527 quotient_definition
 
   547 quotient_definition
 
   528   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
 
   548   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
 
   529   is "ffold_raw"
 
   549   is "ffold_raw"
 
   530 
       
   531 quotient_definition
 
       
   532   finter (infix "|\<inter>|" 50)
 
       
   533 where
 
       
   534   "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 
       
   535 is "finter_raw"
 
       
   536 
       
   537 lemma funion_sym_pre:
 
       
   538   "xs @ ys \<approx> ys @ xs"
 
       
   539   by auto
 
       
   540 
   550 
   541 lemma set_cong: 
   551 lemma set_cong: 
   542   shows "(set x = set y) = (x \<approx> y)"
 
   552   shows "(set x = set y) = (x \<approx> y)"
 
   543   by auto
 
   553   by auto
 
   544 
   554 
   549 quotient_definition
 
   559 quotient_definition
 
   550   "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
 
   560   "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
 
   551 is
 
   561 is
 
   552   "concat"
 
   562   "concat"
 
   553 
   563 
   554 lemma list_equiv_rsp[quot_respect]:
 
       
   555   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
 
       
   556   by auto
 
       
   557 
   564 
   558 text {* alternate formulation with a different decomposition principle
 
   565 text {* alternate formulation with a different decomposition principle
 
   559   and a proof of equivalence *}
 
   566   and a proof of equivalence *}
 
   560 
   567 
   561 inductive
 
   568 inductive
 
   577   apply (induct A)
 
   584   apply (induct A)
 
   578   apply (simp add: memb_def list_eq2_refl)
 
   585   apply (simp add: memb_def list_eq2_refl)
 
   579   apply (case_tac "memb a (aa # A)")
 
   586   apply (case_tac "memb a (aa # A)")
 
   580   apply (simp_all only: memb_cons_iff)
 
   587   apply (simp_all only: memb_cons_iff)
 
   581   apply (case_tac [!] "a = aa")
 
   588   apply (case_tac [!] "a = aa")
 
   582   apply (simp_all add: delete_raw.simps)
 
   589   apply (simp_all)
 
   583   apply (case_tac "memb a A")
 
   590   apply (case_tac "memb a A")
 
   584   apply (auto simp add: memb_def)[2]
 
   591   apply (auto simp add: memb_def)[2]
 
   585   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))
 
   586   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))
 
   587   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)
 
   590 lemma memb_delete_list_eq2:
 
   597 lemma memb_delete_list_eq2:
 
   591   assumes a: "memb e r"
 
   598   assumes a: "memb e r"
 
   592   shows "list_eq2 (e # delete_raw r e) r"
 
   599   shows "list_eq2 (e # delete_raw r e) r"
 
   593   using a cons_delete_list_eq2[of e r]
 
   600   using a cons_delete_list_eq2[of e r]
 
   594   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)
 
   595 
   606 
   596 lemma list_eq2_equiv_aux:
 
   607 lemma list_eq2_equiv_aux:
 
   597   assumes a: "fcard_raw l = n"
 
   608   assumes a: "fcard_raw l = n"
 
   598   and b: "l \<approx> r"
 
   609   and b: "l \<approx> r"
 
   599   shows "list_eq2 l r"
 
   610   shows "list_eq2 l r"
 
   729 
   740 
   730 lemma funion_empty[simp]:
 
   741 lemma funion_empty[simp]:
 
   731   shows "S |\<union>| {||} = S"
 
   742   shows "S |\<union>| {||} = S"
 
   732   by (lifting append_Nil2)
 
   743   by (lifting append_Nil2)
 
   733 
   744 
   734 lemma funion_sym:
 
   745 thm sup.commute[where 'a="'a fset"]
 
   735   shows "S |\<union>| T = T |\<union>| S"
 
   746 
   736   by (lifting funion_sym_pre)
 
   747 thm sup.assoc[where 'a="'a fset"]
 
   737 
       
   738 lemma funion_assoc:
 
       
   739   shows "S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)"
 
       
   740   by (lifting append_assoc)
 
       
   741 
   748 
   742 lemma singleton_union_left:
 
   749 lemma singleton_union_left:
 
   743   "{|a|} |\<union>| S = finsert a S"
 
   750   "{|a|} |\<union>| S = finsert a S"
 
   744   by simp
 
   751   by simp
 
   745 
   752 
   746 lemma singleton_union_right:
 
   753 lemma singleton_union_right:
 
   747   "S |\<union>| {|a|} = finsert a S"
 
   754   "S |\<union>| {|a|} = finsert a S"
 
   748   by (subst funion_sym) simp
 
   755   by (subst sup.commute) simp
 
   749 
   756 
   750 section {* Induction and Cases rules for finite sets *}
 
   757 section {* Induction and Cases rules for finite sets *}
 
   751 
   758 
   752 lemma fset_strong_cases:
 
   759 lemma fset_strong_cases:
 
   753   "S = {||} \<or> (\<exists>x T. x |\<notin>| T \<and> S = finsert x T)"
 
   760   "S = {||} \<or> (\<exists>x T. x |\<notin>| T \<and> S = finsert x T)"
nominal2