src/HOLCF/Tutorial/New_Domain.thy
author huffman
Wed Oct 06 10:49:27 2010 -0700 (2010-10-06)
changeset 39974 b525988432e9
parent 37000 41a22e7c1145
child 39986 38677db30cad
permissions -rw-r--r--
major reorganization/simplification of HOLCF type classes:
removed profinite/bifinite classes and approx function;
universal domain uses approx_chain locale instead of bifinite class;
ideal_completion locale does not use 'take' functions, requires countable basis instead;
replaced type 'udom alg_defl' with type 'sfp';
replaced class 'rep' with class 'sfp';
renamed REP('a) to SFP('a);
     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 SFP domains,
    13   i.e. types in class @{text sfp}.
    14 *}
    15 
    16 default_sort sfp
    17 
    18 text {*
    19   Provided that @{text sfp} 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