no message
This commit is contained in:
parent
7de68e7564
commit
b030859ddf
|
|
@ -1,75 +0,0 @@
|
|||
theory MathExam
|
||||
imports "../../ontologies/mathex_onto"
|
||||
Real
|
||||
begin
|
||||
|
||||
open_monitor*[exam::MathExam]
|
||||
|
||||
section*[idir::Author, affiliation="''CentraleSupelec''",
|
||||
email="''idir.aitsadoune@centralesupelec.fr''"]
|
||||
{*Idir AIT SADOUNE*}
|
||||
|
||||
subsection*[header::Header,examSubject= "[algebra]", examTitle="''Exam number 1''",
|
||||
date="''02-05-2018''", timeAllowed="90::int"]
|
||||
{*
|
||||
\begin{itemize}
|
||||
\item Use black ink or black ball-point pen.
|
||||
\item Draw diagrams in pencil.
|
||||
\item Answer all questions in the spaces provided.
|
||||
\end{itemize}
|
||||
*}
|
||||
|
||||
(*
|
||||
text*[fig1::figure, width = "Some(textwidth 80)",
|
||||
"file"="@{file ''../../../figures/Dogfood-Intro.png''}"]
|
||||
{* Ouroboros I : This paper from inside ... *}
|
||||
*)
|
||||
|
||||
subsubsection*[exo1 :: Exercise, Exercise.content="[q1::Task,q2::Task]"]
|
||||
{*
|
||||
Here are the first four lines of a number pattern.
|
||||
\begin{itemize}
|
||||
\item Line 1 : @{term "1*6 + 2*4 = 2*7"}
|
||||
\item Line 2 : @{term "2*7 + 2*5 = 3*8"}
|
||||
\item Line 3 : @{term "3*8 + 2*6 = 4*9"}
|
||||
\item Line 4 : @{term "4*9 + 2*7 = 5*10"}
|
||||
\end{itemize}
|
||||
*}
|
||||
|
||||
(* a bit brutal, as long as lemma* does not yet work *)
|
||||
(*<*)
|
||||
lemma check_polynome :
|
||||
fixes x::real
|
||||
shows "(x^3) - 6 * x^2 + 5 * x + 12 = (x-4) * (x+1) * (x - 3)"
|
||||
|
||||
proof -
|
||||
have * : "(x-4) * (x+1) * (x - 3) = (x-4) * ((x+1) * (x-3))"
|
||||
by simp
|
||||
have ** : "... = (x-4) * (x^2 - 2*x - 3)"
|
||||
apply(auto simp: right_diff_distrib add.commute semiring_normalization_rules(1)[symmetric])
|
||||
by (simp add: semiring_normalization_rules(29))
|
||||
have *** : "... = x^3 - 6 * x^2 + 5 * x + 12"
|
||||
apply(auto simp: right_diff_distrib left_diff_distrib add.commute semiring_normalization_rules(1)[symmetric])
|
||||
by (simp add: numeral_3_eq_3 semiring_normalization_rules(29))
|
||||
show ?thesis
|
||||
by(simp only: * ** ***)
|
||||
qed
|
||||
(*>*)
|
||||
|
||||
text*[a1::Answer_Formal_Step]{* First Step: Fill in term and justification *}
|
||||
text*[a2::Answer_Formal_Step]{* Next Step: Fill in term and justification *}
|
||||
text*[a3::Answer_Formal_Step]{* Next Step: Fill in term and justification *}
|
||||
text*[a4::Answer_Formal_Step]{* Next Step: Fill in term and justification *}
|
||||
|
||||
text*[q1::Task, level="oneStar", mark="1::int", type="formal"]
|
||||
{* Complete Line 10 : @{term "10*x + 2*y = 11*16"} *}
|
||||
|
||||
text*[q2::Task, level="threeStars", mark="3::int", type="formal"]
|
||||
{*
|
||||
Prove that @{term "n*(n+5) + 2*(n+3) "} is always the product of two numbers with a difference of 5.
|
||||
*}
|
||||
|
||||
|
||||
close_monitor*[exam]
|
||||
|
||||
end
|
||||
|
|
@ -9,7 +9,7 @@ section*[idir::Author, affiliation="''CentraleSupelec''",
|
|||
email="''idir.aitsadoune@centralesupelec.fr''"]
|
||||
{*Idir AIT SADOUNE*}
|
||||
|
||||
subsection*[header::Header,examSubject= "algebra", examTitle="''Exam number 1''",
|
||||
subsection*[header::Header,examSubject= "[algebra]", examTitle="''Exam number 1''",
|
||||
date="''02-05-2018''", timeAllowed="90::int"]
|
||||
{*
|
||||
\begin{itemize}
|
||||
|
|
|
|||
|
|
@ -1,91 +0,0 @@
|
|||
theory mathex_onto
|
||||
imports "../Isa_DOF"
|
||||
begin
|
||||
|
||||
doc_class Author =
|
||||
affiliation :: "string"
|
||||
email :: "string"
|
||||
|
||||
datatype Subject =
|
||||
algebra | geometry | statistical
|
||||
|
||||
datatype Level =
|
||||
oneStar | twoStars | threeStars
|
||||
|
||||
text{* In our scenario, content has three different types of addressees:
|
||||
\<^item> the @{emph \<open>examiner\<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>validator\<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.
|
||||
*}
|
||||
|
||||
|
||||
datatype Grade =
|
||||
A1 | A2 | A3
|
||||
|
||||
doc_class Header =
|
||||
examTitle :: string
|
||||
examSubject :: "(Subject) list"
|
||||
date :: string
|
||||
timeAllowed :: int -- minutes
|
||||
|
||||
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"
|
||||
|
||||
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 +
|
||||
level :: Level
|
||||
type :: Question_Type
|
||||
subitems :: "(SubQuestion * (Answer_Formal_Step list + Answer_YesNo)list) list"
|
||||
concerns :: "ContentClass set" <= "{examiner,validator,student}"
|
||||
mark :: int
|
||||
|
||||
|
||||
doc_class Exercise = Exam_item +
|
||||
content :: "(Task) list"
|
||||
concerns :: "ContentClass set" <= "{examiner,validator,student}"
|
||||
|
||||
|
||||
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 \<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 :: "Exercise list"
|
||||
valids :: "Validation list"
|
||||
concerns :: "ContentClass set" <= "{examiner,validator}"
|
||||
|
||||
doc_class MathExam=
|
||||
content :: "(Header + Author + Exercise) list"
|
||||
global_grade :: Grade
|
||||
where "\<lbrace>Author\<rbrace>\<^sup>+ ~~ Header ~~ \<lbrace>Exercise ~~ Solution\<rbrace>\<^sup>+ "
|
||||
|
||||
end
|
||||
|
|
@ -29,7 +29,7 @@ datatype Grade =
|
|||
|
||||
doc_class Header =
|
||||
examTitle :: string
|
||||
examSubject :: Subject
|
||||
examSubject :: "(Subject) list"
|
||||
date :: string
|
||||
timeAllowed :: int -- minutes
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue