Removed outdated BAC2017 example.
This commit is contained in:
parent
a85bcacd5b
commit
7f8ea1c115
|
@ -1,117 +0,0 @@
|
||||||
theory BAC2017
|
|
||||||
imports "Isabelle_DOF.mathex_onto"
|
|
||||||
Deriv
|
|
||||||
Transcendental
|
|
||||||
begin
|
|
||||||
|
|
||||||
open_monitor*[exam::MathExam]
|
|
||||||
|
|
||||||
(* currently rethinking on "deep ontologies" necessary ... Achim
|
|
||||||
text*[idir::Author,affiliation="''LRI, CentraleSupelec''",
|
|
||||||
email="''idir.aitsadoune@centralesupelec.fr''"]
|
|
||||||
{*Idir AIT SADOUNE*}
|
|
||||||
|
|
||||||
text*[keller::Author,affiliation="''LRI, Univ. Paris-Sud''",
|
|
||||||
email="''Chantal.Keller@lri.fr''"]
|
|
||||||
{*Chantal KELLER*}
|
|
||||||
|
|
||||||
text{* This example is an excerpt from the french baccaleareat 2017.
|
|
||||||
The textual explanations were kept in french.
|
|
||||||
*}
|
|
||||||
*)
|
|
||||||
|
|
||||||
text*[header::Header,examSubject="[analysis,geometry]", date="''21-06-2017''",
|
|
||||||
timeAllowed="240::int"]{* BACCALAUREAT GENERAL MATHEMATIQUES *}
|
|
||||||
text{*
|
|
||||||
\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}
|
|
||||||
*}
|
|
||||||
|
|
||||||
|
|
||||||
text*[exo1 :: Exercise,
|
|
||||||
concerns= "{setter,student,checker,externalExaminer}"]
|
|
||||||
{* On considère la fonction h définie sur l’intervalle [0..+\<infinity>] par :
|
|
||||||
@{term "h(x) = x * exponent (-x)"}
|
|
||||||
*}
|
|
||||||
|
|
||||||
definition h :: "real \<Rightarrow> real"
|
|
||||||
where "h x \<equiv> x * exp (- x)"
|
|
||||||
|
|
||||||
|
|
||||||
text*[q1::Task, concerns= "{setter,student}",
|
|
||||||
level="oneStar", mark="1::int", type="formal"]
|
|
||||||
{* Déterminer la limite de la fonction @{term h} en +\<infinity>. *}
|
|
||||||
|
|
||||||
text*[a1::Answer_Formal_Step] {* Fill in term and justification*}
|
|
||||||
|
|
||||||
lemma q1 : "(h \<longlongrightarrow> (0::real)) at_top" sorry
|
|
||||||
|
|
||||||
text*[v1::Validation, proofs="[@{thm ''HOL.refl''}::thm]"] {* See lemma @{thm q1}. *}
|
|
||||||
|
|
||||||
|
|
||||||
text*[q2::Task, concerns= "{setter,checker,student}",
|
|
||||||
level="oneStar", mark="1::int", type="formal"]
|
|
||||||
{* Étudier les variations de la fonction @{term h} sur l'intervalle [0..+\<infinity>] et
|
|
||||||
dresser son tableau de variation *}
|
|
||||||
|
|
||||||
text*[a2::Answer_Formal_Step]
|
|
||||||
{* Fill in term and justification*}
|
|
||||||
|
|
||||||
definition h' :: "real \<Rightarrow> real"
|
|
||||||
where "h' x \<equiv> (1 - x) * exp (- x)"
|
|
||||||
|
|
||||||
lemma q2_a : "DERIV h x :> h' x"
|
|
||||||
proof -
|
|
||||||
have * : "DERIV (exp \<circ> uminus) x :> - (exp (-x))"
|
|
||||||
sorry (* by (simp add: has_derivative_compose) *)
|
|
||||||
have ** : "DERIV id x :> 1"
|
|
||||||
by (metis DERIV_ident eq_id_iff)
|
|
||||||
have *** : "DERIV h x :> x * (- (exp (- x))) + 1 * (exp (- x))"
|
|
||||||
sorry (* by (simp add: * ** has_derivative_mult comp_def) *)
|
|
||||||
show ?thesis
|
|
||||||
sorry (* by (metis "***" left_diff_distrib mult_minus_right uminus_add_conv_diff) *)
|
|
||||||
qed
|
|
||||||
|
|
||||||
lemma q2_b : "0 \<le> x \<and> x \<le> y \<and> y \<le> 1 \<Longrightarrow> h x \<le> h y"
|
|
||||||
sorry
|
|
||||||
|
|
||||||
lemma q2_c : "1 \<le> x \<and> x \<le> y \<Longrightarrow> h x \<ge> h y"
|
|
||||||
sorry
|
|
||||||
|
|
||||||
text*[v2::Validation, proofs="[@{thm ''BAC2017.q2_b''}, @{thm ''BAC2017.q2_c''}]"]
|
|
||||||
{* See lemmas @{thm q2_b} and @{thm q2_c}. *}
|
|
||||||
|
|
||||||
|
|
||||||
text*[q3a::Task, concerns= "{setter,checker,student}",
|
|
||||||
level="oneStar", mark="1::int", type="formal"]
|
|
||||||
{* Vérifier que pour tout nombre réel x appartenant à l'intervalle [0..+\<infinity>], on a :
|
|
||||||
@{term "h x = (exp (- x)) - (h' x)"}. *}
|
|
||||||
|
|
||||||
text*[a3a::Answer_Formal_Step]
|
|
||||||
{* Fill in term and justification*}
|
|
||||||
|
|
||||||
lemma q3a : "h x = (exp (- x)) - (h' x)"
|
|
||||||
by (simp add : h_def h'_def left_diff_distrib)
|
|
||||||
|
|
||||||
subsubsection*[v3a::Validation, proofs="[@{thm ''BAC2017.q3a''}::thm]"]
|
|
||||||
{* See lemma @{thm q3a}. *}
|
|
||||||
|
|
||||||
|
|
||||||
subsection*[sol1 :: Solution,
|
|
||||||
content="[exo1::Exercise]",
|
|
||||||
valids = "[v1::Validation,v2,v3a]"]
|
|
||||||
{* See validations. *}
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
close_monitor*[exam]
|
|
||||||
|
|
||||||
end
|
|
|
@ -1,11 +0,0 @@
|
||||||
session "BAC2017" = "Isabelle_DOF" +
|
|
||||||
options [document = pdf, document_output = "output",quick_and_dirty=true]
|
|
||||||
theories [document = false]
|
|
||||||
"Deriv"
|
|
||||||
"Transcendental"
|
|
||||||
theories
|
|
||||||
BAC2017
|
|
||||||
document_files
|
|
||||||
"isadof.cfg"
|
|
||||||
"preamble.tex"
|
|
||||||
"build"
|
|
|
@ -1,46 +0,0 @@
|
||||||
#!/usr/bin/env bash
|
|
||||||
# Copyright (c) 2018-2019 The University of Sheffield. All rights reserved.
|
|
||||||
# 2018 The University of Paris-Sud. All rights reserved.
|
|
||||||
#
|
|
||||||
# Redistribution and use in source and binary forms, with or without
|
|
||||||
# modification, are permitted provided that the following conditions
|
|
||||||
# are met:
|
|
||||||
# 1. Redistributions of source code must retain the above copyright
|
|
||||||
# notice, this list of conditions and the following disclaimer.
|
|
||||||
# 2. Redistributions in binary form must reproduce the above copyright
|
|
||||||
# notice, this list of conditions and the following disclaimer in
|
|
||||||
# the documentation and/or other materials provided with the
|
|
||||||
# distribution.
|
|
||||||
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
|
||||||
# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
|
||||||
# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
|
|
||||||
# FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
|
|
||||||
# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
|
|
||||||
# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
|
|
||||||
# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
|
|
||||||
# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
|
||||||
# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
|
|
||||||
# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
|
|
||||||
# ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
|
||||||
# POSSIBILITY OF SUCH DAMAGE.
|
|
||||||
#
|
|
||||||
# SPDX-License-Identifier: BSD-2-Clause
|
|
||||||
|
|
||||||
set -e
|
|
||||||
if [ ! -f $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh ]; then
|
|
||||||
echo ""
|
|
||||||
echo "Error: Isabelle/DOF not installed"
|
|
||||||
echo "====="
|
|
||||||
echo "This is a Isabelle/DOF project. The document preparation requires"
|
|
||||||
echo "the Isabelle/DOF framework. Please obtain the framework by cloning"
|
|
||||||
echo "the Isabelle/DOF git repository, i.e.: "
|
|
||||||
echo " git clone https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF"
|
|
||||||
echo "You can install the framework as follows:"
|
|
||||||
echo " cd Isabelle_DOF/document-generator"
|
|
||||||
echo " ./install"
|
|
||||||
echo ""
|
|
||||||
exit 1
|
|
||||||
fi
|
|
||||||
|
|
||||||
cp $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh .
|
|
||||||
source build_lib.sh
|
|
|
@ -1,2 +0,0 @@
|
||||||
Template: scrartcl
|
|
||||||
Ontology: mathex
|
|
|
@ -1,47 +0,0 @@
|
||||||
%% Copyright (C) 2018 The University of Sheffield
|
|
||||||
%% 2018 The University of Paris-Sud
|
|
||||||
%%
|
|
||||||
%% License:
|
|
||||||
%% This program can be redistributed and/or modified under the terms
|
|
||||||
%% of the LaTeX Project Public License Distributed from CTAN
|
|
||||||
%% archives in directory macros/latex/base/lppl.txt; either
|
|
||||||
%% version 1 of the License, or any later version.
|
|
||||||
%% OR
|
|
||||||
%% The 2-clause BSD-style license.
|
|
||||||
%%
|
|
||||||
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
|
|
||||||
|
|
||||||
%% This is a placeholder for user-specific configuration and packages.
|
|
||||||
|
|
||||||
\title{<TITLE>}
|
|
||||||
\author{<AUTHOR>}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofTextExercise[label=,type=,Exercise.content=,content=,concerns=,][1]{%
|
|
||||||
\begin{Exercise}
|
|
||||||
#1
|
|
||||||
\end{Exercise}
|
|
||||||
}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofTextSolution[Task.concerns=,concerns=,content=,valids=,][1]{%
|
|
||||||
#1
|
|
||||||
}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofSectionSolution[Task.concerns=,concerns=,content=,valids=,][1]{%
|
|
||||||
#1
|
|
||||||
}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofSubsectionSolution[Task.concerns=,concerns=,content=,valids=,][1]{%
|
|
||||||
#1
|
|
||||||
}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofSubsubsectionSolution[Task.concerns=,concerns=,content=,valids=,][1]{%
|
|
||||||
#1
|
|
||||||
}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofTextExercise[Task.concerns=,concerns=,content=,][1]{%
|
|
||||||
#1
|
|
||||||
}
|
|
||||||
|
|
||||||
\newkeycommand\isaDofTextValidation[tests=,proofs=,][1]{%
|
|
||||||
#1
|
|
||||||
}
|
|
Loading…
Reference in New Issue