4 |
4 |
5 subsubsection \<open>Complete Specification at once\<close> |
5 subsubsection \<open>Complete Specification at once\<close> |
6 text \<open> |
6 text \<open> |
7 Just a test, that this works also in $ISABELLE_ISAC_TEST |
7 Just a test, that this works also in $ISABELLE_ISAC_TEST |
8 \<close> |
8 \<close> |
9 Example "Diff_App/No.123 a" |
9 Example "Diff_App-No.123a" |
10 Specification: |
10 Specification: |
11 Model: |
11 Model: |
12 Given: \<open>Constants [r = 7]\<close> |
12 Given: \<open>Constants [r = 7]\<close> |
13 Where: \<open>0 < r\<close> |
13 Where: \<open>0 < r\<close> |
14 Find: \<open>Maximum A\<close> \<open>AdditionalValues [u, v]\<close> |
14 Find: \<open>Maximum A\<close> \<open>AdditionalValues [u, v]\<close> |
24 |
24 |
25 subsubsection \<open>Specification step by step\<close> |
25 subsubsection \<open>Specification step by step\<close> |
26 |
26 |
27 text \<open> |
27 text \<open> |
28 In an electronic textbook there shall be references to examples given, for instance, |
28 In an electronic textbook there shall be references to examples given, for instance, |
29 by \<open>Example "Diff_App/No.123 a"\<close>. Such a reference shall be easily "activated" |
29 by \<open>Example "Diff_App-No.123a"\<close>. Such a reference shall be easily "activated" |
30 to start a Solution at the spot ?and?or? to open a separate window. |
30 to start a Solution at the spot ?and?or? to open a separate window. |
31 |
31 |
32 Activating the reference \<open>Example "Diff_App/No.123 a"\<close> shall result in a threefold alternative, |
32 Activating the reference \<open>Example "Diff_App-No.123a"\<close> shall result in a threefold alternative, |
33 where (2)=(3) for the parsers: |
33 where (2)=(3) for the parsers: |
34 (1) the Example presents a "normal problem" with a Specification (preferred by engineers), |
34 (1) the Example presents a "normal problem" with a Specification (preferred by engineers), |
35 see above subsubsection \<open>Empty Specification\<close>, |
35 see above subsubsection \<open>Empty Specification\<close>, |
36 (2) the Example presents a "normal problem" without a Specification (preferred in high-school): |
36 (2) the Example presents a "normal problem" without a Specification (preferred in high-school): |
37 |Example "Diff_App/No.123 a" |
37 |Example "Diff_App-No.123a" |
38 | Specification: |
38 | Specification: |
39 | Solution: |
39 | Solution: |
40 | ..first formula as given by the specifid Method.. |
40 | ..first formula as given by the specifid Method.. |
41 (3) the Example presents a "CAS_Cmd": |
41 (3) the Example presents a "CAS_Cmd": |
42 |Example "Linear_Equation/No.123 a" |
42 |Example "Linear_Equation/No.123 a" |
60 # 1: ISAC starts the Example by presenting an "empty" Specification: |
60 # 1: ISAC starts the Example by presenting an "empty" Specification: |
61 \<close> |
61 \<close> |
62 ML \<open> (* # 1: At the first call of \<open>Example\<close> ISAC initialises a calculation *) |
62 ML \<open> (* # 1: At the first call of \<open>Example\<close> ISAC initialises a calculation *) |
63 val p = ([], Pos.Pbl); |
63 val p = ([], Pos.Pbl); |
64 val pt = update_state (*here we have Ctree.EmptyPtree and thus call init_ctree*) |
64 val pt = update_state (*here we have Ctree.EmptyPtree and thus call init_ctree*) |
65 ("Diff_App/No.123 a", |
65 ("Diff_App-No.123a", |
66 (* Problem.parse_model_input results in markup, which is accepted by \<open>fun update_state\<close>, too: |
66 (* Problem.parse_model_input results in markup, which is accepted by \<open>fun update_state\<close>, too: |
67 Constants [r = 7] *) |
67 Constants [r = 7] *) |
68 ( [("#Given", ["Constants [r = 7]"]), |
68 ( [("#Given", ["Constants [r = 7]"]), |
69 ("#Where", ["0 < r"]), |
69 ("#Where", ["0 < r"]), |
70 ("#Find", ["Maximum A", "AdditionalValues [u, v]"]), |
70 ("#Find", ["Maximum A", "AdditionalValues [u, v]"]), |
75 (*References_Def.explode_id ^^^^^^^^^^^^^^^^^^^^^^, ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) |
75 (*References_Def.explode_id ^^^^^^^^^^^^^^^^^^^^^^, ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) |
76 ) |
76 ) |
77 ) Ctree.EmptyPtree; |
77 ) Ctree.EmptyPtree; |
78 val ptp = (pt, p); |
78 val ptp = (pt, p); |
79 \<close> |
79 \<close> |
80 Example "Diff_App/No.123 a" |
80 Example "Diff_App-No.123a" |
81 Specification: |
81 Specification: |
82 Model: |
82 Model: |
83 Given: \<open>Constants [r = 7]\<close> |
83 Given: \<open>Constants [r = 7]\<close> |
84 Where: \<open>0 < r\<close> |
84 Where: \<open>0 < r\<close> |
85 Find: \<open>Maximum _\<close> \<open>AdditionalValues [_]\<close> |
85 Find: \<open>Maximum _\<close> \<open>AdditionalValues [_]\<close> |
97 \<close> |
97 \<close> |
98 ML \<open> (* # 2: ISAC suggests a next item on request *) |
98 ML \<open> (* # 2: ISAC suggests a next item on request *) |
99 val ("ok", ([(Tactic.Add_Given "Constants [r = 7]", _, _)], _, ptp)) |
99 val ("ok", ([(Tactic.Add_Given "Constants [r = 7]", _, _)], _, ptp)) |
100 = Step.specify_do_next ptp; |
100 = Step.specify_do_next ptp; |
101 \<close> |
101 \<close> |
102 Example "Diff_App/No.123 a" |
102 Example "Diff_App-No.123a" |
103 Specification: |
103 Specification: |
104 Model: |
104 Model: |
105 Given: \<open>Constants r = 7\<close> |
105 Given: \<open>Constants r = 7\<close> |
106 Where: \<open>0 < r\<close> |
106 Where: \<open>0 < r\<close> |
107 Find: \<open>Maximum _\<close> \<open>AdditionalValues [_]\<close> |
107 Find: \<open>Maximum _\<close> \<open>AdditionalValues [_]\<close> |
120 \<close> |
120 \<close> |
121 ML \<open> (* 3: ISAC suggests a next item within a term list *) |
121 ML \<open> (* 3: ISAC suggests a next item within a term list *) |
122 val ("ok", ([(Tactic.Add_Find "Maximum A", _, _)], _, ptp)) |
122 val ("ok", ([(Tactic.Add_Find "Maximum A", _, _)], _, ptp)) |
123 = Step.specify_do_next ptp; |
123 = Step.specify_do_next ptp; |
124 \<close> |
124 \<close> |
125 Example "Diff_App/No.123 a" |
125 Example "Diff_App-No.123a" |
126 Specification: |
126 Specification: |
127 Model: |
127 Model: |
128 Given: \<open>Constants r = 7\<close> |
128 Given: \<open>Constants r = 7\<close> |
129 Where: \<open>0 < r\<close> |
129 Where: \<open>0 < r\<close> |
130 Find: \<open>Maximum _\<close> \<open>AdditionalValues [u]\<close> |
130 Find: \<open>Maximum _\<close> \<open>AdditionalValues [u]\<close> |
143 ML \<open> (* # 4: ISAC suggests a next step on request, even a next element within a list *) |
143 ML \<open> (* # 4: ISAC suggests a next step on request, even a next element within a list *) |
144 val ("ok", ([(Tactic.Add_Find "AdditionalValues [u]", _, _)], _, ptp)) |
144 val ("ok", ([(Tactic.Add_Find "AdditionalValues [u]", _, _)], _, ptp)) |
145 = Step.specify_do_next ptp; |
145 = Step.specify_do_next ptp; |
146 \<close> |
146 \<close> |
147 |
147 |
148 Example "Diff_App/No.123 a" |
148 Example "Diff_App-No.123a" |
149 Specification: |
149 Specification: |
150 Model: |
150 Model: |
151 Given: \<open>Constants r = 7\<close> |
151 Given: \<open>Constants r = 7\<close> |
152 Where: \<open>0 < r\<close> |
152 Where: \<open>0 < r\<close> |
153 Find: \<open>Maximum _\<close> \<open>AdditionalValues [u, v]\<close> |
153 Find: \<open>Maximum _\<close> \<open>AdditionalValues [u, v]\<close> |
163 text \<open> |
163 text \<open> |
164 # 5: Input to \<open>Problem_Ref\<close> is according to the (hidden) formalisation: |
164 # 5: Input to \<open>Problem_Ref\<close> is according to the (hidden) formalisation: |
165 \<close> |
165 \<close> |
166 ML \<open> (* # 5: Input to \<open>Problem_Ref\<close> might change the \<open>Model\<close> *) |
166 ML \<open> (* # 5: Input to \<open>Problem_Ref\<close> might change the \<open>Model\<close> *) |
167 \<close> |
167 \<close> |
168 Example "Diff_App/No.123 a" |
168 Example "Diff_App-No.123a" |
169 Specification: |
169 Specification: |
170 Model: |
170 Model: |
171 Given: \<open>Constants r = 7\<close> |
171 Given: \<open>Constants r = 7\<close> |
172 Where: \<open>0 < r\<close> |
172 Where: \<open>0 < r\<close> |
173 Find: \<open>Maximum _\<close> \<open>AdditionalValues [u, v]\<close> |
173 Find: \<open>Maximum _\<close> \<open>AdditionalValues [u, v]\<close> |
186 direct manipulation of \<open>\<Otimes>\<close> and \<open>\<Odot>\<close>. |
186 direct manipulation of \<open>\<Otimes>\<close> and \<open>\<Odot>\<close>. |
187 \<close> |
187 \<close> |
188 ML \<open> (* # 6: Input to \<open>Method_Ref\<close> changes the \<open>Model\<close> to the respective \<open>Method\<close> *) |
188 ML \<open> (* # 6: Input to \<open>Method_Ref\<close> changes the \<open>Model\<close> to the respective \<open>Method\<close> *) |
189 \<close> |
189 \<close> |
190 text \<open> --- remove this line and make content Isar input---\ |
190 text \<open> --- remove this line and make content Isar input---\ |
191 Example "Diff_App/No.123 a" |
191 Example "Diff_App-No.123a" |
192 Specification: |
192 Specification: |
193 Model: GOON: lookup model of method GOON GOON GOON GOON GOON! |
193 Model: GOON: lookup model of method GOON GOON GOON GOON GOON! |
194 Given: \<open>Constants r = 7\<close> |
194 Given: \<open>Constants r = 7\<close> |
195 Where: \<open>0 < r\<close> |
195 Where: \<open>0 < r\<close> |
196 Find: \<open>Maximum _\<close> \<open>AdditionalValues [u, v]\<close> |
196 Find: \<open>Maximum _\<close> \<open>AdditionalValues [u, v]\<close> |