nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Fix DOF manual and tests to work with assert*

This commit is contained in:
Nicolas Méric 2022-04-01 09:54:16 +02:00
parent 2351e00be6
commit 9603311a9a
2 changed files with 12 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
View File

@ -707,9 +707,10 @@ author*[bu::author, email = "\<open>wolff@lri.fr\<close>",
\<close>
text\<open>Assertions allow for logical statements to be checked in the global context.
This is particularly useful to explore formal definitions wrt. their border cases. \<close>
assert*[ass1::assertion, short_name = "\<open>This is an assertion\<close>"] \<open>last [3] < (4::int)\<close>
This is particularly useful to explore formal definitions wrt. their border cases.
@{boxed_theory_text [display]\<open>
assert*[ass1::assertion, short_name = "\<open>This is an assertion\<close>"] \<open>last [3] < (4::int)\<close>\<close>}
\<close>
text\<open>We want to check the consequences of this definition and can add the following statements:
@{boxed_theory_text [display]\<open>

11
src/tests/AssnsLemmaThmEtc.thy
View File

@ -29,10 +29,15 @@ print_doc_items
section\<open>Definitions, Lemmas, Theorems, Assertions\<close>
term\<open>True\<close>
text*[aa::F, properties = "[@{term ''True''}]"]
\<open>Our definition of the HOL-Logic has the following properties:\<close>
assert*[aa::F] "True"
assert*\<open>F.properties @{F \<open>aa\<close>} = [@{term ''True''}]\<close>
text\<open>For now, as the term annotation is not bound to a meta logic which will translate
\<^term>\<open>[@{term ''True''}]\<close> to \<^term>\<open>[True]\<close>, we can not use the HOL \<^const>\<open>True\<close> constant
in the assertion.
\<close>
(* does not work in batch mode ...
(* sample for accessing a property filled with previous assert's of "aa" *)
@ -70,7 +75,7 @@ different class. "F" and "assertion" have only in common that they posses the at
text\<open>Creation just like that: \<close>
assert*[ababa::assertion] "3 < (4::int)"
assert*[ababa::assertion] "0 < (4::int)"
assert*[ababab::assertion] "0 < (4::int)"
end