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 -