executable relation operations contributed by Tjark Weber
authorhaftmann
Tue Aug 10 09:11:23 2010 +0200 (2010-08-10)
changeset 38304df7d5143db55
parent 38303 ad4b59e9d0f9
child 38305 ebc2abe6e160
executable relation operations contributed by Tjark Weber
src/HOL/Library/Executable_Set.thy
     1.1 --- a/src/HOL/Library/Executable_Set.thy	Mon Aug 09 16:56:00 2010 +0200
     1.2 +++ b/src/HOL/Library/Executable_Set.thy	Tue Aug 10 09:11:23 2010 +0200
     1.3 @@ -268,4 +268,55 @@
     1.4  hide_const (open) is_empty empty remove
     1.5    set_eq subset_eq subset inter union subtract Inf Sup Inter Union
     1.6  
     1.7 +
     1.8 +subsection {* Operations on relations *}
     1.9 +
    1.10 +text {* Initially contributed by Tjark Weber. *}
    1.11 +
    1.12 +lemma bounded_Collect_code [code_unfold]:
    1.13 +  "{x\<in>S. P x} = project P S"
    1.14 +  by (auto simp add: project_def)
    1.15 +
    1.16 +lemma Id_on_code [code]:
    1.17 +  "Id_on (Set xs) = Set [(x,x). x \<leftarrow> xs]"
    1.18 +  by (auto simp add: Id_on_def)
    1.19 +
    1.20 +lemma Domain_fst [code]:
    1.21 +  "Domain r = fst ` r"
    1.22 +  by (auto simp add: image_def Bex_def)
    1.23 +
    1.24 +lemma Range_snd [code]:
    1.25 +  "Range r = snd ` r"
    1.26 +  by (auto simp add: image_def Bex_def)
    1.27 +
    1.28 +lemma irrefl_code [code]:
    1.29 +  "irrefl r \<longleftrightarrow> (\<forall>(x, y)\<in>r. x \<noteq> y)"
    1.30 +  by (auto simp add: irrefl_def)
    1.31 +
    1.32 +lemma trans_def [code]:
    1.33 +  "trans r \<longleftrightarrow> (\<forall>(x, y1)\<in>r. \<forall>(y2, z)\<in>r. y1 = y2 \<longrightarrow> (x, z)\<in>r)"
    1.34 +  by (auto simp add: trans_def)
    1.35 +
    1.36 +definition "exTimes A B = Sigma A (%_. B)"
    1.37 +
    1.38 +lemma [code_unfold]:
    1.39 +  "Sigma A (%_. B) = exTimes A B"
    1.40 +  by (simp add: exTimes_def)
    1.41 +
    1.42 +lemma exTimes_code [code]:
    1.43 +  "exTimes (Set xs) (Set ys) = Set [(x,y). x \<leftarrow> xs, y \<leftarrow> ys]"
    1.44 +  by (auto simp add: exTimes_def)
    1.45 +
    1.46 +lemma rel_comp_code [code]:
    1.47 +  "(Set xys) O (Set yzs) = Set (remdups [(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
    1.48 + by (auto simp add: Bex_def)
    1.49 +
    1.50 +lemma acyclic_code [code]:
    1.51 +  "acyclic r = irrefl (r^+)"
    1.52 +  by (simp add: acyclic_def irrefl_def)
    1.53 +
    1.54 +lemma wf_code [code]:
    1.55 +  "wf (Set xs) = acyclic (Set xs)"
    1.56 +  by (simp add: wf_iff_acyclic_if_finite)
    1.57 +
    1.58  end