(*  Nominal Function Core

    Author:  Christian Urban

    heavily based on the code of Alexander Krauss

    (code forked on 14 January 2011)

Core of the nominal function package.

*)

signature NOMINAL_FUNCTION_CORE =

sig

  val trace: bool Unsynchronized.ref

  val prepare_nominal_function : Function_Common.function_config

    -> string (* defname *)

    -> ((bstring * typ) * mixfix) list (* defined symbol *)

    -> ((bstring * typ) list * term list * term * term) list (* specification *)

    -> local_theory

    -> (term   (* f *)

        * thm  (* goalstate *)

        * (thm -> Function_Common.function_result) (* continuation *)

       ) * local_theory

end

structure Nominal_Function_Core : NOMINAL_FUNCTION_CORE =

struct

val trace = Unsynchronized.ref false

fun trace_msg msg = if ! trace then tracing (msg ()) else ()

val boolT = HOLogic.boolT

val mk_eq = HOLogic.mk_eq

open Function_Lib

open Function_Common

datatype globals = Globals of

 {fvar: term,

  domT: typ,

  ranT: typ,

  h: term,

  y: term,

  x: term,

  z: term,

  a: term,

  P: term,

  D: term,

  Pbool:term}

datatype rec_call_info = RCInfo of

 {RIvs: (string * typ) list,  (* Call context: fixes and assumes *)

  CCas: thm list,

  rcarg: term,                 (* The recursive argument *)

  llRI: thm,

  h_assum: term}

datatype clause_context = ClauseContext of

 {ctxt : Proof.context,

  qs : term list,

  gs : term list,

  lhs: term,

  rhs: term,

  cqs: cterm list,

  ags: thm list,

  case_hyp : thm}

fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =

  ClauseContext { ctxt = ProofContext.transfer thy ctxt,

    qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }

datatype clause_info = ClauseInfo of

 {no: int,

  qglr : ((string * typ) list * term list * term * term),

  cdata : clause_context,

  tree: Function_Ctx_Tree.ctx_tree,

  lGI: thm,

  RCs: rec_call_info list}

(* Theory dependencies. *)

val acc_induct_rule = @{thm accp_induct_rule}

val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence}

val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness}

val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff}

val acc_downward = @{thm accp_downward}

val accI = @{thm accp.accI}

val case_split = @{thm HOL.case_split}

val fundef_default_value = @{thm FunDef.fundef_default_value}

val not_acc_down = @{thm not_accp_down}

fun find_calls tree =

  let

    fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) =

      ([], (fixes, assumes, arg) :: xs)

      | add_Ri _ _ _ _ = raise Match

  in

    rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])

  end

(* nominal *)

fun mk_eqvt_at (f_trm, arg_trm) =

  let

    val f_ty = fastype_of f_trm

    val arg_ty = domain_type f_ty

  in

    Const (@{const_name eqvt_at}, [f_ty, arg_ty] ---> @{typ bool}) $ f_trm $ arg_trm

    |> HOLogic.mk_Trueprop

  end

fun mk_eqvt trm =

  let

    val ty = fastype_of trm

  in

    Const (@{const_name eqvt}, ty --> @{typ bool}) $ trm

    |> HOLogic.mk_Trueprop

  end

(* nominal *)

fun find_calls2 f t = 

  let

    fun aux (g $ arg) = aux g #> aux arg #> (if f = g then cons ((g, arg)) else I)

      | aux (Abs (_, _, t)) = aux t 

      | aux _ = I

  in

    aux t []

  end 

(** building proof obligations *)

fun mk_compat_proof_obligations domT ranT fvar f glrs =

  let

    fun mk_impl ((qs, gs, lhs, rhs), (qs', gs', lhs', rhs')) =

      let

        val shift = incr_boundvars (length qs')

        val RCs_rhs  = find_calls2 fvar rhs (* nominal : FIXME : recursive calls should be passed here *)

      in

        Logic.mk_implies

          (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'),

            HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs'))

        |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')

        |> fold_rev (curry Logic.mk_implies) (map (shift o mk_eqvt_at) RCs_rhs) (* nominal *)

        |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs')

        |> curry abstract_over fvar

        |> curry subst_bound f

      end

  in

    map mk_impl (unordered_pairs glrs)

  end

fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =

  let

    fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =

      HOLogic.mk_Trueprop Pbool

      |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs)))

      |> fold_rev (curry Logic.mk_implies) gs

      |> fold_rev mk_forall_rename (map fst oqs ~~ qs)

  in

    HOLogic.mk_Trueprop Pbool

    |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)

    |> mk_forall_rename ("x", x)

    |> mk_forall_rename ("P", Pbool)

  end

(** making a context with it's own local bindings **)

fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =

  let

    val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt

      |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs

    val thy = ProofContext.theory_of ctxt'

    fun inst t = subst_bounds (rev qs, t)

    val gs = map inst pre_gs

    val lhs = inst pre_lhs

    val rhs = inst pre_rhs

    val cqs = map (cterm_of thy) qs

    val ags = map (Thm.assume o cterm_of thy) gs

    val case_hyp = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))

  in

    ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,

      cqs = cqs, ags = ags, case_hyp = case_hyp }

  end

(* lowlevel term function. FIXME: remove *)

fun abstract_over_list vs body =

  let

    fun abs lev v tm =

      if v aconv tm then Bound lev

      else

        (case tm of

          Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)

        | t $ u => abs lev v t $ abs lev v u

        | t => t)

  in

    fold_index (fn (i, v) => fn t => abs i v t) vs body

  end

fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =

  let

    val Globals {h, ...} = globals

    val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata

    val cert = Thm.cterm_of (ProofContext.theory_of ctxt)

    (* Instantiate the GIntro thm with "f" and import into the clause context. *)

    val lGI = GIntro_thm

      |> Thm.forall_elim (cert f)

      |> fold Thm.forall_elim cqs

      |> fold Thm.elim_implies ags

    fun mk_call_info (rcfix, rcassm, rcarg) RI =

      let

        val llRI = RI

          |> fold Thm.forall_elim cqs

          |> fold (Thm.forall_elim o cert o Free) rcfix

          |> fold Thm.elim_implies ags

          |> fold Thm.elim_implies rcassm

        val h_assum =

          HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))

          |> fold_rev (curry Logic.mk_implies o prop_of) rcassm

          |> fold_rev (Logic.all o Free) rcfix

          |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []

          |> abstract_over_list (rev qs)

      in

        RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}

      end

    val RC_infos = map2 mk_call_info RCs RIntro_thms

  in

    ClauseInfo {no=no, cdata=cdata, qglr=qglr, lGI=lGI, RCs=RC_infos,

      tree=tree}

  end

fun store_compat_thms 0 thms = []

  | store_compat_thms n thms =

  let

    val (thms1, thms2) = chop n thms

  in

    (thms1 :: store_compat_thms (n - 1) thms2)

  end

(* expects i <= j *)

fun lookup_compat_thm i j cts =

  nth (nth cts (i - 1)) (j - i)

(* nominal *)

(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)

(* if j < i, then turn around *)

fun get_compat_thm thy cts eqvtsi eqvtsj i j ctxi ctxj =

  let

    val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi

    val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj

    val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj)))

  in if j < i then

    let

      val compat = lookup_compat_thm j i cts

    in

      compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)

      |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)

      |> fold Thm.elim_implies (rev eqvtsj) (* nominal *)

      |> fold Thm.elim_implies agsj

      |> fold Thm.elim_implies agsi

      |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)

    end

    else

    let

      val compat = lookup_compat_thm i j cts

    in

      compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)

      |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)

      |> fold Thm.elim_implies (rev eqvtsi)  (* nominal *)

      |> fold Thm.elim_implies agsi

      |> fold Thm.elim_implies agsj

      |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj)

      |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)

    end

  end

(* Generates the replacement lemma in fully quantified form. *)

fun mk_replacement_lemma thy h ih_elim clause =

  let

    val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...},

      RCs, tree, ...} = clause

    local open Conv in

      val ih_conv = arg1_conv o arg_conv o arg_conv

    end

    val ih_elim_case =

      Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim

    val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs

    val h_assums = map (fn RCInfo {h_assum, ...} =>

      Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs

    val (eql, _) =

      Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree

    val replace_lemma = (eql RS meta_eq_to_obj_eq)

      |> Thm.implies_intr (cprop_of case_hyp)

      |> fold_rev (Thm.implies_intr o cprop_of) h_assums

      |> fold_rev (Thm.implies_intr o cprop_of) ags

      |> fold_rev Thm.forall_intr cqs

      |> Thm.close_derivation

  in

    replace_lemma

  end

(* nominal *)

(* Generates the eqvt lemmas for each clause *) 

fun mk_eqvt_lemma thy ih_eqvt clause =

  let

    val ClauseInfo {cdata=ClauseContext {cqs, ags, case_hyp, ...}, RCs, ...} = clause

    local open Conv in

      val ih_conv = arg1_conv o arg_conv o arg_conv

    end

    val ih_eqvt_case =

      Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_eqvt

    fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = 

        (llRI RS ih_eqvt_case)

        |> fold_rev (Thm.implies_intr o cprop_of) CCas

        |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs

  in

    map prep_eqvt RCs

    |> map (fold_rev (Thm.implies_intr o cprop_of) ags)

    |> map (Thm.implies_intr (cprop_of case_hyp))

    |> map (fold_rev Thm.forall_intr cqs)

    |> map (Thm.close_derivation) 

  end

(* nominal *)

fun mk_uniqueness_clause thy globals compat_store eqvts clausei clausej RLj =

  let

    val Globals {h, y, x, fvar, ...} = globals

    val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, cqs = cqsi, 

      ags = agsi, ...}, ...} = clausei

    val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej

    val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} =

      mk_clause_context x ctxti cdescj 

    val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'

    val Ghsj' = map 

      (fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj

    val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))

    val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj'))))

       (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) 

    val case_hypj' = trans OF [case_hyp, lhsi_eq_lhsj']

    val RLj_import = RLj

      |> fold Thm.forall_elim cqsj'

      |> fold Thm.elim_implies agsj'

      |> fold Thm.elim_implies Ghsj'

    val eqvtsi = nth eqvts (i - 1)

      |> map (fold Thm.forall_elim cqsi)

      |> map (fold Thm.elim_implies [case_hyp])

      |> map (fold Thm.elim_implies agsi)

    val eqvtsj = nth eqvts (j - 1)

      |> map (fold Thm.forall_elim cqsj')

      |> map (fold Thm.elim_implies [case_hypj'])

      |> map (fold Thm.elim_implies agsj')

    val compat = get_compat_thm thy compat_store eqvtsi eqvtsj i j cctxi cctxj

  in

    (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)

    |> Thm.implies_elim RLj_import

      (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)

    |> (fn it => trans OF [it, compat])

      (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)

    |> (fn it => trans OF [y_eq_rhsj'h, it])

      (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)

    |> fold_rev (Thm.implies_intr o cprop_of) Ghsj'

    |> fold_rev (Thm.implies_intr o cprop_of) agsj'

      (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)

    |> Thm.implies_intr (cprop_of y_eq_rhsj'h)

    |> Thm.implies_intr (cprop_of lhsi_eq_lhsj')

    |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj')

  end

(* nominal *)

fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses replems eqvtlems clausei =

  let

    val Globals {x, y, ranT, fvar, ...} = globals

    val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei

    val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs

    val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro

    fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = 

        (llRI RS ih_intro_case)

        |> fold_rev (Thm.implies_intr o cprop_of) CCas

        |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs

    val existence = fold (curry op COMP o prep_RC) RCs lGI

    val P = cterm_of thy (mk_eq (y, rhsC))

    val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))

    val unique_clauses =

      map2 (mk_uniqueness_clause thy globals compat_store eqvtlems clausei) clauses replems

    fun elim_implies_eta A AB =

      Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single

    val uniqueness = G_cases

      |> Thm.forall_elim (cterm_of thy lhs)

      |> Thm.forall_elim (cterm_of thy y)

      |> Thm.forall_elim P

      |> Thm.elim_implies G_lhs_y

      |> fold elim_implies_eta unique_clauses

      |> Thm.implies_intr (cprop_of G_lhs_y)

      |> Thm.forall_intr (cterm_of thy y)

    val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)

    val exactly_one =

      ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]

      |> curry (op COMP) existence

      |> curry (op COMP) uniqueness

      |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])

      |> Thm.implies_intr (cprop_of case_hyp)

      |> fold_rev (Thm.implies_intr o cprop_of) ags

      |> fold_rev Thm.forall_intr cqs

    val function_value =

      existence

      |> Thm.implies_intr ihyp

      |> Thm.implies_intr (cprop_of case_hyp)

      |> Thm.forall_intr (cterm_of thy x)

      |> Thm.forall_elim (cterm_of thy lhs)

      |> curry (op RS) refl

  in

    (exactly_one, function_value)

  end

(* nominal *)

fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt f_def =

  let

    val Globals {h, domT, ranT, x, ...} = globals

    val thy = ProofContext.theory_of ctxt

    (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)

    val ihyp = Term.all domT $ Abs ("z", domT,

      Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),

        HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $

          Abs ("y", ranT, G $ Bound 1 $ Bound 0))))

      |> cterm_of thy

    val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0

    val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)

    val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)

      |> instantiate' [] [NONE, SOME (cterm_of thy h)]

    val ih_eqvt = ihyp_thm RS (G_eqvt RS (f_def RS @{thm fundef_ex1_eqvt_at}))

    val _ = trace_msg (K "Proving Replacement lemmas...")

    val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses

    val _ = trace_msg (K "Proving Equivariance lemmas...")

    val eqvtLemmas = map (mk_eqvt_lemma thy ih_eqvt) clauses

    val _ = trace_msg (K "Proving cases for unique existence...")

    val (ex1s, values) =

      split_list (map (mk_uniqueness_case thy globals G f 

        ihyp ih_intro G_elim compat_store clauses repLemmas eqvtLemmas) clauses)

    val _ = trace_msg (K "Proving: Graph is a function")

    val graph_is_function = complete

      |> Thm.forall_elim_vars 0

      |> fold (curry op COMP) ex1s

      |> Thm.implies_intr (ihyp)

      |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))

      |> Thm.forall_intr (cterm_of thy x)

      |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)

      |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)

    val goalstate =  

         Conjunction.intr (Conjunction.intr graph_is_function complete) G_eqvt 

      |> Thm.close_derivation

      |> Goal.protect

      |> fold_rev (Thm.implies_intr o cprop_of) compat

      |> Thm.implies_intr (cprop_of complete)

      |> Thm.implies_intr (cprop_of G_eqvt)

  in

    (goalstate, values)

  end

(* wrapper -- restores quantifiers in rule specifications *)

fun inductive_def (binding as ((R, T), _)) intrs lthy =

  let

    val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =

      lthy

      |> Local_Theory.conceal 

      |> Inductive.add_inductive_i

          {quiet_mode = true,

            verbose = ! trace,

            alt_name = Binding.empty,