(* Title:  tactics, tacticals etc. for scripts

    Author: Walther Neuper 000224

    (c) due to copyright terms

  *)

 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 :: "[char list, 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"

   Check'_elementwise ::

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

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

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

   SubProblem   :: "[char list * char list list * char list 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").

 *)

 end