1 (* auxiliary functions used in scripts |
|
2 author: Walther Neuper 000301 |
|
3 WN0509 shift into Atools ?!? (because used also in where of models !) |
|
4 |
|
5 (c) copyright due to lincense terms. |
|
6 |
|
7 remove_thy"Tools"; |
|
8 use_thy"Scripts/Tools"; |
|
9 *) |
|
10 |
|
11 theory Tools imports ListG begin |
|
12 |
|
13 (*belongs to theory ListG*) |
|
14 ML {* |
|
15 val first_isac_thy = @{theory ListG} |
|
16 *} |
|
17 |
|
18 (*for Descript.thy*) |
|
19 |
|
20 (***********************************************************************) |
|
21 (* 'fun is_dsc' in Scripts/scrtools.smlMUST contain ALL these types !!!*) |
|
22 (***********************************************************************) |
|
23 typedecl nam (* named variables *) |
|
24 typedecl una (* unnamed variables *) |
|
25 typedecl unl (* unnamed variables of type list, elementwise input prohibited*) |
|
26 typedecl str (* structured variables *) |
|
27 typedecl toreal (* var with undef real value: forces typing *) |
|
28 typedecl toreall (* var with undef real list value: forces typing *) |
|
29 typedecl tobooll (* var with undef bool list value: forces typing *) |
|
30 typedecl unknow (* input without dsc in fmz=[] *) |
|
31 typedecl cpy (* UNUSED: copy-named variables |
|
32 identified by .._0, .._i .._' in pbt *) |
|
33 (***********************************************************************) |
|
34 (* 'fun is_dsc' in Scripts/scrtools.smlMUST contain ALL these types !!!*) |
|
35 (***********************************************************************) |
|
36 |
|
37 consts |
|
38 |
|
39 UniversalList :: "bool list" |
|
40 |
|
41 lhs :: "bool => real" (*of an equality*) |
|
42 rhs :: "bool => real" (*of an equality*) |
|
43 Vars :: "'a => real list" (*get the variables of a term *) |
|
44 matches :: "['a, 'a] => bool" |
|
45 matchsub :: "['a, 'a] => bool" |
|
46 |
|
47 constdefs |
|
48 |
|
49 Testvar :: "[real, 'a] => bool" (*is a variable in a term: unused 6.5.03*) |
|
50 "Testvar v t == v mem (Vars t)" (*by rewriting only,no Calcunused 6.5.03*) |
|
51 |
|
52 ML {* (*the former Tools.ML*) |
|
53 (* auxiliary functions for scripts WN.9.00*) |
|
54 (*11.02: for equation solving only*) |
|
55 val UniversalList = (term_of o the o (parse @{theory})) "UniversalList"; |
|
56 val EmptyList = (term_of o the o (parse @{theory})) "[]::bool list"; |
|
57 |
|
58 (*+ for Or_to_List +*) |
|
59 fun or2list (Const ("True",_)) = (writeln"### or2list True";UniversalList) |
|
60 | or2list (Const ("False",_)) = (writeln"### or2list False";EmptyList) |
|
61 | or2list (t as Const ("op =",_) $ _ $ _) = |
|
62 (writeln"### or2list _ = _";list2isalist bool [t]) |
|
63 | or2list ors = |
|
64 (writeln"### or2list _ | _"; |
|
65 let fun get ls (Const ("op |",_) $ o1 $ o2) = |
|
66 case o2 of |
|
67 Const ("op |",_) $ _ $ _ => get (ls @ [o1]) o2 |
|
68 | _ => ls @ [o1, o2] |
|
69 in (((list2isalist bool) o (get [])) ors) |
|
70 handle _ => raise error ("or2list: no ORs= "^(term2str ors)) end |
|
71 ); |
|
72 (*>val t = HOLogic.true_const; |
|
73 > val t' = or2list t; |
|
74 > term2str t'; |
|
75 "Atools.UniversalList" |
|
76 > val t = HOLogic.false_const; |
|
77 > val t' = or2list t; |
|
78 > term2str t'; |
|
79 "[]" |
|
80 > val t=(term_of o the o (parse thy)) "x=3"; |
|
81 > val t' = or2list t; |
|
82 > term2str t'; |
|
83 "[x = 3]" |
|
84 > val t=(term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)"; |
|
85 > val t' = or2list t; |
|
86 > term2str t'; |
|
87 "[x = #3, x = #-3, x = #0]" : string *) |
|
88 |
|
89 |
|
90 (** evaluation on the meta-level **) |
|
91 |
|
92 (*. evaluate the predicate matches (match on whole term only) .*) |
|
93 (*("matches",("Tools.matches",eval_matches "#matches_")):calc*) |
|
94 fun eval_matches (thmid:string) "Tools.matches" |
|
95 (t as Const ("Tools.matches",_) $ pat $ tst) thy = |
|
96 if matches thy tst pat |
|
97 then let val prop = Trueprop $ (mk_equality (t, true_as_term)) |
|
98 in SOME (Syntax.string_of_term @{context} prop, prop) end |
|
99 else let val prop = Trueprop $ (mk_equality (t, false_as_term)) |
|
100 in SOME (Syntax.string_of_term @{context} prop, prop) end |
|
101 | eval_matches _ _ _ _ = NONE; |
|
102 (* |
|
103 > val t = (term_of o the o (parse thy)) |
|
104 "matches (?x = 0) (1 * x ^^^ 2 = 0)"; |
|
105 > eval_matches "/thmid/" "/op_/" t thy; |
|
106 val it = |
|
107 SOME |
|
108 ("matches (x = 0) (1 * x ^^^ 2 = 0) = False", |
|
109 Const (#,#) $ (# $ # $ Const #)) : (string * term) option |
|
110 |
|
111 > val t = (term_of o the o (parse thy)) |
|
112 "matches (?a = #0) (#1 * x ^^^ #2 = #0)"; |
|
113 > eval_matches "/thmid/" "/op_/" t thy; |
|
114 val it = |
|
115 SOME |
|
116 ("matches (?a = #0) (#1 * x ^^^ #2 = #0) = True", |
|
117 Const (#,#) $ (# $ # $ Const #)) : (string * term) option |
|
118 |
|
119 > val t = (term_of o the o (parse thy)) |
|
120 "matches (?a * x = #0) (#1 * x ^^^ #2 = #0)"; |
|
121 > eval_matches "/thmid/" "/op_/" t thy; |
|
122 val it = |
|
123 SOME |
|
124 ("matches (?a * x = #0) (#1 * x ^^^ #2 = #0) = False", |
|
125 Const (#,#) $ (# $ # $ Const #)) : (string * term) option |
|
126 |
|
127 > val t = (term_of o the o (parse thy)) |
|
128 "matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0)"; |
|
129 > eval_matches "/thmid/" "/op_/" t thy; |
|
130 val it = |
|
131 SOME |
|
132 ("matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0) = True", |
|
133 Const (#,#) $ (# $ # $ Const #)) : (string * term) option |
|
134 ----- before ?patterns ---: |
|
135 > val t = (term_of o the o (parse thy)) |
|
136 "matches (a * b^^^#2 = c) (#3 * x^^^#2 = #1)"; |
|
137 > eval_matches "/thmid/" "/op_/" t thy; |
|
138 SOME |
|
139 ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2 = #1) = True", |
|
140 Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#))) |
|
141 : (string * term) option |
|
142 |
|
143 > val t = (term_of o the o (parse thy)) |
|
144 "matches (a * b^^^#2 = c) (#3 * x^^^#2222 = #1)"; |
|
145 > eval_matches "/thmid/" "/op_/" t thy; |
|
146 SOME ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2222 = #1) = False", |
|
147 Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#))) |
|
148 |
|
149 > val t = (term_of o the o (parse thy)) |
|
150 "matches (a = b) (x + #1 + #-1 * #2 = #0)"; |
|
151 > eval_matches "/thmid/" "/op_/" t thy; |
|
152 SOME ("matches (a = b) (x + #1 + #-1 * #2 = #0) = True",Const # $ (# $ #)) |
|
153 *) |
|
154 |
|
155 (*.does a pattern match some subterm ?.*) |
|
156 fun matchsub thy t pat = |
|
157 let fun matchs (t as Const _) = matches thy t pat |
|
158 | matchs (t as Free _) = matches thy t pat |
|
159 | matchs (t as Var _) = matches thy t pat |
|
160 | matchs (Bound _) = false |
|
161 | matchs (t as Abs (_, _, body)) = |
|
162 if matches thy t pat then true else matches thy body pat |
|
163 | matchs (t as f1 $ f2) = |
|
164 if matches thy t pat then true |
|
165 else if matchs f1 then true else matchs f2 |
|
166 in matchs t end; |
|
167 |
|
168 (*("matchsub",("Tools.matchsub",eval_matchsub "#matchsub_")):calc*) |
|
169 fun eval_matchsub (thmid:string) "Tools.matchsub" |
|
170 (t as Const ("Tools.matchsub",_) $ pat $ tst) thy = |
|
171 if matchsub thy tst pat |
|
172 then let val prop = Trueprop $ (mk_equality (t, true_as_term)) |
|
173 in SOME (Syntax.string_of_term @{context} prop, prop) end |
|
174 else let val prop = Trueprop $ (mk_equality (t, false_as_term)) |
|
175 in SOME (Syntax.string_of_term @{context} prop, prop) end |
|
176 | eval_matchsub _ _ _ _ = NONE; |
|
177 |
|
178 (*get the variables in an isabelle-term*) |
|
179 (*("Vars" ,("Tools.Vars" ,eval_var "#Vars_")):calc*) |
|
180 fun eval_var (thmid:string) "Tools.Vars" |
|
181 (t as (Const(op0,t0) $ arg)) thy = |
|
182 let |
|
183 val t' = ((list2isalist HOLogic.realT) o vars) t; |
|
184 val thmId = thmid^(Syntax.string_of_term @{context} arg); |
|
185 in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end |
|
186 | eval_var _ _ _ _ = NONE; |
|
187 |
|
188 fun lhs (Const ("op =",_) $ l $ _) = l |
|
189 | lhs t = error("lhs called with (" ^ term2str t ^ ")"); |
|
190 (*("lhs" ,("Tools.lhs" ,eval_lhs "")):calc*) |
|
191 fun eval_lhs _ "Tools.lhs" |
|
192 (t as (Const ("Tools.lhs",_) $ (Const ("op =",_) $ l $ _))) _ = |
|
193 SOME ((term2str t) ^ " = " ^ (term2str l), |
|
194 Trueprop $ (mk_equality (t, l))) |
|
195 | eval_lhs _ _ _ _ = NONE; |
|
196 (* |
|
197 > val t = (term_of o the o (parse thy)) "lhs (1 * x ^^^ 2 = 0)"; |
|
198 > val SOME (id,t') = eval_lhs 0 0 t 0; |
|
199 val id = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string |
|
200 > term2str t'; |
|
201 val it = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string |
|
202 *) |
|
203 |
|
204 fun rhs (Const ("op =",_) $ _ $ r) = r |
|
205 | rhs t = error("rhs called with (" ^ term2str t ^ ")"); |
|
206 (*("rhs" ,("Tools.rhs" ,eval_rhs "")):calc*) |
|
207 fun eval_rhs _ "Tools.rhs" |
|
208 (t as (Const ("Tools.rhs",_) $ (Const ("op =",_) $ _ $ r))) _ = |
|
209 SOME ((term2str t) ^ " = " ^ (term2str r), |
|
210 Trueprop $ (mk_equality (t, r))) |
|
211 | eval_rhs _ _ _ _ = NONE; |
|
212 |
|
213 |
|
214 (*for evaluating scripts*) |
|
215 |
|
216 val list_rls = append_rls "list_rls" list_rls |
|
217 [Calc ("Tools.rhs",eval_rhs "")]; |
|
218 ruleset' := overwritelthy @{theory} (!ruleset', |
|
219 [("list_rls",list_rls) |
|
220 ]); |
|
221 calclist':= overwritel (!calclist', |
|
222 [("matches",("Tools.matches",eval_matches "#matches_")), |
|
223 ("matchsub",("Tools.matchsub",eval_matchsub "#matchsub_")), |
|
224 ("Vars" ,("Tools.Vars" ,eval_var "#Vars_")), |
|
225 ("lhs" ,("Tools.lhs" ,eval_lhs "")), |
|
226 ("rhs" ,("Tools.rhs" ,eval_rhs "")) |
|
227 ]); |
|
228 |
|
229 *} |
|
230 end |
|