(* Title:  tactics, tacticals etc. for scripts

   Author: Walther Neuper 000224

   (c) due to copyright terms

12345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80

 *)

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; used 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").

*)

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 ([]: string list);

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