1.1 --- a/test/Tools/isac/Test_Some.thy Thu Jan 14 16:14:27 2021 +0100
1.2 +++ b/test/Tools/isac/Test_Some.thy Sun Jan 17 13:16:25 2021 +0100
1.3 @@ -119,6 +119,435 @@
1.4 (*1*)
1.5 Solution:
1.6
1.7 +subsection \<open><Output> BY CLICK ON Problem..Specification\<close>
1.8 +text \<open>
1.9 + Comparison of the two subsections below:
1.10 +(1) <Output> AFTER session Isac (after ./zcoding-to-test.sh) WITH click on Problem..Specification:
1.11 + ((WHILE click ON Example SHOWS NO ERROR))
1.12 +# headline = ..(1) == (2) ..PARSED + Specification
1.13 +# i_model = Inc ..IN 4 ELEMENTS, (1) == (2) ..?!? FROM PARSED ?!?
1.14 +# o_model = COMPLETE WITH 7 ELEMENTS ..FROM Example
1.15 +# refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])..FROM References
1.16 +
1.17 +(2) <Output> WITHOUT session Isac (after ./ztest-to-coding.sh) WITH click on Problem..Specification:
1.18 + ((WHILE click ON Example SHOWS !!! ERROR))
1.19 +# headline = ..(1) == (2) ..PARSED + Specification
1.20 +# i_model = Inc ..IN 4 ELEMENTS, (1) == (2) ..?!? FROM PARSED ?!?
1.21 +# o_model = [] ..NO Example
1.22 +# refs = ("Biegelinie", ["Biegelinien"], ["empty_meth_id"]) ..FROM headline ONLY
1.23 +\<close>
1.24 +
1.25 +subsubsection \<open>(1) WITH session Isac (AFTER ./zcoding-to-test.sh)\<close>
1.26 +text \<open>
1.27 +{a = "//--- Spark_Commands.prove_vc", headline =
1.28 + (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),
1.29 + ((((("Specification", ":"),
1.30 + ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]),
1.31 + "Where"),
1.32 + ":"),
1.33 + ["<markup>", "<markup>"]),
1.34 + "Find"),
1.35 + ":"),
1.36 + "<markup>"),
1.37 + "Relate"),
1.38 + ":"),
1.39 + ["<markup>"]),
1.40 + (("References", ":"),
1.41 + (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),
1.42 + "Solution"),
1.43 + ":"),
1.44 + [])),
1.45 + "")} (line 677 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
1.46 +{a = "prove_vc", i_model =
1.47 + [(0, [], false, "#Given",
1.48 + Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
1.49 + (0, [], false, "#Given",
1.50 + Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
1.51 + (0, [], false, "#Find",
1.52 + Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []),
1.53 + (Const ("empty", "??.'a"), []))),
1.54 + (0, [], false, "#Relate",
1.55 + Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []),
1.56 + (Const ("empty", "??.'a"), [])))],
1.57 + o_model =
1.58 + [(1, [1], "#Given", Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), [Free ("L", "real")]),
1.59 + (2, [1], "#Given", Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), [Free ("q_0", "real")]),
1.60 + (3, [1], "#Find", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"),
1.61 + [Free ("y", "real \<Rightarrow> real")]),
1.62 + (4, [1], "#Relate", Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"),
1.63 + [Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
1.64 + (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("0", "real")) $
1.65 + Free ("0", "real")) $
1.66 + Const ("List.list.Nil", "bool list"),
1.67 + Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
1.68 + (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("L", "real")) $
1.69 + Free ("0", "real")) $
1.70 + Const ("List.list.Nil", "bool list"),
1.71 + Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
1.72 + (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
1.73 + (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("0", "real")) $ Free ("0", "real")) $
1.74 + Const ("List.list.Nil", "bool list"),
1.75 + Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
1.76 + (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
1.77 + (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("L", "real")) $ Free ("0", "real")) $
1.78 + Const ("List.list.Nil", "bool list")]),
1.79 + (5, [1], "#undef", Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), [Free ("x", "real")]),
1.80 + (6, [1], "#undef", Const ("Biegelinie.GleichungsVariablen", "real list \<Rightarrow> una"),
1.81 + [Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $
1.82 + Const ("List.list.Nil", "real list"),
1.83 + Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_2", "real") $
1.84 + Const ("List.list.Nil", "real list"),
1.85 + Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_3", "real") $
1.86 + Const ("List.list.Nil", "real list"),
1.87 + Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_4", "real") $
1.88 + Const ("List.list.Nil", "real list")]),
1.89 + (7, [1], "#undef", Const ("Biegelinie.AbleitungBiegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"),
1.90 + [Free ("dy", "real \<Rightarrow> real")])],
1.91 + refs =
1.92 + ("Biegelinie", ["Biegelinien"],
1.93 + ["IntegrierenUndKonstanteBestimmen2"])} (line 690 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
1.94 +### Proof_Context.gen_fixes
1.95 +### Proof_Context.gen_fixes
1.96 +### Proof_Context.gen_fixes
1.97 +### Syntax_Phases.check_terms
1.98 +### Syntax_Phases.check_typs
1.99 +### Syntax_Phases.check_typs
1.100 +### Syntax_Phases.check_typs
1.101 +## calling Output.report
1.102 +#### Syntax_Phases.check_props
1.103 +### Syntax_Phases.check_terms
1.104 +### Syntax_Phases.check_typs
1.105 +### Syntax_Phases.check_typs
1.106 +## calling Output.report
1.107 +#### Syntax_Phases.check_props
1.108 +### Syntax_Phases.check_terms
1.109 +### Syntax_Phases.check_typs
1.110 +### Syntax_Phases.check_typs
1.111 +## calling Output.report
1.112 +#### Syntax_Phases.check_props
1.113 +### Syntax_Phases.check_terms
1.114 +### Syntax_Phases.check_typs
1.115 +### Syntax_Phases.check_typs
1.116 +## calling Output.report
1.117 +#### Syntax_Phases.check_props
1.118 +### Syntax_Phases.check_terms
1.119 +### Syntax_Phases.check_typs
1.120 +### Syntax_Phases.check_typs
1.121 +## calling Output.report
1.122 +#### Syntax_Phases.check_props
1.123 +### Syntax_Phases.check_terms
1.124 +### Syntax_Phases.check_typs
1.125 +### Syntax_Phases.check_typs
1.126 +## calling Output.report
1.127 +#### Syntax_Phases.check_props
1.128 +### Syntax_Phases.check_terms
1.129 +### Syntax_Phases.check_typs
1.130 +### Syntax_Phases.check_typs
1.131 +## calling Output.report
1.132 +#### Syntax_Phases.check_props
1.133 +### Syntax_Phases.check_terms
1.134 +### Syntax_Phases.check_typs
1.135 +### Syntax_Phases.check_typs
1.136 +## calling Output.report
1.137 +#### Syntax_Phases.check_props
1.138 +### Syntax_Phases.check_terms
1.139 +### Syntax_Phases.check_typs
1.140 +### Syntax_Phases.check_typs
1.141 +## calling Output.report
1.142 +#### Syntax_Phases.check_props
1.143 +### Syntax_Phases.check_terms
1.144 +### Syntax_Phases.check_typs
1.145 +### Syntax_Phases.check_typs
1.146 +## calling Output.report
1.147 +#### Syntax_Phases.check_props
1.148 +### Syntax_Phases.check_terms
1.149 +### Syntax_Phases.check_typs
1.150 +### Syntax_Phases.check_typs
1.151 +## calling Output.report
1.152 +#### Syntax_Phases.check_props
1.153 +### Syntax_Phases.check_terms
1.154 +### Syntax_Phases.check_typs
1.155 +### Syntax_Phases.check_typs
1.156 +## calling Output.report
1.157 +#### Syntax_Phases.check_props
1.158 +### Syntax_Phases.check_terms
1.159 +### Syntax_Phases.check_typs
1.160 +### Syntax_Phases.check_typs
1.161 +## calling Output.report
1.162 +#### Syntax_Phases.check_props
1.163 +### Syntax_Phases.check_terms
1.164 +### Syntax_Phases.check_typs
1.165 +### Syntax_Phases.check_typs
1.166 +## calling Output.report
1.167 +#### Syntax_Phases.check_props
1.168 +### Syntax_Phases.check_terms
1.169 +### Syntax_Phases.check_typs
1.170 +### Syntax_Phases.check_typs
1.171 +## calling Output.report
1.172 +#### Syntax_Phases.check_props
1.173 +### Syntax_Phases.check_terms
1.174 +### Syntax_Phases.check_typs
1.175 +### Syntax_Phases.check_typs
1.176 +## calling Output.report
1.177 +#### Syntax_Phases.check_props
1.178 +### Syntax_Phases.check_terms
1.179 +### Syntax_Phases.check_typs
1.180 +### Syntax_Phases.check_typs
1.181 +## calling Output.report
1.182 +#### Syntax_Phases.check_props
1.183 +### Syntax_Phases.check_terms
1.184 +### Syntax_Phases.check_typs
1.185 +### Syntax_Phases.check_typs
1.186 +## calling Output.report
1.187 +#### Syntax_Phases.check_props
1.188 +### Syntax_Phases.check_terms
1.189 +### Syntax_Phases.check_typs
1.190 +### Syntax_Phases.check_typs
1.191 +## calling Output.report
1.192 +#### Syntax_Phases.check_props
1.193 +### Syntax_Phases.check_terms
1.194 +### Syntax_Phases.check_typs
1.195 +### Syntax_Phases.check_typs
1.196 +## calling Output.report
1.197 +#### Syntax_Phases.check_props
1.198 +### Syntax_Phases.check_terms
1.199 +### Syntax_Phases.check_typs
1.200 +### Syntax_Phases.check_typs
1.201 +## calling Output.report
1.202 +#### Syntax_Phases.check_props
1.203 +### Syntax_Phases.check_terms
1.204 +### Syntax_Phases.check_typs
1.205 +### Syntax_Phases.check_typs
1.206 +## calling Output.report
1.207 +#### Syntax_Phases.check_props
1.208 +### Syntax_Phases.check_terms
1.209 +### Syntax_Phases.check_typs
1.210 +### Syntax_Phases.check_typs
1.211 +### Syntax_Phases.check_typs
1.212 +## calling Output.report
1.213 +#### Syntax_Phases.check_props
1.214 +### Syntax_Phases.check_terms
1.215 +### Syntax_Phases.check_typs
1.216 +### Syntax_Phases.check_typs
1.217 +### Syntax_Phases.check_typs
1.218 +## calling Output.report
1.219 +### Syntax_Phases.check_terms
1.220 +### Syntax_Phases.check_typs
1.221 +### Syntax_Phases.check_typs
1.222 +### Syntax_Phases.check_typs
1.223 +## calling Output.report
1.224 +### Syntax_Phases.check_terms
1.225 +### Syntax_Phases.check_typs
1.226 +### Syntax_Phases.check_typs
1.227 +### Syntax_Phases.check_typs
1.228 +## calling Output.report
1.229 +### Syntax_Phases.check_terms
1.230 +### Syntax_Phases.check_typs
1.231 +### Syntax_Phases.check_typs
1.232 +### Syntax_Phases.check_typs
1.233 +## calling Output.report
1.234 +### Syntax_Phases.check_terms
1.235 +### Syntax_Phases.check_typs
1.236 +### Syntax_Phases.check_typs
1.237 +### Syntax_Phases.check_typs
1.238 +## calling Output.report
1.239 +### Syntax_Phases.check_terms
1.240 +### Syntax_Phases.check_typs
1.241 +### Syntax_Phases.check_typs
1.242 +### Syntax_Phases.check_typs
1.243 +## calling Output.report
1.244 +### Proof_Context.gen_fixes
1.245 +### Proof_Context.gen_fixes
1.246 +\<close>
1.247 +
1.248 +subsubsection \<open>(2) WITHOUT session Isac (AFTER ./ztest-to-coding.sh)\<close>
1.249 +text \<open>
1.250 +{a = "//--- Spark_Commands.prove_vc", headline =
1.251 + (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),
1.252 + ((((("Specification", ":"),
1.253 + ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]),
1.254 + "Where"),
1.255 + ":"),
1.256 + ["<markup>", "<markup>"]),
1.257 + "Find"),
1.258 + ":"),
1.259 + "<markup>"),
1.260 + "Relate"),
1.261 + ":"),
1.262 + ["<markup>"]),
1.263 + (("References", ":"),
1.264 + (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),
1.265 + "Solution"),
1.266 + ":"),
1.267 + [])),
1.268 + "")}
1.269 +{a = "prove_vc", i_model =
1.270 + [(0, [], false, "#Given",
1.271 + Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
1.272 + (0, [], false, "#Given",
1.273 + Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
1.274 + (0, [], false, "#Find",
1.275 + Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []),
1.276 + (Const ("empty", "??.'a"), []))),
1.277 + (0, [], false, "#Relate",
1.278 + Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []),
1.279 + (Const ("empty", "??.'a"), [])))],
1.280 + o_model = [], refs = ("Biegelinie", ["Biegelinien"], ["empty_meth_id"])}
1.281 +### Proof_Context.gen_fixes
1.282 +### Proof_Context.gen_fixes
1.283 +### Proof_Context.gen_fixes
1.284 +### Syntax_Phases.check_terms
1.285 +### Syntax_Phases.check_typs
1.286 +### Syntax_Phases.check_typs
1.287 +### Syntax_Phases.check_typs
1.288 +## calling Output.report
1.289 +#### Syntax_Phases.check_props
1.290 +### Syntax_Phases.check_terms
1.291 +### Syntax_Phases.check_typs
1.292 +### Syntax_Phases.check_typs
1.293 +## calling Output.report
1.294 +#### Syntax_Phases.check_props
1.295 +### Syntax_Phases.check_terms
1.296 +### Syntax_Phases.check_typs
1.297 +### Syntax_Phases.check_typs
1.298 +## calling Output.report
1.299 +#### Syntax_Phases.check_props
1.300 +### Syntax_Phases.check_terms
1.301 +### Syntax_Phases.check_typs
1.302 +### Syntax_Phases.check_typs
1.303 +## calling Output.report
1.304 +#### Syntax_Phases.check_props
1.305 +### Syntax_Phases.check_terms
1.306 +### Syntax_Phases.check_typs
1.307 +### Syntax_Phases.check_typs
1.308 +## calling Output.report
1.309 +#### Syntax_Phases.check_props
1.310 +### Syntax_Phases.check_terms
1.311 +### Syntax_Phases.check_typs
1.312 +### Syntax_Phases.check_typs
1.313 +## calling Output.report
1.314 +#### Syntax_Phases.check_props
1.315 +### Syntax_Phases.check_terms
1.316 +### Syntax_Phases.check_typs
1.317 +### Syntax_Phases.check_typs
1.318 +## calling Output.report
1.319 +#### Syntax_Phases.check_props
1.320 +### Syntax_Phases.check_terms
1.321 +### Syntax_Phases.check_typs
1.322 +### Syntax_Phases.check_typs
1.323 +## calling Output.report
1.324 +#### Syntax_Phases.check_props
1.325 +### Syntax_Phases.check_terms
1.326 +### Syntax_Phases.check_typs
1.327 +### Syntax_Phases.check_typs
1.328 +## calling Output.report
1.329 +#### Syntax_Phases.check_props
1.330 +### Syntax_Phases.check_terms
1.331 +### Syntax_Phases.check_typs
1.332 +### Syntax_Phases.check_typs
1.333 +## calling Output.report
1.334 +#### Syntax_Phases.check_props
1.335 +### Syntax_Phases.check_terms
1.336 +### Syntax_Phases.check_typs
1.337 +### Syntax_Phases.check_typs
1.338 +## calling Output.report
1.339 +#### Syntax_Phases.check_props
1.340 +### Syntax_Phases.check_terms
1.341 +### Syntax_Phases.check_typs
1.342 +### Syntax_Phases.check_typs
1.343 +## calling Output.report
1.344 +#### Syntax_Phases.check_props
1.345 +### Syntax_Phases.check_terms
1.346 +### Syntax_Phases.check_typs
1.347 +### Syntax_Phases.check_typs
1.348 +## calling Output.report
1.349 +#### Syntax_Phases.check_props
1.350 +### Syntax_Phases.check_terms
1.351 +### Syntax_Phases.check_typs
1.352 +### Syntax_Phases.check_typs
1.353 +## calling Output.report
1.354 +#### Syntax_Phases.check_props
1.355 +### Syntax_Phases.check_terms
1.356 +### Syntax_Phases.check_typs
1.357 +### Syntax_Phases.check_typs
1.358 +## calling Output.report
1.359 +#### Syntax_Phases.check_props
1.360 +### Syntax_Phases.check_terms
1.361 +### Syntax_Phases.check_typs
1.362 +### Syntax_Phases.check_typs
1.363 +## calling Output.report
1.364 +#### Syntax_Phases.check_props
1.365 +### Syntax_Phases.check_terms
1.366 +### Syntax_Phases.check_typs
1.367 +### Syntax_Phases.check_typs
1.368 +## calling Output.report
1.369 +#### Syntax_Phases.check_props
1.370 +### Syntax_Phases.check_terms
1.371 +### Syntax_Phases.check_typs
1.372 +### Syntax_Phases.check_typs
1.373 +## calling Output.report
1.374 +#### Syntax_Phases.check_props
1.375 +### Syntax_Phases.check_terms
1.376 +### Syntax_Phases.check_typs
1.377 +### Syntax_Phases.check_typs
1.378 +## calling Output.report
1.379 +#### Syntax_Phases.check_props
1.380 +### Syntax_Phases.check_terms
1.381 +### Syntax_Phases.check_typs
1.382 +### Syntax_Phases.check_typs
1.383 +## calling Output.report
1.384 +#### Syntax_Phases.check_props
1.385 +### Syntax_Phases.check_terms
1.386 +### Syntax_Phases.check_typs
1.387 +### Syntax_Phases.check_typs
1.388 +## calling Output.report
1.389 +#### Syntax_Phases.check_props
1.390 +### Syntax_Phases.check_terms
1.391 +### Syntax_Phases.check_typs
1.392 +### Syntax_Phases.check_typs
1.393 +## calling Output.report
1.394 +#### Syntax_Phases.check_props
1.395 +### Syntax_Phases.check_terms
1.396 +### Syntax_Phases.check_typs
1.397 +### Syntax_Phases.check_typs
1.398 +### Syntax_Phases.check_typs
1.399 +## calling Output.report
1.400 +#### Syntax_Phases.check_props
1.401 +### Syntax_Phases.check_terms
1.402 +### Syntax_Phases.check_typs
1.403 +### Syntax_Phases.check_typs
1.404 +### Syntax_Phases.check_typs
1.405 +## calling Output.report
1.406 +### Syntax_Phases.check_terms
1.407 +### Syntax_Phases.check_typs
1.408 +### Syntax_Phases.check_typs
1.409 +### Syntax_Phases.check_typs
1.410 +## calling Output.report
1.411 +### Syntax_Phases.check_terms
1.412 +### Syntax_Phases.check_typs
1.413 +### Syntax_Phases.check_typs
1.414 +### Syntax_Phases.check_typs
1.415 +## calling Output.report
1.416 +### Syntax_Phases.check_terms
1.417 +### Syntax_Phases.check_typs
1.418 +### Syntax_Phases.check_typs
1.419 +### Syntax_Phases.check_typs
1.420 +## calling Output.report
1.421 +### Syntax_Phases.check_terms
1.422 +### Syntax_Phases.check_typs
1.423 +### Syntax_Phases.check_typs
1.424 +### Syntax_Phases.check_typs
1.425 +## calling Output.report
1.426 +### Syntax_Phases.check_terms
1.427 +### Syntax_Phases.check_typs
1.428 +### Syntax_Phases.check_typs
1.429 +### Syntax_Phases.check_typs
1.430 +## calling Output.report
1.431 +### Proof_Context.gen_fixes
1.432 +### Proof_Context.gen_fixes
1.433 +\<close>
1.434 +
1.435 +subsection \<open>How complete must SPARK's sequence of keywords be?\<close>
1.436 ML \<open>
1.437 (*
1.438 AT ABOVE "ML" WE HAVE:
1.439 @@ -150,99 +579,6 @@
1.440
1.441 ( *\\--------- SPARK keywords do work IF THERE IS NO spark_open ABOVE.. ----------------------//*)
1.442
1.443 -subsection \<open>result Problem 1: got data from Example\<close>
1.444 -text \<open>
1.445 -trace:
1.446 -
1.447 -{a = "//--- Spark_Commands.prove_vc", o_model =
1.448 - [(1, [1], "#Given", Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), [Free ("L", "real")]), (2, [1], "#Given", Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), [Free ("q_0", "real")]),
1.449 - (3, [1], "#Find", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]),
1.450 - (4, [1], "#Relate", Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"),
1.451 - [Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $ (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("0", "real")) $ Free ("0", "real")) $
1.452 - Const ("List.list.Nil", "bool list"),
1.453 - Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $ (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("L", "real")) $ Free ("0", "real")) $
1.454 - Const ("List.list.Nil", "bool list"),
1.455 - Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $ (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("0", "real")) $ Free ("0", "real")) $
1.456 - Const ("List.list.Nil", "bool list"),
1.457 - Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $ (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("L", "real")) $ Free ("0", "real")) $
1.458 - Const ("List.list.Nil", "bool list")]),
1.459 - (5, [1], "#undef", Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), [Free ("x", "real")]),
1.460 - (6, [1], "#undef", Const ("Biegelinie.GleichungsVariablen", "real list \<Rightarrow> una"),
1.461 - [Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $ Const ("List.list.Nil", "real list"),
1.462 - Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_2", "real") $ Const ("List.list.Nil", "real list"),
1.463 - Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_3", "real") $ Const ("List.list.Nil", "real list"),
1.464 - Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_4", "real") $ Const ("List.list.Nil", "real list")]),
1.465 - (7, [1], "#undef", Const ("Biegelinie.AbleitungBiegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("dy", "real \<Rightarrow> real")])],
1.466 - refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])} (line 654 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
1.467 -*)
1.468 -\<close>
1.469 -
1.470 -subsection \<open>result Problem 2: initial Specification parsed\<close>
1.471 -text \<open>
1.472 - Note: this kind of parsing is inappropriate with respect to integration:
1.473 - the Position.T are dropped, so no feedback can be allocated.
1.474 -
1.475 - trace:
1.476 -
1.477 -### Private_Output.report keyword1
1.478 -{a = "//--- Spark_Commands.prove_vc", headline =
1.479 - (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),
1.480 - ((((("Specification", ":"),
1.481 - ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]), "Where"), ":"),
1.482 - ["<markup>", "<markup>"]),
1.483 - "Find"),
1.484 - ":"),
1.485 - "<markup>"),
1.486 - "Relate"),
1.487 - ":"),
1.488 - ["<markup>"]),
1.489 - (("References", ":"), (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),
1.490 - "Solution"),
1.491 - ":"),
1.492 - [])),
1.493 - "")} (line 677 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
1.494 -{a = "prove_vc", i_model =
1.495 - [(0, [], false, "#Given", Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
1.496 - (0, [], false, "#Given", Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
1.497 - (0, [], false, "#Find", Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
1.498 - (0, [], false, "#Relate",
1.499 - Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []), (Const ("empty", "??.'a"), [])))],
1.500 - o_model =
1.501 - [(1, [1], "#Given", Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), [Free ("L", "real")]),
1.502 - (2, [1], "#Given", Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), [Free ("q_0", "real")]),
1.503 - (3, [1], "#Find", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]),
1.504 - (4, [1], "#Relate", Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"),
1.505 - [Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
1.506 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("0", "real")) $ Free ("0", "real")) $
1.507 - Const ("List.list.Nil", "bool list"),
1.508 - Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
1.509 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("L", "real")) $ Free ("0", "real")) $
1.510 - Const ("List.list.Nil", "bool list"),
1.511 - Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
1.512 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("0", "real")) $
1.513 - Free ("0", "real")) $
1.514 - Const ("List.list.Nil", "bool list"),
1.515 - Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
1.516 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("L", "real")) $
1.517 - Free ("0", "real")) $
1.518 - Const ("List.list.Nil", "bool list")]),
1.519 - (5, [1], "#undef", Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), [Free ("x", "real")]),
1.520 - (6, [1], "#undef", Const ("Biegelinie.GleichungsVariablen", "real list \<Rightarrow> una"),
1.521 - [Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $ Const ("List.list.Nil", "real list"),
1.522 - Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_2", "real") $ Const ("List.list.Nil", "real list"),
1.523 - Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_3", "real") $ Const ("List.list.Nil", "real list"),
1.524 - Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_4", "real") $ Const ("List.list.Nil", "real list")]),
1.525 - (7, [1], "#undef", Const ("Biegelinie.AbleitungBiegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("dy", "real \<Rightarrow> real")])],
1.526 - refs =
1.527 - ("Biegelinie", ["Biegelinien"],
1.528 - ["IntegrierenUndKonstanteBestimmen2"])} (line 690 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
1.529 -### Private_Output.report
1.530 -### Syntax_Phases.check_typs
1.531 -:
1.532 -### Syntax_Phases.check_terms
1.533 -:
1.534 -\<close>
1.535 -
1.536 section \<open>===================================================================================\<close>
1.537 ML \<open>
1.538 \<close> ML \<open>