# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271771997 -7200
# Node ID dbc9e88c44dac2c4e6148312c366cba00da94c48
# Parent  4fa94551eebc6ead5e2a785b53c18c077a988d42
fsets are distributive lattices.

diff -r 4fa94551eebc -r dbc9e88c44da Nominal/FSet.thy
--- a/Nominal/FSet.thy	Tue Apr 20 10:23:39 2010 +0200
+++ b/Nominal/FSet.thy	Tue Apr 20 15:59:57 2010 +0200
@@ -63,7 +63,76 @@
   "sub_list [] x"
   by (simp add: sub_list_def)
 
-instantiation fset :: (type) bot
+primrec
+  finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
+  "finter_raw [] l = []"
+| "finter_raw (h # t) l =
+     (if memb h l then h # (finter_raw t l) else finter_raw t l)"
+
+lemma not_memb_nil:
+  shows "\<not> memb x []"
+  by (simp add: memb_def)
+
+lemma memb_cons_iff:
+  shows "memb x (y # xs) = (x = y \<or> memb x xs)"
+  by (induct xs) (auto simp add: memb_def)
+
+lemma memb_finter_raw:
+  "memb x (finter_raw xs ys) \<longleftrightarrow> memb x xs \<and> memb x ys"
+  apply (induct xs)
+  apply (simp add: not_memb_nil)
+  apply (simp add: finter_raw.simps)
+  apply (simp add: memb_cons_iff)
+  apply auto
+  done
+
+lemma [quot_respect]:
+  "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
+  by (simp add: memb_def[symmetric] memb_finter_raw)
+
+
+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_inter_left:
+  shows "sub_list (finter_raw x y) x"
+  by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+
+lemma sub_list_inter_right:
+  shows "sub_list (finter_raw x y) y"
+  by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+
+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
+
+lemma sub_list_inter:
+  "sub_list x y \<Longrightarrow> sub_list x z \<Longrightarrow> sub_list x (finter_raw y z)"
+  by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
+
+lemma append_inter_distrib:
+  "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
+  apply (induct x)
+  apply simp
+  apply simp
+  apply (rule conjI)
+  apply (simp_all add: memb_def)
+  apply (simp add: memb_def[symmetric] memb_finter_raw)
+  apply (simp add: memb_def)
+  apply auto
+  done
+
+instantiation fset :: (type) "{bot,distrib_lattice}"
 begin
 
 quotient_definition
@@ -93,40 +162,6 @@
 where
   "xs |\<subset>| ys \<equiv> xs < ys"
 
-instance
-proof
-  fix x y z :: "'a fset"
-  show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)"
-    unfolding less_fset by (lifting sub_list_not_eq)
-  show "x |\<subseteq>| x" by (lifting sub_list_refl)
-  show "{||} |\<subseteq>| x" by (lifting sub_list_empty)
-next
-  fix x y z :: "'a fset"
-  assume a: "x |\<subseteq>| y"
-  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
@@ -137,11 +172,33 @@
 where
   "xs |\<union>| ys \<equiv> sup (xs :: 'a fset) ys"
 
+quotient_definition
+  "inf  \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)"
+is
+  "finter_raw \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)"
+
+abbreviation
+  finter (infixl "|\<inter>|" 65)
+where
+  "xs |\<inter>| ys \<equiv> inf (xs :: 'a fset) ys"
+
 instance
 proof
-  fix x y :: "'a fset"
+  fix x y z :: "'a fset"
+  show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)"
+    unfolding less_fset by (lifting sub_list_not_eq)
+  show "x |\<subseteq>| x" by (lifting sub_list_refl)
+  show "{||} |\<subseteq>| x" by (lifting sub_list_empty)
   show "x |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_left)
   show "y |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_right)
+  show "x |\<inter>| y |\<subseteq>| x" by (lifting sub_list_inter_left)
+  show "x |\<inter>| y |\<subseteq>| y" by (lifting sub_list_inter_right)
+  show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" by (lifting append_inter_distrib)
+next
+  fix x y z :: "'a fset"
+  assume a: "x |\<subseteq>| y"
+  assume b: "y |\<subseteq>| z"
+  show "x |\<subseteq>| z" using a b by (lifting sub_list_trans)
 next
   fix x y :: "'a fset"
   assume a: "x |\<subseteq>| y"
@@ -152,7 +209,13 @@
   assume a: "y |\<subseteq>| x"
   assume b: "z |\<subseteq>| x"
   show "y |\<union>| z |\<subseteq>| x" using a b by (lifting sub_list_append)
+next
+  fix x y z :: "'a fset"
+  assume a: "x |\<subseteq>| y"
+  assume b: "x |\<subseteq>| z"
+  show "x |\<subseteq>| y |\<inter>| z" using a b by (lifting sub_list_inter)
 qed
+
 end
 
 section {* Empty fset, Finsert and Membership *}
@@ -197,10 +260,6 @@
   and   "\<not> (x # xs \<approx> [])"
   by auto
 
-lemma not_memb_nil:
-  shows "\<not> memb x []"
-  by (simp add: memb_def)
-
 lemma no_memb_nil:
   "(\<forall>x. \<not> memb x xs) = (xs = [])"
   by (simp add: memb_def)
@@ -209,10 +268,6 @@
   "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
   by (simp add: memb_def)
 
-lemma memb_cons_iff:
-  shows "memb x (y # xs) = (x = y \<or> memb x xs)"
-  by (induct xs) (auto simp add: memb_def)
-
 lemma memb_consI1:
   shows "memb x (x # xs)"
   by (simp add: memb_def)
@@ -490,30 +545,10 @@
   "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
   by (simp add: memb_def[symmetric] ffold_raw_rsp_pre)
 
-primrec
-  finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
-  "finter_raw [] l = []"
-| "finter_raw (h # t) l =
-     (if memb h l then h # (finter_raw t l) else finter_raw t l)"
-
 lemma finter_raw_empty:
   "finter_raw l [] = []"
   by (induct l) (simp_all add: not_memb_nil)
 
-lemma memb_finter_raw:
-  "memb x (finter_raw xs ys) \<longleftrightarrow> memb x xs \<and> memb x ys"
-  apply (induct xs)
-  apply (simp add: not_memb_nil)
-  apply (simp add: finter_raw.simps)
-  apply (simp add: memb_cons_iff)
-  apply auto
-  done
-
-lemma [quot_respect]:
-  "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
-  by (simp add: memb_def[symmetric] memb_finter_raw)
-
 section {* Constants on the Quotient Type *} 
 
 quotient_definition
@@ -528,12 +563,6 @@
   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
   is "ffold_raw"
 
-quotient_definition
-  finter (infix "|\<inter>|" 50)
-where
-  "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is "finter_raw"
-
 lemma funion_sym_pre:
   "xs @ ys \<approx> ys @ xs"
   by auto