From 7f8ea1c115ea5d29fbf087139cad59bb144a8d5f Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 20 Jul 2019 15:15:04 +0100 Subject: [PATCH] Removed outdated BAC2017 example. --- examples/math_exam/BAC2017/BAC2017.thy | 117 ------------------ examples/math_exam/BAC2017/ROOT | 11 -- examples/math_exam/BAC2017/document/build | 46 ------- .../math_exam/BAC2017/document/isadof.cfg | 2 - .../math_exam/BAC2017/document/preamble.tex | 47 ------- 5 files changed, 223 deletions(-) delete mode 100644 examples/math_exam/BAC2017/BAC2017.thy delete mode 100644 examples/math_exam/BAC2017/ROOT delete mode 100755 examples/math_exam/BAC2017/document/build delete mode 100644 examples/math_exam/BAC2017/document/isadof.cfg delete mode 100644 examples/math_exam/BAC2017/document/preamble.tex diff --git a/examples/math_exam/BAC2017/BAC2017.thy b/examples/math_exam/BAC2017/BAC2017.thy deleted file mode 100644 index 5177fb7..0000000 --- a/examples/math_exam/BAC2017/BAC2017.thy +++ /dev/null @@ -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..+\] par : - @{term "h(x) = x * exponent (-x)"} -*} - -definition h :: "real \ real" - where "h x \ 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 +\. *} - -text*[a1::Answer_Formal_Step] {* Fill in term and justification*} - -lemma q1 : "(h \ (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..+\] et - dresser son tableau de variation *} - -text*[a2::Answer_Formal_Step] -{* Fill in term and justification*} - -definition h' :: "real \ real" - where "h' x \ (1 - x) * exp (- x)" - -lemma q2_a : "DERIV h x :> h' x" -proof - - have * : "DERIV (exp \ 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 \ x \ x \ y \ y \ 1 \ h x \ h y" - sorry - -lemma q2_c : "1 \ x \ x \ y \ h x \ 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..+\], 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 diff --git a/examples/math_exam/BAC2017/ROOT b/examples/math_exam/BAC2017/ROOT deleted file mode 100644 index cf67197..0000000 --- a/examples/math_exam/BAC2017/ROOT +++ /dev/null @@ -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" diff --git a/examples/math_exam/BAC2017/document/build b/examples/math_exam/BAC2017/document/build deleted file mode 100755 index c4a05ab..0000000 --- a/examples/math_exam/BAC2017/document/build +++ /dev/null @@ -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 diff --git a/examples/math_exam/BAC2017/document/isadof.cfg b/examples/math_exam/BAC2017/document/isadof.cfg deleted file mode 100644 index f13f22b..0000000 --- a/examples/math_exam/BAC2017/document/isadof.cfg +++ /dev/null @@ -1,2 +0,0 @@ -Template: scrartcl -Ontology: mathex diff --git a/examples/math_exam/BAC2017/document/preamble.tex b/examples/math_exam/BAC2017/document/preamble.tex deleted file mode 100644 index 5e5251d..0000000 --- a/examples/math_exam/BAC2017/document/preamble.tex +++ /dev/null @@ -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{} -\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 -}