theory Test_VSCode_Example

   imports "Isac.Calculation"

 begin 

 subsubsection \<open>Complete Specification at once\<close>

 text \<open>

   Just a test, that this works also in $ISABELLE_ISAC_TEST

 \<close>

 Example "Diff_App-No.123a"

   Specification:

     Model:

       Given: \<open>Constants [r = 7]\<close>

       Where: \<open>0 < r\<close>

       Find:  \<open>Maximum A\<close> \<open>AdditionalValues [u, v]\<close>

       Relate: \<open>Extremum A = 2 * u * v - u \<up> 2\<close> 

         \<open>SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\<close>

     References: 

 (**  )

        Theory_Ref: "Diff_App"

     \<Otimes> Problem_Ref: "univariate_calculus/Optimisation"

     \<Odot> Method_Ref: "Optimisation/by_univariate_calculus"

   Solution:

 (  **)

 subsubsection \<open>Specification step by step\<close>

 text \<open>

   In an electronic textbook there shall be references to examples given, for instance,

   by \<open>Example "Diff_App-No.123a"\<close>. Such a reference shall be easily "activated" 

   to start a Solution at the spot ?and?or? to open a separate window.

   Activating the reference \<open>Example "Diff_App-No.123a"\<close> shall result in a threefold alternative,

   where (2)=(3) for the parsers:

   (1) the Example presents a "normal problem" with a Specification (preferred by engineers),

     see above subsubsection \<open>Empty Specification\<close>,

   (2) the Example presents a "normal problem" without a Specification (preferred in high-school):

     |Example "Diff_App-No.123a"

     |  Specification:

     |  Solution:

     |    ..first formula as given by the specifid Method..

   (3) the Example presents a "CAS_Cmd":

     |Example "Linear_Equation/No.123 a"

     |  Specification:

     |  Solution:

     |    solve (x + 1 = 2, x)

   \<open>Specification\<close> is always visible in order to remind of the existence.

   \<open>Outer_Syntax.command \<^command_keyword>\<open>Example\<close>\<close> shall be able to parse all three cases

   (while still skipping considerations about \<open>Specification\<close> and sub-problems).

   Below is the Example with case (1):

   * The lines \<open>text --- remove this line and make content Isar input---\\<close>

     and      ---------- remove this line and make content Isar input---/

     will be deleted after correct implementation

   * The \<open>ML \<open>blocks\<close>\<close> in between show, that ISAC is able of "next step guidance"; 

     can be deleted as well.

   * This Example also shows the toggle between \<open>\<Otimes>\<close> and \<open>\<Odot>\<close>.

 \<close> 

 text \<open>

   # 1: ISAC starts the Example by presenting an "empty" Specification:

 \<close> 

 ML \<open> (* # 1: At the first call of \<open>Example\<close> ISAC initialises a calculation *)

 val p = ([], Pos.Pbl);

 val pt = update_state (*here we have Ctree.EmptyPtree and thus call init_ctree*)

 ("Diff_App-No.123a", 

     (* Problem.parse_model_input results in markup, which is accepted by \<open>fun update_state\<close>, too:

                  Constants [r = 7] *)

   ( [("#Given", ["Constants [r = 7]"]),

      ("#Where", ["0 < r"]), 

      ("#Find", ["Maximum A", "AdditionalValues [u, v]"]), 

      ("#Relate", ["Extremum A = 2 * u * v - u \<up> 2", 

         "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"])

     ],

     ("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"])

     (*References_Def.explode_id ^^^^^^^^^^^^^^^^^^^^^^, ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)

   )

 ) Ctree.EmptyPtree;

 val ptp = (pt, p);

 \<close>

 Example "Diff_App-No.123a"

   Specification:

     Model:

       Given: \<open>Constants [r = 7]\<close>

       Where: \<open>0 < r\<close>

       Find:  \<open>Maximum _\<close> \<open>AdditionalValues [_]\<close>

       Relate: \<open>Extremum _\<close> \<open>SideConditions [_]\<close>

     References: 

 (**  )

        Theory_Ref: "_"

     \<Otimes> Problem_Ref: "_/_"

     \<Odot> Method_Ref: "_/_"

   Solution:

 (  **)

 text \<open>

   # 2: The user inputs a next item, which is marked "correct" by ISAC:

 \<close> 

 ML \<open> (* # 2: ISAC suggests a next item on request *)

 val ("ok", ([(Tactic.Add_Given "Constants [r = 7]", _, _)], _, ptp))

   = Step.specify_do_next ptp;

 \<close>

 Example "Diff_App-No.123a"

   Specification:

     Model:

       Given: \<open>Constants r = 7\<close>

       Where: \<open>0 < r\<close>

       Find:  \<open>Maximum _\<close> \<open>AdditionalValues [_]\<close>

       Relate: \<open>Extremum _\<close> \<open>SideConditions [_]\<close>

     References:

 (**  )

        Theory_Ref: "_"

     \<Otimes> Problem_Ref: "_/_"

     \<Odot> Method_Ref: "_/_"

   Solution:

 (  **)

 text \<open>

   # 3: The user inputs a next item somewhere in the \<open>Specification\<close>;

        Since this item requests for a list, \<open>AdditionalValues\<close> is marked "incomplete":

 \<close> 

 ML \<open> (* 3: ISAC suggests a next item within a term list *)

 val ("ok", ([(Tactic.Add_Find "Maximum A", _, _)], _, ptp))

   = Step.specify_do_next ptp;

 \<close>

 Example "Diff_App-No.123a"

   Specification:

     Model:

       Given: \<open>Constants r = 7\<close>

       Where: \<open>0 < r\<close>

       Find:  \<open>Maximum _\<close> \<open>AdditionalValues [u]\<close>

       Relate: \<open>Extremum _\<close> \<open>SideConditions [_]\<close>

     References:

 (**  )

        Theory_Ref: "_"

     \<Otimes> Problem_Ref: "_/_"

     \<Odot> Method_Ref: "_/_"

   Solution:

 (  **)

 text \<open>

   # 4: The user inputs a next item, and the item \<open>AdditionalValues\<close> is marked "correct":

 \<close> 

 ML \<open> (* # 4: ISAC suggests a next step on request, even a next element within a list *)

 val ("ok", ([(Tactic.Add_Find "AdditionalValues [u]", _, _)], _, ptp))

   = Step.specify_do_next ptp;

 \<close>

 Example "Diff_App-No.123a"

   Specification:

     Model:

       Given: \<open>Constants r = 7\<close>

       Where: \<open>0 < r\<close>

       Find:  \<open>Maximum _\<close> \<open>AdditionalValues [u, v]\<close>

       Relate: \<open>Extremum _\<close> \<open>SideConditions [_]\<close>

     References:

 (**  )

        Theory_Ref: "_"

     \<Otimes> Problem_Ref: "_/_"

     \<Odot> Method_Ref: "_/_"

   Solution:

 (  **)

 text \<open>

   # 5: Input to \<open>Problem_Ref\<close> is according to the (hidden) formalisation:

 \<close> 

 ML \<open> (* # 5: Input to \<open>Problem_Ref\<close> might change the \<open>Model\<close> *)

 \<close>

 Example "Diff_App-No.123a"

   Specification:

     Model:

       Given: \<open>Constants r = 7\<close>

       Where: \<open>0 < r\<close>

       Find:  \<open>Maximum _\<close> \<open>AdditionalValues [u, v]\<close>

       Relate: \<open>Extremum _\<close> \<open>SideConditions [_]\<close>

     References:

 (**  )

        Theory_Ref: "_"

     \<Otimes> Problem_Ref: "_/_"

     \<Odot> Method_Ref: "_/_"

   Solution:

 (  **)

 text \<open>

   # 6: Input to \<open>Method_Ref\<close> changes the \<open>Model\<close> to the respective \<open>Method\<close>;

        There is also a feature to change the \<open>Model\<close> according to 

        direct manipulation of \<open>\<Otimes>\<close> and \<open>\<Odot>\<close>.

 \<close> 

 ML \<open> (* # 6: Input to \<open>Method_Ref\<close> changes the \<open>Model\<close> to the respective \<open>Method\<close> *)

 \<close>

 text \<open> --- remove this line and make content Isar input---\

 Example "Diff_App-No.123a"

   Specification:

     Model:                                          GOON: lookup model of method GOON GOON GOON GOON GOON!

       Given: \<open>Constants r = 7\<close>

       Where: \<open>0 < r\<close>

       Find:  \<open>Maximum _\<close> \<open>AdditionalValues [u, v]\<close>

       Relate: \<open>Extremum _\<close> \<open>SideConditions [_]\<close>

     References:

        Theory_Ref: "_"

     \<Odot> Problem_Ref: "univariate_calculus/Optimisation"

     \<Otimes> Method_Ref: "Optimisation/by_univariate_calculus"

   Solution:

 ---------- remove this line and make content Isar input---/

 \<close>

 text \<open>

   # 7: xxxxx:

 \<close> 

 ML \<open> (* # 7: ISAC suggests a next step on request *)

 \<close>

 text \<open> --- remove this line and make content Isar input---\

 ---------- remove this line and make content Isar input---/

 \<close>

 text \<open>

   # 8: xxxxx:

 \<close> 

 ML \<open> (* # 8: ISAC suggests a next step on request *)

 \<close>

 text \<open> --- remove this line and make content Isar input---\

 ---------- remove this line and make content Isar input---/

 \<close>

 text \<open>

   # 9: xxxxx:

 \<close> 

 ML \<open> (* # 9: ISAC suggests a next step on request *)

 \<close>

 text \<open> --- remove this line and make content Isar input---\

 ---------- remove this line and make content Isar input---/

 \<close>

 ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 end