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

Merged updates from main and ported them to Isabelle's development version.
ci/woodpecker/push/build Pipeline failed Details

This commit is contained in:
Achim D. Brucker 2023-03-05 10:29:16 +00:00
parent 684a775b07 5bf0b00fbc
commit cc805cadbe
30 changed files with 1563 additions and 402 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
.woodpecker/build.yml
View File

@ -2,14 +2,16 @@ pipeline:
build:
image: docker.io/logicalhacking/isabelle-dev
commands:
- ./.woodpecker/check_dangeling_theories
- ./.woodpecker/check_dangling_theories
- ./.woodpecker/check_external_file_refs
- ./.woodpecker/check_quick_and_dirty
- export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/$LATEX
- mkdir -p $ARTIFACT_DIR
- export `isabelle getenv ISABELLE_HOME_USER`
- mkdir -p $ISABELLE_HOME_USER/etc
- echo "ISABELLE_PDFLATEX=\"$LATEX --file-line-error\"" >> $ISABELLE_HOME_USER/etc/settings
- isabelle build -v -x HOL-Proofs -x Isabelle_DOF-Proofs -D . -o browser_info
- isabelle build -x HOL-Proofs -x Isabelle_DOF-Proofs -D . -o browser_info
- if [ "$LATEX" = "lualatex" ]; then isabelle build -o 'timeout_scale=2' -D . -o browser_info; else echo "Skipping Isabelle_DOF-Proofs for pdflatex build."; fi
- isabelle components -u .
- isabelle dof_mkroot -q DOF_test
- isabelle build -D DOF_test
@ -40,7 +42,7 @@ pipeline:
from_secret: artifacts_ssh
user: artifacts
notify:
image: drillster/drone-email
image: docker.io/drillster/drone-email
settings:
host: smtp.0x5f.org
username: woodpecker

8
.woodpecker/check_dangeling_theories
View File

@ -1,8 +0,0 @@
#!/bin/bash
PWD=`pwd`
TMPDIR=`mktemp -d`
isabelle build -D . -l -n | grep $PWD | sed -e "s| *${PWD}/||" | sort -u | grep thy$ > ${TMPDIR}/sessions-thy-files.txt
find * -type f | sort -u | grep thy$ > ${TMPDIR}/actual-thy-files.txt
echo "Theories that are not part of a Isabelle session:"
echo "================================================="
comm -13 ${TMPDIR}/sessions-thy-files.txt ${TMPDIR}/actual-thy-files.txt

33
.woodpecker/check_dangling_theories Executable file
View File

@ -0,0 +1,33 @@
#!/bin/bash
set -e
failuremsg="Error"
failurecode=1
while [ $# -gt 0 ]
do
case "$1" in
--warning|-w)
failuremsg="Warning"
failurecode=0;;
esac
shift
done
echo "Checking for theories that are not part of an Isabelle session:"
echo "==============================================================="
PWD=`pwd`
TMPDIR=`mktemp -d`
isabelle build -D . -l -n | grep $PWD | sed -e "s| *${PWD}/||" | sort -u | grep thy$ > ${TMPDIR}/sessions-thy-files.txt
find * -type f | sort -u | grep thy$ > ${TMPDIR}/actual-thy-files.txt
thylist=`comm -13 ${TMPDIR}/sessions-thy-files.txt ${TMPDIR}/actual-thy-files.txt`
if [ -z "$thylist" ] ; then
echo " * Success: No dangling theories found."
exit 0
else
echo -e "$thylist"
echo "$failuremsg: Dangling theories found (see list above)!"
exit $failurecode
fi

20
.woodpecker/check_external_file_refs
View File

@ -1,4 +1,20 @@
#!/bin/sh
failuremsg="Error"
failurecode=1
while [ $# -gt 0 ]
do
case "$1" in
--warning|-w)
failuremsg="Warning"
failurecode=0;;
esac
shift
done
DIRREGEXP="\\.\\./"
echo "Checking for references pointing outside of session directory:"
@ -21,8 +37,8 @@ done
if [ "$failed" -ne 0 ] ; then
echo "Error: Forbidden reference to files outside of their session directory!"
exit 1
echo "$failuremsg: Forbidden reference to files outside of their session directory!"
exit $failurecode
fi
echo " * Success: No relative references to files outside of their session directory found."

30
.woodpecker/check_quick_and_dirty Executable file
View File

@ -0,0 +1,30 @@
#!/bin/bash
set -e
failuremsg="Error"
failurecode=1
while [ $# -gt 0 ]
do
case "$1" in
--warning|-w)
failuremsg="Warning"
failurecode=0;;
esac
shift
done
echo "Checking for sessions with quick_and_dirty mode enabled:"
echo "========================================================"
rootlist=`find -name 'ROOT' -exec grep -l 'quick_and_dirty *= *true' {} \;`
if [ -z "$rootlist" ] ; then
echo " * Success: No sessions with quick_and_dirty mode enabled found."
exit 0
else
echo -e "$rootlist"
echo "$failuremsg: Sessions with quick_and_dirty mode enabled found (see list above)!"
exit $failurecode
fi

8
Isabelle_DOF-Example-Extra/CC_ISO15408/PikeOS_study/PikeOS_ST.thy
View File

@ -17,18 +17,20 @@ text*[pkosstref::st_ref_cls, title="''PikeOS Security Target''", st_version ="(0
It complies with the Common Criteria for Information Technology Security Evaluation
Version 3.1 Revision 4.\<close>
subsection*[pkossttoerefsubsec::st_ref_cls]\<open>TOE Reference\<close>
text*[pkostoeref::toe_ref_cls, dev_name="''''", toe_name="''PikeOS''",
toe_version= "(0,3,4)", prod_name="Some ''S3725''"]
\<open>The @{docitem toe_def} is the operating system PikeOS version 3.4
\<open>The @{docitem toeDef} is the operating system PikeOS version 3.4
running on the microprocessor family x86 hosting different applications.
The @{docitem toe_def} is referenced as PikeOS 3.4 base
The @{docitem toeDef} is referenced as PikeOS 3.4 base
product build S3725 for Linux and Windows development host with PikeOS 3.4
Certification Kit build S4250 and PikeOS 3.4 Common Criteria Kit build S4388.\<close>
subsection*[pkossttoeovrvwsubsec::st_ref_cls]\<open> TOE Overview \<close>
text*[pkosovrw1::toe_ovrw_cls]\<open>The @{definition \<open>toe\<close> } is a special kind of operating
text*[pkosovrw1::toe_ovrw_cls]\<open>The @{docitem \<open>toeDef\<close> } is a special kind of operating
system, that allows to effectively separate
different applications running on the same platform from each other. The TOE can host
user applications that can also be operating systems. User applications can also be

4
Isabelle_DOF-Example-Extra/CC_ISO15408/PikeOS_study/ROOT Normal file
View File

@ -0,0 +1,4 @@
session "PikeOS_study" = "Isabelle_DOF-Ontologies" +
options [document = false]
theories
"PikeOS_ST"

1
Isabelle_DOF-Example-Extra/CC_ISO15408/ROOTS Normal file
View File

@ -0,0 +1 @@
PikeOS_study

1
Isabelle_DOF-Example-Extra/ROOTS
View File

@ -2,3 +2,4 @@ scholarly_paper
technical_report
CENELEC_50128
cytology
CC_ISO15408

2
Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/ROOT
View File

@ -1,5 +1,5 @@
session "TR_MyCommentedIsabelle" = "Isabelle_DOF" +
options [document = pdf, document_output = "output", document_build = dof, quick_and_dirty = true]
options [document = pdf, document_output = "output", document_build = dof]
theories
"TR_MyCommentedIsabelle"
document_files

2
Isabelle_DOF-Example-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
View File

@ -1634,7 +1634,7 @@ val data = \<comment> \<open>Derived from Yakoub's example ;-)\<close>
, (\<open>Frédéric II\<close>, \<open>King of Sicily\<close>)
, (\<open>Frédéric III\<close>, \<open>the Handsome\<close>)
, (\<open>Frédéric IV\<close>, \<open>of the Empty Pockets\<close>)
, (\<open>Frédéric V\<close>, \<open>King of Denmark–Norway\<close>)
, (\<open>Frédéric V\<close>, \<open>King of Denmark-Norway\<close>)
, (\<open>Frédéric VI\<close>, \<open>the Knight\<close>)
, (\<open>Frédéric VII\<close>, \<open>Count of Toggenburg\<close>)
, (\<open>Frédéric VIII\<close>, \<open>Count of Zollern\<close>)

23
Isabelle_DOF-Ontologies/CC_v3_1_R5/CC_v3_1_R5.thy
View File

@ -47,7 +47,7 @@ doc_class toe_ref_cls = CC_text_element +
toe_version:: "(int \<times> int \<times> int)"
prod_name::"string option" <= None
(*
doc_class toe_ovrw_cls = CC_text_element +
toe_type :: string
software_req :: "CC_text_element list" <= "[]"
@ -55,26 +55,25 @@ doc_class toe_ovrw_cls = CC_text_element +
firmeware_req:: "CC_text_element list" <= "[]"
features_req :: "CC_text_element list" <= "[]"
invariant eal_consistency::
"\<lambda> X::toe_ovrw_cls .
(case eval_level X of
EAL1 \<Rightarrow> software_req X \<noteq> []
| EAL2 \<Rightarrow> software_req X \<noteq> []
| EAL3 \<Rightarrow> software_req X \<noteq> []
| EAL4 \<Rightarrow> software_req X \<noteq> []
"(case eval_level \<sigma> of
EAL1 \<Rightarrow> software_req \<sigma> \<noteq> []
| EAL2 \<Rightarrow> software_req \<sigma> \<noteq> []
| EAL3 \<Rightarrow> software_req \<sigma> \<noteq> []
| EAL4 \<Rightarrow> software_req \<sigma> \<noteq> []
| _ \<Rightarrow> undefined)"
thm eal_consistency_inv_def
*)
doc_class toe_desc_cls = CC_text_element +
software_list :: "CC_text_element list" <= "[]"
hardware_list :: "CC_text_element list" <= "[]"
firmeware_list :: "CC_text_element list" <= "[]"
sec_features_list:: "CC_text_element list" <= "[]"
(*
doc_class ST_INTRO_MNT = CC_structure_element +
tag_id:: string
accepts "\<lbrace>st_ref_cls\<rbrace>\<^sup>* ~~ \<lbrace>toe_ref_cls\<rbrace>\<^sup>* ~~ \<lbrace>toe_ovrw_cls\<rbrace>\<^sup>* ~~ \<lbrace>toe_desc_cls\<rbrace>\<^sup>*"
*)
doc_class cc_conf_claim_cls = CC_text_element +
cc_version:: string
ext_srs_list::"CC_text_element list option"
@ -162,7 +161,7 @@ doc_class sars_ratio_cls = CC_text_element +
doc_class SEC_REQ_MNT =
spd_id:: string
accepts "(\<lbrace>sfrs_cls\<rbrace>\<^sup>+ ~~ \<lbrace>sfrs_ratio_cls\<rbrace>\<^sup>+ ~~ \<lbrace>sars_cls\<rbrace>\<^sup>+ ~~ \<lbrace>sars_ratio_cls\<rbrace>\<^sup>+)"
(*
doc_class ST_MNT = CC_structure_element +
tag_id :: string
level :: EALs
@ -171,6 +170,6 @@ doc_class ST_MNT = CC_structure_element +
SEC_PROB_DEF_MNT ~~
SEC_OBJ_MNT ~~
SEC_REQ_MNT)"
*)
end

13
Isabelle_DOF-Ontologies/CENELEC_50128/CENELEC_50128.thy
View File

@ -1038,8 +1038,10 @@ fun check_sil oid _ ctxt =
setup\<open>
(fn thy =>
let val ctxt = Proof_Context.init_global thy
val binding = DOF_core.binding_from_onto_class_pos "monitor_SIL0" thy
in DOF_core.add_ml_invariant binding check_sil thy end)
val cid = "monitor_SIL0"
val binding = DOF_core.binding_from_onto_class_pos cid thy
val cid_long = DOF_core.get_onto_class_name_global cid thy
in DOF_core.add_ml_invariant binding (DOF_core.make_ml_invariant (check_sil, cid_long)) thy end)
\<close>
text\<open>
@ -1114,8 +1116,11 @@ fun check_required_documents oid _ ctxt =
setup\<open>
fn thy =>
let val ctxt = Proof_Context.init_global thy
val binding = DOF_core.binding_from_onto_class_pos "monitor_SIL0" thy
in DOF_core.add_closing_ml_invariant binding check_required_documents thy end
val cid = "monitor_SIL0"
val binding = DOF_core.binding_from_onto_class_pos cid thy
val cid_long = DOF_core.get_onto_class_name_global cid thy
in DOF_core.add_closing_ml_invariant binding
(DOF_core.make_ml_invariant (check_required_documents, cid_long)) thy end
\<close>
(* Test pattern matching for the records of the current CENELEC implementation classes,

131
Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy
View File

@ -20,12 +20,14 @@ imports
"Isabelle_DOF.Isa_COL"
begin
section\<open>Excursion: On the semantic consequences of this definition: \<close>
text\<open>Consider the following document class definition and its consequences:\<close>
doc_class A =
level :: "int option"
x :: int
section\<open>Excursion: On the semantic consequences of this definition: \<close>
text\<open>This class definition leads an implicit Isabelle/HOL \<^theory_text>\<open>record\<close> definition
(cf. \<^url>\<open>https://isabelle.in.tum.de/doc/isar-ref.pdf\<close>, chapter 11.6.).
@ -49,23 +51,61 @@ Consequently, \<^theory_text>\<open>doc_class\<close>'es inherit the entire theo
\<^enum> @{thm [display] A.simps(6)}
\<^enum> ...
\<close>
(* the generated theory of the \<^theory_text>\<open>doc_class\<close> A can be inspected, of course, by *)
text\<open>The generated theory of the \<^theory_text>\<open>doc_class\<close> A can be inspected, of course, by:\<close>
find_theorems (60) name:Conceptual name:A
text\<open>A more abstract view on the state of the DOF machine can be found here:\<close>
print_doc_classes
print_doc_items
text\<open>... and an ML-level output:\<close>
ML\<open>
val docitem_tab = DOF_core.get_instances \<^context>;
val isa_transformer_tab = DOF_core.get_isa_transformers \<^context>;
val docclass_tab = DOF_core.get_onto_classes \<^context>;
\<close>
ML\<open>
Name_Space.dest_table docitem_tab;
Name_Space.dest_table isa_transformer_tab;
Name_Space.dest_table docclass_tab;
\<close>
text\<open>... or as ML assertion: \<close>
ML\<open>
@{assert} (Name_Space.dest_table docitem_tab = []);
fun match ("Conceptual.A", (* the long-name *)
DOF_core.Onto_Class {params, name, virtual,inherits_from=NONE,
attribute_decl, rejectS=[],rex=[], invs=[]})
= (Binding.name_of name = "A")
| match _ = false;
@{assert} (exists match (Name_Space.dest_table docclass_tab))
\<close>
text\<open>As a consequence of the theory of the \<^theory_text>\<open>doc_class\<close> \<open>A\<close>, the code-generator setup lets us
evaluate statements such as: \<close>
value\<open> the(A.level (A.make 3 (Some 4) 5)) = 4\<close>
text\<open>And finally, as a consequence of the above semantic construction of \<^theory_text>\<open>doc_class\<close>'es, the internal
text\<open>And further, as a consequence of the above semantic construction of \<^theory_text>\<open>doc_class\<close>'es, the internal
\<open>\<lambda>\<close>-calculus representation of class instances looks as follows:\<close>
ML\<open>
val tt = @{term \<open>the(A.level (A.make 3 (Some 4) 5))\<close>}
@{term \<open>the(A.level (A.make 3 (Some 4) 5))\<close>};
fun match (Const("Option.option.the",_) $
(Const ("Conceptual.A.level",_) $
(Const ("Conceptual.A.make", _) $ u $ v $ w))) = true
|match _ = false;
@{assert} (match @{term \<open>the(A.level (A.make 3 (Some 4) 5))\<close>})
\<close>
text\<open>For the code-generation, we have the following access to values representing class instances:\<close>
text\<open>And finally, via the code-generation, we have the following programmable
access to values representing class instances:\<close>
ML\<open>
val A_make = @{code A.make};
val zero = @{code "0::int"};
@ -75,9 +115,9 @@ val add = @{code "(+) :: int \<Rightarrow> int \<Rightarrow> int"};
A_make zero (SOME one) (add one one)
\<close>
section\<open>Building up a conceptual class hierarchy:\<close>
section\<open>An independent class-tree root: \<close>
text\<open>An independent class-tree root: \<close>
doc_class B =
level :: "int option"
@ -125,7 +165,7 @@ doc_class F =
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
text\<open>The effect of the invariant declaration is to provide intern HOL definitions for validation
functions of this invariant. They can be referenced as follows:\<close>
thm br_inv_def
thm br'_inv_def
@ -133,7 +173,7 @@ thm cr_inv_def
term "\<lparr>F.tag_attribute = 5, properties = [], r = [], u = undefined, s = [], b = {}, b' = []\<rparr>"
term "br' (\<lparr>F.tag_attribute = 5, properties = [], r = [], u = undefined, s = [], b = {}, b' = []\<rparr>) "
term "br'_inv (\<lparr>F.tag_attribute = 5, properties = [], r = [], u = undefined, s = [], b = {}, b' = []\<rparr>) "
text\<open>Now, we can use these definitions in order to generate code for these validation functions.
Note, however, that not everything that we can write in an invariant (basically: HOL) is executable,
@ -141,7 +181,7 @@ or even compilable by the code generator setup:\<close>
ML\<open> val cr_inv_code = @{code "cr_inv"} \<close> \<comment> \<open>works albeit thm is abstract ...\<close>
text\<open>while in :\<close>
(* ML\<open> val br_inv_code = @{code "br_inv"} \<close> \<comment>\<open>this does not work ...\<close> *)
ML\<open> val br_inv_code = @{code "br_inv"} \<close> \<comment>\<open>this does not work ...\<close>
text\<open>... the compilation fails due to the fact that nothing prevents the user
to define an infinite relation between \<^typ>\<open>A\<close> and \<^typ>\<open>C\<close>. However, the alternative
@ -151,74 +191,33 @@ ML\<open> val br'_inv_code = @{code "br'_inv"} \<close> \<comment> \<open>does w
text\<open>... is compilable ...\<close>
doc_class G = C +
g :: "thm" <= "@{thm \<open>HOL.refl\<close>}"
g :: "thm" <= "@{thm \<open>HOL.refl\<close>}" (* warning overriding attribute expected*)
doc_class M =
ok :: "unit"
accepts "A ~~ \<lbrace>C || D\<rbrace>\<^sup>* ~~ \<lbrakk>F\<rbrakk>"
text\<open>The final class and item tables look like this:\<close>
print_doc_classes
print_doc_items
(*
ML\<open> Document.state();\<close>
ML\<open> Outer_Syntax.command; \<close>
ML\<open> Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \<close>
*)
ML\<open>
let val class_ids_so_far = ["Conceptual.A", "Conceptual.B", "Conceptual.C", "Conceptual.D",
"Conceptual.E", "Conceptual.F", "Conceptual.G", "Conceptual.M",
"Isa_COL.figure", "Isa_COL.chapter", "Isa_COL.figure2", "Isa_COL.section",
"Isa_COL.subsection", "Isa_COL.figure_group", "Isa_COL.text_element",
"Isa_COL.subsubsection", "Isa_COL.side_by_side_figure"]
val docclass_tab = map fst (Name_Space.dest_table (DOF_core.get_onto_classes \<^context>));
in @{assert} (class_ids_so_far = docclass_tab) end\<close>
open_monitor*[aaa::M]
section*[test::A]\<open>Test and Validation\<close>
term\<open>Conceptual.M.make\<close>
text\<open>Defining some document elements to be referenced in later on in another theory: \<close>
text*[sdf]\<open> Lorem ipsum @{thm refl}\<close>
text*[ sdfg :: F] \<open> Lorem ipsum @{thm refl}\<close>
text*[ xxxy ] \<open> Lorem ipsum @{F \<open>sdfg\<close>} rate @{thm refl}\<close>
close_monitor*[aaa]
doc_class test_monitor_free =
tmhd :: int
doc_class test_monitor_head =
tmhd :: int
doc_class test_monitor_A = test_monitor_head +
tmA :: int
doc_class test_monitor_B = test_monitor_A +
tmB :: int
doc_class test_monitor_C = test_monitor_A +
tmC :: int
doc_class test_monitor_D = test_monitor_B +
tmD :: int
doc_class test_monitor_E = test_monitor_D +
tmE :: int
section\<open>For Test and Validation\<close>
doc_class monitor_M =
tmM :: int
rejects "test_monitor_A"
accepts "test_monitor_head ~~ test_monitor_B ~~ test_monitor_C"
text*[sdf] \<open> Lorem ipsum ... \<close> \<comment> \<open>anonymous reference\<close>
text*[sdfg :: F] \<open> Lorem ipsum ...\<close> \<comment> \<open>some F instance \<close>
declare[[free_class_in_monitor_checking]]
open_monitor*[test_monitor_M::monitor_M]
text*[testFree::test_monitor_free]\<open>\<close>
open_monitor*[test_monitor_M2::monitor_M]
text*[test_monitor_A1::test_monitor_A]\<open>\<close>
text*[testFree2::test_monitor_free]\<open>\<close>
text*[test_monitor_head1::test_monitor_head]\<open>\<close>
text*[testFree3::test_monitor_free]\<open>\<close>
text*[test_monitor_B1::test_monitor_B]\<open>\<close>
text*[testFree4::test_monitor_free]\<open>\<close>
text*[test_monitor_D1::test_monitor_D]\<open>\<close>
text*[testFree5::test_monitor_free]\<open>\<close>
text*[test_monitor_C1::test_monitor_C]\<open>\<close>
text*[testFree6::test_monitor_free]\<open>\<close>
close_monitor*[test_monitor_M2]
close_monitor*[test_monitor_M]
declare[[free_class_in_monitor_checking = false]]
end

13
Isabelle_DOF-Ontologies/small_math/small_math.thy
View File

@ -76,8 +76,11 @@ let fun check_invariant_invariant oid {is_monitor:bool} ctxt =
else error("class class invariant violation")
| _ => false
end
val binding = DOF_core.binding_from_onto_class_pos "result" thy
in DOF_core.add_ml_invariant binding check_invariant_invariant thy end
val cid = "result"
val cid_long = DOF_core.get_onto_class_name_global cid thy
val binding = DOF_core.binding_from_onto_class_pos cid thy
in DOF_core.add_ml_invariant binding
(DOF_core.make_ml_invariant (check_invariant_invariant, cid_long)) thy end
\<close>
(*setup\<open>DOF_core.add_ml_invariant "small_math.result" check_invariant_invariant\<close>*)
@ -175,8 +178,10 @@ let val cidS = ["small_math.introduction","small_math.technical", "small_math.co
fun body moni_oid _ ctxt = (Small_Math_trace_invariant.check ctxt cidS moni_oid NONE;
true)
val ctxt = Proof_Context.init_global thy
val binding = DOF_core.binding_from_onto_class_pos "article" thy
in DOF_core.add_ml_invariant binding body thy end
val cid = "article"
val cid_long = DOF_core.get_onto_class_name_global cid thy
val binding = DOF_core.binding_from_onto_class_pos cid thy
in DOF_core.add_ml_invariant binding (DOF_core.make_ml_invariant (body, cid_long)) thy end
\<close>
end

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

@ -16,9 +16,10 @@ theory
imports
"Isabelle_DOF-Unit-Tests_document"
"Isabelle_DOF-Ontologies.Conceptual"
Concept_MonitorTest1
begin
section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
ML\<open>@{assert} (1 = 1)\<close>
section\<open>Elementar Creation of Doc-items and Access of their Attibutes\<close>
text\<open>Current status:\<close>
print_doc_classes
@ -29,14 +30,15 @@ ML\<open>
val docitem_tab = DOF_core.get_instances \<^context>
val isa_transformer_tab = DOF_core.get_isa_transformers \<^context>
val docclass_tab = DOF_core.get_onto_classes @{context};
Name_Space.dest_table docitem_tab;
Name_Space.dest_table docclass_tab;
\<close>
ML\<open>
val (oid, DOF_core.Instance {value, ...}) =
Name_Space.check (Context.Proof \<^context>) (DOF_core.get_instances \<^context>) ("aaa", Position.none)
map fst (Name_Space.dest_table docitem_tab);
Name_Space.dest_table docclass_tab;
\<close>
find_theorems (60) name:"Conceptual.M."
value [simp]"M.trace(M.make undefined [] ())"
@ -128,7 +130,6 @@ DOF_core.get_attribute_info "Conceptual.C" "z" @{theory};
ML\<open>
DOF_core.get_value_local "sdf" @{context};
DOF_core.get_value_local "sdfg" @{context};
DOF_core.get_value_local "xxxy" @{context};
DOF_core.get_value_local "dfgdfg" @{context};
DOF_core.get_value_local "omega" @{context};
\<close>
@ -232,14 +233,13 @@ ML \<open>@{trace_attribute figs1}\<close>
text\<open>Resulting trace of figs as text antiquotation:\<close>
text\<open>@{trace_attribute figs1}\<close>
section\<open>A Complex Evaluation involving Automatas\<close>
text\<open>Test trace\_attribute term antiquotation:\<close>
term*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>
value*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>
term*\<open>map fst @{trace-attribute \<open>aaa\<close>}\<close>
value*\<open>map fst @{trace-attribute \<open>aaa\<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>
definition example_expression where "example_expression \<equiv> \<lbrace>\<lfloor>''Conceptual.A''\<rfloor> || \<lfloor>''Conceptual.F''\<rfloor>\<rbrace>\<^sup>*"
value* \<open> DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace-attribute \<open>aaa\<close>}) \<close>

71
Isabelle_DOF-Unit-Tests/Concept_Example.thy
View File

@ -1,71 +0,0 @@
(*************************************************************************
* Copyright (C)
* 2019 The University of Exeter
* 2018-2019 The 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
*************************************************************************)
chapter\<open>Setting and modifying attributes of doc-items\<close>
theory
Concept_Example
imports
"Isabelle_DOF-Unit-Tests_document"
"Isabelle_DOF-Ontologies.Conceptual" (* we use the generic "Conceptual" ontology *)
begin
text\<open>@{theory "Isabelle_DOF-Ontologies.Conceptual"} provides a monitor @{typ M} enforcing a particular document structure.
Here, we say: From now on, this structural rules are respected wrt. all doc\_classes M is
enabled for.\<close>
open_monitor*[struct::M]
section*[a::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... \<close>
text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
text*[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus,
... @{C "c1"} @{thm "refl"} \<close>
update_instance*[d::D, a1 := X2]
text\<open> ... in ut tortor ... @{docitem \<open>a\<close>} ... @{A \<open>a\<close>}\<close>
text*[c2::C, x = "\<open>delta\<close>"] \<open> ... in ut tortor eleifend augue pretium consectetuer. \<close>
text\<open>Note that both the notations @{term "''beta''"} and @{term "\<open>beta\<close>"} are possible;
the former is a more ancient format only supporting pure ascii, while the latter also supports
fancy unicode such as: @{term "\<open>\<beta>\<^sub>i''\<close>"} \<close>
text*[f::F] \<open> Lectus accumsan velit ultrices, ... \<close>
theorem some_proof : "True" by simp
text\<open>This is an example where we add a theorem into a kind of "result-list" of the doc-item f.\<close>
update_instance*[f::F,r:="[@{thm ''Concept_Example.some_proof''}]"]
text\<open> ..., mauris amet, id elit aliquam aptent id, ... @{docitem \<open>a\<close>} \<close>
text\<open>Here we add and maintain a link that is actually modeled as m-to-n relation ...\<close>
update_instance*[f::F,b:="{(@{docitem \<open>a\<close>}::A,@{docitem \<open>c1\<close>}::C),
(@{docitem \<open>a\<close>}, @{docitem \<open>c2\<close>})}"]
close_monitor*[struct]
text\<open>And the trace of the monitor is:\<close>
ML\<open>@{trace_attribute struct}\<close>
print_doc_classes
print_doc_items
end

68
Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy
View File

@ -1,7 +1,7 @@
(*************************************************************************
* Copyright (C)
* 2019 The University of Exeter
* 2018-2019 The University of Paris-Saclay
* 2019-2023 The University of Exeter
* 2018-2023 The University of Paris-Saclay
* 2018 The University of Sheffield
*
* License:
@ -11,22 +11,28 @@
* SPDX-License-Identifier: BSD-2-Clause
*************************************************************************)
chapter\<open>Setting and modifying attributes of doc-items\<close>
chapter\<open>Testing hand-programmed (low-level) Invariants\<close>
theory
Concept_Example_Low_Level_Invariant
theory Concept_Example_Low_Level_Invariant
imports
"Isabelle_DOF-Unit-Tests_document"
"Isabelle_DOF-Ontologies.Conceptual" (* we use the generic "Conceptual" ontology *)
TestKit
begin
section\<open>Example: Standard Class Invariant\<close>
section\<open>Test Purpose.\<close>
text\<open> Via @{ML "DOF_core.add_ml_invariant"} it is possible to attach user-defined
ML-code to classes which is executed at each creation or modification of
class instances. We test exection of creation and updates. \<close>
text\<open>Status:\<close>
text\<open>Consult the status of the DOF engine:\<close>
print_doc_classes
print_doc_items
section\<open>Example: Standard Class Invariant\<close>
text\<open>Watch out: The current programming interface to document class invariants is pretty low-level:
\<^item> No inheritance principle
\<^item> No high-level notation in HOL
@ -35,39 +41,44 @@ The implementor of an ontology must know what he does ...
\<close>
text\<open>Setting a sample invariant, which simply produces some side-effect:\<close>
setup\<open>
fn thy =>
let val ctxt = Proof_Context.init_global thy
val binding = DOF_core.binding_from_onto_class_pos "A" thy
in DOF_core.add_ml_invariant binding (fn oid =>
fn {is_monitor = b} =>
fn ctxt =>
(writeln ("sample echo : "^oid); true)) thy end
val cid_long = DOF_core.get_onto_class_name_global "A" thy
val bind = Binding.name "Sample_Echo"
val exec = (fn oid => fn {is_monitor = b} => fn ctxt =>
(writeln ("sample echo : "^oid); true))
in DOF_core.add_ml_invariant bind (DOF_core.make_ml_invariant (exec, cid_long)) thy end
\<close>
subsection*[b::A, x = "5"] \<open> Lorem ipsum dolor sit amet, ... \<close>
text\<open>The checker \<open>exec\<close> above is set. Just used to provoke output: "sample echo : b"\<close>
text*[b::A, x = "5"] \<open> Lorem ipsum dolor sit amet, ... \<close>
text\<open>Setting a sample invariant, referring to attribute value "x":\<close>
ML\<open>
setup\<open>
fn thy =>
let fun check_A_invariant oid {is_monitor:bool} ctxt =
let val term = ISA_core.compute_attr_access ctxt "x" oid NONE @{here}
val (@{typ "int"},x_value) = HOLogic.dest_number term
in if x_value > 5 then error("class A invariant violation") else true end
val binding = DOF_core.binding_from_onto_class_pos "A" thy
in DOF_core.add_ml_invariant binding check_A_invariant thy end
in if x_value > 5 then error("class A invariant violation") else true end
val cid_long = DOF_core.get_onto_class_name_global "A" thy
val bind = Binding.name "Check_A_Invariant"
in DOF_core.add_ml_invariant bind (DOF_core.make_ml_invariant (check_A_invariant, cid_long)) thy end
\<close>
(* borderline test *)
text*[d0::A, x = "5"] \<open>Lorem ipsum dolor sit amet, ...\<close>
text-assert-error[d1::A, x = "6"]\<open>Lorem ipsum dolor sit amet, ...\<close>\<open>class A invariant violation\<close>
subsection*[d::A, x = "4"] \<open> Lorem ipsum dolor sit amet, ... \<close>
(* test : update should not fail, invariant still valid *)
(* invariant still valid *)
update_instance*[d::A, x += "1"]
(* test : with the next step it should fail :
update_instance*[d::A, x += "1"]
*)
(* invariant no longer holds*)
update_instance-assert-error[d::A, x += "1"]\<open>class A invariant violation\<close>
section\<open>Example: Monitor Class Invariant\<close>
@ -86,7 +97,7 @@ that instances of class C occur more often as those of class D; note that this i
to take sub-classing into account:
\<close>
ML\<open>
setup\<open>
fn thy =>
let fun check_M_invariant oid {is_monitor} ctxt =
let val term = ISA_core.compute_attr_access ctxt "trace" oid NONE @{here}
@ -102,8 +113,9 @@ let fun check_M_invariant oid {is_monitor} ctxt =
val n = length (filter is_C cid_list)
val m = length (filter is_D cid_list)
in if m > n then error("class M invariant violation") else true end
val binding = DOF_core.binding_from_onto_class_pos "M" thy
in DOF_core.add_ml_invariant binding check_M_invariant thy end
val cid_long = DOF_core.get_onto_class_name_global "M" thy
val binding = Binding.name "Check_M_Invariant"
in DOF_core.add_ml_invariant binding (DOF_core.make_ml_invariant (check_M_invariant, cid_long)) thy end
\<close>
@ -121,9 +133,9 @@ text*[c2:: C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium
subsection*[f::E] \<open> Lectus accumsan velit ultrices, ... \<close>
(*
section*[f2::E] \<open> Lectus accumsan velit ultrices, ... \<close>
*)
text-assert-error[f2::E] \<open> Lectus accumsan velit ultrices, ... \<close>\<open>class M invariant violation\<close>
ML\<open>val ctxt = @{context}
val term = ISA_core.compute_attr_access

111
Isabelle_DOF-Unit-Tests/Concept_MonitorTest1.thy Normal file
View File

@ -0,0 +1,111 @@
(*************************************************************************
* Copyright (C)
* 2019-2023 The University of Exeter
* 2018-2023 The 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
*************************************************************************)
chapter\<open>Testing Nested Monitors\<close>
theory
Concept_MonitorTest1
imports
"Isabelle_DOF-Unit-Tests_document"
"Isabelle_DOF-Ontologies.Conceptual" (* we use the generic "Conceptual" ontology *)
TestKit
begin
section\<open>Test Purpose.\<close>
text\<open> Creation of document parts that are controlled by (nested, locally defined) monitors. \<close>
open_monitor*[aaa::Conceptual.M]
text*[test::A]\<open>For Test and Validation\<close>
text\<open>Defining some document elements to be referenced in later on in another theory: \<close>
text*[sdf] \<open> Lorem ipsum ... \<close> \<comment> \<open>anonymous reference, ignored by monitor.\<close>
text*[sdfg :: F] \<open> Lorem ipsum ...\<close> \<comment> \<open>causes just warnings for invariant violations
due to non-strict checking mode\<close>
close_monitor*[aaa] \<comment> \<open>causes warning: accept clause 1
not in final state .\<close>
section\<open>A Local Monitor Class Definition\<close>
doc_class test_monitor_free =
tmhd :: int
doc_class test_monitor_head =
tmhd :: int
doc_class test_monitor_A = test_monitor_head +
tmA :: int
doc_class test_monitor_B = test_monitor_A +
tmB :: int
doc_class test_monitor_C = test_monitor_A +
tmC :: int
doc_class test_monitor_D = test_monitor_B +
tmD :: int
doc_class test_monitor_E = test_monitor_D +
tmE :: int
doc_class monitor_M =
tmM :: int
rejects "test_monitor_A"
accepts "test_monitor_head ~~ test_monitor_B ~~ test_monitor_C"
section\<open>A more Complex Monitoring Example \<close>
text\<open>Consult the status of the DOF engine:\<close>
print_doc_classes
print_doc_items
declare[[free_class_in_monitor_checking]]
open_monitor*[test_monitor_M::monitor_M]
text*[testFree::test_monitor_free]\<open>...\<close>
open_monitor*[test_monitor_M2::monitor_M]
declare[[strict_monitor_checking]]
text-assert-error[test_monitor_A1::test_monitor_A]\<open>\<close>
\<open>accepts clause 1 of monitor Concept_MonitorTest1.test_monitor_M rejected\<close>
declare[[strict_monitor_checking=false]]
text*[test_monitor_A1::test_monitor_A]\<open>\<close> \<comment> \<open>the same in non-strict monitor checking.\<close>
text*[testFree2::test_monitor_free]\<open>\<close>
text*[test_monitor_head1::test_monitor_head]\<open>\<close>
text*[testFree3::test_monitor_free]\<open>\<close>
text*[test_monitor_B1::test_monitor_B]\<open>\<close>
text*[testFree4::test_monitor_free]\<open>\<close>
text*[test_monitor_D1::test_monitor_D]\<open>\<close>
text*[testFree5::test_monitor_free]\<open>\<close>
text*[test_monitor_C1::test_monitor_C]\<open>\<close>
text*[testFree6::test_monitor_free]\<open>\<close>
close_monitor*[test_monitor_M2]
close_monitor*[test_monitor_M]
declare[[free_class_in_monitor_checking = false]]
text\<open>Consult the final status of the DOF engine:\<close>
print_doc_classes
print_doc_items
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>
ML\<open>@{assert} ([("Conceptual.A", "test"), ("Conceptual.F", "sdfg")] = @{trace_attribute aaa}) \<close>
end

164
Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy Normal file
View File

@ -0,0 +1,164 @@
(*************************************************************************
* Copyright (C)
* 2019-2023 The University of Exeter
* 2018-2023 The 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
*************************************************************************)
chapter\<open>Creating and Referencing Ontological Instances\<close>
theory Concept_OntoReferencing
imports "TestKit"
"Isabelle_DOF-Unit-Tests_document"
"Isabelle_DOF-Ontologies.Conceptual"
begin
section\<open>Test Purpose.\<close>
text\<open> Creation of ontological instances along the \<^theory>\<open>Isabelle_DOF-Ontologies.Conceptual\<close>
Ontology. Emphasis is put on type-safe (ontologically consistent) referencing of text, code and
proof elements. Some tests cover also the critical cases concerning name spaces of oid's. \<close>
section\<open>Setting up a monitor.\<close>
text\<open>\<^theory>\<open>Isabelle_DOF-Ontologies.Conceptual\<close> provides a monitor \<^typ>\<open>M\<close> enforcing a
particular document structure. Here, we say: From now on, this structural rules are
respected wrt. all \<^theory_text>\<open>doc_classes M\<close> is enabled for.\<close>
open_monitor*[struct::M]
section\<open>Defining Text Elements and Referring to them... \<close>
text\<open> This uses elements of two ontologies, notably
\<^theory>\<open>Isabelle_DOF-Ontologies.Conceptual\<close> and \<^theory>\<open>Isabelle_DOF.Isa_COL\<close>.\<close>
(*<*)
title*[abbb::title, short_title="Some\<open>ooups.\<close>"]\<open>Lorem ipsum dolor sit amet ...\<close>
subtitle*[abbbb::subtitle, abbrev = "Some\<open>ooups-oups.\<close>"]\<open>Lorem ipsum dolor sit amet ...\<close>
chapter*[abbbbbb::A, x = "3"] \<open> Lorem ipsum dolor sit amet ... \<close>
section*[a::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... \<close>
subsection*[ab::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ...
As mentioned in the @{title \<open>abbb\<close>}... \<close> \<comment> \<open>old-style and ...\<close>
subsubsection*[abb::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ...
As mentioned in the \<^title>\<open>abbb\<close>\<close> \<comment> \<open>new-style references to
ontological instances
assigned to text
elements ...\<close>
(*>*)
text\<open>Meta-Objects are typed, and references have to respect this : \<close>
(*<*)
text-assert-error[ac]\<open> \<^title>\<open>a\<close> \<close> \<open>reference ontologically inconsistent\<close>
text-assert-error[ad]\<open> \<^title>\<open>abbbb\<close> \<close>\<open>reference ontologically inconsistent\<close>
\<comment> \<open>erroneous reference: please consider class hierarchy!\<close>
(*>*)
text\<open>References to Meta-Objects can be forward-declared:\<close>
text-assert-error[ae1]\<open>@{C \<open>c1\<close>}\<close>\<open>Undefined instance:\<close>
declare_reference*[c1::C] \<comment> \<open>forward declaration\<close>
text\<open>@{C \<open>c1\<close>} \<close> \<comment> \<open>THIS IS A BUG !!! OVERLY SIMPLISTIC BEHAVIOUR. THIS SHOULD FAIL! \<close>
text\<open>@{C (unchecked) \<open>c1\<close>} \<close> \<comment> \<open>THIS SHOULD BE THE CORRECT BEHAVIOUR! \<close>
text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
text-assert-error[c1::C, x = "''gamma''"]
\<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
\<open>Duplicate instance declaration\<close>
text*[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus,
... @{C "c1"} or @{C \<open>c1\<close>} or \<^C>\<open>c1\<close>
similar to @{thm "refl"} and \<^thm>"refl"\<close> \<comment> \<open>ontological and built-in
references\<close>
text\<open>Not only text-elements are "ontology-aware", proofs and code can this be too !\<close>
ML*[c4::C]\<open>fun fac x = if x = 0 then 1 else x * (fac(x-1))\<close> (* TODO : BUG *)
lemma*[e5::E] asd: "True" by simp
declare_reference-assert-error[c1::C]\<open>Duplicate instance declaration\<close> \<comment> \<open>forward declaration\<close>
declare_reference*[e6::E]
text\<open>This is the answer to the "OutOfOrder Presentation Problem": @{E (unchecked) \<open>e6\<close>} \<close>
definition*[e6::E] facu :: "nat \<Rightarrow> nat" where "facu arg = undefined"
text\<open>As shown in @{E [display]\<open>e5\<close>} following from @{E [display]\<open>e6\<close>}\<close>
(* BUG ?: why is option [display] necessary ? *)
text\<open>As shown in @{C [display]\<open>c4\<close>}\<close>
text\<open>Ontological information ("class instances") is mutable: \<close>
update_instance*[d::D, a1 := X2]
text\<open> ... in ut tortor ... @{docitem \<open>a\<close>} ... @{A \<open>a\<close>} ... \<close> \<comment> \<open>untyped or typed referencing \<close>
(* THIS IS A BUG : this weird option is necessary *)
text-assert-error[ae::text_element]\<open>the function @{C [display] "c4"} \<close>\<open>referred text-element is macro!\<close>
text*[c2::C, x = "\<open>delta\<close>"] \<open> ... in ut tortor eleifend augue pretium consectetuer. \<close>
text\<open>Note that both the notations @{term "''beta''"} and @{term "\<open>beta\<close>"} are possible;
the former is a more ancient format only supporting pure ascii, while the latter also supports
fancy unicode such as: @{term "\<open>\<beta>\<^sub>i''\<close>"} \<close>
text*[f::F] \<open> Lectus accumsan velit ultrices, ... \<close>
theorem some_proof : "True" by simp
text\<open>This is an example where we add a theorem into a kind of "result-list" of the doc-item f.\<close>
update_instance*[f::F,r:="[@{thm ''Concept_OntoReferencing.some_proof''}]"]
text\<open> ..., mauris amet, id elit aliquam aptent id, ... @{docitem \<open>a\<close>} \<close>
text\<open>Here we add and maintain a link that is actually modeled as m-to-n relation ...\<close>
update_instance*[f::F,b:="{(@{docitem \<open>a\<close>}::A,@{docitem \<open>c1\<close>}::C),
(@{docitem \<open>a\<close>}, @{docitem \<open>c2\<close>})}"]
section\<open>Closing the Monitor and testing the Results.\<close>
close_monitor*[struct]
text\<open>And the trace of the monitor is:\<close>
ML\<open>val trace = @{trace_attribute struct}\<close>
ML\<open>@{assert} (trace =
[("Conceptual.A", "abbbbbb"), ("Conceptual.A", "a"), ("Conceptual.A", "ab"), ("Conceptual.A", "abb"),
("Conceptual.C", "c1"), ("Conceptual.C", "c1"), ("Conceptual.D", "d"), ("Conceptual.C", "c4"),
("Conceptual.E", "e5"), ("Conceptual.E", "e6"), ("Conceptual.E", "e6"), ("Conceptual.C", "c2"),
("Conceptual.F", "f")]) \<close>
(* BUG : DECLARATIONS SHOULD NOT BE TRACED, JUST DEFINITIONS.
ML\<open>@{assert} (trace = [("Conceptual.A", "abbbbbb"), ("Conceptual.A", "a"), ("Conceptual.A", "ab"),
("Conceptual.A", "abb"), ("Conceptual.C", "c1"), ("Conceptual.D", "d"), ("Conceptual.C", "c4"),
("Conceptual.E", "e5"), ("Conceptual.E", "e6"), ("Conceptual.C", "c2"), ("Conceptual.F", "f")]) \<close>
*)
text\<open>Note that the monitor \<^typ>\<open>M\<close> of the ontology \<^theory>\<open>Isabelle_DOF-Ontologies.Conceptual\<close> does
not observe the common entities of \<^theory>\<open>Isabelle_DOF.Isa_COL\<close>, but just those defined in the
accept- clause of \<^typ>\<open>M\<close>.\<close>
text\<open>One final check of the status DOF core: observe that no new classes have been defined,
just a couple of new document elements have been introduced.\<close>
print_doc_classes
print_doc_items
end

10
Isabelle_DOF-Unit-Tests/Evaluation.thy
View File

@ -81,9 +81,9 @@ term*\<open>@{A \<open>xcv1\<close>}\<close>
text\<open>The instance class @{docitem \<open>xcv1\<close>} is not an instance of the class @{doc_class B}:
\<close>
(* Error:
term*\<open>@{B \<open>xcv1\<close>}\<close>*)
(* Error:
term*\<open>@{B \<open>xcv1\<close>}\<close>
*)
text\<open>We can evaluate the instance class. The current implementation returns
the value of the instance, i.e. a collection of every attribute of the instance:
\<close>
@ -158,10 +158,10 @@ value*\<open>@{A-instances}\<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.
In the following example, we request the instances of the @{doc_class A}.
But we have defined an instance @{docitem \<open>test\<close>} in theory @{theory "Isabelle_DOF-Ontologies.Conceptual"}
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>test\<close>}:\<close>
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>
section\<open>Limitations\<close>

438
Isabelle_DOF-Unit-Tests/Latex_Tests.thy Normal file
View File

@ -0,0 +1,438 @@
(*************************************************************************
* Copyright (C)
* 2019-2023 The University of Exeter
* 2018-2023 The 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 Latex_Tests
imports "TestKit"
"Isabelle_DOF-Unit-Tests_document"
keywords "Figure*" :: document_body (* still experimental feature *)
begin
section\<open>Test Purpose.\<close>
text\<open> Testing the generation of LaTeX code. Serves in particular during development. \<close>
text\<open>Output status:\<close>
print_doc_classes
print_doc_items
section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
text\<open>And here a tex - text macro.\<close>
text\<open>Pythons ReStructuredText (RST).
@{url \<open>https://de.wikipedia.org/wiki/ReStructuredText\<close>}. Tool: Sphinx.
\<close>
text*[aaaa::B]\<open>dfg @{thm [display] refl}\<close>
text-[dfgdfg::B]
\<open> Lorem ipsum ... @{thm [display] refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
text-latex\<open> Lorem ipsum ... @{thm [display] refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
text-[asd::B]
\<open>... and here is its application macro expansion:
@{B [display] "dfgdfg"}
\textbf{TEST}
@{cartouche [display]
\<open>text*[dfgdfg::B]
\<open> Lorem ipsum ... @{thm refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
\<close>}
\<close>
text-latex\<open>... and here is its application macro expansion:
@{B [display] "dfgdfg"}
\textbf{TEST}
@{cartouche [display]
\<open>text*[dfgdfg::B]
\<open> Lorem ipsum ... @{thm refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
\<close>}\<close>
(*<*)
text-latex\<open> \<^theory_text>\<open>definition df = ...
\<close>
@{ML [display] \<open> let val x = 3 + 4 in true end
\<close>}
@{ML_text [display] \<open> val x = ...
\<close>}
@{verbatim [display] \<open> Lorem ipsum ... @{thm refl}
Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>}
@{theory_text [display] \<open>definition df = ... \<lambda>x.
\<close>}
@{cartouche [display] \<open> @{figure "cfgdfg"}\<close>} \<close>
(*>*)
text\<open>Final Status:\<close>
print_doc_items
print_doc_classes
section\<open>Experiments on Inline-Textelements\<close>
text\<open>Std Abbreviations. Inspired by the block *\<open>control spacing\<close>
in @{file \<open>$ISABELLE_HOME/src/Pure/Thy/document_antiquotations.ML\<close>}.
We mechanize the table-construction and even attach the LaTeX
quirks to be dumped into the prelude. \<close>
ML\<open>
val _ =
Theory.setup
( Document_Output.antiquotation_raw \<^binding>\<open>doof\<close> (Scan.succeed ())
(fn _ => fn () => Latex.string "\\emph{doof}")
#> Document_Output.antiquotation_raw \<^binding>\<open>LATEX\<close> (Scan.succeed ())
(fn _ => fn () => Latex.string "\\textbf{LaTeX}")
)
\<close>
text-latex\<open> \<^doof> \<^LATEX> \<close>
(* the same effect is achieved with : *)
setup \<open>DOF_lib.define_shortcut (Binding.make("bla",\<^here>)) "\\blabla"\<close>
(* Note that this assumes that the generated LaTeX macro call "\blabla" is defined somewhere in the
target document, for example, in the tex prelude. Note that the "Binding.make" can be avoided
using the alternative \<^binding> notation (see above).*)
setup\<open>DOF_lib.define_macro (Binding.make("blong",\<^here>)) "\\blong{" "}" (K(K()))\<close>
(*<*)
text-latex\<open> \<^blong>\<open>asd\<close> outer \<^blong>\<open>syntax| ! see {syntax, outer}\<close> \<close>
(*>*)
section\<open>Experimental Code and Test of advanced LaTeX for free-form text units\<close>
ML\<open>
fun report_text ctxt text =
let val pos = Input.pos_of text in
Context_Position.reports ctxt
[(pos, Markup.language_text (Input.is_delimited text)),
(pos, Markup.raw_text)]
end;
fun report_theory_text ctxt text =
let val keywords = Thy_Header.get_keywords' ctxt;
val _ = report_text ctxt text;
val _ =
Input.source_explode text
|> Token.tokenize keywords {strict = true}
|> maps (Token.reports keywords)
|> Context_Position.reports_text ctxt;
in () end
fun prepare_text ctxt =
Input.source_content #> #1 #> Document_Antiquotation.prepare_lines ctxt;
(* This also produces indent-expansion and changes space to "\_" and the introduction of "\newline",
I believe. Otherwise its in Thy_Output.output_source, the compiler from string to LaTeX.text. *)
fun string_2_text_antiquotation ctxt text =
prepare_text ctxt text
|> Document_Output.output_source ctxt
|> Document_Output.isabelle ctxt
fun string_2_theory_text_antiquotation ctxt text =
let
val keywords = Thy_Header.get_keywords' ctxt;
in
prepare_text ctxt text
|> Token.explode0 keywords
|> maps (Document_Output.output_token ctxt)
|> Document_Output.isabelle ctxt
end
fun gen_text_antiquotation name reportNcheck compile =
Document_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input)
(fn ctxt => fn text:Input.source =>
let
val _ = reportNcheck ctxt text;
in
compile ctxt text
end);
fun std_text_antiquotation name (* redefined in these more abstract terms *) =
gen_text_antiquotation name report_text string_2_text_antiquotation
(* should be the same as (2020):
fun text_antiquotation name =
Thy_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input)
(fn ctxt => fn text =>
let
val _ = report_text ctxt text;
in
prepare_text ctxt text
|> Thy_Output.output_source ctxt
|> Thy_Output.isabelle ctxt
end);
*)
fun std_theory_text_antiquotation name (* redefined in these more abstract terms *) =
gen_text_antiquotation name report_theory_text string_2_theory_text_antiquotation
(* should be the same as (2020):
fun theory_text_antiquotation name =
Thy_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input)
(fn ctxt => fn text =>
let
val keywords = Thy_Header.get_keywords' ctxt;
val _ = report_text ctxt text;
val _ =
Input.source_explode text
|> Token.tokenize keywords {strict = true}
|> maps (Token.reports keywords)
|> Context_Position.reports_text ctxt;
in
prepare_text ctxt text
|> Token.explode0 keywords
|> maps (Thy_Output.output_token ctxt)
|> Thy_Output.isabelle ctxt
|> enclose_env ctxt "isarbox"
end);
*)
fun enclose_env ctxt block_env body =
if Config.get ctxt Document_Antiquotation.thy_output_display
then Latex.environment block_env body
else body;
fun boxed_text_antiquotation name (* redefined in these more abstract terms *) =
gen_text_antiquotation name report_text
(fn ctxt => string_2_text_antiquotation ctxt
#> enclose_env ctxt "isarbox")
fun boxed_theory_text_antiquotation name (* redefined in these more abstract terms *) =
gen_text_antiquotation name report_theory_text
(fn ctxt => string_2_theory_text_antiquotation ctxt
#> enclose_env ctxt "isarbox")
(* #> enclose_env ctxt "isarbox" *)
val _ = Theory.setup
(std_text_antiquotation \<^binding>\<open>my_text\<close> #>
boxed_text_antiquotation \<^binding>\<open>boxed_text\<close> #>
std_text_antiquotation \<^binding>\<open>my_cartouche\<close> #>
boxed_text_antiquotation \<^binding>\<open>boxed_cartouche\<close> #>
std_theory_text_antiquotation \<^binding>\<open>my_theory_text\<close>#>
boxed_theory_text_antiquotation \<^binding>\<open>boxed_theory_text\<close>); (* is overriding possible ?*)
\<close>
(*<*)
text-latex\<open>
@{boxed_cartouche [display] \<open>definition dfg = \<lambda>x. x\<close>}
@{boxed_theory_text [display] \<open>doc_class dfg = \<lambda>x... \<Gamma>\<close>} \<close>
(*>*)
section\<open>Experimental Section for Multiple Figure Content\<close>
ML\<open>
val thy_output_display = Attrib.setup_option_bool ("thy_output_display", \<^here>);
val caption_param = Config.declare_string ("caption", \<^here>) (K "");
val width_param = Config.declare_int ("width", \<^here>) (K 80); \<comment> \<open>char per line\<close>
val scale_param = Config.declare_int ("scale", \<^here>) (K 100); \<comment> \<open>in percent\<close>
Config.put caption_param;
Config.put_global;
Config.get ;
(*
Latex.string (enclose "[" "]" (String.concat [ label_and_type, ", args={", (commas str_args), "}"]))
*)
(*
\begin{figure}[h]
\centering
\includegraphics[scale=0.5]{graph_a}
\caption{An example graph}
\label{fig:x cubed graph}
\end{figure}
\begin{figure}
\centering
\begin{subfigure}[b]{0.3\textwidth}
\centering
\includegraphics[width=\textwidth]{graph1}
\caption{$y=x$}
\label{fig:y equals x} (* PROBLEM *)
\end{subfigure}
\hfill
\begin{subfigure}[b]{0.3\textwidth}
\centering
\includegraphics[width=\textwidth]{graph2}
\caption{$y=3sinx$}
\label{fig:three sin x} (* PROBLEM *)
\end{subfigure}
\hfill
\begin{subfigure}[b]{0.3\textwidth}
\centering
\includegraphics[width=\textwidth]{graph3}
\caption{$y=5/x$}
\label{fig:five over x} (* PROBLEM *)
\end{subfigure}
\caption{Three simple graphs}
\label{fig:three graphs}
\end{figure}
\begin{wrapfigure}{l}{0.5\textwidth}
\centering
\includegraphics[width=1.5cm]{logo.png}
\caption{$y=5/x$}
\end{wrapfigure}
*)
datatype figure_type = single | subfigure | float_embedded
(* to check if this can be done more properly: user-state or attributes ??? *)
val figure_mode = Unsynchronized.ref(float_embedded)
val figure_label = Unsynchronized.ref(NONE:string option)
val figure_proportions = Unsynchronized.ref([]:int list)
(* invariant : !figure_mode = subfigure_embedded ==> length(!figure_proportions) > 1 *)
fun figure_antiq (check: Proof.context -> Path.T option -> Input.source -> Path.T) =
Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) =>
(check ctxt NONE source;
let val cap = Config.get ctxt caption_param
val cap_txt = if cap = "" then "" else (Library.enclose "\n\\caption{" "}\n" cap)
\<comment> \<open>this is naive. one should add an evaluation of doc antiquotations here\<close>
val wdth= Config.get ctxt width_param
val wdth_ltx = (if wdth = 100 then ""
else if 10<=wdth andalso wdth<=99
then "width=0."^(Int.toString wdth)
else if 1<=wdth then "width=0.0"^(Int.toString wdth)
else error "width out of range (must be between 1 and 100"
)^"\\textwidth"
val scl = Config.get ctxt scale_param
val scl_ltx = if scl = 100 then ""
else if 10<=scl andalso scl<=99 then "scale=0."^(Int.toString scl)
else if 1<=scl then "scale=0.0"^(Int.toString scl)
else error "scale out of range (must be between 1 and 100"
val fig_args = Library.enclose "[" "]" (commas [wdth_ltx,scl_ltx])
val _ = writeln cap
fun proportion () = "0."^ (Int.toString (100 div List.length(!figure_proportions)))
\<comment> \<open>naive: assumes equal proportions\<close>
fun core arg = "\n\\centering\n"
^"\\includegraphics"
^fig_args^(Library.enclose "{" "}" arg)
^cap_txt
\<comment> \<open>add internal labels here\<close>
fun pat arg = case !figure_mode of
single => core arg
|subfigure => "\n\\begin{subfigure}[b]{"^proportion ()^"\\textwidth}"
^ core arg
^"\n\\end{subfigure}\n"
|float_embedded => "\n\\begin{wrapfigure}{r}{"^wdth_ltx^"}"
^ core arg
^"\n\\end{wrapfigure}\n"
in (Latex.output_ascii_breakable "/" (Input.string_of source))
|> pat
|> Latex.string
end));
val _ = Theory.setup
(Document_Antiquotation.setup_option \<^binding>\<open>width\<close>
(Config.put width_param o Document_Antiquotation.integer) #>
Document_Antiquotation.setup_option \<^binding>\<open>scale\<close>
(Config.put scale_param o Document_Antiquotation.integer) #>
Document_Antiquotation.setup_option \<^binding>\<open>caption\<close>
(Config.put caption_param) #>
Document_Output.antiquotation_raw_embedded \<^binding>\<open>figure_content\<close>
(figure_antiq Resources.check_file) (K I)
);
\<close>
(*<*)
text-latex\<open>
@{figure_content [width=40, scale=35, caption="This is a test"] "ROOT"}
\<close>
(*>*)
ML\<open>
fun gen_enriched_document_command3 name {body} cid_transform attr_transform markdown
(((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t,
xstring_opt:(xstring * Position.T) option),
toks:Input.source list)
= gen_enriched_document_command2 name {body=body} cid_transform attr_transform markdown
(((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t,
xstring_opt:(xstring * Position.T) option),
toks) \<comment> \<open>Hack : drop second and thrd args.\<close>
val _ =
Outer_Syntax.command ("Figure*", @{here}) "multiple figure"
(ODL_Meta_Args_Parser.attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source
>> (Toplevel.theory o (gen_enriched_document_command2 "TTT" {body=true} I I {markdown = true} )));
\<close>
(*
Figure*[fff::figure,src="\<open>this is a side-by-side\<close>"]
\<open>@{figure_content [width=40, scale=35, caption="This is a test"] "ROOT"}\<close>
\<open> \<^doof> \<^LATEX> \<close>
\<open> \<^theory_text>\<open>definition df = ... \<close>
@{ML [display] \<open> let val x = 3 + 4 in true end\<close>}
@{cartouche [display] \<open> @{figure "cfgdfg"}\<close>}
\<close>
*)
(*<*)
Figure*[ffff::figure2, caption="\<open>this is another 2 side-by-side\<close>"]
\<open>@{figure_content [width=40, scale=35, caption="This is a left test"] "ROOT"}\<close>
\<open>@{figure_content [width=40, scale=35, caption="This is a right test"] "ROOT"}\<close>
(* proposed syntax for sub-figure labels : text\<open> @{figure "ffff(2)"}\<close> *)
Figure*[figxxx::figure2,caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
\<open>@{boxed_theory_text [display]
\<open>lemma inv_c2_preserved : "c2_inv \<sigma> \<Longrightarrow> c1_inv (\<sigma> \<langle>Hardware\<rangle>\<^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
Computer_Hardware_to_Hardware_morphism_def
Product_to_Component_morphism_def
by (auto simp: comp_def)
lemma Computer_Hardware_to_Hardware_total :
"Computer_Hardware_to_Hardware_morphism ` ({X. c2_inv X})
\<subseteq> ({X::Hardware. c1_inv X})"
using inv_c2_preserved by auto\<close>}\<close>
end
(*>*)

63
Isabelle_DOF-Unit-Tests/Ontology_Matching_Example.thy
View File

@ -1,11 +1,32 @@
chapter\<open>Ontologys Mathing\<close>
(*************************************************************************
* Copyright (C)
* 2019-2023 The University of Exeter
* 2018-2023 The 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
*************************************************************************)
chapter\<open>Ontologys Matching\<close>
theory Ontology_Matching_Example
imports "Isabelle_DOF.Isa_DOF"
"Isabelle_DOF-Unit-Tests_document"
imports TestKit
"Isabelle_DOF.Isa_DOF"
"Isabelle_DOF-Unit-Tests_document"
begin
section\<open>Test Purpose.\<close>
text\<open> This is merely an example that shows that the generated invariants
fit nicely together; i.e. allow for sensible consistency and invariant
preservation proofs related to ontological matchings. \<close>
section\<open>The Scenario.\<close>
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.
@ -14,19 +35,21 @@ text\<open>Using HOL, we can define a mapping between two ontologies.
type_synonym UTF8 = string
definition utf8_to_string
where "utf8_to_string x = x"
where "utf8_to_string xx = xx"
doc_class A =
first_name :: UTF8
last_name :: UTF8
age :: nat
married_to :: "string option"
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
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,
@ -39,6 +62,15 @@ definition A_to_B_morphism
, adult = (age X \<ge> 18)
, is_married = (married_to X \<noteq> None) \<rparr>"
text\<open>Sanity check: Invariants are non-contradictory, i.e. there is a witness.\<close>
lemma inv_a_satisfyable : " Ex (a_inv::A \<Rightarrow> bool)"
unfolding a_inv_def
apply(rule_tac x ="\<lparr>Ontology_Matching_Example.A.tag_attribute = xxx,
first_name = yyy, last_name = zzz, age = 17,
married_to = None\<rparr>" in exI)
by auto
text\<open>Now we check that the invariant is preserved through the morphism:\<close>
lemma inv_a_preserved :
@ -46,6 +78,15 @@ lemma inv_a_preserved :
unfolding a_inv_def b_inv_def A_to_B_morphism_def
by auto
text\<open>This also implies that B invariants are non-contradictory: \<close>
lemma inv_b_preserved : "\<exists>x. (b_inv::B \<Rightarrow> bool) x"
apply(rule_tac x ="A_to_B_morphism \<lparr>Ontology_Matching_Example.A.tag_attribute = xxx,
first_name = yyy, last_name = zzz, age = 17,
married_to = None\<rparr>" in exI)
by(rule inv_a_preserved,auto simp: a_inv_def)
lemma A_morphism_B_total :
"A_to_B_morphism ` ({X::A. a_inv X}) \<subseteq> ({X::B. b_inv X})"
using inv_a_preserved

136
Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy
View File

@ -15,133 +15,29 @@ theory
OutOfOrderPresntn
imports
"Isabelle_DOF-Unit-Tests_document"
"TestKit"
"Isabelle_DOF-Ontologies.Conceptual"
keywords "text-" "textN" :: document_body
and "Figure*" :: document_body
keywords "Figure*" :: document_body
begin
section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
text\<open>Current status:\<close>
print_doc_classes
print_doc_items
(* this corresponds to low-level accesses : *)
ML\<open>
val docitem_tab = DOF_core.get_instances \<^context>;
val isa_transformer_tab = DOF_core.get_isa_transformers \<^context>;
val docclass_tab = DOF_core.get_onto_classes \<^context>;
Name_Space.dest_table docitem_tab;
Name_Space.dest_table isa_transformer_tab;
Name_Space.dest_table docclass_tab;
app;
\<close>
ML\<open>
val _ = Document_Output.document_output
fun gen_enriched_document_command2 name {body} cid_transform attr_transform markdown
(((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t,
xstring_opt:(xstring * Position.T) option),
toks_list:Input.source list)
: theory -> theory =
let fun toplvl thy = Toplevel.make_state (SOME thy)
(* as side-effect, generates markup *)
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)),
(pos, Markup.plain_text)];
fun markup xml = let val m = if body then Markup.latex_body
else Markup.latex_heading
in [XML.Elem (m (Latex.output_name name),
xml)] end;
val text = Document_Output.output_document
(Proof_Context.init_global thy)
markdown toks
(* type file = {path: Path.T, pos: Position.T, content: string} *)
val strg = XML.string_of (hd (Latex.output text))
val file = {path = Path.make [oid ^ "_snippet.tex"],
pos = @{here},
content = Bytes.string strg}
val _ = Generated_Files.write_file (Path.make ["latex_test"])
file
val _ = writeln (strg)
in () end \<comment> \<open>important observation: thy is not modified.
This implies that several text block can be
processed in parallel in a future, as long
as they are associated to one meta arg.\<close>
(* ... generating the level-attribute syntax *)
in
( Value_Command.Docitem_Parser.create_and_check_docitem
{is_monitor = false} {is_inline = false} {define = true}
oid pos (cid_transform cid_pos) (attr_transform doc_attrs)
#> (fn thy => (app (check_n_tex_text thy) toks_list; thy)))
end;
val _ =
Outer_Syntax.command ("text-", @{here}) "formal comment macro"
(ODL_Meta_Args_Parser.attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source
>> (Toplevel.theory o (gen_enriched_document_command2 "TTT" {body=true} I I {markdown = true} )));
(* copied from Pure_syn for experiments *)
fun output_document2 state markdown txt =
let
val ctxt = Toplevel.presentation_context state;
val pos = Input.pos_of txt;
val _ =
Context_Position.reports ctxt
[(pos, Markup.language_document (Input.is_delimited txt)),
(pos, Markup.plain_text)];
val txt' = Document_Output.output_document ctxt markdown txt
val strg = XML.string_of (hd (Latex.output txt'))
val _ = writeln (strg)
in Document_Output.output_document ctxt markdown txt end;
fun document_command2 markdown (loc, txt) =
Toplevel.keep (fn state =>
(case loc of
NONE => ignore (output_document2 state markdown txt)
| SOME (_, pos) =>
error ("Illegal target specification -- not a theory context"
^ Position.here pos)))
o
Toplevel.present_local_theory loc
(fn state => (output_document2 state markdown txt));
val _ =
Outer_Syntax.command ("textN", \<^here>) "formal comment (primary style)"
(Parse.opt_target -- Parse.document_source >> document_command2 {markdown = true});
\<close>
ML\<open>open Bytes\<close>
(*
text\<open>And here a tex - text macro.\<close>
text\<open>Pythons ReStructuredText (RST).
@{url \<open>https://de.wikipedia.org/wiki/ReStructuredText\<close>}. Tool: Sphinx.
\<close>
text*[aaaa::B]\<open>dfg @{thm [display] refl}\<close>
(*<*)
text-[dfgdfg::B]
\<open> Lorem ipsum ... @{thm [display] refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
textN\<open> Lorem ipsum ... @{thm [display] refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
text-latex\<open> Lorem ipsum ... @{thm [display] refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
text-[asd::B]
\<open>... and here is its application macro expansion:
@ -153,7 +49,7 @@ text-[asd::B]
\<close>}
\<close>
textN\<open>... and here is its application macro expansion:
text-latex\<open>... and here is its application macro expansion:
@{B [display] "dfgdfg"}
\textbf{TEST}
@{cartouche [display]
@ -161,7 +57,7 @@ textN\<open>... and here is its application macro expansion:
\<open> Lorem ipsum ... @{thm refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
\<close>}\<close>
textN\<open> \<^theory_text>\<open>definition df = ...
text-latex\<open> \<^theory_text>\<open>definition df = ...
\<close>
@{ML [display] \<open> let val x = 3 + 4 in true end
\<close>}
@ -174,8 +70,8 @@ textN\<open> \<^theory_text>\<open>definition df = ...
@{theory_text [display] \<open>definition df = ... \<lambda>x.
\<close>}
@{cartouche [display] \<open> @{figure "cfgdfg"}\<close>} \<close>
*)
(*<*)
text\<open>Final Status:\<close>
print_doc_items
print_doc_classes
@ -196,7 +92,7 @@ val _ =
)
\<close>
textN\<open> \<^doof> \<^LATEX> \<close>
text-latex\<open> \<^doof> \<^LATEX> \<close>
(* the same effect is achieved with : *)
setup \<open>DOF_lib.define_shortcut (Binding.make("bla",\<^here>)) "\\blabla"\<close>
@ -204,10 +100,10 @@ setup \<open>DOF_lib.define_shortcut (Binding.make("bla",\<^here>)) "\\blabla"\<
target document, for example, in the tex prelude. Note that the "Binding.make" can be avoided
using the alternative \<^binding> notation (see above).*)
setup\<open>DOF_lib.define_macro (Binding.make("blong",\<^here>)) "\\blong{" "}" (K(K()))\<close>
textN\<open> \<^blong>\<open>asd\<close> outer \<^blong>\<open>syntax| ! see {syntax, outer}\<close> \<close>
text-latex\<open> \<^blong>\<open>asd\<close> outer \<^blong>\<open>syntax| ! see {syntax, outer}\<close> \<close>
(*>*)
ML\<open>
@ -330,14 +226,16 @@ val _ = Theory.setup
\<close>
textN\<open>
(*<*)
text-latex\<open>
@{boxed_cartouche [display] \<open>definition dfg = \<lambda>x. x\<close>}
@{boxed_theory_text [display] \<open>doc_class dfg = \<lambda>x... \<Gamma>\<close>} \<close>
(*>*)
section\<open>Section Experiments of picture-content\<close>
(*<*)
ML\<open>
@ -477,7 +375,7 @@ val _ = Theory.setup
);
\<close>
textN\<open>
text-latex\<open>
@{figure_content [width=40, scale=35, caption="This is a test"] "ROOT"}
\<close>

7
Isabelle_DOF-Unit-Tests/ROOT
View File

@ -1,12 +1,15 @@
session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" +
options [document = pdf, document_output = "output", document_build = dof]
theories
"AssnsLemmaThmEtc"
"TestKit"
"Latex_Tests"
"Concept_OntoReferencing"
"Concept_Example_Low_Level_Invariant"
"Concept_Example"
"Concept_MonitorTest1"
"TermAntiquotations"
"Attributes"
"Evaluation"
"AssnsLemmaThmEtc"
"High_Level_Syntax_Invariants"
"Ontology_Matching_Example"
"Cenelec_Test"

1
Isabelle_DOF-Unit-Tests/TermAntiquotations.thy
View File

@ -95,7 +95,6 @@ text\<open>And here is the results of some ML-term antiquotations:\<close>
ML\<open> @{docitem_attribute b::xcv4} \<close>
ML\<open> @{docitem xcv4} \<close>
ML\<open> @{docitem_name xcv4} \<close>
ML\<open> @{trace_attribute aaa} \<close>
text\<open>Now we might need to reference a class instance in a term command and we would like
Isabelle to check that this instance is indeed an instance of this class.

164
Isabelle_DOF-Unit-Tests/TestKit.thy Normal file
View File

@ -0,0 +1,164 @@
(*************************************************************************
* Copyright (C)
* 2019-2023 The University of Exeter
* 2018-2023 The 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
TestKit
imports
"Isabelle_DOF-Unit-Tests_document"
"Isabelle_DOF-Ontologies.Conceptual"
keywords "text-" "text-latex" :: document_body
and "text-assert-error" :: document_body
and "update_instance-assert-error" :: document_body
and "declare_reference-assert-error" :: document_body
begin
section\<open>Testing Commands (exec-catch-verify - versions of std commands)\<close>
ML\<open>
fun gen_enriched_document_command2 name {body} cid_transform attr_transform markdown
(((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t,
xstring_opt:(xstring * Position.T) option),
toks_list:Input.source list)
: theory -> theory =
let
(* as side-effect, generates markup *)
fun check_n_tex_text thy toks = let val ctxt = Toplevel.presentation_context (Toplevel.make_state (SOME thy))
val pos = Input.pos_of toks;
val _ = Context_Position.reports ctxt
[(pos, Markup.language_document (Input.is_delimited toks)),
(pos, Markup.plain_text)];
fun markup xml = let val m = if body then Markup.latex_body
else Markup.latex_heading
in [XML.Elem (m (Latex.output_name name),
xml)] end;
val text = Document_Output.output_document
(Proof_Context.init_global thy)
markdown toks
(* type file = {path: Path.T, pos: Position.T, content: string} *)
val strg = XML.string_of (hd (Latex.output text))
val file = {path = Path.make [oid ^ "_snippet.tex"],
pos = @{here},
content = Bytes.string strg}
val _ = Generated_Files.write_file (Path.make ["latex_test"])
file
val _ = writeln (strg)
in () end \<comment> \<open>important observation: thy is not modified.
This implies that several text block can be
processed in parallel in a future, as long
as they are associated to one meta arg.\<close>
(* ... generating the level-attribute syntax *)
in
( Value_Command.Docitem_Parser.create_and_check_docitem
{is_monitor = false} {is_inline = false} {define = true}
oid pos (cid_transform cid_pos) (attr_transform doc_attrs)
#> (fn thy => (app (check_n_tex_text thy) toks_list; thy)))
end;
val _ =
Outer_Syntax.command ("text-", @{here}) "formal comment macro"
(ODL_Meta_Args_Parser.attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source
>> (Toplevel.theory o (gen_enriched_document_command2 "TTT" {body=true} I I {markdown = true} )));
(* copied from Pure_syn for experiments *)
fun output_document2 state markdown txt =
let
val ctxt = Toplevel.presentation_context state;
val pos = Input.pos_of txt;
val _ =
Context_Position.reports ctxt
[(pos, Markup.language_document (Input.is_delimited txt)),
(pos, Markup.plain_text)];
val txt' = Document_Output.output_document ctxt markdown txt
val strg = XML.string_of (hd (Latex.output txt'))
val _ = writeln (strg)
in Document_Output.output_document ctxt markdown txt end;
fun document_command2 markdown (loc, txt) =
Toplevel.keep (fn state =>
(case loc of
NONE => ignore (output_document2 state markdown txt)
| SOME (_, pos) =>(ISA_core.err
"Illegal target specification -- not a theory context"
pos)))
o
Toplevel.present_local_theory loc (fn state => (output_document2 state markdown txt));
fun gen_enriched_document_command3 assert name body trans at md (margs, src_list) thy
= (gen_enriched_document_command2 name body trans at md (margs, src_list) thy)
handle ERROR msg => (if assert src_list msg then (writeln ("Correct error:"^msg^":reported.");thy)
else error"Wrong error reported")
fun error_match src msg = (writeln((Input.string_of src)); String.isPrefix (Input.string_of src) msg)
fun error_match2 [_, src] msg = error_match src msg
| error_match2 _ _ = error "Wrong text-assertion-error. Argument format <arg><match> required."
val _ =
Outer_Syntax.command ("text-assert-error", @{here}) "formal comment macro"
(ODL_Meta_Args_Parser.attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source
>> (Toplevel.theory o (gen_enriched_document_command3 error_match2 "TTT" {body=true}
I I {markdown = true})
));
fun update_instance_command (args,src) thy =
(Monitor_Command_Parser.update_instance_command args thy
handle ERROR msg => (if error_match src msg
then (writeln ("Correct error:"^msg^":reported.");thy)
else error"Wrong error reported"))
val _ =
Outer_Syntax.command \<^command_keyword>\<open>update_instance-assert-error\<close>
"update meta-attributes of an instance of a document class"
(ODL_Meta_Args_Parser.attributes_upd -- Parse.document_source
>> (Toplevel.theory o update_instance_command));
val _ =
let fun create_and_check_docitem ((((oid, pos),cid_pos),doc_attrs),src) thy=
(Value_Command.Docitem_Parser.create_and_check_docitem
{is_monitor = false} {is_inline=true}
{define = false} oid pos (cid_pos) (doc_attrs) thy)
handle ERROR msg => (if error_match src msg
then (writeln ("Correct error:"^msg^":reported.");thy)
else error"Wrong error reported")
in Outer_Syntax.command \<^command_keyword>\<open>declare_reference-assert-error\<close>
"declare document reference"
(ODL_Meta_Args_Parser.attributes -- Parse.document_source
>> (Toplevel.theory o create_and_check_docitem))
end;
val _ =
Outer_Syntax.command ("text-latex", \<^here>) "formal comment (primary style)"
(Parse.opt_target -- Parse.document_source >> document_command2 {markdown = true});
\<close>
(* auto-tests *)
text-latex\<open>dfg\<close>
text-assert-error[aaaa::A]\<open> @{A \<open>sdf\<close>}\<close>\<open>reference ontologically inconsistent\<close>
end
(*>*)

6
Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy
View File

@ -495,8 +495,10 @@ let val cidS = ["scholarly_paper.introduction","scholarly_paper.technical",
"scholarly_paper.example", "scholarly_paper.conclusion"];
fun body moni_oid _ ctxt = (Scholarly_paper_trace_invariant.check ctxt cidS moni_oid NONE; true)
val ctxt = Proof_Context.init_global thy
val binding = DOF_core.binding_from_onto_class_pos "article" thy
in DOF_core.add_ml_invariant binding body thy end)
val cid = "article"
val binding = DOF_core.binding_from_onto_class_pos cid thy
val cid_long = DOF_core.get_onto_class_name_global cid thy
in DOF_core.add_ml_invariant binding (DOF_core.make_ml_invariant (body, cid_long)) thy end)
\<close>
section\<open>Miscelleous\<close>

400
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -39,6 +39,9 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
"doc_class" "onto_class" (* a syntactic alternative *)
"ML*"
"define_shortcut*" "define_macro*" :: thy_decl
and "definition*" :: thy_defn
and "theorem*" "lemma*" "corollary*" "proposition*" :: thy_goal_stmt
and "schematic_goal*" :: thy_goal_stmt
and "text*" "text-macro*" :: document_body
and "term*" "value*" "assert*" :: document_body
@ -139,6 +142,9 @@ fun map_snd f (x,y) = (x,f y)
fun map_eq_fst_triple f (x,_,_) (y,_,_) = equal (f x) (f y)
fun lst_and_fun _ [] = true
| lst_and_fun x (f::fs) = (f x) andalso (lst_and_fun x fs)
\<close>
section\<open> A HomeGrown Document Type Management (the ''Model'') \<close>
@ -348,7 +354,12 @@ struct
| NONE => raise TYPE ("Unknown isa_transformer: " ^ quote i, [], []));
type ml_invariant = string -> {is_monitor:bool} -> Context.generic -> bool
datatype ml_invariant = ML_Invariant of
{check : string -> {is_monitor:bool} -> Context.generic -> bool
, class : string}
fun make_ml_invariant (check, class) =
ML_Invariant {check = check, class = class}
structure ML_Invariants = Theory_Data
(
@ -483,8 +494,8 @@ struct
fun make_monitor_info (accepted_cids, rejected_cids, automatas) =
Monitor_Info {accepted_cids = accepted_cids,
rejected_cids = rejected_cids,
automatas = automatas}
rejected_cids = rejected_cids,
automatas = automatas}
structure Monitor_Info = Theory_Data
(
@ -1602,11 +1613,20 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy =
val _ = if null enabled_monitors then () else writeln "registrating in monitors ..."
val _ = app (fn (n, _) => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors;
(* check that any transition is possible : *)
fun inst_class_inv x = let val invs = DOF_core.get_ml_invariants ctxt
val check_option = Name_Space.lookup invs (cid_of x)
in case check_option of
NONE => (K true)
| SOME check => (check x {is_monitor=false}) end
fun inst_class_inv x ctxt =
let val cid_long = let val DOF_core.Instance cid =
DOF_core.get_instance_global x (Context.theory_of ctxt)
in cid |> #cid end
val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy)
|> Name_Space.dest_table
val check_list = invs |> filter (fn (_, inv) =>
let val DOF_core.ML_Invariant {class, ...} = inv
in class |> equal cid_long end)
|> map (fn (_, inv) =>
let val DOF_core.ML_Invariant {check, ...} = inv
in check end)
val check_list' = check_list |> map (fn check => check x {is_monitor=false})
in (lst_and_fun ctxt check_list') end
fun class_inv_checks ctxt = map (fn (x, _) => inst_class_inv x ctxt) enabled_monitors
val delta_autoS = map is_enabled_for_cid enabled_monitors;
fun update_info (n, aS, monitor_info) =
@ -1734,12 +1754,18 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi
thy cid_long assns' defaults
in (input_term, value_term') end
else (\<^term>\<open>()\<close>, value_term') end
val check_inv = Context.Theory
#> (let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy)
val check_option = Name_Space.lookup invs cid_long
in case check_option of
NONE => (K true)
| SOME check => (check oid is_monitor) end)
fun check_inv thy =
thy |> Context.Theory
|> (fn ctxt => let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy)
|> Name_Space.dest_table
val check_list = invs |> filter (fn (_, inv) =>
let val DOF_core.ML_Invariant {class, ...} = inv
in class |> equal cid_long end)
|> map (fn (_, inv) =>
let val DOF_core.ML_Invariant {check, ...} = inv
in check end)
val check_list' = check_list |> map (fn check => check oid is_monitor)
in (lst_and_fun ctxt check_list') end)
in thy |> DOF_core.define_object_global
{define = define} ((oid, pos), DOF_core.make_instance
(false, fst value_terms,
@ -1749,13 +1775,18 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi
|> register_oid_cid_in_open_monitors oid pos cid_pos'
|> (fn thy => if #is_monitor(is_monitor)
then ((Context.Theory
#> (let val invs = DOF_core.get_opening_ml_invariants (Proof_Context.init_global thy)
val check_option = Name_Space.lookup invs cid_long
in case check_option of
NONE => (K true)
| SOME check => (check oid is_monitor) end)) thy; thy)
#> (fn ctxt => let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy)
|> Name_Space.dest_table
val check_list = invs |> filter (fn (_, inv) =>
let val DOF_core.ML_Invariant {class, ...} = inv
in class |> equal cid_long end)
|> map (fn (_, inv) =>
let val DOF_core.ML_Invariant {check, ...} = inv
in check end)
val check_list' = check_list |> map (fn check => check oid is_monitor)
in (lst_and_fun ctxt check_list') end)) thy; thy)
else thy)
|> (fn thy => (check_inv thy; thy))
|> tap check_inv
(* Bypass checking of high-level invariants when the class default_cid = "text",
the top (default) document class.
We want the class default_cid to stay abstract
@ -1947,12 +1978,17 @@ fun update_instance_command (((oid, pos), cid_pos),
thy cid_long assns')
#> Value_Command.value (Proof_Context.init_global thy)
fun check_inv thy =
((Context.Theory
#> (let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy)
val check_option = Name_Space.lookup invs cid_long
in case check_option of
NONE => (K true)
| SOME check => (check oid {is_monitor=false}) end) ) thy ; thy)
((Context.Theory
#> (fn ctxt => let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy)
|> Name_Space.dest_table
val check_list = invs |> filter (fn (_, inv) =>
let val DOF_core.ML_Invariant {class, ...} = inv
in class |> equal cid_long end)
|> map (fn (_, inv) =>
let val DOF_core.ML_Invariant {check, ...} = inv
in check end)
val check_list' = check_list |> map (fn check => check oid {is_monitor=false})
in (lst_and_fun ctxt check_list') end) ) thy ; thy)
in
thy |> (if Config.get_global thy DOF_core.object_value_debug
then DOF_core.update_value_input_term_global oid
@ -2017,22 +2053,32 @@ fun close_monitor_command (args as (((oid, pos), cid_pos),
|> Name_Space.markup (Name_Space.space_of_table instances)
val _ = Context_Position.report ctxt pos markup;
val check_inv =
Context.Theory
#> (let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy)
val check_option = Name_Space.lookup invs cid_long
in case check_option of
NONE => (K true)
| SOME check => (check oid {is_monitor=true}) end)
Context.Theory
#> (fn ctxt => let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy)
|> Name_Space.dest_table
val check_list = invs |> filter (fn (_, inv) =>
let val DOF_core.ML_Invariant {class, ...} = inv
in class |> equal cid_long end)
|> map (fn (_, inv) =>
let val DOF_core.ML_Invariant {check, ...} = inv
in check end)
val check_list' = check_list |> map (fn check => check oid {is_monitor=true})
in (lst_and_fun ctxt check_list') end)
val check_closing_inv =
Context.Theory
#> (let val invs = DOF_core.get_closing_ml_invariants (Proof_Context.init_global thy)
val check_option = Name_Space.lookup invs cid_long
in case check_option of
NONE => (K true)
| SOME check => (check oid {is_monitor=true}) end)
Context.Theory
#> (fn ctxt => let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy)
|> Name_Space.dest_table
val check_list = invs |> filter (fn (_, inv) =>
let val DOF_core.ML_Invariant {class, ...} = inv
in class |> equal cid_long end)
|> map (fn (_, inv) =>
let val DOF_core.ML_Invariant {check, ...} = inv
in check end)
val check_list' = check_list |> map (fn check => check oid {is_monitor=true})
in (lst_and_fun ctxt check_list') end)
in thy |> (fn thy => (check_closing_inv thy; thy))
|> update_instance_command args
|> (fn thy => (check_inv thy; thy))
|> tap check_inv
|> (fn thy => if Config.get_global thy DOF_core.invariants_checking
then Value_Command.Docitem_Parser.check_invariants thy (oid, pos)
else thy)
@ -2179,13 +2225,18 @@ val _ =
{markdown = true, body = true}
(gen_enriched_document_cmd {inline=false} (* declare as macro *) I I);
val _ =
Outer_Syntax.command \<^command_keyword>\<open>declare_reference*\<close>
val _ =
let fun create_and_check_docitem (((oid, pos),cid_pos),doc_attrs)
= (Value_Command.Docitem_Parser.create_and_check_docitem
{is_monitor = false} {is_inline=true}
{define = false} oid pos (cid_pos) (doc_attrs))
in Outer_Syntax.command \<^command_keyword>\<open>declare_reference*\<close>
"declare document reference"
(ODL_Meta_Args_Parser.attributes >> (fn (((oid, pos),cid_pos),doc_attrs) =>
(Toplevel.theory (Value_Command.Docitem_Parser.create_and_check_docitem
{is_monitor = false} {is_inline=true}
{define = false} oid pos (cid_pos) (doc_attrs)))));
(ODL_Meta_Args_Parser.attributes
>> (Toplevel.theory o create_and_check_docitem))
end;
end (* structure Monitor_Command_Parser *)
\<close>
@ -2313,6 +2364,265 @@ val _ =
end
\<close>
\<comment> \<open>c.f. \<^file>\<open>~~/src/Pure/Isar/specification.ML\<close> and \<^file>\<open>~~/src/Pure/Pure.thy\<close>\<close>
ML\<open>
structure Definition_Star_Command =
struct
fun get_positions ctxt x =
let
fun get Cs (Const ("_type_constraint_", C) $ t) = get (C :: Cs) t
| get Cs (Free (y, T)) =
if x = y then
map_filter Term_Position.decode_positionT
(T :: map (Type.constraint_type ctxt) Cs)
else []
| get _ (t $ u) = get [] t @ get [] u
| get _ (Abs (_, _, t)) = get [] t
| get _ _ = [];
in get [] end;
fun prep_decls prep_var raw_vars ctxt =
let
val (vars, ctxt') = fold_map prep_var raw_vars ctxt;
val (xs, ctxt'') = ctxt'
|> Context_Position.set_visible false
|> Proof_Context.add_fixes vars
||> Context_Position.restore_visible ctxt';
val _ =
Context_Position.reports ctxt''
(map (Binding.pos_of o #1) vars ~~
map (Variable.markup_entity_def ctxt'' ##> Properties.remove Markup.kindN) xs);
in ((vars, xs), ctxt'') end;
fun dummy_frees ctxt xs tss =
let
val names =
Variable.names_of ((fold o fold) Variable.declare_term tss ctxt)
|> fold Name.declare xs;
val (tss', _) = (fold_map o fold_map) Term.free_dummy_patterns tss names;
in tss' end;
fun prep_spec_open prep_var parse_prop raw_vars raw_params raw_prems raw_concl ctxt =
let
val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt;
val (ys, params_ctxt) = vars_ctxt |> fold_map prep_var raw_params |-> Proof_Context.add_fixes;
val props =
map (parse_prop params_ctxt) (raw_concl :: raw_prems)
|> singleton (dummy_frees params_ctxt (xs @ ys));
val concl :: prems = Syntax.check_props params_ctxt props;
val spec = Logic.list_implies (prems, concl);
val spec' = DOF_core.transduce_term_global {mk_elaboration=true}
(spec , Position.none)
(Proof_Context.theory_of ctxt)
val spec_ctxt = Variable.declare_term spec' params_ctxt;
fun get_pos x = maps (get_positions spec_ctxt x) props;
in ((vars, xs, get_pos, spec'), spec_ctxt) end;
val read_spec_open = prep_spec_open Proof_Context.read_var Syntax.parse_prop;
(* definition *)
fun gen_def prep_spec prep_att raw_var raw_params raw_prems ((a, raw_atts), raw_spec) int lthy =
let
val atts = map (prep_att lthy) raw_atts;
val ((vars, xs, get_pos, spec), _) = lthy
|> prep_spec (the_list raw_var) raw_params raw_prems raw_spec;
val (((x, T), rhs), prove) = Local_Defs.derived_def lthy get_pos {conditional = true} spec;
val _ = Name.reject_internal (x, []);
val (b, mx) =
(case (vars, xs) of
([], []) => (Binding.make (x, (case get_pos x of [] => Position.none | p :: _ => p)), NoSyn)
| ([(b, _, mx)], [y]) =>
if x = y then (b, mx)
else
error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
Position.here (Binding.pos_of b)));
val name = Thm.def_binding_optional b a;
val ((lhs, (_, raw_th)), lthy2) = lthy
|> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
val th = prove lthy2 raw_th;
val lthy3 = lthy2 |> Spec_Rules.add name Spec_Rules.equational [lhs] [th];
val ([(def_name, [th'])], lthy4) = lthy3
|> Local_Theory.notes [((name, atts), [([th], [])])];
val lthy5 = lthy4
|> Code.declare_default_eqns [(th', true)];
val lhs' = Morphism.term (Local_Theory.target_morphism lthy5) lhs;
val _ =
Proof_Display.print_consts int (Position.thread_data ()) lthy5
(Frees.defined (Frees.build (Frees.add_frees lhs'))) [(x, T)];
in ((lhs, (def_name, th')), lthy5) end;
val definition_cmd = gen_def read_spec_open Attrib.check_src;
fun definition_cmd' meta_args_opt decl params prems spec bool ctxt =
Local_Theory.background_theory (Value_Command.meta_args_exec meta_args_opt) ctxt
|> definition_cmd decl params prems spec bool
val _ =
Outer_Syntax.local_theory' \<^command_keyword>\<open>definition*\<close> "constant definition"
(ODL_Meta_Args_Parser.opt_attributes --
(Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) --
Parse_Spec.if_assumes -- Parse.for_fixes)
>> (fn (meta_args_opt, (((decl, spec), prems), params)) =>
#2 oo definition_cmd' meta_args_opt decl params prems spec));
end
\<close>
\<comment> \<open>c.f. \<^file>\<open>~~/src/Pure/Isar/specification.ML\<close> and \<^file>\<open>~~/src/Pure/Pure.thy\<close>\<close>
ML\<open>
(* theorem*, lemma*, etc. commands *)
local
fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt =
let
val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt;
val prems = Assumption.local_prems_of elems_ctxt ctxt;
val stmt_ctxt = fold (fold (Proof_Context.augment o fst) o snd) stmt elems_ctxt;
in
(case raw_stmt of
Element.Shows _ =>
let val stmt' = Attrib.map_specs (map prep_att) stmt
val stmt'' = map (fn (b, ts) =>
(b, map (fn (t', t's) =>
(DOF_core.transduce_term_global {mk_elaboration=true}
(t' , Position.none)
(Proof_Context.theory_of ctxt),
map (fn t'' =>
DOF_core.transduce_term_global {mk_elaboration=true}
(t'' , Position.none)
(Proof_Context.theory_of ctxt))
t's)) ts)) stmt'
in (([], prems, stmt'', NONE), stmt_ctxt) end
| Element.Obtains raw_obtains =>
let
val asms_ctxt = stmt_ctxt
|> fold (fn ((name, _), asm) =>
snd o Proof_Context.add_assms Assumption.assume_export
[((name, [Context_Rules.intro_query NONE]), asm)]) stmt;
val that = Assumption.local_prems_of asms_ctxt stmt_ctxt;
val ([(_, that')], that_ctxt) = asms_ctxt
|> Proof_Context.set_stmt true
|> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(that, [])])]
||> Proof_Context.restore_stmt asms_ctxt;
val stmt' = [(Binding.empty_atts, [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])];
val stmt'' = map (fn (b, ts) =>
(b, map (fn (t', t's) =>
(DOF_core.transduce_term_global {mk_elaboration=true}
(t' , Position.none)
(Proof_Context.theory_of ctxt),
map (fn t'' =>
DOF_core.transduce_term_global {mk_elaboration=true}
(t'' , Position.none)
(Proof_Context.theory_of ctxt))
t's)) ts)) stmt'
in ((Obtain.obtains_attribs raw_obtains, prems, stmt'', SOME that'), that_ctxt) end)
end;
fun gen_theorem schematic bundle_includes prep_att prep_stmt
long kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
let
val _ = Local_Theory.assert lthy;
val elems = raw_elems |> map (Element.map_ctxt_attrib (prep_att lthy));
val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy
|> bundle_includes raw_includes
|> prep_statement (prep_att lthy) prep_stmt elems raw_concl;
val atts = more_atts @ map (prep_att lthy) raw_atts;
val pos = Position.thread_data ();
fun after_qed' results goal_ctxt' =
let
val results' =
burrow (map (Goal.norm_result lthy) o Proof_Context.export goal_ctxt' lthy) results;
val (res, lthy') =
if forall (Binding.is_empty_atts o fst) stmt then (map (pair "") results', lthy)
else
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 int pos 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 int pos lthy' ((kind, res_name), res);
in lthy'' end;
in after_qed results' lthy'' end;
val prems_name = if long then Auto_Bind.assmsN else Auto_Bind.thatN;
in
goal_ctxt
|> not (null prems) ?
(Proof_Context.note_thmss "" [((Binding.name prems_name, []), [(prems, [])])] #> snd)
|> Proof.theorem before_qed after_qed' (map snd stmt)
|> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
|> tap (fn state => not schematic andalso Proof.schematic_goal state andalso
error "Illegal schematic goal statement")
end;
in
val theorem_cmd =
gen_theorem false Bundle.includes_cmd Attrib.check_src Expression.read_statement;
fun theorem_cmd' meta_args_opt long kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
Local_Theory.background_theory (Value_Command.meta_args_exec meta_args_opt) lthy
|> theorem_cmd long kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int;
val schematic_theorem_cmd =
gen_theorem true Bundle.includes_cmd Attrib.check_src Expression.read_statement;
fun schematic_theorem_cmd' meta_args_opt long kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
Local_Theory.background_theory (Value_Command.meta_args_exec meta_args_opt) lthy
|> schematic_theorem_cmd long kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int;
end;
local
val long_keyword =
Parse_Spec.includes >> K "" ||
Parse_Spec.long_statement_keyword;
val long_statement =
ODL_Meta_Args_Parser.opt_attributes --
Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts --
Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement
>> (fn (((meta_args_opt, binding), includes), (elems, concl)) => (meta_args_opt, true, binding, includes, elems, concl));
val short_statement =
ODL_Meta_Args_Parser.opt_attributes --
Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
>> (fn (((meta_args_opt, shows), assumes), fixes) =>
(meta_args_opt, false, Binding.empty_atts, [], [Element.Fixes fixes, Element.Assumes assumes],
Element.Shows shows));
fun theorem spec schematic descr =
Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr)
((long_statement || short_statement) >> (fn (meta_args_opt, long, binding, includes, elems, concl) =>
((if schematic then schematic_theorem_cmd' else theorem_cmd')
meta_args_opt long Thm.theoremK NONE (K I) binding includes elems concl)));
val _ = theorem \<^command_keyword>\<open>theorem*\<close> false "theorem";
val _ = theorem \<^command_keyword>\<open>lemma*\<close> false "lemma";
val _ = theorem \<^command_keyword>\<open>corollary*\<close> false "corollary";
val _ = theorem \<^command_keyword>\<open>proposition*\<close> false "proposition";
val _ = theorem \<^command_keyword>\<open>schematic_goal*\<close> true "schematic goal";
in end
\<close>
ML\<open>
structure ODL_LTX_Converter =
struct

7
README_DEVELOPMENT.md
View File

@ -14,7 +14,6 @@ Isabelle/DOF has three major prerequisites:
[TeX Live 2022](https://www.tug.org/texlive/) with all available updates
applied.
<!--
### Note on Installing the AFP
@ -26,12 +25,15 @@ Both have their own advantages and disadvantages.
If you use the AFP with other Isabelle projects, you might want to install the
complete AFP. For this, please follow the instructions given at
<https://www.isa-afp.org/using.html>. As Isabelle session names need to be
<https://www.isa-afp.org/using.html>.
<!--
As Isabelle session names need to be
unique, you will need to disable the entries ``Isabelle_DOF`` and
``Isabelle_DOF-Example-Scholarly_Paper`` provided as part of the AFP. For this,
you will need to edit the file ``$AFP/thys/ROOTS`` (where ``$AFP`` refers to the
directory in which you installed the AFP) and delete the two entries
``Isabelle_DOF`` and ``Isabelle_DOF-Example-Scholarly_Paper``.
-->
For the development version of Isabelle, installing the complete AFP
by cloning the [afp-devel](https://foss.heptapod.net/isa-afp/afp-devel/)
@ -49,7 +51,6 @@ foo@bar:~$ isabelle env install-afp
Note that this option is not supported for the development version of
Isabelle.
-->
## Installation