1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Fri Jan 22 16:03:15 2021 +0100
     1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Tue Jan 26 12:46:12 2021 +0100
     1.3 @@ -15,7 +15,8 @@
     1.4    and "Problem" :: thy_decl (* root-problem + recursively in Solution;
     1.5                                 "spark_vc" :: thy_goal *)
     1.6    and "Specification" "Model" "References" "Solution" (* structure only *)
     1.7 -  and "Given" "Find" "Relate" "Where" (* await input of term *)
     1.8 +  and "Given" "Find" "Relate" :: prf_chain (* await input of term *)
     1.9 +  and "Where" (* only output, preliminarily *)
    1.10    and "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *)
    1.11    and "RProblem" "RMethod" (* await input of string list *)
    1.12      "Tactic" (* optional for each step 0..end of calculation *)
    1.13 @@ -36,14 +37,18 @@
    1.14  \<close> ML \<open>
    1.15  \<close> 
    1.16  
    1.17 -subsubsection \<open>TODO\<close>
    1.18 +subsubsection \<open>cp from Pure.thy\<close>
    1.19  ML \<open>
    1.20  \<close> ML \<open>
    1.21 +(* original *)
    1.22 +val facts = Parse.and_list1 Parse.thms1;
    1.23 +facts: (Facts.ref * Token.src list) list list parser;
    1.24  \<close> ML \<open>
    1.25 -\<close>
    1.26 -
    1.27 -subsubsection \<open>TODO\<close>
    1.28 -ML \<open>
    1.29 +val facts =
    1.30 +  (writeln "####-## from parser";
    1.31 +    Parse.$$$ ":" |-- Parse.and_list1 Parse.thms1)(** ) --| Parse.$$$ "Where"( **);
    1.32 +facts: (Facts.ref * Token.src list) list list parser;
    1.33 +\<close> ML \<open>
    1.34  \<close> ML \<open>
    1.35  \<close> ML \<open>
    1.36  \<close>
    1.37 @@ -71,32 +76,47 @@
    1.38  Preliminary.prove_vc: ParseC.problem -> Proof.context -> Proof.state;
    1.39  SPARK_Commands.prove_vc: string -> Proof.context -> Proof.state
    1.40  \<close> ML \<open>
    1.41 +\<close> ML \<open> (*-----------------------------------------------------------------------------------*)
    1.42 +val _ =
    1.43 +  Outer_Syntax.command \<^command_keyword>\<open>Given\<close> "input Given items to the Model of a Specification"
    1.44 +    (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
    1.45 +val _ =
    1.46 +  Outer_Syntax.command \<^command_keyword>\<open>Find\<close> "input Find item to the Model of a Specification"
    1.47 +    (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
    1.48 +val _ =
    1.49 +  Outer_Syntax.command \<^command_keyword>\<open>Relate\<close> "input Relate items to the Model of a Specification"
    1.50 +    (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
    1.51 +\<close> ML \<open>
    1.52 +\<close> ML \<open>
    1.53 +\<close> ML \<open>
    1.54  \<close>
    1.55  
    1.56  subsection \<open>test runs with Example\<close>
    1.57 +(**)
    1.58 +Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>
    1.59 +(*(1) outcomment before creating session Isac* )
    1.60  
    1.61 -Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>
    1.62 -
    1.63 -(*vvvvvvvv--- makes Outer_Syntax..Problem run; Isac code is just added*)
    1.64 +(*makes Outer_Syntax..Problem run; Isac code is just added..*)
    1.65  spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>
    1.66  
    1.67 -(*..Problem adds to SPARK..*)
    1.68 -Problem (*procedure_g_c_d_4*)("Biegelinie", ["Biegelinien"])
    1.69 +( *(2) outcomment before creating session Isac* )
    1.70 +Problem ("Biegelinie", ["Biegelinien"]) (*procedure_g_c_d_4 .."Problem" adds to SPARK*)
    1.71    Specification:
    1.72 -(*1*)
    1.73 +(*1 collapse*)
    1.74      Model:
    1.75 -      Given: "Traegerlaenge ", "Streckenlast "
    1.76 -      Where: "q_0 ist_integrierbar_auf {| 0, L |}", "0 < L"
    1.77 +      Given: "Traegerlaenge "(*,*) "Streckenlast "
    1.78 +      Where: "q_0 ist_integrierbar_auf {| 0, L |}"(*,*) "0 < L"
    1.79        Find: "Biegelinie "
    1.80        Relate: "Randbedingungen "
    1.81      References:
    1.82 -  (*2*)
    1.83 +  (*2 collapse*)
    1.84        RTheory: ""
    1.85        RProblem: ["", ""]
    1.86        RMethod: ["", ""]
    1.87 -  (*2*)
    1.88 -(*1*)
    1.89 +  (*2 collapse*)
    1.90 +(*1 collapse*)
    1.91    Solution:
    1.92 +( **)
    1.93  (*
    1.94    compare click on above Given: "Traegerlaenge ", "Streckenlast " 
    1.95    with click on from \<open>0 < d\<close> in SPARK/../Greatest_Common_Divisorthy
    1.96 @@ -554,7 +574,10 @@
    1.97    see text in SPARK/Examples/Gcd/Greatest_Common_Divisor.thy.
    1.98  \<close>
    1.99  
   1.100 -end(* SEE "outcomment before creating session Isac" ABOVE !!! OTHERWISE YOU HAVE..
   1.101 -  ERROR: Found the end of the theory, but the last SPARK environment is still open.
   1.102 -  ..is acceptable for testing spark_vc .. proof - ...
   1.103 -*)
   1.104 +end(* HERE SEVERAL ERRORS SHOW UP, CAUSED FROM ABOVE..
   1.105 +"(1) outcomment before creating session Isac" ABOVE OTHERWISE YOU HAVE..
   1.106 +    Bad context for command "end"\<^here> -- using reset state 
   1.107 +    Found the end of the theory, but the last SPARK environment is still open.
   1.108 +"(2) outcomment before creating session Isac" ABOVE OTHERWISE YOU HAVE..
   1.109 +  ERROR: 
   1.110 +    Bad context for command "end"\<^here> -- using reset state*)