forked from Isabelle_DOF/Isabelle_DOF
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
This commit is contained in:
commit
543c647bcc
|
|
@ -131,7 +131,7 @@ text\<open>Now assume the following ontology:\<close>
|
|||
doc_class title =
|
||||
short_title :: "string option" <= "None"
|
||||
|
||||
doc_class Author =
|
||||
doc_class author =
|
||||
email :: "string" <= "''''"
|
||||
|
||||
datatype classification = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
|
||||
|
|
@ -141,18 +141,18 @@ doc_class abstract =
|
|||
safety_level :: "classification" <= "SIL3"
|
||||
|
||||
doc_class text_section =
|
||||
authored_by :: "Author set" <= "{}"
|
||||
authored_by :: "author set" <= "{}"
|
||||
level :: "int option" <= "None"
|
||||
|
||||
type_synonym notion = string
|
||||
|
||||
doc_class Introduction = text_section +
|
||||
authored_by :: "Author set" <= "UNIV"
|
||||
doc_class introduction = text_section +
|
||||
authored_by :: "author set" <= "UNIV"
|
||||
uses :: "notion set"
|
||||
invariant author_finite :: "finite (authored_by \<sigma>)"
|
||||
and force_level :: "(level \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 1"
|
||||
|
||||
doc_class claim = Introduction +
|
||||
doc_class claim = introduction +
|
||||
based_on :: "notion list"
|
||||
|
||||
doc_class technical = text_section +
|
||||
|
|
@ -181,7 +181,10 @@ text\<open>Next we define some instances (docitems): \<close>
|
|||
|
||||
declare[[invariants_checking_with_tactics = true]]
|
||||
|
||||
text*[church::Author, email="\<open>church@lambda.org\<close>"]\<open>\<close>
|
||||
text*[church::author, email="\<open>church@lambda.org\<close>"]\<open>\<close>
|
||||
|
||||
text\<open>We can also reference instances of classes defined in parent theories:\<close>
|
||||
text*[church'::scholarly_paper.author, email="\<open>church'@lambda.org\<close>"]\<open>\<close>
|
||||
|
||||
text*[resultProof::result, evidence = "proof", property="[@{thm \<open>HOL.refl\<close>}]"]\<open>\<close>
|
||||
text*[resultArgument::result, evidence = "argument"]\<open>\<close>
|
||||
|
|
@ -193,29 +196,41 @@ text\<open>The invariants \<^theory_text>\<open>author_finite\<close> and \<^the
|
|||
|
||||
declare[[invariants_checking_with_tactics = true]]
|
||||
|
||||
text*[curry::Author, email="\<open>curry@lambda.org\<close>"]\<open>\<close>
|
||||
text*[introduction2::Introduction, authored_by = "{@{Author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
|
||||
text*[curry::author, email="\<open>curry@lambda.org\<close>"]\<open>\<close>
|
||||
|
||||
text*[introduction2::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
|
||||
(* When not commented, should violated the invariant:
|
||||
update_instance*[introduction2::Introduction
|
||||
, authored_by := "{@{Author \<open>church\<close>}}"
|
||||
, level := "Some 1"]
|
||||
*)
|
||||
text\<open>Use of the instance @{docitem_name "church'"}
|
||||
to instantiate a \<^doc_class>\<open>scholarly_paper.introduction\<close> class:\<close>
|
||||
text*[introduction2'::scholarly_paper.introduction,
|
||||
main_author = "Some @{scholarly-paper.author \<open>church'\<close>}", level = "Some 2"]\<open>\<close>
|
||||
|
||||
value*\<open>@{scholarly-paper.author \<open>church'\<close>}\<close>
|
||||
value*\<open>@{author \<open>church\<close>}\<close>
|
||||
value*\<open>@{Concept-High-Level-Invariants.author \<open>church\<close>}\<close>
|
||||
|
||||
text*[introduction3::Introduction, authored_by = "{@{Author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
|
||||
text*[introduction4::Introduction, authored_by = "{@{Author \<open>curry\<close>}}", level = "Some 4"]\<open>\<close>
|
||||
value*\<open>@{scholarly-paper.author-instances}\<close>
|
||||
value*\<open>@{author-instances}\<close>
|
||||
value*\<open>@{Concept-High-Level-Invariants.author-instances}\<close>
|
||||
|
||||
text*[introduction3::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
|
||||
text*[introduction4::introduction, authored_by = "{@{author \<open>curry\<close>}}", level = "Some 4"]\<open>\<close>
|
||||
|
||||
text*[resultProof2::result, evidence = "proof", property="[@{thm \<open>HOL.sym\<close>}]"]\<open>\<close>
|
||||
|
||||
text\<open>Then we can evaluate expressions with instances:\<close>
|
||||
|
||||
term*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction3\<close>}\<close>
|
||||
value*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction3\<close>}\<close>
|
||||
value*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction4\<close>}\<close>
|
||||
term*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
|
||||
value*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
|
||||
value*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction4\<close>}\<close>
|
||||
|
||||
value*\<open>@{Introduction \<open>introduction2\<close>}\<close>
|
||||
value*\<open>@{introduction \<open>introduction2\<close>}\<close>
|
||||
|
||||
value*\<open>{@{Author \<open>curry\<close>}} = {@{Author \<open>church\<close>}}\<close>
|
||||
value*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>
|
||||
|
||||
term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
|
||||
value*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
|
||||
|
|
|
|||
|
|
@ -22,9 +22,12 @@ begin
|
|||
section\<open>Test Purpose.\<close>
|
||||
text\<open> Creation of document parts that are controlled by (nested, locally defined) monitors. \<close>
|
||||
|
||||
doc_class test_monitor_B =
|
||||
tmB :: int
|
||||
|
||||
doc_class monitor_M =
|
||||
tmM :: int
|
||||
rejects "test_monitor_B"
|
||||
rejects "Concept_MonitorTest1.test_monitor_B"
|
||||
accepts "test_monitor_E ~~ test_monitor_C"
|
||||
|
||||
doc_class test_monitor_head =
|
||||
|
|
|
|||
|
|
@ -200,10 +200,10 @@ 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 @{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:
|
||||
|
|
|
|||
|
|
@ -806,24 +806,24 @@ fun binding_from_onto_class_pos name thy =
|
|||
fun binding_from_instance_pos name thy =
|
||||
binding_from_pos get_instances get_instance_name_global name thy
|
||||
|
||||
fun check_invs get_ml_invs cid_long oid is_monitor thy =
|
||||
fun check_invs get_ml_invs invariant_class_of invariant_check_of cid_long oid is_monitor thy =
|
||||
thy |> Context.Theory
|
||||
|> (fn ctxt =>
|
||||
let val invs = get_ml_invs (Proof_Context.init_global thy)
|
||||
|> Name_Space.dest_table
|
||||
val checks = invs |> filter (fn (_, inv) => let val ML_Invariant class = inv
|
||||
in class |> #class |> equal cid_long
|
||||
end)
|
||||
|> map (fn (_, inv) => let val ML_Invariant check = inv
|
||||
in check |> #check end)
|
||||
val checks = invs |> filter (fn (name, _) =>
|
||||
equal (invariant_class_of name thy) cid_long)
|
||||
|> map (fn (name, _) => invariant_check_of name thy)
|
||||
|> map (fn check => check oid is_monitor ctxt)
|
||||
in (List.all I checks) end)
|
||||
in (forall I checks) end)
|
||||
|
||||
val check_ml_invs = check_invs get_ml_invariants
|
||||
val check_ml_invs = check_invs get_ml_invariants ml_invariant_class_of ml_invariant_check_of
|
||||
|
||||
val check_opening_ml_invs = check_invs get_opening_ml_invariants
|
||||
val check_opening_ml_invs =
|
||||
check_invs get_opening_ml_invariants opening_ml_invariant_class_of opening_ml_invariant_check_of
|
||||
|
||||
val check_closing_ml_invs = check_invs get_closing_ml_invariants
|
||||
val check_closing_ml_invs =
|
||||
check_invs get_closing_ml_invariants closing_ml_invariant_class_of closing_ml_invariant_check_of
|
||||
|
||||
(* Output name for LaTeX macros.
|
||||
Also rewrite "." to allow macros with objects long names *)
|
||||
|
|
@ -833,12 +833,10 @@ val ISA_prefix = "Isabelle_DOF_"
|
|||
|
||||
val doc_class_prefix = ISA_prefix ^ "doc_class_"
|
||||
|
||||
val long_doc_class_prefix = ISA_prefix ^ "long_doc_class_"
|
||||
|
||||
fun is_ISA s = String.isPrefix ISA_prefix (Long_Name.base_name s)
|
||||
|
||||
fun get_class_name_without_prefix s = String.extract (s, String.size(doc_class_prefix), NONE)
|
||||
|
||||
fun get_doc_class_name_without_ISA_prefix s = String.extract (s, String.size(ISA_prefix), NONE)
|
||||
|
||||
|
||||
fun transduce_term_global {mk_elaboration=mk_elaboration} (term,pos) thy =
|
||||
(* pre: term should be fully typed in order to allow type-related term-transformations *)
|
||||
|
|
@ -1115,19 +1113,20 @@ fun ML_isa_check_thm thy (term, _, pos) _ =
|
|||
|
||||
fun ML_isa_check_file thy (term, _, pos) _ =
|
||||
let fun check thy (name, _) = name |> Syntax.read_input
|
||||
|> Resources.check_file (Proof_Context.init_global thy) NONE
|
||||
|> Resources.check_file (Proof_Context.init_global thy) NONE
|
||||
in ML_isa_check_generic check thy (term, pos) end;
|
||||
|
||||
fun check_instance thy (term, _, pos) s =
|
||||
let
|
||||
val bname = Long_Name.base_name s;
|
||||
val qual = Long_Name.qualifier s;
|
||||
val class_name =
|
||||
Long_Name.qualify qual (String.extract(bname , String.size(DOF_core.doc_class_prefix), NONE));
|
||||
val class_name = (case try (unprefix DOF_core.doc_class_prefix) bname of
|
||||
NONE => unprefix DOF_core.long_doc_class_prefix bname
|
||||
| SOME name => name)
|
||||
|> Long_Name.qualify qual
|
||||
fun check thy (name, _) =
|
||||
let
|
||||
val object_cid = let val DOF_core.Instance cid = DOF_core.get_instance_global name thy
|
||||
in cid |> #cid end
|
||||
val object_cid = DOF_core.cid_of name thy
|
||||
fun check' (class_name, object_cid) =
|
||||
if class_name = object_cid then
|
||||
DOF_core.value_of name thy
|
||||
|
|
@ -1150,6 +1149,11 @@ fun ML_isa_check_trace_attribute thy (term, _, _) _ =
|
|||
val _ = DOF_core.get_instance_global oid thy
|
||||
in SOME term end
|
||||
|
||||
fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ =
|
||||
case term_option of
|
||||
NONE => error("Wrong term option. You must use a defined term")
|
||||
| SOME term => Const (isa_name, ty) $ term
|
||||
|
||||
(* Convert excluded mixfix symbols.
|
||||
Unfortunately due to different lexical conventions for constant symbols and mixfix symbols
|
||||
we can not use "_" or "'" for classes names in term antiquotation.
|
||||
|
|
@ -1159,10 +1163,19 @@ val clean_string = translate_string
|
|||
| "'" => "-"
|
||||
| c => c);
|
||||
|
||||
fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ =
|
||||
case term_option of
|
||||
NONE => error("Wrong term option. You must use a defined term")
|
||||
| SOME term => Const (isa_name, ty) $ term
|
||||
fun rm_mixfix name mixfix thy =
|
||||
let
|
||||
val old_constants =
|
||||
Consts.dest (Sign.consts_of thy) |> #constants
|
||||
|> map fst
|
||||
|> filter (Long_Name.base_name #> equal name)
|
||||
|> map (pair mixfix)
|
||||
|> map swap
|
||||
|> map (apfst (Syntax.read_term_global thy))
|
||||
|> map (apsnd Mixfix.mixfix)
|
||||
in thy |> (Local_Theory.notation false Syntax.mode_default old_constants
|
||||
|> Named_Target.theory_map)
|
||||
end
|
||||
|
||||
fun elaborate_instance thy _ _ term_option pos =
|
||||
case term_option of
|
||||
|
|
@ -1177,49 +1190,64 @@ fun elaborate_instance thy _ _ term_option pos =
|
|||
because the class name is already bound to "doc_class Regular_Exp.rexp" constant
|
||||
by add_doc_class_cmd function
|
||||
*)
|
||||
fun declare_ISA_class_accessor_and_check_instance doc_class_name =
|
||||
fun declare_ISA_class_accessor_and_check_instance (doc_class_name, bind_pos) thy =
|
||||
let
|
||||
val bind = Binding.prefix_name DOF_core.doc_class_prefix doc_class_name
|
||||
val typestring = "string => " ^ (Binding.name_of doc_class_name)
|
||||
val conv_class_name = clean_string (Binding.name_of doc_class_name)
|
||||
val mixfix_string = "@{" ^ conv_class_name ^ " _}"
|
||||
val bname = Long_Name.base_name doc_class_name
|
||||
val bname' = prefix DOF_core.doc_class_prefix bname
|
||||
val bind = bname' |> pair bind_pos |> swap |> Binding.make
|
||||
val bind' = prefix DOF_core.long_doc_class_prefix bname
|
||||
|> pair bind_pos |> swap |> Binding.make
|
||||
val const_typ = \<^typ>\<open>string\<close> --> Syntax.read_typ (Proof_Context.init_global thy) doc_class_name
|
||||
fun mixfix_enclose name = name |> enclose "@{" " _}"
|
||||
val mixfix = clean_string bname |> mixfix_enclose
|
||||
val mixfix' = clean_string doc_class_name |> mixfix_enclose
|
||||
in
|
||||
Sign.add_consts_cmd [(bind, typestring, Mixfix.mixfix(mixfix_string))]
|
||||
#> DOF_core.add_isa_transformer bind ((check_instance, elaborate_instance)
|
||||
|> DOF_core.make_isa_transformer)
|
||||
thy |> rm_mixfix bname' mixfix
|
||||
|> Sign.add_consts [(bind, const_typ, Mixfix.mixfix mixfix)]
|
||||
|> DOF_core.add_isa_transformer bind ((check_instance, elaborate_instance)
|
||||
|> DOF_core.make_isa_transformer)
|
||||
|> Sign.add_consts [(bind', const_typ, Mixfix.mixfix mixfix')]
|
||||
|> DOF_core.add_isa_transformer bind' ((check_instance, elaborate_instance)
|
||||
|> DOF_core.make_isa_transformer)
|
||||
end
|
||||
|
||||
fun elaborate_instances_list thy isa_name _ _ _ =
|
||||
let
|
||||
val base_name = Long_Name.base_name isa_name
|
||||
fun get_isa_name_without_intances_suffix s =
|
||||
String.extract (s, 0, SOME (String.size(s) - String.size(instances_of_suffixN)))
|
||||
val base_name_without_suffix = get_isa_name_without_intances_suffix base_name
|
||||
val base_name' = DOF_core.get_class_name_without_prefix (base_name_without_suffix)
|
||||
val class_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
|
||||
(base_name')
|
||||
val long_class_name = DOF_core.get_onto_class_name_global base_name' thy
|
||||
val qualifier = Long_Name.qualifier isa_name
|
||||
val isa_name' = (case try (unprefix DOF_core.doc_class_prefix) base_name of
|
||||
NONE => unprefix DOF_core.long_doc_class_prefix base_name
|
||||
| SOME name => name)
|
||||
|> unsuffix instances_of_suffixN
|
||||
|> Long_Name.qualify qualifier
|
||||
val class_typ = isa_name' |> Proof_Context.read_typ (Proof_Context.init_global thy)
|
||||
val long_class_name = DOF_core.get_onto_class_name_global isa_name' thy
|
||||
val values = thy |> Proof_Context.init_global |> DOF_core.get_instances
|
||||
|> Name_Space.dest_table
|
||||
|> filter (fn (_, instance) =>
|
||||
let val DOF_core.Instance cid = instance
|
||||
in (cid |> #cid) = long_class_name end)
|
||||
|> filter (fn (name, _) => equal (DOF_core.cid_of name thy) long_class_name)
|
||||
|> map (fn (oid, _) => DOF_core.value_of oid thy)
|
||||
in HOLogic.mk_list class_typ values end
|
||||
|
||||
|
||||
fun declare_class_instances_annotation thy doc_class_name =
|
||||
fun declare_class_instances_annotation (doc_class_name, bind_pos) thy =
|
||||
let
|
||||
val bind = Binding.prefix_name DOF_core.doc_class_prefix doc_class_name
|
||||
|> Binding.suffix_name instances_of_suffixN
|
||||
val class_list_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
|
||||
((Binding.name_of doc_class_name) ^ " List.list")
|
||||
val conv_class_name' = clean_string ((Binding.name_of doc_class_name) ^ instances_of_suffixN)
|
||||
val mixfix_string = "@{" ^ conv_class_name' ^ "}"
|
||||
val bname = Long_Name.base_name doc_class_name
|
||||
val bname' = prefix DOF_core.doc_class_prefix bname |> suffix instances_of_suffixN
|
||||
val bind = bname' |> pair bind_pos |> swap |> Binding.make
|
||||
val bind' = prefix DOF_core.long_doc_class_prefix bname
|
||||
|> suffix instances_of_suffixN |> pair bind_pos |> swap |> Binding.make
|
||||
val class_typ = doc_class_name |> Proof_Context.read_typ (Proof_Context.init_global thy)
|
||||
fun mixfix_enclose name = name |> enclose "@{" "}"
|
||||
val mixfix = clean_string (bname ^ instances_of_suffixN) |> mixfix_enclose
|
||||
val mixfix' = clean_string (doc_class_name ^ instances_of_suffixN) |> mixfix_enclose
|
||||
in
|
||||
Sign.add_consts [(bind, class_list_typ, Mixfix.mixfix(mixfix_string))]
|
||||
#> DOF_core.add_isa_transformer bind ((check_identity, elaborate_instances_list)
|
||||
|> DOF_core.make_isa_transformer)
|
||||
thy |> rm_mixfix bname' mixfix
|
||||
|> Sign.add_consts [(bind, \<^Type>\<open>list class_typ\<close>, Mixfix.mixfix mixfix)]
|
||||
|> DOF_core.add_isa_transformer bind ((check_identity, elaborate_instances_list)
|
||||
|> DOF_core.make_isa_transformer)
|
||||
|> Sign.add_consts [(bind', \<^Type>\<open>list class_typ\<close>, Mixfix.mixfix mixfix')]
|
||||
|> DOF_core.add_isa_transformer bind' ((check_identity, elaborate_instances_list)
|
||||
|> DOF_core.make_isa_transformer)
|
||||
end
|
||||
|
||||
fun symbex_attr_access0 ctxt proj_term term =
|
||||
|
|
@ -2968,6 +2996,7 @@ fun define_inv cid_long ((lbl, pos), inv) thy =
|
|||
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 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;
|
||||
|
|
@ -3024,8 +3053,8 @@ fun add_doc_class_cmd overloaded (raw_params, binding)
|
|||
(* 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 *)
|
||||
|> ISA_core.declare_ISA_class_accessor_and_check_instance binding
|
||||
|> (fn thy => (ISA_core.declare_class_instances_annotation thy binding) thy)
|
||||
|> (fn thy => ISA_core.declare_ISA_class_accessor_and_check_instance (cid thy, bind_pos) thy)
|
||||
|> (fn thy => ISA_core.declare_class_instances_annotation (cid thy, bind_pos) thy)
|
||||
end;
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue