# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1287123859 -32400
# Node ID 9bde8a508594ef6c70b761bb9ff690ce72241794
# Parent  40187684fc160bda95f08ddb0500ba50f8c7ca8c
Partially merging changes from Isabelle

diff -r 40187684fc16 -r 9bde8a508594 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Thu Oct 14 17:32:06 2010 +0100
+++ b/Nominal/FSet.thy	Fri Oct 15 15:24:19 2010 +0900
@@ -6,7 +6,7 @@
 *)
 
 theory FSet
-imports Quotient_List Quotient_Product
+imports Quotient_List
 begin
 
 text {* Definiton of List relation and the quotient type *}
@@ -26,7 +26,7 @@
   'a fset = "'a list" / "list_eq"
   by (rule list_eq_equivp)
 
-text {* Raw definitions of membership, sublist, cardinality, 
+text {* Raw definitions of membership, sublist, cardinality,
   intersection
 *}
 
@@ -379,7 +379,7 @@
   apply (auto)
   done
 
-instantiation fset :: (type) "{bounded_lattice_bot,distrib_lattice,minus}"
+instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
 begin
 
 quotient_definition
@@ -438,35 +438,42 @@
 instance
 proof
   fix x y z :: "'a fset"
-  show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)"
+  show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x"
     unfolding less_fset_def 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)
+  show "x |\<subseteq>| x"  by (descending) (simp add: sub_list_def)
+  show "{||} |\<subseteq>| x" by (descending) (simp add: sub_list_def)
+  show "x |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
+  show "y |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
+  show "x |\<inter>| y |\<subseteq>| x"
+    by (descending) (simp add: sub_list_def memb_def[symmetric])
+  show "x |\<inter>| y |\<subseteq>| y" 
+    by (descending) (simp add: sub_list_def memb_def[symmetric])
+  show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" 
+    by (descending) (rule 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)
+  show "x |\<subseteq>| z" using a b 
+    by (descending) (simp add: sub_list_def)
 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)
+  show "x = y" using a b 
+    by (descending) (unfold sub_list_def list_eq.simps, blast)
 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)
+  show "y |\<union>| z |\<subseteq>| x" using a b 
+    by (descending) (simp add: sub_list_def)
 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)
+  show "x |\<subseteq>| y |\<inter>| z" using a b 
+    by (descending) (simp add: sub_list_def memb_def[symmetric])
 qed
 
 end
@@ -543,11 +550,6 @@
   apply auto
   done
 
-lemma insert_preserve2:
-  shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) =
-         (id ---> rep_fset ---> abs_fset) op #"
-  by (simp add: fun_eq_iff abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])
-
 lemma [quot_preserve]:
   "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
   by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
@@ -828,17 +830,17 @@
   by (lifting not_memb_nil)
 
 lemma fin_finsert_iff[simp]:
-  "x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"
-  by (lifting memb_cons_iff)
+  "x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
+  by (descending) (simp add: memb_def)
 
 lemma
   shows finsertI1: "x |\<in>| finsert x S"
   and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
-  by (lifting memb_consI1, lifting memb_consI2)
+  by (lifting memb_consI1 memb_consI2)
 
 lemma finsert_absorb[simp]:
   shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
-  by (lifting memb_absorb)
+  by (descending) (auto simp add: memb_def)
 
 lemma fempty_not_finsert[simp]:
   "{||} \<noteq> finsert x S"
@@ -847,15 +849,15 @@
 
 lemma finsert_left_comm:
   "finsert x (finsert y S) = finsert y (finsert x S)"
-  by (lifting cons_left_comm)
+  by (descending) (auto)
 
 lemma finsert_left_idem:
   "finsert x (finsert x S) = finsert x S"
-  by (lifting cons_left_idem)
+  by (descending) (auto)
 
 lemma fsingleton_eq[simp]:
   shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
-  by (lifting singleton_list_eq)
+  by (descending) (auto)
 
 
 text {* fset *}
@@ -1013,8 +1015,9 @@
 section {* fmap *}
 
 lemma fmap_simps[simp]:
-  "fmap (f :: 'a \<Rightarrow> 'b) {||} = {||}"
-  "fmap f (finsert x S) = finsert (f x) (fmap f S)"
+  fixes f::"'a \<Rightarrow> 'b"
+  shows "fmap f {||} = {||}"
+  and   "fmap f (finsert x S) = finsert (f x) (fmap f S)"
   by (lifting map.simps)
 
 lemma fmap_set_image:
@@ -1025,11 +1028,12 @@
   "inj f \<Longrightarrow> (fmap f S = fmap f T) = (S = T)"
   by (lifting inj_map_eq_iff)
 
-lemma fmap_funion: "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
+lemma fmap_funion: 
+  shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
   by (lifting map_append)
 
 lemma fin_funion:
-  "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
+  shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
   by (lifting memb_append)
 
 
@@ -1158,7 +1162,7 @@
   by (simp add: fminus_red)
 
 lemma fset_eq_iff:
-  "(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
+  shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
   by (descending) (auto simp add: memb_def)
 
 (* We cannot write it as "assumes .. shows" since Isabelle changes
@@ -1197,6 +1201,10 @@
   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
   by (lifting concat.simps(2))
 
+lemma 
+  shows "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
+  by (lifting concat_append)
+
 
 section {* ffilter *}
 
@@ -1318,7 +1326,6 @@
 
 lemma fcard_fminus_subset_finter:
   shows "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
-  using assms 
   unfolding finter_set fcard_set fminus_set
   by (rule card_Diff_subset_Int) (simp)
 
@@ -1394,6 +1401,12 @@
   qed
 qed
 
+
+ML {*
+fun dest_fsetT (Type (@{type_name fset}, [T])) = T
+  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
+*}
+
 no_notation
   list_eq (infix "\<approx>" 50)
 
diff -r 40187684fc16 -r 9bde8a508594 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Thu Oct 14 17:32:06 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Fri Oct 15 15:24:19 2010 +0900
@@ -57,6 +57,11 @@
   Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))
 *}
 
+lemma insert_preserve2:
+  shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) =
+         (id ---> rep_fset ---> abs_fset) op #"
+  by (simp add: fun_eq_iff abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])
+
 (*>*)