wneuper/isac: src/sml/Scripts/Script.thy@cac1f942e1a1

     1 (* tactics, tacticals etc. for scripts

     2    W.N.24.2.00

     3    use_thy_only"Scripts/Script";

     4    use_thy"../Scripts/Script";

     5    use_thy"Script";

     6  *)

     8 Script = ListG + Tools +

    10 types

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

    13   arg	(* argument of subproblem           *)

    15 arities

    17   ID, arg :: type

    19 consts

    21 (*types of subproblems' arguments*)

    22   real_        :: real => arg

    23   real_list_   :: (real list) => arg

    24   real_set_    :: (real set) => arg

    25   bool_	       :: bool => arg

    26   bool_list_   :: (bool list) => arg

    28 (*tactics*)

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

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

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

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

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

    34   Rewrite'_Set'_Inst

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

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

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

    38   Calculate    :: "[ID, 'a] => 'a"

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

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

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

    42   Check'_elementwise ::

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

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

    45   Assumptions  :: bool

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

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

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

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

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

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

    55 (*script-expressions (tacticals)*)

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

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

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

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

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

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

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

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

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

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

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

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

    68   --- *)

    71   failtac, idletac :: 'a

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

    74 (*for scripts generated automatically from rls*)

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

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

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

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

    81 (*script-names: initial capital letter,

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

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

    84              "['a, ... , \

    85 	       \         'r] => 'r

    86 *)

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

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

    91   max'_on'_interval

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

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

    94   find'_vals

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

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

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

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

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

   102   solve'_univar

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

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

   105   solve'_univar'_err

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

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

   108 ----------*)

   110   Testeq     :: "[bool, \

   111 		  \ bool] => bool"

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

   113                  \ (_))" 9)

   115   Testeq2    :: "[bool, \

   116 		  \ bool list] => bool list"

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

   118                  \ (_))" 9)

   120   Testterm   :: "[real, \

   121 		  \ real] => real"

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

   123                  \ (_))" 9)

   125   Testchk    :: "[bool, real, \

   126 		  \ real list] => real list"

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

   128                  \ (_))" 9)

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

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

   132 syntax

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

   136 translations

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

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

   141 end

author	wneuper
	Sat, 20 Aug 2005 21:20:16 +0200
changeset 2918	cac1f942e1a1
parent 1330	1d7b3872e940
child 3758	6d7bf1d2f94d
permissions	-rw-r--r--