# HG changeset patch
# User haftmann
# Date 1245751754 -7200
# Node ID 5c8cfaed32e644b4b48a8fc62671d2959c56e16d
# Parent  4d33c5d7575bcb21de9cc47b8ac8221ab85d56a2
renamed ioa to automaton

diff -r 4d33c5d7575b -r 5c8cfaed32e6 src/HOLCF/IOA/meta_theory/automaton.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/automaton.ML	Tue Jun 23 12:09:14 2009 +0200
@@ -0,0 +1,536 @@
+(*  Title:      HOLCF/IOA/meta_theory/automaton.ML
+    Author:     Tobias Hamberger, TU Muenchen
+*)
+
+signature AUTOMATON =
+sig
+  val add_ioa: string -> string
+    -> (string) list -> (string) list -> (string) list
+    -> (string * string) list -> string
+    -> (string * string * (string * string)list) list
+    -> theory -> theory
+  val add_composition : string -> (string)list -> theory -> theory
+  val add_hiding : string -> string -> (string)list -> theory -> theory
+  val add_restriction : string -> string -> (string)list -> theory -> theory
+  val add_rename : string -> string -> string -> theory -> theory
+end;
+
+structure Automaton: AUTOMATON =
+struct
+
+val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
+val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global;
+
+exception malformed;
+
+(* stripping quotes *)
+fun strip [] = [] |
+strip ("\""::r) = strip r |
+strip (a::r) = a :: (strip r);
+fun strip_quote s = implode(strip(explode(s)));
+
+(* used by *_of_varlist *)
+fun extract_first (a,b) = strip_quote a;
+fun extract_second (a,b) = strip_quote b;
+(* following functions producing sth from a varlist *)
+fun comma_list_of_varlist [] = "" |
+comma_list_of_varlist [a] = extract_first a |
+comma_list_of_varlist (a::r) = (extract_first a) ^ "," ^ (comma_list_of_varlist r);
+fun primed_comma_list_of_varlist [] = "" |
+primed_comma_list_of_varlist [a] = (extract_first a) ^ "'" |
+primed_comma_list_of_varlist (a::r) = (extract_first a) ^ "'," ^
+ (primed_comma_list_of_varlist r);
+fun type_product_of_varlist [] = "" |
+type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" |
+type_product_of_varlist(a::r) = "(" ^ extract_second(a) ^ ")*" ^ type_product_of_varlist r;
+
+(* listing a list *)
+fun list_elements_of [] = "" |
+list_elements_of (a::r) = a ^ " " ^ (list_elements_of r);
+
+(* extracting type parameters from a type list *)
+(* fun param_tupel thy [] res = res |
+param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res |
+param_tupel thy ((TFree(a,_))::r) res = 
+if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) |
+param_tupel thy (a::r) res =
+error ("one component of a statetype is a TVar: " ^ (string_of_typ thy a));
+*)
+
+(* used by constr_list *)
+fun extract_constrs thy [] = [] |
+extract_constrs thy (a::r) =
+let
+fun delete_bold [] = []
+| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
+        then (let val (_::_::_::s) = xs in delete_bold s end)
+        else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
+                then  (let val (_::_::_::s) = xs in delete_bold s end)
+                else (x::delete_bold xs));
+fun delete_bold_string s = implode(delete_bold(explode s));
+(* from a constructor term in *.induct (with quantifiers,
+"Trueprop" and ?P stripped away) delivers the head *)
+fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r |
+extract_hd (Const("Trueprop",_) $ r) = extract_hd r |
+extract_hd (Var(_,_) $ r) = extract_hd r |
+extract_hd (a $ b) = extract_hd a |
+extract_hd (Const(s,_)) = s |
+extract_hd _ = raise malformed;
+(* delivers constructor term string from a prem of *.induct *)
+fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))|
+extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r |
+extract_constr thy (Var(_,_) $ r) =  delete_bold_string(string_of_term thy r) |
+extract_constr _ _ = raise malformed;
+in
+(extract_hd a,extract_constr thy a) :: (extract_constrs thy r)
+end;
+
+(* delivering list of constructor terms of a datatype *)
+fun constr_list thy atyp =
+let
+fun act_name thy (Type(s,_)) = s |
+act_name _ s = 
+error("malformed action type: " ^ (string_of_typ thy s));
+fun afpl ("." :: a) = [] |
+afpl [] = [] |
+afpl (a::r) = a :: (afpl r);
+fun unqualify s = implode(rev(afpl(rev(explode s))));
+val q_atypstr = act_name thy atyp;
+val uq_atypstr = unqualify q_atypstr;
+val prem = prems_of (PureThy.get_thm thy (uq_atypstr ^ ".induct"));
+in
+extract_constrs thy prem
+handle malformed =>
+error("malformed theorem : " ^ uq_atypstr ^ ".induct")
+end;
+
+fun check_for_constr thy atyp (a $ b) =
+let
+fun all_free (Free(_,_)) = true |
+all_free (a $ b) = if (all_free a) then (all_free b) else false |
+all_free _ = false; 
+in 
+if (all_free b) then (check_for_constr thy atyp a) else false
+end |
+check_for_constr thy atyp (Const(a,_)) =
+let
+val cl = constr_list thy atyp;
+fun fstmem a [] = false |
+fstmem a ((f,s)::r) = if (a=f) then true else (fstmem a r)
+in
+if (fstmem a cl) then true else false
+end |
+check_for_constr _ _ _ = false;
+
+(* delivering the free variables of a constructor term *)
+fun free_vars_of (t1 $ t2) = (free_vars_of t1) @ (free_vars_of t2) |
+free_vars_of (Const(_,_)) = [] |
+free_vars_of (Free(a,_)) = [a] |
+free_vars_of _ = raise malformed;
+
+(* making a constructor set from a constructor term (of signature) *)
+fun constr_set_string thy atyp ctstr =
+let
+val trm = OldGoals.simple_read_term thy atyp ctstr;
+val l = free_vars_of trm
+in
+if (check_for_constr thy atyp trm) then
+(if (l=[]) then ("{" ^ ctstr ^ "}")
+else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})")
+else (raise malformed) 
+handle malformed => 
+error("malformed action term: " ^ (string_of_term thy trm))
+end;
+
+(* extracting constructor heads *)
+fun constructor_head thy atypstr s =
+let
+fun hd_of (Const(a,_)) = a |
+hd_of (t $ _) = hd_of t |
+hd_of _ = raise malformed;
+val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
+in
+hd_of trm handle malformed =>
+error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
+end;
+fun constructor_head_list _ _ [] = [] |
+constructor_head_list thy atypstr (a::r) =
+ (constructor_head thy atypstr a)::(constructor_head_list thy atypstr r);
+
+(* producing an action set *)
+(*FIXME*)
+fun action_set_string thy atyp [] = "Set.empty" |
+action_set_string thy atyp [a] = constr_set_string thy atyp (strip_quote a) |
+action_set_string thy atyp (a::r) = (constr_set_string thy atyp (strip_quote a)) ^
+         " Un " ^ (action_set_string thy atyp r);
+
+(* used by extend *)
+fun pstr s [] = "(" ^ s ^ "' = " ^ s ^ ")" |
+pstr s ((a,b)::r) =
+if (s=a) then ("(" ^ s ^ "' = (" ^ b ^ "))") else (pstr s r);
+fun poststring [] l = "" |
+poststring [(a,b)] l = pstr a l |
+poststring ((a,b)::r) l = (pstr a l) ^ " & " ^ (poststring r l);
+
+(* extends a (action string,condition,assignlist) tupel by a
+(action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list 
+(where bool indicates whether there is a precondition *)
+fun extend thy atyp statetupel (actstr,r,[]) =
+let
+val trm = OldGoals.simple_read_term thy atyp actstr;
+val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
+val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
+in
+if (check_for_constr thy atyp trm)
+then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag)
+else
+error("transition " ^ actstr ^ " is not a pure constructor term")
+end |
+extend thy atyp statetupel (actstr,r,(a,b)::c) =
+let
+fun pseudo_poststring [] = "" |
+pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
+pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); 
+val trm = OldGoals.simple_read_term thy atyp actstr;
+val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
+val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
+in
+if (check_for_constr thy atyp trm) then
+(if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false)
+(* the case with transrel *)
+ else 
+ (trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)),
+	"(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag))
+else
+error("transition " ^ actstr ^ " is not a pure constructor term")
+end;
+(* used by make_alt_string *) 
+fun extended_list _ _ _ [] = [] |
+extended_list thy atyp statetupel (a::r) =
+	 (extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r);
+
+(* used by write_alts *)
+fun write_alt thy (chead,tr) inp out int [] =
+if (chead mem inp) then
+(
+error("Input action " ^ tr ^ " was not specified")
+) else (
+if (chead mem (out@int)) then
+(writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else ();
+(tr ^ " => False",tr ^ " => False")) |
+write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) =
+let
+fun hd_of (Const(a,_)) = a |
+hd_of (t $ _) = hd_of t |
+hd_of _ = raise malformed;
+fun occurs_again c [] = false |
+occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r);
+in
+if (chead=(hd_of a)) then 
+(if ((chead mem inp) andalso e) then (
+error("Input action " ^ b ^ " has a precondition")
+) else (if (chead mem (inp@out@int)) then 
+		(if (occurs_again chead r) then (
+error("Two specifications for action: " ^ b)
+		) else (b ^ " => " ^ c,b ^ " => " ^ d))
+	else (
+error("Action " ^ b ^ " is not in automaton signature")
+))) else (write_alt thy (chead,ctrm) inp out int r)
+handle malformed =>
+error ("malformed action term: " ^ (string_of_term thy a))
+end;
+
+(* used by make_alt_string *)
+fun write_alts thy (a,b) inp out int [] ttr = (a,b) |
+write_alts thy (a,b) inp out int [c] ttr =
+let
+val wa = write_alt thy c inp out int ttr
+in
+ (a ^ (fst wa),b ^ (snd wa))
+end |
+write_alts thy (a,b) inp out int (c::r) ttr =
+let
+val wa = write_alt thy c inp out int ttr
+in
+ write_alts thy (a ^ (fst wa) ^ " | ", b ^ (snd wa) ^ " | ") inp out int r ttr
+end;
+
+fun make_alt_string thy inp out int atyp statetupel trans =
+let
+val cl = constr_list thy atyp;
+val ttr = extended_list thy atyp statetupel trans;
+in
+write_alts thy ("","") inp out int cl ttr
+end;
+
+(* used in add_ioa *)
+fun check_free_primed (Free(a,_)) = 
+let
+val (f::r) = rev(explode a)
+in
+if (f="'") then [a] else []
+end | 
+check_free_primed (a $ b) = ((check_free_primed a) @ (check_free_primed b)) |
+check_free_primed (Abs(_,_,t)) = check_free_primed t |
+check_free_primed _ = [];
+
+fun overlap [] _ = true |
+overlap (a::r) l = if (a mem l) then (
+error("Two occurences of action " ^ a ^ " in automaton signature")
+) else (overlap r l);
+
+(* delivering some types of an automaton *)
+fun aut_type_of thy aut_name =
+let
+fun left_of (( _ $ left) $ _) = left |
+left_of _ = raise malformed;
+val aut_def = concl_of (PureThy.get_thm thy (aut_name ^ "_def"));
+in
+(#T(rep_cterm(cterm_of thy (left_of aut_def))))
+handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
+end;
+
+fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp |
+act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^
+(string_of_typ thy t));
+fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp |
+st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^
+(string_of_typ thy t));
+
+fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) |
+comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) |
+comp_st_type_of _ _ = error "empty automaton list";
+
+(* checking consistency of action types (for composition) *)
+fun check_ac thy (a::r) =
+let
+fun ch_f_a thy acttyp [] = acttyp |
+ch_f_a thy acttyp (a::r) =
+let
+val auttyp = aut_type_of thy a;
+val ac = (act_type_of thy auttyp);
+in
+if (ac=acttyp) then (ch_f_a thy acttyp r) else (error "A")
+end;
+val auttyp = aut_type_of thy a;
+val acttyp = (act_type_of thy auttyp);
+in
+ch_f_a thy acttyp r
+end |
+check_ac _ [] = error "empty automaton list";
+
+fun clist [] = "" |
+clist [a] = a |
+clist (a::r) = a ^ " || " ^ (clist r);
+
+val add_defs = snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes o map (apfst Binding.name));
+
+
+(* add_ioa *)
+
+fun add_ioa automaton_name action_type inp out int statetupel ini trans thy =
+(writeln("Constructing automaton " ^ automaton_name ^ " ...");
+let
+val state_type_string = type_product_of_varlist(statetupel);
+val styp = Syntax.read_typ_global thy state_type_string;
+val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")";
+val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")";
+val atyp = Syntax.read_typ_global thy action_type;
+val inp_set_string = action_set_string thy atyp inp;
+val out_set_string = action_set_string thy atyp out;
+val int_set_string = action_set_string thy atyp int;
+val inp_head_list = constructor_head_list thy action_type inp;
+val out_head_list = constructor_head_list thy action_type out;
+val int_head_list = constructor_head_list thy action_type int;
+val overlap_flag = ((overlap inp out) andalso (overlap inp int) andalso (overlap out int)); 
+val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list 
+							atyp statetupel trans;
+val thy2 = (thy
+|> Sign.add_consts
+[(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn),
+(Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn),
+(Binding.name (automaton_name ^ "_trans"),
+ "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
+(Binding.name automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
+|> add_defs
+[(automaton_name ^ "_initial_def",
+automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
+(automaton_name ^ "_asig_def",
+automaton_name ^ "_asig == (" ^
+ inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"),
+(automaton_name ^ "_trans_def",
+automaton_name ^ "_trans == {(" ^
+ state_vars_tupel ^ ", act_of_" ^ automaton_name ^ ", " ^ state_vars_primed ^
+"). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"),
+(automaton_name ^ "_def",
+automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
+"_initial, " ^ automaton_name ^ "_trans,{},{})")
+])
+val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[]))
+( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
+in
+(
+if (chk_prime_list = []) then thy2
+else (
+error("Precondition or assignment terms in postconditions contain following primed variables:\n"
+ ^ (list_elements_of chk_prime_list)))
+)
+end)
+
+fun add_composition automaton_name aut_list thy =
+(writeln("Constructing automaton " ^ automaton_name ^ " ...");
+let
+val acttyp = check_ac thy aut_list; 
+val st_typ = comp_st_type_of thy aut_list; 
+val comp_list = clist aut_list;
+in
+thy
+|> Sign.add_consts_i
+[(Binding.name automaton_name,
+Type("*",
+[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
+ Type("*",[Type("set",[st_typ]),
+  Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
+   Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
+,NoSyn)]
+|> add_defs
+[(automaton_name ^ "_def",
+automaton_name ^ " == " ^ comp_list)]
+end)
+
+fun add_restriction automaton_name aut_source actlist thy =
+(writeln("Constructing automaton " ^ automaton_name ^ " ...");
+let
+val auttyp = aut_type_of thy aut_source;
+val acttyp = act_type_of thy auttyp; 
+val rest_set = action_set_string thy acttyp actlist
+in
+thy
+|> Sign.add_consts_i
+[(Binding.name automaton_name, auttyp,NoSyn)]
+|> add_defs
+[(automaton_name ^ "_def",
+automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] 
+end)
+fun add_hiding automaton_name aut_source actlist thy =
+(writeln("Constructing automaton " ^ automaton_name ^ " ...");
+let
+val auttyp = aut_type_of thy aut_source;
+val acttyp = act_type_of thy auttyp; 
+val hid_set = action_set_string thy acttyp actlist
+in
+thy
+|> Sign.add_consts_i
+[(Binding.name automaton_name, auttyp,NoSyn)]
+|> add_defs
+[(automaton_name ^ "_def",
+automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] 
+end)
+
+fun ren_act_type_of thy funct =
+  (case Term.fastype_of (Syntax.read_term_global thy funct) of
+    Type ("fun", [a, b]) => a
+  | _ => error "could not extract argument type of renaming function term");
+ 
+fun add_rename automaton_name aut_source fun_name thy =
+(writeln("Constructing automaton " ^ automaton_name ^ " ...");
+let
+val auttyp = aut_type_of thy aut_source;
+val st_typ = st_type_of thy auttyp;
+val acttyp = ren_act_type_of thy fun_name
+in
+thy
+|> Sign.add_consts_i
+[(Binding.name automaton_name,
+Type("*",
+[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
+ Type("*",[Type("set",[st_typ]),
+  Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
+   Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
+,NoSyn)]
+|> add_defs
+[(automaton_name ^ "_def",
+automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
+end)
+
+
+(** outer syntax **)
+
+(* prepare results *)
+
+(*encoding transition specifications with a element of ParseTrans*)
+datatype ParseTrans = Rel of string | PP of string*(string*string)list;
+fun mk_trans_of_rel s = Rel(s);
+fun mk_trans_of_prepost (s,l) = PP(s,l); 
+
+fun trans_of (a, Rel b) = (a, b, [("", "")])
+  | trans_of (a, PP (b, l)) = (a, b, l);
+
+
+fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) =
+  add_ioa aut action_type inp out int states initial (map trans_of trans);
+
+fun mk_composition_decl (aut, autlist) =
+  add_composition aut autlist;
+
+fun mk_hiding_decl (aut, (actlist, source_aut)) =
+  add_hiding aut source_aut actlist;
+
+fun mk_restriction_decl (aut, (source_aut, actlist)) =
+  add_restriction aut source_aut actlist;
+
+fun mk_rename_decl (aut, (source_aut, rename_f)) =
+  add_rename aut source_aut rename_f;
+
+
+(* outer syntax *)
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs",
+  "outputs", "internals", "states", "initially", "transitions", "pre",
+  "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
+  "rename"];
+
+val actionlist = P.list1 P.term;
+val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
+val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
+val internalslist = P.$$$ "internals" |-- P.!!! actionlist;
+val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ));
+val initial = P.$$$ "initially" |-- P.!!! P.term;
+val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term);
+val pre = P.$$$ "pre" |-- P.!!! P.term;
+val post = P.$$$ "post" |-- P.!!! assign_list;
+val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost;
+val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost;
+val transrel =  (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel;
+val transition = P.term -- (transrel || pre1 || post1);
+val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition);
+
+val ioa_decl =
+  (P.name -- (P.$$$ "=" |--
+    (P.$$$ "signature" |--
+      P.!!! (P.$$$ "actions" |--
+        (P.typ --
+          (Scan.optional inputslist []) --
+          (Scan.optional outputslist []) --
+          (Scan.optional internalslist []) --
+          stateslist --
+          (Scan.optional initial "True") --
+        translist))))) >> mk_ioa_decl ||
+  (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name))))
+    >> mk_composition_decl ||
+  (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |--
+      P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl ||
+  (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |--
+      P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl ||
+  (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
+    >> mk_rename_decl;
+
+val _ =
+  OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
+    (ioa_decl >> Toplevel.theory);
+
+end;
+
+end;
diff -r 4d33c5d7575b -r 5c8cfaed32e6 src/HOLCF/IOA/meta_theory/ioa.ML
--- a/src/HOLCF/IOA/meta_theory/ioa.ML	Tue Jun 23 12:08:35 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,536 +0,0 @@
-(*  Title:      HOLCF/IOA/meta_theory/ioa.ML
-    Author:     Tobias Hamberger, TU Muenchen
-*)
-
-signature IOA =
-sig
-  val add_ioa: string -> string
-    -> (string) list -> (string) list -> (string) list
-    -> (string * string) list -> string
-    -> (string * string * (string * string)list) list
-    -> theory -> theory
-  val add_composition : string -> (string)list -> theory -> theory
-  val add_hiding : string -> string -> (string)list -> theory -> theory
-  val add_restriction : string -> string -> (string)list -> theory -> theory
-  val add_rename : string -> string -> string -> theory -> theory
-end;
-
-structure Ioa: IOA =
-struct
-
-val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
-val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global;
-
-exception malformed;
-
-(* stripping quotes *)
-fun strip [] = [] |
-strip ("\""::r) = strip r |
-strip (a::r) = a :: (strip r);
-fun strip_quote s = implode(strip(explode(s)));
-
-(* used by *_of_varlist *)
-fun extract_first (a,b) = strip_quote a;
-fun extract_second (a,b) = strip_quote b;
-(* following functions producing sth from a varlist *)
-fun comma_list_of_varlist [] = "" |
-comma_list_of_varlist [a] = extract_first a |
-comma_list_of_varlist (a::r) = (extract_first a) ^ "," ^ (comma_list_of_varlist r);
-fun primed_comma_list_of_varlist [] = "" |
-primed_comma_list_of_varlist [a] = (extract_first a) ^ "'" |
-primed_comma_list_of_varlist (a::r) = (extract_first a) ^ "'," ^
- (primed_comma_list_of_varlist r);
-fun type_product_of_varlist [] = "" |
-type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" |
-type_product_of_varlist(a::r) = "(" ^ extract_second(a) ^ ")*" ^ type_product_of_varlist r;
-
-(* listing a list *)
-fun list_elements_of [] = "" |
-list_elements_of (a::r) = a ^ " " ^ (list_elements_of r);
-
-(* extracting type parameters from a type list *)
-(* fun param_tupel thy [] res = res |
-param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res |
-param_tupel thy ((TFree(a,_))::r) res = 
-if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) |
-param_tupel thy (a::r) res =
-error ("one component of a statetype is a TVar: " ^ (string_of_typ thy a));
-*)
-
-(* used by constr_list *)
-fun extract_constrs thy [] = [] |
-extract_constrs thy (a::r) =
-let
-fun delete_bold [] = []
-| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
-        then (let val (_::_::_::s) = xs in delete_bold s end)
-        else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
-                then  (let val (_::_::_::s) = xs in delete_bold s end)
-                else (x::delete_bold xs));
-fun delete_bold_string s = implode(delete_bold(explode s));
-(* from a constructor term in *.induct (with quantifiers,
-"Trueprop" and ?P stripped away) delivers the head *)
-fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r |
-extract_hd (Const("Trueprop",_) $ r) = extract_hd r |
-extract_hd (Var(_,_) $ r) = extract_hd r |
-extract_hd (a $ b) = extract_hd a |
-extract_hd (Const(s,_)) = s |
-extract_hd _ = raise malformed;
-(* delivers constructor term string from a prem of *.induct *)
-fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))|
-extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r |
-extract_constr thy (Var(_,_) $ r) =  delete_bold_string(string_of_term thy r) |
-extract_constr _ _ = raise malformed;
-in
-(extract_hd a,extract_constr thy a) :: (extract_constrs thy r)
-end;
-
-(* delivering list of constructor terms of a datatype *)
-fun constr_list thy atyp =
-let
-fun act_name thy (Type(s,_)) = s |
-act_name _ s = 
-error("malformed action type: " ^ (string_of_typ thy s));
-fun afpl ("." :: a) = [] |
-afpl [] = [] |
-afpl (a::r) = a :: (afpl r);
-fun unqualify s = implode(rev(afpl(rev(explode s))));
-val q_atypstr = act_name thy atyp;
-val uq_atypstr = unqualify q_atypstr;
-val prem = prems_of (PureThy.get_thm thy (uq_atypstr ^ ".induct"));
-in
-extract_constrs thy prem
-handle malformed =>
-error("malformed theorem : " ^ uq_atypstr ^ ".induct")
-end;
-
-fun check_for_constr thy atyp (a $ b) =
-let
-fun all_free (Free(_,_)) = true |
-all_free (a $ b) = if (all_free a) then (all_free b) else false |
-all_free _ = false; 
-in 
-if (all_free b) then (check_for_constr thy atyp a) else false
-end |
-check_for_constr thy atyp (Const(a,_)) =
-let
-val cl = constr_list thy atyp;
-fun fstmem a [] = false |
-fstmem a ((f,s)::r) = if (a=f) then true else (fstmem a r)
-in
-if (fstmem a cl) then true else false
-end |
-check_for_constr _ _ _ = false;
-
-(* delivering the free variables of a constructor term *)
-fun free_vars_of (t1 $ t2) = (free_vars_of t1) @ (free_vars_of t2) |
-free_vars_of (Const(_,_)) = [] |
-free_vars_of (Free(a,_)) = [a] |
-free_vars_of _ = raise malformed;
-
-(* making a constructor set from a constructor term (of signature) *)
-fun constr_set_string thy atyp ctstr =
-let
-val trm = OldGoals.simple_read_term thy atyp ctstr;
-val l = free_vars_of trm
-in
-if (check_for_constr thy atyp trm) then
-(if (l=[]) then ("{" ^ ctstr ^ "}")
-else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})")
-else (raise malformed) 
-handle malformed => 
-error("malformed action term: " ^ (string_of_term thy trm))
-end;
-
-(* extracting constructor heads *)
-fun constructor_head thy atypstr s =
-let
-fun hd_of (Const(a,_)) = a |
-hd_of (t $ _) = hd_of t |
-hd_of _ = raise malformed;
-val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
-in
-hd_of trm handle malformed =>
-error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
-end;
-fun constructor_head_list _ _ [] = [] |
-constructor_head_list thy atypstr (a::r) =
- (constructor_head thy atypstr a)::(constructor_head_list thy atypstr r);
-
-(* producing an action set *)
-(*FIXME*)
-fun action_set_string thy atyp [] = "Set.empty" |
-action_set_string thy atyp [a] = constr_set_string thy atyp (strip_quote a) |
-action_set_string thy atyp (a::r) = (constr_set_string thy atyp (strip_quote a)) ^
-         " Un " ^ (action_set_string thy atyp r);
-
-(* used by extend *)
-fun pstr s [] = "(" ^ s ^ "' = " ^ s ^ ")" |
-pstr s ((a,b)::r) =
-if (s=a) then ("(" ^ s ^ "' = (" ^ b ^ "))") else (pstr s r);
-fun poststring [] l = "" |
-poststring [(a,b)] l = pstr a l |
-poststring ((a,b)::r) l = (pstr a l) ^ " & " ^ (poststring r l);
-
-(* extends a (action string,condition,assignlist) tupel by a
-(action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list 
-(where bool indicates whether there is a precondition *)
-fun extend thy atyp statetupel (actstr,r,[]) =
-let
-val trm = OldGoals.simple_read_term thy atyp actstr;
-val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
-val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
-in
-if (check_for_constr thy atyp trm)
-then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag)
-else
-error("transition " ^ actstr ^ " is not a pure constructor term")
-end |
-extend thy atyp statetupel (actstr,r,(a,b)::c) =
-let
-fun pseudo_poststring [] = "" |
-pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
-pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); 
-val trm = OldGoals.simple_read_term thy atyp actstr;
-val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
-val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
-in
-if (check_for_constr thy atyp trm) then
-(if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false)
-(* the case with transrel *)
- else 
- (trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)),
-	"(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag))
-else
-error("transition " ^ actstr ^ " is not a pure constructor term")
-end;
-(* used by make_alt_string *) 
-fun extended_list _ _ _ [] = [] |
-extended_list thy atyp statetupel (a::r) =
-	 (extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r);
-
-(* used by write_alts *)
-fun write_alt thy (chead,tr) inp out int [] =
-if (chead mem inp) then
-(
-error("Input action " ^ tr ^ " was not specified")
-) else (
-if (chead mem (out@int)) then
-(writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else ();
-(tr ^ " => False",tr ^ " => False")) |
-write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) =
-let
-fun hd_of (Const(a,_)) = a |
-hd_of (t $ _) = hd_of t |
-hd_of _ = raise malformed;
-fun occurs_again c [] = false |
-occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r);
-in
-if (chead=(hd_of a)) then 
-(if ((chead mem inp) andalso e) then (
-error("Input action " ^ b ^ " has a precondition")
-) else (if (chead mem (inp@out@int)) then 
-		(if (occurs_again chead r) then (
-error("Two specifications for action: " ^ b)
-		) else (b ^ " => " ^ c,b ^ " => " ^ d))
-	else (
-error("Action " ^ b ^ " is not in automaton signature")
-))) else (write_alt thy (chead,ctrm) inp out int r)
-handle malformed =>
-error ("malformed action term: " ^ (string_of_term thy a))
-end;
-
-(* used by make_alt_string *)
-fun write_alts thy (a,b) inp out int [] ttr = (a,b) |
-write_alts thy (a,b) inp out int [c] ttr =
-let
-val wa = write_alt thy c inp out int ttr
-in
- (a ^ (fst wa),b ^ (snd wa))
-end |
-write_alts thy (a,b) inp out int (c::r) ttr =
-let
-val wa = write_alt thy c inp out int ttr
-in
- write_alts thy (a ^ (fst wa) ^ " | ", b ^ (snd wa) ^ " | ") inp out int r ttr
-end;
-
-fun make_alt_string thy inp out int atyp statetupel trans =
-let
-val cl = constr_list thy atyp;
-val ttr = extended_list thy atyp statetupel trans;
-in
-write_alts thy ("","") inp out int cl ttr
-end;
-
-(* used in add_ioa *)
-fun check_free_primed (Free(a,_)) = 
-let
-val (f::r) = rev(explode a)
-in
-if (f="'") then [a] else []
-end | 
-check_free_primed (a $ b) = ((check_free_primed a) @ (check_free_primed b)) |
-check_free_primed (Abs(_,_,t)) = check_free_primed t |
-check_free_primed _ = [];
-
-fun overlap [] _ = true |
-overlap (a::r) l = if (a mem l) then (
-error("Two occurences of action " ^ a ^ " in automaton signature")
-) else (overlap r l);
-
-(* delivering some types of an automaton *)
-fun aut_type_of thy aut_name =
-let
-fun left_of (( _ $ left) $ _) = left |
-left_of _ = raise malformed;
-val aut_def = concl_of (PureThy.get_thm thy (aut_name ^ "_def"));
-in
-(#T(rep_cterm(cterm_of thy (left_of aut_def))))
-handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
-end;
-
-fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp |
-act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^
-(string_of_typ thy t));
-fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp |
-st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^
-(string_of_typ thy t));
-
-fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) |
-comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) |
-comp_st_type_of _ _ = error "empty automaton list";
-
-(* checking consistency of action types (for composition) *)
-fun check_ac thy (a::r) =
-let
-fun ch_f_a thy acttyp [] = acttyp |
-ch_f_a thy acttyp (a::r) =
-let
-val auttyp = aut_type_of thy a;
-val ac = (act_type_of thy auttyp);
-in
-if (ac=acttyp) then (ch_f_a thy acttyp r) else (error "A")
-end;
-val auttyp = aut_type_of thy a;
-val acttyp = (act_type_of thy auttyp);
-in
-ch_f_a thy acttyp r
-end |
-check_ac _ [] = error "empty automaton list";
-
-fun clist [] = "" |
-clist [a] = a |
-clist (a::r) = a ^ " || " ^ (clist r);
-
-val add_defs = snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes o map (apfst Binding.name));
-
-
-(* add_ioa *)
-
-fun add_ioa automaton_name action_type inp out int statetupel ini trans thy =
-(writeln("Constructing automaton " ^ automaton_name ^ " ...");
-let
-val state_type_string = type_product_of_varlist(statetupel);
-val styp = Syntax.read_typ_global thy state_type_string;
-val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")";
-val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")";
-val atyp = Syntax.read_typ_global thy action_type;
-val inp_set_string = action_set_string thy atyp inp;
-val out_set_string = action_set_string thy atyp out;
-val int_set_string = action_set_string thy atyp int;
-val inp_head_list = constructor_head_list thy action_type inp;
-val out_head_list = constructor_head_list thy action_type out;
-val int_head_list = constructor_head_list thy action_type int;
-val overlap_flag = ((overlap inp out) andalso (overlap inp int) andalso (overlap out int)); 
-val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list 
-							atyp statetupel trans;
-val thy2 = (thy
-|> Sign.add_consts
-[(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn),
-(Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn),
-(Binding.name (automaton_name ^ "_trans"),
- "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
-(Binding.name automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
-|> add_defs
-[(automaton_name ^ "_initial_def",
-automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
-(automaton_name ^ "_asig_def",
-automaton_name ^ "_asig == (" ^
- inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"),
-(automaton_name ^ "_trans_def",
-automaton_name ^ "_trans == {(" ^
- state_vars_tupel ^ ", act_of_" ^ automaton_name ^ ", " ^ state_vars_primed ^
-"). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"),
-(automaton_name ^ "_def",
-automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
-"_initial, " ^ automaton_name ^ "_trans,{},{})")
-])
-val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[]))
-( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
-in
-(
-if (chk_prime_list = []) then thy2
-else (
-error("Precondition or assignment terms in postconditions contain following primed variables:\n"
- ^ (list_elements_of chk_prime_list)))
-)
-end)
-
-fun add_composition automaton_name aut_list thy =
-(writeln("Constructing automaton " ^ automaton_name ^ " ...");
-let
-val acttyp = check_ac thy aut_list; 
-val st_typ = comp_st_type_of thy aut_list; 
-val comp_list = clist aut_list;
-in
-thy
-|> Sign.add_consts_i
-[(Binding.name automaton_name,
-Type("*",
-[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
- Type("*",[Type("set",[st_typ]),
-  Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
-   Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
-,NoSyn)]
-|> add_defs
-[(automaton_name ^ "_def",
-automaton_name ^ " == " ^ comp_list)]
-end)
-
-fun add_restriction automaton_name aut_source actlist thy =
-(writeln("Constructing automaton " ^ automaton_name ^ " ...");
-let
-val auttyp = aut_type_of thy aut_source;
-val acttyp = act_type_of thy auttyp; 
-val rest_set = action_set_string thy acttyp actlist
-in
-thy
-|> Sign.add_consts_i
-[(Binding.name automaton_name, auttyp,NoSyn)]
-|> add_defs
-[(automaton_name ^ "_def",
-automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] 
-end)
-fun add_hiding automaton_name aut_source actlist thy =
-(writeln("Constructing automaton " ^ automaton_name ^ " ...");
-let
-val auttyp = aut_type_of thy aut_source;
-val acttyp = act_type_of thy auttyp; 
-val hid_set = action_set_string thy acttyp actlist
-in
-thy
-|> Sign.add_consts_i
-[(Binding.name automaton_name, auttyp,NoSyn)]
-|> add_defs
-[(automaton_name ^ "_def",
-automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] 
-end)
-
-fun ren_act_type_of thy funct =
-  (case Term.fastype_of (Syntax.read_term_global thy funct) of
-    Type ("fun", [a, b]) => a
-  | _ => error "could not extract argument type of renaming function term");
- 
-fun add_rename automaton_name aut_source fun_name thy =
-(writeln("Constructing automaton " ^ automaton_name ^ " ...");
-let
-val auttyp = aut_type_of thy aut_source;
-val st_typ = st_type_of thy auttyp;
-val acttyp = ren_act_type_of thy fun_name
-in
-thy
-|> Sign.add_consts_i
-[(Binding.name automaton_name,
-Type("*",
-[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
- Type("*",[Type("set",[st_typ]),
-  Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
-   Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
-,NoSyn)]
-|> add_defs
-[(automaton_name ^ "_def",
-automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
-end)
-
-
-(** outer syntax **)
-
-(* prepare results *)
-
-(*encoding transition specifications with a element of ParseTrans*)
-datatype ParseTrans = Rel of string | PP of string*(string*string)list;
-fun mk_trans_of_rel s = Rel(s);
-fun mk_trans_of_prepost (s,l) = PP(s,l); 
-
-fun trans_of (a, Rel b) = (a, b, [("", "")])
-  | trans_of (a, PP (b, l)) = (a, b, l);
-
-
-fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) =
-  add_ioa aut action_type inp out int states initial (map trans_of trans);
-
-fun mk_composition_decl (aut, autlist) =
-  add_composition aut autlist;
-
-fun mk_hiding_decl (aut, (actlist, source_aut)) =
-  add_hiding aut source_aut actlist;
-
-fun mk_restriction_decl (aut, (source_aut, actlist)) =
-  add_restriction aut source_aut actlist;
-
-fun mk_rename_decl (aut, (source_aut, rename_f)) =
-  add_rename aut source_aut rename_f;
-
-
-(* outer syntax *)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs",
-  "outputs", "internals", "states", "initially", "transitions", "pre",
-  "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
-  "rename"];
-
-val actionlist = P.list1 P.term;
-val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
-val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
-val internalslist = P.$$$ "internals" |-- P.!!! actionlist;
-val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ));
-val initial = P.$$$ "initially" |-- P.!!! P.term;
-val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term);
-val pre = P.$$$ "pre" |-- P.!!! P.term;
-val post = P.$$$ "post" |-- P.!!! assign_list;
-val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost;
-val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost;
-val transrel =  (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel;
-val transition = P.term -- (transrel || pre1 || post1);
-val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition);
-
-val ioa_decl =
-  (P.name -- (P.$$$ "=" |--
-    (P.$$$ "signature" |--
-      P.!!! (P.$$$ "actions" |--
-        (P.typ --
-          (Scan.optional inputslist []) --
-          (Scan.optional outputslist []) --
-          (Scan.optional internalslist []) --
-          stateslist --
-          (Scan.optional initial "True") --
-        translist))))) >> mk_ioa_decl ||
-  (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name))))
-    >> mk_composition_decl ||
-  (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |--
-      P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl ||
-  (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |--
-      P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl ||
-  (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
-    >> mk_rename_decl;
-
-val _ =
-  OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
-    (ioa_decl >> Toplevel.theory);
-
-end;
-
-end;