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