2 imports "../QuotMain" List

     2 imports "../QuotMain" "../QuotList" List

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

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

    15 quotient_type fset = "'a list" / "list_eq"

    15 quotient_type 

    16   by (rule list_eq_equivp)

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

    17 

    17 by (rule list_eq_equivp)

    18 lemma not_nil_equiv_cons: 

    18 

    19   "\<not>[] \<approx> a # A" 

    19 

    20 by auto

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

    21 

    22 quotient_definition

    23   "fempty :: 'a fset" ("{||}")

    24 as "[]::'a list"

    25 

    26 quotient_definition

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

    28 as "op #"

    29 

    30 syntax

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

    32 

    33 translations

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

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

    36 

    37 definition 

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

    39 where

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

    41 

    42 quotient_definition

    43   "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<in>| _" [50, 51] 50)

    44 as "memb"

    45 

    46 abbreviation

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

    48 where

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

    50 

    51 lemma memb_rsp[quot_respect]: 

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

    53 by (auto simp add: memb_def)

    24   by simp

    57 by simp

    28   by simp

    61 by simp

    29 

    62 

    30 (*

    63 

    31 lemma mem_rsp[quot_respect]:

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

    32   "(op = ===> op \<approx> ===> op =) (op mem) (op mem)"

    65 

    66 text {* raw section *}

    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)

    87 

    88 text {* lifted section *}

    89 

    90 lemma fempty_not_finsert[simp]:

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

    92 by (lifting nil_not_cons)

    93 

    94 lemma fin_finsert_iff[simp]:

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

    96 by (lifting memb_cons_iff) 

    97 

    98 lemma

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

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

   101   by (lifting memb_consI1, lifting memb_consI2)

   102 

   103 lemma finsert_absorb [simp]: 

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

   105 by (lifting memb_absorb)

   106 

   107 

   108 section {* Singletons *}

   109 

   110 text {* raw section *}

   111 

   112 lemma singleton_list_eq:

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

   114 by auto

   115 

   116 text {* lifted section *}

   117 

   118 lemma fsingleton_eq[simp]:

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

   120 by (lifting singleton_list_eq)

   121 

   122 

   123 section {* Cardinality of finite sets *}

   124 

   125 fun

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

   127 where

   128   fcard_raw_nil:  "fcard_raw [] = 0"

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

   130 

   131 quotient_definition

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

   133 as "fcard_raw"

   134 

   135 text {* raw section *}

   136 

   137 lemma fcard_raw_ge_0:

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

   139   shows "0 < fcard_raw xs"

   140 using a

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

   142 

   143 lemma fcard_raw_delete_one:

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

   145 by (induct xs) (auto dest: fcard_raw_ge_0 simp add: memb_def)

   146 

   147 lemma fcard_raw_rsp_aux:

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

   149   shows "fcard_raw a = fcard_raw b"

   150 using a

   151 apply(induct a arbitrary: b)

   152 apply(auto simp add: memb_def)

   153 apply(metis)

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

   155 apply(simp add: fcard_raw_delete_one)

   156 apply(metis Suc_pred' fcard_raw_ge_0 fcard_raw_delete_one memb_def)

   157 done

   158 

   159 lemma fcard_raw_rsp[quot_respect]:

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

   161   by (simp add: fcard_raw_rsp_aux)

   162 

   163 text {* lifted section *}

   164 

   165 lemma fcard_fempty [simp]:

   166   shows "fcard {||} = 0"

   167 by (lifting fcard_raw_nil)

   168 

   169 lemma fcard_finsert_if [simp]:

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

   171 by (lifting fcard_raw_cons)

   172 

   173 

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

   175 

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

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

   178 by (lifting list.exhaust)

   179 

   180 lemma fset_induct[case_names fempty finsert]:

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

   182 by (lifting list.induct)

   183 

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

   185   assumes prem1: "P {||}" 

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

   187   shows "P S"

   188 proof(induct S rule: fset_induct)

   189   case fempty

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

   191 next

   192   case (finsert x S)

   193   have asm: "P S" by fact

   194   show "P (finsert x S)"

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

   196     case True

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

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

   199   next

   200     case False

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

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

   203   qed

   204 qed

   205 

   206 

   207 section {* fmap and fset comprehension *}

   208 

   209 quotient_definition

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

   211 as

   212  "map"

   213 

   214 (* PROPBLEM

   215 quotient_definition

   216   "fconcat :: ('a fset) fset => 'a fset"

   217 as

   218  "concat"

   219 

   220 term concat

   221 term fconcat

   111 fun

   416 

   112   card_raw :: "'a list \<Rightarrow> nat"

   417 

   113 where

   418 

   114   card_raw_nil: "card_raw [] = 0"

   115 | card_raw_cons: "card_raw (x # xs) = (if x \<in> set xs then card_raw xs else Suc (card_raw xs))"

   116 

   117 lemma not_mem_card_raw:

   118   fixes x :: "'a"

   119   fixes xs :: "'a list"

   120   shows "(\<not>(x mem xs)) = (card_raw (x # xs) = Suc (card_raw xs))"

   121   sorry

   122 

   123 lemma card_raw_suc:

   124   assumes c: "card_raw xs = Suc n"

   125   shows "\<exists>a ys. (a \<notin> set ys) \<and> xs \<approx> (a # ys)"

   126   using c apply(induct xs)

   127   apply(simp)

   128   sorry

   129 

   130 lemma mem_card_raw_gt_0:

   131   "a \<in> set A \<Longrightarrow> 0 < card_raw A"

   132   by (induct A) (auto)

   133 

   134 lemma card_raw_cons_gt_0:

   135   "0 < card_raw (a # A)"

   136   by (induct A) (auto)

   137 

   138 lemma card_raw_delete_raw:

   139   "card_raw (delete_raw A a) = (if a \<in> set A then card_raw A - 1 else card_raw A)"

   140 sorry

   141 

   142 lemma card_raw_rsp_aux:

   143   assumes e: "a \<approx> b"

   144   shows "card_raw a = card_raw b"

   145   using e sorry

   146 

   147 lemma card_raw_rsp[quot_respect]:

   148   "(op \<approx> ===> op =) card_raw card_raw"

   149   by (simp add: card_raw_rsp_aux)

   150 

   151 lemma card_raw_0:

   152   "(card_raw A = 0) = (A = [])"

   153   by (induct A) (auto)

   274 thm card_raw.simps

   519 (*thm card_raw.simps*)

   275 thm not_mem_card_raw

   520 (*thm not_mem_card_raw*)

   276 thm card_raw_suc

   521 (*thm card_raw_suc*)

   282 thm card_raw_cons_gt_0

   527 (*thm card_raw_cons_gt_0

   287 thm card_raw_delete_raw

   533 (*thm card_raw_delete_raw*)