Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/FSet.thy
changeset 2546 3a7155fce1da
parent 2544 3b24b5d2b68c
child 2547 17b369a73f15 
--- a/Nominal/FSet.thy	Mon Oct 18 09:42:51 2010 +0100
+++ b/Nominal/FSet.thy	Mon Oct 18 11:51:22 2010 +0100
@@ -9,12 +9,15 @@
 imports Quotient_List
 begin
 
-text {* Definition of the equivalence relation over lists *}
+text {* 
+  The type of finite sets is created by a quotient construction
+  over lists. The definition of the equivalence:
+*}
 
 fun
   list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
 where
-  "list_eq xs ys = (set xs = set ys)"
+  "list_eq xs ys \<longleftrightarrow> set xs = set ys"
 
 lemma list_eq_equivp:
   shows "equivp list_eq"
@@ -34,20 +37,30 @@
   lists.
 *}
 
-definition
-  "memb x xs \<equiv> x \<in> set xs"
+fun
+  memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
+where
+  "memb x xs \<longleftrightarrow> x \<in> set xs"
 
-definition
-  "sub_list xs ys \<equiv> set xs \<subseteq> set ys"
+fun
+  sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+where 
+  "sub_list xs ys \<longleftrightarrow> set xs \<subseteq> set ys"
 
-definition
+fun
+  card_list :: "'a list \<Rightarrow> nat"
+where
   "card_list xs = card (set xs)"
 
-definition
+fun
+  inter_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
   "inter_list xs ys = [x \<leftarrow> xs. x \<in> set xs \<and> x \<in> set ys]"
 
-definition
-  "diff_list xs ys \<equiv> [x \<leftarrow> xs. x \<notin> set ys]"
+fun
+  diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
+  "diff_list xs ys = [x \<leftarrow> xs. x \<notin> set ys]"
 
 definition
   rsp_fold
@@ -160,11 +173,11 @@
 
 lemma sub_list_rsp [quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
-  by (auto simp add: sub_list_def)
+  by simp
 
 lemma memb_rsp [quot_respect]:
   shows "(op = ===> op \<approx> ===> op =) memb memb"
-  by (auto simp add: memb_def)
+  by simp
 
 lemma nil_rsp [quot_respect]:
   shows "(op \<approx>) Nil Nil"
@@ -184,7 +197,7 @@
 
 lemma inter_list_rsp [quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) inter_list inter_list"
-  by (simp add: inter_list_def)
+  by simp
 
 lemma removeAll_rsp [quot_respect]:
   shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
@@ -192,11 +205,11 @@
 
 lemma diff_list_rsp [quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) diff_list diff_list"
-  by (simp add: diff_list_def)
+  by simp
 
 lemma card_list_rsp [quot_respect]:
   shows "(op \<approx> ===> op =) card_list card_list"
-  by (simp add: card_list_def)
+  by simp
 
 lemma filter_rsp [quot_respect]:
   shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
@@ -339,41 +352,35 @@
   fix x y z :: "'a fset"
   show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x"
     unfolding less_fset_def 
-    by (descending) (auto simp add: sub_list_def)
-  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) (auto simp add: inter_list_def sub_list_def memb_def)
-  show "x |\<inter>| y |\<subseteq>| y" 
-    by (descending) (auto simp add: inter_list_def sub_list_def memb_def)
+    by (descending) (auto)
+  show "x |\<subseteq>| x"  by (descending) (simp)
+  show "{||} |\<subseteq>| x" by (descending) (simp)
+  show "x |\<subseteq>| x |\<union>| y" by (descending) (simp)
+  show "y |\<subseteq>| x |\<union>| y" by (descending) (simp)
+  show "x |\<inter>| y |\<subseteq>| x" by (descending) (auto)
+  show "x |\<inter>| y |\<subseteq>| y" by (descending) (auto)
   show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" 
-    by (descending) (auto simp add: inter_list_def)
+    by (descending) (auto)
 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 (descending) (simp add: sub_list_def)
+  show "x |\<subseteq>| z" using a b by (descending) (simp)
 next
   fix x y :: "'a fset"
   assume a: "x |\<subseteq>| y"
   assume b: "y |\<subseteq>| x"
-  show "x = y" using a b 
-    by (descending) (unfold sub_list_def list_eq.simps, blast)
+  show "x = y" using a b by (descending) (auto)
 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 (descending) (simp add: sub_list_def)
+  show "y |\<union>| z |\<subseteq>| x" using a b by (descending) (simp)
 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 (descending) (auto simp add: inter_list_def sub_list_def memb_def)
+  show "x |\<subseteq>| y |\<inter>| z" using a b by (descending) (auto)
 qed
 
 end
@@ -549,7 +556,7 @@
 
 lemma inter_fset [simp]: 
   shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"
-  by (descending) (auto simp add: inter_list_def)
+  by (descending) (auto)
 
 lemma union_fset [simp]: 
   shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"
@@ -557,14 +564,14 @@
 
 lemma minus_fset [simp]: 
   shows "fset (xs - ys) = fset xs - fset ys"
-  by (descending) (auto simp add: diff_list_def)
+  by (descending) (auto)
 
 
 subsection {* in_fset *}
 
 lemma in_fset: 
   shows "x |\<in>| S \<longleftrightarrow> x \<in> fset S"
-  by (descending) (simp add: memb_def)
+  by (descending) (simp)
 
 lemma notin_fset: 
   shows "x |\<notin>| S \<longleftrightarrow> x \<notin> fset S"
@@ -576,18 +583,18 @@
 
 lemma fset_eq_iff:
   shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
-  by (descending) (auto simp add: memb_def)
+  by (descending) (auto)
 
 lemma none_in_empty_fset:
   shows "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
-  by (descending) (simp add: memb_def)
+  by (descending) (simp)
 
 
 subsection {* insert_fset *}
 
 lemma in_insert_fset_iff [simp]:
   shows "x |\<in>| insert_fset y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
-  by (descending) (simp add: memb_def)
+  by (descending) (simp)
 
 lemma
   shows insert_fsetI1: "x |\<in>| insert_fset x S"
@@ -596,7 +603,7 @@
 
 lemma insert_absorb_fset [simp]:
   shows "x |\<in>| S \<Longrightarrow> insert_fset x S = S"
-  by (descending) (auto simp add: memb_def)
+  by (descending) (auto)
 
 lemma empty_not_insert_fset[simp]:
   shows "{||} \<noteq> insert_fset x S"
@@ -619,7 +626,7 @@
 (* FIXME: is this a useful lemma ? *)
 lemma in_fset_mdef:
   shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = insert_fset x (F - {|x|})"
-  by (descending) (auto simp add: memb_def diff_list_def)
+  by (descending) (auto)
 
 
 subsection {* union_fset *}
@@ -642,18 +649,18 @@
 
 lemma in_union_fset:
   shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
-  by (descending) (simp add: memb_def)
+  by (descending) (simp)
 
 
 subsection {* minus_fset *}
 
 lemma minus_in_fset: 
   shows "x |\<in>| (xs - ys) \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
-  by (descending) (simp add: diff_list_def memb_def)
+  by (descending) (simp)
 
 lemma minus_insert_fset: 
   shows "insert_fset x xs - ys = (if x |\<in>| ys then xs - ys else insert_fset x (xs - ys))"
-  by (descending) (auto simp add: diff_list_def memb_def)
+  by (descending) (auto)
 
 lemma minus_insert_in_fset[simp]: 
   shows "x |\<in>| ys \<Longrightarrow> insert_fset x xs - ys = xs - ys"
@@ -678,19 +685,19 @@
 
 lemma in_remove_fset:
   shows "x |\<in>| remove_fset y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
-  by (descending) (simp add: memb_def)
+  by (descending) (simp)
 
 lemma notin_remove_fset:
   shows "x |\<notin>| remove_fset x S"
-  by (descending) (simp add: memb_def)
+  by (descending) (simp)
 
 lemma notin_remove_ident_fset:
   shows "x |\<notin>| S \<Longrightarrow> remove_fset x S = S"
-  by (descending) (simp add: memb_def)
+  by (descending) (simp)
 
 lemma remove_fset_cases:
   shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = insert_fset x (remove_fset x S))"
-  by (descending) (auto simp add: memb_def insert_absorb)
+  by (descending) (auto simp add: insert_absorb)
   
 
 subsection {* inter_fset *}
@@ -705,35 +712,35 @@
 
 lemma inter_insert_fset:
   shows "insert_fset x S |\<inter>| T = (if x |\<in>| T then insert_fset x (S |\<inter>| T) else S |\<inter>| T)"
-  by (descending) (auto simp add: inter_list_def memb_def)
+  by (descending) (auto)
 
 lemma in_inter_fset:
   shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
-  by (descending) (simp add: inter_list_def memb_def)
+  by (descending) (simp)
 
 
 subsection {* subset_fset and psubset_fset *}
 
 lemma subset_fset: 
   shows "xs |\<subseteq>| ys \<longleftrightarrow> fset xs \<subseteq> fset ys"
-  by (descending) (simp add: sub_list_def)
+  by (descending) (simp)
 
 lemma psubset_fset: 
   shows "xs |\<subset>| ys \<longleftrightarrow> fset xs \<subset> fset ys"
   unfolding less_fset_def 
-  by (descending) (auto simp add: sub_list_def)
+  by (descending) (auto)
 
 lemma subset_insert_fset:
   shows "(insert_fset x xs) |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"
-  by (descending) (simp add: sub_list_def memb_def)
+  by (descending) (simp)
 
 lemma subset_in_fset: 
   shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
-  by (descending) (auto simp add: sub_list_def memb_def)
+  by (descending) (auto)
 
 lemma subset_empty_fset:
   shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
-  by (descending) (simp add: sub_list_def)
+  by (descending) (simp)
 
 lemma not_psubset_empty_fset: 
   shows "\<not> xs |\<subset>| {||}"
@@ -764,15 +771,15 @@
 
 lemma card_fset: 
   shows "card_fset xs = card (fset xs)"
-  by (lifting card_list_def)
+  by (descending) (simp)
 
 lemma card_insert_fset_iff [simp]:
   shows "card_fset (insert_fset x S) = (if x |\<in>| S then card_fset S else Suc (card_fset S))"
-  by (descending) (auto simp add: card_list_def memb_def insert_absorb)
+  by (descending) (simp add: insert_absorb)
 
 lemma card_fset_0[simp]:
   shows "card_fset S = 0 \<longleftrightarrow> S = {||}"
-  by (descending) (simp add: card_list_def)
+  by (descending) (simp)
 
 lemma card_empty_fset[simp]:
   shows "card_fset {||} = 0"
@@ -780,11 +787,11 @@
 
 lemma card_fset_1:
   shows "card_fset S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})"
-  by (descending) (auto simp add: card_list_def card_Suc_eq)
+  by (descending) (auto simp add: card_Suc_eq)
 
 lemma card_fset_gt_0:
   shows "x \<in> fset S \<Longrightarrow> 0 < card_fset S"
-  by (descending) (auto simp add: card_list_def card_gt_0_iff)
+  by (descending) (auto simp add: card_gt_0_iff)
   
 lemma card_notin_fset:
   shows "(x |\<notin>| S) = (card_fset (insert_fset x S) = Suc (card_fset S))"
@@ -793,12 +800,12 @@
 lemma card_fset_Suc: 
   shows "card_fset S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = insert_fset x T \<and> card_fset T = n"
   apply(descending)
-  apply(auto simp add: card_list_def memb_def dest!: card_eq_SucD)
+  apply(auto dest!: card_eq_SucD)
   by (metis Diff_insert_absorb set_removeAll)
 
 lemma card_remove_fset_iff [simp]:
   shows "card_fset (remove_fset y S) = (if y |\<in>| S then card_fset S - 1 else card_fset S)"
-  by (descending) (simp add: card_list_def memb_def)
+  by (descending) (simp)
 
 lemma card_Suc_exists_in_fset: 
   shows "card_fset S = Suc n \<Longrightarrow> \<exists>a. a |\<in>| S"
@@ -806,12 +813,12 @@
 
 lemma in_card_fset_not_0: 
   shows "a |\<in>| A \<Longrightarrow> card_fset A \<noteq> 0"
-  by (descending) (auto simp add: card_list_def memb_def)
+  by (descending) (auto)
 
 lemma card_fset_mono: 
   shows "xs |\<subseteq>| ys \<Longrightarrow> card_fset xs \<le> card_fset ys"
   unfolding card_fset psubset_fset
-  by (simp add:  card_mono subset_fset)
+  by (simp add: card_mono subset_fset)
 
 lemma card_subset_fset_eq: 
   shows "xs |\<subseteq>| ys \<Longrightarrow> card_fset ys \<le> card_fset xs \<Longrightarrow> xs = ys"
@@ -898,11 +905,11 @@
 
 lemma subset_filter_fset: 
   shows "filter_fset P xs |\<subseteq>| filter_fset Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
-  by  (descending) (auto simp add: memb_def sub_list_def)
+  by  (descending) (auto)
 
 lemma eq_filter_fset: 
   shows "(filter_fset P xs = filter_fset Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
-  by (descending) (auto simp add: memb_def)
+  by (descending) (auto)
 
 lemma psubset_filter_fset:
   shows "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> 
@@ -918,11 +925,11 @@
 
 lemma fold_insert_fset: "fold_fset f z (insert_fset a A) =
   (if rsp_fold f then if a |\<in>| A then fold_fset f z A else f a (fold_fset f z A) else z)"
-  by (descending) (simp add: memb_def)
+  by (descending) (simp)
 
 lemma in_commute_fold_fset:
   "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> fold_fset f z b = f h (fold_fset f z (remove_fset h b))"
-  by (descending) (simp add: memb_def memb_commute_fold_list)
+  by (descending) (simp add: memb_commute_fold_list)
 
 
 subsection {* Choice in fsets *}
@@ -933,7 +940,7 @@
   using a
   apply(descending)
   using finite_set_choice
-  by (auto simp add: memb_def Ball_def)
+  by (auto simp add: Ball_def)
 
 
 section {* Induction and Cases rules for fsets *}
@@ -992,8 +999,9 @@
   case (Cons a xs)
   have a: "\<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis" by fact
   have b: "\<And>x' ys'. \<lbrakk>\<not> memb x' ys'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
-  have c: "xs = [] \<Longrightarrow> thesis" using b unfolding memb_def
-    by (metis in_set_conv_nth less_zeroE list.size(3) list_eq.simps member_set)
+  have c: "xs = [] \<Longrightarrow> thesis" using b 
+    apply(simp)
+    by (metis List.set.simps(1) emptyE empty_subsetI)
   have "\<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
   proof -
     fix x :: 'a
@@ -1008,9 +1016,9 @@
       show thesis using b f g by simp
     next
       assume h: "x \<noteq> a"
-      then have f: "\<not> memb x (a # ys)" using d unfolding memb_def by auto
+      then have f: "\<not> memb x (a # ys)" using d by auto
       have g: "a # xs \<approx> x # (a # ys)" using e h by auto
-      show thesis using b f g by simp
+      show thesis using b f g by (simp del: memb.simps) 
     qed
   qed
   then show thesis using a c by blast
@@ -1058,13 +1066,13 @@
 lemma cons_delete_list_eq2:
   shows "(a # (removeAll a A)) \<approx>2 (if memb a A then A else a # A)"
   apply (induct A)
-  apply (simp add: memb_def list_eq2_refl)
+  apply (simp add: list_eq2_refl)
   apply (case_tac "memb a (aa # A)")
-  apply (simp_all only: memb_def)
+  apply (simp_all)
   apply (case_tac [!] "a = aa")
   apply (simp_all)
   apply (case_tac "memb a A")
-  apply (auto simp add: memb_def)[2]
+  apply (auto)[2]
   apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
   apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
   apply (auto simp add: list_eq2_refl memb_def)
@@ -1089,8 +1097,8 @@
     proof (induct n arbitrary: l r)
       case 0
       have "card_list l = 0" by fact
-      then have "\<forall>x. \<not> memb x l" unfolding card_list_def memb_def by auto
-      then have z: "l = []" unfolding memb_def by auto
+      then have "\<forall>x. \<not> memb x l" by auto
+      then have z: "l = []" by auto
       then have "r = []" using `l \<approx> r` by simp
       then show ?case using z list_eq2_refl by simp
     next
@@ -1098,14 +1106,14 @@
       have b: "l \<approx> r" by fact
       have d: "card_list l = Suc m" by fact
       then have "\<exists>a. memb a l" 
-	apply(simp add: card_list_def memb_def)
+	apply(simp)
 	apply(drule card_eq_SucD)
 	apply(blast)
 	done
       then obtain a where e: "memb a l" by auto
       then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b 
-	unfolding memb_def by auto
-      have f: "card_list (removeAll a l) = m" using e d by (simp add: card_list_def memb_def)
+	by auto
+      have f: "card_list (removeAll a l) = m" using e d by (simp)
       have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
       have "(removeAll a l) \<approx>2 (removeAll a r)" by (rule Suc.hyps[OF f g])
       then have h: "(a # removeAll a l) \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(5))
nominal2