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