1(*  Title:      HOL/HOLCF/Tutorial/New_Domain.thy
2    Author:     Brian Huffman
3*)
4
5section \<open>Definitional domain package\<close>
6
7theory New_Domain
8imports HOLCF
9begin
10
11text \<open>
12  UPDATE: The definitional back-end is now the default mode of the domain
13  package. This file should be merged with \<open>Domain_ex.thy\<close>.
14\<close>
15
16text \<open>
17  Provided that \<open>domain\<close> is the default sort, the \<open>new_domain\<close>
18  package should work with any type definition supported by the old
19  domain package.
20\<close>
21
22domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
23
24text \<open>
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\<close>
29
30thm type_definition_llist
31thm llist_abs_def llist_rep_def
32
33text \<open>
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\<close>
38
39domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
40
41text \<open>
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\<close>
48
49thm ltree.reach
50
51text \<open>
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\<close>
56
57thm ltree.take_rews
58thm llist_map_def
59
60lemma 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"
67proof -
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)
88qed
89
90end
91