src/HOL/ex/Coercion_Examples.thy
author wenzelm
Thu, 30 May 2013 20:38:50 +0200
changeset 52252 81fcc11d8c65
parent 51335 6bac04a6a197
child 54438 82ef58dba83b
permissions -rw-r--r--
minor tuning -- more linebreaks;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
     1
(*  Title:      HOL/ex/Coercion_Examples.thy
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
     2
    Author:     Dmitriy Traytel, TU Muenchen
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
     3
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
     4
Examples for coercive subtyping via subtype constraints.
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
     5
*)
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
     6
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
     7
theory Coercion_Examples
51247
064683ba110c Coercion_Examples defines required coercions itself (no Complex_Main needed)
traytel
parents: 40839
diff changeset
     8
imports Main
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
     9
begin
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    10
51247
064683ba110c Coercion_Examples defines required coercions itself (no Complex_Main needed)
traytel
parents: 40839
diff changeset
    11
declare[[coercion_enabled]]
064683ba110c Coercion_Examples defines required coercions itself (no Complex_Main needed)
traytel
parents: 40839
diff changeset
    12
40297
c753e3f8b4d6 Attribute map_function -> coercion_map;
traytel
parents: 40283
diff changeset
    13
(* Error messages test *)
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    14
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    15
consts func :: "(nat \<Rightarrow> int) \<Rightarrow> nat"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    16
consts arg :: "int \<Rightarrow> nat"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    17
(* Invariant arguments
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    18
term "func arg"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    19
*)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    20
(* No subtype relation - constraint
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    21
term "(1::nat)::int"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    22
*)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    23
consts func' :: "int \<Rightarrow> int"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    24
consts arg' :: "nat"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    25
(* No subtype relation - function application
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    26
term "func' arg'"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    27
*)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    28
(* Uncomparable types in bound
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    29
term "arg' = True"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    30
*)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    31
(* Unfullfilled type class requirement
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    32
term "1 = True"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    33
*)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    34
(* Different constructors
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    35
term "[1::int] = func"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    36
*)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    37
40297
c753e3f8b4d6 Attribute map_function -> coercion_map;
traytel
parents: 40283
diff changeset
    38
(* Coercion/type maps definitions *)
c753e3f8b4d6 Attribute map_function -> coercion_map;
traytel
parents: 40283
diff changeset
    39
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    40
primrec nat_of_bool :: "bool \<Rightarrow> nat"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    41
where
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    42
  "nat_of_bool False = 0"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    43
| "nat_of_bool True = 1"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    44
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    45
declare [[coercion nat_of_bool]]
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    46
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    47
declare [[coercion int]]
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    48
40297
c753e3f8b4d6 Attribute map_function -> coercion_map;
traytel
parents: 40283
diff changeset
    49
declare [[coercion_map map]]
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    50
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    51
definition map_fun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'd)" where
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
    52
 "map_fun f g h = g o h o f"
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    53
40297
c753e3f8b4d6 Attribute map_function -> coercion_map;
traytel
parents: 40283
diff changeset
    54
declare [[coercion_map "\<lambda> f g h . g o h o f"]]
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    55
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    56
primrec map_pair :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a * 'b) \<Rightarrow> ('c * 'd)" where
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    57
 "map_pair f g (x,y) = (f x, g y)"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    58
40297
c753e3f8b4d6 Attribute map_function -> coercion_map;
traytel
parents: 40283
diff changeset
    59
declare [[coercion_map map_pair]]
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    60
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    61
(* Examples taken from the haskell draft implementation *)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    62
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    63
term "(1::nat) = True"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    64
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    65
term "True = (1::nat)"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    66
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    67
term "(1::nat) = (True = (1::nat))"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    68
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    69
term "op = (True = (1::nat))"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    70
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    71
term "[1::nat,True]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    72
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    73
term "[True,1::nat]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    74
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    75
term "[1::nat] = [True]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    76
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    77
term "[True] = [1::nat]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    78
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    79
term "[[True]] = [[1::nat]]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    80
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    81
term "[[[[[[[[[[True]]]]]]]]]] = [[[[[[[[[[1::nat]]]]]]]]]]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    82
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    83
term "[[True],[42::nat]] = rev [[True]]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    84
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    85
term "rev [10000::nat] = [False, 420000::nat, True]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    86
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    87
term "\<lambda> x . x = (3::nat)"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    88
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    89
term "(\<lambda> x . x = (3::nat)) True"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    90
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    91
term "map (\<lambda> x . x = (3::nat))"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    92
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    93
term "map (\<lambda> x . x = (3::nat)) [True,1::nat]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    94
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    95
consts bnn :: "(bool \<Rightarrow> nat) \<Rightarrow> nat"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    96
consts nb :: "nat \<Rightarrow> bool"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    97
consts ab :: "'a \<Rightarrow> bool"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    98
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
    99
term "bnn nb"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   100
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   101
term "bnn ab"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   102
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   103
term "\<lambda> x . x = (3::int)"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   104
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   105
term "map (\<lambda> x . x = (3::int)) [True]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   106
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   107
term "map (\<lambda> x . x = (3::int)) [True,1::nat]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   108
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   109
term "map (\<lambda> x . x = (3::int)) [True,1::nat,1::int]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   110
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   111
term "[1::nat,True,1::int,False]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   112
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   113
term "map (map (\<lambda> x . x = (3::int))) [[True],[1::nat],[True,1::int]]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   114
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   115
consts cbool :: "'a \<Rightarrow> bool"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   116
consts cnat :: "'a \<Rightarrow> nat"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   117
consts cint :: "'a \<Rightarrow> int"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   118
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   119
term "[id, cbool, cnat, cint]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   120
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   121
consts funfun :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   122
consts flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   123
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   124
term "flip funfun"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   125
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   126
term "map funfun [id,cnat,cint,cbool]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   127
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   128
term "map (flip funfun True)"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   129
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   130
term "map (flip funfun True) [id,cnat,cint,cbool]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   131
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   132
consts ii :: "int \<Rightarrow> int"
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   133
consts aaa :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   134
consts nlist :: "nat list"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   135
consts ilil :: "int list \<Rightarrow> int list"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   136
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   137
term "ii (aaa (1::nat) True)"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   138
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   139
term "map ii nlist"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   140
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   141
term "ilil nlist"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   142
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   143
(***************************************************)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   144
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   145
(* Other examples *)
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   146
40282
329cd9dd5949 proper header;
wenzelm
parents: 40281
diff changeset
   147
definition xs :: "bool list" where "xs = [True]"
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   148
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   149
term "(xs::nat list)"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   150
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   151
term "(1::nat) = True"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   152
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   153
term "True = (1::nat)"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   154
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   155
term "int (1::nat)"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   156
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   157
term "((True::nat)::int)"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   158
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   159
term "1::nat"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   160
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   161
term "nat 1"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   162
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   163
definition C :: nat
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   164
where "C = 123"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   165
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   166
consts g :: "int \<Rightarrow> int"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   167
consts h :: "nat \<Rightarrow> nat"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   168
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   169
term "(g (1::nat)) + (h 2)"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   170
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   171
term "g 1"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   172
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   173
term "1+(1::nat)"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   174
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   175
term "((1::int) + (1::nat),(1::int))"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   176
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   177
definition ys :: "bool list list list list list" where "ys=[[[[[True]]]]]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   178
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   179
term "ys=[[[[[1::nat]]]]]"
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   180
51335
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51320
diff changeset
   181
typedecl ('a, 'b, 'c) F
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51320
diff changeset
   182
consts Fmap :: "('a \<Rightarrow> 'd) \<Rightarrow> ('a, 'b, 'c) F \<Rightarrow> ('d, 'b, 'c) F"
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51320
diff changeset
   183
consts z :: "(bool, nat, bool) F"
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51320
diff changeset
   184
declare [[coercion_map "Fmap :: ('a \<Rightarrow> 'd) \<Rightarrow> ('a, 'b, 'c) F \<Rightarrow> ('d, 'b, 'c) F"]]
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51320
diff changeset
   185
term "z :: (nat, nat, bool) F"
6bac04a6a197 allow more general coercion maps; tuned;
traytel
parents: 51320
diff changeset
   186
51320
c1cb872ccb2b coercion-invariant arguments at work
traytel
parents: 51247
diff changeset
   187
consts
c1cb872ccb2b coercion-invariant arguments at work
traytel
parents: 51247
diff changeset
   188
  case_nil :: "'a \<Rightarrow> 'b"
c1cb872ccb2b coercion-invariant arguments at work
traytel
parents: 51247
diff changeset
   189
  case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
c1cb872ccb2b coercion-invariant arguments at work
traytel
parents: 51247
diff changeset
   190
  case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
c1cb872ccb2b coercion-invariant arguments at work
traytel
parents: 51247
diff changeset
   191
  case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
c1cb872ccb2b coercion-invariant arguments at work
traytel
parents: 51247
diff changeset
   192
c1cb872ccb2b coercion-invariant arguments at work
traytel
parents: 51247
diff changeset
   193
declare [[coercion_args case_cons - -]]
c1cb872ccb2b coercion-invariant arguments at work
traytel
parents: 51247
diff changeset
   194
declare [[coercion_args case_abs -]]
c1cb872ccb2b coercion-invariant arguments at work
traytel
parents: 51247
diff changeset
   195
declare [[coercion_args case_elem - +]]
c1cb872ccb2b coercion-invariant arguments at work
traytel
parents: 51247
diff changeset
   196
c1cb872ccb2b coercion-invariant arguments at work
traytel
parents: 51247
diff changeset
   197
term "case_cons (case_abs (\<lambda>n. case_abs (\<lambda>is. case_elem (((n::nat),(is::int list))) (n#is)))) case_nil"
c1cb872ccb2b coercion-invariant arguments at work
traytel
parents: 51247
diff changeset
   198
c1cb872ccb2b coercion-invariant arguments at work
traytel
parents: 51247
diff changeset
   199
consts n :: nat m :: nat
c1cb872ccb2b coercion-invariant arguments at work
traytel
parents: 51247
diff changeset
   200
term "- (n + m)"
c1cb872ccb2b coercion-invariant arguments at work
traytel
parents: 51247
diff changeset
   201
declare [[coercion_args uminus -]]
c1cb872ccb2b coercion-invariant arguments at work
traytel
parents: 51247
diff changeset
   202
declare [[coercion_args plus + +]]
c1cb872ccb2b coercion-invariant arguments at work
traytel
parents: 51247
diff changeset
   203
term "- (n + m)"
c1cb872ccb2b coercion-invariant arguments at work
traytel
parents: 51247
diff changeset
   204
 
40281
3c6198fd0937 Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
diff changeset
   205
end