src/HOL/Tools/Function/sum_tree.ML

made "query" type systes a bit more sound -- local facts, e.g. the negated conjecture, may make invalid the infinity check, e.g. if we are proving that there exists two values of an infinite type, we can use the negated conjecture that there is only one value to derive unsound proofs unless the type is properly encoded

(*  Title:      HOL/Tools/Function/sum_tree.ML
    Author:     Alexander Krauss, TU Muenchen

Some common tools for working with sum types in balanced tree form.
*)

structure SumTree =
struct

(* Theory dependencies *)
val sumcase_split_ss =
  HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases})

(* top-down access in balanced tree *)
fun access_top_down {left, right, init} len i =
  Balanced_Tree.access
    {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init

(* Sum types *)
fun mk_sumT LT RT = Type (@{type_name Sum_Type.sum}, [LT, RT])
fun mk_sumcase TL TR T l r =
  Const (@{const_name sum.sum_case},
    (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r

val App = curry op $

fun mk_inj ST n i =
  access_top_down
  { init = (ST, I : term -> term),
    left = (fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), inj) =>
      (LT, inj o App (Const (@{const_name Inl}, LT --> T)))),
    right =(fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), inj) =>
      (RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i
  |> snd

fun mk_proj ST n i =
  access_top_down
  { init = (ST, I : term -> term),
    left = (fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), proj) =>
      (LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)),
    right =(fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), proj) =>
      (RT, App (Const (@{const_name Sum_Type.Projr}, T --> RT)) o proj))} n i
  |> snd

fun mk_sumcases T fs =
  Balanced_Tree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) 
    (map (fn f => (f, domain_type (fastype_of f))) fs)
  |> fst

end