Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
ci/woodpecker/push/build Pipeline failed
Details
ci/woodpecker/push/build Pipeline failed
Details
This commit is contained in:
commit
d353ff07cc
|
|
@ -201,10 +201,12 @@ Consequently, it has the same limitations as \<^emph>\<open>value*\<close>.
|
|||
text\<open>Using the ontology defined in \<^theory>\<open>Isabelle_DOF-Unit-Tests.Concept_High_Level_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>
|
||||
term*\<open>authored_by @{Concept-High-Level-Invariants.introduction \<open>introduction2\<close>}
|
||||
= authored_by @{Concept-High-Level-Invariants.introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>authored_by @{Concept-High-Level-Invariants.introduction \<open>introduction2\<close>}
|
||||
= authored_by @{Concept-High-Level-Invariants.introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>\<not>(authored_by @{Concept-High-Level-Invariants.introduction \<open>introduction2\<close>}
|
||||
= authored_by @{Concept-High-Level-Invariants.introduction \<open>introduction4\<close>})\<close>
|
||||
|
||||
text\<open>Assertions must be boolean expressions, so the following assertion triggers an error:\<close>
|
||||
(* Error:
|
||||
|
|
@ -229,4 +231,13 @@ value* [optional_test_A::A, x=6] [nbe] \<open>filter (\<lambda>\<sigma>. A.x \<s
|
|||
assert* [resultProof3::result, evidence = "proof", property="[@{thm \<open>HOL.sym\<close>}]"] [nbe]
|
||||
\<open>evidence @{result \<open>resultProof3\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
|
||||
|
||||
text\<open>
|
||||
The evaluation of @{command "assert*"} can be disabled
|
||||
using the *\<open>disable_assert_evaluation\<close> theory attribute.
|
||||
Then only the checking of the term is done:
|
||||
\<close>
|
||||
declare[[disable_assert_evaluation]]
|
||||
assert*\<open>evidence @{result \<open>resultProof3\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
|
||||
declare[[disable_assert_evaluation = false]]
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -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 \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 0"
|
||||
invariant level :: "(level \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 0"
|
||||
|
||||
doc_class related_work = "conclusion" +
|
||||
main_author :: "author option" <= None
|
||||
invariant L\<^sub>r\<^sub>w :: "(level \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 0"
|
||||
invariant level :: "(level \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 0"
|
||||
|
||||
doc_class bibliography = text_section +
|
||||
style :: "string option" <= "Some ''LNCS''"
|
||||
invariant L\<^sub>b\<^sub>i\<^sub>b :: "(level \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 0"
|
||||
invariant level :: "(level \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 0"
|
||||
|
||||
doc_class annex = "text_section" +
|
||||
main_author :: "author option" <= None
|
||||
invariant L\<^sub>a\<^sub>n\<^sub>n\<^sub>e\<^sub>x :: "(level \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 0"
|
||||
invariant level :: "(level \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 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 \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 0"
|
||||
invariant level :: "(level \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 0"
|
||||
|
||||
text\<open>Technical text-elements posses a status: they can be either an \<^emph>\<open>informal explanation\<close> /
|
||||
description or a kind of introductory text to definition etc. or a \<^emph>\<open>formal statement\<close> 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 \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 0"
|
||||
invariant level :: "(level \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 0"
|
||||
|
||||
|
||||
section\<open>Technical Content and Free-form Semi-formal Formats\<close>
|
||||
|
|
@ -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 \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 0"
|
||||
invariant level :: "(level \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 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 \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 0"
|
||||
invariant level :: "(level \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 0"
|
||||
|
||||
text\<open>The intended use for the \<open>doc_class\<close>es \<^verbatim>\<open>math_motivation\<close> (or \<^verbatim>\<open>math_mtv\<close> for short),
|
||||
\<^verbatim>\<open>math_explanation\<close> (or \<^verbatim>\<open>math_exp\<close> 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 \<sigma> = prpo" (* can not be changed anymore. *)
|
||||
invariant d :: "mcc \<sigma> = prpo" (* can not be changed anymore. *)
|
||||
|
||||
text\<open>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 \<sigma> = defn" (* can not be changed anymore. *)
|
||||
invariant d :: "mcc \<sigma> = 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 \<sigma> = axm" (* can not be changed anymore. *)
|
||||
invariant d :: "mcc \<sigma> = axm" (* can not be changed anymore. *)
|
||||
|
||||
text\<open>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 \<sigma> = lemm"
|
||||
invariant d :: "mcc \<sigma> = lemm"
|
||||
|
||||
doc_class "theorem" = math_content +
|
||||
referentiable :: bool <= True
|
||||
level :: "int option" <= "Some 2"
|
||||
mcc :: "math_content_class" <= "theom"
|
||||
invariant d4 :: "mcc \<sigma> = theom"
|
||||
invariant d :: "mcc \<sigma> = theom"
|
||||
|
||||
text\<open>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 \<sigma> = corr"
|
||||
invariant d :: "mcc \<sigma> = corr"
|
||||
|
||||
|
||||
text\<open>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 \<sigma> = prms"
|
||||
invariant d :: "mcc \<sigma> = prms"
|
||||
|
||||
text\<open>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 \<sigma> = cons"
|
||||
invariant d :: "mcc \<sigma> = cons"
|
||||
|
||||
doc_class "conclusion_stmt" = math_content + \<comment> \<open>not to confuse with a section element: Conclusion\<close>
|
||||
referentiable :: bool <= "True"
|
||||
level :: "int option" <= "Some 2"
|
||||
mcc :: "math_content_class" <= "conc_stmt"
|
||||
invariant d8 :: "mcc \<sigma> = conc_stmt"
|
||||
invariant d :: "mcc \<sigma> = conc_stmt"
|
||||
|
||||
text\<open>An assertion is a statement that asserts that a certain premise is true.\<close>
|
||||
doc_class "assertion" = math_content +
|
||||
referentiable :: bool <= "True"
|
||||
level :: "int option" <= "Some 2"
|
||||
mcc :: "math_content_class" <= "assn"
|
||||
invariant d9 :: "mcc \<sigma> = assn"
|
||||
invariant d :: "mcc \<sigma> = assn"
|
||||
|
||||
text\<open>An assumption is an explicit or a tacit proposition about the world or a background belief
|
||||
relating to an proposition.\<close>
|
||||
|
|
@ -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 \<sigma> = assm"
|
||||
invariant d :: "mcc \<sigma> = assm"
|
||||
|
||||
text\<open> 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 \<sigma> = hypt"
|
||||
invariant d :: "mcc \<sigma> = hypt"
|
||||
|
||||
doc_class "math_proof" = math_content +
|
||||
referentiable :: bool <= "True"
|
||||
level :: "int option" <= "Some 2"
|
||||
mcc :: "math_content_class" <= "prf_stmt"
|
||||
invariant d12 :: "mcc \<sigma> = prf_stmt"
|
||||
invariant d :: "mcc \<sigma> = 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 \<sigma> = expl_stmt"
|
||||
invariant d :: "mcc \<sigma> = expl_stmt"
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -1867,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
|
||||
\<comment> \<open>c.f. \<^file>\<open>~~/src/Pure/Isar/isar_cmd.ML\<close>\<close>
|
||||
|
||||
(*
|
||||
|
|
@ -1895,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>\<open>disable_assert_evaluation\<close> (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 _ =
|
||||
|
|
@ -1922,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>\<open>assert*\<close> "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
|
||||
|
|
@ -2277,7 +2293,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 +2939,13 @@ fun def_cmd (decl, spec, prems, params) lthy =
|
|||
|
||||
fun mk_meta_eq (t, u) = \<^Const>\<open>Pure.eq \<open>fastype_of t\<close> for t u\<close>;
|
||||
|
||||
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 +2983,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 +3029,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 +3037,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 +3061,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)
|
||||
|
|
|
|||
|
|
@ -520,6 +520,11 @@ The @{command "assert*"}-command allows for logical statements to be checked in
|
|||
% 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.
|
||||
For @{command "assert*"}, the evaluation of the term can be disabled
|
||||
with the \<^boxed_theory_text>\<open>disable_assert_evaluation\<close> theory attribute:
|
||||
@{boxed_theory_text [display]\<open>
|
||||
declare[[disable_assert_evaluation]]\<close>}
|
||||
Then @{command "assert*"} will act like @{command "term*"}.
|
||||
|
||||
The @{command "definition*"}-command allows \<open>prop\<close>, \<open>spec_prems\<close>, and \<open>for_fixes\<close>
|
||||
(see the @{command "definition"} command in @{cite "wenzel:isabelle-isar:2020"}) to contain
|
||||
|
|
|
|||
Loading…
Reference in New Issue