Added FSet3 with a formalisation of finite sets based on Michael's one.
theory FSet3+ −
imports "../QuotMain" List+ −
begin+ −
+ −
definition+ −
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)+ −
sorry+ −
+ −
quotient 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 #"+ −
sorry+ −
+ −
lemma mem_rsp[quot_respect]:+ −
"(op = ===> op \<approx> ===> op =) (op mem) (op mem)"+ −
sorry+ −
+ −
lemma no_mem_nil: "(\<forall>a. \<not>(a mem A)) = (A = [])"+ −
sorry+ −
+ −
lemma none_mem_nil: "(\<forall>a. \<not>(a mem A)) = (A \<approx> [])"+ −
sorry+ −
+ −
lemma mem_cons: "a mem A \<Longrightarrow> a # A \<approx> A"+ −
sorry+ −
+ −
lemma cons_left_comm: "x # y # A \<approx> y # x # A"+ −
sorry+ −
+ −
lemma cons_left_idem: "x # x # A \<approx> x # A"+ −
sorry+ −
+ −
lemma finite_set_raw_strong_cases:+ −
"(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))"+ −
apply (induct X)+ −
apply (simp)+ −
sorry+ −
+ −
primrec+ −
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)"+ −
sorry+ −
+ −
lemma mem_delete_raw_ident:+ −
"\<not>(MEM a (A delete_raw a))"+ −
sorry+ −
+ −
lemma not_mem_delete_raw_ident:+ −
"\<not>(b mem A) \<Longrightarrow> (delete_raw A b = A)"+ −
sorry+ −
+ −
lemma delete_raw_RSP:+ −
"A \<approx> B \<Longrightarrow> delete_raw A a \<approx> delete_raw B a"+ −
sorry+ −
+ −
lemma cons_delete_raw:+ −
"a # (delete_raw A a) \<approx> (if a mem A then A else (a # A))"+ −
sorry+ −
+ −
lemma mem_cons_delete_raw:+ −
"a mem A \<Longrightarrow> a # (delete_raw A a) \<approx> A"+ −
sorry+ −
+ −
lemma finite_set_raw_delete_raw_cases1:+ −
"X = [] \<or> (\<exists>a. X \<approx> a # delete_raw X a)"+ −
sorry+ −
+ −
lemma finite_set_raw_delete_raw_cases:+ −
"X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)"+ −
sorry+ −
+ −
fun+ −
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))"+ −
sorry+ −
+ −
lemma 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 c+ −
apply(induct xs)+ −
apply(metis mem_delete_raw)+ −
apply(metis mem_delete_raw)+ −
done+ −
+ −
lemma mem_card_raw_not_0:+ −
"a mem A \<Longrightarrow> \<not>(card_raw A = 0)"+ −
sorry+ −
+ −
lemma card_raw_cons_gt_0:+ −
"0 < card_raw (a # A)"+ −
sorry+ −
+ −
lemma card_raw_delete_raw:+ −
"card_raw (delete_raw A a) = (if a mem A then card_raw A - 1 else card_raw A)"+ −
sorry+ −
+ −
lemma card_raw_rsp_aux:+ −
assumes e: "a \<approx> b"+ −
shows "card_raw a = card_raw b"+ −
using e sorry+ −
+ −
lemma 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 = [])"+ −
sorry+ −
+ −
lemma list2set_thm:+ −
shows "set [] = {}"+ −
and "set (h # t) = insert h (set t)"+ −
sorry+ −
+ −
lemma list2set_RSP:+ −
"A \<approx> B \<Longrightarrow> set A = set B"+ −
sorry+ −
+ −
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)"+ −
+ −
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))"+ −
sorry+ −
+ −
lemma fold_rsp[quot_respect]:+ −
"(op = ===> op = ===> op \<approx> ===> op =) fold_raw fold_raw"+ −
apply (auto)+ −
apply (case_tac "rsp_fold x")+ −
sorry+ −
+ −
lemma append_rsp[quot_respect]:+ −
"(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"+ −
sorry+ −
+ −
primrec+ −
inter_raw+ −
where+ −
"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"+ −
sorry+ −
+ −
lemma 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_comm+ −
lemma "Insert a (Insert b x) = Insert b (Insert a x)"+ −
by (lifting cons_left_comm)+ −
+ −
thm cons_left_idem+ −
lemma "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_nil+ −
thm mem_cons+ −
thm finite_set_raw_strong_cases+ −
thm card_raw.simps+ −
thm not_mem_card_raw+ −
thm card_raw_suc+ −
lemma "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_0+ −
thm mem_card_raw_not_0+ −
thm not_nil_equiv_cons+ −
thm delete_raw.simps+ −
thm mem_delete_raw+ −
thm card_raw_delete_raw+ −
thm cons_delete_raw+ −
thm mem_cons_delete_raw+ −
thm finite_set_raw_delete_raw_cases+ −
thm append.simps+ −
(* MEM_APPEND: MEM e (APPEND l1 l2) = MEM e l1 \/ MEM e l2 *)+ −
thm inter_raw.simps+ −
thm mem_inter_raw+ −
thm fold_raw.simps+ −
thm list2set_thm+ −
thm list_eq_def+ −
thm list.induct+ −
lemma "\<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+ −