1.1 --- a/src/HOL/Library/Executable_Set.thy	Tue Sep 20 15:23:17 2011 +0200
     1.2 +++ b/src/HOL/Library/Executable_Set.thy	Tue Sep 20 21:47:52 2011 +0200
     1.3 @@ -101,12 +101,12 @@
     1.4  lemma insert_Set [code]:
     1.5    "insert x (Set xs) = Set (List.insert x xs)"
     1.6    "insert x (Coset xs) = Coset (removeAll x xs)"
     1.7 -  by (simp_all add: set_insert)
     1.8 +  by simp_all
     1.9  
    1.10  lemma remove_Set [code]:
    1.11    "remove x (Set xs) = Set (removeAll x xs)"
    1.12    "remove x (Coset xs) = Coset (List.insert x xs)"
    1.13 -  by (auto simp add: set_insert remove_def)
    1.14 +  by (auto simp add: remove_def)
    1.15  
    1.16  lemma image_Set [code]:
    1.17    "image f (Set xs) = Set (remdups (map f xs))"
    1.18 @@ -254,12 +254,12 @@
    1.19  lemma Inf_inf [code]:
    1.20    "Inf (Set xs) = foldr inf xs (top :: 'a::complete_lattice)"
    1.21    "Inf (Coset []) = (bot :: 'a::complete_lattice)"
    1.22 -  by (simp_all add: Inf_UNIV Inf_set_foldr)
    1.23 +  by (simp_all add: Inf_set_foldr)
    1.24  
    1.25  lemma Sup_sup [code]:
    1.26    "Sup (Set xs) = foldr sup xs (bot :: 'a::complete_lattice)"
    1.27    "Sup (Coset []) = (top :: 'a::complete_lattice)"
    1.28 -  by (simp_all add: Sup_UNIV Sup_set_foldr)
    1.29 +  by (simp_all add: Sup_set_foldr)
    1.30  
    1.31  lemma Inter_inter [code]:
    1.32    "Inter (Set xs) = foldr inter xs (Coset [])"
    1.33 @@ -279,50 +279,40 @@
    1.34  
    1.35  text {* Initially contributed by Tjark Weber. *}
    1.36  
    1.37 -lemma bounded_Collect_code [code_unfold]:
    1.38 -  "{x\<in>S. P x} = project P S"
    1.39 -  by (auto simp add: project_def)
    1.40 +lemma [code]:
    1.41 +  "Domain r = fst ` r"
    1.42 +  by (fact Domain_fst)
    1.43  
    1.44 -lemma Id_on_code [code]:
    1.45 -  "Id_on (Set xs) = Set [(x,x). x \<leftarrow> xs]"
    1.46 -  by (auto simp add: Id_on_def)
    1.47 +lemma [code]:
    1.48 +  "Range r = snd ` r"
    1.49 +  by (fact Range_snd)
    1.50  
    1.51 -lemma Domain_fst [code]:
    1.52 -  "Domain r = fst ` r"
    1.53 -  by (auto simp add: image_def Bex_def)
    1.54 +lemma [code]:
    1.55 +  "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
    1.56 +  by (fact trans_join)
    1.57  
    1.58 -lemma Range_snd [code]:
    1.59 -  "Range r = snd ` r"
    1.60 -  by (auto simp add: image_def Bex_def)
    1.61 +lemma [code]:
    1.62 +  "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
    1.63 +  by (fact irrefl_distinct)
    1.64  
    1.65 -lemma irrefl_code [code]:
    1.66 -  "irrefl r \<longleftrightarrow> (\<forall>(x, y)\<in>r. x \<noteq> y)"
    1.67 -  by (auto simp add: irrefl_def)
    1.68 +lemma [code]:
    1.69 +  "acyclic r \<longleftrightarrow> irrefl (r^+)"
    1.70 +  by (fact acyclic_irrefl)
    1.71  
    1.72 -lemma trans_def [code]:
    1.73 -  "trans r \<longleftrightarrow> (\<forall>(x, y1)\<in>r. \<forall>(y2, z)\<in>r. y1 = y2 \<longrightarrow> (x, z)\<in>r)"
    1.74 -  by (auto simp add: trans_def)
    1.75 +lemma [code]:
    1.76 +  "More_Set.product (Set xs) (Set ys) = Set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
    1.77 +  by (unfold Set_def) (fact product_code)
    1.78  
    1.79 -definition "exTimes A B = Sigma A (%_. B)"
    1.80 +lemma [code]:
    1.81 +  "Id_on (Set xs) = Set [(x, x). x \<leftarrow> xs]"
    1.82 +  by (unfold Set_def) (fact Id_on_set)
    1.83  
    1.84 -lemma [code_unfold]:
    1.85 -  "Sigma A (%_. B) = exTimes A B"
    1.86 -  by (simp add: exTimes_def)
    1.87 +lemma [code]:
    1.88 +  "Set xys O Set yzs = Set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
    1.89 +  by (unfold Set_def) (fact set_rel_comp)
    1.90  
    1.91 -lemma exTimes_code [code]:
    1.92 -  "exTimes (Set xs) (Set ys) = Set [(x,y). x \<leftarrow> xs, y \<leftarrow> ys]"
    1.93 -  by (auto simp add: exTimes_def)
    1.94 -
    1.95 -lemma rel_comp_code [code]:
    1.96 -  "(Set xys) O (Set yzs) = Set (remdups [(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
    1.97 - by (auto simp add: Bex_def)
    1.98 -
    1.99 -lemma acyclic_code [code]:
   1.100 -  "acyclic r = irrefl (r^+)"
   1.101 -  by (simp add: acyclic_def irrefl_def)
   1.102 -
   1.103 -lemma wf_code [code]:
   1.104 +lemma [code]:
   1.105    "wf (Set xs) = acyclic (Set xs)"
   1.106 -  by (simp add: wf_iff_acyclic_if_finite)
   1.107 +  by (unfold Set_def) (fact wf_set)
   1.108  
   1.109  end

     2.1 --- a/src/HOL/Library/More_Set.thy	Tue Sep 20 15:23:17 2011 +0200
     2.2 +++ b/src/HOL/Library/More_Set.thy	Tue Sep 20 21:47:52 2011 +0200
     2.3 @@ -31,7 +31,20 @@
     2.4  qed
     2.5  
     2.6  definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
     2.7 -  "project P A = {a\<in>A. P a}"
     2.8 +  "project P A = {a \<in> A. P a}"
     2.9 +
    2.10 +lemma bounded_Collect_code [code_unfold_post]:
    2.11 +  "{x \<in> A. P x} = project P A"
    2.12 +  by (simp add: project_def)
    2.13 +
    2.14 +definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
    2.15 +  "product A B = Sigma A (\<lambda>_. B)"
    2.16 +
    2.17 +hide_const (open) product
    2.18 +
    2.19 +lemma [code_unfold_post]:
    2.20 +  "Sigma A (\<lambda>_. B) = More_Set.product A B"
    2.21 +  by (simp add: product_def)
    2.22  
    2.23  
    2.24  subsection {* Basic set operations *}
    2.25 @@ -75,7 +88,7 @@
    2.26    "set xs \<union> A = foldr Set.insert xs A"
    2.27  proof -
    2.28    have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
    2.29 -    by (auto intro: ext)
    2.30 +    by auto
    2.31    then show ?thesis by (simp add: union_set foldr_fold)
    2.32  qed
    2.33  
    2.34 @@ -92,7 +105,7 @@
    2.35    "A - set xs = foldr remove xs A"
    2.36  proof -
    2.37    have "\<And>x y :: 'a. remove y \<circ> remove x = remove x \<circ> remove y"
    2.38 -    by (auto simp add: remove_def intro: ext)
    2.39 +    by (auto simp add: remove_def)
    2.40    then show ?thesis by (simp add: minus_set foldr_fold)
    2.41  qed
    2.42  
    2.43 @@ -120,10 +133,22 @@
    2.44    by (auto simp add: project_def)
    2.45  
    2.46  
    2.47 -subsection {* Various lemmas *}
    2.48 +subsection {* Theorems on relations *}
    2.49  
    2.50 -lemma not_set_compl:
    2.51 -  "Not \<circ> set xs = - set xs"
    2.52 -  by (simp add: fun_Compl_def comp_def fun_eq_iff)
    2.53 +lemma product_code:
    2.54 +  "More_Set.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
    2.55 +  by (auto simp add: product_def)
    2.56 +
    2.57 +lemma Id_on_set:
    2.58 +  "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
    2.59 +  by (auto simp add: Id_on_def)
    2.60 +
    2.61 +lemma set_rel_comp:
    2.62 +  "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
    2.63 +  by (auto simp add: Bex_def)
    2.64 +
    2.65 +lemma wf_set:
    2.66 +  "wf (set xs) = acyclic (set xs)"
    2.67 +  by (simp add: wf_iff_acyclic_if_finite)
    2.68  
    2.69  end

     3.1 --- a/src/HOL/Relation.thy	Tue Sep 20 15:23:17 2011 +0200
     3.2 +++ b/src/HOL/Relation.thy	Tue Sep 20 21:47:52 2011 +0200
     3.3 @@ -275,6 +275,10 @@
     3.4  
     3.5  subsection {* Transitivity *}
     3.6  
     3.7 +lemma trans_join:
     3.8 +  "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
     3.9 +  by (auto simp add: trans_def)
    3.10 +
    3.11  lemma transI:
    3.12    "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
    3.13  by (unfold trans_def) iprover
    3.14 @@ -296,6 +300,10 @@
    3.15  
    3.16  subsection {* Irreflexivity *}
    3.17  
    3.18 +lemma irrefl_distinct:
    3.19 +  "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
    3.20 +  by (auto simp add: irrefl_def)
    3.21 +
    3.22  lemma irrefl_diff_Id[simp]: "irrefl(r-Id)"
    3.23  by(simp add:irrefl_def)
    3.24  
    3.25 @@ -386,6 +394,10 @@
    3.26    "a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
    3.27  by (iprover dest!: iffD1 [OF Domain_iff])
    3.28  
    3.29 +lemma Domain_fst:
    3.30 +  "Domain r = fst ` r"
    3.31 +  by (auto simp add: image_def Bex_def)
    3.32 +
    3.33  lemma Domain_empty [simp]: "Domain {} = {}"
    3.34  by blast
    3.35  
    3.36 @@ -440,6 +452,10 @@
    3.37  lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
    3.38  by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
    3.39  
    3.40 +lemma Range_snd:
    3.41 +  "Range r = snd ` r"
    3.42 +  by (auto simp add: image_def Bex_def)
    3.43 +
    3.44  lemma Range_empty [simp]: "Range {} = {}"
    3.45  by blast
    3.46  

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