# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271685295 -7200
# Node ID a71ace4a4becac93c2050f8a8925d3a993fac04c
# Parent  464dd13efff68ca0ba3680b6d9bd77bfd82eb2b9# Parent  54ad41f9e505b3e89ace33fe51fa3e475b9a4686
merge

diff -r 54ad41f9e505 -r a71ace4a4bec Nominal/FSet.thy
--- a/Nominal/FSet.thy	Mon Apr 19 15:37:54 2010 +0200
+++ b/Nominal/FSet.thy	Mon Apr 19 15:54:55 2010 +0200
@@ -29,14 +29,9 @@
 where
   "sub_list xs ys \<equiv> (\<forall>x. x \<in> set xs \<longrightarrow> x \<in> set ys)"
 
-lemma sub_list_cons:
-  "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
-  by (auto simp add: memb_def sub_list_def)
-
-lemma nil_not_cons:
-  shows "\<not> ([] \<approx> x # xs)"
-  and   "\<not> (x # xs \<approx> [])"
-  by auto
+quotient_type
+  'a fset = "'a list" / "list_eq"
+by (rule list_eq_equivp)
 
 lemma sub_list_rsp1: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list xs zs = sub_list ys zs"
   by (simp add: sub_list_def)
@@ -48,20 +43,72 @@
   "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
   by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2)
 
-quotient_type
-  'a fset = "'a list" / "list_eq"
-by (rule list_eq_equivp)
+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)
+
+lemma sub_list_refl:
+  "sub_list x x"
+  by (simp add: sub_list_def)
+
+lemma sub_list_trans:
+  "sub_list x y \<Longrightarrow> sub_list y z \<Longrightarrow> sub_list x z"
+  by (simp add: sub_list_def)
+
+lemma sub_list_empty:
+  "sub_list [] x"
+  by (simp add: sub_list_def)
+
+instantiation fset :: (type) bot
+begin
+
+quotient_definition
+  "bot :: 'a fset" is "[] :: 'a list"
+
+abbreviation
+  fempty  ("{||}")
+where
+  "{||} \<equiv> bot :: 'a fset"
+
+quotient_definition
+  "less_eq_fset \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)"
+is
+  "sub_list \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> bool)"
+
+abbreviation
+  f_subset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50)
+where
+  "xs |\<subseteq>| ys \<equiv> xs \<le> ys"
+
+definition
+  less_fset:
+  "(xs :: 'a fset) < ys \<equiv> xs \<le> ys \<and> xs \<noteq> ys"
+
+abbreviation
+  f_subset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50)
+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
 
 section {* Empty fset, Finsert and Membership *}
 
 quotient_definition
-  fempty  ("{||}")
-where
-  "fempty :: 'a fset"
-is "[]::'a list"
-
-quotient_definition
-  "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" 
+  "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is "op #"
 
 syntax
@@ -95,6 +142,11 @@
 
 section {* Augmenting an fset -- @{const finsert} *}
 
+lemma nil_not_cons:
+  shows "\<not> ([] \<approx> x # xs)"
+  and   "\<not> (x # xs \<approx> [])"
+  by auto
+
 lemma not_memb_nil:
   shows "\<not> memb x []"
   by (simp add: memb_def)
@@ -138,6 +190,12 @@
 is
   "op @"
 
+section {* sub_list *}
+
+lemma sub_list_cons:
+  "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
+  by (auto simp add: memb_def sub_list_def)
+
 section {* Cardinality of finite sets *}
 
 fun
@@ -770,6 +828,16 @@
   "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
   by (lifting memb_finter_raw)
 
+lemma fsubset_finsert:
+  "(finsert x xs |\<subseteq>| ys) = (x |\<in>| ys \<and> xs |\<subseteq>| ys)"
+  by (lifting sub_list_cons)
+
+thm sub_list_def[simplified memb_def[symmetric], quot_lifted, no_vars]
+
+lemma fsubset_fin: "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
+by (rule meta_eq_to_obj_eq)
+   (lifting sub_list_def[simplified memb_def[symmetric]])
+
 lemma expand_fset_eq:
   "(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
   by (lifting list_eq.simps[simplified memb_def[symmetric]])