src/Tools/isac/IsacKnowledge/Descript.thy
branchisac-update-Isa09-2
changeset 37947 22235e4dbe5f
parent 37944 18794c7f43e2
equal deleted inserted replaced
37946:a28b5fc129b7 37947:22235e4dbe5f
     1 (* Title:  descriptions for items in model-patterns of problems and in method's 
       
     2            guards
       
     3    Author: Walther Neuper 000301
       
     4    (c) due to copyright terms
       
     5    + see WN, Reactive User-Guidance ... Vers. Oct.2000 p.48 ff
       
     6 
       
     7 remove_thy"Descript";
       
     8 use_thy"IsacKnowledge/Descript";
       
     9 use_thy_only"IsacKnowledge/Descript";
       
    10 
       
    11 remove_thy"Typefix";
       
    12 use_thy"IsacKnowledge/Isac";
       
    13 *)
       
    14 
       
    15 theory Descript imports "../Scripts/Script" begin
       
    16 
       
    17 consts
       
    18 
       
    19   someList       :: "'a list => unl" (*not for elementwise input, eg. inssort*)
       
    20 
       
    21   additionalRels :: "bool list => una"
       
    22   boundVariable  :: "real => una"
       
    23 (*derivative     :: 'a => toreal 28.11.00*)
       
    24   derivative     :: "real => una"
       
    25   equalities     :: "bool list => tobooll" (*WN071228 see fixedValues*)
       
    26   equality       :: "bool => una"
       
    27   errorBound     :: "bool => nam"
       
    28   
       
    29   fixedValues    :: "bool list => nam"
       
    30   functionEq     :: "bool => una"     (*6.5.03: functionTerm -> functionEq*)
       
    31   antiDerivative :: "bool => una"
       
    32   functionOf     :: "real => una"
       
    33 (*functionTerm   :: 'a => toreal 28.11.00*)
       
    34   functionTerm   :: "real => una"     (*6.5.03: functionTerm -> functionEq*)
       
    35   interval       :: "real set => una"
       
    36   maxArgument    :: "bool => toreal"
       
    37   maximum        :: "real => toreal"
       
    38   
       
    39   relations      :: "bool list => una"
       
    40   solutions      :: "bool list => toreall"
       
    41 (*solution       :: bool => toreal  WN0509 bool list=> toreall --->EqSystem*)
       
    42   solveFor       :: "real => una"
       
    43   differentiateFor:: "real => una"
       
    44   unknown        :: "'a => unknow"
       
    45   valuesFor      :: "real list => toreall"
       
    46 
       
    47   realTestGiven  :: "real => una"
       
    48   realTestFind   :: "real => una"
       
    49   boolTestGiven  :: "bool => una"
       
    50   boolTestFind   :: "bool => una"
       
    51 
       
    52 end