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 Calc_Binop ListC Program
12 Specific constants are defined for where_-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>consts of functions in where_-conditions and program-expressions\<close>
19 lhs :: "bool => real" (*of an equality*)
20 rhs :: "bool => real" (*of an equality*)
21 Vars :: "'a => real list" (*get the variables of a term *)
22 matches :: "['a, 'a] => bool"
23 matchsub :: "['a, 'a] => bool"
24 some_occur_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
25 occurs_in :: "[real , 'a] => bool" ("_ occurs'_in _")
27 abs :: "real => real" ("(|| _ ||)")
28 (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
29 absset :: "real set => real" ("(||| _ |||)")
30 is_atom :: "real => bool" ("_ is'_atom" 10)
31 is_num :: "real => bool" ("_ is'_num" 10)
32 is_even :: "real => bool" ("_ is'_even" 10)
34 (* identity on term level*)
35 ident :: "['a, 'a] => bool" ("(_ =!=/ _)" [51, 51] 50)
36 argument_in :: "real => real" ("argument'_in _" 10)
37 sameFunId :: "[real, bool] => bool" (* "same_funid _ _" 10
38 WN0609 changed the id, because ".. _ _" inhibits currying *)
39 filter_sameFunId:: "[real, bool list] => bool list" ("filter'_sameFunId _ _" 10)
40 boollist2sum :: "bool list => real"
41 lastI :: "'a list \<Rightarrow> 'a"
43 subsection \<open>ML code for functions in where_-conditions and program-expressions\<close>
47 val eval_lhs: 'a -> string -> term -> 'b -> (string * term) option
48 val eval_matches: string -> string -> term -> Proof.context -> (string * term) option
49 val matchsub: theory -> term -> term -> bool
50 val eval_matchsub: string -> string -> term -> Proof.context -> (string * term) option
51 val eval_rhs: 'a -> string -> term -> 'b -> (string * term) option
52 val eval_var: string -> string -> term -> Proof.context -> (string * term) option
54 val or2list: term -> term
56 val occurs_in: term -> term -> bool
57 val eval_occurs_in: 'a -> string -> term -> 'b -> (string * term) option
58 val some_occur_in: term list -> term -> bool
59 val eval_some_occur_in: 'a -> string -> term -> 'b -> (string * term) option
60 val eval_is_atom: string -> string -> term -> 'a -> (string * term) option
61 val eval_is_num: string -> string -> term -> 'a -> (string * term) option
63 val eval_is_even: string -> string -> term -> 'a -> (string * term) option
64 val eval_equ: string -> string -> term -> 'a -> (string * term) option
65 val eval_ident: string -> string -> term -> Proof.context -> (string * term) option
66 val eval_equal: string -> string -> term -> Proof.context -> (string * term) option
67 val eval_cancel: string -> string -> term -> 'a -> (string * term) option
68 val eval_argument_in: string -> string -> term -> 'a -> (string * term) option
69 val same_funid: term -> term -> bool
70 val eval_sameFunId: string -> string -> term -> 'a -> (string * term) option
71 val eval_filter_sameFunId: string -> string -> term -> 'a -> (string * term) option
72 val list2sum: term list -> term
73 val eval_boollist2sum: string -> string -> term -> 'a -> (string * term) option
75 val mk_thmid_f: string -> (int * int) * (int * int) -> (int * int) * (int * int) -> string
79 structure Prog_Expr(**): PROG_EXPR(**) =
83 (*+ for Or_to_List +*)
84 fun or2list (Const (\<^const_name>\<open>True\<close>,_)) = ((*tracing"### or2list True";*) UniversalList)
85 | or2list (Const (\<^const_name>\<open>False\<close>,_)) = ((*tracing"### or2list False";*) EmptyList)
86 | or2list (t as Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ _) = TermC.list2isalist HOLogic.boolT [t]
89 fun get ls (Const (\<^const_name>\<open>disj\<close>,_) $ o1 $ o2) =
91 Const (\<^const_name>\<open>disj\<close>,_) $ _ $ _ => get (ls @ [o1]) o2
93 | get _ t = raise TERM ("or2list: missing pattern in fun.def", [t])
94 in (((TermC.list2isalist HOLogic.boolT) o (get [])) ors) end
97 (** evaluation on the meta-level **)
99 (*. evaluate the predicate matches (match on whole term only) .*)
100 (*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*)
101 fun eval_matches (_:string) "Prog_Expr.matches"
102 (t as Const (\<^const_name>\<open>Prog_Expr.matches\<close>, _) $ pat $ tst) ctxt =
103 if TermC.matches (Proof_Context.theory_of ctxt) tst pat
106 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
107 in SOME (UnparseC.term ctxt prop, prop) end
110 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
111 in SOME (UnparseC.term ctxt prop, prop) end
112 | eval_matches _ _ _ _ = NONE;
114 (*.does a pattern match some subterm ?.*)
115 fun matchsub thy t pat =
117 fun matchs (t as Const _) = TermC.matches thy t pat
118 | matchs (t as Free _) = TermC.matches thy t pat
119 | matchs (t as Var _) = TermC.matches thy t pat
120 | matchs (Bound _) = false
121 | matchs (t as Abs (_, _, body)) =
122 if TermC.matches thy t pat then true else TermC.matches thy body pat
123 | matchs (t as f1 $ f2) =
124 if TermC.matches thy t pat then true
125 else if matchs f1 then true else matchs f2
128 (*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*)
129 fun eval_matchsub (_:string) "Prog_Expr.matchsub"
130 (t as Const (\<^const_name>\<open>Prog_Expr.matchsub\<close>, _) $ pat $ tst) ctxt =
131 if matchsub (Proof_Context.theory_of ctxt) tst pat
133 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
134 in SOME (UnparseC.term ctxt prop, prop) end
136 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
137 in SOME (UnparseC.term ctxt prop, prop) end
138 | eval_matchsub _ _ _ _ = NONE;
140 (*get the variables in an isabelle-term*)
141 (*("Vars" ,("Prog_Expr.Vars" , eval_var "#Vars_")):calc*)
142 fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) ctxt =
144 val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t;
145 val thmId = thmid ^ UnparseC.term ctxt arg;
146 in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end
147 | eval_var _ _ _ _ = NONE;
149 (*("lhs" ,("Prog_Expr.lhs" , eval_lhs "")):calc*)
150 fun eval_lhs _ "Prog_Expr.lhs" (t as (Const (\<^const_name>\<open>lhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _))) _ =
151 SOME ((UnparseC.term @{context} t) ^ " = " ^ (UnparseC.term @{context} l),
152 HOLogic.Trueprop $ (TermC.mk_equality (t, l)))
153 | eval_lhs _ _ _ _ = NONE;
155 fun rhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r) = r
156 | rhs t = raise ERROR("rhs called with (" ^ UnparseC.term @{context} t ^ ")");
157 (*("rhs" ,("Prog_Expr.rhs" , eval_rhs "")):calc*)
158 fun eval_rhs _ "Prog_Expr.rhs" (t as (Const (\<^const_name>\<open>rhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r))) _ =
159 SOME (UnparseC.term @{context} t ^ " = " ^ UnparseC.term @{context} r,
160 HOLogic.Trueprop $ (TermC.mk_equality (t, r)))
161 | eval_rhs _ _ _ _ = NONE;
163 fun occurs_in v t = member op = (((map ThmC.cut_longid) o TermC.ids2str) t) (Term.term_name v);
164 (*("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""))*)
165 fun eval_occurs_in _ "Prog_Expr.occurs_in" (p as (Const (\<^const_name>\<open>occurs_in\<close>, _) $ v $ t)) _ =
166 ((*tracing("#>@ eval_occurs_in: v= " ^ UnparseC.term @{context} v);
167 tracing("#>@ eval_occurs_in: t= " ^ UnparseC.term @{context} t);*)
169 then SOME ((UnparseC.term @{context} p) ^ " = True",
170 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
171 else SOME ((UnparseC.term @{context} p) ^ " = False",
172 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))))
173 | eval_occurs_in _ _ _ _ = NONE;
175 (*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)
176 fun some_occur_in vs t =
177 let fun occurs_in' a b = occurs_in b a
178 in foldl or_ (false, map (occurs_in' t) vs) end;
180 (*("some_occur_in", ("Prog_Expr.some_occur_in",
181 eval_some_occur_in "#eval_some_occur_in_"))*)
182 fun eval_some_occur_in _ "Prog_Expr.some_occur_in"
183 (p as (Const (\<^const_name>\<open>some_occur_in\<close>,_) $ vs $ t)) _ =
184 if some_occur_in (TermC.isalist2list vs) t
185 then SOME ((UnparseC.term @{context} p) ^ " = True",
186 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
187 else SOME ((UnparseC.term @{context} p) ^ " = False",
188 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
189 | eval_some_occur_in _ _ _ _ = NONE;
191 (*("is_atom",("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"))*)
192 fun eval_is_atom (thmid:string) "Prog_Expr.is_atom" (t as (Const _ $ arg)) _ =
194 then SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "",
195 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
196 else SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "",
197 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
198 | eval_is_atom _ _ _ _ = NONE;
200 (*("is_num",("Prog_Expr.is_num", Prog_Expr.eval_is_num "#is_num_"))*)
201 fun eval_is_num (thmid:string) "Prog_Expr.is_num" (t as (Const _ $ arg)) _ =
203 then SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "",
204 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
205 else SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "",
206 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
207 | eval_is_num _ _ _ _ = NONE;
209 fun even i = (i div 2) * 2 = i;
210 (*("is_even",("Prog_Expr.is_even", eval_is_even "#is_even_"))*)
211 fun eval_is_even (thmid:string) "Prog_Expr.is_even" (t as (Const _ $ arg)) _ =
215 val i = arg |> HOLogic.dest_number |> snd
218 then SOME (TermC.mk_thmid thmid (string_of_int i) "",
219 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
220 else SOME (TermC.mk_thmid thmid "" "",
221 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
224 | eval_is_even _ _ _ _ = NONE;
226 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
227 (*("PLUS" ,(\<^const_name>\<open>plus\<close> , (**)eval_binop "#add_")),
228 ("TIMES" ,(\<^const_name>\<open>times\<close> , (**)eval_binop "#mult_")),
229 ("POWER" ,(\<^const_name>\<open>realpow\<close> , (**)eval_binop "#power_"))*)
231 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
232 ("xxxxxx",op_,t,thy);
234 fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) = (* dropped *)
236 (string_of_int v11)^", "^(string_of_int v12)^"), ("^
237 (string_of_int p11)^", "^(string_of_int p12)^")) __ (("^
238 (string_of_int v21)^", "^(string_of_int v22)^"), ("^
239 (string_of_int p21)^", "^(string_of_int p22)^"))";
241 (*.evaluate < and <= for numerals.*)
242 (*("le" ,(\<^const_name>\<open>less\<close> , Prog_Expr.eval_equ "#less_")),
243 ("leq" ,(\<^const_name>\<open>less_eq\<close> , Prog_Expr.eval_equ "#less_equal_"))*)
245 fun eval_equ (thmid:string) (_(*op_*)) (t as (Const (op0, _)) $ t1 $ t2) _ =
246 if TermC.is_num t1 andalso TermC.is_num t2 then
248 val n1 = t1 |> HOLogic.dest_number |> snd
249 val n2 = t2 |> HOLogic.dest_number |> snd
251 if Eval.calc_equ (ThmC.cut_longid op0) (n1, n2)
252 then SOME (TermC.mk_thmid thmid (string_of_int n1) (string_of_int n2),
253 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
254 else SOME (TermC.mk_thmid thmid (string_of_int n1) (string_of_int n2),
255 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
258 | eval_equ _ _ _ _ = NONE;
263 val it = "(?t = ?t) = True"
264 > val t = TermC.parse_test @{context} "x = 0";
265 > val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
267 > val t = TermC.parse_test @{context} "1 = 0";
268 > val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
269 ----------- thus needs Rule.Eval !
270 > val t = TermC.parse_test @{context} "0 = 0";
271 > val SOME (t',_) = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
272 > UnparseC.term @{context} t';
273 val it = \<^const_name>\<open>True\<close>
275 val t = TermC.parse_test @{context} "Not (x = 0)";
276 atomt t; UnparseC.term @{context} t;
282 val it = "x ~= 0" : string*)
284 (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of
285 the arguments: thus special handling by 'fun eval_binop'*)
286 (*("ident" ,("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")):calc*)
287 fun eval_ident (thmid:string) "Prog_Expr.ident" (t as
288 (Const _(*op0, t0*) $ t1 $ t2 )) ctxt =
290 then SOME (TermC.mk_thmid thmid
291 ("(" ^ (UnparseC.term ctxt t1) ^ ")")
292 ("(" ^ (UnparseC.term ctxt t2) ^ ")"),
293 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
294 else SOME (TermC.mk_thmid thmid
295 ("(" ^ (UnparseC.term ctxt t1) ^ ")")
296 ("(" ^ (UnparseC.term ctxt t2) ^ ")"),
297 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
298 | eval_ident _ _ _ _ = NONE;
300 > val t = TermC.parse_test @{context} "x =!= 0";
301 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
302 > UnparseC.term @{context} t';
303 val str = "ident_(x)_(0)" : string
304 val it = "(x =!= 0) = False" : string
305 > val t = TermC.parse_test @{context} "1 =!= 0";
306 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
307 > UnparseC.term @{context} t';
308 val str = "ident_(1)_(0)" : string
309 val it = "(1 =!= 0) = False" : string
310 > val t = TermC.parse_test @{context} "0 =!= 0";
311 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
312 > UnparseC.term @{context} t';
313 val str = "ident_(0)_(0)" : string
314 val it = "(0 =!= 0) = True" : string
318 (* evaluate identity of terms, which stay ready for further evaluation;
319 thus returns False only for atoms *)
320 (*("equal" ,(\<^const_name>\<open>HOL.eq\<close>, Prog_Expr.eval_equal "#equal_")):calc*)
321 fun eval_equal (thmid : string) \<^const_name>\<open>HOL.eq\<close> (t as (Const _(*op0,t0*) $ t1 $ t2 )) ctxt =
324 SOME (TermC.mk_thmid thmid
325 ("(" ^ UnparseC.term ctxt t1 ^ ")") ("(" ^ UnparseC.term ctxt t2 ^ ")"),
326 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
328 (case (TermC.is_atom t1, TermC.is_atom t2) of
330 if TermC.variable_constant_pair (t1, t2)
332 else SOME (TermC.mk_thmid thmid
333 ("(" ^ UnparseC.term ctxt t1 ^ ")") ("(" ^ UnparseC.term ctxt t2 ^ ")"),
334 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
335 | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
336 | eval_equal _ _ _ _ = NONE; (* error-exit *)
338 (*. evaluate HOL.divide .*)
339 (*("DIVIDE" ,("Rings.divide_class.divide" , eval_cancel "#divide_e"))*)
340 fun eval_cancel thmid "Rings.divide_class.divide" (t as (Const _ $ t1 $ t2)) _ =
341 if TermC.is_num t1 andalso TermC.is_num t2 then
343 val (T, _) = HOLogic.dest_number t1;
344 val (i1, i2) = (Eval.int_of_numeral t1, Eval.int_of_numeral t2);
345 val res_int as (d, (i1', i2')) = Eval.cancel_int (i1, i2);
347 if abs d = 1 andalso (abs i1, abs i2) = (abs i1', abs i2') then NONE
350 val res = TermC.mk_frac T res_int;
351 val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
352 in SOME (TermC.mk_thmid thmid (string_of_int i1) (string_of_int i2), prop) end
355 | eval_cancel _ _ _ _ = NONE;
357 (* get the argument from a function-definition *)
358 (*("argument_in" ,("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in"))*)
359 fun eval_argument_in _ "Prog_Expr.argument_in"
360 (t as (Const ("Prog_Expr.argument_in", _) $ (_(*f*) $ arg))) _ =
361 if TermC.is_atom arg (*could be something to be simplified before*)
363 SOME (UnparseC.term @{context} t ^ " = " ^ UnparseC.term @{context} arg,
364 HOLogic.Trueprop $ (TermC.mk_equality (t, arg)))
366 | eval_argument_in _ _ _ _ = NONE;
368 (* check if the function-identifier of the first argument matches
369 the function-identifier of the lhs of the second argument *)
370 (*("sameFunId" ,("Prog_Expr.sameFunId", eval_same_funid "Prog_Expr.sameFunId"))*)
371 fun eval_sameFunId _ "Prog_Expr.sameFunId"
372 (p as Const ("Prog_Expr.sameFunId",_) $ (f1 $ _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _)) _ =
374 then SOME ((UnparseC.term @{context} p) ^ " = True",
375 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
376 else SOME ((UnparseC.term @{context} p) ^ " = False",
377 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
378 | eval_sameFunId _ _ _ _ = NONE;
381 (*.from a list of fun-definitions "f x = ..." as 2nd argument
382 filter the elements with the same fun-identfier in "f y"
384 this is, because Isabelles filter takes more than 1 sec.*)
385 fun same_funid f1 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _) = f1 = f2
386 | same_funid f1 t = raise ERROR ("same_funid called with t = ("
387 ^ UnparseC.term @{context} f1 ^ ") (" ^ UnparseC.term @{context} t ^ ")");
388 (*("filter_sameFunId" ,("Prog_Expr.filter_sameFunId",
389 eval_filter_sameFunId "Prog_Expr.filter_sameFunId"))*)
390 fun eval_filter_sameFunId _ "Prog_Expr.filter_sameFunId"
391 (p as Const ("Prog_Expr.filter_sameFunId",_) $
393 let val fs' = ((TermC.list2isalist HOLogic.boolT) o
394 (filter (same_funid fid))) (TermC.isalist2list fs)
395 in SOME (UnparseC.term @{context} (TermC.mk_equality (p, fs')),
396 HOLogic.Trueprop $ (TermC.mk_equality (p, fs'))) end
397 | eval_filter_sameFunId _ _ _ _ = NONE;
399 (* make a list of terms to a sum *)
400 fun list2sum [] = raise ERROR ("list2sum called with []")
404 fun sum su [s'] = Const (\<^const_name>\<open>plus\<close>,
405 [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s'
406 | sum su (s'::ss') = sum (Const (\<^const_name>\<open>plus\<close>,
407 [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s') ss'
408 | sum _ _ = raise ERROR "list2sum: pattern in fun.def is missing"
411 (* make a list of equalities to the sum of the lhs *)
412 (*("boollist2sum" ,("Prog_Expr.boollist2sum" , eval_boollist2sum "")):calc*)
413 fun eval_boollist2sum _ "Prog_Expr.boollist2sum"
414 (p as Const ("Prog_Expr.boollist2sum", _) $ (l as Const (\<^const_name>\<open>Cons\<close>, _) $ _ $ _)) _ =
416 val isal = TermC.isalist2list l
417 val lhss = map TermC.lhs isal
418 val sum = list2sum lhss
420 SOME ((UnparseC.term @{context} p) ^ " = " ^ (UnparseC.term @{context} sum),
421 HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))
423 | eval_boollist2sum _ _ _ _ = NONE;
426 \<close> text \<open>
432 subsection \<open>extend rule-set for evaluating where_-conditions and program-expressions\<close>
434 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [\<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs "")];
439 subsection \<open>setup for rule-sets and ML-functions\<close>
441 rule_set_knowledge prog_expr = prog_expr
443 calculation lhs = \<open>Prog_Expr.eval_lhs ""\<close>
444 calculation rhs = \<open>Prog_Expr.eval_rhs ""\<close>
445 calculation Vars = \<open>Prog_Expr.eval_var "#Vars_"\<close>
446 calculation matches = \<open>Prog_Expr.eval_matches "#matches_"\<close>
447 calculation matchsub = \<open>Prog_Expr.eval_matchsub "#matchsub_"\<close>
449 calculation some_occur_in = \<open>Prog_Expr.eval_some_occur_in "#some_occur_in_"\<close>
450 calculation occurs_in = \<open>Prog_Expr.eval_occurs_in "#occurs_in_"\<close>
451 calculation is_atom = \<open>Prog_Expr.eval_is_atom "#is_atom_"\<close>
452 calculation is_num = \<open>Prog_Expr.eval_is_num "#is_num_"\<close>
453 calculation is_even = \<open>Prog_Expr.eval_is_even "#is_even_"\<close>