From 350ff6fe76bf824b8a840463c14b40bb4970a25f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Tue, 23 May 2023 07:49:41 +0200 Subject: [PATCH 1/3] Make class invariants long-names unique MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Now class invariants names use internally the class name as a user Binding.qualifier. This way one can use the same name for an invariant in two different classes in the same theory: doc_class "hypothesis" = math_content + referentiable :: bool <= "True" level :: "int option" <= "Some 2" mcc :: "math_content_class" <= "hypt" invariant d :: "mcc σ = hypt" doc_class "math_proof" = math_content + referentiable :: bool <= "True" level :: "int option" <= "Some 2" mcc :: "math_content_class" <= "prf_stmt" invariant d :: "mcc σ = prf_stmt" find_consts name:"math_proof.d_inv" find_consts name:"hypothesis.d_inv" --- .../scholarly_paper/scholarly_paper.thy | 46 ++++++------ Isabelle_DOF/thys/Isa_DOF.thy | 74 +++++++++++-------- 2 files changed, 66 insertions(+), 54 deletions(-) diff --git a/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy b/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy index 7e83c624..732200f1 100644 --- a/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy +++ b/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy @@ -85,19 +85,21 @@ doc_class text_section = text_element + doc_class "conclusion" = text_section + main_author :: "author option" <= None - invariant L\<^sub>c\<^sub>o\<^sub>n\<^sub>c :: "(level \) \ None \ the (level \) > 0" + invariant level :: "(level \) \ None \ the (level \) > 0" doc_class related_work = "conclusion" + main_author :: "author option" <= None - invariant L\<^sub>r\<^sub>w :: "(level \) \ None \ the (level \) > 0" + invariant level :: "(level \) \ None \ the (level \) > 0" doc_class bibliography = text_section + style :: "string option" <= "Some ''LNCS''" - invariant L\<^sub>b\<^sub>i\<^sub>b :: "(level \) \ None \ the (level \) > 0" + invariant level :: "(level \) \ None \ the (level \) > 0" doc_class annex = "text_section" + main_author :: "author option" <= None - invariant L\<^sub>a\<^sub>n\<^sub>n\<^sub>e\<^sub>x :: "(level \) \ None \ the (level \) > 0" + invariant level :: "(level \) \ None \ the (level \) > 0" + +find_consts name:"scholarly_paper.*Leeee" (* datatype sc_dom = math | info | natsc | eng @@ -107,7 +109,7 @@ datatype sc_dom = math | info | natsc | eng doc_class introduction = text_section + comment :: string claims :: "thm list" - invariant L\<^sub>i\<^sub>n\<^sub>t\<^sub>r\<^sub>o :: "(level \) \ None \ the (level \) > 0" + invariant level :: "(level \) \ None \ the (level \) > 0" text\Technical text-elements posses a status: they can be either an \<^emph>\informal explanation\ / description or a kind of introductory text to definition etc. or a \<^emph>\formal statement\ similar @@ -122,7 +124,7 @@ A formal statement can, but must not have a reference to true formal Isabelle/Is doc_class background = text_section + comment :: string claims :: "thm list" - invariant L\<^sub>b\<^sub>a\<^sub>c\<^sub>k :: "(level \) \ None \ the (level \) > 0" + invariant level :: "(level \) \ None \ the (level \) > 0" section\Technical Content and Free-form Semi-formal Formats\ @@ -140,7 +142,7 @@ doc_class technical = text_section + definition_list :: "string list" <= "[]" status :: status <= "description" formal_results :: "thm list" - invariant L\<^sub>t\<^sub>e\<^sub>c\<^sub>h :: "(level \) \ None \ the (level \) > 0" + invariant level :: "(level \) \ None \ the (level \) > 0" type_synonym tc = technical (* technical content *) @@ -156,7 +158,7 @@ doc_class example = text_section + referentiable :: bool <= True status :: status <= "description" short_name :: string <= "''''" - invariant L\<^sub>e\<^sub>x\<^sub>a :: "(level \) \ None \ the (level \) > 0" + invariant level :: "(level \) \ None \ the (level \) > 0" text\The intended use for the \doc_class\es \<^verbatim>\math_motivation\ (or \<^verbatim>\math_mtv\ for short), \<^verbatim>\math_explanation\ (or \<^verbatim>\math_exp\ for short) and @@ -239,7 +241,7 @@ doc_class "proposition" = math_content + referentiable :: bool <= True level :: "int option" <= "Some 2" mcc :: "math_content_class" <= "prpo" - invariant d0 :: "mcc \ = prpo" (* can not be changed anymore. *) + invariant d :: "mcc \ = prpo" (* can not be changed anymore. *) text\A definition is used to give a precise meaning to a new term, by describing a condition which unambiguously qualifies what a mathematical term is and is not. Definitions and @@ -248,13 +250,13 @@ doc_class "definition" = math_content + referentiable :: bool <= True level :: "int option" <= "Some 2" mcc :: "math_content_class" <= "defn" - invariant d1 :: "mcc \ = defn" (* can not be changed anymore. *) + invariant d :: "mcc \ = defn" (* can not be changed anymore. *) doc_class "axiom" = math_content + referentiable :: bool <= True level :: "int option" <= "Some 2" mcc :: "math_content_class" <= "axm" - invariant d2 :: "mcc \ = axm" (* can not be changed anymore. *) + invariant d :: "mcc \ = axm" (* can not be changed anymore. *) text\A lemma (plural lemmas or lemmata) is a generally minor, proven proposition which is used as a stepping stone to a larger result. For that reason, it is also known as a "helping theorem" or an @@ -263,13 +265,13 @@ doc_class "lemma" = math_content + referentiable :: bool <= "True" level :: "int option" <= "Some 2" mcc :: "math_content_class" <= "lemm" - invariant d3 :: "mcc \ = lemm" + invariant d :: "mcc \ = lemm" doc_class "theorem" = math_content + referentiable :: bool <= True level :: "int option" <= "Some 2" mcc :: "math_content_class" <= "theom" - invariant d4 :: "mcc \ = theom" + invariant d :: "mcc \ = theom" text\A corollary is a theorem of less importance which can be readily deduced from a previous, more notable lemma or theorem. A corollary could, for instance, be a proposition which is incidentally @@ -278,7 +280,7 @@ doc_class "corollary" = math_content + referentiable :: bool <= "True" level :: "int option" <= "Some 2" mcc :: "math_content_class" <= "corr" - invariant d5 :: "mcc \ = corr" + invariant d :: "mcc \ = corr" text\A premise or premiss[a] is a proposition — a true or false declarative statement— @@ -287,7 +289,7 @@ doc_class "premise" = math_content + referentiable :: bool <= "True" level :: "int option" <= "Some 2" mcc :: "math_content_class" <= "prms" - invariant d6 :: "mcc \ = prms" + invariant d :: "mcc \ = prms" text\A consequence describes the relationship between statements that hold true when one statement logically follows from one or more statements. A valid logical argument is one in which the @@ -298,20 +300,20 @@ doc_class "consequence" = math_content + referentiable :: bool <= "True" level :: "int option" <= "Some 2" mcc :: "math_content_class" <= "cons" - invariant d7 :: "mcc \ = cons" + invariant d :: "mcc \ = cons" doc_class "conclusion_stmt" = math_content + \ \not to confuse with a section element: Conclusion\ referentiable :: bool <= "True" level :: "int option" <= "Some 2" mcc :: "math_content_class" <= "conc_stmt" - invariant d8 :: "mcc \ = conc_stmt" + invariant d :: "mcc \ = conc_stmt" text\An assertion is a statement that asserts that a certain premise is true.\ doc_class "assertion" = math_content + referentiable :: bool <= "True" level :: "int option" <= "Some 2" mcc :: "math_content_class" <= "assn" - invariant d9 :: "mcc \ = assn" + invariant d :: "mcc \ = assn" text\An assumption is an explicit or a tacit proposition about the world or a background belief relating to an proposition.\ @@ -319,7 +321,7 @@ doc_class "assumption" = math_content + referentiable :: bool <= "True" level :: "int option" <= "Some 2" mcc :: "math_content_class" <= "assm" - invariant d10 :: "mcc \ = assm" + invariant d :: "mcc \ = assm" text\ A working hypothesis is a provisionally accepted hypothesis proposed for further research in a process beginning with an educated guess or thought. @@ -331,19 +333,19 @@ doc_class "hypothesis" = math_content + referentiable :: bool <= "True" level :: "int option" <= "Some 2" mcc :: "math_content_class" <= "hypt" - invariant d11 :: "mcc \ = hypt" + invariant d :: "mcc \ = hypt" doc_class "math_proof" = math_content + referentiable :: bool <= "True" level :: "int option" <= "Some 2" mcc :: "math_content_class" <= "prf_stmt" - invariant d12 :: "mcc \ = prf_stmt" + invariant d :: "mcc \ = prf_stmt" doc_class "math_example"= math_content + referentiable :: bool <= "True" level :: "int option" <= "Some 2" mcc :: "math_content_class" <= "expl_stmt" - invariant d13 :: "mcc \ = expl_stmt" + invariant d :: "mcc \ = expl_stmt" diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index 3b62c5d8..19720e00 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -100,7 +100,7 @@ struct attribute_decl : (binding*typ*term option)list, (* class local *) rejectS : term list, rex : term list, - invs : ((string * Position.T) * term) list } (* monitoring regexps --- product semantics*) + invs : (binding * term) list } (* monitoring regexps --- product semantics*) fun make_onto_class (params, name, virtual, inherits_from, attribute_decl , rejectS, rex, invs) = Onto_Class {params = params, name = name, virtual = virtual, inherits_from = inherits_from @@ -702,8 +702,9 @@ fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms i val _ = map check_regexps reg_exps val _ = if not(null rejectS) andalso (null reg_exps) then error ("reject clause requires accept clause ! " ) else (); - val _ = if has_duplicates (op =) (map (fst o fst) invs) - then error("invariant labels must be unique"^ Position.here (snd(fst(hd invs)))) + val _ = if invs |> map (Binding.name_of o fst) |> has_duplicates (uncurry equal) + then invs |> hd |> fst |> Binding.pos_of + |> (fn pos => error("invariant labels must be unique"^ Position.here pos)) else () val invs' = map (apsnd(Syntax.read_term_global thy)) invs in thy |> add_onto_class binding (make_onto_class (params', binding, virtual, parent', fields @@ -1688,25 +1689,32 @@ fun register_oid_cid_in_open_monitors oid _ cid_pos thy = fun check_invariants thy (oid, _) = let val docitem_value = DOF_core.value_of oid thy - val DOF_core.Instance params = DOF_core.get_instance_global oid thy - val cid = #cid params + val cid = DOF_core.cid_of oid thy fun get_all_invariants cid thy = case DOF_core.get_onto_class_global cid thy of - DOF_core.Onto_Class {inherits_from=NONE, invs, ...} => invs + DOF_core.Onto_Class {inherits_from=NONE, invs, ...} => single (cid, invs) | DOF_core.Onto_Class {inherits_from=SOME(_,father), invs, ...} => - (invs) @ (get_all_invariants father thy) - val invariants = get_all_invariants cid thy + (cid, invs) :: (get_all_invariants father thy) + val cids_invariants = get_all_invariants cid thy val inv_and_apply_list = - let fun mk_inv_and_apply inv value thy = - let val ((s, pos), _ (*term*)) = inv - val inv_def = Syntax.read_term_global thy (s ^ invariant_suffixN) + let fun mk_inv_and_apply cid_invs value thy = + let val (cid_long, invs) = cid_invs val inv_def_typ = Term.type_of value - in case inv_def of - Const (s, Type (st, [_ (*ty*), ty'])) => - ((s, pos), Const (s, Type (st,[inv_def_typ, ty'])) $ value) - | _ => ((s, pos), inv_def $ value) + in invs |> map + (fn (bind, _) => + let + val inv_name = Binding.name_of bind + |> Long_Name.qualify (Long_Name.base_name cid_long) + val pos = Binding.pos_of bind + val inv_def = inv_name + |> Syntax.read_term_global thy + in case inv_def of + Const (s, Type (st, [_ (*ty*), ty'])) => + ((inv_name, pos), Const (s, Type (st,[inv_def_typ, ty'])) $ value) + | _ => ((inv_name, pos), inv_def $ value) end) end - in map (fn inv => mk_inv_and_apply inv docitem_value thy) invariants + in cids_invariants |> map (fn cid_invs => mk_inv_and_apply cid_invs docitem_value thy) + |> flat end fun check_invariants' ((inv_name, pos), term) = let val ctxt = Proof_Context.init_global thy @@ -2277,7 +2285,8 @@ fun print_doc_classes _ ctxt = val _ = writeln "====================================="; fun print_attr (n, _, NONE) = (Binding.print n) | print_attr (n, _, SOME t)= (Binding.print n^"("^Syntax.string_of_term ctxt t^")") - fun print_inv ((lab,_),trm) = (lab ^"::"^Syntax.string_of_term ctxt trm) + fun print_inv (bind,trm) = ((Binding.name_of bind |> unsuffix invariant_suffixN) + ^"::"^Syntax.string_of_term ctxt trm) fun print_virtual {virtual} = Bool.toString virtual fun print_class (n, DOF_core.Onto_Class {attribute_decl, name, inherits_from, virtual , invs, ...}) = @@ -2922,15 +2931,13 @@ fun def_cmd (decl, spec, prems, params) lthy = fun mk_meta_eq (t, u) = \<^Const>\Pure.eq \fastype_of t\ for t u\; -fun define_cond binding f_sty cond_suffix read_cond (ctxt:local_theory) = - let val bdg = Binding.suffix_name cond_suffix binding - val eq = mk_meta_eq(Free(Binding.name_of bdg, f_sty),read_cond) - val args = (SOME(bdg,NONE,NoSyn), (Binding.empty_atts,eq),[],[]) +fun define_cond bind f_sty read_cond (ctxt:local_theory) = + let val eq = mk_meta_eq(Free(Binding.name_of bind, f_sty),read_cond) + val args = (SOME(bind,NONE,NoSyn), (Binding.empty_atts,eq),[],[]) in def_cmd args ctxt end -fun define_inv cid_long ((lbl, pos), inv) thy = - let val bdg = Binding.make (lbl,pos) - val inv_term = Syntax.read_term (Proof_Context.init_global thy) inv +fun define_inv cid_long (bind, inv) thy = + let val inv_term = Syntax.read_term (Proof_Context.init_global thy) inv (* Rewrite selectors types to allow invariants on attributes of the superclasses using the polymorphic type of the class *) fun update_attribute_type thy class_scheme_ty cid_long @@ -2968,17 +2975,18 @@ fun define_inv cid_long ((lbl, pos), inv) thy = val inv_term' = update_attribute_type thy inv_ty cid_long inv_term val eq_inv_ty = inv_ty --> HOLogic.boolT val abs_term = Term.lambda (Free (instance_placeholderN, inv_ty)) inv_term' - in thy |> Named_Target.theory_map (define_cond bdg eq_inv_ty invariant_suffixN abs_term) end + in thy |> Named_Target.theory_map (define_cond bind eq_inv_ty abs_term) end fun add_doc_class_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdefaults reject_Atoms regexps invariants thy = let val bind_pos = Binding.pos_of binding + val name = Binding.name_of binding val ctxt = Proof_Context.init_global thy; val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params; val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt; fun cid thy = (* takes class synonyms into account *) - DOF_core.get_onto_class_name_global' (Binding.name_of binding) thy + DOF_core.get_onto_class_name_global' name thy val (parent, ctxt2) = read_parent raw_parent ctxt1; (* takes class synonyms into account *) val parent' = parent |> Option.map (fn (x, y) => (x, DOF_core.get_onto_class_name_global' y thy)) @@ -3013,7 +3021,7 @@ fun add_doc_class_cmd overloaded (raw_params, binding) |> mk_meta_eq val args = (SOME(binding,NONE,NoSyn) , (Binding.empty_atts, Binding.name_of binding |> mk_eq_pair), [], []) - fun add record_fields virtual = + fun add record_fields invariants virtual = Record.add_record overloaded (params', binding) parent' record_fields #> (Local_Theory.notation true Syntax.mode_default RegExpInterface_Notations.notations |> Named_Target.theory_map) @@ -3021,16 +3029,18 @@ fun add_doc_class_cmd overloaded (raw_params, binding) reject_Atoms invariants virtual #> (Local_Theory.notation false Syntax.mode_default RegExpInterface_Notations.notations |> Named_Target.theory_map) + val invariants' = invariants |> map (apfst (Binding.qualify false name + #> Binding.suffix_name invariant_suffixN)) in thy (* adding const symbol representing doc-class for Monitor-RegExps.*) |> Named_Target.theory_map (def_cmd args) |> (case parent' of - NONE => add (DOF_core.tag_attr::record_fields) {virtual=false} + NONE => add (DOF_core.tag_attr::record_fields) invariants' {virtual=false} | SOME _ => if (not o null) record_fields - then add record_fields {virtual=false} - else add [DOF_core.tag_attr] {virtual=true}) + then add record_fields invariants' {virtual=false} + else add [DOF_core.tag_attr] invariants' {virtual=true}) |> (fn thy => OntoLinkParser.docitem_antiquotation binding (cid thy) thy) (* defines the ontology-checked text antiquotation to this document class *) - |> (fn thy => fold(define_inv (cid thy)) (invariants) thy) + |> (fn thy => fold(define_inv (cid thy)) (invariants') thy) (* The function declare_ISA_class_accessor_and_check_instance uses a prefix because the class name is already bound to "doc_class Regular_Exp.rexp" constant by add_doc_class_cmd function *) @@ -3043,7 +3053,7 @@ fun add_doc_class_cmd overloaded (raw_params, binding) fun add_doc_class_cmd' (((overloaded, hdr), (parent, attrs)),((rejects,accept_rex),invars)) = (add_doc_class_cmd {overloaded = overloaded} hdr parent attrs rejects accept_rex invars) -val parse_invariants = Parse.and_list (Args.name_position --| Parse.$$$ "::" -- Parse.term) +val parse_invariants = Parse.and_list (Parse.binding --| Parse.$$$ "::" -- Parse.term) val parse_doc_class = (Parse_Spec.overloaded -- (Parse.type_args_constrained -- Parse.binding) From 2c0b51779e8a19a53fe937e80d7fea52dd181be5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Wed, 24 May 2023 12:38:29 +0200 Subject: [PATCH 2/3] Add the possibility to disable evaluation for assert* --- .../Concept_TermEvaluation.thy | 18 ++++++-- Isabelle_DOF/thys/Isa_DOF.thy | 42 +++++++++++-------- 2 files changed, 39 insertions(+), 21 deletions(-) diff --git a/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy b/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy index f241a16f..027d6b9b 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy @@ -201,10 +201,12 @@ Consequently, it has the same limitations as \<^emph>\value*\. text\Using the ontology defined in \<^theory>\Isabelle_DOF-Unit-Tests.Concept_High_Level_Invariants\ we can check logical statements:\ -term*\authored_by @{introduction \introduction2\} = authored_by @{introduction \introduction3\}\ -assert*\authored_by @{introduction \introduction2\} = authored_by @{introduction \introduction3\}\ -assert*\\(authored_by @{introduction \introduction2\} - = authored_by @{introduction \introduction4\})\ +term*\authored_by @{Concept-High-Level-Invariants.introduction \introduction2\} + = authored_by @{Concept-High-Level-Invariants.introduction \introduction3\}\ +assert*\authored_by @{Concept-High-Level-Invariants.introduction \introduction2\} + = authored_by @{Concept-High-Level-Invariants.introduction \introduction3\}\ +assert*\\(authored_by @{Concept-High-Level-Invariants.introduction \introduction2\} + = authored_by @{Concept-High-Level-Invariants.introduction \introduction4\})\ text\Assertions must be boolean expressions, so the following assertion triggers an error:\ (* Error: @@ -229,4 +231,12 @@ value* [optional_test_A::A, x=6] [nbe] \filter (\\. A.x \evidence @{result \resultProof3\} = evidence @{result \resultProof2\}\ +text\ +Evaluation of \assert*\ can be disabled using the *\disable_assert_evaluation\ theory attribute. +Then only the checking of the term is done: +\ +declare[[disable_assert_evaluation]] +assert*\evidence @{result \resultProof3\} = evidence @{result \resultProof2\}\ +declare[[disable_assert_evaluation = false]] + end diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index 19720e00..c3209403 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -1708,10 +1708,10 @@ fun check_invariants thy (oid, _) = val pos = Binding.pos_of bind val inv_def = inv_name |> Syntax.read_term_global thy - in case inv_def of - Const (s, Type (st, [_ (*ty*), ty'])) => + in case inv_def of + Const (s, Type (st, [_ (*ty*), ty'])) => ((inv_name, pos), Const (s, Type (st,[inv_def_typ, ty'])) $ value) - | _ => ((inv_name, pos), inv_def $ value) end) + | _ => ((inv_name, pos), inv_def $ value) end) end in cids_invariants |> map (fn cid_invs => mk_inv_and_apply cid_invs docitem_value thy) |> flat @@ -1875,11 +1875,6 @@ in trans |> Toplevel.theory (value_cmd {assert=false} meta_args_opt name modes t pos) end -fun pass_trans_to_assert_value_cmd meta_args_opt ((name, modes), t) trans = -let val pos = Toplevel.pos_of trans -in - trans |> Toplevel.theory (value_cmd {assert=true} meta_args_opt name modes t pos) -end \ \c.f. \<^file>\~~/src/Pure/Isar/isar_cmd.ML\\ (* @@ -1903,21 +1898,32 @@ end; fun print_item string_of (modes, arg) state = Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) (); +fun prin t pos state _ = string_of_term t pos (Toplevel.context_of state) + fun print_term meta_args_opt (string_list, string) trans = let val pos = Toplevel.pos_of trans - fun prin state _ = string_of_term string pos (Toplevel.context_of state) -in - Toplevel.theory(fn thy => - (print_item prin (string_list, string) (Toplevel.theory_toplevel thy); - thy |> meta_args_exec meta_args_opt ) - ) trans +in meta_args_exec meta_args_opt + #> tap (fn thy => print_item (prin string pos) (string_list, string) (Toplevel.theory_toplevel thy)) + |> (fn thy => Toplevel.theory thy trans) end -val _ = Toplevel.theory -val _ = Toplevel.theory_toplevel +val (disable_assert_evaluation, disable_assert_evaluation_setup) + = Attrib.config_bool \<^binding>\disable_assert_evaluation\ (K false); +val _ = Theory.setup disable_assert_evaluation_setup +fun pass_trans_to_assert_value_cmd meta_args_opt ((name, modes), t) trans = +let val pos = Toplevel.pos_of trans +in trans + |> Toplevel.theory + (fn thy => + if Config.get_global thy disable_assert_evaluation + then (meta_args_exec meta_args_opt + #> tap (fn thy => print_item (prin t pos) (modes, t) (Toplevel.theory_toplevel thy))) + thy + else value_cmd {assert=true} meta_args_opt name modes t pos thy) +end (* setup ontology aware commands *) val _ = @@ -1930,10 +1936,12 @@ val _ = (ODL_Meta_Args_Parser.opt_attributes -- (opt_evaluator -- opt_modes -- Parse.term) >> (uncurry pass_trans_to_value_cmd)); + + val _ = Outer_Syntax.command \<^command_keyword>\assert*\ "evaluate and assert term" (ODL_Meta_Args_Parser.opt_attributes -- (opt_evaluator -- opt_modes -- Parse.term) - >> (uncurry pass_trans_to_assert_value_cmd)); + >> uncurry pass_trans_to_assert_value_cmd); (* setup ontology - aware text and ML antiquotations. Due to lexical restrictions, we can not From 4f8e5881383e960c3ed6c07888a34601834b1c0d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Wed, 24 May 2023 14:17:16 +0200 Subject: [PATCH 3/3] Document disable_assert_evaluation theory atttribute in the manual --- Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy | 3 ++- Isabelle_DOF/thys/manual/M_04_RefMan.thy | 5 +++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy b/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy index 027d6b9b..b1cb58eb 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_TermEvaluation.thy @@ -232,7 +232,8 @@ assert* [resultProof3::result, evidence = "proof", property="[@{thm \HOL.s \evidence @{result \resultProof3\} = evidence @{result \resultProof2\}\ text\ -Evaluation of \assert*\ can be disabled using the *\disable_assert_evaluation\ theory attribute. +The evaluation of @{command "assert*"} can be disabled +using the *\disable_assert_evaluation\ theory attribute. Then only the checking of the term is done: \ declare[[disable_assert_evaluation]] diff --git a/Isabelle_DOF/thys/manual/M_04_RefMan.thy b/Isabelle_DOF/thys/manual/M_04_RefMan.thy index 541735df..3a398e95 100644 --- a/Isabelle_DOF/thys/manual/M_04_RefMan.thy +++ b/Isabelle_DOF/thys/manual/M_04_RefMan.thy @@ -520,6 +520,11 @@ The @{command "assert*"}-command allows for logical statements to be checked in % TODO: % Section reference @{docitem (unchecked) \text-elements-expls\} has not the right number This is particularly useful to explore formal definitions wrt. their border cases. +For @{command "assert*"}, the evaluation of the term can be disabled +with the \<^boxed_theory_text>\disable_assert_evaluation\ theory attribute: + @{boxed_theory_text [display]\ + declare[[disable_assert_evaluation]]\} +Then @{command "assert*"} will act like @{command "term*"}. The @{command "definition*"}-command allows \prop\, \spec_prems\, and \for_fixes\ (see the @{command "definition"} command in @{cite "wenzel:isabelle-isar:2020"}) to contain