1(*  Title:      HOL/ex/Coercion_Examples.thy
2    Author:     Dmitriy Traytel, TU Muenchen
3
4Examples for coercive subtyping via subtype constraints.
5*)
6
7theory Coercion_Examples
8imports Main
9begin
10
11declare[[coercion_enabled]]
12
13(* Error messages test *)
14
15consts func :: "(nat \<Rightarrow> int) \<Rightarrow> nat"
16consts arg :: "int \<Rightarrow> nat"
17(* Invariant arguments
18term "func arg"
19*)
20(* No subtype relation - constraint
21term "(1::nat)::int"
22*)
23consts func' :: "int \<Rightarrow> int"
24consts arg' :: "nat"
25(* No subtype relation - function application
26term "func' arg'"
27*)
28(* Uncomparable types in bound
29term "arg' = True"
30*)
31(* Unfullfilled type class requirement
32term "1 = True"
33*)
34(* Different constructors
35term "[1::int] = func"
36*)
37
38(* Coercion/type maps definitions *)
39
40abbreviation nat_of_bool :: "bool \<Rightarrow> nat"
41where
42  "nat_of_bool \<equiv> of_bool"
43
44declare [[coercion nat_of_bool]]
45
46declare [[coercion int]]
47
48declare [[coercion_map map]]
49
50definition map_fun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'd)" where
51 "map_fun f g h = g o h o f"
52
53declare [[coercion_map "\<lambda> f g h . g o h o f"]]
54
55primrec map_prod :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a * 'b) \<Rightarrow> ('c * 'd)" where
56 "map_prod f g (x,y) = (f x, g y)"
57
58declare [[coercion_map map_prod]]
59
60(* Examples taken from the haskell draft implementation *)
61
62term "(1::nat) = True"
63
64term "True = (1::nat)"
65
66term "(1::nat) = (True = (1::nat))"
67
68term "(=) (True = (1::nat))"
69
70term "[1::nat,True]"
71
72term "[True,1::nat]"
73
74term "[1::nat] = [True]"
75
76term "[True] = [1::nat]"
77
78term "[[True]] = [[1::nat]]"
79
80term "[[[[[[[[[[True]]]]]]]]]] = [[[[[[[[[[1::nat]]]]]]]]]]"
81
82term "[[True],[42::nat]] = rev [[True]]"
83
84term "rev [10000::nat] = [False, 420000::nat, True]"
85
86term "\<lambda> x . x = (3::nat)"
87
88term "(\<lambda> x . x = (3::nat)) True"
89
90term "map (\<lambda> x . x = (3::nat))"
91
92term "map (\<lambda> x . x = (3::nat)) [True,1::nat]"
93
94consts bnn :: "(bool \<Rightarrow> nat) \<Rightarrow> nat"
95consts nb :: "nat \<Rightarrow> bool"
96consts ab :: "'a \<Rightarrow> bool"
97
98term "bnn nb"
99
100term "bnn ab"
101
102term "\<lambda> x . x = (3::int)"
103
104term "map (\<lambda> x . x = (3::int)) [True]"
105
106term "map (\<lambda> x . x = (3::int)) [True,1::nat]"
107
108term "map (\<lambda> x . x = (3::int)) [True,1::nat,1::int]"
109
110term "[1::nat,True,1::int,False]"
111
112term "map (map (\<lambda> x . x = (3::int))) [[True],[1::nat],[True,1::int]]"
113
114consts cbool :: "'a \<Rightarrow> bool"
115consts cnat :: "'a \<Rightarrow> nat"
116consts cint :: "'a \<Rightarrow> int"
117
118term "[id, cbool, cnat, cint]"
119
120consts funfun :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
121consts flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c"
122
123term "flip funfun"
124
125term "map funfun [id,cnat,cint,cbool]"
126
127term "map (flip funfun True)"
128
129term "map (flip funfun True) [id,cnat,cint,cbool]"
130
131consts ii :: "int \<Rightarrow> int"
132consts aaa :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
133consts nlist :: "nat list"
134consts ilil :: "int list \<Rightarrow> int list"
135
136term "ii (aaa (1::nat) True)"
137
138term "map ii nlist"
139
140term "ilil nlist"
141
142(***************************************************)
143
144(* Other examples *)
145
146definition xs :: "bool list" where "xs = [True]"
147
148term "(xs::nat list)"
149
150term "(1::nat) = True"
151
152term "True = (1::nat)"
153
154term "int (1::nat)"
155
156term "((True::nat)::int)"
157
158term "1::nat"
159
160term "nat 1"
161
162definition C :: nat
163where "C = 123"
164
165consts g :: "int \<Rightarrow> int"
166consts h :: "nat \<Rightarrow> nat"
167
168term "(g (1::nat)) + (h 2)"
169
170term "g 1"
171
172term "1+(1::nat)"
173
174term "((1::int) + (1::nat),(1::int))"
175
176definition ys :: "bool list list list list list" where "ys=[[[[[True]]]]]"
177
178term "ys=[[[[[1::nat]]]]]"
179
180typedecl ('a, 'b, 'c) F
181consts Fmap :: "('a \<Rightarrow> 'd) \<Rightarrow> ('a, 'b, 'c) F \<Rightarrow> ('d, 'b, 'c) F"
182consts z :: "(bool, nat, bool) F"
183declare [[coercion_map "Fmap :: ('a \<Rightarrow> 'd) \<Rightarrow> ('a, 'b, 'c) F \<Rightarrow> ('d, 'b, 'c) F"]]
184term "z :: (nat, nat, bool) F"
185
186consts
187  case_nil :: "'a \<Rightarrow> 'b"
188  case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
189  case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
190  case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
191
192declare [[coercion_args case_cons - -]]
193declare [[coercion_args case_abs -]]
194declare [[coercion_args case_elem - +]]
195
196term "case_cons (case_abs (\<lambda>n. case_abs (\<lambda>is. case_elem (((n::nat),(is::int list))) (n#is)))) case_nil"
197
198consts n :: nat m :: nat
199term "- (n + m)"
200declare [[coercion_args uminus -]]
201declare [[coercion_args plus + +]]
202term "- (n + m)"
203
204end
205