Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
ci/woodpecker/push/build Pipeline failed Details

This commit is contained in:
Burkhart Wolff 2023-11-25 17:06:39 +01:00
parent e2b3184a77 331fcd07f0
commit 443d63f3b5
1 changed files with 15 additions and 50 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

65
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -1798,20 +1798,16 @@ fun check_invariants thy binding =
val cids_invariants = get_all_invariants name thy
val inv_and_apply_list =
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
let val ctxt = Proof_Context.init_global thy
val (cid_long, invs) = cid_invs
in invs |> map
(fn (bind, _) =>
let
val inv_name = Binding.name_of bind
|> Long_Name.qualify (Long_Name.base_name cid_long)
|> Long_Name.qualify 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)
val inv_def = inv_name |> Syntax.parse_term ctxt
in ((inv_name, pos), Syntax.check_term ctxt (inv_def $ value)) end)
end
in cids_invariants |> map (fn cid_invs => mk_inv_and_apply cid_invs docitem_value thy)
|> flat
@ -3054,49 +3050,18 @@ 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 bind f_sty read_cond (ctxt:local_theory) =
let val eq = mk_meta_eq(Free(Binding.name_of bind, f_sty),read_cond)
fun define_cond bind eq (ctxt:local_theory) =
let
val args = (SOME(bind,NONE,NoSyn), (Binding.empty_atts,eq),[],[])
in def_cmd args ctxt end
fun define_inv (params, cid_long) (bind, inv) thy =
let val inv_term = Syntax.read_term (Proof_Context.init_global thy) inv
fun update_attribute_type thy class_scheme_ty cid_long
(Const (s, Type (st,[ty, ty'])) $ t) =
let
val cid = Long_Name.qualifier s
in case Name_Space.lookup
(DOF_core.get_onto_classes (Proof_Context.init_global thy)) cid of
NONE => Const (s, Type(st,[ty, ty']))
$ (update_attribute_type thy class_scheme_ty cid_long t)
| SOME _ => if DOF_core.is_subclass_global thy cid_long cid
then let val Type(st', tys') = ty
in if tys' = [\<^typ>\<open>unit\<close>]
then Const (s, Type(st,[ty, ty']))
$ (update_attribute_type thy class_scheme_ty cid_long t)
else Const(s, Type(st,[class_scheme_ty, ty']))
$ (update_attribute_type thy class_scheme_ty cid_long t)
end
else Const (s, Type(st,[ty, ty']))
$ (update_attribute_type thy class_scheme_ty cid_long t)
end
| update_attribute_type thy class_scheme_ty cid_long (t $ t') =
(update_attribute_type thy class_scheme_ty cid_long t)
$ (update_attribute_type thy class_scheme_ty cid_long t')
| update_attribute_type thy class_scheme_ty cid_long (Abs(s, ty, t)) =
Abs(s, ty, update_attribute_type thy class_scheme_ty cid_long t)
| update_attribute_type _ class_scheme_ty _ (Free(s, ty)) = if s = instance_placeholderN
then Free (s, class_scheme_ty)
else Free (s, ty)
| update_attribute_type _ _ _ t = t
val zeta = (singleton (Name.variant_list (map #1 params)) "'z", \<^sort>\<open>type\<close>)
val typ = Type (cid_long ^ schemeN, map TFree (params @ [zeta]))
(* Update the type of each attribute update function to match the type of the
current class. *)
val inv_term' = update_attribute_type thy typ cid_long inv_term
val eq_inv_ty = typ --> HOLogic.boolT
val abs_term = Term.lambda (Free (instance_placeholderN, typ)) inv_term'
in thy |> Named_Target.theory_map (define_cond bind eq_inv_ty abs_term) end
fun define_inv (bind, inv) thy =
let val inv_parsed_term = Syntax.parse_term (Proof_Context.init_global thy) inv
val abs_term = Term.lambda (Free (instance_placeholderN, dummyT)) inv_parsed_term
val eq = Logic.mk_equals (Free(Binding.name_of bind, dummyT), abs_term)
|> Syntax.check_term (Proof_Context.init_global thy)
in thy |> Named_Target.theory_map (define_cond bind eq) end
fun add_doc_class_cmd overloaded (raw_params, binding)
raw_parent raw_fieldsNdefaults reject_Atoms regexps invariants thy =
@ -3169,7 +3134,7 @@ fun add_doc_class_cmd overloaded (raw_params, binding)
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 (params', (cid thy))) (invariants') thy)
|> (fn thy => fold define_inv (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 *)