src/HOLCF/Bifinite.thy
 changeset 35525 fa231b86cb1e parent 33808 31169fdc5ae7 child 37678 0040bafffdef
equal inserted replaced
35524:a2a59e92b02e 35525:fa231b86cb1e
`   293     by (rule finite_range_cfun_map)`
`   293     by (rule finite_range_cfun_map)`
`   294   thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"`
`   294   thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"`
`   295     by (rule finite_range_imp_finite_fixes)`
`   295     by (rule finite_range_imp_finite_fixes)`
`   296 qed`
`   296 qed`
`   297 `
`   297 `
`   298 instantiation "->" :: (profinite, profinite) profinite`
`   298 instantiation cfun :: (profinite, profinite) profinite`
`   299 begin`
`   299 begin`
`   300 `
`   300 `
`   301 definition`
`   301 definition`
`   302   approx_cfun_def:`
`   302   approx_cfun_def:`
`   303     "approx = (\<lambda>n. cfun_map\<cdot>(approx n)\<cdot>(approx n))"`
`   303     "approx = (\<lambda>n. cfun_map\<cdot>(approx n)\<cdot>(approx n))"`
`   323               finite_deflation_approx)`
`   323               finite_deflation_approx)`
`   324 qed`
`   324 qed`
`   325 `
`   325 `
`   326 end`
`   326 end`
`   327 `
`   327 `
`   328 instance "->" :: (profinite, bifinite) bifinite ..`
`   328 instance cfun :: (profinite, bifinite) bifinite ..`
`   329 `
`   329 `
`   330 lemma approx_cfun: "approx n\<cdot>f\<cdot>x = approx n\<cdot>(f\<cdot>(approx n\<cdot>x))"`
`   330 lemma approx_cfun: "approx n\<cdot>f\<cdot>x = approx n\<cdot>(f\<cdot>(approx n\<cdot>x))"`
`   331 by (simp add: approx_cfun_def)`
`   331 by (simp add: approx_cfun_def)`
`   332 `
`   332 `
`   333 end`
`   333 end`