2 imports "../Quotient" "../Quotient_List" List

     2 imports "../../../Nominal/FSet"

     5 ML {*

     5 notation

     6 structure QuotientRules = Named_Thms

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

     7   (val name = "quot_thm"

     8    val description = "Quotient theorems.")

     9 *}

    10 

    11 ML {*

    12 open QuotientRules

    13 *}

    14 

    15 fun

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

    17 where

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

    19 

    20 lemma list_eq_equivp:

    21   shows "equivp list_eq"

    22 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def

    23 by auto

    24 

    25 (* FIXME-TODO: because of beta-reduction, one cannot give the *)

    26 (* FIXME-TODO: relation as a term or abbreviation             *) 

    27 quotient_type 

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

    29 by (rule list_eq_equivp)

    30 

    31 

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

    33 

    34 quotient_definition

    35   fempty  ("{||}")

    36 where

    37   "fempty :: 'a fset"

    38 is "[]::'a list"

    39 

    40 quotient_definition

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

    42 is "op #"

    43 

    44 syntax

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

    46 

    47 translations

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

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

    50 

    51 definition 

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

    53 where

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

    55 

    56 quotient_definition

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

    58 where

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

    60 is "memb"

    61 

    62 abbreviation

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

    64 where

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

    66 

    67 lemma memb_rsp[quot_respect]: 

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

    69 by (auto simp add: memb_def)

    70 

    71 lemma nil_rsp[quot_respect]:

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

    73 by simp

    74 

    75 lemma cons_rsp:

    76   "xa \<approx> ya \<Longrightarrow> y # xa \<approx> y # ya"

    77   by simp

    78 

    79 lemma [quot_respect]:

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

    81   by simp

    82 

    83 

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

    85 

    86 text {* raw section *}

    87 

    88 lemma nil_not_cons:

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

    90   by auto

    91 

    92 lemma memb_cons_iff:

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

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

    95 

    96 lemma memb_consI1:

    97   shows "memb x (x # xs)"

    98   by (simp add: memb_def)

    99 

   100 lemma memb_consI2:

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

   102   by (simp add: memb_def)

   103 

   104 lemma memb_absorb:

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

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

   107 

   108 text {* lifted section *}

   109 

   110 lemma fin_finsert_iff[simp]:

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

   112 by (lifting memb_cons_iff) 

   113 

   114 lemma

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

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

   117   by (lifting memb_consI1, lifting memb_consI2)

   118 

   119 

   120 lemma finsert_absorb [simp]: 

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

   122   by (lifting memb_absorb)

   123 

   124 

   125 section {* Singletons *}

   126 

   127 text {* raw section *}

   128 

   129 lemma singleton_list_eq:

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

   131   by (simp add: id_simps) auto

   132 

   133 text {* lifted section *}

   134 

   135 lemma fempty_not_finsert[simp]:

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

   137   by (lifting nil_not_cons)

   138 

   139 lemma fsingleton_eq[simp]:

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

   141   by (lifting singleton_list_eq)

   142 

   143 section {* Union *}

   144 

   145 quotient_definition

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

   147 where

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

   149 is

   150   "op @"

   151 

   152 section {* Cardinality of finite sets *}

   153 

   154 fun

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

   156 where

   157   fcard_raw_nil:  "fcard_raw [] = 0"

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

   159 

   160 quotient_definition

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

   162 is "fcard_raw"

   163 

   164 text {* raw section *}

   165 

   166 lemma fcard_raw_ge_0:

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

   168   shows "0 < fcard_raw xs"

   169 using a

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

   171 

   172 lemma fcard_raw_delete_one:

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

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

   175 

   176 lemma fcard_raw_rsp_aux:

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

   178   shows "fcard_raw a = fcard_raw b"

   179 using a

   180 apply(induct a arbitrary: b)

   181 apply(auto simp add: memb_def)

   182 apply(metis)

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

   184 apply(simp add: fcard_raw_delete_one)

   185 apply(metis Suc_pred' fcard_raw_ge_0 fcard_raw_delete_one memb_def)

   186 done

   187 

   188 lemma fcard_raw_rsp[quot_respect]:

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

   190   by (simp add: fcard_raw_rsp_aux)

   191 

   192 text {* lifted section *}

   193 

   194 lemma fcard_fempty [simp]:

   195   shows "fcard {||} = 0"

   196 by (lifting fcard_raw_nil)

   197 

   198 lemma fcard_finsert_if [simp]:

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

   200 by (lifting fcard_raw_cons)

   201 

   202 

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

   254 by (simp add: id_simps)

    19 by (simp)

   277   apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)

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

   278   done

   364   apply(simp add: comp_def)

   128   apply(simp add: comp_def bot_fset_def)

   365   apply(fold fempty_def[simplified id_simps])

   366   apply(rule refl)

   376   apply (rule cons_rsp)

   138   apply auto

   377   apply simp

   378   apply (auto)[1]