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.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
```