Moved unit tests into tests directory and added test session.
This commit is contained in:
parent
189110dc0f
commit
a85bcacd5b
8
ROOT
8
ROOT
|
@ -10,3 +10,11 @@ session "Isabelle_DOF" = "Functional-Automata" +
|
|||
"ontologies/technical_report"
|
||||
"ontologies/mathex_onto"
|
||||
|
||||
session "Isabelle_DOF-tests" = "Isabelle_DOF" +
|
||||
options [document = false]
|
||||
theories
|
||||
"tests/AssnsLemmaThmEtc"
|
||||
"tests/Concept_ExampleInvariant"
|
||||
"tests/Concept_Example"
|
||||
"tests/InnerSyntaxAntiquotations"
|
||||
"tests/Attributes"
|
||||
|
|
|
@ -1,5 +1,8 @@
|
|||
theory AssnsLemmaThmEtc
|
||||
imports "../../ontologies/Conceptual" "../../ontologies/math_paper"
|
||||
theory
|
||||
AssnsLemmaThmEtc
|
||||
imports
|
||||
"../ontologies/Conceptual"
|
||||
"../ontologies/math_paper"
|
||||
begin
|
||||
|
||||
section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
|
||||
|
@ -17,14 +20,18 @@ text*[aa::F, property = "[@{term ''True''}]"]
|
|||
\<open>Our definition of the HOL-Logic has the following properties:\<close>
|
||||
assert*[aa::F] "True"
|
||||
|
||||
|
||||
(* does not work in batch mode ...
|
||||
(* sample for accessing a property filled with previous assert's of "aa" *)
|
||||
ML\<open> ISA_core.property_list_dest @{context} @{docitem_attribute property :: aa};\<close>
|
||||
|
||||
|
||||
|
||||
assert*[aa::F] " X \<and> Y \<longrightarrow> True" (*example with uni-code *)
|
||||
ML\<open> ISA_core.property_list_dest @{context} @{docitem_attribute property :: aa};
|
||||
app writeln (tl (rev it));\<close>
|
||||
|
||||
*)
|
||||
|
||||
assert*[aa::F] "\<forall>x::bool. X \<and> Y \<longrightarrow> True" (*problem with uni-code *)
|
||||
|
||||
ML\<open>
|
||||
|
@ -33,12 +40,12 @@ Syntax.read_term_global @{theory} "[@{termrepr ''True @<longrightarrow> True''}]
|
|||
@{term "[@{term '' True @<longrightarrow> True ''}]"}; (* with isa-check *)
|
||||
@{term "[@{termrepr '' True @<longrightarrow> True ''}]"}; (* without isa check *)
|
||||
\<close>
|
||||
|
||||
(*
|
||||
ML\<open>val [_,_,Const _ $ s,_] = (HOLogic.dest_list @{docitem_attribute property :: aa});
|
||||
val t = HOLogic.dest_string s;
|
||||
holstring_to_bstring @{context} t
|
||||
\<close>
|
||||
|
||||
*)
|
||||
lemma "All (\<lambda>x. X \<and> Y \<longrightarrow> True)" oops
|
||||
|
||||
|
|
@ -1,5 +1,7 @@
|
|||
theory Attributes
|
||||
imports "../../ontologies/Conceptual"
|
||||
theory
|
||||
Attributes
|
||||
imports
|
||||
"../ontologies/Conceptual"
|
||||
begin
|
||||
|
||||
section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
|
||||
|
@ -18,7 +20,10 @@ Symtab.dest docclass_tab;
|
|||
|
||||
|
||||
text\<open>A text item containing standard theorem antiquotations and complex meta-information.\<close>
|
||||
text*[dfgdfg::B, Conceptual.B.x ="''f''", y = "[''sdf'']"]\<open> Lorem ipsum ... @{thm refl} \<close>
|
||||
(* crashes in batch mode ...
|
||||
text*[dfgdfg::B, Conceptual.B.x ="''f''", y = "[''sdf'']"]\<open> Lorem ipsum ... @{thm refl} \<close>
|
||||
*)
|
||||
text*[dfgdfg::B]\<open> Lorem ipsum ... @{thm refl} \<close>
|
||||
|
||||
text\<open>document class declarations lead also HOL-type declarations (relevant for ontological links).\<close>
|
||||
typ "C"
|
||||
|
@ -106,7 +111,6 @@ text\<open> @{docitem_attribute omega::y} \<close>
|
|||
section\<open>Simulation of a Monitor\<close>
|
||||
|
||||
open_monitor*[figs1::figure_group,
|
||||
(* anchor="''fig-demo''", ? ? ? apparently eliminated by Achim *)
|
||||
caption="''Sample ''"]
|
||||
|
||||
figure*[fig_A::figure, spawn_columns=False,
|
||||
|
@ -130,6 +134,6 @@ text\<open>@{trace_attribute figs1}\<close>
|
|||
text\<open>Final Status:\<close>
|
||||
print_doc_items
|
||||
print_doc_classes
|
||||
check_doc_global
|
||||
|
||||
end
|
||||
(*>*)
|
|
@ -1,10 +1,12 @@
|
|||
chapter\<open>Setting and modifying attributes of doc-items\<close>
|
||||
|
||||
theory Concept_Example
|
||||
imports "../../ontologies/Conceptual" (* we use the generic "Conceptual" ontology *)
|
||||
theory
|
||||
Concept_Example
|
||||
imports
|
||||
"../ontologies/Conceptual" (* we use the generic "Conceptual" ontology *)
|
||||
begin
|
||||
|
||||
text\<open>@{theory Draft.Conceptual} provides a monitor @{typ M} enforcing a particular document structure.
|
||||
text\<open>@{theory "Isabelle_DOF-tests.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]
|
||||
|
@ -29,7 +31,7 @@ fancy unicode such as: @{term "\<open>\<beta>\<^sub>i''\<close>"} \<close>
|
|||
|
||||
text*[f::F] \<open> Lectus accumsan velit ultrices, ... }\<close>
|
||||
|
||||
theorem some_proof : "P" sorry
|
||||
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''}]"]
|
||||
|
@ -52,4 +54,4 @@ print_doc_items
|
|||
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -1,7 +1,9 @@
|
|||
chapter\<open>Setting and modifying attributes of doc-items\<close>
|
||||
|
||||
theory Concept_ExampleInvariant
|
||||
imports "../../ontologies/Conceptual" (* we use the generic "Conceptual" ontology *)
|
||||
theory
|
||||
Concept_ExampleInvariant
|
||||
imports
|
||||
"../ontologies/Conceptual" (* we use the generic "Conceptual" ontology *)
|
||||
begin
|
||||
|
||||
section\<open>Example: Standard Class Invariant\<close>
|
||||
|
@ -108,4 +110,4 @@ close_monitor*[struct]
|
|||
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -1,7 +1,9 @@
|
|||
chapter\<open>Inner Syntax Antiquotations (ISA)'s\<close>
|
||||
|
||||
theory InnerSyntaxAntiquotations
|
||||
imports "../../ontologies/Conceptual"
|
||||
theory
|
||||
InnerSyntaxAntiquotations
|
||||
imports
|
||||
"../ontologies/Conceptual"
|
||||
begin
|
||||
|
||||
text\<open>Since the syntax chosen for values of doc-class attributes is HOL-syntax --- requiring
|
||||
|
@ -14,7 +16,7 @@ They are the key-mechanism to denote
|
|||
\<^item> Ontological Links, i.e. attributes refering to document classes defined by the ontology
|
||||
\<^item> Ontological F-Links, i.e. attributes referring to formal entities inside Isabelle (such as thm's)
|
||||
|
||||
This file contains a number of examples resulting from the @{theory "Draft.Conceptual"} - ontology;
|
||||
This file contains a number of examples resulting from the @{theory "Isabelle_DOF-tests.Conceptual"} - ontology;
|
||||
the emphasis of this presentation is to present the expressivity of ODL on a paradigmatical example.
|
||||
\<close>
|
||||
|
||||
|
@ -26,11 +28,13 @@ val {docobj_tab={tab = x, ...},docclass_tab, ISA_transformer_tab,...} = DOF_core
|
|||
\<close>
|
||||
|
||||
text\<open>Some sample lemma:\<close>
|
||||
lemma murks : "Example" sorry
|
||||
lemma murks : "Example=Example" by simp
|
||||
|
||||
text\<open>Example for a meta-attribute of ODL-type @{typ "file"} with an appropriate ISA for the
|
||||
file @{file "./Attributes.thy"}\<close>
|
||||
text*[xcv::F, u="@{file ''./examples/conceptual/Attributes.thy''}"]\<open>Lorem ipsum ...\<close>
|
||||
file @{file "InnerSyntaxAntiquotations.thy"}\<close>
|
||||
(* not working:
|
||||
text*[xcv::F, u="@{file ''InnerSyntaxAntiquotations.thy''}"]\<open>Lorem ipsum ...\<close>
|
||||
*)
|
||||
|
||||
text*[xcv1::A, x=5]\<open>Lorem ipsum ...\<close>
|
||||
text*[xcv3::A, x=7]\<open>Lorem ipsum ...\<close>
|
Before Width: | Height: | Size: 12 KiB After Width: | Height: | Size: 12 KiB |
Before Width: | Height: | Size: 96 KiB After Width: | Height: | Size: 96 KiB |
Loading…
Reference in New Issue