# HG changeset patch
# User haftmann
# Date 1281424283 -7200
# Node ID df7d5143db5529daf8e419d79666688eea3ad4c9
# Parent  ad4b59e9d0f9c86abea924922dda59d86ce3610f
executable relation operations contributed by Tjark Weber

diff -r ad4b59e9d0f9 -r df7d5143db55 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Mon Aug 09 16:56:00 2010 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Tue Aug 10 09:11:23 2010 +0200
@@ -268,4 +268,55 @@
 hide_const (open) is_empty empty remove
   set_eq subset_eq subset inter union subtract Inf Sup Inter Union
 
+
+subsection {* Operations on relations *}
+
+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]:
+  "Domain r = fst ` r"
+  by (auto simp add: image_def Bex_def)
+
+lemma Range_snd [code]:
+  "Range r = snd ` r"
+  by (auto simp add: image_def Bex_def)
+
+lemma irrefl_code [code]:
+  "irrefl r \<longleftrightarrow> (\<forall>(x, y)\<in>r. x \<noteq> y)"
+  by (auto simp add: irrefl_def)
+
+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)
+
+definition "exTimes A B = Sigma A (%_. B)"
+
+lemma [code_unfold]:
+  "Sigma A (%_. B) = exTimes A B"
+  by (simp add: exTimes_def)
+
+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 acyclic_code [code]:
+  "acyclic r = irrefl (r^+)"
+  by (simp add: acyclic_def irrefl_def)
+
+lemma wf_code [code]:
+  "wf (Set xs) = acyclic (Set xs)"
+  by (simp add: wf_iff_acyclic_if_finite)
+
 end