# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271836115 -7200
# Node ID 9972dc5bd7ad1b0336fd7239a2af1ba1f3b61280
# Parent  880fe1d2234e9e2fe2d264b23ba216a99b88c1f3
Reorder FSet

diff -r 880fe1d2234e -r 9972dc5bd7ad Nominal/FSet.thy
--- a/Nominal/FSet.thy	Wed Apr 21 09:13:55 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 21 09:48:35 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,35 +235,6 @@
   "sub_list [] x"
   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 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)
@@ -123,14 +266,9 @@
 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
+  by (auto simp add: memb_def)
 
 instantiation fset :: (type) "{bot,distrib_lattice}"
 begin
@@ -218,7 +356,7 @@
 
 end
 
-section {* Empty fset, Finsert and Membership *}
+section {* Finsert and Membership *}
 
 quotient_definition
   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
@@ -241,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:
@@ -264,10 +390,6 @@
   "(\<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_consI1:
   shows "memb x (x # xs)"
   by (simp add: memb_def)
@@ -276,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:
@@ -294,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
@@ -309,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)"
@@ -339,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"
@@ -362,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"
@@ -402,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
@@ -437,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)
@@ -475,75 +526,9 @@
   "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)
 
 lemma finter_raw_empty:
   "finter_raw l [] = []"
@@ -576,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 *}
@@ -604,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))
@@ -618,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"