1 (* Title: HOL/HOLCF/Tutorial/Domain_ex.thy |
1 (* Title: HOL/HOLCF/Tutorial/Domain_ex.thy |
2 Author: Brian Huffman |
2 Author: Brian Huffman |
3 *) |
3 *) |
4 |
4 |
5 section {* Domain package examples *} |
5 section \<open>Domain package examples\<close> |
6 |
6 |
7 theory Domain_ex |
7 theory Domain_ex |
8 imports HOLCF |
8 imports HOLCF |
9 begin |
9 begin |
10 |
10 |
11 text {* Domain constructors are strict by default. *} |
11 text \<open>Domain constructors are strict by default.\<close> |
12 |
12 |
13 domain d1 = d1a | d1b "d1" "d1" |
13 domain d1 = d1a | d1b "d1" "d1" |
14 |
14 |
15 lemma "d1b\<cdot>\<bottom>\<cdot>y = \<bottom>" by simp |
15 lemma "d1b\<cdot>\<bottom>\<cdot>y = \<bottom>" by simp |
16 |
16 |
17 text {* Constructors can be made lazy using the @{text "lazy"} keyword. *} |
17 text \<open>Constructors can be made lazy using the \<open>lazy\<close> keyword.\<close> |
18 |
18 |
19 domain d2 = d2a | d2b (lazy "d2") |
19 domain d2 = d2a | d2b (lazy "d2") |
20 |
20 |
21 lemma "d2b\<cdot>x \<noteq> \<bottom>" by simp |
21 lemma "d2b\<cdot>x \<noteq> \<bottom>" by simp |
22 |
22 |
23 text {* Strict and lazy arguments may be mixed arbitrarily. *} |
23 text \<open>Strict and lazy arguments may be mixed arbitrarily.\<close> |
24 |
24 |
25 domain d3 = d3a | d3b (lazy "d2") "d2" |
25 domain d3 = d3a | d3b (lazy "d2") "d2" |
26 |
26 |
27 lemma "P (d3b\<cdot>x\<cdot>y = \<bottom>) \<longleftrightarrow> P (y = \<bottom>)" by simp |
27 lemma "P (d3b\<cdot>x\<cdot>y = \<bottom>) \<longleftrightarrow> P (y = \<bottom>)" by simp |
28 |
28 |
29 text {* Selectors can be used with strict or lazy constructor arguments. *} |
29 text \<open>Selectors can be used with strict or lazy constructor arguments.\<close> |
30 |
30 |
31 domain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2") |
31 domain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2") |
32 |
32 |
33 lemma "y \<noteq> \<bottom> \<Longrightarrow> d4b_left\<cdot>(d4b\<cdot>x\<cdot>y) = x" by simp |
33 lemma "y \<noteq> \<bottom> \<Longrightarrow> d4b_left\<cdot>(d4b\<cdot>x\<cdot>y) = x" by simp |
34 |
34 |
35 text {* Mixfix declarations can be given for data constructors. *} |
35 text \<open>Mixfix declarations can be given for data constructors.\<close> |
36 |
36 |
37 domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70) |
37 domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70) |
38 |
38 |
39 lemma "d5a \<noteq> x :#: y :#: z" by simp |
39 lemma "d5a \<noteq> x :#: y :#: z" by simp |
40 |
40 |
41 text {* Mixfix declarations can also be given for type constructors. *} |
41 text \<open>Mixfix declarations can also be given for type constructors.\<close> |
42 |
42 |
43 domain ('a, 'b) lazypair (infixl ":*:" 25) = |
43 domain ('a, 'b) lazypair (infixl ":*:" 25) = |
44 lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75) |
44 lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75) |
45 |
45 |
46 lemma "\<forall>p::('a :*: 'b). p \<sqsubseteq> lfst\<cdot>p :*: lsnd\<cdot>p" |
46 lemma "\<forall>p::('a :*: 'b). p \<sqsubseteq> lfst\<cdot>p :*: lsnd\<cdot>p" |
47 by (rule allI, case_tac p, simp_all) |
47 by (rule allI, case_tac p, simp_all) |
48 |
48 |
49 text {* Non-recursive constructor arguments can have arbitrary types. *} |
49 text \<open>Non-recursive constructor arguments can have arbitrary types.\<close> |
50 |
50 |
51 domain ('a, 'b) d6 = d6 "int lift" "'a \<oplus> 'b u" (lazy "('a :*: 'b) \<times> ('b \<rightarrow> 'a)") |
51 domain ('a, 'b) d6 = d6 "int lift" "'a \<oplus> 'b u" (lazy "('a :*: 'b) \<times> ('b \<rightarrow> 'a)") |
52 |
52 |
53 text {* |
53 text \<open> |
54 Indirect recusion is allowed for sums, products, lifting, and the |
54 Indirect recusion is allowed for sums, products, lifting, and the |
55 continuous function space. However, the domain package does not |
55 continuous function space. However, the domain package does not |
56 generate an induction rule in terms of the constructors. |
56 generate an induction rule in terms of the constructors. |
57 *} |
57 \<close> |
58 |
58 |
59 domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a") |
59 domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a") |
60 -- "Indirect recursion detected, skipping proofs of (co)induction rules" |
60 \<comment> "Indirect recursion detected, skipping proofs of (co)induction rules" |
61 |
61 |
62 text {* Note that @{text d7.induct} is absent. *} |
62 text \<open>Note that \<open>d7.induct\<close> is absent.\<close> |
63 |
63 |
64 text {* |
64 text \<open> |
65 Indirect recursion is also allowed using previously-defined datatypes. |
65 Indirect recursion is also allowed using previously-defined datatypes. |
66 *} |
66 \<close> |
67 |
67 |
68 domain 'a slist = SNil | SCons 'a "'a slist" |
68 domain 'a slist = SNil | SCons 'a "'a slist" |
69 |
69 |
70 domain 'a stree = STip | SBranch "'a stree slist" |
70 domain 'a stree = STip | SBranch "'a stree slist" |
71 |
71 |
72 text {* Mutually-recursive datatypes can be defined using the @{text "and"} keyword. *} |
72 text \<open>Mutually-recursive datatypes can be defined using the \<open>and\<close> keyword.\<close> |
73 |
73 |
74 domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8") |
74 domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8") |
75 |
75 |
76 text {* Non-regular recursion is not allowed. *} |
76 text \<open>Non-regular recursion is not allowed.\<close> |
77 (* |
77 (* |
78 domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist" |
78 domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist" |
79 -- "illegal direct recursion with different arguments" |
79 -- "illegal direct recursion with different arguments" |
80 domain 'a nest = Nest1 'a | Nest2 "'a nest nest" |
80 domain 'a nest = Nest1 'a | Nest2 "'a nest nest" |
81 -- "illegal direct recursion with different arguments" |
81 -- "illegal direct recursion with different arguments" |
82 *) |
82 *) |
83 |
83 |
84 text {* |
84 text \<open> |
85 Mutually-recursive datatypes must have all the same type arguments, |
85 Mutually-recursive datatypes must have all the same type arguments, |
86 not necessarily in the same order. |
86 not necessarily in the same order. |
87 *} |
87 \<close> |
88 |
88 |
89 domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2" |
89 domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2" |
90 and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1" |
90 and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1" |
91 |
91 |
92 text {* Induction rules for flat datatypes have no admissibility side-condition. *} |
92 text \<open>Induction rules for flat datatypes have no admissibility side-condition.\<close> |
93 |
93 |
94 domain 'a flattree = Tip | Branch "'a flattree" "'a flattree" |
94 domain 'a flattree = Tip | Branch "'a flattree" "'a flattree" |
95 |
95 |
96 lemma "\<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" |
96 lemma "\<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" |
97 by (rule flattree.induct) -- "no admissibility requirement" |
97 by (rule flattree.induct) \<comment> "no admissibility requirement" |
98 |
98 |
99 text {* Trivial datatypes will produce a warning message. *} |
99 text \<open>Trivial datatypes will produce a warning message.\<close> |
100 |
100 |
101 domain triv = Triv triv triv |
101 domain triv = Triv triv triv |
102 -- "domain @{text Domain_ex.triv} is empty!" |
102 \<comment> "domain \<open>Domain_ex.triv\<close> is empty!" |
103 |
103 |
104 lemma "(x::triv) = \<bottom>" by (induct x, simp_all) |
104 lemma "(x::triv) = \<bottom>" by (induct x, simp_all) |
105 |
105 |
106 text {* Lazy constructor arguments may have unpointed types. *} |
106 text \<open>Lazy constructor arguments may have unpointed types.\<close> |
107 |
107 |
108 domain natlist = nnil | ncons (lazy "nat discr") natlist |
108 domain natlist = nnil | ncons (lazy "nat discr") natlist |
109 |
109 |
110 text {* Class constraints may be given for type parameters on the LHS. *} |
110 text \<open>Class constraints may be given for type parameters on the LHS.\<close> |
111 |
111 |
112 domain ('a::predomain) box = Box (lazy 'a) |
112 domain ('a::predomain) box = Box (lazy 'a) |
113 |
113 |
114 domain ('a::countable) stream = snil | scons (lazy "'a discr") "'a stream" |
114 domain ('a::countable) stream = snil | scons (lazy "'a discr") "'a stream" |
115 |
115 |
116 |
116 |
117 subsection {* Generated constants and theorems *} |
117 subsection \<open>Generated constants and theorems\<close> |
118 |
118 |
119 domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree") |
119 domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree") |
120 |
120 |
121 lemmas tree_abs_bottom_iff = |
121 lemmas tree_abs_bottom_iff = |
122 iso.abs_bottom_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]] |
122 iso.abs_bottom_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]] |
123 |
123 |
124 text {* Rules about ismorphism *} |
124 text \<open>Rules about ismorphism\<close> |
125 term tree_rep |
125 term tree_rep |
126 term tree_abs |
126 term tree_abs |
127 thm tree.rep_iso |
127 thm tree.rep_iso |
128 thm tree.abs_iso |
128 thm tree.abs_iso |
129 thm tree.iso_rews |
129 thm tree.iso_rews |
130 |
130 |
131 text {* Rules about constructors *} |
131 text \<open>Rules about constructors\<close> |
132 term Leaf |
132 term Leaf |
133 term Node |
133 term Node |
134 thm Leaf_def Node_def |
134 thm Leaf_def Node_def |
135 thm tree.nchotomy |
135 thm tree.nchotomy |
136 thm tree.exhaust |
136 thm tree.exhaust |