Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Coercion_Examples.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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 *)

abbreviation nat_of_bool :: "bool \ nat"
where
  "nat_of_bool \ of_bool"

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_prod :: "('a \ 'c) \ ('b \ 'd) \ ('a * 'b) \ ('c * 'd)" where
"map_prod f g (x,y) = (f x, g y)"

declare [[coercion_map map_prod]]

(* Examples taken from the haskell draft implementation *)

term "(1::nat) = True"

term "True = (1::nat)"

term "(1::nat) = (True = (1::nat))"

term "(=) (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]]]]]"

typedecl ('a, 'b, 'c) F
consts Fmap :: "('a \ 'd) \ ('a, 'b, 'c) F \ ('d, 'b, 'c) F"
consts z :: "(bool, nat, bool) F"
declare [[coercion_map "Fmap :: ('a \ 'd) \ ('a, 'b, 'c) F \ ('d, 'b, 'c) F"]]
term "z :: (nat, nat, bool) F"

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

¤ Dauer der Verarbeitung: 0.31 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.