src/HOL/Lifting_Sum.thy
 changeset 55084 8ee9aabb2bca parent 55083 0a689157e3ce child 55414 eab03e9cee8a
```     1.1 --- a/src/HOL/Lifting_Sum.thy	Mon Jan 20 20:21:12 2014 +0100
1.2 +++ b/src/HOL/Lifting_Sum.thy	Mon Jan 20 20:42:43 2014 +0100
1.3 @@ -12,19 +12,12 @@
1.4
1.5  abbreviation (input) "sum_pred \<equiv> sum_case"
1.6
1.7 -lemma sum_rel_eq [relator_eq]:
1.8 -  "sum_rel (op =) (op =) = (op =)"
1.9 -  by (simp add: sum_rel_def fun_eq_iff split: sum.split)
1.10 -
1.11 -lemma sum_rel_mono[relator_mono]:
1.12 -  assumes "A \<le> C"
1.13 -  assumes "B \<le> D"
1.14 -  shows "(sum_rel A B) \<le> (sum_rel C D)"
1.15 -using assms by (auto simp: sum_rel_def split: sum.splits)
1.16 +lemmas sum_rel_eq[relator_eq] = sum.rel_eq
1.17 +lemmas sum_rel_mono[relator_mono] = sum.rel_mono
1.18
1.19  lemma sum_rel_OO[relator_distr]:
1.20    "(sum_rel A B) OO (sum_rel C D) = sum_rel (A OO C) (B OO D)"
1.21 -by (rule ext)+ (auto simp add: sum_rel_def OO_def split_sum_ex split: sum.split)
1.22 +  by (rule ext)+ (auto simp add: sum_rel_def OO_def split_sum_ex split: sum.split)
1.23
1.24  lemma Domainp_sum[relator_domain]:
1.25    assumes "Domainp R1 = P1"
1.26 @@ -94,4 +87,3 @@
1.27  end
1.28
1.29  end
1.30 -
```