# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271837347 -7200
# Node ID 39951d71bfceb3640b8908f74d8887ffa3f73bd1
# Parent  0a857f662e4c72c30e38fae443da80fe35aeb1ef# Parent  9972dc5bd7ad1b0336fd7239a2af1ba1f3b61280
merged

diff -r 0a857f662e4c -r 39951d71bfce Nominal/FSet.thy
--- a/Nominal/FSet.thy	Wed Apr 21 10:08:47 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 21 10:09:07 2010 +0200
@@ -8,6 +8,8 @@
 imports Quotient Quotient_List List
 begin
 
+text {* Definiton of List relation and the quotient type *}
+
 fun
   list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
 where
@@ -15,10 +17,16 @@
 
 lemma list_eq_equivp:
   shows "equivp list_eq"
-  unfolding equivp_reflp_symp_transp 
+  unfolding equivp_reflp_symp_transp
   unfolding reflp_def symp_def transp_def
   by auto
 
+quotient_type
+  'a fset = "'a list" / "list_eq"
+  by (rule list_eq_equivp)
+
+text {* Raw definitions *}
+
 definition
   memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
 where
@@ -29,24 +37,188 @@
 where
   "sub_list xs ys \<equiv> (\<forall>x. x \<in> set xs \<longrightarrow> x \<in> set ys)"
 
-quotient_type
-  'a fset = "'a list" / "list_eq"
-by (rule list_eq_equivp)
+fun
+  fcard_raw :: "'a list \<Rightarrow> nat"
+where
+  fcard_raw_nil:  "fcard_raw [] = 0"
+| fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))"
 
-lemma sub_list_rsp1: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list xs zs = sub_list ys zs"
-  by (simp add: sub_list_def)
+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 sub_list_rsp2: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list zs xs = sub_list zs ys"
-  by (simp add: sub_list_def)
+fun
+  delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
+where
+  "delete_raw [] x = []"
+| "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
+
+definition
+  rsp_fold
+where
+  "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
 
-lemma [quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
-  by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2)
+primrec
+  ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
+where
+  "ffold_raw f z [] = z"
+| "ffold_raw f z (a # A) =
+     (if (rsp_fold f) then
+       if memb a A then ffold_raw f z A
+       else f a (ffold_raw f z A)
+     else z)"
+
+text {* Respectfullness *}
 
 lemma [quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   by auto
 
+lemma [quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
+  by (auto simp add: sub_list_def)
+
+lemma memb_rsp[quot_respect]:
+  shows "(op = ===> op \<approx> ===> op =) memb memb"
+  by (auto simp add: memb_def)
+
+lemma nil_rsp[quot_respect]:
+  shows "[] \<approx> []"
+  by simp
+
+lemma cons_rsp[quot_respect]:
+  shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
+  by simp
+
+lemma map_rsp[quot_respect]:
+  shows "(op = ===> op \<approx> ===> op \<approx>) map map"
+  by auto
+
+lemma set_rsp[quot_respect]:
+  "(op \<approx> ===> op =) set set"
+  by auto
+
+lemma list_equiv_rsp[quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
+  by auto
+
+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"
+  by (induct xs) (auto simp add: not_memb_nil memb_cons_iff)
+
+lemma [quot_respect]:
+  "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
+  by (simp add: memb_def[symmetric] memb_finter_raw)
+
+lemma memb_delete_raw:
+  "memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)"
+  by (induct xs arbitrary: x y) (auto simp add: memb_def)
+
+lemma [quot_respect]:
+  "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
+  by (simp add: memb_def[symmetric] memb_delete_raw)
+
+lemma fcard_raw_gt_0:
+  assumes a: "x \<in> set xs"
+  shows "0 < fcard_raw xs"
+  using a by (induct xs) (auto simp add: memb_def)
+
+lemma fcard_raw_delete_one:
+  shows "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
+  by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)
+
+lemma fcard_raw_rsp_aux:
+  assumes a: "xs \<approx> ys"
+  shows "fcard_raw xs = fcard_raw ys"
+  using a
+  apply (induct xs arbitrary: ys)
+  apply (auto simp add: memb_def)
+  apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys)")
+  apply (auto)
+  apply (drule_tac x="x" in spec)
+  apply (blast)
+  apply (drule_tac x="[x \<leftarrow> ys. x \<noteq> a]" in meta_spec)
+  apply (simp add: fcard_raw_delete_one memb_def)
+  apply (case_tac "a \<in> set ys")
+  apply (simp only: if_True)
+  apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)")
+  apply (drule Suc_pred'[OF fcard_raw_gt_0])
+  apply (auto)
+  done
+
+lemma fcard_raw_rsp[quot_respect]:
+  shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
+  by (simp add: fcard_raw_rsp_aux)
+
+lemma memb_absorb:
+  shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
+  by (induct xs) (auto simp add: memb_def)
+
+lemma none_memb_nil:
+  "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
+  by (simp add: memb_def)
+
+lemma not_memb_delete_raw_ident:
+  shows "\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"
+  by (induct xs) (auto simp add: memb_def)
+
+lemma memb_commute_ffold_raw:
+  "rsp_fold f \<Longrightarrow> memb h b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (delete_raw b h))"
+  apply (induct b)
+  apply (simp_all add: not_memb_nil)
+  apply (auto)
+  apply (simp_all add: memb_delete_raw not_memb_delete_raw_ident  rsp_fold_def  memb_cons_iff)
+  done
+
+lemma ffold_raw_rsp_pre:
+  "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
+  apply (induct a arbitrary: b)
+  apply (simp add: memb_absorb memb_def none_memb_nil)
+  apply (simp)
+  apply (rule conjI)
+  apply (rule_tac [!] impI)
+  apply (rule_tac [!] conjI)
+  apply (rule_tac [!] impI)
+  apply (subgoal_tac "\<forall>e. memb e a2 = memb e b")
+  apply (simp)
+  apply (simp add: memb_cons_iff memb_def)
+  apply (auto)[1]
+  apply (drule_tac x="e" in spec)
+  apply (blast)
+  apply (case_tac b)
+  apply (simp_all)
+  apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))")
+  apply (simp only:)
+  apply (rule_tac f="f a1" in arg_cong)
+  apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)")
+  apply (simp)
+  apply (simp add: memb_delete_raw)
+  apply (auto simp add: memb_cons_iff)[1]
+  apply (erule memb_commute_ffold_raw)
+  apply (drule_tac x="a1" in spec)
+  apply (simp add: memb_cons_iff)
+  apply (simp add: memb_cons_iff)
+  apply (case_tac b)
+  apply (simp_all)
+  done
+
+lemma [quot_respect]:
+  "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
+  by (simp add: memb_def[symmetric] ffold_raw_rsp_pre)
+
+text {* Distributive lattice with bot *}
+
 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)
@@ -63,7 +235,42 @@
   "sub_list [] x"
   by (simp add: sub_list_def)
 
-instantiation fset :: (type) bot
+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_all add: memb_def)
+  apply (simp add: memb_def[symmetric] memb_finter_raw)
+  by (auto simp add: memb_def)
+
+instantiation fset :: (type) "{bot,distrib_lattice}"
 begin
 
 quotient_definition
@@ -93,40 +300,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 +310,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,10 +347,16 @@
   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 *}
+section {* Finsert and Membership *}
 
 quotient_definition
   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
@@ -178,18 +379,6 @@
 where
   "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
 
-lemma memb_rsp[quot_respect]:
-  shows "(op = ===> op \<approx> ===> op =) memb memb"
-by (auto simp add: memb_def)
-
-lemma nil_rsp[quot_respect]:
-  shows "[] \<approx> []"
-by simp
-
-lemma cons_rsp[quot_respect]:
-  shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
-by simp
-
 section {* Augmenting an fset -- @{const finsert} *}
 
 lemma nil_not_cons:
@@ -197,22 +386,10 @@
   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)
 
-lemma none_memb_nil:
-  "(\<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)
@@ -221,10 +398,6 @@
   shows "memb x xs \<Longrightarrow> memb x (y # xs)"
   by (simp add: memb_def)
 
-lemma memb_absorb:
-  shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
-  by (induct xs) (auto simp add: memb_def id_simps)
-
 section {* Singletons *}
 
 lemma singleton_list_eq:
@@ -239,12 +412,6 @@
 
 section {* Cardinality of finite sets *}
 
-fun
-  fcard_raw :: "'a list \<Rightarrow> nat"
-where
-  fcard_raw_nil:  "fcard_raw [] = 0"
-| fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))"
-
 quotient_definition
   "fcard :: 'a fset \<Rightarrow> nat" 
 is
@@ -254,10 +421,6 @@
   shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
   by (induct xs) (auto simp add: memb_def)
 
-lemma fcard_raw_gt_0:
-  assumes a: "x \<in> set xs"
-  shows "0 < fcard_raw xs"
-  using a by (induct xs) (auto simp add: memb_def)
 
 lemma fcard_raw_not_memb:
   shows "\<not> memb x xs \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)"
@@ -284,10 +447,6 @@
   apply auto
   done
 
-lemma fcard_raw_delete_one:
-  shows "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
-  by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)
-
 lemma fcard_raw_suc_memb:
   assumes a: "fcard_raw A = Suc n"
   shows "\<exists>a. memb a A"
@@ -307,32 +466,7 @@
   then show ?thesis using fcard_raw_0[of A] by simp
 qed
 
-lemma fcard_raw_rsp_aux:
-  assumes a: "xs \<approx> ys"
-  shows "fcard_raw xs = fcard_raw ys"
-  using a
-  apply(induct xs arbitrary: ys)
-  apply(auto simp add: memb_def)
-  apply(subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys)")
-  apply simp
-  apply auto
-  apply (drule_tac x="x" in spec)
-  apply blast
-  apply(drule_tac x="[x \<leftarrow> ys. x \<noteq> a]" in meta_spec)
-  apply(simp add: fcard_raw_delete_one memb_def)
-  apply (case_tac "a \<in> set ys")
-  apply (simp only: if_True)
-  apply (subgoal_tac "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)")
-  apply (drule Suc_pred'[OF fcard_raw_gt_0])
-  apply auto
-  done
-
-lemma fcard_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
-  by (simp add: fcard_raw_rsp_aux)
-
-
-section {* fmap and fset comprehension *}
+section {* fmap *}
 
 quotient_definition
   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
@@ -347,12 +481,6 @@
   "memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys"
   by (induct xs) (simp_all add: not_memb_nil memb_cons_iff)
 
-text {* raw section *}
-
-lemma map_rsp[quot_respect]:
-  shows "(op = ===> op \<approx> ===> op \<approx>) map map"
-  by auto
-
 lemma cons_left_comm:
   "x # y # xs \<approx> y # x # xs"
   by auto
@@ -382,32 +510,10 @@
 
 section {* deletion *}
 
-fun
-  delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
-where
-  "delete_raw [] x = []"
-| "delete_raw (a # A) x = (if (a = x) then delete_raw A x else a # (delete_raw A x))"
-
-lemma memb_delete_raw:
-  "memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)"
-  by (induct xs arbitrary: x y) (auto simp add: memb_def)
-
-lemma delete_raw_rsp:
-  "xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x"
-  by (simp add: memb_def[symmetric] memb_delete_raw)
-
-lemma [quot_respect]:
-  "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
-  by (simp add: memb_def[symmetric] memb_delete_raw)
-
 lemma memb_delete_raw_ident:
   shows "\<not> memb x (delete_raw xs x)"
   by (induct xs) (auto simp add: memb_def)
 
-lemma not_memb_delete_raw_ident:
-  shows "\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"
-  by (induct xs) (auto simp add: memb_def)
-
 lemma fset_raw_delete_raw_cases:
   "xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # delete_raw xs x)"
   by (induct xs) (auto simp add: memb_def)
@@ -420,100 +526,14 @@
   "fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
   by (simp add: fdelete_raw_filter fcard_raw_delete_one)
 
-lemma set_rsp[quot_respect]:
-  "(op \<approx> ===> op =) set set"
-  by auto
 
-definition
-  rsp_fold
-where
-  "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
-
-primrec
-  ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
-where
-  "ffold_raw f z [] = z"
-| "ffold_raw f z (a # A) =
-     (if (rsp_fold f) then
-       if memb a A then ffold_raw f z A
-       else f a (ffold_raw f z A)
-     else z)"
-
-lemma memb_commute_ffold_raw:
-  "rsp_fold f \<Longrightarrow> memb h b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (delete_raw b h))"
-  apply (induct b)
-  apply (simp add: not_memb_nil)
-  apply (simp add: ffold_raw.simps)
-  apply (rule conjI)
-  apply (rule_tac [!] impI)
-  apply (rule_tac [!] conjI)
-  apply (rule_tac [!] impI)
-  apply (simp_all add: memb_delete_raw)
-  apply (simp add: memb_cons_iff)
-  apply (simp add: not_memb_delete_raw_ident)
-  apply (simp add: memb_cons_iff rsp_fold_def)
-  done
 
-lemma ffold_raw_rsp_pre:
-  "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
-  apply (induct a arbitrary: b)
-  apply (simp add: hd_in_set memb_absorb memb_def none_memb_nil)
-  apply (simp add: ffold_raw.simps)
-  apply (rule conjI)
-  apply (rule_tac [!] impI)
-  apply (rule_tac [!] conjI)
-  apply (rule_tac [!] impI)
-  apply (subgoal_tac "\<forall>e. memb e a2 = memb e b")
-  apply (simp)
-  apply (simp add: memb_cons_iff memb_def)
-  apply auto
-  apply (drule_tac x="e" in spec)
-  apply blast
-  apply (case_tac b)
-  apply simp_all
-  apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))")
-  apply (simp only:)
-  apply (rule_tac f="f a1" in arg_cong)
-  apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)")
-  apply simp
-  apply (simp add: memb_delete_raw)
-  apply (auto simp add: memb_cons_iff)[1]
-  apply (erule memb_commute_ffold_raw)
-  apply (drule_tac x="a1" in spec)
-  apply (simp add: memb_cons_iff)
-  apply (simp add: memb_cons_iff)
-  apply (case_tac b)
-  apply simp_all
-  done
 
-lemma [quot_respect]:
-  "(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,16 +548,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
-
 lemma set_cong: 
   shows "(set x = set y) = (x \<approx> y)"
   by auto
@@ -551,9 +561,6 @@
 is
   "concat"
 
-lemma list_equiv_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
-  by auto
 
 text {* alternate formulation with a different decomposition principle
   and a proof of equivalence *}
@@ -579,7 +586,7 @@
   apply (case_tac "memb a (aa # A)")
   apply (simp_all only: memb_cons_iff)
   apply (case_tac [!] "a = aa")
-  apply (simp_all add: delete_raw.simps)
+  apply (simp_all)
   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))
@@ -593,6 +600,10 @@
   using a cons_delete_list_eq2[of e r]
   by simp
 
+lemma delete_raw_rsp:
+  "xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x"
+  by (simp add: memb_def[symmetric] memb_delete_raw)
+
 lemma list_eq2_equiv_aux:
   assumes a: "fcard_raw l = n"
   and b: "l \<approx> r"
@@ -731,13 +742,9 @@
   shows "S |\<union>| {||} = S"
   by (lifting append_Nil2)
 
-lemma funion_sym:
-  shows "S |\<union>| T = T |\<union>| S"
-  by (lifting funion_sym_pre)
+thm sup.commute[where 'a="'a fset"]
 
-lemma funion_assoc:
-  shows "S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)"
-  by (lifting append_assoc)
+thm sup.assoc[where 'a="'a fset"]
 
 lemma singleton_union_left:
   "{|a|} |\<union>| S = finsert a S"
@@ -745,7 +752,7 @@
 
 lemma singleton_union_right:
   "S |\<union>| {|a|} = finsert a S"
-  by (subst funion_sym) simp
+  by (subst sup.commute) simp
 
 section {* Induction and Cases rules for finite sets *}
 
diff -r 0a857f662e4c -r 39951d71bfce Nominal/Manual/Term4.thy
--- a/Nominal/Manual/Term4.thy	Wed Apr 21 10:08:47 2010 +0200
+++ b/Nominal/Manual/Term4.thy	Wed Apr 21 10:09:07 2010 +0200
@@ -1,5 +1,5 @@
 theory Term4
-imports "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "Quotient_List"
+imports "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "Quotient_List" "../../Attic/Prove"
 begin
 
 atom_decl name
@@ -28,7 +28,7 @@
   done
 
 thm permute_rtrm4_permute_rtrm4_list.simps
-lemmas rawperm=permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
+lemmas perm_fixed = permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
 
 
 local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term4.rtrm4")
@@ -48,42 +48,45 @@
 apply simp_all
 done
 
-(* We need sth like:
-lemma fix3: "fv_rtrm4_list = set o map fv_rtrm4" *)
+ML {* @{term "\<Union>a"} *}
+
+lemma fix3: "fv_rtrm4_list = Union o (set o (map fv_rtrm4))"
+apply (rule ext)
+apply (induct_tac x)
+apply simp_all
+done
 
 notation
   alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and
   alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
 thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]
 
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *}
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
 thm alpha4_inj
 
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
-thm alpha4_inj_no
+lemmas alpha4_inj_fixed = alpha4_inj[simplified fix2 fix3]
 
 local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] fv_rtrm4_fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *}
 thm eqvts(1-2)
 
 local_setup {*
-(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt_no}, []),
-  build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj_no} ctxt 1) ctxt) ctxt))
+(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []),
+  build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} ctxt 1) ctxt) ctxt))
 *}
-lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2]
+thm alpha4_eqvt
+lemmas alpha4_eqvt_fixed = alpha4_eqvt[simplified fix2 fix3]
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []),
-  build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj_no} ctxt) ctxt)) *}
+  build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj} ctxt) ctxt)) *}
 thm alpha4_reflp
-ML build_equivps
+lemmas alpha4_reflp_fixed = alpha4_reflp[simplified fix2 fix3]
 
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []),
-  (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thms alpha4_reflp} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *}
-lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2]
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),
+  (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thms alpha4_reflp} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}
+lemmas alpha4_equivp_fixed = alpha4_equivp[simplified fix2 fix3]
 
 quotient_type 
   trm4 = rtrm4 / alpha_rtrm4
-(*and
-  trm4list = "rtrm4 list" / alpha_rtrm4_list*)
   by (simp_all add: alpha4_equivp)
 
 local_setup {*
@@ -96,7 +99,6 @@
 print_theorems
 
 
-
 lemma fv_rtrm4_rsp:
   "xa \<approx>4 ya \<Longrightarrow> fv_rtrm4 xa = fv_rtrm4 ya"
   "x \<approx>4l y \<Longrightarrow> fv_rtrm4_list x = fv_rtrm4_list y"
@@ -115,31 +117,61 @@
 
 lemma [quot_respect]:
   "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4"
-  by (simp add: alpha4_inj)
+  by (simp add: alpha4_inj_fixed)
 
-(* Maybe also need: @{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"} *)
 local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp}
   [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}]
   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *}
-print_theorems
 
-setup {* define_lifted_perms [@{typ trm4}] ["Term4.trm4"] [("permute_trm4", @{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"})] @{thms permute_rtrm4_permute_rtrm4_list_zero permute_rtrm4_permute_rtrm4_list_append} *}
+setup {* define_lifted_perms [@{typ trm4}] ["Term4.trm4"] [("permute_trm4", @{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"})] @{thms permute_rtrm4_permute_rtrm4_list_zero permute_rtrm4_permute_rtrm4_list_plus} *}
 print_theorems
 
-
+(* Instead of permute for trm4_list we may need the following 2 lemmas: *)
+lemma [quot_preserve]: "(id ---> map rep_trm4 ---> map abs_trm4) permute = permute"
+  apply (simp add: expand_fun_eq)
+  apply clarify
+  apply (rename_tac "pi" x)
+  apply (induct_tac x)
+  apply simp
+  apply simp
+  apply (simp add: meta_eq_to_obj_eq[OF permute_trm4_def,simplified expand_fun_eq,simplified])
+  done
 
-lemma bla: "(Ap4 trm4 list = Ap4 trm4a lista) =
-  (trm4 = trm4a \<and> list_rel (op =) list lista)"
-  by (lifting alpha4_inj(2))
+lemma [quot_respect]: "(op = ===> list_rel alpha_rtrm4 ===> list_rel alpha_rtrm4) permute permute"
+  apply simp
+  apply (rule allI)+
+  apply (induct_tac xa y rule: list_induct2')
+  apply simp_all
+  apply clarify
+  apply (erule alpha4_eqvt)
+  done
 
-thm bla[simplified list_rel_eq]
+ML {*
+  map (lift_thm [@{typ trm4}] @{context}) @{thms perm_fixed}
+*}
 
-ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(1)} *}
-ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(2)} *}
-ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(3)[unfolded alpha_gen]} *}
 ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *}
-.
+
+ML {*
+  map (lift_thm [@{typ trm4}] @{context}) @{thms fv_rtrm4_fv_rtrm4_list.simps[simplified fix3]}
+*}
 
-(*lemmas trm1_bp_induct = rtrm4.induct[quot_lifted]*)
+ML {*
+val liftd =
+  map (Local_Defs.unfold @{context} @{thms id_simps}) (
+    map (Local_Defs.fold @{context} @{thms alphas}) (
+      map (lift_thm [@{typ trm4}] @{context}) @{thms alpha4_inj_fixed[unfolded alphas]}
+    )
+  )
+*}
+
+ML {*
+  map (lift_thm [@{typ trm4}] @{context})
+  (flat (map (distinct_rel @{context} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases}) [(@{thms rtrm4.distinct},@{term "alpha_rtrm4"})]))
+*}
+
+ML {*
+  map (lift_thm [@{typ trm4}] @{context}) @{thms eqvts(1-2)[simplified fix3]}
+*}
 
 end
diff -r 0a857f662e4c -r 39951d71bfce Nominal/Parser.thy
--- a/Nominal/Parser.thy	Wed Apr 21 10:08:47 2010 +0200
+++ b/Nominal/Parser.thy	Wed Apr 21 10:09:07 2010 +0200
@@ -336,7 +336,7 @@
 Rsp.thy/prove_const_rsp
  17) prove respects for all datatype constructors
      (unfold eq_iff and alpha_gen; introduce zero permutations; simp)
-Lift.thy/quotient_lift_consts_export
+Perm.thy/quotient_lift_consts_export
  18) define lifted constructors, fv, bn, alpha_bn, permutations
 Perm.thy/define_lifted_perms
  19) lift permutation zero and add properties to show that quotient type is in the pt typeclass