# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271686757 -7200
# Node ID 91d67240c9c1873e21305796115508b8631fc78d
# Parent  a71ace4a4becac93c2050f8a8925d3a993fac04c
FSet is a semi-lattice

diff -r a71ace4a4bec -r 91d67240c9c1 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Mon Apr 19 15:54:55 2010 +0200
+++ b/Nominal/FSet.thy	Mon Apr 19 16:19:17 2010 +0200
@@ -40,9 +40,13 @@
   by (simp add: sub_list_def)
 
 lemma [quot_respect]:
-  "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
+  shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
   by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2)
 
+lemma [quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
+  by auto
+
 lemma sub_list_not_eq:
   "(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)"
   by (auto simp add: sub_list_def)
@@ -102,7 +106,53 @@
   assume b: "y |\<subseteq>| z"
   show "x |\<subseteq>| z" using a b by (lifting sub_list_trans)
 qed
+end
 
+lemma sub_list_append_left:
+  "sub_list x (x @ y)"
+  by (simp add: sub_list_def)
+
+lemma sub_list_append_right:
+  "sub_list y (x @ y)"
+  by (simp add: sub_list_def)
+
+lemma sub_list_list_eq:
+  "sub_list x y \<Longrightarrow> sub_list y x \<Longrightarrow> list_eq x y"
+  unfolding sub_list_def list_eq.simps by blast
+
+lemma sub_list_append:
+  "sub_list y x \<Longrightarrow> sub_list z x \<Longrightarrow> sub_list (y @ z) x"
+  unfolding sub_list_def by auto
+
+instantiation fset :: (type) "semilattice_sup"
+begin
+
+quotient_definition
+  "sup  \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
+is
+  "(op @) \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
+
+abbreviation
+  funion  (infixl "|\<union>|" 65)
+where
+  "xs |\<union>| ys \<equiv> sup (xs :: 'a fset) ys"
+
+instance
+proof
+  fix x y :: "'a fset"
+  show "x |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_left)
+  show "y |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_right)
+next
+  fix x y :: "'a fset"
+  assume a: "x |\<subseteq>| y"
+  assume b: "y |\<subseteq>| x"
+  show "x = y" using a b by (lifting sub_list_list_eq)
+next
+  fix x y z :: "'a fset"
+  assume a: "y |\<subseteq>| x"
+  assume b: "z |\<subseteq>| x"
+  show "y |\<union>| z |\<subseteq>| x" using a b by (lifting sub_list_append)
+qed
 end
 
 section {* Empty fset, Finsert and Membership *}
@@ -181,15 +231,6 @@
   shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
   by (simp add: id_simps) auto
 
-section {* Unions *}
-
-quotient_definition
-  funion  (infixl "|\<union>|" 65)
-where
-  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
-  "op @"
-
 section {* sub_list *}
 
 lemma sub_list_cons:
@@ -497,10 +538,6 @@
   "xs @ ys \<approx> ys @ xs"
   by auto
 
-lemma append_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
-  by auto
-
 lemma set_cong: 
   shows "(set x = set y) = (x \<approx> y)"
   by auto
@@ -546,7 +583,7 @@
   apply (case_tac "memb a A")
   apply (auto simp add: memb_def)[2]
   apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
-  apply (metis delete_raw.simps(2) list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
+  apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
   apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident)
   done