Added FSet3 with a formalisation of finite sets based on Michael's one.
theory FSet3imports "../QuotMain" Listbegindefinition list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)where "list_eq x y = (\<forall>e. e mem x = e mem y)"lemma list_eq_reflp: shows "xs \<approx> xs" by (metis list_eq_def)lemma list_eq_equivp: shows "equivp list_eq" unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def apply (auto intro: list_eq_def) apply (metis list_eq_def) apply (metis list_eq_def) sorryquotient fset = "'a list" / "list_eq" by (rule list_eq_equivp)lemma not_nil_equiv_cons: "[] \<noteq> a # A" sorry(* The 2 lemmas below are different from the ones in QuotList *)lemma nil_rsp[quot_respect]: shows "[] \<approx> []"by (rule list_eq_reflp)lemma cons_rsp[quot_respect]: (* Better then the one from QuotList *) " (op = ===> op \<approx> ===> op \<approx>) op # op #" sorrylemma mem_rsp[quot_respect]: "(op = ===> op \<approx> ===> op =) (op mem) (op mem)" sorrylemma no_mem_nil: "(\<forall>a. \<not>(a mem A)) = (A = [])"sorrylemma none_mem_nil: "(\<forall>a. \<not>(a mem A)) = (A \<approx> [])"sorrylemma mem_cons: "a mem A \<Longrightarrow> a # A \<approx> A"sorrylemma cons_left_comm: "x # y # A \<approx> y # x # A"sorrylemma cons_left_idem: "x # x # A \<approx> x # A"sorrylemma finite_set_raw_strong_cases: "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))" apply (induct X) apply (simp) sorryprimrec 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 mem (delete_raw A a) = x mem A \<and> \<not>(x = a)"sorrylemma mem_delete_raw_ident: "\<not>(MEM a (A delete_raw a))"sorrylemma not_mem_delete_raw_ident: "\<not>(b mem A) \<Longrightarrow> (delete_raw A b = A)"sorrylemma delete_raw_RSP: "A \<approx> B \<Longrightarrow> delete_raw A a \<approx> delete_raw B a"sorrylemma cons_delete_raw: "a # (delete_raw A a) \<approx> (if a mem A then A else (a # A))"sorrylemma mem_cons_delete_raw: "a mem A \<Longrightarrow> a # (delete_raw A a) \<approx> A"sorrylemma finite_set_raw_delete_raw_cases1: "X = [] \<or> (\<exists>a. X \<approx> a # delete_raw X a)"sorrylemma finite_set_raw_delete_raw_cases: "X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)"sorryfun card_raw :: "'a list \<Rightarrow> nat"where card_raw_nil: "card_raw [] = 0"| card_raw_cons: "card_raw (x # xs) = (if x mem xs then card_raw xs else Suc (card_raw xs))"lemma not_mem_card_raw: fixes x :: "'a" fixes xs :: "'a list" shows "(\<not>(x mem xs)) = (card_raw (x # xs) = Suc (card_raw xs))" sorrylemma card_raw_suc: fixes xs :: "'a list" fixes n :: "nat" assumes c: "card_raw xs = Suc n" shows "\<exists>a ys. \<not>(a mem ys) \<and> xs \<approx> (a # ys)" using capply(induct xs)apply(metis mem_delete_raw)apply(metis mem_delete_raw)donelemma mem_card_raw_not_0: "a mem A \<Longrightarrow> \<not>(card_raw A = 0)"sorrylemma card_raw_cons_gt_0: "0 < card_raw (a # A)"sorrylemma card_raw_delete_raw: "card_raw (delete_raw A a) = (if a mem A then card_raw A - 1 else card_raw A)"sorrylemma card_raw_rsp_aux: assumes e: "a \<approx> b" shows "card_raw a = card_raw b" using e sorrylemma card_raw_rsp[quot_respect]: "(op \<approx> ===> op =) card_raw card_raw" by (simp add: card_raw_rsp_aux)lemma card_raw_0: "(card_raw A = 0) = (A = [])"sorrylemma list2set_thm: shows "set [] = {}" and "set (h # t) = insert h (set t)"sorrylemma list2set_RSP: "A \<approx> B \<Longrightarrow> set A = set B"sorrydefinition rsp_foldwhere "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)"lemma mem_lcommuting_fold_raw: "rsp_fold f \<Longrightarrow> h mem B \<Longrightarrow> fold_raw f z B = f h (fold_raw f z (delete_raw B h))"sorrylemma fold_rsp[quot_respect]: "(op = ===> op = ===> op \<approx> ===> op =) fold_raw fold_raw" apply (auto) apply (case_tac "rsp_fold x")sorrylemma append_rsp[quot_respect]: "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" sorryprimrec inter_rawwhere "inter_raw [] B = []"| "inter_raw (a # A) B = (if a mem B then a # inter_raw A B else inter_raw A B)"lemma mem_inter_raw: "x mem (inter_raw A B) = x mem A \<and> x mem B"sorrylemma inter_raw_RSP: "A1 \<approx> A2 \<and> B1 \<approx> B2 \<Longrightarrow> (inter_raw A1 B1) \<approx> (inter_raw A2 B2)"sorry(* LIFTING DEFS *)quotient_def "Empty :: 'a fset" as "[]::'a list"quotient_def "Insert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "op #"quotient_def "In :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" as "op mem"quotient_def "Card :: 'a fset \<Rightarrow> nat" as "card_raw"quotient_def "Delete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" as "delete_raw"quotient_def "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "op @"quotient_def "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" as "inter_raw"quotient_def "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" as "fold_raw"quotient_def "fset_to_set :: 'a fset \<Rightarrow> 'a set" as "set"(* LIFTING THMS *)thm list.cases (* ??? *)thm cons_left_commlemma "Insert a (Insert b x) = Insert b (Insert a x)"by (lifting cons_left_comm)thm cons_left_idemlemma "Insert a (Insert a x) = Insert a x"by (lifting cons_left_idem)(* thm MEM: MEM x [] = F MEM x (h::t) = (x=h) \/ MEM x t *)thm none_mem_nilthm mem_consthm finite_set_raw_strong_casesthm card_raw.simpsthm not_mem_card_rawthm card_raw_suclemma "Card x = Suc n \<Longrightarrow> (\<exists>a b. \<not> In a b & x = Insert a b)"by (lifting card_raw_suc)thm card_raw_cons_gt_0thm mem_card_raw_not_0thm not_nil_equiv_consthm delete_raw.simpsthm mem_delete_rawthm card_raw_delete_rawthm cons_delete_rawthm mem_cons_delete_rawthm finite_set_raw_delete_raw_casesthm append.simps(* MEM_APPEND: MEM e (APPEND l1 l2) = MEM e l1 \/ MEM e l2 *)thm inter_raw.simpsthm mem_inter_rawthm fold_raw.simpsthm list2set_thmthm list_eq_defthm list.inductlemma "\<lbrakk>P Empty; \<And>a x. P x \<Longrightarrow> P (Insert a x)\<rbrakk> \<Longrightarrow> P l"by (lifting list.induct)(* We also have map and some properties of it in FSet *)(* and the following which still lifts ok *)lemma "funion (funion x xa) xb = funion x (funion xa xb)"by (lifting append_assoc)end