src/HOL/ex/Transfer_Int_Nat.thy
changeset 55938 f20d1db5aa3c
parent 53013 3fbcfa911863
child 55945 e96383acecf9
     1.1 --- a/src/HOL/ex/Transfer_Int_Nat.thy	Thu Mar 06 14:25:55 2014 +0100
     1.2 +++ b/src/HOL/ex/Transfer_Int_Nat.thy	Thu Mar 06 14:57:14 2014 +0100
     1.3 @@ -96,19 +96,19 @@
     1.4    unfolding fun_rel_def ZN_def by (simp add: transfer_int_nat_gcd)
     1.5  
     1.6  lemma ZN_atMost [transfer_rule]:
     1.7 -  "(ZN ===> set_rel ZN) (atLeastAtMost 0) atMost"
     1.8 -  unfolding fun_rel_def ZN_def set_rel_def
     1.9 +  "(ZN ===> rel_set ZN) (atLeastAtMost 0) atMost"
    1.10 +  unfolding fun_rel_def ZN_def rel_set_def
    1.11    by (clarsimp simp add: Bex_def, arith)
    1.12  
    1.13  lemma ZN_atLeastAtMost [transfer_rule]:
    1.14 -  "(ZN ===> ZN ===> set_rel ZN) atLeastAtMost atLeastAtMost"
    1.15 -  unfolding fun_rel_def ZN_def set_rel_def
    1.16 +  "(ZN ===> ZN ===> rel_set ZN) atLeastAtMost atLeastAtMost"
    1.17 +  unfolding fun_rel_def ZN_def rel_set_def
    1.18    by (clarsimp simp add: Bex_def, arith)
    1.19  
    1.20  lemma ZN_setsum [transfer_rule]:
    1.21 -  "bi_unique A \<Longrightarrow> ((A ===> ZN) ===> set_rel A ===> ZN) setsum setsum"
    1.22 +  "bi_unique A \<Longrightarrow> ((A ===> ZN) ===> rel_set A ===> ZN) setsum setsum"
    1.23    apply (intro fun_relI)
    1.24 -  apply (erule (1) bi_unique_set_rel_lemma)
    1.25 +  apply (erule (1) bi_unique_rel_set_lemma)
    1.26    apply (simp add: setsum.reindex int_setsum ZN_def fun_rel_def)
    1.27    apply (rule setsum_cong2, simp)
    1.28    done