(*  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>RProblem\<close> | \<open>RMethod\<close> is set to \<open>RProblem\<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>RProblem\<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.

 \<close>

 subsubsection \<open>Complete Specification\<close>

 text \<open>

 Example \<open>No.123 a\<close>

   Problem ''univariate_calculus/Optimisation''

     Specification:

       Model:

         Given: "Constants r = 7"

         Where: "0 < r"

         Find:  "Maximum A" "AdditionalValues u, v"

         Relate: "Extremum A = 2 \<sqdot> u \<sqdot> v − u \<up> 2" "SideCondition (u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2"

       References:

         RTheory: ''Diff_App''

       x RProblem: ''univariate_calculus/Optimisation''

         RMethod: ''Optimisation/by_univariate_calculus''

     Solution:

 \<close>

 subsubsection \<open>Empty Specification\<close>

 text \<open>

 Example \<open>No.123 a\<close>

   Problem ''univariate_calculus/Optimisation''

     Specification:

       Model:

         Given: "Constants _"

         Where: "_"

         Find:  "Maximum _" "AdditionalValues _"

         Relate: "Extremum _ "SideCondition _"

       References:

         RTheory: ''_''

       x RProblem: ''_''

         RMethod: ''_''

     Solution:

 \<close>

 section \<open>Stepwise Development\<close>

 subsection \<open>Specification Phase\<close>

 text \<open> 

   stepwise development to be inspected from

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

   onwards.

 \<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>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 end