1 theory FSet

     2 imports Quotient Quotient_List List

     3 begin

     4 

     5 fun

     6   list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)

     7 where

     8   "list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)"

     9 

    10 lemma list_eq_equivp:

    11   shows "equivp list_eq"

    12 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def

    13 by auto

    14 

    15 quotient_type

    16   'a fset = "'a list" / "list_eq"

    17 by (rule list_eq_equivp)

    18 

    19 section {* empty fset, finsert and membership *}

    20 

    21 quotient_definition

    22   fempty  ("{||}")

    23 where

    24   "fempty :: 'a fset"

    25 is "[]::'a list"

    26 

    27 quotient_definition

    28   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" 

    29 is "op #"

    30 

    31 syntax

    32   "@Finset"     :: "args => 'a fset"  ("{|(_)|}")

    33 

    34 translations

    35   "{|x, xs|}" == "CONST finsert x {|xs|}"

    36   "{|x|}"     == "CONST finsert x {||}"

    37 

    38 definition

    39   memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"

    40 where

    41   "memb x xs \<equiv> x \<in> set xs"

    42 

    43 quotient_definition

    44   fin ("_ |\<in>| _" [50, 51] 50)

    45 where

    46   "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"

    47 is "memb"

    48 

    49 abbreviation

    50   fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)

    51 where

    52   "a |\<notin>| S \<equiv> \<not>(a |\<in>| S)"

    53 

    54 lemma memb_rsp[quot_respect]:

    55   shows "(op = ===> op \<approx> ===> op =) memb memb"

    56 by (auto simp add: memb_def)

    57 

    58 lemma nil_rsp[quot_respect]:

    59   shows "[] \<approx> []"

    60 by simp

    61 

    62 lemma cons_rsp[quot_respect]:

    63   shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"

    64 by simp

    65 

    66 section {* Augmenting a set -- @{const finsert} *}

    67 

    68 lemma nil_not_cons:

    69   shows "\<not>[] \<approx> x # xs"

    70   by auto

    71 

    72 lemma memb_cons_iff:

    73   shows "memb x (y # xs) = (x = y \<or> memb x xs)"

    74   by (induct xs) (auto simp add: memb_def)

    75 

    76 lemma memb_consI1:

    77   shows "memb x (x # xs)"

    78   by (simp add: memb_def)

    79 

    80 lemma memb_consI2:

    81   shows "memb x xs \<Longrightarrow> memb x (y # xs)"

    82   by (simp add: memb_def)

    83 

    84 lemma memb_absorb:

    85   shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"

    86   by (induct xs) (auto simp add: memb_def id_simps)

    87 

    88 section {* Singletons *}

    89 

    90 lemma singleton_list_eq:

    91   shows "[x] \<approx> [y] \<longleftrightarrow> x = y"

    92   by (simp add: id_simps) auto

    93 

    94 section {* Union *}

    95 

    96 quotient_definition

    97   funion  (infixl "|\<union>|" 65)

    98 where

    99   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"

   100 is

   101   "op @"

   102 

   103 section {* Cardinality of finite sets *}

   104 

   105 fun

   106   fcard_raw :: "'a list \<Rightarrow> nat"

   107 where

   108   fcard_raw_nil:  "fcard_raw [] = 0"

   109 | fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))"

   110 

   111 quotient_definition

   112   "fcard :: 'a fset \<Rightarrow> nat" 

   113 is

   114   "fcard_raw"

   115 

   116 lemma fcard_raw_gt_0:

   117   assumes a: "x \<in> set xs"

   118   shows "0 < fcard_raw xs"

   119   using a

   120   by (induct xs) (auto simp add: memb_def)

   121 

   122 lemma fcard_raw_delete_one:

   123   "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"

   124   by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)

   125 

   126 lemma fcard_raw_rsp_aux:

   127   assumes a: "a \<approx> b"

   128   shows "fcard_raw a = fcard_raw b"

   129   using a

   130   apply(induct a arbitrary: b)

   131   apply(auto simp add: memb_def)

   132   apply(metis)

   133   apply(drule_tac x="[x \<leftarrow> b. x \<noteq> a1]" in meta_spec)

   134   apply(simp add: fcard_raw_delete_one)

   135   apply(metis Suc_pred' fcard_raw_gt_0 fcard_raw_delete_one memb_def)

   136   done

   137 

   138 lemma fcard_raw_rsp[quot_respect]:

   139   "(op \<approx> ===> op =) fcard_raw fcard_raw"

   140   by (simp add: fcard_raw_rsp_aux)

   141 

   142 

   143 section {* fmap and fset comprehension *}

   144 

   145 quotient_definition

   146   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"

   147 is

   148  "map"

   149 

   150 text {* raw section *}

   151 

   152 lemma map_rsp_aux:

   153   assumes a: "a \<approx> b"

   154   shows "map f a \<approx> map f b"

   155   using a

   156   apply(induct a arbitrary: b)

   157   apply(auto)

   158   apply(metis rev_image_eqI)

   159   done

   160 

   161 lemma map_rsp[quot_respect]:

   162   shows "(op = ===> op \<approx> ===> op \<approx>) map map"

   163   by (auto simp add: map_rsp_aux)

   164 

   165 lemma cons_left_comm:

   166   "x # y # A \<approx> y # x # A"

   167   by (auto simp add: id_simps)

   168 

   169 lemma cons_left_idem:

   170   "x # x # A \<approx> x # A"

   171   by (auto simp add: id_simps)

   172 

   173 lemma none_mem_nil:

   174   "(\<forall>a. a \<notin> set A) = (A \<approx> [])"

   175   by simp

   176 

   177 lemma finite_set_raw_strong_cases:

   178   "(X = []) \<or> (\<exists>a Y. ((a \<notin> set Y) \<and> (X \<approx> a # Y)))"

   179   apply (induct X)

   180   apply (simp)

   181   apply (rule disjI2)

   182   apply (erule disjE)

   183   apply (rule_tac x="a" in exI)

   184   apply (rule_tac x="[]" in exI)

   185   apply (simp)

   186   apply (erule exE)+

   187   apply (case_tac "a = aa")

   188   apply (rule_tac x="a" in exI)

   189   apply (rule_tac x="Y" in exI)

   190   apply (simp)

   191   apply (rule_tac x="aa" in exI)

   192   apply (rule_tac x="a # Y" in exI)

   193   apply (auto)

   194   done

   195 

   196 fun

   197   delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"

   198 where

   199   "delete_raw [] x = []"

   200 | "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"

   201 

   202 lemma mem_delete_raw:

   203   "x \<in> set (delete_raw A a) = (x \<in> set A \<and> \<not>(x = a))"

   204   by (induct A arbitrary: x a) (auto)

   205 

   206 lemma mem_delete_raw_ident:

   207   "\<not>(a \<in> set (delete_raw A a))"

   208   by (induct A) (auto)

   209 

   210 lemma not_mem_delete_raw_ident:

   211   "b \<notin> set A \<Longrightarrow> (delete_raw A b = A)"

   212   by (induct A) (auto)

   213 

   214 lemma finite_set_raw_delete_raw_cases:

   215   "X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)"

   216   by (induct X) (auto)

   217 

   218 lemma list2set_thm:

   219   shows "set [] = {}"

   220   and "set (h # t) = insert h (set t)"

   221   by (auto)

   222 

   223 lemma list2set_rsp[quot_respect]:

   224   "(op \<approx> ===> op =) set set"

   225   by auto

   226 

   227 definition

   228   rsp_fold

   229 where

   230   "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"

   231 

   232 primrec

   233   fold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"

   234 where

   235   "fold_raw f z [] = z"

   236 | "fold_raw f z (a # A) =

   237      (if (rsp_fold f) then

   238        if a mem A then fold_raw f z A

   239        else f a (fold_raw f z A)

   240      else z)"

   241 

   242 section {* Constants on the Quotient Type *} 

   243 

   244 quotient_definition

   245   "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" 

   246   is "delete_raw"

   247 

   248 quotient_definition

   249   "fset_to_set :: 'a fset \<Rightarrow> 'a set" 

   250   is "set"

   251 

   252 lemma funion_sym_pre:

   253   "a @ b \<approx> b @ a"

   254   by auto

   255 

   256 

   257 lemma append_rsp[quot_respect]:

   258   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"

   259   by (auto)

   260 

   261 

   262 

   263 section {* lifted part *}

   264 

   265 

   266 lemma fin_finsert_iff[simp]:

   267   "x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"

   268   by (lifting memb_cons_iff)

   269 

   270 lemma

   271   shows finsertI1: "x |\<in>| finsert x S"

   272   and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"

   273   by (lifting memb_consI1, lifting memb_consI2)

   274 

   275 lemma finsert_absorb[simp]:

   276   shows "x |\<in>| S \<Longrightarrow> finsert x S = S"

   277   by (lifting memb_absorb)

   278 

   279 lemma fempty_not_finsert[simp]:

   280   shows "{||} \<noteq> finsert x S"

   281   by (lifting nil_not_cons)

   282 

   283 lemma finsert_left_comm:

   284   "finsert a (finsert b S) = finsert b (finsert a S)"

   285   by (lifting cons_left_comm)

   286 

   287 lemma finsert_left_idem:

   288   "finsert a (finsert a S) = finsert a S"

   289   by (lifting cons_left_idem)

   290 

   291 lemma fsingleton_eq[simp]:

   292   shows "{|x|} = {|y|} \<longleftrightarrow> x = y"

   293   by (lifting singleton_list_eq)

   294 

   295 text {* fset_to_set *}

   296 

   297 lemma fset_to_set_simps:

   298   "fset_to_set {||} = {}"

   299   "fset_to_set (finsert (h :: 'b) t) = insert h (fset_to_set t)"

   300   by (lifting list2set_thm)

   301 

   302 lemma in_fset_to_set:

   303   "x \<in> fset_to_set xs \<equiv> x |\<in>| xs"

   304   by (lifting memb_def[symmetric])

   305 

   306 lemma none_in_fempty:

   307   "(\<forall>a. a \<notin> fset_to_set A) = (A = {||})"

   308   by (lifting none_mem_nil)

   309 

   310 text {* fcard *}

   311 

   312 lemma fcard_fempty [simp]:

   313   shows "fcard {||} = 0"

   314   by (lifting fcard_raw_nil)

   315 

   316 lemma fcard_finsert_if [simp]:

   317   shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"

   318   by (lifting fcard_raw_cons)

   319 

   320 lemma fcard_gt_0: "x \<in> fset_to_set xs \<Longrightarrow> 0 < fcard xs"

   321   by (lifting fcard_raw_gt_0)

   322 

   323 text {* funion *}

   324 

   325 lemma funion_simps[simp]:

   326   "{||} |\<union>| ys = ys"

   327   "finsert x xs |\<union>| ys = finsert x (xs |\<union>| ys)"

   328   by (lifting append.simps)

   329 

   330 lemma funion_sym:

   331   "a |\<union>| b = b |\<union>| a"

   332   by (lifting funion_sym_pre)

   333 

   334 lemma funion_assoc:

   335  "x |\<union>| xa |\<union>| xb = x |\<union>| (xa |\<union>| xb)"

   336   by (lifting append_assoc)

   337 

   338 section {* Induction and Cases rules for finite sets *}

   339 

   340 lemma fset_strong_cases:

   341   "X = {||} \<or> (\<exists>a Y. a \<notin> fset_to_set Y \<and> X = finsert a Y)"

   342   by (lifting finite_set_raw_strong_cases)

   343 

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

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

   346   by (lifting list.exhaust)

   347 

   348 lemma fset_induct[case_names fempty finsert]:

   349   shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S"

   350   by (lifting list.induct)

   351 

   352 lemma fset_induct2[case_names fempty finsert, induct type: fset]:

   353   assumes prem1: "P {||}" 

   354   and     prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"

   355   shows "P S"

   356 proof(induct S rule: fset_induct)

   357   case fempty

   358   show "P {||}" by (rule prem1)

   359 next

   360   case (finsert x S)

   361   have asm: "P S" by fact

   362   show "P (finsert x S)"

   363   proof(cases "x |\<in>| S")

   364     case True

   365     have "x |\<in>| S" by fact

   366     then show "P (finsert x S)" using asm by simp

   367   next

   368     case False

   369     have "x |\<notin>| S" by fact

   370     then show "P (finsert x S)" using prem2 asm by simp

   371   qed

   372 qed

   373 

   374 

   375 

   376 end