theory FSet+
−
imports Quotient Quotient_List List+
−
begin+
−
+
−
fun+
−
  list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)+
−
where+
−
  "list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)"+
−
+
−
lemma list_eq_equivp:+
−
  shows "equivp list_eq"+
−
unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def+
−
by auto+
−
+
−
quotient_type+
−
  'a fset = "'a list" / "list_eq"+
−
by (rule list_eq_equivp)+
−
+
−
section {* empty fset, finsert and membership *}+
−
+
−
quotient_definition+
−
  fempty  ("{||}")+
−
where+
−
  "fempty :: 'a fset"+
−
is "[]::'a list"+
−
+
−
quotient_definition+
−
  "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" +
−
is "op #"+
−
+
−
syntax+
−
  "@Finset"     :: "args => 'a fset"  ("{|(_)|}")+
−
+
−
translations+
−
  "{|x, xs|}" == "CONST finsert x {|xs|}"+
−
  "{|x|}"     == "CONST finsert x {||}"+
−
+
−
definition+
−
  memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"+
−
where+
−
  "memb x xs \<equiv> x \<in> set xs"+
−
+
−
quotient_definition+
−
  fin ("_ |\<in>| _" [50, 51] 50)+
−
where+
−
  "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"+
−
is "memb"+
−
+
−
abbreviation+
−
  fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)+
−
where+
−
  "a |\<notin>| S \<equiv> \<not>(a |\<in>| S)"+
−
+
−
lemma memb_rsp[quot_respect]:+
−
  shows "(op = ===> op \<approx> ===> op =) memb memb"+
−
by (auto simp add: memb_def)+
−
+
−
lemma nil_rsp[quot_respect]:+
−
  shows "[] \<approx> []"+
−
by simp+
−
+
−
lemma cons_rsp[quot_respect]:+
−
  shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"+
−
by simp+
−
+
−
section {* Augmenting a set -- @{const finsert} *}+
−
+
−
lemma nil_not_cons:+
−
  shows+
−
  "\<not>[] \<approx> x # xs"+
−
  "\<not>x # xs \<approx> []"+
−
  by auto+
−
+
−
lemma memb_cons_iff:+
−
  shows "memb x (y # xs) = (x = y \<or> memb x xs)"+
−
  by (induct xs) (auto simp add: memb_def)+
−
+
−
lemma memb_consI1:+
−
  shows "memb x (x # xs)"+
−
  by (simp add: memb_def)+
−
+
−
lemma memb_consI2:+
−
  shows "memb x xs \<Longrightarrow> memb x (y # xs)"+
−
  by (simp add: memb_def)+
−
+
−
lemma memb_absorb:+
−
  shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"+
−
  by (induct xs) (auto simp add: memb_def id_simps)+
−
+
−
section {* Singletons *}+
−
+
−
lemma singleton_list_eq:+
−
  shows "[x] \<approx> [y] \<longleftrightarrow> x = y"+
−
  by (simp add: id_simps) auto+
−
+
−
section {* Union *}+
−
+
−
quotient_definition+
−
  funion  (infixl "|\<union>|" 65)+
−
where+
−
  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"+
−
is+
−
  "op @"+
−
+
−
section {* Cardinality of finite sets *}+
−
+
−
fun+
−
  fcard_raw :: "'a list \<Rightarrow> nat"+
−
where+
−
  fcard_raw_nil:  "fcard_raw [] = 0"+
−
| fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))"+
−
+
−
quotient_definition+
−
  "fcard :: 'a fset \<Rightarrow> nat" +
−
is+
−
  "fcard_raw"+
−
+
−
lemma fcard_raw_gt_0:+
−
  assumes a: "x \<in> set xs"+
−
  shows "0 < fcard_raw xs"+
−
  using a+
−
  by (induct xs) (auto simp add: memb_def)+
−
+
−
lemma fcard_raw_delete_one:+
−
  "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"+
−
  by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)+
−
+
−
lemma fcard_raw_rsp_aux:+
−
  assumes a: "a \<approx> b"+
−
  shows "fcard_raw a = fcard_raw b"+
−
  using a+
−
  apply(induct a arbitrary: b)+
−
  apply(auto simp add: memb_def)+
−
  apply(metis)+
−
  apply(drule_tac x="[x \<leftarrow> b. x \<noteq> a1]" in meta_spec)+
−
  apply(simp add: fcard_raw_delete_one)+
−
  apply(metis Suc_pred'[OF fcard_raw_gt_0] fcard_raw_delete_one memb_def)+
−
  done+
−
+
−
lemma fcard_raw_rsp[quot_respect]:+
−
  "(op \<approx> ===> op =) fcard_raw fcard_raw"+
−
  by (simp add: fcard_raw_rsp_aux)+
−
+
−
+
−
section {* fmap and fset comprehension *}+
−
+
−
quotient_definition+
−
  "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"+
−
is+
−
 "map"+
−
+
−
text {* raw section *}+
−
+
−
lemma map_rsp_aux:+
−
  assumes a: "a \<approx> b"+
−
  shows "map f a \<approx> map f b"+
−
  using a+
−
  apply(induct a arbitrary: b)+
−
  apply(auto)+
−
  apply(metis rev_image_eqI)+
−
  done+
−
+
−
lemma map_rsp[quot_respect]:+
−
  shows "(op = ===> op \<approx> ===> op \<approx>) map map"+
−
  by (auto simp add: map_rsp_aux)+
−
+
−
lemma cons_left_comm:+
−
  "x # y # A \<approx> y # x # A"+
−
  by (auto simp add: id_simps)+
−
+
−
lemma cons_left_idem:+
−
  "x # x # A \<approx> x # A"+
−
  by (auto simp add: id_simps)+
−
+
−
lemma none_mem_nil:+
−
  "(\<forall>a. a \<notin> set A) = (A \<approx> [])"+
−
  by simp+
−
+
−
lemma finite_set_raw_strong_cases:+
−
  "(X = []) \<or> (\<exists>a Y. ((a \<notin> set Y) \<and> (X \<approx> a # Y)))"+
−
  apply (induct X)+
−
  apply (simp)+
−
  apply (rule disjI2)+
−
  apply (erule disjE)+
−
  apply (rule_tac x="a" in exI)+
−
  apply (rule_tac x="[]" in exI)+
−
  apply (simp)+
−
  apply (erule exE)++
−
  apply (case_tac "a = aa")+
−
  apply (rule_tac x="a" in exI)+
−
  apply (rule_tac x="Y" in exI)+
−
  apply (simp)+
−
  apply (rule_tac x="aa" in exI)+
−
  apply (rule_tac x="a # Y" in exI)+
−
  apply (auto)+
−
  done+
−
+
−
fun+
−
  delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"+
−
where+
−
  "delete_raw [] x = []"+
−
| "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"+
−
+
−
lemma mem_delete_raw:+
−
  "x \<in> set (delete_raw A a) = (x \<in> set A \<and> \<not>(x = a))"+
−
  by (induct A arbitrary: x a) (auto)+
−
+
−
lemma mem_delete_raw_ident:+
−
  "\<not>(a \<in> set (delete_raw A a))"+
−
  by (induct A) (auto)+
−
+
−
lemma not_mem_delete_raw_ident:+
−
  "b \<notin> set A \<Longrightarrow> (delete_raw A b = A)"+
−
  by (induct A) (auto)+
−
+
−
lemma finite_set_raw_delete_raw_cases:+
−
  "X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)"+
−
  by (induct X) (auto)+
−
+
−
lemma list2set_thm:+
−
  shows "set [] = {}"+
−
  and "set (h # t) = insert h (set t)"+
−
  by (auto)+
−
+
−
lemma list2set_rsp[quot_respect]:+
−
  "(op \<approx> ===> op =) set set"+
−
  by auto+
−
+
−
definition+
−
  rsp_fold+
−
where+
−
  "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"+
−
+
−
primrec+
−
  fold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"+
−
where+
−
  "fold_raw f z [] = z"+
−
| "fold_raw f z (a # A) =+
−
     (if (rsp_fold f) then+
−
       if a mem A then fold_raw f z A+
−
       else f a (fold_raw f z A)+
−
     else z)"+
−
+
−
section {* Constants on the Quotient Type *} +
−
+
−
quotient_definition+
−
  "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" +
−
  is "delete_raw"+
−
+
−
quotient_definition+
−
  "fset_to_set :: 'a fset \<Rightarrow> 'a set" +
−
  is "set"+
−
+
−
lemma funion_sym_pre:+
−
  "a @ b \<approx> b @ a"+
−
  by auto+
−
+
−
lemma append_rsp[quot_respect]:+
−
  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"+
−
  by (auto)+
−
+
−
lemma set_cong: "(set x = set y) = (x \<approx> y)"+
−
  apply rule+
−
  apply simp_all+
−
  apply (induct x y rule: list_induct2')+
−
  apply simp_all+
−
  apply auto+
−
  done+
−
+
−
lemma inj_map_eq_iff:+
−
  "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"+
−
  by (simp add: expand_set_eq[symmetric] inj_image_eq_iff)+
−
+
−
+
−
+
−
+
−
section {* lifted part *}+
−
+
−
+
−
lemma fin_finsert_iff[simp]:+
−
  "x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"+
−
  by (lifting memb_cons_iff)+
−
+
−
lemma+
−
  shows finsertI1: "x |\<in>| finsert x S"+
−
  and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"+
−
  by (lifting memb_consI1, lifting memb_consI2)+
−
+
−
lemma finsert_absorb[simp]:+
−
  shows "x |\<in>| S \<Longrightarrow> finsert x S = S"+
−
  by (lifting memb_absorb)+
−
+
−
lemma fempty_not_finsert[simp]:+
−
  "{||} \<noteq> finsert x S"+
−
  "finsert x S \<noteq> {||}"+
−
  by (lifting nil_not_cons)+
−
+
−
lemma finsert_left_comm:+
−
  "finsert a (finsert b S) = finsert b (finsert a S)"+
−
  by (lifting cons_left_comm)+
−
+
−
lemma finsert_left_idem:+
−
  "finsert a (finsert a S) = finsert a S"+
−
  by (lifting cons_left_idem)+
−
+
−
lemma fsingleton_eq[simp]:+
−
  shows "{|x|} = {|y|} \<longleftrightarrow> x = y"+
−
  by (lifting singleton_list_eq)+
−
+
−
text {* fset_to_set *}+
−
+
−
lemma fset_to_set_simps[simp]:+
−
  "fset_to_set {||} = {}"+
−
  "fset_to_set (finsert (h :: 'b) t) = insert h (fset_to_set t)"+
−
  by (lifting list2set_thm)+
−
+
−
lemma in_fset_to_set:+
−
  "x \<in> fset_to_set xs \<equiv> x |\<in>| xs"+
−
  by (lifting memb_def[symmetric])+
−
+
−
lemma none_in_fempty:+
−
  "(\<forall>a. a \<notin> fset_to_set A) = (A = {||})"+
−
  by (lifting none_mem_nil)+
−
+
−
lemma fset_cong:+
−
  "(fset_to_set x = fset_to_set y) = (x = y)"+
−
  by (lifting set_cong)+
−
+
−
text {* fcard *}+
−
+
−
lemma fcard_fempty [simp]:+
−
  shows "fcard {||} = 0"+
−
  by (lifting fcard_raw_nil)+
−
+
−
lemma fcard_finsert_if [simp]:+
−
  shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"+
−
  by (lifting fcard_raw_cons)+
−
+
−
lemma fcard_gt_0: "x \<in> fset_to_set xs \<Longrightarrow> 0 < fcard xs"+
−
  by (lifting fcard_raw_gt_0)+
−
+
−
text {* funion *}+
−
+
−
lemma funion_simps[simp]:+
−
  "{||} |\<union>| ys = ys"+
−
  "finsert x xs |\<union>| ys = finsert x (xs |\<union>| ys)"+
−
  by (lifting append.simps)+
−
+
−
lemma funion_sym:+
−
  "a |\<union>| b = b |\<union>| a"+
−
  by (lifting funion_sym_pre)+
−
+
−
lemma funion_assoc:+
−
 "x |\<union>| xa |\<union>| xb = x |\<union>| (xa |\<union>| xb)"+
−
  by (lifting append_assoc)+
−
+
−
section {* Induction and Cases rules for finite sets *}+
−
+
−
lemma fset_strong_cases:+
−
  "X = {||} \<or> (\<exists>a Y. a \<notin> fset_to_set Y \<and> X = finsert a Y)"+
−
  by (lifting finite_set_raw_strong_cases)+
−
+
−
lemma fset_exhaust[case_names fempty finsert, cases type: fset]:+
−
  shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"+
−
  by (lifting list.exhaust)+
−
+
−
lemma fset_induct_weak[case_names fempty finsert]:+
−
  shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S"+
−
  by (lifting list.induct)+
−
+
−
lemma fset_induct[case_names fempty finsert, induct type: fset]:+
−
  assumes prem1: "P {||}" +
−
  and     prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"+
−
  shows "P S"+
−
proof(induct S rule: fset_induct_weak)+
−
  case fempty+
−
  show "P {||}" by (rule prem1)+
−
next+
−
  case (finsert x S)+
−
  have asm: "P S" by fact+
−
  show "P (finsert x S)"+
−
  proof(cases "x |\<in>| S")+
−
    case True+
−
    have "x |\<in>| S" by fact+
−
    then show "P (finsert x S)" using asm by simp+
−
  next+
−
    case False+
−
    have "x |\<notin>| S" by fact+
−
    then show "P (finsert x S)" using prem2 asm by simp+
−
  qed+
−
qed+
−
+
−
lemma fset_induct2:+
−
  "P {||} {||} \<Longrightarrow>+
−
  (\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (finsert x xs) {||}) \<Longrightarrow>+
−
  (\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (finsert y ys)) \<Longrightarrow>+
−
  (\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (finsert x xs) (finsert y ys)) \<Longrightarrow>+
−
  P xsa ysa"+
−
  apply (induct xsa arbitrary: ysa)+
−
  apply (induct_tac x rule: fset_induct)+
−
  apply simp_all+
−
  apply (induct_tac xa rule: fset_induct)+
−
  apply simp_all+
−
  done+
−
+
−
(* fmap *)+
−
lemma fmap_simps[simp]:+
−
  "fmap (f :: 'a \<Rightarrow> 'b) {||} = {||}"+
−
  "fmap f (finsert x xs) = finsert (f x) (fmap f xs)"+
−
  by (lifting map.simps)+
−
+
−
lemma fmap_set_image:+
−
  "fset_to_set (fmap f fs) = f ` (fset_to_set fs)"+
−
  apply (induct fs)+
−
  apply (simp_all)+
−
done+
−
+
−
lemma inj_fmap_eq_iff:+
−
  "inj f \<Longrightarrow> (fmap f l = fmap f m) = (l = m)"+
−
  by (lifting inj_map_eq_iff)+
−
+
−
ML {*+
−
fun dest_fsetT (Type ("FSet.fset", [T])) = T+
−
  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);+
−
*}+
−
+
−
no_notation+
−
  list_eq (infix "\<approx>" 50)+
−
+
−
end+
−