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 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