discontinued ancient tradition to suffix certain ML module names with "_package"
authorhaftmann
Sun Jun 21 15:45:57 2009 +0200 (2009-06-21)
changeset 31740002da20f442e
parent 31739 8155c4d94354
child 31741 41788a3ffd6a
discontinued ancient tradition to suffix certain ML module names with "_package"
src/HOLCF/IOA/meta_theory/ioa.ML
src/HOLCF/IOA/meta_theory/ioa_package.ML
src/HOLCF/Tools/fixrec.ML
src/HOLCF/Tools/fixrec_package.ML
src/HOLCF/Tools/pcpodef.ML
src/HOLCF/Tools/pcpodef_package.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/IOA/meta_theory/ioa.ML	Sun Jun 21 15:45:57 2009 +0200
     1.3 @@ -0,0 +1,536 @@
     1.4 +(*  Title:      HOLCF/IOA/meta_theory/ioa.ML
     1.5 +    Author:     Tobias Hamberger, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +signature IOA =
     1.9 +sig
    1.10 +  val add_ioa: string -> string
    1.11 +    -> (string) list -> (string) list -> (string) list
    1.12 +    -> (string * string) list -> string
    1.13 +    -> (string * string * (string * string)list) list
    1.14 +    -> theory -> theory
    1.15 +  val add_composition : string -> (string)list -> theory -> theory
    1.16 +  val add_hiding : string -> string -> (string)list -> theory -> theory
    1.17 +  val add_restriction : string -> string -> (string)list -> theory -> theory
    1.18 +  val add_rename : string -> string -> string -> theory -> theory
    1.19 +end;
    1.20 +
    1.21 +structure Ioa: IOA =
    1.22 +struct
    1.23 +
    1.24 +val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
    1.25 +val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global;
    1.26 +
    1.27 +exception malformed;
    1.28 +
    1.29 +(* stripping quotes *)
    1.30 +fun strip [] = [] |
    1.31 +strip ("\""::r) = strip r |
    1.32 +strip (a::r) = a :: (strip r);
    1.33 +fun strip_quote s = implode(strip(explode(s)));
    1.34 +
    1.35 +(* used by *_of_varlist *)
    1.36 +fun extract_first (a,b) = strip_quote a;
    1.37 +fun extract_second (a,b) = strip_quote b;
    1.38 +(* following functions producing sth from a varlist *)
    1.39 +fun comma_list_of_varlist [] = "" |
    1.40 +comma_list_of_varlist [a] = extract_first a |
    1.41 +comma_list_of_varlist (a::r) = (extract_first a) ^ "," ^ (comma_list_of_varlist r);
    1.42 +fun primed_comma_list_of_varlist [] = "" |
    1.43 +primed_comma_list_of_varlist [a] = (extract_first a) ^ "'" |
    1.44 +primed_comma_list_of_varlist (a::r) = (extract_first a) ^ "'," ^
    1.45 + (primed_comma_list_of_varlist r);
    1.46 +fun type_product_of_varlist [] = "" |
    1.47 +type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" |
    1.48 +type_product_of_varlist(a::r) = "(" ^ extract_second(a) ^ ")*" ^ type_product_of_varlist r;
    1.49 +
    1.50 +(* listing a list *)
    1.51 +fun list_elements_of [] = "" |
    1.52 +list_elements_of (a::r) = a ^ " " ^ (list_elements_of r);
    1.53 +
    1.54 +(* extracting type parameters from a type list *)
    1.55 +(* fun param_tupel thy [] res = res |
    1.56 +param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res |
    1.57 +param_tupel thy ((TFree(a,_))::r) res = 
    1.58 +if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) |
    1.59 +param_tupel thy (a::r) res =
    1.60 +error ("one component of a statetype is a TVar: " ^ (string_of_typ thy a));
    1.61 +*)
    1.62 +
    1.63 +(* used by constr_list *)
    1.64 +fun extract_constrs thy [] = [] |
    1.65 +extract_constrs thy (a::r) =
    1.66 +let
    1.67 +fun delete_bold [] = []
    1.68 +| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
    1.69 +        then (let val (_::_::_::s) = xs in delete_bold s end)
    1.70 +        else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
    1.71 +                then  (let val (_::_::_::s) = xs in delete_bold s end)
    1.72 +                else (x::delete_bold xs));
    1.73 +fun delete_bold_string s = implode(delete_bold(explode s));
    1.74 +(* from a constructor term in *.induct (with quantifiers,
    1.75 +"Trueprop" and ?P stripped away) delivers the head *)
    1.76 +fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r |
    1.77 +extract_hd (Const("Trueprop",_) $ r) = extract_hd r |
    1.78 +extract_hd (Var(_,_) $ r) = extract_hd r |
    1.79 +extract_hd (a $ b) = extract_hd a |
    1.80 +extract_hd (Const(s,_)) = s |
    1.81 +extract_hd _ = raise malformed;
    1.82 +(* delivers constructor term string from a prem of *.induct *)
    1.83 +fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))|
    1.84 +extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r |
    1.85 +extract_constr thy (Var(_,_) $ r) =  delete_bold_string(string_of_term thy r) |
    1.86 +extract_constr _ _ = raise malformed;
    1.87 +in
    1.88 +(extract_hd a,extract_constr thy a) :: (extract_constrs thy r)
    1.89 +end;
    1.90 +
    1.91 +(* delivering list of constructor terms of a datatype *)
    1.92 +fun constr_list thy atyp =
    1.93 +let
    1.94 +fun act_name thy (Type(s,_)) = s |
    1.95 +act_name _ s = 
    1.96 +error("malformed action type: " ^ (string_of_typ thy s));
    1.97 +fun afpl ("." :: a) = [] |
    1.98 +afpl [] = [] |
    1.99 +afpl (a::r) = a :: (afpl r);
   1.100 +fun unqualify s = implode(rev(afpl(rev(explode s))));
   1.101 +val q_atypstr = act_name thy atyp;
   1.102 +val uq_atypstr = unqualify q_atypstr;
   1.103 +val prem = prems_of (PureThy.get_thm thy (uq_atypstr ^ ".induct"));
   1.104 +in
   1.105 +extract_constrs thy prem
   1.106 +handle malformed =>
   1.107 +error("malformed theorem : " ^ uq_atypstr ^ ".induct")
   1.108 +end;
   1.109 +
   1.110 +fun check_for_constr thy atyp (a $ b) =
   1.111 +let
   1.112 +fun all_free (Free(_,_)) = true |
   1.113 +all_free (a $ b) = if (all_free a) then (all_free b) else false |
   1.114 +all_free _ = false; 
   1.115 +in 
   1.116 +if (all_free b) then (check_for_constr thy atyp a) else false
   1.117 +end |
   1.118 +check_for_constr thy atyp (Const(a,_)) =
   1.119 +let
   1.120 +val cl = constr_list thy atyp;
   1.121 +fun fstmem a [] = false |
   1.122 +fstmem a ((f,s)::r) = if (a=f) then true else (fstmem a r)
   1.123 +in
   1.124 +if (fstmem a cl) then true else false
   1.125 +end |
   1.126 +check_for_constr _ _ _ = false;
   1.127 +
   1.128 +(* delivering the free variables of a constructor term *)
   1.129 +fun free_vars_of (t1 $ t2) = (free_vars_of t1) @ (free_vars_of t2) |
   1.130 +free_vars_of (Const(_,_)) = [] |
   1.131 +free_vars_of (Free(a,_)) = [a] |
   1.132 +free_vars_of _ = raise malformed;
   1.133 +
   1.134 +(* making a constructor set from a constructor term (of signature) *)
   1.135 +fun constr_set_string thy atyp ctstr =
   1.136 +let
   1.137 +val trm = OldGoals.simple_read_term thy atyp ctstr;
   1.138 +val l = free_vars_of trm
   1.139 +in
   1.140 +if (check_for_constr thy atyp trm) then
   1.141 +(if (l=[]) then ("{" ^ ctstr ^ "}")
   1.142 +else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})")
   1.143 +else (raise malformed) 
   1.144 +handle malformed => 
   1.145 +error("malformed action term: " ^ (string_of_term thy trm))
   1.146 +end;
   1.147 +
   1.148 +(* extracting constructor heads *)
   1.149 +fun constructor_head thy atypstr s =
   1.150 +let
   1.151 +fun hd_of (Const(a,_)) = a |
   1.152 +hd_of (t $ _) = hd_of t |
   1.153 +hd_of _ = raise malformed;
   1.154 +val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
   1.155 +in
   1.156 +hd_of trm handle malformed =>
   1.157 +error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
   1.158 +end;
   1.159 +fun constructor_head_list _ _ [] = [] |
   1.160 +constructor_head_list thy atypstr (a::r) =
   1.161 + (constructor_head thy atypstr a)::(constructor_head_list thy atypstr r);
   1.162 +
   1.163 +(* producing an action set *)
   1.164 +(*FIXME*)
   1.165 +fun action_set_string thy atyp [] = "Set.empty" |
   1.166 +action_set_string thy atyp [a] = constr_set_string thy atyp (strip_quote a) |
   1.167 +action_set_string thy atyp (a::r) = (constr_set_string thy atyp (strip_quote a)) ^
   1.168 +         " Un " ^ (action_set_string thy atyp r);
   1.169 +
   1.170 +(* used by extend *)
   1.171 +fun pstr s [] = "(" ^ s ^ "' = " ^ s ^ ")" |
   1.172 +pstr s ((a,b)::r) =
   1.173 +if (s=a) then ("(" ^ s ^ "' = (" ^ b ^ "))") else (pstr s r);
   1.174 +fun poststring [] l = "" |
   1.175 +poststring [(a,b)] l = pstr a l |
   1.176 +poststring ((a,b)::r) l = (pstr a l) ^ " & " ^ (poststring r l);
   1.177 +
   1.178 +(* extends a (action string,condition,assignlist) tupel by a
   1.179 +(action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list 
   1.180 +(where bool indicates whether there is a precondition *)
   1.181 +fun extend thy atyp statetupel (actstr,r,[]) =
   1.182 +let
   1.183 +val trm = OldGoals.simple_read_term thy atyp actstr;
   1.184 +val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
   1.185 +val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
   1.186 +in
   1.187 +if (check_for_constr thy atyp trm)
   1.188 +then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag)
   1.189 +else
   1.190 +error("transition " ^ actstr ^ " is not a pure constructor term")
   1.191 +end |
   1.192 +extend thy atyp statetupel (actstr,r,(a,b)::c) =
   1.193 +let
   1.194 +fun pseudo_poststring [] = "" |
   1.195 +pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
   1.196 +pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); 
   1.197 +val trm = OldGoals.simple_read_term thy atyp actstr;
   1.198 +val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
   1.199 +val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
   1.200 +in
   1.201 +if (check_for_constr thy atyp trm) then
   1.202 +(if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false)
   1.203 +(* the case with transrel *)
   1.204 + else 
   1.205 + (trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)),
   1.206 +	"(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag))
   1.207 +else
   1.208 +error("transition " ^ actstr ^ " is not a pure constructor term")
   1.209 +end;
   1.210 +(* used by make_alt_string *) 
   1.211 +fun extended_list _ _ _ [] = [] |
   1.212 +extended_list thy atyp statetupel (a::r) =
   1.213 +	 (extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r);
   1.214 +
   1.215 +(* used by write_alts *)
   1.216 +fun write_alt thy (chead,tr) inp out int [] =
   1.217 +if (chead mem inp) then
   1.218 +(
   1.219 +error("Input action " ^ tr ^ " was not specified")
   1.220 +) else (
   1.221 +if (chead mem (out@int)) then
   1.222 +(writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else ();
   1.223 +(tr ^ " => False",tr ^ " => False")) |
   1.224 +write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) =
   1.225 +let
   1.226 +fun hd_of (Const(a,_)) = a |
   1.227 +hd_of (t $ _) = hd_of t |
   1.228 +hd_of _ = raise malformed;
   1.229 +fun occurs_again c [] = false |
   1.230 +occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r);
   1.231 +in
   1.232 +if (chead=(hd_of a)) then 
   1.233 +(if ((chead mem inp) andalso e) then (
   1.234 +error("Input action " ^ b ^ " has a precondition")
   1.235 +) else (if (chead mem (inp@out@int)) then 
   1.236 +		(if (occurs_again chead r) then (
   1.237 +error("Two specifications for action: " ^ b)
   1.238 +		) else (b ^ " => " ^ c,b ^ " => " ^ d))
   1.239 +	else (
   1.240 +error("Action " ^ b ^ " is not in automaton signature")
   1.241 +))) else (write_alt thy (chead,ctrm) inp out int r)
   1.242 +handle malformed =>
   1.243 +error ("malformed action term: " ^ (string_of_term thy a))
   1.244 +end;
   1.245 +
   1.246 +(* used by make_alt_string *)
   1.247 +fun write_alts thy (a,b) inp out int [] ttr = (a,b) |
   1.248 +write_alts thy (a,b) inp out int [c] ttr =
   1.249 +let
   1.250 +val wa = write_alt thy c inp out int ttr
   1.251 +in
   1.252 + (a ^ (fst wa),b ^ (snd wa))
   1.253 +end |
   1.254 +write_alts thy (a,b) inp out int (c::r) ttr =
   1.255 +let
   1.256 +val wa = write_alt thy c inp out int ttr
   1.257 +in
   1.258 + write_alts thy (a ^ (fst wa) ^ " | ", b ^ (snd wa) ^ " | ") inp out int r ttr
   1.259 +end;
   1.260 +
   1.261 +fun make_alt_string thy inp out int atyp statetupel trans =
   1.262 +let
   1.263 +val cl = constr_list thy atyp;
   1.264 +val ttr = extended_list thy atyp statetupel trans;
   1.265 +in
   1.266 +write_alts thy ("","") inp out int cl ttr
   1.267 +end;
   1.268 +
   1.269 +(* used in add_ioa *)
   1.270 +fun check_free_primed (Free(a,_)) = 
   1.271 +let
   1.272 +val (f::r) = rev(explode a)
   1.273 +in
   1.274 +if (f="'") then [a] else []
   1.275 +end | 
   1.276 +check_free_primed (a $ b) = ((check_free_primed a) @ (check_free_primed b)) |
   1.277 +check_free_primed (Abs(_,_,t)) = check_free_primed t |
   1.278 +check_free_primed _ = [];
   1.279 +
   1.280 +fun overlap [] _ = true |
   1.281 +overlap (a::r) l = if (a mem l) then (
   1.282 +error("Two occurences of action " ^ a ^ " in automaton signature")
   1.283 +) else (overlap r l);
   1.284 +
   1.285 +(* delivering some types of an automaton *)
   1.286 +fun aut_type_of thy aut_name =
   1.287 +let
   1.288 +fun left_of (( _ $ left) $ _) = left |
   1.289 +left_of _ = raise malformed;
   1.290 +val aut_def = concl_of (PureThy.get_thm thy (aut_name ^ "_def"));
   1.291 +in
   1.292 +(#T(rep_cterm(cterm_of thy (left_of aut_def))))
   1.293 +handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
   1.294 +end;
   1.295 +
   1.296 +fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp |
   1.297 +act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^
   1.298 +(string_of_typ thy t));
   1.299 +fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp |
   1.300 +st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^
   1.301 +(string_of_typ thy t));
   1.302 +
   1.303 +fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) |
   1.304 +comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) |
   1.305 +comp_st_type_of _ _ = error "empty automaton list";
   1.306 +
   1.307 +(* checking consistency of action types (for composition) *)
   1.308 +fun check_ac thy (a::r) =
   1.309 +let
   1.310 +fun ch_f_a thy acttyp [] = acttyp |
   1.311 +ch_f_a thy acttyp (a::r) =
   1.312 +let
   1.313 +val auttyp = aut_type_of thy a;
   1.314 +val ac = (act_type_of thy auttyp);
   1.315 +in
   1.316 +if (ac=acttyp) then (ch_f_a thy acttyp r) else (error "A")
   1.317 +end;
   1.318 +val auttyp = aut_type_of thy a;
   1.319 +val acttyp = (act_type_of thy auttyp);
   1.320 +in
   1.321 +ch_f_a thy acttyp r
   1.322 +end |
   1.323 +check_ac _ [] = error "empty automaton list";
   1.324 +
   1.325 +fun clist [] = "" |
   1.326 +clist [a] = a |
   1.327 +clist (a::r) = a ^ " || " ^ (clist r);
   1.328 +
   1.329 +val add_defs = snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes o map (apfst Binding.name));
   1.330 +
   1.331 +
   1.332 +(* add_ioa *)
   1.333 +
   1.334 +fun add_ioa automaton_name action_type inp out int statetupel ini trans thy =
   1.335 +(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   1.336 +let
   1.337 +val state_type_string = type_product_of_varlist(statetupel);
   1.338 +val styp = Syntax.read_typ_global thy state_type_string;
   1.339 +val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")";
   1.340 +val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")";
   1.341 +val atyp = Syntax.read_typ_global thy action_type;
   1.342 +val inp_set_string = action_set_string thy atyp inp;
   1.343 +val out_set_string = action_set_string thy atyp out;
   1.344 +val int_set_string = action_set_string thy atyp int;
   1.345 +val inp_head_list = constructor_head_list thy action_type inp;
   1.346 +val out_head_list = constructor_head_list thy action_type out;
   1.347 +val int_head_list = constructor_head_list thy action_type int;
   1.348 +val overlap_flag = ((overlap inp out) andalso (overlap inp int) andalso (overlap out int)); 
   1.349 +val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list 
   1.350 +							atyp statetupel trans;
   1.351 +val thy2 = (thy
   1.352 +|> Sign.add_consts
   1.353 +[(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn),
   1.354 +(Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn),
   1.355 +(Binding.name (automaton_name ^ "_trans"),
   1.356 + "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
   1.357 +(Binding.name automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
   1.358 +|> add_defs
   1.359 +[(automaton_name ^ "_initial_def",
   1.360 +automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
   1.361 +(automaton_name ^ "_asig_def",
   1.362 +automaton_name ^ "_asig == (" ^
   1.363 + inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"),
   1.364 +(automaton_name ^ "_trans_def",
   1.365 +automaton_name ^ "_trans == {(" ^
   1.366 + state_vars_tupel ^ ", act_of_" ^ automaton_name ^ ", " ^ state_vars_primed ^
   1.367 +"). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"),
   1.368 +(automaton_name ^ "_def",
   1.369 +automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
   1.370 +"_initial, " ^ automaton_name ^ "_trans,{},{})")
   1.371 +])
   1.372 +val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[]))
   1.373 +( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
   1.374 +in
   1.375 +(
   1.376 +if (chk_prime_list = []) then thy2
   1.377 +else (
   1.378 +error("Precondition or assignment terms in postconditions contain following primed variables:\n"
   1.379 + ^ (list_elements_of chk_prime_list)))
   1.380 +)
   1.381 +end)
   1.382 +
   1.383 +fun add_composition automaton_name aut_list thy =
   1.384 +(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   1.385 +let
   1.386 +val acttyp = check_ac thy aut_list; 
   1.387 +val st_typ = comp_st_type_of thy aut_list; 
   1.388 +val comp_list = clist aut_list;
   1.389 +in
   1.390 +thy
   1.391 +|> Sign.add_consts_i
   1.392 +[(Binding.name automaton_name,
   1.393 +Type("*",
   1.394 +[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
   1.395 + Type("*",[Type("set",[st_typ]),
   1.396 +  Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
   1.397 +   Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
   1.398 +,NoSyn)]
   1.399 +|> add_defs
   1.400 +[(automaton_name ^ "_def",
   1.401 +automaton_name ^ " == " ^ comp_list)]
   1.402 +end)
   1.403 +
   1.404 +fun add_restriction automaton_name aut_source actlist thy =
   1.405 +(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   1.406 +let
   1.407 +val auttyp = aut_type_of thy aut_source;
   1.408 +val acttyp = act_type_of thy auttyp; 
   1.409 +val rest_set = action_set_string thy acttyp actlist
   1.410 +in
   1.411 +thy
   1.412 +|> Sign.add_consts_i
   1.413 +[(Binding.name automaton_name, auttyp,NoSyn)]
   1.414 +|> add_defs
   1.415 +[(automaton_name ^ "_def",
   1.416 +automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] 
   1.417 +end)
   1.418 +fun add_hiding automaton_name aut_source actlist thy =
   1.419 +(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   1.420 +let
   1.421 +val auttyp = aut_type_of thy aut_source;
   1.422 +val acttyp = act_type_of thy auttyp; 
   1.423 +val hid_set = action_set_string thy acttyp actlist
   1.424 +in
   1.425 +thy
   1.426 +|> Sign.add_consts_i
   1.427 +[(Binding.name automaton_name, auttyp,NoSyn)]
   1.428 +|> add_defs
   1.429 +[(automaton_name ^ "_def",
   1.430 +automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] 
   1.431 +end)
   1.432 +
   1.433 +fun ren_act_type_of thy funct =
   1.434 +  (case Term.fastype_of (Syntax.read_term_global thy funct) of
   1.435 +    Type ("fun", [a, b]) => a
   1.436 +  | _ => error "could not extract argument type of renaming function term");
   1.437 + 
   1.438 +fun add_rename automaton_name aut_source fun_name thy =
   1.439 +(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   1.440 +let
   1.441 +val auttyp = aut_type_of thy aut_source;
   1.442 +val st_typ = st_type_of thy auttyp;
   1.443 +val acttyp = ren_act_type_of thy fun_name
   1.444 +in
   1.445 +thy
   1.446 +|> Sign.add_consts_i
   1.447 +[(Binding.name automaton_name,
   1.448 +Type("*",
   1.449 +[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
   1.450 + Type("*",[Type("set",[st_typ]),
   1.451 +  Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
   1.452 +   Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
   1.453 +,NoSyn)]
   1.454 +|> add_defs
   1.455 +[(automaton_name ^ "_def",
   1.456 +automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
   1.457 +end)
   1.458 +
   1.459 +
   1.460 +(** outer syntax **)
   1.461 +
   1.462 +(* prepare results *)
   1.463 +
   1.464 +(*encoding transition specifications with a element of ParseTrans*)
   1.465 +datatype ParseTrans = Rel of string | PP of string*(string*string)list;
   1.466 +fun mk_trans_of_rel s = Rel(s);
   1.467 +fun mk_trans_of_prepost (s,l) = PP(s,l); 
   1.468 +
   1.469 +fun trans_of (a, Rel b) = (a, b, [("", "")])
   1.470 +  | trans_of (a, PP (b, l)) = (a, b, l);
   1.471 +
   1.472 +
   1.473 +fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) =
   1.474 +  add_ioa aut action_type inp out int states initial (map trans_of trans);
   1.475 +
   1.476 +fun mk_composition_decl (aut, autlist) =
   1.477 +  add_composition aut autlist;
   1.478 +
   1.479 +fun mk_hiding_decl (aut, (actlist, source_aut)) =
   1.480 +  add_hiding aut source_aut actlist;
   1.481 +
   1.482 +fun mk_restriction_decl (aut, (source_aut, actlist)) =
   1.483 +  add_restriction aut source_aut actlist;
   1.484 +
   1.485 +fun mk_rename_decl (aut, (source_aut, rename_f)) =
   1.486 +  add_rename aut source_aut rename_f;
   1.487 +
   1.488 +
   1.489 +(* outer syntax *)
   1.490 +
   1.491 +local structure P = OuterParse and K = OuterKeyword in
   1.492 +
   1.493 +val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs",
   1.494 +  "outputs", "internals", "states", "initially", "transitions", "pre",
   1.495 +  "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
   1.496 +  "rename"];
   1.497 +
   1.498 +val actionlist = P.list1 P.term;
   1.499 +val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
   1.500 +val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
   1.501 +val internalslist = P.$$$ "internals" |-- P.!!! actionlist;
   1.502 +val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ));
   1.503 +val initial = P.$$$ "initially" |-- P.!!! P.term;
   1.504 +val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term);
   1.505 +val pre = P.$$$ "pre" |-- P.!!! P.term;
   1.506 +val post = P.$$$ "post" |-- P.!!! assign_list;
   1.507 +val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost;
   1.508 +val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost;
   1.509 +val transrel =  (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel;
   1.510 +val transition = P.term -- (transrel || pre1 || post1);
   1.511 +val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition);
   1.512 +
   1.513 +val ioa_decl =
   1.514 +  (P.name -- (P.$$$ "=" |--
   1.515 +    (P.$$$ "signature" |--
   1.516 +      P.!!! (P.$$$ "actions" |--
   1.517 +        (P.typ --
   1.518 +          (Scan.optional inputslist []) --
   1.519 +          (Scan.optional outputslist []) --
   1.520 +          (Scan.optional internalslist []) --
   1.521 +          stateslist --
   1.522 +          (Scan.optional initial "True") --
   1.523 +        translist))))) >> mk_ioa_decl ||
   1.524 +  (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name))))
   1.525 +    >> mk_composition_decl ||
   1.526 +  (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |--
   1.527 +      P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl ||
   1.528 +  (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |--
   1.529 +      P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl ||
   1.530 +  (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
   1.531 +    >> mk_rename_decl;
   1.532 +
   1.533 +val _ =
   1.534 +  OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
   1.535 +    (ioa_decl >> Toplevel.theory);
   1.536 +
   1.537 +end;
   1.538 +
   1.539 +end;
     2.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sun Jun 21 15:45:42 2009 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,536 +0,0 @@
     2.4 -(*  Title:      HOLCF/IOA/meta_theory/ioa.ML
     2.5 -    Author:     Tobias Hamberger, TU Muenchen
     2.6 -*)
     2.7 -
     2.8 -signature IOA =
     2.9 -sig
    2.10 -  val add_ioa: string -> string
    2.11 -    -> (string) list -> (string) list -> (string) list
    2.12 -    -> (string * string) list -> string
    2.13 -    -> (string * string * (string * string)list) list
    2.14 -    -> theory -> theory
    2.15 -  val add_composition : string -> (string)list -> theory -> theory
    2.16 -  val add_hiding : string -> string -> (string)list -> theory -> theory
    2.17 -  val add_restriction : string -> string -> (string)list -> theory -> theory
    2.18 -  val add_rename : string -> string -> string -> theory -> theory
    2.19 -end;
    2.20 -
    2.21 -structure Ioa: IOA =
    2.22 -struct
    2.23 -
    2.24 -val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
    2.25 -val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global;
    2.26 -
    2.27 -exception malformed;
    2.28 -
    2.29 -(* stripping quotes *)
    2.30 -fun strip [] = [] |
    2.31 -strip ("\""::r) = strip r |
    2.32 -strip (a::r) = a :: (strip r);
    2.33 -fun strip_quote s = implode(strip(explode(s)));
    2.34 -
    2.35 -(* used by *_of_varlist *)
    2.36 -fun extract_first (a,b) = strip_quote a;
    2.37 -fun extract_second (a,b) = strip_quote b;
    2.38 -(* following functions producing sth from a varlist *)
    2.39 -fun comma_list_of_varlist [] = "" |
    2.40 -comma_list_of_varlist [a] = extract_first a |
    2.41 -comma_list_of_varlist (a::r) = (extract_first a) ^ "," ^ (comma_list_of_varlist r);
    2.42 -fun primed_comma_list_of_varlist [] = "" |
    2.43 -primed_comma_list_of_varlist [a] = (extract_first a) ^ "'" |
    2.44 -primed_comma_list_of_varlist (a::r) = (extract_first a) ^ "'," ^
    2.45 - (primed_comma_list_of_varlist r);
    2.46 -fun type_product_of_varlist [] = "" |
    2.47 -type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" |
    2.48 -type_product_of_varlist(a::r) = "(" ^ extract_second(a) ^ ")*" ^ type_product_of_varlist r;
    2.49 -
    2.50 -(* listing a list *)
    2.51 -fun list_elements_of [] = "" |
    2.52 -list_elements_of (a::r) = a ^ " " ^ (list_elements_of r);
    2.53 -
    2.54 -(* extracting type parameters from a type list *)
    2.55 -(* fun param_tupel thy [] res = res |
    2.56 -param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res |
    2.57 -param_tupel thy ((TFree(a,_))::r) res = 
    2.58 -if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) |
    2.59 -param_tupel thy (a::r) res =
    2.60 -error ("one component of a statetype is a TVar: " ^ (string_of_typ thy a));
    2.61 -*)
    2.62 -
    2.63 -(* used by constr_list *)
    2.64 -fun extract_constrs thy [] = [] |
    2.65 -extract_constrs thy (a::r) =
    2.66 -let
    2.67 -fun delete_bold [] = []
    2.68 -| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
    2.69 -        then (let val (_::_::_::s) = xs in delete_bold s end)
    2.70 -        else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
    2.71 -                then  (let val (_::_::_::s) = xs in delete_bold s end)
    2.72 -                else (x::delete_bold xs));
    2.73 -fun delete_bold_string s = implode(delete_bold(explode s));
    2.74 -(* from a constructor term in *.induct (with quantifiers,
    2.75 -"Trueprop" and ?P stripped away) delivers the head *)
    2.76 -fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r |
    2.77 -extract_hd (Const("Trueprop",_) $ r) = extract_hd r |
    2.78 -extract_hd (Var(_,_) $ r) = extract_hd r |
    2.79 -extract_hd (a $ b) = extract_hd a |
    2.80 -extract_hd (Const(s,_)) = s |
    2.81 -extract_hd _ = raise malformed;
    2.82 -(* delivers constructor term string from a prem of *.induct *)
    2.83 -fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))|
    2.84 -extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r |
    2.85 -extract_constr thy (Var(_,_) $ r) =  delete_bold_string(string_of_term thy r) |
    2.86 -extract_constr _ _ = raise malformed;
    2.87 -in
    2.88 -(extract_hd a,extract_constr thy a) :: (extract_constrs thy r)
    2.89 -end;
    2.90 -
    2.91 -(* delivering list of constructor terms of a datatype *)
    2.92 -fun constr_list thy atyp =
    2.93 -let
    2.94 -fun act_name thy (Type(s,_)) = s |
    2.95 -act_name _ s = 
    2.96 -error("malformed action type: " ^ (string_of_typ thy s));
    2.97 -fun afpl ("." :: a) = [] |
    2.98 -afpl [] = [] |
    2.99 -afpl (a::r) = a :: (afpl r);
   2.100 -fun unqualify s = implode(rev(afpl(rev(explode s))));
   2.101 -val q_atypstr = act_name thy atyp;
   2.102 -val uq_atypstr = unqualify q_atypstr;
   2.103 -val prem = prems_of (PureThy.get_thm thy (uq_atypstr ^ ".induct"));
   2.104 -in
   2.105 -extract_constrs thy prem
   2.106 -handle malformed =>
   2.107 -error("malformed theorem : " ^ uq_atypstr ^ ".induct")
   2.108 -end;
   2.109 -
   2.110 -fun check_for_constr thy atyp (a $ b) =
   2.111 -let
   2.112 -fun all_free (Free(_,_)) = true |
   2.113 -all_free (a $ b) = if (all_free a) then (all_free b) else false |
   2.114 -all_free _ = false; 
   2.115 -in 
   2.116 -if (all_free b) then (check_for_constr thy atyp a) else false
   2.117 -end |
   2.118 -check_for_constr thy atyp (Const(a,_)) =
   2.119 -let
   2.120 -val cl = constr_list thy atyp;
   2.121 -fun fstmem a [] = false |
   2.122 -fstmem a ((f,s)::r) = if (a=f) then true else (fstmem a r)
   2.123 -in
   2.124 -if (fstmem a cl) then true else false
   2.125 -end |
   2.126 -check_for_constr _ _ _ = false;
   2.127 -
   2.128 -(* delivering the free variables of a constructor term *)
   2.129 -fun free_vars_of (t1 $ t2) = (free_vars_of t1) @ (free_vars_of t2) |
   2.130 -free_vars_of (Const(_,_)) = [] |
   2.131 -free_vars_of (Free(a,_)) = [a] |
   2.132 -free_vars_of _ = raise malformed;
   2.133 -
   2.134 -(* making a constructor set from a constructor term (of signature) *)
   2.135 -fun constr_set_string thy atyp ctstr =
   2.136 -let
   2.137 -val trm = OldGoals.simple_read_term thy atyp ctstr;
   2.138 -val l = free_vars_of trm
   2.139 -in
   2.140 -if (check_for_constr thy atyp trm) then
   2.141 -(if (l=[]) then ("{" ^ ctstr ^ "}")
   2.142 -else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})")
   2.143 -else (raise malformed) 
   2.144 -handle malformed => 
   2.145 -error("malformed action term: " ^ (string_of_term thy trm))
   2.146 -end;
   2.147 -
   2.148 -(* extracting constructor heads *)
   2.149 -fun constructor_head thy atypstr s =
   2.150 -let
   2.151 -fun hd_of (Const(a,_)) = a |
   2.152 -hd_of (t $ _) = hd_of t |
   2.153 -hd_of _ = raise malformed;
   2.154 -val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
   2.155 -in
   2.156 -hd_of trm handle malformed =>
   2.157 -error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
   2.158 -end;
   2.159 -fun constructor_head_list _ _ [] = [] |
   2.160 -constructor_head_list thy atypstr (a::r) =
   2.161 - (constructor_head thy atypstr a)::(constructor_head_list thy atypstr r);
   2.162 -
   2.163 -(* producing an action set *)
   2.164 -(*FIXME*)
   2.165 -fun action_set_string thy atyp [] = "Set.empty" |
   2.166 -action_set_string thy atyp [a] = constr_set_string thy atyp (strip_quote a) |
   2.167 -action_set_string thy atyp (a::r) = (constr_set_string thy atyp (strip_quote a)) ^
   2.168 -         " Un " ^ (action_set_string thy atyp r);
   2.169 -
   2.170 -(* used by extend *)
   2.171 -fun pstr s [] = "(" ^ s ^ "' = " ^ s ^ ")" |
   2.172 -pstr s ((a,b)::r) =
   2.173 -if (s=a) then ("(" ^ s ^ "' = (" ^ b ^ "))") else (pstr s r);
   2.174 -fun poststring [] l = "" |
   2.175 -poststring [(a,b)] l = pstr a l |
   2.176 -poststring ((a,b)::r) l = (pstr a l) ^ " & " ^ (poststring r l);
   2.177 -
   2.178 -(* extends a (action string,condition,assignlist) tupel by a
   2.179 -(action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list 
   2.180 -(where bool indicates whether there is a precondition *)
   2.181 -fun extend thy atyp statetupel (actstr,r,[]) =
   2.182 -let
   2.183 -val trm = OldGoals.simple_read_term thy atyp actstr;
   2.184 -val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
   2.185 -val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
   2.186 -in
   2.187 -if (check_for_constr thy atyp trm)
   2.188 -then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag)
   2.189 -else
   2.190 -error("transition " ^ actstr ^ " is not a pure constructor term")
   2.191 -end |
   2.192 -extend thy atyp statetupel (actstr,r,(a,b)::c) =
   2.193 -let
   2.194 -fun pseudo_poststring [] = "" |
   2.195 -pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
   2.196 -pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); 
   2.197 -val trm = OldGoals.simple_read_term thy atyp actstr;
   2.198 -val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
   2.199 -val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
   2.200 -in
   2.201 -if (check_for_constr thy atyp trm) then
   2.202 -(if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false)
   2.203 -(* the case with transrel *)
   2.204 - else 
   2.205 - (trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)),
   2.206 -	"(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag))
   2.207 -else
   2.208 -error("transition " ^ actstr ^ " is not a pure constructor term")
   2.209 -end;
   2.210 -(* used by make_alt_string *) 
   2.211 -fun extended_list _ _ _ [] = [] |
   2.212 -extended_list thy atyp statetupel (a::r) =
   2.213 -	 (extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r);
   2.214 -
   2.215 -(* used by write_alts *)
   2.216 -fun write_alt thy (chead,tr) inp out int [] =
   2.217 -if (chead mem inp) then
   2.218 -(
   2.219 -error("Input action " ^ tr ^ " was not specified")
   2.220 -) else (
   2.221 -if (chead mem (out@int)) then
   2.222 -(writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else ();
   2.223 -(tr ^ " => False",tr ^ " => False")) |
   2.224 -write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) =
   2.225 -let
   2.226 -fun hd_of (Const(a,_)) = a |
   2.227 -hd_of (t $ _) = hd_of t |
   2.228 -hd_of _ = raise malformed;
   2.229 -fun occurs_again c [] = false |
   2.230 -occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r);
   2.231 -in
   2.232 -if (chead=(hd_of a)) then 
   2.233 -(if ((chead mem inp) andalso e) then (
   2.234 -error("Input action " ^ b ^ " has a precondition")
   2.235 -) else (if (chead mem (inp@out@int)) then 
   2.236 -		(if (occurs_again chead r) then (
   2.237 -error("Two specifications for action: " ^ b)
   2.238 -		) else (b ^ " => " ^ c,b ^ " => " ^ d))
   2.239 -	else (
   2.240 -error("Action " ^ b ^ " is not in automaton signature")
   2.241 -))) else (write_alt thy (chead,ctrm) inp out int r)
   2.242 -handle malformed =>
   2.243 -error ("malformed action term: " ^ (string_of_term thy a))
   2.244 -end;
   2.245 -
   2.246 -(* used by make_alt_string *)
   2.247 -fun write_alts thy (a,b) inp out int [] ttr = (a,b) |
   2.248 -write_alts thy (a,b) inp out int [c] ttr =
   2.249 -let
   2.250 -val wa = write_alt thy c inp out int ttr
   2.251 -in
   2.252 - (a ^ (fst wa),b ^ (snd wa))
   2.253 -end |
   2.254 -write_alts thy (a,b) inp out int (c::r) ttr =
   2.255 -let
   2.256 -val wa = write_alt thy c inp out int ttr
   2.257 -in
   2.258 - write_alts thy (a ^ (fst wa) ^ " | ", b ^ (snd wa) ^ " | ") inp out int r ttr
   2.259 -end;
   2.260 -
   2.261 -fun make_alt_string thy inp out int atyp statetupel trans =
   2.262 -let
   2.263 -val cl = constr_list thy atyp;
   2.264 -val ttr = extended_list thy atyp statetupel trans;
   2.265 -in
   2.266 -write_alts thy ("","") inp out int cl ttr
   2.267 -end;
   2.268 -
   2.269 -(* used in add_ioa *)
   2.270 -fun check_free_primed (Free(a,_)) = 
   2.271 -let
   2.272 -val (f::r) = rev(explode a)
   2.273 -in
   2.274 -if (f="'") then [a] else []
   2.275 -end | 
   2.276 -check_free_primed (a $ b) = ((check_free_primed a) @ (check_free_primed b)) |
   2.277 -check_free_primed (Abs(_,_,t)) = check_free_primed t |
   2.278 -check_free_primed _ = [];
   2.279 -
   2.280 -fun overlap [] _ = true |
   2.281 -overlap (a::r) l = if (a mem l) then (
   2.282 -error("Two occurences of action " ^ a ^ " in automaton signature")
   2.283 -) else (overlap r l);
   2.284 -
   2.285 -(* delivering some types of an automaton *)
   2.286 -fun aut_type_of thy aut_name =
   2.287 -let
   2.288 -fun left_of (( _ $ left) $ _) = left |
   2.289 -left_of _ = raise malformed;
   2.290 -val aut_def = concl_of (PureThy.get_thm thy (aut_name ^ "_def"));
   2.291 -in
   2.292 -(#T(rep_cterm(cterm_of thy (left_of aut_def))))
   2.293 -handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
   2.294 -end;
   2.295 -
   2.296 -fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp |
   2.297 -act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^
   2.298 -(string_of_typ thy t));
   2.299 -fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp |
   2.300 -st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^
   2.301 -(string_of_typ thy t));
   2.302 -
   2.303 -fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) |
   2.304 -comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) |
   2.305 -comp_st_type_of _ _ = error "empty automaton list";
   2.306 -
   2.307 -(* checking consistency of action types (for composition) *)
   2.308 -fun check_ac thy (a::r) =
   2.309 -let
   2.310 -fun ch_f_a thy acttyp [] = acttyp |
   2.311 -ch_f_a thy acttyp (a::r) =
   2.312 -let
   2.313 -val auttyp = aut_type_of thy a;
   2.314 -val ac = (act_type_of thy auttyp);
   2.315 -in
   2.316 -if (ac=acttyp) then (ch_f_a thy acttyp r) else (error "A")
   2.317 -end;
   2.318 -val auttyp = aut_type_of thy a;
   2.319 -val acttyp = (act_type_of thy auttyp);
   2.320 -in
   2.321 -ch_f_a thy acttyp r
   2.322 -end |
   2.323 -check_ac _ [] = error "empty automaton list";
   2.324 -
   2.325 -fun clist [] = "" |
   2.326 -clist [a] = a |
   2.327 -clist (a::r) = a ^ " || " ^ (clist r);
   2.328 -
   2.329 -val add_defs = snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes o map (apfst Binding.name));
   2.330 -
   2.331 -
   2.332 -(* add_ioa *)
   2.333 -
   2.334 -fun add_ioa automaton_name action_type inp out int statetupel ini trans thy =
   2.335 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   2.336 -let
   2.337 -val state_type_string = type_product_of_varlist(statetupel);
   2.338 -val styp = Syntax.read_typ_global thy state_type_string;
   2.339 -val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")";
   2.340 -val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")";
   2.341 -val atyp = Syntax.read_typ_global thy action_type;
   2.342 -val inp_set_string = action_set_string thy atyp inp;
   2.343 -val out_set_string = action_set_string thy atyp out;
   2.344 -val int_set_string = action_set_string thy atyp int;
   2.345 -val inp_head_list = constructor_head_list thy action_type inp;
   2.346 -val out_head_list = constructor_head_list thy action_type out;
   2.347 -val int_head_list = constructor_head_list thy action_type int;
   2.348 -val overlap_flag = ((overlap inp out) andalso (overlap inp int) andalso (overlap out int)); 
   2.349 -val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list 
   2.350 -							atyp statetupel trans;
   2.351 -val thy2 = (thy
   2.352 -|> Sign.add_consts
   2.353 -[(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn),
   2.354 -(Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn),
   2.355 -(Binding.name (automaton_name ^ "_trans"),
   2.356 - "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
   2.357 -(Binding.name automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
   2.358 -|> add_defs
   2.359 -[(automaton_name ^ "_initial_def",
   2.360 -automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
   2.361 -(automaton_name ^ "_asig_def",
   2.362 -automaton_name ^ "_asig == (" ^
   2.363 - inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"),
   2.364 -(automaton_name ^ "_trans_def",
   2.365 -automaton_name ^ "_trans == {(" ^
   2.366 - state_vars_tupel ^ ", act_of_" ^ automaton_name ^ ", " ^ state_vars_primed ^
   2.367 -"). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"),
   2.368 -(automaton_name ^ "_def",
   2.369 -automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
   2.370 -"_initial, " ^ automaton_name ^ "_trans,{},{})")
   2.371 -])
   2.372 -val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[]))
   2.373 -( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
   2.374 -in
   2.375 -(
   2.376 -if (chk_prime_list = []) then thy2
   2.377 -else (
   2.378 -error("Precondition or assignment terms in postconditions contain following primed variables:\n"
   2.379 - ^ (list_elements_of chk_prime_list)))
   2.380 -)
   2.381 -end)
   2.382 -
   2.383 -fun add_composition automaton_name aut_list thy =
   2.384 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   2.385 -let
   2.386 -val acttyp = check_ac thy aut_list; 
   2.387 -val st_typ = comp_st_type_of thy aut_list; 
   2.388 -val comp_list = clist aut_list;
   2.389 -in
   2.390 -thy
   2.391 -|> Sign.add_consts_i
   2.392 -[(Binding.name automaton_name,
   2.393 -Type("*",
   2.394 -[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
   2.395 - Type("*",[Type("set",[st_typ]),
   2.396 -  Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
   2.397 -   Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
   2.398 -,NoSyn)]
   2.399 -|> add_defs
   2.400 -[(automaton_name ^ "_def",
   2.401 -automaton_name ^ " == " ^ comp_list)]
   2.402 -end)
   2.403 -
   2.404 -fun add_restriction automaton_name aut_source actlist thy =
   2.405 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   2.406 -let
   2.407 -val auttyp = aut_type_of thy aut_source;
   2.408 -val acttyp = act_type_of thy auttyp; 
   2.409 -val rest_set = action_set_string thy acttyp actlist
   2.410 -in
   2.411 -thy
   2.412 -|> Sign.add_consts_i
   2.413 -[(Binding.name automaton_name, auttyp,NoSyn)]
   2.414 -|> add_defs
   2.415 -[(automaton_name ^ "_def",
   2.416 -automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] 
   2.417 -end)
   2.418 -fun add_hiding automaton_name aut_source actlist thy =
   2.419 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   2.420 -let
   2.421 -val auttyp = aut_type_of thy aut_source;
   2.422 -val acttyp = act_type_of thy auttyp; 
   2.423 -val hid_set = action_set_string thy acttyp actlist
   2.424 -in
   2.425 -thy
   2.426 -|> Sign.add_consts_i
   2.427 -[(Binding.name automaton_name, auttyp,NoSyn)]
   2.428 -|> add_defs
   2.429 -[(automaton_name ^ "_def",
   2.430 -automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] 
   2.431 -end)
   2.432 -
   2.433 -fun ren_act_type_of thy funct =
   2.434 -  (case Term.fastype_of (Syntax.read_term_global thy funct) of
   2.435 -    Type ("fun", [a, b]) => a
   2.436 -  | _ => error "could not extract argument type of renaming function term");
   2.437 - 
   2.438 -fun add_rename automaton_name aut_source fun_name thy =
   2.439 -(writeln("Constructing automaton " ^ automaton_name ^ " ...");
   2.440 -let
   2.441 -val auttyp = aut_type_of thy aut_source;
   2.442 -val st_typ = st_type_of thy auttyp;
   2.443 -val acttyp = ren_act_type_of thy fun_name
   2.444 -in
   2.445 -thy
   2.446 -|> Sign.add_consts_i
   2.447 -[(Binding.name automaton_name,
   2.448 -Type("*",
   2.449 -[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
   2.450 - Type("*",[Type("set",[st_typ]),
   2.451 -  Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
   2.452 -   Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
   2.453 -,NoSyn)]
   2.454 -|> add_defs
   2.455 -[(automaton_name ^ "_def",
   2.456 -automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
   2.457 -end)
   2.458 -
   2.459 -
   2.460 -(** outer syntax **)
   2.461 -
   2.462 -(* prepare results *)
   2.463 -
   2.464 -(*encoding transition specifications with a element of ParseTrans*)
   2.465 -datatype ParseTrans = Rel of string | PP of string*(string*string)list;
   2.466 -fun mk_trans_of_rel s = Rel(s);
   2.467 -fun mk_trans_of_prepost (s,l) = PP(s,l); 
   2.468 -
   2.469 -fun trans_of (a, Rel b) = (a, b, [("", "")])
   2.470 -  | trans_of (a, PP (b, l)) = (a, b, l);
   2.471 -
   2.472 -
   2.473 -fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) =
   2.474 -  add_ioa aut action_type inp out int states initial (map trans_of trans);
   2.475 -
   2.476 -fun mk_composition_decl (aut, autlist) =
   2.477 -  add_composition aut autlist;
   2.478 -
   2.479 -fun mk_hiding_decl (aut, (actlist, source_aut)) =
   2.480 -  add_hiding aut source_aut actlist;
   2.481 -
   2.482 -fun mk_restriction_decl (aut, (source_aut, actlist)) =
   2.483 -  add_restriction aut source_aut actlist;
   2.484 -
   2.485 -fun mk_rename_decl (aut, (source_aut, rename_f)) =
   2.486 -  add_rename aut source_aut rename_f;
   2.487 -
   2.488 -
   2.489 -(* outer syntax *)
   2.490 -
   2.491 -local structure P = OuterParse and K = OuterKeyword in
   2.492 -
   2.493 -val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs",
   2.494 -  "outputs", "internals", "states", "initially", "transitions", "pre",
   2.495 -  "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
   2.496 -  "rename"];
   2.497 -
   2.498 -val actionlist = P.list1 P.term;
   2.499 -val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
   2.500 -val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
   2.501 -val internalslist = P.$$$ "internals" |-- P.!!! actionlist;
   2.502 -val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ));
   2.503 -val initial = P.$$$ "initially" |-- P.!!! P.term;
   2.504 -val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term);
   2.505 -val pre = P.$$$ "pre" |-- P.!!! P.term;
   2.506 -val post = P.$$$ "post" |-- P.!!! assign_list;
   2.507 -val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost;
   2.508 -val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost;
   2.509 -val transrel =  (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel;
   2.510 -val transition = P.term -- (transrel || pre1 || post1);
   2.511 -val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition);
   2.512 -
   2.513 -val ioa_decl =
   2.514 -  (P.name -- (P.$$$ "=" |--
   2.515 -    (P.$$$ "signature" |--
   2.516 -      P.!!! (P.$$$ "actions" |--
   2.517 -        (P.typ --
   2.518 -          (Scan.optional inputslist []) --
   2.519 -          (Scan.optional outputslist []) --
   2.520 -          (Scan.optional internalslist []) --
   2.521 -          stateslist --
   2.522 -          (Scan.optional initial "True") --
   2.523 -        translist))))) >> mk_ioa_decl ||
   2.524 -  (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name))))
   2.525 -    >> mk_composition_decl ||
   2.526 -  (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |--
   2.527 -      P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl ||
   2.528 -  (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |--
   2.529 -      P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl ||
   2.530 -  (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
   2.531 -    >> mk_rename_decl;
   2.532 -
   2.533 -val _ =
   2.534 -  OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
   2.535 -    (ioa_decl >> Toplevel.theory);
   2.536 -
   2.537 -end;
   2.538 -
   2.539 -end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOLCF/Tools/fixrec.ML	Sun Jun 21 15:45:57 2009 +0200
     3.3 @@ -0,0 +1,435 @@
     3.4 +(*  Title:      HOLCF/Tools/fixrec.ML
     3.5 +    Author:     Amber Telfer and Brian Huffman
     3.6 +
     3.7 +Recursive function definition package for HOLCF.
     3.8 +*)
     3.9 +
    3.10 +signature FIXREC =
    3.11 +sig
    3.12 +  val add_fixrec: bool -> (binding * typ option * mixfix) list
    3.13 +    -> (Attrib.binding * term) list -> local_theory -> local_theory
    3.14 +  val add_fixrec_cmd: bool -> (binding * string option * mixfix) list
    3.15 +    -> (Attrib.binding * string) list -> local_theory -> local_theory
    3.16 +  val add_fixpat: Thm.binding * term list -> theory -> theory
    3.17 +  val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory
    3.18 +  val add_matchers: (string * string) list -> theory -> theory
    3.19 +  val setup: theory -> theory
    3.20 +end;
    3.21 +
    3.22 +structure Fixrec :> FIXREC =
    3.23 +struct
    3.24 +
    3.25 +val def_cont_fix_eq = @{thm def_cont_fix_eq};
    3.26 +val def_cont_fix_ind = @{thm def_cont_fix_ind};
    3.27 +
    3.28 +
    3.29 +fun fixrec_err s = error ("fixrec definition error:\n" ^ s);
    3.30 +fun fixrec_eq_err thy s eq =
    3.31 +  fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
    3.32 +
    3.33 +(*************************************************************************)
    3.34 +(***************************** building types ****************************)
    3.35 +(*************************************************************************)
    3.36 +
    3.37 +(* ->> is taken from holcf_logic.ML *)
    3.38 +fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
    3.39 +
    3.40 +infixr 6 ->>; val (op ->>) = cfunT;
    3.41 +
    3.42 +fun cfunsT (Ts, U) = foldr cfunT U Ts;
    3.43 +
    3.44 +fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
    3.45 +  | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
    3.46 +
    3.47 +fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
    3.48 +  | binder_cfun _   =  [];
    3.49 +
    3.50 +fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
    3.51 +  | body_cfun T   =  T;
    3.52 +
    3.53 +fun strip_cfun T : typ list * typ =
    3.54 +  (binder_cfun T, body_cfun T);
    3.55 +
    3.56 +fun maybeT T = Type(@{type_name "maybe"}, [T]);
    3.57 +
    3.58 +fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T
    3.59 +  | dest_maybeT T = raise TYPE ("dest_maybeT", [T], []);
    3.60 +
    3.61 +fun tupleT [] = HOLogic.unitT
    3.62 +  | tupleT [T] = T
    3.63 +  | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
    3.64 +
    3.65 +fun matchT (T, U) =
    3.66 +  body_cfun T ->> cfunsT (binder_cfun T, U) ->> U;
    3.67 +
    3.68 +
    3.69 +(*************************************************************************)
    3.70 +(***************************** building terms ****************************)
    3.71 +(*************************************************************************)
    3.72 +
    3.73 +val mk_trp = HOLogic.mk_Trueprop;
    3.74 +
    3.75 +(* splits a cterm into the right and lefthand sides of equality *)
    3.76 +fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
    3.77 +
    3.78 +(* similar to Thm.head_of, but for continuous application *)
    3.79 +fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f
    3.80 +  | chead_of u = u;
    3.81 +
    3.82 +fun capply_const (S, T) =
    3.83 +  Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T));
    3.84 +
    3.85 +fun cabs_const (S, T) =
    3.86 +  Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T));
    3.87 +
    3.88 +fun mk_cabs t =
    3.89 +  let val T = Term.fastype_of t
    3.90 +  in cabs_const (Term.domain_type T, Term.range_type T) $ t end
    3.91 +
    3.92 +fun mk_capply (t, u) =
    3.93 +  let val (S, T) =
    3.94 +    case Term.fastype_of t of
    3.95 +        Type(@{type_name "->"}, [S, T]) => (S, T)
    3.96 +      | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
    3.97 +  in capply_const (S, T) $ t $ u end;
    3.98 +
    3.99 +infix 0 ==;  val (op ==) = Logic.mk_equals;
   3.100 +infix 1 ===; val (op ===) = HOLogic.mk_eq;
   3.101 +infix 9 `  ; val (op `) = mk_capply;
   3.102 +
   3.103 +(* builds the expression (LAM v. rhs) *)
   3.104 +fun big_lambda v rhs =
   3.105 +  cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs;
   3.106 +
   3.107 +(* builds the expression (LAM v1 v2 .. vn. rhs) *)
   3.108 +fun big_lambdas [] rhs = rhs
   3.109 +  | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs);
   3.110 +
   3.111 +fun mk_return t =
   3.112 +  let val T = Term.fastype_of t
   3.113 +  in Const(@{const_name Fixrec.return}, T ->> maybeT T) ` t end;
   3.114 +
   3.115 +fun mk_bind (t, u) =
   3.116 +  let val (T, mU) = dest_cfunT (Term.fastype_of u);
   3.117 +      val bindT = maybeT T ->> (T ->> mU) ->> mU;
   3.118 +  in Const(@{const_name Fixrec.bind}, bindT) ` t ` u end;
   3.119 +
   3.120 +fun mk_mplus (t, u) =
   3.121 +  let val mT = Term.fastype_of t
   3.122 +  in Const(@{const_name Fixrec.mplus}, mT ->> mT ->> mT) ` t ` u end;
   3.123 +
   3.124 +fun mk_run t =
   3.125 +  let val mT = Term.fastype_of t
   3.126 +      val T = dest_maybeT mT
   3.127 +  in Const(@{const_name Fixrec.run}, mT ->> T) ` t end;
   3.128 +
   3.129 +fun mk_fix t =
   3.130 +  let val (T, _) = dest_cfunT (Term.fastype_of t)
   3.131 +  in Const(@{const_name fix}, (T ->> T) ->> T) ` t end;
   3.132 +
   3.133 +fun mk_cont t =
   3.134 +  let val T = Term.fastype_of t
   3.135 +  in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end;
   3.136 +
   3.137 +val mk_fst = HOLogic.mk_fst
   3.138 +val mk_snd = HOLogic.mk_snd
   3.139 +
   3.140 +(* builds the expression (v1,v2,..,vn) *)
   3.141 +fun mk_tuple [] = HOLogic.unit
   3.142 +|   mk_tuple (t::[]) = t
   3.143 +|   mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts);
   3.144 +
   3.145 +(* builds the expression (%(v1,v2,..,vn). rhs) *)
   3.146 +fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs
   3.147 +  | lambda_tuple (v::[]) rhs = Term.lambda v rhs
   3.148 +  | lambda_tuple (v::vs) rhs =
   3.149 +      HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs));
   3.150 +
   3.151 +
   3.152 +(*************************************************************************)
   3.153 +(************* fixed-point definitions and unfolding theorems ************)
   3.154 +(*************************************************************************)
   3.155 +
   3.156 +fun add_fixdefs
   3.157 +  (fixes : ((binding * typ) * mixfix) list)
   3.158 +  (spec : (Attrib.binding * term) list)
   3.159 +  (lthy : local_theory) =
   3.160 +  let
   3.161 +    val thy = ProofContext.theory_of lthy;
   3.162 +    val names = map (Binding.name_of o fst o fst) fixes;
   3.163 +    val all_names = space_implode "_" names;
   3.164 +    val (lhss,rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
   3.165 +    val functional = lambda_tuple lhss (mk_tuple rhss);
   3.166 +    val fixpoint = mk_fix (mk_cabs functional);
   3.167 +    
   3.168 +    val cont_thm =
   3.169 +      Goal.prove lthy [] [] (mk_trp (mk_cont functional))
   3.170 +        (K (simp_tac (local_simpset_of lthy) 1));
   3.171 +
   3.172 +    fun one_def (l as Free(n,_)) r =
   3.173 +          let val b = Long_Name.base_name n
   3.174 +          in ((Binding.name (b^"_def"), []), r) end
   3.175 +      | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form";
   3.176 +    fun defs [] _ = []
   3.177 +      | defs (l::[]) r = [one_def l r]
   3.178 +      | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r);
   3.179 +    val fixdefs = defs lhss fixpoint;
   3.180 +    val define_all = fold_map (LocalTheory.define Thm.definitionK);
   3.181 +    val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy
   3.182 +      |> define_all (map (apfst fst) fixes ~~ fixdefs);
   3.183 +    fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
   3.184 +    val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms);
   3.185 +    val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT);
   3.186 +    val predicate = lambda_tuple lhss (list_comb (P, lhss));
   3.187 +    val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm])
   3.188 +      |> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)]
   3.189 +      |> LocalDefs.unfold lthy @{thms split_paired_all split_conv split_strict};
   3.190 +    val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
   3.191 +      |> LocalDefs.unfold lthy' @{thms split_conv};
   3.192 +    fun unfolds [] thm = []
   3.193 +      | unfolds (n::[]) thm = [(n^"_unfold", thm)]
   3.194 +      | unfolds (n::ns) thm = let
   3.195 +          val thmL = thm RS @{thm Pair_eqD1};
   3.196 +          val thmR = thm RS @{thm Pair_eqD2};
   3.197 +        in (n^"_unfold", thmL) :: unfolds ns thmR end;
   3.198 +    val unfold_thms = unfolds names tuple_unfold_thm;
   3.199 +    fun mk_note (n, thm) = ((Binding.name n, []), [thm]);
   3.200 +    val (thmss, lthy'') = lthy'
   3.201 +      |> fold_map (LocalTheory.note Thm.generatedK o mk_note)
   3.202 +        ((all_names ^ "_induct", tuple_induct_thm) :: unfold_thms);
   3.203 +  in
   3.204 +    (lthy'', names, fixdef_thms, map snd unfold_thms)
   3.205 +  end;
   3.206 +
   3.207 +(*************************************************************************)
   3.208 +(*********** monadic notation and pattern matching compilation ***********)
   3.209 +(*************************************************************************)
   3.210 +
   3.211 +structure FixrecMatchData = TheoryDataFun (
   3.212 +  type T = string Symtab.table;
   3.213 +  val empty = Symtab.empty;
   3.214 +  val copy = I;
   3.215 +  val extend = I;
   3.216 +  fun merge _ tabs : T = Symtab.merge (K true) tabs;
   3.217 +);
   3.218 +
   3.219 +(* associate match functions with pattern constants *)
   3.220 +fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms);
   3.221 +
   3.222 +fun taken_names (t : term) : bstring list =
   3.223 +  let
   3.224 +    fun taken (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
   3.225 +      | taken (Free(a,_) , bs) = insert (op =) a bs
   3.226 +      | taken (f $ u     , bs) = taken (f, taken (u, bs))
   3.227 +      | taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs)
   3.228 +      | taken (_         , bs) = bs;
   3.229 +  in
   3.230 +    taken (t, [])
   3.231 +  end;
   3.232 +
   3.233 +(* builds a monadic term for matching a constructor pattern *)
   3.234 +fun pre_build match_name pat rhs vs taken =
   3.235 +  case pat of
   3.236 +    Const(@{const_name Rep_CFun},_)$f$(v as Free(n,T)) =>
   3.237 +      pre_build match_name f rhs (v::vs) taken
   3.238 +  | Const(@{const_name Rep_CFun},_)$f$x =>
   3.239 +      let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
   3.240 +      in pre_build match_name f rhs' (v::vs) taken' end
   3.241 +  | Const(c,T) =>
   3.242 +      let
   3.243 +        val n = Name.variant taken "v";
   3.244 +        fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
   3.245 +          | result_type T _ = T;
   3.246 +        val v = Free(n, result_type T vs);
   3.247 +        val m = Const(match_name c, matchT (T, fastype_of rhs));
   3.248 +        val k = big_lambdas vs rhs;
   3.249 +      in
   3.250 +        (m`v`k, v, n::taken)
   3.251 +      end
   3.252 +  | Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n)
   3.253 +  | _ => fixrec_err "pre_build: invalid pattern";
   3.254 +
   3.255 +(* builds a monadic term for matching a function definition pattern *)
   3.256 +(* returns (name, arity, matcher) *)
   3.257 +fun building match_name pat rhs vs taken =
   3.258 +  case pat of
   3.259 +    Const(@{const_name Rep_CFun}, _)$f$(v as Free(n,T)) =>
   3.260 +      building match_name f rhs (v::vs) taken
   3.261 +  | Const(@{const_name Rep_CFun}, _)$f$x =>
   3.262 +      let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
   3.263 +      in building match_name f rhs' (v::vs) taken' end
   3.264 +  | Free(_,_) => ((pat, length vs), big_lambdas vs rhs)
   3.265 +  | Const(_,_) => ((pat, length vs), big_lambdas vs rhs)
   3.266 +  | _ => fixrec_err ("function is not declared as constant in theory: "
   3.267 +                    ^ ML_Syntax.print_term pat);
   3.268 +
   3.269 +fun strip_alls t =
   3.270 +  if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t;
   3.271 +
   3.272 +fun match_eq match_name eq =
   3.273 +  let
   3.274 +    val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq));
   3.275 +  in
   3.276 +    building match_name lhs (mk_return rhs) [] (taken_names eq)
   3.277 +  end;
   3.278 +
   3.279 +(* returns the sum (using +++) of the terms in ms *)
   3.280 +(* also applies "run" to the result! *)
   3.281 +fun fatbar arity ms =
   3.282 +  let
   3.283 +    fun LAM_Ts 0 t = ([], Term.fastype_of t)
   3.284 +      | LAM_Ts n (_ $ Abs(_,T,t)) =
   3.285 +          let val (Ts, U) = LAM_Ts (n-1) t in (T::Ts, U) end
   3.286 +      | LAM_Ts _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
   3.287 +    fun unLAM 0 t = t
   3.288 +      | unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t
   3.289 +      | unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
   3.290 +    fun reLAM ([], U) t = t
   3.291 +      | reLAM (T::Ts, U) t = reLAM (Ts, T ->> U) (cabs_const(T,U)$Abs("",T,t));
   3.292 +    val msum = foldr1 mk_mplus (map (unLAM arity) ms);
   3.293 +    val (Ts, U) = LAM_Ts arity (hd ms)
   3.294 +  in
   3.295 +    reLAM (rev Ts, dest_maybeT U) (mk_run msum)
   3.296 +  end;
   3.297 +
   3.298 +(* this is the pattern-matching compiler function *)
   3.299 +fun compile_pats match_name eqs =
   3.300 +  let
   3.301 +    val (((n::names),(a::arities)),mats) =
   3.302 +      apfst ListPair.unzip (ListPair.unzip (map (match_eq match_name) eqs));
   3.303 +    val cname = if forall (fn x => n=x) names then n
   3.304 +          else fixrec_err "all equations in block must define the same function";
   3.305 +    val arity = if forall (fn x => a=x) arities then a
   3.306 +          else fixrec_err "all equations in block must have the same arity";
   3.307 +    val rhs = fatbar arity mats;
   3.308 +  in
   3.309 +    mk_trp (cname === rhs)
   3.310 +  end;
   3.311 +
   3.312 +(*************************************************************************)
   3.313 +(********************** Proving associated theorems **********************)
   3.314 +(*************************************************************************)
   3.315 +
   3.316 +(* proves a block of pattern matching equations as theorems, using unfold *)
   3.317 +fun make_simps lthy (unfold_thm, eqns : (Attrib.binding * term) list) =
   3.318 +  let
   3.319 +    val tacs =
   3.320 +      [rtac (unfold_thm RS @{thm ssubst_lhs}) 1,
   3.321 +       asm_simp_tac (local_simpset_of lthy) 1];
   3.322 +    fun prove_term t = Goal.prove lthy [] [] t (K (EVERY tacs));
   3.323 +    fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t);
   3.324 +  in
   3.325 +    map prove_eqn eqns
   3.326 +  end;
   3.327 +
   3.328 +(*************************************************************************)
   3.329 +(************************* Main fixrec function **************************)
   3.330 +(*************************************************************************)
   3.331 +
   3.332 +local
   3.333 +(* code adapted from HOL/Tools/primrec.ML *)
   3.334 +
   3.335 +fun gen_fixrec
   3.336 +  (set_group : bool)
   3.337 +  prep_spec
   3.338 +  (strict : bool)
   3.339 +  raw_fixes
   3.340 +  raw_spec
   3.341 +  (lthy : local_theory) =
   3.342 +  let
   3.343 +    val (fixes : ((binding * typ) * mixfix) list,
   3.344 +         spec : (Attrib.binding * term) list) =
   3.345 +          fst (prep_spec raw_fixes raw_spec lthy);
   3.346 +    val chead_of_spec =
   3.347 +      chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd;
   3.348 +    fun name_of (Free (n, _)) = n
   3.349 +      | name_of t = fixrec_err ("unknown term");
   3.350 +    val all_names = map (name_of o chead_of_spec) spec;
   3.351 +    val names = distinct (op =) all_names;
   3.352 +    fun block_of_name n =
   3.353 +      map_filter
   3.354 +        (fn (m,eq) => if m = n then SOME eq else NONE)
   3.355 +        (all_names ~~ spec);
   3.356 +    val blocks = map block_of_name names;
   3.357 +
   3.358 +    val matcher_tab = FixrecMatchData.get (ProofContext.theory_of lthy);
   3.359 +    fun match_name c =
   3.360 +      case Symtab.lookup matcher_tab c of SOME m => m
   3.361 +        | NONE => fixrec_err ("unknown pattern constructor: " ^ c);
   3.362 +
   3.363 +    val matches = map (compile_pats match_name) (map (map snd) blocks);
   3.364 +    val spec' = map (pair Attrib.empty_binding) matches;
   3.365 +    val (lthy', cnames, fixdef_thms, unfold_thms) =
   3.366 +      add_fixdefs fixes spec' lthy;
   3.367 +  in
   3.368 +    if strict then let (* only prove simp rules if strict = true *)
   3.369 +      val simps : (Attrib.binding * thm) list list =
   3.370 +        map (make_simps lthy') (unfold_thms ~~ blocks);
   3.371 +      fun mk_bind n : Attrib.binding =
   3.372 +       (Binding.name (n ^ "_simps"),
   3.373 +         [Attrib.internal (K Simplifier.simp_add)]);
   3.374 +      val simps1 : (Attrib.binding * thm list) list =
   3.375 +        map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps);
   3.376 +      val simps2 : (Attrib.binding * thm list) list =
   3.377 +        map (apsnd (fn thm => [thm])) (List.concat simps);
   3.378 +      val (_, lthy'') = lthy'
   3.379 +        |> fold_map (LocalTheory.note Thm.generatedK) (simps1 @ simps2);
   3.380 +    in
   3.381 +      lthy''
   3.382 +    end
   3.383 +    else lthy'
   3.384 +  end;
   3.385 +
   3.386 +in
   3.387 +
   3.388 +val add_fixrec = gen_fixrec false Specification.check_spec;
   3.389 +val add_fixrec_cmd = gen_fixrec true Specification.read_spec;
   3.390 +
   3.391 +end; (* local *)
   3.392 +
   3.393 +(*************************************************************************)
   3.394 +(******************************** Fixpat *********************************)
   3.395 +(*************************************************************************)
   3.396 +
   3.397 +fun fix_pat thy t = 
   3.398 +  let
   3.399 +    val T = fastype_of t;
   3.400 +    val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
   3.401 +    val cname = case chead_of t of Const(c,_) => c | _ =>
   3.402 +              fixrec_err "function is not declared as constant in theory";
   3.403 +    val unfold_thm = PureThy.get_thm thy (cname^"_unfold");
   3.404 +    val simp = Goal.prove_global thy [] [] eq
   3.405 +          (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
   3.406 +  in simp end;
   3.407 +
   3.408 +fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
   3.409 +  let
   3.410 +    val atts = map (prep_attrib thy) srcs;
   3.411 +    val ts = map (prep_term thy) strings;
   3.412 +    val simps = map (fix_pat thy) ts;
   3.413 +  in
   3.414 +    (snd o PureThy.add_thmss [((name, simps), atts)]) thy
   3.415 +  end;
   3.416 +
   3.417 +val add_fixpat = gen_add_fixpat Sign.cert_term (K I);
   3.418 +val add_fixpat_cmd = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
   3.419 +
   3.420 +
   3.421 +(*************************************************************************)
   3.422 +(******************************** Parsers ********************************)
   3.423 +(*************************************************************************)
   3.424 +
   3.425 +local structure P = OuterParse and K = OuterKeyword in
   3.426 +
   3.427 +val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl
   3.428 +  ((P.opt_keyword "permissive" >> not) -- P.fixes -- SpecParse.where_alt_specs
   3.429 +    >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
   3.430 +
   3.431 +val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
   3.432 +  (SpecParse.specs >> (Toplevel.theory o add_fixpat_cmd));
   3.433 +  
   3.434 +end;
   3.435 +
   3.436 +val setup = FixrecMatchData.init;
   3.437 +
   3.438 +end;
     4.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Sun Jun 21 15:45:42 2009 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,435 +0,0 @@
     4.4 -(*  Title:      HOLCF/Tools/fixrec.ML
     4.5 -    Author:     Amber Telfer and Brian Huffman
     4.6 -
     4.7 -Recursive function definition package for HOLCF.
     4.8 -*)
     4.9 -
    4.10 -signature FIXREC =
    4.11 -sig
    4.12 -  val add_fixrec: bool -> (binding * typ option * mixfix) list
    4.13 -    -> (Attrib.binding * term) list -> local_theory -> local_theory
    4.14 -  val add_fixrec_cmd: bool -> (binding * string option * mixfix) list
    4.15 -    -> (Attrib.binding * string) list -> local_theory -> local_theory
    4.16 -  val add_fixpat: Thm.binding * term list -> theory -> theory
    4.17 -  val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory
    4.18 -  val add_matchers: (string * string) list -> theory -> theory
    4.19 -  val setup: theory -> theory
    4.20 -end;
    4.21 -
    4.22 -structure Fixrec :> FIXREC =
    4.23 -struct
    4.24 -
    4.25 -val def_cont_fix_eq = @{thm def_cont_fix_eq};
    4.26 -val def_cont_fix_ind = @{thm def_cont_fix_ind};
    4.27 -
    4.28 -
    4.29 -fun fixrec_err s = error ("fixrec definition error:\n" ^ s);
    4.30 -fun fixrec_eq_err thy s eq =
    4.31 -  fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
    4.32 -
    4.33 -(*************************************************************************)
    4.34 -(***************************** building types ****************************)
    4.35 -(*************************************************************************)
    4.36 -
    4.37 -(* ->> is taken from holcf_logic.ML *)
    4.38 -fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
    4.39 -
    4.40 -infixr 6 ->>; val (op ->>) = cfunT;
    4.41 -
    4.42 -fun cfunsT (Ts, U) = foldr cfunT U Ts;
    4.43 -
    4.44 -fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
    4.45 -  | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
    4.46 -
    4.47 -fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
    4.48 -  | binder_cfun _   =  [];
    4.49 -
    4.50 -fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
    4.51 -  | body_cfun T   =  T;
    4.52 -
    4.53 -fun strip_cfun T : typ list * typ =
    4.54 -  (binder_cfun T, body_cfun T);
    4.55 -
    4.56 -fun maybeT T = Type(@{type_name "maybe"}, [T]);
    4.57 -
    4.58 -fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T
    4.59 -  | dest_maybeT T = raise TYPE ("dest_maybeT", [T], []);
    4.60 -
    4.61 -fun tupleT [] = HOLogic.unitT
    4.62 -  | tupleT [T] = T
    4.63 -  | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
    4.64 -
    4.65 -fun matchT (T, U) =
    4.66 -  body_cfun T ->> cfunsT (binder_cfun T, U) ->> U;
    4.67 -
    4.68 -
    4.69 -(*************************************************************************)
    4.70 -(***************************** building terms ****************************)
    4.71 -(*************************************************************************)
    4.72 -
    4.73 -val mk_trp = HOLogic.mk_Trueprop;
    4.74 -
    4.75 -(* splits a cterm into the right and lefthand sides of equality *)
    4.76 -fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
    4.77 -
    4.78 -(* similar to Thm.head_of, but for continuous application *)
    4.79 -fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f
    4.80 -  | chead_of u = u;
    4.81 -
    4.82 -fun capply_const (S, T) =
    4.83 -  Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T));
    4.84 -
    4.85 -fun cabs_const (S, T) =
    4.86 -  Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T));
    4.87 -
    4.88 -fun mk_cabs t =
    4.89 -  let val T = Term.fastype_of t
    4.90 -  in cabs_const (Term.domain_type T, Term.range_type T) $ t end
    4.91 -
    4.92 -fun mk_capply (t, u) =
    4.93 -  let val (S, T) =
    4.94 -    case Term.fastype_of t of
    4.95 -        Type(@{type_name "->"}, [S, T]) => (S, T)
    4.96 -      | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
    4.97 -  in capply_const (S, T) $ t $ u end;
    4.98 -
    4.99 -infix 0 ==;  val (op ==) = Logic.mk_equals;
   4.100 -infix 1 ===; val (op ===) = HOLogic.mk_eq;
   4.101 -infix 9 `  ; val (op `) = mk_capply;
   4.102 -
   4.103 -(* builds the expression (LAM v. rhs) *)
   4.104 -fun big_lambda v rhs =
   4.105 -  cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs;
   4.106 -
   4.107 -(* builds the expression (LAM v1 v2 .. vn. rhs) *)
   4.108 -fun big_lambdas [] rhs = rhs
   4.109 -  | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs);
   4.110 -
   4.111 -fun mk_return t =
   4.112 -  let val T = Term.fastype_of t
   4.113 -  in Const(@{const_name Fixrec.return}, T ->> maybeT T) ` t end;
   4.114 -
   4.115 -fun mk_bind (t, u) =
   4.116 -  let val (T, mU) = dest_cfunT (Term.fastype_of u);
   4.117 -      val bindT = maybeT T ->> (T ->> mU) ->> mU;
   4.118 -  in Const(@{const_name Fixrec.bind}, bindT) ` t ` u end;
   4.119 -
   4.120 -fun mk_mplus (t, u) =
   4.121 -  let val mT = Term.fastype_of t
   4.122 -  in Const(@{const_name Fixrec.mplus}, mT ->> mT ->> mT) ` t ` u end;
   4.123 -
   4.124 -fun mk_run t =
   4.125 -  let val mT = Term.fastype_of t
   4.126 -      val T = dest_maybeT mT
   4.127 -  in Const(@{const_name Fixrec.run}, mT ->> T) ` t end;
   4.128 -
   4.129 -fun mk_fix t =
   4.130 -  let val (T, _) = dest_cfunT (Term.fastype_of t)
   4.131 -  in Const(@{const_name fix}, (T ->> T) ->> T) ` t end;
   4.132 -
   4.133 -fun mk_cont t =
   4.134 -  let val T = Term.fastype_of t
   4.135 -  in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end;
   4.136 -
   4.137 -val mk_fst = HOLogic.mk_fst
   4.138 -val mk_snd = HOLogic.mk_snd
   4.139 -
   4.140 -(* builds the expression (v1,v2,..,vn) *)
   4.141 -fun mk_tuple [] = HOLogic.unit
   4.142 -|   mk_tuple (t::[]) = t
   4.143 -|   mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts);
   4.144 -
   4.145 -(* builds the expression (%(v1,v2,..,vn). rhs) *)
   4.146 -fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs
   4.147 -  | lambda_tuple (v::[]) rhs = Term.lambda v rhs
   4.148 -  | lambda_tuple (v::vs) rhs =
   4.149 -      HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs));
   4.150 -
   4.151 -
   4.152 -(*************************************************************************)
   4.153 -(************* fixed-point definitions and unfolding theorems ************)
   4.154 -(*************************************************************************)
   4.155 -
   4.156 -fun add_fixdefs
   4.157 -  (fixes : ((binding * typ) * mixfix) list)
   4.158 -  (spec : (Attrib.binding * term) list)
   4.159 -  (lthy : local_theory) =
   4.160 -  let
   4.161 -    val thy = ProofContext.theory_of lthy;
   4.162 -    val names = map (Binding.name_of o fst o fst) fixes;
   4.163 -    val all_names = space_implode "_" names;
   4.164 -    val (lhss,rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
   4.165 -    val functional = lambda_tuple lhss (mk_tuple rhss);
   4.166 -    val fixpoint = mk_fix (mk_cabs functional);
   4.167 -    
   4.168 -    val cont_thm =
   4.169 -      Goal.prove lthy [] [] (mk_trp (mk_cont functional))
   4.170 -        (K (simp_tac (local_simpset_of lthy) 1));
   4.171 -
   4.172 -    fun one_def (l as Free(n,_)) r =
   4.173 -          let val b = Long_Name.base_name n
   4.174 -          in ((Binding.name (b^"_def"), []), r) end
   4.175 -      | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form";
   4.176 -    fun defs [] _ = []
   4.177 -      | defs (l::[]) r = [one_def l r]
   4.178 -      | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r);
   4.179 -    val fixdefs = defs lhss fixpoint;
   4.180 -    val define_all = fold_map (LocalTheory.define Thm.definitionK);
   4.181 -    val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy
   4.182 -      |> define_all (map (apfst fst) fixes ~~ fixdefs);
   4.183 -    fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
   4.184 -    val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms);
   4.185 -    val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT);
   4.186 -    val predicate = lambda_tuple lhss (list_comb (P, lhss));
   4.187 -    val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm])
   4.188 -      |> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)]
   4.189 -      |> LocalDefs.unfold lthy @{thms split_paired_all split_conv split_strict};
   4.190 -    val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
   4.191 -      |> LocalDefs.unfold lthy' @{thms split_conv};
   4.192 -    fun unfolds [] thm = []
   4.193 -      | unfolds (n::[]) thm = [(n^"_unfold", thm)]
   4.194 -      | unfolds (n::ns) thm = let
   4.195 -          val thmL = thm RS @{thm Pair_eqD1};
   4.196 -          val thmR = thm RS @{thm Pair_eqD2};
   4.197 -        in (n^"_unfold", thmL) :: unfolds ns thmR end;
   4.198 -    val unfold_thms = unfolds names tuple_unfold_thm;
   4.199 -    fun mk_note (n, thm) = ((Binding.name n, []), [thm]);
   4.200 -    val (thmss, lthy'') = lthy'
   4.201 -      |> fold_map (LocalTheory.note Thm.generatedK o mk_note)
   4.202 -        ((all_names ^ "_induct", tuple_induct_thm) :: unfold_thms);
   4.203 -  in
   4.204 -    (lthy'', names, fixdef_thms, map snd unfold_thms)
   4.205 -  end;
   4.206 -
   4.207 -(*************************************************************************)
   4.208 -(*********** monadic notation and pattern matching compilation ***********)
   4.209 -(*************************************************************************)
   4.210 -
   4.211 -structure FixrecMatchData = TheoryDataFun (
   4.212 -  type T = string Symtab.table;
   4.213 -  val empty = Symtab.empty;
   4.214 -  val copy = I;
   4.215 -  val extend = I;
   4.216 -  fun merge _ tabs : T = Symtab.merge (K true) tabs;
   4.217 -);
   4.218 -
   4.219 -(* associate match functions with pattern constants *)
   4.220 -fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms);
   4.221 -
   4.222 -fun taken_names (t : term) : bstring list =
   4.223 -  let
   4.224 -    fun taken (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
   4.225 -      | taken (Free(a,_) , bs) = insert (op =) a bs
   4.226 -      | taken (f $ u     , bs) = taken (f, taken (u, bs))
   4.227 -      | taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs)
   4.228 -      | taken (_         , bs) = bs;
   4.229 -  in
   4.230 -    taken (t, [])
   4.231 -  end;
   4.232 -
   4.233 -(* builds a monadic term for matching a constructor pattern *)
   4.234 -fun pre_build match_name pat rhs vs taken =
   4.235 -  case pat of
   4.236 -    Const(@{const_name Rep_CFun},_)$f$(v as Free(n,T)) =>
   4.237 -      pre_build match_name f rhs (v::vs) taken
   4.238 -  | Const(@{const_name Rep_CFun},_)$f$x =>
   4.239 -      let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
   4.240 -      in pre_build match_name f rhs' (v::vs) taken' end
   4.241 -  | Const(c,T) =>
   4.242 -      let
   4.243 -        val n = Name.variant taken "v";
   4.244 -        fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
   4.245 -          | result_type T _ = T;
   4.246 -        val v = Free(n, result_type T vs);
   4.247 -        val m = Const(match_name c, matchT (T, fastype_of rhs));
   4.248 -        val k = big_lambdas vs rhs;
   4.249 -      in
   4.250 -        (m`v`k, v, n::taken)
   4.251 -      end
   4.252 -  | Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n)
   4.253 -  | _ => fixrec_err "pre_build: invalid pattern";
   4.254 -
   4.255 -(* builds a monadic term for matching a function definition pattern *)
   4.256 -(* returns (name, arity, matcher) *)
   4.257 -fun building match_name pat rhs vs taken =
   4.258 -  case pat of
   4.259 -    Const(@{const_name Rep_CFun}, _)$f$(v as Free(n,T)) =>
   4.260 -      building match_name f rhs (v::vs) taken
   4.261 -  | Const(@{const_name Rep_CFun}, _)$f$x =>
   4.262 -      let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
   4.263 -      in building match_name f rhs' (v::vs) taken' end
   4.264 -  | Free(_,_) => ((pat, length vs), big_lambdas vs rhs)
   4.265 -  | Const(_,_) => ((pat, length vs), big_lambdas vs rhs)
   4.266 -  | _ => fixrec_err ("function is not declared as constant in theory: "
   4.267 -                    ^ ML_Syntax.print_term pat);
   4.268 -
   4.269 -fun strip_alls t =
   4.270 -  if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t;
   4.271 -
   4.272 -fun match_eq match_name eq =
   4.273 -  let
   4.274 -    val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq));
   4.275 -  in
   4.276 -    building match_name lhs (mk_return rhs) [] (taken_names eq)
   4.277 -  end;
   4.278 -
   4.279 -(* returns the sum (using +++) of the terms in ms *)
   4.280 -(* also applies "run" to the result! *)
   4.281 -fun fatbar arity ms =
   4.282 -  let
   4.283 -    fun LAM_Ts 0 t = ([], Term.fastype_of t)
   4.284 -      | LAM_Ts n (_ $ Abs(_,T,t)) =
   4.285 -          let val (Ts, U) = LAM_Ts (n-1) t in (T::Ts, U) end
   4.286 -      | LAM_Ts _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
   4.287 -    fun unLAM 0 t = t
   4.288 -      | unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t
   4.289 -      | unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
   4.290 -    fun reLAM ([], U) t = t
   4.291 -      | reLAM (T::Ts, U) t = reLAM (Ts, T ->> U) (cabs_const(T,U)$Abs("",T,t));
   4.292 -    val msum = foldr1 mk_mplus (map (unLAM arity) ms);
   4.293 -    val (Ts, U) = LAM_Ts arity (hd ms)
   4.294 -  in
   4.295 -    reLAM (rev Ts, dest_maybeT U) (mk_run msum)
   4.296 -  end;
   4.297 -
   4.298 -(* this is the pattern-matching compiler function *)
   4.299 -fun compile_pats match_name eqs =
   4.300 -  let
   4.301 -    val (((n::names),(a::arities)),mats) =
   4.302 -      apfst ListPair.unzip (ListPair.unzip (map (match_eq match_name) eqs));
   4.303 -    val cname = if forall (fn x => n=x) names then n
   4.304 -          else fixrec_err "all equations in block must define the same function";
   4.305 -    val arity = if forall (fn x => a=x) arities then a
   4.306 -          else fixrec_err "all equations in block must have the same arity";
   4.307 -    val rhs = fatbar arity mats;
   4.308 -  in
   4.309 -    mk_trp (cname === rhs)
   4.310 -  end;
   4.311 -
   4.312 -(*************************************************************************)
   4.313 -(********************** Proving associated theorems **********************)
   4.314 -(*************************************************************************)
   4.315 -
   4.316 -(* proves a block of pattern matching equations as theorems, using unfold *)
   4.317 -fun make_simps lthy (unfold_thm, eqns : (Attrib.binding * term) list) =
   4.318 -  let
   4.319 -    val tacs =
   4.320 -      [rtac (unfold_thm RS @{thm ssubst_lhs}) 1,
   4.321 -       asm_simp_tac (local_simpset_of lthy) 1];
   4.322 -    fun prove_term t = Goal.prove lthy [] [] t (K (EVERY tacs));
   4.323 -    fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t);
   4.324 -  in
   4.325 -    map prove_eqn eqns
   4.326 -  end;
   4.327 -
   4.328 -(*************************************************************************)
   4.329 -(************************* Main fixrec function **************************)
   4.330 -(*************************************************************************)
   4.331 -
   4.332 -local
   4.333 -(* code adapted from HOL/Tools/primrec.ML *)
   4.334 -
   4.335 -fun gen_fixrec
   4.336 -  (set_group : bool)
   4.337 -  prep_spec
   4.338 -  (strict : bool)
   4.339 -  raw_fixes
   4.340 -  raw_spec
   4.341 -  (lthy : local_theory) =
   4.342 -  let
   4.343 -    val (fixes : ((binding * typ) * mixfix) list,
   4.344 -         spec : (Attrib.binding * term) list) =
   4.345 -          fst (prep_spec raw_fixes raw_spec lthy);
   4.346 -    val chead_of_spec =
   4.347 -      chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd;
   4.348 -    fun name_of (Free (n, _)) = n
   4.349 -      | name_of t = fixrec_err ("unknown term");
   4.350 -    val all_names = map (name_of o chead_of_spec) spec;
   4.351 -    val names = distinct (op =) all_names;
   4.352 -    fun block_of_name n =
   4.353 -      map_filter
   4.354 -        (fn (m,eq) => if m = n then SOME eq else NONE)
   4.355 -        (all_names ~~ spec);
   4.356 -    val blocks = map block_of_name names;
   4.357 -
   4.358 -    val matcher_tab = FixrecMatchData.get (ProofContext.theory_of lthy);
   4.359 -    fun match_name c =
   4.360 -      case Symtab.lookup matcher_tab c of SOME m => m
   4.361 -        | NONE => fixrec_err ("unknown pattern constructor: " ^ c);
   4.362 -
   4.363 -    val matches = map (compile_pats match_name) (map (map snd) blocks);
   4.364 -    val spec' = map (pair Attrib.empty_binding) matches;
   4.365 -    val (lthy', cnames, fixdef_thms, unfold_thms) =
   4.366 -      add_fixdefs fixes spec' lthy;
   4.367 -  in
   4.368 -    if strict then let (* only prove simp rules if strict = true *)
   4.369 -      val simps : (Attrib.binding * thm) list list =
   4.370 -        map (make_simps lthy') (unfold_thms ~~ blocks);
   4.371 -      fun mk_bind n : Attrib.binding =
   4.372 -       (Binding.name (n ^ "_simps"),
   4.373 -         [Attrib.internal (K Simplifier.simp_add)]);
   4.374 -      val simps1 : (Attrib.binding * thm list) list =
   4.375 -        map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps);
   4.376 -      val simps2 : (Attrib.binding * thm list) list =
   4.377 -        map (apsnd (fn thm => [thm])) (List.concat simps);
   4.378 -      val (_, lthy'') = lthy'
   4.379 -        |> fold_map (LocalTheory.note Thm.generatedK) (simps1 @ simps2);
   4.380 -    in
   4.381 -      lthy''
   4.382 -    end
   4.383 -    else lthy'
   4.384 -  end;
   4.385 -
   4.386 -in
   4.387 -
   4.388 -val add_fixrec = gen_fixrec false Specification.check_spec;
   4.389 -val add_fixrec_cmd = gen_fixrec true Specification.read_spec;
   4.390 -
   4.391 -end; (* local *)
   4.392 -
   4.393 -(*************************************************************************)
   4.394 -(******************************** Fixpat *********************************)
   4.395 -(*************************************************************************)
   4.396 -
   4.397 -fun fix_pat thy t = 
   4.398 -  let
   4.399 -    val T = fastype_of t;
   4.400 -    val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
   4.401 -    val cname = case chead_of t of Const(c,_) => c | _ =>
   4.402 -              fixrec_err "function is not declared as constant in theory";
   4.403 -    val unfold_thm = PureThy.get_thm thy (cname^"_unfold");
   4.404 -    val simp = Goal.prove_global thy [] [] eq
   4.405 -          (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
   4.406 -  in simp end;
   4.407 -
   4.408 -fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
   4.409 -  let
   4.410 -    val atts = map (prep_attrib thy) srcs;
   4.411 -    val ts = map (prep_term thy) strings;
   4.412 -    val simps = map (fix_pat thy) ts;
   4.413 -  in
   4.414 -    (snd o PureThy.add_thmss [((name, simps), atts)]) thy
   4.415 -  end;
   4.416 -
   4.417 -val add_fixpat = gen_add_fixpat Sign.cert_term (K I);
   4.418 -val add_fixpat_cmd = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
   4.419 -
   4.420 -
   4.421 -(*************************************************************************)
   4.422 -(******************************** Parsers ********************************)
   4.423 -(*************************************************************************)
   4.424 -
   4.425 -local structure P = OuterParse and K = OuterKeyword in
   4.426 -
   4.427 -val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl
   4.428 -  ((P.opt_keyword "permissive" >> not) -- P.fixes -- SpecParse.where_alt_specs
   4.429 -    >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
   4.430 -
   4.431 -val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
   4.432 -  (SpecParse.specs >> (Toplevel.theory o add_fixpat_cmd));
   4.433 -  
   4.434 -end;
   4.435 -
   4.436 -val setup = FixrecMatchData.init;
   4.437 -
   4.438 -end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Sun Jun 21 15:45:57 2009 +0200
     5.3 @@ -0,0 +1,201 @@
     5.4 +(*  Title:      HOLCF/Tools/pcpodef.ML
     5.5 +    Author:     Brian Huffman
     5.6 +
     5.7 +Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
     5.8 +typedef (see also ~~/src/HOL/Tools/typedef.ML).
     5.9 +*)
    5.10 +
    5.11 +signature PCPODEF =
    5.12 +sig
    5.13 +  val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
    5.14 +    * (binding * binding) option -> theory -> Proof.state
    5.15 +  val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
    5.16 +    * (binding * binding) option -> theory -> Proof.state
    5.17 +  val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
    5.18 +    * (binding * binding) option -> theory -> Proof.state
    5.19 +  val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
    5.20 +    * (binding * binding) option -> theory -> Proof.state
    5.21 +end;
    5.22 +
    5.23 +structure Pcpodef :> PCPODEF =
    5.24 +struct
    5.25 +
    5.26 +(** type definitions **)
    5.27 +
    5.28 +(* prepare_cpodef *)
    5.29 +
    5.30 +fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
    5.31 +
    5.32 +fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
    5.33 +fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
    5.34 +
    5.35 +fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =
    5.36 +  let
    5.37 +    val _ = Theory.requires thy "Pcpodef" "pcpodefs";
    5.38 +    val ctxt = ProofContext.init thy;
    5.39 +
    5.40 +    val full = Sign.full_name thy;
    5.41 +    val full_name = full name;
    5.42 +    val bname = Binding.name_of name;
    5.43 +
    5.44 +    (*rhs*)
    5.45 +    val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
    5.46 +    val setT = Term.fastype_of set;
    5.47 +    val rhs_tfrees = Term.add_tfrees set [];
    5.48 +    val oldT = HOLogic.dest_setT setT handle TYPE _ =>
    5.49 +      error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
    5.50 +
    5.51 +    (*goal*)
    5.52 +    val goal_UU_mem = HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
    5.53 +    val goal_nonempty =
    5.54 +      HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
    5.55 +    val goal_admissible =
    5.56 +      HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
    5.57 +
    5.58 +    (*lhs*)
    5.59 +    val defS = Sign.defaultS thy;
    5.60 +    val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
    5.61 +    val lhs_sorts = map snd lhs_tfrees;
    5.62 +
    5.63 +    val tname = Binding.map_name (Syntax.type_name mx) t;
    5.64 +    val full_tname = full tname;
    5.65 +    val newT = Type (full_tname, map TFree lhs_tfrees);
    5.66 +
    5.67 +    val (Rep_name, Abs_name) =
    5.68 +      (case opt_morphs of
    5.69 +        NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
    5.70 +      | SOME morphs => morphs);
    5.71 +    val RepC = Const (full Rep_name, newT --> oldT);
    5.72 +    fun belowC T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
    5.73 +    val below_def = Logic.mk_equals (belowC newT,
    5.74 +      Abs ("x", newT, Abs ("y", newT, belowC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
    5.75 +
    5.76 +    fun make_po tac thy1 =
    5.77 +      let
    5.78 +        val ((_, {type_definition, set_def, ...}), thy2) = thy1
    5.79 +          |> Typedef.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
    5.80 +        val lthy3 = thy2
    5.81 +          |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
    5.82 +        val below_def' = Syntax.check_term lthy3 below_def;
    5.83 +        val ((_, (_, below_definition')), lthy4) = lthy3
    5.84 +          |> Specification.definition (NONE,
    5.85 +              ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def'));
    5.86 +        val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
    5.87 +        val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition';
    5.88 +        val thy5 = lthy4
    5.89 +          |> Class.prove_instantiation_instance
    5.90 +              (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
    5.91 +          |> LocalTheory.exit_global;
    5.92 +      in ((type_definition, below_definition, set_def), thy5) end;
    5.93 +
    5.94 +    fun make_cpo admissible (type_def, below_def, set_def) theory =
    5.95 +      let
    5.96 +        val admissible' = fold_rule (the_list set_def) admissible;
    5.97 +        val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible'];
    5.98 +        val theory' = theory
    5.99 +          |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
   5.100 +            (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
   5.101 +        val cpo_thms' = map (Thm.transfer theory') cpo_thms;
   5.102 +      in
   5.103 +        theory'
   5.104 +        |> Sign.add_path (Binding.name_of name)
   5.105 +        |> PureThy.add_thms
   5.106 +          ([((Binding.prefix_name "adm_" name, admissible'), []),
   5.107 +            ((Binding.prefix_name "cont_" Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []),
   5.108 +            ((Binding.prefix_name "cont_" Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []),
   5.109 +            ((Binding.prefix_name "lub_" name, @{thm typedef_lub} OF cpo_thms'), []),
   5.110 +            ((Binding.prefix_name "thelub_" name, @{thm typedef_thelub} OF cpo_thms'), []),
   5.111 +            ((Binding.prefix_name "compact_" name, @{thm typedef_compact} OF cpo_thms'), [])])
   5.112 +        |> snd
   5.113 +        |> Sign.parent_path
   5.114 +      end;
   5.115 +
   5.116 +    fun make_pcpo UU_mem (type_def, below_def, set_def) theory =
   5.117 +      let
   5.118 +        val UU_mem' = fold_rule (the_list set_def) UU_mem;
   5.119 +        val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem'];
   5.120 +        val theory' = theory
   5.121 +          |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
   5.122 +            (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
   5.123 +        val pcpo_thms' = map (Thm.transfer theory') pcpo_thms;
   5.124 +      in
   5.125 +        theory'
   5.126 +        |> Sign.add_path (Binding.name_of name)
   5.127 +        |> PureThy.add_thms
   5.128 +          ([((Binding.suffix_name "_strict" Rep_name, @{thm typedef_Rep_strict} OF pcpo_thms'), []),
   5.129 +            ((Binding.suffix_name "_strict" Abs_name, @{thm typedef_Abs_strict} OF pcpo_thms'), []),
   5.130 +            ((Binding.suffix_name "_strict_iff" Rep_name, @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
   5.131 +            ((Binding.suffix_name "_strict_iff" Abs_name, @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
   5.132 +            ((Binding.suffix_name "_defined" Rep_name, @{thm typedef_Rep_defined} OF pcpo_thms'), []),
   5.133 +            ((Binding.suffix_name "_defined" Abs_name, @{thm typedef_Abs_defined} OF pcpo_thms'), [])])
   5.134 +        |> snd
   5.135 +        |> Sign.parent_path
   5.136 +      end;
   5.137 +
   5.138 +    fun pcpodef_result UU_mem admissible =
   5.139 +      make_po (Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1)
   5.140 +      #-> (fn defs => make_cpo admissible defs #> make_pcpo UU_mem defs);
   5.141 +
   5.142 +    fun cpodef_result nonempty admissible =
   5.143 +      make_po (Tactic.rtac nonempty 1)
   5.144 +      #-> make_cpo admissible;
   5.145 +  in
   5.146 +    if pcpo
   5.147 +    then (goal_UU_mem, goal_admissible, pcpodef_result)
   5.148 +    else (goal_nonempty, goal_admissible, cpodef_result)
   5.149 +  end
   5.150 +  handle ERROR msg =>
   5.151 +    cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
   5.152 +
   5.153 +
   5.154 +(* proof interface *)
   5.155 +
   5.156 +local
   5.157 +
   5.158 +fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy =
   5.159 +  let
   5.160 +    val (goal1, goal2, make_result) =
   5.161 +      prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
   5.162 +    fun after_qed [[th1, th2]] = ProofContext.theory (make_result th1 th2);
   5.163 +  in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end;
   5.164 +
   5.165 +in
   5.166 +
   5.167 +fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term true x;
   5.168 +fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term true x;
   5.169 +
   5.170 +fun cpodef_proof x = gen_pcpodef_proof Syntax.check_term false x;
   5.171 +fun cpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term false x;
   5.172 +
   5.173 +end;
   5.174 +
   5.175 +
   5.176 +
   5.177 +(** outer syntax **)
   5.178 +
   5.179 +local structure P = OuterParse and K = OuterKeyword in
   5.180 +
   5.181 +val typedef_proof_decl =
   5.182 +  Scan.optional (P.$$$ "(" |--
   5.183 +      ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
   5.184 +        --| P.$$$ ")") (true, NONE) --
   5.185 +    (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
   5.186 +    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
   5.187 +
   5.188 +fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
   5.189 +  (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
   5.190 +    ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs);
   5.191 +
   5.192 +val _ =
   5.193 +  OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
   5.194 +    (typedef_proof_decl >>
   5.195 +      (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
   5.196 +
   5.197 +val _ =
   5.198 +  OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
   5.199 +    (typedef_proof_decl >>
   5.200 +      (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
   5.201 +
   5.202 +end;
   5.203 +
   5.204 +end;
     6.1 --- a/src/HOLCF/Tools/pcpodef_package.ML	Sun Jun 21 15:45:42 2009 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,201 +0,0 @@
     6.4 -(*  Title:      HOLCF/Tools/pcpodef.ML
     6.5 -    Author:     Brian Huffman
     6.6 -
     6.7 -Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
     6.8 -typedef (see also ~~/src/HOL/Tools/typedef.ML).
     6.9 -*)
    6.10 -
    6.11 -signature PCPODEF =
    6.12 -sig
    6.13 -  val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
    6.14 -    * (binding * binding) option -> theory -> Proof.state
    6.15 -  val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
    6.16 -    * (binding * binding) option -> theory -> Proof.state
    6.17 -  val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
    6.18 -    * (binding * binding) option -> theory -> Proof.state
    6.19 -  val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
    6.20 -    * (binding * binding) option -> theory -> Proof.state
    6.21 -end;
    6.22 -
    6.23 -structure Pcpodef :> PCPODEF =
    6.24 -struct
    6.25 -
    6.26 -(** type definitions **)
    6.27 -
    6.28 -(* prepare_cpodef *)
    6.29 -
    6.30 -fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
    6.31 -
    6.32 -fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
    6.33 -fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
    6.34 -
    6.35 -fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =
    6.36 -  let
    6.37 -    val _ = Theory.requires thy "Pcpodef" "pcpodefs";
    6.38 -    val ctxt = ProofContext.init thy;
    6.39 -
    6.40 -    val full = Sign.full_name thy;
    6.41 -    val full_name = full name;
    6.42 -    val bname = Binding.name_of name;
    6.43 -
    6.44 -    (*rhs*)
    6.45 -    val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
    6.46 -    val setT = Term.fastype_of set;
    6.47 -    val rhs_tfrees = Term.add_tfrees set [];
    6.48 -    val oldT = HOLogic.dest_setT setT handle TYPE _ =>
    6.49 -      error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
    6.50 -
    6.51 -    (*goal*)
    6.52 -    val goal_UU_mem = HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
    6.53 -    val goal_nonempty =
    6.54 -      HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
    6.55 -    val goal_admissible =
    6.56 -      HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
    6.57 -
    6.58 -    (*lhs*)
    6.59 -    val defS = Sign.defaultS thy;
    6.60 -    val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
    6.61 -    val lhs_sorts = map snd lhs_tfrees;
    6.62 -
    6.63 -    val tname = Binding.map_name (Syntax.type_name mx) t;
    6.64 -    val full_tname = full tname;
    6.65 -    val newT = Type (full_tname, map TFree lhs_tfrees);
    6.66 -
    6.67 -    val (Rep_name, Abs_name) =
    6.68 -      (case opt_morphs of
    6.69 -        NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
    6.70 -      | SOME morphs => morphs);
    6.71 -    val RepC = Const (full Rep_name, newT --> oldT);
    6.72 -    fun belowC T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
    6.73 -    val below_def = Logic.mk_equals (belowC newT,
    6.74 -      Abs ("x", newT, Abs ("y", newT, belowC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
    6.75 -
    6.76 -    fun make_po tac thy1 =
    6.77 -      let
    6.78 -        val ((_, {type_definition, set_def, ...}), thy2) = thy1
    6.79 -          |> Typedef.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
    6.80 -        val lthy3 = thy2
    6.81 -          |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
    6.82 -        val below_def' = Syntax.check_term lthy3 below_def;
    6.83 -        val ((_, (_, below_definition')), lthy4) = lthy3
    6.84 -          |> Specification.definition (NONE,
    6.85 -              ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def'));
    6.86 -        val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
    6.87 -        val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition';
    6.88 -        val thy5 = lthy4
    6.89 -          |> Class.prove_instantiation_instance
    6.90 -              (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
    6.91 -          |> LocalTheory.exit_global;
    6.92 -      in ((type_definition, below_definition, set_def), thy5) end;
    6.93 -
    6.94 -    fun make_cpo admissible (type_def, below_def, set_def) theory =
    6.95 -      let
    6.96 -        val admissible' = fold_rule (the_list set_def) admissible;
    6.97 -        val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible'];
    6.98 -        val theory' = theory
    6.99 -          |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
   6.100 -            (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
   6.101 -        val cpo_thms' = map (Thm.transfer theory') cpo_thms;
   6.102 -      in
   6.103 -        theory'
   6.104 -        |> Sign.add_path (Binding.name_of name)
   6.105 -        |> PureThy.add_thms
   6.106 -          ([((Binding.prefix_name "adm_" name, admissible'), []),
   6.107 -            ((Binding.prefix_name "cont_" Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []),
   6.108 -            ((Binding.prefix_name "cont_" Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []),
   6.109 -            ((Binding.prefix_name "lub_" name, @{thm typedef_lub} OF cpo_thms'), []),
   6.110 -            ((Binding.prefix_name "thelub_" name, @{thm typedef_thelub} OF cpo_thms'), []),
   6.111 -            ((Binding.prefix_name "compact_" name, @{thm typedef_compact} OF cpo_thms'), [])])
   6.112 -        |> snd
   6.113 -        |> Sign.parent_path
   6.114 -      end;
   6.115 -
   6.116 -    fun make_pcpo UU_mem (type_def, below_def, set_def) theory =
   6.117 -      let
   6.118 -        val UU_mem' = fold_rule (the_list set_def) UU_mem;
   6.119 -        val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem'];
   6.120 -        val theory' = theory
   6.121 -          |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
   6.122 -            (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
   6.123 -        val pcpo_thms' = map (Thm.transfer theory') pcpo_thms;
   6.124 -      in
   6.125 -        theory'
   6.126 -        |> Sign.add_path (Binding.name_of name)
   6.127 -        |> PureThy.add_thms
   6.128 -          ([((Binding.suffix_name "_strict" Rep_name, @{thm typedef_Rep_strict} OF pcpo_thms'), []),
   6.129 -            ((Binding.suffix_name "_strict" Abs_name, @{thm typedef_Abs_strict} OF pcpo_thms'), []),
   6.130 -            ((Binding.suffix_name "_strict_iff" Rep_name, @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
   6.131 -            ((Binding.suffix_name "_strict_iff" Abs_name, @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
   6.132 -            ((Binding.suffix_name "_defined" Rep_name, @{thm typedef_Rep_defined} OF pcpo_thms'), []),
   6.133 -            ((Binding.suffix_name "_defined" Abs_name, @{thm typedef_Abs_defined} OF pcpo_thms'), [])])
   6.134 -        |> snd
   6.135 -        |> Sign.parent_path
   6.136 -      end;
   6.137 -
   6.138 -    fun pcpodef_result UU_mem admissible =
   6.139 -      make_po (Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1)
   6.140 -      #-> (fn defs => make_cpo admissible defs #> make_pcpo UU_mem defs);
   6.141 -
   6.142 -    fun cpodef_result nonempty admissible =
   6.143 -      make_po (Tactic.rtac nonempty 1)
   6.144 -      #-> make_cpo admissible;
   6.145 -  in
   6.146 -    if pcpo
   6.147 -    then (goal_UU_mem, goal_admissible, pcpodef_result)
   6.148 -    else (goal_nonempty, goal_admissible, cpodef_result)
   6.149 -  end
   6.150 -  handle ERROR msg =>
   6.151 -    cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
   6.152 -
   6.153 -
   6.154 -(* proof interface *)
   6.155 -
   6.156 -local
   6.157 -
   6.158 -fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy =
   6.159 -  let
   6.160 -    val (goal1, goal2, make_result) =
   6.161 -      prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
   6.162 -    fun after_qed [[th1, th2]] = ProofContext.theory (make_result th1 th2);
   6.163 -  in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end;
   6.164 -
   6.165 -in
   6.166 -
   6.167 -fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term true x;
   6.168 -fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term true x;
   6.169 -
   6.170 -fun cpodef_proof x = gen_pcpodef_proof Syntax.check_term false x;
   6.171 -fun cpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term false x;
   6.172 -
   6.173 -end;
   6.174 -
   6.175 -
   6.176 -
   6.177 -(** outer syntax **)
   6.178 -
   6.179 -local structure P = OuterParse and K = OuterKeyword in
   6.180 -
   6.181 -val typedef_proof_decl =
   6.182 -  Scan.optional (P.$$$ "(" |--
   6.183 -      ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
   6.184 -        --| P.$$$ ")") (true, NONE) --
   6.185 -    (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
   6.186 -    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
   6.187 -
   6.188 -fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
   6.189 -  (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
   6.190 -    ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs);
   6.191 -
   6.192 -val _ =
   6.193 -  OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
   6.194 -    (typedef_proof_decl >>
   6.195 -      (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
   6.196 -
   6.197 -val _ =
   6.198 -  OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
   6.199 -    (typedef_proof_decl >>
   6.200 -      (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
   6.201 -
   6.202 -end;
   6.203 -
   6.204 -end;