forked from Isabelle_DOF/Isabelle_DOF
Add support invariants on attributes of attributes
Support invariants on attributes of classes atttributes. Example: doc_class inv_test1 = a :: int doc_class inv_test2 = b :: "inv_test1" c:: int invariant inv_test2 :: "c σ = 1" invariant inv_test2' :: "a (b σ) = 2" doc_class inv_test3 = inv_test1 + b :: "inv_test1" c:: int invariant inv_test3 :: "a σ = 1" invariant inv_test3' :: "a (b σ) = 2" To support invariant on attributes in attributes and invariant on attributes of the superclasses, we check that the type of the attribute of the subclass is ground:› ML‹ val Type(st, [ty]) = \<^typ>‹inv_test1› val Type(st', [ty']) = \<^typ>‹'a inv_test1_scheme› val t = ty = \<^typ>‹unit› ›
This commit is contained in:
parent
cd758d2c44
commit
2b1a9d009e
|
@ -2649,30 +2649,40 @@ fun define_cond binding f_sty cond_suffix read_cond (ctxt:local_theory) =
|
||||||
fun define_inv cid_long ((lbl, pos), inv) thy =
|
fun define_inv cid_long ((lbl, pos), inv) thy =
|
||||||
let val bdg = Binding.make (lbl,pos)
|
let val bdg = Binding.make (lbl,pos)
|
||||||
val inv_term = Syntax.read_term (Proof_Context.init_global thy) inv
|
val inv_term = Syntax.read_term (Proof_Context.init_global thy) inv
|
||||||
fun update_attribute_type thy class_scheme_ty
|
(* Rewrite selectors types to allow invariants on attributes of the superclasses
|
||||||
|
using the polymorphic type of the class *)
|
||||||
|
fun update_attribute_type thy class_scheme_ty cid_long
|
||||||
(Const (s, Type (st,[ty, ty'])) $ t) =
|
(Const (s, Type (st,[ty, ty'])) $ t) =
|
||||||
let
|
let
|
||||||
val cid = Long_Name.qualifier s
|
val cid = Long_Name.qualifier s
|
||||||
in case DOF_core.get_doc_class_global cid thy of
|
in case DOF_core.get_doc_class_global cid thy of
|
||||||
NONE => Const (s, Type(st,[ty, ty']))
|
NONE => Const (s, Type(st,[ty, ty']))
|
||||||
$ (update_attribute_type thy class_scheme_ty t)
|
$ (update_attribute_type thy class_scheme_ty cid_long t)
|
||||||
| SOME _ => Const(s, Type(st,[class_scheme_ty, ty']))
|
| SOME _ => if DOF_core.is_subclass_global thy cid_long cid
|
||||||
$ (update_attribute_type thy class_scheme_ty t)
|
then let val Type(st', tys') = ty
|
||||||
|
in if tys' = [\<^typ>\<open>unit\<close>]
|
||||||
|
then Const (s, Type(st,[ty, ty']))
|
||||||
|
$ (update_attribute_type thy class_scheme_ty cid_long t)
|
||||||
|
else Const(s, Type(st,[class_scheme_ty, ty']))
|
||||||
|
$ (update_attribute_type thy class_scheme_ty cid_long t)
|
||||||
|
end
|
||||||
|
else Const (s, Type(st,[ty, ty']))
|
||||||
|
$ (update_attribute_type thy class_scheme_ty cid_long t)
|
||||||
end
|
end
|
||||||
| update_attribute_type thy class_scheme_ty (t $ t') =
|
| update_attribute_type thy class_scheme_ty cid_long (t $ t') =
|
||||||
(update_attribute_type thy class_scheme_ty t)
|
(update_attribute_type thy class_scheme_ty cid_long t)
|
||||||
$ (update_attribute_type thy class_scheme_ty t')
|
$ (update_attribute_type thy class_scheme_ty cid_long t')
|
||||||
| update_attribute_type thy class_scheme_ty (Abs(s, ty, t)) =
|
| update_attribute_type thy class_scheme_ty cid_long (Abs(s, ty, t)) =
|
||||||
Abs(s, ty, update_attribute_type thy class_scheme_ty t)
|
Abs(s, ty, update_attribute_type thy class_scheme_ty cid_long t)
|
||||||
| update_attribute_type _ class_scheme_ty (Free(s, ty)) = if s = invariantN
|
| update_attribute_type _ class_scheme_ty _ (Free(s, ty)) = if s = invariantN
|
||||||
then Free (s, class_scheme_ty)
|
then Free (s, class_scheme_ty)
|
||||||
else Free (s, ty)
|
else Free (s, ty)
|
||||||
| update_attribute_type _ _ t = t
|
| update_attribute_type _ _ _ t = t
|
||||||
val inv_ty = Syntax.read_typ (Proof_Context.init_global thy)
|
val inv_ty = Syntax.read_typ (Proof_Context.init_global thy)
|
||||||
(Name.aT ^ " " ^ cid_long ^ schemeN)
|
(Name.aT ^ " " ^ cid_long ^ schemeN)
|
||||||
(* Update the type of each attribute update function to match the type of the
|
(* Update the type of each attribute update function to match the type of the
|
||||||
current class. *)
|
current class. *)
|
||||||
val inv_term' = update_attribute_type thy inv_ty inv_term
|
val inv_term' = update_attribute_type thy inv_ty cid_long inv_term
|
||||||
val eq_inv_ty = inv_ty --> HOLogic.boolT
|
val eq_inv_ty = inv_ty --> HOLogic.boolT
|
||||||
val abs_term = Term.lambda (Free (invariantN, inv_ty)) inv_term'
|
val abs_term = Term.lambda (Free (invariantN, inv_ty)) inv_term'
|
||||||
in thy |> Named_Target.theory_map (define_cond bdg eq_inv_ty invariant_suffixN abs_term) end
|
in thy |> Named_Target.theory_map (define_cond bdg eq_inv_ty invariant_suffixN abs_term) end
|
||||||
|
|
|
@ -47,6 +47,32 @@ text\<open>
|
||||||
it inherits @{doc_class class_inv1} invariants.
|
it inherits @{doc_class class_inv1} invariants.
|
||||||
Hence the \<^term>\<open>int1\<close> invariant is checked when the instance @{docitem testinv2} is defined.\<close>
|
Hence the \<^term>\<open>int1\<close> invariant is checked when the instance @{docitem testinv2} is defined.\<close>
|
||||||
|
|
||||||
|
text\<open>Test invariant for attributes of attributes: \<close>
|
||||||
|
|
||||||
|
doc_class inv_test1 =
|
||||||
|
a :: int
|
||||||
|
|
||||||
|
doc_class inv_test2 =
|
||||||
|
b :: "inv_test1"
|
||||||
|
c:: int
|
||||||
|
invariant inv_test2 :: "c \<sigma> = 1"
|
||||||
|
invariant inv_test2' :: "a (b \<sigma>) = 2"
|
||||||
|
|
||||||
|
doc_class inv_test3 = inv_test1 +
|
||||||
|
b :: "inv_test1"
|
||||||
|
c:: int
|
||||||
|
invariant inv_test3 :: "a \<sigma> = 1"
|
||||||
|
invariant inv_test3' :: "a (b \<sigma>) = 2"
|
||||||
|
|
||||||
|
text\<open>To support invariant on attributes in attributes
|
||||||
|
and invariant on attributes of the superclasses,
|
||||||
|
we check that the type of the attribute of the subclass is ground:\<close>
|
||||||
|
ML\<open>
|
||||||
|
val Type(st, [ty]) = \<^typ>\<open>inv_test1\<close>
|
||||||
|
val Type(st', [ty']) = \<^typ>\<open>'a inv_test1_scheme\<close>
|
||||||
|
val t = ty = \<^typ>\<open>unit\<close>
|
||||||
|
\<close>
|
||||||
|
|
||||||
text\<open>Now assume the following ontology:\<close>
|
text\<open>Now assume the following ontology:\<close>
|
||||||
|
|
||||||
doc_class title =
|
doc_class title =
|
||||||
|
|
Reference in New Issue