1.1 --- a/src/HOL/Relation.thy	Tue Jul 31 13:55:39 2012 +0200
     1.2 +++ b/src/HOL/Relation.thy	Tue Jul 31 13:55:39 2012 +0200
     1.3 @@ -1041,5 +1041,83 @@
     1.4  
     1.5  lemmas Powp_mono [mono] = Pow_mono [to_pred]
     1.6  
     1.7 +subsubsection {* Expressing relation operations via @{const Finite_Set.fold} *}
     1.8 +
     1.9 +lemma Id_on_fold:
    1.10 +  assumes "finite A"
    1.11 +  shows "Id_on A = Finite_Set.fold (\<lambda>x. Set.insert (Pair x x)) {} A"
    1.12 +proof -
    1.13 +  interpret comp_fun_commute "\<lambda>x. Set.insert (Pair x x)" by default auto
    1.14 +  show ?thesis using assms unfolding Id_on_def by (induct A) simp_all
    1.15 +qed
    1.16 +
    1.17 +lemma comp_fun_commute_Image_fold:
    1.18 +  "comp_fun_commute (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A)"
    1.19 +proof -
    1.20 +  interpret comp_fun_idem Set.insert
    1.21 +      by (fact comp_fun_idem_insert)
    1.22 +  show ?thesis 
    1.23 +  by default (auto simp add: fun_eq_iff comp_fun_commute split:prod.split)
    1.24 +qed
    1.25 +
    1.26 +lemma Image_fold:
    1.27 +  assumes "finite R"
    1.28 +  shows "R `` S = Finite_Set.fold (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A) {} R"
    1.29 +proof -
    1.30 +  interpret comp_fun_commute "(\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A)" 
    1.31 +    by (rule comp_fun_commute_Image_fold)
    1.32 +  have *: "\<And>x F. Set.insert x F `` S = (if fst x \<in> S then Set.insert (snd x) (F `` S) else (F `` S))"
    1.33 +    by (auto intro: rev_ImageI)
    1.34 +  show ?thesis using assms by (induct R) (auto simp: *)
    1.35 +qed
    1.36 +
    1.37 +lemma insert_relcomp_union_fold:
    1.38 +  assumes "finite S"
    1.39 +  shows "{x} O S \<union> X = Finite_Set.fold (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') X S"
    1.40 +proof -
    1.41 +  interpret comp_fun_commute "\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A'"
    1.42 +  proof - 
    1.43 +    interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
    1.44 +    show "comp_fun_commute (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A')"
    1.45 +    by default (auto simp add: fun_eq_iff split:prod.split)
    1.46 +  qed
    1.47 +  have *: "{x} O S = {(x', z). x' = fst x \<and> (snd x,z) \<in> S}" by (auto simp: relcomp_unfold intro!: exI)
    1.48 +  show ?thesis unfolding *
    1.49 +  using `finite S` by (induct S) (auto split: prod.split)
    1.50 +qed
    1.51 +
    1.52 +lemma insert_relcomp_fold:
    1.53 +  assumes "finite S"
    1.54 +  shows "Set.insert x R O S = 
    1.55 +    Finite_Set.fold (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') (R O S) S"
    1.56 +proof -
    1.57 +  have "Set.insert x R O S = ({x} O S) \<union> (R O S)" by auto
    1.58 +  then show ?thesis by (auto simp: insert_relcomp_union_fold[OF assms])
    1.59 +qed
    1.60 +
    1.61 +lemma comp_fun_commute_relcomp_fold:
    1.62 +  assumes "finite S"
    1.63 +  shows "comp_fun_commute (\<lambda>(x,y) A. 
    1.64 +    Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S)"
    1.65 +proof -
    1.66 +  have *: "\<And>a b A. 
    1.67 +    Finite_Set.fold (\<lambda>(w, z) A'. if b = w then Set.insert (a, z) A' else A') A S = {(a,b)} O S \<union> A"
    1.68 +    by (auto simp: insert_relcomp_union_fold[OF assms] cong: if_cong)
    1.69 +  show ?thesis by default (auto simp: *)
    1.70 +qed
    1.71 +
    1.72 +lemma relcomp_fold:
    1.73 +  assumes "finite R"
    1.74 +  assumes "finite S"
    1.75 +  shows "R O S = Finite_Set.fold 
    1.76 +    (\<lambda>(x,y) A. Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S) {} R"
    1.77 +proof -
    1.78 +  show ?thesis using assms by (induct R) 
    1.79 +    (auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold 
    1.80 +      cong: if_cong)
    1.81 +qed
    1.82 +
    1.83 +
    1.84 +
    1.85  end
    1.86