src/Tools/isac/Knowledge/Descript.thy
branchisac-update-Isa09-2
changeset 37947 22235e4dbe5f
parent 37944 18794c7f43e2
child 37948 ed85f172569c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Knowledge/Descript.thy	Wed Aug 25 16:20:07 2010 +0200
     1.3 @@ -0,0 +1,52 @@
     1.4 +(* Title:  descriptions for items in model-patterns of problems and in method's 
     1.5 +           guards
     1.6 +   Author: Walther Neuper 000301
     1.7 +   (c) due to copyright terms
     1.8 +   + see WN, Reactive User-Guidance ... Vers. Oct.2000 p.48 ff
     1.9 +
    1.10 +remove_thy"Descript";
    1.11 +use_thy"Knowledge/Descript";
    1.12 +use_thy_only"Knowledge/Descript";
    1.13 +
    1.14 +remove_thy"Typefix";
    1.15 +use_thy"Knowledge/Isac";
    1.16 +*)
    1.17 +
    1.18 +theory Descript imports "../ProgLang/Script" begin
    1.19 +
    1.20 +consts
    1.21 +
    1.22 +  someList       :: "'a list => unl" (*not for elementwise input, eg. inssort*)
    1.23 +
    1.24 +  additionalRels :: "bool list => una"
    1.25 +  boundVariable  :: "real => una"
    1.26 +(*derivative     :: 'a => toreal 28.11.00*)
    1.27 +  derivative     :: "real => una"
    1.28 +  equalities     :: "bool list => tobooll" (*WN071228 see fixedValues*)
    1.29 +  equality       :: "bool => una"
    1.30 +  errorBound     :: "bool => nam"
    1.31 +  
    1.32 +  fixedValues    :: "bool list => nam"
    1.33 +  functionEq     :: "bool => una"     (*6.5.03: functionTerm -> functionEq*)
    1.34 +  antiDerivative :: "bool => una"
    1.35 +  functionOf     :: "real => una"
    1.36 +(*functionTerm   :: 'a => toreal 28.11.00*)
    1.37 +  functionTerm   :: "real => una"     (*6.5.03: functionTerm -> functionEq*)
    1.38 +  interval       :: "real set => una"
    1.39 +  maxArgument    :: "bool => toreal"
    1.40 +  maximum        :: "real => toreal"
    1.41 +  
    1.42 +  relations      :: "bool list => una"
    1.43 +  solutions      :: "bool list => toreall"
    1.44 +(*solution       :: bool => toreal  WN0509 bool list=> toreall --->EqSystem*)
    1.45 +  solveFor       :: "real => una"
    1.46 +  differentiateFor:: "real => una"
    1.47 +  unknown        :: "'a => unknow"
    1.48 +  valuesFor      :: "real list => toreall"
    1.49 +
    1.50 +  realTestGiven  :: "real => una"
    1.51 +  realTestFind   :: "real => una"
    1.52 +  boolTestGiven  :: "bool => una"
    1.53 +  boolTestFind   :: "bool => una"
    1.54 +
    1.55 +end
    1.56 \ No newline at end of file