src/HOL/HOLCF/Fix.thy
changeset 61424 c3658c18b7bc
parent 58880 0baae4311a9f
child 61998 b66d2ca1f907
     1.1 --- a/src/HOL/HOLCF/Fix.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/HOLCF/Fix.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -178,15 +178,15 @@
     1.4    assumes step: "\<And>x y. P x y \<Longrightarrow> P (F\<cdot>x) (G\<cdot>y)"
     1.5    shows "P (fix\<cdot>F) (fix\<cdot>G)"
     1.6  proof -
     1.7 -  from adm have adm': "adm (split P)"
     1.8 +  from adm have adm': "adm (case_prod P)"
     1.9      unfolding split_def .
    1.10    have "\<And>i. P (iterate i\<cdot>F\<cdot>\<bottom>) (iterate i\<cdot>G\<cdot>\<bottom>)"
    1.11      by (induct_tac i, simp add: base, simp add: step)
    1.12 -  hence "\<And>i. split P (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>)"
    1.13 +  hence "\<And>i. case_prod P (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>)"
    1.14      by simp
    1.15 -  hence "split P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
    1.16 +  hence "case_prod P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
    1.17      by - (rule admD [OF adm'], simp, assumption)
    1.18 -  hence "split P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
    1.19 +  hence "case_prod P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
    1.20      by (simp add: lub_Pair)
    1.21    hence "P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>) (\<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
    1.22      by simp