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