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)

(* 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)

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 (Insert a xa) = f2 a xa"

apply (lifting list.cases(2))

done

end