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

Update OntoMathPro_Ontology.thy

This commit is contained in:
Nicolas Méric 2022-02-04 17:21:26 +01:00
parent 36276fc3b4
commit 33d991a1c7
1 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
src/tests/OntoMathPro_Ontology.thy
View File

@ -23,13 +23,15 @@ datatype annotation = DC dc | OWL owl | RDFS rdfs
onto_class Top =
Annotations :: "annotation list"
onto_class Field_of_mathematics =
onto_class Field_of_mathematics =
Annotations :: "annotation list"
invariant restrict_annotation ::"set (Annotations \<sigma>) \<subseteq>
range (RDFS o label) \<union> range (OWL o versionInfo)"
invariant restrict_annotation_F ::"set (Annotations \<sigma>) \<subseteq>
range (RDFS o label) \<union> range (RDFS o comment)"
onto_class Mathematical_knowledge_object =
onto_class Mathematical_knowledge_object =
Annotations :: "annotation list"
invariant restrict_annotation_M ::"set (Annotations \<sigma>) \<subseteq>
range (RDFS o label) \<union> range (RDFS o comment)"
onto_class assoc_F_M =
contains:: "(Field_of_mathematics \<times> Mathematical_knowledge_object) set"
@ -52,9 +54,9 @@ onto_class assoc_M_M' =
\<longrightarrow> (\<exists> y \<in> Range (defines \<sigma>). (x, y) \<in> defines \<sigma>)"
onto_class assoc_M_M_see_also =
see_also :: "(Mathematical_knowledge_object \<times> Mathematical_knowledge_object) set"
invariant see_also_defined :: "\<forall> x. x \<in> Domain (see_also \<sigma>)
\<longrightarrow> (\<exists> y \<in> Range (see_also \<sigma>). (x, y) \<in> see_also \<sigma>)"
see_also :: "(Mathematical_knowledge_object rel) set"
invariant see_also_trans :: "\<forall> r \<in> (see_also \<sigma>). trans r"
invariant see_also_sym :: "\<forall> r \<in> (see_also \<sigma>). sym r"
onto_class Problem = Mathematical_knowledge_object +
Annotations :: "annotation list"
@ -71,5 +73,3 @@ onto_class assoc_Method_Problem =
solves :: "(Method \<times> Problem) set"
invariant solves_defined :: "\<forall> x. x \<in> Domain (solves \<sigma>)
\<longrightarrow> (\<exists> y \<in> Range (solves \<sigma>). (x, y) \<in> solves \<sigma>)"