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

section ‹Definitional domain package›

theory New_Domain
imports HOLCF
begin

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

text ‹
 Provided that ‹domain› is the default sort, the ‹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 → bool"
  assumes adm: "adm P"
  assumes bot: "P ⊥"
  assumes Leaf: "∧x. P (Leaf⋅x)"
  assumes Branch: "∧f l. ∀x. P (f⋅x) ==> P (Branch⋅(llist_map⋅f⋅l))"
  shows "P x"
proof -
  have "P (⊔i. ltree_take i⋅x)"
  using adm
  proof (rule admD)
    fix i
    show "P (ltree_take i⋅x)"
    proof (induct i arbitrary: x)
      case (0 x)
      show "P (ltree_take 0⋅x)" by (simp add: bot)
    next
      case (Suc n x)
      show "P (ltree_take (Suc n)⋅x)"
        apply (cases x)
        apply (simp add: bot)
        apply (simp add: Leaf)
        apply (simp add: Branch Suc)
        done
    qed
  qed (simp add: ltree.chain_take)
  thus ?thesis
    by (simp add: ltree.reach)
qed

end