Add checking of invariants for class instances
- Warning: the current implementation does yet not support
some use-cases, like invariant on monitors,
or the initialization of docitem without a class associated.
- Add first draft of the checking of invariants.
For now, it is disabled by default because some cases
are not yet supported, like the initialization of docitem
without a class associated.
ex: text*[sdf]‹ Lorem ipsum @{thm refl}›
- To enable the checking, one can use the theory attribute
"invariants_checking" by declaring it in a theory like this:
declare [[invariants_strict_checking = true]]
- A checking using basic tactics (unfolding and auto) can be enable
with the "invariants_checking_with_tactics" theory attribute
for specific use-cases
- The specification of invariants is now automatically abstracted,
so one must define an invariant like this now:
doc_class W =
w::"int"
invariant w :: "w σ ≥ 3"
The old form:
doc_class W =
w::"int"
invariant w :: "λσ. w σ ≥ 3"
is now deprecated.
The specification of the invariant still uses the σ-notation
and is defined globally by the name component "invariantN"
- Update the invariants definition in the theories to match
the new implementation
- Update the manual to explain this new feature
- Add small examples in src/tests/High_Level_Syntax_Invariants.thy
and src/tests/Ontology_Matching_Example.thy
This commit is contained in:
Nicolas Méric
parent
96112ff893
commit
76612ae6f3
|
|
@ -234,15 +234,16 @@ A document class\<^bindex>\<open>document class\<close> can be defined using the
|
|||
We call document classes with an \<open>accepts_clause\<close>
|
||||
\<^emph>\<open>monitor classes\<close> or \<^emph>\<open>monitors\<close> for short.
|
||||
\<^rail>\<open> @@{command "doc_class"} class_id '=' (class_id '+')? (attribute_decl+) \<newline>
|
||||
(invariant_decl*)
|
||||
(invariant_decl?)
|
||||
(accepts_clause rejects_clause?)?\<close>
|
||||
\<^item> \<open>attribute_decl\<close>:\<^index>\<open>attribute\_decl@\<open>attribute_decl\<close>\<close>
|
||||
\<^rail>\<open> name '::' '"' type '"' default_clause? \<close>
|
||||
\<^item> \<open>invariant_decl\<close>:\<^index>\<open>invariant\_decl@\<open>invariant_decl\<close>\<close>
|
||||
Invariants can be specified as predicates over document classes represented as
|
||||
records in HOL. Note that sufficient type information must be provided in order to
|
||||
disambiguate the argument of the \<open>\<lambda>\<close>-expression.
|
||||
\<^rail>\<open> 'inv' (name '::')? '"' term '"' \<close>
|
||||
disambiguate the argument of the expression
|
||||
and the \<^boxed_text>\<open>\<sigma>\<close> symbol is reserved to reference the instance of the class itself.
|
||||
\<^rail>\<open> 'invariant' name '::' '"' term '"' + 'and' \<close>
|
||||
\<^item> \<open>accepts_clause\<close>:\<^index>\<open>accepts\_clause@\<open>accepts_clause\<close>\<close>
|
||||
\<^rail>\<open> 'accepts' '"' regexpr '"'\<close>
|
||||
\<^item> \<open>rejects_clause\<close>:\<^index>\<open>rejects\_clause@\<open>rejects_clause\<close>\<close>
|
||||
|
|
@ -900,39 +901,43 @@ schemata:
|
|||
|
||||
|
||||
section*["sec:advanced"::technical]\<open>Advanced ODL Concepts\<close>
|
||||
text\<open>This section will be based on the following example.\<close>
|
||||
|
||||
text\<open>For example, assume the following local ontology:
|
||||
subsection*["sec:example"::technical]\<open>Example\<close>
|
||||
text\<open>Assume the following local ontology:
|
||||
|
||||
@{boxed_theory_text [display] \<open>
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class title =
|
||||
short_title :: "string option" <= "None"
|
||||
doc_class author = email :: "string" <= "''''"
|
||||
short_title :: "string option" <= "None"
|
||||
doc_class author =
|
||||
email :: "string" <= "''''"
|
||||
datatype classification = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
|
||||
doc_class abstract =
|
||||
keywordlist :: "string list" <= [] safety_level :: "classification" <= "SIL3"
|
||||
keywordlist :: "string list" <= "[]"
|
||||
safety_level :: "classification" <= "SIL3"
|
||||
doc_class text_section =
|
||||
authored_by :: "author set" <= "{}" level :: "int option" <= "None"
|
||||
authored_by :: "author set" <= "{}"
|
||||
level :: "int option" <= "None"
|
||||
type_synonym notion = string
|
||||
doc_class introduction = text_section +
|
||||
authored_by :: "author set" <= "UNIV"
|
||||
uses :: "notion set"
|
||||
authored_by :: "author set" <= "UNIV"
|
||||
uses :: "notion set"
|
||||
doc_class claim = introduction +
|
||||
based_on :: "notion list"
|
||||
based_on :: "notion list"
|
||||
doc_class technical = text_section +
|
||||
formal_results :: "thm list"
|
||||
formal_results :: "thm list"
|
||||
doc_class "definition" = technical +
|
||||
is_formal :: "bool"
|
||||
property :: "term list" <= "[]"
|
||||
datatype kind = expert_opinion | argument | proof
|
||||
is_formal :: "bool"
|
||||
property :: "term list" <= "[]"
|
||||
datatype kind = expert_opinion | argument | "proof"
|
||||
doc_class result = technical +
|
||||
evidence :: kind
|
||||
property :: "thm list" <= "[]"
|
||||
evidence :: kind
|
||||
property :: "thm list" <= "[]"
|
||||
doc_class example = technical +
|
||||
referring_to :: "(notion + definition) set" <= "{}"
|
||||
referring_to :: "(notion + definition) set" <= "{}"
|
||||
doc_class "conclusion" = text_section +
|
||||
establish :: "(claim \<times> result) set"
|
||||
\<close>
|
||||
}
|
||||
establish :: "(claim \<times> result) set"
|
||||
\<close>}
|
||||
\<close>
|
||||
|
||||
subsection\<open>Meta-types as Types\<close>
|
||||
|
|
@ -950,20 +955,101 @@ text\<open>
|
|||
conventional type-checking that this string represents actually a
|
||||
defined entity in the context of the system state
|
||||
\<^boxed_theory_text>\<open>\<theta>\<close>. For example, the \<^boxed_theory_text>\<open>establish\<close>
|
||||
attribute in the previous section is the power of the ODL: here, we model
|
||||
attribute in our example is the power of the ODL: here, we model
|
||||
a relation between \<^emph>\<open>claims\<close> and \<^emph>\<open>results\<close> which may be a
|
||||
formal, machine-check theorem of type \<^ML_type>\<open>thm\<close> denoted by, for
|
||||
example: \<^boxed_theory_text>\<open>property = "[@{thm "system_is_safe"}]"\<close> in a
|
||||
system context \<^boxed_theory_text>\<open>\<theta>\<close> where this theorem is
|
||||
established. Similarly, attribute values like
|
||||
\<^boxed_theory_text>\<open>property = "@{term \<open>A \<leftrightarrow> B\<close>}"\<close>
|
||||
require that the HOL-string \<^boxed_theory_text>\<open>A \<leftrightarrow> B\<close> is
|
||||
\<^boxed_theory_text>\<open>property = "@{term \<open>A \<longleftrightarrow> B\<close>}"\<close>
|
||||
require that the HOL-string \<^boxed_theory_text>\<open>A \<longleftrightarrow> B\<close> is
|
||||
again type-checked and represents indeed a formula in \<open>\<theta>\<close>. Another instance of
|
||||
this process, which we call \<open>second-level type-checking\<close>, are term-constants
|
||||
generated from the ontology such as
|
||||
\<^boxed_theory_text>\<open>@{definition <string>}\<close>.
|
||||
\<close>
|
||||
|
||||
(*<*)
|
||||
declare_reference*["sec:monitors"::technical]
|
||||
declare_reference*["sec:low_level_inv"::technical]
|
||||
(*>*)
|
||||
|
||||
subsection*["sec:class_inv"::technical]\<open>ODL Class Invariants\<close>
|
||||
|
||||
|
||||
text\<open>
|
||||
Ontological classes as described so far are too liberal in many situations.
|
||||
There is a first high-level syntax implementation for class invariants.
|
||||
These invariants can be checked when an instance of the class is defined.
|
||||
To enable the checking of the invariants, the \<^boxed_theory_text>\<open>invariants_checking\<close>
|
||||
theory attribute must be set:
|
||||
@{boxed_theory_text [display]\<open>
|
||||
declare[[invariants_checking = true]]\<close>}
|
||||
|
||||
For example, let's define the following two classes:
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class class_inv1 =
|
||||
int1 :: "int"
|
||||
invariant inv1 :: "int1 \<sigma> \<ge> 3"
|
||||
|
||||
doc_class class_inv2 = class_inv1 +
|
||||
int2 :: "int"
|
||||
invariant inv2 :: "int2 \<sigma> < 2"
|
||||
\<close>}
|
||||
|
||||
The \<^boxed_theory_text>\<open>\<sigma>\<close> symbol is reserved and references the future instance class.
|
||||
By relying on the implementation of the Records
|
||||
in Isabelle/HOL~@{cite "wenzel:isabelle-isar:2020"},
|
||||
one can reference an attribute of an instance using its selector function.
|
||||
For example, \<^boxed_theory_text>\<open>int1 \<sigma>\<close> denotes the value
|
||||
of the \<^boxed_theory_text>\<open>int1\<close> attribute
|
||||
of the future instance of the class \<^boxed_theory_text>\<open>class_inv1\<close>.
|
||||
|
||||
Now let's define two instances, one of each class:
|
||||
|
||||
@{boxed_theory_text [display]\<open>
|
||||
text*[testinv1::class_inv1, int1=4]\<open>lorem ipsum...\<close>
|
||||
text*[testinv2::class_inv2, int1=3, int2=1]\<open>lorem ipsum...\<close>
|
||||
\<close>}
|
||||
|
||||
The value of each attribute defined for the instances is checked against their classes invariants.
|
||||
As the class \<^boxed_theory_text>\<open>class_inv2\<close> is a subsclass
|
||||
of the class \<^boxed_theory_text>\<open>class_inv1\<close>, it inherits \<^boxed_theory_text>\<open>class_inv1\<close> invariants.
|
||||
Hence the \<^boxed_theory_text>\<open>inv1\<close> invariant is checked
|
||||
when the instance \<^boxed_theory_text>\<open>testinv2\<close> is defined.
|
||||
|
||||
Now let's add some invariants to our example in \<^technical>\<open>sec:example\<close>.
|
||||
For example, one
|
||||
would like to express that any instance of a \<^boxed_theory_text>\<open>result\<close> class finally has
|
||||
a non-empty property list, if its \<^boxed_theory_text>\<open>kind\<close> is \<^boxed_theory_text>\<open>proof\<close>, or that
|
||||
the \<^boxed_theory_text>\<open>establish\<close> relation between \<^boxed_theory_text>\<open>claim\<close> and
|
||||
\<^boxed_theory_text>\<open>result\<close> is total.
|
||||
In a high-level syntax, this type of constraints could be expressed, \<^eg>, by:
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class introduction = text_section +
|
||||
authored_by :: "author set" <= "UNIV"
|
||||
uses :: "notion set"
|
||||
invariant author_finite :: "finite (authored_by \<sigma>)"
|
||||
doc_class result = technical +
|
||||
evidence :: kind
|
||||
property :: "thm list" <= "[]"
|
||||
invariant has_property :: "evidence \<sigma> = proof \<longleftrightarrow> property \<sigma> \<noteq> []"
|
||||
doc_class example = technical +
|
||||
referring_to :: "(notion + definition) set" <= "{}"
|
||||
doc_class conclusion = text_section +
|
||||
establish :: "(claim \<times> result) set"
|
||||
invariant total_rel :: "\<forall> x. x \<in> Domain (establish \<sigma>)
|
||||
\<longrightarrow> (\<exists> y \<in> Range (establish \<sigma>). (x, y) \<in> establish \<sigma>)"
|
||||
\<close>}
|
||||
All specified constraints are already checked in the IDE of \<^dof> while editing.
|
||||
The invariant \<^boxed_theory_text>\<open>author_finite\<close> enforces that the user sets the
|
||||
\<^boxed_theory_text>\<open>authored_by\<close> set.
|
||||
There are still some limitations with this high-level syntax.
|
||||
For now, the high-level syntax does not support monitors (see \<^technical>\<open>sec:monitors\<close>).
|
||||
For example, one would like to delay a final error message till the
|
||||
closing of a monitor.
|
||||
For this use-case you can use low-level class invariants (see \<^technical>\<open>sec:low_level_inv\<close>).
|
||||
\<close>
|
||||
|
||||
subsection*["sec:monitors"::technical]\<open>ODL Monitors\<close>
|
||||
text\<open>
|
||||
|
|
@ -1014,49 +1100,33 @@ text\<open>
|
|||
smaller than the others. Thus, an introduction is forced to have a
|
||||
header delimiting the borders of its representation. Class invariants
|
||||
on monitors allow for specifying structural properties on document
|
||||
sections.\<close>
|
||||
sections.
|
||||
For now, the high-level syntax of invariants is not supported for monitors and you must use the
|
||||
the low-level class invariants (see \<^technical>\<open>sec:low_level_inv\<close>.\<close>
|
||||
|
||||
|
||||
subsection*["sec:class_inv"::technical]\<open>ODL Class Invariants\<close>
|
||||
|
||||
subsection*["sec:low_level_inv"::technical]\<open>ODL Low-level Class Invariants\<close>
|
||||
|
||||
text\<open>
|
||||
Ontological classes as described so far are too liberal in many situations. For example, one
|
||||
would like to express that any instance of a \<^boxed_theory_text>\<open>result\<close> class finally has a
|
||||
non-empty property list, if its \<^boxed_theory_text>\<open>kind\<close> is \<^boxed_theory_text>\<open>proof\<close>, or that
|
||||
the \<^boxed_theory_text>\<open>establish\<close> relation between \<^boxed_theory_text>\<open>claim\<close> and
|
||||
\<^boxed_theory_text>\<open>result\<close> is surjective.
|
||||
|
||||
In a high-level syntax, this type of constraints could be expressed, \<^eg>, by:
|
||||
|
||||
@{boxed_theory_text [display]\<open>
|
||||
(* 1 *) \<forall> x \<in> result. x@evidence = proo$$f \<leftrightarrow> x@property \<noteq> []
|
||||
(* 2 *) \<forall> x \<in> conclusion. \<forall> y \<in> Domain(x@establish)
|
||||
\<rightarrow> \<exists> y \<in> Range(x@establish). (y,z) \<in> x@establish
|
||||
(* 3 *) \<forall> x \<in> introduction. finite(x@authored_by)
|
||||
\<close>}
|
||||
|
||||
where \<^boxed_theory_text>\<open>result\<close>, \<^boxed_theory_text>\<open>conclusion\<close>, and \<^boxed_theory_text>\<open>introduction\<close> are the set of
|
||||
all possible instances of these document classes. All specified constraints are already checked
|
||||
in the IDE of \<^dof> while editing; it is however possible to delay a final error message till the
|
||||
closing of a monitor (see next section). The third constraint enforces that the user sets the
|
||||
\<^boxed_theory_text>\<open>authored_by\<close> set, otherwise an error will be reported.
|
||||
|
||||
For the moment, there is no high-level syntax for the definition of class invariants. A
|
||||
formulation, in SML, of the first class-invariant in \<^technical>\<open>sec:class_inv\<close> is straight-forward:
|
||||
If one want to go over the limitations of the actual high-level syntax of the invariant,
|
||||
one can define a function using SML.
|
||||
A formulation, in SML, of the class-invariant \<^boxed_theory_text>\<open>has_property\<close>
|
||||
in \<^technical>\<open>sec:class_inv\<close>, defined in the supposedly \<open>Low_Level_Syntax_Invariants\<close> theory
|
||||
(note the long name of the class),
|
||||
is straight-forward:
|
||||
|
||||
\begin{sml}
|
||||
fun check_result_inv oid {is_monitor:bool} ctxt =
|
||||
let val kind = compute_attr_access ctxt "kind" oid <@>{here} <@>{here}
|
||||
val prop = compute_attr_access ctxt "property" oid <@>{here} <@>{here}
|
||||
let val kind = AttributeAccess.compute_attr_access ctxt "evidence" oid <@>{here} <@>{here}
|
||||
val prop = AttributeAccess.compute_attr_access ctxt "property" oid <@>{here} <@>{here}
|
||||
val tS = HOLogic.dest_list prop
|
||||
in case kind_term of
|
||||
in case kind of
|
||||
<@>{term "proof"} => if not(null tS) then true
|
||||
else error("class result invariant violation")
|
||||
| _ => false
|
||||
end
|
||||
val _ = Theory.setup (DOF_core.update_class_invariant
|
||||
"tiny_cert.result" check_result_inv)
|
||||
"Low_Level_Syntax_Invariants.result" check_result_inv)
|
||||
\end{sml}
|
||||
|
||||
The \<^ML>\<open>Theory.setup\<close>-command (last line) registers the \<^boxed_theory_text>\<open>check_result_inv\<close> function
|
||||
|
|
|
|||
|
|
@ -180,27 +180,7 @@ text\<open>
|
|||
|
||||
section\<open>Programming Class Invariants\<close>
|
||||
text\<open>
|
||||
For the moment, there is no high-level syntax for the definition of class invariants. A
|
||||
formulation, in SML, of the first class-invariant in @{docitem "sec:class_inv"} is straight-forward:
|
||||
|
||||
@{boxed_sml [display]
|
||||
\<open>fun check_result_inv oid {is_monitor:bool} ctxt =
|
||||
let val kind = compute_attr_access ctxt "kind" oid <@>{here} <@>{here}
|
||||
val prop = compute_attr_access ctxt "property" oid <@>{here} <@>{here}
|
||||
val tS = HOLogic.dest_list prop
|
||||
in case kind_term of
|
||||
<@>{term "proof"} => if not(null tS) then true
|
||||
else error("class result invariant violation")
|
||||
| _ => false
|
||||
end
|
||||
val _ = Theory.setup (DOF_core.update_class_invariant
|
||||
"tiny_cert.result" check_result_inv)\<close>}
|
||||
|
||||
The \<^boxed_sml>\<open>setup\<close>-command (last line) registers the \<^boxed_theory_text>\<open>check_result_inv\<close> function
|
||||
into the \<^isadof> kernel, which activates any creation or modification of an instance of
|
||||
\<^boxed_theory_text>\<open>result\<close>. We cannot replace \<^boxed_theory_text>\<open>compute_attr_access\<close> by the corresponding
|
||||
antiquotation \<^boxed_theory_text>\<open>@{docitem_value kind::oid}\<close>, since \<^boxed_theory_text>\<open>oid\<close> is
|
||||
bound to a variable here and can therefore not be statically expanded.
|
||||
See \<^technical>\<open>sec:low_level_inv\<close>.
|
||||
\<close>
|
||||
|
||||
section\<open>Implementing Monitors\<close>
|
||||
|
|
|
|||
|
|
@ -63,8 +63,14 @@ val docclassN = "doc_class";
|
|||
|
||||
(** name components **)
|
||||
|
||||
val makeN = "make";
|
||||
val defN = "def"
|
||||
val def_suffixN = "_" ^ defN
|
||||
val defsN = defN ^ "s"
|
||||
val instances_of_suffixN = "_instances"
|
||||
val invariant_suffixN = "_inv"
|
||||
val invariantN = "\<sigma>"
|
||||
val makeN = "make"
|
||||
val schemeN = "_scheme"
|
||||
|
||||
(* derived from: theory_markup *)
|
||||
fun docref_markup_gen refN def name id pos =
|
||||
|
|
@ -534,13 +540,13 @@ fun get_object_local oid ctxt = case get_object_local_opt oid ctxt of
|
|||
|SOME(bbb) => bbb
|
||||
|
||||
fun get_doc_class_global cid thy =
|
||||
if cid = default_cid then error("default class acces") (* TODO *)
|
||||
if cid = default_cid then error("default class access") (* TODO *)
|
||||
else let val t = #docclass_tab(get_data_global thy)
|
||||
in (Symtab.lookup t cid) end
|
||||
|
||||
|
||||
fun get_doc_class_local cid ctxt =
|
||||
if cid = default_cid then error("default class acces") (* TODO *)
|
||||
if cid = default_cid then error("default class access") (* TODO *)
|
||||
else let val t = #docclass_tab(get_data ctxt)
|
||||
in (Symtab.lookup t cid) end
|
||||
|
||||
|
|
@ -799,11 +805,20 @@ val _ =
|
|||
val (strict_monitor_checking, strict_monitor_checking_setup)
|
||||
= Attrib.config_bool \<^binding>\<open>strict_monitor_checking\<close> (K false);
|
||||
|
||||
val (invariants_checking, invariants_checking_setup)
|
||||
= Attrib.config_bool \<^binding>\<open>invariants_checking\<close> (K false);
|
||||
|
||||
val (invariants_checking_with_tactics, invariants_checking_with_tactics_setup)
|
||||
= Attrib.config_bool \<^binding>\<open>invariants_checking_with_tactics\<close> (K false);
|
||||
|
||||
|
||||
end (* struct *)
|
||||
|
||||
\<close>
|
||||
|
||||
setup\<open>DOF_core.strict_monitor_checking_setup\<close>
|
||||
setup\<open>DOF_core.strict_monitor_checking_setup
|
||||
#> DOF_core.invariants_checking_setup
|
||||
#> DOF_core.invariants_checking_with_tactics_setup\<close>
|
||||
|
||||
section\<open> Syntax for Term Annotation Antiquotations (TA)\<close>
|
||||
|
||||
|
|
@ -1121,7 +1136,6 @@ fun declare_class_instances_annotation thy doc_class_name =
|
|||
val qual = Long_Name.qualifier long_name
|
||||
val transformer_name = Long_Name.qualify qual
|
||||
(DOF_core.get_doc_class_name_without_ISA_prefix (Binding.name_of bind'))
|
||||
val _ = writeln ("transformer_name: " ^ transformer_name)
|
||||
in
|
||||
DOF_core.update_isa_global (transformer_name,
|
||||
{check=check_identity, elaborate= elaborate_instances_list}) thy end)
|
||||
|
|
@ -1258,7 +1272,6 @@ fun cid_2_cidType cid_long thy =
|
|||
fun fathers cid_long = case Symtab.lookup t cid_long of
|
||||
NONE => let val ctxt = Proof_Context.init_global thy
|
||||
val tty = Syntax.parse_typ (Proof_Context.init_global thy) cid_long
|
||||
val _ = writeln ("XXX"^(Syntax.string_of_typ ctxt tty))
|
||||
in error("undefined doc class id :"^cid_long)
|
||||
end
|
||||
| SOME ({inherits_from=NONE, ...}) => [cid_long]
|
||||
|
|
@ -1413,9 +1426,59 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy =
|
|||
DOF_core.map_data_global(update_automatons)
|
||||
end
|
||||
|
||||
fun check_invariants thy oid =
|
||||
let
|
||||
val value = the (DOF_core.get_value_global oid thy)
|
||||
val cid = #cid (the (DOF_core.get_object_global oid thy))
|
||||
fun get_all_invariants cid thy =
|
||||
let val invs = #invs (the (DOF_core.get_doc_class_global cid thy))
|
||||
in case DOF_core.get_doc_class_global cid thy of
|
||||
NONE => error("undefined class id for invariants: " ^ cid)
|
||||
| SOME ({inherits_from=NONE, ...}) => invs
|
||||
| SOME ({inherits_from=SOME(_,father), ...}) => (invs) @ (get_all_invariants father thy)
|
||||
end
|
||||
val invariants = get_all_invariants cid thy
|
||||
val inv_and_apply_list =
|
||||
let fun mk_inv_and_apply inv value thy =
|
||||
let val ((s, pos), _ (*term*)) = inv
|
||||
val inv_def = Syntax.read_term_global thy (s ^ invariant_suffixN)
|
||||
val inv_def_typ = Term.type_of value
|
||||
in case inv_def of
|
||||
Const (s, Type (st, [_ (*ty*), ty'])) =>
|
||||
((s, pos), Const (s, Type (st,[inv_def_typ, ty'])) $ value)
|
||||
| _ => ((s, pos), inv_def $ value)
|
||||
end
|
||||
in map (fn inv => mk_inv_and_apply inv value thy) invariants
|
||||
end
|
||||
fun check_invariants' ((inv_name, pos), term) =
|
||||
let val ctxt = Proof_Context.init_global thy
|
||||
val evaluated_term = Value_Command.value ctxt term
|
||||
handle ERROR e =>
|
||||
if (String.isSubstring "Wellsortedness error" e)
|
||||
andalso (Config.get_global thy DOF_core.invariants_checking_with_tactics)
|
||||
then (warning("Invariants checking uses proof tactics");
|
||||
let val prop_term = HOLogic.mk_Trueprop term
|
||||
val thms = Proof_Context.get_thms ctxt (inv_name ^ def_suffixN)
|
||||
(* Get the make definition (def(1) of the record) *)
|
||||
val thms' =
|
||||
(Proof_Context.get_thms ctxt (Long_Name.append cid defsN)) @ thms
|
||||
val _ = Goal.prove ctxt [] [] prop_term
|
||||
(K ((unfold_tac ctxt thms') THEN (auto_tac ctxt)))
|
||||
|> Thm.close_derivation \<^here>
|
||||
(* If Goal.prove does not fail, then the evaluation is considered True,
|
||||
else an error is triggered by Goal.prove *)
|
||||
in @{term True} end)
|
||||
else (error e)
|
||||
in (if evaluated_term = \<^term>\<open>True\<close>
|
||||
then ((inv_name, pos), term)
|
||||
else ISA_core.err ("Invariant " ^ inv_name ^ " violated") pos)
|
||||
end
|
||||
val _ = map check_invariants' inv_and_apply_list
|
||||
in thy end
|
||||
|
||||
fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos doc_attrs thy =
|
||||
let val id = serial ();
|
||||
let
|
||||
val id = serial ();
|
||||
val _ = Position.report pos (docref_markup true oid id pos);
|
||||
(* creates a markup label for this position and reports it to the PIDE framework;
|
||||
this label is used as jump-target for point-and-click feature. *)
|
||||
|
|
@ -1442,7 +1505,8 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do
|
|||
val (value_term', _(*ty*), _) = calc_update_term thy cid_long assns' defaults
|
||||
in value_term' end
|
||||
val check_inv = (DOF_core.get_class_invariant cid_long thy oid is_monitor)
|
||||
o Context.Theory
|
||||
o Context.Theory
|
||||
|
||||
in thy |> DOF_core.define_object_global (oid, {pos = pos,
|
||||
thy_name = Context.theory_name thy,
|
||||
value = value_term,
|
||||
|
|
@ -1452,6 +1516,9 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do
|
|||
vcid = vcid})
|
||||
|> register_oid_cid_in_open_monitors oid pos cid_long
|
||||
|> (fn thy => (check_inv thy; thy))
|
||||
|> (fn thy => if Config.get_global thy DOF_core.invariants_checking = true
|
||||
then check_invariants thy oid
|
||||
else thy)
|
||||
end
|
||||
|
||||
|
||||
|
|
@ -2134,15 +2201,39 @@ fun mk_meta_eq (t, u) = meta_eq_const (fastype_of t) $ t $ u;
|
|||
|
||||
fun define_cond binding f_sty cond_suffix read_cond (ctxt:local_theory) =
|
||||
let val bdg = Binding.suffix_name cond_suffix binding
|
||||
val eq = mk_meta_eq(Free(Binding.name_of bdg, f_sty),read_cond ctxt)
|
||||
val eq = mk_meta_eq(Free(Binding.name_of bdg, f_sty),read_cond)
|
||||
val args = (SOME(bdg,NONE,NoSyn), (Binding.empty_atts,eq),[],[])
|
||||
in def_cmd args true ctxt end
|
||||
|
||||
fun define_inv cid_long ((lbl, pos), inv) thy =
|
||||
let val bdg = (* Binding.suffix_name cid_long *) (Binding.make (lbl,pos))
|
||||
fun inv_term ctxt = Syntax.read_term ctxt inv
|
||||
val inv_ty = (Syntax.read_typ_global thy cid_long) --> HOLogic.boolT
|
||||
in thy |> Named_Target.theory_map (define_cond bdg inv_ty "_inv" inv_term) end
|
||||
let val bdg = Binding.make (lbl,pos)
|
||||
val inv_term = Syntax.read_term (Proof_Context.init_global thy) inv
|
||||
fun update_attribute_type thy class_scheme_ty
|
||||
(Const (s, Type (st,[ty, ty'])) $ t) =
|
||||
let
|
||||
val cid = Long_Name.qualifier s
|
||||
in case DOF_core.get_doc_class_global cid thy of
|
||||
NONE => Const (s, Type(st,[ty, ty']))
|
||||
$ (update_attribute_type thy class_scheme_ty t)
|
||||
| SOME _ => Const(s, Type(st,[class_scheme_ty, ty']))
|
||||
$ (update_attribute_type thy class_scheme_ty t)
|
||||
end
|
||||
| update_attribute_type thy class_scheme_ty (t $ t') =
|
||||
(update_attribute_type thy class_scheme_ty t)
|
||||
$ (update_attribute_type thy class_scheme_ty t')
|
||||
| update_attribute_type thy class_scheme_ty (Abs(s, ty, t)) =
|
||||
Abs(s, ty, update_attribute_type thy class_scheme_ty t)
|
||||
| update_attribute_type _ class_scheme_ty (Free(s, ty)) = if s = invariantN
|
||||
then Free (s, class_scheme_ty)
|
||||
else Free (s, ty)
|
||||
| update_attribute_type _ _ t = t
|
||||
val inv_ty = Syntax.read_typ (Proof_Context.init_global thy) ("'a " ^ cid_long ^ schemeN)
|
||||
(* Update the type of each attribute update function to match the type of the
|
||||
current class. *)
|
||||
val inv_term' = update_attribute_type thy inv_ty inv_term
|
||||
val eq_inv_ty = inv_ty --> HOLogic.boolT
|
||||
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
|
||||
|
||||
fun add_doc_class_cmd overloaded (raw_params, binding)
|
||||
raw_parent raw_fieldsNdefaults reject_Atoms regexps invariants thy =
|
||||
|
|
|
|||
|
|
@ -118,9 +118,9 @@ doc_class F =
|
|||
to an association class. It can be used to track
|
||||
claims to result - relations, for example.*)
|
||||
b' :: "(A \<times> C) list" <= "[]"
|
||||
invariant br :: "\<lambda>\<sigma>::F. r \<sigma> \<noteq> [] \<and> card(b \<sigma>) \<ge> 3"
|
||||
and br':: "\<lambda>\<sigma>::F. r \<sigma> \<noteq> [] \<and> length(b' \<sigma>) \<ge> 3"
|
||||
and cr :: "\<lambda>\<sigma>::F. properties \<sigma> \<noteq> []"
|
||||
invariant br :: "r \<sigma> \<noteq> [] \<and> card(b \<sigma>) \<ge> 3"
|
||||
and br':: "r \<sigma> \<noteq> [] \<and> length(b' \<sigma>) \<ge> 3"
|
||||
and cr :: "properties \<sigma> \<noteq> []"
|
||||
|
||||
text\<open>The effect of the invariant declaration is to provide intern definitions for validation
|
||||
functions of this invariant. They can be referenced as follows:\<close>
|
||||
|
|
|
|||
|
|
@ -137,7 +137,7 @@ doc_class technical = text_section +
|
|||
definition_list :: "string list" <= "[]"
|
||||
status :: status <= "description"
|
||||
formal_results :: "thm list"
|
||||
invariant L1 :: "\<lambda>\<sigma>::technical. the (level \<sigma>) > 0"
|
||||
invariant L1 :: "the (level \<sigma>) > 0"
|
||||
|
||||
type_synonym tc = technical (* technical content *)
|
||||
|
||||
|
|
@ -186,8 +186,8 @@ doc_class math_content = tc +
|
|||
short_name :: string <= "''''"
|
||||
status :: status <= "semiformal"
|
||||
mcc :: "math_content_class" <= "thm"
|
||||
invariant s1 :: "\<lambda> \<sigma>::math_content. \<not>referentiable \<sigma> \<longrightarrow> short_name \<sigma> = ''''"
|
||||
invariant s2 :: "\<lambda> \<sigma>::math_content. technical.status \<sigma> = semiformal"
|
||||
invariant s1 :: "\<not>referentiable \<sigma> \<longrightarrow> short_name \<sigma> = ''''"
|
||||
invariant s2 :: "technical.status \<sigma> = semiformal"
|
||||
type_synonym math_tc = math_content
|
||||
|
||||
text\<open>The class \<^typ>\<open>math_content\<close> is perhaps more adequaltely described as "math-alike content".
|
||||
|
|
@ -236,27 +236,28 @@ text\<open>The key class definitions are motivated by the AMS style.\<close>
|
|||
doc_class "definition" = math_content +
|
||||
referentiable :: bool <= True
|
||||
mcc :: "math_content_class" <= "defn"
|
||||
invariant d1 :: "\<lambda> \<sigma>::definition. mcc \<sigma> = defn" (* can not be changed anymore. *)
|
||||
invariant d1 :: "mcc \<sigma> = defn" (* can not be changed anymore. *)
|
||||
|
||||
|
||||
doc_class "theorem" = math_content +
|
||||
referentiable :: bool <= True
|
||||
mcc :: "math_content_class" <= "thm"
|
||||
invariant d2 :: "\<lambda> \<sigma>::theorem. mcc \<sigma> = thm"
|
||||
invariant d2 :: "mcc \<sigma> = thm"
|
||||
|
||||
doc_class "lemma" = math_content +
|
||||
referentiable :: bool <= "True"
|
||||
mcc :: "math_content_class" <= "lem"
|
||||
invariant d3 :: "\<lambda> \<sigma>::lemma. mcc \<sigma> = lem"
|
||||
invariant d3 :: "mcc \<sigma> = lem"
|
||||
|
||||
doc_class "corollary" = math_content +
|
||||
referentiable :: bool <= "True"
|
||||
mcc :: "math_content_class" <= "cor"
|
||||
invariant d4 :: "\<lambda> \<sigma>::corollary. mcc \<sigma> = thm"
|
||||
invariant d4 :: "mcc \<sigma> = thm"
|
||||
|
||||
doc_class "math_example" = math_content +
|
||||
referentiable :: bool <= "True"
|
||||
mcc :: "math_content_class" <= "expl"
|
||||
invariant d5 :: "\<lambda> \<sigma>::math_example. mcc \<sigma> = expl"
|
||||
invariant d5 :: "mcc \<sigma> = expl"
|
||||
|
||||
|
||||
subsubsection\<open>Ontological Macros \<^verbatim>\<open>Definition*\<close> , \<^verbatim>\<open>Lemma**\<close>, \<^verbatim>\<open>Theorem*\<close> ... \<close>
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@
|
|||
chapter\<open>Setting and modifying attributes of doc-items\<close>
|
||||
|
||||
theory
|
||||
Concept_ExampleInvariant
|
||||
Concept_Example_Low_Level_Invariant
|
||||
imports
|
||||
"Isabelle_DOF.Conceptual" (* we use the generic "Conceptual" ontology *)
|
||||
begin
|
||||
|
|
@ -0,0 +1,114 @@
|
|||
chapter\<open>High level syntax Invariants\<close>
|
||||
|
||||
theory High_Level_Syntax_Invariants
|
||||
imports "Isabelle_DOF.Isa_DOF"
|
||||
begin
|
||||
|
||||
text\<open>
|
||||
Ontological classes as described so far are too liberal in many situations.
|
||||
There is a first high-level syntax implementation for class invariants.
|
||||
These invariants can be checked when an instance of the class is defined.
|
||||
To enable the checking of the invariants, the \<open>invariants_checking\<close>
|
||||
theory attribute must be set:\<close>
|
||||
|
||||
|
||||
declare[[invariants_checking = true]]
|
||||
|
||||
text\<open>For example, let's define the following two classes:\<close>
|
||||
|
||||
doc_class class_inv1 =
|
||||
int1 :: "int"
|
||||
invariant inv1 :: "int1 \<sigma> \<ge> 3"
|
||||
|
||||
doc_class class_inv2 = class_inv1 +
|
||||
int2 :: "int"
|
||||
invariant inv2 :: "int2 \<sigma> < 2"
|
||||
|
||||
text\<open>The symbol \<^term>\<open>\<sigma>\<close> is reserved and references the future instance class.
|
||||
By relying on the implementation of the Records
|
||||
in Isabelle/HOL~@{cite "wenzel:isabelle-isar:2020"},
|
||||
one can reference an attribute of an instance using its selector function.
|
||||
For example, \<^term>\<open>int1 \<sigma>\<close> denotes the value
|
||||
of the \<^term>\<open>int1\<close> attribute
|
||||
of the future instance of the class @{doc_class class_inv1}.
|
||||
Now let's define two instances, one of each class:\<close>
|
||||
|
||||
text*[testinv1::class_inv1, int1=4]\<open>lorem ipsum...\<close>
|
||||
text*[testinv2::class_inv2, int1=3, int2=1]\<open>lorem ipsum...\<close>
|
||||
|
||||
text\<open>
|
||||
The value of each attribute defined for the instances is checked against their classes invariants.
|
||||
As the class @{doc_class class_inv2} is a subsclass of the class @{doc_class class_inv1},
|
||||
it inherits @{doc_class class_inv1} invariants.
|
||||
Hence the \<^term>\<open>int1\<close> invariant is checked when the instance @{docitem testinv2} is defined.\<close>
|
||||
|
||||
text\<open>Now assume the following ontology:\<close>
|
||||
|
||||
doc_class title =
|
||||
short_title :: "string option" <= "None"
|
||||
|
||||
doc_class author =
|
||||
email :: "string" <= "''''"
|
||||
|
||||
datatype classification = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
|
||||
|
||||
doc_class abstract =
|
||||
keywordlist :: "string list" <= "[]"
|
||||
safety_level :: "classification" <= "SIL3"
|
||||
|
||||
doc_class text_section =
|
||||
authored_by :: "author set" <= "{}"
|
||||
level :: "int option" <= "None"
|
||||
|
||||
type_synonym notion = string
|
||||
|
||||
doc_class introduction = text_section +
|
||||
authored_by :: "author set" <= "UNIV"
|
||||
uses :: "notion set"
|
||||
invariant author_finite :: "finite (authored_by \<sigma>)"
|
||||
|
||||
doc_class claim = introduction +
|
||||
based_on :: "notion list"
|
||||
|
||||
doc_class technical = text_section +
|
||||
formal_results :: "thm list"
|
||||
|
||||
doc_class "definition" = technical +
|
||||
is_formal :: "bool"
|
||||
property :: "term list" <= "[]"
|
||||
|
||||
datatype kind = expert_opinion | argument | "proof"
|
||||
|
||||
doc_class result = technical +
|
||||
evidence :: kind
|
||||
property :: "thm list" <= "[]"
|
||||
invariant has_property :: "evidence \<sigma> = proof \<longleftrightarrow> property \<sigma> \<noteq> []"
|
||||
doc_class example = technical +
|
||||
referring_to :: "(notion + definition) set" <= "{}"
|
||||
|
||||
doc_class conclusion = text_section +
|
||||
establish :: "(claim \<times> result) set"
|
||||
invariant total_rel :: "\<forall> x. x \<in> Domain (establish \<sigma>)
|
||||
\<longrightarrow> (\<exists> y \<in> Range (establish \<sigma>). (x, y) \<in> establish \<sigma>)"
|
||||
|
||||
text\<open>Next we define some instances (docitems): \<close>
|
||||
text*[church::author, email="\<open>church@lambda.org\<close>"]\<open>\<close>
|
||||
|
||||
text*[resultProof::result, evidence = "proof", property="[@{thm \<open>HOL.refl\<close>}]"]\<open>\<close>
|
||||
text*[resultArgument::result, evidence = "argument"]\<open>\<close>
|
||||
|
||||
text\<open>The invariants \<open>author_finite\<close> and \<open>total_rel\<close> can not be checked directly
|
||||
and need a little help.
|
||||
We can set the \<open>invariants_checking_with_tactics\<close> theory attribute to help the checking.
|
||||
It will enable a basic tactic, using unfold and auto:\<close>
|
||||
|
||||
declare[[invariants_checking_with_tactics = true]]
|
||||
|
||||
text*[introductionTest::introduction, authored_by = "{@{author \<open>church\<close>}}"]\<open>\<close>
|
||||
|
||||
text*[claimNotion::claim, authored_by = "{@{author \<open>church\<close>}}", based_on= "[\<open>Notion1\<close>, \<open>Notion2\<close>]"]\<open>\<close>
|
||||
|
||||
text*[conclusionProof::conclusion,
|
||||
establish = "{(@{claim \<open>claimNotion\<close>}, @{result \<open>resultProof\<close>})}"]\<open>\<close>
|
||||
|
||||
end
|
||||
|
|
@ -0,0 +1,52 @@
|
|||
chapter\<open>Ontologys Mathing\<close>
|
||||
|
||||
theory Ontology_Matching_Example
|
||||
imports "Isabelle_DOF.Isa_DOF"
|
||||
begin
|
||||
|
||||
text\<open>Using HOL, we can define a mapping between two ontologies.
|
||||
It is called ontology matching or ontology alignment.
|
||||
Here is an example which show how to map two classes.
|
||||
HOL also allows us to map the invariants (ontological rules) of the classes!\<close>
|
||||
|
||||
type_synonym UTF8 = string
|
||||
|
||||
definition utf8_to_string
|
||||
where "utf8_to_string x = x"
|
||||
|
||||
|
||||
doc_class A =
|
||||
first_name :: UTF8
|
||||
last_name :: UTF8
|
||||
age :: nat
|
||||
married_to :: "string option"
|
||||
invariant a :: "age \<sigma> < 18 \<longrightarrow> married_to \<sigma> = None"
|
||||
doc_class B =
|
||||
name :: string
|
||||
adult :: bool
|
||||
is_married :: bool
|
||||
invariant b :: "is_married \<sigma> \<longrightarrow> adult \<sigma>"
|
||||
|
||||
text\<open>We define the mapping between the two classes,
|
||||
i.e. how to transform the class @{doc_class A} in to the class @{doc_class B}:\<close>
|
||||
|
||||
definition A_to_B_morphism
|
||||
where "A_to_B_morphism X =
|
||||
\<lparr> tag_attribute = A.tag_attribute X
|
||||
, name = utf8_to_string (first_name X) @ '' '' @ utf8_to_string (last_name X)
|
||||
, adult = (age X \<ge> 18)
|
||||
, is_married = (married_to X \<noteq> None) \<rparr>"
|
||||
|
||||
text\<open>Now we check that the invariant is preserved through the morphism:\<close>
|
||||
|
||||
lemma inv_a_preserved :
|
||||
"a_inv X \<Longrightarrow> b_inv (A_to_B_morphism X)"
|
||||
unfolding a_inv_def b_inv_def A_to_B_morphism_def
|
||||
by auto
|
||||
|
||||
lemma A_morphism_B_total :
|
||||
"A_to_B_morphism ` ({X::A. a_inv X}) \<subseteq> ({X::B. b_inv X})"
|
||||
using inv_a_preserved
|
||||
by auto
|
||||
|
||||
end
|
||||
|
|
@ -2,8 +2,10 @@ session "Isabelle_DOF-tests" = "Isabelle_DOF" +
|
|||
options [document = false]
|
||||
theories
|
||||
"AssnsLemmaThmEtc"
|
||||
"Concept_ExampleInvariant"
|
||||
"Concept_Example_Low_Level_Invariant"
|
||||
"Concept_Example"
|
||||
"TermAntiquotations"
|
||||
"Attributes"
|
||||
"Evaluation"
|
||||
"High_Level_Syntax_Invariants"
|
||||
"Ontology_Matching_Example"
|
||||
|
|
|
|||
Loading…
Reference in New Issue