src/HOL/Tools/function_package/fundef_common.ML

Major update to function package, including new syntax and the (only theoretical)
ability to handle local contexts.

(*  Title:      HOL/Tools/function_package/fundef_common.ML
    ID:         $Id$
    Author:     Alexander Krauss, TU Muenchen

A package for general recursive function definitions. 
Common type definitions and other infrastructure.
*)

structure FundefCommon =
struct

(* Theory Dependencies *)
val acc_const_name = "Accessible_Part.acc"

fun mk_acc domT R =
    Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R 


type depgraph = int IntGraph.T


datatype ctx_tree 
  = Leaf of term
  | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
  | RCall of (term * ctx_tree)

type glrs = (term list * term list * term * term) list


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: ctx_tree,
      lGI: thm,
      RCs: rec_call_info list
     }




type qgar = string * (string * typ) list * term list * term list * term

fun name_of_fqgar (f, _, _, _, _) = f

datatype mutual_part =
  MutualPart of 
	 {
          fvar : string * typ,
	  cargTs: typ list,
	  pthA: SumTools.sum_path,
	  pthR: SumTools.sum_path,
	  f_def: term,

	  f: term option,
          f_defthm : thm option
	 }
	 

datatype mutual_info =
  Mutual of 
	 { 
	  defname: string,
          fsum_var : string * typ,

	  ST: typ,
	  RST: typ,
	  streeA: SumTools.sum_tree,
	  streeR: SumTools.sum_tree,

	  parts: mutual_part list,
	  fqgars: qgar list,
	  qglrs: ((string * typ) list * term list * term * term) list,

          fsum : term option
	 }


datatype prep_result =
  Prep of
     {
      globals: globals,
      f: term,
      G: term,
      R: term,
 
      goal: term,
      goalI: thm,
      values: thm list,
      clauses: clause_info list,

      R_cases: thm,
      ex1_iff: thm
     }

datatype fundef_result =
  FundefResult of
     {
      f: term,
      G : term,
      R : term,
      completeness : thm,

      psimps : thm list, 
      subset_pinduct : thm, 
      simple_pinduct : thm, 
      total_intro : thm,
      dom_intros : thm list
     }

datatype fundef_mresult =
  FundefMResult of
     {
      f: term,
      G: term,
      R: term,

      psimps : thm list, 
      subset_pinducts : thm list, 
      simple_pinducts : thm list, 
      cases : thm,
      termination : thm,
      domintros : thm list
     }


type fundef_spec = ((string * typ) * mixfix) list *((string * Attrib.src list) * term list) list list
type result_with_names = fundef_mresult * mutual_info * fundef_spec

structure FundefData = GenericDataFun
(struct
  val name = "HOL/function_def/data";
  type T = string * result_with_names Symtab.table

  val empty = ("", Symtab.empty);
  val copy = I;
  val extend = I;
  fun merge _ ((l1,tab1),(l2,tab2)) = (l1, Symtab.merge (K true) (tab1, tab2))

  fun print _ _ = ();
end);


structure FundefCongs = GenericDataFun
(struct
    val name = "HOL/function_def/congs"
    type T = thm list
    val empty = []
    val extend = I
    fun merge _ (l1, l2) = l1 @ l2
    fun print  _ _ = ()
end);


fun add_fundef_data name fundef_data =
    FundefData.map (fn (_,tab) => (name, Symtab.update_new (name, fundef_data) tab))

fun get_fundef_data name thy = Symtab.lookup (snd (FundefData.get thy)) name

fun get_last_fundef thy = fst (FundefData.get thy)

val map_fundef_congs = FundefCongs.map 
val get_fundef_congs = FundefCongs.get

end



(* Common Abbreviations *)

structure FundefAbbrev =
struct

fun implies_elim_swp x y = implies_elim y x

(* Some HOL things frequently used *)
val boolT = HOLogic.boolT
val mk_prod = HOLogic.mk_prod
val mk_mem = HOLogic.mk_mem
val mk_eq = HOLogic.mk_eq
val eq_const = HOLogic.eq_const
val Trueprop = HOLogic.mk_Trueprop

val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT
fun mk_relmem (x,y) R = Trueprop (mk_mem (mk_prod (x, y), R))

fun mk_subset T A B = 
    let val sT = HOLogic.mk_setT T
    in Const ("Orderings.less_eq", sT --> sT --> boolT) $ A $ B end


(* with explicit types: Needed with loose bounds *)
fun mk_relmemT xT yT (x,y) R = 
    let 
	val pT = HOLogic.mk_prodT (xT, yT)
	val RT = HOLogic.mk_setT pT
    in
	Const ("op :", [pT, RT] ---> boolT)
	      $ (HOLogic.pair_const xT yT $ x $ y)
	      $ R
    end

fun free_to_var (Free (v,T)) = Var ((v,0),T)
  | free_to_var _ = raise Match

fun var_to_free (Var ((v,_),T)) = Free (v,T)
  | var_to_free _ = raise Match


end