src/HOL/HOLCF/Tutorial/New_Domain.thy
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 40497 src/HOLCF/Tutorial/New_Domain.thy@d2e876d6da8c
child 42151 4da4fc77664b
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
     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   UPDATE: The definitional back-end is now the default mode of the domain
    13   package. This file should be merged with @{text Domain_ex.thy}.
    14 *}
    15 
    16 text {*
    17   Provided that @{text domain} is the default sort, the @{text new_domain}
    18   package should work with any type definition supported by the old
    19   domain package.
    20 *}
    21 
    22 domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
    23 
    24 text {*
    25   The difference is that the new domain package is completely
    26   definitional, and does not generate any axioms.  The following type
    27   and constant definitions are not produced by the old domain package.
    28 *}
    29 
    30 thm type_definition_llist
    31 thm llist_abs_def llist_rep_def
    32 
    33 text {*
    34   The new domain package also adds support for indirect recursion with
    35   user-defined datatypes.  This definition of a tree datatype uses
    36   indirect recursion through the lazy list type constructor.
    37 *}
    38 
    39 domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
    40 
    41 text {*
    42   For indirect-recursive definitions, the domain package is not able to
    43   generate a high-level induction rule.  (It produces a warning
    44   message instead.)  The low-level reach lemma (now proved as a
    45   theorem, no longer generated as an axiom) can be used to derive
    46   other induction rules.
    47 *}
    48 
    49 thm ltree.reach
    50 
    51 text {*
    52   The definition of the take function uses map functions associated with
    53   each type constructor involved in the definition.  A map function
    54   for the lazy list type has been generated by the new domain package.
    55 *}
    56 
    57 thm ltree.take_rews
    58 thm llist_map_def
    59 
    60 lemma ltree_induct:
    61   fixes P :: "'a ltree \<Rightarrow> bool"
    62   assumes adm: "adm P"
    63   assumes bot: "P \<bottom>"
    64   assumes Leaf: "\<And>x. P (Leaf\<cdot>x)"
    65   assumes Branch: "\<And>f l. \<forall>x. P (f\<cdot>x) \<Longrightarrow> P (Branch\<cdot>(llist_map\<cdot>f\<cdot>l))"
    66   shows "P x"
    67 proof -
    68   have "P (\<Squnion>i. ltree_take i\<cdot>x)"
    69   using adm
    70   proof (rule admD)
    71     fix i
    72     show "P (ltree_take i\<cdot>x)"
    73     proof (induct i arbitrary: x)
    74       case (0 x)
    75       show "P (ltree_take 0\<cdot>x)" by (simp add: bot)
    76     next
    77       case (Suc n x)
    78       show "P (ltree_take (Suc n)\<cdot>x)"
    79         apply (cases x)
    80         apply (simp add: bot)
    81         apply (simp add: Leaf)
    82         apply (simp add: Branch Suc)
    83         done
    84     qed
    85   qed (simp add: ltree.chain_take)
    86   thus ?thesis
    87     by (simp add: ltree.reach)
    88 qed
    89 
    90 end