--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/FSet.thy	Thu Mar 18 18:10:20 2010 +0100
@@ -0,0 +1,376 @@
+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"
+  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' 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)
+
+
+
+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]:
+  shows "{||} \<noteq> finsert x S"
+  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:
+  "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)
+
+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[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_induct2[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)
+  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
+
+
+
+end