(*  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 problem*)

 problem 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"

 text \<open> (*Output from: Example pbl_bieg : "Biegelinien" = .. *)

 === Outer_Syntax.command 4 

 === the_data thy \<Rightarrow> NONE

        (*Output from: problem pbl_bieg : "Biegelinien" = .. *)

 --- Outer_Syntax.command 4 

 --- the_data thy \<Rightarrow> (Rule_Def.Repeat {id = empty, preconds = [], rew_ord = (dummy_ord, _: fn),

   erls = _, srls = _, calc = _, errpatts = _, ,

   rules = [],

   rules = Empty_Prog}) 

 --- Outer_Syntax.command 5

 \<close> ML \<open>

 Rule_Set.append_rules "empty" Rule_Set.empty []

 \<close> 

 text \<open> (*Output from: Example pbl_bieg : "Biegelinien" = .. HERE*)

 val it = Repeat {calc = [], erls = Empty, errpatts = [], id = "empty", preconds = [], 

   rew_ord = ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Empty}: Rule_Def.rule_set

        (*Output from: problem pbl_bieg : "Biegelinien" = .. HERE*)

 val it = Repeat {calc = [], erls = Empty, errpatts = [], id = "empty", preconds = [], 

   rew_ord = ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Empty}: Rule_Def.rule_set

        (*Output from: problem pbl_bieg : "Biegelinien" = .. IN Biegelinie.thy*)

 val it = Repeat {calc = [], erls = Empty, errpatts = [], id = "empty", preconds = [], 

   rew_ord = ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Empty}: Rule_Def.rule_set

        (*^^^ all the same*)

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 end