From 862bb782ac9e39aa9ddac639f4fddf034a245db0 Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 12 Jun 2018 20:20:44 +0200 Subject: [PATCH] Reworked MathExam. --- examples/math_exam/MathExam/MathExam.thy | 33 ++++++++++++++---- .../document/figures/Polynomialdeg5.png | Bin 0 -> 5030 bytes ontologies/mathex_onto.thy | 11 ++++++ 3 files changed, 38 insertions(+), 6 deletions(-) create mode 100644 examples/math_exam/MathExam/document/figures/Polynomialdeg5.png diff --git a/examples/math_exam/MathExam/MathExam.thy b/examples/math_exam/MathExam/MathExam.thy index 00a51df..0a0f26c 100644 --- a/examples/math_exam/MathExam/MathExam.thy +++ b/examples/math_exam/MathExam/MathExam.thy @@ -20,14 +20,13 @@ subsection*[header::Header,examSubject= "[algebra]", examTitle="''Exam number 1 \end{itemize} *} +(* should be in DOF-core *) (* -text*[fig1::figure, width = "Some(textwidth 80)", - "file"="@{file ''../../../figures/Dogfood-Intro.png''}"] - {* Ouroboros I : This paper from inside ... *} +figure*[figure::figure, spawn_columns=False,relative_width="''80''", + src="''figures/Polynomialdeg5.png''"] \ A Polynome. \ *) - -subsubsection*[exo1 :: Exercise, Exercise.content="[q1::Task,q2::Task]"] -{* +subsubsection*[exo1 :: Exercise, Exercise.content="[q1::Task,q2::Task]"]\Exercise 1\ +text{* Here are the first four lines of a number pattern. \begin{itemize} \item Line 1 : @{term "1*6 + 2*4 = 2*7"} @@ -37,6 +36,26 @@ Here are the first four lines of a number pattern. \end{itemize} *} +declare [[show_sorts=false]] +subsubsection*[exo2 :: Exercise, Exercise.content="[q1::Task,q2::Task]"]\Exercise 2\ + +text{* Find the roots of the polynome: +@{term "(x^3) - 6 * x^2 + 5 * x + 12"}. +Note the intermediate steps in the following fields and submit the solution. *} +text{* +\begin{Form}[action={http://your-web-server.com/path/receiveform.cgi}] +\begin{tabular}{l} + From @{term "(x^3) - 6 * x^2 + 5 * x + 12"} \\\\ + \TextField{have 1} \\\\ + \TextField{have 2} \\\\ + \TextField{have 3} \\\\ + \TextField{finally show} \\\\ + \CheckBox[width=1em]{Has the polynomial as many solutions as its degree ? } \\\\ + \Submit{Submit}\\ +\end{tabular} +\end{Form} +*} + (* a bit brutal, as long as lemma* does not yet work *) (*<*) lemma check_polynome : @@ -65,6 +84,8 @@ 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"} *} +subsubsection*[exo3 :: Exercise, Exercise.content="[q1::Task,q2::Task]"]\Exercise 3\ + 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 diff --git a/examples/math_exam/MathExam/document/figures/Polynomialdeg5.png b/examples/math_exam/MathExam/document/figures/Polynomialdeg5.png new file mode 100644 index 0000000000000000000000000000000000000000..5eeec1260e68ac2c8145c95b7be4028967804911 GIT binary patch literal 5030 zcmYLN2{=@5`<^jlWKUxmV^_9pV;f8MLd0a35K;CR`_7=qPWG`Y2{BQYAz3CnMMHkX z&x~ZtGG)#BpT6(<_&Y|I7i)U zEHu-RWpD#<{&y?ytj?xJ=mHH*^yp?G40Mw8xxU1Q008u+;SC+j(BjRK zDEp}?z5%TZ@I{b{z;L3FgS>Puwh#|7Nn5r=iaot-_oEJrGb^+R%o^#m_i0ph9Mez@ zP_3)72(TTgo?FK1yrc8VsuY&*9RB{pUqCySac<%4kbyzizHKGs6Fz_YSZl}sQ)~VK z;ZN!IAI-qJxV;S5`+Kr;KFW)Wi|G9gTY&bRJ1__nto*Br!{OWtCYeD{%J}H3 zkW?Ew|dUIqLBLNT;l zfsvFRIzR(^d8ulEexn||C+;UC0m!S#6uHlRk&k(_l=*RDT}v`Om|aW;6w9gDID>f% zcG|p~jNF{1oeP(wY<1L1yU+kN$?e)fN|^;0UQ~k?{(Qu>ME&^D|USRXH35{5a}&=(9~jG`pB5n9k&xpNHla$ zN-Bv#s&W^oafFg-cQ&1ASedubM~ps1QPPlD)cMKnXd3TtkYaU@QWImR#X$3-fG4Zc zZNL2mmGep%Nu`oJ>zGC(#qBa?9(bRr9oRh_f|Z(Ts)^JTlF z`b9<2HT709NNt;*u+HvpjyEI&x=0UAKn`}d4_Ly)!Z=}6Eqm)wT_9e_FjpPYy(g z4CN!#XjyIKF{3FiejcUTnmj?Q8vO)W{N7iu9IY;*)b%T&O{uWEvNoAE#KGSm6S2+F zv3$_Q`r6Lm;QGrIGczC)cjYVtGi}H+lY@_*BU;RaMn7$Fol=@S|0&KZpH*w)%q7Gv zayuetZgf}ukR^ogY)62!)iGv!O^%Hcin(ksYFjqJRg^|MEh7+Pyj5naek?WrqoDN3 zJPQ-g%UOmo@X8*|pFcSu56+<>Z5<$bqaZ8-aa1uxXuTIFDGqRUZoijK+n8tYdEYG+Jx-60=lFYcgO>C9jYmHnJ z**S2Yw6Lo)3GwL!hit$ua*4U&s>>k3TUTr@|MM#pQz`6;jR?b{GIX=WfZDD0!zYnO zgl9UI?3BUF-Lla-K><4YxJ75FdYo7W`6LWW7;lwDlWE3r0tjFJ(=Xhb_RTfR&kYyl z%Zcjn4quDAf*fBhqNmNd{3KHc=%l(e~j(Bwr%<>I8?>+Y)|$zGi$Z*T+1D) z?w!xX5_~!463y_)k8hHUoc7mvwf;TJCwN;ofTK^nNQ-)ZB2s$41M_5Pt#SHe4G!oB z54tDD$HRc@nL^$Bo4d%cg{UPT$Ytym8IamM*|Hc7p#1qvOvR5CtwqUsaODtdbWdGjofpT;}c#@{Vt0yuZnqv1Vr4JWDEn{VW4O4WCnu0)FqWnYo6{yE@wH zWA!#BL?wp*@OQq%mqUVpxhyKi@HXAn`|LTQQ?DzrziRS2nx9oq!pfEA^olqJx@;_p=XX~&xEnxT2mZsM1nhzGFAL>l2R`$^hKyEE;|J2Ywcy=mXr7F zA9;nEst)&~-3n{=&ziS-5}dTNKR(nJ>q+B&KFa_P*dvy$^E3wHF@*{egN^Q4VaKW5 zASqkjEl))G-}y};p-R5EczSqCQJQfRP6qRoP;q!+o_>h*+o8eoU@kgVY*+q_3U6d@ z^WrGC21*69rPuX`+2LJKMGbxEu9?%uop!HbLB*WtUk@IDgGG%VNk5!&kK>QK7Ijyk zhgkq6Hpm)XKKo3P${F=5W=|4-EP4gdI{)&#v*og)zZlQ~Tz!3f$x~h)bMPd^g9<#>TF0`@z1R z&#v{^`2L2O^3z`D3JLvKtZ%JZ6`(wxBx4WIPq%#3*F0Lr3WHE)y*&40R`~v^bJQ_r z@TL+{F}u)k>vhA#w{&sosamjMC+W5Iqc1*p*)GwXY=ulV+6IfBk_qh3w9pvrbgk>I z`>^uqrmvOVm!RR{cf-t9vTXq?yX?GxIe*3~)uG6YqZKU)VSJ3%CXTVNFz3mo3xz5+ zgg7q(KEN{Vwd6=XQEN6&dU-o&14bG1HUF8I1RYzzNzO$oQ2JzPt_8npdExcu)(phK zVc1podW~oJ7@YKxerI3eYUS(mG@d?IdA7c$hwROYOjCJ>C|hn0xK~_w&)SAL63Si?8Rq^oH&au(G*eqt8Uqb>ebT4G|PskTE= z2b1DXMA4&1M_V220M(e%@OP=ahBLw`T*P=kL{P60>Lv8v+a;29PQKS3gl<)^4Ihw; z6-?#veUYG9S#-2I%&cr`J^B-uO$mJQE~h=y1Kg2gd=R!F*Ev7@#heBEZt)~+J#rK* z3KcV7GYxL>yfs^0savORq+La-ty@DujSsM;gDx3ab~Ts#`lQ-8lT-Fy?Kz)Z7I_k< z$IM(S?U6Qpt5EdxxUS^|$2!=?ywa^onWzL|g>1Fo>QYuMGU>P=Qf`ihy8;pOFYpPs z#f*&ZpzFnDr$2SMwhztWClM_TsAdtHSFgsms4u>0-b9Lvj|E9+1uke#<=N{HsIt_2 ztA?BFN)4CxM_iz^HDl}OPcMb@{BPnk3(Z?=Zw;hOKKUhZ*FnVT@eGt9A#rWQ&O5A z&G+a)`*}YcS&;_WYTNUY2s$3FXP=@F^h$97c#KYbj`!G2Vc|HVU>5$I4%|!CoUucx zHV#Q^r-QBevu*cQ3%bRTk9~bT(ue*fWn~#N(VuL+GMIUgPJ{&J-suvJ2;}dbohLXi zNFobg?_ys{)G_7ck7h@1?+3?6G@|WMU6Gt~Rk!j;+WowoL(nOj(QH z+uLgk{UscEdJ?3p9t9^~Ppn-2t#%K`g{p?$i_N}6?O@YBK3F~1*7ZqLLg6e?UhDSowWvtUt8N=wu0e7S(Tn9{eH zeIh9-$;Qv0eiq%rS7hUm*0KKc*GZ-j08lrTZ1!Bg!ba9_+Aw1vet6g@^&&6*BYq#4 zNa(tWp&@+&6L*{@O`RCEAl(SQMisd?N7z z*@5&}klzbmM*uv!E0Ql4TUzSl{jFu}ys%E|9Do1yz4_k*tE=vWwZNmUEvuy;Ke&JW z`lUOq$V3<%9+q!vYI=<05fJdD0`v~VwLo}QR@Q&ee>y^NjcBs&LQFRqk$RuNMEJf& zaiLBNR1~IfW;P-abR0dDVQy_@CVTy*+eHq&=j|*4$Qay9QO_~~CbMC~Y*C@RAAfd^ zeKkS{ERX8=_V|iYpIx9C)jqBSbee1PgDLwIQ-Z2*m!%I5-X#CT_E5+Kzt0*6ft!iu z7O^PdOx+KT){+kk?0;yk@1HWrG4%))f4XT>m4zy?ujD>=-}3kpxow#|kBZlNZCxvh zNI5E1QfPk%AqIcPw6DO&#KV%sLt&kOt5zQ@YCrFP#nT%3`MhFXT%;ofBW zi;o%eK*0tQ@k|e)rX9LQ3~xekw{uCFS=3CzstcNp^|x?f7HmO!6a6a(p{opS2ltGS zrOKbr_cV_#6v+3T2VD`gLEAIBsSS&k2j?d8)0|Q0Ky$qfi84_>XQ2^{`In0Rh!#t*;x7m;kcm5&)2bAUk> z&XAO0$+P;b?CS?T0G(1&ZEf2(c_KCmDp5FJW{I1#cUrgfLl&m0_sncY#<(>6ND{+H z+qECOWoGV96riD}cYY+#h8N>C5HD-$eArJAKdDmwdR_n@00V)!RY1XuQFMbKFcb=!47zF}q|WWQ10W$kMn3Osrpk;00Uq-%8zNO0>5^HR~IH@Aimm&nk+hKv~1pSe*= zYU`vS+^pq9chnf=%avecwVC}#afv&jukvb|zDz!X3A;0x#8V_w=m)520U{G! kU^V~Cjn0H>8J*Mlc)tmRTkGmkZ8m_R9_mJeu2bCq0c`ez2LJ#7 literal 0 HcmV?d00001 diff --git a/ontologies/mathex_onto.thy b/ontologies/mathex_onto.thy index c862542..00629de 100644 --- a/ontologies/mathex_onto.thy +++ b/ontologies/mathex_onto.thy @@ -26,6 +26,8 @@ doc_class Author = affiliation :: "string" email :: "string" + + datatype Subject = algebra | geometry | statistical | analysis @@ -45,6 +47,15 @@ doc_class Header = doc_class Exam_item = concerns :: "ContentClass set" +(* should go into something more fundamental on texts. *) +datatype placement = h | t | b | ht | hb +doc_class figure = Exam_item + + relative_width :: "string" (* percent of textwidth *) + src :: "string" + placement :: placement + spawn_columns :: bool <= True + + type_synonym SubQuestion = string doc_class Answer_Formal_Step = Exam_item +