diff --git a/examples/simple/MathExam.thy b/examples/simple/MathExam.thy index 558e674..8317d78 100644 --- a/examples/simple/MathExam.thy +++ b/examples/simple/MathExam.thy @@ -1,29 +1,32 @@ theory MathExam imports "../../ontologies/mathex_onto" begin - + open_monitor*[exam::MathExam] -text*[idir::Author, affiliation="''CentraleSupelec''", email="''idir.aitsadoune@centralesupelec.fr''"] +text*[idir::Author, affiliation="''CentraleSupelec''", + email="''idir.aitsadoune@centralesupelec.fr''"] {*Idir AIT SADOUNE*} -text*[header::Header,examGrade="A1", examSubject= "algebra", examTitle="Exam number 1"] +text*[header::Header,examSubject= "algebra", examTitle="''Exam number 1''"] {* Please follow directions carefully and show all your work.*} -section*[exo1 :: Exercise, content="[q1,q2,q3]", mark="15"]{* Exercise 1.*} -text*[q1::Question, level="twoStars", mark="5"] +section*[exo1 :: Exercise, Exercise.content="[q1::Question,q2,q3]", mark="15::int"]{* Exercise 1.*} +text*[q1::Question, level="twoStars", Question.mark="5::int"] {* Give an example of each of the following : -a - a rational number which is not integer. -b - a real number which is not rational. +\begin{itemize} +\item - a rational number which is not integer. +\item - a real number which is not rational. +\end{itemize} *} -text*[q2::Question, level="oneStar", mark="5"] +text*[q2::Question, level="oneStar", Question.mark="5::int"] {* Write in interval notation : @{term "-3 < x"} and @{term "x < 5"} *} -text*[q3::Question, level="oneStar", mark="5"] +text*[q3::Question, level="oneStar", Question.mark="5::int"] {* True or false : @{term "0/8 = 0"} *} close_monitor*[exam] diff --git a/ontologies/mathex_onto.thy b/ontologies/mathex_onto.thy index c4775f2..6d36a01 100644 --- a/ontologies/mathex_onto.thy +++ b/ontologies/mathex_onto.thy @@ -24,32 +24,57 @@ where for organizational reasons the execution of an exam takes place in facilit where the author of the exam is not expected to be physically present. *} -datatype ContentClass = - examiner | validator | student datatype Grade = A1 | A2 | A3 doc_class Header = examTitle :: string - examGrade :: Grade examSubject :: Subject -doc_class Question = - level :: Level - mark :: integer +datatype ContentClass = + examiner -- \the 'author' of the exam\ + | validator -- \the 'proof-reader' of the exam\ + | student -- \the victim ;-) ... \ -doc_class Exercise= - content :: "(Question) list" - mark :: integer +doc_class Exam_item = + concerns :: "ContentClass set" -doc_class Solution = - content :: "(Question) list" +datatype Question_Type = + formal | informal +doc_class Question = Exam_item + + level :: Level + type :: Question_Type + concerns :: "ContentClass set" <= "{examiner,validator,student}" + mark :: int + +doc_class Exercise = Exam_item + + content :: "(Question) list" + concerns :: "ContentClass set" <= "{examiner,validator,student}" + mark :: int + +text{* 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 examiner} validates a +question by a sample proof validated by Isabelle. In our scenario this sample proofs +are completely @{emph \intern\}, i.e. not exposed to the students but just additional +material for the internal review process of the exam.*} + +doc_class Validation = + tests :: "term list" <="[]" + proofs :: "thm list" <="[]" + +doc_class Solution = Exam_item + + content :: "Question list" + valids :: "Validation list" + concerns :: "ContentClass set" <= "{examiner,validator}" doc_class MathExam= content :: "(Header + Author + Exercise) list" + global_grade :: Grade where "((Author)+ ~ Header ~ - (Exercise)+ )" + (Exercise ~ Solution)+ )" + end \ No newline at end of file