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