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