theory FSet3+
−
imports "../QuotMain" List+
−
begin+
−
+
−
fun+
−
  list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)+
−
where+
−
  "list_eq xs ys = (\<forall>e. (e \<in> set xs) = (e \<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 fset = "'a list" / "list_eq"+
−
  by (rule list_eq_equivp)+
−
+
−
lemma not_nil_equiv_cons: +
−
  "\<not>[] \<approx> a # A" +
−
by auto+
−
+
−
lemma nil_rsp[quot_respect]:+
−
  shows "[] \<approx> []"+
−
  by simp+
−
+
−
lemma cons_rsp[quot_respect]: +
−
  shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"+
−
  by simp+
−
+
−
(*+
−
lemma mem_rsp[quot_respect]:+
−
  "(op = ===> op \<approx> ===> op =) (op mem) (op mem)"+
−
*)+
−
+
−
+
−
lemma no_mem_nil: +
−
  "(\<forall>a. a \<notin> set A) = (A = [])"+
−
by (induct A) (auto)+
−
+
−
lemma none_mem_nil: +
−
  "(\<forall>a. a \<notin> set A) = (A \<approx> [])"+
−
by simp+
−
+
−
lemma mem_cons: +
−
  "a \<in> set A \<Longrightarrow> a # A \<approx> A"+
−
by auto+
−
+
−
lemma cons_left_comm: +
−
  "x #y # A \<approx> y # x # A"+
−
by auto+
−
+
−
lemma cons_left_idem: +
−
  "x # x # A \<approx> x # A"+
−
by auto+
−
+
−
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 delete_raw_RSP:+
−
  "A \<approx> B \<Longrightarrow> delete_raw A a \<approx> delete_raw B a"+
−
apply(induct A arbitrary: B a)+
−
apply(auto)+
−
sorry+
−
+
−
lemma cons_delete_raw:+
−
  "a # (delete_raw A a) \<approx> (if a \<in> set A then A else (a # A))"+
−
sorry+
−
+
−
lemma mem_cons_delete_raw:+
−
    "a \<in> set A \<Longrightarrow> a # (delete_raw A a) \<approx> A"+
−
sorry+
−
+
−
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)+
−
+
−
fun+
−
  card_raw :: "'a list \<Rightarrow> nat"+
−
where+
−
  card_raw_nil: "card_raw [] = 0"+
−
| card_raw_cons: "card_raw (x # xs) = (if x \<in> set 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:+
−
  assumes c: "card_raw xs = Suc n"+
−
  shows "\<exists>a ys. (a \<notin> set ys) \<and> xs \<approx> (a # ys)"+
−
  using c apply(induct xs)+
−
  apply(simp)+
−
  sorry+
−
+
−
lemma mem_card_raw_gt_0:+
−
  "a \<in> set A \<Longrightarrow> 0 < card_raw A"+
−
  by (induct A) (auto)+
−
+
−
lemma card_raw_cons_gt_0:+
−
  "0 < card_raw (a # A)"+
−
  by (induct A) (auto)+
−
+
−
lemma card_raw_delete_raw:+
−
  "card_raw (delete_raw A a) = (if a \<in> set 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 = [])"+
−
  by (induct A) (auto)+
−
+
−
lemma list2set_thm:+
−
  shows "set [] = {}"+
−
  and "set (h # t) = insert h (set t)"+
−
  by (auto)+
−
+
−
lemma list2set_RSP:+
−
  "A \<approx> B \<Longrightarrow> set A = set B"+
−
  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)"+
−
+
−
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)+
−
sorry+
−
+
−
lemma append_rsp[quot_respect]:+
−
  "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"+
−
by auto+
−
+
−
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 *)+
−
+
−
+
−
section {* Constants on the Quotient Type *} +
−
+
−
quotient_def+
−
  "fempty :: 'a fset" +
−
  as "[]::'a list"+
−
+
−
quotient_def+
−
  "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" +
−
  as "op #"+
−
+
−
quotient_def+
−
  "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)+
−
  as "\<lambda>x X. x \<in> set X"+
−
+
−
abbreviation+
−
  fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<notin>f _" [50, 51] 50)+
−
where+
−
  "a \<notin>f S \<equiv> \<not>(a \<in>f S)"+
−
+
−
quotient_def+
−
  "fcard :: 'a fset \<Rightarrow> nat" +
−
  as "card_raw"+
−
+
−
quotient_def+
−
  "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" +
−
  as "delete_raw"+
−
+
−
quotient_def+
−
  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [50, 51] 50)+
−
  as "op @"+
−
+
−
quotient_def+
−
  "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)+
−
  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"+
−
+
−
+
−
section {* Lifted Theorems *}+
−
+
−
thm list.cases (* ??? *)+
−
+
−
thm cons_left_comm+
−
lemma "finsert a (finsert b S) = finsert b (finsert a S)"+
−
by (lifting cons_left_comm)+
−
+
−
thm cons_left_idem+
−
lemma "finsert a (finsert a S) = finsert a S"+
−
by (lifting cons_left_idem)+
−
+
−
(* thm MEM:+
−
  MEM x [] = F+
−
  MEM x (h::t) = (x=h) \/ MEM x t *)+
−
thm none_mem_nil+
−
(*lemma "(\<forall>a. a \<notin>f A) = (A = fempty)"*)+
−
+
−
thm mem_cons+
−
thm finite_set_raw_strong_cases+
−
thm card_raw.simps+
−
thm not_mem_card_raw+
−
thm card_raw_suc+
−
+
−
lemma "fcard X = Suc n \<Longrightarrow> (\<exists>a S. a \<notin>f S & X = finsert a S)"+
−
(*by (lifting card_raw_suc)*)+
−
sorry+
−
+
−
thm card_raw_cons_gt_0+
−
thm mem_card_raw_gt_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 fempty; \<And>a x. P x \<Longrightarrow> P (finsert 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)+
−
+
−
quotient_def+
−
  "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"+
−
as+
−
  "list_case"+
−
+
−
(* NOT SURE IF TRUE *)+
−
lemma list_case_rsp[quot_respect]:+
−
  "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"+
−
  apply (auto)+
−
  sorry+
−
+
−
lemma "fset_case (f1::'t) f2 (finsert a xa) = f2 a xa"+
−
apply (lifting list.cases(2))+
−
done+
−
+
−
+
−
end+
−