author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 42151 4da4fc77664b
child 58880 0baae4311a9f
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;

(*  Title:      HOL/HOLCF/Tutorial/New_Domain.thy
    Author:     Brian Huffman

header {* Definitional domain package *}

theory New_Domain
imports HOLCF

text {*
  UPDATE: The definitional back-end is now the default mode of the domain
  package. This file should be merged with @{text Domain_ex.thy}.

text {*
  Provided that @{text domain} is the default sort, the @{text new_domain}
  package should work with any type definition supported by the old
  domain package.

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.

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 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.take_rews
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 "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)
      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)
  qed (simp add: ltree.chain_take)
  thus ?thesis
    by (simp add: ltree.reach)