nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Make class invariants long-names unique 

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"
This commit is contained in:
Nicolas Méric 2023-05-23 07:49:41 +02:00
parent e17f09e624
commit 350ff6fe76
2 changed files with 66 additions and 54 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy
View File

@ -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"

74
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -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>\<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 +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)