theory FSet2

imports "../QuotMain" "../QuotList" List

begin

inductive

  list_eq (infix "\<approx>" 50)

where

  "a#b#xs \<approx> b#a#xs"

| "[] \<approx> []"

| "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"

| "a#a#xs \<approx> a#xs"

| "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"

| "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"

lemma list_eq_refl:

  shows "xs \<approx> xs"

by (induct xs) (auto intro: list_eq.intros)

lemma equivp_list_eq:

  shows "equivp list_eq"

unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def

by (auto intro: list_eq.intros list_eq_refl)

quotient_type 

  'a fset = "'a list" / "list_eq"

  by (rule equivp_list_eq)

quotient_definition

  "fempty :: 'a fset" ("{||}")

as

  "[]"

quotient_definition

  "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"

as

  "(op #)"

lemma finsert_rsp[quot_respect]:

  shows "(op = ===> op \<approx> ===> op \<approx>) (op #) (op #)"

by (auto intro: list_eq.intros)

quotient_definition

  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [65,66] 65)

as

  "(op @)"

lemma append_rsp_aux1:

  assumes a : "l2 \<approx> r2 "

  shows "(h @ l2) \<approx> (h @ r2)"

using a

apply(induct h)

apply(auto intro: list_eq.intros(5))

done

lemma append_rsp_aux2:

  assumes a : "l1 \<approx> r1" "l2 \<approx> r2 "

  shows "(l1 @ l2) \<approx> (r1 @ r2)"

using a

apply(induct arbitrary: l2 r2)

apply(simp_all)

apply(blast intro: list_eq.intros append_rsp_aux1)+

done

lemma append_rsp[quot_respect]:

  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"

  by (auto simp add: append_rsp_aux2)

quotient_definition

  "fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)

as

  "(op mem)"

lemma memb_rsp_aux:

  assumes a: "x \<approx> y"

  shows "(z mem x) = (z mem y)"

  using a by induct auto

lemma memb_rsp[quot_respect]:

  shows "(op = ===> (op \<approx> ===> op =)) (op mem) (op mem)"

  by (simp add: memb_rsp_aux)

definition 

  fnot_mem :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<notin>f _" [50, 51] 50)

where

  "x \<notin>f S \<equiv> \<not>(x \<in>f S)"

definition

  "inter_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"

where

  "inter_list X Y \<equiv> [x \<leftarrow> X. x\<in>set Y]"

quotient_definition

  "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)

as

  "inter_list"

no_syntax

  "@Finset"     :: "args => 'a fset"                       ("{|(_)|}")

syntax

  "@Finfset"     :: "args => 'a fset"                       ("{|(_)|}")

translations

  "{|x, xs|}"     == "CONST finsert x {|xs|}"

  "{|x|}"         == "CONST finsert x {||}"

subsection {* Empty sets *}

lemma test:

  shows "\<not>(x # xs \<approx> [])"

sorry

lemma finsert_not_empty[simp]: 

  shows "finsert x S \<noteq> {||}"

  by (lifting test)

end;