1 (* title: ProgLang/Prog_Expr.thy
2 functions for expressions (which do NOT contain Prog_Tac and Tactical, by definition))
3 author: Walther Neuper, Aug.2019
4 (c) copyright due to lincense terms.
8 imports Calculate ListC Program
12 Specific constants are defined for pre-conditions of programs and for program-expressions.
13 The constants are connected with ML functions for evaluation of respective expressions
14 (all named eval_*), such that Isac's rewrite engine can handle it.
17 subsection \<open>Power re-defined for a specific type\<close>
19 pow :: "[real, real] => real" (infixr "^^^" 80)
21 subsection \<open>consts of functions in pre-conditions and program-expressions\<close>
23 lhs :: "bool => real" (*of an equality*)
24 rhs :: "bool => real" (*of an equality*)
25 Vars :: "'a => real list" (*get the variables of a term *)
26 matches :: "['a, 'a] => bool"
27 matchsub :: "['a, 'a] => bool"
28 some'_occur'_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
29 occurs'_in :: "[real , 'a] => bool" ("_ occurs'_in _")
31 abs :: "real => real" ("(|| _ ||)")
32 (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
33 absset :: "real set => real" ("(||| _ |||)")
34 (*is numeral constant ?*)
35 is'_const :: "real => bool" ("_ is'_const" 10)
36 (*is_const rename to is_num FIXXXME.WN.16.5.03 *)
37 is'_atom :: "real => bool" ("_ is'_atom" 10)
38 is'_even :: "real => bool" ("_ is'_even" 10)
40 (* identity on term level*)
41 ident :: "['a, 'a] => bool" ("(_ =!=/ _)" [51, 51] 50)
42 argument'_in :: "real => real" ("argument'_in _" 10)
43 sameFunId :: "[real, bool] => bool" (* "same'_funid _ _" 10
44 WN0609 changed the id, because ".. _ _" inhibits currying *)
45 filter'_sameFunId:: "[real, bool list] => bool list"
46 ("filter'_sameFunId _ _" 10)
47 boollist2sum :: "bool list => real"
48 lastI :: "'a list \<Rightarrow> 'a"
50 subsection \<open>ML code for functions in pre-conditions and program-expressions\<close>
54 (*//------------------------- from Tools .thy-------------------------------------------------\\*)
56 val eval_lhs: 'a -> string -> term -> 'b -> (string * term) option
57 val eval_matches: string -> string -> term -> theory -> (string * term) option
58 val matchsub: theory -> term -> term -> bool
59 val eval_matchsub: string -> string -> term -> theory -> (string * term) option
61 val eval_rhs: 'a -> string -> term -> 'b -> (string * term) option
62 val eval_var: string -> string -> term -> theory -> (string * term) option
64 val or2list: term -> term
65 (*\\------------------------- from Tools .thy-------------------------------------------------//*)
66 (*//------------------------- from Atools .thy------------------------------------------------\\*)
67 val occurs_in: term -> term -> bool
68 val eval_occurs_in: 'a -> string -> term -> 'b -> (string * term) option
69 val some_occur_in: term list -> term -> bool
70 val eval_some_occur_in: 'a -> string -> term -> 'b -> (string * term) option
71 val eval_is_atom: string -> string -> term -> 'a -> (string * term) option
73 val eval_is_even: string -> string -> term -> 'a -> (string * term) option
74 val eval_const: string -> string -> term -> 'a -> (string * term) option
75 val eval_equ: string -> string -> term -> 'a -> (string * term) option
76 val eval_ident: string -> string -> term -> theory -> (string * term) option
77 val eval_equal: string -> string -> term -> theory -> (string * term) option
78 val eval_cancel: string -> string -> term -> 'a -> (string * term) option
79 val eval_argument_in: string -> string -> term -> 'a -> (string * term) option
80 val same_funid: term -> term -> bool
81 val eval_sameFunId: string -> string -> term -> 'a -> (string * term) option
82 val eval_filter_sameFunId: string -> string -> term -> 'a -> (string * term) option
83 val list2sum: term list -> term
84 val eval_boollist2sum: string -> string -> term -> 'a -> (string * term) option
86 val mk_thmid_f: string -> (int * int) * (int * int) -> (int * int) * (int * int) -> string
87 (*\\------------------------- from Atools.thy------------------------------------------------//*)
88 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
90 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
92 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
96 structure Prog_Expr(**): PROG_EXPR =(**)
100 (*+ for Or_to_List +*)
101 fun or2list (Const ("HOL.True",_)) = ((*tracing"### or2list True";*) UniversalList)
102 | or2list (Const ("HOL.False",_)) = ((*tracing"### or2list False";*) EmptyList)
103 | or2list (t as Const ("HOL.eq",_) $ _ $ _) = TermC.list2isalist HOLogic.boolT [t]
106 fun get ls (Const ("HOL.disj",_) $ o1 $ o2) =
108 Const ("HOL.disj",_) $ _ $ _ => get (ls @ [o1]) o2
109 | _ => ls @ [o1, o2])
110 | get _ t = raise TERM ("or2list: missing pattern in fun.def", [t])
111 in (((TermC.list2isalist HOLogic.boolT) o (get [])) ors) end
112 (*>val t = @{term True};
113 > val t' = or2list t;
115 "ListC.UniversalList"
116 > val t = @{term False};
117 > val t' = or2list t;
120 > val t=(Thm.term_of o the o (parse thy)) "x=3";
121 > val t' = or2list t;
124 > val t=(Thm.term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";
125 > val t' = or2list t;
127 "[x = #3, x = #-3, x = #0]" : string *)
130 (** evaluation on the meta-level **)
132 (*. evaluate the predicate matches (match on whole term only) .*)
133 (*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*)
134 fun eval_matches (_:string) "Prog_Expr.matches" (t as Const ("Prog_Expr.matches",_) $ pat $ tst) thy =
135 if TermC.matches thy tst pat
138 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
139 in SOME (UnparseC.term_in_thy thy prop, prop) end
142 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
143 in SOME (UnparseC.term_in_thy thy prop, prop) end
144 | eval_matches _ _ _ _ = NONE;
146 > val t = (Thm.term_of o the o (parse thy))
147 "matches (?x = 0) (1 * x ^^^ 2 = 0)";
148 > eval_matches "/thmid/" "/op_/" t thy;
151 ("matches (x = 0) (1 * x ^^^ 2 = 0) = False",
152 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
154 > val t = (Thm.term_of o the o (parse thy))
155 "matches (?a = #0) (#1 * x ^^^ #2 = #0)";
156 > eval_matches "/thmid/" "/op_/" t thy;
159 ("matches (?a = #0) (#1 * x ^^^ #2 = #0) = True",
160 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
162 > val t = (Thm.term_of o the o (parse thy))
163 "matches (?a * x = #0) (#1 * x ^^^ #2 = #0)";
164 > eval_matches "/thmid/" "/op_/" t thy;
167 ("matches (?a * x = #0) (#1 * x ^^^ #2 = #0) = False",
168 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
170 > val t = (Thm.term_of o the o (parse thy))
171 "matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0)";
172 > eval_matches "/thmid/" "/op_/" t thy;
175 ("matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0) = True",
176 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
177 ----- before ?patterns ---:
178 > val t = (Thm.term_of o the o (parse thy))
179 "matches (a * b^^^#2 = c) (#3 * x^^^#2 = #1)";
180 > eval_matches "/thmid/" "/op_/" t thy;
182 ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2 = #1) = True",
183 Const ("HOL.Trueprop", "bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
184 : (string * term) option
186 > val t = (Thm.term_of o the o (parse thy))
187 "matches (a * b^^^#2 = c) (#3 * x^^^#2222 = #1)";
188 > eval_matches "/thmid/" "/op_/" t thy;
189 SOME ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2222 = #1) = False",
190 Const ("HOL.Trueprop", "bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
192 > val t = (Thm.term_of o the o (parse thy))
193 "matches (a = b) (x + #1 + #-1 * #2 = #0)";
194 > eval_matches "/thmid/" "/op_/" t thy;
195 SOME ("matches (a = b) (x + #1 + #-1 * #2 = #0) = True",Const # $ (# $ #))
198 (*.does a pattern match some subterm ?.*)
199 fun matchsub thy t pat =
201 fun matchs (t as Const _) = TermC.matches thy t pat
202 | matchs (t as Free _) = TermC.matches thy t pat
203 | matchs (t as Var _) = TermC.matches thy t pat
204 | matchs (Bound _) = false
205 | matchs (t as Abs (_, _, body)) =
206 if TermC.matches thy t pat then true else TermC.matches thy body pat
207 | matchs (t as f1 $ f2) =
208 if TermC.matches thy t pat then true
209 else if matchs f1 then true else matchs f2
212 (*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*)
213 fun eval_matchsub (_:string) "Prog_Expr.matchsub"
214 (t as Const ("Prog_Expr.matchsub",_) $ pat $ tst) thy =
215 if matchsub thy tst pat
217 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
218 in SOME (UnparseC.term_in_thy thy prop, prop) end
220 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
221 in SOME (UnparseC.term_in_thy thy prop, prop) end
222 | eval_matchsub _ _ _ _ = NONE;
224 (*get the variables in an isabelle-term*)
225 (*("Vars" ,("Prog_Expr.Vars" , eval_var "#Vars_")):calc*)
226 fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) thy =
228 val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t;
229 val thmId = thmid ^ UnparseC.term_in_thy thy arg;
230 in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end
231 | eval_var _ _ _ _ = NONE;
233 (* refer to Thm.lhs_of *)
234 fun lhs (Const ("HOL.eq",_) $ l $ _) = l
235 | lhs t = raise ERROR("lhs called with (" ^ UnparseC.term t ^ ")");
236 (*("lhs" ,("Prog_Expr.lhs" , eval_lhs "")):calc*)
237 fun eval_lhs _ "Prog_Expr.lhs" (t as (Const ("Prog_Expr.lhs",_) $ (Const ("HOL.eq",_) $ l $ _))) _ =
238 SOME ((UnparseC.term t) ^ " = " ^ (UnparseC.term l),
239 HOLogic.Trueprop $ (TermC.mk_equality (t, l)))
240 | eval_lhs _ _ _ _ = NONE;
242 > val t = (Thm.term_of o the o (parse thy)) "lhs (1 * x ^^^ 2 = 0)";
243 > val SOME (id,t') = eval_lhs 0 0 t 0;
244 val id = "Prog_Expr.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
246 val it = "Prog_Expr.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
249 fun rhs (Const ("HOL.eq",_) $ _ $ r) = r
250 | rhs t = raise ERROR("rhs called with (" ^ UnparseC.term t ^ ")");
251 (*("rhs" ,("Prog_Expr.rhs" , eval_rhs "")):calc*)
252 fun eval_rhs _ "Prog_Expr.rhs" (t as (Const ("Prog_Expr.rhs",_) $ (Const ("HOL.eq",_) $ _ $ r))) _ =
253 SOME (UnparseC.term t ^ " = " ^ UnparseC.term r,
254 HOLogic.Trueprop $ (TermC.mk_equality (t, r)))
255 | eval_rhs _ _ _ _ = NONE;
256 (*\\------------------------- from Prog_Expr.thy-------------------------------------------------//*)
258 (*//------------------------- from Atools.thy------------------------------------------------\\*)
259 fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
261 (*("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""))*)
262 fun eval_occurs_in _ "Prog_Expr.occurs'_in" (p as (Const ("Prog_Expr.occurs'_in",_) $ v $ t)) _ =
263 ((*tracing("#>@ eval_occurs_in: v= "^(UnparseC.term v));
264 tracing("#>@ eval_occurs_in: t= "^(UnparseC.term t));*)
266 then SOME ((UnparseC.term p) ^ " = True",
267 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
268 else SOME ((UnparseC.term p) ^ " = False",
269 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))))
270 | eval_occurs_in _ _ _ _ = NONE;
272 (*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)
273 fun some_occur_in vs t =
274 let fun occurs_in' a b = occurs_in b a
275 in foldl or_ (false, map (occurs_in' t) vs) end;
277 (*("some_occur_in", ("Prog_Expr.some'_occur'_in",
278 eval_some_occur_in "#eval_some_occur_in_"))*)
279 fun eval_some_occur_in _ "Prog_Expr.some'_occur'_in"
280 (p as (Const ("Prog_Expr.some'_occur'_in",_) $ vs $ t)) _ =
281 if some_occur_in (TermC.isalist2list vs) t
282 then SOME ((UnparseC.term p) ^ " = True",
283 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
284 else SOME ((UnparseC.term p) ^ " = False",
285 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
286 | eval_some_occur_in _ _ _ _ = NONE;
288 (*("is_atom",("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_"))*)
289 fun eval_is_atom (thmid:string) "Prog_Expr.is'_atom"
290 (t as (Const _ $ arg)) _ =
292 Free (n,_) => SOME (TermC.mk_thmid thmid n "",
293 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
294 | _ => SOME (TermC.mk_thmid thmid "" "",
295 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
296 | eval_is_atom _ _ _ _ = NONE;
298 fun even i = (i div 2) * 2 = i;
299 (*("is_even",("Prog_Expr.is'_even", eval_is_even "#is_even_"))*)
300 fun eval_is_even (thmid:string) "Prog_Expr.is'_even"
301 (t as (Const _ $ arg)) _ =
304 (case ThmC_Def.int_opt_of_string n of
306 if even i then SOME (TermC.mk_thmid thmid n "",
307 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
308 else SOME (TermC.mk_thmid thmid "" "",
309 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
312 | eval_is_even _ _ _ _ = NONE;
314 (*evaluate 'is_const'*)
315 (*("is_const",("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"))*)
316 fun eval_const (thmid:string) _ (t as (Const _ $ arg)) _ =
319 SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
322 then SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
323 else SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
325 SOME (TermC.mk_thmid thmid (UnparseC.term arg) "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
326 | eval_const _ _ _ _ = NONE;
328 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
329 (*("PLUS" ,("Groups.plus_class.plus" , (**)eval_binop "#add_")),
330 ("TIMES" ,("Groups.times_class.times" , (**)eval_binop "#mult_")),
331 ("POWER" ,("Prog_Expr.pow" , (**)eval_binop "#power_"))*)
333 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
334 ("xxxxxx",op_,t,thy);
336 fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) = (* dropped *)
338 (string_of_int v11)^", "^(string_of_int v12)^"), ("^
339 (string_of_int p11)^", "^(string_of_int p12)^")) __ (("^
340 (string_of_int v21)^", "^(string_of_int v22)^"), ("^
341 (string_of_int p21)^", "^(string_of_int p22)^"))";
343 (*.evaluate < and <= for numerals.*)
344 (*("le" ,("Orderings.ord_class.less" , Prog_Expr.eval_equ "#less_")),
345 ("leq" ,("Orderings.ord_class.less_eq" , Prog_Expr.eval_equ "#less_equal_"))*)
346 fun eval_equ (thmid:string) (_(*op_*)) (t as
347 (Const (op0, _) $ Free (n1, _) $ Free(n2, _))) _ =
348 (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of
349 (SOME n1', SOME n2') =>
350 if Eval.calc_equ (strip_thy op0) (n1', n2')
351 then SOME (TermC.mk_thmid thmid n1 n2,
352 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
353 else SOME (TermC.mk_thmid thmid n1 n2,
354 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
357 | eval_equ _ _ _ _ = NONE;
362 val it = "(?t = ?t) = True"
363 > val t = str2term "x = 0";
364 > val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
366 > val t = str2term "1 = 0";
367 > val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
368 ----------- thus needs Rule.Eval !
369 > val t = str2term "0 = 0";
370 > val SOME (t',_) = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
374 val t = str2term "Not (x = 0)";
375 atomt t; UnparseC.term t;
381 val it = "x ~= 0" : string*)
383 (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of
384 the arguments: thus special handling by 'fun eval_binop'*)
385 (*("ident" ,("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")):calc*)
386 fun eval_ident (thmid:string) "Prog_Expr.ident" (t as
387 (Const _(*op0, t0*) $ t1 $ t2 )) thy =
389 then SOME (TermC.mk_thmid thmid
390 ("(" ^ (UnparseC.term_in_thy thy t1) ^ ")")
391 ("(" ^ (UnparseC.term_in_thy thy t2) ^ ")"),
392 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
393 else SOME (TermC.mk_thmid thmid
394 ("(" ^ (UnparseC.term_in_thy thy t1) ^ ")")
395 ("(" ^ (UnparseC.term_in_thy thy t2) ^ ")"),
396 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
397 | eval_ident _ _ _ _ = NONE;
399 > val t = str2term "x =!= 0";
400 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
402 val str = "ident_(x)_(0)" : string
403 val it = "(x =!= 0) = False" : string
404 > val t = str2term "1 =!= 0";
405 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
407 val str = "ident_(1)_(0)" : string
408 val it = "(1 =!= 0) = False" : string
409 > val t = str2term "0 =!= 0";
410 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
412 val str = "ident_(0)_(0)" : string
413 val it = "(0 =!= 0) = True" : string
417 (* evaluate identity of terms, which stay ready for further evaluation;
418 thus returns False only for atoms *)
419 (*("equal" ,("HOL.eq", Prog_Expr.eval_equal "#equal_")):calc*)
420 fun eval_equal (thmid : string) "HOL.eq" (t as (Const _(*op0,t0*) $ t1 $ t2 )) thy =
423 SOME (TermC.mk_thmid thmid
424 ("(" ^ UnparseC.term_in_thy thy t1 ^ ")") ("(" ^ UnparseC.term_in_thy thy t2 ^ ")"),
425 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
427 (case (TermC.is_atom t1, TermC.is_atom t2) of
429 if TermC.variable_constant_pair (t1, t2)
431 else SOME (TermC.mk_thmid thmid
432 ("(" ^ UnparseC.term_in_thy thy t1 ^ ")") ("(" ^ UnparseC.term_in_thy thy t2 ^ ")"),
433 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
434 | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
435 | eval_equal _ _ _ _ = NONE; (* error-exit *)
437 (*. evaluate HOL.divide .*)
438 (*("DIVIDE" ,("Rings.divide_class.divide" , eval_cancel "#divide_e"))*)
439 fun eval_cancel (thmid: string) "Rings.divide_class.divide" (t as
440 (Const (op0,t0) $ Free (n1, _) $ Free(n2, _))) _ =
441 (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of
442 (SOME n1', SOME n2') =>
444 val sg = Eval.sign_mult n1' n2';
445 val (T1,T2,Trange) = TermC.dest_binop_typ t0;
446 val gcd' = Eval.gcd (abs n1') (abs n2');
448 then let val rhs = TermC.term_of_num Trange (sg * (abs n1') div gcd')
449 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
450 in SOME (TermC.mk_thmid thmid n1 n2, prop) end
451 else if 0 < n2' andalso gcd' = 1 then NONE
452 else let val rhs = TermC.mk_num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
454 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
455 in SOME (TermC.mk_thmid thmid n1 n2, prop) end
457 | _ => ((*tracing"#>@ eval_cancel NONE";*)NONE))
458 | eval_cancel _ _ _ _ = NONE;
460 (* get the argument from a function-definition *)
461 (*("argument_in" ,("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in"))*)
462 fun eval_argument_in _ "Prog_Expr.argument'_in"
463 (t as (Const ("Prog_Expr.argument'_in", _) $ (_(*f*) $ arg))) _ =
464 if is_Free arg (*could be something to be simplified before*)
466 SOME (UnparseC.term t ^ " = " ^ UnparseC.term arg,
467 HOLogic.Trueprop $ (TermC.mk_equality (t, arg)))
469 | eval_argument_in _ _ _ _ = NONE;
471 (* check if the function-identifier of the first argument matches
472 the function-identifier of the lhs of the second argument *)
473 (*("sameFunId" ,("Prog_Expr.sameFunId", eval_same_funid "Prog_Expr.sameFunId"))*)
474 fun eval_sameFunId _ "Prog_Expr.sameFunId"
475 (p as Const ("Prog_Expr.sameFunId",_) $ (f1 $ _) $ (Const ("HOL.eq", _) $ (f2 $ _) $ _)) _ =
477 then SOME ((UnparseC.term p) ^ " = True",
478 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
479 else SOME ((UnparseC.term p) ^ " = False",
480 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
481 | eval_sameFunId _ _ _ _ = NONE;
484 (*.from a list of fun-definitions "f x = ..." as 2nd argument
485 filter the elements with the same fun-identfier in "f y"
487 this is, because Isabelles filter takes more than 1 sec.*)
488 fun same_funid f1 (Const ("HOL.eq", _) $ (f2 $ _) $ _) = f1 = f2
489 | same_funid f1 t = raise ERROR ("same_funid called with t = ("
490 ^ UnparseC.term f1 ^ ") (" ^ UnparseC.term t ^ ")");
491 (*("filter_sameFunId" ,("Prog_Expr.filter'_sameFunId",
492 eval_filter_sameFunId "Prog_Expr.filter'_sameFunId"))*)
493 fun eval_filter_sameFunId _ "Prog_Expr.filter'_sameFunId"
494 (p as Const ("Prog_Expr.filter'_sameFunId",_) $
496 let val fs' = ((TermC.list2isalist HOLogic.boolT) o
497 (filter (same_funid fid))) (TermC.isalist2list fs)
498 in SOME (UnparseC.term (TermC.mk_equality (p, fs')),
499 HOLogic.Trueprop $ (TermC.mk_equality (p, fs'))) end
500 | eval_filter_sameFunId _ _ _ _ = NONE;
502 (* make a list of terms to a sum *)
503 fun list2sum [] = raise ERROR ("list2sum called with []")
507 fun sum su [s'] = Const ("Groups.plus_class.plus",
508 [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s'
509 | sum su (s'::ss') = sum (Const ("Groups.plus_class.plus",
510 [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s') ss'
511 | sum _ _ = raise ERROR "list2sum: pattern in fun.def is missing"
514 (* make a list of equalities to the sum of the lhs *)
515 (*("boollist2sum" ,("Prog_Expr.boollist2sum" , eval_boollist2sum "")):calc*)
516 fun eval_boollist2sum _ "Prog_Expr.boollist2sum"
517 (p as Const ("Prog_Expr.boollist2sum", _) $ (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
519 val isal = TermC.isalist2list l
520 val lhss = map lhs isal
521 val sum = list2sum lhss
523 SOME ((UnparseC.term p) ^ " = " ^ (UnparseC.term sum),
524 HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))
526 | eval_boollist2sum _ _ _ _ = NONE;
529 \<close> text \<open>
535 subsection \<open>extend rule-set for evaluating pre-conditions and program-expressions\<close>
537 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs "")];
542 subsection \<open>setup for rule-sets and ML-functions\<close>
543 setup \<open>KEStore_Elems.add_rlss [("prog_expr", (Context.theory_name @{theory}, prog_expr))]\<close>
544 setup \<open>KEStore_Elems.add_calcs
545 [("matches", ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")),
546 ("matchsub", ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub "#matchsub_")),
547 ("Vars", ("Prog_Expr.Vars", Prog_Expr.eval_var "#Vars_")),
548 ("lhs", ("Prog_Expr.lhs", Prog_Expr.eval_lhs "")),
549 ("rhs", ("Prog_Expr.rhs", Prog_Expr.eval_rhs ""))]\<close>
550 (*\\------------------------- from Tools .thy-------------------------------------------------//*)