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 theory Tools imports ListC begin
10 (*belongs to theory ListC*)
12 val first_isac_thy = @{theory ListC}
17 (***********************************************************************)
18 (* 'fun is_dsc' in ProgLang/scrtools.smlMUST contain ALL these types !!*)
19 (***********************************************************************)
20 typedecl nam (* named variables *)
21 typedecl una (* unnamed variables *)
22 typedecl unl (* unnamed variables of type list, elementwise input prohibited*)
23 typedecl str (* structured variables *)
24 typedecl toreal (* var with undef real value: forces typing *)
25 typedecl toreall (* var with undef real list value: forces typing *)
26 typedecl tobooll (* var with undef bool list value: forces typing *)
27 typedecl unknow (* input without dsc in fmz=[] *)
28 typedecl cpy (* UNUSED: copy-named variables
29 identified by .._0, .._i .._' in pbt *)
30 (***********************************************************************)
31 (* 'fun is_dsc' in ProgLang/scrtools.smlMUST contain ALL these types !!*)
32 (***********************************************************************)
36 UniversalList :: "bool list"
38 lhs :: "bool => real" (*of an equality*)
39 rhs :: "bool => real" (*of an equality*)
40 Vars :: "'a => real list" (*get the variables of a term *)
41 matches :: "['a, 'a] => bool"
42 matchsub :: "['a, 'a] => bool"
47 Testvar :: "[real, 'a] => bool" (*is a variable in a term: unused 6.5.03*)
48 "Testvar v t == v mem (Vars t)" (*by rewriting only,no Calcunused 6.5.03*)
51 ML {* (*the former Tools.ML*)
52 (* auxiliary functions for scripts WN.9.00*)
53 (*11.02: for equation solving only*)
54 val UniversalList = (Thm.term_of o the o (TermC.parse @{theory})) "UniversalList";
55 val EmptyList = (Thm.term_of o the o (TermC.parse @{theory})) "[]::bool list";
57 (*+ for Or_to_List +*)
58 fun or2list (Const ("HOL.True",_)) = (tracing"### or2list True";UniversalList)
59 | or2list (Const ("HOL.False",_)) = (tracing"### or2list False";EmptyList)
60 | or2list (t as Const ("HOL.eq",_) $ _ $ _) =
61 (tracing"### or2list _ = _"; TermC.list2isalist HOLogic.boolT [t])
63 (tracing"### or2list _ | _";
64 let fun get ls (Const ("HOL.disj",_) $ o1 $ o2) =
66 Const ("HOL.disj",_) $ _ $ _ => get (ls @ [o1]) o2
68 in (((TermC.list2isalist HOLogic.boolT) o (get [])) ors)
69 handle _ => error ("or2list: no ORs= "^(term2str ors)) end
71 (*>val t = @{term True};
74 "Atools.UniversalList"
75 > val t = @{term False};
79 > val t=(Thm.term_of o the o (parse thy)) "x=3";
83 > val t=(Thm.term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";
86 "[x = #3, x = #-3, x = #0]" : string *)
89 (** evaluation on the meta-level **)
91 (*. evaluate the predicate matches (match on whole term only) .*)
92 (*("matches",("Tools.matches",eval_matches "#matches_")):calc*)
93 fun eval_matches (thmid:string) "Tools.matches"
94 (t as Const ("Tools.matches",_) $ pat $ tst) thy =
95 if TermC.matches thy tst pat
98 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
99 in SOME (term_to_string''' thy prop, prop) end
102 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
103 in SOME (term_to_string''' thy prop, prop) end
104 | eval_matches _ _ _ _ = NONE;
106 > val t = (Thm.term_of o the o (parse thy))
107 "matches (?x = 0) (1 * x ^^^ 2 = 0)";
108 > eval_matches "/thmid/" "/op_/" t thy;
111 ("matches (x = 0) (1 * x ^^^ 2 = 0) = False",
112 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
114 > val t = (Thm.term_of o the o (parse thy))
115 "matches (?a = #0) (#1 * x ^^^ #2 = #0)";
116 > eval_matches "/thmid/" "/op_/" t thy;
119 ("matches (?a = #0) (#1 * x ^^^ #2 = #0) = True",
120 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
122 > val t = (Thm.term_of o the o (parse thy))
123 "matches (?a * x = #0) (#1 * x ^^^ #2 = #0)";
124 > eval_matches "/thmid/" "/op_/" t thy;
127 ("matches (?a * x = #0) (#1 * x ^^^ #2 = #0) = False",
128 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
130 > val t = (Thm.term_of o the o (parse thy))
131 "matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0)";
132 > eval_matches "/thmid/" "/op_/" t thy;
135 ("matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0) = True",
136 Const (#,#) $ (# $ # $ Const #)) : (string * term) option
137 ----- before ?patterns ---:
138 > val t = (Thm.term_of o the o (parse thy))
139 "matches (a * b^^^#2 = c) (#3 * x^^^#2 = #1)";
140 > eval_matches "/thmid/" "/op_/" t thy;
142 ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2 = #1) = True",
143 Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
144 : (string * term) option
146 > val t = (Thm.term_of o the o (parse thy))
147 "matches (a * b^^^#2 = c) (#3 * x^^^#2222 = #1)";
148 > eval_matches "/thmid/" "/op_/" t thy;
149 SOME ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2222 = #1) = False",
150 Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
152 > val t = (Thm.term_of o the o (parse thy))
153 "matches (a = b) (x + #1 + #-1 * #2 = #0)";
154 > eval_matches "/thmid/" "/op_/" t thy;
155 SOME ("matches (a = b) (x + #1 + #-1 * #2 = #0) = True",Const # $ (# $ #))
158 (*.does a pattern match some subterm ?.*)
159 fun matchsub thy t pat =
161 fun matchs (t as Const _) = TermC.matches thy t pat
162 | matchs (t as Free _) = TermC.matches thy t pat
163 | matchs (t as Var _) = TermC.matches thy t pat
164 | matchs (Bound _) = false
165 | matchs (t as Abs (_, _, body)) =
166 if TermC.matches thy t pat then true else TermC.matches thy body pat
167 | matchs (t as f1 $ f2) =
168 if TermC.matches thy t pat then true
169 else if matchs f1 then true else matchs f2
172 (*("matchsub",("Tools.matchsub",eval_matchsub "#matchsub_")):calc*)
173 fun eval_matchsub (thmid:string) "Tools.matchsub"
174 (t as Const ("Tools.matchsub",_) $ pat $ tst) thy =
175 if matchsub thy tst pat
177 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
178 in SOME (term_to_string''' thy prop, prop) end
180 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
181 in SOME (term_to_string''' thy prop, prop) end
182 | eval_matchsub _ _ _ _ = NONE;
184 (*get the variables in an isabelle-term*)
185 (*("Vars" ,("Tools.Vars" ,eval_var "#Vars_")):calc*)
186 fun eval_var (thmid:string) "Tools.Vars" (t as (Const(op0,t0) $ arg)) thy =
188 val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t;
189 val thmId = thmid ^ term_to_string''' thy arg;
190 in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end
191 | eval_var _ _ _ _ = NONE;
193 fun lhs (Const ("HOL.eq",_) $ l $ _) = l
194 | lhs t = error("lhs called with (" ^ term2str t ^ ")");
195 (*("lhs" ,("Tools.lhs" ,eval_lhs "")):calc*)
196 fun eval_lhs _ "Tools.lhs"
197 (t as (Const ("Tools.lhs",_) $ (Const ("HOL.eq",_) $ l $ _))) _ =
198 SOME ((term2str t) ^ " = " ^ (term2str l),
199 HOLogic.Trueprop $ (TermC.mk_equality (t, l)))
200 | eval_lhs _ _ _ _ = NONE;
202 > val t = (Thm.term_of o the o (parse thy)) "lhs (1 * x ^^^ 2 = 0)";
203 > val SOME (id,t') = eval_lhs 0 0 t 0;
204 val id = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
206 val it = "Tools.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string
209 fun rhs (Const ("HOL.eq",_) $ _ $ r) = r
210 | rhs t = error("rhs called with (" ^ term2str t ^ ")");
211 (*("rhs" ,("Tools.rhs" ,eval_rhs "")):calc*)
212 fun eval_rhs _ "Tools.rhs"
213 (t as (Const ("Tools.rhs",_) $ (Const ("HOL.eq",_) $ _ $ r))) _ =
214 SOME ((term2str t) ^ " = " ^ (term2str r),
215 HOLogic.Trueprop $ (TermC.mk_equality (t, r)))
216 | eval_rhs _ _ _ _ = NONE;
219 (*for evaluating scripts*)
221 val list_rls = append_rls "list_rls" list_rls [Calc ("Tools.rhs", eval_rhs "")];
223 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
224 setup {* KEStore_Elems.add_calcs
225 [("matches", ("Tools.matches", eval_matches "#matches_")),
226 ("matchsub", ("Tools.matchsub", eval_matchsub "#matchsub_")),
227 ("Vars", ("Tools.Vars", eval_var "#Vars_")),
228 ("lhs", ("Tools.lhs", eval_lhs "")),
229 ("rhs", ("Tools.rhs", eval_rhs ""))] *}