2018-06-08 09:46:44 +00:00
|
|
|
(*<*)
|
2018-04-17 14:43:08 +00:00
|
|
|
theory MathExam
|
2018-06-08 09:46:44 +00:00
|
|
|
imports "../../../ontologies/mathex_onto"
|
2018-05-29 10:02:13 +00:00
|
|
|
Real
|
2018-04-17 14:43:08 +00:00
|
|
|
begin
|
|
|
|
open_monitor*[exam::MathExam]
|
2018-06-11 17:34:41 +00:00
|
|
|
(*>*)
|
2018-04-17 14:43:08 +00:00
|
|
|
|
2018-05-02 07:40:47 +00:00
|
|
|
section*[idir::Author, affiliation="''CentraleSupelec''",
|
|
|
|
email="''idir.aitsadoune@centralesupelec.fr''"]
|
2018-06-08 15:42:58 +00:00
|
|
|
{*Idir AIT SADOUNE*}
|
2018-04-17 14:43:08 +00:00
|
|
|
|
2018-06-04 12:46:11 +00:00
|
|
|
subsection*[header::Header,examSubject= "[algebra]", examTitle="''Exam number 1''",
|
2018-05-02 07:40:47 +00:00
|
|
|
date="''02-05-2018''", timeAllowed="90::int"]
|
2018-04-30 11:13:53 +00:00
|
|
|
{*
|
|
|
|
\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}
|
|
|
|
*}
|
2018-04-18 07:36:21 +00:00
|
|
|
|
2018-05-29 10:02:13 +00:00
|
|
|
(*
|
|
|
|
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]"]
|
2018-04-30 11:13:53 +00:00
|
|
|
{*
|
|
|
|
Here are the first four lines of a number pattern.
|
2018-04-29 10:42:00 +00:00
|
|
|
\begin{itemize}
|
2018-04-30 11:13:53 +00:00
|
|
|
\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"}
|
2018-04-29 10:42:00 +00:00
|
|
|
\end{itemize}
|
2018-04-17 14:43:08 +00:00
|
|
|
*}
|
|
|
|
|
2018-05-29 12:13:49 +00:00
|
|
|
(* 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)"
|
2018-05-29 12:03:07 +00:00
|
|
|
|
2018-05-29 10:02:13 +00:00
|
|
|
proof -
|
2018-05-29 12:03:07 +00:00
|
|
|
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])
|
2018-05-29 12:13:49 +00:00
|
|
|
by (simp add: numeral_3_eq_3 semiring_normalization_rules(29))
|
2018-05-29 10:02:13 +00:00
|
|
|
show ?thesis
|
2018-05-29 12:03:07 +00:00
|
|
|
by(simp only: * ** ***)
|
2018-05-29 10:02:13 +00:00
|
|
|
qed
|
2018-05-29 12:13:49 +00:00
|
|
|
(*>*)
|
2018-05-29 10:02:13 +00:00
|
|
|
|
2018-05-29 12:03:07 +00:00
|
|
|
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 *}
|
2018-05-29 10:02:13 +00:00
|
|
|
|
|
|
|
text*[q1::Task, level="oneStar", mark="1::int", type="formal"]
|
2018-05-29 12:03:07 +00:00
|
|
|
{* Complete Line 10 : @{term "10*x + 2*y = 11*16"} *}
|
2018-04-30 11:13:53 +00:00
|
|
|
|
2018-05-29 10:02:13 +00:00
|
|
|
text*[q2::Task, level="threeStars", mark="3::int", type="formal"]
|
2018-04-17 14:43:08 +00:00
|
|
|
{*
|
2018-04-30 11:13:53 +00:00
|
|
|
Prove that @{term "n*(n+5) + 2*(n+3) "} is always the product of two numbers with a difference of 5.
|
2018-04-17 14:43:08 +00:00
|
|
|
*}
|
|
|
|
|
2018-06-11 17:34:41 +00:00
|
|
|
(*<*)
|
2018-04-18 07:36:21 +00:00
|
|
|
close_monitor*[exam]
|
2018-06-11 17:34:41 +00:00
|
|
|
(*>*)
|
2018-04-18 07:36:21 +00:00
|
|
|
end
|