theory Barf
imports Main
begin

    datatype (discs_sels) 't "term" =
      Prim 't
    | Unit
    | Tensor "'t term * 't term"
    | Comp "'t term * 't term"
    | Lunit "'t term"
    | Runit "'t term"
    | Assoc "'t term * 't term * 't term"

    fun normalize :: "'t term \<Rightarrow> 't term"
    where "normalize t = t"

    fun redTensor
    and red
    where "redTensor (Unit, Unit) = Lunit Unit"
        | "redTensor (Prim f, Unit) = Runit (Prim f)"
        | "redTensor (Tensor (a, b), Unit) = Comp (redTensor (a, b), Runit (Tensor (a, b)))"
        | "redTensor (Unit, a) = Lunit a"
        | "redTensor (Prim f, a) = Tensor (Prim f, a)"
        | "redTensor (Tensor (a, b), c) =
              Comp (redTensor (a, normalize (Tensor (b, c))), Tensor (a, redTensor (b, c)))"
        | "redTensor (a, b) = Tensor (a, b)"

        | "red Unit = Unit"
        | "red (Prim f) = Prim f"
        | "red (Tensor (a, Unit)) = Comp (red a, Runit a)"
        | "red (Tensor (Unit, a)) = Comp (red a, Lunit a)"
        | "red (Tensor (Prim f, a)) = Tensor (Prim f, red a)"
        | "red (Tensor (Tensor (a, b), c)) =
             Comp (redTensor (red a, redTensor (red b, red c)), Assoc (a, b, c))"
        | "red a = a"

    lemma
    shows "\<And>b. P a b \<Longrightarrow> Q a b"
    and "R a \<Longrightarrow> S a"
    proof (induct a and a rule: redTensor_red.induct)
      show ?thesis
      sorry
    qed

end