32 quotient_type

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

    34 by (rule list_eq_equivp)

    35 

    36 lemma sub_list_rsp1: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list xs zs = sub_list ys zs"

    37   by (simp add: sub_list_def)

    38 

    39 lemma sub_list_rsp2: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list zs xs = sub_list zs ys"

    40   by (simp add: sub_list_def)

    41 

    42 lemma [quot_respect]:

    43   shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"

    44   by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2)

    45 

    46 lemma [quot_respect]:

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

    48   by auto

    49 

    50 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)"

    52   by (auto simp add: sub_list_def)

    53 

    54 lemma sub_list_refl:

    55   "sub_list x x"

    56   by (simp add: sub_list_def)

    57 

    58 lemma sub_list_trans:

    59   "sub_list x y \<Longrightarrow> sub_list y z \<Longrightarrow> sub_list x z"

    60   by (simp add: sub_list_def)

    61 

    62 lemma sub_list_empty:

    63   "sub_list [] x"

    64   by (simp add: sub_list_def)

    65 

    66 instantiation fset :: (type) bot

    67 begin

    68 

    69 quotient_definition

    70   "bot :: 'a fset" is "[] :: 'a list"

    71 

    72 abbreviation

    73   fempty  ("{||}")

    74 where

    75   "{||} \<equiv> bot :: 'a fset"

    76 

    77 quotient_definition

    78   "less_eq_fset \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)"

    79 is

    80   "sub_list \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> bool)"

    81 

    82 abbreviation

    83   f_subset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50)

    84 where

    85   "xs |\<subseteq>| ys \<equiv> xs \<le> ys"

    86 

    87 definition

    88   less_fset:

    89   "(xs :: 'a fset) < ys \<equiv> xs \<le> ys \<and> xs \<noteq> ys"

    90 

    91 abbreviation

    92   f_subset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50)

    93 where

    94   "xs |\<subset>| ys \<equiv> xs < ys"

    95 

    96 instance

    97 proof

    98   fix x y z :: "'a fset"

    99   show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)"

   100     unfolding less_fset by (lifting sub_list_not_eq)

   101   show "x |\<subseteq>| x" by (lifting sub_list_refl)

   102   show "{||} |\<subseteq>| x" by (lifting sub_list_empty)

   103 next

   104   fix x y z :: "'a fset"

   105   assume a: "x |\<subseteq>| y"

   106   assume b: "y |\<subseteq>| z"

   107   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

   146   fix x y :: "'a fset"

   147   assume a: "x |\<subseteq>| y"

   148   assume b: "y |\<subseteq>| x"

   149   show "x = y" using a b by (lifting sub_list_list_eq)

   150 next

   151   fix x y z :: "'a fset"

   152   assume a: "y |\<subseteq>| x"

   153   assume b: "z |\<subseteq>| x"

   154   show "y |\<union>| z |\<subseteq>| x" using a b by (lifting sub_list_append)

   155 qed

   156 end

   157 

   158 section {* Empty fset, Finsert and Membership *}

   159 

   160 quotient_definition

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

   162 is "op #"

   163 

   164 syntax

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

   166 

   167 translations

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

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

   170 

   171 quotient_definition

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

   173 where

   174   "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb"

   175 

   176 abbreviation

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

   178 where

   179   "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 

   193 section {* Augmenting an fset -- @{const finsert} *}

   194 

   195 lemma nil_not_cons:

   196   shows "\<not> ([] \<approx> x # xs)"

   197   and   "\<not> (x # xs \<approx> [])"

   198   by auto

   199 

   200 lemma not_memb_nil:

   201   shows "\<not> memb x []"

   202   by (simp add: memb_def)

   203 

   204 lemma no_memb_nil:

   205   "(\<forall>x. \<not> memb x xs) = (xs = [])"

   206   by (simp add: memb_def)

   207 

   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:

   217   shows "memb x (x # xs)"

   218   by (simp add: memb_def)

   219 

   220 lemma memb_consI2:

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

   222   by (simp add: memb_def)

   223 

   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 *}

   229 

   230 lemma singleton_list_eq:

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

   232   by (simp add: id_simps) auto

   233 

   234 section {* sub_list *}

   235 

   868 lemma fsubset_finsert:

   869   "(finsert x xs |\<subseteq>| ys) = (x |\<in>| ys \<and> xs |\<subseteq>| ys)"

   870   by (lifting sub_list_cons)

   871 

   872 thm sub_list_def[simplified memb_def[symmetric], quot_lifted, no_vars]

   873 

   874 lemma fsubset_fin: "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"

   875 by (rule meta_eq_to_obj_eq)

   876    (lifting sub_list_def[simplified memb_def[symmetric]])

   877