src/Tools/isac/Knowledge/Descript.thy
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 25 Aug 2010 16:49:56 +0200
branchisac-update-Isa09-2
changeset 37948 ed85f172569c
parent 37947 22235e4dbe5f
child 37949 aaf528d3ebd5
permissions -rw-r--r--
stuck at Atools.thy again; resume test on dependencies
neuper@37944
     1
(* Title:  descriptions for items in model-patterns of problems and in method's 
neuper@37944
     2
           guards
neuper@37944
     3
   Author: Walther Neuper 000301
neuper@37944
     4
   (c) due to copyright terms
neuper@37906
     5
   + see WN, Reactive User-Guidance ... Vers. Oct.2000 p.48 ff
neuper@37906
     6
*)
neuper@37906
     7
neuper@37948
     8
theory Descript imports "ProgLang/Script" begin
neuper@37948
     9
(*theory Descript imports "../ProgLang/Script" begin*)
neuper@37906
    10
neuper@37906
    11
consts
neuper@37906
    12
neuper@37944
    13
  someList       :: "'a list => unl" (*not for elementwise input, eg. inssort*)
neuper@37906
    14
neuper@37944
    15
  additionalRels :: "bool list => una"
neuper@37944
    16
  boundVariable  :: "real => una"
neuper@37906
    17
(*derivative     :: 'a => toreal 28.11.00*)
neuper@37944
    18
  derivative     :: "real => una"
neuper@37944
    19
  equalities     :: "bool list => tobooll" (*WN071228 see fixedValues*)
neuper@37944
    20
  equality       :: "bool => una"
neuper@37944
    21
  errorBound     :: "bool => nam"
neuper@37906
    22
  
neuper@37944
    23
  fixedValues    :: "bool list => nam"
neuper@37944
    24
  functionEq     :: "bool => una"     (*6.5.03: functionTerm -> functionEq*)
neuper@37944
    25
  antiDerivative :: "bool => una"
neuper@37944
    26
  functionOf     :: "real => una"
neuper@37906
    27
(*functionTerm   :: 'a => toreal 28.11.00*)
neuper@37944
    28
  functionTerm   :: "real => una"     (*6.5.03: functionTerm -> functionEq*)
neuper@37944
    29
  interval       :: "real set => una"
neuper@37944
    30
  maxArgument    :: "bool => toreal"
neuper@37944
    31
  maximum        :: "real => toreal"
neuper@37906
    32
  
neuper@37944
    33
  relations      :: "bool list => una"
neuper@37944
    34
  solutions      :: "bool list => toreall"
neuper@37906
    35
(*solution       :: bool => toreal  WN0509 bool list=> toreall --->EqSystem*)
neuper@37944
    36
  solveFor       :: "real => una"
neuper@37944
    37
  differentiateFor:: "real => una"
neuper@37944
    38
  unknown        :: "'a => unknow"
neuper@37944
    39
  valuesFor      :: "real list => toreall"
neuper@37906
    40
neuper@37944
    41
  realTestGiven  :: "real => una"
neuper@37944
    42
  realTestFind   :: "real => una"
neuper@37944
    43
  boolTestGiven  :: "bool => una"
neuper@37944
    44
  boolTestFind   :: "bool => una"
neuper@37906
    45
neuper@37906
    46
end