|
1 theory Coercion_Examples |
|
2 imports Main |
|
3 uses "~~/src/Tools/subtyping.ML" |
|
4 begin |
|
5 |
|
6 (* Coercion/type maps definitions*) |
|
7 |
|
8 consts func :: "(nat \<Rightarrow> int) \<Rightarrow> nat" |
|
9 consts arg :: "int \<Rightarrow> nat" |
|
10 (* Invariant arguments |
|
11 term "func arg" |
|
12 *) |
|
13 (* No subtype relation - constraint |
|
14 term "(1::nat)::int" |
|
15 *) |
|
16 consts func' :: "int \<Rightarrow> int" |
|
17 consts arg' :: "nat" |
|
18 (* No subtype relation - function application |
|
19 term "func' arg'" |
|
20 *) |
|
21 (* Uncomparable types in bound |
|
22 term "arg' = True" |
|
23 *) |
|
24 (* Unfullfilled type class requirement |
|
25 term "1 = True" |
|
26 *) |
|
27 (* Different constructors |
|
28 term "[1::int] = func" |
|
29 *) |
|
30 |
|
31 primrec nat_of_bool :: "bool \<Rightarrow> nat" |
|
32 where |
|
33 "nat_of_bool False = 0" |
|
34 | "nat_of_bool True = 1" |
|
35 |
|
36 declare [[coercion nat_of_bool]] |
|
37 |
|
38 declare [[coercion int]] |
|
39 |
|
40 declare [[map_function map]] |
|
41 |
|
42 definition map_fun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'd)" where |
|
43 "map_fun f g h = g o h o f" |
|
44 |
|
45 declare [[map_function "\<lambda> f g h . g o h o f"]] |
|
46 |
|
47 primrec map_pair :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a * 'b) \<Rightarrow> ('c * 'd)" where |
|
48 "map_pair f g (x,y) = (f x, g y)" |
|
49 |
|
50 declare [[map_function map_pair]] |
|
51 |
|
52 (* Examples taken from the haskell draft implementation *) |
|
53 |
|
54 term "(1::nat) = True" |
|
55 |
|
56 term "True = (1::nat)" |
|
57 |
|
58 term "(1::nat) = (True = (1::nat))" |
|
59 |
|
60 term "op = (True = (1::nat))" |
|
61 |
|
62 term "[1::nat,True]" |
|
63 |
|
64 term "[True,1::nat]" |
|
65 |
|
66 term "[1::nat] = [True]" |
|
67 |
|
68 term "[True] = [1::nat]" |
|
69 |
|
70 term "[[True]] = [[1::nat]]" |
|
71 |
|
72 term "[[[[[[[[[[True]]]]]]]]]] = [[[[[[[[[[1::nat]]]]]]]]]]" |
|
73 |
|
74 term "[[True],[42::nat]] = rev [[True]]" |
|
75 |
|
76 term "rev [10000::nat] = [False, 420000::nat, True]" |
|
77 |
|
78 term "\<lambda> x . x = (3::nat)" |
|
79 |
|
80 term "(\<lambda> x . x = (3::nat)) True" |
|
81 |
|
82 term "map (\<lambda> x . x = (3::nat))" |
|
83 |
|
84 term "map (\<lambda> x . x = (3::nat)) [True,1::nat]" |
|
85 |
|
86 consts bnn :: "(bool \<Rightarrow> nat) \<Rightarrow> nat" |
|
87 consts nb :: "nat \<Rightarrow> bool" |
|
88 consts ab :: "'a \<Rightarrow> bool" |
|
89 |
|
90 term "bnn nb" |
|
91 |
|
92 term "bnn ab" |
|
93 |
|
94 term "\<lambda> x . x = (3::int)" |
|
95 |
|
96 term "map (\<lambda> x . x = (3::int)) [True]" |
|
97 |
|
98 term "map (\<lambda> x . x = (3::int)) [True,1::nat]" |
|
99 |
|
100 term "map (\<lambda> x . x = (3::int)) [True,1::nat,1::int]" |
|
101 |
|
102 term "[1::nat,True,1::int,False]" |
|
103 |
|
104 term "map (map (\<lambda> x . x = (3::int))) [[True],[1::nat],[True,1::int]]" |
|
105 |
|
106 consts cbool :: "'a \<Rightarrow> bool" |
|
107 consts cnat :: "'a \<Rightarrow> nat" |
|
108 consts cint :: "'a \<Rightarrow> int" |
|
109 |
|
110 term "[id, cbool, cnat, cint]" |
|
111 |
|
112 consts funfun :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
|
113 consts flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" |
|
114 |
|
115 term "flip funfun" |
|
116 |
|
117 term "map funfun [id,cnat,cint,cbool]" |
|
118 |
|
119 term "map (flip funfun True)" |
|
120 |
|
121 term "map (flip funfun True) [id,cnat,cint,cbool]" |
|
122 |
|
123 consts ii :: "int \<Rightarrow> int" |
|
124 consts aaa :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
125 consts nlist :: "nat list" |
|
126 consts ilil :: "int list \<Rightarrow> int list" |
|
127 |
|
128 term "ii (aaa (1::nat) True)" |
|
129 |
|
130 term "map ii nlist" |
|
131 |
|
132 term "ilil nlist" |
|
133 |
|
134 (***************************************************) |
|
135 |
|
136 (* Other examples *) |
|
137 |
|
138 definition xs :: "bool list" where "xs = [True]" |
|
139 |
|
140 term "(xs::nat list)" |
|
141 |
|
142 term "(1::nat) = True" |
|
143 |
|
144 term "True = (1::nat)" |
|
145 |
|
146 term "int (1::nat)" |
|
147 |
|
148 term "((True::nat)::int)" |
|
149 |
|
150 term "1::nat" |
|
151 |
|
152 term "nat 1" |
|
153 |
|
154 definition C :: nat |
|
155 where "C = 123" |
|
156 |
|
157 consts g :: "int \<Rightarrow> int" |
|
158 consts h :: "nat \<Rightarrow> nat" |
|
159 |
|
160 term "(g (1::nat)) + (h 2)" |
|
161 |
|
162 term "g 1" |
|
163 |
|
164 term "1+(1::nat)" |
|
165 |
|
166 term "((1::int) + (1::nat),(1::int))" |
|
167 |
|
168 definition ys :: "bool list list list list list" where "ys=[[[[[True]]]]]" |
|
169 |
|
170 term "ys=[[[[[1::nat]]]]]" |
|
171 |
|
172 end |