(*  Nominal Termination
    Author: Christian Urban

    heavily based on the code of Alexander Krauss
    (code forked on 18 July 2011)

Redefinition of the termination command
*)

signature NOMINAL_FUNCTION_TERMINATION =
sig
  include NOMINAL_FUNCTION_DATA

  val termination : bool -> term option -> local_theory -> Proof.state
  val termination_cmd : bool -> string option -> local_theory -> Proof.state

end

structure Nominal_Function_Termination : NOMINAL_FUNCTION_TERMINATION =
struct

open Function_Lib
open Function_Common
open Nominal_Function_Common

val simp_attribs = map (Attrib.internal o K)
  [Simplifier.simp_add,
   Code.add_default_eqn_attribute,
   Nitpick_Simps.add]

val eqvt_attrib =  Attrib.internal (K Nominal_ThmDecls.eqvt_add)

fun prepare_termination_proof prep_term is_eqvt raw_term_opt lthy =
  let
    val term_opt = Option.map (prep_term lthy) raw_term_opt
    val info = the (case term_opt of
                      SOME t => (import_function_data t lthy
                        handle Option.Option =>
                          error ("Not a function: " ^ quote (Syntax.string_of_term lthy t)))
                    | NONE => (import_last_function lthy handle Option.Option => error "Not a function"))

      val { termination, fs, R, add_simps, case_names, psimps,
        pinducts, defname, eqvts, ...} = info
      val domT = domain_type (fastype_of R)

      val goal = HOLogic.mk_Trueprop
                   (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
      fun afterqed [[totality]] lthy =
        let
          val totality = Thm.close_derivation totality
          val remove_domain_condition =
            full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}])
          val tsimps = map remove_domain_condition psimps
          val tinducts = map remove_domain_condition pinducts
          val teqvts = map remove_domain_condition eqvts

          fun qualify n = Binding.name n
            |> Binding.qualify true defname
        in
          lthy
          |> add_simps I "simps" I simp_attribs tsimps
          ||>> Local_Theory.note ((qualify "eqvt", if is_eqvt then [eqvt_attrib] else []), teqvts)
          ||>> Local_Theory.note
             ((qualify "induct",
               [Attrib.internal (K (Rule_Cases.case_names case_names))]),
              tinducts)
          |-> (fn ((simps, (_, eqvts)), (_, inducts)) => fn lthy =>
            let val info' = { is_partial=false, defname=defname, add_simps=add_simps,
              case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
              simps=SOME simps, inducts=SOME inducts, termination=termination, eqvts=teqvts }
            in
              (info',
               lthy 
               |> Local_Theory.declaration {syntax = false, pervasive = false}
                    (add_function_data o morph_function_data info')
               |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
            end)
        end
  in
    (goal, afterqed, termination)
  end

fun gen_termination prep_term is_eqvt raw_term_opt lthy =
  let
    val (goal, afterqed, termination) = prepare_termination_proof prep_term is_eqvt raw_term_opt lthy
  in
    lthy
    |> Proof_Context.note_thmss ""
       [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd
    |> Proof_Context.note_thmss ""
       [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
    |> Proof_Context.note_thmss ""
       [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
         [([Goal.norm_result termination], [])])] |> snd
    |> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]]
  end

val termination = gen_termination Syntax.check_term
val termination_cmd = gen_termination Syntax.read_term

(* outer syntax *)

val option_parser =
  (Scan.optional (@{keyword "("} |-- Parse.!!! 
    ((Parse.reserved "eqvt" >> K (true, true)) ||
     (Parse.reserved "no_eqvt" >> K (true, false))) --| @{keyword ")"}) (false, false))

val _ =
  Outer_Syntax.local_theory_to_proof ("termination", Keyword.thy_goal) 
    "prove termination of a recursive function"
      (option_parser -- Scan.option Parse.term >> 
        (fn ((is_nominal, is_eqvt), opt_trm) => 
           if is_nominal then termination_cmd is_eqvt opt_trm else Function.termination_cmd opt_trm))

end