Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Merge branch 'main' into isabelle_nightly
ci/woodpecker/push/build Pipeline failed Details

This commit is contained in:
Achim D. Brucker 2023-09-12 18:58:58 +01:00
parent e4ee3ff240 ec7297f1d3
commit 792fd60055
8 changed files with 140 additions and 73 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Isabelle_DOF-Proofs/Very_Deep_Interpretation.thy
View File

@ -17,7 +17,7 @@ no_notation "Isabelle_DOF_file" ("@{file _}")
no_notation "Isabelle_DOF_thy" ("@{thy _}")
no_notation "Isabelle_DOF_docitem" ("@{docitem _}")
no_notation "Isabelle_DOF_docitem_attr" ("@{docitemattr (_) :: (_)}")
no_notation "Isabelle_DOF_trace_attribute" ("@{trace-attribute _}")
no_notation "Isabelle_DOF_trace_attribute" ("@{trace'_-attribute _}")
consts Isabelle_DOF_typ :: "string \<Rightarrow> typ" ("@{typ _}")
consts Isabelle_DOF_term :: "string \<Rightarrow> term" ("@{term _}")
@ -27,7 +27,7 @@ datatype "file" = Isabelle_DOF_file string ("@{file _}")
datatype "thy" = Isabelle_DOF_thy string ("@{thy _}")
consts Isabelle_DOF_docitem :: "string \<Rightarrow> 'a" ("@{docitem _}")
datatype "docitem_attr" = Isabelle_DOF_docitem_attr string string ("@{docitemattr (_) :: (_)}")
consts Isabelle_DOF_trace_attribute :: "string \<Rightarrow> (string * string) list" ("@{trace-attribute _}")
consts Isabelle_DOF_trace_attribute :: "string \<Rightarrow> (string * string) list" ("@{trace'_-attribute _}")
subsection\<open> Semantics \<close>

4
Isabelle_DOF-Unit-Tests/Attributes.thy
View File

@ -214,12 +214,12 @@ no_notation Plus (infixr "||" 55)
no_notation Times (infixr "~~" 60)
no_notation Atom ("\<lfloor>_\<rfloor>" 65)
value* \<open> DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace-attribute \<open>aaa\<close>}) \<close>
value* \<open> DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace_attribute \<open>aaa\<close>}) \<close>
definition word_test :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> bool" (infix "is-in" 60)
where " w is-in rexp \<equiv> DA.accepts (na2da (rexp2na rexp)) (w)"
value* \<open> (map fst @{trace-attribute \<open>aaa\<close>}) is-in example_expression \<close>
value* \<open> (map fst @{trace_attribute \<open>aaa\<close>}) is-in example_expression \<close>
(*<*)

6
Isabelle_DOF-Unit-Tests/Concept_High_Level_Invariants.thy
View File

@ -213,9 +213,9 @@ value*\<open>@{scholarly_paper.author \<open>church'\<close>}\<close>
value*\<open>@{author \<open>church\<close>}\<close>
value*\<open>@{Concept_High_Level_Invariants.author \<open>church\<close>}\<close>
value*\<open>@{scholarly_paper.author_instances}\<close>
value*\<open>@{author_instances}\<close>
value*\<open>@{Concept_High_Level_Invariants.author_instances}\<close>
value*\<open>@{instances_of \<open>scholarly_paper.author\<close>}\<close>
value*\<open>@{instances_of \<open>author\<close>}\<close>
value*\<open>@{instances_of \<open>Concept_High_Level_Invariants.author\<close>}\<close>
text*[introduction3::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
text*[introduction4::introduction, authored_by = "{@{author \<open>curry\<close>}}", level = "Some 4"]\<open>\<close>

4
Isabelle_DOF-Unit-Tests/Concept_MonitorTest1.thy
View File

@ -104,8 +104,8 @@ ML\<open>
val (oid, DOF_core.Instance {value, ...}) =
Name_Space.check (Context.Proof \<^context>) (DOF_core.get_instances \<^context>) ("aaa", Position.none)
\<close>
term*\<open>map fst @{trace-attribute \<open>test_monitor_M\<close>}\<close>
value*\<open>map fst @{trace-attribute \<open>test_monitor_M\<close>}\<close>
term*\<open>map fst @{trace_attribute \<open>test_monitor_M\<close>}\<close>
value*\<open>map fst @{trace_attribute \<open>test_monitor_M\<close>}\<close>
ML\<open>@{assert} ([("Conceptual.A", "test"), ("Conceptual.F", "sdfg")] = @{trace_attribute aaa}) \<close>

32
Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy
View File

@ -136,6 +136,9 @@ ML\<open>@{thm "refl"}\<close>
section\<open>Request on instances\<close>
text\<open>The instances directly attached to the default super class \<open>text\<close>: \<close>
value*\<open>@{instances_of \<open>text\<close>}\<close>
text\<open>We define a new class Z:\<close>
doc_class Z =
z::"int"
@ -146,28 +149,27 @@ text*[test2Z::Z, z=4]\<open>lorem ipsum...\<close>
text*[test3Z::Z, z=3]\<open>lorem ipsum...\<close>
text\<open>We want to get all the instances of the @{doc_class Z}:\<close>
value*\<open>@{Z_instances}\<close>
value*\<open>@{instances_of \<open>Z\<close>}\<close>
text\<open>Now we want to get the instances of the @{doc_class Z} whose attribute z > 2:\<close>
value*\<open>filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z_instances}\<close>
value*\<open>filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{instances_of \<open>Z\<close>}\<close>
text\<open>We can check that we have the list of instances we wanted:\<close>
value*\<open>filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z_instances} = [@{Z \<open>test3Z\<close>}, @{Z \<open>test2Z\<close>}]
\<or> filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z_instances} = [@{Z \<open>test2Z\<close>}, @{Z \<open>test3Z\<close>}]\<close>
assert*\<open>filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{instances_of \<open>Z\<close>} = [@{Z \<open>test3Z\<close>}, @{Z \<open>test2Z\<close>}]
\<or> filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{instances_of \<open>Z\<close>} = [@{Z \<open>test2Z\<close>}, @{Z \<open>test3Z\<close>}]\<close>
text\<open>Now, we want to get all the instances of the @{doc_class A}\<close>
value*\<open>@{A_instances}\<close>
value*\<open>@{instances_of \<open>A\<close>}\<close>
(*<*)
text\<open>Warning: If you make a request on attributes that are undefined in some instances,
you will get a result which includes these unresolved cases.
text\<open>Warning: Requests on attributes that are undefined in some instances
include all the instances.
In the following example, we request the instances of the @{doc_class A}.
But we have defined an instance @{docitem \<open>sdf\<close>} in theory @{theory "Isabelle_DOF-Ontologies.Conceptual"}
whose our theory inherits from, and this docitem instance does not initialize its attribute \<^emph>\<open>x\<close>.
So in the request result we get an unresolved case because the evaluator can not get
the value of the \<^emph>\<open>x\<close> attribute of the instance @{docitem \<open>sdf\<close>}:\<close>
value*\<open>filter (\<lambda>\<sigma>. A.x \<sigma> > 5) @{A_instances}\<close>
(*>*)
But we have defined instances @{A \<open>axx\<close>} and @{A \<open>axx\<close>} previously
and these docitem instances do not initialize their \<^const>\<open>A.x\<close> attribute.
So the request can not be evaluated:\<close>
value*\<open>filter (\<lambda>\<sigma>. A.x \<sigma> > 5) @{instances_of \<open>A\<close>}\<close>
section\<open>Limitations\<close>
text\<open>There are still some limitations.
@ -226,7 +228,7 @@ text\<open>... and here we reference @{A \<open>assertionA\<close>}.\<close>
assert*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
text\<open>The optional evaluator of \<open>value*\<close> and \<open>assert*\<close> must be specified before the meta arguments:\<close>
value* [nbe] [optional_test_A::A, x=6] \<open>filter (\<lambda>\<sigma>. A.x \<sigma> > 5) @{A_instances}\<close>
value* [nbe] [optional_test_A::A, x=6] \<open>filter (\<lambda>\<sigma>. A.x \<sigma> > 5) @{instances_of \<open>A\<close>}\<close>
assert* [nbe] [resultProof3::result, evidence = "proof", property="[@{thm \<open>HOL.sym\<close>}]"]
\<open>evidence @{result \<open>resultProof3\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>

5
Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy
View File

@ -3,6 +3,11 @@ theory Test_Polymorphic_Classes
TestKit
begin
text\<open>The name \<open>text\<close> is reserved by the implementation and refers to the default super class:\<close>
doc_class-assert-error "text" =
a::int
\<open>text: This name is reserved by the implementation\<close>
doc_class title =
short_title :: "string option" <= "None"

111
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -1050,7 +1050,8 @@ datatype "file" = Isabelle_DOF_file string ("@{file _}")
datatype "thy" = Isabelle_DOF_thy string ("@{thy _}")
consts Isabelle_DOF_docitem :: "string \<Rightarrow> 'a" ("@{docitem _}")
datatype "docitem_attr" = Isabelle_DOF_docitem_attr string string ("@{docitemattr (_) :: (_)}")
consts Isabelle_DOF_trace_attribute :: "string \<Rightarrow> (string * string) list" ("@{trace-attribute _}")
consts Isabelle_DOF_trace_attribute :: "string \<Rightarrow> (string * string) list" ("@{trace'_attribute _}")
consts Isabelle_DOF_instances_of :: "string \<Rightarrow> 'a list" ("@{instances'_of _}")
\<comment> \<open>Dynamic setup of inner syntax cartouche\<close>
@ -1192,12 +1193,27 @@ fun check_instance thy (term, _, pos) s =
val name' = DOF_core.cid_of name thy
|> DOF_core.get_onto_class_cid thy |> (fst o fst)
fun check' (class_name, object_cid) =
if class_name = object_cid then
DOF_core.value_of name thy
if class_name = object_cid
then ()
else err (name ^ " is not an instance of " ^ class_name) pos
in check' (class_name, name') end;
in ML_isa_check_generic check thy (term, pos) end
fun check_instance_of thy (term, _, pos) _ =
let
fun check thy (name, _) =
if equal name DOF_core.default_cid
then ()
else
let
val class_typ = name |> DOF_core.get_onto_class_cid thy |> snd
fun check' (class_name, typ) =
if equal (class_name |> Syntax.read_typ_global thy) typ
then ()
else err (name ^ " is not a class name") pos
in check' (name, class_typ) end;
in ML_isa_check_generic check thy (term, pos) end
fun ML_isa_id _ (term,_) = SOME term
@ -1273,44 +1289,44 @@ fun declare_ISA_class_accessor_and_check_instance (params, doc_class_name, bind_
end
fun elaborate_instances_list thy isa_name _ _ _ =
fun elaborate_instances_of thy _ _ term_option _ =
let
val base_name = Long_Name.base_name isa_name
val qualifier = Long_Name.qualifier isa_name
val isa_name' = (case try (unprefix DOF_core.doc_class_prefix) base_name of
NONE => unprefix DOF_core.long_doc_class_prefix base_name
| SOME name => name)
|> unsuffix instances_of_suffixN
|> Long_Name.qualify qualifier
val class_typ = isa_name' |> Proof_Context.read_typ (Proof_Context.init_global thy)
val long_class_name = DOF_core.get_onto_class_name_global isa_name' thy
val values = thy |> Proof_Context.init_global |> DOF_core.get_instances
|> Name_Space.dest_table
|> filter (fn (name, _) => equal (DOF_core.cid_of name thy) long_class_name)
|> map (fn (oid, _) => DOF_core.value_of oid thy)
in HOLogic.mk_list class_typ values end
fun declare_class_instances_annotation (params, doc_class_name, bind_pos) thy =
let
val bname = Long_Name.base_name doc_class_name
val bname' = prefix DOF_core.doc_class_prefix bname |> suffix instances_of_suffixN
val bind = bname' |> pair bind_pos |> swap |> Binding.make
val bind' = prefix DOF_core.long_doc_class_prefix bname
|> suffix instances_of_suffixN |> pair bind_pos |> swap |> Binding.make
val typ = Type (doc_class_name, map TFree params)
fun mixfix_enclose name = name |> enclose "@{" "}"
val mixfix = clean_mixfix (bname ^ instances_of_suffixN) |> mixfix_enclose
val mixfix' = clean_mixfix (doc_class_name ^ instances_of_suffixN) |> mixfix_enclose
in
thy |> rm_mixfix bname' mixfix
|> Sign.add_consts [(bind, \<^Type>\<open>list typ\<close>, Mixfix.mixfix mixfix)]
|> DOF_core.add_isa_transformer bind ((check_identity, elaborate_instances_list)
|> DOF_core.make_isa_transformer)
|> Sign.add_consts [(bind', \<^Type>\<open>list typ\<close>, Mixfix.mixfix mixfix')]
|> DOF_core.add_isa_transformer bind' ((check_identity, elaborate_instances_list)
|> DOF_core.make_isa_transformer)
end
val class_name = case term_option of
NONE => error ("Malformed term annotation")
| SOME term => HOLogic.dest_string term
fun mk_list class_typ f =
let
val values = thy |> Proof_Context.init_global |> DOF_core.get_instances
|> Name_Space.dest_table
|> map fst
|> tap (fn is => writeln ("In elaborate_instances_list instances: " ^ \<^make_string> is))
|> f
|> tap (fn is => writeln ("In elaborate_instances_list instances after filter: " ^ \<^make_string> is))
|> map (fn oid => DOF_core.value_of oid thy)
in HOLogic.mk_list class_typ values end
in if equal class_name DOF_core.default_cid
then
(* When the class name is default_cid = "text",
return the instances attached to this default class.
We want the class default_cid to stay abstract
and not have the capability to be defined with attribute, invariants, etc.
Hence this can handle docitem without a class associated,
for example when you just want a document element to be referentiable
without using the burden of ontology classes.
ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close> *)
(filter (fn name => DOF_core.cid_of name thy |> equal DOF_core.default_cid))
|> mk_list \<^typ>\<open>unit\<close>
else
let
val class_typ = class_name |> Syntax.read_typ_global thy
in
(filter_out (fn name => DOF_core.cid_of name thy |> equal DOF_core.default_cid)
#> filter (fn name => DOF_core.cid_of name thy
|> Syntax.read_typ_global thy
|> equal class_typ))
|> mk_list class_typ
end
end
fun symbex_attr_access0 ctxt proj_term term =
let
@ -1393,7 +1409,9 @@ end)
([(\<^const_name>\<open>Isabelle_DOF_docitem\<close>,
ISA_core.ML_isa_check_docitem, ISA_core.ML_isa_elaborate_generic)
, (\<^const_name>\<open>Isabelle_DOF_trace_attribute\<close>,
ISA_core.ML_isa_check_trace_attribute, ISA_core.ML_isa_elaborate_trace_attribute)]
ISA_core.ML_isa_check_trace_attribute, ISA_core.ML_isa_elaborate_trace_attribute)
, (\<^const_name>\<open>Isabelle_DOF_instances_of\<close>,
ISA_core.check_instance_of, ISA_core.elaborate_instances_of)]
|> fold (fn (n, check, elaborate) => fn thy =>
let val ns = Sign.consts_of thy |> Consts.space_of
val name = n
@ -1877,7 +1895,7 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} bi
else NONE
val value_terms = if default_cid
then let
val undefined_value = Free ("Undefined_Value", \<^Type>\<open>unit\<close>)
val undefined_value = Free (oid ^ "_Undefined_Value", \<^Type>\<open>unit\<close>)
in (undefined_value, undefined_value) end
(* Handle initialization of docitem without a class associated,
for example when you just want a document element to be referentiable
@ -3095,7 +3113,13 @@ fun add_doc_class_cmd overloaded (raw_params, binding)
raw_parent raw_fieldsNdefaults reject_Atoms regexps invariants thy =
let
val bind_pos = Binding.pos_of binding
val name = Binding.name_of binding
val name =
let val name = Binding.name_of binding
in case name |> Option.filter (not o equal DOF_core.default_cid) of
NONE => bind_pos |> ISA_core.err (name
^ ": This name is reserved by the implementation")
| SOME name => name
end
val ctxt = Proof_Context.init_global thy;
val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
@ -3161,7 +3185,6 @@ fun add_doc_class_cmd overloaded (raw_params, binding)
because the class name is already bound to "doc_class Regular_Exp.rexp" constant
by add_doc_class_cmd function *)
|> (fn thy => ISA_core.declare_ISA_class_accessor_and_check_instance (params', cid thy, bind_pos) thy)
|> (fn thy => ISA_core.declare_class_instances_annotation (params', cid thy, bind_pos) thy)
end;

47
Isabelle_DOF/thys/manual/M_04_RefMan.thy
View File

@ -1019,6 +1019,38 @@ schemata:
section*["sec_advanced"::technical]\<open>Advanced ODL Concepts\<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"
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" <= "[]"
doc_class example = technical +
referring_to :: "(notion + definition) set" <= "{}"
doc_class "conclusion" = text_section +
establish :: "(claim \<times> result) set"
(*>*)
subsection*["sec_example"::technical]\<open>Example\<close>
text\<open>We assume in this section the following local ontology:
@ -1301,6 +1333,12 @@ text\<open>
(See @{technical "sec_low_level_inv"} for an example).
\<close>
(*<*)
value*\<open>map (result.property) @{instances_of \<open>result\<close>}\<close>
value*\<open>map (text_section.authored_by) @{instances_of \<open>introduction\<close>}\<close>
value*\<open>filter (\<lambda>\<sigma>. result.evidence \<sigma> = proof) @{instances_of \<open>result\<close>}\<close>
value*\<open>filter (\<lambda>\<sigma>. the (text_section.level \<sigma>) > 1) @{instances_of \<open>introduction\<close>}\<close>
(*>*)
subsection*["sec_queries_on_instances"::technical]\<open>Queries On Instances\<close>
@ -1315,19 +1353,18 @@ text\<open>
or to get the list of the authors of the instances of \<open>introduction\<close>,
it suffices to treat this meta-data as usual:
@{theory_text [display,indent=5, margin=70] \<open>
value*\<open>map (result.property) @{result_instances}\<close>
value*\<open>map (text_section.authored_by) @{introduction_instances}\<close>
value*\<open>map (result.property) @{instances_of \<open>result\<close>}\<close>
value*\<open>map (text_section.authored_by) @{instances_of \<open>introduction\<close>}\<close>
\<close>}
In order to get the list of the instances of the class \<open>myresult\<close>
whose \<open>evidence\<close> is a \<open>proof\<close>, one can use the command:
@{theory_text [display,indent=5, margin=70] \<open>
value*\<open>filter (\<lambda>\<sigma>. result.evidence \<sigma> = proof) @{result_instances}\<close>
value*\<open>filter (\<lambda>\<sigma>. result.evidence \<sigma> = proof) @{instances_of \<open>result\<close>}\<close>
\<close>}
The list of the instances of the class \<open>introduction\<close> whose \<open>level\<close> > 1,
can be filtered by:
@{theory_text [display,indent=5, margin=70] \<open>
value*\<open>filter (\<lambda>\<sigma>. the (text_section.level \<sigma>) > 1)
@{introduction_instances}\<close>
value*\<open>filter (\<lambda>\<sigma>. the (text_section.level \<sigma>) > 1) @{instances_of \<open>introduction\<close>}\<close>
\<close>}
\<close>