--- a/src/HOLCF/IsaMakefile Thu Nov 19 23:15:24 2009 -0800
+++ b/src/HOLCF/IsaMakefile Fri Nov 20 00:06:04 2009 -0800
@@ -100,6 +100,7 @@
ex/Focus_ex.thy \
ex/Hoare.thy \
ex/Loop.thy \
+ ex/New_Domain.thy \
ex/Powerdomain_ex.thy \
ex/Stream.thy \
ex/ROOT.ML
--- /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
--- a/src/HOLCF/ex/ROOT.ML Thu Nov 19 23:15:24 2009 -0800
+++ b/src/HOLCF/ex/ROOT.ML Fri Nov 20 00:06:04 2009 -0800
@@ -4,4 +4,5 @@
*)
use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
- "Loop", "Fixrec_ex", "Powerdomain_ex", "Domain_ex", "Domain_Proofs"];
+ "Loop", "Fixrec_ex", "Powerdomain_ex", "Domain_ex", "Domain_Proofs",
+ "New_Domain"];