(* Title: HOL/ex/Coercion_Examples.thy Author: Dmitriy Traytel, TU Muenchen Examples for coercive subtyping via subtype constraints. *) theory Coercion_Examples imports Main begin declare[[coercion_enabled]] (* Error messages test *) consts func :: "(nat \ int) \ nat" consts arg :: "int \ nat" (* Invariant arguments term "func arg" *) (* No subtype relation - constraint term "(1::nat)::int" *) consts func' :: "int \ int" consts arg' :: "nat" (* No subtype relation - function application term "func' arg'" *) (* Uncomparable types in bound term "arg' = True" *) (* Unfullfilled type class requirement term "1 = True" *) (* Different constructors term "[1::int] = func" *) (* Coercion/type maps definitions *) primrec nat_of_bool :: "bool \ nat" where "nat_of_bool False = 0" | "nat_of_bool True = 1" declare [[coercion nat_of_bool]] declare [[coercion int]] declare [[coercion_map map]] definition map_fun :: "('a \ 'b) \ ('c \ 'd) \ ('b \ 'c) \ ('a \ 'd)" where "map_fun f g h = g o h o f" declare [[coercion_map "\ f g h . g o h o f"]] primrec map_pair :: "('a \ 'c) \ ('b \ 'd) \ ('a * 'b) \ ('c * 'd)" where "map_pair f g (x,y) = (f x, g y)" declare [[coercion_map map_pair]] (* Examples taken from the haskell draft implementation *) term "(1::nat) = True" term "True = (1::nat)" term "(1::nat) = (True = (1::nat))" term "op = (True = (1::nat))" term "[1::nat,True]" term "[True,1::nat]" term "[1::nat] = [True]" term "[True] = [1::nat]" term "[[True]] = [[1::nat]]" term "[[[[[[[[[[True]]]]]]]]]] = [[[[[[[[[[1::nat]]]]]]]]]]" term "[[True],[42::nat]] = rev [[True]]" term "rev [10000::nat] = [False, 420000::nat, True]" term "\ x . x = (3::nat)" term "(\ x . x = (3::nat)) True" term "map (\ x . x = (3::nat))" term "map (\ x . x = (3::nat)) [True,1::nat]" consts bnn :: "(bool \ nat) \ nat" consts nb :: "nat \ bool" consts ab :: "'a \ bool" term "bnn nb" term "bnn ab" term "\ x . x = (3::int)" term "map (\ x . x = (3::int)) [True]" term "map (\ x . x = (3::int)) [True,1::nat]" term "map (\ x . x = (3::int)) [True,1::nat,1::int]" term "[1::nat,True,1::int,False]" term "map (map (\ x . x = (3::int))) [[True],[1::nat],[True,1::int]]" consts cbool :: "'a \ bool" consts cnat :: "'a \ nat" consts cint :: "'a \ int" term "[id, cbool, cnat, cint]" consts funfun :: "('a \ 'b) \ 'a \ 'b" consts flip :: "('a \ 'b \ 'c) \ 'b \ 'a \ 'c" term "flip funfun" term "map funfun [id,cnat,cint,cbool]" term "map (flip funfun True)" term "map (flip funfun True) [id,cnat,cint,cbool]" consts ii :: "int \ int" consts aaa :: "'a \ 'a \ 'a" consts nlist :: "nat list" consts ilil :: "int list \ int list" term "ii (aaa (1::nat) True)" term "map ii nlist" term "ilil nlist" (***************************************************) (* Other examples *) definition xs :: "bool list" where "xs = [True]" term "(xs::nat list)" term "(1::nat) = True" term "True = (1::nat)" term "int (1::nat)" term "((True::nat)::int)" term "1::nat" term "nat 1" definition C :: nat where "C = 123" consts g :: "int \ int" consts h :: "nat \ nat" term "(g (1::nat)) + (h 2)" term "g 1" term "1+(1::nat)" term "((1::int) + (1::nat),(1::int))" definition ys :: "bool list list list list list" where "ys=[[[[[True]]]]]" term "ys=[[[[[1::nat]]]]]" consts case_nil :: "'a \ 'b" case_cons :: "('a \ 'b) \ ('a \ 'b) \ 'a \ 'b" case_abs :: "('c \ 'b) \ 'b" case_elem :: "'a \ 'b \ 'a \ 'b" declare [[coercion_args case_cons - -]] declare [[coercion_args case_abs -]] declare [[coercion_args case_elem - +]] term "case_cons (case_abs (\n. case_abs (\is. case_elem (((n::nat),(is::int list))) (n#is)))) case_nil" consts n :: nat m :: nat term "- (n + m)" declare [[coercion_args uminus -]] declare [[coercion_args plus + +]] term "- (n + m)" end