(*  Title:      src/Tools/isac/BridgeJEdit/Calculation.thy

     Author:     Walther Neuper, JKU Linz

     (c) due to copyright terms

 Outer syntax for Isabelle/Isac's Calculation.

 *)

 theory Calculation

 imports

   "~~/src/Tools/isac/MathEngine/MathEngine"

 (**)"HOL-SPARK.SPARK" (** ) preliminarily for parsing Example files *)

 (** )"HOL-Word.Word"( ** ) trial on ERROR in definition sdiv below *)

 keywords

     "Example" :: thy_load ("str") (* "spark_vc" :: thy_goal *)

   and "Problem" :: thy_goal (* root-problem + recursively in Solution *)

   and "Specification" "Model" "References" "Solution" (* structure only *)

   and"Given" "Find" "Relate" "Where" (* await input of term *)

   and "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *)

   and "RProblem" "RMethod" (* await input of string list *)

     "Tactic" (* optional for each step 0..end of calculation *)

 (*//-------------------- investigate Outer_Syntax.local_theory_to_proof -------------------\\*)

   and"global_interpretationC" :: thy_goal

 (*\\-------------------- investigate Outer_Syntax.local_theory_to_proof -------------------//*)

 begin

 (**)ML_file parseC.sml(**)

 section \<open>new code for Outer_Syntax Example, Problem, ...\<close>

 subsection \<open>code for Example\<close>

 ML \<open>

 \<close> ML \<open>

 structure Refs_Data = Theory_Data

 (

   type T = References.T

   val empty : T = References.empty

   val extend = I

   fun merge (_, refs) = refs

 );

 (*/----------------------------- shift to test/../? ----------------------------------------\*)

 (* Pure/context.ML

 signature THEORY_DATA =

 sig

   type T

   val get: theory -> T

   val put: T -> theory -> theory

   val map: (T -> T) -> theory -> theory

 end;*)

 (*

 Refs_Data.empty;                                    (*in Refs_Data defined workers are hidden*)

 Refs_Data.extend;                                   (*in Refs_Data defined workers are hidden*)

 Refs_Data.merge;                                    (*in Refs_Data defined workers are hidden*)

 ML error\<^here>:

 Value or constructor (empty) has not been declared in structure Refs *)

 Refs_Data.get: theory -> Refs_Data.T;                            (*from signature THEORY_DATA*)

 Refs_Data.put: Refs_Data.T -> theory -> theory;                  (*from signature THEORY_DATA*)

 Refs_Data.map: (Refs_Data.T -> Refs_Data.T) -> theory -> theory; (*from signature THEORY_DATA*)

 (*\----------------------------- shift to test/../? ----------------------------------------/*)

 \<close> ML \<open>

 structure OMod_Data = Theory_Data

 (

   type T = O_Model.T

   val empty : T = []

   val extend = I

   fun merge (_, o_model) = o_model

 )

 \<close> ML \<open>

 structure Ctxt_Data = Theory_Data

 (

   type T = Proof.context

   val empty : T = ContextC.empty

   val extend = I

   fun merge (_, ctxt) = ctxt

 )

 \<close> ML \<open>

 fun store_and_show formalise thy =

   let

 (**)val file_read_correct = case formalise of xxx as

       [(["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"],

         ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))] => hd xxx

       | _ => error "magic failed: handling file exp_Statics_Biegel_Timischl_7-70.str failed"

 (**)

     val formalise = hd formalise (*we expect only one Formalise.T in the list*)

     val (hdlPIDE, _, refs, o_model, var_type_ctxt) = Step_Specify.initialisePIDE formalise

   (*              ^^ TODO remove with cleanup in nxt_specify_init_calc *)

 (*

   TODO: present "Problem hdlPIDE" via PIDE

 *)

   in

     thy

       |> Refs_Data.put refs

       |> OMod_Data.put o_model

       |> Ctxt_Data.put var_type_ctxt

   end;

 \<close> ML \<open>

 fun load_formalisation parser (files, _) thy =

   let

     val ([{lines, pos, ...}: Token.file], thy') = files thy;

   in

     store_and_show

       (ParseC.read_out_formalise (fst (parser (fst (ParseC.scan' pos (cat_lines lines))))))

         thy'

   end;

 \<close> ML \<open>

 \<close>

 subsection \<open>code to write Problem ("Biegelinie", ["Biegelinien"]) to thy\<close>

 ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 subsection \<open>code for Problem\<close>

 text \<open>

   Again, we copy code from spark_vc into Calculation.thy and

   add functionality for Problem

   such that the code keeps running during adaption from spark_vc to Problem.

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> 

 subsubsection \<open>copied from fdl_parser.ML\<close>

 ML \<open>

 \<close> ML \<open>

 datatype expr =

     Ident of string

   | Number of int

   | Quantifier of string * string list * string * expr

   | Funct of string * expr list

   | Element of expr * expr list

   | Update of expr * expr list * expr

   | Record of string * (string * expr) list

   | Array of string * expr option *

       ((expr * expr option) list list * expr) list;

 \<close> ML \<open>

   datatype fdl_type =

       Basic_Type of string

     | Enum_Type of string list

     | Array_Type of string list * string

     | Record_Type of (string list * string) list

     | Pending_Type;

 \<close> ML \<open>

 (* also store items in a list to preserve order *)

 type 'a tab = 'a Symtab.table * (string * 'a) list;

 \<close> ML \<open>

 fun lookup ((tab, _) : 'a tab) = Symtab.lookup tab;

 \<close> ML \<open>

 \<close>

 subsubsection \<open>copied from spark_vcs.ML\<close>

 ML \<open>

 \<close> ML \<open>

 fun err_unfinished () = error "An unfinished SPARK environment is still open."

 \<close> ML \<open>

 val strip_number = apply2 implode o chop_suffix Fdl_Lexer.is_digit o raw_explode;

 \<close> ML \<open>

 val name_ord = prod_ord string_ord (option_ord int_ord) o

   apply2 (strip_number ##> Int.fromString);

 \<close> ML \<open>

 structure VCtab = Table(type key = string val ord = name_ord);

 \<close> ML \<open>

 val builtin = Symtab.make (map (rpair ())

   ["->", "<->", "or", "and", "not", "=", "<>", "<", ">", "<=", ">=",

    "+", "-", "*", "/", "div", "mod", "**"]);

 \<close> ML \<open>

 val is_pfun =

   Symtab.defined builtin orf

   can (unprefix "fld_") orf can (unprefix "upf_") orf

   can (unsuffix "__pos") orf can (unsuffix "__val") orf

   equal "succ" orf equal "pred";

 \<close> ML \<open>

 fun fold_opt f = the_default I o Option.map f;

 fun fold_pair f g (x, y) = f x #> g y;

 \<close> ML \<open>

 fun fold_expr f g (Funct (s, es)) = f s #> fold (fold_expr f g) es

   | fold_expr f g (Ident s) = g s

   | fold_expr f g (Number _) = I

   | fold_expr f g (Quantifier (_, _, _, e)) = fold_expr f g e

   | fold_expr f g (Element (e, es)) =

       fold_expr f g e #> fold (fold_expr f g) es

   | fold_expr f g (Update (e, es, e')) =

       fold_expr f g e #> fold (fold_expr f g) es #> fold_expr f g e'

   | fold_expr f g (Record (_, flds)) = fold (fold_expr f g o snd) flds

   | fold_expr f g (Array (_, default, assocs)) =

       fold_opt (fold_expr f g) default #>

       fold (fold_pair

         (fold (fold (fold_pair

           (fold_expr f g) (fold_opt (fold_expr f g)))))

         (fold_expr f g)) assocs;

 \<close> ML \<open>

 fun add_expr_pfuns funs = fold_expr

   (fn s => if is_pfun s then I else insert (op =) s)

   (fn s => if is_none (lookup funs s) then I else insert (op =) s);

 \<close> ML \<open>

 fun fold_vcs f vcs =

   VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs;

 \<close> ML \<open>

 fun lookup_prfx "" tab s = Symtab.lookup tab s

   | lookup_prfx prfx tab s = (case Symtab.lookup tab s of

         NONE => Symtab.lookup tab (prfx ^ "__" ^ s)

       | x => x);

 \<close> ML \<open>

 fun pfuns_of_vcs prfx funs pfuns vcs =

   fold_vcs (add_expr_pfuns funs o snd) vcs [] |>

   filter (is_none o lookup_prfx prfx pfuns);

 \<close> ML \<open>

 fun pfuns_of_vcs prfx funs pfuns vcs =

   fold_vcs (add_expr_pfuns funs o snd) vcs [] |>

   filter (is_none o lookup_prfx prfx pfuns);

 \<close> ML \<open>

 structure VCs = Theory_Data

 (

   type T =

     {pfuns: ((string list * string) option * term) Symtab.table,

      type_map: (typ * (string * string) list) Symtab.table,

      env:

        {ctxt: Element.context_i list,

         defs: (binding * thm) list,

         types: fdl_type tab,

         funs: (string list * string) tab,

         pfuns: ((string list * string) option * term) Symtab.table,

         ids: (term * string) Symtab.table * Name.context,

         proving: bool,

         vcs: (string * thm list option *

           (string * expr) list * (string * expr) list) VCtab.table,

         path: Path.T,

         prefix: string} option}

   val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE}

   val extend = I

   fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE},

         {pfuns = pfuns2, type_map = type_map2, env = NONE}) =

         {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),

          type_map = Symtab.merge (op =) (type_map1, type_map2),

          env = NONE}

     | merge _ = err_unfinished ()

 )

 \<close> ML \<open>

 fun get_type thy prfx ty =

   let val {type_map, ...} = VCs.get thy

   in lookup_prfx prfx type_map ty end;

 \<close> ML \<open>

 fun mk_type' _ _ "integer" = (HOLogic.intT, [])

   | mk_type' _ _ "boolean" = (HOLogic.boolT, [])

   | mk_type' thy prfx ty =

       (case get_type thy prfx ty of

          NONE =>

            (Syntax.check_typ (Proof_Context.init_global thy)

               (Type (Sign.full_name thy (Binding.name ty), [])),

             [])

        | SOME p => p);

 \<close> ML \<open>

 fun mk_type thy prfx ty = fst (mk_type' thy prfx ty);

 \<close> ML \<open>

 fun pfun_type thy prfx (argtys, resty) =

   map (mk_type thy prfx) argtys ---> mk_type thy prfx resty;

 \<close> ML \<open>

 fun declare_missing_pfuns thy prfx funs pfuns vcs (tab, ctxt) =

   let

     val (fs, (tys, Ts)) =

       pfuns_of_vcs prfx funs pfuns vcs |>

       map_filter (fn s => lookup funs s |>

         Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |>

       split_list ||> split_list;

     val (fs', ctxt') = fold_map Name.variant fs ctxt

   in

     (fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns,

      Element.Fixes (map2 (fn s => fn T =>

        (Binding.name s, SOME T, NoSyn)) fs' Ts),

      (tab, ctxt'))

   end;

 \<close> ML \<open>

 fun strip_underscores s =

   strip_underscores (unsuffix "_" s) handle Fail _ => s;

 fun strip_tilde s =

   unsuffix "~" s ^ "_init" handle Fail _ => s;

 \<close> ML \<open>

 val mangle_name = strip_underscores #> strip_tilde;

 \<close> ML \<open>

 fun mk_variables thy prfx xs ty (tab, ctxt) =

   let

     val T = mk_type thy prfx ty;

     val (ys, ctxt') = fold_map Name.variant (map mangle_name xs) ctxt;

     val zs = map (Free o rpair T) ys;

   in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;

 \<close> ML \<open>

 fun mk_unop s t =

   let val T = fastype_of t

   in Const (s, T --> T) $ t end;

 \<close> ML \<open>

 val booleanN = "boolean";

 val integerN = "integer";

 \<close> ML \<open>

 val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode;

 val lcase_eq = (op =) o apply2 (to_lower o Long_Name.base_name);

 \<close> ML \<open>

 fun find_field [] fname fields =

       find_first (curry lcase_eq fname o fst) fields

   | find_field cmap fname fields =

       (case AList.lookup (op =) cmap fname of

          NONE => NONE

        | SOME fname' => SOME (fname', the (AList.lookup (op =) fields fname')));

 \<close> ML \<open>

 fun get_record_info thy T = (case Record.dest_recTs T of

     [(tyname, [\<^typ>\<open>unit\<close>])] =>

       Record.get_info thy (Long_Name.qualifier tyname)

   | _ => NONE);

 \<close> ML \<open>

 fun find_field' fname = get_first (fn (flds, fldty) =>

   if member (op =) flds fname then SOME fldty else NONE);

 \<close> ML \<open>

 fun invert_map [] = I

   | invert_map cmap =

       map (apfst (the o AList.lookup (op =) (map swap cmap)));

 \<close> ML \<open>

 fun mk_times (t, u) =

   let

     val setT = fastype_of t;

     val T = HOLogic.dest_setT setT;

     val U = HOLogic.dest_setT (fastype_of u)

   in

     Const (\<^const_name>\<open>Sigma\<close>, setT --> (T --> HOLogic.mk_setT U) -->

       HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)

   end;

 \<close> ML \<open>

 fun term_of_expr thy prfx types pfuns =

   let

     fun tm_of vs (Funct ("->", [e, e'])) =

           (HOLogic.mk_imp (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

       | tm_of vs (Funct ("<->", [e, e'])) =

           (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

       | tm_of vs (Funct ("or", [e, e'])) =

           (HOLogic.mk_disj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

       | tm_of vs (Funct ("and", [e, e'])) =

           (HOLogic.mk_conj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

       | tm_of vs (Funct ("not", [e])) =

           (HOLogic.mk_not (fst (tm_of vs e)), booleanN)

       | tm_of vs (Funct ("=", [e, e'])) =

           (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

       | tm_of vs (Funct ("<>", [e, e'])) = (HOLogic.mk_not

           (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e'))), booleanN)

       | tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>

           (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

       | tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>

           (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)

       | tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>

           (fst (tm_of vs e), fst (tm_of vs e')), booleanN)

       | tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>

           (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)

       | tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>plus\<close>

           (fst (tm_of vs e), fst (tm_of vs e')), integerN)

       | tm_of vs (Funct ("-", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>minus\<close>

           (fst (tm_of vs e), fst (tm_of vs e')), integerN)

       | tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>times\<close>

           (fst (tm_of vs e), fst (tm_of vs e')), integerN)

       | tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>divide\<close>

           (fst (tm_of vs e), fst (tm_of vs e')), integerN)

       | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>sdiv\<close>

           (fst (tm_of vs e), fst (tm_of vs e')), integerN)

       | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>modulo\<close>

           (fst (tm_of vs e), fst (tm_of vs e')), integerN)

       | tm_of vs (Funct ("-", [e])) =

           (mk_unop \<^const_name>\<open>uminus\<close> (fst (tm_of vs e)), integerN)

       | tm_of vs (Funct ("**", [e, e'])) =

           (Const (\<^const_name>\<open>power\<close>, HOLogic.intT --> HOLogic.natT -->

              HOLogic.intT) $ fst (tm_of vs e) $

                (\<^const>\<open>nat\<close> $ fst (tm_of vs e')), integerN)

       | tm_of (tab, _) (Ident s) =

           (case Symtab.lookup tab s of

              SOME t_ty => t_ty

            | NONE => (case lookup_prfx prfx pfuns s of

                SOME (SOME ([], resty), t) => (t, resty)

              | _ => error ("Undeclared identifier " ^ s)))

       | tm_of _ (Number i) = (HOLogic.mk_number HOLogic.intT i, integerN)

       | tm_of vs (Quantifier (s, xs, ty, e)) =

           let

             val (ys, vs') = mk_variables thy prfx xs ty vs;

             val q = (case s of

                 "for_all" => HOLogic.mk_all

               | "for_some" => HOLogic.mk_exists)

           in

             (fold_rev (fn Free (x, T) => fn t => q (x, T, t))

                ys (fst (tm_of vs' e)),

              booleanN)

           end

       | tm_of vs (Funct (s, es)) =

           (* record field selection *)

           (case try (unprefix "fld_") s of

              SOME fname => (case es of

                [e] =>

                  let

                    val (t, rcdty) = tm_of vs e;

                    val (rT, cmap) = mk_type' thy prfx rcdty

                  in case (get_record_info thy rT, lookup types rcdty) of

                      (SOME {fields, ...}, SOME (Record_Type fldtys)) =>

                        (case (find_field cmap fname fields,

                             find_field' fname fldtys) of

                           (SOME (fname', fT), SOME fldty) =>

                             (Const (fname', rT --> fT) $ t, fldty)

                         | _ => error ("Record " ^ rcdty ^

                             " has no field named " ^ fname))

                    | _ => error (rcdty ^ " is not a record type")

                  end

              | _ => error ("Function " ^ s ^ " expects one argument"))

            | NONE =>

           (* record field update *)

           (case try (unprefix "upf_") s of

              SOME fname => (case es of

                [e, e'] =>

                  let

                    val (t, rcdty) = tm_of vs e;

                    val (rT, cmap) = mk_type' thy prfx rcdty;

                    val (u, fldty) = tm_of vs e';

                    val fT = mk_type thy prfx fldty

                  in case get_record_info thy rT of

                      SOME {fields, ...} =>

                        (case find_field cmap fname fields of

                           SOME (fname', fU) =>

                             if fT = fU then

                               (Const (fname' ^ "_update",

                                  (fT --> fT) --> rT --> rT) $

                                    Abs ("x", fT, u) $ t,

                                rcdty)

                             else error ("Type\n" ^

                               Syntax.string_of_typ_global thy fT ^

                               "\ndoes not match type\n" ^

                               Syntax.string_of_typ_global thy fU ^

                               "\nof field " ^ fname)

                         | NONE => error ("Record " ^ rcdty ^

                             " has no field named " ^ fname))

                    | _ => error (rcdty ^ " is not a record type")

                  end

              | _ => error ("Function " ^ s ^ " expects two arguments"))

            | NONE =>

           (* enumeration type to integer *)

           (case try (unsuffix "__pos") s of

              SOME tyname => (case es of

                [e] => (Const (\<^const_name>\<open>pos\<close>,

                    mk_type thy prfx tyname --> HOLogic.intT) $ fst (tm_of vs e),

                  integerN)

              | _ => error ("Function " ^ s ^ " expects one argument"))

            | NONE =>

           (* integer to enumeration type *)

           (case try (unsuffix "__val") s of

              SOME tyname => (case es of

                [e] => (Const (\<^const_name>\<open>val\<close>,

                    HOLogic.intT --> mk_type thy prfx tyname) $ fst (tm_of vs e),

                  tyname)

              | _ => error ("Function " ^ s ^ " expects one argument"))

            | NONE =>

           (* successor / predecessor of enumeration type element *)

           if s = "succ" orelse s = "pred" then (case es of

               [e] =>

                 let

                   val (t, tyname) = tm_of vs e;

                   val T = mk_type thy prfx tyname

                 in (Const

                   (if s = "succ" then \<^const_name>\<open>succ\<close>

                    else \<^const_name>\<open>pred\<close>, T --> T) $ t, tyname)

                 end

             | _ => error ("Function " ^ s ^ " expects one argument"))

           (* user-defined proof function *)

           else

             (case lookup_prfx prfx pfuns s of

                SOME (SOME (_, resty), t) =>

                  (list_comb (t, map (fst o tm_of vs) es), resty)

              | _ => error ("Undeclared proof function " ^ s))))))

       | tm_of vs (Element (e, es)) =

           let val (t, ty) = tm_of vs e

           in case lookup types ty of

               SOME (Array_Type (_, elty)) =>

                 (t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es), elty)

             | _ => error (ty ^ " is not an array type")

           end

       | tm_of vs (Update (e, es, e')) =

           let val (t, ty) = tm_of vs e

           in case lookup types ty of

               SOME (Array_Type (idxtys, elty)) =>

                 let

                   val T = foldr1 HOLogic.mk_prodT

                     (map (mk_type thy prfx) idxtys);

                   val U = mk_type thy prfx elty;

                   val fT = T --> U

                 in

                   (Const (\<^const_name>\<open>fun_upd\<close>, fT --> T --> U --> fT) $

                      t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $

                        fst (tm_of vs e'),

                    ty)

                 end

             | _ => error (ty ^ " is not an array type")

           end

       | tm_of vs (Record (s, flds)) =

           let

             val (T, cmap) = mk_type' thy prfx s;

             val {extension = (ext_name, _), fields, ...} =

               (case get_record_info thy T of

                  NONE => error (s ^ " is not a record type")

                | SOME info => info);

             val flds' = map (apsnd (tm_of vs)) flds;

             val fnames = fields |> invert_map cmap |>

               map (Long_Name.base_name o fst);

             val fnames' = map fst flds;

             val (fvals, ftys) = split_list (map (fn s' =>

               case AList.lookup lcase_eq flds' s' of

                 SOME fval_ty => fval_ty

               | NONE => error ("Field " ^ s' ^ " missing in record " ^ s))

                   fnames);

             val _ = (case subtract lcase_eq fnames fnames' of

                 [] => ()

               | xs => error ("Extra field(s) " ^ commas xs ^

                   " in record " ^ s));

             val _ = (case duplicates (op =) fnames' of

                 [] => ()

               | xs => error ("Duplicate field(s) " ^ commas xs ^

                   " in record " ^ s))

           in

             (list_comb

                (Const (ext_name,

                   map (mk_type thy prfx) ftys @ [HOLogic.unitT] ---> T),

                 fvals @ [HOLogic.unit]),

              s)

           end

       | tm_of vs (Array (s, default, assocs)) =

           (case lookup types s of

              SOME (Array_Type (idxtys, elty)) =>

                let

                  val Ts = map (mk_type thy prfx) idxtys;

                  val T = foldr1 HOLogic.mk_prodT Ts;

                  val U = mk_type thy prfx elty;

                  fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)]

                    | mk_idx' T (e, SOME e') = Const (\<^const_name>\<open>atLeastAtMost\<close>,

                        T --> T --> HOLogic.mk_setT T) $

                          fst (tm_of vs e) $ fst (tm_of vs e');

                  fun mk_idx idx =

                    if length Ts <> length idx then

                      error ("Arity mismatch in construction of array " ^ s)

                    else foldr1 mk_times (map2 mk_idx' Ts idx);

                  fun mk_upd (idxs, e) t =

                    if length idxs = 1 andalso forall (is_none o snd) (hd idxs)

                    then

                      Const (\<^const_name>\<open>fun_upd\<close>, (T --> U) -->

                          T --> U --> T --> U) $ t $

                        foldl1 HOLogic.mk_prod

                          (map (fst o tm_of vs o fst) (hd idxs)) $

                        fst (tm_of vs e)

                    else

                      Const (\<^const_name>\<open>fun_upds\<close>, (T --> U) -->

                          HOLogic.mk_setT T --> U --> T --> U) $ t $

                        foldl1 (HOLogic.mk_binop \<^const_name>\<open>sup\<close>)

                          (map mk_idx idxs) $

                        fst (tm_of vs e)

                in

                  (fold mk_upd assocs

                     (case default of

                        SOME e => Abs ("x", T, fst (tm_of vs e))

                      | NONE => Const (\<^const_name>\<open>undefined\<close>, T --> U)),

                   s)

                end

            | _ => error (s ^ " is not an array type"))

   in tm_of end;

 \<close> ML \<open>

 fun mk_pat s = (case Int.fromString s of

     SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))]

   | NONE => error ("Bad conclusion identifier: C" ^ s));

 \<close> ML \<open>

 fun mk_vc thy prfx types pfuns ids name_concl (tr, proved, ps, cs) =

   let val prop_of =

     HOLogic.mk_Trueprop o fst o term_of_expr thy prfx types pfuns ids

   in

     (tr, proved,

      Element.Assumes (map (fn (s', e) =>

        ((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps),

      Element.Shows (map (fn (s', e) =>

        (if name_concl then (Binding.name ("C" ^ s'), [])

         else Binding.empty_atts,

         [(prop_of e, mk_pat s')])) cs))

   end;

 \<close> ML \<open>

 (*val lookup_vc: theory -> bool -> string -> (Element.context_i list *

     (string * thm list option * Element.context_i * Element.statement_i)) option

 *)

 fun lookup_vc thy name_concl name =

   (case VCs.get thy of

     {env = SOME {vcs, types, funs, pfuns, ids, ctxt, prefix, ...}, ...} =>

       (case VCtab.lookup vcs name of

          SOME vc =>

            let val (pfuns', ctxt', ids') =

              declare_missing_pfuns thy prefix funs pfuns vcs ids

            in

              SOME (ctxt @ [ctxt'],

                mk_vc thy prefix types pfuns' ids' name_concl vc)

            end

        | NONE => NONE)

   | _ => NONE);

 \<close> ML \<open>

 \<close> 

 subsubsection \<open>copied from spark_commands.ML\<close>

 ML \<open>

 \<close> ML \<open>

 fun get_vc thy vc_name =

   (case SPARK_VCs.lookup_vc thy false vc_name of

     SOME (ctxt, (_, proved, ctxt', stmt)) =>

       if is_some proved then

         error ("The verification condition " ^

           quote vc_name ^ " has already been proved.")

       else (ctxt @ [ctxt'], stmt)

   | NONE => error ("There is no verification condition " ^

       quote vc_name ^ "."));

 \<close> ML \<open>

 (*

 val prefer_input: ThyC.id * Problem.id -> References.T -> O_Model.T -> References.T * O_Model.T

 *)

 fun prefer_input (inthy, inpbl : Problem.id) (thy, pbl, met_id) o_model =

   if inthy = thy andalso inpbl = pbl

   then ((thy, pbl, met_id) : References.T, o_model)

   else ((inthy, inpbl, Method.id_empty), [])

 \<close> ML \<open>

 (*

 val prove_vc : string -> Proof.context -> Proof.state

 \<rightarrow>

 val prove_vc : string -> Proof.context -> Proof.state

 *)

 fun prove_vc vc_name lthy =

   let

     val _ = @{print} {a = "//--- Spark_Commands.prove_vc", vc_name = vc_name}

     val thy = Proof_Context.theory_of lthy;

     val (ctxt, stmt) = get_vc thy vc_name

 (*//--------------------------------- new code --------------------------------\\*)

     val refs'' = ("Biegelinie", ["Biegelinien"]) (*until Parse.name \<rightarrow> ParseC.problem_headline*)

     val refs' = Refs_Data.get thy

     val (refs as (_, pbl_id, _), o_model) = prefer_input refs'' refs' (OMod_Data.get thy)

     val i_model = I_Model.initPIDE pbl_id

 (*

   TODO: present Specification = i_model () + refs via PIDE

 *)

 (*----------------------------------- new code ----------------------------------*)

     val _ = @{print} {a = "prove_vc", o_model = o_model, refs = refs, i_model = i_model}

 (*\\--------------------------------- new code --------------------------------//*)

   in

     Specification.theorem true Thm.theoremK NONE

       (fn thmss => (Local_Theory.background_theory

          (SPARK_VCs.mark_proved vc_name (flat thmss))))

       (Binding.name vc_name, []) [] ctxt stmt false lthy

   end;

 \<close> ML \<open>

 \<close>

 section \<open>setup command_keyword \<close>

 ML \<open>

 \<close> ML \<open>

 val _ =                                                  

   Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file"

     (Resources.provide_parse_files "Example" -- Parse.parname

       >> (Toplevel.theory o (load_formalisation ParseC.formalisation)));

 \<close> ML \<open>

 val _ =

   Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>Problem\<close>

     "start a Specification, either from scratch or from preceding 'Example'"

     (Parse.name >> prove_vc);

 \<close> ML \<open>

 \<close>

 subsection \<open>test runs with Example\<close>

 text \<open>

   Starting the Calculation for the Example requires session Isac with Isac.Biegelinie etc.

   So, do ~~$ ./zcoding-to-test.sh and use Test_Some.thy to evaluate

     Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>

   This now gives no error, but also no <Output>. See child of 3ea616c84845.

 \<close>

 (*required for proof below..*)

 spark_proof_functions

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

 (**)

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

 (*Output..* )

 The following verification conditions remain to be proved:

   procedure_g_c_d_4

   procedure_g_c_d_11

 ( **)

 spark_vc procedure_g_c_d_4

 proof -

   from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)

   with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1

     by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])

 (** )

 proof -

   from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)

   with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1

     by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])

 next

   from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C2

     by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)

 qed

 ( **)oops(**)

 (** )sorry( **)

 spark_vc procedure_g_c_d_11

   sorry

 (** )

 spark_end

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

 section \<open>adapt spark_vc to Problem\<close>

 subsection \<open>survey on steps of investigation\<close>

 text \<open>

 1.prove_vc: string -> Proof.context -> Proof.state

   ? where does        ^^^^^^^^^^^^^ come from:

   fun get_vc: (case SPARK_VCs.lookup_vc .. of SOME (ctxt, (_, proved, ctxt', stmt)) => ...

 \<close>

 subsection \<open>notes and testbed for spark_vcs\<close>

 ML \<open>

 \<close> ML \<open> (* Outer_Syntax.local_theory_to_proof..global_interpretationC *)

 val interpretation_args_with_defs =

   Parse.!!! Parse_Spec.locale_expression --

     (Scan.optional (\<^keyword>\<open>defines\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"

       -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\<open>=\<close> -- Parse.term))) ([]));

 \<close> ML \<open>

   Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>global_interpretationC\<close>

     "prove interpretation of locale expression into global theory"

     (interpretation_args_with_defs >> (fn (expr, defs) =>

       Interpretation.global_interpretation_cmd expr defs));

 \<close> ML \<open>

     (interpretation_args_with_defs >> (fn (expr, defs) =>

       Interpretation.global_interpretation_cmd expr defs))

 : Token.T list -> (local_theory -> Proof.state) * Token.T list;

 \<close> ML \<open>

 \<close> ML \<open> (* Outer_Syntax.local_theory_to_proof..Problem *)

     (Parse.name >> prove_vc)

 : Token.T list -> (Proof.context -> Proof.state) * Token.T list;

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 subsection \<open>testbed for Problem\<close>

 ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 end

 (*

   ERROR: Found the end of the theory, but the last SPARK environment is still open.

   ..is OK, since "spark_end" does NOT work here for some reason.

 *)