From 7de68e7564f2f85ed3796acaf98ebd9d98f6dfea Mon Sep 17 00:00:00 2001 From: Idir AIT SADOUNE Date: Mon, 4 Jun 2018 13:44:08 +0200 Subject: [PATCH 1/2] no message --- examples/math_exam/#MathExam.thy# | 75 +++++++++++++++++++++++++ examples/math_exam/BAC2017.thy | 45 +++++++++++++++ ontologies/#mathex_onto.thy# | 91 +++++++++++++++++++++++++++++++ 3 files changed, 211 insertions(+) create mode 100644 examples/math_exam/#MathExam.thy# create mode 100644 examples/math_exam/BAC2017.thy create mode 100644 ontologies/#mathex_onto.thy# diff --git a/examples/math_exam/#MathExam.thy# b/examples/math_exam/#MathExam.thy# new file mode 100644 index 00000000..c4e7cb9c --- /dev/null +++ b/examples/math_exam/#MathExam.thy# @@ -0,0 +1,75 @@ +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 diff --git a/examples/math_exam/BAC2017.thy b/examples/math_exam/BAC2017.thy new file mode 100644 index 00000000..9ba4a9ae --- /dev/null +++ b/examples/math_exam/BAC2017.thy @@ -0,0 +1,45 @@ +theory BAC2017 + imports "../../ontologies/mathex_onto" + Real +begin + +open_monitor*[exam::MathExam] + +section*[idir::Author,affiliation="''CentraleSupelec''", +email="''idir.aitsadoune@centralesupelec.fr''"] +{*Idir AIT SADOUNE*} + +section*[header::Header,examSubject= "[algebra,geometry]", + examTitle="''BACCALAUREAT GENERAL MATHEMATIQUES''", +date="''21-06-2017''", +timeAllowed="240::int"] +{* +\begin{itemize} +\item Les calculatrices électroniques de poche sont autorisées, conformément à la réglementation en vigueur. +\item Le sujet est composé de 4 exercices indépendants. +\item Le candidat doit traiter tous les exercices. +\item Le candidat est invité à faire figurer sur la copie toute trace de recherche, même incomplète ou non fructueuse, qu’il aura développée. +\item Il est rappelé que la qualité de la rédaction, la clarté et la précision des raisonnements entreront pour une part importante dans l’appréciation des copies. +\end{itemize} +*} + +section*[exo1 :: Exercise,Exercise.concerns= "{examiner,validator,student}", +Exercise.content="[q1::Task]"] +{* +On considère la fonction h définie sur l’intervalle [0..+\] par : @{term "h(x) = x * e^(-x)"} +*} + + +subsection*[q1::Task, Task.concerns= "{examiner,validator,student}", +subitems="[q11]", +level="oneStar", mark="1::int", type="formal"] +{* Déterminer la limite de la fonction h en +\. *} + +text*[q11::Answer_Formal_Step] +{* First Step: Fill in term and justifi*} + + + +close_monitor*[exam] + +end diff --git a/ontologies/#mathex_onto.thy# b/ontologies/#mathex_onto.thy# new file mode 100644 index 00000000..09846ca2 --- /dev/null +++ b/ontologies/#mathex_onto.thy# @@ -0,0 +1,91 @@ +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 \examiner\}, i.e. the author of the exam, +\<^item> the @{emph \student\}, i.e. the addressee of the exam, +\<^item> the @{emph \validator\}, 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 -- \the 'author' of the exam\ + | validator -- \the 'proof-reader' of the exam\ + | student -- \the victim ;-) ... \ + +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 -- \for checkboxes\ + +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 \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 :: "Exercise list" + valids :: "Validation list" + concerns :: "ContentClass set" <= "{examiner,validator}" + +doc_class MathExam= + content :: "(Header + Author + Exercise) list" + global_grade :: Grade + where "\Author\\<^sup>+ ~~ Header ~~ \Exercise ~~ Solution\\<^sup>+ " + +end \ No newline at end of file From b030859ddf7bf2b85712d40e3136511ca22a4b42 Mon Sep 17 00:00:00 2001 From: Idir AIT SADOUNE Date: Mon, 4 Jun 2018 14:46:11 +0200 Subject: [PATCH 2/2] no message --- examples/math_exam/#MathExam.thy# | 75 ------------------------- examples/math_exam/MathExam.thy | 2 +- ontologies/#mathex_onto.thy# | 91 ------------------------------- ontologies/mathex_onto.thy | 2 +- 4 files changed, 2 insertions(+), 168 deletions(-) delete mode 100644 examples/math_exam/#MathExam.thy# delete mode 100644 ontologies/#mathex_onto.thy# diff --git a/examples/math_exam/#MathExam.thy# b/examples/math_exam/#MathExam.thy# deleted file mode 100644 index c4e7cb9c..00000000 --- a/examples/math_exam/#MathExam.thy# +++ /dev/null @@ -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 diff --git a/examples/math_exam/MathExam.thy b/examples/math_exam/MathExam.thy index 1f9bbaf2..c4e7cb9c 100644 --- a/examples/math_exam/MathExam.thy +++ b/examples/math_exam/MathExam.thy @@ -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} diff --git a/ontologies/#mathex_onto.thy# b/ontologies/#mathex_onto.thy# deleted file mode 100644 index 09846ca2..00000000 --- a/ontologies/#mathex_onto.thy# +++ /dev/null @@ -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 \examiner\}, i.e. the author of the exam, -\<^item> the @{emph \student\}, i.e. the addressee of the exam, -\<^item> the @{emph \validator\}, 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 -- \the 'author' of the exam\ - | validator -- \the 'proof-reader' of the exam\ - | student -- \the victim ;-) ... \ - -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 -- \for checkboxes\ - -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 \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 :: "Exercise list" - valids :: "Validation list" - concerns :: "ContentClass set" <= "{examiner,validator}" - -doc_class MathExam= - content :: "(Header + Author + Exercise) list" - global_grade :: Grade - where "\Author\\<^sup>+ ~~ Header ~~ \Exercise ~~ Solution\\<^sup>+ " - -end \ No newline at end of file diff --git a/ontologies/mathex_onto.thy b/ontologies/mathex_onto.thy index db35095c..09846ca2 100644 --- a/ontologies/mathex_onto.thy +++ b/ontologies/mathex_onto.thy @@ -29,7 +29,7 @@ datatype Grade = doc_class Header = examTitle :: string - examSubject :: Subject + examSubject :: "(Subject) list" date :: string timeAllowed :: int -- minutes