Remove outdated and obsoleted ontologies.
This commit is contained in:
parent
a0993b6eea
commit
fee83a2a29
|
@ -181,7 +181,6 @@ Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
|
||||||
-o ONTOLOGY (default: scholarly_paper)
|
-o ONTOLOGY (default: scholarly_paper)
|
||||||
Available ontologies:
|
Available ontologies:
|
||||||
* CENELEC_50128
|
* CENELEC_50128
|
||||||
* math_exam
|
|
||||||
* scholarly_paper
|
* scholarly_paper
|
||||||
* technical_report
|
* technical_report
|
||||||
-t TEMPLATE (default: scrartcl)
|
-t TEMPLATE (default: scrartcl)
|
||||||
|
|
2
src/ROOT
2
src/ROOT
|
@ -7,8 +7,6 @@ session "Isabelle_DOF" = "Functional-Automata" +
|
||||||
"ontologies"
|
"ontologies"
|
||||||
"ontologies/CENELEC_50128"
|
"ontologies/CENELEC_50128"
|
||||||
"ontologies/Conceptual"
|
"ontologies/Conceptual"
|
||||||
"ontologies/math_exam"
|
|
||||||
"ontologies/math_paper"
|
|
||||||
"ontologies/scholarly_paper"
|
"ontologies/scholarly_paper"
|
||||||
"ontologies/small_math"
|
"ontologies/small_math"
|
||||||
"ontologies/technical_report"
|
"ontologies/technical_report"
|
||||||
|
|
|
@ -1,102 +0,0 @@
|
||||||
%% Copyright (C) 2018 The University of Sheffield
|
|
||||||
%% 2018 The University of Paris-Saclay
|
|
||||||
%%
|
|
||||||
%% License:
|
|
||||||
%% This program can be redistributed and/or modified under the terms
|
|
||||||
%% of the LaTeX Project Public License Distributed from CTAN
|
|
||||||
%% archives in directory macros/latex/base/lppl.txt; either
|
|
||||||
%% version 1.3c of the License, or (at your option) any later version.
|
|
||||||
%% OR
|
|
||||||
%% The 2-clause BSD-style license.
|
|
||||||
%%
|
|
||||||
%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
|
|
||||||
|
|
||||||
\NeedsTeXFormat{LaTeX2e}\relax
|
|
||||||
\ProvidesPackage{DOF-math_exam}
|
|
||||||
[<isadofltxversion>%
|
|
||||||
Document-Type Support Framework for math classes.]
|
|
||||||
|
|
||||||
\RequirePackage{DOF-COL}
|
|
||||||
\usepackage{sfmath}
|
|
||||||
\usepackage{amsmath}
|
|
||||||
\usepackage{lastpage}
|
|
||||||
\usepackage{scrlayer-scrpage}
|
|
||||||
\usepackage{exercise}
|
|
||||||
|
|
||||||
\cfoot{\small\textnormal{Page \thepage\ of \pageref{LastPage}}}
|
|
||||||
|
|
||||||
\def\dof@author{}%
|
|
||||||
\def\dof@affiliation{}%
|
|
||||||
|
|
||||||
\AtBeginDocument{%
|
|
||||||
\author{\dof@author}
|
|
||||||
% \institute{\dof@affiliation}
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
\def\leftadd#1#2{\expandafter\leftaddaux\expandafter{#1}{#2}{#1}}
|
|
||||||
\def\leftaddaux#1#2#3{\gdef#3{#1#2}}
|
|
||||||
|
|
||||||
\newcommand{\addauthor}[1]{%
|
|
||||||
\ifthenelse{\equal{\dof@author}{}}{%
|
|
||||||
\gdef\dof@author{#1}%
|
|
||||||
}{%
|
|
||||||
\leftadd\dof@author{\protect\and #1}%
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofSectionAuthor[label=,type=,affiliation=,email=][1]{%
|
|
||||||
\immediate\write\@auxout{\noexpand\addauthor{#1}}%
|
|
||||||
}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofTextHeader[label=,type=,examSubject=,date=,timeAllowed=][1]{%
|
|
||||||
\immediate\write\@auxout{\noexpand\title{#1}}%
|
|
||||||
}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofSectionHeader[label=,type=,examSubject=,date=,timeAllowed=][1]{%
|
|
||||||
\immediate\write\@auxout{\noexpand\title{#1}}%
|
|
||||||
}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofSubsectionHeader[label=,type=,examSubject=,date=,timeAllowed=][1]{%
|
|
||||||
\immediate\write\@auxout{\noexpand\title{#1}}%
|
|
||||||
}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofTextAnswerFormalStep[label=,type=,justification=,term=][1]{%
|
|
||||||
#1
|
|
||||||
}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofTextAnswerYesNo[label=,type=,step_label=,yes_no=][1]{%
|
|
||||||
#1
|
|
||||||
}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofTextExamitem[label=,type=,concerns=][1]{%
|
|
||||||
#1
|
|
||||||
}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofTextTask[label=,type=,level=,type=,subitems=concerns=,mark=][1]{%
|
|
||||||
#1
|
|
||||||
}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofSubsubsectionExercise[label=,type=,Exercise.content=,concerns=,][1]{%
|
|
||||||
\begin{Exercise}
|
|
||||||
#1
|
|
||||||
\end{Exercise}
|
|
||||||
}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofSubsubsectionValidation[label=,type=,tests=,proofs=][1]{%
|
|
||||||
#1
|
|
||||||
}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofSubsubsectionSolution[label=,type=,content=,valids=,concerns=][1]{%
|
|
||||||
\begin{Answer}
|
|
||||||
#1
|
|
||||||
\end{Answer}
|
|
||||||
}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofSubsubsectionMathExam[label=,type=,content=,global_grade=][1]{%
|
|
||||||
#1
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
\newkeycommand\isaDofOpenMonitorMathExam[label=,type=]{}
|
|
||||||
\newkeycommand\isaDofCloseMonitorMathExam[label=,type=]{}
|
|
|
@ -1,195 +0,0 @@
|
||||||
(*************************************************************************
|
|
||||||
* Copyright (C)
|
|
||||||
* 2019 The University of Exeter
|
|
||||||
* 2018-2019 The University of Paris-Saclay
|
|
||||||
* 2018 The University of Sheffield
|
|
||||||
*
|
|
||||||
* License:
|
|
||||||
* This program can be redistributed and/or modified under the terms
|
|
||||||
* of the 2-clause BSD-style license.
|
|
||||||
*
|
|
||||||
* SPDX-License-Identifier: BSD-2-Clause
|
|
||||||
*************************************************************************)
|
|
||||||
|
|
||||||
theory Nmath_exam
|
|
||||||
imports "../../DOF/Isa_COL"
|
|
||||||
begin
|
|
||||||
|
|
||||||
text\<open>In our scenario, content has four different types of addressees:
|
|
||||||
\<^item> the @{emph \<open>setter\<close>}, i.e. the author of the exam,
|
|
||||||
\<^item> the @{emph \<open>student\<close>}, i.e. the addressee of the exam,
|
|
||||||
\<^item> the @{emph \<open>checker\<close>}, i.e. a person that checks the exam for
|
|
||||||
\<^item> the @{emph \<open>external\_examiner\<close>}, i.e. a person that checks the exam for
|
|
||||||
feasibility and non-ambiguity.
|
|
||||||
|
|
||||||
Note that the latter quality assurance mechanism is used in many universities,
|
|
||||||
where for organizational reasons the execution of an exam takes place in facilities
|
|
||||||
where the author of the exam is not expected to be physically present.
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
|
|
||||||
datatype content_class = setter | checker | external_examiner | student
|
|
||||||
|
|
||||||
text\<open>Tasks, Answers and Solutions are grouped into the \<^emph>\<open>categories\<close>
|
|
||||||
\<^enum> \<open>main\<close> and
|
|
||||||
\<^enum> \<open>sub\<close>. \<close>
|
|
||||||
|
|
||||||
datatype category = main | sub
|
|
||||||
|
|
||||||
doc_class author =
|
|
||||||
affiliation :: "string"
|
|
||||||
roles :: "content_class set"
|
|
||||||
email :: "string"
|
|
||||||
|
|
||||||
doc_class context_description =
|
|
||||||
label :: string
|
|
||||||
|
|
||||||
doc_class exam_item =
|
|
||||||
level :: "int option"
|
|
||||||
concerns :: "content_class set"
|
|
||||||
visible_for :: "content_class set"
|
|
||||||
|
|
||||||
doc_class header = exam_item +
|
|
||||||
date :: string
|
|
||||||
authors :: "author list"
|
|
||||||
timeAllowed :: int (* minutes *)
|
|
||||||
|
|
||||||
|
|
||||||
datatype prog_lang = python | C | java | Haskell | SML
|
|
||||||
|
|
||||||
|
|
||||||
doc_class marking = exam_item +
|
|
||||||
marks :: int
|
|
||||||
|
|
||||||
doc_class answer_element = exam_item +
|
|
||||||
cat :: category
|
|
||||||
(* justification :: string
|
|
||||||
"term" :: "string" *)
|
|
||||||
|
|
||||||
|
|
||||||
doc_class text_answer = answer_element +
|
|
||||||
"term" :: "string"
|
|
||||||
|
|
||||||
doc_class program_text = answer_element +
|
|
||||||
prog_lang :: prog_lang
|
|
||||||
pre_filled :: "string" <= "\<open>This is a text with \<alpha>, \<beta>, \<gamma>\<close>"
|
|
||||||
|
|
||||||
doc_class formula_text = answer_element +
|
|
||||||
"term" :: "string"
|
|
||||||
|
|
||||||
doc_class checkbox = exam_item +
|
|
||||||
"value" :: "bool option"
|
|
||||||
|
|
||||||
doc_class checkboxes = answer_element +
|
|
||||||
marks :: int
|
|
||||||
accepts "\<lbrace>checkbox\<rbrace>\<^sup>+"
|
|
||||||
|
|
||||||
doc_class radiobutton = exam_item +
|
|
||||||
"value" :: "bool option"
|
|
||||||
"term" :: "string"
|
|
||||||
|
|
||||||
doc_class radiobuttons = answer_element +
|
|
||||||
"term" :: "string"
|
|
||||||
accepts "\<lbrace>radiobutton\<rbrace>\<^sup>+ "
|
|
||||||
|
|
||||||
datatype opn = eq | equiv | refines | refined_by
|
|
||||||
|
|
||||||
doc_class equational_derivation = answer_element +
|
|
||||||
eq_deriv :: "(opn option \<times> term option) list"
|
|
||||||
|
|
||||||
(* these two could be refined substantially *)
|
|
||||||
doc_class proof_derivation = answer_element +
|
|
||||||
"term" :: "term list"
|
|
||||||
|
|
||||||
doc_class answer = exam_item +
|
|
||||||
cat :: category
|
|
||||||
accepts "\<lbrace>answer_element\<rbrace>\<^sup>+ "
|
|
||||||
|
|
||||||
|
|
||||||
datatype task_type = formal | informal | mixed
|
|
||||||
|
|
||||||
doc_class task = exam_item +
|
|
||||||
cat :: category
|
|
||||||
local_grade :: marking
|
|
||||||
type :: task_type
|
|
||||||
concerns :: "content_class set" <= "{setter,student,checker,external_examiner}"
|
|
||||||
mark :: int
|
|
||||||
|
|
||||||
doc_class validation =
|
|
||||||
tests :: "term list" <="[]"
|
|
||||||
proofs :: "thm list" <="[]"
|
|
||||||
|
|
||||||
doc_class solution = exam_item +
|
|
||||||
cat :: category
|
|
||||||
motivation :: string
|
|
||||||
valids :: "validation list"
|
|
||||||
objectives :: string
|
|
||||||
responds_to :: answer
|
|
||||||
concerns :: "content_class set" <= "{setter,checker,external_examiner}"
|
|
||||||
accepts "\<lbrace>answer_element\<rbrace>\<^sup>+"
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
doc_class exercise = exam_item +
|
|
||||||
concerns :: "content_class set" <= "{setter,student,checker,external_examiner}"
|
|
||||||
accepts "header ~~ \<lbrace>author\<rbrace>\<^sup>+ ~~ context_description ~~ \<lbrace>task ~~ answer\<rbrace>\<^sup>+ ~~ \<lbrace>solution\<rbrace>\<^sup>+" (* PSud style*)
|
|
||||||
(* accepts "\<lbrace>task ~~ answer ~~ \<lbrace>solution\<rbrace>\<^sup>+ \<rbrace>\<^sup>+ " (*Exeter style *) *)
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
ML\<open>fun check_exercise_inv_1 oid {is_monitor} ctxt =
|
|
||||||
let fun get_attr oid attr = AttributeAccess.compute_attr_access ctxt attr oid @{here} @{here}
|
|
||||||
(* val term = AttributeAccess.compute_attr_access ctxt "trace" oid @{here} @{here} *)
|
|
||||||
fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
|
|
||||||
val string_pair_list = map conv (HOLogic.dest_list (get_attr oid "trace" ))
|
|
||||||
val cid_list = map fst string_pair_list
|
|
||||||
val ctxt' = Proof_Context.init_global(Context.theory_of ctxt)
|
|
||||||
fun is_task x = DOF_core.is_subclass ctxt' x "Nmath_exam.task"
|
|
||||||
fun is_answer x = DOF_core.is_subclass ctxt' x "Nmath_exam.answer"
|
|
||||||
val task_answer_part = (filter (fn x => is_task x orelse is_answer x) cid_list)
|
|
||||||
val _ = case get_attr (hd task_answer_part) "cat" of
|
|
||||||
@{term "main"} => ()
|
|
||||||
| _ => error("class exercise invariant violation: must start with main category. ")
|
|
||||||
fun check_match [] = ()
|
|
||||||
|check_match (task_id::answer_id::S) =
|
|
||||||
(if get_attr task_id "cat" = get_attr answer_id "cat"
|
|
||||||
then check_match S
|
|
||||||
else error("class exercise invariant violation: \
|
|
||||||
\ task and answer category does not match. "))
|
|
||||||
val _ = check_match task_answer_part
|
|
||||||
in true end
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
setup\<open>DOF_core.update_class_invariant
|
|
||||||
"Nmath_exam.exercise"
|
|
||||||
check_exercise_inv_1\<close>
|
|
||||||
|
|
||||||
|
|
||||||
doc_class math_exam =
|
|
||||||
global_grade :: int
|
|
||||||
accepts "header ~~ \<lbrace>author\<rbrace>\<^sup>+ ~~ context_description ~~ \<lbrace>exercise\<rbrace>\<^sup>+ "
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
text\<open> Invariants (not yet implemented):
|
|
||||||
|
|
||||||
\<^enum> the task list must start with a \<open>main\<close> category.
|
|
||||||
|
|
||||||
\<^enum> \<open>solutions\<close> must structurally match to answer blocks, i.e. coincide in
|
|
||||||
category and corresponding answer elements
|
|
||||||
|
|
||||||
\<^enum> one-to-n relation between answer_elements and solutions
|
|
||||||
|
|
||||||
\<^enum> invariants over markings and grades : sub-task must sum up to task grades, exo
|
|
||||||
marks to the global grade.
|
|
||||||
|
|
||||||
\<^enum> distribution constraints: subtask should have no more than 25 % of overall grade.
|
|
||||||
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
(*>*)
|
|
||||||
end
|
|
||||||
(*<*)
|
|
|
@ -1,114 +0,0 @@
|
||||||
(*************************************************************************
|
|
||||||
* Copyright (C)
|
|
||||||
* 2019 The University of Exeter
|
|
||||||
* 2018-2019 The University of Paris-Saclay
|
|
||||||
* 2018 The University of Sheffield
|
|
||||||
*
|
|
||||||
* License:
|
|
||||||
* This program can be redistributed and/or modified under the terms
|
|
||||||
* of the 2-clause BSD-style license.
|
|
||||||
*
|
|
||||||
* SPDX-License-Identifier: BSD-2-Clause
|
|
||||||
*************************************************************************)
|
|
||||||
|
|
||||||
theory math_exam
|
|
||||||
imports "../../DOF/Isa_COL"
|
|
||||||
begin
|
|
||||||
|
|
||||||
(*<<*)
|
|
||||||
text\<open>In our scenario, content has four different types of addressees:
|
|
||||||
\<^item> the @{emph \<open>setter\<close>}, i.e. the author of the exam,
|
|
||||||
\<^item> the @{emph \<open>student\<close>}, i.e. the addressee of the exam,
|
|
||||||
\<^item> the @{emph \<open>checker\<close>}, i.e. a person that checks the exam for
|
|
||||||
\<^item> the @{emph \<open>external\_examiner\<close>}, i.e. a person that checks the exam for
|
|
||||||
feasibility and non-ambiguity.
|
|
||||||
|
|
||||||
Note that the latter quality assurance mechanism is used in many universities,
|
|
||||||
where for organizational reasons the execution of an exam takes place in facilities
|
|
||||||
where the author of the exam is not expected to be physically present.
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
|
|
||||||
datatype ContentClass =
|
|
||||||
setter (* \<open>the 'author' of the exam\<close> *)
|
|
||||||
| checker (* \<open>the 'proof-reader' of the exam\<close> *)
|
|
||||||
| externalExaminer (* \<open>an external 'proof-reader' of the exam\<close> *)
|
|
||||||
| student (* \<open>the victim ;-) ... \<close> *)
|
|
||||||
|
|
||||||
|
|
||||||
doc_class Author =
|
|
||||||
affiliation :: "string"
|
|
||||||
email :: "string"
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
datatype Subject =
|
|
||||||
algebra | geometry | statistical | analysis
|
|
||||||
|
|
||||||
datatype Level =
|
|
||||||
oneStar | twoStars | threeStars
|
|
||||||
|
|
||||||
|
|
||||||
datatype Grade =
|
|
||||||
A1 | A2 | A3
|
|
||||||
|
|
||||||
|
|
||||||
doc_class Exam_item =
|
|
||||||
level :: "int option"
|
|
||||||
concerns :: "ContentClass set"
|
|
||||||
|
|
||||||
doc_class Header = Exam_item +
|
|
||||||
examSubject :: "(Subject) list"
|
|
||||||
date :: string
|
|
||||||
timeAllowed :: int (* minutes *)
|
|
||||||
|
|
||||||
|
|
||||||
type_synonym SubQuestion = string
|
|
||||||
|
|
||||||
doc_class Answer_Formal_Step = Exam_item +
|
|
||||||
justification :: string
|
|
||||||
"term" :: "string"
|
|
||||||
|
|
||||||
doc_class Answer_YesNo = Exam_item +
|
|
||||||
step_label :: string
|
|
||||||
yes_no :: bool (* \<open>for checkboxes\<close> *)
|
|
||||||
|
|
||||||
datatype Question_Type =
|
|
||||||
formal | informal | mixed
|
|
||||||
|
|
||||||
doc_class Task = Exam_item +
|
|
||||||
local_grade :: Level
|
|
||||||
type :: Question_Type
|
|
||||||
subitems :: "(SubQuestion * (Answer_Formal_Step list + Answer_YesNo)list) list"
|
|
||||||
concerns :: "ContentClass set" <= "{setter,student,checker,externalExaminer}"
|
|
||||||
mark :: int
|
|
||||||
|
|
||||||
|
|
||||||
doc_class Exercise = Exam_item +
|
|
||||||
content :: "(Task) list"
|
|
||||||
concerns :: "ContentClass set" <= "{setter,student,checker,externalExaminer}"
|
|
||||||
|
|
||||||
|
|
||||||
text\<open>In many institutions, it makes sense to have a rigorous process of validation
|
|
||||||
for exam subjects : is the initial question correct ? Is a proof in the sense of the
|
|
||||||
question possible ? We model the possibility that the @{term setter} validates a
|
|
||||||
question by a sample proof validated by Isabelle. In our scenario this sample proofs
|
|
||||||
are completely @{emph \<open>intern\<close>}, i.e. not exposed to the students but just additional
|
|
||||||
material for the internal review process of the exam.\<close>
|
|
||||||
|
|
||||||
doc_class Validation =
|
|
||||||
tests :: "term list" <="[]"
|
|
||||||
proofs :: "thm list" <="[]"
|
|
||||||
|
|
||||||
doc_class Solution = Exam_item +
|
|
||||||
content :: "Exercise list"
|
|
||||||
valids :: "Validation list"
|
|
||||||
concerns :: "ContentClass set" <= "{setter,checker,externalExaminer}"
|
|
||||||
|
|
||||||
doc_class MathExam =
|
|
||||||
content :: "(Header + Author + Exercise) list"
|
|
||||||
global_grade :: Grade
|
|
||||||
accepts "\<lbrace>Author\<rbrace>\<^sup>+ ~~ Header ~~ \<lbrace>Exercise ~~ Solution\<rbrace>\<^sup>+ "
|
|
||||||
|
|
||||||
(*>>*)
|
|
||||||
end
|
|
|
@ -1,116 +0,0 @@
|
||||||
(*************************************************************************
|
|
||||||
* Copyright (C)
|
|
||||||
* 2019 The University of Exeter
|
|
||||||
* 2018-2019 The University of Paris-Saclay
|
|
||||||
* 2018 The University of Sheffield
|
|
||||||
*
|
|
||||||
* License:
|
|
||||||
* This program can be redistributed and/or modified under the terms
|
|
||||||
* of the 2-clause BSD-style license.
|
|
||||||
*
|
|
||||||
* SPDX-License-Identifier: BSD-2-Clause
|
|
||||||
*************************************************************************)
|
|
||||||
|
|
||||||
chapter \<open>A Math Paper Ontology (obsolete vs. scholarly_paper)\<close>
|
|
||||||
|
|
||||||
text\<open> Offering support for common Isabelle Elements like definitions, lemma- and theorem
|
|
||||||
statements, proofs, etc. Isabelle is a lot of things, but it is an interactive theorem
|
|
||||||
proving environment after all ! So this ontology provides:
|
|
||||||
\<^item> declarations for textual descriptions of definitions, lemmas, theorems, assertions, ...
|
|
||||||
and the usual means for typed referencing on them,
|
|
||||||
\<^item> monitors allowing for filtering content; this means (typed) brackets that can be
|
|
||||||
put around formal content that is more or less relevant for different types of users,
|
|
||||||
\fixme{find nicer formulation}
|
|
||||||
\<^item> LaTeX support. \<close>
|
|
||||||
|
|
||||||
|
|
||||||
theory math_paper
|
|
||||||
imports "../../DOF/Isa_DOF"
|
|
||||||
|
|
||||||
begin
|
|
||||||
|
|
||||||
section\<open>Some attempt to model standardized links to Standard Isabelle Formal Content\<close>
|
|
||||||
|
|
||||||
text\<open> These document classes are intended to present a number of key-elements
|
|
||||||
in mathematical papers and generate LaTeX in the style of, for example:
|
|
||||||
\begin{verbatim}
|
|
||||||
\begin{definition}[Dilating function]
|
|
||||||
A dilating function for a run \(\rho'\) is a function \(\mathbb{N} \longrightarrow \mathbb{N}\)
|
|
||||||
that satisfies:
|
|
||||||
\begin{enumerate}
|
|
||||||
\item \(f\) is strictly monotonic, so that the order of the instants in not changed in \(\rho'\);
|
|
||||||
\item \(\forall n.~f(n) \geq n\), so that instants are inserted into \(\rho\);
|
|
||||||
\item \(f(0) = 0\), so that no instant is inserted before the first one;
|
|
||||||
\item \(\forall n.~(\not\exists n_0.~f(n_0) = n) \Longrightarrow
|
|
||||||
(\forall c.~\neg\mathsf{ticks}(\rho'_{n}(c))\),
|
|
||||||
there is no tick in stuttering instants;
|
|
||||||
\item \(\forall n.~(\not\exists n_0.~f(n_0) = n+1) \Longrightarrow
|
|
||||||
(\forall c.~\mathsf{time}(\rho'_{n+1}(c)) = \mathsf{time}(\rho'_{n}(c)))\),
|
|
||||||
time does not elapse during stuttering instants;
|
|
||||||
\end{enumerate}
|
|
||||||
\end{definition}
|
|
||||||
\end{verbatim}
|
|
||||||
which are intended to \<^emph>\<open>complement\<close> Isabelle's formal content elements such as definitions,
|
|
||||||
lemmas and formal proofs.
|
|
||||||
|
|
||||||
We are aware that there is a certain tension between the interest to have more formal checking in
|
|
||||||
a definition as the above one and the interest in a notationally more liberal presentation that hides
|
|
||||||
technical details imposed by strict formality (even at the price that a chosen notation may be
|
|
||||||
intuitive, but an abstraction that is, fi donc, technically incorrect).
|
|
||||||
|
|
||||||
We argue that it should be up to the user to decide in each individual case how to draw this line ... \<close>
|
|
||||||
|
|
||||||
doc_class formal_stmt =
|
|
||||||
property :: "term list"
|
|
||||||
|
|
||||||
datatype relevance = key | vital | working | auxilliary | alternative
|
|
||||||
|
|
||||||
doc_class "definition" = formal_stmt +
|
|
||||||
relevance :: "relevance option"
|
|
||||||
property :: "term list" <= "[]"
|
|
||||||
|
|
||||||
text\<open>Which gives rise to a presentation like:\<close>
|
|
||||||
(*<*)
|
|
||||||
type_notation nat ("\<nat>")
|
|
||||||
(*>*)
|
|
||||||
text*[dil_fun :: "definition"]\<open>A dilating function for a run @{term "\<rho>"} is a function
|
|
||||||
@{typ "\<nat> \<Rightarrow> \<nat>"} that satisfies:
|
|
||||||
\<^enum> @{term "f"} is strictly monotonic ...
|
|
||||||
\<^enum> ...
|
|
||||||
\<^enum> ...
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
|
|
||||||
doc_class assertion = formal_stmt +
|
|
||||||
relevance :: "relevance option"
|
|
||||||
properties :: "term list" <= "[]"
|
|
||||||
|
|
||||||
doc_class "lemma" = formal_stmt +
|
|
||||||
relevance :: "relevance"
|
|
||||||
properties :: "term list" <= "[]"
|
|
||||||
|
|
||||||
doc_class "theorem" = formal_stmt +
|
|
||||||
relevance :: "relevance"
|
|
||||||
properties :: "term list" <= "[]"
|
|
||||||
|
|
||||||
|
|
||||||
doc_class "corrollary" = formal_stmt +
|
|
||||||
relevance :: "relevance"
|
|
||||||
properties :: "term list" <= "[]"
|
|
||||||
|
|
||||||
text\<open>This monitor is used to group formal content in a way to classify the
|
|
||||||
relevance. On the presentation level, this gives the possibility to adapt or omit
|
|
||||||
Isabelle/Isar lemma and theorem commands according to their relevance level.
|
|
||||||
By using inheritance, the document class @{text \<open>formal_content\<close>} can also be used
|
|
||||||
to introduce organisational information (for example: developer or tester or validator )
|
|
||||||
as a systematic means to produce documents oriented to specific needs of user (sub-)groups.\<close>
|
|
||||||
|
|
||||||
doc_class formal_content =
|
|
||||||
relevance :: "relevance"
|
|
||||||
accepts "\<lbrace>definition || assertion || lemma || theorem || corrollary \<rbrace>\<^sup>+"
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
end
|
|
|
@ -16,8 +16,6 @@ theory
|
||||||
imports
|
imports
|
||||||
"CENELEC_50128/CENELEC_50128"
|
"CENELEC_50128/CENELEC_50128"
|
||||||
"Conceptual/Conceptual"
|
"Conceptual/Conceptual"
|
||||||
"math_exam/math_exam"
|
|
||||||
"math_paper/math_paper"
|
|
||||||
"scholarly_paper/scholarly_paper"
|
"scholarly_paper/scholarly_paper"
|
||||||
"small_math/small_math"
|
"small_math/small_math"
|
||||||
"technical_report/technical_report"
|
"technical_report/technical_report"
|
||||||
|
|
|
@ -15,8 +15,7 @@ theory
|
||||||
AssnsLemmaThmEtc
|
AssnsLemmaThmEtc
|
||||||
imports
|
imports
|
||||||
"Isabelle_DOF.Conceptual"
|
"Isabelle_DOF.Conceptual"
|
||||||
"Isabelle_DOF.math_paper"
|
"Isabelle_DOF.scholarly_paper"
|
||||||
"Isabelle_DOF.scholarly_paper" (* for assert notation *)
|
|
||||||
begin
|
begin
|
||||||
|
|
||||||
section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
|
section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
|
||||||
|
|
Loading…
Reference in New Issue