1.1 --- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Thu Feb 11 17:45:29 2021 +0100
1.2 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Wed Feb 17 15:43:34 2021 +0100
1.3 @@ -19,7 +19,9 @@
1.4
1.5 section \<open>example 1\<close>
1.6 spark_vc procedure_g_c_d_4 (*..select 1st VC for proof: *)
1.7 +(*1*)
1.8 proof -
1.9 + (*2*)
1.10 from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)
1.11 (*^^^^^^^^^^^^-Syntax.read_props..Output.report
1.12 ^^^^^^^^^^^^^^^^^-Proof.have_cmd..Output.report 2x
1.13 @@ -35,7 +37,10 @@
1.14 ^^^^^^^^-Proof.gen_show..Output.report 2x*)
1.15 by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)
1.16 (* ^^^-Successful attempt to solve goal by exported rule: gcd d (c - c sdiv d * d) = gcd m n*)
1.17 + (*2a*)
1.18 qed
1.19 + (*2b*)
1.20 +(*1*)
1.21
1.22 subsection \<open>observing interaction on the proof\<close>
1.23 text \<open>
2.1 --- a/src/Pure/Isar/keyword.ML Thu Feb 11 17:45:29 2021 +0100
2.2 +++ b/src/Pure/Isar/keyword.ML Wed Feb 17 15:43:34 2021 +0100
2.3 @@ -82,7 +82,7 @@
2.4 val is_printed: keywords -> string -> bool
2.5 end;
2.6
2.7 -structure Keyword: KEYWORD =
2.8 +structure Keyword(**): KEYWORD(**) =
2.9 struct
2.10
2.11 (** keyword classification **)
2.12 @@ -241,6 +241,7 @@
2.13
2.14 (* command categories *)
2.15
2.16 +(* : Symtab.key list -> keywords -> Symtab.key -> bool*)
2.17 fun command_category ks =
2.18 let
2.19 val tab = Symtab.make_set ks;
3.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Thu Feb 11 17:45:29 2021 +0100
3.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Wed Feb 17 15:43:34 2021 +0100
3.3 @@ -15,7 +15,7 @@
3.4 and "Problem" :: thy_decl (* root-problem + recursively in Solution;
3.5 "spark_vc" :: thy_goal *)
3.6 and "Specification" "Model" "References" "Solution" (* structure only *)
3.7 - and "Given" "Find" "Relate" :: prf_chain (* await input of term *)
3.8 + and "Given" "Find" "Relate" :: prf_chain (* await input of term, cp.from "from".."have" *)
3.9 and "Where" (* only output, preliminarily *)
3.10 and "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *)
3.11 and "RProblem" "RMethod" (* await input of string list *)
3.12 @@ -27,19 +27,13 @@
3.13
3.14
3.15 section \<open>new code for Outer_Syntax Example, Problem, ...\<close>
3.16 -
3.17 -subsection \<open>code for Problem\<close>
3.18 text \<open>
3.19 - Again, we copy code from spark_vc into Calculation.thy and
3.20 - add functionality for Problem
3.21 - such that the code keeps running during adaption from spark_vc to Problem.
3.22 -\<close> ML \<open>
3.23 -\<close> ML \<open>
3.24 -\<close>
3.25 + code for Example, Problem shifted into structure Preliminary.
3.26 +\<close>
3.27
3.28 subsubsection \<open>cp from Pure.thy\<close>
3.29 ML \<open>
3.30 -\<close> ML \<open>
3.31 +\<close> ML \<open> (* for "from" ~~ "Given:" *)
3.32 (* original *)
3.33 val facts = Parse.and_list1 Parse.thms1;
3.34 facts: (Facts.ref * Token.src list) list list parser;
3.35 @@ -50,7 +44,6 @@
3.36 facts: (Facts.ref * Token.src list) list list parser;
3.37 \<close> ML \<open>
3.38 \<close> ML \<open>
3.39 -\<close> ML \<open>
3.40 \<close>
3.41
3.42 subsubsection \<open>TODO\<close>
3.43 @@ -75,59 +68,18 @@
3.44 (* ^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^*)
3.45 \<close> ML \<open>
3.46 val _ =
3.47 - Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>Problem\<close>
3.48 + Outer_Syntax.command \<^command_keyword>\<open>Problem\<close>
3.49 "start a Specification, either from scratch or from preceding 'Example'"
3.50 -(**)(ParseC.problem >> Preliminary.prove_vc);(**)
3.51 -(** )(ParseC.problem_headline >> Preliminary.prove_vc);( **)
3.52 +(** )(ParseC.problem >> (Toplevel.theory o Preliminary.init_specify));( **)
3.53 +(**)(ParseC.problem_headline >> (Toplevel.theory o Preliminary.init_specify));(**)
3.54 \<close> ML \<open>
3.55 -(**)Preliminary.prove_vc: ParseC.problem -> Proof.context -> Proof.state;(**)
3.56 -(* ^^^^^^^^^^^^^ ^^^^^^^^^^^*)
3.57 -SPARK_Commands.prove_vc: string -> Proof.context -> Proof.state
3.58 -\<close> ML \<open> (*//-----------------------------------------------------------------------------\\*)
3.59 +(**) Preliminary.init_specify: ParseC.problem_headline -> theory -> theory;(**)
3.60 +(* ^^^^^^ ^^^^^^*)
3.61 +(**)(Toplevel.theory o Preliminary.init_specify):
3.62 + ParseC.problem_headline -> Toplevel.transition -> Toplevel.transition;(**)
3.63 +(* ^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^*)
3.64 \<close> ML \<open>
3.65 -fun prove_vc (_: ParseC.problem) thy = @{theory}
3.66 \<close> ML \<open>
3.67 -Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition
3.68 -\<close> ML \<open>
3.69 -Toplevel.theory o prove_vc: ParseC.problem -> Toplevel.transition -> Toplevel.transition
3.70 -\<close> ML \<open>
3.71 -\<close> ML \<open>
3.72 -\<close> ML \<open> (*\\-----------------------------------------------------------------------------//*)
3.73 -(* how does ctxt go into Proof.state ?..*)
3.74 -Specification.theorem:
3.75 - bool -> string -> Method.text option -> (thm list list -> local_theory -> local_theory) ->
3.76 - Attrib.binding -> string list -> Element.context_i list -> Element.statement_i -> bool ->
3.77 - local_theory -> Proof.state
3.78 -\<close> ML \<open>
3.79 -K I: Proof.context -> Token.src -> Token.src
3.80 -\<close> ML \<open>
3.81 -\<close> text \<open> NEWS 2014 ? still valid ???
3.82 -* ML antiquotation @ {here} refers to its source position, which is
3.83 -occasionally useful for experimentation and diagnostic purposes.
3.84 -
3.85 -\<close> ML \<open>
3.86 -fn xxx => xxx + 1
3.87 -\<close> ML \<open>
3.88 -fn xxx => xxx + 1
3.89 -\<close> ML \<open>
3.90 -\<close> ML \<open>
3.91 -\<close> ML \<open>
3.92 -\<close> ML \<open>
3.93 -\<close> ML \<open>
3.94 -\<close> ML \<open>
3.95 -\<close> ML \<open>
3.96 -\<close> ML \<open>
3.97 -\<close> ML \<open>
3.98 -\<close> ML \<open>
3.99 -\<close> ML \<open>
3.100 -\<close> ML \<open>
3.101 -\<close> ML \<open>
3.102 -\<close> ML \<open>
3.103 -\<close> ML \<open>
3.104 -\<close> ML \<open>
3.105 -\<close> ML \<open>
3.106 -\<close> ML \<open>
3.107 -\<close> ML \<open> (*-----------------------------------------------------------------------------------*)
3.108 val _ =
3.109 Outer_Syntax.command \<^command_keyword>\<open>Given\<close> "input Given items to the Model of a Specification"
3.110 (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
3.111 @@ -143,35 +95,38 @@
3.112 (Facts.ref * Token.src list) list list -> Toplevel.transition -> Toplevel.transition
3.113 (* ^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^*)
3.114 \<close> ML \<open>
3.115 +\<close> text \<open> NEWS 2014
3.116 +* ML antiquotation @ {here} refers to its source position, which is
3.117 +occasionally useful for experimentation and diagnostic purposes.
3.118 +\<close> ML \<open>
3.119 +@{here}(*val it = {offset=8, end_offset=12, id=-4402}: Position.T*)
3.120 \<close> ML \<open>
3.121 \<close>
3.122
3.123 subsection \<open>test runs with test-Example\<close>
3.124 (**)
3.125 Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>
3.126 -(*(1) outcomment before creating session Isac* )
3.127 +(*(1) outcomment before creating session Isac*)
3.128
3.129 -(*makes Outer_Syntax..Problem run; Isac code is just added..*)
3.130 -spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>
3.131 -
3.132 -(*(2) outcomment before creating session Isac*)
3.133 -Problem ("Biegelinie", ["Biegelinien"]) (*procedure_g_c_d_4 .."Problem" adds to SPARK*)
3.134 +Problem ("Biegelinie", ["Biegelinien"])
3.135 +(*1 collapse* )
3.136 Specification: (*Outer syntax error\<^here>: command expected, but keyword Specification\<^here> was found*)
3.137 -(*1 collapse*)
3.138 + (*2 collapse* )
3.139 Model:
3.140 - Given: "Traegerlaenge ", "Streckenlast "
3.141 - Where: "q_0 ist_integrierbar_auf {| 0, L |}", "0 < L" (*Outer syntax error\<^here>: command expected, but keyword Where\<^here> was found*)
3.142 + Given: "Traegerlaenge " "Streckenlast "
3.143 + Where: "q_0 ist_integrierbar_auf {| 0, L |}" "0 < L" (*Outer syntax error\<^here>: command expected, but keyword Where\<^here> was found*)
3.144 Find: "Biegelinie " (*Bad context for command "Find"\<^here> -- using reset state*)
3.145 Relate: "Randbedingungen "
3.146 References: (*Outer syntax error\<^here>: command expected, but keyword References\<^here> was found*)
3.147 - (*2 collapse*)
3.148 + (*3 collapse*)
3.149 RTheory: ""
3.150 RProblem: ["", ""]
3.151 RMethod: ["", ""]
3.152 - (*2 collapse*)
3.153 -(*1 collapse*)
3.154 + (*3 collapse*)
3.155 + ( *2 collapse*)
3.156 Solution:
3.157 -( *(1) outcomment before creating session Isac*)
3.158 +( *1 collapse*)
3.159 +(*(1) outcomment before creating session Isac*)
3.160 (*
3.161 compare click on above Given: "Traegerlaenge ", "Streckenlast "
3.162 with click on from \<open>0 < d\<close> in SPARK/../Greatest_Common_Divisorthy
3.163 @@ -195,232 +150,9 @@
3.164 # refs = ("Biegelinie", ["Biegelinien"], ["empty_meth_id"]) ..FROM headline ONLY
3.165 \<close>
3.166
3.167 -subsubsection \<open>(1) WITH session Isac (AFTER ./zcoding-to-test.sh)\<close>
3.168 -text \<open>
3.169 -{a = "//--- Spark_Commands.prove_vc", headline =
3.170 - (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),
3.171 - ((((("Specification", ":"),
3.172 - ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]),
3.173 - "Where"),
3.174 - ":"),
3.175 - ["<markup>", "<markup>"]),
3.176 - "Find"),
3.177 - ":"),
3.178 - "<markup>"),
3.179 - "Relate"),
3.180 - ":"),
3.181 - ["<markup>"]),
3.182 - (("References", ":"),
3.183 - (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),
3.184 - "Solution"),
3.185 - ":"),
3.186 - [])),
3.187 - "")} (line 677 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
3.188 -{a = "prove_vc", i_model =
3.189 - [(0, [], false, "#Given",
3.190 - Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
3.191 - (0, [], false, "#Given",
3.192 - Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
3.193 - (0, [], false, "#Find",
3.194 - Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []),
3.195 - (Const ("empty", "??.'a"), []))),
3.196 - (0, [], false, "#Relate",
3.197 - Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []),
3.198 - (Const ("empty", "??.'a"), [])))],
3.199 - o_model =
3.200 - [(1, [1], "#Given", Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), [Free ("L", "real")]),
3.201 - (2, [1], "#Given", Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), [Free ("q_0", "real")]),
3.202 - (3, [1], "#Find", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"),
3.203 - [Free ("y", "real \<Rightarrow> real")]),
3.204 - (4, [1], "#Relate", Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"),
3.205 - [Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
3.206 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("0", "real")) $
3.207 - Free ("0", "real")) $
3.208 - Const ("List.list.Nil", "bool list"),
3.209 - Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
3.210 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("L", "real")) $
3.211 - Free ("0", "real")) $
3.212 - Const ("List.list.Nil", "bool list"),
3.213 - Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
3.214 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
3.215 - (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("0", "real")) $ Free ("0", "real")) $
3.216 - Const ("List.list.Nil", "bool list"),
3.217 - Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $
3.218 - (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $
3.219 - (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("L", "real")) $ Free ("0", "real")) $
3.220 - Const ("List.list.Nil", "bool list")]),
3.221 - (5, [1], "#undef", Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), [Free ("x", "real")]),
3.222 - (6, [1], "#undef", Const ("Biegelinie.GleichungsVariablen", "real list \<Rightarrow> una"),
3.223 - [Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $
3.224 - Const ("List.list.Nil", "real list"),
3.225 - Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_2", "real") $
3.226 - Const ("List.list.Nil", "real list"),
3.227 - Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_3", "real") $
3.228 - Const ("List.list.Nil", "real list"),
3.229 - Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_4", "real") $
3.230 - Const ("List.list.Nil", "real list")]),
3.231 - (7, [1], "#undef", Const ("Biegelinie.AbleitungBiegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"),
3.232 - [Free ("dy", "real \<Rightarrow> real")])],
3.233 - refs =
3.234 - ("Biegelinie", ["Biegelinien"],
3.235 - ["IntegrierenUndKonstanteBestimmen2"])} (line 690 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
3.236 -### Proof_Context.gen_fixes
3.237 -### Proof_Context.gen_fixes
3.238 -### Proof_Context.gen_fixes
3.239 -### Syntax_Phases.check_terms
3.240 -### Syntax_Phases.check_typs
3.241 -### Syntax_Phases.check_typs
3.242 -### Syntax_Phases.check_typs
3.243 -## calling Output.report
3.244 -#### Syntax_Phases.check_props
3.245 -### Syntax_Phases.check_terms
3.246 -### Syntax_Phases.check_typs
3.247 -### Syntax_Phases.check_typs
3.248 -## calling Output.report
3.249 -#### Syntax_Phases.check_props
3.250 -### Syntax_Phases.check_terms
3.251 -### Syntax_Phases.check_typs
3.252 -### Syntax_Phases.check_typs
3.253 -## calling Output.report
3.254 -#### Syntax_Phases.check_props
3.255 -### Syntax_Phases.check_terms
3.256 -### Syntax_Phases.check_typs
3.257 -### Syntax_Phases.check_typs
3.258 -## calling Output.report
3.259 -#### Syntax_Phases.check_props
3.260 -### Syntax_Phases.check_terms
3.261 -### Syntax_Phases.check_typs
3.262 -### Syntax_Phases.check_typs
3.263 -## calling Output.report
3.264 -#### Syntax_Phases.check_props
3.265 -### Syntax_Phases.check_terms
3.266 -### Syntax_Phases.check_typs
3.267 -### Syntax_Phases.check_typs
3.268 -## calling Output.report
3.269 -#### Syntax_Phases.check_props
3.270 -### Syntax_Phases.check_terms
3.271 -### Syntax_Phases.check_typs
3.272 -### Syntax_Phases.check_typs
3.273 -## calling Output.report
3.274 -#### Syntax_Phases.check_props
3.275 -### Syntax_Phases.check_terms
3.276 -### Syntax_Phases.check_typs
3.277 -### Syntax_Phases.check_typs
3.278 -## calling Output.report
3.279 -#### Syntax_Phases.check_props
3.280 -### Syntax_Phases.check_terms
3.281 -### Syntax_Phases.check_typs
3.282 -### Syntax_Phases.check_typs
3.283 -## calling Output.report
3.284 -#### Syntax_Phases.check_props
3.285 -### Syntax_Phases.check_terms
3.286 -### Syntax_Phases.check_typs
3.287 -### Syntax_Phases.check_typs
3.288 -## calling Output.report
3.289 -#### Syntax_Phases.check_props
3.290 -### Syntax_Phases.check_terms
3.291 -### Syntax_Phases.check_typs
3.292 -### Syntax_Phases.check_typs
3.293 -## calling Output.report
3.294 -#### Syntax_Phases.check_props
3.295 -### Syntax_Phases.check_terms
3.296 -### Syntax_Phases.check_typs
3.297 -### Syntax_Phases.check_typs
3.298 -## calling Output.report
3.299 -#### Syntax_Phases.check_props
3.300 -### Syntax_Phases.check_terms
3.301 -### Syntax_Phases.check_typs
3.302 -### Syntax_Phases.check_typs
3.303 -## calling Output.report
3.304 -#### Syntax_Phases.check_props
3.305 -### Syntax_Phases.check_terms
3.306 -### Syntax_Phases.check_typs
3.307 -### Syntax_Phases.check_typs
3.308 -## calling Output.report
3.309 -#### Syntax_Phases.check_props
3.310 -### Syntax_Phases.check_terms
3.311 -### Syntax_Phases.check_typs
3.312 -### Syntax_Phases.check_typs
3.313 -## calling Output.report
3.314 -#### Syntax_Phases.check_props
3.315 -### Syntax_Phases.check_terms
3.316 -### Syntax_Phases.check_typs
3.317 -### Syntax_Phases.check_typs
3.318 -## calling Output.report
3.319 -#### Syntax_Phases.check_props
3.320 -### Syntax_Phases.check_terms
3.321 -### Syntax_Phases.check_typs
3.322 -### Syntax_Phases.check_typs
3.323 -## calling Output.report
3.324 -#### Syntax_Phases.check_props
3.325 -### Syntax_Phases.check_terms
3.326 -### Syntax_Phases.check_typs
3.327 -### Syntax_Phases.check_typs
3.328 -## calling Output.report
3.329 -#### Syntax_Phases.check_props
3.330 -### Syntax_Phases.check_terms
3.331 -### Syntax_Phases.check_typs
3.332 -### Syntax_Phases.check_typs
3.333 -## calling Output.report
3.334 -#### Syntax_Phases.check_props
3.335 -### Syntax_Phases.check_terms
3.336 -### Syntax_Phases.check_typs
3.337 -### Syntax_Phases.check_typs
3.338 -## calling Output.report
3.339 -#### Syntax_Phases.check_props
3.340 -### Syntax_Phases.check_terms
3.341 -### Syntax_Phases.check_typs
3.342 -### Syntax_Phases.check_typs
3.343 -## calling Output.report
3.344 -#### Syntax_Phases.check_props
3.345 -### Syntax_Phases.check_terms
3.346 -### Syntax_Phases.check_typs
3.347 -### Syntax_Phases.check_typs
3.348 -## calling Output.report
3.349 -#### Syntax_Phases.check_props
3.350 -### Syntax_Phases.check_terms
3.351 -### Syntax_Phases.check_typs
3.352 -### Syntax_Phases.check_typs
3.353 -### Syntax_Phases.check_typs
3.354 -## calling Output.report
3.355 -#### Syntax_Phases.check_props
3.356 -### Syntax_Phases.check_terms
3.357 -### Syntax_Phases.check_typs
3.358 -### Syntax_Phases.check_typs
3.359 -### Syntax_Phases.check_typs
3.360 -## calling Output.report
3.361 -### Syntax_Phases.check_terms
3.362 -### Syntax_Phases.check_typs
3.363 -### Syntax_Phases.check_typs
3.364 -### Syntax_Phases.check_typs
3.365 -## calling Output.report
3.366 -### Syntax_Phases.check_terms
3.367 -### Syntax_Phases.check_typs
3.368 -### Syntax_Phases.check_typs
3.369 -### Syntax_Phases.check_typs
3.370 -## calling Output.report
3.371 -### Syntax_Phases.check_terms
3.372 -### Syntax_Phases.check_typs
3.373 -### Syntax_Phases.check_typs
3.374 -### Syntax_Phases.check_typs
3.375 -## calling Output.report
3.376 -### Syntax_Phases.check_terms
3.377 -### Syntax_Phases.check_typs
3.378 -### Syntax_Phases.check_typs
3.379 -### Syntax_Phases.check_typs
3.380 -## calling Output.report
3.381 -### Syntax_Phases.check_terms
3.382 -### Syntax_Phases.check_typs
3.383 -### Syntax_Phases.check_typs
3.384 -### Syntax_Phases.check_typs
3.385 -## calling Output.report
3.386 -### Proof_Context.gen_fixes
3.387 -### Proof_Context.gen_fixes
3.388 -\<close>
3.389 -
3.390 subsubsection \<open>(2) WITHOUT session Isac (AFTER ./ztest-to-coding.sh)\<close>
3.391 text \<open>
3.392 -{a = "//--- Spark_Commands.prove_vc", headline =
3.393 +{a = "//--- Spark_Commands.init_specify", headline =
3.394 (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),
3.395 ((((("Specification", ":"),
3.396 ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]),
3.397 @@ -439,7 +171,7 @@
3.398 ":"),
3.399 [])),
3.400 "")}
3.401 -{a = "prove_vc", i_model =
3.402 +{a = "init_specify", i_model =
3.403 [(0, [], false, "#Given",
3.404 Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),
3.405 (0, [], false, "#Given",
4.1 --- a/src/Tools/isac/BridgeJEdit/preliminary.sml Thu Feb 11 17:45:29 2021 +0100
4.2 +++ b/src/Tools/isac/BridgeJEdit/preliminary.sml Wed Feb 17 15:43:34 2021 +0100
4.3 @@ -14,8 +14,9 @@
4.4 (theory -> Token.file list * theory) * 'c -> theory -> theory
4.5
4.6 (* for keyword Problem*)
4.7 -(**)val prove_vc: ParseC.problem -> Proof.context -> Proof.state(**)
4.8 -(** )val prove_vc: ParseC.problem_headline -> Proof.context -> Proof.state( **)
4.9 +(**)val init_specify: ParseC.problem_headline -> theory -> theory(**)
4.10 +(** )val init_specify: ParseC.problem -> theory -> theory( **)
4.11 +
4.12 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.13 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.14 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.15 @@ -104,505 +105,7 @@
4.16 end;
4.17
4.18 (*** code for keyword Problem ***)
4.19 -(*
4.20 - Code for Isac's keyword Problem is added to SPARK code copied here, too.
4.21 - We leave SPARK code here as long as Isac does not yet adopt SPARK's functionality
4.22 - w.r.t. Outer_Syntax.command.
4.23 -*)
4.24
4.25 -(** copied from fdl_parser.ML **)
4.26 -
4.27 -datatype expr =
4.28 - Ident of string
4.29 - | Number of int
4.30 - | Quantifier of string * string list * string * expr
4.31 - | Funct of string * expr list
4.32 - | Element of expr * expr list
4.33 - | Update of expr * expr list * expr
4.34 - | Record of string * (string * expr) list
4.35 - | Array of string * expr option *
4.36 - ((expr * expr option) list list * expr) list;
4.37 - datatype fdl_type =
4.38 - Basic_Type of string
4.39 - | Enum_Type of string list
4.40 - | Array_Type of string list * string
4.41 - | Record_Type of (string list * string) list
4.42 - | Pending_Type;
4.43 -(* also store items in a list to preserve order *)
4.44 -type 'a tab = 'a Symtab.table * (string * 'a) list;
4.45 -fun lookup ((tab, _) : 'a tab) = Symtab.lookup tab;
4.46 -
4.47 -
4.48 -(** copied from spark_vcs.ML **)
4.49 -
4.50 -fun err_unfinished () = error "An unfinished SPARK environment is still open."
4.51 -val strip_number = apply2 implode o chop_suffix Fdl_Lexer.is_digit o raw_explode;
4.52 -
4.53 -val name_ord = prod_ord string_ord (option_ord int_ord) o
4.54 - apply2 (strip_number ##> Int.fromString);
4.55 -structure VCtab = Table(type key = string val ord = name_ord);
4.56 -val builtin = Symtab.make (map (rpair ())
4.57 - ["->", "<->", "or", "and", "not", "=", "<>", "<", ">", "<=", ">=",
4.58 - "+", "-", "*", "/", "div", "mod", "**"]);
4.59 -
4.60 -open Library; (*orf is infix and cannot take Library.*)
4.61 -val is_pfun =
4.62 - Symtab.defined builtin orf
4.63 - can (unprefix "fld_") orf can (unprefix "upf_") orf
4.64 - can (unsuffix "__pos") orf can (unsuffix "__val") orf
4.65 - Library.equal "succ" orf Library.equal "pred";
4.66 -
4.67 -fun fold_opt f = the_default I o Option.map f;
4.68 -fun fold_pair f g (x, y) = f x #> g y;
4.69 -
4.70 -fun fold_expr f g (Funct (s, es)) = f s #> fold (fold_expr f g) es
4.71 - | fold_expr f g (Ident s) = g s
4.72 - | fold_expr f g (Number _) = I
4.73 - | fold_expr f g (Quantifier (_, _, _, e)) = fold_expr f g e
4.74 - | fold_expr f g (Element (e, es)) =
4.75 - fold_expr f g e #> fold (fold_expr f g) es
4.76 - | fold_expr f g (Update (e, es, e')) =
4.77 - fold_expr f g e #> fold (fold_expr f g) es #> fold_expr f g e'
4.78 - | fold_expr f g (Record (_, flds)) = fold (fold_expr f g o snd) flds
4.79 - | fold_expr f g (Array (_, default, assocs)) =
4.80 - fold_opt (fold_expr f g) default #>
4.81 - fold (fold_pair
4.82 - (fold (fold (fold_pair
4.83 - (fold_expr f g) (fold_opt (fold_expr f g)))))
4.84 - (fold_expr f g)) assocs;
4.85 -
4.86 -fun add_expr_pfuns funs = fold_expr
4.87 - (fn s => if is_pfun s then I else insert (op =) s)
4.88 - (fn s => if is_none (lookup funs s) then I else insert (op =) s);
4.89 -fun fold_vcs f vcs =
4.90 - VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs;
4.91 -fun lookup_prfx "" tab s = Symtab.lookup tab s
4.92 - | lookup_prfx prfx tab s = (case Symtab.lookup tab s of
4.93 - NONE => Symtab.lookup tab (prfx ^ "__" ^ s)
4.94 - | x => x);
4.95 -
4.96 -fun pfuns_of_vcs prfx funs pfuns vcs =
4.97 - fold_vcs (add_expr_pfuns funs o snd) vcs [] |>
4.98 - filter (is_none o lookup_prfx prfx pfuns);
4.99 -structure VCs = Theory_Data
4.100 -(
4.101 - type T =
4.102 - {pfuns: ((string list * string) option * term) Symtab.table,
4.103 - type_map: (typ * (string * string) list) Symtab.table,
4.104 - env:
4.105 - {ctxt: Element.context_i list,
4.106 - defs: (binding * thm) list,
4.107 - types: fdl_type tab,
4.108 - funs: (string list * string) tab,
4.109 - pfuns: ((string list * string) option * term) Symtab.table,
4.110 - ids: (term * string) Symtab.table * Name.context,
4.111 - proving: bool,
4.112 - vcs: (string * thm list option *
4.113 - (string * expr) list * (string * expr) list) VCtab.table,
4.114 - path: Path.T,
4.115 - prefix: string} option}
4.116 - val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE}
4.117 - val extend = I
4.118 - fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE},
4.119 - {pfuns = pfuns2, type_map = type_map2, env = NONE}) =
4.120 - {pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),
4.121 - type_map = Symtab.merge (op =) (type_map1, type_map2),
4.122 - env = NONE}
4.123 - | merge _ = err_unfinished ()
4.124 -)
4.125 -
4.126 -fun get_type thy prfx ty =
4.127 - let val {type_map, ...} = VCs.get thy
4.128 - in lookup_prfx prfx type_map ty end;
4.129 -fun mk_type' _ _ "integer" = (HOLogic.intT, [])
4.130 - | mk_type' _ _ "boolean" = (HOLogic.boolT, [])
4.131 - | mk_type' thy prfx ty =
4.132 - (case get_type thy prfx ty of
4.133 - NONE =>
4.134 - (Syntax.check_typ (Proof_Context.init_global thy)
4.135 - (Type (Sign.full_name thy (Binding.name ty), [])),
4.136 - [])
4.137 - | SOME p => p);
4.138 -fun mk_type thy prfx ty = fst (mk_type' thy prfx ty);
4.139 -fun pfun_type thy prfx (argtys, resty) =
4.140 - map (mk_type thy prfx) argtys ---> mk_type thy prfx resty;
4.141 -fun declare_missing_pfuns thy prfx funs pfuns vcs (tab, ctxt) =
4.142 - let
4.143 - val (fs, (tys, Ts)) =
4.144 - pfuns_of_vcs prfx funs pfuns vcs |>
4.145 - map_filter (fn s => lookup funs s |>
4.146 - Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |>
4.147 - split_list ||> split_list;
4.148 - val (fs', ctxt') = fold_map Name.variant fs ctxt
4.149 - in
4.150 - (fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns,
4.151 - Element.Fixes (map2 (fn s => fn T =>
4.152 - (Binding.name s, SOME T, NoSyn)) fs' Ts),
4.153 - (tab, ctxt'))
4.154 - end;
4.155 -
4.156 -fun strip_underscores s =
4.157 - strip_underscores (unsuffix "_" s) handle Fail _ => s;
4.158 -fun strip_tilde s =
4.159 - unsuffix "~" s ^ "_init" handle Fail _ => s;
4.160 -val mangle_name = strip_underscores #> strip_tilde;
4.161 -
4.162 -fun mk_variables thy prfx xs ty (tab, ctxt) =
4.163 - let
4.164 - val T = mk_type thy prfx ty;
4.165 - val (ys, ctxt') = fold_map Name.variant (map mangle_name xs) ctxt;
4.166 - val zs = map (Free o rpair T) ys;
4.167 - in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
4.168 -fun mk_unop s t =
4.169 - let val T = fastype_of t
4.170 - in Const (s, T --> T) $ t end;
4.171 -
4.172 -val booleanN = "boolean";
4.173 -val integerN = "integer";
4.174 -
4.175 -val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode;
4.176 -val lcase_eq = (op =) o apply2 (to_lower o Long_Name.base_name);
4.177 -
4.178 -fun find_field [] fname fields =
4.179 - find_first (curry lcase_eq fname o fst) fields
4.180 - | find_field cmap fname fields =
4.181 - (case AList.lookup (op =) cmap fname of
4.182 - NONE => NONE
4.183 - | SOME fname' => SOME (fname', the (AList.lookup (op =) fields fname')));
4.184 -fun get_record_info thy T = (case Record.dest_recTs T of
4.185 - [(tyname, [\<^typ>\<open>unit\<close>])] =>
4.186 - Record.get_info thy (Long_Name.qualifier tyname)
4.187 - | _ => NONE);
4.188 -fun find_field' fname = get_first (fn (flds, fldty) =>
4.189 - if member (op =) flds fname then SOME fldty else NONE);
4.190 -
4.191 -fun invert_map [] = I
4.192 - | invert_map cmap =
4.193 - map (apfst (the o AList.lookup (op =) (map swap cmap)));
4.194 -
4.195 -fun mk_times (t, u) =
4.196 - let
4.197 - val setT = fastype_of t;
4.198 - val T = HOLogic.dest_setT setT;
4.199 - val U = HOLogic.dest_setT (fastype_of u)
4.200 - in
4.201 - Const (\<^const_name>\<open>Sigma\<close>, setT --> (T --> HOLogic.mk_setT U) -->
4.202 - HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)
4.203 - end;
4.204 -fun term_of_expr thy prfx types pfuns =
4.205 - let
4.206 - fun tm_of vs (Funct ("->", [e, e'])) =
4.207 - (HOLogic.mk_imp (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
4.208 -
4.209 - | tm_of vs (Funct ("<->", [e, e'])) =
4.210 - (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
4.211 -
4.212 - | tm_of vs (Funct ("or", [e, e'])) =
4.213 - (HOLogic.mk_disj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
4.214 -
4.215 - | tm_of vs (Funct ("and", [e, e'])) =
4.216 - (HOLogic.mk_conj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
4.217 -
4.218 - | tm_of vs (Funct ("not", [e])) =
4.219 - (HOLogic.mk_not (fst (tm_of vs e)), booleanN)
4.220 -
4.221 - | tm_of vs (Funct ("=", [e, e'])) =
4.222 - (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
4.223 -
4.224 - | tm_of vs (Funct ("<>", [e, e'])) = (HOLogic.mk_not
4.225 - (HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e'))), booleanN)
4.226 -
4.227 - | tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
4.228 - (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
4.229 -
4.230 - | tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
4.231 - (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
4.232 -
4.233 - | tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
4.234 - (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
4.235 -
4.236 - | tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
4.237 - (fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
4.238 -
4.239 - | tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>plus\<close>
4.240 - (fst (tm_of vs e), fst (tm_of vs e')), integerN)
4.241 -
4.242 - | tm_of vs (Funct ("-", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>minus\<close>
4.243 - (fst (tm_of vs e), fst (tm_of vs e')), integerN)
4.244 -
4.245 - | tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>times\<close>
4.246 - (fst (tm_of vs e), fst (tm_of vs e')), integerN)
4.247 -
4.248 - | tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>divide\<close>
4.249 - (fst (tm_of vs e), fst (tm_of vs e')), integerN)
4.250 -
4.251 - | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>sdiv\<close>
4.252 - (fst (tm_of vs e), fst (tm_of vs e')), integerN)
4.253 -
4.254 - | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>modulo\<close>
4.255 - (fst (tm_of vs e), fst (tm_of vs e')), integerN)
4.256 -
4.257 - | tm_of vs (Funct ("-", [e])) =
4.258 - (mk_unop \<^const_name>\<open>uminus\<close> (fst (tm_of vs e)), integerN)
4.259 -
4.260 - | tm_of vs (Funct ("**", [e, e'])) =
4.261 - (Const (\<^const_name>\<open>power\<close>, HOLogic.intT --> HOLogic.natT -->
4.262 - HOLogic.intT) $ fst (tm_of vs e) $
4.263 - (\<^const>\<open>nat\<close> $ fst (tm_of vs e')), integerN)
4.264 -
4.265 - | tm_of (tab, _) (Ident s) =
4.266 - (case Symtab.lookup tab s of
4.267 - SOME t_ty => t_ty
4.268 - | NONE => (case lookup_prfx prfx pfuns s of
4.269 - SOME (SOME ([], resty), t) => (t, resty)
4.270 - | _ => error ("Undeclared identifier " ^ s)))
4.271 -
4.272 - | tm_of _ (Number i) = (HOLogic.mk_number HOLogic.intT i, integerN)
4.273 -
4.274 - | tm_of vs (Quantifier (s, xs, ty, e)) =
4.275 - let
4.276 - val (ys, vs') = mk_variables thy prfx xs ty vs;
4.277 - val q = (case s of
4.278 - "for_all" => HOLogic.mk_all
4.279 - | "for_some" => HOLogic.mk_exists)
4.280 - in
4.281 - (fold_rev (fn Free (x, T) => fn t => q (x, T, t))
4.282 - ys (fst (tm_of vs' e)),
4.283 - booleanN)
4.284 - end
4.285 -
4.286 - | tm_of vs (Funct (s, es)) =
4.287 -
4.288 - (* record field selection *)
4.289 - (case try (unprefix "fld_") s of
4.290 - SOME fname => (case es of
4.291 - [e] =>
4.292 - let
4.293 - val (t, rcdty) = tm_of vs e;
4.294 - val (rT, cmap) = mk_type' thy prfx rcdty
4.295 - in case (get_record_info thy rT, lookup types rcdty) of
4.296 - (SOME {fields, ...}, SOME (Record_Type fldtys)) =>
4.297 - (case (find_field cmap fname fields,
4.298 - find_field' fname fldtys) of
4.299 - (SOME (fname', fT), SOME fldty) =>
4.300 - (Const (fname', rT --> fT) $ t, fldty)
4.301 - | _ => error ("Record " ^ rcdty ^
4.302 - " has no field named " ^ fname))
4.303 - | _ => error (rcdty ^ " is not a record type")
4.304 - end
4.305 - | _ => error ("Function " ^ s ^ " expects one argument"))
4.306 - | NONE =>
4.307 -
4.308 - (* record field update *)
4.309 - (case try (unprefix "upf_") s of
4.310 - SOME fname => (case es of
4.311 - [e, e'] =>
4.312 - let
4.313 - val (t, rcdty) = tm_of vs e;
4.314 - val (rT, cmap) = mk_type' thy prfx rcdty;
4.315 - val (u, fldty) = tm_of vs e';
4.316 - val fT = mk_type thy prfx fldty
4.317 - in case get_record_info thy rT of
4.318 - SOME {fields, ...} =>
4.319 - (case find_field cmap fname fields of
4.320 - SOME (fname', fU) =>
4.321 - if fT = fU then
4.322 - (Const (fname' ^ "_update",
4.323 - (fT --> fT) --> rT --> rT) $
4.324 - Abs ("x", fT, u) $ t,
4.325 - rcdty)
4.326 - else error ("Type\n" ^
4.327 - Syntax.string_of_typ_global thy fT ^
4.328 - "\ndoes not match type\n" ^
4.329 - Syntax.string_of_typ_global thy fU ^
4.330 - "\nof field " ^ fname)
4.331 - | NONE => error ("Record " ^ rcdty ^
4.332 - " has no field named " ^ fname))
4.333 - | _ => error (rcdty ^ " is not a record type")
4.334 - end
4.335 - | _ => error ("Function " ^ s ^ " expects two arguments"))
4.336 - | NONE =>
4.337 -
4.338 - (* enumeration type to integer *)
4.339 - (case try (unsuffix "__pos") s of
4.340 - SOME tyname => (case es of
4.341 - [e] => (Const (\<^const_name>\<open>pos\<close>,
4.342 - mk_type thy prfx tyname --> HOLogic.intT) $ fst (tm_of vs e),
4.343 - integerN)
4.344 - | _ => error ("Function " ^ s ^ " expects one argument"))
4.345 - | NONE =>
4.346 -
4.347 - (* integer to enumeration type *)
4.348 - (case try (unsuffix "__val") s of
4.349 - SOME tyname => (case es of
4.350 - [e] => (Const (\<^const_name>\<open>val\<close>,
4.351 - HOLogic.intT --> mk_type thy prfx tyname) $ fst (tm_of vs e),
4.352 - tyname)
4.353 - | _ => error ("Function " ^ s ^ " expects one argument"))
4.354 - | NONE =>
4.355 -
4.356 - (* successor / predecessor of enumeration type element *)
4.357 - if s = "succ" orelse s = "pred" then (case es of
4.358 - [e] =>
4.359 - let
4.360 - val (t, tyname) = tm_of vs e;
4.361 - val T = mk_type thy prfx tyname
4.362 - in (Const
4.363 - (if s = "succ" then \<^const_name>\<open>succ\<close>
4.364 - else \<^const_name>\<open>pred\<close>, T --> T) $ t, tyname)
4.365 - end
4.366 - | _ => error ("Function " ^ s ^ " expects one argument"))
4.367 -
4.368 - (* user-defined proof function *)
4.369 - else
4.370 - (case lookup_prfx prfx pfuns s of
4.371 - SOME (SOME (_, resty), t) =>
4.372 - (list_comb (t, map (fst o tm_of vs) es), resty)
4.373 - | _ => error ("Undeclared proof function " ^ s))))))
4.374 -
4.375 - | tm_of vs (Element (e, es)) =
4.376 - let val (t, ty) = tm_of vs e
4.377 - in case lookup types ty of
4.378 - SOME (Array_Type (_, elty)) =>
4.379 - (t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es), elty)
4.380 - | _ => error (ty ^ " is not an array type")
4.381 - end
4.382 -
4.383 - | tm_of vs (Update (e, es, e')) =
4.384 - let val (t, ty) = tm_of vs e
4.385 - in case lookup types ty of
4.386 - SOME (Array_Type (idxtys, elty)) =>
4.387 - let
4.388 - val T = foldr1 HOLogic.mk_prodT
4.389 - (map (mk_type thy prfx) idxtys);
4.390 - val U = mk_type thy prfx elty;
4.391 - val fT = T --> U
4.392 - in
4.393 - (Const (\<^const_name>\<open>fun_upd\<close>, fT --> T --> U --> fT) $
4.394 - t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $
4.395 - fst (tm_of vs e'),
4.396 - ty)
4.397 - end
4.398 - | _ => error (ty ^ " is not an array type")
4.399 - end
4.400 -
4.401 - | tm_of vs (Record (s, flds)) =
4.402 - let
4.403 - val (T, cmap) = mk_type' thy prfx s;
4.404 - val {extension = (ext_name, _), fields, ...} =
4.405 - (case get_record_info thy T of
4.406 - NONE => error (s ^ " is not a record type")
4.407 - | SOME info => info);
4.408 - val flds' = map (apsnd (tm_of vs)) flds;
4.409 - val fnames = fields |> invert_map cmap |>
4.410 - map (Long_Name.base_name o fst);
4.411 - val fnames' = map fst flds;
4.412 - val (fvals, ftys) = split_list (map (fn s' =>
4.413 - case AList.lookup lcase_eq flds' s' of
4.414 - SOME fval_ty => fval_ty
4.415 - | NONE => error ("Field " ^ s' ^ " missing in record " ^ s))
4.416 - fnames);
4.417 - val _ = (case subtract lcase_eq fnames fnames' of
4.418 - [] => ()
4.419 - | xs => error ("Extra field(s) " ^ commas xs ^
4.420 - " in record " ^ s));
4.421 - val _ = (case duplicates (op =) fnames' of
4.422 - [] => ()
4.423 - | xs => error ("Duplicate field(s) " ^ commas xs ^
4.424 - " in record " ^ s))
4.425 - in
4.426 - (list_comb
4.427 - (Const (ext_name,
4.428 - map (mk_type thy prfx) ftys @ [HOLogic.unitT] ---> T),
4.429 - fvals @ [HOLogic.unit]),
4.430 - s)
4.431 - end
4.432 -
4.433 - | tm_of vs (Array (s, default, assocs)) =
4.434 - (case lookup types s of
4.435 - SOME (Array_Type (idxtys, elty)) =>
4.436 - let
4.437 - val Ts = map (mk_type thy prfx) idxtys;
4.438 - val T = foldr1 HOLogic.mk_prodT Ts;
4.439 - val U = mk_type thy prfx elty;
4.440 - fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)]
4.441 - | mk_idx' T (e, SOME e') = Const (\<^const_name>\<open>atLeastAtMost\<close>,
4.442 - T --> T --> HOLogic.mk_setT T) $
4.443 - fst (tm_of vs e) $ fst (tm_of vs e');
4.444 - fun mk_idx idx =
4.445 - if length Ts <> length idx then
4.446 - error ("Arity mismatch in construction of array " ^ s)
4.447 - else foldr1 mk_times (map2 mk_idx' Ts idx);
4.448 - fun mk_upd (idxs, e) t =
4.449 - if length idxs = 1 andalso forall (is_none o snd) (hd idxs)
4.450 - then
4.451 - Const (\<^const_name>\<open>fun_upd\<close>, (T --> U) -->
4.452 - T --> U --> T --> U) $ t $
4.453 - foldl1 HOLogic.mk_prod
4.454 - (map (fst o tm_of vs o fst) (hd idxs)) $
4.455 - fst (tm_of vs e)
4.456 - else
4.457 - Const (\<^const_name>\<open>fun_upds\<close>, (T --> U) -->
4.458 - HOLogic.mk_setT T --> U --> T --> U) $ t $
4.459 - foldl1 (HOLogic.mk_binop \<^const_name>\<open>sup\<close>)
4.460 - (map mk_idx idxs) $
4.461 - fst (tm_of vs e)
4.462 - in
4.463 - (fold mk_upd assocs
4.464 - (case default of
4.465 - SOME e => Abs ("x", T, fst (tm_of vs e))
4.466 - | NONE => Const (\<^const_name>\<open>undefined\<close>, T --> U)),
4.467 - s)
4.468 - end
4.469 - | _ => error (s ^ " is not an array type"))
4.470 -
4.471 - in tm_of end;
4.472 -
4.473 -fun mk_pat s = (case Int.fromString s of
4.474 - SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))]
4.475 - | NONE => error ("Bad conclusion identifier: C" ^ s));
4.476 -fun mk_vc thy prfx types pfuns ids name_concl (tr, proved, ps, cs) =
4.477 - let val prop_of =
4.478 - HOLogic.mk_Trueprop o fst o term_of_expr thy prfx types pfuns ids
4.479 - in
4.480 - (tr, proved,
4.481 - Element.Assumes (map (fn (s', e) =>
4.482 - ((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps),
4.483 - Element.Shows (map (fn (s', e) =>
4.484 - (if name_concl then (Binding.name ("C" ^ s'), [])
4.485 - else Binding.empty_atts,
4.486 - [(prop_of e, mk_pat s')])) cs))
4.487 - end;
4.488 -(*val lookup_vc: theory -> bool -> string -> (Element.context_i list *
4.489 - (string * thm list option * Element.context_i * Element.statement_i)) option
4.490 -*)
4.491 -fun lookup_vc thy name_concl name =
4.492 - (case VCs.get thy of
4.493 - {env = SOME {vcs, types, funs, pfuns, ids, ctxt, prefix, ...}, ...} =>
4.494 - (case VCtab.lookup vcs name of
4.495 - SOME vc =>
4.496 - let val (pfuns', ctxt', ids') =
4.497 - declare_missing_pfuns thy prefix funs pfuns vcs ids
4.498 - in
4.499 - SOME (ctxt @ [ctxt'],
4.500 - mk_vc thy prefix types pfuns' ids' name_concl vc)
4.501 - end
4.502 - | NONE => NONE)
4.503 - | _ => NONE);
4.504 -
4.505 -
4.506 -(** copied from spark_commands.ML **)
4.507 -
4.508 -(* get_vc: theory -> string -> (typ, term, thm list) Element.ctxt list * ('a, term) Element.stmt *)
4.509 -fun get_vc thy vc_name =
4.510 - (case SPARK_VCs.lookup_vc thy false vc_name of
4.511 - SOME (ctxt, (_, proved, ctxt', stmt)) =>
4.512 - if is_some proved then
4.513 - error ("The verification condition " ^
4.514 - quote vc_name ^ " has already been proved.")
4.515 - else (ctxt @ [ctxt'], stmt)
4.516 - | NONE => error ("There is no verification condition " ^
4.517 - quote vc_name ^ "."));
4.518 (*
4.519 val prefer_input: ThyC.id * Problem.id -> References.T -> O_Model.T -> References.T * O_Model.T
4.520 *)
4.521 @@ -611,31 +114,17 @@
4.522 then ((thy, pbl, met_id) : References.T, o_model)
4.523 else ((inthy, inpbl, MethodC.id_empty), [])
4.524
4.525 -fun prove_vc (*vc_name*)problem lthy(*Proof.context*) =
4.526 +fun init_specify problem thy =
4.527 let
4.528 - val _ = @{print} {a = "//--- Spark_Commands.prove_vc", headline = problem}
4.529 - val thy = Proof_Context.theory_of lthy;
4.530 - val vc_name = "procedure_g_c_d_4" (*fixed for spark_open \<open>greatest_common_divisor/g_c_d\<close>*)
4.531 - val (ctxt(*Element.context_i list*), stmt) = get_vc thy vc_name
4.532 -(*//--------------------------------- new code --------------------------------\\*)
4.533 -(**)val {thy_id, pbl_id, (*givens, wheres, ..*)...} = ParseC.read_out_problem problem(*_headline*)
4.534 -(** )val (thy_id, pbl_id) = ParseC.read_out_headline problem( *_headline*)
4.535 + val _ = @{print} {a = "//--- Spark_Commands.init_specify", headline = problem}
4.536 + val (thy_id, pbl_id) = ParseC.read_out_headline problem (*how handle Position?!?*)
4.537 val refs' = Refs_Data.get thy
4.538 - val (refs as (_, pbl_id, _), o_model) = prefer_input (thy_id, pbl_id) refs' (OMod_Data.get thy)
4.539 + val ((_, pbl_id, _), _(*o_model*)) =
4.540 + prefer_input (thy_id, pbl_id) refs' (OMod_Data.get thy)
4.541 val i_model = I_Model.initPIDE pbl_id
4.542 - val thy = IMod_Data.put i_model (* the Model-items with Descriptor only *)
4.543 -(*
4.544 - TODO: present Specification = i_model () + refs via PIDE
4.545 -*)
4.546 -(*----------------------------------- new code ----------------------------------*)
4.547 - val _ = @{print} {a = "prove_vc", o_model = o_model, refs = refs, i_model = i_model}
4.548 -(*\\--------------------------------- new code --------------------------------//*)
4.549 - val ctxt = ctxt
4.550 +(* TODO: present Specification = i_model + refs via PIDE, if specify is done explicitly. *)
4.551 in
4.552 - Specification.theorem true Thm.theoremK NONE
4.553 - (fn thmss => (Local_Theory.background_theory
4.554 - (SPARK_VCs.mark_proved vc_name (flat thmss))))
4.555 - (Binding.name vc_name, []) [] ctxt stmt false lthy
4.556 + IMod_Data.put i_model thy (* the Model-items with Descriptor s only *)
4.557 end;
4.558 -
4.559 +(**)
4.560 (**)end(**)