author | wneuper <Walther.Neuper@jku.at> |
Tue, 31 May 2022 10:17:11 +0200 | |
changeset 60439 | 848667c5dd56 |
parent 60438 | 0121ef469160 |
child 60441 | 9488084c3441 |
permissions | -rw-r--r-- |
Walther@60433 | 1 |
(* Title: src/Tools/isac/BridgeJEdit/Demo_Example.thy |
Walther@60433 | 2 |
Author: Walther Neuper, JKU Linz |
Walther@60433 | 3 |
(c) due to copyright terms |
Walther@60433 | 4 |
|
Walther@60433 | 5 |
Runnig example for developing Isabelle/Isac via Isabelle/PIDE in BridgeJEdit |
Walther@60433 | 6 |
*) |
Walther@60433 | 7 |
|
Walther@60433 | 8 |
theory Demo_Example |
Walther@60433 | 9 |
imports Calculation |
Walther@60433 | 10 |
begin |
Walther@60433 | 11 |
|
Walther@60434 | 12 |
section \<open>Boilerplate, the example from Isabelle Workshop 2022\<close> |
Walther@60433 | 13 |
|
Walther@60433 | 14 |
subsection \<open>Specification Phase\<close> |
Walther@60433 | 15 |
text \<open>Goal for Isabelle Workshop 2022: this part of the example should be ready for demonstration: |
Walther@60434 | 16 |
1. The keyword \<open>Example\<close> inserts the template underneath |
Walther@60433 | 17 |
2. The template is filled from a (hidden) formalisation with the following items in the |
Walther@60434 | 18 |
2.1. \<open>Model\<close>: |
Walther@60433 | 19 |
* Constants _ ("_" indicates some kind of place holder for input) |
Walther@60433 | 20 |
* the complete Where-field (the pre-condition), items marked as True | False |
Walther@60433 | 21 |
* Maximum _, AdditionalValues _ |
Walther@60433 | 22 |
* Extremum _, SideCondition _ |
Walther@60434 | 23 |
2.2 \<open>References\<close>: |
Walther@60433 | 24 |
* place holders "_" for input |
Walther@60434 | 25 |
* The toggle switch before \<open>RProblem\<close> | \<open>RMethod\<close> is set to \<open>RProblem\<close> |
Walther@60433 | 26 |
This might be postponed after the Isabelle Workshop. |
Walther@60433 | 27 |
3. Input to 2.1 is |
Walther@60433 | 28 |
* type checked and marked as Type-Error |
Walther@60433 | 29 |
* marked as Correct | Superfluous | Incomplete | Unknown (compare Specify/p-model.sml) |
Walther@60433 | 30 |
4. Input to 2.2 by selection from a list / tree |
Walther@60434 | 31 |
5. On update of \<open>RProblem\<close> (in the root problem) also \<open>Problem\<close> is updated; |
Walther@60434 | 32 |
The argument of \<open>Problem\<close> comes with the template and is read-only. |
Walther@60433 | 33 |
\<close> |
Walther@60433 | 34 |
|
Walther@60433 | 35 |
subsubsection \<open>Complete Specification\<close> |
Walther@60433 | 36 |
text \<open> |
Walther@60434 | 37 |
Example \<open>No.123 a\<close> |
Walther@60433 | 38 |
Problem ''univariate_calculus/Optimisation'' |
Walther@60433 | 39 |
Specification: |
Walther@60433 | 40 |
Model: |
Walther@60433 | 41 |
Given: "Constants r = 7" |
Walther@60433 | 42 |
Where: "0 < r" |
Walther@60433 | 43 |
Find: "Maximum A" "AdditionalValues u, v" |
Walther@60433 | 44 |
Relate: "Extremum A = 2 \<sqdot> u \<sqdot> v − u \<up> 2" "SideCondition (u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2" |
Walther@60433 | 45 |
References: |
Walther@60433 | 46 |
RTheory: ''Diff_App'' |
Walther@60433 | 47 |
x RProblem: ''univariate_calculus/Optimisation'' |
Walther@60433 | 48 |
RMethod: ''Optimisation/by_univariate_calculus'' |
Walther@60433 | 49 |
Solution: |
Walther@60433 | 50 |
\<close> |
Walther@60433 | 51 |
|
Walther@60433 | 52 |
subsubsection \<open>Empty Specification\<close> |
Walther@60433 | 53 |
text \<open> |
Walther@60434 | 54 |
Example \<open>No.123 a\<close> |
Walther@60433 | 55 |
Problem ''univariate_calculus/Optimisation'' |
Walther@60433 | 56 |
Specification: |
Walther@60433 | 57 |
Model: |
Walther@60433 | 58 |
Given: "Constants _" |
Walther@60433 | 59 |
Where: "_" |
Walther@60433 | 60 |
Find: "Maximum _" "AdditionalValues _" |
Walther@60433 | 61 |
Relate: "Extremum _ "SideCondition _" |
Walther@60433 | 62 |
References: |
Walther@60433 | 63 |
RTheory: ''_'' |
Walther@60433 | 64 |
x RProblem: ''_'' |
Walther@60433 | 65 |
RMethod: ''_'' |
Walther@60433 | 66 |
Solution: |
Walther@60433 | 67 |
\<close> |
Walther@60433 | 68 |
|
Walther@60433 | 69 |
section \<open>Stepwise Development\<close> |
Walther@60434 | 70 |
|
Walther@60433 | 71 |
subsection \<open>Specification Phase\<close> |
Walther@60434 | 72 |
text \<open> UPDATE: |
Walther@60434 | 73 |
1. The \<open>Example\<close> below is a minimal adaptation of \<open>problem pbl_bieg : "Biegelinien" ..\<close> |
Walther@60434 | 74 |
in Knowledge/Biegelinie.thy. |
Walther@60434 | 75 |
2. GOON |
Walther@60434 | 76 |
\<close> |
Walther@60433 | 77 |
|
Walther@60434 | 78 |
(* |
Walther@60434 | 79 |
vvvvvvv why raises \<open>Example\<close> exception Option raised (line 82 of "General/basics.ML")? Although |
Walther@60434 | 80 |
* code (Outer_Syntax.command..Example..) and |
Walther@60434 | 81 |
* application (Example pbl_bieg : "Biegelinien".) are exact copies from Makarius? |
Walther@60434 | 82 |
* Although the application below with \<open>problem\<close> works? |
Walther@60434 | 83 |
* Although \<open>ExampleSPARK\<close> is disambiguated in Calculation_OLD.thy ?!? |
Walther@60434 | 84 |
HOW CAN SUCH AN ERROR BE INVESTIGATED ? debugger ? .. ? |
Walther@60436 | 85 |
Example problem*) |
Walther@60438 | 86 |
Example pbl_bieg : "Biegelinien" = |
Walther@60434 | 87 |
Method: "IntegrierenUndKonstanteBestimmen2" |
Walther@60434 | 88 |
Given: "Traegerlaenge l_l" "Streckenlast q_q" |
Walther@60434 | 89 |
(* Where: "0 < l_l" ...wait for < and handling Arbfix*) |
Walther@60434 | 90 |
Find: "Biegelinie b_b" |
Walther@60434 | 91 |
Relate: "Randbedingungen r_b" |
Walther@60433 | 92 |
|
Walther@60439 | 93 |
ML \<open> |
Walther@60436 | 94 |
\<close> ML \<open> |
Walther@60436 | 95 |
\<close> ML \<open> |
Walther@60436 | 96 |
\<close> ML \<open> |
Walther@60434 | 97 |
\<close> ML \<open> |
Walther@60434 | 98 |
\<close> ML \<open> |
Walther@60434 | 99 |
\<close> |
Walther@60433 | 100 |
|
Walther@60433 | 101 |
end |