wneuper/isa: test/Tools/isac/Test

     1 theory Test_Some

     2   imports "Isac.Build_Isac"

     3 begin

     5 ML \<open>open ML_System\<close>

     6 ML \<open>

     7 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)

     8                       (* these vvv test, if funs are intermediately opened in structure

     9                          in case of errors here consider ~~/xtest-to-coding.sh      *)

    10   open Kernel;

    11   open Math_Engine;

    12   open Test_Code;              CalcTreeTEST;

    13   open LItool;                 arguments_from_model;

    14   open Sub_Problem;

    15   open Fetch_Tacs;

    16   open Step

    17   open Env;

    18   open LI;                     scan_dn;

    19   open Istate;

    20   open Error_Pattern;

    21   open Error_Pattern_Def;

    22   open Specification;

    23   open Ctree;                  append_problem;

    24   open Pos;

    25   open Program;

    26   open Prog_Tac;

    27   open Tactical;

    28   open Prog_Expr;

    29   open Auto_Prog;              rule2stac;

    30   open Input_Descript;

    31   open Specify;

    32   open Specify;

    33   open Step_Specify;

    34   open Step_Solve;

    35   open Step;

    36   open Solve;                  (* NONE *)

    37   open ContextC;               transfer_asms_from_to;

    38   open Tactic;                 (* NONE *)

    39   open I_Model;

    40   open O_Model;

    41   open P_Model;                (* NONE *)

    42   open Rewrite;

    43   open Eval;                   get_pair;

    44   open TermC;                  atomt;

    45   open Rule;

    46   open Rule_Set;               Sequence;

    47   open Eval_Def

    48   open ThyC

    49   open ThmC_Def

    50   open ThmC

    51   open Rewrite_Ord

    52   open UnparseC

    53 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

    54 \<close>

    55 ML_file "BaseDefinitions/libraryC.sml"

    57 section \<open>code for copy & paste ===============================================================\<close>

    58 ML \<open>

    59 "~~~~~ fun xxx , args:"; val () = ();

    60 "~~~~~ and xxx , args:"; val () = ();

    61 "~~~~~ fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();

    62 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return from xxx*);

    63 "xx"

    64 ^ "xxx"   (*+*) (*!for return!*) (*isa*) (*REP*) (**)

    65 (*/------------------- step into XXXXX -----------------------------------------------------\*)

    66 (*-------------------- stop step into XXXXX -------------------------------------------------*)

    67 (*\------------------- step into XXXXX -----------------------------------------------------/*)

    68 (*-------------------- contiue step into XXXXX ----------------------------------------------*)

    69 (*/------------------- check entry to XXXXX ------------------------------------------------\*)

    70 (*\------------------- check entry to XXXXX ------------------------------------------------/*)

    71 (*/------------------- check within XXXXX --------------------------------------------------\*)

    72 (*\------------------- check within XXXXX --------------------------------------------------/*)

    73 (*/------------------- check result of XXXXX -----------------------------------------------\*)

    74 (*\------------------- check result of XXXXX -----------------------------------------------/*)

    75 (* final test ...*)

    76 (*/------------------- build new fun XXXXX -------------------------------------------------\*)

    77 (*\------------------- build new fun XXXXX -------------------------------------------------/*)

    78 \<close> ML \<open>

    79 \<close>

    80 ML \<open>

    81 \<close> ML \<open>

    82 \<close> ML \<open>

    83 \<close>

    84 text \<open>

    85   declare [[show_types]]

    86   declare [[show_sorts]]

    87   find_theorems "?a <= ?a"

    89   print_theorems

    90   print_facts

    91   print_statement ""

    92   print_theory

    93   ML_command \<open>Pretty.writeln prt\<close>

    94   declare [[ML_print_depth = 999]]

    95   declare [[ML_exception_trace]]

    96 \<close>

    98 section \<open>=============== test prove_vc for Problem + sprak_vc (KEEP!) ======================\<close>

   100 (* requires startup with ./zcoding-to-test.sh ..*)

   101 Example \<open>~~/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>

   103 spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>

   104 (*..Problem adds to spark..*)

   105 Problem (*procedure_g_c_d_4*)("Biegelinie", ["Biegelinien"])

   106   Specification:

   107 (*1*)

   108     Model:

   109       Given: "Traegerlaenge ", "Streckenlast "

   110       Where: "q_0 ist_integrierbar_auf {| 0, L |}", "0 < L"

   111       Find: "Biegelinie "

   112       Relate: "Randbedingungen "

   113     References:

   114   (*2*)

   115       RTheory: ""

   116       RProblem: ["", ""]

   117       RMethod: ["", ""]

   118   (*2*)

   119 (*1*)

   120   Solution:

   122 subsection \<open><Output> BY CLICK ON Problem..Specification\<close>

   123 text \<open>

   124   Comparison of the two subsections below:

   125 (1) <Output> AFTER session Isac (after ./zcoding-to-test.sh) WITH click on Problem..Specification:

   126   ((WHILE click ON Example SHOWS NO ERROR))

   127 # headline =  ..(1) == (2)                                                     ..PARSED + Specification

   128 # i_model = Inc  ..IN 4 ELEMENTS, (1) == (2)                                   ..?!? FROM PARSED ?!?

   129 # o_model = COMPLETE WITH 7 ELEMENTS                                           ..FROM Example

   130 # refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])..FROM References

   132 (2) <Output> WITHOUT session Isac (after ./ztest-to-coding.sh) WITH click on Problem..Specification:

   133   ((WHILE click ON Example SHOWS !!! ERROR))

   134 # headline =  ..(1) == (2)                                                     ..PARSED + Specification

   135 # i_model = Inc  ..IN 4 ELEMENTS, (1) == (2)                                   ..?!? FROM PARSED ?!?

   136 # o_model = []                                                                 ..NO Example

   137 # refs = ("Biegelinie", ["Biegelinien"], ["empty_meth_id"])                    ..FROM headline ONLY

   138 \<close>

   140 subsubsection \<open>(1) WITH session Isac (AFTER ./zcoding-to-test.sh)\<close>

   141 text \<open>

   142 {a = "//--- Spark_Commands.prove_vc", headline =

   143  (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),

   144    ((((("Specification", ":"),

   145        ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]),

   146                  "Where"),

   147                 ":"),

   148                ["<markup>", "<markup>"]),

   149               "Find"),

   150              ":"),

   151             "<markup>"),

   152            "Relate"),

   153           ":"),

   154          ["<markup>"]),

   155         (("References", ":"),

   156          (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),

   157       "Solution"),

   158      ":"),

   159     [])),

   160   "")} (line 677 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")

   161 {a = "prove_vc", i_model =

   162  [(0, [], false, "#Given",

   163    Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),

   164   (0, [], false, "#Given",

   165    Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),

   166   (0, [], false, "#Find",

   167    Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []),

   168         (Const ("empty", "??.'a"), []))),

   169   (0, [], false, "#Relate",

   170    Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []),

   171         (Const ("empty", "??.'a"), [])))],

   172  o_model =

   173  [(1, [1], "#Given", Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), [Free ("L", "real")]),

   174   (2, [1], "#Given", Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), [Free ("q_0", "real")]),

   175   (3, [1], "#Find", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"),

   176    [Free ("y", "real \<Rightarrow> real")]),

   177   (4, [1], "#Relate", Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"),

   178    [Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $

   179       (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("0", "real")) $

   180         Free ("0", "real")) $

   181       Const ("List.list.Nil", "bool list"),

   182     Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $

   183       (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("L", "real")) $

   184         Free ("0", "real")) $

   185       Const ("List.list.Nil", "bool list"),

   186     Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $

   187       (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $

   188         (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("0", "real")) $ Free ("0", "real")) $

   189       Const ("List.list.Nil", "bool list"),

   190     Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $

   191       (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $

   192         (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("L", "real")) $ Free ("0", "real")) $

   193       Const ("List.list.Nil", "bool list")]),

   194   (5, [1], "#undef", Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), [Free ("x", "real")]),

   195   (6, [1], "#undef", Const ("Biegelinie.GleichungsVariablen", "real list \<Rightarrow> una"),

   196    [Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $

   197       Const ("List.list.Nil", "real list"),

   198     Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_2", "real") $

   199       Const ("List.list.Nil", "real list"),

   200     Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_3", "real") $

   201       Const ("List.list.Nil", "real list"),

   202     Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_4", "real") $

   203       Const ("List.list.Nil", "real list")]),

   204   (7, [1], "#undef", Const ("Biegelinie.AbleitungBiegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"),

   205    [Free ("dy", "real \<Rightarrow> real")])],

   206  refs =

   207  ("Biegelinie", ["Biegelinien"],

   208   ["IntegrierenUndKonstanteBestimmen2"])} (line 690 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")

   209 ### Proof_Context.gen_fixes

   210 ### Proof_Context.gen_fixes

   211 ### Proof_Context.gen_fixes

   212 ### Syntax_Phases.check_terms

   213 ### Syntax_Phases.check_typs

   214 ### Syntax_Phases.check_typs

   215 ### Syntax_Phases.check_typs

   216 ## calling Output.report

   217 #### Syntax_Phases.check_props

   218 ### Syntax_Phases.check_terms

   219 ### Syntax_Phases.check_typs

   220 ### Syntax_Phases.check_typs

   221 ## calling Output.report

   222 #### Syntax_Phases.check_props

   223 ### Syntax_Phases.check_terms

   224 ### Syntax_Phases.check_typs

   225 ### Syntax_Phases.check_typs

   226 ## calling Output.report

   227 #### Syntax_Phases.check_props

   228 ### Syntax_Phases.check_terms

   229 ### Syntax_Phases.check_typs

   230 ### Syntax_Phases.check_typs

   231 ## calling Output.report

   232 #### Syntax_Phases.check_props

   233 ### Syntax_Phases.check_terms

   234 ### Syntax_Phases.check_typs

   235 ### Syntax_Phases.check_typs

   236 ## calling Output.report

   237 #### Syntax_Phases.check_props

   238 ### Syntax_Phases.check_terms

   239 ### Syntax_Phases.check_typs

   240 ### Syntax_Phases.check_typs

   241 ## calling Output.report

   242 #### Syntax_Phases.check_props

   243 ### Syntax_Phases.check_terms

   244 ### Syntax_Phases.check_typs

   245 ### Syntax_Phases.check_typs

   246 ## calling Output.report

   247 #### Syntax_Phases.check_props

   248 ### Syntax_Phases.check_terms

   249 ### Syntax_Phases.check_typs

   250 ### Syntax_Phases.check_typs

   251 ## calling Output.report

   252 #### Syntax_Phases.check_props

   253 ### Syntax_Phases.check_terms

   254 ### Syntax_Phases.check_typs

   255 ### Syntax_Phases.check_typs

   256 ## calling Output.report

   257 #### Syntax_Phases.check_props

   258 ### Syntax_Phases.check_terms

   259 ### Syntax_Phases.check_typs

   260 ### Syntax_Phases.check_typs

   261 ## calling Output.report

   262 #### Syntax_Phases.check_props

   263 ### Syntax_Phases.check_terms

   264 ### Syntax_Phases.check_typs

   265 ### Syntax_Phases.check_typs

   266 ## calling Output.report

   267 #### Syntax_Phases.check_props

   268 ### Syntax_Phases.check_terms

   269 ### Syntax_Phases.check_typs

   270 ### Syntax_Phases.check_typs

   271 ## calling Output.report

   272 #### Syntax_Phases.check_props

   273 ### Syntax_Phases.check_terms

   274 ### Syntax_Phases.check_typs

   275 ### Syntax_Phases.check_typs

   276 ## calling Output.report

   277 #### Syntax_Phases.check_props

   278 ### Syntax_Phases.check_terms

   279 ### Syntax_Phases.check_typs

   280 ### Syntax_Phases.check_typs

   281 ## calling Output.report

   282 #### Syntax_Phases.check_props

   283 ### Syntax_Phases.check_terms

   284 ### Syntax_Phases.check_typs

   285 ### Syntax_Phases.check_typs

   286 ## calling Output.report

   287 #### Syntax_Phases.check_props

   288 ### Syntax_Phases.check_terms

   289 ### Syntax_Phases.check_typs

   290 ### Syntax_Phases.check_typs

   291 ## calling Output.report

   292 #### Syntax_Phases.check_props

   293 ### Syntax_Phases.check_terms

   294 ### Syntax_Phases.check_typs

   295 ### Syntax_Phases.check_typs

   296 ## calling Output.report

   297 #### Syntax_Phases.check_props

   298 ### Syntax_Phases.check_terms

   299 ### Syntax_Phases.check_typs

   300 ### Syntax_Phases.check_typs

   301 ## calling Output.report

   302 #### Syntax_Phases.check_props

   303 ### Syntax_Phases.check_terms

   304 ### Syntax_Phases.check_typs

   305 ### Syntax_Phases.check_typs

   306 ## calling Output.report

   307 #### Syntax_Phases.check_props

   308 ### Syntax_Phases.check_terms

   309 ### Syntax_Phases.check_typs

   310 ### Syntax_Phases.check_typs

   311 ## calling Output.report

   312 #### Syntax_Phases.check_props

   313 ### Syntax_Phases.check_terms

   314 ### Syntax_Phases.check_typs

   315 ### Syntax_Phases.check_typs

   316 ## calling Output.report

   317 #### Syntax_Phases.check_props

   318 ### Syntax_Phases.check_terms

   319 ### Syntax_Phases.check_typs

   320 ### Syntax_Phases.check_typs

   321 ## calling Output.report

   322 #### Syntax_Phases.check_props

   323 ### Syntax_Phases.check_terms

   324 ### Syntax_Phases.check_typs

   325 ### Syntax_Phases.check_typs

   326 ### Syntax_Phases.check_typs

   327 ## calling Output.report

   328 #### Syntax_Phases.check_props

   329 ### Syntax_Phases.check_terms

   330 ### Syntax_Phases.check_typs

   331 ### Syntax_Phases.check_typs

   332 ### Syntax_Phases.check_typs

   333 ## calling Output.report

   334 ### Syntax_Phases.check_terms

   335 ### Syntax_Phases.check_typs

   336 ### Syntax_Phases.check_typs

   337 ### Syntax_Phases.check_typs

   338 ## calling Output.report

   339 ### Syntax_Phases.check_terms

   340 ### Syntax_Phases.check_typs

   341 ### Syntax_Phases.check_typs

   342 ### Syntax_Phases.check_typs

   343 ## calling Output.report

   344 ### Syntax_Phases.check_terms

   345 ### Syntax_Phases.check_typs

   346 ### Syntax_Phases.check_typs

   347 ### Syntax_Phases.check_typs

   348 ## calling Output.report

   349 ### Syntax_Phases.check_terms

   350 ### Syntax_Phases.check_typs

   351 ### Syntax_Phases.check_typs

   352 ### Syntax_Phases.check_typs

   353 ## calling Output.report

   354 ### Syntax_Phases.check_terms

   355 ### Syntax_Phases.check_typs

   356 ### Syntax_Phases.check_typs

   357 ### Syntax_Phases.check_typs

   358 ## calling Output.report

   359 ### Proof_Context.gen_fixes

   360 ### Proof_Context.gen_fixes

   361 \<close>

   363 subsubsection \<open>(2) WITHOUT session Isac (AFTER ./ztest-to-coding.sh)\<close>

   364 text \<open>

   365 {a = "//--- Spark_Commands.prove_vc", headline =

   366  (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),

   367    ((((("Specification", ":"),

   368        ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]),

   369                  "Where"),

   370                 ":"),

   371                ["<markup>", "<markup>"]),

   372               "Find"),

   373              ":"),

   374             "<markup>"),

   375            "Relate"),

   376           ":"),

   377          ["<markup>"]),

   378         (("References", ":"),

   379          (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),

   380       "Solution"),

   381      ":"),

   382     [])),

   383   "")}

   384 {a = "prove_vc", i_model =

   385  [(0, [], false, "#Given",

   386    Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),

   387   (0, [], false, "#Given",

   388    Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),

   389   (0, [], false, "#Find",

   390    Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []),

   391         (Const ("empty", "??.'a"), []))),

   392   (0, [], false, "#Relate",

   393    Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []),

   394         (Const ("empty", "??.'a"), [])))],

   395  o_model = [], refs = ("Biegelinie", ["Biegelinien"], ["empty_meth_id"])}

   396 ### Proof_Context.gen_fixes

   397 ### Proof_Context.gen_fixes

   398 ### Proof_Context.gen_fixes

   399 ### Syntax_Phases.check_terms

   400 ### Syntax_Phases.check_typs

   401 ### Syntax_Phases.check_typs

   402 ### Syntax_Phases.check_typs

   403 ## calling Output.report

   404 #### Syntax_Phases.check_props

   405 ### Syntax_Phases.check_terms

   406 ### Syntax_Phases.check_typs

   407 ### Syntax_Phases.check_typs

   408 ## calling Output.report

   409 #### Syntax_Phases.check_props

   410 ### Syntax_Phases.check_terms

   411 ### Syntax_Phases.check_typs

   412 ### Syntax_Phases.check_typs

   413 ## calling Output.report

   414 #### Syntax_Phases.check_props

   415 ### Syntax_Phases.check_terms

   416 ### Syntax_Phases.check_typs

   417 ### Syntax_Phases.check_typs

   418 ## calling Output.report

   419 #### Syntax_Phases.check_props

   420 ### Syntax_Phases.check_terms

   421 ### Syntax_Phases.check_typs

   422 ### Syntax_Phases.check_typs

   423 ## calling Output.report

   424 #### Syntax_Phases.check_props

   425 ### Syntax_Phases.check_terms

   426 ### Syntax_Phases.check_typs

   427 ### Syntax_Phases.check_typs

   428 ## calling Output.report

   429 #### Syntax_Phases.check_props

   430 ### Syntax_Phases.check_terms

   431 ### Syntax_Phases.check_typs

   432 ### Syntax_Phases.check_typs

   433 ## calling Output.report

   434 #### Syntax_Phases.check_props

   435 ### Syntax_Phases.check_terms

   436 ### Syntax_Phases.check_typs

   437 ### Syntax_Phases.check_typs

   438 ## calling Output.report

   439 #### Syntax_Phases.check_props

   440 ### Syntax_Phases.check_terms

   441 ### Syntax_Phases.check_typs

   442 ### Syntax_Phases.check_typs

   443 ## calling Output.report

   444 #### Syntax_Phases.check_props

   445 ### Syntax_Phases.check_terms

   446 ### Syntax_Phases.check_typs

   447 ### Syntax_Phases.check_typs

   448 ## calling Output.report

   449 #### Syntax_Phases.check_props

   450 ### Syntax_Phases.check_terms

   451 ### Syntax_Phases.check_typs

   452 ### Syntax_Phases.check_typs

   453 ## calling Output.report

   454 #### Syntax_Phases.check_props

   455 ### Syntax_Phases.check_terms

   456 ### Syntax_Phases.check_typs

   457 ### Syntax_Phases.check_typs

   458 ## calling Output.report

   459 #### Syntax_Phases.check_props

   460 ### Syntax_Phases.check_terms

   461 ### Syntax_Phases.check_typs

   462 ### Syntax_Phases.check_typs

   463 ## calling Output.report

   464 #### Syntax_Phases.check_props

   465 ### Syntax_Phases.check_terms

   466 ### Syntax_Phases.check_typs

   467 ### Syntax_Phases.check_typs

   468 ## calling Output.report

   469 #### Syntax_Phases.check_props

   470 ### Syntax_Phases.check_terms

   471 ### Syntax_Phases.check_typs

   472 ### Syntax_Phases.check_typs

   473 ## calling Output.report

   474 #### Syntax_Phases.check_props

   475 ### Syntax_Phases.check_terms

   476 ### Syntax_Phases.check_typs

   477 ### Syntax_Phases.check_typs

   478 ## calling Output.report

   479 #### Syntax_Phases.check_props

   480 ### Syntax_Phases.check_terms

   481 ### Syntax_Phases.check_typs

   482 ### Syntax_Phases.check_typs

   483 ## calling Output.report

   484 #### Syntax_Phases.check_props

   485 ### Syntax_Phases.check_terms

   486 ### Syntax_Phases.check_typs

   487 ### Syntax_Phases.check_typs

   488 ## calling Output.report

   489 #### Syntax_Phases.check_props

   490 ### Syntax_Phases.check_terms

   491 ### Syntax_Phases.check_typs

   492 ### Syntax_Phases.check_typs

   493 ## calling Output.report

   494 #### Syntax_Phases.check_props

   495 ### Syntax_Phases.check_terms

   496 ### Syntax_Phases.check_typs

   497 ### Syntax_Phases.check_typs

   498 ## calling Output.report

   499 #### Syntax_Phases.check_props

   500 ### Syntax_Phases.check_terms

   501 ### Syntax_Phases.check_typs

   502 ### Syntax_Phases.check_typs

   503 ## calling Output.report

   504 #### Syntax_Phases.check_props

   505 ### Syntax_Phases.check_terms

   506 ### Syntax_Phases.check_typs

   507 ### Syntax_Phases.check_typs

   508 ## calling Output.report

   509 #### Syntax_Phases.check_props

   510 ### Syntax_Phases.check_terms

   511 ### Syntax_Phases.check_typs

   512 ### Syntax_Phases.check_typs

   513 ### Syntax_Phases.check_typs

   514 ## calling Output.report

   515 #### Syntax_Phases.check_props

   516 ### Syntax_Phases.check_terms

   517 ### Syntax_Phases.check_typs

   518 ### Syntax_Phases.check_typs

   519 ### Syntax_Phases.check_typs

   520 ## calling Output.report

   521 ### Syntax_Phases.check_terms

   522 ### Syntax_Phases.check_typs

   523 ### Syntax_Phases.check_typs

   524 ### Syntax_Phases.check_typs

   525 ## calling Output.report

   526 ### Syntax_Phases.check_terms

   527 ### Syntax_Phases.check_typs

   528 ### Syntax_Phases.check_typs

   529 ### Syntax_Phases.check_typs

   530 ## calling Output.report

   531 ### Syntax_Phases.check_terms

   532 ### Syntax_Phases.check_typs

   533 ### Syntax_Phases.check_typs

   534 ### Syntax_Phases.check_typs

   535 ## calling Output.report

   536 ### Syntax_Phases.check_terms

   537 ### Syntax_Phases.check_typs

   538 ### Syntax_Phases.check_typs

   539 ### Syntax_Phases.check_typs

   540 ## calling Output.report

   541 ### Syntax_Phases.check_terms

   542 ### Syntax_Phases.check_typs

   543 ### Syntax_Phases.check_typs

   544 ### Syntax_Phases.check_typs

   545 ## calling Output.report

   546 ### Proof_Context.gen_fixes

   547 ### Proof_Context.gen_fixes

   548 \<close>

   550 subsection \<open>How complete must SPARK's sequence of keywords be?\<close>

   551 ML \<open>

   552   (*

   553   AT ABOVE "ML" WE HAVE:

   554       Bad context for command "ML"\<^here> -- using reset state

   555   ..CAUSED BY INSUFFICIENT SEQUENCE OF SPARK keywords here in this test sequence,

   556   BUT spark_open + Problem  ABOVE SHOWS NO ERROR -- THAT IS WHAT WE WANT DURING ADAPTATION!

   557   *)

   558 \<close>

   559 (*//--------- SPARK keywords do work IF THERE IS NO spark_open ABOVE.. ----------------------\\* )

   560 (** )

   561 spark_proof_functions gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"

   562 ( **)

   564 (** )

   565 spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>

   566 ( ** )

   567 The following verification conditions remain to be proved:

   568   procedure_g_c_d_4

   569   procedure_g_c_d_11

   570 ( **)

   572 spark_vc procedure_g_c_d_4  (*Bad context for command "spark_vc"\<^here> -- using reset state*)

   573   sorry

   574 spark_vc procedure_g_c_d_11

   575   sorry

   576 (** )

   577 spark_end

   578 ( *Bad path binding: "$ISABELLE_HOME/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.prv"*)

   580 ( *\\--------- SPARK keywords do work IF THERE IS NO spark_open ABOVE.. ----------------------//*)

   582 section \<open>===================================================================================\<close>

   583 ML \<open>

   584 \<close> ML \<open>

   585 \<close> ML \<open>

   586 \<close> ML \<open>

   587 \<close>

   589 section \<open>===================================================================================\<close>

   590 ML \<open>

   591 \<close> ML \<open>

   592 \<close> ML \<open>

   593 \<close> ML \<open>

   594 \<close>

   596 section \<open>===================================================================================\<close>

   597 ML \<open>

   598 \<close> ML \<open>

   599 \<close> ML \<open>

   600 \<close> ML \<open>

   601 \<close>

   603 section \<open>code for copy & paste ===============================================================\<close>

   604 ML \<open>

   605 "~~~~~ fun xxx , args:"; val () = ();

   606 "~~~~~ and xxx , args:"; val () = ();

   607 "~~~~~ from xxx to yyy return val:"; val ((*yyy*)) = ((*xxx*));

   608 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*);

   609 "xx"

   610 ^ "xxx"   (*+*)

   611 \<close>

   612 end

author	Walther Neuper <walther.neuper@jku.at>
	Sun, 17 Jan 2021 13:16:25 +0100
changeset 60145	d2659cf8652c
parent 60137	12f0c14fc333
child 60147	d3cb5af53d3d
permissions	-rw-r--r--