(* auxiliary functions used in scripts

   author: Walther Neuper 000301

   WN0509 shift into Atools ?!? (because used also in where of models !)

   (c) copyright due to lincense terms.

remove_thy"Tools";

use_thy"Scripts/Tools";

*)

theory Tools

imports ListG

begin

(*belongs to theory ListG*)

ML {*

val first_isac_thy = @{theory ListG}

*}

(*for Descript.thy*)

  (***********************************************************************)

  (* 'fun is_dsc' in Scripts/scrtools.smlMUST contain ALL these types !!!*)

  (***********************************************************************)

typedecl nam     (* named variables                                             *)

typedecl  una     (* unnamed variables                                           *)

typedecl  unl     (* unnamed variables of type list, elementwise input prohibited*)

typedecl  str     (* structured variables                                        *)

typedecl  toreal  (* var with undef real value: forces typing                    *)

typedecl  toreall (* var with undef real list value: forces typing               *)

typedecl  tobooll (* var with undef bool list value: forces typing               *)

typedecl  unknow  (* input without dsc in fmz=[]                                 *)

typedecl  cpy     (* UNUSED: copy-named variables

             identified by .._0, .._i .._' in pbt                        *)

  (***********************************************************************)

  (* 'fun is_dsc' in Scripts/scrtools.smlMUST contain ALL these types !!!*)

  (***********************************************************************)

consts

  UniversalList   :: "bool list"

  lhs             :: "bool => real"           (*of an equality*)

  rhs             :: "bool => real"           (*of an equality*)

  Vars            :: "'a => real list"        (*get the variables of a term *)

  matches         :: "['a, 'a] => bool"

  matchsub        :: "['a, 'a] => bool"

constdefs

  Testvar   :: "[real, 'a] => bool"  (*is a variable in a term: unused 6.5.03*)

 "Testvar v t == v mem (Vars t)"     (*by rewriting only,no Calcunused 6.5.03*)

end