From 7791538b54616830a9211ab6c9c1857692550a95 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Thu, 4 Apr 2024 00:10:51 +0200 Subject: [PATCH] Update to isabelle 2023 and add morphism examples --- Isabelle_DOF-Unit-Tests/TestKit.thy | 5 +- Isabelle_DOF/ROOT | 6 +- Isabelle_DOF/document/dof_session.tex | 6 +- Isabelle_DOF/thys/Isa_DOF.thy | 11 +- .../thys/manual/Isabelle_DOF_Manual.thy | 2 +- .../thys/manual/M_04_Document_Ontology.thy | 230 ++++++++++ .../thys/manual/M_05_Proofs_Ontologies.thy | 417 ++++++++++++++++++ .../{M_04_RefMan.thy => M_06_RefMan.thy} | 0 ...ementation.thy => M_07_Implementation.thy} | 6 +- 9 files changed, 669 insertions(+), 14 deletions(-) create mode 100644 Isabelle_DOF/thys/manual/M_04_Document_Ontology.thy create mode 100644 Isabelle_DOF/thys/manual/M_05_Proofs_Ontologies.thy rename Isabelle_DOF/thys/manual/{M_04_RefMan.thy => M_06_RefMan.thy} (100%) rename Isabelle_DOF/thys/manual/{M_05_Implementation.thy => M_07_Implementation.thy} (99%) diff --git a/Isabelle_DOF-Unit-Tests/TestKit.thy b/Isabelle_DOF-Unit-Tests/TestKit.thy index 3423834..0bdfe77 100644 --- a/Isabelle_DOF-Unit-Tests/TestKit.thy +++ b/Isabelle_DOF-Unit-Tests/TestKit.thy @@ -37,13 +37,14 @@ fun gen_enriched_document_command2 name {body} cid_transform attr_transform mark xstring_opt:(xstring * Position.T) option), toks_list:Input.source list) : theory -> theory = - let val ((binding,cid_pos), doc_attrs) = meta_args + let val toplvl = Toplevel.make_state o SOME + val ((binding,cid_pos), doc_attrs) = meta_args val oid = Binding.name_of binding val oid' = if meta_args = ODL_Meta_Args_Parser.empty_meta_args then "output" else oid (* as side-effect, generates markup *) - fun check_n_tex_text thy toks = let val ctxt = Toplevel.presentation_context (Toplevel.make_state (SOME thy)) + fun check_n_tex_text thy toks = let val ctxt = Toplevel.presentation_context (toplvl thy) val pos = Input.pos_of toks; val _ = Context_Position.reports ctxt [(pos, Markup.language_document (Input.is_delimited toks)), diff --git a/Isabelle_DOF/ROOT b/Isabelle_DOF/ROOT index 878d12b..3f0dc70 100644 --- a/Isabelle_DOF/ROOT +++ b/Isabelle_DOF/ROOT @@ -22,8 +22,10 @@ session "Isabelle_DOF" (AFP) = "Functional-Automata" + "thys/manual/M_01_Introduction" "thys/manual/M_02_Background" "thys/manual/M_03_GuidedTour" - "thys/manual/M_04_RefMan" - "thys/manual/M_05_Implementation" + "thys/manual/M_04_Document_Ontology" + "thys/manual/M_05_Proofs_Ontologies" + "thys/manual/M_06_RefMan" + "thys/manual/M_07_Implementation" "thys/manual/Isabelle_DOF_Manual" document_files "root.bib" diff --git a/Isabelle_DOF/document/dof_session.tex b/Isabelle_DOF/document/dof_session.tex index 9a57842..468deb0 100644 --- a/Isabelle_DOF/document/dof_session.tex +++ b/Isabelle_DOF/document/dof_session.tex @@ -2,6 +2,8 @@ \input{M_01_Introduction.tex} \input{M_02_Background.tex} \input{M_03_GuidedTour.tex} -\input{M_04_RefMan.tex} -\input{M_05_Implementation.tex} +\input{M_04_Document_Ontology.tex} +\input{M_05_Proofs_Ontologies.tex} +\input{M_06_RefMan.tex} +\input{M_07_Implementation.tex} \input{Isabelle_DOF_Manual.tex} diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index bbc3baa..395a5c2 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -2359,6 +2359,7 @@ fun onto_macro_cmd_command (name, pos) descr cmd output_cmd = )))) + (* Core Command Definitions *) val _ = @@ -2691,7 +2692,9 @@ fun gen_theorem schematic bundle_includes prep_att prep_stmt |> prep_statement (prep_att lthy) prep_stmt elems raw_concl; val atts = more_atts @ map (prep_att lthy) raw_atts; - val print_cfg = {interactive = int, pos = Position.thread_data (), proof_state= false} + val pos = Position.thread_data (); + val print_results = + Proof_Display.print_results {interactive = int, pos = pos, proof_state = false}; fun after_qed' results goal_ctxt' = let @@ -2703,13 +2706,13 @@ fun gen_theorem schematic bundle_includes prep_att prep_stmt Local_Theory.notes_kind kind (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy; val lthy'' = - if Binding.is_empty_atts (name, atts) then - (Proof_Display.print_results print_cfg lthy' ((kind, ""), res); lthy') + if Binding.is_empty_atts (name, atts) + then (print_results lthy' ((kind, ""), res); lthy') else let val ([(res_name, _)], lthy'') = Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy'; - val _ = Proof_Display.print_results print_cfg lthy' ((kind, res_name), res); + val _ = print_results lthy' ((kind, res_name), res); in lthy'' end; in after_qed results' lthy'' end; diff --git a/Isabelle_DOF/thys/manual/Isabelle_DOF_Manual.thy b/Isabelle_DOF/thys/manual/Isabelle_DOF_Manual.thy index 2fb144a..e6a7dde 100644 --- a/Isabelle_DOF/thys/manual/Isabelle_DOF_Manual.thy +++ b/Isabelle_DOF/thys/manual/Isabelle_DOF_Manual.thy @@ -13,7 +13,7 @@ (*<*) theory "Isabelle_DOF_Manual" - imports "M_05_Implementation" + imports "M_07_Implementation" begin close_monitor*[this] check_doc_global diff --git a/Isabelle_DOF/thys/manual/M_04_Document_Ontology.thy b/Isabelle_DOF/thys/manual/M_04_Document_Ontology.thy new file mode 100644 index 0000000..2a1aff9 --- /dev/null +++ b/Isabelle_DOF/thys/manual/M_04_Document_Ontology.thy @@ -0,0 +1,230 @@ +(************************************************************************* + * Copyright (C) + * 2019-2022 University of Exeter + * 2018-2022 University of Paris-Saclay + * 2018 The University of Sheffield + * + * License: + * This program can be redistributed and/or modified under the terms + * of the 2-clause BSD-style license. + * + * SPDX-License-Identifier: BSD-2-Clause + *************************************************************************) + +(*<*) +theory + "M_04_Document_Ontology" + imports + "M_03_GuidedTour" + keywords "class_synonym" :: thy_defn +begin + +(*>*) + + +(*<*) +definition combinator1 :: "'a \ ('a \ 'b) \ 'b" (infixl "|>" 65) + where "x |> f = f x" + + +ML\ +local +val _ = + Outer_Syntax.local_theory \<^command_keyword>\class_synonym\ "declare type abbreviation" + (Parse.type_args -- Parse.binding -- + (\<^keyword>\=\ |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix')) + >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)); + +in end +\ + +(*>*) + + +(*<*) + +doc_class "title" = short_title :: "string option" <= "None" + +(*doc_class '\ affiliation = + journal_style :: '\ +*) + +doc_class elsevier = + organization :: string + address_line :: string + postcode :: int + city :: string + +(*doc_class elsevier_affiliation = affiliation +*) + +doc_class acm = + position :: string + institution :: string + department :: int + street_address :: string + city :: string + state :: int + country :: string + postcode :: int + +(*doc_class acm_affiliation = affiliation +*) + +doc_class lncs = + institution :: string + +(*doc_class lncs_affiliation = affiliation +*) + + +doc_class author = + name :: string + email :: "string" <= "''''" + invariant ne_name :: "name \ \ ''''" + +doc_class elsevier_author = "author" + + affiliations :: "elsevier list" + short_author :: string + url :: string + footnote :: string + +text*[el1:: "elsevier"]\\ +(*text*[el_aff1:: "affiliation", journal_style = "@{elsevier \el1\}"]\\*) +term*\@{elsevier \el1\}\ +text*[el_auth1:: "elsevier_author", affiliations = "[@{elsevier \el1\}]"]\\ + +doc_class acm_author = "author" + + affiliations :: "acm list" + orcid :: int + footnote :: string + +text*[acm1:: "acm"]\\ +(*text*[acm_aff1:: "acm affiliation", journal_style = "@{acm \acm1\}"]\\*) +text*[acm_auth1:: "acm_author", affiliations = "[@{acm \acm1\}]"]\\ + +doc_class lncs_author = "author" + + affiliations :: "lncs list" + orcid :: int + short_author :: string + footnote :: string + +text*[lncs1:: "lncs"]\\ +(*text*[lncs_aff1:: "lncs affiliation", journal_style = "@{lncs \lncs1\}"]\\*) +text*[lncs_auth1:: "lncs_author", affiliations = "[@{lncs \lncs1\}]"]\\ + + +doc_class "text_element" = + authored_by :: "author set" <= "{}" + level :: "int option" <= "None" + invariant authors_req :: "authored_by \ \ {}" + and level_req :: "the (level \) > 1" + +doc_class "introduction" = "text_element" + + authored_by :: "(author) set" <= "UNIV" + +doc_class "technical" = "text_element" + + formal_results :: "thm list" + +doc_class "definition" = "technical" + + is_formal :: "bool" + +doc_class "theorem" = "technical" + + is_formal :: "bool" + assumptions :: "term list" <= "[]" + statement :: "term option" <= "None" + +doc_class "conclusion" = "text_element" + + resumee :: "(definition set \ theorem set)" + invariant is_form :: "(\x\(fst (resumee \)). definition.is_formal x) \ + (\y\(snd (resumee \)). is_formal y)" + +text*[def::"definition", is_formal = "True"]\\ +text*[theo::"theorem", is_formal = "False"]\\ +text*[conc::"conclusion", resumee="({@{definition \def\}}, {@{theorem \theo\}})"]\\ + +value*\resumee @{conclusion \conc\} |> fst\ +value*\resumee @{conclusion \conc\} |> snd\ + +doc_class "article" = + style_id :: string <= "''LNCS''" + accepts "(title ~~ \author\\<^sup>+ ~~ \introduction\\<^sup>+ + ~~ \\definition ~~ example\\<^sup>+ || theorem\\<^sup>+ ~~ \conclusion\\<^sup>+)" + + +datatype kind = expert_opinion | argument | "proof" + +onto_class result = " technical" + + evidence :: kind + property :: " theorem list" <= "[]" + invariant has_property :: "evidence \ = proof \ property \ \ []" + +(*>*) + +text*[paper_m::float, main_caption="\A Basic Document Ontology: paper$^m$\"]\ + @{boxed_theory_text [display,indent=5] + \doc_class "title" = short_title :: "string option" <= "None" +doc_class affiliation = + journal_style :: '\ +doc_class author = + affiliations :: "'\ affiliation list" + name :: string + email :: "string" <= "''''" + invariant ne_name :: "name \ \ ''''" +doc_class "text_element" = + authored_by :: "('\ author) set" <= "{}" + level :: "int option" <= "None" + invariant authors_req :: "authored_by \ {}" + and level_req :: "the (level) > 1" +doc_class "introduction" = text_element + + authored_by :: "('\ author) set" <= "UNIV" +doc_class "technical" = text_element + + formal_results :: "thm list" +doc_class "definition" = technical + + is_formal :: "bool" +doc_class "theorem" = technical + + assumptions :: "term list" <= "[]" + statement :: "term option" <= "None" +doc_class "conclusion" = text_element + + resumee :: "(definition set \ theorem set)" + invariant (\x\fst resumee. is_formal x) + \ (\y\snd resumee. is_formal y) +doc_class "article" = + style_id :: string <= "''LNCS''" + accepts "(title ~~ \author\\<^sup>+ ~~ \introduction\\<^sup>+ + ~~ \\definition ~~ example\\<^sup>+ || theorem\\<^sup>+ ~~ \conclusion\\<^sup>+)"\} +\ + + +(*<*) +datatype role = PM \ \Program Manager\ + | RQM \ \Requirements Manager\ + | DES \ \Designer\ + | IMP \ \Implementer\ + | ASR \ \Assessor\ + | INT \ \Integrator\ + | TST \ \Tester\ + | VER \ \Verifier\ + | VnV \ \Verification and Validation\ + | VAL \ \Validator\ + +abbreviation developer where "developer == DES" +abbreviation validator where "validator == VAL" +abbreviation verifier where "verifier == VER" + +doc_class requirement = Isa_COL.text_element + + long_name :: "string option" + is_concerned :: "role set" + +text*[req1::requirement, + is_concerned="{developer, validator}"] +\The operating system shall provide secure +memory separation.\ + +text\ +The recurring issue of the certification +is @{requirement \req1\} ...\ + +term "\long_name = None,is_concerned = {developer,validator}\" +(*>*) + +(*<*) +end +(*>*) diff --git a/Isabelle_DOF/thys/manual/M_05_Proofs_Ontologies.thy b/Isabelle_DOF/thys/manual/M_05_Proofs_Ontologies.thy new file mode 100644 index 0000000..dd3a0c7 --- /dev/null +++ b/Isabelle_DOF/thys/manual/M_05_Proofs_Ontologies.thy @@ -0,0 +1,417 @@ +(************************************************************************* + * Copyright (C) + * 2019-2022 University of Exeter + * 2018-2022 University of Paris-Saclay + * 2018 The University of Sheffield + * + * License: + * This program can be redistributed and/or modified under the terms + * of the 2-clause BSD-style license. + * + * SPDX-License-Identifier: BSD-2-Clause + *************************************************************************) + +(*<*) +theory + "M_05_Proofs_Ontologies" + imports + "M_04_Document_Ontology" + keywords "onto_morphism" :: thy_decl + and "to" +begin + +(*>*) + +section*["morphisms"::scholarly_paper.text_section] \Proving Morphisms on Ontologies\ + +(* rethink examples: should we "morph" previdence too ? ? ? *) + +(*<*) +(* Mapped_PILIB_Ontology example *) +term\fold (+) S 0\ + +definition sum + where "sum S = (fold (+) S 0)" + +datatype Hardware_Type = + Motherboard | + Expansion_Card | + Storage_Device | + Fixed_Media | + Removable_Media | + Input_Device | + Output_Device + +datatype Software_Type = + Operating_system | + Text_editor | + Web_Navigator | + Development_Environment + +(* Reference Ontology *) +onto_class Resource = + name :: string + +onto_class Electronic = Resource + + provider :: string + manufacturer :: string + +onto_class Component = Electronic + + mass :: int + +onto_class Simulation_Model = Electronic + + simulate :: Component + composed_of :: "Component list" + version :: int + +onto_class Informatic = Resource + + description :: string + +onto_class Hardware = Informatic + + type :: Hardware_Type + mass :: int + composed_of :: "Component list" + invariant c1 :: "mass \ = sum(map Component.mass (composed_of \))" + +onto_class Software = Informatic + + type :: Software_Type + version :: int + +(* Local Ontology *) +onto_class Item = + name :: string + +onto_class Product = Item + + serial_number :: int + provider :: string + mass :: int + +onto_class Electronic_Component = Product + + serial_number :: int + +onto_class Monitor = Product + + composed_of :: "Electronic_Component list" + invariant c2 :: "Product.mass \ = sum(map Product.mass (composed_of \))" + +term\Product.mass \ = sum(map Product.mass (composed_of \))\ + +onto_class Computer_Software = Item + + type :: Software_Type + version :: int + +(* Mapping or Morphism *) +definition Item_to_Resource_morphism :: "Item \ Resource" + ("_ \Resource\\<^sub>I\<^sub>t\<^sub>e\<^sub>m" [1000]999) + where " \ \Resource\\<^sub>I\<^sub>t\<^sub>e\<^sub>m = + \ Resource.tag_attribute = 1::int , + Resource.name = name \ \" + +definition Product_to_Resource_morphism :: "Product \ Resource" + ("_ \Resource\\<^sub>P\<^sub>r\<^sub>o\<^sub>d\<^sub>u\<^sub>c\<^sub>t" [1000]999) + where " \ \Resource\\<^sub>P\<^sub>r\<^sub>o\<^sub>d\<^sub>u\<^sub>c\<^sub>t = + \ Resource.tag_attribute = 2::int , + Resource.name = name \ \" + +definition Computer_Software_to_Software_morphism :: "Computer_Software \ Software" + ("_ \Software\\<^sub>S\<^sub>o\<^sub>f\<^sub>t\<^sub>C\<^sub>m\<^sub>p" [1000]999) + where "\ \Software\\<^sub>S\<^sub>o\<^sub>f\<^sub>t\<^sub>C\<^sub>m\<^sub>p = + \ Resource.tag_attribute = 3::int , + Resource.name = name \ , + Informatic.description = ''no description'', + Software.type = type \ , + Software.version = version \ \" + +definition Electronic_Component_to_Component_morphism :: "Electronic_Component \ Component" + ("_ \Component\\<^sub>E\<^sub>l\<^sub>e\<^sub>c\<^sub>C\<^sub>m\<^sub>p" [1000]999) + where "\ \Component\\<^sub>E\<^sub>l\<^sub>e\<^sub>c\<^sub>C\<^sub>m\<^sub>p = + \ Resource.tag_attribute = 4::int , + Resource.name = name \ , + Electronic.provider = provider \ , + Electronic.manufacturer = ''no manufacturer'' , + Component.mass = mass \ \" + +definition Monitor_to_Hardware_morphism :: "Monitor \ Hardware" + ("_ \Hardware\\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e" [1000]999) + where "\ \Hardware\\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e = + \ Resource.tag_attribute = 5::int , + Resource.name = name \ , + Informatic.description = ''no description'', + Hardware.type = Output_Device, + Hardware.mass = mass \ , + Hardware.composed_of = map Electronic_Component_to_Component_morphism (composed_of \) + \" + + +lemma inv_c2_preserved : + "c2_inv \ \ c1_inv (\ \Hardware\\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e)" + unfolding c1_inv_def c2_inv_def + Monitor_to_Hardware_morphism_def Electronic_Component_to_Component_morphism_def + by (auto simp: comp_def) + +lemma Monitor_to_Hardware_morphism_total : + "Monitor_to_Hardware_morphism ` ({X::Monitor. c2_inv X}) \ ({X::Hardware. c1_inv X})" + using inv_c2_preserved + by auto + +type_synonym local_ontology = "Item * Electronic_Component * Monitor" +type_synonym reference_ontology = "Resource * Component * Hardware" + +fun ontology_mapping :: "local_ontology \ reference_ontology" where + "ontology_mapping (x, y, z) = (x \Resource\\<^sub>I\<^sub>t\<^sub>e\<^sub>m , y \Component\\<^sub>E\<^sub>l\<^sub>e\<^sub>c\<^sub>C\<^sub>m\<^sub>p, z \Hardware\\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e)" + +lemma ontology_mapping_total : + "ontology_mapping ` {X. c2_inv (snd (snd X))} + \ {X. c1_inv (snd (snd X))}" + using inv_c2_preserved + by auto + + +doc_class "title" = short_title :: "string option" <= "None" + +(*doc_class '\ affiliation = + journal_style :: '\ +*) + +doc_class elsevier = + organization :: string + address_line :: string + postcode :: int + city :: string + +(*doc_class elsevier_affiliation = affiliation +*) + +doc_class acm = + position :: string + institution :: string + department :: int + street_address :: string + city :: string + state :: int + country :: string + postcode :: int + +(*doc_class acm_affiliation = affiliation +*) + +doc_class lncs = + institution :: string + +(*doc_class lncs_affiliation = affiliation +*) + + +doc_class author = + firstname :: string + surname :: string + email :: "string" <= "''''" + invariant ne_fsnames :: "firstname \ \ '''' \ surname \ \ ''''" + +doc_class elsevier_author = "author" + + affiliations :: "elsevier list" + short_author :: string + url :: string + footnote :: string + +text*[el1:: "elsevier"]\\ +(*text*[el_aff1:: "affiliation", journal_style = "@{elsevier \el1\}"]\\*) +term*\@{elsevier \el1\}\ +text*[el_auth1:: "elsevier_author", affiliations = "[@{elsevier \el1\}]"]\\ + +doc_class acm_author = "author" + + affiliations :: "acm list" + orcid :: int + footnote :: string + +text*[acm1:: "acm"]\\ +(*text*[acm_aff1:: "acm affiliation", journal_style = "@{acm \acm1\}"]\\*) +text*[acm_auth1:: "acm_author", affiliations = "[@{acm \acm1\}]"]\\ + +doc_class lncs_author = "author" + + affiliations :: "lncs list" + orcid :: int + short_author :: string + footnote :: string + +text*[lncs1:: "lncs"]\\ +(*text*[lncs_aff1:: "lncs affiliation", journal_style = "@{lncs \lncs1\}"]\\*) +text*[lncs_auth1:: "lncs_author", affiliations = "[@{lncs \lncs1\}]"]\\ + + +doc_class "text_element" = + authored_by :: "author set" <= "{}" + level :: "int option" <= "None" + invariant authors_req :: "authored_by \ \ {}" + and level_req :: "the (level \) > 1" + +doc_class "introduction" = "text_element" + + authored_by :: "(author) set" <= "UNIV" + +doc_class "technical" = "text_element" + + formal_results :: "thm list" + +doc_class "definition" = "technical" + + is_formal :: "bool" + +doc_class "theorem" = "technical" + + is_formal :: "bool" + assumptions :: "term list" <= "[]" + statement :: "term option" <= "None" + +doc_class "conclusion" = "text_element" + + resumee :: "(definition set \ theorem set)" + invariant is_form :: "(\x\(fst (resumee \)). definition.is_formal x) \ + (\y\(snd (resumee \)). is_formal y)" + +text*[def::"definition", is_formal = "True"]\\ +text*[theo::"theorem", is_formal = "False"]\\ +text*[conc::"conclusion", resumee="({@{definition \def\}}, {@{theorem \theo\}})"]\\ + +value*\resumee @{conclusion \conc\} |> fst\ +value*\resumee @{conclusion \conc\} |> snd\ + +doc_class "article" = + style_id :: string <= "''LNCS''" + accepts "(title ~~ \author\\<^sup>+ ~~ \introduction\\<^sup>+ + ~~ \\definition ~~ example\\<^sup>+ || theorem\\<^sup>+ ~~ \conclusion\\<^sup>+)" + + +definition elsevier_to_acm_morphism :: "elsevier \ M_04_Document_Ontology.acm" + ("_ \acm\\<^sub>e\<^sub>l\<^sub>s\<^sub>e\<^sub>v\<^sub>i\<^sub>e\<^sub>r" [1000]999) + where "\ \acm\\<^sub>e\<^sub>l\<^sub>s\<^sub>e\<^sub>v\<^sub>i\<^sub>e\<^sub>r = + \ M_04_Document_Ontology.acm.tag_attribute = 1::int, + M_04_Document_Ontology.acm.position = ''no position'', + M_04_Document_Ontology.acm.institution = organization \, + M_04_Document_Ontology.acm.department = 0, + M_04_Document_Ontology.acm.street_address = address_line \, + M_04_Document_Ontology.acm.city = elsevier.city \, + M_04_Document_Ontology.acm.state = 0, + M_04_Document_Ontology.acm.country = ''no country'', + M_04_Document_Ontology.acm.postcode = elsevier.postcode \ \" + +(*definition elsevier_aff_to_acm_aff_morphism :: "elsevier affiliation \ Introduction.acm Introduction.affiliation" + ("_ \acm'_aff\\<^sub>e\<^sub>l\<^sub>s\<^sub>e\<^sub>v\<^sub>i\<^sub>e\<^sub>r'_\<^sub>a\<^sub>f\<^sub>f" [1000]999) + where "\ \acm_aff\\<^sub>e\<^sub>l\<^sub>s\<^sub>e\<^sub>v\<^sub>i\<^sub>e\<^sub>r_\<^sub>a\<^sub>f\<^sub>f = + \ Introduction.affiliation.tag_attribute = 1::int, + Introduction.affiliation.journal_style = (affiliation.journal_style \) + |> (\x. x \acm\\<^sub>e\<^sub>l\<^sub>s\<^sub>e\<^sub>v\<^sub>i\<^sub>e\<^sub>r) \"*) + +definition acm_name where "acm_name f s = f @ '' '' @ s" + +definition elsevier_author_to_acm_author_morphism :: "elsevier_author \ M_04_Document_Ontology.acm_author" + ("_ \acm'_auth\\<^sub>e\<^sub>l\<^sub>s\<^sub>e\<^sub>v\<^sub>i\<^sub>e\<^sub>r'_\<^sub>a\<^sub>u\<^sub>t\<^sub>h" [1000]999) + where "\ \acm_auth\\<^sub>e\<^sub>l\<^sub>s\<^sub>e\<^sub>v\<^sub>i\<^sub>e\<^sub>r_\<^sub>a\<^sub>u\<^sub>t\<^sub>h = + \ M_04_Document_Ontology.author.tag_attribute = 1::int, + M_04_Document_Ontology.author.name = acm_name (firstname \) (surname \), + M_04_Document_Ontology.author.email = author.email \, + M_04_Document_Ontology.acm_author.affiliations = (elsevier_author.affiliations \) + |> map (\x. x \acm\\<^sub>e\<^sub>l\<^sub>s\<^sub>e\<^sub>v\<^sub>i\<^sub>e\<^sub>r) , + + M_04_Document_Ontology.acm_author.orcid = 0, + M_04_Document_Ontology.acm_author.footnote = elsevier_author.footnote \ \" + + +lemma elsevier_inv_preserved : + "ne_fsnames_inv \ \ M_04_Document_Ontology.ne_name_inv (\ \acm_auth\\<^sub>e\<^sub>l\<^sub>s\<^sub>e\<^sub>v\<^sub>i\<^sub>e\<^sub>r_\<^sub>a\<^sub>u\<^sub>t\<^sub>h)" + unfolding ne_fsnames_inv_def M_04_Document_Ontology.ne_name_inv_def + elsevier_author_to_acm_author_morphism_def + by (simp add: combinator1_def acm_name_def) + +lemma elsevier_author_to_acm_author_morphism_total : + "elsevier_author_to_acm_author_morphism ` ({X::elsevier_author. ne_fsnames_inv X}) \ ({X::M_04_Document_Ontology.acm_author. M_04_Document_Ontology.ne_name_inv X})" + using elsevier_inv_preserved + by auto + +ML\ +fun add_onto_morphism classes_mappings eqs thy = + if (length classes_mappings = length eqs) then + let + val specs = map (fn x => (Binding.empty_atts, x)) eqs + val converts = + map (fn (oclasses, dclass) => + let + val oclasses_string = map YXML.content_of oclasses + val dclass_string = YXML.content_of dclass + val const_sub_name = dclass_string + |> (oclasses_string |> fold_rev (fn x => fn y => x ^ "_" ^ y)) + |> String.explode |> map (fn x => "\<^sub>" ^ (String.str x)) |> String.concat + val convert_typ = oclasses_string |> rev |> hd + |> (oclasses_string |> rev |> tl |> fold (fn x => fn y => x ^ " \ " ^ y)) + val convert_typ' = convert_typ ^ " \ " ^ dclass_string + val oclasses_sub_string = oclasses_string + |> map (fn x => x |> String.explode |> map (fn y => "\<^sub>" ^ (String.str y)) |> String.concat) + val mixfix = oclasses_sub_string |> rev |> hd + |> (oclasses_sub_string |> rev |> tl |> fold (fn x => fn y => x ^ "\<^sub>\" ^ y)) + val mixfix' = "convert" ^ mixfix ^ "\<^sub>\" + ^ (dclass_string |> String.explode + |> map (fn x => "\<^sub>" ^ (String.str x)) |> String.concat) + in SOME (Binding.name ("convert" ^ const_sub_name), SOME convert_typ', Mixfix.mixfix mixfix') end) + classes_mappings + val args = map (fn (x, y) => (x, y, [], [])) (converts ~~ specs) + val lthy = Named_Target.theory_init thy + val updated_lthy = fold (fn (decl, spec, prems, params) => fn lthy => + let + val (_, lthy') = Specification.definition_cmd decl params prems spec true lthy + in lthy' end) args lthy + in Local_Theory.exit_global updated_lthy end + (* alternative way to update the theory using the Theory.join_theory function *) + (*val lthys = map (fn (decl, spec, prems, params) => + let + val (_, lthy') = Specification.definition_cmd decl params prems spec true lthy + in lthy' end) args + val thys = map (Local_Theory.exit_global) lthys + + in Theory.join_theory thys end*) + else error("The number of morphisms declarations does not match the number of definitions") + +fun add_onto_morphism' (classes_mappings, eqs) = add_onto_morphism classes_mappings eqs + +val parse_onto_morphism = Parse.and_list + ((Parse.$$$ "(" |-- Parse.enum1 "," Parse.typ --| Parse.$$$ ")" --| \<^keyword>\to\) + -- Parse.typ) + -- (\<^keyword>\where\ |-- Parse.and_list Parse.prop) + +(* The name of the definitions must follow this rule: + for the declaration "onto_morphism (AA, BB) to CC", + the name of the constant must be "convert\<^sub>A\<^sub>A\<^sub>\\<^sub>B\<^sub>B\<^sub>\\<^sub>C\<^sub>C". + See the examples below. + *) +val _ = + Outer_Syntax.command \<^command_keyword>\onto_morphism\ "define ontology morpism" + (parse_onto_morphism >> (Toplevel.theory o add_onto_morphism')); + +\ + +find_consts name:"convert" + +doc_class AA = +aa :: int +doc_class BB = +bb :: int +doc_class CC = +cc :: int +doc_class DD = +dd :: int +doc_class EE = +ee :: int +doc_class FF = +ff :: int + +onto_morphism (AA, BB) to CC + and (DD, EE) to FF + where "convert\<^sub>A\<^sub>A\<^sub>\\<^sub>B\<^sub>B\<^sub>\\<^sub>C\<^sub>C \ = \ CC.tag_attribute = 1::int, CC.cc = aa (fst \) + bb (snd \)\" + and "convert\<^sub>D\<^sub>D\<^sub>\\<^sub>E\<^sub>E\<^sub>\\<^sub>F\<^sub>F \ = \ FF.tag_attribute = 1::int, FF.ff = dd (fst \) + ee (snd \) \" + +onto_morphism (AA, BB, CC, DD, EE) to FF + where "convert\<^sub>A\<^sub>A\<^sub>\\<^sub>B\<^sub>B\<^sub>\\<^sub>C\<^sub>C\<^sub>\\<^sub>D\<^sub>D\<^sub>\\<^sub>E\<^sub>E\<^sub>\\<^sub>F\<^sub>F \ = \ FF.tag_attribute = 1::int, FF.ff = aa (fst \) + bb (fst (snd \))\" + +find_consts name:"convert" +find_theorems name:"convert" + +(*>*) + + +chapter*[onto_proofs::technical]\Proofs on Ontologies\ + + +(*<*) +end +(*>*) + diff --git a/Isabelle_DOF/thys/manual/M_04_RefMan.thy b/Isabelle_DOF/thys/manual/M_06_RefMan.thy similarity index 100% rename from Isabelle_DOF/thys/manual/M_04_RefMan.thy rename to Isabelle_DOF/thys/manual/M_06_RefMan.thy diff --git a/Isabelle_DOF/thys/manual/M_05_Implementation.thy b/Isabelle_DOF/thys/manual/M_07_Implementation.thy similarity index 99% rename from Isabelle_DOF/thys/manual/M_05_Implementation.thy rename to Isabelle_DOF/thys/manual/M_07_Implementation.thy index b5dadd0..bea1f34 100644 --- a/Isabelle_DOF/thys/manual/M_05_Implementation.thy +++ b/Isabelle_DOF/thys/manual/M_07_Implementation.thy @@ -12,9 +12,9 @@ *************************************************************************) (*<*) -theory "M_05_Implementation" - imports "M_04_RefMan" -begin +theory "M_07_Implementation" + imports "M_06_RefMan" +begin (*>*)