removed unused/untested IOA 'automaton' package;
authorwenzelm
Mon Jul 12 22:35:41 2010 +0200 (2010-07-12)
changeset 37785173667d73115
parent 37784 1d639d28832c
child 37786 4eb98849c5c0
removed unused/untested IOA 'automaton' package;
Admin/update-keywords
etc/isar-keywords.el
src/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOLCF/IOA/meta_theory/automaton.ML
src/HOLCF/IsaMakefile
     1.1 --- a/Admin/update-keywords	Mon Jul 12 22:17:31 2010 +0200
     1.2 +++ b/Admin/update-keywords	Mon Jul 12 22:35:41 2010 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  isabelle keywords \
     1.6    "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" \
     1.7 -  "$LOG/IOA.gz" "$LOG/HOL-Boogie.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz"
     1.8 +  "$LOG/HOL-Boogie.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz"
     1.9  
    1.10  isabelle keywords -k ZF \
    1.11    "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
     2.1 --- a/etc/isar-keywords.el	Mon Jul 12 22:17:31 2010 +0200
     2.2 +++ b/etc/isar-keywords.el	Mon Jul 12 22:35:41 2010 +0200
     2.3 @@ -1,6 +1,6 @@
     2.4  ;;
     2.5  ;; Keyword classification tables for Isabelle/Isar.
     2.6 -;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Boogie + HOL-Nominal + HOL-Statespace.
     2.7 +;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + HOL-Boogie + HOL-Nominal + HOL-Statespace.
     2.8  ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     2.9  ;;
    2.10  
    2.11 @@ -31,7 +31,6 @@
    2.12      "assume"
    2.13      "atom_decl"
    2.14      "attribute_setup"
    2.15 -    "automaton"
    2.16      "ax_specification"
    2.17      "axiomatization"
    2.18      "axioms"
    2.19 @@ -279,15 +278,13 @@
    2.20      "}"))
    2.21  
    2.22  (defconst isar-keywords-minor
    2.23 -  '("actions"
    2.24 -    "advanced"
    2.25 +  '("advanced"
    2.26      "and"
    2.27      "assumes"
    2.28      "attach"
    2.29      "avoids"
    2.30      "begin"
    2.31      "binder"
    2.32 -    "compose"
    2.33      "congs"
    2.34      "constrains"
    2.35      "contains"
    2.36 @@ -297,7 +294,6 @@
    2.37      "fixes"
    2.38      "for"
    2.39      "functions"
    2.40 -    "hide_action"
    2.41      "hints"
    2.42      "identifier"
    2.43      "if"
    2.44 @@ -306,9 +302,6 @@
    2.45      "infix"
    2.46      "infixl"
    2.47      "infixr"
    2.48 -    "initially"
    2.49 -    "inputs"
    2.50 -    "internals"
    2.51      "is"
    2.52      "lazy"
    2.53      "module_name"
    2.54 @@ -318,21 +311,11 @@
    2.55      "obtains"
    2.56      "open"
    2.57      "output"
    2.58 -    "outputs"
    2.59      "overloaded"
    2.60      "permissive"
    2.61      "pervasive"
    2.62 -    "post"
    2.63 -    "pre"
    2.64 -    "rename"
    2.65 -    "restrict"
    2.66      "shows"
    2.67 -    "signature"
    2.68 -    "states"
    2.69      "structure"
    2.70 -    "to"
    2.71 -    "transitions"
    2.72 -    "transrel"
    2.73      "unchecked"
    2.74      "uses"
    2.75      "where"))
    2.76 @@ -453,7 +436,6 @@
    2.77      "arities"
    2.78      "atom_decl"
    2.79      "attribute_setup"
    2.80 -    "automaton"
    2.81      "axiomatization"
    2.82      "axioms"
    2.83      "boogie_end"
     3.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Mon Jul 12 22:17:31 2010 +0200
     3.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Mon Jul 12 22:35:41 2010 +0200
     3.3 @@ -6,7 +6,6 @@
     3.4  
     3.5  theory Abstraction
     3.6  imports LiveIOA
     3.7 -uses ("automaton.ML")
     3.8  begin
     3.9  
    3.10  default_sort type
    3.11 @@ -613,6 +612,4 @@
    3.12  
    3.13  method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} ""
    3.14  
    3.15 -use "automaton.ML"
    3.16 -
    3.17  end
     4.1 --- a/src/HOLCF/IOA/meta_theory/automaton.ML	Mon Jul 12 22:17:31 2010 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,529 +0,0 @@
     4.4 -(*  Title:      HOLCF/IOA/meta_theory/automaton.ML
     4.5 -    Author:     Tobias Hamberger, TU Muenchen
     4.6 -*)
     4.7 -
     4.8 -signature AUTOMATON =
     4.9 -sig
    4.10 -  val add_ioa: string -> string
    4.11 -    -> (string) list -> (string) list -> (string) list
    4.12 -    -> (string * string) list -> string
    4.13 -    -> (string * string * (string * string)list) list
    4.14 -    -> theory -> theory
    4.15 -  val add_composition : string -> (string)list -> theory -> theory
    4.16 -  val add_hiding : string -> string -> (string)list -> theory -> theory
    4.17 -  val add_restriction : string -> string -> (string)list -> theory -> theory
    4.18 -  val add_rename : string -> string -> string -> theory -> theory
    4.19 -end;
    4.20 -
    4.21 -structure Automaton: AUTOMATON =
    4.22 -struct
    4.23 -
    4.24 -val string_of_typ = Print_Mode.setmp [] o Syntax.string_of_typ_global;
    4.25 -val string_of_term = Print_Mode.setmp [] o Syntax.string_of_term_global;
    4.26 -
    4.27 -exception malformed;
    4.28 -
    4.29 -(* stripping quotes *)
    4.30 -fun strip [] = [] |
    4.31 -strip ("\""::r) = strip r |
    4.32 -strip (a::r) = a :: (strip r);
    4.33 -fun strip_quote s = implode(strip(explode(s)));
    4.34 -
    4.35 -(* used by *_of_varlist *)
    4.36 -fun extract_first (a,b) = strip_quote a;
    4.37 -fun extract_second (a,b) = strip_quote b;
    4.38 -(* following functions producing sth from a varlist *)
    4.39 -fun comma_list_of_varlist [] = "" |
    4.40 -comma_list_of_varlist [a] = extract_first a |
    4.41 -comma_list_of_varlist (a::r) = (extract_first a) ^ "," ^ (comma_list_of_varlist r);
    4.42 -fun primed_comma_list_of_varlist [] = "" |
    4.43 -primed_comma_list_of_varlist [a] = (extract_first a) ^ "'" |
    4.44 -primed_comma_list_of_varlist (a::r) = (extract_first a) ^ "'," ^
    4.45 - (primed_comma_list_of_varlist r);
    4.46 -fun type_product_of_varlist [] = "" |
    4.47 -type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" |
    4.48 -type_product_of_varlist(a::r) = "(" ^ extract_second(a) ^ ")*" ^ type_product_of_varlist r;
    4.49 -
    4.50 -(* listing a list *)
    4.51 -fun list_elements_of [] = "" |
    4.52 -list_elements_of (a::r) = a ^ " " ^ (list_elements_of r);
    4.53 -
    4.54 -(* extracting type parameters from a type list *)
    4.55 -(* fun param_tupel thy [] res = res |
    4.56 -param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res |
    4.57 -param_tupel thy ((TFree(a,_))::r) res = 
    4.58 -if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) |
    4.59 -param_tupel thy (a::r) res =
    4.60 -error ("one component of a statetype is a TVar: " ^ (string_of_typ thy a));
    4.61 -*)
    4.62 -
    4.63 -(* used by constr_list *)
    4.64 -fun extract_constrs thy [] = [] |
    4.65 -extract_constrs thy (a::r) =
    4.66 -let
    4.67 -fun delete_bold [] = []
    4.68 -| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
    4.69 -        then (let val (_::_::_::s) = xs in delete_bold s end)
    4.70 -        else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
    4.71 -                then  (let val (_::_::_::s) = xs in delete_bold s end)
    4.72 -                else (x::delete_bold xs));
    4.73 -fun delete_bold_string s = implode(delete_bold(explode s));
    4.74 -(* from a constructor term in *.induct (with quantifiers,
    4.75 -"Trueprop" and ?P stripped away) delivers the head *)
    4.76 -fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r |
    4.77 -extract_hd (Const("Trueprop",_) $ r) = extract_hd r |
    4.78 -extract_hd (Var(_,_) $ r) = extract_hd r |
    4.79 -extract_hd (a $ b) = extract_hd a |
    4.80 -extract_hd (Const(s,_)) = s |
    4.81 -extract_hd _ = raise malformed;
    4.82 -(* delivers constructor term string from a prem of *.induct *)
    4.83 -fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))|
    4.84 -extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r |
    4.85 -extract_constr thy (Var(_,_) $ r) =  delete_bold_string(string_of_term thy r) |
    4.86 -extract_constr _ _ = raise malformed;
    4.87 -in
    4.88 -(extract_hd a,extract_constr thy a) :: (extract_constrs thy r)
    4.89 -end;
    4.90 -
    4.91 -(* delivering list of constructor terms of a datatype *)
    4.92 -fun constr_list thy atyp =
    4.93 -let
    4.94 -fun act_name thy (Type(s,_)) = s |
    4.95 -act_name _ s = 
    4.96 -error("malformed action type: " ^ (string_of_typ thy s));
    4.97 -fun afpl ("." :: a) = [] |
    4.98 -afpl [] = [] |
    4.99 -afpl (a::r) = a :: (afpl r);
   4.100 -fun unqualify s = implode(rev(afpl(rev(explode s))));
   4.101 -val q_atypstr = act_name thy atyp;
   4.102 -val uq_atypstr = unqualify q_atypstr;
   4.103 -val prem = prems_of (PureThy.get_thm thy (uq_atypstr ^ ".induct"));
   4.104 -in
   4.105 -extract_constrs thy prem
   4.106 -handle malformed =>
   4.107 -error("malformed theorem : " ^ uq_atypstr ^ ".induct")
   4.108 -end;
   4.109 -
   4.110 -fun check_for_constr thy atyp (a $ b) =
   4.111 -let
   4.112 -fun all_free (Free(_,_)) = true |
   4.113 -all_free (a $ b) = if (all_free a) then (all_free b) else false |
   4.114 -all_free _ = false; 
   4.115 -in 
   4.116 -if (all_free b) then (check_for_constr thy atyp a) else false
   4.117 -end |
   4.118 -check_for_constr thy atyp (Const(a,_)) =
   4.119 -let
   4.120 -val cl = constr_list thy atyp;
   4.121 -fun fstmem a [] = false |
   4.122 -fstmem a ((f,s)::r) = if (a=f) then true else (fstmem a r)
   4.123 -in
   4.124 -if (fstmem a cl) then true else false
   4.125 -end |
   4.126 -check_for_constr _ _ _ = false;
   4.127 -
   4.128 -(* delivering the free variables of a constructor term *)
   4.129 -fun free_vars_of (t1 $ t2) = (free_vars_of t1) @ (free_vars_of t2) |
   4.130 -free_vars_of (Const(_,_)) = [] |
   4.131 -free_vars_of (Free(a,_)) = [a] |
   4.132 -free_vars_of _ = raise malformed;
   4.133 -
   4.134 -(* making a constructor set from a constructor term (of signature) *)
   4.135 -fun constr_set_string thy atyp ctstr =
   4.136 -let
   4.137 -val trm = Misc_Legacy.simple_read_term thy atyp ctstr;
   4.138 -val l = free_vars_of trm
   4.139 -in
   4.140 -if (check_for_constr thy atyp trm) then
   4.141 -(if (l=[]) then ("{" ^ ctstr ^ "}")
   4.142 -else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})")
   4.143 -else (raise malformed) 
   4.144 -handle malformed => 
   4.145 -error("malformed action term: " ^ (string_of_term thy trm))
   4.146 -end;
   4.147 -
   4.148 -(* extracting constructor heads *)
   4.149 -fun constructor_head thy atypstr s =
   4.150 -let
   4.151 -fun hd_of (Const(a,_)) = a |
   4.152 -hd_of (t $ _) = hd_of t |
   4.153 -hd_of _ = raise malformed;
   4.154 -val trm = Misc_Legacy.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
   4.155 -in
   4.156 -hd_of trm handle malformed =>
   4.157 -error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
   4.158 -end;
   4.159 -fun constructor_head_list _ _ [] = [] |
   4.160 -constructor_head_list thy atypstr (a::r) =
   4.161 - (constructor_head thy atypstr a)::(constructor_head_list thy atypstr r);
   4.162 -
   4.163 -(* producing an action set *)
   4.164 -(*FIXME*)
   4.165 -fun action_set_string thy atyp [] = "Set.empty" |
   4.166 -action_set_string thy atyp [a] = constr_set_string thy atyp (strip_quote a) |
   4.167 -action_set_string thy atyp (a::r) = (constr_set_string thy atyp (strip_quote a)) ^
   4.168 -         " Un " ^ (action_set_string thy atyp r);
   4.169 -
   4.170 -(* used by extend *)
   4.171 -fun pstr s [] = "(" ^ s ^ "' = " ^ s ^ ")" |
   4.172 -pstr s ((a,b)::r) =
   4.173 -if (s=a) then ("(" ^ s ^ "' = (" ^ b ^ "))") else (pstr s r);
   4.174 -fun poststring [] l = "" |
   4.175 -poststring [(a,b)] l = pstr a l |
   4.176 -poststring ((a,b)::r) l = (pstr a l) ^ " & " ^ (poststring r l);
   4.177 -
   4.178 -(* extends a (action string,condition,assignlist) tupel by a
   4.179 -(action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list 
   4.180 -(where bool indicates whether there is a precondition *)
   4.181 -fun extend thy atyp statetupel (actstr,r,[]) =
   4.182 -let
   4.183 -val trm = Misc_Legacy.simple_read_term thy atyp actstr;
   4.184 -val rtrm = Misc_Legacy.simple_read_term thy (Type("bool",[])) r;
   4.185 -val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
   4.186 -in
   4.187 -if (check_for_constr thy atyp trm)
   4.188 -then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag)
   4.189 -else
   4.190 -error("transition " ^ actstr ^ " is not a pure constructor term")
   4.191 -end |
   4.192 -extend thy atyp statetupel (actstr,r,(a,b)::c) =
   4.193 -let
   4.194 -fun pseudo_poststring [] = "" |
   4.195 -pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
   4.196 -pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); 
   4.197 -val trm = Misc_Legacy.simple_read_term thy atyp actstr;
   4.198 -val rtrm = Misc_Legacy.simple_read_term thy (Type("bool",[])) r;
   4.199 -val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
   4.200 -in
   4.201 -if (check_for_constr thy atyp trm) then
   4.202 -(if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false)
   4.203 -(* the case with transrel *)
   4.204 - else 
   4.205 - (trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)),
   4.206 -  "(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag))
   4.207 -else
   4.208 -error("transition " ^ actstr ^ " is not a pure constructor term")
   4.209 -end;
   4.210 -(* used by make_alt_string *) 
   4.211 -fun extended_list _ _ _ [] = [] |
   4.212 -extended_list thy atyp statetupel (a::r) =
   4.213 -   (extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r);
   4.214 -
   4.215 -(* used by write_alts *)
   4.216 -fun write_alt thy (chead,tr) inp out int [] =
   4.217 -if member (op =) inp chead then
   4.218 -(
   4.219 -error("Input action " ^ tr ^ " was not specified")
   4.220 -) else (
   4.221 -if member (op =) out chead orelse member (op =) int chead then
   4.222 -(writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else ();
   4.223 -(tr ^ " => False",tr ^ " => False")) |
   4.224 -write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) =
   4.225 -let
   4.226 -fun hd_of (Const(a,_)) = a |
   4.227 -hd_of (t $ _) = hd_of t |
   4.228 -hd_of _ = raise malformed;
   4.229 -fun occurs_again c [] = false |
   4.230 -occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r);
   4.231 -in
   4.232 -if (chead=(hd_of a)) then 
   4.233 -(if member (op =) inp chead andalso e then (
   4.234 -error("Input action " ^ b ^ " has a precondition")
   4.235 -) else (if member (op =) (inp@out@int) chead then 
   4.236 -    (if (occurs_again chead r) then (
   4.237 -error("Two specifications for action: " ^ b)
   4.238 -    ) else (b ^ " => " ^ c,b ^ " => " ^ d))
   4.239 -  else (
   4.240 -error("Action " ^ b ^ " is not in automaton signature")
   4.241 -))) else (write_alt thy (chead,ctrm) inp out int r)
   4.242 -handle malformed =>
   4.243 -error ("malformed action term: " ^ (string_of_term thy a))
   4.244 -end;
   4.245 -
   4.246 -(* used by make_alt_string *)
   4.247 -fun write_alts thy (a,b) inp out int [] ttr = (a,b) |
   4.248 -write_alts thy (a,b) inp out int [c] ttr =
   4.249 -let
   4.250 -val wa = write_alt thy c inp out int ttr
   4.251 -in
   4.252 - (a ^ (fst wa),b ^ (snd wa))
   4.253 -end |
   4.254 -write_alts thy (a,b) inp out int (c::r) ttr =
   4.255 -let
   4.256 -val wa = write_alt thy c inp out int ttr
   4.257 -in
   4.258 - write_alts thy (a ^ (fst wa) ^ " | ", b ^ (snd wa) ^ " | ") inp out int r ttr
   4.259 -end;
   4.260 -
   4.261 -fun make_alt_string thy inp out int atyp statetupel trans =
   4.262 -let
   4.263 -val cl = constr_list thy atyp;
   4.264 -val ttr = extended_list thy atyp statetupel trans;
   4.265 -in
   4.266 -write_alts thy ("","") inp out int cl ttr
   4.267 -end;
   4.268 -
   4.269 -(* used in add_ioa *)
   4.270 -fun check_free_primed (Free(a,_)) = 
   4.271 -let
   4.272 -val (f::r) = rev(explode a)
   4.273 -in
   4.274 -if (f="'") then [a] else []
   4.275 -end | 
   4.276 -check_free_primed (a $ b) = ((check_free_primed a) @ (check_free_primed b)) |
   4.277 -check_free_primed (Abs(_,_,t)) = check_free_primed t |
   4.278 -check_free_primed _ = [];
   4.279 -
   4.280 -fun overlap [] _ = true |
   4.281 -overlap (a::r) l = if member (op =) l a then (
   4.282 -error("Two occurences of action " ^ a ^ " in automaton signature")
   4.283 -) else (overlap r l);
   4.284 -
   4.285 -(* delivering some types of an automaton *)
   4.286 -fun aut_type_of thy aut_name =
   4.287 -let
   4.288 -fun left_of (( _ $ left) $ _) = left |
   4.289 -left_of _ = raise malformed;
   4.290 -val aut_def = concl_of (PureThy.get_thm thy (aut_name ^ "_def"));
   4.291 -in
   4.292 -(#T(rep_cterm(cterm_of thy (left_of aut_def))))
   4.293 -handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
   4.294 -end;
   4.295 -
   4.296 -fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp |
   4.297 -act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^
   4.298 -(string_of_typ thy t));
   4.299 -fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp |
   4.300 -st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^
   4.301 -(string_of_typ thy t));
   4.302 -
   4.303 -fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) |
   4.304 -comp_st_type_of thy (a::r) = HOLogic.mk_prodT (st_type_of thy (aut_type_of thy a), comp_st_type_of thy r) |
   4.305 -comp_st_type_of _ _ = error "empty automaton list";
   4.306 -
   4.307 -(* checking consistency of action types (for composition) *)
   4.308 -fun check_ac thy (a::r) =
   4.309 -let
   4.310 -fun ch_f_a thy acttyp [] = acttyp |
   4.311 -ch_f_a thy acttyp (a::r) =
   4.312 -let
   4.313 -val auttyp = aut_type_of thy a;
   4.314 -val ac = (act_type_of thy auttyp);
   4.315 -in
   4.316 -if (ac=acttyp) then (ch_f_a thy acttyp r) else (error "A")
   4.317 -end;
   4.318 -val auttyp = aut_type_of thy a;
   4.319 -val acttyp = (act_type_of thy auttyp);
   4.320 -in
   4.321 -ch_f_a thy acttyp r
   4.322 -end |
   4.323 -check_ac _ [] = error "empty automaton list";
   4.324 -
   4.325 -fun clist [] = "" |
   4.326 -clist [a] = a |
   4.327 -clist (a::r) = a ^ " || " ^ (clist r);
   4.328 -
   4.329 -val add_defs = snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes o map (apfst Binding.name));
   4.330 -
   4.331 -
   4.332 -(* add_ioa *)
   4.333 -
   4.334 -fun add_ioa automaton_name action_type inp out int statetupel ini trans thy =
   4.335 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   4.336 -let
   4.337 -val state_type_string = type_product_of_varlist(statetupel);
   4.338 -val styp = Syntax.read_typ_global thy state_type_string;
   4.339 -val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")";
   4.340 -val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")";
   4.341 -val atyp = Syntax.read_typ_global thy action_type;
   4.342 -val inp_set_string = action_set_string thy atyp inp;
   4.343 -val out_set_string = action_set_string thy atyp out;
   4.344 -val int_set_string = action_set_string thy atyp int;
   4.345 -val inp_head_list = constructor_head_list thy action_type inp;
   4.346 -val out_head_list = constructor_head_list thy action_type out;
   4.347 -val int_head_list = constructor_head_list thy action_type int;
   4.348 -val overlap_flag = ((overlap inp out) andalso (overlap inp int) andalso (overlap out int)); 
   4.349 -val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list 
   4.350 -              atyp statetupel trans;
   4.351 -val thy2 = (thy
   4.352 -|> Sign.add_consts
   4.353 -[(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn),
   4.354 -(Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn),
   4.355 -(Binding.name (automaton_name ^ "_trans"),
   4.356 - "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
   4.357 -(Binding.name automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
   4.358 -|> add_defs
   4.359 -[(automaton_name ^ "_initial_def",
   4.360 -automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
   4.361 -(automaton_name ^ "_asig_def",
   4.362 -automaton_name ^ "_asig == (" ^
   4.363 - inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"),
   4.364 -(automaton_name ^ "_trans_def",
   4.365 -automaton_name ^ "_trans == {(" ^
   4.366 - state_vars_tupel ^ ", act_of_" ^ automaton_name ^ ", " ^ state_vars_primed ^
   4.367 -"). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"),
   4.368 -(automaton_name ^ "_def",
   4.369 -automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
   4.370 -"_initial, " ^ automaton_name ^ "_trans,{},{})")
   4.371 -])
   4.372 -val chk_prime_list = (check_free_primed (Misc_Legacy.simple_read_term thy2 (Type("bool",[]))
   4.373 -( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
   4.374 -in
   4.375 -(
   4.376 -if (chk_prime_list = []) then thy2
   4.377 -else (
   4.378 -error("Precondition or assignment terms in postconditions contain following primed variables:\n"
   4.379 - ^ (list_elements_of chk_prime_list)))
   4.380 -)
   4.381 -end)
   4.382 -
   4.383 -fun add_composition automaton_name aut_list thy =
   4.384 -  let
   4.385 -    val _ = writeln("Constructing automaton " ^ automaton_name ^ " ...")
   4.386 -    val acttyp = check_ac thy aut_list; 
   4.387 -    val st_typ = comp_st_type_of thy aut_list; 
   4.388 -    val comp_list = clist aut_list;
   4.389 -  in
   4.390 -    thy
   4.391 -    |> Sign.add_consts_i
   4.392 -        [(Binding.name automaton_name, HOLogic.mk_prodT (HOLogic.mk_prodT
   4.393 -          (HOLogic.mk_setT acttyp, HOLogic.mk_prodT (HOLogic.mk_setT acttyp, HOLogic.mk_setT acttyp)),
   4.394 -          HOLogic.mk_prodT (HOLogic.mk_setT st_typ, HOLogic.mk_prodT (HOLogic.mk_setT
   4.395 -          (HOLogic.mk_prodT (st_typ, HOLogic.mk_prodT (acttyp, st_typ))),
   4.396 -          HOLogic.mk_prodT (HOLogic.mk_setT (HOLogic.mk_setT acttyp), HOLogic.mk_setT (HOLogic.mk_setT acttyp))))),
   4.397 -            NoSyn)]
   4.398 -    |> add_defs [(automaton_name ^ "_def", automaton_name ^ " == " ^ comp_list)]
   4.399 -  end
   4.400 -
   4.401 -fun add_restriction automaton_name aut_source actlist thy =
   4.402 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   4.403 -let
   4.404 -val auttyp = aut_type_of thy aut_source;
   4.405 -val acttyp = act_type_of thy auttyp; 
   4.406 -val rest_set = action_set_string thy acttyp actlist
   4.407 -in
   4.408 -thy
   4.409 -|> Sign.add_consts_i
   4.410 -[(Binding.name automaton_name, auttyp,NoSyn)]
   4.411 -|> add_defs
   4.412 -[(automaton_name ^ "_def",
   4.413 -automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] 
   4.414 -end)
   4.415 -fun add_hiding automaton_name aut_source actlist thy =
   4.416 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   4.417 -let
   4.418 -val auttyp = aut_type_of thy aut_source;
   4.419 -val acttyp = act_type_of thy auttyp; 
   4.420 -val hid_set = action_set_string thy acttyp actlist
   4.421 -in
   4.422 -thy
   4.423 -|> Sign.add_consts_i
   4.424 -[(Binding.name automaton_name, auttyp,NoSyn)]
   4.425 -|> add_defs
   4.426 -[(automaton_name ^ "_def",
   4.427 -automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] 
   4.428 -end)
   4.429 -
   4.430 -fun ren_act_type_of thy funct =
   4.431 -  (case Term.fastype_of (Syntax.read_term_global thy funct) of
   4.432 -    Type ("fun", [a, b]) => a
   4.433 -  | _ => error "could not extract argument type of renaming function term");
   4.434 - 
   4.435 -fun add_rename automaton_name aut_source fun_name thy =
   4.436 -  let
   4.437 -    val _ = writeln("Constructing automaton " ^ automaton_name ^ " ...")
   4.438 -    val auttyp = aut_type_of thy aut_source;
   4.439 -    val st_typ = st_type_of thy auttyp;
   4.440 -    val acttyp = ren_act_type_of thy fun_name
   4.441 -  in
   4.442 -    thy
   4.443 -    |> Sign.add_consts_i
   4.444 -        [(Binding.name automaton_name,
   4.445 -        Type(@{type_name prod},
   4.446 -        [Type(@{type_name prod},[HOLogic.mk_setT acttyp,Type(@{type_name prod},[HOLogic.mk_setT acttyp,HOLogic.mk_setT acttyp])]),
   4.447 -         Type(@{type_name prod},[HOLogic.mk_setT st_typ,
   4.448 -          Type(@{type_name prod},[HOLogic.mk_setT (Type(@{type_name prod},[st_typ,Type(@{type_name prod},[acttyp,st_typ])])),
   4.449 -           Type(@{type_name prod},[HOLogic.mk_setT (HOLogic.mk_setT acttyp),HOLogic.mk_setT (HOLogic.mk_setT acttyp)])])])])
   4.450 -        ,NoSyn)]
   4.451 -    |> add_defs [(automaton_name ^ "_def", automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
   4.452 -  end
   4.453 -
   4.454 -
   4.455 -(** outer syntax **)
   4.456 -
   4.457 -(* prepare results *)
   4.458 -
   4.459 -(*encoding transition specifications with a element of ParseTrans*)
   4.460 -datatype ParseTrans = Rel of string | PP of string*(string*string)list;
   4.461 -fun mk_trans_of_rel s = Rel(s);
   4.462 -fun mk_trans_of_prepost (s,l) = PP(s,l); 
   4.463 -
   4.464 -fun trans_of (a, Rel b) = (a, b, [("", "")])
   4.465 -  | trans_of (a, PP (b, l)) = (a, b, l);
   4.466 -
   4.467 -
   4.468 -fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) =
   4.469 -  add_ioa aut action_type inp out int states initial (map trans_of trans);
   4.470 -
   4.471 -fun mk_composition_decl (aut, autlist) =
   4.472 -  add_composition aut autlist;
   4.473 -
   4.474 -fun mk_hiding_decl (aut, (actlist, source_aut)) =
   4.475 -  add_hiding aut source_aut actlist;
   4.476 -
   4.477 -fun mk_restriction_decl (aut, (source_aut, actlist)) =
   4.478 -  add_restriction aut source_aut actlist;
   4.479 -
   4.480 -fun mk_rename_decl (aut, (source_aut, rename_f)) =
   4.481 -  add_rename aut source_aut rename_f;
   4.482 -
   4.483 -
   4.484 -(* outer syntax *)
   4.485 -
   4.486 -val _ = List.app Keyword.keyword ["signature", "actions", "inputs",
   4.487 -  "outputs", "internals", "states", "initially", "transitions", "pre",
   4.488 -  "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
   4.489 -  "rename"];
   4.490 -
   4.491 -val actionlist = Parse.list1 Parse.term;
   4.492 -val inputslist = Parse.$$$ "inputs" |-- Parse.!!! actionlist;
   4.493 -val outputslist = Parse.$$$ "outputs" |-- Parse.!!! actionlist;
   4.494 -val internalslist = Parse.$$$ "internals" |-- Parse.!!! actionlist;
   4.495 -val stateslist =
   4.496 -  Parse.$$$ "states" |-- Parse.!!! (Scan.repeat1 (Parse.name --| Parse.$$$ "::" -- Parse.typ));
   4.497 -val initial = Parse.$$$ "initially" |-- Parse.!!! Parse.term;
   4.498 -val assign_list = Parse.list1 (Parse.name --| Parse.$$$ ":=" -- Parse.!!! Parse.term);
   4.499 -val pre = Parse.$$$ "pre" |-- Parse.!!! Parse.term;
   4.500 -val post = Parse.$$$ "post" |-- Parse.!!! assign_list;
   4.501 -val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost;
   4.502 -val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost;
   4.503 -val transrel =  (Parse.$$$ "transrel" |-- Parse.!!! Parse.term) >> mk_trans_of_rel;
   4.504 -val transition = Parse.term -- (transrel || pre1 || post1);
   4.505 -val translist = Parse.$$$ "transitions" |-- Parse.!!! (Scan.repeat1 transition);
   4.506 -
   4.507 -val ioa_decl =
   4.508 -  (Parse.name -- (Parse.$$$ "=" |--
   4.509 -    (Parse.$$$ "signature" |--
   4.510 -      Parse.!!! (Parse.$$$ "actions" |--
   4.511 -        (Parse.typ --
   4.512 -          (Scan.optional inputslist []) --
   4.513 -          (Scan.optional outputslist []) --
   4.514 -          (Scan.optional internalslist []) --
   4.515 -          stateslist --
   4.516 -          (Scan.optional initial "True") --
   4.517 -        translist))))) >> mk_ioa_decl ||
   4.518 -  (Parse.name -- (Parse.$$$ "=" |-- (Parse.$$$ "compose" |-- Parse.!!! (Parse.list1 Parse.name))))
   4.519 -    >> mk_composition_decl ||
   4.520 -  (Parse.name -- (Parse.$$$ "=" |-- (Parse.$$$ "hide_action" |--
   4.521 -      Parse.!!! (Parse.list1 Parse.term -- (Parse.$$$ "in" |-- Parse.name))))) >> mk_hiding_decl ||
   4.522 -  (Parse.name -- (Parse.$$$ "=" |-- (Parse.$$$ "restrict" |--
   4.523 -      Parse.!!! (Parse.name -- (Parse.$$$ "to" |-- Parse.list1 Parse.term))))) >> mk_restriction_decl ||
   4.524 -  (Parse.name -- (Parse.$$$ "=" |--
   4.525 -      (Parse.$$$ "rename" |-- (Parse.!!! (Parse.name -- (Parse.$$$ "to" |-- Parse.term))))))
   4.526 -    >> mk_rename_decl;
   4.527 -
   4.528 -val _ =
   4.529 -  Outer_Syntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" Keyword.thy_decl
   4.530 -    (ioa_decl >> Toplevel.theory);
   4.531 -
   4.532 -end;
     5.1 --- a/src/HOLCF/IsaMakefile	Mon Jul 12 22:17:31 2010 +0200
     5.2 +++ b/src/HOLCF/IsaMakefile	Mon Jul 12 22:35:41 2010 +0200
     5.3 @@ -166,7 +166,7 @@
     5.4    IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy		       \
     5.5    IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy		       \
     5.6    IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy      \
     5.7 -  IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/automaton.ML
     5.8 +  IOA/meta_theory/SimCorrectness.thy
     5.9  	@cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA
    5.10  
    5.11