--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/New_Domain.thy Fri Nov 20 00:06:04 2009 -0800
@@ -0,0 +1,92 @@
+(* Title: HOLCF/ex/New_Domain.thy
+ Author: Brian Huffman
+*)
+
+header {* Definitional domain package *}
+
+theory New_Domain
+imports HOLCF
+begin
+
+text {*
+ The definitional domain package only works with representable domains,
+ i.e. types in class @{text rep}.
+*}
+
+defaultsort rep
+
+text {*
+ Provided that @{text rep} is the default sort, the @{text new_domain}
+ package should work with any type definition supported by the old
+ domain package.
+*}
+
+new_domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
+
+text {*
+ The difference is that the new domain package is completely
+ definitional, and does not generate any axioms. The following type
+ and constant definitions are not produced by the old domain package.
+*}
+
+thm type_definition_llist
+thm llist_abs_def llist_rep_def
+
+text {*
+ The new domain package also adds support for indirect recursion with
+ user-defined datatypes. This definition of a tree datatype uses
+ indirect recursion through the lazy list type constructor.
+*}
+
+new_domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
+
+text {*
+ For indirect-recursive definitions, the domain package is not able to
+ generate a high-level induction rule. (It produces a warning
+ message instead.) The low-level reach lemma (now proved as a
+ theorem, no longer generated as an axiom) can be used to derive
+ other induction rules.
+*}
+
+thm ltree.reach
+
+text {*
+ The definition of the copy 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 llist_map_def
+
+lemma ltree_induct:
+ fixes P :: "'a ltree \<Rightarrow> bool"
+ assumes adm: "adm P"
+ assumes bot: "P \<bottom>"
+ assumes Leaf: "\<And>x. P (Leaf\<cdot>x)"
+ 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
+ thus ?thesis
+ by (simp add: ltree.reach)
+qed
+
+end