Theory Cases_Tactics_HOL

✐‹creator "Kevin Kappelmann"›
theory Cases_Tactics_HOL
  imports
    Cases_Tactics
    HOL.HOL
begin

ML‹
structure Cases_Tactic_HOL = Cases_Tactic(open Induct
  fun get_casesP ctxt (fact :: _) = find_casesP ctxt (Thm.concl_of fact)
    | get_casesP _ _ = []
  fun get_casesT ctxt binderTs (SOME t :: _) = find_casesT ctxt (Term.fastype_of1 (binderTs, t))
  | get_casesT _ _ _ = [])
structure Cases_Data_Args_Tactic_HOL = Cases_Data_Args_Tactic(Cases_Tactic_HOL)
›

text ‹For a function ‹f :: T⇩₁ ⇒ … ⇒ T⇩_n ⇒ T› with multiple arguments, the function package creates a
cases rule ‹f.cases› where ‹f›'s arguments are tupled and equated to a single variable. As a result,
one has to supply the cases tactic a single instantiation ‹(t⇩₁,…,t⇩_n)› when using ‹f.cases› while
users would expect being able to supply ‹n› instantiations ‹t⇩₁,…,t⇩_n›. Below attribute transforms
such rules to the expected form.›

local_setup ‹
  let
    fun add_prodTs T acc = try HOLogic.dest_prodT T
      |> (fn NONE => T :: acc | SOME (T, T') => T :: add_prodTs T' acc)
    fun inst_prod_cases ctxt thm = case Thm.prop_of thm |> Term.add_vars |> build |> rev of
        [] => error "No schematic variable in passed cases theorem."
      | ((n, _), T) :: _ =>
        let
          val maxidx = Thm.maxidx_of thm
          val inst = build (add_prodTs T)
            |> map_index (fn (idx, T) => Var ((n, maxidx + idx + 1), T))
            |> rev
            |> (fn t :: ts => fold (curry HOLogic.mk_prod) ts t)
            |> Thm.cterm_of ctxt
        in Thm.instantiate' [] [SOME inst] thm end
  in
    Attrib.local_setup @{binding deprod_cases}
      (Scan.succeed (Thm.rule_attribute [] (Context.proof_of #> inst_prod_cases)))
      ("Transform cases rule that uses a single product for instantiation to a cases rule using "
        ^ "multiple instantiations.")
  end
›

end