(*  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 : Nominal_Function_Common.nominal_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 -> Nominal_Function_Common.nominal_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

open Nominal_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 = Proof_Context.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

fun mk_inv inv (f_trm, arg_trm) = 

  betapplys (inv, [arg_trm, (f_trm $ arg_trm)])

  |> HOLogic.mk_Trueprop

fun mk_invariant (Globals {x, y, ...}) G invariant = 

  let

    val prem = HOLogic.mk_Trueprop (G $ x $ y)

    val concl = HOLogic.mk_Trueprop (betapplys (invariant, [x, y]))

  in

    Logic.mk_implies (prem, concl)

    |> mk_forall_rename ("y", y)

    |> mk_forall_rename ("x", x)

  end  

(** building proof obligations *)

fun mk_eqvt_proof_obligation qs fvar (vs, assms, arg) = 

  mk_eqvt_at (fvar, arg)

  |> curry Logic.list_implies (map prop_of assms)

  |> curry Term.list_all_free vs

  |> fold_rev absfree qs

  |> strip_abs_body

fun mk_inv_proof_obligation inv qs fvar (vs, assms, arg) = 

  mk_inv inv (fvar, arg)

  |> curry Logic.list_implies (map prop_of assms)

  |> curry Term.list_all_free vs

  |> fold_rev absfree qs

  |> strip_abs_body

(** building proof obligations *)

fun mk_compat_proof_obligations domT ranT fvar f RCss inv glrs =

  let

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

      let

        val shift = incr_boundvars (length qs')

        val eqvts_obligations_lhs = map (shift o mk_eqvt_proof_obligation qs fvar) RCs_lhs

        val eqvts_obligations_rhs = map (mk_eqvt_proof_obligation qs' fvar) RCs_rhs

        val invs_obligations_lhs = map (shift o mk_inv_proof_obligation inv qs fvar) RCs_lhs

        val invs_obligations_rhs = map (mk_inv_proof_obligation inv qs' fvar) RCs_rhs

      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) invs_obligations_rhs (* nominal *)

        |> fold_rev (curry Logic.mk_implies) invs_obligations_lhs (* nominal *)

        |> fold_rev (curry Logic.mk_implies) eqvts_obligations_rhs (* nominal *)

        |> fold_rev (curry Logic.mk_implies) eqvts_obligations_lhs (* 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 ~~ RCss))

  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 = Proof_Context.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 (Proof_Context.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 (Proof_Context.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 invsi invsj i j ctxi ctxj =

  let

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

    val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,case_hyp=case_hypj,...} = 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 eqvtsj (* nominal *)

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

      |> fold Thm.elim_implies invsj (* nominal *)

      |> fold Thm.elim_implies invsi (* 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 eqvtsi  (* nominal *)

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

      |> fold Thm.elim_implies invsi  (* nominal *)

      |> fold Thm.elim_implies invsj  (* 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_invariant_lemma thy ih_inv 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_inv_case =

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

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

        (llRI RS ih_inv_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_inv 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 invs 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 invsi = nth invs (i - 1)

      |> map (fold Thm.forall_elim cqsi)

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

      |> map (fold Thm.elim_implies agsi)

    val invsj = nth invs (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 invsi invsj 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 invlems 

  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 invlems 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