(*  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>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 pbl_bieg : "Biegelinien" =

  Method: "IntegrierenUndKonstanteBestimmen2"

  Given: "Traegerlaenge l_l" "Streckenlast q_q"

  (* Where: "0 < l_l" ...wait for &lt; and handling Arbfix*)

  Find: "Biegelinie b_b"

  Relate: "Randbedingungen r_b"

ML \<open>

val state = the_data @{theory};

if Ctree.get_obj Ctree.g_spec state [] =

("empty_thy_id", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]) then ()

else error "Example's values not stored correctly";

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

end