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