forked from Isabelle_DOF/Isabelle_DOF
Typechecked , corrected and pimped up the MathExam scenario
with solution sections and an adapted role model. Added explanations
This commit is contained in:
parent
d9dd46f1ac
commit
4d3371705c
|
@ -4,26 +4,29 @@ begin
|
||||||
|
|
||||||
open_monitor*[exam::MathExam]
|
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*}
|
{*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.*}
|
{* Please follow directions carefully and show all your work.*}
|
||||||
|
|
||||||
section*[exo1 :: Exercise, content="[q1,q2,q3]", mark="15"]{* Exercise 1.*}
|
section*[exo1 :: Exercise, Exercise.content="[q1::Question,q2,q3]", mark="15::int"]{* Exercise 1.*}
|
||||||
text*[q1::Question, level="twoStars", mark="5"]
|
text*[q1::Question, level="twoStars", Question.mark="5::int"]
|
||||||
{*
|
{*
|
||||||
Give an example of each of the following :
|
Give an example of each of the following :
|
||||||
a - a rational number which is not integer.
|
\begin{itemize}
|
||||||
b - a real number which is not rational.
|
\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"}
|
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"} *}
|
{* True or false : @{term "0/8 = 0"} *}
|
||||||
|
|
||||||
close_monitor*[exam]
|
close_monitor*[exam]
|
||||||
|
|
|
@ -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.
|
where the author of the exam is not expected to be physically present.
|
||||||
*}
|
*}
|
||||||
|
|
||||||
datatype ContentClass =
|
|
||||||
examiner | validator | student
|
|
||||||
|
|
||||||
datatype Grade =
|
datatype Grade =
|
||||||
A1 | A2 | A3
|
A1 | A2 | A3
|
||||||
|
|
||||||
doc_class Header =
|
doc_class Header =
|
||||||
examTitle :: string
|
examTitle :: string
|
||||||
examGrade :: Grade
|
|
||||||
examSubject :: Subject
|
examSubject :: Subject
|
||||||
|
|
||||||
doc_class Question =
|
datatype ContentClass =
|
||||||
|
examiner -- \<open>the 'author' of the exam\<close>
|
||||||
|
| validator -- \<open>the 'proof-reader' of the exam\<close>
|
||||||
|
| student -- \<open>the victim ;-) ... \<close>
|
||||||
|
|
||||||
|
doc_class Exam_item =
|
||||||
|
concerns :: "ContentClass set"
|
||||||
|
|
||||||
|
datatype Question_Type =
|
||||||
|
formal | informal
|
||||||
|
|
||||||
|
doc_class Question = Exam_item +
|
||||||
level :: Level
|
level :: Level
|
||||||
mark :: integer
|
type :: Question_Type
|
||||||
|
concerns :: "ContentClass set" <= "{examiner,validator,student}"
|
||||||
|
mark :: int
|
||||||
|
|
||||||
doc_class Exercise=
|
doc_class Exercise = Exam_item +
|
||||||
content :: "(Question) list"
|
content :: "(Question) list"
|
||||||
mark :: integer
|
concerns :: "ContentClass set" <= "{examiner,validator,student}"
|
||||||
|
mark :: int
|
||||||
|
|
||||||
doc_class Solution =
|
text{* In many institutions, it makes sense to have a rigorous process of validation
|
||||||
content :: "(Question) list"
|
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 \<open>intern\<close>}, 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=
|
doc_class MathExam=
|
||||||
content :: "(Header + Author + Exercise) list"
|
content :: "(Header + Author + Exercise) list"
|
||||||
|
global_grade :: Grade
|
||||||
where "((Author)+ ~
|
where "((Author)+ ~
|
||||||
Header ~
|
Header ~
|
||||||
(Exercise)+ )"
|
(Exercise ~ Solution)+ )"
|
||||||
|
|
||||||
end
|
end
|
Reference in New Issue