src/HOLCF/ex/New_Domain.thy

move some powerdomain stuff into a new file

(*  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