Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF
This commit is contained in:
commit
5a4896cf06
|
|
@ -1,15 +1,19 @@
|
|||
theory BAC2017
|
||||
imports "../../ontologies/mathex_onto"
|
||||
Real
|
||||
Deriv Transcendental
|
||||
begin
|
||||
|
||||
open_monitor*[exam::MathExam]
|
||||
|
||||
section*[idir::Author,affiliation="''CentraleSupelec''",
|
||||
section*[idir::Author,affiliation="''LRI, CentraleSupelec''",
|
||||
email="''idir.aitsadoune@centralesupelec.fr''"]
|
||||
{*Idir AIT SADOUNE*}
|
||||
|
||||
section*[header::Header,examSubject= "[algebra,geometry]",
|
||||
section*[keller::Author,affiliation="''LRI, Univ. Paris-Sud''",
|
||||
email="''Chantal.Keller@lri.fr''"]
|
||||
{*Chantal KELLER*}
|
||||
|
||||
subsection*[header::Header,examSubject= "[algebra,geometry]",
|
||||
examTitle="''BACCALAUREAT GENERAL MATHEMATIQUES''",
|
||||
date="''21-06-2017''",
|
||||
timeAllowed="240::int"]
|
||||
|
|
@ -23,21 +27,72 @@ timeAllowed="240::int"]
|
|||
\end{itemize}
|
||||
*}
|
||||
|
||||
section*[exo1 :: Exercise,Exercise.concerns= "{examiner,validator,student}",
|
||||
Exercise.content="[q1::Task]"]
|
||||
subsubsection*[exo1 :: Exercise,Exercise.concerns= "{examiner,validator,student}",
|
||||
Exercise.content="[q1::Task,q2,q3a]"]
|
||||
{*
|
||||
On considère la fonction h définie sur l’intervalle [0..+\<infinity>] par : @{term "h(x) = x * e^(-x)"}
|
||||
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)"
|
||||
|
||||
|
||||
subsection*[q1::Task, Task.concerns= "{examiner,validator,student}",
|
||||
subitems="[q11]",
|
||||
subsubsection*[q1::Task, Task.concerns= "{examiner,validator,student}",
|
||||
level="oneStar", mark="1::int", type="formal"]
|
||||
{* Déterminer la limite de la fonction h en +\<infinity>. *}
|
||||
{* Déterminer la limite de la fonction @{term h} en +\<infinity>. *}
|
||||
|
||||
text*[q11::Answer_Formal_Step]
|
||||
{* First Step: Fill in term and justifi*}
|
||||
text*[a1::Answer_Formal_Step]
|
||||
{* Fill in term and justification*}
|
||||
|
||||
lemma q1 : "(h \<longlongrightarrow> (0::real)) at_top"
|
||||
sorry
|
||||
|
||||
|
||||
subsubsection*[q2::Task, Task.concerns= "{examiner,validator,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))"
|
||||
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))"
|
||||
by (simp add: * ** has_derivative_mult comp_def)
|
||||
show ?thesis
|
||||
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
|
||||
|
||||
|
||||
subsubsection*[q3a::Task, Task.concerns= "{examiner,validator,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)} *}
|
||||
|
||||
lemma q3a : "h x = (exp (- x)) - (h' x)"
|
||||
by (simp add : h_def h'_def left_diff_distrib)
|
||||
|
||||
|
||||
text*[a3a::Answer_Formal_Step]
|
||||
{* Fill in term and justification*}
|
||||
|
||||
|
||||
close_monitor*[exam]
|
||||
|
|
|
|||
|
|
@ -50,17 +50,21 @@ Thm.concl_of;
|
|||
|
||||
ML{*
|
||||
val X = (@{term scholarly_paper.example.comment})
|
||||
val Y = Type.legacy_freeze @{docitem_value \<open>bgrnd\<close>}
|
||||
val Y = Type.legacy_freeze @{docitem_value \<open>bgrnd\<close>};
|
||||
Syntax.string_of_term
|
||||
*}
|
||||
ML{*
|
||||
fun calculate_attr_access ctxt f term =
|
||||
let val term = Type.legacy_freeze term;
|
||||
val ty = type_of term
|
||||
(* term assumed to be ground type, (f term) not necessarily *)
|
||||
let val _ = writeln("XXX"^(Syntax.string_of_term ctxt term))
|
||||
val [subterm'] = Type_Infer_Context.infer_types ctxt [f term]
|
||||
val ty = type_of (subterm')
|
||||
val _ = writeln("YYY"^(Syntax.string_of_term ctxt subterm'))
|
||||
val term' = (Const(@{const_name "HOL.eq"}, ty --> ty --> HOLogic.boolT)
|
||||
$ (Type.legacy_freeze(f term))
|
||||
$ subterm'
|
||||
$ Free("_XXXXXXX", ty))
|
||||
val term'' = (HOLogic.mk_Trueprop(term'))
|
||||
val thm = simplify @{context} (Thm.assume(Thm.cterm_of ctxt term''));
|
||||
val _ = writeln("ZZZ"^(Syntax.string_of_term ctxt term'))
|
||||
val thm = simplify ctxt (Thm.assume(Thm.cterm_of ctxt (HOLogic.mk_Trueprop term')));
|
||||
val Const(@{const_name "HOL.eq"},_) $ lhs $ _ = HOLogic.dest_Trueprop (Thm.concl_of thm)
|
||||
in lhs end
|
||||
|
||||
|
|
@ -69,6 +73,9 @@ val H = fn X => @{term scholarly_paper.example.comment} $ X
|
|||
|
||||
*}
|
||||
|
||||
ML{*val t = calculate_attr_access @{context} H @{docitem_value \<open>bgrnd\<close>}; *}
|
||||
|
||||
|
||||
term "scholarly_paper.author.affiliation_update"
|
||||
term "scholarly_paper.abstract.keywordlist_update"
|
||||
term "scholarly_paper.introduction.comment_update"
|
||||
|
|
|
|||
Loading…
Reference in New Issue