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;