1.1 --- a/src/HOL/SPARK/SPARK_Setup.thy	Wed Feb 03 16:39:44 2021 +0100
     1.2 +++ b/src/HOL/SPARK/SPARK_Setup.thy	Thu Feb 11 17:45:29 2021 +0100
     1.3 @@ -184,5 +184,14 @@
     1.4  
     1.5  ML_file \<open>Tools/spark_vcs.ML\<close>
     1.6  ML_file \<open>Tools/spark_commands.ML\<close>
     1.7 +ML \<open>
     1.8 +\<close> ML \<open>
     1.9 +\<close> ML \<open>
    1.10 +Toplevel.theory o (SPARK_Commands.spark_open Fdl_Lexer.siv_header)
    1.11 +: (theory -> Token.file list * theory) * string -> Toplevel.transition -> Toplevel.transition
    1.12 +\<close> ML \<open>
    1.13 +\<close> ML \<open>
    1.14 +\<close> ML \<open>
    1.15 +\<close>
    1.16  
    1.17  end

     2.1 --- a/src/Pure/Pure.thy	Wed Feb 03 16:39:44 2021 +0100
     2.2 +++ b/src/Pure/Pure.thy	Thu Feb 11 17:45:29 2021 +0100
     2.3 @@ -497,7 +497,7 @@
     2.4  subsubsection \<open>Theorems\<close>
     2.5  
     2.6  ML \<open>
     2.7 -local
     2.8 +(**)local(**)
     2.9  
    2.10  val long_keyword =
    2.11    Parse_Spec.includes >> K "" ||
    2.12 @@ -526,7 +526,7 @@
    2.13  val _ = theorem \<^command_keyword>\<open>proposition\<close> false "proposition";
    2.14  val _ = theorem \<^command_keyword>\<open>schematic_goal\<close> true "schematic goal";
    2.15  
    2.16 -in end\<close>
    2.17 +(**)in end(**)\<close>
    2.18  
    2.19  ML \<open>
    2.20  local
    2.21 @@ -1418,6 +1418,56 @@
    2.22  
    2.23  in end\<close>
    2.24  
    2.25 +ML \<open> (** types of **)
    2.26 +\<close> text \<open> (*prep.for theorem: outcomment (** )local( **) above!*)
    2.27 +long_statement:
    2.28 +  Token.T list -> (bool * Attrib.binding * (xstring * Position.T) list * Element.context list * Element.statement) * Token.T list
    2.29 +\<close> text \<open>
    2.30 +short_statement:
    2.31 +  Token.T list -> (bool * (binding * _d list) * _c list * (string, string, _b) Element.ctxt list * (_a, string) Element.stmt) * Token.T list
    2.32 +\<close> text \<open>
    2.33 +fun theorem spec schematic descr =
    2.34 +  Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr)
    2.35 +    ((long_statement || (*short_statement*)long_statement) >> (fn (long, binding, includes, elems, concl) =>
    2.36 +      ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
    2.37 +        long Thm.theoremK NONE (K I) binding includes elems concl)) );
    2.38 +\<close> text \<open>
    2.39 +theorem: Outer_Syntax.command_keyword -> bool -> string -> unit;
    2.40 +val schematic = false;
    2.41 +\<close> ML \<open>
    2.42 +\<close> text \<open> (*Outer_Syntax.local_theory_to_proof' ...    :: thy_goal_stmt*)
    2.43 +(fn (long, binding, includes, elems, concl) =>
    2.44 +      ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
    2.45 +        long Thm.theoremK NONE (K I) binding includes elems concl))
    2.46 +: 
    2.47 +  bool * Attrib.binding * (xstring * Position.T) list * Element.context list * Element.statement -> bool ->
    2.48 +    local_theory(*Proof.context*) -> Proof.state
    2.49 +(*  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^*)
    2.50 +\<close> ML \<open>
    2.51 +\<close> ML \<open> (*Outer_Syntax.command \<^command_keyword>\<open>from\<close>  :: prf_chain % "proof" *)
    2.52 +Toplevel.proof o Proof.from_thmss_cmd:
    2.53 +  (Facts.ref * Token.src list) list list -> Toplevel.transition -> Toplevel.transition
    2.54 +(*                                          ^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^*)
    2.55 +\<close> ML \<open>
    2.56 +\<close> ML \<open> (**)
    2.57 +\<close> ML \<open>
    2.58 +\<close> ML \<open> (**)
    2.59 +\<close> ML \<open>
    2.60 +\<close> ML \<open> (**)
    2.61 +\<close> ML \<open>
    2.62 +\<close> ML \<open> (**)
    2.63 +\<close> ML \<open>
    2.64 +\<close> ML \<open> (**)
    2.65 +\<close> ML \<open>
    2.66 +\<close> ML \<open> (**)
    2.67 +\<close> ML \<open>
    2.68 +\<close> ML \<open> (**)
    2.69 +\<close> ML \<open>
    2.70 +\<close> ML \<open> (**)
    2.71 +\<close> ML \<open>
    2.72 +\<close> ML \<open>
    2.73 +\<close>
    2.74 +
    2.75  
    2.76  section \<open>Auxiliary lemmas\<close>
    2.77  

     3.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Wed Feb 03 16:39:44 2021 +0100
     3.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Thu Feb 11 17:45:29 2021 +0100
     3.3 @@ -21,7 +21,7 @@
     3.4    and "RProblem" "RMethod" (* await input of string list *)
     3.5      "Tactic" (* optional for each step 0..end of calculation *)
     3.6  begin
     3.7 -
     3.8 +declare [[ML_print_depth = 99999]]
     3.9  (**)ML_file parseC.sml(**)
    3.10  (**)ML_file preliminary.sml(**)
    3.11  
    3.12 @@ -65,8 +65,14 @@
    3.13  val _ =                                                  
    3.14    Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file"
    3.15      (Resources.provide_parse_files "Example" -- Parse.parname
    3.16 -      >> (Toplevel.theory o           (*vvvvvvvvvvvvvvvvvvvv--- HACK: test independent from session Isac*)
    3.17 -        (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation)));
    3.18 +      >> (Toplevel.theory o           (*vvvvvvvvvvvvvvvvvvvv--- HACK makes test independent from session Isac*)
    3.19 +        (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation)) );
    3.20 +\<close> ML \<open>
    3.21 +(Toplevel.theory o (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation))
    3.22 +:
    3.23 +  (theory -> Token.file list * theory) * (*_a*)Token.T ->
    3.24 +    Toplevel.transition -> Toplevel.transition
    3.25 +(*  ^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^*)
    3.26  \<close> ML \<open>
    3.27  val _ =
    3.28    Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>Problem\<close>
    3.29 @@ -75,20 +81,67 @@
    3.30  (** )(ParseC.problem_headline >> Preliminary.prove_vc);( **)
    3.31  \<close> ML \<open>
    3.32  (**)Preliminary.prove_vc: ParseC.problem -> Proof.context -> Proof.state;(**)
    3.33 -(** )Preliminary.prove_vc: ParseC.problem_headline -> Proof.context -> Proof.state;( **)
    3.34 +(*                                          ^^^^^^^^^^^^^    ^^^^^^^^^^^*)
    3.35  SPARK_Commands.prove_vc: string -> Proof.context -> Proof.state
    3.36 +\<close> ML \<open> (*//-----------------------------------------------------------------------------\\*)
    3.37 +\<close> ML \<open>
    3.38 +fun prove_vc (_: ParseC.problem) thy = @{theory}
    3.39 +\<close> ML \<open>
    3.40 +Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition
    3.41 +\<close> ML \<open>
    3.42 +Toplevel.theory o prove_vc: ParseC.problem -> Toplevel.transition -> Toplevel.transition
    3.43 +\<close> ML \<open>
    3.44 +\<close> ML \<open>
    3.45 +\<close> ML \<open> (*\\-----------------------------------------------------------------------------//*)
    3.46 +(* how does ctxt go into Proof.state ?..*)
    3.47 +Specification.theorem:
    3.48 +  bool -> string -> Method.text option -> (thm list list -> local_theory -> local_theory) ->
    3.49 +    Attrib.binding -> string list -> Element.context_i list -> Element.statement_i -> bool ->
    3.50 +      local_theory -> Proof.state
    3.51 +\<close> ML \<open>
    3.52 +K I: Proof.context -> Token.src -> Token.src
    3.53 +\<close> ML \<open>
    3.54 +\<close> text \<open> NEWS 2014 ? still valid ???
    3.55 +* ML antiquotation @ {here} refers to its source position, which is
    3.56 +occasionally useful for experimentation and diagnostic purposes.
    3.57 +
    3.58 +\<close> ML \<open>
    3.59 +fn xxx => xxx + 1
    3.60 +\<close> ML \<open>
    3.61 +fn xxx => xxx + 1
    3.62 +\<close> ML \<open>
    3.63 +\<close> ML \<open>
    3.64 +\<close> ML \<open>
    3.65 +\<close> ML \<open>
    3.66 +\<close> ML \<open>
    3.67 +\<close> ML \<open>
    3.68 +\<close> ML \<open>
    3.69 +\<close> ML \<open>
    3.70 +\<close> ML \<open>
    3.71 +\<close> ML \<open>
    3.72 +\<close> ML \<open>
    3.73 +\<close> ML \<open>
    3.74 +\<close> ML \<open>
    3.75 +\<close> ML \<open>
    3.76 +\<close> ML \<open>
    3.77 +\<close> ML \<open>
    3.78 +\<close> ML \<open>
    3.79  \<close> ML \<open>
    3.80  \<close> ML \<open> (*-----------------------------------------------------------------------------------*)
    3.81  val _ =
    3.82    Outer_Syntax.command \<^command_keyword>\<open>Given\<close> "input Given items to the Model of a Specification"
    3.83      (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
    3.84  val _ =
    3.85 -  Outer_Syntax.command \<^command_keyword>\<open>Find\<close> "input Find item to the Model of a Specification"
    3.86 +  Outer_Syntax.command \<^command_keyword>\<open>Find\<close> "input Find items to the Model of a Specification"
    3.87      (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
    3.88  val _ =
    3.89    Outer_Syntax.command \<^command_keyword>\<open>Relate\<close> "input Relate items to the Model of a Specification"
    3.90      (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
    3.91  \<close> ML \<open>
    3.92 +(Toplevel.proof o Proof.from_thmss_cmd)
    3.93 +:
    3.94 +  (Facts.ref * Token.src list) list list -> Toplevel.transition -> Toplevel.transition
    3.95 +(*                                          ^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^*)
    3.96  \<close> ML \<open>
    3.97  \<close> ML \<open>
    3.98  \<close>
    3.99 @@ -106,11 +159,11 @@
   3.100    Specification:                                               (*Outer syntax error\<^here>: command expected, but keyword Specification\<^here> was found*)
   3.101  (*1 collapse*)
   3.102      Model:
   3.103 -      Given: "Traegerlaenge "(*,*) "Streckenlast "
   3.104 -      Where: "q_0 ist_integrierbar_auf {| 0, L |}"(*,*) "0 < L"(*Outer syntax error\<^here>: command expected, but keyword Where\<^here> was found*)
   3.105 +      Given: "Traegerlaenge ", "Streckenlast "
   3.106 +      Where: "q_0 ist_integrierbar_auf {| 0, L |}", "0 < L"    (*Outer syntax error\<^here>: command expected, but keyword Where\<^here> was found*)
   3.107        Find: "Biegelinie "                                      (*Bad context for command "Find"\<^here> -- using reset state*)
   3.108        Relate: "Randbedingungen "
   3.109 -    References:                                                 (*Outer syntax error\<^here>: command expected, but keyword References\<^here> was found*)
   3.110 +    References:                                                (*Outer syntax error\<^here>: command expected, but keyword References\<^here> was found*)
   3.111    (*2 collapse*)
   3.112        RTheory: ""
   3.113        RProblem: ["", ""]

     4.1 --- a/src/Tools/isac/BridgeJEdit/preliminary.sml	Wed Feb 03 16:39:44 2021 +0100
     4.2 +++ b/src/Tools/isac/BridgeJEdit/preliminary.sml	Thu Feb 11 17:45:29 2021 +0100
     4.3 @@ -10,8 +10,8 @@
     4.4  sig
     4.5    (* for keyword Example *)
     4.6    val store_and_show: theory -> Formalise.T list -> theory -> theory;
     4.7 -  val load_formalisation: theory ->(Fdl_Lexer.T list -> ParseC.form_model_refs * 'a) ->
     4.8 -  (theory -> Token.file list * theory) * 'c -> theory -> theory
     4.9 +  val load_formalisation: theory -> (Fdl_Lexer.T list -> ParseC.form_model_refs * 'a) ->
    4.10 +    (theory -> Token.file list * theory) * 'c -> theory -> theory
    4.11    
    4.12    (* for keyword Problem*)
    4.13  (**)val prove_vc: ParseC.problem -> Proof.context -> Proof.state(**)
    4.14 @@ -37,6 +37,13 @@
    4.15    val extend = I
    4.16    fun merge (_, o_model) = o_model
    4.17  );
    4.18 +structure IMod_Data = Theory_Data
    4.19 +(
    4.20 +  type T = I_Model.T
    4.21 +  val empty : T = []
    4.22 +  val extend = I
    4.23 +  fun merge (_, i_model) = i_model
    4.24 +);
    4.25  structure Ctxt_Data = Theory_Data
    4.26  (
    4.27    type T = Proof.context
    4.28 @@ -91,7 +98,7 @@
    4.29        |> fst
    4.30        |> ParseC.read_out_formalise
    4.31        |> store_and_show HACKthy
    4.32 -(** )val _ = @{print} {a = "### load_formalisation \<rightarrow>", formalise = formalise}( **)
    4.33 +(**)val _ = @{print} {a = "### load_formalisation \<rightarrow>", formalise = formalise}(**)
    4.34    in
    4.35      formalise thy'
    4.36    end;
    4.37 @@ -586,6 +593,7 @@
    4.38  
    4.39  (** copied from spark_commands.ML **)
    4.40  
    4.41 +(*  get_vc: theory -> string -> (typ, term, thm list) Element.ctxt list * ('a, term) Element.stmt *)
    4.42  fun get_vc thy vc_name =
    4.43    (case SPARK_VCs.lookup_vc thy false vc_name of
    4.44      SOME (ctxt, (_, proved, ctxt', stmt)) =>
    4.45 @@ -603,24 +611,26 @@
    4.46    then ((thy, pbl, met_id) : References.T, o_model)
    4.47    else ((inthy, inpbl, MethodC.id_empty), [])
    4.48  
    4.49 -fun prove_vc (*vc_name*)problem lthy =
    4.50 +fun prove_vc (*vc_name*)problem lthy(*Proof.context*) =
    4.51    let
    4.52      val _ = @{print} {a = "//--- Spark_Commands.prove_vc", headline = problem}
    4.53      val thy = Proof_Context.theory_of lthy;
    4.54      val vc_name = "procedure_g_c_d_4" (*fixed for spark_open \<open>greatest_common_divisor/g_c_d\<close>*)
    4.55 -    val (ctxt, stmt) = get_vc thy vc_name
    4.56 +    val (ctxt(*Element.context_i list*), stmt) = get_vc thy vc_name
    4.57  (*//--------------------------------- new code --------------------------------\\*)
    4.58  (**)val {thy_id, pbl_id, (*givens, wheres, ..*)...} = ParseC.read_out_problem problem(*_headline*)
    4.59  (** )val (thy_id, pbl_id) = ParseC.read_out_headline problem( *_headline*)
    4.60      val refs' = Refs_Data.get thy
    4.61      val (refs as (_, pbl_id, _), o_model) = prefer_input (thy_id, pbl_id) refs' (OMod_Data.get thy)
    4.62      val i_model = I_Model.initPIDE pbl_id
    4.63 +    val thy = IMod_Data.put i_model (* the Model-items with Descriptor only *)
    4.64  (*
    4.65    TODO: present Specification = i_model () + refs via PIDE
    4.66  *)
    4.67  (*----------------------------------- new code ----------------------------------*)
    4.68      val _ = @{print} {a = "prove_vc", o_model = o_model, refs = refs, i_model = i_model}
    4.69  (*\\--------------------------------- new code --------------------------------//*)
    4.70 +    val ctxt = ctxt
    4.71    in
    4.72      Specification.theorem true Thm.theoremK NONE
    4.73        (fn thmss => (Local_Theory.background_theory