1.1 --- a/src/Tools/isac/BridgeJEdit/Demo_Example.thy Sun Jun 19 16:10:11 2022 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,235 +0,0 @@
1.4 -(* Title: src/Tools/isac/BridgeJEdit/Demo_Example.thy
1.5 - Author: Walther Neuper, JKU Linz
1.6 - (c) due to copyright terms
1.7 -
1.8 -Runnig example for developing Isabelle/Isac via Isabelle/PIDE in BridgeJEdit
1.9 -*)
1.10 -
1.11 -theory Demo_Example
1.12 - imports Calculation
1.13 -begin
1.14 -
1.15 -section \<open>Boilerplate, the example from Isabelle Workshop 2022\<close>
1.16 -
1.17 -subsection \<open>Specification Phase\<close>
1.18 -text \<open>Goal for Isabelle Workshop 2022: this part of the example should be ready for demonstration:
1.19 - 1. The keyword \<open>Example\<close> inserts the template underneath
1.20 - 2. The template is filled from a (hidden) formalisation with the following items in the
1.21 - 2.1. \<open>Model\<close>:
1.22 - * Constants _ ("_" indicates some kind of place holder for input)
1.23 - * the complete Where-field (the pre-condition), items marked as True | False
1.24 - * Maximum _, AdditionalValues _
1.25 - * Extremum _, SideCondition _
1.26 - 2.2 \<open>References\<close>:
1.27 - * place holders "_" for input
1.28 - * The toggle switch before \<open>Problem_Ref\<close> | \<open>Method_Ref\<close> is set to \<open>Problem_Ref\<close>
1.29 - This might be postponed after the Isabelle Workshop.
1.30 - 3. Input to 2.1 is
1.31 - * type checked and marked as Type-Error
1.32 - * marked as Correct | Superfluous | Incomplete | Unknown (compare Specify/p-model.sml)
1.33 - 4. Input to 2.2 by selection from a list / tree
1.34 - 5. On update of \<open>Problem_Ref\<close> (in the root problem) also \<open>Problem\<close> is updated;
1.35 - The argument of \<open>Problem\<close> comes with the template and is read-only.
1.36 -
1.37 -The specific representation of the Demo_Example demonstrate different situations
1.38 -in educational settings.
1.39 -\<close>
1.40 -
1.41 -subsubsection \<open>Complete Specification\<close>
1.42 -text \<open>
1.43 -* This is one correct result of interactive Specification.
1.44 -* Or this might be presented to the student in one go in order to start Solution immediately
1.45 - (and nevertheless make the Specification explicit)
1.46 -Note that \<open>Problem "univariate_calculus/Optimisation"\<close> and
1.47 -\<open>Problem_Ref: "univariate_calculus/Optimisation"\<close> are redundant; the latter is for input,
1.48 -the former is given initially and needs to be updated in accordance to \<open>Problem_Ref\<close>.
1.49 -\<close>
1.50 -text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
1.51 -
1.52 -Example "Diff_App/No.123 a"
1.53 - Problem "univariate_calculus/Optimisation"
1.54 - Specification:
1.55 - Model:
1.56 - Given: \<open>Constants r = 7\<close>
1.57 - Where: \<open>0 < r\<close>
1.58 - Find: \<open>Maximum A\<close> \<open>AdditionalValues u, v\<close>
1.59 - Relate: \<open>Extremum A = 2 \<sqdot> u \<sqdot> v − u \<up> 2\<close> \<open>SideCondition (u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2\<close>
1.60 - References:
1.61 - Theory_Ref: "Diff_App"
1.62 - \<Otimes> Problem_Ref: "univariate_calculus/Optimisation"
1.63 - \<Odot> Method_Ref: "Optimisation/by_univariate_calculus"
1.64 - Solution:
1.65 -
1.66 - (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>
1.67 -
1.68 -subsubsection \<open>Empty Specification\<close>
1.69 -text \<open>
1.70 - This is presented to the student in one go in order to start interactive Specification.
1.71 -\<close>
1.72 -text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
1.73 -
1.74 -Example "Diff_App/No.123 a"
1.75 - Problem "univariate_calculus/Optimisation"
1.76 - Specification:
1.77 - Model:
1.78 - Given: \<open>Constants _\<close>
1.79 - Where: \<open>0 < r\<close>
1.80 - Find: \<open>Maximum _\<close> \<open>AdditionalValues _\<close>
1.81 - Relate: \<open>Extremum _\<close> \<open>SideCondition _\<close>
1.82 - References:
1.83 - Theory_Ref: "_"
1.84 - \<Otimes> Problem_Ref: "_"
1.85 - \<Odot> Method_Ref: "_"
1.86 - Solution:
1.87 -
1.88 - (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>
1.89 -
1.90 -subsubsection \<open>Plain Example\<close>
1.91 -text \<open>
1.92 - This can occur in between text offering to start an interactive Calculation by using
1.93 - "Diff_App/No.123 a" as a link.
1.94 -\<close>
1.95 -text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
1.96 -
1.97 -Example "Diff_App/No.123 a"
1.98 -
1.99 - (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>
1.100 -
1.101 -subsubsection \<open>Immediate Start of Interactive Solving\<close>
1.102 -text \<open>
1.103 - This
1.104 -\<close>
1.105 -text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
1.106 -
1.107 -Example "Diff_App/No.123 a"
1.108 - Problem "univariate_calculus/Optimisation"
1.109 - Specification:
1.110 - Solution:
1.111 -
1.112 - (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>
1.113 -
1.114 -subsubsection \<open>Show the Model associated to Method_Ref\<close>
1.115 -text \<open>
1.116 - The Model of a method usually comprises more items than the model of a Problem: all these
1.117 - are required to run the program such that it automatically generates a Solution. For instance,
1.118 - compare \<open>problem pbl_bieg\<close> and \<open>method met_biege_2\<close> in \<open>Biegelinie.thy\<close>
1.119 - (TODO: method/program for \<open>Problem "univariate_calculus/Optimisation"\<close>)
1.120 - The Model of a method is usually called a guard.
1.121 -\<close>
1.122 -text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
1.123 -
1.124 -Example "Diff_App/No.123 a"
1.125 - Problem "univariate_calculus/Optimisation"
1.126 - Specification:
1.127 - Model:
1.128 - Given: \<open>Constants r = 7\<close>
1.129 - Where: \<open>0 < r\<close>
1.130 - Find: \<open>Maximum A\<close> \<open>AdditionalValues u, v\<close>
1.131 - Relate: \<open>Extremum A = 2 \<sqdot> u \<sqdot> v − u \<up> 2\<close> \<open>SideCondition (u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2\<close>
1.132 - References:
1.133 - Theory_Ref: "Diff_App"
1.134 - \<Odot> Problem_Ref: "univariate_calculus/Optimisation"
1.135 - \<Otimes> Method_Ref: "Optimisation/by_univariate_calculus"
1.136 - Solution:
1.137 -
1.138 - (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>
1.139 -
1.140 -
1.141 -section \<open>Stepwise Development\<close>
1.142 -
1.143 -subsection \<open>preparing VSCode_Example\<close>
1.144 -ML \<open>
1.145 -(**** preparing VSCode_Example ########################################################### ****)
1.146 -"----------- preparing VSCode_Example ----------------------------------------------------------";
1.147 -"----------- preparing VSCode_Example ----------------------------------------------------------";
1.148 -\<close> text \<open>
1.149 ---- maximum example with Step.specify_do_next --- from test/../step.sml
1.150 -val fmz = [
1.151 -(*Problem model:*)
1.152 - "fixedValues [r=Arbfix]", "maximum A",
1.153 - "valuesFor [a,b::real]",
1.154 - "relations [A=a*(b::real), (a/2) \<up> 2 + (b/2) \<up> 2 = (r::real) \<up> 2]",
1.155 - "relations [A=a*(b::real), (a/2) \<up> 2 + (b/2) \<up> 2 = (r::real) \<up> 2]",
1.156 - "relations [A=a*(b::real), a/2=r*sin alpha, b/2 = (r::real)*cos (alpha::real)]",
1.157 -(*MethodC model:*)
1.158 - "boundVariable a", "boundVariable b", "boundVariable alpha",
1.159 - "interval {x::real. 0 <= x & x <= 2*r}",
1.160 - "interval {x::real. 0 <= x & x <= 2*r}",
1.161 - "interval {x::real. 0 <= x & x <= pi}",
1.162 - "errorBound (eps=(0::real))"];
1.163 -val (dI',pI',mI') =
1.164 -("Diff_App", ["maximum_of", "function"], ["Diff_App", "max_by_calculus"]);
1.165 -\<close> text \<open>
1.166 -from paper "Towards Accessible Formal Mathematics with ISAC and Isabelle/VSCode"
1.167 -
1.168 -F_I \<equiv> [ [r = 7], [A, [u, v]], [A = 2 * u * v - u \<up> 2 , ( 2 / u ) \<up> 2 + ( 2 / v ) \<up> 2 = r \<up> 2], {0 <..< r} ]
1.169 ---- type conflict ^^ ----------^^
1.170 -F_II \<equiv> [ [r = 7], [A, \<alpha>], [A = 2 * u * v - u \<up> 2 , u / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>], {0 <..< \<pi> / 2} ]
1.171 -\<close> ML \<open>
1.172 -val fmz = [
1.173 -(*Problem model:*)
1.174 - "Constants [r = (7::real)]", "Maximum A", "AdditionalValues [u, v]",
1.175 - "Extremum (A = 2 * u * v - u \<up> 2)",
1.176 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
1.177 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
1.178 - "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]",
1.179 -(*MethodC model:*)
1.180 - "FunctionVariable a", "FunctionVariable b", "FunctionVariable \<alpha>",
1.181 - "Domain {0 <..< r}",
1.182 - "Domain {0 <..< r}",
1.183 - "Domain {0 <..< \<pi> / 2}",
1.184 - "ErrorBound (\<epsilon> = (0::real))"
1.185 -]: TermC.as_string list;
1.186 -\<close> ML \<open>
1.187 -if (fmz |> map (TermC.parseNEW @{context}) |> filter is_some |> length) = 14
1.188 -then () else error "Formalise.model not parsed completely";
1.189 -\<close> ML \<open>
1.190 -val refs =
1.191 -("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"]);
1.192 -\<close> ML \<open>
1.193 -\<close> ML \<open>
1.194 -\<close> ML \<open>
1.195 -\<close> ML \<open>
1.196 -\<close>
1.197 -
1.198 -
1.199 -subsection \<open>Specification Phase\<close>
1.200 -text \<open>
1.201 - Stepwise development of \<open>Outer_Syntax.command \<^command_keyword>\<open>Example\<close>\<close> begins with
1.202 - the changeset https://hg.risc.uni-linz.ac.at/wneuper/isa/rev/9d98791b4080
1.203 - in the repository.
1.204 -
1.205 - The intermediate steps below will be deleted as soon as all above representations
1.206 - of \<open>Example "Diff_App/No.123 a"\<close> work out.
1.207 -\<close>
1.208 -
1.209 -Example "Diff_App/No.123 a"
1.210 - Problem "univariate_calculus/Optimisation"
1.211 - Specification:
1.212 - Model:
1.213 - Given: \<open>Constants [r = 7]\<close>
1.214 - Where: \<open>0 < r\<close>
1.215 - Find: \<open>Maximum A\<close> \<open>AdditionalValues [u, v]\<close>
1.216 - Relate: \<open>Extremum A = 2 * u * v - u \<up> 2\<close> \<open>SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\<close>
1.217 - References:
1.218 -(** )
1.219 - Theory_Ref: "Diff_App"
1.220 - (*\<Odot>*) Problem_Ref: "univariate_calculus/Optimisation"
1.221 - (*\<Otimes>*) Method_Ref: "Optimisation/by_univariate_calculus"
1.222 -( **)
1.223 -ML \<open>
1.224 -val state = the_data @{theory};
1.225 -\<close> ML \<open>
1.226 -if Ctree.get_obj Ctree.g_spec state [] =
1.227 -("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"])
1.228 -then () else error "Example's values not stored correctly";
1.229 -\<close> ML \<open>
1.230 -Ctree.get_obj Ctree.g_spec state []
1.231 -\<close> ML \<open>
1.232 -\<close> ML \<open>
1.233 -\<close>
1.234 -
1.235 -end
1.236 -
1.237 -
1.238 -
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/Tools/isac/BridgeJEdit/VSCode_Example.thy Sun Jun 19 16:55:13 2022 +0200
2.3 @@ -0,0 +1,237 @@
2.4 +(* Title: src/Tools/isac/BridgeJEdit/VSCode_Example.thy
2.5 + Author: Walther Neuper, JKU Linz
2.6 + (c) due to copyright terms
2.7 +
2.8 +Runnig example for developing Isabelle/Isac via Isabelle/PIDE in BridgeJEdit.
2.9 +File will go to test/Tools/isac/BridgeJEdit/VSCode_Example.thy
2.10 +compare test/Tools/isac/BridgeJEdit/vscode-example.sml
2.11 +*)
2.12 +
2.13 +theory VSCode_Example
2.14 + imports Calculation
2.15 +begin
2.16 +
2.17 +section \<open>Boilerplate, the example for Isabelle Workshop 2022\<close>
2.18 +
2.19 +subsection \<open>Specification Phase\<close>
2.20 +text \<open>Goal for Isabelle Workshop 2022: this part of the example should be ready for demonstration:
2.21 + 1. The keyword \<open>Example\<close> inserts the template underneath
2.22 + 2. The template is filled from a (hidden) formalisation with the following items in the
2.23 + 2.1. \<open>Model\<close>:
2.24 + * Constants _ ("_" indicates some kind of place holder for input)
2.25 + * the complete Where-field (the pre-condition), items marked as True | False
2.26 + * Maximum _, AdditionalValues _
2.27 + * Extremum _, SideCondition _
2.28 + 2.2 \<open>References\<close>:
2.29 + * place holders "_" for input
2.30 + * The toggle switch before \<open>Problem_Ref\<close> | \<open>Method_Ref\<close> is set to \<open>Problem_Ref\<close>
2.31 + This might be postponed after the Isabelle Workshop.
2.32 + 3. Input to 2.1 is
2.33 + * type checked and marked as Type-Error
2.34 + * marked as Correct | Superfluous | Incomplete | Unknown (compare Specify/p-model.sml)
2.35 + 4. Input to 2.2 by selection from a list / tree
2.36 + 5. On update of \<open>Problem_Ref\<close> (in the root problem) also \<open>Problem\<close> is updated;
2.37 + The argument of \<open>Problem\<close> comes with the template and is read-only.
2.38 +
2.39 +The specific representation of the Demo_Example demonstrate different situations
2.40 +in educational settings.
2.41 +\<close>
2.42 +
2.43 +subsubsection \<open>Complete Specification\<close>
2.44 +text \<open>
2.45 +* This is one correct result of interactive Specification.
2.46 +* Or this might be presented to the student in one go in order to start Solution immediately
2.47 + (and nevertheless make the Specification explicit)
2.48 +Note that \<open>Problem "univariate_calculus/Optimisation"\<close> and
2.49 +\<open>Problem_Ref: "univariate_calculus/Optimisation"\<close> are redundant; the latter is for input,
2.50 +the former is given initially and needs to be updated in accordance to \<open>Problem_Ref\<close>.
2.51 +\<close>
2.52 +text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
2.53 +
2.54 +Example "Diff_App/No.123 a"
2.55 + Problem "univariate_calculus/Optimisation"
2.56 + Specification:
2.57 + Model:
2.58 + Given: \<open>Constants r = 7\<close>
2.59 + Where: \<open>0 < r\<close>
2.60 + Find: \<open>Maximum A\<close> \<open>AdditionalValues u, v\<close>
2.61 + Relate: \<open>Extremum A = 2 \<sqdot> u \<sqdot> v − u \<up> 2\<close> \<open>SideCondition (u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2\<close>
2.62 + References:
2.63 + Theory_Ref: "Diff_App"
2.64 + \<Otimes> Problem_Ref: "univariate_calculus/Optimisation"
2.65 + \<Odot> Method_Ref: "Optimisation/by_univariate_calculus"
2.66 + Solution:
2.67 +
2.68 + (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>
2.69 +
2.70 +subsubsection \<open>Empty Specification\<close>
2.71 +text \<open>
2.72 + This is presented to the student in one go in order to start interactive Specification.
2.73 +\<close>
2.74 +text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
2.75 +
2.76 +Example "Diff_App/No.123 a"
2.77 + Problem "univariate_calculus/Optimisation"
2.78 + Specification:
2.79 + Model:
2.80 + Given: \<open>Constants _\<close>
2.81 + Where: \<open>0 < r\<close>
2.82 + Find: \<open>Maximum _\<close> \<open>AdditionalValues _\<close>
2.83 + Relate: \<open>Extremum _\<close> \<open>SideCondition _\<close>
2.84 + References:
2.85 + Theory_Ref: "_"
2.86 + \<Otimes> Problem_Ref: "_"
2.87 + \<Odot> Method_Ref: "_"
2.88 + Solution:
2.89 +
2.90 + (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>
2.91 +
2.92 +subsubsection \<open>Plain Example\<close>
2.93 +text \<open>
2.94 + This can occur in between text offering to start an interactive Calculation by using
2.95 + "Diff_App/No.123 a" as a link.
2.96 +\<close>
2.97 +text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
2.98 +
2.99 +Example "Diff_App/No.123 a"
2.100 +
2.101 + (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>
2.102 +
2.103 +subsubsection \<open>Immediate Start of Interactive Solving\<close>
2.104 +text \<open>
2.105 + This
2.106 +\<close>
2.107 +text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
2.108 +
2.109 +Example "Diff_App/No.123 a"
2.110 + Problem "univariate_calculus/Optimisation"
2.111 + Specification:
2.112 + Solution:
2.113 +
2.114 + (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>
2.115 +
2.116 +subsubsection \<open>Show the Model associated to Method_Ref\<close>
2.117 +text \<open>
2.118 + The Model of a method usually comprises more items than the model of a Problem: all these
2.119 + are required to run the program such that it automatically generates a Solution. For instance,
2.120 + compare \<open>problem pbl_bieg\<close> and \<open>method met_biege_2\<close> in \<open>Biegelinie.thy\<close>
2.121 + (TODO: method/program for \<open>Problem "univariate_calculus/Optimisation"\<close>)
2.122 + The Model of a method is usually called a guard.
2.123 +\<close>
2.124 +text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
2.125 +
2.126 +Example "Diff_App/No.123 a"
2.127 + Problem "univariate_calculus/Optimisation"
2.128 + Specification:
2.129 + Model:
2.130 + Given: \<open>Constants r = 7\<close>
2.131 + Where: \<open>0 < r\<close>
2.132 + Find: \<open>Maximum A\<close> \<open>AdditionalValues u, v\<close>
2.133 + Relate: \<open>Extremum A = 2 \<sqdot> u \<sqdot> v − u \<up> 2\<close> \<open>SideCondition (u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2\<close>
2.134 + References:
2.135 + Theory_Ref: "Diff_App"
2.136 + \<Odot> Problem_Ref: "univariate_calculus/Optimisation"
2.137 + \<Otimes> Method_Ref: "Optimisation/by_univariate_calculus"
2.138 + Solution:
2.139 +
2.140 + (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>
2.141 +
2.142 +
2.143 +section \<open>Stepwise Development\<close>
2.144 +
2.145 +subsection \<open>preparing VSCode_Example\<close>
2.146 +ML \<open>
2.147 +(**** preparing VSCode_Example ########################################################### ****)
2.148 +"----------- preparing VSCode_Example ----------------------------------------------------------";
2.149 +"----------- preparing VSCode_Example ----------------------------------------------------------";
2.150 +\<close> text \<open>
2.151 +--- maximum example with Step.specify_do_next --- from test/../step.sml
2.152 +val fmz = [
2.153 +(*Problem model:*)
2.154 + "fixedValues [r=Arbfix]", "maximum A",
2.155 + "valuesFor [a,b::real]",
2.156 + "relations [A=a*(b::real), (a/2) \<up> 2 + (b/2) \<up> 2 = (r::real) \<up> 2]",
2.157 + "relations [A=a*(b::real), (a/2) \<up> 2 + (b/2) \<up> 2 = (r::real) \<up> 2]",
2.158 + "relations [A=a*(b::real), a/2=r*sin alpha, b/2 = (r::real)*cos (alpha::real)]",
2.159 +(*MethodC model:*)
2.160 + "boundVariable a", "boundVariable b", "boundVariable alpha",
2.161 + "interval {x::real. 0 <= x & x <= 2*r}",
2.162 + "interval {x::real. 0 <= x & x <= 2*r}",
2.163 + "interval {x::real. 0 <= x & x <= pi}",
2.164 + "errorBound (eps=(0::real))"];
2.165 +val (dI',pI',mI') =
2.166 +("Diff_App", ["maximum_of", "function"], ["Diff_App", "max_by_calculus"]);
2.167 +\<close> text \<open>
2.168 +from paper "Towards Accessible Formal Mathematics with ISAC and Isabelle/VSCode"
2.169 +
2.170 +F_I \<equiv> [ [r = 7], [A, [u, v]], [A = 2 * u * v - u \<up> 2 , ( 2 / u ) \<up> 2 + ( 2 / v ) \<up> 2 = r \<up> 2], {0 <..< r} ]
2.171 +--- type conflict ^^ ----------^^
2.172 +F_II \<equiv> [ [r = 7], [A, \<alpha>], [A = 2 * u * v - u \<up> 2 , u / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>], {0 <..< \<pi> / 2} ]
2.173 +\<close> ML \<open>
2.174 +val fmz = [
2.175 +(*Problem model:*)
2.176 + "Constants [r = (7::real)]", "Maximum A", "AdditionalValues [u, v]",
2.177 + "Extremum (A = 2 * u * v - u \<up> 2)",
2.178 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
2.179 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
2.180 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]",
2.181 +(*MethodC model:*)
2.182 + "FunctionVariable a", "FunctionVariable b", "FunctionVariable \<alpha>",
2.183 + "Domain {0 <..< r}",
2.184 + "Domain {0 <..< r}",
2.185 + "Domain {0 <..< \<pi> / 2}",
2.186 + "ErrorBound (\<epsilon> = (0::real))"
2.187 +]: TermC.as_string list;
2.188 +\<close> ML \<open>
2.189 +if (fmz |> map (TermC.parseNEW @{context}) |> filter is_some |> length) = 14
2.190 +then () else error "Formalise.model not parsed completely";
2.191 +\<close> ML \<open>
2.192 +val refs =
2.193 +("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"]);
2.194 +\<close> ML \<open>
2.195 +\<close> ML \<open>
2.196 +\<close> ML \<open>
2.197 +\<close> ML \<open>
2.198 +\<close>
2.199 +
2.200 +
2.201 +subsection \<open>Specification Phase\<close>
2.202 +text \<open>
2.203 + Stepwise development of \<open>Outer_Syntax.command \<^command_keyword>\<open>Example\<close>\<close> begins with
2.204 + the changeset https://hg.risc.uni-linz.ac.at/wneuper/isa/rev/9d98791b4080
2.205 + in the repository.
2.206 +
2.207 + The intermediate steps below will be deleted as soon as all above representations
2.208 + of \<open>Example "Diff_App/No.123 a"\<close> work out.
2.209 +\<close>
2.210 +
2.211 +Example "Diff_App/No.123 a"
2.212 + Problem "univariate_calculus/Optimisation"
2.213 + Specification:
2.214 + Model:
2.215 + Given: \<open>Constants [r = 7]\<close>
2.216 + Where: \<open>0 < r\<close>
2.217 + Find: \<open>Maximum A\<close> \<open>AdditionalValues [u, v]\<close>
2.218 + Relate: \<open>Extremum A = 2 * u * v - u \<up> 2\<close> \<open>SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\<close>
2.219 + References:
2.220 +(** )
2.221 + Theory_Ref: "Diff_App"
2.222 + (*\<Odot>*) Problem_Ref: "univariate_calculus/Optimisation"
2.223 + (*\<Otimes>*) Method_Ref: "Optimisation/by_univariate_calculus"
2.224 +( **)
2.225 +ML \<open>
2.226 +val state = the_data @{theory};
2.227 +\<close> ML \<open>
2.228 +if Ctree.get_obj Ctree.g_spec state [] =
2.229 +("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"])
2.230 +then () else error "Example's values not stored correctly";
2.231 +\<close> ML \<open>
2.232 +Ctree.get_obj Ctree.g_spec state []
2.233 +\<close> ML \<open>
2.234 +\<close> ML \<open>
2.235 +\<close>
2.236 +
2.237 +end
2.238 +
2.239 +
2.240 +
3.1 --- a/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Sun Jun 19 16:10:11 2022 +0200
3.2 +++ b/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Sun Jun 19 16:55:13 2022 +0200
3.3 @@ -18,7 +18,7 @@
3.4 "----------- fun pbl_hierarchy2file ------------------------------------------------------------";
3.5 if Pbl_Met_Hierarchy.pbl_hierarchy2file "dummy/path/" =
3.6 ("dummy/path/pbl_hierarchy.xml",
3.7 - "<NODE>\n <ID> problem hierarchy </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_ROOT </CONTENTREF>\n <NODE>\n <ID> empty_probl_id </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_empty </CONTENTREF>\n </NODE>\n <NODE>\n <ID> simplification </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_simp </CONTENTREF>\n <NODE>\n <ID> polynomial </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_simp_poly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> rational </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_simp_rat </CONTENTREF>\n <NODE>\n <ID> partial_fraction </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_simp_rat_partfrac </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> vereinfachen </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_vereinfache </CONTENTREF>\n <NODE>\n <ID> polynom </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_vereinf_poly </CONTENTREF>\n <NODE>\n <ID> plus_minus </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_vereinf_poly_minus </CONTENTREF>\n </NODE>\n <NODE>\n <ID> klammer </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_vereinf_poly_klammer </CONTENTREF>\n </NODE>\n <NODE>\n <ID> binom_klammer </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_vereinf_poly_klammer_mal </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> probe </ID>\n <NO> 4 </NO>\n <CONTENTREF> pbl_probe </CONTENTREF>\n <NODE>\n <ID> polynom </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_probe_poly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> bruch </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_probe_bruch </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> equation </ID>\n <NO> 5 </NO>\n <CONTENTREF> pbl_equ </CONTENTREF>\n <NODE>\n <ID> univariate </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equ_univ </CONTENTREF>\n <NODE>\n <ID> rootX </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equ_univ_root </CONTENTREF>\n <NODE>\n <ID> sq </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equ_univ_root_sq </CONTENTREF>\n <NODE>\n <ID> rat </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equ_univ_root_sq_rat </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> normalise </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_equ_univ_root_norm </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> LINEAR </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_equ_univ_lin </CONTENTREF>\n </NODE>\n <NODE>\n <ID> rational </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_equ_univ_rat </CONTENTREF>\n </NODE>\n <NODE>\n <ID> polynomial </ID>\n <NO> 4 </NO>\n <CONTENTREF> pbl_equ_univ_poly </CONTENTREF>\n <NODE>\n <ID> degree_0 </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equ_univ_poly_deg0 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> degree_1 </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_equ_univ_poly_deg1 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> degree_2 </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_equ_univ_poly_deg2 </CONTENTREF>\n <NODE>\n <ID> sq_only </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equ_univ_poly_deg2_sqonly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> bdv_only </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_equ_univ_poly_deg2_bdvonly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> pqFormula </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_equ_univ_poly_deg2_pq </CONTENTREF>\n </NODE>\n <NODE>\n <ID> abcFormula </ID>\n <NO> 4 </NO>\n <CONTENTREF> pbl_equ_univ_poly_deg2_abc </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> degree_3 </ID>\n <NO> 4 </NO>\n <CONTENTREF> pbl_equ_univ_poly_deg3 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> degree_4 </ID>\n <NO> 5 </NO>\n <CONTENTREF> pbl_equ_univ_poly_deg4 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> normalise </ID>\n <NO> 6 </NO>\n <CONTENTREF> pbl_equ_univ_poly_norm </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> expanded </ID>\n <NO> 5 </NO>\n <CONTENTREF> pbl_equ_univ_expand </CONTENTREF>\n <NODE>\n <ID> degree_2 </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equ_univ_expand_deg2 </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> logarithmic </ID>\n <NO> 6 </NO>\n <CONTENTREF> pbl_test_equ_univ_log </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> makeFunctionTo </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_equ_fromfun </CONTENTREF>\n </NODE>\n <NODE>\n <ID> diophantine </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_equ_dio </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> function </ID>\n <NO> 6 </NO>\n <CONTENTREF> pbl_fun </CONTENTREF>\n <NODE>\n <ID> derivative_of </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_fun_deriv </CONTENTREF>\n <NODE>\n <ID> named </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_fun_deriv_nam </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> integrate </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_fun_integ </CONTENTREF>\n <NODE>\n <ID> named </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_fun_integ_nam </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> maximum_of </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_fun_max </CONTENTREF>\n <NODE>\n <ID> on_interval </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_fun_max_interv </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> make </ID>\n <NO> 4 </NO>\n <CONTENTREF> pbl_fun_make </CONTENTREF>\n <NODE>\n <ID> by_explicit </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_fun_max_expl </CONTENTREF>\n </NODE>\n <NODE>\n <ID> by_new_variable </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_fun_max_newvar </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> system </ID>\n <NO> 7 </NO>\n <CONTENTREF> pbl_equsys </CONTENTREF>\n <NODE>\n <ID> LINEAR </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equsys_lin </CONTENTREF>\n <NODE>\n <ID> 2x2 </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equsys_lin_2x2 </CONTENTREF>\n <NODE>\n <ID> triangular </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equsys_lin_2x2_tri </CONTENTREF>\n </NODE>\n <NODE>\n <ID> normalise </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_equsys_lin_2x2_norm </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> 3x3 </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_equsys_lin_3x3 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> 4x4 </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_equsys_lin_4x4 </CONTENTREF>\n <NODE>\n <ID> triangular </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equsys_lin_4x4_tri </CONTENTREF>\n </NODE>\n <NODE>\n <ID> normalise </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_equsys_lin_4x4_norm </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> Biegelinien </ID>\n <NO> 8 </NO>\n <CONTENTREF> pbl_bieg </CONTENTREF>\n <NODE>\n <ID> MomentBestimmte </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_bieg_mom </CONTENTREF>\n </NODE>\n <NODE>\n <ID> MomentGegebene </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_bieg_momg </CONTENTREF>\n </NODE>\n <NODE>\n <ID> einfache </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_bieg_einf </CONTENTREF>\n </NODE>\n <NODE>\n <ID> QuerkraftUndMomentBestimmte </ID>\n <NO> 4 </NO>\n <CONTENTREF> pbl_bieg_momquer </CONTENTREF>\n </NODE>\n <NODE>\n <ID> vonBelastungZu </ID>\n <NO> 5 </NO>\n <CONTENTREF> pbl_bieg_vonq </CONTENTREF>\n </NODE>\n <NODE>\n <ID> setzeRandbedingungen </ID>\n <NO> 6 </NO>\n <CONTENTREF> pbl_bieg_randbed </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Berechnung </ID>\n <NO> 9 </NO>\n <CONTENTREF> pbl_algein </CONTENTREF>\n <NODE>\n <ID> numerischSymbolische </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_algein_numsym </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Programming </ID>\n <NO> 10 </NO>\n <CONTENTREF> pbl_Programming </CONTENTREF>\n <NODE>\n <ID> SORT </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_Prog_sort </CONTENTREF>\n <NODE>\n <ID> insertion </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_Prog_sort_ins </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> test </ID>\n <NO> 11 </NO>\n <CONTENTREF> pbl_test </CONTENTREF>\n <NODE>\n <ID> equation </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_test_equ </CONTENTREF>\n <NODE>\n <ID> univariate </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_test_uni </CONTENTREF>\n <NODE>\n <ID> LINEAR </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_test_uni_lin </CONTENTREF>\n </NODE>\n <NODE>\n <ID> plain_square </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_test_uni_plain2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> polynomial </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_test_uni_poly </CONTENTREF>\n <NODE>\n <ID> degree_two </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_test_uni_poly_deg2 </CONTENTREF>\n <NODE>\n <ID> pq_formula </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_test_uni_poly_deg2_pq </CONTENTREF>\n </NODE>\n <NODE>\n <ID> abc_formula </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_test_uni_poly_deg2_abc </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> squareroot </ID>\n <NO> 4 </NO>\n <CONTENTREF> pbl_test_uni_root </CONTENTREF>\n </NODE>\n <NODE>\n <ID> normalise </ID>\n <NO> 5 </NO>\n <CONTENTREF> pbl_test_uni_norm </CONTENTREF>\n </NODE>\n <NODE>\n <ID> sqroot-test </ID>\n <NO> 6 </NO>\n <CONTENTREF> pbl_test_uni_roottest </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> inttype </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_test_intsimp </CONTENTREF>\n </NODE>\n <NODE>\n <ID> refine </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_test_refine </CONTENTREF>\n <NODE>\n <ID> pbla </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_pbla </CONTENTREF>\n <NODE>\n <ID> pbla1 </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_pbla1 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> pbla2 </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_pbla2 </CONTENTREF>\n <NODE>\n <ID> pbla2x </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_pbla2x </CONTENTREF>\n </NODE>\n <NODE>\n <ID> pbla2y </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_pbla2y </CONTENTREF>\n </NODE>\n <NODE>\n <ID> pbla2z </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_pbla2z </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> pbla3 </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_pbla3 </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> calculate </ID>\n <NO> 4 </NO>\n <CONTENTREF> pbl_ttest_calc </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> tool </ID>\n <NO> 12 </NO>\n <CONTENTREF> pbl_tool </CONTENTREF>\n <NODE>\n <ID> find_values </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_tool_findvals </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> SignalProcessing </ID>\n <NO> 13 </NO>\n <CONTENTREF> pbl_SP </CONTENTREF>\n <NODE>\n <ID> Z_Transform </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_SP_Ztrans </CONTENTREF>\n <NODE>\n <ID> Inverse </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_SP_Ztrans_inv </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n</NODE>")
3.8 + "<NODE>\n <ID> problem hierarchy </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_ROOT </CONTENTREF>\n <NODE>\n <ID> empty_probl_id </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_empty </CONTENTREF>\n </NODE>\n <NODE>\n <ID> simplification </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_simp </CONTENTREF>\n <NODE>\n <ID> polynomial </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_simp_poly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> rational </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_simp_rat </CONTENTREF>\n <NODE>\n <ID> partial_fraction </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_simp_rat_partfrac </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> vereinfachen </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_vereinfache </CONTENTREF>\n <NODE>\n <ID> polynom </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_vereinf_poly </CONTENTREF>\n <NODE>\n <ID> plus_minus </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_vereinf_poly_minus </CONTENTREF>\n </NODE>\n <NODE>\n <ID> klammer </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_vereinf_poly_klammer </CONTENTREF>\n </NODE>\n <NODE>\n <ID> binom_klammer </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_vereinf_poly_klammer_mal </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> probe </ID>\n <NO> 4 </NO>\n <CONTENTREF> pbl_probe </CONTENTREF>\n <NODE>\n <ID> polynom </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_probe_poly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> bruch </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_probe_bruch </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> equation </ID>\n <NO> 5 </NO>\n <CONTENTREF> pbl_equ </CONTENTREF>\n <NODE>\n <ID> univariate </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equ_univ </CONTENTREF>\n <NODE>\n <ID> rootX </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equ_univ_root </CONTENTREF>\n <NODE>\n <ID> sq </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equ_univ_root_sq </CONTENTREF>\n <NODE>\n <ID> rat </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equ_univ_root_sq_rat </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> normalise </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_equ_univ_root_norm </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> LINEAR </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_equ_univ_lin </CONTENTREF>\n </NODE>\n <NODE>\n <ID> rational </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_equ_univ_rat </CONTENTREF>\n </NODE>\n <NODE>\n <ID> polynomial </ID>\n <NO> 4 </NO>\n <CONTENTREF> pbl_equ_univ_poly </CONTENTREF>\n <NODE>\n <ID> degree_0 </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equ_univ_poly_deg0 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> degree_1 </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_equ_univ_poly_deg1 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> degree_2 </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_equ_univ_poly_deg2 </CONTENTREF>\n <NODE>\n <ID> sq_only </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equ_univ_poly_deg2_sqonly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> bdv_only </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_equ_univ_poly_deg2_bdvonly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> pqFormula </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_equ_univ_poly_deg2_pq </CONTENTREF>\n </NODE>\n <NODE>\n <ID> abcFormula </ID>\n <NO> 4 </NO>\n <CONTENTREF> pbl_equ_univ_poly_deg2_abc </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> degree_3 </ID>\n <NO> 4 </NO>\n <CONTENTREF> pbl_equ_univ_poly_deg3 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> degree_4 </ID>\n <NO> 5 </NO>\n <CONTENTREF> pbl_equ_univ_poly_deg4 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> normalise </ID>\n <NO> 6 </NO>\n <CONTENTREF> pbl_equ_univ_poly_norm </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> expanded </ID>\n <NO> 5 </NO>\n <CONTENTREF> pbl_equ_univ_expand </CONTENTREF>\n <NODE>\n <ID> degree_2 </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equ_univ_expand_deg2 </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> logarithmic </ID>\n <NO> 6 </NO>\n <CONTENTREF> pbl_test_equ_univ_log </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> makeFunctionTo </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_equ_fromfun </CONTENTREF>\n </NODE>\n <NODE>\n <ID> diophantine </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_equ_dio </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> function </ID>\n <NO> 6 </NO>\n <CONTENTREF> pbl_fun </CONTENTREF>\n <NODE>\n <ID> derivative_of </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_fun_deriv </CONTENTREF>\n <NODE>\n <ID> named </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_fun_deriv_nam </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> integrate </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_fun_integ </CONTENTREF>\n <NODE>\n <ID> named </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_fun_integ_nam </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> maximum_of </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_fun_max </CONTENTREF>\n <NODE>\n <ID> on_interval </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_fun_max_interv </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> make </ID>\n <NO> 4 </NO>\n <CONTENTREF> pbl_fun_make </CONTENTREF>\n <NODE>\n <ID> by_explicit </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_fun_max_expl </CONTENTREF>\n </NODE>\n <NODE>\n <ID> by_new_variable </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_fun_max_newvar </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> system </ID>\n <NO> 7 </NO>\n <CONTENTREF> pbl_equsys </CONTENTREF>\n <NODE>\n <ID> LINEAR </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equsys_lin </CONTENTREF>\n <NODE>\n <ID> 2x2 </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equsys_lin_2x2 </CONTENTREF>\n <NODE>\n <ID> triangular </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equsys_lin_2x2_tri </CONTENTREF>\n </NODE>\n <NODE>\n <ID> normalise </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_equsys_lin_2x2_norm </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> 3x3 </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_equsys_lin_3x3 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> 4x4 </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_equsys_lin_4x4 </CONTENTREF>\n <NODE>\n <ID> triangular </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_equsys_lin_4x4_tri </CONTENTREF>\n </NODE>\n <NODE>\n <ID> normalise </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_equsys_lin_4x4_norm </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> Biegelinien </ID>\n <NO> 8 </NO>\n <CONTENTREF> pbl_bieg </CONTENTREF>\n <NODE>\n <ID> MomentBestimmte </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_bieg_mom </CONTENTREF>\n </NODE>\n <NODE>\n <ID> MomentGegebene </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_bieg_momg </CONTENTREF>\n </NODE>\n <NODE>\n <ID> einfache </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_bieg_einf </CONTENTREF>\n </NODE>\n <NODE>\n <ID> QuerkraftUndMomentBestimmte </ID>\n <NO> 4 </NO>\n <CONTENTREF> pbl_bieg_momquer </CONTENTREF>\n </NODE>\n <NODE>\n <ID> vonBelastungZu </ID>\n <NO> 5 </NO>\n <CONTENTREF> pbl_bieg_vonq </CONTENTREF>\n </NODE>\n <NODE>\n <ID> setzeRandbedingungen </ID>\n <NO> 6 </NO>\n <CONTENTREF> pbl_bieg_randbed </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Berechnung </ID>\n <NO> 9 </NO>\n <CONTENTREF> pbl_algein </CONTENTREF>\n <NODE>\n <ID> numerischSymbolische </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_algein_numsym </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Programming </ID>\n <NO> 10 </NO>\n <CONTENTREF> pbl_Programming </CONTENTREF>\n <NODE>\n <ID> SORT </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_Prog_sort </CONTENTREF>\n <NODE>\n <ID> insertion </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_Prog_sort_ins </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> test </ID>\n <NO> 11 </NO>\n <CONTENTREF> pbl_test </CONTENTREF>\n <NODE>\n <ID> equation </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_test_equ </CONTENTREF>\n <NODE>\n <ID> univariate </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_test_uni </CONTENTREF>\n <NODE>\n <ID> LINEAR </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_test_uni_lin </CONTENTREF>\n </NODE>\n <NODE>\n <ID> plain_square </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_test_uni_plain2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> polynomial </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_test_uni_poly </CONTENTREF>\n <NODE>\n <ID> degree_two </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_test_uni_poly_deg2 </CONTENTREF>\n <NODE>\n <ID> pq_formula </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_test_uni_poly_deg2_pq </CONTENTREF>\n </NODE>\n <NODE>\n <ID> abc_formula </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_test_uni_poly_deg2_abc </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> squareroot </ID>\n <NO> 4 </NO>\n <CONTENTREF> pbl_test_uni_root </CONTENTREF>\n </NODE>\n <NODE>\n <ID> normalise </ID>\n <NO> 5 </NO>\n <CONTENTREF> pbl_test_uni_norm </CONTENTREF>\n </NODE>\n <NODE>\n <ID> sqroot-test </ID>\n <NO> 6 </NO>\n <CONTENTREF> pbl_test_uni_roottest </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> inttype </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_test_intsimp </CONTENTREF>\n </NODE>\n <NODE>\n <ID> refine </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_test_refine </CONTENTREF>\n <NODE>\n <ID> pbla </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_pbla </CONTENTREF>\n <NODE>\n <ID> pbla1 </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_pbla1 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> pbla2 </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_pbla2 </CONTENTREF>\n <NODE>\n <ID> pbla2x </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_pbla2x </CONTENTREF>\n </NODE>\n <NODE>\n <ID> pbla2y </ID>\n <NO> 2 </NO>\n <CONTENTREF> pbl_pbla2y </CONTENTREF>\n </NODE>\n <NODE>\n <ID> pbla2z </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_pbla2z </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> pbla3 </ID>\n <NO> 3 </NO>\n <CONTENTREF> pbl_pbla3 </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> calculate </ID>\n <NO> 4 </NO>\n <CONTENTREF> pbl_ttest_calc </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> tool </ID>\n <NO> 12 </NO>\n <CONTENTREF> pbl_tool </CONTENTREF>\n <NODE>\n <ID> find_values </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_tool_findvals </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Optimisation </ID>\n <NO> 13 </NO>\n <CONTENTREF> pbl_opti </CONTENTREF>\n <NODE>\n <ID> univariate_calculus </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_opti_univ </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> SignalProcessing </ID>\n <NO> 14 </NO>\n <CONTENTREF> pbl_SP </CONTENTREF>\n <NODE>\n <ID> Z_Transform </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_SP_Ztrans </CONTENTREF>\n <NODE>\n <ID> Inverse </ID>\n <NO> 1 </NO>\n <CONTENTREF> pbl_SP_Ztrans_inv </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n</NODE>")
3.9 then () else error "pbl_hierarchy2file CHANGED: has a Problem_Pattern been updated?"
3.10
3.11 "----------- fun met_hierarchy2file ------------------------------------------------------------";
3.12 @@ -26,5 +26,5 @@
3.13 "----------- fun met_hierarchy2file ------------------------------------------------------------";
3.14 if Pbl_Met_Hierarchy.met_hierarchy2file "dummy/path/" =
3.15 ("dummy/path/met_hierarchy.xml",
3.16 - "<NODE>\n <ID> method hierarchy </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_ROOT </CONTENTREF>\n <NODE>\n <ID> empty_meth_id </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_empty </CONTENTREF>\n </NODE>\n <NODE>\n <ID> simplification </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_tsimp </CONTENTREF>\n <NODE>\n <ID> for_polynomials </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_simp_poly </CONTENTREF>\n <NODE>\n <ID> with_minus </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_simp_poly_minus </CONTENTREF>\n </NODE>\n <NODE>\n <ID> with_parentheses </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_simp_poly_parenth </CONTENTREF>\n </NODE>\n <NODE>\n <ID> with_parentheses_mult </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_simp_poly_parenth_mult </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> of_rationals </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_simp_rat </CONTENTREF>\n <NODE>\n <ID> to_partial_fraction </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_partial_fraction </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> probe </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_probe </CONTENTREF>\n <NODE>\n <ID> fuer_polynom </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_probe_poly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> fuer_bruch </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_probe_bruch </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Equation </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_equ </CONTENTREF>\n <NODE>\n <ID> solve_log </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_equ_log </CONTENTREF>\n </NODE>\n <NODE>\n <ID> fromFunction </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_equ_fromfun </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> RootEq </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_rooteq </CONTENTREF>\n <NODE>\n <ID> norm_sq_root_equation </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_rooteq_norm </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_sq_root_equation </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_rooteq_sq </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_right_sq_root_equation </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_rooteq_sq_right </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_left_sq_root_equation </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_rooteq_sq_left </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> LinEq </ID>\n <NO> 6 </NO>\n <CONTENTREF> met_eqlin </CONTENTREF>\n <NODE>\n <ID> solve_lineq_equation </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_eq_lin </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> RatEq </ID>\n <NO> 7 </NO>\n <CONTENTREF> met_rateq </CONTENTREF>\n <NODE>\n <ID> solve_rat_equation </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_rat_eq </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> RootRatEq </ID>\n <NO> 8 </NO>\n <CONTENTREF> met_rootrateq </CONTENTREF>\n <NODE>\n <ID> elim_rootrat_equation </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_rootrateq_elim </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> PolyEq </ID>\n <NO> 9 </NO>\n <CONTENTREF> met_polyeq </CONTENTREF>\n <NODE>\n <ID> normalise_poly </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_polyeq_norm </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d0_polyeq_equation </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_polyeq_d0 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d1_polyeq_equation </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_polyeq_d1 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_equation </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_polyeq_d22 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_bdvonly_equation </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_polyeq_d2_bdvonly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_sqonly_equation </ID>\n <NO> 6 </NO>\n <CONTENTREF> met_polyeq_d2_sqonly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_pq_equation </ID>\n <NO> 7 </NO>\n <CONTENTREF> met_polyeq_d2_pq </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_abc_equation </ID>\n <NO> 8 </NO>\n <CONTENTREF> met_polyeq_d2_abc </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d3_polyeq_equation </ID>\n <NO> 9 </NO>\n <CONTENTREF> met_polyeq_d3 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> complete_square </ID>\n <NO> 10 </NO>\n <CONTENTREF> met_polyeq_complsq </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> diff </ID>\n <NO> 10 </NO>\n <CONTENTREF> met_diff </CONTENTREF>\n <NODE>\n <ID> differentiate_on_R </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_diff_onR </CONTENTREF>\n </NODE>\n <NODE>\n <ID> diff_simpl </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_diff_simpl </CONTENTREF>\n </NODE>\n <NODE>\n <ID> differentiate_equality </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_diff_equ </CONTENTREF>\n </NODE>\n <NODE>\n <ID> after_simplification </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_diff_after_simp </CONTENTREF>\n </NODE>\n <NODE>\n <ID> integration </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_diffint </CONTENTREF>\n <NODE>\n <ID> named </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_diffint_named </CONTENTREF>\n </NODE>\n <NODE>\n <ID> test </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_testint </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> EqSystem </ID>\n <NO> 11 </NO>\n <CONTENTREF> met_eqsys </CONTENTREF>\n <NODE>\n <ID> top_down_substitution </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_eqsys_topdown </CONTENTREF>\n <NODE>\n <ID> 2x2 </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_eqsys_topdown_2x2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> 4x4 </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_eqsys_topdown_4x4 </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> normalise </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_eqsys_norm </CONTENTREF>\n <NODE>\n <ID> 2x2 </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_eqsys_norm_2x2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> 4x4 </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_eqsys_norm_4x4 </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> IntegrierenUndKonstanteBestimmen </ID>\n <NO> 12 </NO>\n <CONTENTREF> met_biege </CONTENTREF>\n <NODE>\n <ID> 2xIntegrieren </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_biege_intconst_2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> 4x4System </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_biege_intconst_4 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> 1xIntegrieren </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_biege_intconst_1 </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> IntegrierenUndKonstanteBestimmen2 </ID>\n <NO> 13 </NO>\n <CONTENTREF> met_biege_2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> Biegelinien </ID>\n <NO> 14 </NO>\n <CONTENTREF> met_biege2 </CONTENTREF>\n <NODE>\n <ID> ausBelastung </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_biege_ausbelast </CONTENTREF>\n </NODE>\n <NODE>\n <ID> setzeRandbedingungenEin </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_biege_setzrand </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Berechnung </ID>\n <NO> 15 </NO>\n <CONTENTREF> met_algein </CONTENTREF>\n <NODE>\n <ID> erstNumerisch </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_algein_numsym_1num </CONTENTREF>\n </NODE>\n <NODE>\n <ID> erstSymbolisch </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_algein_symnum </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Programming </ID>\n <NO> 16 </NO>\n <CONTENTREF> met_Programming </CONTENTREF>\n <NODE>\n <ID> SORT </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_Prog_sort </CONTENTREF>\n <NODE>\n <ID> insertion </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_Prog_sort_ins </CONTENTREF>\n </NODE>\n <NODE>\n <ID> insertion_steps </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_Prog_sort_ins_steps </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> Test </ID>\n <NO> 17 </NO>\n <CONTENTREF> met_test </CONTENTREF>\n <NODE>\n <ID> solve_linear </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_test_solvelin </CONTENTREF>\n </NODE>\n <NODE>\n <ID> sqrt-equ-test </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_test_sqrt </CONTENTREF>\n </NODE>\n <NODE>\n <ID> squ-equ-test-subpbl1 </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_test_squ_sub </CONTENTREF>\n </NODE>\n <NODE>\n <ID> square_equation1 </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_test_eq1 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> square_equation2 </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_test_squ2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> square_equation </ID>\n <NO> 6 </NO>\n <CONTENTREF> met_test_squeq </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_plain_square </ID>\n <NO> 7 </NO>\n <CONTENTREF> met_test_eq_plain </CONTENTREF>\n </NODE>\n <NODE>\n <ID> norm_univar_equation </ID>\n <NO> 8 </NO>\n <CONTENTREF> met_test_norm_univ </CONTENTREF>\n </NODE>\n <NODE>\n <ID> intsimp </ID>\n <NO> 9 </NO>\n <CONTENTREF> met_test_intsimp </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_diophant </ID>\n <NO> 10 </NO>\n <CONTENTREF> met_test_diophant </CONTENTREF>\n </NODE>\n <NODE>\n <ID> test_calculate </ID>\n <NO> 11 </NO>\n <CONTENTREF> met_testcal </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Diff_App </ID>\n <NO> 18 </NO>\n <CONTENTREF> met_diffapp </CONTENTREF>\n <NODE>\n <ID> max_by_calculus </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_diffapp_max </CONTENTREF>\n </NODE>\n <NODE>\n <ID> make_fun_by_new_variable </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_diffapp_funnew </CONTENTREF>\n </NODE>\n <NODE>\n <ID> make_fun_by_explicit </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_diffapp_funexp </CONTENTREF>\n </NODE>\n <NODE>\n <ID> max_on_interval_by_calculus </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_diffapp_max_oninterval </CONTENTREF>\n </NODE>\n <NODE>\n <ID> find_values </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_diffapp_findvals </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> SignalProcessing </ID>\n <NO> 19 </NO>\n <CONTENTREF> met_SP </CONTENTREF>\n <NODE>\n <ID> Z_Transform </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_SP_Ztrans </CONTENTREF>\n <NODE>\n <ID> Inverse </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_SP_Ztrans_inv </CONTENTREF>\n </NODE>\n <NODE>\n <ID> Inverse_sub </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_SP_Ztrans_inv_sub </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n</NODE>")
3.17 + "<NODE>\n <ID> method hierarchy </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_ROOT </CONTENTREF>\n <NODE>\n <ID> empty_meth_id </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_empty </CONTENTREF>\n </NODE>\n <NODE>\n <ID> simplification </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_tsimp </CONTENTREF>\n <NODE>\n <ID> for_polynomials </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_simp_poly </CONTENTREF>\n <NODE>\n <ID> with_minus </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_simp_poly_minus </CONTENTREF>\n </NODE>\n <NODE>\n <ID> with_parentheses </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_simp_poly_parenth </CONTENTREF>\n </NODE>\n <NODE>\n <ID> with_parentheses_mult </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_simp_poly_parenth_mult </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> of_rationals </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_simp_rat </CONTENTREF>\n <NODE>\n <ID> to_partial_fraction </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_partial_fraction </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> probe </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_probe </CONTENTREF>\n <NODE>\n <ID> fuer_polynom </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_probe_poly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> fuer_bruch </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_probe_bruch </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Equation </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_equ </CONTENTREF>\n <NODE>\n <ID> solve_log </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_equ_log </CONTENTREF>\n </NODE>\n <NODE>\n <ID> fromFunction </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_equ_fromfun </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> RootEq </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_rooteq </CONTENTREF>\n <NODE>\n <ID> norm_sq_root_equation </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_rooteq_norm </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_sq_root_equation </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_rooteq_sq </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_right_sq_root_equation </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_rooteq_sq_right </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_left_sq_root_equation </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_rooteq_sq_left </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> LinEq </ID>\n <NO> 6 </NO>\n <CONTENTREF> met_eqlin </CONTENTREF>\n <NODE>\n <ID> solve_lineq_equation </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_eq_lin </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> RatEq </ID>\n <NO> 7 </NO>\n <CONTENTREF> met_rateq </CONTENTREF>\n <NODE>\n <ID> solve_rat_equation </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_rat_eq </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> RootRatEq </ID>\n <NO> 8 </NO>\n <CONTENTREF> met_rootrateq </CONTENTREF>\n <NODE>\n <ID> elim_rootrat_equation </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_rootrateq_elim </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> PolyEq </ID>\n <NO> 9 </NO>\n <CONTENTREF> met_polyeq </CONTENTREF>\n <NODE>\n <ID> normalise_poly </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_polyeq_norm </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d0_polyeq_equation </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_polyeq_d0 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d1_polyeq_equation </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_polyeq_d1 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_equation </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_polyeq_d22 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_bdvonly_equation </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_polyeq_d2_bdvonly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_sqonly_equation </ID>\n <NO> 6 </NO>\n <CONTENTREF> met_polyeq_d2_sqonly </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_pq_equation </ID>\n <NO> 7 </NO>\n <CONTENTREF> met_polyeq_d2_pq </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d2_polyeq_abc_equation </ID>\n <NO> 8 </NO>\n <CONTENTREF> met_polyeq_d2_abc </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_d3_polyeq_equation </ID>\n <NO> 9 </NO>\n <CONTENTREF> met_polyeq_d3 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> complete_square </ID>\n <NO> 10 </NO>\n <CONTENTREF> met_polyeq_complsq </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> diff </ID>\n <NO> 10 </NO>\n <CONTENTREF> met_diff </CONTENTREF>\n <NODE>\n <ID> differentiate_on_R </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_diff_onR </CONTENTREF>\n </NODE>\n <NODE>\n <ID> diff_simpl </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_diff_simpl </CONTENTREF>\n </NODE>\n <NODE>\n <ID> differentiate_equality </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_diff_equ </CONTENTREF>\n </NODE>\n <NODE>\n <ID> after_simplification </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_diff_after_simp </CONTENTREF>\n </NODE>\n <NODE>\n <ID> integration </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_diffint </CONTENTREF>\n <NODE>\n <ID> named </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_diffint_named </CONTENTREF>\n </NODE>\n <NODE>\n <ID> test </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_testint </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> EqSystem </ID>\n <NO> 11 </NO>\n <CONTENTREF> met_eqsys </CONTENTREF>\n <NODE>\n <ID> top_down_substitution </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_eqsys_topdown </CONTENTREF>\n <NODE>\n <ID> 2x2 </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_eqsys_topdown_2x2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> 4x4 </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_eqsys_topdown_4x4 </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> normalise </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_eqsys_norm </CONTENTREF>\n <NODE>\n <ID> 2x2 </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_eqsys_norm_2x2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> 4x4 </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_eqsys_norm_4x4 </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> IntegrierenUndKonstanteBestimmen </ID>\n <NO> 12 </NO>\n <CONTENTREF> met_biege </CONTENTREF>\n <NODE>\n <ID> 2xIntegrieren </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_biege_intconst_2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> 4x4System </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_biege_intconst_4 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> 1xIntegrieren </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_biege_intconst_1 </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> IntegrierenUndKonstanteBestimmen2 </ID>\n <NO> 13 </NO>\n <CONTENTREF> met_biege_2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> Biegelinien </ID>\n <NO> 14 </NO>\n <CONTENTREF> met_biege2 </CONTENTREF>\n <NODE>\n <ID> ausBelastung </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_biege_ausbelast </CONTENTREF>\n </NODE>\n <NODE>\n <ID> setzeRandbedingungenEin </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_biege_setzrand </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Berechnung </ID>\n <NO> 15 </NO>\n <CONTENTREF> met_algein </CONTENTREF>\n <NODE>\n <ID> erstNumerisch </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_algein_numsym_1num </CONTENTREF>\n </NODE>\n <NODE>\n <ID> erstSymbolisch </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_algein_symnum </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Programming </ID>\n <NO> 16 </NO>\n <CONTENTREF> met_Programming </CONTENTREF>\n <NODE>\n <ID> SORT </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_Prog_sort </CONTENTREF>\n <NODE>\n <ID> insertion </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_Prog_sort_ins </CONTENTREF>\n </NODE>\n <NODE>\n <ID> insertion_steps </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_Prog_sort_ins_steps </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n <NODE>\n <ID> Test </ID>\n <NO> 17 </NO>\n <CONTENTREF> met_test </CONTENTREF>\n <NODE>\n <ID> solve_linear </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_test_solvelin </CONTENTREF>\n </NODE>\n <NODE>\n <ID> sqrt-equ-test </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_test_sqrt </CONTENTREF>\n </NODE>\n <NODE>\n <ID> squ-equ-test-subpbl1 </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_test_squ_sub </CONTENTREF>\n </NODE>\n <NODE>\n <ID> square_equation1 </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_test_eq1 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> square_equation2 </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_test_squ2 </CONTENTREF>\n </NODE>\n <NODE>\n <ID> square_equation </ID>\n <NO> 6 </NO>\n <CONTENTREF> met_test_squeq </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_plain_square </ID>\n <NO> 7 </NO>\n <CONTENTREF> met_test_eq_plain </CONTENTREF>\n </NODE>\n <NODE>\n <ID> norm_univar_equation </ID>\n <NO> 8 </NO>\n <CONTENTREF> met_test_norm_univ </CONTENTREF>\n </NODE>\n <NODE>\n <ID> intsimp </ID>\n <NO> 9 </NO>\n <CONTENTREF> met_test_intsimp </CONTENTREF>\n </NODE>\n <NODE>\n <ID> solve_diophant </ID>\n <NO> 10 </NO>\n <CONTENTREF> met_test_diophant </CONTENTREF>\n </NODE>\n <NODE>\n <ID> test_calculate </ID>\n <NO> 11 </NO>\n <CONTENTREF> met_testcal </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Diff_App </ID>\n <NO> 18 </NO>\n <CONTENTREF> met_diffapp </CONTENTREF>\n <NODE>\n <ID> max_by_calculus </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_diffapp_max </CONTENTREF>\n </NODE>\n <NODE>\n <ID> make_fun_by_new_variable </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_diffapp_funnew </CONTENTREF>\n </NODE>\n <NODE>\n <ID> make_fun_by_explicit </ID>\n <NO> 3 </NO>\n <CONTENTREF> met_diffapp_funexp </CONTENTREF>\n </NODE>\n <NODE>\n <ID> max_on_interval_by_calculus </ID>\n <NO> 4 </NO>\n <CONTENTREF> met_diffapp_max_oninterval </CONTENTREF>\n </NODE>\n <NODE>\n <ID> find_values </ID>\n <NO> 5 </NO>\n <CONTENTREF> met_diffapp_findvals </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> Optimisation </ID>\n <NO> 19 </NO>\n <CONTENTREF> met_opti </CONTENTREF>\n <NODE>\n <ID> by_univariate_calculus </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_opti_univ </CONTENTREF>\n </NODE>\n </NODE>\n <NODE>\n <ID> SignalProcessing </ID>\n <NO> 20 </NO>\n <CONTENTREF> met_SP </CONTENTREF>\n <NODE>\n <ID> Z_Transform </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_SP_Ztrans </CONTENTREF>\n <NODE>\n <ID> Inverse </ID>\n <NO> 1 </NO>\n <CONTENTREF> met_SP_Ztrans_inv </CONTENTREF>\n </NODE>\n <NODE>\n <ID> Inverse_sub </ID>\n <NO> 2 </NO>\n <CONTENTREF> met_SP_Ztrans_inv_sub </CONTENTREF>\n </NODE>\n </NODE>\n </NODE>\n</NODE>")
3.18 then () else error "met_hierarchy2file CHANGED: has a Method been updated?"
4.1 --- a/test/Tools/isac/Test_Isac.thy Sun Jun 19 16:10:11 2022 +0200
4.2 +++ b/test/Tools/isac/Test_Isac.thy Sun Jun 19 16:55:13 2022 +0200
4.3 @@ -275,6 +275,8 @@
4.4 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
4.5
4.6 ML_file "BridgeJEdit/parseC.sml"
4.7 + ML_file "BridgeJEdit/preliminary.sml"
4.8 + ML_file "BridgeJEdit/vscode-example.sml"
4.9
4.10 ML_file "Knowledge/delete.sml"
4.11 ML_file "Knowledge/descript.sml"
5.1 --- a/test/Tools/isac/Test_Isac_Short.thy Sun Jun 19 16:10:11 2022 +0200
5.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Sun Jun 19 16:55:13 2022 +0200
5.3 @@ -275,6 +275,7 @@
5.4 ML_file "BridgeLibisabelle/interface.sml"
5.5 ML_file "BridgeJEdit/parseC.sml"
5.6 ML_file "BridgeJEdit/preliminary.sml"
5.7 + ML_file "BridgeJEdit/vscode-example.sml"
5.8
5.9 ML_file "Knowledge/delete.sml"
5.10 ML_file "Knowledge/descript.sml"
5.11 @@ -284,7 +285,7 @@
5.12 ML_file "Knowledge/gcd_poly_ml.sml"
5.13 ML_file "Knowledge/rational-1.sml"
5.14 (*ML_file "Knowledge/rational-2.sml" Test_Isac_Short*)
5.15 - ML_file "Knowledge/equation.sml"
5.16 +ML_file "Knowledge/equation.sml"
5.17 ML_file "Knowledge/root.sml"
5.18 ML_file "Knowledge/lineq.sml"
5.19
6.1 --- a/test/Tools/isac/Test_Some.thy Sun Jun 19 16:10:11 2022 +0200
6.2 +++ b/test/Tools/isac/Test_Some.thy Sun Jun 19 16:55:13 2022 +0200
6.3 @@ -129,138 +129,80 @@
6.4 "Domain {0 <..< \<pi> / 2}",
6.5 "ErrorBound (\<epsilon> = (0::real))"
6.6 ]: TermC.as_string list;
6.7 -\<close> ML \<open>
6.8 -TermC.parseNEW @{context} "FunctionVariable a"
6.9 -\<close> ML \<open>
6.10 -\<close> ML \<open>
6.11 -\<close> ML \<open>
6.12 -(fmz |> map (TermC.parseNEW @{context}) |> filter is_some |> length);
6.13 -\<close> ML \<open>
6.14 -val refs = ("Diff_App", ["maximum_of", "function"], ["Diff_App", "max_by_calculus"]);
6.15 -\<close> ML \<open>
6.16 +val refs =
6.17 +("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"]);
6.18 val (p,_,f, nxt,_,pt) = CalcTreeTEST [(fmz, refs)];
6.19 -(* BEFORE CORRECTION we had:
6.20 -
6.21 -exception TYPE raised (line 641 of "~/repos/isa/src/Tools/isac/BaseDefinitions/termC.sml"):
6.22 - formalisation inconsistent w.r.t. type inference:
6.23 - real
6.24 - real
6.25 - real
6.26 - 'a
6.27 - 'a
6.28 - 'a
6.29 - 'a
6.30 - real
6.31 - r
6.32 - u
6.33 - v
6.34 - u
6.35 - r
6.36 - \<alpha>
6.37 - v
6.38 - \<alpha>*)
6.39 -\<close> ML \<open>
6.40 -fmz |> map (TermC.parseNEW @{context})
6.41 -(*val it =
6.42 - [SOME
6.43 - (
6.44 - Const ("Input_Descript.Constants", "bool list \<Rightarrow> nam") $
6.45 - (Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
6.46 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ Free ("r", "real") $
6.47 - (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit1", "num \<Rightarrow> num") $ (Const ("Num.num.Bit1", "num \<Rightarrow> num") $ Const ("Num.num.One", "num"))))) $
6.48 - Const ("List.list.Nil", "bool list"))
6.49 - ),
6.50 - SOME (Const ("Input_Descript.Maximum", "real \<Rightarrow> toreal") $ Free ("A", "real")),
6.51 - SOME
6.52 - (
6.53 - Const ("Input_Descript.AdditionalValues", "real list \<Rightarrow> toreall") $
6.54 - (Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("u", "real") $
6.55 - (Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("v", "real") $ Const ("List.list.Nil", "real list")))
6.56 - ),
6.57 - SOME
6.58 - (
6.59 - Const ("Input_Descript.Extremum", "bool \<Rightarrow> toreal") $
6.60 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ Free ("A", "real") $
6.61 - (Const ("Groups.minus_class.minus", "real \<Rightarrow> real \<Rightarrow> real") $
6.62 - (Const ("Groups.times_class.times", "real \<Rightarrow> real \<Rightarrow> real") $
6.63 - (Const ("Groups.times_class.times", "real \<Rightarrow> real \<Rightarrow> real") $ (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num"))) $
6.64 - Free ("u", "real")) $
6.65 - Free ("v", "real")) $
6.66 - (Const ("BaseDefinitions.realpow", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("u", "real") $
6.67 - (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num"))))))
6.68 - ),
6.69 - SOME
6.70 - (
6.71 - Const ("Input_Descript.SideConditions", "bool list \<Rightarrow> una") $
6.72 - (Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
6.73 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
6.74 - (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $
6.75 - (Const ("BaseDefinitions.realpow", "real \<Rightarrow> real \<Rightarrow> real") $
6.76 - (Const ("Rings.divide_class.divide", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("u", "real") $
6.77 - (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))) $
6.78 - (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))) $
6.79 - (Const ("BaseDefinitions.realpow", "real \<Rightarrow> real \<Rightarrow> real") $
6.80 - (Const ("Rings.divide_class.divide", "real \<Rightarrow> real \<Rightarrow> real") $ (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num"))) $
6.81 - Free ("v", "real")) $
6.82 - (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num"))))) $
6.83 - (Const ("BaseDefinitions.realpow", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("r", "real") $
6.84 - (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num"))))) $
6.85 - Const ("List.list.Nil", "bool list"))
6.86 - ),
6.87 - SOME
6.88 - (
6.89 - Const ("Input_Descript.SideConditions", "bool list \<Rightarrow> una") $
6.90 - (Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
6.91 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
6.92 - (Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $
6.93 - (Const ("BaseDefinitions.realpow", "real \<Rightarrow> real \<Rightarrow> real") $
6.94 - (Const ("Rings.divide_class.divide", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("u", "real") $
6.95 - (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))) $
6.96 - (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))) $
6.97 - (Const ("BaseDefinitions.realpow", "real \<Rightarrow> real \<Rightarrow> real") $
6.98 - (Const ("Rings.divide_class.divide", "real \<Rightarrow> real \<Rightarrow> real") $ (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num"))) $
6.99 - Free ("v", "real")) $
6.100 - (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num"))))) $
6.101 - (Const ("BaseDefinitions.realpow", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("r", "real") $
6.102 - (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num"))))) $
6.103 - Const ("List.list.Nil", "bool list"))
6.104 - ),
6.105 - SOME
6.106 - (
6.107 - Const ("Input_Descript.SideConditions", "bool list \<Rightarrow> una") $
6.108 - (Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
6.109 - (Const ("HOL.eq", "'a \<Rightarrow> 'a \<Rightarrow> bool") $
6.110 - (Const ("Rings.divide_class.divide", "'a \<Rightarrow> 'a \<Rightarrow> 'a") $ Free ("u", "'a") $
6.111 - (Const ("Num.numeral_class.numeral", "num \<Rightarrow> 'a") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))) $
6.112 - (Const ("Groups.times_class.times", "'a \<Rightarrow> 'a \<Rightarrow> 'a") $ Free ("r", "'a") $ (Const ("Transcendental.sin", "'a \<Rightarrow> 'a") $ Free ("\<alpha>", "'a")))) $
6.113 - (Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
6.114 - (Const ("HOL.eq", "'a \<Rightarrow> 'a \<Rightarrow> bool") $
6.115 - (Const ("Rings.divide_class.divide", "'a \<Rightarrow> 'a \<Rightarrow> 'a") $ (Const ("Num.numeral_class.numeral", "num \<Rightarrow> 'a") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num"))) $
6.116 - Free ("v", "'a")) $
6.117 - (Const ("Groups.times_class.times", "'a \<Rightarrow> 'a \<Rightarrow> 'a") $ Free ("r", "'a") $ (Const ("Transcendental.cos", "'a \<Rightarrow> 'a") $ Free ("\<alpha>", "'a")))) $
6.118 - Const ("List.list.Nil", "bool list")))
6.119 - ),
6.120 - SOME (Const ("Input_Descript.FunctionVariable", "real \<Rightarrow> una") $ Free ("a", "real")), SOME (Const ("Input_Descript.FunctionVariable", "real \<Rightarrow> una") $ Free ("b", "real")),
6.121 - SOME (Const ("Input_Descript.FunctionVariable", "real \<Rightarrow> una") $ Free ("\<alpha>", "real")),
6.122 - SOME (Const ("Input_Descript.Domain", "real set \<Rightarrow> una") $ (Const ("Set_Interval.ord_class.greaterThanLessThan", "real \<Rightarrow> real \<Rightarrow> real set") $ Const ("Groups.zero_class.zero", "real") $ Free ("r", "real"))),
6.123 - SOME (Const ("Input_Descript.Domain", "real set \<Rightarrow> una") $ (Const ("Set_Interval.ord_class.greaterThanLessThan", "real \<Rightarrow> real \<Rightarrow> real set") $ Const ("Groups.zero_class.zero", "real") $ Free ("r", "real"))),
6.124 - SOME
6.125 - (
6.126 - Const ("Input_Descript.Domain", "real set \<Rightarrow> una") $
6.127 - (Const ("Set_Interval.ord_class.greaterThanLessThan", "real \<Rightarrow> real \<Rightarrow> real set") $ Const ("Groups.zero_class.zero", "real") $
6.128 - (Const ("Rings.divide_class.divide", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("\<pi>", "real") $
6.129 - (Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))))
6.130 - ),
6.131 - SOME (Const ("Input_Descript.ErrorBound", "bool \<Rightarrow> nam") $ (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ Free ("\<epsilon>", "real") $ Const ("Groups.zero_class.zero", "real")))]:
6.132 - term option list*)
6.133 -\<close> ML \<open>
6.134 -\<close> ML \<open>
6.135 -\<close> text \<open>
6.136 -
6.137
6.138 (*** stepwise Specification: Problem model================================================= ***)
6.139 -val ("ok", ([(Model_Problem, Model_Problem' (["maximum_of", "function"], _, _), _)], _, ptp))
6.140 +val ("ok", ([(Model_Problem, Model_Problem' (["univariate_calculus", "Optimisation"], _, _), _)], _, ptp))
6.141 = Step.specify_do_next (pt, p);
6.142 +val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], _, ptp))
6.143 + = Step.specify_do_next ptp;
6.144 +val ("ok", ([(Add_Find "Maximum A", _, _)], _, ptp))
6.145 + = Step.specify_do_next ptp;
6.146 +val ("ok", ([(Add_Find "AdditionalValues [u]", _, _)], _, ptp))
6.147 + = Step.specify_do_next ptp;
6.148 +val ("ok", ([(Add_Find "AdditionalValues [v]", _, _)], _, ptp))
6.149 + = Step.specify_do_next ptp;
6.150 +val ("ok", ([(Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)", _, _)], _, ptp))
6.151 + = Step.specify_do_next ptp;
6.152 +val ("ok", ([(Add_Relation "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", _, _)], _, ptp))
6.153 + = Step.specify_do_next ptp;
6.154 +
6.155 +(*** Problem model is complete ============================================================ ***)
6.156 +val PblObj {probl, ...} = get_obj I (fst ptp) [];
6.157 +if I_Model.to_string @{context} probl = "[\n" ^
6.158 + "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] ,(fixes, [[r = 7]])), \n" ^
6.159 + "(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A ,(maxx, [A])), \n" ^
6.160 + "(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] ,(vals, [[u, v]])), \n" ^
6.161 + "(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) ,(extr, [A = 2 * u * v - u \<up> 2])), \n" ^
6.162 + "(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ,(sideconds, [[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]]))]"
6.163 +then () else error "I_Model.to_string probl CHANGED";
6.164 +
6.165 +(*** Specification of References ========================================================== ***)
6.166 +val ("ok", ([(Specify_Theory "Diff_App", _, _)], _, ptp))
6.167 + = Step.specify_do_next ptp;
6.168 +val ("ok", ([(Specify_Problem ["univariate_calculus", "Optimisation"], _, _)], _, ptp))
6.169 + = Step.specify_do_next ptp;
6.170 +val ("ok", ([(Specify_Method ["Optimisation", "by_univariate_calculus"], _, _)], _, ptp))
6.171 + = Step.specify_do_next ptp;
6.172 +
6.173 +(*** stepwise Specification: MethodC model ================================================ ***)
6.174 +val ("ok", ([(Add_Given "FunctionVariable a", _, _)], _, ptp))
6.175 + = Step.specify_do_next ptp;
6.176 +val ("ok", ([(Add_Given "Input_Descript.Domain {0<..<r}", _, _)], _, ptp))
6.177 + = Step.specify_do_next ptp;
6.178 +val ("ok", ([(Add_Given "ErrorBound (\<epsilon> = 0)", _, _)], _, ptp))
6.179 + = Step.specify_do_next ptp;
6.180 +
6.181 +val PblObj {meth, ...} = get_obj I (fst ptp) [];
6.182 +if I_Model.to_string @{context} meth = "[\n" ^
6.183 + "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] ,(fixes, [[r = 7]])), \n" ^
6.184 + "(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A ,(maxx, [A])), \n" ^
6.185 + "(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] ,(vals, [[u, v]])), \n" ^
6.186 + "(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) ,(extr, [A = 2 * u * v - u \<up> 2])), \n" ^
6.187 + "(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ,(sideconds, [[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]])), \n" ^
6.188 + "(7 ,[1] ,true ,#Given ,Cor FunctionVariable a ,(funvar, [a])), \n" ^
6.189 + "(10 ,[1, 2] ,true ,#Given ,Cor Input_Descript.Domain {0<..<r} ,(doma, [{0<..<r}])), \n" ^
6.190 + "(12 ,[1, 2, 3] ,true ,#Given ,Cor ErrorBound (\<epsilon> = 0) ,(err, [\<epsilon> = 0]))]"
6.191 +then () else error "I_Model.to_string meth CHANGED";
6.192 +(*** Specification of Problem and MethodC model is complete, Solution starts ============== ***)
6.193 +
6.194 +(*---
6.195 +Step.specify_do_next ptp;
6.196 +(*ERROR in creating the environment from formal args. of partial_function "Diff_App.univar_optimisation"
6.197 +and the actual args., ie. items of the guard of "["Optimisation", "by_univariate_calculus"]" by "assoc_by_type":
6.198 +formal arg "err" of type "bool" doesn't mach an actual arg.
6.199 +with:
6.200 +7 formal args: ["fixes", "maxx", "extr", "sideconds", "funvar", "doma", "err"]
6.201 +7 actual args: ["[r = 7]", "A", "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", "a", "{0<..<r}", "\<epsilon> = 0", "[u, v]"]
6.202 + with types: ["bool list", "real", "bool list", "real", "real set", "bool", "real list"]*)
6.203 +---*)
6.204 +\<close> ML \<open>
6.205 +\<close> ML \<open>
6.206 +\<close> ML \<open>
6.207 +\<close> ML \<open>
6.208 +\<close> ML \<open>
6.209 \<close> ML \<open>
6.210 \<close> ML \<open>
6.211 \<close>