walther@60096
|
1 |
(* Title: src/Tools/isac/BridgeJEdit/Calculation.thy
|
walther@60095
|
2 |
Author: Walther Neuper, JKU Linz
|
walther@60095
|
3 |
(c) due to copyright terms
|
walther@60095
|
4 |
|
walther@60121
|
5 |
Outer syntax for Isabelle/Isac's Calculation.
|
walther@60095
|
6 |
*)
|
walther@60095
|
7 |
|
walther@60095
|
8 |
theory Calculation
|
walther@60115
|
9 |
imports
|
walther@60115
|
10 |
"~~/src/Tools/isac/MathEngine/MathEngine"
|
walther@60121
|
11 |
(**)"HOL-SPARK.SPARK" (** ) preliminarily for parsing Example files *)
|
walther@60123
|
12 |
(** )"HOL-Word.Word"( ** ) trial on ERROR in definition sdiv below *)
|
walther@60095
|
13 |
keywords
|
walther@60127
|
14 |
"Example" :: thy_load ("str") (* "spark_vc" :: thy_goal *)
|
walther@60127
|
15 |
and "Problem" :: thy_goal (* root-problem + recursively in Solution *)
|
walther@60127
|
16 |
and "Specification" "Model" "References" "Solution" (* structure only *)
|
walther@60127
|
17 |
and"Given" "Find" "Relate" "Where" (* await input of term *)
|
walther@60127
|
18 |
and "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *)
|
walther@60127
|
19 |
and "RProblem" "RMethod" (* await input of string list *)
|
walther@60127
|
20 |
"Tactic" (* optional for each step 0..end of calculation *)
|
walther@60127
|
21 |
(*//-------------------- investigate Outer_Syntax.local_theory_to_proof -------------------\\*)
|
walther@60127
|
22 |
and"global_interpretationC" :: thy_goal
|
walther@60127
|
23 |
(*\\-------------------- investigate Outer_Syntax.local_theory_to_proof -------------------//*)
|
walther@60095
|
24 |
begin
|
walther@60095
|
25 |
|
walther@60123
|
26 |
(**)ML_file parseC.sml(**)
|
walther@60095
|
27 |
|
walther@60123
|
28 |
section \<open>new code for Outer_Syntax Example, Problem, ...\<close>
|
walther@60117
|
29 |
|
walther@60123
|
30 |
subsection \<open>code for Example\<close>
|
walther@60106
|
31 |
ML \<open>
|
walther@60097
|
32 |
\<close> ML \<open>
|
walther@60114
|
33 |
structure Refs_Data = Theory_Data
|
walther@60114
|
34 |
(
|
walther@60114
|
35 |
type T = References.T
|
walther@60114
|
36 |
val empty : T = References.empty
|
walther@60114
|
37 |
val extend = I
|
walther@60114
|
38 |
fun merge (_, refs) = refs
|
walther@60114
|
39 |
);
|
walther@60116
|
40 |
(*/----------------------------- shift to test/../? ----------------------------------------\*)
|
walther@60116
|
41 |
(* Pure/context.ML
|
walther@60116
|
42 |
signature THEORY_DATA =
|
walther@60116
|
43 |
sig
|
walther@60116
|
44 |
type T
|
walther@60116
|
45 |
val get: theory -> T
|
walther@60116
|
46 |
val put: T -> theory -> theory
|
walther@60116
|
47 |
val map: (T -> T) -> theory -> theory
|
walther@60116
|
48 |
end;*)
|
walther@60114
|
49 |
(*
|
walther@60114
|
50 |
Refs_Data.empty; (*in Refs_Data defined workers are hidden*)
|
walther@60114
|
51 |
Refs_Data.extend; (*in Refs_Data defined workers are hidden*)
|
walther@60114
|
52 |
Refs_Data.merge; (*in Refs_Data defined workers are hidden*)
|
walther@60114
|
53 |
ML error\<^here>:
|
walther@60114
|
54 |
Value or constructor (empty) has not been declared in structure Refs *)
|
walther@60114
|
55 |
|
walther@60114
|
56 |
Refs_Data.get: theory -> Refs_Data.T; (*from signature THEORY_DATA*)
|
walther@60114
|
57 |
Refs_Data.put: Refs_Data.T -> theory -> theory; (*from signature THEORY_DATA*)
|
walther@60114
|
58 |
Refs_Data.map: (Refs_Data.T -> Refs_Data.T) -> theory -> theory; (*from signature THEORY_DATA*)
|
walther@60116
|
59 |
(*\----------------------------- shift to test/../? ----------------------------------------/*)
|
walther@60114
|
60 |
\<close> ML \<open>
|
walther@60114
|
61 |
structure OMod_Data = Theory_Data
|
walther@60114
|
62 |
(
|
walther@60114
|
63 |
type T = O_Model.T
|
walther@60114
|
64 |
val empty : T = []
|
walther@60114
|
65 |
val extend = I
|
walther@60114
|
66 |
fun merge (_, o_model) = o_model
|
walther@60114
|
67 |
)
|
walther@60114
|
68 |
\<close> ML \<open>
|
walther@60114
|
69 |
structure Ctxt_Data = Theory_Data
|
walther@60114
|
70 |
(
|
walther@60114
|
71 |
type T = Proof.context
|
walther@60114
|
72 |
val empty : T = ContextC.empty
|
walther@60114
|
73 |
val extend = I
|
walther@60114
|
74 |
fun merge (_, ctxt) = ctxt
|
walther@60114
|
75 |
)
|
walther@60114
|
76 |
\<close> ML \<open>
|
walther@60122
|
77 |
fun store_and_show formalise thy =
|
walther@60101
|
78 |
let
|
walther@60122
|
79 |
(**)val file_read_correct = case formalise of xxx as
|
walther@60110
|
80 |
[(["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"],
|
walther@60114
|
81 |
("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))] => hd xxx
|
walther@60110
|
82 |
| _ => error "magic failed: handling file exp_Statics_Biegel_Timischl_7-70.str failed"
|
walther@60122
|
83 |
(**)
|
walther@60122
|
84 |
val formalise = hd formalise (*we expect only one Formalise.T in the list*)
|
walther@60114
|
85 |
val (hdlPIDE, _, refs, o_model, var_type_ctxt) = Step_Specify.initialisePIDE formalise
|
walther@60126
|
86 |
(* ^^ TODO remove with cleanup in nxt_specify_init_calc *)
|
walther@60126
|
87 |
(*
|
walther@60126
|
88 |
TODO: present "Problem hdlPIDE" via PIDE
|
walther@60126
|
89 |
*)
|
walther@60101
|
90 |
in
|
walther@60116
|
91 |
thy
|
walther@60114
|
92 |
|> Refs_Data.put refs
|
walther@60114
|
93 |
|> OMod_Data.put o_model
|
walther@60114
|
94 |
|> Ctxt_Data.put var_type_ctxt
|
walther@60101
|
95 |
end;
|
walther@60097
|
96 |
\<close> ML \<open>
|
walther@60122
|
97 |
fun load_formalisation parser (files, _) thy =
|
walther@60101
|
98 |
let
|
walther@60122
|
99 |
val ([{lines, pos, ...}: Token.file], thy') = files thy;
|
walther@60101
|
100 |
in
|
walther@60122
|
101 |
store_and_show
|
walther@60122
|
102 |
(ParseC.read_out_formalise (fst (parser (fst (ParseC.scan' pos (cat_lines lines))))))
|
walther@60117
|
103 |
thy'
|
walther@60101
|
104 |
end;
|
walther@60097
|
105 |
\<close> ML \<open>
|
walther@60123
|
106 |
\<close>
|
walther@60123
|
107 |
|
walther@60123
|
108 |
subsection \<open>code to write Problem ("Biegelinie", ["Biegelinien"]) to thy\<close>
|
walther@60123
|
109 |
ML \<open>
|
walther@60107
|
110 |
\<close> ML \<open>
|
walther@60110
|
111 |
\<close> ML \<open>
|
walther@60123
|
112 |
\<close> ML \<open>
|
walther@60123
|
113 |
\<close>
|
walther@60123
|
114 |
|
walther@60123
|
115 |
subsection \<open>code for Problem\<close>
|
walther@60123
|
116 |
text \<open>
|
walther@60123
|
117 |
Again, we copy code from spark_vc into Calculation.thy and
|
walther@60123
|
118 |
add functionality for Problem
|
walther@60123
|
119 |
such that the code keeps running during adaption from spark_vc to Problem.
|
walther@60123
|
120 |
\<close> ML \<open>
|
walther@60123
|
121 |
\<close> ML \<open>
|
walther@60123
|
122 |
\<close>
|
walther@60123
|
123 |
|
walther@60123
|
124 |
subsubsection \<open>copied from fdl_parser.ML\<close>
|
walther@60123
|
125 |
ML \<open>
|
walther@60123
|
126 |
\<close> ML \<open>
|
walther@60123
|
127 |
datatype expr =
|
walther@60123
|
128 |
Ident of string
|
walther@60123
|
129 |
| Number of int
|
walther@60123
|
130 |
| Quantifier of string * string list * string * expr
|
walther@60123
|
131 |
| Funct of string * expr list
|
walther@60123
|
132 |
| Element of expr * expr list
|
walther@60123
|
133 |
| Update of expr * expr list * expr
|
walther@60123
|
134 |
| Record of string * (string * expr) list
|
walther@60123
|
135 |
| Array of string * expr option *
|
walther@60123
|
136 |
((expr * expr option) list list * expr) list;
|
walther@60123
|
137 |
\<close> ML \<open>
|
walther@60123
|
138 |
datatype fdl_type =
|
walther@60123
|
139 |
Basic_Type of string
|
walther@60123
|
140 |
| Enum_Type of string list
|
walther@60123
|
141 |
| Array_Type of string list * string
|
walther@60123
|
142 |
| Record_Type of (string list * string) list
|
walther@60123
|
143 |
| Pending_Type;
|
walther@60123
|
144 |
\<close> ML \<open>
|
walther@60123
|
145 |
(* also store items in a list to preserve order *)
|
walther@60123
|
146 |
type 'a tab = 'a Symtab.table * (string * 'a) list;
|
walther@60123
|
147 |
\<close> ML \<open>
|
walther@60123
|
148 |
fun lookup ((tab, _) : 'a tab) = Symtab.lookup tab;
|
walther@60123
|
149 |
\<close> ML \<open>
|
walther@60123
|
150 |
\<close>
|
walther@60123
|
151 |
subsubsection \<open>copied from spark_vcs.ML\<close>
|
walther@60123
|
152 |
ML \<open>
|
walther@60123
|
153 |
\<close> ML \<open>
|
walther@60129
|
154 |
(**)
|
walther@60123
|
155 |
fun err_unfinished () = error "An unfinished SPARK environment is still open."
|
walther@60123
|
156 |
\<close> ML \<open>
|
walther@60123
|
157 |
val strip_number = apply2 implode o chop_suffix Fdl_Lexer.is_digit o raw_explode;
|
walther@60123
|
158 |
\<close> ML \<open>
|
walther@60123
|
159 |
val name_ord = prod_ord string_ord (option_ord int_ord) o
|
walther@60123
|
160 |
apply2 (strip_number ##> Int.fromString);
|
walther@60123
|
161 |
\<close> ML \<open>
|
walther@60123
|
162 |
structure VCtab = Table(type key = string val ord = name_ord);
|
walther@60123
|
163 |
\<close> ML \<open>
|
walther@60123
|
164 |
val builtin = Symtab.make (map (rpair ())
|
walther@60123
|
165 |
["->", "<->", "or", "and", "not", "=", "<>", "<", ">", "<=", ">=",
|
walther@60123
|
166 |
"+", "-", "*", "/", "div", "mod", "**"]);
|
walther@60123
|
167 |
\<close> ML \<open>
|
walther@60123
|
168 |
val is_pfun =
|
walther@60123
|
169 |
Symtab.defined builtin orf
|
walther@60123
|
170 |
can (unprefix "fld_") orf can (unprefix "upf_") orf
|
walther@60123
|
171 |
can (unsuffix "__pos") orf can (unsuffix "__val") orf
|
walther@60123
|
172 |
equal "succ" orf equal "pred";
|
walther@60123
|
173 |
\<close> ML \<open>
|
walther@60123
|
174 |
fun fold_opt f = the_default I o Option.map f;
|
walther@60123
|
175 |
fun fold_pair f g (x, y) = f x #> g y;
|
walther@60123
|
176 |
\<close> ML \<open>
|
walther@60123
|
177 |
fun fold_expr f g (Funct (s, es)) = f s #> fold (fold_expr f g) es
|
walther@60123
|
178 |
| fold_expr f g (Ident s) = g s
|
walther@60123
|
179 |
| fold_expr f g (Number _) = I
|
walther@60123
|
180 |
| fold_expr f g (Quantifier (_, _, _, e)) = fold_expr f g e
|
walther@60123
|
181 |
| fold_expr f g (Element (e, es)) =
|
walther@60123
|
182 |
fold_expr f g e #> fold (fold_expr f g) es
|
walther@60123
|
183 |
| fold_expr f g (Update (e, es, e')) =
|
walther@60123
|
184 |
fold_expr f g e #> fold (fold_expr f g) es #> fold_expr f g e'
|
walther@60123
|
185 |
| fold_expr f g (Record (_, flds)) = fold (fold_expr f g o snd) flds
|
walther@60123
|
186 |
| fold_expr f g (Array (_, default, assocs)) =
|
walther@60123
|
187 |
fold_opt (fold_expr f g) default #>
|
walther@60123
|
188 |
fold (fold_pair
|
walther@60123
|
189 |
(fold (fold (fold_pair
|
walther@60123
|
190 |
(fold_expr f g) (fold_opt (fold_expr f g)))))
|
walther@60123
|
191 |
(fold_expr f g)) assocs;
|
walther@60123
|
192 |
\<close> ML \<open>
|
walther@60123
|
193 |
fun add_expr_pfuns funs = fold_expr
|
walther@60123
|
194 |
(fn s => if is_pfun s then I else insert (op =) s)
|
walther@60123
|
195 |
(fn s => if is_none (lookup funs s) then I else insert (op =) s);
|
walther@60123
|
196 |
\<close> ML \<open>
|
walther@60123
|
197 |
fun fold_vcs f vcs =
|
walther@60123
|
198 |
VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs;
|
walther@60123
|
199 |
\<close> ML \<open>
|
walther@60123
|
200 |
fun lookup_prfx "" tab s = Symtab.lookup tab s
|
walther@60123
|
201 |
| lookup_prfx prfx tab s = (case Symtab.lookup tab s of
|
walther@60123
|
202 |
NONE => Symtab.lookup tab (prfx ^ "__" ^ s)
|
walther@60123
|
203 |
| x => x);
|
walther@60123
|
204 |
\<close> ML \<open>
|
walther@60123
|
205 |
fun pfuns_of_vcs prfx funs pfuns vcs =
|
walther@60123
|
206 |
fold_vcs (add_expr_pfuns funs o snd) vcs [] |>
|
walther@60123
|
207 |
filter (is_none o lookup_prfx prfx pfuns);
|
walther@60123
|
208 |
\<close> ML \<open>
|
walther@60123
|
209 |
fun pfuns_of_vcs prfx funs pfuns vcs =
|
walther@60123
|
210 |
fold_vcs (add_expr_pfuns funs o snd) vcs [] |>
|
walther@60123
|
211 |
filter (is_none o lookup_prfx prfx pfuns);
|
walther@60123
|
212 |
\<close> ML \<open>
|
walther@60123
|
213 |
structure VCs = Theory_Data
|
walther@60123
|
214 |
(
|
walther@60123
|
215 |
type T =
|
walther@60123
|
216 |
{pfuns: ((string list * string) option * term) Symtab.table,
|
walther@60123
|
217 |
type_map: (typ * (string * string) list) Symtab.table,
|
walther@60123
|
218 |
env:
|
walther@60123
|
219 |
{ctxt: Element.context_i list,
|
walther@60123
|
220 |
defs: (binding * thm) list,
|
walther@60123
|
221 |
types: fdl_type tab,
|
walther@60123
|
222 |
funs: (string list * string) tab,
|
walther@60123
|
223 |
pfuns: ((string list * string) option * term) Symtab.table,
|
walther@60123
|
224 |
ids: (term * string) Symtab.table * Name.context,
|
walther@60123
|
225 |
proving: bool,
|
walther@60123
|
226 |
vcs: (string * thm list option *
|
walther@60123
|
227 |
(string * expr) list * (string * expr) list) VCtab.table,
|
walther@60123
|
228 |
path: Path.T,
|
walther@60123
|
229 |
prefix: string} option}
|
walther@60123
|
230 |
val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE}
|
walther@60123
|
231 |
val extend = I
|
walther@60123
|
232 |
fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE},
|
walther@60123
|
233 |
{pfuns = pfuns2, type_map = type_map2, env = NONE}) =
|
walther@60123
|
234 |
{pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),
|
walther@60123
|
235 |
type_map = Symtab.merge (op =) (type_map1, type_map2),
|
walther@60123
|
236 |
env = NONE}
|
walther@60123
|
237 |
| merge _ = err_unfinished ()
|
walther@60123
|
238 |
)
|
walther@60123
|
239 |
\<close> ML \<open>
|
walther@60123
|
240 |
fun get_type thy prfx ty =
|
walther@60123
|
241 |
let val {type_map, ...} = VCs.get thy
|
walther@60123
|
242 |
in lookup_prfx prfx type_map ty end;
|
walther@60123
|
243 |
\<close> ML \<open>
|
walther@60123
|
244 |
fun mk_type' _ _ "integer" = (HOLogic.intT, [])
|
walther@60123
|
245 |
| mk_type' _ _ "boolean" = (HOLogic.boolT, [])
|
walther@60123
|
246 |
| mk_type' thy prfx ty =
|
walther@60123
|
247 |
(case get_type thy prfx ty of
|
walther@60123
|
248 |
NONE =>
|
walther@60123
|
249 |
(Syntax.check_typ (Proof_Context.init_global thy)
|
walther@60123
|
250 |
(Type (Sign.full_name thy (Binding.name ty), [])),
|
walther@60123
|
251 |
[])
|
walther@60123
|
252 |
| SOME p => p);
|
walther@60123
|
253 |
\<close> ML \<open>
|
walther@60123
|
254 |
fun mk_type thy prfx ty = fst (mk_type' thy prfx ty);
|
walther@60123
|
255 |
\<close> ML \<open>
|
walther@60123
|
256 |
fun pfun_type thy prfx (argtys, resty) =
|
walther@60123
|
257 |
map (mk_type thy prfx) argtys ---> mk_type thy prfx resty;
|
walther@60123
|
258 |
\<close> ML \<open>
|
walther@60123
|
259 |
fun declare_missing_pfuns thy prfx funs pfuns vcs (tab, ctxt) =
|
walther@60123
|
260 |
let
|
walther@60123
|
261 |
val (fs, (tys, Ts)) =
|
walther@60123
|
262 |
pfuns_of_vcs prfx funs pfuns vcs |>
|
walther@60123
|
263 |
map_filter (fn s => lookup funs s |>
|
walther@60123
|
264 |
Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |>
|
walther@60123
|
265 |
split_list ||> split_list;
|
walther@60123
|
266 |
val (fs', ctxt') = fold_map Name.variant fs ctxt
|
walther@60123
|
267 |
in
|
walther@60123
|
268 |
(fold Symtab.update_new (fs ~~ (tys ~~ map Free (fs' ~~ Ts))) pfuns,
|
walther@60123
|
269 |
Element.Fixes (map2 (fn s => fn T =>
|
walther@60123
|
270 |
(Binding.name s, SOME T, NoSyn)) fs' Ts),
|
walther@60123
|
271 |
(tab, ctxt'))
|
walther@60123
|
272 |
end;
|
walther@60123
|
273 |
\<close> ML \<open>
|
walther@60123
|
274 |
fun strip_underscores s =
|
walther@60123
|
275 |
strip_underscores (unsuffix "_" s) handle Fail _ => s;
|
walther@60123
|
276 |
|
walther@60123
|
277 |
fun strip_tilde s =
|
walther@60123
|
278 |
unsuffix "~" s ^ "_init" handle Fail _ => s;
|
walther@60123
|
279 |
\<close> ML \<open>
|
walther@60123
|
280 |
val mangle_name = strip_underscores #> strip_tilde;
|
walther@60123
|
281 |
\<close> ML \<open>
|
walther@60123
|
282 |
fun mk_variables thy prfx xs ty (tab, ctxt) =
|
walther@60123
|
283 |
let
|
walther@60123
|
284 |
val T = mk_type thy prfx ty;
|
walther@60123
|
285 |
val (ys, ctxt') = fold_map Name.variant (map mangle_name xs) ctxt;
|
walther@60123
|
286 |
val zs = map (Free o rpair T) ys;
|
walther@60123
|
287 |
in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
|
walther@60123
|
288 |
\<close> ML \<open>
|
walther@60123
|
289 |
fun mk_unop s t =
|
walther@60123
|
290 |
let val T = fastype_of t
|
walther@60123
|
291 |
in Const (s, T --> T) $ t end;
|
walther@60123
|
292 |
\<close> ML \<open>
|
walther@60123
|
293 |
val booleanN = "boolean";
|
walther@60123
|
294 |
val integerN = "integer";
|
walther@60123
|
295 |
\<close> ML \<open>
|
walther@60123
|
296 |
val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode;
|
walther@60123
|
297 |
val lcase_eq = (op =) o apply2 (to_lower o Long_Name.base_name);
|
walther@60123
|
298 |
\<close> ML \<open>
|
walther@60123
|
299 |
fun find_field [] fname fields =
|
walther@60123
|
300 |
find_first (curry lcase_eq fname o fst) fields
|
walther@60123
|
301 |
| find_field cmap fname fields =
|
walther@60123
|
302 |
(case AList.lookup (op =) cmap fname of
|
walther@60123
|
303 |
NONE => NONE
|
walther@60123
|
304 |
| SOME fname' => SOME (fname', the (AList.lookup (op =) fields fname')));
|
walther@60123
|
305 |
\<close> ML \<open>
|
walther@60123
|
306 |
fun get_record_info thy T = (case Record.dest_recTs T of
|
walther@60123
|
307 |
[(tyname, [\<^typ>\<open>unit\<close>])] =>
|
walther@60123
|
308 |
Record.get_info thy (Long_Name.qualifier tyname)
|
walther@60123
|
309 |
| _ => NONE);
|
walther@60123
|
310 |
\<close> ML \<open>
|
walther@60123
|
311 |
fun find_field' fname = get_first (fn (flds, fldty) =>
|
walther@60123
|
312 |
if member (op =) flds fname then SOME fldty else NONE);
|
walther@60123
|
313 |
\<close> ML \<open>
|
walther@60123
|
314 |
fun invert_map [] = I
|
walther@60123
|
315 |
| invert_map cmap =
|
walther@60123
|
316 |
map (apfst (the o AList.lookup (op =) (map swap cmap)));
|
walther@60123
|
317 |
\<close> ML \<open>
|
walther@60123
|
318 |
fun mk_times (t, u) =
|
walther@60123
|
319 |
let
|
walther@60123
|
320 |
val setT = fastype_of t;
|
walther@60123
|
321 |
val T = HOLogic.dest_setT setT;
|
walther@60123
|
322 |
val U = HOLogic.dest_setT (fastype_of u)
|
walther@60123
|
323 |
in
|
walther@60123
|
324 |
Const (\<^const_name>\<open>Sigma\<close>, setT --> (T --> HOLogic.mk_setT U) -->
|
walther@60123
|
325 |
HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)
|
walther@60123
|
326 |
end;
|
walther@60123
|
327 |
\<close> ML \<open>
|
walther@60123
|
328 |
fun term_of_expr thy prfx types pfuns =
|
walther@60123
|
329 |
let
|
walther@60123
|
330 |
fun tm_of vs (Funct ("->", [e, e'])) =
|
walther@60123
|
331 |
(HOLogic.mk_imp (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
|
walther@60123
|
332 |
|
walther@60123
|
333 |
| tm_of vs (Funct ("<->", [e, e'])) =
|
walther@60123
|
334 |
(HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
|
walther@60123
|
335 |
|
walther@60123
|
336 |
| tm_of vs (Funct ("or", [e, e'])) =
|
walther@60123
|
337 |
(HOLogic.mk_disj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
|
walther@60123
|
338 |
|
walther@60123
|
339 |
| tm_of vs (Funct ("and", [e, e'])) =
|
walther@60123
|
340 |
(HOLogic.mk_conj (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
|
walther@60123
|
341 |
|
walther@60123
|
342 |
| tm_of vs (Funct ("not", [e])) =
|
walther@60123
|
343 |
(HOLogic.mk_not (fst (tm_of vs e)), booleanN)
|
walther@60123
|
344 |
|
walther@60123
|
345 |
| tm_of vs (Funct ("=", [e, e'])) =
|
walther@60123
|
346 |
(HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
|
walther@60123
|
347 |
|
walther@60123
|
348 |
| tm_of vs (Funct ("<>", [e, e'])) = (HOLogic.mk_not
|
walther@60123
|
349 |
(HOLogic.mk_eq (fst (tm_of vs e), fst (tm_of vs e'))), booleanN)
|
walther@60123
|
350 |
|
walther@60123
|
351 |
| tm_of vs (Funct ("<", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
|
walther@60123
|
352 |
(fst (tm_of vs e), fst (tm_of vs e')), booleanN)
|
walther@60123
|
353 |
|
walther@60123
|
354 |
| tm_of vs (Funct (">", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less\<close>
|
walther@60123
|
355 |
(fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
|
walther@60123
|
356 |
|
walther@60123
|
357 |
| tm_of vs (Funct ("<=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
|
walther@60123
|
358 |
(fst (tm_of vs e), fst (tm_of vs e')), booleanN)
|
walther@60123
|
359 |
|
walther@60123
|
360 |
| tm_of vs (Funct (">=", [e, e'])) = (HOLogic.mk_binrel \<^const_name>\<open>less_eq\<close>
|
walther@60123
|
361 |
(fst (tm_of vs e'), fst (tm_of vs e)), booleanN)
|
walther@60123
|
362 |
|
walther@60123
|
363 |
| tm_of vs (Funct ("+", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>plus\<close>
|
walther@60123
|
364 |
(fst (tm_of vs e), fst (tm_of vs e')), integerN)
|
walther@60123
|
365 |
|
walther@60123
|
366 |
| tm_of vs (Funct ("-", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>minus\<close>
|
walther@60123
|
367 |
(fst (tm_of vs e), fst (tm_of vs e')), integerN)
|
walther@60123
|
368 |
|
walther@60123
|
369 |
| tm_of vs (Funct ("*", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>times\<close>
|
walther@60123
|
370 |
(fst (tm_of vs e), fst (tm_of vs e')), integerN)
|
walther@60123
|
371 |
|
walther@60123
|
372 |
| tm_of vs (Funct ("/", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>divide\<close>
|
walther@60123
|
373 |
(fst (tm_of vs e), fst (tm_of vs e')), integerN)
|
walther@60123
|
374 |
|
walther@60123
|
375 |
| tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>sdiv\<close>
|
walther@60123
|
376 |
(fst (tm_of vs e), fst (tm_of vs e')), integerN)
|
walther@60123
|
377 |
|
walther@60123
|
378 |
| tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>modulo\<close>
|
walther@60123
|
379 |
(fst (tm_of vs e), fst (tm_of vs e')), integerN)
|
walther@60123
|
380 |
|
walther@60123
|
381 |
| tm_of vs (Funct ("-", [e])) =
|
walther@60123
|
382 |
(mk_unop \<^const_name>\<open>uminus\<close> (fst (tm_of vs e)), integerN)
|
walther@60123
|
383 |
|
walther@60123
|
384 |
| tm_of vs (Funct ("**", [e, e'])) =
|
walther@60123
|
385 |
(Const (\<^const_name>\<open>power\<close>, HOLogic.intT --> HOLogic.natT -->
|
walther@60123
|
386 |
HOLogic.intT) $ fst (tm_of vs e) $
|
walther@60123
|
387 |
(\<^const>\<open>nat\<close> $ fst (tm_of vs e')), integerN)
|
walther@60123
|
388 |
|
walther@60123
|
389 |
| tm_of (tab, _) (Ident s) =
|
walther@60123
|
390 |
(case Symtab.lookup tab s of
|
walther@60123
|
391 |
SOME t_ty => t_ty
|
walther@60123
|
392 |
| NONE => (case lookup_prfx prfx pfuns s of
|
walther@60123
|
393 |
SOME (SOME ([], resty), t) => (t, resty)
|
walther@60123
|
394 |
| _ => error ("Undeclared identifier " ^ s)))
|
walther@60123
|
395 |
|
walther@60123
|
396 |
| tm_of _ (Number i) = (HOLogic.mk_number HOLogic.intT i, integerN)
|
walther@60123
|
397 |
|
walther@60123
|
398 |
| tm_of vs (Quantifier (s, xs, ty, e)) =
|
walther@60123
|
399 |
let
|
walther@60123
|
400 |
val (ys, vs') = mk_variables thy prfx xs ty vs;
|
walther@60123
|
401 |
val q = (case s of
|
walther@60123
|
402 |
"for_all" => HOLogic.mk_all
|
walther@60123
|
403 |
| "for_some" => HOLogic.mk_exists)
|
walther@60123
|
404 |
in
|
walther@60123
|
405 |
(fold_rev (fn Free (x, T) => fn t => q (x, T, t))
|
walther@60123
|
406 |
ys (fst (tm_of vs' e)),
|
walther@60123
|
407 |
booleanN)
|
walther@60123
|
408 |
end
|
walther@60123
|
409 |
|
walther@60123
|
410 |
| tm_of vs (Funct (s, es)) =
|
walther@60123
|
411 |
|
walther@60123
|
412 |
(* record field selection *)
|
walther@60123
|
413 |
(case try (unprefix "fld_") s of
|
walther@60123
|
414 |
SOME fname => (case es of
|
walther@60123
|
415 |
[e] =>
|
walther@60123
|
416 |
let
|
walther@60123
|
417 |
val (t, rcdty) = tm_of vs e;
|
walther@60123
|
418 |
val (rT, cmap) = mk_type' thy prfx rcdty
|
walther@60123
|
419 |
in case (get_record_info thy rT, lookup types rcdty) of
|
walther@60123
|
420 |
(SOME {fields, ...}, SOME (Record_Type fldtys)) =>
|
walther@60123
|
421 |
(case (find_field cmap fname fields,
|
walther@60123
|
422 |
find_field' fname fldtys) of
|
walther@60123
|
423 |
(SOME (fname', fT), SOME fldty) =>
|
walther@60123
|
424 |
(Const (fname', rT --> fT) $ t, fldty)
|
walther@60123
|
425 |
| _ => error ("Record " ^ rcdty ^
|
walther@60123
|
426 |
" has no field named " ^ fname))
|
walther@60123
|
427 |
| _ => error (rcdty ^ " is not a record type")
|
walther@60123
|
428 |
end
|
walther@60123
|
429 |
| _ => error ("Function " ^ s ^ " expects one argument"))
|
walther@60123
|
430 |
| NONE =>
|
walther@60123
|
431 |
|
walther@60123
|
432 |
(* record field update *)
|
walther@60123
|
433 |
(case try (unprefix "upf_") s of
|
walther@60123
|
434 |
SOME fname => (case es of
|
walther@60123
|
435 |
[e, e'] =>
|
walther@60123
|
436 |
let
|
walther@60123
|
437 |
val (t, rcdty) = tm_of vs e;
|
walther@60123
|
438 |
val (rT, cmap) = mk_type' thy prfx rcdty;
|
walther@60123
|
439 |
val (u, fldty) = tm_of vs e';
|
walther@60123
|
440 |
val fT = mk_type thy prfx fldty
|
walther@60123
|
441 |
in case get_record_info thy rT of
|
walther@60123
|
442 |
SOME {fields, ...} =>
|
walther@60123
|
443 |
(case find_field cmap fname fields of
|
walther@60123
|
444 |
SOME (fname', fU) =>
|
walther@60123
|
445 |
if fT = fU then
|
walther@60123
|
446 |
(Const (fname' ^ "_update",
|
walther@60123
|
447 |
(fT --> fT) --> rT --> rT) $
|
walther@60123
|
448 |
Abs ("x", fT, u) $ t,
|
walther@60123
|
449 |
rcdty)
|
walther@60123
|
450 |
else error ("Type\n" ^
|
walther@60123
|
451 |
Syntax.string_of_typ_global thy fT ^
|
walther@60123
|
452 |
"\ndoes not match type\n" ^
|
walther@60123
|
453 |
Syntax.string_of_typ_global thy fU ^
|
walther@60123
|
454 |
"\nof field " ^ fname)
|
walther@60123
|
455 |
| NONE => error ("Record " ^ rcdty ^
|
walther@60123
|
456 |
" has no field named " ^ fname))
|
walther@60123
|
457 |
| _ => error (rcdty ^ " is not a record type")
|
walther@60123
|
458 |
end
|
walther@60123
|
459 |
| _ => error ("Function " ^ s ^ " expects two arguments"))
|
walther@60123
|
460 |
| NONE =>
|
walther@60123
|
461 |
|
walther@60123
|
462 |
(* enumeration type to integer *)
|
walther@60123
|
463 |
(case try (unsuffix "__pos") s of
|
walther@60123
|
464 |
SOME tyname => (case es of
|
walther@60123
|
465 |
[e] => (Const (\<^const_name>\<open>pos\<close>,
|
walther@60123
|
466 |
mk_type thy prfx tyname --> HOLogic.intT) $ fst (tm_of vs e),
|
walther@60123
|
467 |
integerN)
|
walther@60123
|
468 |
| _ => error ("Function " ^ s ^ " expects one argument"))
|
walther@60123
|
469 |
| NONE =>
|
walther@60123
|
470 |
|
walther@60123
|
471 |
(* integer to enumeration type *)
|
walther@60123
|
472 |
(case try (unsuffix "__val") s of
|
walther@60123
|
473 |
SOME tyname => (case es of
|
walther@60123
|
474 |
[e] => (Const (\<^const_name>\<open>val\<close>,
|
walther@60123
|
475 |
HOLogic.intT --> mk_type thy prfx tyname) $ fst (tm_of vs e),
|
walther@60123
|
476 |
tyname)
|
walther@60123
|
477 |
| _ => error ("Function " ^ s ^ " expects one argument"))
|
walther@60123
|
478 |
| NONE =>
|
walther@60123
|
479 |
|
walther@60123
|
480 |
(* successor / predecessor of enumeration type element *)
|
walther@60123
|
481 |
if s = "succ" orelse s = "pred" then (case es of
|
walther@60123
|
482 |
[e] =>
|
walther@60123
|
483 |
let
|
walther@60123
|
484 |
val (t, tyname) = tm_of vs e;
|
walther@60123
|
485 |
val T = mk_type thy prfx tyname
|
walther@60123
|
486 |
in (Const
|
walther@60123
|
487 |
(if s = "succ" then \<^const_name>\<open>succ\<close>
|
walther@60123
|
488 |
else \<^const_name>\<open>pred\<close>, T --> T) $ t, tyname)
|
walther@60123
|
489 |
end
|
walther@60123
|
490 |
| _ => error ("Function " ^ s ^ " expects one argument"))
|
walther@60123
|
491 |
|
walther@60123
|
492 |
(* user-defined proof function *)
|
walther@60123
|
493 |
else
|
walther@60123
|
494 |
(case lookup_prfx prfx pfuns s of
|
walther@60123
|
495 |
SOME (SOME (_, resty), t) =>
|
walther@60123
|
496 |
(list_comb (t, map (fst o tm_of vs) es), resty)
|
walther@60123
|
497 |
| _ => error ("Undeclared proof function " ^ s))))))
|
walther@60123
|
498 |
|
walther@60123
|
499 |
| tm_of vs (Element (e, es)) =
|
walther@60123
|
500 |
let val (t, ty) = tm_of vs e
|
walther@60123
|
501 |
in case lookup types ty of
|
walther@60123
|
502 |
SOME (Array_Type (_, elty)) =>
|
walther@60123
|
503 |
(t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es), elty)
|
walther@60123
|
504 |
| _ => error (ty ^ " is not an array type")
|
walther@60123
|
505 |
end
|
walther@60123
|
506 |
|
walther@60123
|
507 |
| tm_of vs (Update (e, es, e')) =
|
walther@60123
|
508 |
let val (t, ty) = tm_of vs e
|
walther@60123
|
509 |
in case lookup types ty of
|
walther@60123
|
510 |
SOME (Array_Type (idxtys, elty)) =>
|
walther@60123
|
511 |
let
|
walther@60123
|
512 |
val T = foldr1 HOLogic.mk_prodT
|
walther@60123
|
513 |
(map (mk_type thy prfx) idxtys);
|
walther@60123
|
514 |
val U = mk_type thy prfx elty;
|
walther@60123
|
515 |
val fT = T --> U
|
walther@60123
|
516 |
in
|
walther@60123
|
517 |
(Const (\<^const_name>\<open>fun_upd\<close>, fT --> T --> U --> fT) $
|
walther@60123
|
518 |
t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $
|
walther@60123
|
519 |
fst (tm_of vs e'),
|
walther@60123
|
520 |
ty)
|
walther@60123
|
521 |
end
|
walther@60123
|
522 |
| _ => error (ty ^ " is not an array type")
|
walther@60123
|
523 |
end
|
walther@60123
|
524 |
|
walther@60123
|
525 |
| tm_of vs (Record (s, flds)) =
|
walther@60123
|
526 |
let
|
walther@60123
|
527 |
val (T, cmap) = mk_type' thy prfx s;
|
walther@60123
|
528 |
val {extension = (ext_name, _), fields, ...} =
|
walther@60123
|
529 |
(case get_record_info thy T of
|
walther@60123
|
530 |
NONE => error (s ^ " is not a record type")
|
walther@60123
|
531 |
| SOME info => info);
|
walther@60123
|
532 |
val flds' = map (apsnd (tm_of vs)) flds;
|
walther@60123
|
533 |
val fnames = fields |> invert_map cmap |>
|
walther@60123
|
534 |
map (Long_Name.base_name o fst);
|
walther@60123
|
535 |
val fnames' = map fst flds;
|
walther@60123
|
536 |
val (fvals, ftys) = split_list (map (fn s' =>
|
walther@60123
|
537 |
case AList.lookup lcase_eq flds' s' of
|
walther@60123
|
538 |
SOME fval_ty => fval_ty
|
walther@60123
|
539 |
| NONE => error ("Field " ^ s' ^ " missing in record " ^ s))
|
walther@60123
|
540 |
fnames);
|
walther@60123
|
541 |
val _ = (case subtract lcase_eq fnames fnames' of
|
walther@60123
|
542 |
[] => ()
|
walther@60123
|
543 |
| xs => error ("Extra field(s) " ^ commas xs ^
|
walther@60123
|
544 |
" in record " ^ s));
|
walther@60123
|
545 |
val _ = (case duplicates (op =) fnames' of
|
walther@60123
|
546 |
[] => ()
|
walther@60123
|
547 |
| xs => error ("Duplicate field(s) " ^ commas xs ^
|
walther@60123
|
548 |
" in record " ^ s))
|
walther@60123
|
549 |
in
|
walther@60123
|
550 |
(list_comb
|
walther@60123
|
551 |
(Const (ext_name,
|
walther@60123
|
552 |
map (mk_type thy prfx) ftys @ [HOLogic.unitT] ---> T),
|
walther@60123
|
553 |
fvals @ [HOLogic.unit]),
|
walther@60123
|
554 |
s)
|
walther@60123
|
555 |
end
|
walther@60123
|
556 |
|
walther@60123
|
557 |
| tm_of vs (Array (s, default, assocs)) =
|
walther@60123
|
558 |
(case lookup types s of
|
walther@60123
|
559 |
SOME (Array_Type (idxtys, elty)) =>
|
walther@60123
|
560 |
let
|
walther@60123
|
561 |
val Ts = map (mk_type thy prfx) idxtys;
|
walther@60123
|
562 |
val T = foldr1 HOLogic.mk_prodT Ts;
|
walther@60123
|
563 |
val U = mk_type thy prfx elty;
|
walther@60123
|
564 |
fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)]
|
walther@60123
|
565 |
| mk_idx' T (e, SOME e') = Const (\<^const_name>\<open>atLeastAtMost\<close>,
|
walther@60123
|
566 |
T --> T --> HOLogic.mk_setT T) $
|
walther@60123
|
567 |
fst (tm_of vs e) $ fst (tm_of vs e');
|
walther@60123
|
568 |
fun mk_idx idx =
|
walther@60123
|
569 |
if length Ts <> length idx then
|
walther@60123
|
570 |
error ("Arity mismatch in construction of array " ^ s)
|
walther@60123
|
571 |
else foldr1 mk_times (map2 mk_idx' Ts idx);
|
walther@60123
|
572 |
fun mk_upd (idxs, e) t =
|
walther@60123
|
573 |
if length idxs = 1 andalso forall (is_none o snd) (hd idxs)
|
walther@60123
|
574 |
then
|
walther@60123
|
575 |
Const (\<^const_name>\<open>fun_upd\<close>, (T --> U) -->
|
walther@60123
|
576 |
T --> U --> T --> U) $ t $
|
walther@60123
|
577 |
foldl1 HOLogic.mk_prod
|
walther@60123
|
578 |
(map (fst o tm_of vs o fst) (hd idxs)) $
|
walther@60123
|
579 |
fst (tm_of vs e)
|
walther@60123
|
580 |
else
|
walther@60123
|
581 |
Const (\<^const_name>\<open>fun_upds\<close>, (T --> U) -->
|
walther@60123
|
582 |
HOLogic.mk_setT T --> U --> T --> U) $ t $
|
walther@60123
|
583 |
foldl1 (HOLogic.mk_binop \<^const_name>\<open>sup\<close>)
|
walther@60123
|
584 |
(map mk_idx idxs) $
|
walther@60123
|
585 |
fst (tm_of vs e)
|
walther@60123
|
586 |
in
|
walther@60123
|
587 |
(fold mk_upd assocs
|
walther@60123
|
588 |
(case default of
|
walther@60123
|
589 |
SOME e => Abs ("x", T, fst (tm_of vs e))
|
walther@60123
|
590 |
| NONE => Const (\<^const_name>\<open>undefined\<close>, T --> U)),
|
walther@60123
|
591 |
s)
|
walther@60123
|
592 |
end
|
walther@60123
|
593 |
| _ => error (s ^ " is not an array type"))
|
walther@60123
|
594 |
|
walther@60123
|
595 |
in tm_of end;
|
walther@60123
|
596 |
\<close> ML \<open>
|
walther@60123
|
597 |
fun mk_pat s = (case Int.fromString s of
|
walther@60123
|
598 |
SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))]
|
walther@60123
|
599 |
| NONE => error ("Bad conclusion identifier: C" ^ s));
|
walther@60123
|
600 |
\<close> ML \<open>
|
walther@60123
|
601 |
fun mk_vc thy prfx types pfuns ids name_concl (tr, proved, ps, cs) =
|
walther@60123
|
602 |
let val prop_of =
|
walther@60123
|
603 |
HOLogic.mk_Trueprop o fst o term_of_expr thy prfx types pfuns ids
|
walther@60123
|
604 |
in
|
walther@60123
|
605 |
(tr, proved,
|
walther@60123
|
606 |
Element.Assumes (map (fn (s', e) =>
|
walther@60123
|
607 |
((Binding.name ("H" ^ s'), []), [(prop_of e, [])])) ps),
|
walther@60123
|
608 |
Element.Shows (map (fn (s', e) =>
|
walther@60123
|
609 |
(if name_concl then (Binding.name ("C" ^ s'), [])
|
walther@60123
|
610 |
else Binding.empty_atts,
|
walther@60123
|
611 |
[(prop_of e, mk_pat s')])) cs))
|
walther@60123
|
612 |
end;
|
walther@60123
|
613 |
\<close> ML \<open>
|
walther@60123
|
614 |
(*val lookup_vc: theory -> bool -> string -> (Element.context_i list *
|
walther@60123
|
615 |
(string * thm list option * Element.context_i * Element.statement_i)) option
|
walther@60123
|
616 |
*)
|
walther@60123
|
617 |
fun lookup_vc thy name_concl name =
|
walther@60123
|
618 |
(case VCs.get thy of
|
walther@60123
|
619 |
{env = SOME {vcs, types, funs, pfuns, ids, ctxt, prefix, ...}, ...} =>
|
walther@60123
|
620 |
(case VCtab.lookup vcs name of
|
walther@60123
|
621 |
SOME vc =>
|
walther@60123
|
622 |
let val (pfuns', ctxt', ids') =
|
walther@60123
|
623 |
declare_missing_pfuns thy prefix funs pfuns vcs ids
|
walther@60123
|
624 |
in
|
walther@60123
|
625 |
SOME (ctxt @ [ctxt'],
|
walther@60123
|
626 |
mk_vc thy prefix types pfuns' ids' name_concl vc)
|
walther@60123
|
627 |
end
|
walther@60123
|
628 |
| NONE => NONE)
|
walther@60123
|
629 |
| _ => NONE);
|
walther@60123
|
630 |
\<close> ML \<open>
|
walther@60123
|
631 |
\<close>
|
walther@60123
|
632 |
subsubsection \<open>copied from spark_commands.ML\<close>
|
walther@60123
|
633 |
ML \<open>
|
walther@60123
|
634 |
\<close> ML \<open>
|
walther@60123
|
635 |
fun get_vc thy vc_name =
|
walther@60123
|
636 |
(case SPARK_VCs.lookup_vc thy false vc_name of
|
walther@60123
|
637 |
SOME (ctxt, (_, proved, ctxt', stmt)) =>
|
walther@60123
|
638 |
if is_some proved then
|
walther@60123
|
639 |
error ("The verification condition " ^
|
walther@60123
|
640 |
quote vc_name ^ " has already been proved.")
|
walther@60123
|
641 |
else (ctxt @ [ctxt'], stmt)
|
walther@60123
|
642 |
| NONE => error ("There is no verification condition " ^
|
walther@60123
|
643 |
quote vc_name ^ "."));
|
walther@60123
|
644 |
\<close> ML \<open>
|
walther@60127
|
645 |
(*
|
walther@60127
|
646 |
val prefer_input: ThyC.id * Problem.id -> References.T -> O_Model.T -> References.T * O_Model.T
|
walther@60127
|
647 |
*)
|
walther@60127
|
648 |
fun prefer_input (inthy, inpbl : Problem.id) (thy, pbl, met_id) o_model =
|
walther@60124
|
649 |
if inthy = thy andalso inpbl = pbl
|
walther@60124
|
650 |
then ((thy, pbl, met_id) : References.T, o_model)
|
walther@60124
|
651 |
else ((inthy, inpbl, Method.id_empty), [])
|
walther@60124
|
652 |
\<close> ML \<open>
|
walther@60127
|
653 |
(*
|
walther@60128
|
654 |
val prove_vc: ParseC.headline_string -> Proof.context -> Proof.state
|
walther@60127
|
655 |
*)
|
walther@60128
|
656 |
fun prove_vc (*vc_name*)headline lthy =
|
walther@60123
|
657 |
let
|
walther@60128
|
658 |
val _ = @{print} {a = "//--- Spark_Commands.prove_vc", headline = headline}
|
walther@60123
|
659 |
val thy = Proof_Context.theory_of lthy;
|
walther@60128
|
660 |
val vc_name = "procedure_g_c_d_4" (*fixed for spark_open \<open>greatest_common_divisor/g_c_d\<close>*)
|
walther@60123
|
661 |
val (ctxt, stmt) = get_vc thy vc_name
|
walther@60124
|
662 |
(*//--------------------------------- new code --------------------------------\\*)
|
walther@60128
|
663 |
val refs'' = ParseC.read_out_headline headline
|
walther@60127
|
664 |
val refs' = Refs_Data.get thy
|
walther@60127
|
665 |
val (refs as (_, pbl_id, _), o_model) = prefer_input refs'' refs' (OMod_Data.get thy)
|
walther@60126
|
666 |
val i_model = I_Model.initPIDE pbl_id
|
walther@60126
|
667 |
(*
|
walther@60126
|
668 |
TODO: present Specification = i_model () + refs via PIDE
|
walther@60126
|
669 |
*)
|
walther@60124
|
670 |
(*----------------------------------- new code ----------------------------------*)
|
walther@60126
|
671 |
val _ = @{print} {a = "prove_vc", o_model = o_model, refs = refs, i_model = i_model}
|
walther@60124
|
672 |
(*\\--------------------------------- new code --------------------------------//*)
|
walther@60123
|
673 |
in
|
walther@60123
|
674 |
Specification.theorem true Thm.theoremK NONE
|
walther@60123
|
675 |
(fn thmss => (Local_Theory.background_theory
|
walther@60123
|
676 |
(SPARK_VCs.mark_proved vc_name (flat thmss))))
|
walther@60123
|
677 |
(Binding.name vc_name, []) [] ctxt stmt false lthy
|
walther@60123
|
678 |
end;
|
walther@60123
|
679 |
\<close> ML \<open>
|
walther@60097
|
680 |
\<close>
|
walther@60097
|
681 |
|
walther@60103
|
682 |
section \<open>setup command_keyword \<close>
|
walther@60103
|
683 |
ML \<open>
|
walther@60103
|
684 |
\<close> ML \<open>
|
walther@60103
|
685 |
val _ =
|
walther@60117
|
686 |
Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file"
|
walther@60117
|
687 |
(Resources.provide_parse_files "Example" -- Parse.parname
|
walther@60122
|
688 |
>> (Toplevel.theory o (load_formalisation ParseC.formalisation)));
|
walther@60110
|
689 |
\<close> ML \<open>
|
walther@60123
|
690 |
val _ =
|
walther@60123
|
691 |
Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>Problem\<close>
|
walther@60123
|
692 |
"start a Specification, either from scratch or from preceding 'Example'"
|
walther@60128
|
693 |
(ParseC.problem_headline >> prove_vc);
|
walther@60123
|
694 |
\<close> ML \<open>
|
walther@60128
|
695 |
prove_vc\<close>
|
walther@60103
|
696 |
|
walther@60116
|
697 |
subsection \<open>test runs with Example\<close>
|
walther@60129
|
698 |
subsubsection \<open>with new code\<close>
|
walther@60116
|
699 |
text \<open>
|
walther@60118
|
700 |
Starting the Calculation for the Example requires session Isac with Isac.Biegelinie etc.
|
walther@60118
|
701 |
So, do ~~$ ./zcoding-to-test.sh and use Test_Some.thy to evaluate
|
walther@60107
|
702 |
|
walther@60116
|
703 |
Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>
|
walther@60107
|
704 |
|
walther@60118
|
705 |
This now gives no error, but also no <Output>. See child of 3ea616c84845.
|
walther@60102
|
706 |
\<close>
|
walther@60129
|
707 |
|
walther@60129
|
708 |
subsubsection \<open>with original SPARK code\<close>
|
walther@60129
|
709 |
text \<open>
|
walther@60129
|
710 |
The sequence of code below is copied from SPARK/Examples/Gcd/Greatest_Common_Divisor.thy.
|
walther@60129
|
711 |
But here the code works only partially (see ERROR at end).
|
walther@60129
|
712 |
Thus it is advisable to run tests in Greatest_Common_Divisor.thy.
|
walther@60129
|
713 |
|
walther@60129
|
714 |
spark_proof_functions is required for proof below..
|
walther@60129
|
715 |
\<close>
|
walther@60129
|
716 |
(*//------------------- outcomment before creating session Isac ----------------------------\\* )
|
walther@60129
|
717 |
(**)
|
walther@60129
|
718 |
spark_proof_functions gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
|
walther@60127
|
719 |
(**)
|
walther@60127
|
720 |
spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>
|
walther@60127
|
721 |
(*Output..* )
|
walther@60127
|
722 |
The following verification conditions remain to be proved:
|
walther@60127
|
723 |
procedure_g_c_d_4
|
walther@60127
|
724 |
procedure_g_c_d_11
|
walther@60127
|
725 |
( **)
|
walther@60127
|
726 |
spark_vc procedure_g_c_d_4
|
walther@60127
|
727 |
proof -
|
walther@60127
|
728 |
from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)
|
walther@60127
|
729 |
with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1
|
walther@60127
|
730 |
by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])
|
walther@60127
|
731 |
(** )
|
walther@60127
|
732 |
proof -
|
walther@60127
|
733 |
from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)
|
walther@60127
|
734 |
with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1
|
walther@60127
|
735 |
by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])
|
walther@60127
|
736 |
next
|
walther@60127
|
737 |
from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C2
|
walther@60127
|
738 |
by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)
|
walther@60127
|
739 |
qed
|
walther@60127
|
740 |
( **)oops(**)
|
walther@60127
|
741 |
(** )sorry( **)
|
walther@60127
|
742 |
|
walther@60127
|
743 |
spark_vc procedure_g_c_d_11
|
walther@60127
|
744 |
sorry
|
walther@60127
|
745 |
(** )
|
walther@60127
|
746 |
spark_end
|
walther@60127
|
747 |
( *Bad path binding: "$ISABELLE_HOME/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.prv"*)
|
walther@60127
|
748 |
|
walther@60129
|
749 |
( *\\------------------- outcomment before creating session Isac ----------------------------//*)
|
walther@60129
|
750 |
|
walther@60104
|
751 |
|
walther@60123
|
752 |
section \<open>adapt spark_vc to Problem\<close>
|
walther@60123
|
753 |
|
walther@60123
|
754 |
subsection \<open>survey on steps of investigation\<close>
|
walther@60119
|
755 |
text \<open>
|
walther@60123
|
756 |
1.prove_vc: string -> Proof.context -> Proof.state
|
walther@60123
|
757 |
? where does ^^^^^^^^^^^^^ come from:
|
walther@60123
|
758 |
fun get_vc: (case SPARK_VCs.lookup_vc .. of SOME (ctxt, (_, proved, ctxt', stmt)) => ...
|
walther@60123
|
759 |
|
walther@60119
|
760 |
\<close>
|
walther@60119
|
761 |
|
walther@60123
|
762 |
subsection \<open>notes and testbed for spark_vcs\<close>
|
walther@60119
|
763 |
ML \<open>
|
walther@60127
|
764 |
\<close> ML \<open> (* Outer_Syntax.local_theory_to_proof..global_interpretationC *)
|
walther@60127
|
765 |
val interpretation_args_with_defs =
|
walther@60127
|
766 |
Parse.!!! Parse_Spec.locale_expression --
|
walther@60127
|
767 |
(Scan.optional (\<^keyword>\<open>defines\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
|
walther@60127
|
768 |
-- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\<open>=\<close> -- Parse.term))) ([]));
|
walther@60119
|
769 |
\<close> ML \<open>
|
walther@60127
|
770 |
Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>global_interpretationC\<close>
|
walther@60127
|
771 |
"prove interpretation of locale expression into global theory"
|
walther@60127
|
772 |
(interpretation_args_with_defs >> (fn (expr, defs) =>
|
walther@60127
|
773 |
Interpretation.global_interpretation_cmd expr defs));
|
walther@60119
|
774 |
\<close> ML \<open>
|
walther@60127
|
775 |
(interpretation_args_with_defs >> (fn (expr, defs) =>
|
walther@60127
|
776 |
Interpretation.global_interpretation_cmd expr defs))
|
walther@60127
|
777 |
: Token.T list -> (local_theory -> Proof.state) * Token.T list;
|
walther@60123
|
778 |
\<close> ML \<open>
|
walther@60127
|
779 |
\<close> ML \<open> (* Outer_Syntax.local_theory_to_proof..Problem *)
|
walther@60128
|
780 |
(ParseC.problem_headline >> prove_vc);
|
walther@60123
|
781 |
\<close> ML \<open>
|
walther@60128
|
782 |
Parse.name: string parser;
|
walther@60128
|
783 |
Parse.name: Token.T list -> string * Token.T list;
|
walther@60128
|
784 |
\<close> ML \<open>
|
walther@60128
|
785 |
SPARK_Commands.prove_vc: string -> Proof.context -> Proof.state
|
walther@60128
|
786 |
\<close> ML \<open>(*-------- new -----------*)
|
walther@60128
|
787 |
ParseC.problem_headline: ParseC.problem_headline parser;
|
walther@60128
|
788 |
ParseC.problem_headline: Token.T list -> ParseC.problem_headline * Token.T list;
|
walther@60128
|
789 |
\<close> ML \<open>
|
walther@60128
|
790 |
prove_vc: ParseC.problem_headline -> Proof.context -> Proof.state
|
walther@60123
|
791 |
\<close> ML \<open>
|
walther@60119
|
792 |
\<close>
|
walther@60119
|
793 |
|
walther@60123
|
794 |
subsection \<open>testbed for Problem\<close>
|
walther@60119
|
795 |
ML \<open>
|
walther@60119
|
796 |
\<close> ML \<open>
|
walther@60128
|
797 |
val headline = "(\"Biegelinie\", [\"Biegelinien\"])";
|
walther@60128
|
798 |
val toks = ParseC.tokenize headline;
|
walther@60128
|
799 |
ParseC.problem_headline toks;
|
walther@60127
|
800 |
\<close> ML \<open>
|
walther@60119
|
801 |
\<close>
|
walther@60105
|
802 |
|
walther@60123
|
803 |
|
walther@60129
|
804 |
end(* SEE "outcomment before creating session Isac" ABOVE !!! OTHERWISE YOU HAVE..
|
walther@60127
|
805 |
ERROR: Found the end of the theory, but the last SPARK environment is still open.
|
walther@60129
|
806 |
..is acceptable for testing spark_vc .. proof - ...
|
walther@60127
|
807 |
*)
|