Update assert* to use isabelle/DOF evaluation
ci/woodpecker/pr/build Pipeline failed
Details
ci/woodpecker/pr/build Pipeline failed
Details
This commit is contained in:
Nicolas Méric
parent
9cd5323063
commit
e4e4a708a5
|
|
@ -324,21 +324,28 @@ is currently only available in the SML API's of the kernel.
|
|||
as specified in @{technical \<open>odl-manual0\<close>}.
|
||||
\<^item> \<open>meta_args\<close> :
|
||||
\<^rail>\<open>obj_id ('::' class_id) ((',' attribute '=' HOL_term) *) \<close>
|
||||
\<^item> \<^emph>\<open>evaluator\<close>: from @{cite "wenzel:isabelle-isar:2020"}, evaluation is tried first using ML,
|
||||
falling back to normalization by evaluation if this fails. Alternatively a specific
|
||||
evaluator can be selected using square brackets; typical evaluators use the
|
||||
current set of code equations to normalize and include \<open>simp\<close> for fully
|
||||
symbolic evaluation using the simplifier, \<open>nbe\<close> for \<^emph>\<open>normalization by
|
||||
evaluation\<close> and \<^emph>\<open>code\<close> for code generation in SML.
|
||||
\<^item> \<open>upd_meta_args\<close> :
|
||||
\<^rail>\<open> (obj_id ('::' class_id) ((',' attribute ('=' | '+=') HOL_term) * ))\<close>
|
||||
\<^item> \<open>annotated_text_element\<close> :
|
||||
\<^rail>\<open>
|
||||
( ( @@{command "text*"} '[' meta_args ']' '\<open>' formal_text '\<close>'
|
||||
( @@{command "text*"} '[' meta_args ']' '\<open>' formal_text '\<close>'
|
||||
| @@{command "ML*"} ('[' meta_args ']')? '\<open>' SML_code '\<close>'
|
||||
| @@{command "term*"} ('[' meta_args ']')? '\<open>' HOL_term '\<close>'
|
||||
| @@{command "value*"} ('[' meta_args ']')? '\<open>' HOL_term '\<close>'
|
||||
)
|
||||
|
|
||||
( @@{command "open_monitor*"}
|
||||
| @@{command "value*"} \<newline> ('[' meta_args ']' ('[' evaluator ']')?)? '\<open>' HOL_term '\<close>'
|
||||
| @@{command "assert*"} \<newline> ('[' meta_args ']' ('[' evaluator ']')?)? '\<open>' HOL_term '\<close>'
|
||||
)
|
||||
\<close>
|
||||
\<^rail>\<open>
|
||||
( @@{command "open_monitor*"}
|
||||
| @@{command "close_monitor*"}
|
||||
| @@{command "declare_reference*"}
|
||||
) '[' meta_args ']'
|
||||
)
|
||||
) '[' meta_args ']'
|
||||
| change_status_command
|
||||
| inspection_command
|
||||
| macro_command
|
||||
|
|
@ -399,23 +406,35 @@ in the context of the SML toplevel of the Isabelle system as in the correspondin
|
|||
\<^theory_text>\<open>ML\<open> \<dots> SML-code \<dots> \<close>\<close>-command.
|
||||
\<close>
|
||||
|
||||
(*<*)
|
||||
declare_reference*["text-elements-expls"::technical]
|
||||
(*>*)
|
||||
|
||||
subsection\<open>Ontological Term-Contexts and their Management\<close>
|
||||
text\<open>The major commands providing term-contexts are
|
||||
\<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close> and
|
||||
\<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>\<^footnote>\<open>The meta-argument list is optional.\<close>.
|
||||
\<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>,
|
||||
\<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close> and
|
||||
\<^theory_text>\<open>assert*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>\<^footnote>\<open>The meta-argument list is optional.\<close>.
|
||||
Wrt. creation, track-ability and checking they are analogous to the ontological text and
|
||||
code-commands. However the argument terms may contain term-antiquotations stemming from an
|
||||
ontology definition. Both term-contexts were type-checked and \<^emph>\<open>validated\<close> against
|
||||
the global context (so: in the term \<open>@{A \<open>oid\<close>}\<close>, \<open>oid\<close> is indeed a string which refers
|
||||
to a meta-object belonging to the document class \<open>A\<close>, for example).
|
||||
The term-context in the \<open>value*\<close>-command is additionally expanded (\<^eg> replaced) by a term
|
||||
denoting the meta-object. This expansion happens \<^emph>\<open>before\<close> evaluation of the term, thus permitting
|
||||
The term-context in the \<open>value*\<close>-command and \<^emph>\<open>assert*\<close>-command is additionally expanded
|
||||
(\<^eg> replaced) by a term denoting the meta-object.
|
||||
This expansion happens \<^emph>\<open>before\<close> evaluation of the term, thus permitting
|
||||
executable HOL-functions to interact with meta-objects.
|
||||
The \<^emph>\<open>assert*\<close>-command allows for logical statements to be checked in the global context
|
||||
(see @{technical (unchecked) \<open>text-elements-expls\<close>}).
|
||||
% TODO:
|
||||
% Section reference @{docitem (unchecked) \<open>text-elements-expls\<close>} has not the right number
|
||||
This is particularly useful to explore formal definitions wrt. their border cases.
|
||||
|
||||
Note unspecified attribute values were represented by free fresh variables which constrains \<^dof>
|
||||
to choose either the normalization-by-evaluation strategy \<^theory_text>\<open>nbe\<close> or a proof attempt via
|
||||
the \<^theory_text>\<open>auto\<close> method. A failure of these strategies will be reported and regarded as non-validation
|
||||
of this meta-object. The latter leads to a failure of the entire command.
|
||||
|
||||
\<close>
|
||||
|
||||
(*<*)
|
||||
|
|
@ -619,9 +638,6 @@ during the editing process but is only visible in the integrated source but usua
|
|||
a \<^typ>\<open>text_element\<close> to a specific \<^typ>\<open>author\<close>. Note that this is possible since \<^isadof> assigns to each
|
||||
document class also a class-type which is declared in the HOL environment.\<close>
|
||||
|
||||
(*<*)
|
||||
declare_reference*["text-elements-expls"::example]
|
||||
(*>*)
|
||||
text*[s23::example, main_author = "Some(@{author \<open>bu\<close>})"]\<open>
|
||||
Recall that concrete authors can be denoted by term-antiquotations generated by \<^isadof>; for example,
|
||||
this may be for a text fragment like
|
||||
|
|
@ -649,7 +665,7 @@ of the \<^isadof> language:
|
|||
\<newline>
|
||||
'[' meta_args ']' '\<open>' text '\<close>'
|
||||
)
|
||||
| @@{command "assert*"} '[' meta_args ']' '\<open>' term '\<close>'
|
||||
|
||||
\<close>
|
||||
\<close>
|
||||
|
||||
|
|
@ -680,14 +696,13 @@ text\<open>
|
|||
\<^boxed_theory_text>\<open>title*\<open> ... \<close>\<close> or \<^boxed_theory_text>\<open>section*\<open> ... \<close>\<close>, \<^eg>:
|
||||
|
||||
@{boxed_theory_text [display]\<open>
|
||||
title*[title::title]\<open>Isabelle/DOF\<close>
|
||||
subtitle*[subtitle::subtitle]\<open>User and Implementation Manual\<close>
|
||||
author*[adb::author, email="\<open>a.brucker@exeter.ac.uk\<close>",
|
||||
orcid="\<open>0000-0002-6355-1200\<close>", http_site="\<open>https://brucker.ch/\<close>",
|
||||
affiliation="\<open>University of Exeter, Exeter, UK\<close>"] \<open>Achim D. Brucker\<close>
|
||||
author*[bu::author, email = "\<open>wolff@lri.fr\<close>",
|
||||
affiliation = "\<open>Université Paris-Saclay, LRI, Paris, France\<close>"]\<open>Burkhart Wolff\<close>
|
||||
\<close>}
|
||||
title*[title::title]\<open>Isabelle/DOF\<close>
|
||||
subtitle*[subtitle::subtitle]\<open>User and Implementation Manual\<close>
|
||||
author*[adb::author, email="\<open>a.brucker@exeter.ac.uk\<close>",
|
||||
orcid="\<open>0000-0002-6355-1200\<close>", http_site="\<open>https://brucker.ch/\<close>",
|
||||
affiliation="\<open>University of Exeter, Exeter, UK\<close>"] \<open>Achim D. Brucker\<close>
|
||||
author*[bu::author, email = "\<open>wolff@lri.fr\<close>",
|
||||
affiliation = "\<open>Université Paris-Saclay, LRI, Paris, France\<close>"]\<open>Burkhart Wolff\<close>\<close>}
|
||||
|
||||
\<close>
|
||||
|
||||
|
|
@ -701,8 +716,7 @@ text\<open>We want to check the consequences of this definition and can add the
|
|||
text*[claim::assertion]\<open>For non-empty lists, our definition yields indeed
|
||||
the last element of a list.\<close>
|
||||
assert*[claim1::assertion] \<open>last[4::int] = 4\<close>
|
||||
assert*[claim2::assertion] \<open>last[1,2,3,4::int] = 4\<close>
|
||||
\<close>}
|
||||
assert*[claim2::assertion] \<open>last[1,2,3,4::int] = 4\<close>\<close>}
|
||||
\<close>
|
||||
|
||||
text\<open>
|
||||
|
|
@ -714,14 +728,12 @@ However, in order to avoid the somewhat tedious consequence:
|
|||
|
||||
the choice of the default class can be influenced by setting globally an attribute such as
|
||||
@{boxed_theory_text [display]
|
||||
\<open>declare[[ Definition_default_class = "definition"]]
|
||||
declare[[ Theorem_default_class = "theorem"]]
|
||||
\<close>}
|
||||
\<open>declare[[Definition_default_class = "definition"]]
|
||||
declare[[Theorem_default_class = "theorem"]]\<close>}
|
||||
|
||||
which allows the above example be shortened to:
|
||||
@{boxed_theory_text [display]
|
||||
\<open>Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>"] \<open> \<dots> \<close>
|
||||
\<close>}
|
||||
\<open>Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>"] \<open> \<dots> \<close>\<close>}
|
||||
\<close>
|
||||
|
||||
subsection\<open>The Ontology \<^verbatim>\<open>technical_report\<close>\<close>
|
||||
|
|
|
|||
Binary file not shown.
|
|
@ -1,82 +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
|
||||
*************************************************************************)
|
||||
|
||||
section \<open> Little theory implementing the an assertion command in Isabelle/HOL. \<close>
|
||||
text\<open>This command is useful for certification documents allowing to validate
|
||||
corner-cases of (executable) definitions. \<close>
|
||||
|
||||
theory Assert
|
||||
imports Main
|
||||
keywords "assert" ::thy_decl
|
||||
|
||||
begin
|
||||
|
||||
subsection\<open>Core\<close>
|
||||
|
||||
ML\<open>
|
||||
local
|
||||
(* Reimplementation needed because not exported from ML structure Value_Command *)
|
||||
fun value_maybe_select some_name =
|
||||
case some_name
|
||||
of NONE => Value_Command.value
|
||||
| SOME name => Value_Command.value_select name;
|
||||
in
|
||||
(* Reimplementation needed because not exported from ML structure Value_Command *)
|
||||
val opt_modes =
|
||||
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
|
||||
|
||||
(* Reimplementation needed because not exported from ML structure Value_Command *)
|
||||
val opt_evaluator =
|
||||
Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"})
|
||||
|
||||
(* Reimplementation structure Value_Command due to tiny modification of value_cmd. *)
|
||||
fun assert_cmd some_name modes raw_t ctxt (* state*) =
|
||||
let
|
||||
(* val ctxt = Toplevel.context_of state; *)
|
||||
val t = Syntax.read_term ctxt raw_t;
|
||||
val t' = value_maybe_select some_name ctxt t;
|
||||
val ty' = Term.type_of t';
|
||||
val ty' = case ty' of @{typ "bool"} => ty' | _ => error "Assertion expressions must be boolean.";
|
||||
val t' = case t' of @{term "True"} => t' | _ => error "Assertion failed.";
|
||||
val ctxt' = Proof_Context.augment t' ctxt;
|
||||
val p = Print_Mode.with_modes modes (fn () =>
|
||||
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
|
||||
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
|
||||
in Pretty.writeln p end;
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword assert} "evaluate and print term"
|
||||
(opt_evaluator -- opt_modes -- Parse.term
|
||||
>> (fn ((some_name, modes), t) =>
|
||||
Toplevel.keep ( (assert_cmd some_name modes t) o Toplevel.context_of) ));
|
||||
end
|
||||
\<close>
|
||||
|
||||
|
||||
|
||||
subsection\<open> Test: \<close>
|
||||
(*
|
||||
assert ""
|
||||
assert "3 = 4"
|
||||
assert "False"
|
||||
assert "5 * 5 = 25"
|
||||
*)
|
||||
|
||||
subsection\<open>Example\<close>
|
||||
|
||||
assert "True \<and> True "
|
||||
|
||||
assert "(5::int) * 5 = 25 "
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -1,70 +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
|
||||
*************************************************************************)
|
||||
|
||||
theory AssertLong
|
||||
imports Main
|
||||
keywords "assert" ::thy_decl
|
||||
|
||||
begin
|
||||
|
||||
|
||||
|
||||
|
||||
ML\<open>
|
||||
|
||||
fun value_maybe_select some_name =
|
||||
case some_name
|
||||
of NONE => Value_Command.value
|
||||
| SOME name => Value_Command.value_select name;
|
||||
|
||||
val TT = Unsynchronized.ref (HOLogic.boolT);
|
||||
|
||||
fun value_cmd2 some_name modes raw_t state =
|
||||
let
|
||||
val ctxt = Toplevel.context_of state;
|
||||
val t = Syntax.read_term ctxt raw_t;
|
||||
val t' = value_maybe_select some_name ctxt t;
|
||||
val ty' = Term.type_of t';
|
||||
val t' = case ty' of @{typ "bool"} => t' | _ => error "Assertion expressions must be boolean.";
|
||||
val t' = case t' of @{term "True"} => t' | _ => error "Assertion failed.";
|
||||
val ctxt' = Variable.auto_fixes t' ctxt;
|
||||
val p = Print_Mode.with_modes modes (fn () =>
|
||||
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
|
||||
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
|
||||
in Pretty.writeln p end;
|
||||
|
||||
\<close>
|
||||
ML\<open>value_cmd2\<close>
|
||||
definition ASSERT :: "bool \<Rightarrow> bool" where "ASSERT p == (p=True)"
|
||||
ML\<open>val x = @{code "ASSERT"}\<close>
|
||||
ML\<open>
|
||||
val opt_modes =
|
||||
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
|
||||
|
||||
val opt_evaluator =
|
||||
Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"})
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword assert} "evaluate and print term"
|
||||
(opt_evaluator -- opt_modes -- Parse.term
|
||||
>> (fn ((some_name, modes), t) =>
|
||||
let val _ = writeln t in
|
||||
(* Toplevel.keep (Value_Command.value_cmd some_name modes (enclose "ASSERT(" ")" t)) *)
|
||||
Toplevel.keep (value_cmd2 some_name modes t)
|
||||
end));
|
||||
\<close>
|
||||
|
||||
assert "True"
|
||||
assert "True \<and> True "
|
||||
ML\<open>!TT ;
|
||||
@{term "True"}\<close>
|
||||
|
|
@ -31,7 +31,6 @@ that provide direct support in the PIDE framework. \<close>
|
|||
theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
||||
imports Main
|
||||
RegExpInterface (* Interface to functional regular automata for monitoring *)
|
||||
Assert
|
||||
|
||||
keywords "+=" ":=" "accepts" "rejects" "invariant"
|
||||
|
||||
|
|
@ -42,7 +41,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
|||
"define_shortcut*" "define_macro*" :: thy_decl
|
||||
|
||||
and "text*" "text-macro*" :: document_body
|
||||
and "term*" "value*" :: diag
|
||||
and "term*" "value*" "assert*" :: diag
|
||||
|
||||
and "print_doc_classes" "print_doc_items"
|
||||
"print_doc_class_template" "check_doc_global" :: diag
|
||||
|
|
@ -1767,7 +1766,6 @@ end
|
|||
|
||||
\<close>
|
||||
|
||||
|
||||
ML \<comment> \<open>c.f. \<^file>\<open>~~/src/HOL/Tools/value_command.ML\<close>\<close>
|
||||
(*
|
||||
The value* command uses the same code as the value command
|
||||
|
|
@ -1786,7 +1784,7 @@ sig
|
|||
val value: Proof.context -> term -> term
|
||||
val value_without_elaboration: Proof.context -> term -> term
|
||||
val value_select: string -> Proof.context -> term -> term
|
||||
val value_cmd: (ODL_Command_Parser.meta_args_t option) -> xstring -> string list -> string
|
||||
val value_cmd: {assert: bool} -> (ODL_Command_Parser.meta_args_t option) -> xstring -> string list -> string
|
||||
-> Toplevel.state -> Position.T -> unit
|
||||
val add_evaluator: binding * (Proof.context -> term -> term)
|
||||
-> theory -> string * theory
|
||||
|
|
@ -1800,7 +1798,6 @@ structure Evaluators = Theory_Data
|
|||
(
|
||||
type T = (Proof.context -> term -> term) Name_Space.table;
|
||||
val empty = Name_Space.empty_table "evaluator";
|
||||
val extend = I;
|
||||
val merge = Name_Space.merge_tables;
|
||||
)
|
||||
|
||||
|
|
@ -1837,7 +1834,7 @@ fun meta_args_exec NONE thy = thy
|
|||
{is_monitor = false} {is_inline = false}
|
||||
oid pos (I cid_pos) (I doc_attrs))
|
||||
|
||||
fun value_cmd meta_args_opt raw_name modes raw_t state pos =
|
||||
fun value_cmd {assert=assert} meta_args_opt raw_name modes raw_t state pos =
|
||||
let
|
||||
val _ = meta_args_exec meta_args_opt
|
||||
val ctxt = Toplevel.context_of state;
|
||||
|
|
@ -1847,6 +1844,16 @@ fun value_cmd meta_args_opt raw_name modes raw_t state pos =
|
|||
(Proof_Context.theory_of ctxt);
|
||||
val t' = value_select name ctxt term';
|
||||
val ty' = Term.type_of t';
|
||||
val ty' = if assert
|
||||
then case ty' of
|
||||
\<^typ>\<open>bool\<close> => ty'
|
||||
| _ => error "Assertion expressions must be boolean."
|
||||
else ty'
|
||||
val t' = if assert
|
||||
then case t' of
|
||||
\<^term>\<open>True\<close> => t'
|
||||
| _ => error "Assertion failed."
|
||||
else t'
|
||||
val ctxt' = Proof_Context.augment t' ctxt;
|
||||
val p = Print_Mode.with_modes modes (fn () =>
|
||||
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
|
||||
|
|
@ -1869,7 +1876,13 @@ val opt_attributes = Scan.option ODL_Command_Parser.attributes
|
|||
fun pass_trans_to_value_cmd meta_args_opt ((name, modes), t) trans =
|
||||
let val pos = Toplevel.pos_of trans
|
||||
in
|
||||
Toplevel.keep (fn state => value_cmd meta_args_opt name modes t state pos) trans
|
||||
Toplevel.keep (fn state => value_cmd {assert=false} meta_args_opt name modes t state pos) trans
|
||||
end
|
||||
|
||||
fun pass_trans_to_assert_value_cmd meta_args_opt ((name, modes), t) trans =
|
||||
let val pos = Toplevel.pos_of trans
|
||||
in
|
||||
Toplevel.keep (fn state => value_cmd {assert=true} meta_args_opt name modes t state pos) trans
|
||||
end
|
||||
\<comment> \<open>c.f. \<^file>\<open>~~/src/Pure/Isar/isar_cmd.ML\<close>\<close>
|
||||
|
||||
|
|
@ -1927,6 +1940,11 @@ val _ = Theory.setup
|
|||
#> add_evaluator (\<^binding>\<open>nbe\<close>, Nbe.dynamic_value) #> snd
|
||||
#> add_evaluator (\<^binding>\<open>code\<close>, Code_Evaluation.dynamic_value_strict) #> snd);
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command \<^command_keyword>\<open>assert*\<close> "evaluate and assert term"
|
||||
(opt_attributes -- (opt_evaluator -- opt_modes -- Parse.term)
|
||||
>> (fn (meta_args_opt, eval_args ) => pass_trans_to_assert_value_cmd meta_args_opt eval_args));
|
||||
|
||||
end;
|
||||
\<close>
|
||||
|
||||
|
|
@ -2050,7 +2068,6 @@ val _ =
|
|||
end
|
||||
\<close>
|
||||
|
||||
|
||||
ML\<open>
|
||||
structure ODL_LTX_Converter =
|
||||
struct
|
||||
|
|
|
|||
|
|
@ -17,8 +17,6 @@ theory scholarly_paper
|
|||
imports "../../DOF/Isa_COL"
|
||||
keywords "author*" "abstract*"
|
||||
"Definition*" "Lemma*" "Theorem*" :: document_body
|
||||
and "assert*" :: thy_decl
|
||||
|
||||
|
||||
begin
|
||||
|
||||
|
|
@ -347,39 +345,7 @@ doc_class assertion = math_formal +
|
|||
properties :: "term list"
|
||||
|
||||
|
||||
ML\<open>
|
||||
(* TODO : Rework this code and make it closer to Definition*. There is still
|
||||
a rest of "abstract classes in it: any class possessing a properties attribute
|
||||
is admissible to this command, not just ... *)
|
||||
local open ODL_Command_Parser in
|
||||
|
||||
fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list),
|
||||
prop) =
|
||||
let fun conv_2_holstring thy = (bstring_to_holstring (Proof_Context.init_global thy))
|
||||
fun conv_attrs thy = (("properties",pos),"[@{termrepr ''"^conv_2_holstring thy prop ^" ''}]")
|
||||
::doc_attrs
|
||||
fun conv_attrs' thy = map (fn ((lhs,pos),rhs) => (((lhs,pos),"+="),rhs)) (conv_attrs thy)
|
||||
fun mks thy = case DOF_core.get_object_global_opt oid thy of
|
||||
SOME NONE => (error("update of declared but not created doc_item:" ^ oid))
|
||||
| SOME _ => (update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy)
|
||||
| NONE => (create_and_check_docitem
|
||||
{is_monitor = false} {is_inline = false}
|
||||
oid pos cid_pos (conv_attrs thy) thy)
|
||||
val check = (assert_cmd name_opt modes prop) o Proof_Context.init_global
|
||||
in
|
||||
(* Toplevel.keep (check o Toplevel.context_of) *)
|
||||
Toplevel.theory (fn thy => (check thy; mks thy))
|
||||
end
|
||||
|
||||
val attributes = attributes (* re-export *)
|
||||
|
||||
end
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword "assert*"}
|
||||
"evaluate and print term"
|
||||
(attributes -- opt_evaluator -- opt_modes -- Parse.term >> assertion_cmd');
|
||||
|
||||
\<close>
|
||||
|
||||
subsubsection*[ex_ass::example]\<open>Example\<close>
|
||||
text\<open>Assertions allow for logical statements to be checked in the global context). \<close>
|
||||
|
|
|
|||
|
|
@ -6,6 +6,7 @@ theory
|
|||
Evaluation
|
||||
imports
|
||||
"Isabelle_DOF-tests.TermAntiquotations"
|
||||
"Isabelle_DOF-tests.High_Level_Syntax_Invariants"
|
||||
begin
|
||||
|
||||
section\<open>\<^theory_text>\<open>ML*\<close>-Annotated SML-commands\<close>
|
||||
|
|
@ -84,8 +85,8 @@ value*\<open>A.x @{A \<open>xcv1\<close>}\<close>
|
|||
|
||||
text\<open>If the attribute of the instance is not initialized, we get an undefined value,
|
||||
whose type is the type of the attribute:\<close>
|
||||
term*\<open>level @{C \<open>xcv2\<close>}\<close>
|
||||
value*\<open>level @{C \<open>xcv2\<close>}\<close>
|
||||
term*\<open>B.level @{C \<open>xcv2\<close>}\<close>
|
||||
value*\<open>B.level @{C \<open>xcv2\<close>}\<close>
|
||||
|
||||
text\<open>The value of a TA is the term itself:\<close>
|
||||
term*\<open>C.g @{C \<open>xcv2\<close>}\<close>
|
||||
|
|
@ -170,4 +171,31 @@ to update the instance @{docitem \<open>xcv4\<close>}:
|
|||
update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{G ''xcv5''})}"]*)
|
||||
|
||||
|
||||
section\<open>\<^theory_text>\<open>assert*\<close>-Annotated assertion-commands\<close>
|
||||
|
||||
text\<open>The \<^emph>\<open>assert*\<close>-command allows for logical statements to be checked in the global context.
|
||||
It uses the same implementation as the \<^emph>\<open>value*\<close>-command and has the same limitations.
|
||||
\<close>
|
||||
|
||||
text\<open>Using the ontology defined in \<^theory>\<open>Isabelle_DOF-tests.High_Level_Syntax_Invariants\<close>
|
||||
we can check logical statements:\<close>
|
||||
|
||||
term*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>\<not>(authored_by @{introduction \<open>introduction2\<close>}
|
||||
= authored_by @{introduction \<open>introduction4\<close>})\<close>
|
||||
|
||||
text\<open>Assertions must be boolean expressions, so the following assertion triggers an error:\<close>
|
||||
(* Error:
|
||||
assert*\<open>@{introduction \<open>introduction2\<close>}\<close>*)
|
||||
|
||||
text\<open>Assertions must be true, hence the error:\<close>
|
||||
(* Error:
|
||||
assert*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>*)
|
||||
|
||||
term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
|
||||
assert*\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
|
||||
|
||||
assert*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
|
||||
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in New Issue