Theory Decomp

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2013)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2015)
License: LGPL (see file COPYING.LESSER)
*)
theory Decomp
imports
  "../Rewriting/Term"
  Option_Monad
begin

definition
  "decompose s t =
    (case (s, t) of
      (Fun f ss, Fun g ts) ⇒ if f = g then zip_option ss ts else None
    | _ ⇒ None)"

lemma decompose_Some [dest]:
  "decompose (Fun f ss) (Fun g ts) = Some E ⟹
    f = g ∧ length ss = length ts ∧ E = zip ss ts"
  by (cases "f = g") (auto simp: decompose_def)

lemma decompose_None [dest]:
  "decompose (Fun f ss) (Fun g ts) = None ⟹ f ≠ g ∨ length ss ≠ length ts"
  by (cases "f = g") (auto simp: decompose_def)

end