1 (* auxiliary functions used in scripts
2 author: Walther Neuper 000301
3 WN0509 shift into Atools ?!? (because used also in where of models !)
5 (c) copyright due to lincense terms.
8 use_thy"ProgLang/Tools";
11 theory Tools imports ListC begin
13 (*belongs to theory ListC*)
15 val first_isac_thy = @{theory ListC}
20 (***********************************************************************)
21 (* 'fun is_dsc' in ProgLang/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 ProgLang/scrtools.smlMUST contain ALL these types !!*)
35 (***********************************************************************)
39 UniversalList :: "bool list"
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"
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*)
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";
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])
64 (writeln"### or2list _ | _";
65 let fun get ls (Const ("op |",_) $ o1 $ o2) =
67 Const ("op |",_) $ _ $ _ => get (ls @ [o1]) o2
69 in (((list2isalist bool) o (get [])) ors)
70 handle _ => raise error ("or2list: no ORs= "^(term2str ors)) end
72 (*>val t = HOLogic.true_const;
75 "Atools.UniversalList"
76 > val t = HOLogic.false_const;
80 > val t=(term_of o the o (parse thy)) "x=3";
84 > val t=(term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";
87 "[x = #3, x = #-3, x = #0]" : string *)
90 (** evaluation on the meta-level **)
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;
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;
108 ("matches (x = 0) (1 * x ^^^ 2 = 0) = False",
109 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
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;
116 ("matches (?a = #0) (#1 * x ^^^ #2 = #0) = True",
117 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
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;
124 ("matches (?a * x = #0) (#1 * x ^^^ #2 = #0) = False",
125 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
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;
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;
139 ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2 = #1) = True",
140 Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
141 : (string * term) option
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 (#,#)))
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 # $ (# $ #))
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
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;
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 =
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;
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;
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
201 val it = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
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;
214 (*for evaluating scripts*)
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)
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 ""))