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