walther@59603
|
1 |
(* title: ProgLang/Prog_Expr.thy
|
walther@59603
|
2 |
functions for expressions (which do NOT contain Prog_Tac and Tactical, by definition))
|
walther@59603
|
3 |
author: Walther Neuper, Aug.2019
|
walther@59603
|
4 |
(c) copyright due to lincense terms.
|
walther@59603
|
5 |
*)
|
walther@59603
|
6 |
|
walther@59603
|
7 |
theory Prog_Expr imports Calculate
|
walther@59603
|
8 |
begin
|
walther@59603
|
9 |
|
walther@59603
|
10 |
subsection \<open>General constants\<close>
|
walther@59603
|
11 |
consts
|
walther@59603
|
12 |
(*//------------------------- from Tools .thy-------------------------------------------------\\*)
|
walther@59603
|
13 |
EmptyList :: "bool list"
|
walther@59603
|
14 |
UniversalList :: "bool list"
|
walther@59603
|
15 |
(*\\------------------------- from Tools .thy ------------------------------------------------//*)
|
walther@59603
|
16 |
(*\\------------------------- from Atools .thy -----------------------------------------------//*)
|
walther@59603
|
17 |
Arbfix :: "real"
|
walther@59603
|
18 |
Undef :: "real" (* WN190823 probably an outdated design for DiffApp *)
|
walther@59603
|
19 |
|
walther@59603
|
20 |
pow :: "[real, real] => real" (infixr "^^^" 80)
|
walther@59603
|
21 |
(*\\------------------------- from Atools.thy -----------------------------------------------//*)
|
walther@59603
|
22 |
|
walther@59603
|
23 |
subsection \<open>consts of functions in pre-conditions and program-expressions\<close>
|
walther@59603
|
24 |
(*//------------------------- from Tools .thy-------------------------------------------------\\*)
|
walther@59603
|
25 |
consts
|
walther@59603
|
26 |
lhs :: "bool => real" (*of an equality*)
|
walther@59603
|
27 |
rhs :: "bool => real" (*of an equality*)
|
walther@59603
|
28 |
Vars :: "'a => real list" (*get the variables of a term *)
|
walther@59603
|
29 |
matches :: "['a, 'a] => bool"
|
walther@59603
|
30 |
matchsub :: "['a, 'a] => bool"
|
walther@59603
|
31 |
(*\\------------------------- from Tools .thy-------------------------------------------------//*)
|
walther@59603
|
32 |
some'_occur'_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
|
walther@59603
|
33 |
occurs'_in :: "[real , 'a] => bool" ("_ occurs'_in _")
|
walther@59603
|
34 |
|
walther@59603
|
35 |
abs :: "real => real" ("(|| _ ||)")
|
walther@59603
|
36 |
(* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
|
walther@59603
|
37 |
absset :: "real set => real" ("(||| _ |||)")
|
walther@59603
|
38 |
(*is numeral constant ?*)
|
walther@59603
|
39 |
is'_const :: "real => bool" ("_ is'_const" 10)
|
walther@59603
|
40 |
(*is_const rename to is_num FIXXXME.WN.16.5.03 *)
|
walther@59603
|
41 |
is'_atom :: "real => bool" ("_ is'_atom" 10)
|
walther@59603
|
42 |
is'_even :: "real => bool" ("_ is'_even" 10)
|
walther@59603
|
43 |
|
walther@59603
|
44 |
(* identity on term level*)
|
walther@59603
|
45 |
ident :: "['a, 'a] => bool" ("(_ =!=/ _)" [51, 51] 50)
|
walther@59603
|
46 |
|
walther@59603
|
47 |
argument'_in :: "real => real" ("argument'_in _" 10)
|
walther@59603
|
48 |
sameFunId :: "[real, bool] => bool" (**"same'_funid _ _" 10
|
walther@59603
|
49 |
WN0609 changed the id, because ".. _ _" inhibits currying**)
|
walther@59603
|
50 |
filter'_sameFunId:: "[real, bool list] => bool list"
|
walther@59603
|
51 |
("filter'_sameFunId _ _" 10)
|
walther@59603
|
52 |
boollist2sum :: "bool list => real"
|
walther@59603
|
53 |
lastI :: "'a list \<Rightarrow> 'a"
|
walther@59603
|
54 |
|
walther@59603
|
55 |
subsection \<open>Theorems for rule-sets TODO: find a better location in code\<close>
|
walther@59603
|
56 |
axiomatization where
|
walther@59603
|
57 |
rle_refl: "(n::real) <= n" and
|
walther@59603
|
58 |
not_true: "(~ True) = False" and
|
walther@59603
|
59 |
not_false: "(~ False) = True" and
|
walther@59603
|
60 |
and_true: "(a & True) = a" and
|
walther@59603
|
61 |
and_false: "(a & False) = False" and
|
walther@59603
|
62 |
or_true: "(a | True) = True" and
|
walther@59603
|
63 |
or_false: "(a | False) = a" and
|
walther@59603
|
64 |
and_commute: "(a & b) = (b & a)" and
|
walther@59603
|
65 |
or_commute: "(a | b) = (b | a)"
|
walther@59603
|
66 |
|
walther@59603
|
67 |
subsection \<open>ML code for functions in pre-conditions and program-expressions\<close>
|
walther@59603
|
68 |
ML \<open>
|
walther@59603
|
69 |
signature PROG_EXPR =
|
walther@59603
|
70 |
sig
|
walther@59603
|
71 |
(*//------------------------- from Tools .thy-------------------------------------------------\\*)
|
walther@59603
|
72 |
val EmptyList: term
|
walther@59603
|
73 |
val UniversalList: term
|
walther@59603
|
74 |
|
walther@59603
|
75 |
val lhs: term -> term
|
walther@59603
|
76 |
val eval_lhs: 'a -> string -> term -> 'b -> (string * term) option
|
walther@59603
|
77 |
val eval_matches: string -> string -> term -> theory -> (string * term) option
|
walther@59603
|
78 |
val matchsub: theory -> term -> term -> bool
|
walther@59603
|
79 |
val eval_matchsub: string -> string -> term -> theory -> (string * term) option
|
walther@59603
|
80 |
val rhs: term -> term
|
walther@59603
|
81 |
val eval_rhs: 'a -> string -> term -> 'b -> (string * term) option
|
walther@59603
|
82 |
val eval_var: string -> string -> term -> theory -> (string * term) option
|
walther@59603
|
83 |
|
walther@59603
|
84 |
val or2list: term -> term
|
walther@59603
|
85 |
(*\\------------------------- from Tools .thy-------------------------------------------------//*)
|
walther@59603
|
86 |
(*//------------------------- from Atools .thy------------------------------------------------\\*)
|
walther@59603
|
87 |
val occurs_in: term -> term -> bool
|
walther@59603
|
88 |
val eval_occurs_in: 'a -> string -> term -> 'b -> (string * term) option
|
walther@59603
|
89 |
val some_occur_in: term list -> term -> bool
|
walther@59603
|
90 |
val eval_some_occur_in: 'a -> string -> term -> 'b -> (string * term) option
|
walther@59603
|
91 |
val eval_is_atom: string -> string -> term -> 'a -> (string * term) option
|
walther@59603
|
92 |
val even: int -> bool
|
walther@59603
|
93 |
val eval_is_even: string -> string -> term -> 'a -> (string * term) option
|
walther@59603
|
94 |
val eval_const: string -> string -> term -> 'a -> (string * term) option
|
walther@59603
|
95 |
val eval_equ: string -> string -> term -> 'a -> (string * term) option
|
walther@59603
|
96 |
val eval_ident: string -> string -> term -> theory -> (string * term) option
|
walther@59603
|
97 |
val eval_equal: string -> string -> term -> theory -> (string * term) option
|
walther@59603
|
98 |
val eval_cancel: string -> string -> term -> 'a -> (string * term) option
|
walther@59603
|
99 |
val eval_argument_in: string -> string -> term -> 'a -> (string * term) option
|
walther@59603
|
100 |
val same_funid: term -> term -> bool
|
walther@59603
|
101 |
val eval_sameFunId: string -> string -> term -> 'a -> (string * term) option
|
walther@59603
|
102 |
val eval_filter_sameFunId: string -> string -> term -> 'a -> (string * term) option
|
walther@59603
|
103 |
val list2sum: term list -> term
|
walther@59603
|
104 |
val eval_boollist2sum: string -> string -> term -> 'a -> (string * term) option
|
walther@59603
|
105 |
|
walther@59603
|
106 |
val mk_thmid_f: string -> (int * int) * (int * int) -> (int * int) * (int * int) -> string
|
walther@59603
|
107 |
(*\\------------------------- from Atools.thy------------------------------------------------//*)
|
walther@59603
|
108 |
end
|
walther@59603
|
109 |
|
walther@59603
|
110 |
(**)
|
walther@59603
|
111 |
structure Prog_Expr(**): PROG_EXPR =(**)
|
walther@59603
|
112 |
struct
|
walther@59603
|
113 |
(**)
|
walther@59603
|
114 |
(*//------------------------- from Tools .thy-------------------------------------------------\\*)
|
walther@59603
|
115 |
(* auxiliary functions for scripts WN.9.00*)
|
walther@59603
|
116 |
(*11.02: for equation solving only*)
|
walther@59603
|
117 |
val UniversalList = (Thm.term_of o the o (TermC.parse @{theory})) "UniversalList";
|
walther@59603
|
118 |
val EmptyList = (Thm.term_of o the o (TermC.parse @{theory})) "[]::bool list";
|
walther@59603
|
119 |
|
walther@59603
|
120 |
(*+ for Or_to_List +*)
|
walther@59603
|
121 |
fun or2list (Const ("HOL.True",_)) = (tracing"### or2list True";UniversalList)
|
walther@59603
|
122 |
| or2list (Const ("HOL.False",_)) = (tracing"### or2list False";EmptyList)
|
walther@59618
|
123 |
| or2list (t as Const ("HOL.eq",_) $ _ $ _) = TermC.list2isalist HOLogic.boolT [t]
|
walther@59603
|
124 |
| or2list ors =
|
walther@59618
|
125 |
let
|
walther@59618
|
126 |
fun get ls (Const ("HOL.disj",_) $ o1 $ o2) =
|
walther@59618
|
127 |
(case o2 of
|
walther@59618
|
128 |
Const ("HOL.disj",_) $ _ $ _ => get (ls @ [o1]) o2
|
walther@59618
|
129 |
| _ => ls @ [o1, o2])
|
walther@59618
|
130 |
| get _ t = raise TERM ("or2list: missing pattern in fun.def", [t])
|
walther@59618
|
131 |
in (((TermC.list2isalist HOLogic.boolT) o (get [])) ors) end
|
walther@59603
|
132 |
(*>val t = @{term True};
|
walther@59603
|
133 |
> val t' = or2list t;
|
walther@59603
|
134 |
> term2str t';
|
walther@59603
|
135 |
"Prog_Expr.UniversalList"
|
walther@59603
|
136 |
> val t = @{term False};
|
walther@59603
|
137 |
> val t' = or2list t;
|
walther@59603
|
138 |
> term2str t';
|
walther@59603
|
139 |
"[]"
|
walther@59603
|
140 |
> val t=(Thm.term_of o the o (parse thy)) "x=3";
|
walther@59603
|
141 |
> val t' = or2list t;
|
walther@59603
|
142 |
> term2str t';
|
walther@59603
|
143 |
"[x = 3]"
|
walther@59603
|
144 |
> val t=(Thm.term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";
|
walther@59603
|
145 |
> val t' = or2list t;
|
walther@59603
|
146 |
> term2str t';
|
walther@59603
|
147 |
"[x = #3, x = #-3, x = #0]" : string *)
|
walther@59603
|
148 |
|
walther@59603
|
149 |
|
walther@59603
|
150 |
(** evaluation on the meta-level **)
|
walther@59603
|
151 |
|
walther@59603
|
152 |
(*. evaluate the predicate matches (match on whole term only) .*)
|
walther@59603
|
153 |
(*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*)
|
walther@59618
|
154 |
fun eval_matches (_:string) "Prog_Expr.matches"
|
walther@59603
|
155 |
(t as Const ("Prog_Expr.matches",_) $ pat $ tst) thy =
|
walther@59603
|
156 |
if TermC.matches thy tst pat
|
walther@59603
|
157 |
then
|
walther@59603
|
158 |
let
|
walther@59603
|
159 |
val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
|
walther@59603
|
160 |
in SOME (Rule.term_to_string''' thy prop, prop) end
|
walther@59603
|
161 |
else
|
walther@59603
|
162 |
let
|
walther@59603
|
163 |
val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
|
walther@59603
|
164 |
in SOME (Rule.term_to_string''' thy prop, prop) end
|
walther@59603
|
165 |
| eval_matches _ _ _ _ = NONE;
|
walther@59603
|
166 |
(*
|
walther@59603
|
167 |
> val t = (Thm.term_of o the o (parse thy))
|
walther@59603
|
168 |
"matches (?x = 0) (1 * x ^^^ 2 = 0)";
|
walther@59603
|
169 |
> eval_matches "/thmid/" "/op_/" t thy;
|
walther@59603
|
170 |
val it =
|
walther@59603
|
171 |
SOME
|
walther@59603
|
172 |
("matches (x = 0) (1 * x ^^^ 2 = 0) = False",
|
walther@59603
|
173 |
Const (#,#) $ (# $ # $ Const #)) : (string * term) option
|
walther@59603
|
174 |
|
walther@59603
|
175 |
> val t = (Thm.term_of o the o (parse thy))
|
walther@59603
|
176 |
"matches (?a = #0) (#1 * x ^^^ #2 = #0)";
|
walther@59603
|
177 |
> eval_matches "/thmid/" "/op_/" t thy;
|
walther@59603
|
178 |
val it =
|
walther@59603
|
179 |
SOME
|
walther@59603
|
180 |
("matches (?a = #0) (#1 * x ^^^ #2 = #0) = True",
|
walther@59603
|
181 |
Const (#,#) $ (# $ # $ Const #)) : (string * term) option
|
walther@59603
|
182 |
|
walther@59603
|
183 |
> val t = (Thm.term_of o the o (parse thy))
|
walther@59603
|
184 |
"matches (?a * x = #0) (#1 * x ^^^ #2 = #0)";
|
walther@59603
|
185 |
> eval_matches "/thmid/" "/op_/" t thy;
|
walther@59603
|
186 |
val it =
|
walther@59603
|
187 |
SOME
|
walther@59603
|
188 |
("matches (?a * x = #0) (#1 * x ^^^ #2 = #0) = False",
|
walther@59603
|
189 |
Const (#,#) $ (# $ # $ Const #)) : (string * term) option
|
walther@59603
|
190 |
|
walther@59603
|
191 |
> val t = (Thm.term_of o the o (parse thy))
|
walther@59603
|
192 |
"matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0)";
|
walther@59603
|
193 |
> eval_matches "/thmid/" "/op_/" t thy;
|
walther@59603
|
194 |
val it =
|
walther@59603
|
195 |
SOME
|
walther@59603
|
196 |
("matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0) = True",
|
walther@59603
|
197 |
Const (#,#) $ (# $ # $ Const #)) : (string * term) option
|
walther@59603
|
198 |
----- before ?patterns ---:
|
walther@59603
|
199 |
> val t = (Thm.term_of o the o (parse thy))
|
walther@59603
|
200 |
"matches (a * b^^^#2 = c) (#3 * x^^^#2 = #1)";
|
walther@59603
|
201 |
> eval_matches "/thmid/" "/op_/" t thy;
|
walther@59603
|
202 |
SOME
|
walther@59603
|
203 |
("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2 = #1) = True",
|
walther@59603
|
204 |
Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
|
walther@59603
|
205 |
: (string * term) option
|
walther@59603
|
206 |
|
walther@59603
|
207 |
> val t = (Thm.term_of o the o (parse thy))
|
walther@59603
|
208 |
"matches (a * b^^^#2 = c) (#3 * x^^^#2222 = #1)";
|
walther@59603
|
209 |
> eval_matches "/thmid/" "/op_/" t thy;
|
walther@59603
|
210 |
SOME ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2222 = #1) = False",
|
walther@59603
|
211 |
Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
|
walther@59603
|
212 |
|
walther@59603
|
213 |
> val t = (Thm.term_of o the o (parse thy))
|
walther@59603
|
214 |
"matches (a = b) (x + #1 + #-1 * #2 = #0)";
|
walther@59603
|
215 |
> eval_matches "/thmid/" "/op_/" t thy;
|
walther@59603
|
216 |
SOME ("matches (a = b) (x + #1 + #-1 * #2 = #0) = True",Const # $ (# $ #))
|
walther@59603
|
217 |
*)
|
walther@59603
|
218 |
|
walther@59603
|
219 |
(*.does a pattern match some subterm ?.*)
|
walther@59603
|
220 |
fun matchsub thy t pat =
|
walther@59603
|
221 |
let
|
walther@59603
|
222 |
fun matchs (t as Const _) = TermC.matches thy t pat
|
walther@59603
|
223 |
| matchs (t as Free _) = TermC.matches thy t pat
|
walther@59603
|
224 |
| matchs (t as Var _) = TermC.matches thy t pat
|
walther@59603
|
225 |
| matchs (Bound _) = false
|
walther@59603
|
226 |
| matchs (t as Abs (_, _, body)) =
|
walther@59603
|
227 |
if TermC.matches thy t pat then true else TermC.matches thy body pat
|
walther@59603
|
228 |
| matchs (t as f1 $ f2) =
|
walther@59603
|
229 |
if TermC.matches thy t pat then true
|
walther@59603
|
230 |
else if matchs f1 then true else matchs f2
|
walther@59603
|
231 |
in matchs t end;
|
walther@59603
|
232 |
|
walther@59603
|
233 |
(*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*)
|
walther@59618
|
234 |
fun eval_matchsub (_:string) "Prog_Expr.matchsub"
|
walther@59603
|
235 |
(t as Const ("Prog_Expr.matchsub",_) $ pat $ tst) thy =
|
walther@59603
|
236 |
if matchsub thy tst pat
|
walther@59603
|
237 |
then
|
walther@59603
|
238 |
let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
|
walther@59603
|
239 |
in SOME (Rule.term_to_string''' thy prop, prop) end
|
walther@59603
|
240 |
else
|
walther@59603
|
241 |
let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
|
walther@59603
|
242 |
in SOME (Rule.term_to_string''' thy prop, prop) end
|
walther@59603
|
243 |
| eval_matchsub _ _ _ _ = NONE;
|
walther@59603
|
244 |
|
walther@59603
|
245 |
(*get the variables in an isabelle-term*)
|
walther@59603
|
246 |
(*("Vars" ,("Prog_Expr.Vars" , eval_var "#Vars_")):calc*)
|
walther@59618
|
247 |
fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) thy =
|
walther@59603
|
248 |
let
|
walther@59603
|
249 |
val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t;
|
walther@59603
|
250 |
val thmId = thmid ^ Rule.term_to_string''' thy arg;
|
walther@59603
|
251 |
in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end
|
walther@59603
|
252 |
| eval_var _ _ _ _ = NONE;
|
walther@59603
|
253 |
|
walther@59603
|
254 |
fun lhs (Const ("HOL.eq",_) $ l $ _) = l
|
walther@59603
|
255 |
| lhs t = error("lhs called with (" ^ Rule.term2str t ^ ")");
|
walther@59603
|
256 |
(*("lhs" ,("Prog_Expr.lhs" , eval_lhs "")):calc*)
|
walther@59603
|
257 |
fun eval_lhs _ "Prog_Expr.lhs"
|
walther@59603
|
258 |
(t as (Const ("Prog_Expr.lhs",_) $ (Const ("HOL.eq",_) $ l $ _))) _ =
|
walther@59603
|
259 |
SOME ((Rule.term2str t) ^ " = " ^ (Rule.term2str l),
|
walther@59603
|
260 |
HOLogic.Trueprop $ (TermC.mk_equality (t, l)))
|
walther@59603
|
261 |
| eval_lhs _ _ _ _ = NONE;
|
walther@59603
|
262 |
(*
|
walther@59603
|
263 |
> val t = (Thm.term_of o the o (parse thy)) "lhs (1 * x ^^^ 2 = 0)";
|
walther@59603
|
264 |
> val SOME (id,t') = eval_lhs 0 0 t 0;
|
walther@59603
|
265 |
val id = "Prog_Expr.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
|
walther@59603
|
266 |
> term2str t';
|
walther@59603
|
267 |
val it = "Prog_Expr.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
|
walther@59603
|
268 |
*)
|
walther@59603
|
269 |
|
walther@59603
|
270 |
fun rhs (Const ("HOL.eq",_) $ _ $ r) = r
|
walther@59603
|
271 |
| rhs t = error("rhs called with (" ^ Rule.term2str t ^ ")");
|
walther@59603
|
272 |
(*("rhs" ,("Prog_Expr.rhs" , eval_rhs "")):calc*)
|
walther@59603
|
273 |
fun eval_rhs _ "Prog_Expr.rhs"
|
walther@59603
|
274 |
(t as (Const ("Prog_Expr.rhs",_) $ (Const ("HOL.eq",_) $ _ $ r))) _ =
|
walther@59603
|
275 |
SOME (Rule.term2str t ^ " = " ^ Rule.term2str r,
|
walther@59603
|
276 |
HOLogic.Trueprop $ (TermC.mk_equality (t, r)))
|
walther@59603
|
277 |
| eval_rhs _ _ _ _ = NONE;
|
walther@59603
|
278 |
(*\\------------------------- from Prog_Expr.thy-------------------------------------------------//*)
|
walther@59603
|
279 |
|
walther@59603
|
280 |
(*//------------------------- from Atools.thy------------------------------------------------\\*)
|
walther@59603
|
281 |
fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
|
walther@59603
|
282 |
|
walther@59603
|
283 |
(*("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""))*)
|
walther@59603
|
284 |
fun eval_occurs_in _ "Prog_Expr.occurs'_in"
|
walther@59603
|
285 |
(p as (Const ("Prog_Expr.occurs'_in",_) $ v $ t)) _ =
|
walther@59603
|
286 |
((*tracing("@@@ eval_occurs_in: v= "^(Rule.term2str v));
|
walther@59603
|
287 |
tracing("@@@ eval_occurs_in: t= "^(Rule.term2str t));*)
|
walther@59603
|
288 |
if occurs_in v t
|
walther@59603
|
289 |
then SOME ((Rule.term2str p) ^ " = True",
|
walther@59603
|
290 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
|
walther@59603
|
291 |
else SOME ((Rule.term2str p) ^ " = False",
|
walther@59603
|
292 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))))
|
walther@59603
|
293 |
| eval_occurs_in _ _ _ _ = NONE;
|
walther@59603
|
294 |
|
walther@59603
|
295 |
(*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)
|
walther@59603
|
296 |
fun some_occur_in vs t =
|
walther@59603
|
297 |
let fun occurs_in' a b = occurs_in b a
|
walther@59603
|
298 |
in foldl or_ (false, map (occurs_in' t) vs) end;
|
walther@59603
|
299 |
|
walther@59603
|
300 |
(*("some_occur_in", ("Prog_Expr.some'_occur'_in",
|
walther@59603
|
301 |
eval_some_occur_in "#eval_some_occur_in_"))*)
|
walther@59603
|
302 |
fun eval_some_occur_in _ "Prog_Expr.some'_occur'_in"
|
walther@59603
|
303 |
(p as (Const ("Prog_Expr.some'_occur'_in",_)
|
walther@59603
|
304 |
$ vs $ t)) _ =
|
walther@59603
|
305 |
if some_occur_in (TermC.isalist2list vs) t
|
walther@59603
|
306 |
then SOME ((Rule.term2str p) ^ " = True",
|
walther@59603
|
307 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
|
walther@59603
|
308 |
else SOME ((Rule.term2str p) ^ " = False",
|
walther@59603
|
309 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
|
walther@59603
|
310 |
| eval_some_occur_in _ _ _ _ = NONE;
|
walther@59603
|
311 |
|
walther@59603
|
312 |
(*("is_atom",("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_"))*)
|
walther@59603
|
313 |
fun eval_is_atom (thmid:string) "Prog_Expr.is'_atom"
|
walther@59603
|
314 |
(t as (Const _ $ arg)) _ =
|
walther@59603
|
315 |
(case arg of
|
walther@59603
|
316 |
Free (n,_) => SOME (TermC.mk_thmid thmid n "",
|
walther@59603
|
317 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
|
walther@59603
|
318 |
| _ => SOME (TermC.mk_thmid thmid "" "",
|
walther@59603
|
319 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
|
walther@59603
|
320 |
| eval_is_atom _ _ _ _ = NONE;
|
walther@59603
|
321 |
|
walther@59603
|
322 |
fun even i = (i div 2) * 2 = i;
|
walther@59603
|
323 |
(*("is_even",("Prog_Expr.is'_even", eval_is_even "#is_even_"))*)
|
walther@59603
|
324 |
fun eval_is_even (thmid:string) "Prog_Expr.is'_even"
|
walther@59603
|
325 |
(t as (Const _ $ arg)) _ =
|
walther@59603
|
326 |
(case arg of
|
walther@59603
|
327 |
Free (n,_) =>
|
walther@59603
|
328 |
(case TermC.int_of_str_opt n of
|
walther@59603
|
329 |
SOME i =>
|
walther@59603
|
330 |
if even i then SOME (TermC.mk_thmid thmid n "",
|
walther@59603
|
331 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
|
walther@59603
|
332 |
else SOME (TermC.mk_thmid thmid "" "",
|
walther@59603
|
333 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
|
walther@59603
|
334 |
| _ => NONE)
|
walther@59603
|
335 |
| _ => NONE)
|
walther@59603
|
336 |
| eval_is_even _ _ _ _ = NONE;
|
walther@59603
|
337 |
|
walther@59603
|
338 |
(*evaluate 'is_const'*)
|
walther@59603
|
339 |
(*("is_const",("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"))*)
|
walther@59618
|
340 |
fun eval_const (thmid:string) _ (t as (Const _ $ arg)) _ =
|
walther@59603
|
341 |
(case arg of
|
walther@59618
|
342 |
Const (n1, _) =>
|
walther@59618
|
343 |
SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
|
walther@59618
|
344 |
| Free (n1, _) =>
|
walther@59618
|
345 |
if TermC.is_num' n1
|
walther@59618
|
346 |
then SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
|
walther@59618
|
347 |
else SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
|
walther@59603
|
348 |
| _ => (*NONE*)
|
walther@59618
|
349 |
SOME (TermC.mk_thmid thmid (Rule.term2str arg) "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
|
walther@59603
|
350 |
| eval_const _ _ _ _ = NONE;
|
walther@59603
|
351 |
|
walther@59603
|
352 |
(*. evaluate binary, associative, commutative operators: *,+,^ .*)
|
walther@59603
|
353 |
(*("PLUS" ,("Groups.plus_class.plus" , (**)eval_binop "#add_")),
|
walther@59603
|
354 |
("TIMES" ,("Groups.times_class.times" , (**)eval_binop "#mult_")),
|
walther@59603
|
355 |
("POWER" ,("Prog_Expr.pow" , (**)eval_binop "#power_"))*)
|
walther@59603
|
356 |
|
walther@59603
|
357 |
(* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
|
walther@59603
|
358 |
("xxxxxx",op_,t,thy);
|
walther@59603
|
359 |
*)
|
walther@59603
|
360 |
fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) = (* dropped *)
|
walther@59603
|
361 |
thmid ^ "Float ((" ^
|
walther@59603
|
362 |
(string_of_int v11)^","^(string_of_int v12)^"), ("^
|
walther@59603
|
363 |
(string_of_int p11)^","^(string_of_int p12)^")) __ (("^
|
walther@59603
|
364 |
(string_of_int v21)^","^(string_of_int v22)^"), ("^
|
walther@59603
|
365 |
(string_of_int p21)^","^(string_of_int p22)^"))";
|
walther@59603
|
366 |
|
walther@59603
|
367 |
(*.evaluate < and <= for numerals.*)
|
walther@59603
|
368 |
(*("le" ,("Orderings.ord_class.less" , Prog_Expr.eval_equ "#less_")),
|
walther@59603
|
369 |
("leq" ,("Orderings.ord_class.less_eq" , Prog_Expr.eval_equ "#less_equal_"))*)
|
walther@59603
|
370 |
fun eval_equ (thmid:string) (_(*op_*)) (t as
|
walther@59603
|
371 |
(Const (op0, _) $ Free (n1, _) $ Free(n2, _))) _ =
|
walther@59603
|
372 |
(case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of
|
walther@59603
|
373 |
(SOME n1', SOME n2') =>
|
walther@59603
|
374 |
if Calc.calc_equ (strip_thy op0) (n1', n2')
|
walther@59603
|
375 |
then SOME (TermC.mk_thmid thmid n1 n2,
|
walther@59603
|
376 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
|
walther@59603
|
377 |
else SOME (TermC.mk_thmid thmid n1 n2,
|
walther@59603
|
378 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
|
walther@59603
|
379 |
| _ => NONE)
|
walther@59603
|
380 |
|
walther@59603
|
381 |
| eval_equ _ _ _ _ = NONE;
|
walther@59603
|
382 |
|
walther@59603
|
383 |
|
walther@59603
|
384 |
(*evaluate identity
|
walther@59603
|
385 |
> reflI;
|
walther@59603
|
386 |
val it = "(?t = ?t) = True"
|
walther@59603
|
387 |
> val t = str2term "x = 0";
|
walther@59603
|
388 |
> val NONE = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
|
walther@59603
|
389 |
|
walther@59603
|
390 |
> val t = str2term "1 = 0";
|
walther@59603
|
391 |
> val NONE = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
|
walther@59603
|
392 |
----------- thus needs Rule.Calc !
|
walther@59603
|
393 |
> val t = str2term "0 = 0";
|
walther@59603
|
394 |
> val SOME (t',_) = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
|
walther@59603
|
395 |
> Rule.term2str t';
|
walther@59603
|
396 |
val it = "HOL.True"
|
walther@59603
|
397 |
|
walther@59603
|
398 |
val t = str2term "Not (x = 0)";
|
walther@59603
|
399 |
atomt t; Rule.term2str t;
|
walther@59603
|
400 |
*** -------------
|
walther@59603
|
401 |
*** Const ( Not)
|
walther@59603
|
402 |
*** . Const ( op =)
|
walther@59603
|
403 |
*** . . Free ( x, )
|
walther@59603
|
404 |
*** . . Free ( 0, )
|
walther@59603
|
405 |
val it = "x ~= 0" : string*)
|
walther@59603
|
406 |
|
walther@59603
|
407 |
(*.evaluate identity on the term-level, =!= ,i.e. without evaluation of
|
walther@59603
|
408 |
the arguments: thus special handling by 'fun eval_binop'*)
|
walther@59603
|
409 |
(*("ident" ,("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")):calc*)
|
walther@59603
|
410 |
fun eval_ident (thmid:string) "Prog_Expr.ident" (t as
|
walther@59603
|
411 |
(Const _(*op0, t0*) $ t1 $ t2 )) thy =
|
walther@59603
|
412 |
if t1 = t2
|
walther@59603
|
413 |
then SOME (TermC.mk_thmid thmid
|
walther@59603
|
414 |
("(" ^ (Rule.term_to_string''' thy t1) ^ ")")
|
walther@59603
|
415 |
("(" ^ (Rule.term_to_string''' thy t2) ^ ")"),
|
walther@59603
|
416 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
|
walther@59603
|
417 |
else SOME (TermC.mk_thmid thmid
|
walther@59603
|
418 |
("(" ^ (Rule.term_to_string''' thy t1) ^ ")")
|
walther@59603
|
419 |
("(" ^ (Rule.term_to_string''' thy t2) ^ ")"),
|
walther@59603
|
420 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
|
walther@59603
|
421 |
| eval_ident _ _ _ _ = NONE;
|
walther@59603
|
422 |
(* TODO
|
walther@59603
|
423 |
> val t = str2term "x =!= 0";
|
walther@59603
|
424 |
> val SOME (str, t') = eval_ident "ident_" "b" t thy;
|
walther@59603
|
425 |
> Rule.term2str t';
|
walther@59603
|
426 |
val str = "ident_(x)_(0)" : string
|
walther@59603
|
427 |
val it = "(x =!= 0) = False" : string
|
walther@59603
|
428 |
> val t = str2term "1 =!= 0";
|
walther@59603
|
429 |
> val SOME (str, t') = eval_ident "ident_" "b" t thy;
|
walther@59603
|
430 |
> Rule.term2str t';
|
walther@59603
|
431 |
val str = "ident_(1)_(0)" : string
|
walther@59603
|
432 |
val it = "(1 =!= 0) = False" : string
|
walther@59603
|
433 |
> val t = str2term "0 =!= 0";
|
walther@59603
|
434 |
> val SOME (str, t') = eval_ident "ident_" "b" t thy;
|
walther@59603
|
435 |
> Rule.term2str t';
|
walther@59603
|
436 |
val str = "ident_(0)_(0)" : string
|
walther@59603
|
437 |
val it = "(0 =!= 0) = True" : string
|
walther@59603
|
438 |
*)
|
walther@59603
|
439 |
|
walther@59603
|
440 |
(*.evaluate identity of terms, which stay ready for evaluation in turn;
|
walther@59603
|
441 |
thus returns False only for atoms.*)
|
walther@59603
|
442 |
(*("equal" ,("HOL.eq", Prog_Expr.eval_equal "#equal_")):calc*)
|
walther@59603
|
443 |
fun eval_equal (thmid : string) "HOL.eq" (t as (Const _(*op0,t0*) $ t1 $ t2 )) thy =
|
walther@59603
|
444 |
if t1 = t2
|
walther@59603
|
445 |
then SOME (TermC.mk_thmid thmid
|
walther@59603
|
446 |
("(" ^ Rule.term_to_string''' thy t1 ^ ")")
|
walther@59603
|
447 |
("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
|
walther@59603
|
448 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
|
walther@59603
|
449 |
else (case (TermC.is_atom t1, TermC.is_atom t2) of
|
walther@59603
|
450 |
(true, true) =>
|
walther@59603
|
451 |
SOME (TermC.mk_thmid thmid
|
walther@59603
|
452 |
("(" ^ Rule.term_to_string''' thy t1 ^ ")")
|
walther@59603
|
453 |
("(" ^ Rule.term_to_string''' thy t2 ^ ")"),
|
walther@59603
|
454 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
|
walther@59603
|
455 |
| _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
|
walther@59603
|
456 |
| eval_equal _ _ _ _ = NONE; (* error-exit *)
|
walther@59603
|
457 |
(*
|
walther@59603
|
458 |
val t = str2term "x ~= 0";
|
walther@59603
|
459 |
val NONE = eval_equal "equal_" "b" t thy;
|
walther@59603
|
460 |
|
walther@59603
|
461 |
|
walther@59603
|
462 |
> val t = str2term "(x + 1) = (x + 1)";
|
walther@59603
|
463 |
> val SOME (str, t') = eval_equal "equal_" "b" t thy;
|
walther@59603
|
464 |
> Rule.term2str t';
|
walther@59603
|
465 |
val str = "equal_(x + 1)_(x + 1)" : string
|
walther@59603
|
466 |
val it = "(x + 1 = x + 1) = True" : string
|
walther@59603
|
467 |
> val t = str2term "x = 0";
|
walther@59603
|
468 |
> val NONE = eval_equal "equal_" "b" t thy;
|
walther@59603
|
469 |
|
walther@59603
|
470 |
> val t = str2term "1 = 0";
|
walther@59603
|
471 |
> val SOME (str, t') = eval_equal "equal_" "b" t thy;
|
walther@59603
|
472 |
> Rule.term2str t';
|
walther@59603
|
473 |
val str = "equal_(1)_(0)" : string
|
walther@59603
|
474 |
val it = "(1 = 0) = False" : string
|
walther@59603
|
475 |
> val t = str2term "0 = 0";
|
walther@59603
|
476 |
> val SOME (str, t') = eval_equal "equal_" "b" t thy;
|
walther@59603
|
477 |
> Rule.term2str t';
|
walther@59603
|
478 |
val str = "equal_(0)_(0)" : string
|
walther@59603
|
479 |
val it = "(0 = 0) = True" : string
|
walther@59603
|
480 |
*)
|
walther@59603
|
481 |
|
walther@59603
|
482 |
(*. evaluate HOL.divide .*)
|
walther@59603
|
483 |
(*("DIVIDE" ,("Rings.divide_class.divide" , eval_cancel "#divide_e"))*)
|
walther@59603
|
484 |
fun eval_cancel (thmid: string) "Rings.divide_class.divide" (t as
|
walther@59603
|
485 |
(Const (op0,t0) $ Free (n1, _) $ Free(n2, _))) _ =
|
walther@59603
|
486 |
(case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of
|
walther@59603
|
487 |
(SOME n1', SOME n2') =>
|
walther@59603
|
488 |
let
|
walther@59603
|
489 |
val sg = Calc.sign_mult n1' n2';
|
walther@59603
|
490 |
val (T1,T2,Trange) = TermC.dest_binop_typ t0;
|
walther@59603
|
491 |
val gcd' = Calc.gcd (abs n1') (abs n2');
|
walther@59603
|
492 |
in if gcd' = abs n2'
|
walther@59603
|
493 |
then let val rhs = TermC.term_of_num Trange (sg * (abs n1') div gcd')
|
walther@59603
|
494 |
val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
|
walther@59603
|
495 |
in SOME (TermC.mk_thmid thmid n1 n2, prop) end
|
walther@59603
|
496 |
else if 0 < n2' andalso gcd' = 1 then NONE
|
walther@59603
|
497 |
else let val rhs = TermC.mk_num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
|
walther@59603
|
498 |
((abs n2') div gcd')
|
walther@59603
|
499 |
val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
|
walther@59603
|
500 |
in SOME (TermC.mk_thmid thmid n1 n2, prop) end
|
walther@59603
|
501 |
end
|
walther@59603
|
502 |
| _ => ((*tracing"@@@ eval_cancel NONE";*)NONE))
|
walther@59603
|
503 |
| eval_cancel _ _ _ _ = NONE;
|
walther@59603
|
504 |
|
walther@59603
|
505 |
(* get the argument from a function-definition *)
|
walther@59603
|
506 |
(*("argument_in" ,("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in"))*)
|
walther@59603
|
507 |
fun eval_argument_in _ "Prog_Expr.argument'_in"
|
walther@59603
|
508 |
(t as (Const ("Prog_Expr.argument'_in", _) $ (_(*f*) $ arg))) _ =
|
walther@59603
|
509 |
if is_Free arg (*could be something to be simplified before*)
|
walther@59603
|
510 |
then
|
walther@59603
|
511 |
SOME (Rule.term2str t ^ " = " ^ Rule.term2str arg,
|
walther@59603
|
512 |
HOLogic.Trueprop $ (TermC.mk_equality (t, arg)))
|
walther@59603
|
513 |
else NONE
|
walther@59603
|
514 |
| eval_argument_in _ _ _ _ = NONE;
|
walther@59603
|
515 |
|
walther@59603
|
516 |
(* check if the function-identifier of the first argument matches
|
walther@59603
|
517 |
the function-identifier of the lhs of the second argument *)
|
walther@59603
|
518 |
(*("sameFunId" ,("Prog_Expr.sameFunId", eval_same_funid "Prog_Expr.sameFunId"))*)
|
walther@59603
|
519 |
fun eval_sameFunId _ "Prog_Expr.sameFunId"
|
walther@59603
|
520 |
(p as Const ("Prog_Expr.sameFunId",_) $ (f1 $ _) $ (Const ("HOL.eq", _) $ (f2 $ _) $ _)) _ =
|
walther@59603
|
521 |
if f1 = f2
|
walther@59603
|
522 |
then SOME ((Rule.term2str p) ^ " = True",
|
walther@59603
|
523 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
|
walther@59603
|
524 |
else SOME ((Rule.term2str p) ^ " = False",
|
walther@59603
|
525 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
|
walther@59603
|
526 |
| eval_sameFunId _ _ _ _ = NONE;
|
walther@59603
|
527 |
|
walther@59603
|
528 |
|
walther@59603
|
529 |
(*.from a list of fun-definitions "f x = ..." as 2nd argument
|
walther@59603
|
530 |
filter the elements with the same fun-identfier in "f y"
|
walther@59603
|
531 |
as the fst argument;
|
walther@59603
|
532 |
this is, because Isabelles filter takes more than 1 sec.*)
|
walther@59603
|
533 |
fun same_funid f1 (Const ("HOL.eq", _) $ (f2 $ _) $ _) = f1 = f2
|
walther@59603
|
534 |
| same_funid f1 t = error ("same_funid called with t = ("
|
walther@59603
|
535 |
^Rule.term2str f1^") ("^Rule.term2str t^")");
|
walther@59603
|
536 |
(*("filter_sameFunId" ,("Prog_Expr.filter'_sameFunId",
|
walther@59603
|
537 |
eval_filter_sameFunId "Prog_Expr.filter'_sameFunId"))*)
|
walther@59603
|
538 |
fun eval_filter_sameFunId _ "Prog_Expr.filter'_sameFunId"
|
walther@59603
|
539 |
(p as Const ("Prog_Expr.filter'_sameFunId",_) $
|
walther@59603
|
540 |
(fid $ _) $ fs) _ =
|
walther@59603
|
541 |
let val fs' = ((TermC.list2isalist HOLogic.boolT) o
|
walther@59603
|
542 |
(filter (same_funid fid))) (TermC.isalist2list fs)
|
walther@59603
|
543 |
in SOME (Rule.term2str (TermC.mk_equality (p, fs')),
|
walther@59603
|
544 |
HOLogic.Trueprop $ (TermC.mk_equality (p, fs'))) end
|
walther@59603
|
545 |
| eval_filter_sameFunId _ _ _ _ = NONE;
|
walther@59603
|
546 |
|
walther@59603
|
547 |
(* make a list of terms to a sum *)
|
walther@59603
|
548 |
fun list2sum [] = error ("list2sum called with []")
|
walther@59603
|
549 |
| list2sum [s] = s
|
walther@59603
|
550 |
| list2sum (s::ss) =
|
walther@59603
|
551 |
let
|
walther@59603
|
552 |
fun sum su [s'] = Const ("Groups.plus_class.plus",
|
walther@59603
|
553 |
[HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s'
|
walther@59603
|
554 |
| sum su (s'::ss') = sum (Const ("Groups.plus_class.plus",
|
walther@59603
|
555 |
[HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s') ss'
|
walther@59603
|
556 |
| sum _ _ = raise ERROR "list2sum: pattern in fun.def is missing"
|
walther@59603
|
557 |
in sum s ss end;
|
walther@59603
|
558 |
|
walther@59603
|
559 |
(* make a list of equalities to the sum of the lhs *)
|
walther@59603
|
560 |
(*("boollist2sum" ,("Prog_Expr.boollist2sum" , eval_boollist2sum "")):calc*)
|
walther@59603
|
561 |
fun eval_boollist2sum _ "Prog_Expr.boollist2sum"
|
walther@59603
|
562 |
(p as Const ("Prog_Expr.boollist2sum", _) $ (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
|
walther@59603
|
563 |
let
|
walther@59603
|
564 |
val isal = TermC.isalist2list l
|
walther@59603
|
565 |
val lhss = map lhs isal
|
walther@59603
|
566 |
val sum = list2sum lhss
|
walther@59603
|
567 |
in
|
walther@59603
|
568 |
SOME ((Rule.term2str p) ^ " = " ^ (Rule.term2str sum),
|
walther@59603
|
569 |
HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))
|
walther@59603
|
570 |
end
|
walther@59603
|
571 |
| eval_boollist2sum _ _ _ _ = NONE;
|
walther@59603
|
572 |
|
walther@59603
|
573 |
(**) end (*struct*)
|
walther@59603
|
574 |
\<close> text \<open>
|
walther@59603
|
575 |
open Prog_Expr
|
walther@59603
|
576 |
\<close> ML \<open>
|
walther@59603
|
577 |
|
walther@59603
|
578 |
\<close> ML \<open>
|
walther@59603
|
579 |
\<close> ML \<open>
|
walther@59603
|
580 |
\<close> ML \<open>
|
walther@59603
|
581 |
\<close>
|
walther@59603
|
582 |
|
walther@59603
|
583 |
subsection \<open>extend rule-set for evaluating pre-conditions and program-expressions\<close>
|
walther@59603
|
584 |
ML \<open>
|
walther@59603
|
585 |
val list_rls = Rule.append_rls "list_rls" list_rls [Rule.Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs "")];
|
walther@59603
|
586 |
\<close> ML \<open>
|
walther@59603
|
587 |
\<close> ML \<open>
|
walther@59603
|
588 |
\<close>
|
walther@59603
|
589 |
|
walther@59603
|
590 |
subsection \<open>setup for rule-sets and ML-functions\<close>
|
walther@59603
|
591 |
setup \<open>KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))]\<close>
|
walther@59603
|
592 |
setup \<open>KEStore_Elems.add_calcs
|
walther@59603
|
593 |
[("matches", ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")),
|
walther@59603
|
594 |
("matchsub", ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub "#matchsub_")),
|
walther@59603
|
595 |
("Vars", ("Prog_Expr.Vars", Prog_Expr.eval_var "#Vars_")),
|
walther@59603
|
596 |
("lhs", ("Prog_Expr.lhs", Prog_Expr.eval_lhs "")),
|
walther@59603
|
597 |
("rhs", ("Prog_Expr.rhs", Prog_Expr.eval_rhs ""))]\<close>
|
walther@59603
|
598 |
(*\\------------------------- from Tools .thy-------------------------------------------------//*)
|
walther@59603
|
599 |
ML \<open>
|
walther@59603
|
600 |
\<close> ML \<open>
|
walther@59603
|
601 |
\<close> ML \<open>
|
walther@59603
|
602 |
\<close>
|
walther@59603
|
603 |
|
walther@59603
|
604 |
end |