File ‹property.ML›
signature PROPERTY =
sig
val is_property: term -> bool
val add_property_field_const: term -> theory -> theory
val is_property_field: theory -> term -> bool
val strip_property_field: theory -> term -> term list
val is_property_prem: theory -> term -> bool
val get_property_name: term -> string
val get_property_names: term list -> string list
val get_property_arg: term -> term
val get_property_arg_th: thm -> cterm
val can_add_property_update: thm -> theory -> bool
val add_property_update: thm -> theory -> theory
val lookup_property_update: theory -> string -> thm list
val lookup_property_update_fun: theory -> string -> thm list
val instantiate_property_update: Proof.context -> term -> thm -> thm option
end;
functor Property(
structure Basic_UtilBase: BASIC_UTIL_BASE;
structure UtilLogic : UTIL_LOGIC
) : PROPERTY =
struct
structure UpdateData = Theory_Data (
type T = (thm list) Symtab.table;
val empty = Symtab.empty;
val merge = Symtab.merge_list Thm.eq_thm_prop
)
structure UpdateFunData = Theory_Data (
type T = (thm list) Symtab.table;
val empty = Symtab.empty;
val merge = Symtab.merge_list Thm.eq_thm_prop
)
structure FieldData = Theory_Data (
type T = unit Symtab.table;
val empty = Symtab.empty;
val merge = Symtab.merge (K true)
)
fun is_property t =
let
val _ = assert (fastype_of t = Basic_UtilBase.boolT) "is_property: wrong type"
val (f, ts) = Term.strip_comb t
in
if length ts <> 1 orelse not (Term.is_Const f) then false else
let
val T = fastype_of (the_single ts)
val (dT, _) = Term.strip_type T
in
length dT = 0 andalso T <> Basic_UtilBase.boolT
end
end
fun add_property_field_const t thy =
case Term.head_of t of
Const (c, T) =>
let
val (pTs, _) = Term.strip_type T
val _ = if length pTs = 1 then ()
else error "Add property field: input should be a field."
val _ = writeln ("Add field " ^ c ^ " as property field.")
in
thy |> FieldData.map (Symtab.update_new (c, ()))
end
| _ => error "Add property field: input should be a constant."
fun is_property_field thy t =
case t of
Var _ => true
| Const (c, _) $ t' =>
Symtab.defined (FieldData.get thy) c andalso is_property_field thy t'
| _ => false
fun strip_property_field thy t =
case t of
Const (c, _) $ t' =>
if Symtab.defined (FieldData.get thy) c then
t :: strip_property_field thy t'
else [t]
| _ => [t]
fun is_property_prem thy t =
is_property t andalso is_property_field thy (dest_arg t)
val get_property_name = Util.get_head_name
fun get_property_names ts =
ts |> map get_property_name |> distinct (op =)
fun get_property_arg t =
dest_arg t
handle Fail "dest_arg" => raise Fail "get_property_arg: t in wrong form."
fun get_property_arg_th th =
Thm.dest_arg (UtilLogic.cprop_of' th)
handle CTERM _ => raise Fail "get_property_carg"
| Fail "dest_Trueprop" => raise Fail "get_property_carg"
fun can_add_property_update th thy =
let
val (prems, concl) = UtilLogic.strip_horn' th
in
if is_property concl andalso forall (is_property_prem thy) prems
then let
val concl_arg = get_property_arg concl
val all_vars = map Var (Term.add_vars (Thm.prop_of th) [])
in
if is_Var concl_arg then
length all_vars = 1
else
let
val args = Util.dest_args concl_arg
in
forall is_Var args andalso subset (op aconv) (all_vars, args)
end
end
else false
end
fun add_property_update th thy =
let
val (prems, concl) = UtilLogic.strip_horn' th
val _ = assert (is_property concl)
"add_property_update: concl must be a property constant."
val _ = assert (forall (is_property_prem thy) prems)
"add_property_update: prem must be a property premise."
val concl_arg = get_property_arg concl
val all_vars = map Var (Term.add_vars (Thm.prop_of th) [])
in
if is_Var concl_arg then
let
val _ = assert (length all_vars = 1)
"add_property_update: extraneous Vars in th."
val names = get_property_names prems
val _ = writeln ("Add property rule for " ^
(Util.string_of_list I names))
in
thy |> UpdateData.map (
fold (Symtab.update_list Thm.eq_thm_prop) (map (rpair th) names))
end
else
let
val (f, args) = Term.strip_comb concl_arg
val c =
case f of
Const (c, _) => c
| _ => raise Fail "add_property_update: f is not constant."
val _ = assert (forall is_Var args)
"add_property_update: all args of concl must be Vars."
val _ = assert (subset (op aconv) (all_vars, args))
"add_property_update: extraneous Vars in th."
val _ = writeln ("Add property rule for function " ^ c)
in
thy |> UpdateFunData.map (Symtab.update_list Thm.eq_thm_prop (c, th))
end
end
fun lookup_property_update thy c =
Symtab.lookup_list (UpdateData.get thy) c
fun lookup_property_update_fun thy c =
Symtab.lookup_list (UpdateFunData.get thy) c
fun instantiate_property_update ctxt t th =
let
val (_, concl) = UtilLogic.strip_horn' th
val concl_arg = get_property_arg concl
val thy = Proof_Context.theory_of ctxt
in
if Sign.typ_instance thy (fastype_of t, fastype_of concl_arg) then
let
val err_str = "instantiate_property_update: cannot match with t."
val inst = Pattern.first_order_match thy (concl_arg, t) fo_init
handle Pattern.MATCH => raise Fail err_str
in
SOME (Util.subst_thm ctxt inst th)
end
else NONE
end
end