src/HOL/HOLCF/ex/Domain_Proofs.thy
changeset 44066 d74182c93f04
parent 42151 4da4fc77664b
child 49759 ecf1d5d87e5e
equal deleted inserted replaced
44065:eb64ffccfc75 44066:d74182c93f04
   468 apply (simp only: map_apply_thms pair_collapse)
   468 apply (simp only: map_apply_thms pair_collapse)
   469 apply (simp only: fix_def2)
   469 apply (simp only: fix_def2)
   470 apply (rule lub_eq)
   470 apply (rule lub_eq)
   471 apply (rule nat.induct)
   471 apply (rule nat.induct)
   472 apply (simp only: iterate_0 Pair_strict take_0_thms)
   472 apply (simp only: iterate_0 Pair_strict take_0_thms)
   473 apply (simp only: iterate_Suc Pair_fst_snd_eq fst_conv snd_conv
   473 apply (simp only: iterate_Suc prod_eq_iff fst_conv snd_conv
   474                   foo_bar_baz_mapF_beta take_Suc_thms simp_thms)
   474                   foo_bar_baz_mapF_beta take_Suc_thms simp_thms)
   475 done
   475 done
   476 
   476 
   477 lemma lub_foo_take: "(\<Squnion>n. foo_take n) = ID"
   477 lemma lub_foo_take: "(\<Squnion>n. foo_take n) = ID"
   478 apply (rule trans [OF _ foo_map_ID])
   478 apply (rule trans [OF _ foo_map_ID])