Updated API.

Isabelle_DOF-Ontologies/document-templates/root-lipics-v2021-UNSUPPORTED.tex

@@ -23,6 +23,8 @@
 %% All customization and/or additional packages should be added to the file
 %% preamble.tex.
 
+
+\PassOptionsToPackage{english,USenglish}{babel}
 \documentclass[a4paper,UKenglish,cleveref, autoref,thm-restate]{lipics-v2021}
 \bibliographystyle{plainurl}% the mandatory bibstyle
 \title{No Title Given}

Isabelle_DOF-Unit-Tests/Concept_High_Level_Invariants.thy

@@ -241,4 +241,40 @@ declare[[invariants_checking_with_tactics = false]]
 
 declare[[invariants_strict_checking = false]]
 
+text\<open>Invariants can have term anti-quotations\<close>
+doc_class invA =
+a :: int
+
+text*[invA_inst::invA, a = 3]\<open>\<close>
+
+doc_class invB = invA +
+b :: int
+invariant a_pos :: "a \<sigma> \<ge> 0"
+
+text*[invB_inst::invB, a = 3]\<open>\<close>
+
+doc_class invC =
+c :: invB
+invariant a_invB_pos :: "a (c \<sigma>) \<ge> a @{invA \<open>invA_inst\<close>}"
+
+text*[invC_inst::invC, c = "@{invB \<open>invB_inst\<close>}"]\<open>\<close>
+
+text\<open>Bug:
+With the polymorphic class implementation, invariants type inference is to permissive:
+\<close>
+doc_class invA' =
+a :: int
+
+doc_class invB' = invA' +
+b :: int
+invariant a_pos :: "a \<sigma> \<ge> 0"
+
+doc_class ('a, 'b) invC' =
+c :: invB'
+d :: "'a list"
+e :: "'b list"
+invariant a_pos :: "a \<sigma> \<ge> 0"
+text\<open>The \<^const>\<open>a\<close> selector in the \<^const>\<open>a_pos_inv\<close> invariant of the class \<^doc_class>\<open>('a, 'b) invC'\<close>
+should be rejected as the class does not have nor inherit an \<^const>\<open>a\<close> attribute
+\<close>
 end

Isabelle_DOF/ontologies/scholarly_paper/DOF-scholarly_paper.sty

@@ -171,58 +171,58 @@
 %\newtheorem{definition}{Definition}
 %\newtheorem{theorem}{Theorem} 
 \newtheorem{defn}{Definition} 
-\newcommand{\defnautorefname}{Definition} 
+\providecommand{\defnautorefname}{Definition} 
 \NewEnviron{isamarkupDefinition*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
 \newtheorem{axm}{Axiom}
-\newcommand{\axmautorefname}{Axiom}
+\providecommand{\axmautorefname}{Axiom}
 \NewEnviron{isamarkupAxiom*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
 \newtheorem{theom}{Theorem}
-\newcommand{\theomautorefname}{Theorem}
+\providecommand{\theomautorefname}{Theorem}
 \NewEnviron{isamarkupTheorem*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
 \newtheorem{lemm}{Lemma}
-\newcommand{\lemmautorefname}{Lemma}
+\providecommand{\lemmautorefname}{Lemma}
 \NewEnviron{isamarkupLemma*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
 \newtheorem{corr}{Corollary}
-\newcommand{\corrautorefname}{Corollary}
+\providecommand{\corrautorefname}{Corollary}
 \NewEnviron{isamarkupCorollary*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
 \newtheorem{prpo}{Proposition}
-\newcommand{\prpoautorefname}{Proposition}
+\providecommand{\prpoautorefname}{Proposition}
 \NewEnviron{isamarkupProposition*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
 \newtheorem{rulE}{Rule}
-\newcommand{\rulEautorefname}{Rule}
+\providecommand{\rulEautorefname}{Rule}
 \NewEnviron{isamarkupRule*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
 \newtheorem{assn}{Assertion}    
-\newcommand{\assnautorefname}{Assertion}    
+\providecommand{\assnautorefname}{Assertion}    
 \NewEnviron{isamarkupAssertion*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
 \newtheorem{hypt}{Hypothesis}
-\newcommand{\hyptautorefname}{Hypothesis}
+\providecommand{\hyptautorefname}{Hypothesis}
 \NewEnviron{isamarkupHypothesis*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
 \newtheorem{assm}{Assumption}
-\newcommand{\assmautorefname}{Assumption}
+\providecommand{\assmautorefname}{Assumption}
 \NewEnviron{isamarkupAssumption*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
 \newtheorem{prms}{Premise}
-\newcommand{\prmsautorefname}{Premise}
+\providecommand{\prmsautorefname}{Premise}
 \NewEnviron{isamarkupPremise*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
 \newtheorem{cons}{Consequence}
-\newcommand{\consautorefname}{Consequence}
+\providecommand{\consautorefname}{Consequence}
 \NewEnviron{isamarkupConsequence*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
 \newtheorem{concUNDERSCOREstmt}{Conclusion}
-\newcommand{\concUNDERSCOREstmtautorefname}{Conclusion}
+\providecommand{\concUNDERSCOREstmtautorefname}{Conclusion}
 \NewEnviron{isamarkupConclusion*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
 \newtheorem{prfUNDERSCOREstmt}{Proof}
-\newcommand{\prfUNDERSCOREstmtautorefname}{Proof}
+\providecommand{\prfUNDERSCOREstmtautorefname}{Proof}
 \NewEnviron{isamarkupProof*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
 \newtheorem{explUNDERSCOREstmt}{Example}
-\newcommand{\explUNDERSCOREstmtautorefname}{Example}
+\providecommand{\explUNDERSCOREstmtautorefname}{Example}
 \NewEnviron{isamarkupExample*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
 \newtheorem{rmrk}{Remark}
-\newcommand{\rmrkautorefname}{Remark}
+\providecommand{\rmrkautorefname}{Remark}
 \NewEnviron{isamarkupRemark*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
 \newtheorem{notn}{Notation}
-\newcommand{\notnautorefname}{Notation}
+\providecommand{\notnautorefname}{Notation}
 \NewEnviron{isamarkupNotation*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
 \newtheorem{tmgy}{Terminology}
-\newcommand{\tmgyautorefname}{Terminology}
+\providecommand{\tmgyautorefname}{Terminology}
 \NewEnviron{isamarkupTerminology*}[1][]{\isaDof[env={text},#1,type={scholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}]{\BODY}}
 
 \newisadof{textDOTscholarlyUNDERSCOREpaperDOTmathUNDERSCOREcontent}%

Isabelle_DOF/thys/Isa_DOF.thy

@@ -1866,7 +1866,7 @@ fun check_invariants thy binding =
 fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} binding cid_pos doc_attrs thy =
   let
     val oid = Binding.name_of binding
-    val (((name, args_cid), typ), pos') = check_classref is_monitor cid_pos thy
+    val (((name, args_cid), typ:typ), pos') = check_classref is_monitor cid_pos thy
     val cid_pos' = (name, pos')
     val cid_long = fst cid_pos'
     val default_cid = args_cid = DOF_core.default_cid
@@ -1891,13 +1891,13 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} bi
                             val defaults_init = create_default_object thy binding cid_long typ
                             fun conv (na, _(*ty*), parsed_term) =(Binding.name_of na, Binding.pos_of na, "=", parsed_term);
                             val S = map conv (DOF_core.get_attribute_defaults cid_long thy);
-                            val (defaults, _(*ty*), _) = calc_update_term {mk_elaboration=false}
+                            val (defaults, _) = calc_update_term {mk_elaboration=false}
                                                                       thy (name, typ) S defaults_init;
-                            val (value_term', _(*ty*), _) = calc_update_term {mk_elaboration=true}
+                            val (value_term', _) = calc_update_term {mk_elaboration=true}
                                                                       thy (name, typ) assns' defaults
                           in if Config.get_global thy DOF_core.object_value_debug
                              then let
-                                    val (input_term, _(*ty*), _) = calc_update_term {mk_elaboration=false}
+                                    val (input_term, _) = calc_update_term {mk_elaboration=false}
                                                                         thy (name, typ)  assns' defaults
                                   in (input_term, value_term') end
                              else (\<^term>\<open>()\<close>, value_term') end
@@ -3056,7 +3056,8 @@ fun define_cond bind eq (ctxt:local_theory) =
        in def_cmd args ctxt end
 
 fun define_inv (bind, inv) thy = 
-    let val inv_parsed_term = Syntax.parse_term (Proof_Context.init_global thy) inv
+    let val ctxt = Proof_Context.init_global thy
+        val inv_parsed_term = Syntax.parse_term ctxt inv |> DOF_core.elaborate_term' ctxt
         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)

Isabelle_DOF/thys/RegExpInterface.thy

@@ -52,12 +52,6 @@ definition rep1 :: "'a rexp \<Rightarrow> 'a rexp" ("\<lbrace>(_)\<rbrace>\<^sup
 definition opt :: "'a rexp \<Rightarrow> 'a rexp" ("\<lbrakk>(_)\<rbrakk>")
    where "\<lbrakk>A\<rbrakk> \<equiv>  A || One"
 
-find_consts name:"RegExpI*"
-
-ML\<open>
-val t = Sign.syn_of \<^theory>
-\<close>
-print_syntax
 value "Star (Conc(Alt (Atom(CHR ''a'')) (Atom(CHR ''b''))) (Atom(CHR ''c'')))"
 text\<open>or better equivalently:\<close>
 value "\<lbrace>(\<lfloor>CHR ''a''\<rfloor> || \<lfloor>CHR ''b''\<rfloor>) ~~ \<lfloor>CHR ''c''\<rfloor>\<rbrace>\<^sup>*"