src/HOLCF/Tutorial/New_Domain.thy
author huffman
Wed May 19 17:01:07 2010 -0700 (2010-05-19)
changeset 37000 41a22e7c1145
parent 36452 src/HOLCF/ex/New_Domain.thy@d37c6eed8117
child 39974 b525988432e9
permissions -rw-r--r--
move some example files into new HOLCF/Tutorial directory
     1 (*  Title:      HOLCF/ex/New_Domain.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 header {* Definitional domain package *}
     6 
     7 theory New_Domain
     8 imports HOLCF
     9 begin
    10 
    11 text {*
    12   The definitional domain package only works with representable domains,
    13   i.e. types in class @{text rep}.
    14 *}
    15 
    16 default_sort rep
    17 
    18 text {*
    19   Provided that @{text rep} is the default sort, the @{text new_domain}
    20   package should work with any type definition supported by the old
    21   domain package.
    22 *}
    23 
    24 new_domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
    25 
    26 text {*
    27   The difference is that the new domain package is completely
    28   definitional, and does not generate any axioms.  The following type
    29   and constant definitions are not produced by the old domain package.
    30 *}
    31 
    32 thm type_definition_llist
    33 thm llist_abs_def llist_rep_def
    34 
    35 text {*
    36   The new domain package also adds support for indirect recursion with
    37   user-defined datatypes.  This definition of a tree datatype uses
    38   indirect recursion through the lazy list type constructor.
    39 *}
    40 
    41 new_domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
    42 
    43 text {*
    44   For indirect-recursive definitions, the domain package is not able to
    45   generate a high-level induction rule.  (It produces a warning
    46   message instead.)  The low-level reach lemma (now proved as a
    47   theorem, no longer generated as an axiom) can be used to derive
    48   other induction rules.
    49 *}
    50 
    51 thm ltree.reach
    52 
    53 text {*
    54   The definition of the take function uses map functions associated with
    55   each type constructor involved in the definition.  A map function
    56   for the lazy list type has been generated by the new domain package.
    57 *}
    58 
    59 thm ltree.take_rews
    60 thm llist_map_def
    61 
    62 lemma ltree_induct:
    63   fixes P :: "'a ltree \<Rightarrow> bool"
    64   assumes adm: "adm P"
    65   assumes bot: "P \<bottom>"
    66   assumes Leaf: "\<And>x. P (Leaf\<cdot>x)"
    67   assumes Branch: "\<And>f l. \<forall>x. P (f\<cdot>x) \<Longrightarrow> P (Branch\<cdot>(llist_map\<cdot>f\<cdot>l))"
    68   shows "P x"
    69 proof -
    70   have "P (\<Squnion>i. ltree_take i\<cdot>x)"
    71   using adm
    72   proof (rule admD)
    73     fix i
    74     show "P (ltree_take i\<cdot>x)"
    75     proof (induct i arbitrary: x)
    76       case (0 x)
    77       show "P (ltree_take 0\<cdot>x)" by (simp add: bot)
    78     next
    79       case (Suc n x)
    80       show "P (ltree_take (Suc n)\<cdot>x)"
    81         apply (cases x)
    82         apply (simp add: bot)
    83         apply (simp add: Leaf)
    84         apply (simp add: Branch Suc)
    85         done
    86     qed
    87   qed (simp add: ltree.chain_take)
    88   thus ?thesis
    89     by (simp add: ltree.reach)
    90 qed
    91 
    92 end