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;+
−