1.1 --- a/src/Tools/isac/BridgeJEdit/Demo_Example.thy Sun Jun 19 09:35:51 2022 +0200
1.2 +++ b/src/Tools/isac/BridgeJEdit/Demo_Example.thy Sun Jun 19 12:46:43 2022 +0200
1.3 @@ -137,6 +137,62 @@
1.4
1.5 section \<open>Stepwise Development\<close>
1.6
1.7 +subsection \<open>preparing VSCode_Example\<close>
1.8 +ML \<open>
1.9 +(**** preparing VSCode_Example ########################################################### ****)
1.10 +"----------- preparing VSCode_Example ----------------------------------------------------------";
1.11 +"----------- preparing VSCode_Example ----------------------------------------------------------";
1.12 +\<close> text \<open>
1.13 +--- maximum example with Step.specify_do_next --- from test/../step.sml
1.14 +val fmz = [
1.15 +(*Problem model:*)
1.16 + "fixedValues [r=Arbfix]", "maximum A",
1.17 + "valuesFor [a,b::real]",
1.18 + "relations [A=a*(b::real), (a/2) \<up> 2 + (b/2) \<up> 2 = (r::real) \<up> 2]",
1.19 + "relations [A=a*(b::real), (a/2) \<up> 2 + (b/2) \<up> 2 = (r::real) \<up> 2]",
1.20 + "relations [A=a*(b::real), a/2=r*sin alpha, b/2 = (r::real)*cos (alpha::real)]",
1.21 +(*MethodC model:*)
1.22 + "boundVariable a", "boundVariable b", "boundVariable alpha",
1.23 + "interval {x::real. 0 <= x & x <= 2*r}",
1.24 + "interval {x::real. 0 <= x & x <= 2*r}",
1.25 + "interval {x::real. 0 <= x & x <= pi}",
1.26 + "errorBound (eps=(0::real))"];
1.27 +val (dI',pI',mI') =
1.28 +("Diff_App", ["maximum_of", "function"], ["Diff_App", "max_by_calculus"]);
1.29 +\<close> text \<open>
1.30 +from paper "Towards Accessible Formal Mathematics with ISAC and Isabelle/VSCode"
1.31 +
1.32 +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.33 +--- type conflict ^^ ----------^^
1.34 +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.35 +\<close> ML \<open>
1.36 +val fmz = [
1.37 +(*Problem model:*)
1.38 + "Constants [r = (7::real)]", "Maximum A", "AdditionalValues [u, v]",
1.39 + "Extremum (A = 2 * u * v - u \<up> 2)",
1.40 + "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
1.41 + "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
1.42 + "SideConditions [u / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]",
1.43 +(*MethodC model:*)
1.44 + "FunctionVariable a", "FunctionVariable b", "FunctionVariable \<alpha>",
1.45 + "Domain {0 <..< r}",
1.46 + "Domain {0 <..< r}",
1.47 + "Domain {0 <..< \<pi> / 2}",
1.48 + "ErrorBound (\<epsilon> = (0::real))"
1.49 +]: TermC.as_string list;
1.50 +\<close> ML \<open>
1.51 +if (fmz |> map (TermC.parseNEW @{context}) |> filter is_some |> length) = 14
1.52 +then () else error "Formalise.model not parsed completely";
1.53 +\<close> ML \<open>
1.54 +val refs =
1.55 +("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"]);
1.56 +\<close> ML \<open>
1.57 +\<close> ML \<open>
1.58 +\<close> ML \<open>
1.59 +\<close> ML \<open>
1.60 +\<close>
1.61 +
1.62 +
1.63 subsection \<open>Specification Phase\<close>
1.64 text \<open>
1.65 Stepwise development of \<open>Outer_Syntax.command \<^command_keyword>\<open>Example\<close>\<close> begins with
1.66 @@ -151,10 +207,10 @@
1.67 Problem "univariate_calculus/Optimisation"
1.68 Specification:
1.69 Model:
1.70 - Given: \<open>Constants r = 7\<close>
1.71 + Given: \<open>Constants [r = 7]\<close>
1.72 Where: \<open>0 < r\<close>
1.73 - Find: \<open>Maximum A\<close> \<open>AdditionalValues u, v\<close>
1.74 - 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.75 + Find: \<open>Maximum A\<close> \<open>AdditionalValues [u, v]\<close>
1.76 + 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.77 References:
1.78 (** )
1.79 Theory_Ref: "Diff_App"
2.1 --- a/src/Tools/isac/Specify/Input_Descript.thy Sun Jun 19 09:35:51 2022 +0200
2.2 +++ b/src/Tools/isac/Specify/Input_Descript.thy Sun Jun 19 12:46:43 2022 +0200
2.3 @@ -31,13 +31,16 @@
2.4 someList :: "'a list => unl" (*not for elementwise input, eg. inssort*)
2.5
2.6 additionalRels :: "bool list => una"
2.7 - boundVariable :: "real => una"
2.8 + boundVariable :: "real => una"
2.9 + FunctionVariable :: "real => una"
2.10 derivative :: "real => una"
2.11 equalities :: "bool list => tobooll" (*WN071228 see fixedValues*)
2.12 equality :: "bool => una"
2.13 errorBound :: "bool => nam"
2.14 + ErrorBound :: "bool => nam"
2.15
2.16 fixedValues :: "bool list => nam"
2.17 + Constants :: "bool list => nam"
2.18 functionEq :: "bool => una" (*6.5.03: functionTerm -> functionEq*)
2.19 antiDerivative :: "bool => una"
2.20 functionOf :: "real => una"
2.21 @@ -45,16 +48,21 @@
2.22 functionTerm :: "real => una" (*6.5.03: functionTerm -> functionEq*)
2.23 functionName :: "real => una"
2.24 interval :: "real set => una"
2.25 + Domain :: "real set => una"
2.26 maxArgument :: "bool => toreal"
2.27 maximum :: "real => toreal"
2.28 + Maximum :: "real => toreal"
2.29 + Extremum :: "bool => toreal"
2.30
2.31 relations :: "bool list => una"
2.32 + SideConditions :: "bool list => una"
2.33 solutions :: "bool list => toreall"
2.34 (*solution :: bool => toreal WN0509 bool list=> toreall --->EqSystem*)
2.35 solveFor :: "real => una"
2.36 differentiateFor:: "real => una"
2.37 unknown :: "'a => unknow"
2.38 - valuesFor :: "real list => toreall"
2.39 + valuesFor :: "real list => toreall"
2.40 + AdditionalValues :: "real list => toreall"
2.41
2.42 intTestGiven :: "int => una"
2.43 realTestGiven :: "real => una"