minor changes for CICM paper example.
HOL-OCL/Isabelle_DOF/master There was a failure building this commit Details

This commit is contained in:
Burkhart Wolff 2019-03-13 12:49:29 +01:00
parent 7f8c77b2ef
commit ff3f2c9429
2 changed files with 22 additions and 4 deletions

View File

@ -1482,9 +1482,11 @@ val _ = Theory.setup((docitem_antiquotation @{binding docref} DOF_core.default_c
(* deprecated syntax ^^^^^^*)
(docitem_antiquotation @{binding docitem_ref} DOF_core.default_cid) #>
(* deprecated syntax ^^^^^^^^^^*)
(docitem_antiquotation @{binding docitem} DOF_core.default_cid) #>
ML_Antiquotation.inline @{binding docitem_value} ML_antiquotation_docitem_value)
docitem_antiquotation @{binding docitem} DOF_core.default_cid #>
(* Thy_Output.antiquotation @{binding docitem} docitem_antiquotation_parser
(docitem_antiquotation_generic DOF_core.default_cid) #>
*)
ML_Antiquotation.inline @{binding docitem_value} ML_antiquotation_docitem_value)
end (* struct *)
\<close>

View File

@ -47,7 +47,23 @@ datatype kind = expert_opinion | argument | "proof"
doc_class result = technical +
evidence :: kind
property :: "thm list" <= "[]"
c :: "thm list" <= "[]"
ML\<open>fun check_invariant_invariant oid {is_monitor:bool} ctxt =
let val kind_term = AttributeAccess.compute_attr_access ctxt "kind" oid @{here} @{here}
val property_termS = AttributeAccess.compute_attr_access ctxt "property" oid @{here} @{here}
val tS = HOLogic.dest_list property_termS
in case kind_term of
@{term "proof"} => if not(null tS) then true
else error("class class invariant violation")
| _ => false
end
\<close>
setup\<open>DOF_core.update_class_invariant "small_math.result" check_invariant_invariant\<close>
doc_class example = technical +
referring_to :: "(notion + definition) set" <= "{}"