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