fun add_archconstdefs thy =
let
val termof =
HOLogic.mk_list
(HOLogic.mk_list
(HOLogic.mk_list (fn t => HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_bin t)
HOLogic.natT)
(HOLogic.listT(HOLogic.natT)))
(HOLogic.listT(HOLogic.listT(HOLogic.natT)));
val nlll = HOLogic.listT(HOLogic.listT(HOLogic.listT(HOLogic.natT)))
fun def c l =
let val lhs = Const (Sign.full_name thy c,nlll)
val rhs = termof l
in ((Thm.def_name c, Logic.mk_equals (lhs, rhs)), []) end;
val tri = "Tri"
val quad = "Quad"
val pent = "Pent"
val hex = "Hex"
val hept = "Hept"
val oct = "Oct"
in
thy
|> Theory.add_consts_i
[(tri, nlll, Syntax.NoSyn), (quad, nlll, Syntax.NoSyn),
(pent, nlll, Syntax.NoSyn), (hex, nlll, Syntax.NoSyn),
(hept, nlll, Syntax.NoSyn), (oct, nlll, Syntax.NoSyn)]
|> #2 o PureThy.add_defs_i false
[def tri Tri, def quad Quad, def pent Pent, def hex Hex, def hept Hept, def oct Oct]
end;