(* Title:  tactics, tacticals etc. for scripts

    Author: Walther Neuper 000224

    (c) due to copyright terms

 use_thy_only"ProgLang/Script";

 use_thy"../ProgLang/Script";

 use_thy"Script";

  *)

 theory Script imports Tools begin

 typedecl

   ID	(* identifiers for thy, ruleset,... *)

 typedecl

   arg	(* argument of subproblem           *)

 consts

 (*types of subproblems' arguments*)

   REAL        :: "real => arg"

   REAL_LIST   :: "(real list) => arg"

   REAL_SET    :: "(real set) => arg"

   BOOL        :: "bool => arg"

   BOOL_LIST   :: "(bool list) => arg"

   REAL_REAL   :: "(real => real) => arg"

 (*tactics*)

   Rewrite      :: "[ID, bool, 'a] => 'a"

   Rewrite'_Inst:: "[(real * real) list, ID, bool, 'a] => 'a"

 			             ("(Rewrite'_Inst (_ _ _))" 11)

                                      (*without last argument ^^ for @@*)

   Rewrite'_Set :: "[ID, bool, 'a] => 'a" ("(Rewrite'_Set (_ _))" 11)

   Rewrite'_Set'_Inst

                :: "[(real * real) list, ID, bool, 'a] => 'a"

 		                     ("(Rewrite'_Set'_Inst (_ _ _))" 11)

                                      (*without last argument ^^ for @@*)

   Calculate    :: "[ID, 'a] => 'a" (*WN100816 PLUS, TIMES, POWER miss.in scr*)

   Calculate1   :: "[ID, 'a] => 'a" (*FIXXXME: unknown to script-interpreter*)

   (* WN0509 substitution now is rewriting by a list of terms (of type bool)

   Substitute   :: "[(real * real) list, 'a] => 'a"*)

   Substitute   :: "[bool list, 'a] => 'a"

   Map          :: "['a => 'b, 'a list] => 'b list"

   Tac          :: "ID => 'a"         (*deprecated; only use in Test.ML*)

   Check'_elementwise ::

 		  "['a list, 'b set] => 'a list"

                                      ("Check'_elementwise (_ _)" 11)

   Take         :: "'a => 'a"         (*for non-var args as long as no 'o'*)

   SubProblem   :: "[ID * ID list * ID list, arg list] => 'a"

   Or'_to'_List :: "bool => 'a list"  ("Or'_to'_List (_)" 11)

   (*=========== record these ^^^ in 'tacs' in Script.ML =========*)

   Assumptions  :: bool

   Problem      :: "[ID * ID list] => 'a"

 (*special formulas for frontend 'CAS format'*)

   Subproblem   :: "(ID * ID list) => 'a" 

 (*script-expressions (tacticals)*)

   Seq      :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "@@" 10) (*@ used*)

   Try      :: "['a => 'a, 'a] => 'a"

   Repeat   :: "['a => 'a, 'a] => 'a" 

   Or       :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "Or" 10)

   While    :: "[bool, 'a => 'a, 'a] => 'a"     ("((While (_) Do)//(_))" 9)

 (*WN100723 because of "Error in syntax translation" below...

         (*'b => bool doesn't work with "contains_root _"*)

   Letpar   :: "['a, 'a => 'b] => 'b"

   (*--- defined in Isabelle/scr/HOL/HOL.thy:

   Let      :: "['a, 'a => 'b] => 'b"

   "_Let"   :: "[letbinds, 'a] => 'a"       ("(let (_)/ in (_))" 10)

   If       :: "[bool, 'a, 'a] => 'a"       ("(if (_)/ then (_)/ else (_))" 10)

   %x. P x  .. lambda is defined in Isabelles meta logic

   --- *)

 *)

   failtac :: 'a

   idletac :: 'a

   (*... + RECORD IN 'screxpr' in Script.ML *)

 (*for scripts generated automatically from rls*)

   Stepwise      :: "['z,     'z] => 'z" ("((Script Stepwise (_   =))// (_))" 9)

   Stepwise'_inst:: "['z,real,'z] => 'z" 

 	("((Script Stepwise'_inst (_ _ =))// (_))" 9)

 (*SHIFT -> resp.thys ----vvv---------------------------------------------*)

 (*script-names: initial capital letter,

 		type of last arg (=script-body) == result-type !

   Xxxx       :: script ids, duplicate result-type 'r in last argument:

              "['a, ... , \

 	       \         'r] => 'r

 *)

 (*make'_solution'_set :: "bool => bool list" 

 			("(make'_solution'_set (_))" 11)    

   max'_on'_interval

              :: "[ID * (ID list) * ID, bool,real,real set] => real"

                ("(max'_on'_interval (_)/ (_ _ _))" 9)

   find'_vals

              :: "[ID * (ID list) * ID,

 		  real,real,real,real,bool list] => bool list"

                ("(find'_vals (_)/ (_ _ _ _ _))" 9)

   make'_fun  :: "[ID * (ID list) * ID, real,real,bool list] => bool"

                ("(make'_fun (_)/ (_ _ _))" 9)

   solve'_univar

              :: "[ID * (ID list) * ID, bool,real] => bool list"

                ("(solve'_univar (_)/ (_ _ ))" 9)

   solve'_univar'_err

              :: "[ID * (ID list) * ID, bool,real,bool] => bool list"

                ("(solve'_univar (_)/ (_ _ _))" 9)

 ----------*)

   Testeq     :: "[bool, bool] => bool"

                ("((Script Testeq (_ =))// 

                   (_))" 9)

   Testeq2    :: "[bool, bool list] => bool list"

                ("((Script Testeq2 (_ =))// 

                   (_))" 9)

   Testterm   :: "[real, real] => real"

                ("((Script Testterm (_ =))// 

                   (_))" 9)

   Testchk    :: "[bool, real, real list] => real list"

                ("((Script Testchk (_ _ =))// 

                   (_))" 9)

   (*... + RECORD IN 'subpbls' in Script.ML *)

 (*SHIFT -> resp.thys ----^^^----------------------------*)

 (*Makarius 10.03

 syntax

   "_Letpar"     :: "[letbinds, 'a] => 'a"      ("(letpar (_)/ in (_))" 10)

 translations

   "_Letpar (_binds b bs) e"  == "_Letpar b (_Letpar bs e)"

   "letpar x = a in e"        == "Letpar a (%x. e)"

 *** Error in syntax translation rule: rhs contains extra variables

 *** ("_Letpar" ("_bind" x a) e)  ->  (Letpar a ("_abs" x e))

 *** At command "translations" (line 140 of "/usr/local/isabisac/src/Pure/isac/Scripts/Script.thy").

 *)

 ML {* (*the former Script.ML*)

 (*.record all theories defined for Scripts; in order to distinguish them

    from general IsacKnowledge defined later on.*)

 script_thys := !theory';

 (*--vvv----- SHIFT? or delete ?*)

 val IDTyp = Type("Script.ID",[]);

 val tacs = Unsynchronized.ref (distinct (remove op = ""

   ["Calculate",

    "Rewrite","Rewrite'_Inst","Rewrite'_Set","Rewrite'_Set'_Inst",

    "Substitute","Tac","Check'_elementswise",

    "Take","Subproblem","Or'_to'_List"]));

 val screxpr = Unsynchronized.ref (distinct (remove op = ""

   ["Let","If","Repeat","While","Try","Or"]));

 val listfuns = Unsynchronized.ref [(*_all_ functions in Isa99.List.thy *)

     "@","filter","concat","foldl","hd","last","set","list_all",

     "map","mem","nth","list_update","take","drop",	

     "takeWhile","dropWhile","tl","butlast",

     "rev","zip","upt","remdups","nodups","replicate",

     "Cons","Nil"];

 val scrfuns = Unsynchronized.ref (distinct (remove op = ""

   ["Testvar"]));

 val listexpr = Unsynchronized.ref (union op = (!listfuns) (!scrfuns));

 val notsimp = Unsynchronized.ref 

   (distinct (remove op = "" 

              (!tacs @ !screxpr @ (*!subpbls @*) !scrfuns @ !listfuns)));

 val negotiable = Unsynchronized.ref ((!tacs (*@ !subpbls*)));

 val tacpbl = Unsynchronized.ref

   (distinct (remove op = "" (!tacs (*@ !subpbls*))));

 (*--^^^----- SHIFT? or delete ?*)

 *}

 end