--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Examples/FSet2.thy	Thu Dec 10 03:48:39 2009 +0100
@@ -0,0 +1,119 @@
+theory FSet2
+imports "../QuotMain" 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 fset = "'a list" / "list_eq"
+  by (rule equivp_list_eq)
+
+quotient_def 
+  fempty :: "fempty :: 'a fset" ("{||}")
+where
+  "[]"
+
+quotient_def 
+  finsert :: "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+where
+  "(op #)"
+
+lemma finsert_rsp[quot_respect]:
+  shows "(op = ===> op \<approx> ===> op \<approx>) (op #) (op #)"
+by (auto intro: list_eq.intros)
+
+quotient_def 
+  funion :: "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [65,66] 65)
+where
+  "(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_def 
+  fmem :: " fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
+where
+  "(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_def 
+  finter :: "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
+where
+  "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;