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