1.1 --- a/src/Tools/isac/Scripts/Script.thy Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,194 +0,0 @@
1.4 -(* Title: tactics, tacticals etc. for scripts
1.5 - Author: Walther Neuper 000224
1.6 - (c) due to copyright terms
1.7 -
1.8 -use_thy_only"Scripts/Script";
1.9 -use_thy"../Scripts/Script";
1.10 -use_thy"Script";
1.11 - *)
1.12 -
1.13 -theory Script imports Tools begin
1.14 -
1.15 -typedecl
1.16 - ID (* identifiers for thy, ruleset,... *)
1.17 -
1.18 -typedecl
1.19 - arg (* argument of subproblem *)
1.20 -
1.21 -consts
1.22 -
1.23 -(*types of subproblems' arguments*)
1.24 - real_' :: "real => arg"
1.25 - real_list_' :: "(real list) => arg"
1.26 - real_set_' :: "(real set) => arg"
1.27 - bool_' :: "bool => arg"
1.28 - bool_list_' :: "(bool list) => arg"
1.29 - real_real_' :: "(real => real) => arg"
1.30 -
1.31 -(*tactics*)
1.32 - Rewrite :: "[ID, bool, 'a] => 'a"
1.33 - Rewrite'_Inst:: "[(real * real) list, ID, bool, 'a] => 'a"
1.34 - ("(Rewrite'_Inst (_ _ _))" 11)
1.35 - (*without last argument ^^ for @@*)
1.36 - Rewrite'_Set :: "[ID, bool, 'a] => 'a" ("(Rewrite'_Set (_ _))" 11)
1.37 - Rewrite'_Set'_Inst
1.38 - :: "[(real * real) list, ID, bool, 'a] => 'a"
1.39 - ("(Rewrite'_Set'_Inst (_ _ _))" 11)
1.40 - (*without last argument ^^ for @@*)
1.41 - Calculate :: "[ID, 'a] => 'a" (*WN100816 PLUS, TIMES, POWER miss.in scr*)
1.42 - Calculate1 :: "[ID, 'a] => 'a" (*FIXXXME: unknown to script-interpreter*)
1.43 -
1.44 - (* WN0509 substitution now is rewriting by a list of terms (of type bool)
1.45 - Substitute :: "[(real * real) list, 'a] => 'a"*)
1.46 - Substitute :: "[bool list, 'a] => 'a"
1.47 -
1.48 - Map :: "['a => 'b, 'a list] => 'b list"
1.49 - Tac :: "ID => 'a" (*deprecated; only use in Test.ML*)
1.50 - Check'_elementwise ::
1.51 - "['a list, 'b set] => 'a list"
1.52 - ("Check'_elementwise (_ _)" 11)
1.53 - Take :: "'a => 'a" (*for non-var args as long as no 'o'*)
1.54 - SubProblem :: "[ID * ID list * ID list, arg list] => 'a"
1.55 -
1.56 - Or'_to'_List :: "bool => 'a list" ("Or'_to'_List (_)" 11)
1.57 - (*=========== record these ^^^ in 'tacs' in Script.ML =========*)
1.58 -
1.59 - Assumptions :: bool
1.60 - Problem :: "[ID * ID list] => 'a"
1.61 -
1.62 -(*special formulas for frontend 'CAS format'*)
1.63 - Subproblem :: "(ID * ID list) => 'a"
1.64 -
1.65 -(*script-expressions (tacticals)*)
1.66 - Seq :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "@@" 10) (*@ used*)
1.67 - Try :: "['a => 'a, 'a] => 'a"
1.68 - Repeat :: "['a => 'a, 'a] => 'a"
1.69 - Or :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10)
1.70 - While :: "[bool, 'a => 'a, 'a] => 'a" ("((While (_) Do)//(_))" 9)
1.71 -(*WN100723 because of "Error in syntax translation" below...
1.72 - (*'b => bool doesn't work with "contains_root _"*)
1.73 - Letpar :: "['a, 'a => 'b] => 'b"
1.74 - (*--- defined in Isabelle/scr/HOL/HOL.thy:
1.75 - Let :: "['a, 'a => 'b] => 'b"
1.76 - "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
1.77 - If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10)
1.78 - %x. P x .. lambda is defined in Isabelles meta logic
1.79 - --- *)
1.80 -*)
1.81 - failtac :: 'a
1.82 - idletac :: 'a
1.83 - (*... + RECORD IN 'screxpr' in Script.ML *)
1.84 -
1.85 -(*for scripts generated automatically from rls*)
1.86 - Stepwise :: "['z, 'z] => 'z" ("((Script Stepwise (_ =))// (_))" 9)
1.87 - Stepwise'_inst:: "['z,real,'z] => 'z"
1.88 - ("((Script Stepwise'_inst (_ _ =))// (_))" 9)
1.89 -
1.90 -
1.91 -(*SHIFT -> resp.thys ----vvv---------------------------------------------*)
1.92 -(*script-names: initial capital letter,
1.93 - type of last arg (=script-body) == result-type !
1.94 - Xxxx :: script ids, duplicate result-type 'r in last argument:
1.95 - "['a, ... , \
1.96 - \ 'r] => 'r
1.97 -*)
1.98 -
1.99 -(*make'_solution'_set :: "bool => bool list"
1.100 - ("(make'_solution'_set (_))" 11)
1.101 -
1.102 - max'_on'_interval
1.103 - :: "[ID * (ID list) * ID, bool,real,real set] => real"
1.104 - ("(max'_on'_interval (_)/ (_ _ _))" 9)
1.105 - find'_vals
1.106 - :: "[ID * (ID list) * ID,
1.107 - real,real,real,real,bool list] => bool list"
1.108 - ("(find'_vals (_)/ (_ _ _ _ _))" 9)
1.109 -
1.110 - make'_fun :: "[ID * (ID list) * ID, real,real,bool list] => bool"
1.111 - ("(make'_fun (_)/ (_ _ _))" 9)
1.112 -
1.113 - solve'_univar
1.114 - :: "[ID * (ID list) * ID, bool,real] => bool list"
1.115 - ("(solve'_univar (_)/ (_ _ ))" 9)
1.116 - solve'_univar'_err
1.117 - :: "[ID * (ID list) * ID, bool,real,bool] => bool list"
1.118 - ("(solve'_univar (_)/ (_ _ _))" 9)
1.119 -----------*)
1.120 -
1.121 - Testeq :: "[bool, bool] => bool"
1.122 - ("((Script Testeq (_ =))//
1.123 - (_))" 9)
1.124 -
1.125 - Testeq2 :: "[bool, bool list] => bool list"
1.126 - ("((Script Testeq2 (_ =))//
1.127 - (_))" 9)
1.128 -
1.129 - Testterm :: "[real, real] => real"
1.130 - ("((Script Testterm (_ =))//
1.131 - (_))" 9)
1.132 -
1.133 - Testchk :: "[bool, real, real list] => real list"
1.134 - ("((Script Testchk (_ _ =))//
1.135 - (_))" 9)
1.136 - (*... + RECORD IN 'subpbls' in Script.ML *)
1.137 -(*SHIFT -> resp.thys ----^^^----------------------------*)
1.138 -
1.139 -(*Makarius 10.03
1.140 -syntax
1.141 -
1.142 - "_Letpar" :: "[letbinds, 'a] => 'a" ("(letpar (_)/ in (_))" 10)
1.143 -
1.144 -translations
1.145 -
1.146 - "_Letpar (_binds b bs) e" == "_Letpar b (_Letpar bs e)"
1.147 - "letpar x = a in e" == "Letpar a (%x. e)"
1.148 -*** Error in syntax translation rule: rhs contains extra variables
1.149 -*** ("_Letpar" ("_bind" x a) e) -> (Letpar a ("_abs" x e))
1.150 -*** At command "translations" (line 140 of "/usr/local/isabisac/src/Pure/isac/Scripts/Script.thy").
1.151 -*)
1.152 -
1.153 -ML {* (*the former Script.ML*)
1.154 -
1.155 -(*.record all theories defined for Scripts; in order to distinguish them
1.156 - from general IsacKnowledge defined later on.*)
1.157 -script_thys := !theory';
1.158 -
1.159 -(*--vvv----- SHIFT? or delete ?*)
1.160 -val IDTyp = Type("Script.ID",[]);
1.161 -
1.162 -
1.163 -val tacs = ref (distinct (remove op = ""
1.164 - ["Calculate",
1.165 - "Rewrite","Rewrite'_Inst","Rewrite'_Set","Rewrite'_Set'_Inst",
1.166 - "Substitute","Tac","Check'_elementswise",
1.167 - "Take","Subproblem","Or'_to'_List"]));
1.168 -
1.169 -val screxpr = ref (distinct (remove op = ""
1.170 - ["Let","If","Repeat","While","Try","Or"]));
1.171 -
1.172 -val listfuns = ref [(*_all_ functions in Isa99.List.thy *)
1.173 - "@","filter","concat","foldl","hd","last","set","list_all",
1.174 - "map","mem","nth","list_update","take","drop",
1.175 - "takeWhile","dropWhile","tl","butlast",
1.176 - "rev","zip","upt","remdups","nodups","replicate",
1.177 -
1.178 - "Cons","Nil"];
1.179 -
1.180 -val scrfuns = ref (distinct (remove op = ""
1.181 - ["Testvar"]));
1.182 -
1.183 -val listexpr = ref (union op = (!listfuns) (!scrfuns));
1.184 -
1.185 -val notsimp = ref
1.186 - (distinct (remove op = ""
1.187 - (!tacs @ !screxpr @ (*!subpbls @*) !scrfuns @ !listfuns)));
1.188 -
1.189 -val negotiable = ref ((!tacs (*@ !subpbls*)));
1.190 -
1.191 -val tacpbl = ref
1.192 - (distinct (remove op = "" (!tacs (*@ !subpbls*))));
1.193 -(*--^^^----- SHIFT? or delete ?*)
1.194 -
1.195 -*}
1.196 -
1.197 -end