step 5.5: for devel. make test-example independent from session Isac
note: see "HACKthy"
1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Fri Jan 22 14:56:44 2021 +0100
1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Fri Jan 22 16:03:15 2021 +0100
1.3 @@ -60,7 +60,8 @@
1.4 val _ =
1.5 Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file"
1.6 (Resources.provide_parse_files "Example" -- Parse.parname
1.7 - >> (Toplevel.theory o (Preliminary.load_formalisation ParseC.formalisation)));
1.8 + >> (Toplevel.theory o (*vvvvvvvvvvvvvvvvvvvv--- HACK: test independent from session Isac*)
1.9 + (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation)));
1.10 \<close> ML \<open>
1.11 val _ =
1.12 Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>Problem\<close>
1.13 @@ -73,59 +74,461 @@
1.14 \<close>
1.15
1.16 subsection \<open>test runs with Example\<close>
1.17 -subsubsection \<open>with new code\<close>
1.18 +
1.19 +Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>
1.20 +
1.21 +(*vvvvvvvv--- makes Outer_Syntax..Problem run; Isac code is just added*)
1.22 +spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>
1.23 +
1.24 +(*..Problem adds to SPARK..*)
1.25 +Problem (*procedure_g_c_d_4*)("Biegelinie", ["Biegelinien"])
1.26 + Specification:
1.27 +(*1*)
1.28 + Model:
1.29 + Given: "Traegerlaenge ", "Streckenlast "
1.30 + Where: "q_0 ist_integrierbar_auf {| 0, L |}", "0 < L"
1.31 + Find: "Biegelinie "
1.32 + Relate: "Randbedingungen "
1.33 + References:
1.34 + (*2*)
1.35 + RTheory: ""
1.36 + RProblem: ["", ""]
1.37 + RMethod: ["", ""]
1.38 + (*2*)
1.39 +(*1*)
1.40 + Solution:
1.41 +(*
1.42 + compare click on above Given: "Traegerlaenge ", "Streckenlast "
1.43 + with click on from \<open>0 < d\<close> in SPARK/../Greatest_Common_Divisorthy
1.44 +*)
1.45 +
1.46 +subsection \<open><Output> BY CLICK ON Problem..Solution\<close>
1.47 text \<open>
1.48 - Starting the Calculation for the Example requires session Isac with Isac.Biegelinie etc.
1.49 - So, do ~~$ ./zcoding-to-test.sh and use Test_Some.thy to evaluate
1.50 + Comparison of the two subsections below:
1.51 +(1) <Output> AFTER session Isac (after ./zcoding-to-test.sh) WITH click on Problem..Specification:
1.52 + ((WHILE click ON Example SHOWS NO ERROR))
1.53 +# headline = ..(1) == (2) ..PARSED + Specification
1.54 +# i_model = Inc ..IN 4 ELEMENTS, (1) == (2) ..?!? FROM PARSED ?!?
1.55 +# o_model = COMPLETE WITH 7 ELEMENTS ..FROM Example
1.56 +# refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])..FROM References
1.57
1.58 - Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>
1.59 -
1.60 - This now gives no error, but also no <Output>. See child of 3ea616c84845.
1.61 +(2) <Output> WITHOUT session Isac (after ./ztest-to-coding.sh) WITH click on Problem..Specification:
1.62 + ((WHILE click ON Example SHOWS !!! ERROR))
1.63 +# headline = ..(1) == (2) ..PARSED + Specification
1.64 +# i_model = Inc ..IN 4 ELEMENTS, (1) == (2) ..?!? FROM PARSED ?!?
1.65 +# o_model = [] ..NO Example
1.66 +# refs = ("Biegelinie", ["Biegelinien"], ["empty_meth_id"]) ..FROM headline ONLY
1.67 \<close>
1.68
1.69 -subsubsection \<open>with original SPARK code\<close>
1.70 +subsubsection \<open>(1) WITH session Isac (AFTER ./zcoding-to-test.sh)\<close>
1.71 text \<open>
1.72 - The sequence of code below is copied from SPARK/Examples/Gcd/Greatest_Common_Divisor.thy.
1.73 - But here the code works only partially (see ERROR at end).
1.74 - Thus it is advisable to run tests in Test_Some.thy, where "Example" has "Biegelinie".
1.75 +{a = "//--- Spark_Commands.prove_vc", headline =
1.76 + (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),
1.77 + ((((("Specification", ":"),
1.78 + ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]),
1.79 + "Where"),
1.80 + ":"),
1.81 + ["<markup>", "<markup>"]),
1.82 + "Find"),
1.83 + ":"),
1.84 + "<markup>"),
1.85 + "Relate"),
1.86 + ":"),
1.87 + ["<markup>"]),
1.88 + (("References", ":"),
1.89 + (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),
1.90 + "Solution"),
1.91 + ":"),
1.92 + [])),
1.93 + "")} (line 677 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
1.94 +{a = "prove_vc", i_model =
1.95 + [(0, [], false, "#Given",
1.96 + Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
1.97 + (0, [], false, "#Given",
1.98 + Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
1.99 + (0, [], false, "#Find",
1.100 + Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []),
1.101 + (Const ("empty", "??.'a"), []))),
1.102 + (0, [], false, "#Relate",
1.103 + Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []),
1.104 + (Const ("empty", "??.'a"), [])))],
1.105 + o_model =
1.106 + [(1, [1], "#Given", Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), [Free ("L", "real")]),
1.107 + (2, [1], "#Given", Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), [Free ("q_0", "real")]),
1.108 + (3, [1], "#Find", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"),
1.109 + [Free ("y", "real \<Rightarrow> real")]),
1.110 + (4, [1], "#Relate", Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"),
1.111 + [Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
1.112 + (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("0", "real")) $
1.113 + Free ("0", "real")) $
1.114 + Const ("List.list.Nil", "bool list"),
1.115 + Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
1.116 + (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("L", "real")) $
1.117 + Free ("0", "real")) $
1.118 + Const ("List.list.Nil", "bool list"),
1.119 + Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
1.120 + (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
1.121 + (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("0", "real")) $ Free ("0", "real")) $
1.122 + Const ("List.list.Nil", "bool list"),
1.123 + Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
1.124 + (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
1.125 + (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("L", "real")) $ Free ("0", "real")) $
1.126 + Const ("List.list.Nil", "bool list")]),
1.127 + (5, [1], "#undef", Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), [Free ("x", "real")]),
1.128 + (6, [1], "#undef", Const ("Biegelinie.GleichungsVariablen", "real list \<Rightarrow> una"),
1.129 + [Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $
1.130 + Const ("List.list.Nil", "real list"),
1.131 + Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_2", "real") $
1.132 + Const ("List.list.Nil", "real list"),
1.133 + Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_3", "real") $
1.134 + Const ("List.list.Nil", "real list"),
1.135 + Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_4", "real") $
1.136 + Const ("List.list.Nil", "real list")]),
1.137 + (7, [1], "#undef", Const ("Biegelinie.AbleitungBiegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"),
1.138 + [Free ("dy", "real \<Rightarrow> real")])],
1.139 + refs =
1.140 + ("Biegelinie", ["Biegelinien"],
1.141 + ["IntegrierenUndKonstanteBestimmen2"])} (line 690 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
1.142 +### Proof_Context.gen_fixes
1.143 +### Proof_Context.gen_fixes
1.144 +### Proof_Context.gen_fixes
1.145 +### Syntax_Phases.check_terms
1.146 +### Syntax_Phases.check_typs
1.147 +### Syntax_Phases.check_typs
1.148 +### Syntax_Phases.check_typs
1.149 +## calling Output.report
1.150 +#### Syntax_Phases.check_props
1.151 +### Syntax_Phases.check_terms
1.152 +### Syntax_Phases.check_typs
1.153 +### Syntax_Phases.check_typs
1.154 +## calling Output.report
1.155 +#### Syntax_Phases.check_props
1.156 +### Syntax_Phases.check_terms
1.157 +### Syntax_Phases.check_typs
1.158 +### Syntax_Phases.check_typs
1.159 +## calling Output.report
1.160 +#### Syntax_Phases.check_props
1.161 +### Syntax_Phases.check_terms
1.162 +### Syntax_Phases.check_typs
1.163 +### Syntax_Phases.check_typs
1.164 +## calling Output.report
1.165 +#### Syntax_Phases.check_props
1.166 +### Syntax_Phases.check_terms
1.167 +### Syntax_Phases.check_typs
1.168 +### Syntax_Phases.check_typs
1.169 +## calling Output.report
1.170 +#### Syntax_Phases.check_props
1.171 +### Syntax_Phases.check_terms
1.172 +### Syntax_Phases.check_typs
1.173 +### Syntax_Phases.check_typs
1.174 +## calling Output.report
1.175 +#### Syntax_Phases.check_props
1.176 +### Syntax_Phases.check_terms
1.177 +### Syntax_Phases.check_typs
1.178 +### Syntax_Phases.check_typs
1.179 +## calling Output.report
1.180 +#### Syntax_Phases.check_props
1.181 +### Syntax_Phases.check_terms
1.182 +### Syntax_Phases.check_typs
1.183 +### Syntax_Phases.check_typs
1.184 +## calling Output.report
1.185 +#### Syntax_Phases.check_props
1.186 +### Syntax_Phases.check_terms
1.187 +### Syntax_Phases.check_typs
1.188 +### Syntax_Phases.check_typs
1.189 +## calling Output.report
1.190 +#### Syntax_Phases.check_props
1.191 +### Syntax_Phases.check_terms
1.192 +### Syntax_Phases.check_typs
1.193 +### Syntax_Phases.check_typs
1.194 +## calling Output.report
1.195 +#### Syntax_Phases.check_props
1.196 +### Syntax_Phases.check_terms
1.197 +### Syntax_Phases.check_typs
1.198 +### Syntax_Phases.check_typs
1.199 +## calling Output.report
1.200 +#### Syntax_Phases.check_props
1.201 +### Syntax_Phases.check_terms
1.202 +### Syntax_Phases.check_typs
1.203 +### Syntax_Phases.check_typs
1.204 +## calling Output.report
1.205 +#### Syntax_Phases.check_props
1.206 +### Syntax_Phases.check_terms
1.207 +### Syntax_Phases.check_typs
1.208 +### Syntax_Phases.check_typs
1.209 +## calling Output.report
1.210 +#### Syntax_Phases.check_props
1.211 +### Syntax_Phases.check_terms
1.212 +### Syntax_Phases.check_typs
1.213 +### Syntax_Phases.check_typs
1.214 +## calling Output.report
1.215 +#### Syntax_Phases.check_props
1.216 +### Syntax_Phases.check_terms
1.217 +### Syntax_Phases.check_typs
1.218 +### Syntax_Phases.check_typs
1.219 +## calling Output.report
1.220 +#### Syntax_Phases.check_props
1.221 +### Syntax_Phases.check_terms
1.222 +### Syntax_Phases.check_typs
1.223 +### Syntax_Phases.check_typs
1.224 +## calling Output.report
1.225 +#### Syntax_Phases.check_props
1.226 +### Syntax_Phases.check_terms
1.227 +### Syntax_Phases.check_typs
1.228 +### Syntax_Phases.check_typs
1.229 +## calling Output.report
1.230 +#### Syntax_Phases.check_props
1.231 +### Syntax_Phases.check_terms
1.232 +### Syntax_Phases.check_typs
1.233 +### Syntax_Phases.check_typs
1.234 +## calling Output.report
1.235 +#### Syntax_Phases.check_props
1.236 +### Syntax_Phases.check_terms
1.237 +### Syntax_Phases.check_typs
1.238 +### Syntax_Phases.check_typs
1.239 +## calling Output.report
1.240 +#### Syntax_Phases.check_props
1.241 +### Syntax_Phases.check_terms
1.242 +### Syntax_Phases.check_typs
1.243 +### Syntax_Phases.check_typs
1.244 +## calling Output.report
1.245 +#### Syntax_Phases.check_props
1.246 +### Syntax_Phases.check_terms
1.247 +### Syntax_Phases.check_typs
1.248 +### Syntax_Phases.check_typs
1.249 +## calling Output.report
1.250 +#### Syntax_Phases.check_props
1.251 +### Syntax_Phases.check_terms
1.252 +### Syntax_Phases.check_typs
1.253 +### Syntax_Phases.check_typs
1.254 +## calling Output.report
1.255 +#### Syntax_Phases.check_props
1.256 +### Syntax_Phases.check_terms
1.257 +### Syntax_Phases.check_typs
1.258 +### Syntax_Phases.check_typs
1.259 +### Syntax_Phases.check_typs
1.260 +## calling Output.report
1.261 +#### Syntax_Phases.check_props
1.262 +### Syntax_Phases.check_terms
1.263 +### Syntax_Phases.check_typs
1.264 +### Syntax_Phases.check_typs
1.265 +### Syntax_Phases.check_typs
1.266 +## calling Output.report
1.267 +### Syntax_Phases.check_terms
1.268 +### Syntax_Phases.check_typs
1.269 +### Syntax_Phases.check_typs
1.270 +### Syntax_Phases.check_typs
1.271 +## calling Output.report
1.272 +### Syntax_Phases.check_terms
1.273 +### Syntax_Phases.check_typs
1.274 +### Syntax_Phases.check_typs
1.275 +### Syntax_Phases.check_typs
1.276 +## calling Output.report
1.277 +### Syntax_Phases.check_terms
1.278 +### Syntax_Phases.check_typs
1.279 +### Syntax_Phases.check_typs
1.280 +### Syntax_Phases.check_typs
1.281 +## calling Output.report
1.282 +### Syntax_Phases.check_terms
1.283 +### Syntax_Phases.check_typs
1.284 +### Syntax_Phases.check_typs
1.285 +### Syntax_Phases.check_typs
1.286 +## calling Output.report
1.287 +### Syntax_Phases.check_terms
1.288 +### Syntax_Phases.check_typs
1.289 +### Syntax_Phases.check_typs
1.290 +### Syntax_Phases.check_typs
1.291 +## calling Output.report
1.292 +### Proof_Context.gen_fixes
1.293 +### Proof_Context.gen_fixes
1.294 +\<close>
1.295
1.296 - spark_proof_functions is required for proof below..
1.297 +subsubsection \<open>(2) WITHOUT session Isac (AFTER ./ztest-to-coding.sh)\<close>
1.298 +text \<open>
1.299 +{a = "//--- Spark_Commands.prove_vc", headline =
1.300 + (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),
1.301 + ((((("Specification", ":"),
1.302 + ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]),
1.303 + "Where"),
1.304 + ":"),
1.305 + ["<markup>", "<markup>"]),
1.306 + "Find"),
1.307 + ":"),
1.308 + "<markup>"),
1.309 + "Relate"),
1.310 + ":"),
1.311 + ["<markup>"]),
1.312 + (("References", ":"),
1.313 + (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),
1.314 + "Solution"),
1.315 + ":"),
1.316 + [])),
1.317 + "")}
1.318 +{a = "prove_vc", i_model =
1.319 + [(0, [], false, "#Given",
1.320 + Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
1.321 + (0, [], false, "#Given",
1.322 + Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
1.323 + (0, [], false, "#Find",
1.324 + Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []),
1.325 + (Const ("empty", "??.'a"), []))),
1.326 + (0, [], false, "#Relate",
1.327 + Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []),
1.328 + (Const ("empty", "??.'a"), [])))],
1.329 + o_model = [], refs = ("Biegelinie", ["Biegelinien"], ["empty_meth_id"])}
1.330 +### Proof_Context.gen_fixes
1.331 +### Proof_Context.gen_fixes
1.332 +### Proof_Context.gen_fixes
1.333 +### Syntax_Phases.check_terms
1.334 +### Syntax_Phases.check_typs
1.335 +### Syntax_Phases.check_typs
1.336 +### Syntax_Phases.check_typs
1.337 +## calling Output.report
1.338 +#### Syntax_Phases.check_props
1.339 +### Syntax_Phases.check_terms
1.340 +### Syntax_Phases.check_typs
1.341 +### Syntax_Phases.check_typs
1.342 +## calling Output.report
1.343 +#### Syntax_Phases.check_props
1.344 +### Syntax_Phases.check_terms
1.345 +### Syntax_Phases.check_typs
1.346 +### Syntax_Phases.check_typs
1.347 +## calling Output.report
1.348 +#### Syntax_Phases.check_props
1.349 +### Syntax_Phases.check_terms
1.350 +### Syntax_Phases.check_typs
1.351 +### Syntax_Phases.check_typs
1.352 +## calling Output.report
1.353 +#### Syntax_Phases.check_props
1.354 +### Syntax_Phases.check_terms
1.355 +### Syntax_Phases.check_typs
1.356 +### Syntax_Phases.check_typs
1.357 +## calling Output.report
1.358 +#### Syntax_Phases.check_props
1.359 +### Syntax_Phases.check_terms
1.360 +### Syntax_Phases.check_typs
1.361 +### Syntax_Phases.check_typs
1.362 +## calling Output.report
1.363 +#### Syntax_Phases.check_props
1.364 +### Syntax_Phases.check_terms
1.365 +### Syntax_Phases.check_typs
1.366 +### Syntax_Phases.check_typs
1.367 +## calling Output.report
1.368 +#### Syntax_Phases.check_props
1.369 +### Syntax_Phases.check_terms
1.370 +### Syntax_Phases.check_typs
1.371 +### Syntax_Phases.check_typs
1.372 +## calling Output.report
1.373 +#### Syntax_Phases.check_props
1.374 +### Syntax_Phases.check_terms
1.375 +### Syntax_Phases.check_typs
1.376 +### Syntax_Phases.check_typs
1.377 +## calling Output.report
1.378 +#### Syntax_Phases.check_props
1.379 +### Syntax_Phases.check_terms
1.380 +### Syntax_Phases.check_typs
1.381 +### Syntax_Phases.check_typs
1.382 +## calling Output.report
1.383 +#### Syntax_Phases.check_props
1.384 +### Syntax_Phases.check_terms
1.385 +### Syntax_Phases.check_typs
1.386 +### Syntax_Phases.check_typs
1.387 +## calling Output.report
1.388 +#### Syntax_Phases.check_props
1.389 +### Syntax_Phases.check_terms
1.390 +### Syntax_Phases.check_typs
1.391 +### Syntax_Phases.check_typs
1.392 +## calling Output.report
1.393 +#### Syntax_Phases.check_props
1.394 +### Syntax_Phases.check_terms
1.395 +### Syntax_Phases.check_typs
1.396 +### Syntax_Phases.check_typs
1.397 +## calling Output.report
1.398 +#### Syntax_Phases.check_props
1.399 +### Syntax_Phases.check_terms
1.400 +### Syntax_Phases.check_typs
1.401 +### Syntax_Phases.check_typs
1.402 +## calling Output.report
1.403 +#### Syntax_Phases.check_props
1.404 +### Syntax_Phases.check_terms
1.405 +### Syntax_Phases.check_typs
1.406 +### Syntax_Phases.check_typs
1.407 +## calling Output.report
1.408 +#### Syntax_Phases.check_props
1.409 +### Syntax_Phases.check_terms
1.410 +### Syntax_Phases.check_typs
1.411 +### Syntax_Phases.check_typs
1.412 +## calling Output.report
1.413 +#### Syntax_Phases.check_props
1.414 +### Syntax_Phases.check_terms
1.415 +### Syntax_Phases.check_typs
1.416 +### Syntax_Phases.check_typs
1.417 +## calling Output.report
1.418 +#### Syntax_Phases.check_props
1.419 +### Syntax_Phases.check_terms
1.420 +### Syntax_Phases.check_typs
1.421 +### Syntax_Phases.check_typs
1.422 +## calling Output.report
1.423 +#### Syntax_Phases.check_props
1.424 +### Syntax_Phases.check_terms
1.425 +### Syntax_Phases.check_typs
1.426 +### Syntax_Phases.check_typs
1.427 +## calling Output.report
1.428 +#### Syntax_Phases.check_props
1.429 +### Syntax_Phases.check_terms
1.430 +### Syntax_Phases.check_typs
1.431 +### Syntax_Phases.check_typs
1.432 +## calling Output.report
1.433 +#### Syntax_Phases.check_props
1.434 +### Syntax_Phases.check_terms
1.435 +### Syntax_Phases.check_typs
1.436 +### Syntax_Phases.check_typs
1.437 +## calling Output.report
1.438 +#### Syntax_Phases.check_props
1.439 +### Syntax_Phases.check_terms
1.440 +### Syntax_Phases.check_typs
1.441 +### Syntax_Phases.check_typs
1.442 +## calling Output.report
1.443 +#### Syntax_Phases.check_props
1.444 +### Syntax_Phases.check_terms
1.445 +### Syntax_Phases.check_typs
1.446 +### Syntax_Phases.check_typs
1.447 +### Syntax_Phases.check_typs
1.448 +## calling Output.report
1.449 +#### Syntax_Phases.check_props
1.450 +### Syntax_Phases.check_terms
1.451 +### Syntax_Phases.check_typs
1.452 +### Syntax_Phases.check_typs
1.453 +### Syntax_Phases.check_typs
1.454 +## calling Output.report
1.455 +### Syntax_Phases.check_terms
1.456 +### Syntax_Phases.check_typs
1.457 +### Syntax_Phases.check_typs
1.458 +### Syntax_Phases.check_typs
1.459 +## calling Output.report
1.460 +### Syntax_Phases.check_terms
1.461 +### Syntax_Phases.check_typs
1.462 +### Syntax_Phases.check_typs
1.463 +### Syntax_Phases.check_typs
1.464 +## calling Output.report
1.465 +### Syntax_Phases.check_terms
1.466 +### Syntax_Phases.check_typs
1.467 +### Syntax_Phases.check_typs
1.468 +### Syntax_Phases.check_typs
1.469 +## calling Output.report
1.470 +### Syntax_Phases.check_terms
1.471 +### Syntax_Phases.check_typs
1.472 +### Syntax_Phases.check_typs
1.473 +### Syntax_Phases.check_typs
1.474 +## calling Output.report
1.475 +### Syntax_Phases.check_terms
1.476 +### Syntax_Phases.check_typs
1.477 +### Syntax_Phases.check_typs
1.478 +### Syntax_Phases.check_typs
1.479 +## calling Output.report
1.480 +### Proof_Context.gen_fixes
1.481 +### Proof_Context.gen_fixes
1.482 \<close>
1.483 -(*//------------------- outcomment before creating session Isac ----------------------------\\* )
1.484 -(**)
1.485 - spark_proof_functions gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
1.486 -(**)
1.487 -spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>
1.488 -(*Output..* )
1.489 -The following verification conditions remain to be proved:
1.490 - procedure_g_c_d_4
1.491 - procedure_g_c_d_11
1.492 -( **)
1.493 -spark_vc procedure_g_c_d_4
1.494 -proof -
1.495 - from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)
1.496 - with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1
1.497 - by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])
1.498 -(** )
1.499 -proof -
1.500 - from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)
1.501 - with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1
1.502 - by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])
1.503 -next
1.504 - from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C2
1.505 - by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)
1.506 -qed
1.507 -( **)oops(**)
1.508 -(** )sorry( **)
1.509 -
1.510 -spark_vc procedure_g_c_d_11
1.511 - sorry
1.512 -(** )
1.513 -spark_end
1.514 -( *Bad path binding: "$ISABELLE_HOME/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.prv"*)
1.515 -
1.516 -( *\\------------------- outcomment before creating session Isac ----------------------------//*)
1.517 -
1.518
1.519 section \<open>Notes: adapt spark_vc to Problem using Naproche as model\<close>
1.520
2.1 --- a/src/Tools/isac/BridgeJEdit/preliminary.sml Fri Jan 22 14:56:44 2021 +0100
2.2 +++ b/src/Tools/isac/BridgeJEdit/preliminary.sml Fri Jan 22 16:03:15 2021 +0100
2.3 @@ -9,8 +9,8 @@
2.4 signature PRELIMINARY =
2.5 sig
2.6 (* for keyword Example *)
2.7 - val store_and_show: Formalise.T list -> theory -> theory;
2.8 - val load_formalisation: (Fdl_Lexer.T list -> ParseC.form_model_refs * 'a) ->
2.9 + val store_and_show: theory -> Formalise.T list -> theory -> theory;
2.10 + val load_formalisation: theory ->(Fdl_Lexer.T list -> ParseC.form_model_refs * 'a) ->
2.11 (theory -> Token.file list * theory) * 'c -> theory -> theory
2.12
2.13 (* for keyword Problem*)
2.14 @@ -49,7 +49,7 @@
2.15 struct
2.16 (**)
2.17
2.18 -fun store_and_show formalise thy =
2.19 +fun store_and_show HACKthy formalise thy =
2.20 let
2.21 (**)val file_read_correct = case formalise of xxx as
2.22 [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y", "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"],
2.23 @@ -57,7 +57,7 @@
2.24 | _ => error "magic failed: handling file exp_Statics_Biegel_Timischl_7-70.str failed"
2.25 (**)
2.26 val formalise = hd formalise (*we expect only one Formalise.T in the list*)
2.27 - val (hdlPIDE, _, refs, o_model, var_type_ctxt) = Step_Specify.initialisePIDE formalise
2.28 + val (hdlPIDE, _, refs, o_model, var_type_ctxt) = Step_Specify.initialisePIDEHACK HACKthy formalise
2.29 (* ^^ TODO remove with cleanup in nxt_specify_init_calc *)
2.30 (*
2.31 TODO: present "Problem hdlPIDE" via PIDE
2.32 @@ -79,7 +79,7 @@
2.33 thy'
2.34 end;
2.35 *)
2.36 -fun load_formalisation parse (files, _) thy =
2.37 +fun load_formalisation HACKthy parse (files, _) thy =
2.38 let
2.39 val ([{lines, pos, ...}: Token.file], thy') = files thy;
2.40 val formalise = lines
2.41 @@ -89,7 +89,7 @@
2.42 |> parse
2.43 |> fst
2.44 |> ParseC.read_out_formalise
2.45 - |> store_and_show
2.46 + |> store_and_show HACKthy
2.47 (** )val _ = @{print} {a = "### load_formalisation \<rightarrow>", formalise = formalise}( **)
2.48 in
2.49 formalise thy'
3.1 --- a/src/Tools/isac/Specify/step-specify.sml Fri Jan 22 14:56:44 2021 +0100
3.2 +++ b/src/Tools/isac/Specify/step-specify.sml Fri Jan 22 16:03:15 2021 +0100
3.3 @@ -9,6 +9,8 @@
3.4 val by_tactic_input: Tactic.input -> Calc.T -> string * Calc.state_post
3.5 val by_tactic: Tactic.T -> Calc.T -> string * Calc.state_post
3.6
3.7 + val initialisePIDEHACK: theory -> Formalise.T ->
3.8 + term * term * References.T * O_Model.T * Proof.context
3.9 val initialisePIDE: Formalise.T ->
3.10 term * term * References.T * O_Model.T * Proof.context
3.11 val nxt_specify_init_calc: Formalise.T -> Calc.T * State_Steps.T
3.12 @@ -212,6 +214,36 @@
3.13 end
3.14 | by_tactic _ _ = raise ERROR "Step_Specify.by_tactic uncovered pattern in fun.def"
3.15
3.16 +fun initialisePIDEHACK HACKthy (fmz, (dI, pI, mI)) =
3.17 + let
3.18 +(**) val thy = HACKthy(**)
3.19 +(** ) val thy = ThyC.get_theory dI( **)
3.20 + val (pI, (pors, pctxt), mI) =
3.21 + if mI = ["no_met"]
3.22 + then
3.23 + let
3.24 + val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy; (*..TermC.parseNEW'*)
3.25 + val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
3.26 + val pI' = Refine.refine_ori' pors pI;
3.27 + in (pI', (pors (*refinement over models with diff.precond only*), pctxt),
3.28 + (hd o #met o Problem.from_store) pI')
3.29 + end
3.30 + else
3.31 + let
3.32 + val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy; (*..TermC.parseNEW'*)
3.33 + val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
3.34 + in (pI, (pors, pctxt), mI) end;
3.35 + val {cas, ppc, thy = thy', ...} = Problem.from_store pI (*take dI from _refined_ pbl*)
3.36 + val dI = Context.theory_name (ThyC.sub_common (thy, thy'))
3.37 + val hdl = case cas of
3.38 + NONE => Auto_Prog.pblterm dI pI
3.39 + | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t
3.40 + val hdlPIDE = case cas of
3.41 + NONE => Auto_Prog.pbltermPIDE dI pI
3.42 + | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t
3.43 + in
3.44 + (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt)
3.45 + end;
3.46 (* create a calc-tree with oris via an cas.refined pbl *)
3.47 (* initialisePI <- nxt_specify_init_calc *)
3.48 fun initialisePIDE (fmz, (dI, pI, mI)) =
4.1 --- a/test/Tools/isac/Test_Some.thy Fri Jan 22 14:56:44 2021 +0100
4.2 +++ b/test/Tools/isac/Test_Some.thy Fri Jan 22 16:03:15 2021 +0100
4.3 @@ -95,490 +95,6 @@
4.4 declare [[ML_exception_trace]]
4.5 \<close>
4.6
4.7 -section \<open>=============== test prove_vc for Problem + sprak_vc (KEEP!) ======================\<close>
4.8 -
4.9 -(* requires startup with ./zcoding-to-test.sh ..*)
4.10 -Example \<open>~~/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>
4.11 -
4.12 -spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>
4.13 -(*..Problem adds to spark..*)
4.14 -Problem (*procedure_g_c_d_4*)("Biegelinie", ["Biegelinien"])
4.15 - Specification:
4.16 -(*1*)
4.17 - Model:
4.18 - Given: "Traegerlaenge ", "Streckenlast "
4.19 - Where: "q_0 ist_integrierbar_auf {| 0, L |}", "0 < L"
4.20 - Find: "Biegelinie "
4.21 - Relate: "Randbedingungen "
4.22 - References:
4.23 - (*2*)
4.24 - RTheory: ""
4.25 - RProblem: ["", ""]
4.26 - RMethod: ["", ""]
4.27 - (*2*)
4.28 -(*1*)
4.29 - Solution:
4.30 -
4.31 -subsection \<open><Output> BY CLICK ON Problem..Specification\<close>
4.32 -text \<open>
4.33 - Comparison of the two subsections below:
4.34 -(1) <Output> AFTER session Isac (after ./zcoding-to-test.sh) WITH click on Problem..Specification:
4.35 - ((WHILE click ON Example SHOWS NO ERROR))
4.36 -# headline = ..(1) == (2) ..PARSED + Specification
4.37 -# i_model = Inc ..IN 4 ELEMENTS, (1) == (2) ..?!? FROM PARSED ?!?
4.38 -# o_model = COMPLETE WITH 7 ELEMENTS ..FROM Example
4.39 -# refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])..FROM References
4.40 -
4.41 -(2) <Output> WITHOUT session Isac (after ./ztest-to-coding.sh) WITH click on Problem..Specification:
4.42 - ((WHILE click ON Example SHOWS !!! ERROR))
4.43 -# headline = ..(1) == (2) ..PARSED + Specification
4.44 -# i_model = Inc ..IN 4 ELEMENTS, (1) == (2) ..?!? FROM PARSED ?!?
4.45 -# o_model = [] ..NO Example
4.46 -# refs = ("Biegelinie", ["Biegelinien"], ["empty_meth_id"]) ..FROM headline ONLY
4.47 -\<close>
4.48 -
4.49 -subsubsection \<open>(1) WITH session Isac (AFTER ./zcoding-to-test.sh)\<close>
4.50 -text \<open>
4.51 -{a = "//--- Spark_Commands.prove_vc", headline =
4.52 - (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),
4.53 - ((((("Specification", ":"),
4.54 - ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]),
4.55 - "Where"),
4.56 - ":"),
4.57 - ["<markup>", "<markup>"]),
4.58 - "Find"),
4.59 - ":"),
4.60 - "<markup>"),
4.61 - "Relate"),
4.62 - ":"),
4.63 - ["<markup>"]),
4.64 - (("References", ":"),
4.65 - (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),
4.66 - "Solution"),
4.67 - ":"),
4.68 - [])),
4.69 - "")} (line 677 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
4.70 -{a = "prove_vc", i_model =
4.71 - [(0, [], false, "#Given",
4.72 - Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
4.73 - (0, [], false, "#Given",
4.74 - Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
4.75 - (0, [], false, "#Find",
4.76 - Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []),
4.77 - (Const ("empty", "??.'a"), []))),
4.78 - (0, [], false, "#Relate",
4.79 - Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []),
4.80 - (Const ("empty", "??.'a"), [])))],
4.81 - o_model =
4.82 - [(1, [1], "#Given", Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), [Free ("L", "real")]),
4.83 - (2, [1], "#Given", Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), [Free ("q_0", "real")]),
4.84 - (3, [1], "#Find", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"),
4.85 - [Free ("y", "real \<Rightarrow> real")]),
4.86 - (4, [1], "#Relate", Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"),
4.87 - [Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
4.88 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("0", "real")) $
4.89 - Free ("0", "real")) $
4.90 - Const ("List.list.Nil", "bool list"),
4.91 - Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
4.92 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("L", "real")) $
4.93 - Free ("0", "real")) $
4.94 - Const ("List.list.Nil", "bool list"),
4.95 - Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
4.96 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
4.97 - (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("0", "real")) $ Free ("0", "real")) $
4.98 - Const ("List.list.Nil", "bool list"),
4.99 - Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
4.100 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
4.101 - (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("L", "real")) $ Free ("0", "real")) $
4.102 - Const ("List.list.Nil", "bool list")]),
4.103 - (5, [1], "#undef", Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), [Free ("x", "real")]),
4.104 - (6, [1], "#undef", Const ("Biegelinie.GleichungsVariablen", "real list \<Rightarrow> una"),
4.105 - [Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $
4.106 - Const ("List.list.Nil", "real list"),
4.107 - Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_2", "real") $
4.108 - Const ("List.list.Nil", "real list"),
4.109 - Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_3", "real") $
4.110 - Const ("List.list.Nil", "real list"),
4.111 - Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_4", "real") $
4.112 - Const ("List.list.Nil", "real list")]),
4.113 - (7, [1], "#undef", Const ("Biegelinie.AbleitungBiegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"),
4.114 - [Free ("dy", "real \<Rightarrow> real")])],
4.115 - refs =
4.116 - ("Biegelinie", ["Biegelinien"],
4.117 - ["IntegrierenUndKonstanteBestimmen2"])} (line 690 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
4.118 -### Proof_Context.gen_fixes
4.119 -### Proof_Context.gen_fixes
4.120 -### Proof_Context.gen_fixes
4.121 -### Syntax_Phases.check_terms
4.122 -### Syntax_Phases.check_typs
4.123 -### Syntax_Phases.check_typs
4.124 -### Syntax_Phases.check_typs
4.125 -## calling Output.report
4.126 -#### Syntax_Phases.check_props
4.127 -### Syntax_Phases.check_terms
4.128 -### Syntax_Phases.check_typs
4.129 -### Syntax_Phases.check_typs
4.130 -## calling Output.report
4.131 -#### Syntax_Phases.check_props
4.132 -### Syntax_Phases.check_terms
4.133 -### Syntax_Phases.check_typs
4.134 -### Syntax_Phases.check_typs
4.135 -## calling Output.report
4.136 -#### Syntax_Phases.check_props
4.137 -### Syntax_Phases.check_terms
4.138 -### Syntax_Phases.check_typs
4.139 -### Syntax_Phases.check_typs
4.140 -## calling Output.report
4.141 -#### Syntax_Phases.check_props
4.142 -### Syntax_Phases.check_terms
4.143 -### Syntax_Phases.check_typs
4.144 -### Syntax_Phases.check_typs
4.145 -## calling Output.report
4.146 -#### Syntax_Phases.check_props
4.147 -### Syntax_Phases.check_terms
4.148 -### Syntax_Phases.check_typs
4.149 -### Syntax_Phases.check_typs
4.150 -## calling Output.report
4.151 -#### Syntax_Phases.check_props
4.152 -### Syntax_Phases.check_terms
4.153 -### Syntax_Phases.check_typs
4.154 -### Syntax_Phases.check_typs
4.155 -## calling Output.report
4.156 -#### Syntax_Phases.check_props
4.157 -### Syntax_Phases.check_terms
4.158 -### Syntax_Phases.check_typs
4.159 -### Syntax_Phases.check_typs
4.160 -## calling Output.report
4.161 -#### Syntax_Phases.check_props
4.162 -### Syntax_Phases.check_terms
4.163 -### Syntax_Phases.check_typs
4.164 -### Syntax_Phases.check_typs
4.165 -## calling Output.report
4.166 -#### Syntax_Phases.check_props
4.167 -### Syntax_Phases.check_terms
4.168 -### Syntax_Phases.check_typs
4.169 -### Syntax_Phases.check_typs
4.170 -## calling Output.report
4.171 -#### Syntax_Phases.check_props
4.172 -### Syntax_Phases.check_terms
4.173 -### Syntax_Phases.check_typs
4.174 -### Syntax_Phases.check_typs
4.175 -## calling Output.report
4.176 -#### Syntax_Phases.check_props
4.177 -### Syntax_Phases.check_terms
4.178 -### Syntax_Phases.check_typs
4.179 -### Syntax_Phases.check_typs
4.180 -## calling Output.report
4.181 -#### Syntax_Phases.check_props
4.182 -### Syntax_Phases.check_terms
4.183 -### Syntax_Phases.check_typs
4.184 -### Syntax_Phases.check_typs
4.185 -## calling Output.report
4.186 -#### Syntax_Phases.check_props
4.187 -### Syntax_Phases.check_terms
4.188 -### Syntax_Phases.check_typs
4.189 -### Syntax_Phases.check_typs
4.190 -## calling Output.report
4.191 -#### Syntax_Phases.check_props
4.192 -### Syntax_Phases.check_terms
4.193 -### Syntax_Phases.check_typs
4.194 -### Syntax_Phases.check_typs
4.195 -## calling Output.report
4.196 -#### Syntax_Phases.check_props
4.197 -### Syntax_Phases.check_terms
4.198 -### Syntax_Phases.check_typs
4.199 -### Syntax_Phases.check_typs
4.200 -## calling Output.report
4.201 -#### Syntax_Phases.check_props
4.202 -### Syntax_Phases.check_terms
4.203 -### Syntax_Phases.check_typs
4.204 -### Syntax_Phases.check_typs
4.205 -## calling Output.report
4.206 -#### Syntax_Phases.check_props
4.207 -### Syntax_Phases.check_terms
4.208 -### Syntax_Phases.check_typs
4.209 -### Syntax_Phases.check_typs
4.210 -## calling Output.report
4.211 -#### Syntax_Phases.check_props
4.212 -### Syntax_Phases.check_terms
4.213 -### Syntax_Phases.check_typs
4.214 -### Syntax_Phases.check_typs
4.215 -## calling Output.report
4.216 -#### Syntax_Phases.check_props
4.217 -### Syntax_Phases.check_terms
4.218 -### Syntax_Phases.check_typs
4.219 -### Syntax_Phases.check_typs
4.220 -## calling Output.report
4.221 -#### Syntax_Phases.check_props
4.222 -### Syntax_Phases.check_terms
4.223 -### Syntax_Phases.check_typs
4.224 -### Syntax_Phases.check_typs
4.225 -## calling Output.report
4.226 -#### Syntax_Phases.check_props
4.227 -### Syntax_Phases.check_terms
4.228 -### Syntax_Phases.check_typs
4.229 -### Syntax_Phases.check_typs
4.230 -## calling Output.report
4.231 -#### Syntax_Phases.check_props
4.232 -### Syntax_Phases.check_terms
4.233 -### Syntax_Phases.check_typs
4.234 -### Syntax_Phases.check_typs
4.235 -### Syntax_Phases.check_typs
4.236 -## calling Output.report
4.237 -#### Syntax_Phases.check_props
4.238 -### Syntax_Phases.check_terms
4.239 -### Syntax_Phases.check_typs
4.240 -### Syntax_Phases.check_typs
4.241 -### Syntax_Phases.check_typs
4.242 -## calling Output.report
4.243 -### Syntax_Phases.check_terms
4.244 -### Syntax_Phases.check_typs
4.245 -### Syntax_Phases.check_typs
4.246 -### Syntax_Phases.check_typs
4.247 -## calling Output.report
4.248 -### Syntax_Phases.check_terms
4.249 -### Syntax_Phases.check_typs
4.250 -### Syntax_Phases.check_typs
4.251 -### Syntax_Phases.check_typs
4.252 -## calling Output.report
4.253 -### Syntax_Phases.check_terms
4.254 -### Syntax_Phases.check_typs
4.255 -### Syntax_Phases.check_typs
4.256 -### Syntax_Phases.check_typs
4.257 -## calling Output.report
4.258 -### Syntax_Phases.check_terms
4.259 -### Syntax_Phases.check_typs
4.260 -### Syntax_Phases.check_typs
4.261 -### Syntax_Phases.check_typs
4.262 -## calling Output.report
4.263 -### Syntax_Phases.check_terms
4.264 -### Syntax_Phases.check_typs
4.265 -### Syntax_Phases.check_typs
4.266 -### Syntax_Phases.check_typs
4.267 -## calling Output.report
4.268 -### Proof_Context.gen_fixes
4.269 -### Proof_Context.gen_fixes
4.270 -\<close>
4.271 -
4.272 -subsubsection \<open>(2) WITHOUT session Isac (AFTER ./ztest-to-coding.sh)\<close>
4.273 -text \<open>
4.274 -{a = "//--- Spark_Commands.prove_vc", headline =
4.275 - (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),
4.276 - ((((("Specification", ":"),
4.277 - ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]),
4.278 - "Where"),
4.279 - ":"),
4.280 - ["<markup>", "<markup>"]),
4.281 - "Find"),
4.282 - ":"),
4.283 - "<markup>"),
4.284 - "Relate"),
4.285 - ":"),
4.286 - ["<markup>"]),
4.287 - (("References", ":"),
4.288 - (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),
4.289 - "Solution"),
4.290 - ":"),
4.291 - [])),
4.292 - "")}
4.293 -{a = "prove_vc", i_model =
4.294 - [(0, [], false, "#Given",
4.295 - Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
4.296 - (0, [], false, "#Given",
4.297 - Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
4.298 - (0, [], false, "#Find",
4.299 - Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []),
4.300 - (Const ("empty", "??.'a"), []))),
4.301 - (0, [], false, "#Relate",
4.302 - Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []),
4.303 - (Const ("empty", "??.'a"), [])))],
4.304 - o_model = [], refs = ("Biegelinie", ["Biegelinien"], ["empty_meth_id"])}
4.305 -### Proof_Context.gen_fixes
4.306 -### Proof_Context.gen_fixes
4.307 -### Proof_Context.gen_fixes
4.308 -### Syntax_Phases.check_terms
4.309 -### Syntax_Phases.check_typs
4.310 -### Syntax_Phases.check_typs
4.311 -### Syntax_Phases.check_typs
4.312 -## calling Output.report
4.313 -#### Syntax_Phases.check_props
4.314 -### Syntax_Phases.check_terms
4.315 -### Syntax_Phases.check_typs
4.316 -### Syntax_Phases.check_typs
4.317 -## calling Output.report
4.318 -#### Syntax_Phases.check_props
4.319 -### Syntax_Phases.check_terms
4.320 -### Syntax_Phases.check_typs
4.321 -### Syntax_Phases.check_typs
4.322 -## calling Output.report
4.323 -#### Syntax_Phases.check_props
4.324 -### Syntax_Phases.check_terms
4.325 -### Syntax_Phases.check_typs
4.326 -### Syntax_Phases.check_typs
4.327 -## calling Output.report
4.328 -#### Syntax_Phases.check_props
4.329 -### Syntax_Phases.check_terms
4.330 -### Syntax_Phases.check_typs
4.331 -### Syntax_Phases.check_typs
4.332 -## calling Output.report
4.333 -#### Syntax_Phases.check_props
4.334 -### Syntax_Phases.check_terms
4.335 -### Syntax_Phases.check_typs
4.336 -### Syntax_Phases.check_typs
4.337 -## calling Output.report
4.338 -#### Syntax_Phases.check_props
4.339 -### Syntax_Phases.check_terms
4.340 -### Syntax_Phases.check_typs
4.341 -### Syntax_Phases.check_typs
4.342 -## calling Output.report
4.343 -#### Syntax_Phases.check_props
4.344 -### Syntax_Phases.check_terms
4.345 -### Syntax_Phases.check_typs
4.346 -### Syntax_Phases.check_typs
4.347 -## calling Output.report
4.348 -#### Syntax_Phases.check_props
4.349 -### Syntax_Phases.check_terms
4.350 -### Syntax_Phases.check_typs
4.351 -### Syntax_Phases.check_typs
4.352 -## calling Output.report
4.353 -#### Syntax_Phases.check_props
4.354 -### Syntax_Phases.check_terms
4.355 -### Syntax_Phases.check_typs
4.356 -### Syntax_Phases.check_typs
4.357 -## calling Output.report
4.358 -#### Syntax_Phases.check_props
4.359 -### Syntax_Phases.check_terms
4.360 -### Syntax_Phases.check_typs
4.361 -### Syntax_Phases.check_typs
4.362 -## calling Output.report
4.363 -#### Syntax_Phases.check_props
4.364 -### Syntax_Phases.check_terms
4.365 -### Syntax_Phases.check_typs
4.366 -### Syntax_Phases.check_typs
4.367 -## calling Output.report
4.368 -#### Syntax_Phases.check_props
4.369 -### Syntax_Phases.check_terms
4.370 -### Syntax_Phases.check_typs
4.371 -### Syntax_Phases.check_typs
4.372 -## calling Output.report
4.373 -#### Syntax_Phases.check_props
4.374 -### Syntax_Phases.check_terms
4.375 -### Syntax_Phases.check_typs
4.376 -### Syntax_Phases.check_typs
4.377 -## calling Output.report
4.378 -#### Syntax_Phases.check_props
4.379 -### Syntax_Phases.check_terms
4.380 -### Syntax_Phases.check_typs
4.381 -### Syntax_Phases.check_typs
4.382 -## calling Output.report
4.383 -#### Syntax_Phases.check_props
4.384 -### Syntax_Phases.check_terms
4.385 -### Syntax_Phases.check_typs
4.386 -### Syntax_Phases.check_typs
4.387 -## calling Output.report
4.388 -#### Syntax_Phases.check_props
4.389 -### Syntax_Phases.check_terms
4.390 -### Syntax_Phases.check_typs
4.391 -### Syntax_Phases.check_typs
4.392 -## calling Output.report
4.393 -#### Syntax_Phases.check_props
4.394 -### Syntax_Phases.check_terms
4.395 -### Syntax_Phases.check_typs
4.396 -### Syntax_Phases.check_typs
4.397 -## calling Output.report
4.398 -#### Syntax_Phases.check_props
4.399 -### Syntax_Phases.check_terms
4.400 -### Syntax_Phases.check_typs
4.401 -### Syntax_Phases.check_typs
4.402 -## calling Output.report
4.403 -#### Syntax_Phases.check_props
4.404 -### Syntax_Phases.check_terms
4.405 -### Syntax_Phases.check_typs
4.406 -### Syntax_Phases.check_typs
4.407 -## calling Output.report
4.408 -#### Syntax_Phases.check_props
4.409 -### Syntax_Phases.check_terms
4.410 -### Syntax_Phases.check_typs
4.411 -### Syntax_Phases.check_typs
4.412 -## calling Output.report
4.413 -#### Syntax_Phases.check_props
4.414 -### Syntax_Phases.check_terms
4.415 -### Syntax_Phases.check_typs
4.416 -### Syntax_Phases.check_typs
4.417 -## calling Output.report
4.418 -#### Syntax_Phases.check_props
4.419 -### Syntax_Phases.check_terms
4.420 -### Syntax_Phases.check_typs
4.421 -### Syntax_Phases.check_typs
4.422 -### Syntax_Phases.check_typs
4.423 -## calling Output.report
4.424 -#### Syntax_Phases.check_props
4.425 -### Syntax_Phases.check_terms
4.426 -### Syntax_Phases.check_typs
4.427 -### Syntax_Phases.check_typs
4.428 -### Syntax_Phases.check_typs
4.429 -## calling Output.report
4.430 -### Syntax_Phases.check_terms
4.431 -### Syntax_Phases.check_typs
4.432 -### Syntax_Phases.check_typs
4.433 -### Syntax_Phases.check_typs
4.434 -## calling Output.report
4.435 -### Syntax_Phases.check_terms
4.436 -### Syntax_Phases.check_typs
4.437 -### Syntax_Phases.check_typs
4.438 -### Syntax_Phases.check_typs
4.439 -## calling Output.report
4.440 -### Syntax_Phases.check_terms
4.441 -### Syntax_Phases.check_typs
4.442 -### Syntax_Phases.check_typs
4.443 -### Syntax_Phases.check_typs
4.444 -## calling Output.report
4.445 -### Syntax_Phases.check_terms
4.446 -### Syntax_Phases.check_typs
4.447 -### Syntax_Phases.check_typs
4.448 -### Syntax_Phases.check_typs
4.449 -## calling Output.report
4.450 -### Syntax_Phases.check_terms
4.451 -### Syntax_Phases.check_typs
4.452 -### Syntax_Phases.check_typs
4.453 -### Syntax_Phases.check_typs
4.454 -## calling Output.report
4.455 -### Proof_Context.gen_fixes
4.456 -### Proof_Context.gen_fixes
4.457 -\<close>
4.458 -
4.459 -subsection \<open>How complete must SPARK's sequence of keywords be?\<close>
4.460 -ML \<open>
4.461 - (*
4.462 - AT ABOVE "ML" WE HAVE:
4.463 - Bad context for command "ML"\<^here> -- using reset state
4.464 - ..CAUSED BY INSUFFICIENT SEQUENCE OF SPARK keywords here in this test sequence,
4.465 - BUT spark_open + Problem ABOVE SHOWS NO ERROR -- THAT IS WHAT WE WANT DURING ADAPTATION!
4.466 - *)
4.467 -\<close>
4.468 -(*//--------- SPARK keywords do work IF THERE IS NO spark_open ABOVE.. ----------------------\\* )
4.469 -(** )
4.470 -spark_proof_functions gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
4.471 -( **)
4.472 -
4.473 -(** )
4.474 -spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>
4.475 -( ** )
4.476 -The following verification conditions remain to be proved:
4.477 - procedure_g_c_d_4
4.478 - procedure_g_c_d_11
4.479 -( **)
4.480 -
4.481 -spark_vc procedure_g_c_d_4 (*Bad context for command "spark_vc"\<^here> -- using reset state*)
4.482 - sorry
4.483 -spark_vc procedure_g_c_d_11
4.484 - sorry
4.485 -(** )
4.486 -spark_end
4.487 -( *Bad path binding: "$ISABELLE_HOME/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.prv"*)
4.488 -
4.489 -( *\\--------- SPARK keywords do work IF THERE IS NO spark_open ABOVE.. ----------------------//*)
4.490 -
4.491 section \<open>===================================================================================\<close>
4.492 ML \<open>
4.493 \<close> ML \<open>