(*  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 \<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 "Example" inserts the template underneath

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

    2.1. Model:

        * 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 References:

        * place holders "_" for input

        * The toggle switch before RProblem | RMethod is set to RProblem

          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

\<close>

subsubsection \<open>Complete Specification\<close>

text \<open>

Example <No.123 a>

  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 <No.123 a>

  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>

end