src/HOL/HOLCF/Tutorial/New_Domain.thy
changeset 40774 0437dbc127b3
parent 40497 d2e876d6da8c
child 42151 4da4fc77664b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/Tutorial/New_Domain.thy	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,90 @@
     1.4 +(*  Title:      HOLCF/ex/New_Domain.thy
     1.5 +    Author:     Brian Huffman
     1.6 +*)
     1.7 +
     1.8 +header {* Definitional domain package *}
     1.9 +
    1.10 +theory New_Domain
    1.11 +imports HOLCF
    1.12 +begin
    1.13 +
    1.14 +text {*
    1.15 +  UPDATE: The definitional back-end is now the default mode of the domain
    1.16 +  package. This file should be merged with @{text Domain_ex.thy}.
    1.17 +*}
    1.18 +
    1.19 +text {*
    1.20 +  Provided that @{text domain} is the default sort, the @{text new_domain}
    1.21 +  package should work with any type definition supported by the old
    1.22 +  domain package.
    1.23 +*}
    1.24 +
    1.25 +domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
    1.26 +
    1.27 +text {*
    1.28 +  The difference is that the new domain package is completely
    1.29 +  definitional, and does not generate any axioms.  The following type
    1.30 +  and constant definitions are not produced by the old domain package.
    1.31 +*}
    1.32 +
    1.33 +thm type_definition_llist
    1.34 +thm llist_abs_def llist_rep_def
    1.35 +
    1.36 +text {*
    1.37 +  The new domain package also adds support for indirect recursion with
    1.38 +  user-defined datatypes.  This definition of a tree datatype uses
    1.39 +  indirect recursion through the lazy list type constructor.
    1.40 +*}
    1.41 +
    1.42 +domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
    1.43 +
    1.44 +text {*
    1.45 +  For indirect-recursive definitions, the domain package is not able to
    1.46 +  generate a high-level induction rule.  (It produces a warning
    1.47 +  message instead.)  The low-level reach lemma (now proved as a
    1.48 +  theorem, no longer generated as an axiom) can be used to derive
    1.49 +  other induction rules.
    1.50 +*}
    1.51 +
    1.52 +thm ltree.reach
    1.53 +
    1.54 +text {*
    1.55 +  The definition of the take function uses map functions associated with
    1.56 +  each type constructor involved in the definition.  A map function
    1.57 +  for the lazy list type has been generated by the new domain package.
    1.58 +*}
    1.59 +
    1.60 +thm ltree.take_rews
    1.61 +thm llist_map_def
    1.62 +
    1.63 +lemma ltree_induct:
    1.64 +  fixes P :: "'a ltree \<Rightarrow> bool"
    1.65 +  assumes adm: "adm P"
    1.66 +  assumes bot: "P \<bottom>"
    1.67 +  assumes Leaf: "\<And>x. P (Leaf\<cdot>x)"
    1.68 +  assumes Branch: "\<And>f l. \<forall>x. P (f\<cdot>x) \<Longrightarrow> P (Branch\<cdot>(llist_map\<cdot>f\<cdot>l))"
    1.69 +  shows "P x"
    1.70 +proof -
    1.71 +  have "P (\<Squnion>i. ltree_take i\<cdot>x)"
    1.72 +  using adm
    1.73 +  proof (rule admD)
    1.74 +    fix i
    1.75 +    show "P (ltree_take i\<cdot>x)"
    1.76 +    proof (induct i arbitrary: x)
    1.77 +      case (0 x)
    1.78 +      show "P (ltree_take 0\<cdot>x)" by (simp add: bot)
    1.79 +    next
    1.80 +      case (Suc n x)
    1.81 +      show "P (ltree_take (Suc n)\<cdot>x)"
    1.82 +        apply (cases x)
    1.83 +        apply (simp add: bot)
    1.84 +        apply (simp add: Leaf)
    1.85 +        apply (simp add: Branch Suc)
    1.86 +        done
    1.87 +    qed
    1.88 +  qed (simp add: ltree.chain_take)
    1.89 +  thus ?thesis
    1.90 +    by (simp add: ltree.reach)
    1.91 +qed
    1.92 +
    1.93 +end