diff -r b1281a0051ae -r b611aee9f8e7 Attic/Quot/Examples/FSet2.thy
--- a/Attic/Quot/Examples/FSet2.thy	Thu Apr 29 09:13:18 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,128 +0,0 @@
-theory FSet2
-imports "../Quotient" "../Quotient_List" 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 ("{||}")
-where
-  "fempty :: 'a fset"
-is
-  "[]"
-
-quotient_definition
-  "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
-  "(op #)"
-
-lemma finsert_rsp[quot_respect]:
-  shows "(op = ===> op \<approx> ===> op \<approx>) (op #) (op #)"
-by (auto intro: list_eq.intros)
-
-quotient_definition
-  funion ("_ \<union>f _" [65,66] 65)
-where
-  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
-  "(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 ("_ \<in>f _" [50, 51] 50)
-where
-  "fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
-is
-  "(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 ("_ \<inter>f _" [70, 71] 70)
-where
-  "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
-  "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;