1.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Wed Dec 09 14:37:10 2020 +0100
     1.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Wed Dec 09 16:24:26 2020 +0100
     1.3 @@ -77,6 +77,7 @@
     1.4  (*  prove_vc: string -> Proof.context -> Proof.state*)
     1.5  fun prove_vc vc_name lthy =
     1.6    let
     1.7 +    val _ = @{print} {a = "//--- Spark_Commands.prove_vc", vc_name = vc_name}
     1.8      val thy = Proof_Context.theory_of lthy;
     1.9      val (ctxt, stmt) = get_vc thy vc_name
    1.10    in

     2.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Wed Dec 09 14:37:10 2020 +0100
     2.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Wed Dec 09 16:24:26 2020 +0100
     2.3 @@ -11,13 +11,16 @@
     2.4  (**)"HOL-SPARK.SPARK" (** ) preliminarily for parsing Example files *)
     2.5  (** )"HOL-Word.Word"( ** ) trial on ERROR in definition sdiv below *)
     2.6  keywords
     2.7 -  "Example" :: thy_load ("str") and (* "spark_vc" :: thy_goal *)
     2.8 -  "Problem" :: thy_goal and (* root-problem + recursively in Solution *)
     2.9 -  "Specification" "Model" "References" "Solution" and (* structure only *)
    2.10 -  "Given" "Find" "Relate" "Where" and (* await input of term *)
    2.11 -  "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *)
    2.12 -  "RProblem" "RMethod" and (* await input of string list *)
    2.13 -  "Tactic" (* optional for each step 0..end of calculation *)
    2.14 +    "Example" :: thy_load ("str") (* "spark_vc" :: thy_goal *)
    2.15 +  and "Problem" :: thy_goal (* root-problem + recursively in Solution *)
    2.16 +  and "Specification" "Model" "References" "Solution" (* structure only *)
    2.17 +  and"Given" "Find" "Relate" "Where" (* await input of term *)
    2.18 +  and "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *)
    2.19 +  and "RProblem" "RMethod" (* await input of string list *)
    2.20 +    "Tactic" (* optional for each step 0..end of calculation *)
    2.21 +(*//-------------------- investigate Outer_Syntax.local_theory_to_proof -------------------\\*)
    2.22 +  and"global_interpretationC" :: thy_goal
    2.23 +(*\\-------------------- investigate Outer_Syntax.local_theory_to_proof -------------------//*)
    2.24  begin
    2.25  
    2.26  (**)ML_file parseC.sml(**)
    2.27 @@ -638,20 +641,28 @@
    2.28    | NONE => error ("There is no verification condition " ^
    2.29        quote vc_name ^ "."));
    2.30  \<close> ML \<open>
    2.31 -fun prefer_input ((inthy, inpbl : Problem.id), (thy, pbl)) met_id o_model =
    2.32 +(*
    2.33 +val prefer_input: ThyC.id * Problem.id -> References.T -> O_Model.T -> References.T * O_Model.T
    2.34 +*)
    2.35 +fun prefer_input (inthy, inpbl : Problem.id) (thy, pbl, met_id) o_model =
    2.36    if inthy = thy andalso inpbl = pbl
    2.37    then ((thy, pbl, met_id) : References.T, o_model)
    2.38    else ((inthy, inpbl, Method.id_empty), [])
    2.39  \<close> ML \<open>
    2.40 -(*  prove_vc : string -> Proof.context -> Proof.state*)
    2.41 +(*
    2.42 +val prove_vc : string -> Proof.context -> Proof.state
    2.43 +\<rightarrow>
    2.44 +val prove_vc : string -> Proof.context -> Proof.state
    2.45 +*)
    2.46  fun prove_vc vc_name lthy =
    2.47    let
    2.48 +    val _ = @{print} {a = "//--- Spark_Commands.prove_vc", vc_name = vc_name}
    2.49      val thy = Proof_Context.theory_of lthy;
    2.50      val (ctxt, stmt) = get_vc thy vc_name
    2.51  (*//--------------------------------- new code --------------------------------\\*)
    2.52 -    val refs' = ("Biegelinie", ["Biegelinien"]) (*until Parse.name \<rightarrow> ParseC.problem_headline*)
    2.53 -    val (thy_id, pbl_id, met_id) = Refs_Data.get thy
    2.54 -    val (refs, o_model) = prefer_input (refs', (thy_id, pbl_id)) met_id (OMod_Data.get thy)
    2.55 +    val refs'' = ("Biegelinie", ["Biegelinien"]) (*until Parse.name \<rightarrow> ParseC.problem_headline*)
    2.56 +    val refs' = Refs_Data.get thy
    2.57 +    val (refs as (_, pbl_id, _), o_model) = prefer_input refs'' refs' (OMod_Data.get thy)
    2.58      val i_model = I_Model.initPIDE pbl_id
    2.59  (*
    2.60    TODO: present Specification = i_model () + refs via PIDE
    2.61 @@ -692,6 +703,39 @@
    2.62  
    2.63    This now gives no error, but also no <Output>. See child of 3ea616c84845.
    2.64  \<close>
    2.65 +(*required for proof below..*)
    2.66 +spark_proof_functions
    2.67 +  gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
    2.68 +(**)
    2.69 +spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>
    2.70 +(*Output..* )
    2.71 +The following verification conditions remain to be proved:
    2.72 +  procedure_g_c_d_4
    2.73 +  procedure_g_c_d_11
    2.74 +( **)
    2.75 +spark_vc procedure_g_c_d_4
    2.76 +proof -
    2.77 +  from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)
    2.78 +  with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1
    2.79 +    by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])
    2.80 +(** )
    2.81 +proof -
    2.82 +  from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)
    2.83 +  with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1
    2.84 +    by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])
    2.85 +next
    2.86 +  from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C2
    2.87 +    by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)
    2.88 +qed
    2.89 +( **)oops(**)
    2.90 +(** )sorry( **)
    2.91 +
    2.92 +spark_vc procedure_g_c_d_11
    2.93 +  sorry
    2.94 +(** )
    2.95 +spark_end
    2.96 +( *Bad path binding: "$ISABELLE_HOME/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.prv"*)
    2.97 +
    2.98  
    2.99  section \<open>adapt spark_vc to Problem\<close>
   2.100  
   2.101 @@ -705,9 +749,24 @@
   2.102  
   2.103  subsection \<open>notes and testbed for spark_vcs\<close>
   2.104  ML \<open>
   2.105 +\<close> ML \<open> (* Outer_Syntax.local_theory_to_proof..global_interpretationC *)
   2.106 +val interpretation_args_with_defs =
   2.107 +  Parse.!!! Parse_Spec.locale_expression --
   2.108 +    (Scan.optional (\<^keyword>\<open>defines\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
   2.109 +      -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\<open>=\<close> -- Parse.term))) ([]));
   2.110  \<close> ML \<open>
   2.111 +  Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>global_interpretationC\<close>
   2.112 +    "prove interpretation of locale expression into global theory"
   2.113 +    (interpretation_args_with_defs >> (fn (expr, defs) =>
   2.114 +      Interpretation.global_interpretation_cmd expr defs));
   2.115  \<close> ML \<open>
   2.116 +    (interpretation_args_with_defs >> (fn (expr, defs) =>
   2.117 +      Interpretation.global_interpretation_cmd expr defs))
   2.118 +: Token.T list -> (local_theory -> Proof.state) * Token.T list;
   2.119  \<close> ML \<open>
   2.120 +\<close> ML \<open> (* Outer_Syntax.local_theory_to_proof..Problem *)
   2.121 +    (Parse.name >> prove_vc)
   2.122 +: Token.T list -> (Proof.context -> Proof.state) * Token.T list;
   2.123  \<close> ML \<open>
   2.124  \<close> ML \<open>
   2.125  \<close>
   2.126 @@ -716,7 +775,16 @@
   2.127  ML \<open>
   2.128  \<close> ML \<open>
   2.129  \<close> ML \<open>
   2.130 +\<close> ML \<open>
   2.131 +\<close> ML \<open>
   2.132 +\<close> ML \<open>
   2.133 +\<close> ML \<open>
   2.134 +\<close> ML \<open>
   2.135  \<close>
   2.136  
   2.137  
   2.138  end
   2.139 +(*
   2.140 +  ERROR: Found the end of the theory, but the last SPARK environment is still open.
   2.141 +  ..is OK, since "spark_end" does NOT work here for some reason.
   2.142 +*)

     3.1 --- a/src/Tools/isac/BridgeJEdit/parseC.sml	Wed Dec 09 14:37:10 2020 +0100
     3.2 +++ b/src/Tools/isac/BridgeJEdit/parseC.sml	Wed Dec 09 16:24:26 2020 +0100
     3.3 @@ -26,7 +26,7 @@
     3.4    val tokenize: string -> Token.T list
     3.5    val string_of_toks: Token.T list -> string
     3.6    val parse: (Token.T list -> 'a * Token.T list) -> Token.T list -> 'a * Token.T list
     3.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     3.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     3.9  
    3.10    (*Problem headline*)
    3.11    type problem_headline
    3.12 @@ -69,7 +69,7 @@
    3.13    val parse_form_refs: Fdl_Lexer.T list -> form_refs * Fdl_Lexer.T list;
    3.14    val parse_form_model: Fdl_Lexer.T list -> string list * Fdl_Lexer.T list;
    3.15    val parse_string         : Fdl_Lexer.T list -> string * Fdl_Lexer.T list;
    3.16 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    3.17 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    3.18  end
    3.19  
    3.20  (**)