1 (* Title: tactics, tacticals etc. for scripts
2 Author: Walther Neuper 000224
3 (c) due to copyright terms
4 12345678901234567890123456789012345678901234567890123456789012345678901234567890
5 10 20 30 40 50 60 70 80
8 theory Script imports Tools begin
11 ID (* identifiers for thy, ruleset,... *)
14 arg (* argument of subproblem *)
18 (*types of subproblems' arguments*)
20 REAL_LIST :: "(real list) => arg"
21 REAL_SET :: "(real set) => arg"
23 BOOL_LIST :: "(bool list) => arg"
24 REAL_REAL :: "(real => real) => arg"
27 Rewrite :: "[ID, bool, 'a] => 'a"
28 Rewrite'_Inst:: "[(real * real) list, ID, bool, 'a] => 'a"
29 ("(Rewrite'_Inst (_ _ _))" 11)
30 (*without last argument ^^ for @@*)
31 Rewrite'_Set :: "[ID, bool, 'a] => 'a" ("(Rewrite'_Set (_ _))" 11)
33 :: "[(real * real) list, ID, bool, 'a] => 'a"
34 ("(Rewrite'_Set'_Inst (_ _ _))" 11)
35 (*without last argument ^^ for @@*)
36 Calculate :: "[ID, 'a] => 'a" (*WN100816 PLUS, TIMES, POWER miss.in scr*)
37 Calculate1 :: "[ID, 'a] => 'a" (*FIXXXME: unknown to script-interpreter*)
39 (* WN0509 substitution now is rewriting by a list of terms (of type bool)
40 Substitute :: "[(real * real) list, 'a] => 'a"*)
41 Substitute :: "[bool list, 'a] => 'a"
43 Map :: "['a => 'b, 'a list] => 'b list"
44 Tac :: "ID => 'a" (*deprecated; used in Test.ML*)
46 "['a list, 'b set] => 'a list"
47 ("Check'_elementwise (_ _)" 11)
48 Take :: "'a => 'a" (*for non-var args as long as no 'o'*)
49 SubProblem :: "[ID * ID list * ID list, arg list] => 'a"
51 Or'_to'_List :: "bool => 'a list" ("Or'_to'_List (_)" 11)
52 (*=========== record these ^^^ in 'tacs' in Script.ML =========*)
55 Problem :: "[ID * ID list] => 'a"
57 (*special formulas for frontend 'CAS format'*)
58 Subproblem :: "(ID * ID list) => 'a"
60 (*script-expressions (tacticals)*)
61 Seq :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "@@" 10) (*@ used*)
62 Try :: "['a => 'a, 'a] => 'a"
63 Repeat :: "['a => 'a, 'a] => 'a"
64 Or :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10)
65 While :: "[bool, 'a => 'a, 'a] => 'a" ("((While (_) Do)//(_))" 9)
66 (*WN100723 because of "Error in syntax translation" below...
67 (*'b => bool doesn't work with "contains_root _"*)
68 Letpar :: "['a, 'a => 'b] => 'b"
69 (*--- defined in Isabelle/scr/HOL/HOL.thy:
70 Let :: "['a, 'a => 'b] => 'b"
71 "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
72 If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10)
73 %x. P x .. lambda is defined in Isabelles meta logic
78 (*... + RECORD IN 'screxpr' in Script.ML *)
80 (*for scripts generated automatically from rls*)
81 Stepwise :: "['z, 'z] => 'z" ("((Script Stepwise (_ =))// (_))" 9)
82 Stepwise'_inst:: "['z,real,'z] => 'z"
83 ("((Script Stepwise'_inst (_ _ =))// (_))" 9)
86 (*SHIFT -> resp.thys ----vvv---------------------------------------------*)
87 (*script-names: initial capital letter,
88 type of last arg (=script-body) == result-type !
89 Xxxx :: script ids, duplicate result-type 'r in last argument:
94 (*make'_solution'_set :: "bool => bool list"
95 ("(make'_solution'_set (_))" 11)
98 :: "[ID * (ID list) * ID, bool,real,real set] => real"
99 ("(max'_on'_interval (_)/ (_ _ _))" 9)
101 :: "[ID * (ID list) * ID,
102 real,real,real,real,bool list] => bool list"
103 ("(find'_vals (_)/ (_ _ _ _ _))" 9)
105 make'_fun :: "[ID * (ID list) * ID, real,real,bool list] => bool"
106 ("(make'_fun (_)/ (_ _ _))" 9)
109 :: "[ID * (ID list) * ID, bool,real] => bool list"
110 ("(solve'_univar (_)/ (_ _ ))" 9)
112 :: "[ID * (ID list) * ID, bool,real,bool] => bool list"
113 ("(solve'_univar (_)/ (_ _ _))" 9)
116 Testeq :: "[bool, bool] => bool"
117 ("((Script Testeq (_ =))//
120 Testeq2 :: "[bool, bool list] => bool list"
121 ("((Script Testeq2 (_ =))//
124 Testterm :: "[real, real] => real"
125 ("((Script Testterm (_ =))//
128 Testchk :: "[bool, real, real list] => real list"
129 ("((Script Testchk (_ _ =))//
131 (*... + RECORD IN 'subpbls' in Script.ML *)
132 (*SHIFT -> resp.thys ----^^^----------------------------*)
137 "_Letpar" :: "[letbinds, 'a] => 'a" ("(letpar (_)/ in (_))" 10)
141 "_Letpar (_binds b bs) e" == "_Letpar b (_Letpar bs e)"
142 "letpar x = a in e" == "Letpar a (%x. e)"
143 *** Error in syntax translation rule: rhs contains extra variables
144 *** ("_Letpar" ("_bind" x a) e) -> (Letpar a ("_abs" x e))
145 *** At command "translations" (line 140 of "/usr/local/isabisac/src/Pure/isac/Scripts/Script").
148 ML {* (*the former Script.ML*)
150 (*.record all theories defined for Scripts; in order to distinguish them
151 from general IsacKnowledge defined later on.*)
152 script_thys := !theory';
154 (*--vvv----- SHIFT? or delete ?*)
155 val IDTyp = Type("Script.ID",[]);
158 val tacs = Unsynchronized.ref (distinct (remove op = ""
160 "Rewrite","Rewrite'_Inst","Rewrite'_Set","Rewrite'_Set'_Inst",
161 "Substitute","Tac","Check'_elementswise",
162 "Take","Subproblem","Or'_to'_List"]));
164 val screxpr = Unsynchronized.ref (distinct (remove op = ""
165 ["HOL.Let","If","Repeat","While","Try","Or"]));
167 val listfuns = Unsynchronized.ref [(*_all_ functions in Isa99.List.thy *)
168 "@","filter","concat","foldl","hd","last","set","list_all",
169 "map","mem","nth","list_update","take","drop",
170 "takeWhile","dropWhile","tl","butlast",
171 "rev","zip","upt","remdups","nodups","replicate",
175 val scrfuns = Unsynchronized.ref ([]: string list);
177 val listexpr = Unsynchronized.ref (union op = (!listfuns) (!scrfuns));
179 val notsimp = Unsynchronized.ref
180 (distinct (remove op = ""
181 (!tacs @ !screxpr @ (*!subpbls @*) !scrfuns @ !listfuns)));
183 val negotiable = Unsynchronized.ref ((!tacs (*@ !subpbls*)));
185 val tacpbl = Unsynchronized.ref
186 (distinct (remove op = "" (!tacs (*@ !subpbls*))));
187 (*--^^^----- SHIFT? or delete ?*)