(*  Title:      src/Tools/isac/BridgeJEdit/Demo_Example.thy

    Author:     Walther Neuper, JKU Linz

    (c) due to copyright terms

Runnig example for developing Isabelle/Isac via Isabelle/PIDE in BridgeJEdit

*)

theory Demo_Example 

  imports Calculation

begin

section \<open>Boilerplate, the example from Isabelle Workshop 2022\<close>

subsection \<open>Specification Phase\<close>

text \<open>Goal for Isabelle Workshop 2022: this part of the example should be ready for demonstration:

  1. The keyword \<open>Example\<close> inserts the template underneath

  2. The template is filled from a (hidden) formalisation with the following items in the

    2.1. \<open>Model\<close>:

        * Constants _  ("_" indicates some kind of place holder for input)

        * the complete Where-field (the pre-condition), items marked as True | False

        * Maximum _, AdditionalValues _

        * Extremum _, SideCondition _

    2.2 \<open>References\<close>:

        * place holders "_" for input

        * The toggle switch before \<open>Problem_Ref\<close> | \<open>Method_Ref\<close> is set to \<open>Problem_Ref\<close>

          This might be postponed after the Isabelle Workshop.

  3. Input to 2.1 is 

    * type checked and marked as Type-Error

    * marked as Correct | Superfluous | Incomplete | Unknown (compare Specify/p-model.sml)

  4. Input to 2.2 by selection from a list / tree

  5. On update of \<open>Problem_Ref\<close> (in the root problem) also \<open>Problem\<close> is updated;

     The argument of \<open>Problem\<close> comes with the template and is read-only.

The specific representation of the Demo_Example demonstrate different situations

in educational settings.

\<close>

subsubsection \<open>Complete Specification\<close>

text \<open>

* This is one correct result of interactive Specification.

* Or this might be presented to the student in one go in order to start Solution immediately

  (and nevertheless make the Specification explicit)

Note that \<open>Problem "univariate_calculus/Optimisation"\<close> and 

\<open>Problem_Ref: "univariate_calculus/Optimisation"\<close> are redundant; the latter is for input,

the former is given initially and needs to be updated in accordance to \<open>Problem_Ref\<close>.

\<close>

text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)

Example "Diff_App/No.123 a"

  Problem "univariate_calculus/Optimisation"

    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 \<sqdot> u \<sqdot> v − u \<up> 2\<close> \<open>SideCondition (u / 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:

       (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>

subsubsection \<open>Empty Specification\<close>

text \<open>

  This is presented to the student in one go in order to start interactive Specification.

\<close>

text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)

Example "Diff_App/No.123 a"

  Problem "univariate_calculus/Optimisation"

    Specification:

      Model:

        Given: \<open>Constants _\<close>

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

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

        Relate: \<open>Extremum _\<close> \<open>SideCondition _\<close>

      References:

         Theory_Ref: "_"

      \<Otimes> Problem_Ref: "_"

      \<Odot> Method_Ref: "_"

    Solution:

       (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>

subsubsection \<open>Plain Example\<close>

text \<open>

  This can occur in between text offering to start an interactive Calculation by using

  "Diff_App/No.123 a" as a link.

\<close>

text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)

Example "Diff_App/No.123 a"

       (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>

subsubsection \<open>Immediate Start of Interactive Solving\<close>

text \<open>

  This 

\<close>

text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)

Example "Diff_App/No.123 a"

  Problem "univariate_calculus/Optimisation"

    Specification:

    Solution:

       (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>

subsubsection \<open>Show the Model associated to Method_Ref\<close>

text \<open>

  The Model of a method usually comprises more items than the model of a Problem: all these

  are required to run the program such that it automatically generates a Solution. For instance,

  compare \<open>problem pbl_bieg\<close> and \<open>method met_biege_2\<close> in \<open>Biegelinie.thy\<close>

  (TODO: method/program for \<open>Problem "univariate_calculus/Optimisation"\<close>)

  The Model of a method is usually called a guard.

\<close>

text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)

Example "Diff_App/No.123 a"

  Problem "univariate_calculus/Optimisation"

    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 \<sqdot> u \<sqdot> v − u \<up> 2\<close> \<open>SideCondition (u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2\<close>

      References:

         Theory_Ref: "Diff_App"

      \<Odot> Problem_Ref: "univariate_calculus/Optimisation"

      \<Otimes> Method_Ref: "Optimisation/by_univariate_calculus"

    Solution:

       (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>

section \<open>Stepwise Development\<close>

subsection \<open>preparing VSCode_Example\<close>

ML \<open>

(**** preparing VSCode_Example ########################################################### ****)

"----------- preparing VSCode_Example ----------------------------------------------------------";

"----------- preparing VSCode_Example ----------------------------------------------------------";

\<close> text \<open>

--- maximum example with Step.specify_do_next --- from test/../step.sml

val fmz = [

(*Problem model:*)

  "fixedValues [r=Arbfix]", "maximum A",

  "valuesFor [a,b::real]",

  "relations [A=a*(b::real), (a/2) \<up> 2 + (b/2) \<up> 2 = (r::real) \<up> 2]",

  "relations [A=a*(b::real), (a/2) \<up> 2 + (b/2) \<up> 2 = (r::real) \<up> 2]",

  "relations [A=a*(b::real), a/2=r*sin alpha, b/2 = (r::real)*cos (alpha::real)]",

(*MethodC model:*)

  "boundVariable a", "boundVariable b", "boundVariable alpha",

  "interval {x::real. 0 <= x & x <= 2*r}",

  "interval {x::real. 0 <= x & x <= 2*r}",

  "interval {x::real. 0 <= x & x <= pi}",

  "errorBound (eps=(0::real))"];

val (dI',pI',mI') = 

("Diff_App", ["maximum_of", "function"], ["Diff_App", "max_by_calculus"]);

\<close> text \<open>

from paper "Towards Accessible Formal Mathematics with ISAC and Isabelle/VSCode"

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} ]

--- type conflict ^^ ----------^^

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} ]

\<close> ML \<open>

val fmz = [

(*Problem model:*)

  "Constants [r = (7::real)]", "Maximum A", "AdditionalValues [u, v]",

  "Extremum (A = 2 * u * v - u \<up> 2)",

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

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

  "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]",

(*MethodC model:*)

  "FunctionVariable a", "FunctionVariable b", "FunctionVariable \<alpha>",

  "Domain {0 <..< r}",

  "Domain {0 <..< r}",

  "Domain {0 <..< \<pi> / 2}",

  "ErrorBound (\<epsilon> = (0::real))"

]: TermC.as_string list;

\<close> ML \<open>

if (fmz |> map (TermC.parseNEW @{context}) |> filter is_some |> length) = 14

then () else error "Formalise.model not parsed completely";

\<close> ML \<open>

val refs = 

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

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

subsection \<open>Specification Phase\<close>

text \<open> 

  Stepwise development of \<open>Outer_Syntax.command \<^command_keyword>\<open>Example\<close>\<close> begins with 

  the changeset https://hg.risc.uni-linz.ac.at/wneuper/isa/rev/9d98791b4080

  in the repository.

  The intermediate steps below will be deleted as soon as all above representations 

  of \<open>Example "Diff_App/No.123 a"\<close> work out.

\<close>

Example "Diff_App/No.123 a"

  Problem "univariate_calculus/Optimisation"

    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 / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\<close>

      References:

(** )

         Theory_Ref: "Diff_App"

  (*\<Odot>*) Problem_Ref: "univariate_calculus/Optimisation"

  (*\<Otimes>*) Method_Ref: "Optimisation/by_univariate_calculus"

( **)

ML \<open>

val state = the_data @{theory};

\<close> ML \<open>

if Ctree.get_obj Ctree.g_spec state [] =

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

then () else error "Example's values not stored correctly";

\<close> ML \<open>

Ctree.get_obj Ctree.g_spec state []

\<close> ML \<open>

\<close> ML \<open>

\<close>

end