# HG changeset patch
# User huffman
# Date 1258704364 28800
# Node ID 0bc8d4f786bd57ad98107f950fb35de422ff6797
# Parent  10c335383c8bee4c2a390134bd6e2bf065a0777b
example theory for new domain package

diff -r 10c335383c8b -r 0bc8d4f786bd src/HOLCF/IsaMakefile
--- 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
diff -r 10c335383c8b -r 0bc8d4f786bd src/HOLCF/ex/New_Domain.thy
--- /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
diff -r 10c335383c8b -r 0bc8d4f786bd src/HOLCF/ex/ROOT.ML
--- 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"];