1(*  Title:      HOL/HOLCF/Tutorial/Domain_ex.thy
2    Author:     Brian Huffman
3*)
4
5section \<open>Domain package examples\<close>
6
7theory Domain_ex
8imports HOLCF
9begin
10
11text \<open>Domain constructors are strict by default.\<close>
12
13domain d1 = d1a | d1b "d1" "d1"
14
15lemma "d1b\<cdot>\<bottom>\<cdot>y = \<bottom>" by simp
16
17text \<open>Constructors can be made lazy using the \<open>lazy\<close> keyword.\<close>
18
19domain d2 = d2a | d2b (lazy "d2")
20
21lemma "d2b\<cdot>x \<noteq> \<bottom>" by simp
22
23text \<open>Strict and lazy arguments may be mixed arbitrarily.\<close>
24
25domain d3 = d3a | d3b (lazy "d2") "d2"
26
27lemma "P (d3b\<cdot>x\<cdot>y = \<bottom>) \<longleftrightarrow> P (y = \<bottom>)" by simp
28
29text \<open>Selectors can be used with strict or lazy constructor arguments.\<close>
30
31domain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2")
32
33lemma "y \<noteq> \<bottom> \<Longrightarrow> d4b_left\<cdot>(d4b\<cdot>x\<cdot>y) = x" by simp
34
35text \<open>Mixfix declarations can be given for data constructors.\<close>
36
37domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70)
38
39lemma "d5a \<noteq> x :#: y :#: z" by simp
40
41text \<open>Mixfix declarations can also be given for type constructors.\<close>
42
43domain ('a, 'b) lazypair (infixl ":*:" 25) =
44  lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75)
45
46lemma "\<forall>p::('a :*: 'b). p \<sqsubseteq> lfst\<cdot>p :*: lsnd\<cdot>p"
47by (rule allI, case_tac p, simp_all)
48
49text \<open>Non-recursive constructor arguments can have arbitrary types.\<close>
50
51domain ('a, 'b) d6 = d6 "int lift" "'a \<oplus> 'b u" (lazy "('a :*: 'b) \<times> ('b \<rightarrow> 'a)")
52
53text \<open>
54  Indirect recusion is allowed for sums, products, lifting, and the
55  continuous function space.  However, the domain package does not
56  generate an induction rule in terms of the constructors.
57\<close>
58
59domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a")
60  \<comment> \<open>Indirect recursion detected, skipping proofs of (co)induction rules\<close>
61
62text \<open>Note that \<open>d7.induct\<close> is absent.\<close>
63
64text \<open>
65  Indirect recursion is also allowed using previously-defined datatypes.
66\<close>
67
68domain 'a slist = SNil | SCons 'a "'a slist"
69
70domain 'a stree = STip | SBranch "'a stree slist"
71
72text \<open>Mutually-recursive datatypes can be defined using the \<open>and\<close> keyword.\<close>
73
74domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8")
75
76text \<open>Non-regular recursion is not allowed.\<close>
77(*
78domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist"
79  -- "illegal direct recursion with different arguments"
80domain 'a nest = Nest1 'a | Nest2 "'a nest nest"
81  -- "illegal direct recursion with different arguments"
82*)
83
84text \<open>
85  Mutually-recursive datatypes must have all the same type arguments,
86  not necessarily in the same order.
87\<close>
88
89domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2"
90   and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1"
91
92text \<open>Induction rules for flat datatypes have no admissibility side-condition.\<close>
93
94domain 'a flattree = Tip | Branch "'a flattree" "'a flattree"
95
96lemma "\<lbrakk>P \<bottom>; P Tip; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; P x; P y\<rbrakk> \<Longrightarrow> P (Branch\<cdot>x\<cdot>y)\<rbrakk> \<Longrightarrow> P x"
97by (rule flattree.induct) \<comment> \<open>no admissibility requirement\<close>
98
99text \<open>Trivial datatypes will produce a warning message.\<close>
100
101domain triv = Triv triv triv
102  \<comment> \<open>domain \<open>Domain_ex.triv\<close> is empty!\<close>
103
104lemma "(x::triv) = \<bottom>" by (induct x, simp_all)
105
106text \<open>Lazy constructor arguments may have unpointed types.\<close>
107
108domain natlist = nnil | ncons (lazy "nat discr") natlist
109
110text \<open>Class constraints may be given for type parameters on the LHS.\<close>
111
112domain ('a::predomain) box = Box (lazy 'a)
113
114domain ('a::countable) stream = snil | scons (lazy "'a discr") "'a stream"
115
116
117subsection \<open>Generated constants and theorems\<close>
118
119domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree")
120
121lemmas tree_abs_bottom_iff =
122  iso.abs_bottom_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
123
124text \<open>Rules about ismorphism\<close>
125term tree_rep
126term tree_abs
127thm tree.rep_iso
128thm tree.abs_iso
129thm tree.iso_rews
130
131text \<open>Rules about constructors\<close>
132term Leaf
133term Node
134thm Leaf_def Node_def
135thm tree.nchotomy
136thm tree.exhaust
137thm tree.compacts
138thm tree.con_rews
139thm tree.dist_les
140thm tree.dist_eqs
141thm tree.inverts
142thm tree.injects
143
144text \<open>Rules about case combinator\<close>
145term tree_case
146thm tree.tree_case_def
147thm tree.case_rews
148
149text \<open>Rules about selectors\<close>
150term left
151term right
152thm tree.sel_rews
153
154text \<open>Rules about discriminators\<close>
155term is_Leaf
156term is_Node
157thm tree.dis_rews
158
159text \<open>Rules about monadic pattern match combinators\<close>
160term match_Leaf
161term match_Node
162thm tree.match_rews
163
164text \<open>Rules about take function\<close>
165term tree_take
166thm tree.take_def
167thm tree.take_0
168thm tree.take_Suc
169thm tree.take_rews
170thm tree.chain_take
171thm tree.take_take
172thm tree.deflation_take
173thm tree.take_below
174thm tree.take_lemma
175thm tree.lub_take
176thm tree.reach
177thm tree.finite_induct
178
179text \<open>Rules about finiteness predicate\<close>
180term tree_finite
181thm tree.finite_def
182thm tree.finite (* only generated for flat datatypes *)
183
184text \<open>Rules about bisimulation predicate\<close>
185term tree_bisim
186thm tree.bisim_def
187thm tree.coinduct
188
189text \<open>Induction rule\<close>
190thm tree.induct
191
192
193subsection \<open>Known bugs\<close>
194
195text \<open>Declaring a mixfix with spaces causes some strange parse errors.\<close>
196(*
197domain xx = xx ("x y")
198  -- "Inner syntax error: unexpected end of input"
199*)
200
201end
202