wneuper@59596: (* Title: "Specify/input-descript.sml"
wneuper@59596:    Author: Walther Neuper 060605
wneuper@59596:    (c) due to copyright terms
wneuper@59596: *)
wneuper@59596: "----------------------------------------------------------------------------------------------";
wneuper@59596: "table of contents ----------------------------------------------------------------------------";
wneuper@59596: "----------------------------------------------------------------------------------------------";
wneuper@59596: "-------- distinguish input to Model ----------------------------------------------------------";
wneuper@59596: "----------------------------------------------------------------------------------------------";
wneuper@59596: "----------------------------------------------------------------------------------------------";
wneuper@59596: "----------------------------------------------------------------------------------------------";
wneuper@59596: 
wneuper@59596: 
wneuper@59596: "-------- distinguish input to Model ----------------------------------------------------------";
wneuper@59596: "-------- distinguish input to Model ----------------------------------------------------------";
wneuper@59596: "-------- distinguish input to Model ----------------------------------------------------------";
wneuper@59596: "----- fun is_booll_dsc -----";
wneuper@59596: val t as Const ("Input_Descript.relations", 
wneuper@59596:   Type ("fun", [Type ("List.list", [Type ("HOL.bool",[])]), 
wneuper@59596:     Type ("Input_Descript.una", [])])) = @{term "relations"};
wneuper@59596: atomtyp (type_of t);
wneuper@59596: if is_booll_dsc t then () else error "is_booll_dsc changed";
wneuper@59596: "----- fun is_reall_dsc -----";
wneuper@59596: if not (is_reall_dsc t) then () else error "is_reall_dsc changed";
wneuper@59596: 
wneuper@59596: "----- fun is_list_dsc -----";
wneuper@59596: val t = @{term "someList"};
wneuper@59596: if is_list_dsc t then () else error "is_list_dsc changed 1";
wneuper@59596: 
wneuper@59596: val t = @{term "additionalRels [a=b,c=(d::real)]"};
wneuper@59596: if is_list_dsc t then () else error "is_list_dsc changed 2";
wneuper@59596: if is_list_dsc (head_of t) then () else error "is_list_dsc changed 3";
wneuper@59596: 
wneuper@59596: "----- fun is_list_dsc -----";
wneuper@59596: val t = @{term "maximum"};
wneuper@59596: if is_dsc t then () else error "is_dsc changed 1";
wneuper@59596: 
wneuper@59596: val t = head_of @{term "maximum A"};
wneuper@59596: if is_dsc t then () else error "is_dsc changed 2";
wneuper@59596: 
wneuper@59596: val t = head_of @{term "fixedValues [R=(R::real)]"};
wneuper@59596: if is_dsc t then () else error "is_dsc changed 3";
wneuper@59596: