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>
18 abbreviation real_powr :: "real \<Rightarrow> real \<Rightarrow> real" (infixr "\<up>" 80)
19 where "x \<up> a \<equiv> x powr a"
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_num :: "real => bool" ("_ is'_num" 10)
39 is_even :: "real => bool" ("_ is'_even" 10)
41 (* identity on term level*)
42 ident :: "['a, 'a] => bool" ("(_ =!=/ _)" [51, 51] 50)
43 argument_in :: "real => real" ("argument'_in _" 10)
44 sameFunId :: "[real, bool] => bool" (* "same_funid _ _" 10
45 WN0609 changed the id, because ".. _ _" inhibits currying *)
46 filter_sameFunId:: "[real, bool list] => bool list" ("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
72 val eval_is_num: string -> string -> term -> 'a -> (string * term) option
74 val eval_is_even: string -> string -> term -> 'a -> (string * term) option
75 val eval_const: string -> string -> term -> 'a -> (string * term) option
76 val eval_equ: string -> string -> term -> 'a -> (string * term) option
77 val eval_ident: string -> string -> term -> theory -> (string * term) option
78 val eval_equal: string -> string -> term -> theory -> (string * term) option
79 val eval_cancel: string -> string -> term -> 'a -> (string * term) option
80 val eval_argument_in: string -> string -> term -> 'a -> (string * term) option
81 val same_funid: term -> term -> bool
82 val eval_sameFunId: string -> string -> term -> 'a -> (string * term) option
83 val eval_filter_sameFunId: string -> string -> term -> 'a -> (string * term) option
84 val list2sum: term list -> term
85 val eval_boollist2sum: string -> string -> term -> 'a -> (string * term) option
87 val mk_thmid_f: string -> (int * int) * (int * int) -> (int * int) * (int * int) -> string
91 structure Prog_Expr(**): PROG_EXPR =(**)
95 (*+ for Or_to_List +*)
96 fun or2list (Const (\<^const_name>\<open>True\<close>,_)) = ((*tracing"### or2list True";*) UniversalList)
97 | or2list (Const (\<^const_name>\<open>False\<close>,_)) = ((*tracing"### or2list False";*) EmptyList)
98 | or2list (t as Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ _) = TermC.list2isalist HOLogic.boolT [t]
101 fun get ls (Const (\<^const_name>\<open>disj\<close>,_) $ o1 $ o2) =
103 Const (\<^const_name>\<open>disj\<close>,_) $ _ $ _ => get (ls @ [o1]) o2
104 | _ => ls @ [o1, o2])
105 | get _ t = raise TERM ("or2list: missing pattern in fun.def", [t])
106 in (((TermC.list2isalist HOLogic.boolT) o (get [])) ors) end
107 (*>val t = @{term True};
108 > val t' = or2list t;
110 "ListC.UniversalList"
111 > val t = @{term False};
112 > val t' = or2list t;
115 > val t=(Thm.term_of o the o (parse thy)) "x=3";
116 > val t' = or2list t;
119 > val t=(Thm.term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";
120 > val t' = or2list t;
122 "[x = #3, x = #-3, x = #0]" : string *)
125 (** evaluation on the meta-level **)
127 (*. evaluate the predicate matches (match on whole term only) .*)
128 (*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*)
129 fun eval_matches (_:string) "Prog_Expr.matches" (t as Const (\<^const_name>\<open>Prog_Expr.matches\<close>, _) $ pat $ tst) thy =
130 if TermC.matches thy tst pat
133 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
134 in SOME (UnparseC.term_in_thy thy prop, prop) end
137 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
138 in SOME (UnparseC.term_in_thy thy prop, prop) end
139 | eval_matches _ _ _ _ = NONE;
141 > val t = (Thm.term_of o the o (parse thy))
142 "matches (?x = 0) (1 * x \<up> 2 = 0)";
143 > eval_matches "/thmid/" "/op_/" t thy;
146 ("matches (x = 0) (1 * x \<up> 2 = 0) = False",
147 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
149 > val t = (Thm.term_of o the o (parse thy))
150 "matches (?a = #0) (#1 * x \<up> #2 = #0)";
151 > eval_matches "/thmid/" "/op_/" t thy;
154 ("matches (?a = #0) (#1 * x \<up> #2 = #0) = True",
155 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
157 > val t = (Thm.term_of o the o (parse thy))
158 "matches (?a * x = #0) (#1 * x \<up> #2 = #0)";
159 > eval_matches "/thmid/" "/op_/" t thy;
162 ("matches (?a * x = #0) (#1 * x \<up> #2 = #0) = False",
163 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
165 > val t = (Thm.term_of o the o (parse thy))
166 "matches (?a * x \<up> #2 = #0) (#1 * x \<up> #2 = #0)";
167 > eval_matches "/thmid/" "/op_/" t thy;
170 ("matches (?a * x \<up> #2 = #0) (#1 * x \<up> #2 = #0) = True",
171 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
172 ----- before ?patterns ---:
173 > val t = (Thm.term_of o the o (parse thy))
174 "matches (a * b \<up> #2 = c) (#3 * x \<up> #2 = #1)";
175 > eval_matches "/thmid/" "/op_/" t thy;
177 ("matches (a * b \<up> #2 = c) (#3 * x \<up> #2 = #1) = True",
178 Const ("HOL.Trueprop", "bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
179 : (string * term) option
181 > val t = (Thm.term_of o the o (parse thy))
182 "matches (a * b \<up> #2 = c) (#3 * x \<up> #2222 = #1)";
183 > eval_matches "/thmid/" "/op_/" t thy;
184 SOME ("matches (a * b \<up> #2 = c) (#3 * x \<up> #2222 = #1) = False",
185 Const ("HOL.Trueprop", "bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
187 > val t = (Thm.term_of o the o (parse thy))
188 "matches (a = b) (x + #1 + #-1 * #2 = #0)";
189 > eval_matches "/thmid/" "/op_/" t thy;
190 SOME ("matches (a = b) (x + #1 + #-1 * #2 = #0) = True",Const # $ (# $ #))
193 (*.does a pattern match some subterm ?.*)
194 fun matchsub thy t pat =
196 fun matchs (t as Const _) = TermC.matches thy t pat
197 | matchs (t as Free _) = TermC.matches thy t pat
198 | matchs (t as Var _) = TermC.matches thy t pat
199 | matchs (Bound _) = false
200 | matchs (t as Abs (_, _, body)) =
201 if TermC.matches thy t pat then true else TermC.matches thy body pat
202 | matchs (t as f1 $ f2) =
203 if TermC.matches thy t pat then true
204 else if matchs f1 then true else matchs f2
207 (*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*)
208 fun eval_matchsub (_:string) "Prog_Expr.matchsub"
209 (t as Const (\<^const_name>\<open>Prog_Expr.matchsub\<close>, _) $ pat $ tst) thy =
210 if matchsub thy tst pat
212 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
213 in SOME (UnparseC.term_in_thy thy prop, prop) end
215 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
216 in SOME (UnparseC.term_in_thy thy prop, prop) end
217 | eval_matchsub _ _ _ _ = NONE;
219 (*get the variables in an isabelle-term*)
220 (*("Vars" ,("Prog_Expr.Vars" , eval_var "#Vars_")):calc*)
221 fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) thy =
223 val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t;
224 val thmId = thmid ^ UnparseC.term_in_thy thy arg;
225 in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end
226 | eval_var _ _ _ _ = NONE;
228 (* refer to Thm.lhs_of *)
229 fun lhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _) = l
230 | lhs t = raise ERROR("lhs called with (" ^ UnparseC.term t ^ ")");
231 (*("lhs" ,("Prog_Expr.lhs" , eval_lhs "")):calc*)
232 fun eval_lhs _ "Prog_Expr.lhs" (t as (Const (\<^const_name>\<open>lhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _))) _ =
233 SOME ((UnparseC.term t) ^ " = " ^ (UnparseC.term l),
234 HOLogic.Trueprop $ (TermC.mk_equality (t, l)))
235 | eval_lhs _ _ _ _ = NONE;
237 > val t = (Thm.term_of o the o (parse thy)) "lhs (1 * x \<up> 2 = 0)";
238 > val SOME (id,t') = eval_lhs 0 0 t 0;
239 val id = "Prog_Expr.lhs (1 * x \<up> 2 = 0) = 1 * x \<up> 2" : string
241 val it = "Prog_Expr.lhs (1 * x \<up> 2 = 0) = 1 * x \<up> 2" : string
244 fun rhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r) = r
245 | rhs t = raise ERROR("rhs called with (" ^ UnparseC.term t ^ ")");
246 (*("rhs" ,("Prog_Expr.rhs" , eval_rhs "")):calc*)
247 fun eval_rhs _ "Prog_Expr.rhs" (t as (Const (\<^const_name>\<open>rhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r))) _ =
248 SOME (UnparseC.term t ^ " = " ^ UnparseC.term r,
249 HOLogic.Trueprop $ (TermC.mk_equality (t, r)))
250 | eval_rhs _ _ _ _ = NONE;
251 (*\\------------------------- from Prog_Expr.thy-------------------------------------------------//*)
253 (*//------------------------- from Atools.thy------------------------------------------------\\*)
254 fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
256 (*("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""))*)
257 fun eval_occurs_in _ "Prog_Expr.occurs_in" (p as (Const (\<^const_name>\<open>occurs_in\<close>, _) $ v $ t)) _ =
258 ((*tracing("#>@ eval_occurs_in: v= "^(UnparseC.term v));
259 tracing("#>@ eval_occurs_in: t= "^(UnparseC.term t));*)
261 then SOME ((UnparseC.term p) ^ " = True",
262 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
263 else SOME ((UnparseC.term p) ^ " = False",
264 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))))
265 | eval_occurs_in _ _ _ _ = NONE;
267 (*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)
268 fun some_occur_in vs t =
269 let fun occurs_in' a b = occurs_in b a
270 in foldl or_ (false, map (occurs_in' t) vs) end;
272 (*("some_occur_in", ("Prog_Expr.some_occur_in",
273 eval_some_occur_in "#eval_some_occur_in_"))*)
274 fun eval_some_occur_in _ "Prog_Expr.some_occur_in"
275 (p as (Const (\<^const_name>\<open>some_occur_in\<close>,_) $ vs $ t)) _ =
276 if some_occur_in (TermC.isalist2list vs) t
277 then SOME ((UnparseC.term p) ^ " = True",
278 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
279 else SOME ((UnparseC.term p) ^ " = False",
280 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
281 | eval_some_occur_in _ _ _ _ = NONE;
283 (*("is_atom",("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"))*)
284 fun eval_is_atom (thmid:string) "Prog_Expr.is_atom" (t as (Const _ $ arg)) _ =
286 then SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "",
287 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
288 else SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "",
289 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
290 | eval_is_atom _ _ _ _ = NONE;
292 (*("is_num",("Prog_Expr.is_num", Prog_Expr.eval_is_num "#is_num_"))*)
293 fun eval_is_num (thmid:string) "Prog_Expr.is_num" (t as (Const _ $ arg)) _ =
295 then SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "",
296 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
297 else SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "",
298 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
299 | eval_is_num _ _ _ _ = NONE;
301 fun even i = (i div 2) * 2 = i;
302 (*("is_even",("Prog_Expr.is_even", eval_is_even "#is_even_"))*)
303 fun eval_is_even (thmid:string) "Prog_Expr.is_even" (t as (Const _ $ arg)) _ =
307 val i = arg |> HOLogic.dest_number |> snd
310 then SOME (TermC.mk_thmid thmid (string_of_int i) "",
311 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
312 else SOME (TermC.mk_thmid thmid "" "",
313 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
316 | eval_is_even _ _ _ _ = NONE;
318 (*("is_const",("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"))*)
319 fun eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ Const ("Partial_Fractions.AA", _))) _ =
320 (*TODO get rid of this special case*)
321 SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
322 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
323 | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ Const _)) _ =
324 SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
325 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
326 | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ n)) _ =
328 then SOME (TermC.mk_thmid thmid (TermC.string_of_num n) "",
329 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
330 else SOME (TermC.mk_thmid thmid (UnparseC.term n) "",
331 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
332 | eval_const _ _ _ _ = NONE;
334 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
335 (*("PLUS" ,(\<^const_name>\<open>plus\<close> , (**)eval_binop "#add_")),
336 ("TIMES" ,(\<^const_name>\<open>times\<close> , (**)eval_binop "#mult_")),
337 ("POWER" ,(\<^const_name>\<open>powr\<close> , (**)eval_binop "#power_"))*)
339 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
340 ("xxxxxx",op_,t,thy);
342 fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) = (* dropped *)
344 (string_of_int v11)^", "^(string_of_int v12)^"), ("^
345 (string_of_int p11)^", "^(string_of_int p12)^")) __ (("^
346 (string_of_int v21)^", "^(string_of_int v22)^"), ("^
347 (string_of_int p21)^", "^(string_of_int p22)^"))";
349 (*.evaluate < and <= for numerals.*)
350 (*("le" ,(\<^const_name>\<open>less\<close> , Prog_Expr.eval_equ "#less_")),
351 ("leq" ,(\<^const_name>\<open>less_eq\<close> , Prog_Expr.eval_equ "#less_equal_"))*)
353 fun eval_equ (thmid:string) (_(*op_*)) (t as (Const (op0, _)) $ t1 $ t2) _ =
354 if TermC.is_num t1 andalso TermC.is_num t2 then
356 val n1 = t1 |> HOLogic.dest_number |> snd
357 val n2 = t2 |> HOLogic.dest_number |> snd
359 if Eval.calc_equ (strip_thy op0) (n1, n2)
360 then SOME (TermC.mk_thmid thmid (string_of_int n1) (string_of_int n2),
361 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
362 else SOME (TermC.mk_thmid thmid (string_of_int n1) (string_of_int n2),
363 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
366 | eval_equ _ _ _ _ = NONE;
371 val it = "(?t = ?t) = True"
372 > val t = str2term "x = 0";
373 > val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
375 > val t = str2term "1 = 0";
376 > val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
377 ----------- thus needs Rule.Eval !
378 > val t = str2term "0 = 0";
379 > val SOME (t',_) = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
381 val it = \<^const_name>\<open>True\<close>
383 val t = str2term "Not (x = 0)";
384 atomt t; UnparseC.term t;
390 val it = "x ~= 0" : string*)
392 (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of
393 the arguments: thus special handling by 'fun eval_binop'*)
394 (*("ident" ,("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")):calc*)
395 fun eval_ident (thmid:string) "Prog_Expr.ident" (t as
396 (Const _(*op0, t0*) $ t1 $ t2 )) thy =
398 then SOME (TermC.mk_thmid thmid
399 ("(" ^ (UnparseC.term_in_thy thy t1) ^ ")")
400 ("(" ^ (UnparseC.term_in_thy thy t2) ^ ")"),
401 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
402 else SOME (TermC.mk_thmid thmid
403 ("(" ^ (UnparseC.term_in_thy thy t1) ^ ")")
404 ("(" ^ (UnparseC.term_in_thy thy t2) ^ ")"),
405 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
406 | eval_ident _ _ _ _ = NONE;
408 > val t = str2term "x =!= 0";
409 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
411 val str = "ident_(x)_(0)" : string
412 val it = "(x =!= 0) = False" : string
413 > val t = str2term "1 =!= 0";
414 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
416 val str = "ident_(1)_(0)" : string
417 val it = "(1 =!= 0) = False" : string
418 > val t = str2term "0 =!= 0";
419 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
421 val str = "ident_(0)_(0)" : string
422 val it = "(0 =!= 0) = True" : string
426 (* evaluate identity of terms, which stay ready for further evaluation;
427 thus returns False only for atoms *)
428 (*("equal" ,(\<^const_name>\<open>HOL.eq\<close>, Prog_Expr.eval_equal "#equal_")):calc*)
429 fun eval_equal (thmid : string) \<^const_name>\<open>HOL.eq\<close> (t as (Const _(*op0,t0*) $ t1 $ t2 )) thy =
432 SOME (TermC.mk_thmid thmid
433 ("(" ^ UnparseC.term_in_thy thy t1 ^ ")") ("(" ^ UnparseC.term_in_thy thy t2 ^ ")"),
434 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
436 (case (TermC.is_atom t1, TermC.is_atom t2) of
438 if TermC.variable_constant_pair (t1, t2)
440 else SOME (TermC.mk_thmid thmid
441 ("(" ^ UnparseC.term_in_thy thy t1 ^ ")") ("(" ^ UnparseC.term_in_thy thy t2 ^ ")"),
442 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
443 | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
444 | eval_equal _ _ _ _ = NONE; (* error-exit *)
446 (*. evaluate HOL.divide .*)
447 (*("DIVIDE" ,("Rings.divide_class.divide" , eval_cancel "#divide_e"))*)
448 fun eval_cancel thmid "Rings.divide_class.divide" (t as (Const _ $ t1 $ t2)) _ =
449 if TermC.is_num t1 andalso TermC.is_num t2 then
451 val (T, _) = HOLogic.dest_number t1;
452 val (i1, i2) = (Eval.int_of_numeral t1, Eval.int_of_numeral t2);
453 val res_int as (_, (i1', i2')) = Eval.cancel_int (i1, i2);
455 if (i1', i2') = (i1, i2) then NONE
458 val res = TermC.mk_frac T res_int;
459 val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
460 in SOME (TermC.mk_thmid thmid (string_of_int i1) (string_of_int i2), prop) end
463 | eval_cancel _ _ _ _ = NONE;
465 (* get the argument from a function-definition *)
466 (*("argument_in" ,("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in"))*)
467 fun eval_argument_in _ "Prog_Expr.argument_in"
468 (t as (Const ("Prog_Expr.argument_in", _) $ (_(*f*) $ arg))) _ =
469 if is_Free arg (*could be something to be simplified before*)
471 SOME (UnparseC.term t ^ " = " ^ UnparseC.term arg,
472 HOLogic.Trueprop $ (TermC.mk_equality (t, arg)))
474 | eval_argument_in _ _ _ _ = NONE;
476 (* check if the function-identifier of the first argument matches
477 the function-identifier of the lhs of the second argument *)
478 (*("sameFunId" ,("Prog_Expr.sameFunId", eval_same_funid "Prog_Expr.sameFunId"))*)
479 fun eval_sameFunId _ "Prog_Expr.sameFunId"
480 (p as Const ("Prog_Expr.sameFunId",_) $ (f1 $ _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _)) _ =
482 then SOME ((UnparseC.term p) ^ " = True",
483 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
484 else SOME ((UnparseC.term p) ^ " = False",
485 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
486 | eval_sameFunId _ _ _ _ = NONE;
489 (*.from a list of fun-definitions "f x = ..." as 2nd argument
490 filter the elements with the same fun-identfier in "f y"
492 this is, because Isabelles filter takes more than 1 sec.*)
493 fun same_funid f1 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _) = f1 = f2
494 | same_funid f1 t = raise ERROR ("same_funid called with t = ("
495 ^ UnparseC.term f1 ^ ") (" ^ UnparseC.term t ^ ")");
496 (*("filter_sameFunId" ,("Prog_Expr.filter_sameFunId",
497 eval_filter_sameFunId "Prog_Expr.filter_sameFunId"))*)
498 fun eval_filter_sameFunId _ "Prog_Expr.filter_sameFunId"
499 (p as Const ("Prog_Expr.filter_sameFunId",_) $
501 let val fs' = ((TermC.list2isalist HOLogic.boolT) o
502 (filter (same_funid fid))) (TermC.isalist2list fs)
503 in SOME (UnparseC.term (TermC.mk_equality (p, fs')),
504 HOLogic.Trueprop $ (TermC.mk_equality (p, fs'))) end
505 | eval_filter_sameFunId _ _ _ _ = NONE;
507 (* make a list of terms to a sum *)
508 fun list2sum [] = raise ERROR ("list2sum called with []")
512 fun sum su [s'] = Const (\<^const_name>\<open>plus\<close>,
513 [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s'
514 | sum su (s'::ss') = sum (Const (\<^const_name>\<open>plus\<close>,
515 [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s') ss'
516 | sum _ _ = raise ERROR "list2sum: pattern in fun.def is missing"
519 (* make a list of equalities to the sum of the lhs *)
520 (*("boollist2sum" ,("Prog_Expr.boollist2sum" , eval_boollist2sum "")):calc*)
521 fun eval_boollist2sum _ "Prog_Expr.boollist2sum"
522 (p as Const ("Prog_Expr.boollist2sum", _) $ (l as Const (\<^const_name>\<open>Cons\<close>, _) $ _ $ _)) _ =
524 val isal = TermC.isalist2list l
525 val lhss = map lhs isal
526 val sum = list2sum lhss
528 SOME ((UnparseC.term p) ^ " = " ^ (UnparseC.term sum),
529 HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))
531 | eval_boollist2sum _ _ _ _ = NONE;
534 \<close> text \<open>
540 subsection \<open>extend rule-set for evaluating pre-conditions and program-expressions\<close>
542 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [\<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs "")];
547 subsection \<open>setup for rule-sets and ML-functions\<close>
549 rule_set_knowledge prog_expr = prog_expr
551 calculation matches = \<open>Prog_Expr.eval_matches "#matches_"\<close>
552 calculation matchsub = \<open>Prog_Expr.eval_matchsub "#matchsub_"\<close>
553 calculation Vars = \<open>Prog_Expr.eval_var "#Vars_"\<close>
554 calculation lhs = \<open>Prog_Expr.eval_lhs ""\<close>
555 calculation rhs = \<open>Prog_Expr.eval_rhs ""\<close>
556 (*\\------------------------- from Tools .thy-------------------------------------------------//*)