(*  Title:      HOL/Quotient_Examples/FSet.thy

    Author:     Cezary Kaliszyk, TU Munich

    Author:     Christian Urban, TU Munich

    Type of finite sets.

*)

theory FSet

imports Quotient_List

begin

text {* 

  The type of finite sets is created by a quotient construction

  over lists. The definition of the equivalence:

*}

fun

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

where

  "list_eq xs ys \<longleftrightarrow> set xs = set ys"

lemma list_eq_equivp:

  shows "equivp list_eq"

  unfolding equivp_reflp_symp_transp

  unfolding reflp_def symp_def transp_def

  by auto

text {* Fset type *}

quotient_type

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

  by (rule list_eq_equivp)

text {* 

  Definitions for membership, sublist, cardinality, 

  intersection, difference and respectful fold over 

  lists.

*}

fun

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

where

  "memb x xs \<longleftrightarrow> x \<in> set xs"

fun

  sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"

where 

  "sub_list xs ys \<longleftrightarrow> set xs \<subseteq> set ys"

fun

  card_list :: "'a list \<Rightarrow> nat"

where

  "card_list xs = card (set xs)"

fun

  inter_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"

where

  "inter_list xs ys = [x \<leftarrow> xs. x \<in> set xs \<and> x \<in> set ys]"

fun

  diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"

where

  "diff_list xs ys = [x \<leftarrow> xs. x \<notin> set ys]"

definition

  rsp_fold

where

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

primrec

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

where

  "fold_list f z [] = z"

| "fold_list f z (a # xs) =

     (if (rsp_fold f) then

       if a \<in> set xs then fold_list f z xs

       else f a (fold_list f z xs)

     else z)"

section {* Quotient composition lemmas *}

lemma list_all2_refl':

  assumes q: "equivp R"

  shows "(list_all2 R) r r"

  by (rule list_all2_refl) (metis equivp_def q)

lemma compose_list_refl:

  assumes q: "equivp R"

  shows "(list_all2 R OOO op \<approx>) r r"

proof

  have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])

  show "list_all2 R r r" by (rule list_all2_refl'[OF q])

  with * show "(op \<approx> OO list_all2 R) r r" ..

qed

lemma map_list_eq_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"

  unfolding list_eq.simps

  by (simp only: set_map)

lemma quotient_compose_list_g:

  assumes q: "Quotient R Abs Rep"

  and     e: "equivp R"

  shows  "Quotient ((list_all2 R) OOO (op \<approx>))

    (abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)"

  unfolding Quotient_def comp_def

proof (intro conjI allI)

  fix a r s

  show "abs_fset (map Abs (map Rep (rep_fset a))) = a"

    by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map_id)

  have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))"

    by (rule list_all2_refl'[OF e])

  have c: "(op \<approx> OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"

    by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)

  show "(list_all2 R OOO op \<approx>) (map Rep (rep_fset a)) (map Rep (rep_fset a))"

    by (rule, rule list_all2_refl'[OF e]) (rule c)

  show "(list_all2 R OOO op \<approx>) r s = ((list_all2 R OOO op \<approx>) r r \<and>

        (list_all2 R OOO op \<approx>) s s \<and> abs_fset (map Abs r) = abs_fset (map Abs s))"

  proof (intro iffI conjI)

    show "(list_all2 R OOO op \<approx>) r r" by (rule compose_list_refl[OF e])

    show "(list_all2 R OOO op \<approx>) s s" by (rule compose_list_refl[OF e])

  next

    assume a: "(list_all2 R OOO op \<approx>) r s"

    then have b: "map Abs r \<approx> map Abs s"

    proof (elim pred_compE)

      fix b ba

      assume c: "list_all2 R r b"

      assume d: "b \<approx> ba"

      assume e: "list_all2 R ba s"

      have f: "map Abs r = map Abs b"

        using Quotient_rel[OF list_quotient[OF q]] c by blast

      have "map Abs ba = map Abs s"

        using Quotient_rel[OF list_quotient[OF q]] e by blast

      then have g: "map Abs s = map Abs ba" by simp

      then show "map Abs r \<approx> map Abs s" using d f map_list_eq_cong by simp

    qed

    then show "abs_fset (map Abs r) = abs_fset (map Abs s)"

      using Quotient_rel[OF Quotient_fset] by blast

  next

    assume a: "(list_all2 R OOO op \<approx>) r r \<and> (list_all2 R OOO op \<approx>) s s

      \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"

    then have s: "(list_all2 R OOO op \<approx>) s s" by simp

    have d: "map Abs r \<approx> map Abs s"

      by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)

    have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"

      by (rule map_list_eq_cong[OF d])

    have y: "list_all2 R (map Rep (map Abs s)) s"

      by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl'[OF e, of s]])

    have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s"

      by (rule pred_compI) (rule b, rule y)

    have z: "list_all2 R r (map Rep (map Abs r))"

      by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl'[OF e, of r]])

    then show "(list_all2 R OOO op \<approx>) r s"

      using a c pred_compI by simp

  qed

qed

lemma quotient_compose_list[quot_thm]:

  shows  "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))

    (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"

  by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp)

subsection {* Respectfulness lemmas for list operations *}

lemma list_equiv_rsp [quot_respect]:

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

  by auto

lemma append_rsp [quot_respect]:

  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"

  by simp

lemma sub_list_rsp [quot_respect]:

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

  by simp

lemma memb_rsp [quot_respect]:

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

  by simp

lemma nil_rsp [quot_respect]:

  shows "(op \<approx>) Nil Nil"

  by simp

lemma cons_rsp [quot_respect]:

  shows "(op = ===> op \<approx> ===> op \<approx>) Cons Cons"

  by simp

lemma map_rsp [quot_respect]:

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

  by auto

lemma set_rsp [quot_respect]:

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

  by auto

lemma inter_list_rsp [quot_respect]:

  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) inter_list inter_list"

  by simp

lemma removeAll_rsp [quot_respect]:

  shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"

  by simp

lemma diff_list_rsp [quot_respect]:

  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) diff_list diff_list"

  by simp

lemma card_list_rsp [quot_respect]:

  shows "(op \<approx> ===> op =) card_list card_list"

  by simp

lemma filter_rsp [quot_respect]:

  shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"

  by simp

lemma memb_commute_fold_list:

  assumes a: "rsp_fold f"

  and     b: "x \<in> set xs"

  shows "fold_list f y xs = f x (fold_list f y (removeAll x xs))"

  using a b by (induct xs) (auto simp add: rsp_fold_def)

lemma fold_list_rsp_pre:

  assumes a: "set xs = set ys"

  shows "fold_list f z xs = fold_list f z ys"

  using a

  apply (induct xs arbitrary: ys)

  apply (simp)

  apply (simp (no_asm_use))

  apply (rule conjI)

  apply (rule_tac [!] impI)

  apply (rule_tac [!] conjI)

  apply (rule_tac [!] impI)

  apply (metis insert_absorb)

  apply (metis List.insert_def List.set.simps(2) List.set_insert fold_list.simps(2))

  apply (metis Diff_insert_absorb insertI1 memb_commute_fold_list set_removeAll)

  apply(drule_tac x="removeAll a ys" in meta_spec)

  apply(auto)

  apply(drule meta_mp)

  apply(blast)

  by (metis List.set.simps(2) emptyE fold_list.simps(2) in_listsp_conv_set listsp.simps mem_def)

lemma fold_list_rsp [quot_respect]:

  shows "(op = ===> op = ===> op \<approx> ===> op =) fold_list fold_list"

  unfolding fun_rel_def

  by(auto intro: fold_list_rsp_pre)

lemma concat_rsp_pre:

  assumes a: "list_all2 op \<approx> x x'"

  and     b: "x' \<approx> y'"

  and     c: "list_all2 op \<approx> y' y"

  and     d: "\<exists>x\<in>set x. xa \<in> set x"

  shows "\<exists>x\<in>set y. xa \<in> set x"

proof -

  obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto

  have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_all2_find_element[OF e a])

  then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto

  have "ya \<in> set y'" using b h by simp

  then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_all2_find_element)

  then show ?thesis using f i by auto

qed

lemma concat_rsp [quot_respect]:

  shows "(list_all2 op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"

proof (rule fun_relI, elim pred_compE)

  fix a b ba bb

  assume a: "list_all2 op \<approx> a ba"

  assume b: "ba \<approx> bb"

  assume c: "list_all2 op \<approx> bb b"

  have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 

  proof

    fix x

    show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" 

    proof

      assume d: "\<exists>xa\<in>set a. x \<in> set xa"

      show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])

    next

      assume e: "\<exists>xa\<in>set b. x \<in> set xa"

      have a': "list_all2 op \<approx> ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a])

      have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b])

      have c': "list_all2 op \<approx> b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c])

      show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])

    qed

  qed

  then show "concat a \<approx> concat b" by auto

qed

section {* Quotient definitions for fsets *}

subsection {* Finite sets are a bounded, distributive lattice with minus *}

instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"

begin

quotient_definition

  "bot :: 'a fset" 

  is "Nil :: 'a list"

abbreviation

  empty_fset  ("{||}")

where

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

quotient_definition

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

  is "sub_list :: ('a list \<Rightarrow> 'a list \<Rightarrow> bool)"

abbreviation

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

where

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

definition

  less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool"

where  

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

abbreviation

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

where

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

quotient_definition

  "sup :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"

  is "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"

abbreviation

  union_fset (infixl "|\<union>|" 65)

where

  "xs |\<union>| ys \<equiv> sup xs (ys::'a fset)"

quotient_definition

  "inf :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"

  is "inter_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"

abbreviation

  inter_fset (infixl "|\<inter>|" 65)

where

  "xs |\<inter>| ys \<equiv> inf xs (ys::'a fset)"

quotient_definition

  "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"

  is "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"

instance

proof

  fix x y z :: "'a fset"

  show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x"

    unfolding less_fset_def 

    by (descending) (auto)

  show "x |\<subseteq>| x"  by (descending) (simp)

  show "{||} |\<subseteq>| x" by (descending) (simp)

  show "x |\<subseteq>| x |\<union>| y" by (descending) (simp)

  show "y |\<subseteq>| x |\<union>| y" by (descending) (simp)

  show "x |\<inter>| y |\<subseteq>| x" by (descending) (auto)

  show "x |\<inter>| y |\<subseteq>| y" by (descending) (auto)

  show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" 

    by (descending) (auto)

next

  fix x y z :: "'a fset"

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

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

  show "x |\<subseteq>| z" using a b by (descending) (simp)

next

  fix x y :: "'a fset"

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

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

  show "x = y" using a b by (descending) (auto)

next

  fix x y z :: "'a fset"

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

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

  show "y |\<union>| z |\<subseteq>| x" using a b by (descending) (simp)

next

  fix x y z :: "'a fset"

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

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

  show "x |\<subseteq>| y |\<inter>| z" using a b by (descending) (auto)

qed

end

subsection {* Other constants for fsets *}

quotient_definition

  "insert_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"

  is "Cons"

syntax

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

translations

  "{|x, xs|}" == "CONST insert_fset x {|xs|}"

  "{|x|}"     == "CONST insert_fset x {||}"

quotient_definition

  in_fset (infix "|\<in>|" 50)

where

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

abbreviation

  notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50)

where

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

subsection {* Other constants on the Quotient Type *}

quotient_definition

  "card_fset :: 'a fset \<Rightarrow> nat"

  is card_list

quotient_definition

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

  is map

quotient_definition

  "remove_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"

  is removeAll

quotient_definition

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

  is "set"

quotient_definition

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

  is fold_list

quotient_definition

  "concat_fset :: ('a fset) fset \<Rightarrow> 'a fset"

  is concat

quotient_definition

  "filter_fset :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"

  is filter

subsection {* Compositional respectfulness and preservation lemmas *}

lemma Nil_rsp2 [quot_respect]: 

  shows "(list_all2 op \<approx> OOO op \<approx>) Nil Nil"

  by (rule compose_list_refl, rule list_eq_equivp)

lemma Cons_rsp2 [quot_respect]:

  shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"

  apply auto

  apply (rule_tac b="x # b" in pred_compI)

  apply auto

  apply (rule_tac b="x # ba" in pred_compI)

  apply auto

  done

lemma map_prs [quot_preserve]: 

  shows "(abs_fset \<circ> map f) [] = abs_fset []"

  by simp

lemma insert_fset_rsp [quot_preserve]:

  "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) Cons = insert_fset"

  by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]

      abs_o_rep[OF Quotient_fset] map_id insert_fset_def)

lemma union_fset_rsp [quot_preserve]:

  "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) 

  append = union_fset"

  by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]

      abs_o_rep[OF Quotient_fset] map_id sup_fset_def)

lemma list_all2_app_l:

  assumes a: "reflp R"

  and b: "list_all2 R l r"

  shows "list_all2 R (z @ l) (z @ r)"