(*  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> UPDATE:

1. The \<open>Example\<close> below is a minimal adaptation of \<open>problem pbl_bieg : "Biegelinien" ..\<close>

  in Knowledge/Biegelinie.thy.

2. GOON

\<close>

(*

vvvvvvv why raises \<open>Example\<close> exception Option raised (line 82 of "General/basics.ML")? Although 

        * code (Outer_Syntax.command..Example..) and 

        * application (Example pbl_bieg : "Biegelinien".) are exact copies from Makarius?

        * Although the application below with \<open>problem\<close> works?

        * Although \<open>ExampleSPARK\<close> is disambiguated in Calculation_OLD.thy ?!?

        HOW CAN SUCH AN ERROR BE INVESTIGATED ? debugger ? .. ?         

        *)

Example pbl_bieg : "Biegelinien" =

  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>

  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>

end