tuned specification and lemma distribution among theories; tuned proofs

--- a/src/HOL/Library/Executable_Set.thy	Tue Sep 20 15:23:17 2011 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Tue Sep 20 21:47:52 2011 +0200
@@ -101,12 +101,12 @@
 lemma insert_Set [code]:
   "insert x (Set xs) = Set (List.insert x xs)"
   "insert x (Coset xs) = Coset (removeAll x xs)"
-  by (simp_all add: set_insert)
+  by simp_all
 
 lemma remove_Set [code]:
   "remove x (Set xs) = Set (removeAll x xs)"
   "remove x (Coset xs) = Coset (List.insert x xs)"
-  by (auto simp add: set_insert remove_def)
+  by (auto simp add: remove_def)
 
 lemma image_Set [code]:
   "image f (Set xs) = Set (remdups (map f xs))"
@@ -254,12 +254,12 @@
 lemma Inf_inf [code]:
   "Inf (Set xs) = foldr inf xs (top :: 'a::complete_lattice)"
   "Inf (Coset []) = (bot :: 'a::complete_lattice)"
-  by (simp_all add: Inf_UNIV Inf_set_foldr)
+  by (simp_all add: Inf_set_foldr)
 
 lemma Sup_sup [code]:
   "Sup (Set xs) = foldr sup xs (bot :: 'a::complete_lattice)"
   "Sup (Coset []) = (top :: 'a::complete_lattice)"
-  by (simp_all add: Sup_UNIV Sup_set_foldr)
+  by (simp_all add: Sup_set_foldr)
 
 lemma Inter_inter [code]:
   "Inter (Set xs) = foldr inter xs (Coset [])"
@@ -279,50 +279,40 @@
 
 text {* Initially contributed by Tjark Weber. *}
 
-lemma bounded_Collect_code [code_unfold]:
-  "{x\<in>S. P x} = project P S"
-  by (auto simp add: project_def)
-
-lemma Id_on_code [code]:
-  "Id_on (Set xs) = Set [(x,x). x \<leftarrow> xs]"
-  by (auto simp add: Id_on_def)
-
-lemma Domain_fst [code]:
+lemma [code]:
   "Domain r = fst ` r"
-  by (auto simp add: image_def Bex_def)
+  by (fact Domain_fst)
 
-lemma Range_snd [code]:
+lemma [code]:
   "Range r = snd ` r"
-  by (auto simp add: image_def Bex_def)
+  by (fact Range_snd)
 
-lemma irrefl_code [code]:
-  "irrefl r \<longleftrightarrow> (\<forall>(x, y)\<in>r. x \<noteq> y)"
-  by (auto simp add: irrefl_def)
+lemma [code]:
+  "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
+  by (fact trans_join)
+
+lemma [code]:
+  "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
+  by (fact irrefl_distinct)
 
-lemma trans_def [code]:
-  "trans r \<longleftrightarrow> (\<forall>(x, y1)\<in>r. \<forall>(y2, z)\<in>r. y1 = y2 \<longrightarrow> (x, z)\<in>r)"
-  by (auto simp add: trans_def)
+lemma [code]:
+  "acyclic r \<longleftrightarrow> irrefl (r^+)"
+  by (fact acyclic_irrefl)
 
-definition "exTimes A B = Sigma A (%_. B)"
-
-lemma [code_unfold]:
-  "Sigma A (%_. B) = exTimes A B"
-  by (simp add: exTimes_def)
+lemma [code]:
+  "More_Set.product (Set xs) (Set ys) = Set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
+  by (unfold Set_def) (fact product_code)
 
-lemma exTimes_code [code]:
-  "exTimes (Set xs) (Set ys) = Set [(x,y). x \<leftarrow> xs, y \<leftarrow> ys]"
-  by (auto simp add: exTimes_def)
-
-lemma rel_comp_code [code]:
-  "(Set xys) O (Set yzs) = Set (remdups [(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
- by (auto simp add: Bex_def)
+lemma [code]:
+  "Id_on (Set xs) = Set [(x, x). x \<leftarrow> xs]"
+  by (unfold Set_def) (fact Id_on_set)
 
-lemma acyclic_code [code]:
-  "acyclic r = irrefl (r^+)"
-  by (simp add: acyclic_def irrefl_def)
+lemma [code]:
+  "Set xys O Set yzs = Set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
+  by (unfold Set_def) (fact set_rel_comp)
 
-lemma wf_code [code]:
+lemma [code]:
   "wf (Set xs) = acyclic (Set xs)"
-  by (simp add: wf_iff_acyclic_if_finite)
+  by (unfold Set_def) (fact wf_set)
 
 end

--- a/src/HOL/Library/More_Set.thy	Tue Sep 20 15:23:17 2011 +0200
+++ b/src/HOL/Library/More_Set.thy	Tue Sep 20 21:47:52 2011 +0200
@@ -31,7 +31,20 @@
 qed
 
 definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
-  "project P A = {a\<in>A. P a}"
+  "project P A = {a \<in> A. P a}"
+
+lemma bounded_Collect_code [code_unfold_post]:
+  "{x \<in> A. P x} = project P A"
+  by (simp add: project_def)
+
+definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
+  "product A B = Sigma A (\<lambda>_. B)"
+
+hide_const (open) product
+
+lemma [code_unfold_post]:
+  "Sigma A (\<lambda>_. B) = More_Set.product A B"
+  by (simp add: product_def)
 
 
 subsection {* Basic set operations *}
@@ -75,7 +88,7 @@
   "set xs \<union> A = foldr Set.insert xs A"
 proof -
   have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
-    by (auto intro: ext)
+    by auto
   then show ?thesis by (simp add: union_set foldr_fold)
 qed
 
@@ -92,7 +105,7 @@
   "A - set xs = foldr remove xs A"
 proof -
   have "\<And>x y :: 'a. remove y \<circ> remove x = remove x \<circ> remove y"
-    by (auto simp add: remove_def intro: ext)
+    by (auto simp add: remove_def)
   then show ?thesis by (simp add: minus_set foldr_fold)
 qed
 
@@ -120,10 +133,22 @@
   by (auto simp add: project_def)
 
 
-subsection {* Various lemmas *}
+subsection {* Theorems on relations *}
+
+lemma product_code:
+  "More_Set.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
+  by (auto simp add: product_def)
 
-lemma not_set_compl:
-  "Not \<circ> set xs = - set xs"
-  by (simp add: fun_Compl_def comp_def fun_eq_iff)
+lemma Id_on_set:
+  "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
+  by (auto simp add: Id_on_def)
+
+lemma set_rel_comp:
+  "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
+  by (auto simp add: Bex_def)
+
+lemma wf_set:
+  "wf (set xs) = acyclic (set xs)"
+  by (simp add: wf_iff_acyclic_if_finite)
 
 end

--- a/src/HOL/Relation.thy	Tue Sep 20 15:23:17 2011 +0200
+++ b/src/HOL/Relation.thy	Tue Sep 20 21:47:52 2011 +0200
@@ -275,6 +275,10 @@
 
 subsection {* Transitivity *}
 
+lemma trans_join:
+  "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
+  by (auto simp add: trans_def)
+
 lemma transI:
   "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
 by (unfold trans_def) iprover
@@ -296,6 +300,10 @@
 
 subsection {* Irreflexivity *}
 
+lemma irrefl_distinct:
+  "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
+  by (auto simp add: irrefl_def)
+
 lemma irrefl_diff_Id[simp]: "irrefl(r-Id)"
 by(simp add:irrefl_def)
 
@@ -386,6 +394,10 @@
   "a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
 by (iprover dest!: iffD1 [OF Domain_iff])
 
+lemma Domain_fst:
+  "Domain r = fst ` r"
+  by (auto simp add: image_def Bex_def)
+
 lemma Domain_empty [simp]: "Domain {} = {}"
 by blast
 
@@ -440,6 +452,10 @@
 lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
 by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
 
+lemma Range_snd:
+  "Range r = snd ` r"
+  by (auto simp add: image_def Bex_def)
+
 lemma Range_empty [simp]: "Range {} = {}"
 by blast
 

--- a/src/HOL/Wellfounded.thy	Tue Sep 20 15:23:17 2011 +0200
+++ b/src/HOL/Wellfounded.thy	Tue Sep 20 21:47:52 2011 +0200
@@ -387,6 +387,10 @@
 abbreviation acyclicP :: "('a => 'a => bool) => bool" where
   "acyclicP r == acyclic {(x, y). r x y}"
 
+lemma acyclic_irrefl:
+  "acyclic r \<longleftrightarrow> irrefl (r^+)"
+  by (simp add: acyclic_def irrefl_def)
+
 lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
   by (simp add: acyclic_def)