coercion-invariant arguments at work
authortraytel
Fri Mar 01 22:15:31 2013 +0100 (2013-03-01)
changeset 51320c1cb872ccb2b
parent 51319 4a92178011e7
child 51321 75682dfff630
coercion-invariant arguments at work
src/HOL/ex/Coercion_Examples.thy
     1.1 --- a/src/HOL/ex/Coercion_Examples.thy	Fri Mar 01 22:15:31 2013 +0100
     1.2 +++ b/src/HOL/ex/Coercion_Examples.thy	Fri Mar 01 22:15:31 2013 +0100
     1.3 @@ -178,4 +178,22 @@
     1.4  
     1.5  term "ys=[[[[[1::nat]]]]]"
     1.6  
     1.7 +consts
     1.8 +  case_nil :: "'a \<Rightarrow> 'b"
     1.9 +  case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.10 +  case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
    1.11 +  case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
    1.12 +
    1.13 +declare [[coercion_args case_cons - -]]
    1.14 +declare [[coercion_args case_abs -]]
    1.15 +declare [[coercion_args case_elem - +]]
    1.16 +
    1.17 +term "case_cons (case_abs (\<lambda>n. case_abs (\<lambda>is. case_elem (((n::nat),(is::int list))) (n#is)))) case_nil"
    1.18 +
    1.19 +consts n :: nat m :: nat
    1.20 +term "- (n + m)"
    1.21 +declare [[coercion_args uminus -]]
    1.22 +declare [[coercion_args plus + +]]
    1.23 +term "- (n + m)"
    1.24 + 
    1.25  end