--- a/src/HOLCF/ex/New_Domain.thy Mon Mar 01 23:54:50 2010 -0800
+++ b/src/HOLCF/ex/New_Domain.thy Tue Mar 02 00:34:26 2010 -0800
@@ -51,12 +51,12 @@
thm ltree.reach
text {*
- The definition of the copy function uses map functions associated with
+ The definition of the take function uses map functions associated with
each type constructor involved in the definition. A map function
for the lazy list type has been generated by the new domain package.
*}
-thm ltree.copy_def
+thm ltree.take_rews
thm llist_map_def
lemma ltree_induct:
@@ -67,24 +67,24 @@
assumes Branch: "\<And>f l. \<forall>x. P (f\<cdot>x) \<Longrightarrow> P (Branch\<cdot>(llist_map\<cdot>f\<cdot>l))"
shows "P x"
proof -
- have "\<forall>x. P (fix\<cdot>ltree_copy\<cdot>x)"
- proof (rule fix_ind)
- show "adm (\<lambda>a. \<forall>x. P (a\<cdot>x))"
- by (simp add: adm_subst [OF _ adm])
- next
- show "\<forall>x. P (\<bottom>\<cdot>x)"
- by (simp add: bot)
- next
- fix f :: "'a ltree \<rightarrow> 'a ltree"
- assume f: "\<forall>x. P (f\<cdot>x)"
- show "\<forall>x. P (ltree_copy\<cdot>f\<cdot>x)"
- apply (rule allI)
- apply (case_tac x)
- apply (simp add: bot)
- apply (simp add: Leaf)
- apply (simp add: Branch [OF f])
- done
- qed
+ have "P (\<Squnion>i. ltree_take i\<cdot>x)"
+ using adm
+ proof (rule admD)
+ fix i
+ show "P (ltree_take i\<cdot>x)"
+ proof (induct i arbitrary: x)
+ case (0 x)
+ show "P (ltree_take 0\<cdot>x)" by (simp add: bot)
+ next
+ case (Suc n x)
+ show "P (ltree_take (Suc n)\<cdot>x)"
+ apply (cases x)
+ apply (simp add: bot)
+ apply (simp add: Leaf)
+ apply (simp add: Branch Suc)
+ done
+ qed
+ qed (simp add: ltree.chain_take)
thus ?thesis
by (simp add: ltree.reach)
qed