src/HOLCF/Tutorial/New_Domain.thy
changeset 37000 41a22e7c1145
parent 36452 d37c6eed8117
child 39974 b525988432e9
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/Tutorial/New_Domain.thy	Wed May 19 17:01:07 2010 -0700
     1.3 @@ -0,0 +1,92 @@
     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 +  The definitional domain package only works with representable domains,
    1.16 +  i.e. types in class @{text rep}.
    1.17 +*}
    1.18 +
    1.19 +default_sort rep
    1.20 +
    1.21 +text {*
    1.22 +  Provided that @{text rep} is the default sort, the @{text new_domain}
    1.23 +  package should work with any type definition supported by the old
    1.24 +  domain package.
    1.25 +*}
    1.26 +
    1.27 +new_domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
    1.28 +
    1.29 +text {*
    1.30 +  The difference is that the new domain package is completely
    1.31 +  definitional, and does not generate any axioms.  The following type
    1.32 +  and constant definitions are not produced by the old domain package.
    1.33 +*}
    1.34 +
    1.35 +thm type_definition_llist
    1.36 +thm llist_abs_def llist_rep_def
    1.37 +
    1.38 +text {*
    1.39 +  The new domain package also adds support for indirect recursion with
    1.40 +  user-defined datatypes.  This definition of a tree datatype uses
    1.41 +  indirect recursion through the lazy list type constructor.
    1.42 +*}
    1.43 +
    1.44 +new_domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
    1.45 +
    1.46 +text {*
    1.47 +  For indirect-recursive definitions, the domain package is not able to
    1.48 +  generate a high-level induction rule.  (It produces a warning
    1.49 +  message instead.)  The low-level reach lemma (now proved as a
    1.50 +  theorem, no longer generated as an axiom) can be used to derive
    1.51 +  other induction rules.
    1.52 +*}
    1.53 +
    1.54 +thm ltree.reach
    1.55 +
    1.56 +text {*
    1.57 +  The definition of the take function uses map functions associated with
    1.58 +  each type constructor involved in the definition.  A map function
    1.59 +  for the lazy list type has been generated by the new domain package.
    1.60 +*}
    1.61 +
    1.62 +thm ltree.take_rews
    1.63 +thm llist_map_def
    1.64 +
    1.65 +lemma ltree_induct:
    1.66 +  fixes P :: "'a ltree \<Rightarrow> bool"
    1.67 +  assumes adm: "adm P"
    1.68 +  assumes bot: "P \<bottom>"
    1.69 +  assumes Leaf: "\<And>x. P (Leaf\<cdot>x)"
    1.70 +  assumes Branch: "\<And>f l. \<forall>x. P (f\<cdot>x) \<Longrightarrow> P (Branch\<cdot>(llist_map\<cdot>f\<cdot>l))"
    1.71 +  shows "P x"
    1.72 +proof -
    1.73 +  have "P (\<Squnion>i. ltree_take i\<cdot>x)"
    1.74 +  using adm
    1.75 +  proof (rule admD)
    1.76 +    fix i
    1.77 +    show "P (ltree_take i\<cdot>x)"
    1.78 +    proof (induct i arbitrary: x)
    1.79 +      case (0 x)
    1.80 +      show "P (ltree_take 0\<cdot>x)" by (simp add: bot)
    1.81 +    next
    1.82 +      case (Suc n x)
    1.83 +      show "P (ltree_take (Suc n)\<cdot>x)"
    1.84 +        apply (cases x)
    1.85 +        apply (simp add: bot)
    1.86 +        apply (simp add: Leaf)
    1.87 +        apply (simp add: Branch Suc)
    1.88 +        done
    1.89 +    qed
    1.90 +  qed (simp add: ltree.chain_take)
    1.91 +  thus ?thesis
    1.92 +    by (simp add: ltree.reach)
    1.93 +qed
    1.94 +
    1.95 +end