src/HOL/ex/Coercion_Examples.thy
 changeset 51320 c1cb872ccb2b parent 51247 064683ba110c child 51335 6bac04a6a197
equal inserted replaced
51319:4a92178011e7 51320:c1cb872ccb2b
`   176 `
`   176 `
`   177 definition ys :: "bool list list list list list" where "ys=[[[[[True]]]]]"`
`   177 definition ys :: "bool list list list list list" where "ys=[[[[[True]]]]]"`
`   178 `
`   178 `
`   179 term "ys=[[[[[1::nat]]]]]"`
`   179 term "ys=[[[[[1::nat]]]]]"`
`   180 `
`   180 `
`       `
`   181 consts`
`       `
`   182   case_nil :: "'a \<Rightarrow> 'b"`
`       `
`   183   case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"`
`       `
`   184   case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"`
`       `
`   185   case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"`
`       `
`   186 `
`       `
`   187 declare [[coercion_args case_cons - -]]`
`       `
`   188 declare [[coercion_args case_abs -]]`
`       `
`   189 declare [[coercion_args case_elem - +]]`
`       `
`   190 `
`       `
`   191 term "case_cons (case_abs (\<lambda>n. case_abs (\<lambda>is. case_elem (((n::nat),(is::int list))) (n#is)))) case_nil"`
`       `
`   192 `
`       `
`   193 consts n :: nat m :: nat`
`       `
`   194 term "- (n + m)"`
`       `
`   195 declare [[coercion_args uminus -]]`
`       `
`   196 declare [[coercion_args plus + +]]`
`       `
`   197 term "- (n + m)"`
`       `
`   198  `
`   181 end`
`   199 end`