--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/ioa.ML Sun Jun 21 15:45:57 2009 +0200
@@ -0,0 +1,536 @@
+(* Title: HOLCF/IOA/meta_theory/ioa.ML
+ Author: Tobias Hamberger, TU Muenchen
+*)
+
+signature IOA =
+sig
+ val add_ioa: string -> string
+ -> (string) list -> (string) list -> (string) list
+ -> (string * string) list -> string
+ -> (string * string * (string * string)list) list
+ -> theory -> theory
+ val add_composition : string -> (string)list -> theory -> theory
+ val add_hiding : string -> string -> (string)list -> theory -> theory
+ val add_restriction : string -> string -> (string)list -> theory -> theory
+ val add_rename : string -> string -> string -> theory -> theory
+end;
+
+structure Ioa: IOA =
+struct
+
+val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
+val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global;
+
+exception malformed;
+
+(* stripping quotes *)
+fun strip [] = [] |
+strip ("\""::r) = strip r |
+strip (a::r) = a :: (strip r);
+fun strip_quote s = implode(strip(explode(s)));
+
+(* used by *_of_varlist *)
+fun extract_first (a,b) = strip_quote a;
+fun extract_second (a,b) = strip_quote b;
+(* following functions producing sth from a varlist *)
+fun comma_list_of_varlist [] = "" |
+comma_list_of_varlist [a] = extract_first a |
+comma_list_of_varlist (a::r) = (extract_first a) ^ "," ^ (comma_list_of_varlist r);
+fun primed_comma_list_of_varlist [] = "" |
+primed_comma_list_of_varlist [a] = (extract_first a) ^ "'" |
+primed_comma_list_of_varlist (a::r) = (extract_first a) ^ "'," ^
+ (primed_comma_list_of_varlist r);
+fun type_product_of_varlist [] = "" |
+type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" |
+type_product_of_varlist(a::r) = "(" ^ extract_second(a) ^ ")*" ^ type_product_of_varlist r;
+
+(* listing a list *)
+fun list_elements_of [] = "" |
+list_elements_of (a::r) = a ^ " " ^ (list_elements_of r);
+
+(* extracting type parameters from a type list *)
+(* fun param_tupel thy [] res = res |
+param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res |
+param_tupel thy ((TFree(a,_))::r) res =
+if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) |
+param_tupel thy (a::r) res =
+error ("one component of a statetype is a TVar: " ^ (string_of_typ thy a));
+*)
+
+(* used by constr_list *)
+fun extract_constrs thy [] = [] |
+extract_constrs thy (a::r) =
+let
+fun delete_bold [] = []
+| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
+ then (let val (_::_::_::s) = xs in delete_bold s end)
+ else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
+ then (let val (_::_::_::s) = xs in delete_bold s end)
+ else (x::delete_bold xs));
+fun delete_bold_string s = implode(delete_bold(explode s));
+(* from a constructor term in *.induct (with quantifiers,
+"Trueprop" and ?P stripped away) delivers the head *)
+fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r |
+extract_hd (Const("Trueprop",_) $ r) = extract_hd r |
+extract_hd (Var(_,_) $ r) = extract_hd r |
+extract_hd (a $ b) = extract_hd a |
+extract_hd (Const(s,_)) = s |
+extract_hd _ = raise malformed;
+(* delivers constructor term string from a prem of *.induct *)
+fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))|
+extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r |
+extract_constr thy (Var(_,_) $ r) = delete_bold_string(string_of_term thy r) |
+extract_constr _ _ = raise malformed;
+in
+(extract_hd a,extract_constr thy a) :: (extract_constrs thy r)
+end;
+
+(* delivering list of constructor terms of a datatype *)
+fun constr_list thy atyp =
+let
+fun act_name thy (Type(s,_)) = s |
+act_name _ s =
+error("malformed action type: " ^ (string_of_typ thy s));
+fun afpl ("." :: a) = [] |
+afpl [] = [] |
+afpl (a::r) = a :: (afpl r);
+fun unqualify s = implode(rev(afpl(rev(explode s))));
+val q_atypstr = act_name thy atyp;
+val uq_atypstr = unqualify q_atypstr;
+val prem = prems_of (PureThy.get_thm thy (uq_atypstr ^ ".induct"));
+in
+extract_constrs thy prem
+handle malformed =>
+error("malformed theorem : " ^ uq_atypstr ^ ".induct")
+end;
+
+fun check_for_constr thy atyp (a $ b) =
+let
+fun all_free (Free(_,_)) = true |
+all_free (a $ b) = if (all_free a) then (all_free b) else false |
+all_free _ = false;
+in
+if (all_free b) then (check_for_constr thy atyp a) else false
+end |
+check_for_constr thy atyp (Const(a,_)) =
+let
+val cl = constr_list thy atyp;
+fun fstmem a [] = false |
+fstmem a ((f,s)::r) = if (a=f) then true else (fstmem a r)
+in
+if (fstmem a cl) then true else false
+end |
+check_for_constr _ _ _ = false;
+
+(* delivering the free variables of a constructor term *)
+fun free_vars_of (t1 $ t2) = (free_vars_of t1) @ (free_vars_of t2) |
+free_vars_of (Const(_,_)) = [] |
+free_vars_of (Free(a,_)) = [a] |
+free_vars_of _ = raise malformed;
+
+(* making a constructor set from a constructor term (of signature) *)
+fun constr_set_string thy atyp ctstr =
+let
+val trm = OldGoals.simple_read_term thy atyp ctstr;
+val l = free_vars_of trm
+in
+if (check_for_constr thy atyp trm) then
+(if (l=[]) then ("{" ^ ctstr ^ "}")
+else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})")
+else (raise malformed)
+handle malformed =>
+error("malformed action term: " ^ (string_of_term thy trm))
+end;
+
+(* extracting constructor heads *)
+fun constructor_head thy atypstr s =
+let
+fun hd_of (Const(a,_)) = a |
+hd_of (t $ _) = hd_of t |
+hd_of _ = raise malformed;
+val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
+in
+hd_of trm handle malformed =>
+error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
+end;
+fun constructor_head_list _ _ [] = [] |
+constructor_head_list thy atypstr (a::r) =
+ (constructor_head thy atypstr a)::(constructor_head_list thy atypstr r);
+
+(* producing an action set *)
+(*FIXME*)
+fun action_set_string thy atyp [] = "Set.empty" |
+action_set_string thy atyp [a] = constr_set_string thy atyp (strip_quote a) |
+action_set_string thy atyp (a::r) = (constr_set_string thy atyp (strip_quote a)) ^
+ " Un " ^ (action_set_string thy atyp r);
+
+(* used by extend *)
+fun pstr s [] = "(" ^ s ^ "' = " ^ s ^ ")" |
+pstr s ((a,b)::r) =
+if (s=a) then ("(" ^ s ^ "' = (" ^ b ^ "))") else (pstr s r);
+fun poststring [] l = "" |
+poststring [(a,b)] l = pstr a l |
+poststring ((a,b)::r) l = (pstr a l) ^ " & " ^ (poststring r l);
+
+(* extends a (action string,condition,assignlist) tupel by a
+(action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list
+(where bool indicates whether there is a precondition *)
+fun extend thy atyp statetupel (actstr,r,[]) =
+let
+val trm = OldGoals.simple_read_term thy atyp actstr;
+val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
+val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
+in
+if (check_for_constr thy atyp trm)
+then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag)
+else
+error("transition " ^ actstr ^ " is not a pure constructor term")
+end |
+extend thy atyp statetupel (actstr,r,(a,b)::c) =
+let
+fun pseudo_poststring [] = "" |
+pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
+pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r);
+val trm = OldGoals.simple_read_term thy atyp actstr;
+val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
+val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
+in
+if (check_for_constr thy atyp trm) then
+(if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false)
+(* the case with transrel *)
+ else
+ (trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)),
+ "(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag))
+else
+error("transition " ^ actstr ^ " is not a pure constructor term")
+end;
+(* used by make_alt_string *)
+fun extended_list _ _ _ [] = [] |
+extended_list thy atyp statetupel (a::r) =
+ (extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r);
+
+(* used by write_alts *)
+fun write_alt thy (chead,tr) inp out int [] =
+if (chead mem inp) then
+(
+error("Input action " ^ tr ^ " was not specified")
+) else (
+if (chead mem (out@int)) then
+(writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else ();
+(tr ^ " => False",tr ^ " => False")) |
+write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) =
+let
+fun hd_of (Const(a,_)) = a |
+hd_of (t $ _) = hd_of t |
+hd_of _ = raise malformed;
+fun occurs_again c [] = false |
+occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r);
+in
+if (chead=(hd_of a)) then
+(if ((chead mem inp) andalso e) then (
+error("Input action " ^ b ^ " has a precondition")
+) else (if (chead mem (inp@out@int)) then
+ (if (occurs_again chead r) then (
+error("Two specifications for action: " ^ b)
+ ) else (b ^ " => " ^ c,b ^ " => " ^ d))
+ else (
+error("Action " ^ b ^ " is not in automaton signature")
+))) else (write_alt thy (chead,ctrm) inp out int r)
+handle malformed =>
+error ("malformed action term: " ^ (string_of_term thy a))
+end;
+
+(* used by make_alt_string *)
+fun write_alts thy (a,b) inp out int [] ttr = (a,b) |
+write_alts thy (a,b) inp out int [c] ttr =
+let
+val wa = write_alt thy c inp out int ttr
+in
+ (a ^ (fst wa),b ^ (snd wa))
+end |
+write_alts thy (a,b) inp out int (c::r) ttr =
+let
+val wa = write_alt thy c inp out int ttr
+in
+ write_alts thy (a ^ (fst wa) ^ " | ", b ^ (snd wa) ^ " | ") inp out int r ttr
+end;
+
+fun make_alt_string thy inp out int atyp statetupel trans =
+let
+val cl = constr_list thy atyp;
+val ttr = extended_list thy atyp statetupel trans;
+in
+write_alts thy ("","") inp out int cl ttr
+end;
+
+(* used in add_ioa *)
+fun check_free_primed (Free(a,_)) =
+let
+val (f::r) = rev(explode a)
+in
+if (f="'") then [a] else []
+end |
+check_free_primed (a $ b) = ((check_free_primed a) @ (check_free_primed b)) |
+check_free_primed (Abs(_,_,t)) = check_free_primed t |
+check_free_primed _ = [];
+
+fun overlap [] _ = true |
+overlap (a::r) l = if (a mem l) then (
+error("Two occurences of action " ^ a ^ " in automaton signature")
+) else (overlap r l);
+
+(* delivering some types of an automaton *)
+fun aut_type_of thy aut_name =
+let
+fun left_of (( _ $ left) $ _) = left |
+left_of _ = raise malformed;
+val aut_def = concl_of (PureThy.get_thm thy (aut_name ^ "_def"));
+in
+(#T(rep_cterm(cterm_of thy (left_of aut_def))))
+handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
+end;
+
+fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp |
+act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^
+(string_of_typ thy t));
+fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp |
+st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^
+(string_of_typ thy t));
+
+fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) |
+comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) |
+comp_st_type_of _ _ = error "empty automaton list";
+
+(* checking consistency of action types (for composition) *)
+fun check_ac thy (a::r) =
+let
+fun ch_f_a thy acttyp [] = acttyp |
+ch_f_a thy acttyp (a::r) =
+let
+val auttyp = aut_type_of thy a;
+val ac = (act_type_of thy auttyp);
+in
+if (ac=acttyp) then (ch_f_a thy acttyp r) else (error "A")
+end;
+val auttyp = aut_type_of thy a;
+val acttyp = (act_type_of thy auttyp);
+in
+ch_f_a thy acttyp r
+end |
+check_ac _ [] = error "empty automaton list";
+
+fun clist [] = "" |
+clist [a] = a |
+clist (a::r) = a ^ " || " ^ (clist r);
+
+val add_defs = snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes o map (apfst Binding.name));
+
+
+(* add_ioa *)
+
+fun add_ioa automaton_name action_type inp out int statetupel ini trans thy =
+(writeln("Constructing automaton " ^ automaton_name ^ " ...");
+let
+val state_type_string = type_product_of_varlist(statetupel);
+val styp = Syntax.read_typ_global thy state_type_string;
+val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")";
+val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")";
+val atyp = Syntax.read_typ_global thy action_type;
+val inp_set_string = action_set_string thy atyp inp;
+val out_set_string = action_set_string thy atyp out;
+val int_set_string = action_set_string thy atyp int;
+val inp_head_list = constructor_head_list thy action_type inp;
+val out_head_list = constructor_head_list thy action_type out;
+val int_head_list = constructor_head_list thy action_type int;
+val overlap_flag = ((overlap inp out) andalso (overlap inp int) andalso (overlap out int));
+val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list
+ atyp statetupel trans;
+val thy2 = (thy
+|> Sign.add_consts
+[(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn),
+(Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn),
+(Binding.name (automaton_name ^ "_trans"),
+ "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
+(Binding.name automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
+|> add_defs
+[(automaton_name ^ "_initial_def",
+automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
+(automaton_name ^ "_asig_def",
+automaton_name ^ "_asig == (" ^
+ inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"),
+(automaton_name ^ "_trans_def",
+automaton_name ^ "_trans == {(" ^
+ state_vars_tupel ^ ", act_of_" ^ automaton_name ^ ", " ^ state_vars_primed ^
+"). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"),
+(automaton_name ^ "_def",
+automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
+"_initial, " ^ automaton_name ^ "_trans,{},{})")
+])
+val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[]))
+( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
+in
+(
+if (chk_prime_list = []) then thy2
+else (
+error("Precondition or assignment terms in postconditions contain following primed variables:\n"
+ ^ (list_elements_of chk_prime_list)))
+)
+end)
+
+fun add_composition automaton_name aut_list thy =
+(writeln("Constructing automaton " ^ automaton_name ^ " ...");
+let
+val acttyp = check_ac thy aut_list;
+val st_typ = comp_st_type_of thy aut_list;
+val comp_list = clist aut_list;
+in
+thy
+|> Sign.add_consts_i
+[(Binding.name automaton_name,
+Type("*",
+[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
+ Type("*",[Type("set",[st_typ]),
+ Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
+ Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
+,NoSyn)]
+|> add_defs
+[(automaton_name ^ "_def",
+automaton_name ^ " == " ^ comp_list)]
+end)
+
+fun add_restriction automaton_name aut_source actlist thy =
+(writeln("Constructing automaton " ^ automaton_name ^ " ...");
+let
+val auttyp = aut_type_of thy aut_source;
+val acttyp = act_type_of thy auttyp;
+val rest_set = action_set_string thy acttyp actlist
+in
+thy
+|> Sign.add_consts_i
+[(Binding.name automaton_name, auttyp,NoSyn)]
+|> add_defs
+[(automaton_name ^ "_def",
+automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)]
+end)
+fun add_hiding automaton_name aut_source actlist thy =
+(writeln("Constructing automaton " ^ automaton_name ^ " ...");
+let
+val auttyp = aut_type_of thy aut_source;
+val acttyp = act_type_of thy auttyp;
+val hid_set = action_set_string thy acttyp actlist
+in
+thy
+|> Sign.add_consts_i
+[(Binding.name automaton_name, auttyp,NoSyn)]
+|> add_defs
+[(automaton_name ^ "_def",
+automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)]
+end)
+
+fun ren_act_type_of thy funct =
+ (case Term.fastype_of (Syntax.read_term_global thy funct) of
+ Type ("fun", [a, b]) => a
+ | _ => error "could not extract argument type of renaming function term");
+
+fun add_rename automaton_name aut_source fun_name thy =
+(writeln("Constructing automaton " ^ automaton_name ^ " ...");
+let
+val auttyp = aut_type_of thy aut_source;
+val st_typ = st_type_of thy auttyp;
+val acttyp = ren_act_type_of thy fun_name
+in
+thy
+|> Sign.add_consts_i
+[(Binding.name automaton_name,
+Type("*",
+[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
+ Type("*",[Type("set",[st_typ]),
+ Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
+ Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
+,NoSyn)]
+|> add_defs
+[(automaton_name ^ "_def",
+automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
+end)
+
+
+(** outer syntax **)
+
+(* prepare results *)
+
+(*encoding transition specifications with a element of ParseTrans*)
+datatype ParseTrans = Rel of string | PP of string*(string*string)list;
+fun mk_trans_of_rel s = Rel(s);
+fun mk_trans_of_prepost (s,l) = PP(s,l);
+
+fun trans_of (a, Rel b) = (a, b, [("", "")])
+ | trans_of (a, PP (b, l)) = (a, b, l);
+
+
+fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) =
+ add_ioa aut action_type inp out int states initial (map trans_of trans);
+
+fun mk_composition_decl (aut, autlist) =
+ add_composition aut autlist;
+
+fun mk_hiding_decl (aut, (actlist, source_aut)) =
+ add_hiding aut source_aut actlist;
+
+fun mk_restriction_decl (aut, (source_aut, actlist)) =
+ add_restriction aut source_aut actlist;
+
+fun mk_rename_decl (aut, (source_aut, rename_f)) =
+ add_rename aut source_aut rename_f;
+
+
+(* outer syntax *)
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs",
+ "outputs", "internals", "states", "initially", "transitions", "pre",
+ "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
+ "rename"];
+
+val actionlist = P.list1 P.term;
+val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
+val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
+val internalslist = P.$$$ "internals" |-- P.!!! actionlist;
+val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ));
+val initial = P.$$$ "initially" |-- P.!!! P.term;
+val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term);
+val pre = P.$$$ "pre" |-- P.!!! P.term;
+val post = P.$$$ "post" |-- P.!!! assign_list;
+val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost;
+val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost;
+val transrel = (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel;
+val transition = P.term -- (transrel || pre1 || post1);
+val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition);
+
+val ioa_decl =
+ (P.name -- (P.$$$ "=" |--
+ (P.$$$ "signature" |--
+ P.!!! (P.$$$ "actions" |--
+ (P.typ --
+ (Scan.optional inputslist []) --
+ (Scan.optional outputslist []) --
+ (Scan.optional internalslist []) --
+ stateslist --
+ (Scan.optional initial "True") --
+ translist))))) >> mk_ioa_decl ||
+ (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name))))
+ >> mk_composition_decl ||
+ (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |--
+ P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl ||
+ (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |--
+ P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl ||
+ (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
+ >> mk_rename_decl;
+
+val _ =
+ OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
+ (ioa_decl >> Toplevel.theory);
+
+end;
+
+end;
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Sun Jun 21 15:45:42 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,536 +0,0 @@
-(* Title: HOLCF/IOA/meta_theory/ioa.ML
- Author: Tobias Hamberger, TU Muenchen
-*)
-
-signature IOA =
-sig
- val add_ioa: string -> string
- -> (string) list -> (string) list -> (string) list
- -> (string * string) list -> string
- -> (string * string * (string * string)list) list
- -> theory -> theory
- val add_composition : string -> (string)list -> theory -> theory
- val add_hiding : string -> string -> (string)list -> theory -> theory
- val add_restriction : string -> string -> (string)list -> theory -> theory
- val add_rename : string -> string -> string -> theory -> theory
-end;
-
-structure Ioa: IOA =
-struct
-
-val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
-val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global;
-
-exception malformed;
-
-(* stripping quotes *)
-fun strip [] = [] |
-strip ("\""::r) = strip r |
-strip (a::r) = a :: (strip r);
-fun strip_quote s = implode(strip(explode(s)));
-
-(* used by *_of_varlist *)
-fun extract_first (a,b) = strip_quote a;
-fun extract_second (a,b) = strip_quote b;
-(* following functions producing sth from a varlist *)
-fun comma_list_of_varlist [] = "" |
-comma_list_of_varlist [a] = extract_first a |
-comma_list_of_varlist (a::r) = (extract_first a) ^ "," ^ (comma_list_of_varlist r);
-fun primed_comma_list_of_varlist [] = "" |
-primed_comma_list_of_varlist [a] = (extract_first a) ^ "'" |
-primed_comma_list_of_varlist (a::r) = (extract_first a) ^ "'," ^
- (primed_comma_list_of_varlist r);
-fun type_product_of_varlist [] = "" |
-type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" |
-type_product_of_varlist(a::r) = "(" ^ extract_second(a) ^ ")*" ^ type_product_of_varlist r;
-
-(* listing a list *)
-fun list_elements_of [] = "" |
-list_elements_of (a::r) = a ^ " " ^ (list_elements_of r);
-
-(* extracting type parameters from a type list *)
-(* fun param_tupel thy [] res = res |
-param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res |
-param_tupel thy ((TFree(a,_))::r) res =
-if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) |
-param_tupel thy (a::r) res =
-error ("one component of a statetype is a TVar: " ^ (string_of_typ thy a));
-*)
-
-(* used by constr_list *)
-fun extract_constrs thy [] = [] |
-extract_constrs thy (a::r) =
-let
-fun delete_bold [] = []
-| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
- then (let val (_::_::_::s) = xs in delete_bold s end)
- else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
- then (let val (_::_::_::s) = xs in delete_bold s end)
- else (x::delete_bold xs));
-fun delete_bold_string s = implode(delete_bold(explode s));
-(* from a constructor term in *.induct (with quantifiers,
-"Trueprop" and ?P stripped away) delivers the head *)
-fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r |
-extract_hd (Const("Trueprop",_) $ r) = extract_hd r |
-extract_hd (Var(_,_) $ r) = extract_hd r |
-extract_hd (a $ b) = extract_hd a |
-extract_hd (Const(s,_)) = s |
-extract_hd _ = raise malformed;
-(* delivers constructor term string from a prem of *.induct *)
-fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))|
-extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r |
-extract_constr thy (Var(_,_) $ r) = delete_bold_string(string_of_term thy r) |
-extract_constr _ _ = raise malformed;
-in
-(extract_hd a,extract_constr thy a) :: (extract_constrs thy r)
-end;
-
-(* delivering list of constructor terms of a datatype *)
-fun constr_list thy atyp =
-let
-fun act_name thy (Type(s,_)) = s |
-act_name _ s =
-error("malformed action type: " ^ (string_of_typ thy s));
-fun afpl ("." :: a) = [] |
-afpl [] = [] |
-afpl (a::r) = a :: (afpl r);
-fun unqualify s = implode(rev(afpl(rev(explode s))));
-val q_atypstr = act_name thy atyp;
-val uq_atypstr = unqualify q_atypstr;
-val prem = prems_of (PureThy.get_thm thy (uq_atypstr ^ ".induct"));
-in
-extract_constrs thy prem
-handle malformed =>
-error("malformed theorem : " ^ uq_atypstr ^ ".induct")
-end;
-
-fun check_for_constr thy atyp (a $ b) =
-let
-fun all_free (Free(_,_)) = true |
-all_free (a $ b) = if (all_free a) then (all_free b) else false |
-all_free _ = false;
-in
-if (all_free b) then (check_for_constr thy atyp a) else false
-end |
-check_for_constr thy atyp (Const(a,_)) =
-let
-val cl = constr_list thy atyp;
-fun fstmem a [] = false |
-fstmem a ((f,s)::r) = if (a=f) then true else (fstmem a r)
-in
-if (fstmem a cl) then true else false
-end |
-check_for_constr _ _ _ = false;
-
-(* delivering the free variables of a constructor term *)
-fun free_vars_of (t1 $ t2) = (free_vars_of t1) @ (free_vars_of t2) |
-free_vars_of (Const(_,_)) = [] |
-free_vars_of (Free(a,_)) = [a] |
-free_vars_of _ = raise malformed;
-
-(* making a constructor set from a constructor term (of signature) *)
-fun constr_set_string thy atyp ctstr =
-let
-val trm = OldGoals.simple_read_term thy atyp ctstr;
-val l = free_vars_of trm
-in
-if (check_for_constr thy atyp trm) then
-(if (l=[]) then ("{" ^ ctstr ^ "}")
-else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})")
-else (raise malformed)
-handle malformed =>
-error("malformed action term: " ^ (string_of_term thy trm))
-end;
-
-(* extracting constructor heads *)
-fun constructor_head thy atypstr s =
-let
-fun hd_of (Const(a,_)) = a |
-hd_of (t $ _) = hd_of t |
-hd_of _ = raise malformed;
-val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
-in
-hd_of trm handle malformed =>
-error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
-end;
-fun constructor_head_list _ _ [] = [] |
-constructor_head_list thy atypstr (a::r) =
- (constructor_head thy atypstr a)::(constructor_head_list thy atypstr r);
-
-(* producing an action set *)
-(*FIXME*)
-fun action_set_string thy atyp [] = "Set.empty" |
-action_set_string thy atyp [a] = constr_set_string thy atyp (strip_quote a) |
-action_set_string thy atyp (a::r) = (constr_set_string thy atyp (strip_quote a)) ^
- " Un " ^ (action_set_string thy atyp r);
-
-(* used by extend *)
-fun pstr s [] = "(" ^ s ^ "' = " ^ s ^ ")" |
-pstr s ((a,b)::r) =
-if (s=a) then ("(" ^ s ^ "' = (" ^ b ^ "))") else (pstr s r);
-fun poststring [] l = "" |
-poststring [(a,b)] l = pstr a l |
-poststring ((a,b)::r) l = (pstr a l) ^ " & " ^ (poststring r l);
-
-(* extends a (action string,condition,assignlist) tupel by a
-(action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list
-(where bool indicates whether there is a precondition *)
-fun extend thy atyp statetupel (actstr,r,[]) =
-let
-val trm = OldGoals.simple_read_term thy atyp actstr;
-val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
-val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
-in
-if (check_for_constr thy atyp trm)
-then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag)
-else
-error("transition " ^ actstr ^ " is not a pure constructor term")
-end |
-extend thy atyp statetupel (actstr,r,(a,b)::c) =
-let
-fun pseudo_poststring [] = "" |
-pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
-pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r);
-val trm = OldGoals.simple_read_term thy atyp actstr;
-val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
-val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
-in
-if (check_for_constr thy atyp trm) then
-(if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false)
-(* the case with transrel *)
- else
- (trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)),
- "(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag))
-else
-error("transition " ^ actstr ^ " is not a pure constructor term")
-end;
-(* used by make_alt_string *)
-fun extended_list _ _ _ [] = [] |
-extended_list thy atyp statetupel (a::r) =
- (extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r);
-
-(* used by write_alts *)
-fun write_alt thy (chead,tr) inp out int [] =
-if (chead mem inp) then
-(
-error("Input action " ^ tr ^ " was not specified")
-) else (
-if (chead mem (out@int)) then
-(writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else ();
-(tr ^ " => False",tr ^ " => False")) |
-write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) =
-let
-fun hd_of (Const(a,_)) = a |
-hd_of (t $ _) = hd_of t |
-hd_of _ = raise malformed;
-fun occurs_again c [] = false |
-occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r);
-in
-if (chead=(hd_of a)) then
-(if ((chead mem inp) andalso e) then (
-error("Input action " ^ b ^ " has a precondition")
-) else (if (chead mem (inp@out@int)) then
- (if (occurs_again chead r) then (
-error("Two specifications for action: " ^ b)
- ) else (b ^ " => " ^ c,b ^ " => " ^ d))
- else (
-error("Action " ^ b ^ " is not in automaton signature")
-))) else (write_alt thy (chead,ctrm) inp out int r)
-handle malformed =>
-error ("malformed action term: " ^ (string_of_term thy a))
-end;
-
-(* used by make_alt_string *)
-fun write_alts thy (a,b) inp out int [] ttr = (a,b) |
-write_alts thy (a,b) inp out int [c] ttr =
-let
-val wa = write_alt thy c inp out int ttr
-in
- (a ^ (fst wa),b ^ (snd wa))
-end |
-write_alts thy (a,b) inp out int (c::r) ttr =
-let
-val wa = write_alt thy c inp out int ttr
-in
- write_alts thy (a ^ (fst wa) ^ " | ", b ^ (snd wa) ^ " | ") inp out int r ttr
-end;
-
-fun make_alt_string thy inp out int atyp statetupel trans =
-let
-val cl = constr_list thy atyp;
-val ttr = extended_list thy atyp statetupel trans;
-in
-write_alts thy ("","") inp out int cl ttr
-end;
-
-(* used in add_ioa *)
-fun check_free_primed (Free(a,_)) =
-let
-val (f::r) = rev(explode a)
-in
-if (f="'") then [a] else []
-end |
-check_free_primed (a $ b) = ((check_free_primed a) @ (check_free_primed b)) |
-check_free_primed (Abs(_,_,t)) = check_free_primed t |
-check_free_primed _ = [];
-
-fun overlap [] _ = true |
-overlap (a::r) l = if (a mem l) then (
-error("Two occurences of action " ^ a ^ " in automaton signature")
-) else (overlap r l);
-
-(* delivering some types of an automaton *)
-fun aut_type_of thy aut_name =
-let
-fun left_of (( _ $ left) $ _) = left |
-left_of _ = raise malformed;
-val aut_def = concl_of (PureThy.get_thm thy (aut_name ^ "_def"));
-in
-(#T(rep_cterm(cterm_of thy (left_of aut_def))))
-handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
-end;
-
-fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp |
-act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^
-(string_of_typ thy t));
-fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp |
-st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^
-(string_of_typ thy t));
-
-fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) |
-comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) |
-comp_st_type_of _ _ = error "empty automaton list";
-
-(* checking consistency of action types (for composition) *)
-fun check_ac thy (a::r) =
-let
-fun ch_f_a thy acttyp [] = acttyp |
-ch_f_a thy acttyp (a::r) =
-let
-val auttyp = aut_type_of thy a;
-val ac = (act_type_of thy auttyp);
-in
-if (ac=acttyp) then (ch_f_a thy acttyp r) else (error "A")
-end;
-val auttyp = aut_type_of thy a;
-val acttyp = (act_type_of thy auttyp);
-in
-ch_f_a thy acttyp r
-end |
-check_ac _ [] = error "empty automaton list";
-
-fun clist [] = "" |
-clist [a] = a |
-clist (a::r) = a ^ " || " ^ (clist r);
-
-val add_defs = snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes o map (apfst Binding.name));
-
-
-(* add_ioa *)
-
-fun add_ioa automaton_name action_type inp out int statetupel ini trans thy =
-(writeln("Constructing automaton " ^ automaton_name ^ " ...");
-let
-val state_type_string = type_product_of_varlist(statetupel);
-val styp = Syntax.read_typ_global thy state_type_string;
-val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")";
-val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")";
-val atyp = Syntax.read_typ_global thy action_type;
-val inp_set_string = action_set_string thy atyp inp;
-val out_set_string = action_set_string thy atyp out;
-val int_set_string = action_set_string thy atyp int;
-val inp_head_list = constructor_head_list thy action_type inp;
-val out_head_list = constructor_head_list thy action_type out;
-val int_head_list = constructor_head_list thy action_type int;
-val overlap_flag = ((overlap inp out) andalso (overlap inp int) andalso (overlap out int));
-val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list
- atyp statetupel trans;
-val thy2 = (thy
-|> Sign.add_consts
-[(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn),
-(Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn),
-(Binding.name (automaton_name ^ "_trans"),
- "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
-(Binding.name automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
-|> add_defs
-[(automaton_name ^ "_initial_def",
-automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
-(automaton_name ^ "_asig_def",
-automaton_name ^ "_asig == (" ^
- inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"),
-(automaton_name ^ "_trans_def",
-automaton_name ^ "_trans == {(" ^
- state_vars_tupel ^ ", act_of_" ^ automaton_name ^ ", " ^ state_vars_primed ^
-"). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"),
-(automaton_name ^ "_def",
-automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
-"_initial, " ^ automaton_name ^ "_trans,{},{})")
-])
-val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[]))
-( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
-in
-(
-if (chk_prime_list = []) then thy2
-else (
-error("Precondition or assignment terms in postconditions contain following primed variables:\n"
- ^ (list_elements_of chk_prime_list)))
-)
-end)
-
-fun add_composition automaton_name aut_list thy =
-(writeln("Constructing automaton " ^ automaton_name ^ " ...");
-let
-val acttyp = check_ac thy aut_list;
-val st_typ = comp_st_type_of thy aut_list;
-val comp_list = clist aut_list;
-in
-thy
-|> Sign.add_consts_i
-[(Binding.name automaton_name,
-Type("*",
-[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
- Type("*",[Type("set",[st_typ]),
- Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
- Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
-,NoSyn)]
-|> add_defs
-[(automaton_name ^ "_def",
-automaton_name ^ " == " ^ comp_list)]
-end)
-
-fun add_restriction automaton_name aut_source actlist thy =
-(writeln("Constructing automaton " ^ automaton_name ^ " ...");
-let
-val auttyp = aut_type_of thy aut_source;
-val acttyp = act_type_of thy auttyp;
-val rest_set = action_set_string thy acttyp actlist
-in
-thy
-|> Sign.add_consts_i
-[(Binding.name automaton_name, auttyp,NoSyn)]
-|> add_defs
-[(automaton_name ^ "_def",
-automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)]
-end)
-fun add_hiding automaton_name aut_source actlist thy =
-(writeln("Constructing automaton " ^ automaton_name ^ " ...");
-let
-val auttyp = aut_type_of thy aut_source;
-val acttyp = act_type_of thy auttyp;
-val hid_set = action_set_string thy acttyp actlist
-in
-thy
-|> Sign.add_consts_i
-[(Binding.name automaton_name, auttyp,NoSyn)]
-|> add_defs
-[(automaton_name ^ "_def",
-automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)]
-end)
-
-fun ren_act_type_of thy funct =
- (case Term.fastype_of (Syntax.read_term_global thy funct) of
- Type ("fun", [a, b]) => a
- | _ => error "could not extract argument type of renaming function term");
-
-fun add_rename automaton_name aut_source fun_name thy =
-(writeln("Constructing automaton " ^ automaton_name ^ " ...");
-let
-val auttyp = aut_type_of thy aut_source;
-val st_typ = st_type_of thy auttyp;
-val acttyp = ren_act_type_of thy fun_name
-in
-thy
-|> Sign.add_consts_i
-[(Binding.name automaton_name,
-Type("*",
-[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
- Type("*",[Type("set",[st_typ]),
- Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
- Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
-,NoSyn)]
-|> add_defs
-[(automaton_name ^ "_def",
-automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
-end)
-
-
-(** outer syntax **)
-
-(* prepare results *)
-
-(*encoding transition specifications with a element of ParseTrans*)
-datatype ParseTrans = Rel of string | PP of string*(string*string)list;
-fun mk_trans_of_rel s = Rel(s);
-fun mk_trans_of_prepost (s,l) = PP(s,l);
-
-fun trans_of (a, Rel b) = (a, b, [("", "")])
- | trans_of (a, PP (b, l)) = (a, b, l);
-
-
-fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) =
- add_ioa aut action_type inp out int states initial (map trans_of trans);
-
-fun mk_composition_decl (aut, autlist) =
- add_composition aut autlist;
-
-fun mk_hiding_decl (aut, (actlist, source_aut)) =
- add_hiding aut source_aut actlist;
-
-fun mk_restriction_decl (aut, (source_aut, actlist)) =
- add_restriction aut source_aut actlist;
-
-fun mk_rename_decl (aut, (source_aut, rename_f)) =
- add_rename aut source_aut rename_f;
-
-
-(* outer syntax *)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs",
- "outputs", "internals", "states", "initially", "transitions", "pre",
- "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
- "rename"];
-
-val actionlist = P.list1 P.term;
-val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
-val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
-val internalslist = P.$$$ "internals" |-- P.!!! actionlist;
-val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ));
-val initial = P.$$$ "initially" |-- P.!!! P.term;
-val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term);
-val pre = P.$$$ "pre" |-- P.!!! P.term;
-val post = P.$$$ "post" |-- P.!!! assign_list;
-val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost;
-val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost;
-val transrel = (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel;
-val transition = P.term -- (transrel || pre1 || post1);
-val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition);
-
-val ioa_decl =
- (P.name -- (P.$$$ "=" |--
- (P.$$$ "signature" |--
- P.!!! (P.$$$ "actions" |--
- (P.typ --
- (Scan.optional inputslist []) --
- (Scan.optional outputslist []) --
- (Scan.optional internalslist []) --
- stateslist --
- (Scan.optional initial "True") --
- translist))))) >> mk_ioa_decl ||
- (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name))))
- >> mk_composition_decl ||
- (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |--
- P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl ||
- (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |--
- P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl ||
- (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
- >> mk_rename_decl;
-
-val _ =
- OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
- (ioa_decl >> Toplevel.theory);
-
-end;
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/fixrec.ML Sun Jun 21 15:45:57 2009 +0200
@@ -0,0 +1,435 @@
+(* Title: HOLCF/Tools/fixrec.ML
+ Author: Amber Telfer and Brian Huffman
+
+Recursive function definition package for HOLCF.
+*)
+
+signature FIXREC =
+sig
+ val add_fixrec: bool -> (binding * typ option * mixfix) list
+ -> (Attrib.binding * term) list -> local_theory -> local_theory
+ val add_fixrec_cmd: bool -> (binding * string option * mixfix) list
+ -> (Attrib.binding * string) list -> local_theory -> local_theory
+ val add_fixpat: Thm.binding * term list -> theory -> theory
+ val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory
+ val add_matchers: (string * string) list -> theory -> theory
+ val setup: theory -> theory
+end;
+
+structure Fixrec :> FIXREC =
+struct
+
+val def_cont_fix_eq = @{thm def_cont_fix_eq};
+val def_cont_fix_ind = @{thm def_cont_fix_ind};
+
+
+fun fixrec_err s = error ("fixrec definition error:\n" ^ s);
+fun fixrec_eq_err thy s eq =
+ fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
+
+(*************************************************************************)
+(***************************** building types ****************************)
+(*************************************************************************)
+
+(* ->> is taken from holcf_logic.ML *)
+fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
+
+infixr 6 ->>; val (op ->>) = cfunT;
+
+fun cfunsT (Ts, U) = foldr cfunT U Ts;
+
+fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
+ | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
+
+fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
+ | binder_cfun _ = [];
+
+fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
+ | body_cfun T = T;
+
+fun strip_cfun T : typ list * typ =
+ (binder_cfun T, body_cfun T);
+
+fun maybeT T = Type(@{type_name "maybe"}, [T]);
+
+fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T
+ | dest_maybeT T = raise TYPE ("dest_maybeT", [T], []);
+
+fun tupleT [] = HOLogic.unitT
+ | tupleT [T] = T
+ | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
+
+fun matchT (T, U) =
+ body_cfun T ->> cfunsT (binder_cfun T, U) ->> U;
+
+
+(*************************************************************************)
+(***************************** building terms ****************************)
+(*************************************************************************)
+
+val mk_trp = HOLogic.mk_Trueprop;
+
+(* splits a cterm into the right and lefthand sides of equality *)
+fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
+
+(* similar to Thm.head_of, but for continuous application *)
+fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f
+ | chead_of u = u;
+
+fun capply_const (S, T) =
+ Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T));
+
+fun cabs_const (S, T) =
+ Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T));
+
+fun mk_cabs t =
+ let val T = Term.fastype_of t
+ in cabs_const (Term.domain_type T, Term.range_type T) $ t end
+
+fun mk_capply (t, u) =
+ let val (S, T) =
+ case Term.fastype_of t of
+ Type(@{type_name "->"}, [S, T]) => (S, T)
+ | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
+ in capply_const (S, T) $ t $ u end;
+
+infix 0 ==; val (op ==) = Logic.mk_equals;
+infix 1 ===; val (op ===) = HOLogic.mk_eq;
+infix 9 ` ; val (op `) = mk_capply;
+
+(* builds the expression (LAM v. rhs) *)
+fun big_lambda v rhs =
+ cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs;
+
+(* builds the expression (LAM v1 v2 .. vn. rhs) *)
+fun big_lambdas [] rhs = rhs
+ | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs);
+
+fun mk_return t =
+ let val T = Term.fastype_of t
+ in Const(@{const_name Fixrec.return}, T ->> maybeT T) ` t end;
+
+fun mk_bind (t, u) =
+ let val (T, mU) = dest_cfunT (Term.fastype_of u);
+ val bindT = maybeT T ->> (T ->> mU) ->> mU;
+ in Const(@{const_name Fixrec.bind}, bindT) ` t ` u end;
+
+fun mk_mplus (t, u) =
+ let val mT = Term.fastype_of t
+ in Const(@{const_name Fixrec.mplus}, mT ->> mT ->> mT) ` t ` u end;
+
+fun mk_run t =
+ let val mT = Term.fastype_of t
+ val T = dest_maybeT mT
+ in Const(@{const_name Fixrec.run}, mT ->> T) ` t end;
+
+fun mk_fix t =
+ let val (T, _) = dest_cfunT (Term.fastype_of t)
+ in Const(@{const_name fix}, (T ->> T) ->> T) ` t end;
+
+fun mk_cont t =
+ let val T = Term.fastype_of t
+ in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end;
+
+val mk_fst = HOLogic.mk_fst
+val mk_snd = HOLogic.mk_snd
+
+(* builds the expression (v1,v2,..,vn) *)
+fun mk_tuple [] = HOLogic.unit
+| mk_tuple (t::[]) = t
+| mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts);
+
+(* builds the expression (%(v1,v2,..,vn). rhs) *)
+fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs
+ | lambda_tuple (v::[]) rhs = Term.lambda v rhs
+ | lambda_tuple (v::vs) rhs =
+ HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs));
+
+
+(*************************************************************************)
+(************* fixed-point definitions and unfolding theorems ************)
+(*************************************************************************)
+
+fun add_fixdefs
+ (fixes : ((binding * typ) * mixfix) list)
+ (spec : (Attrib.binding * term) list)
+ (lthy : local_theory) =
+ let
+ val thy = ProofContext.theory_of lthy;
+ val names = map (Binding.name_of o fst o fst) fixes;
+ val all_names = space_implode "_" names;
+ val (lhss,rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
+ val functional = lambda_tuple lhss (mk_tuple rhss);
+ val fixpoint = mk_fix (mk_cabs functional);
+
+ val cont_thm =
+ Goal.prove lthy [] [] (mk_trp (mk_cont functional))
+ (K (simp_tac (local_simpset_of lthy) 1));
+
+ fun one_def (l as Free(n,_)) r =
+ let val b = Long_Name.base_name n
+ in ((Binding.name (b^"_def"), []), r) end
+ | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form";
+ fun defs [] _ = []
+ | defs (l::[]) r = [one_def l r]
+ | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r);
+ val fixdefs = defs lhss fixpoint;
+ val define_all = fold_map (LocalTheory.define Thm.definitionK);
+ val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy
+ |> define_all (map (apfst fst) fixes ~~ fixdefs);
+ fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
+ val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms);
+ val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT);
+ val predicate = lambda_tuple lhss (list_comb (P, lhss));
+ val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm])
+ |> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)]
+ |> LocalDefs.unfold lthy @{thms split_paired_all split_conv split_strict};
+ val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
+ |> LocalDefs.unfold lthy' @{thms split_conv};
+ fun unfolds [] thm = []
+ | unfolds (n::[]) thm = [(n^"_unfold", thm)]
+ | unfolds (n::ns) thm = let
+ val thmL = thm RS @{thm Pair_eqD1};
+ val thmR = thm RS @{thm Pair_eqD2};
+ in (n^"_unfold", thmL) :: unfolds ns thmR end;
+ val unfold_thms = unfolds names tuple_unfold_thm;
+ fun mk_note (n, thm) = ((Binding.name n, []), [thm]);
+ val (thmss, lthy'') = lthy'
+ |> fold_map (LocalTheory.note Thm.generatedK o mk_note)
+ ((all_names ^ "_induct", tuple_induct_thm) :: unfold_thms);
+ in
+ (lthy'', names, fixdef_thms, map snd unfold_thms)
+ end;
+
+(*************************************************************************)
+(*********** monadic notation and pattern matching compilation ***********)
+(*************************************************************************)
+
+structure FixrecMatchData = TheoryDataFun (
+ type T = string Symtab.table;
+ val empty = Symtab.empty;
+ val copy = I;
+ val extend = I;
+ fun merge _ tabs : T = Symtab.merge (K true) tabs;
+);
+
+(* associate match functions with pattern constants *)
+fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms);
+
+fun taken_names (t : term) : bstring list =
+ let
+ fun taken (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
+ | taken (Free(a,_) , bs) = insert (op =) a bs
+ | taken (f $ u , bs) = taken (f, taken (u, bs))
+ | taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs)
+ | taken (_ , bs) = bs;
+ in
+ taken (t, [])
+ end;
+
+(* builds a monadic term for matching a constructor pattern *)
+fun pre_build match_name pat rhs vs taken =
+ case pat of
+ Const(@{const_name Rep_CFun},_)$f$(v as Free(n,T)) =>
+ pre_build match_name f rhs (v::vs) taken
+ | Const(@{const_name Rep_CFun},_)$f$x =>
+ let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
+ in pre_build match_name f rhs' (v::vs) taken' end
+ | Const(c,T) =>
+ let
+ val n = Name.variant taken "v";
+ fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
+ | result_type T _ = T;
+ val v = Free(n, result_type T vs);
+ val m = Const(match_name c, matchT (T, fastype_of rhs));
+ val k = big_lambdas vs rhs;
+ in
+ (m`v`k, v, n::taken)
+ end
+ | Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n)
+ | _ => fixrec_err "pre_build: invalid pattern";
+
+(* builds a monadic term for matching a function definition pattern *)
+(* returns (name, arity, matcher) *)
+fun building match_name pat rhs vs taken =
+ case pat of
+ Const(@{const_name Rep_CFun}, _)$f$(v as Free(n,T)) =>
+ building match_name f rhs (v::vs) taken
+ | Const(@{const_name Rep_CFun}, _)$f$x =>
+ let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
+ in building match_name f rhs' (v::vs) taken' end
+ | Free(_,_) => ((pat, length vs), big_lambdas vs rhs)
+ | Const(_,_) => ((pat, length vs), big_lambdas vs rhs)
+ | _ => fixrec_err ("function is not declared as constant in theory: "
+ ^ ML_Syntax.print_term pat);
+
+fun strip_alls t =
+ if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t;
+
+fun match_eq match_name eq =
+ let
+ val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq));
+ in
+ building match_name lhs (mk_return rhs) [] (taken_names eq)
+ end;
+
+(* returns the sum (using +++) of the terms in ms *)
+(* also applies "run" to the result! *)
+fun fatbar arity ms =
+ let
+ fun LAM_Ts 0 t = ([], Term.fastype_of t)
+ | LAM_Ts n (_ $ Abs(_,T,t)) =
+ let val (Ts, U) = LAM_Ts (n-1) t in (T::Ts, U) end
+ | LAM_Ts _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
+ fun unLAM 0 t = t
+ | unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t
+ | unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
+ fun reLAM ([], U) t = t
+ | reLAM (T::Ts, U) t = reLAM (Ts, T ->> U) (cabs_const(T,U)$Abs("",T,t));
+ val msum = foldr1 mk_mplus (map (unLAM arity) ms);
+ val (Ts, U) = LAM_Ts arity (hd ms)
+ in
+ reLAM (rev Ts, dest_maybeT U) (mk_run msum)
+ end;
+
+(* this is the pattern-matching compiler function *)
+fun compile_pats match_name eqs =
+ let
+ val (((n::names),(a::arities)),mats) =
+ apfst ListPair.unzip (ListPair.unzip (map (match_eq match_name) eqs));
+ val cname = if forall (fn x => n=x) names then n
+ else fixrec_err "all equations in block must define the same function";
+ val arity = if forall (fn x => a=x) arities then a
+ else fixrec_err "all equations in block must have the same arity";
+ val rhs = fatbar arity mats;
+ in
+ mk_trp (cname === rhs)
+ end;
+
+(*************************************************************************)
+(********************** Proving associated theorems **********************)
+(*************************************************************************)
+
+(* proves a block of pattern matching equations as theorems, using unfold *)
+fun make_simps lthy (unfold_thm, eqns : (Attrib.binding * term) list) =
+ let
+ val tacs =
+ [rtac (unfold_thm RS @{thm ssubst_lhs}) 1,
+ asm_simp_tac (local_simpset_of lthy) 1];
+ fun prove_term t = Goal.prove lthy [] [] t (K (EVERY tacs));
+ fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t);
+ in
+ map prove_eqn eqns
+ end;
+
+(*************************************************************************)
+(************************* Main fixrec function **************************)
+(*************************************************************************)
+
+local
+(* code adapted from HOL/Tools/primrec.ML *)
+
+fun gen_fixrec
+ (set_group : bool)
+ prep_spec
+ (strict : bool)
+ raw_fixes
+ raw_spec
+ (lthy : local_theory) =
+ let
+ val (fixes : ((binding * typ) * mixfix) list,
+ spec : (Attrib.binding * term) list) =
+ fst (prep_spec raw_fixes raw_spec lthy);
+ val chead_of_spec =
+ chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd;
+ fun name_of (Free (n, _)) = n
+ | name_of t = fixrec_err ("unknown term");
+ val all_names = map (name_of o chead_of_spec) spec;
+ val names = distinct (op =) all_names;
+ fun block_of_name n =
+ map_filter
+ (fn (m,eq) => if m = n then SOME eq else NONE)
+ (all_names ~~ spec);
+ val blocks = map block_of_name names;
+
+ val matcher_tab = FixrecMatchData.get (ProofContext.theory_of lthy);
+ fun match_name c =
+ case Symtab.lookup matcher_tab c of SOME m => m
+ | NONE => fixrec_err ("unknown pattern constructor: " ^ c);
+
+ val matches = map (compile_pats match_name) (map (map snd) blocks);
+ val spec' = map (pair Attrib.empty_binding) matches;
+ val (lthy', cnames, fixdef_thms, unfold_thms) =
+ add_fixdefs fixes spec' lthy;
+ in
+ if strict then let (* only prove simp rules if strict = true *)
+ val simps : (Attrib.binding * thm) list list =
+ map (make_simps lthy') (unfold_thms ~~ blocks);
+ fun mk_bind n : Attrib.binding =
+ (Binding.name (n ^ "_simps"),
+ [Attrib.internal (K Simplifier.simp_add)]);
+ val simps1 : (Attrib.binding * thm list) list =
+ map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps);
+ val simps2 : (Attrib.binding * thm list) list =
+ map (apsnd (fn thm => [thm])) (List.concat simps);
+ val (_, lthy'') = lthy'
+ |> fold_map (LocalTheory.note Thm.generatedK) (simps1 @ simps2);
+ in
+ lthy''
+ end
+ else lthy'
+ end;
+
+in
+
+val add_fixrec = gen_fixrec false Specification.check_spec;
+val add_fixrec_cmd = gen_fixrec true Specification.read_spec;
+
+end; (* local *)
+
+(*************************************************************************)
+(******************************** Fixpat *********************************)
+(*************************************************************************)
+
+fun fix_pat thy t =
+ let
+ val T = fastype_of t;
+ val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
+ val cname = case chead_of t of Const(c,_) => c | _ =>
+ fixrec_err "function is not declared as constant in theory";
+ val unfold_thm = PureThy.get_thm thy (cname^"_unfold");
+ val simp = Goal.prove_global thy [] [] eq
+ (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
+ in simp end;
+
+fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
+ let
+ val atts = map (prep_attrib thy) srcs;
+ val ts = map (prep_term thy) strings;
+ val simps = map (fix_pat thy) ts;
+ in
+ (snd o PureThy.add_thmss [((name, simps), atts)]) thy
+ end;
+
+val add_fixpat = gen_add_fixpat Sign.cert_term (K I);
+val add_fixpat_cmd = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
+
+
+(*************************************************************************)
+(******************************** Parsers ********************************)
+(*************************************************************************)
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl
+ ((P.opt_keyword "permissive" >> not) -- P.fixes -- SpecParse.where_alt_specs
+ >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
+
+val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
+ (SpecParse.specs >> (Toplevel.theory o add_fixpat_cmd));
+
+end;
+
+val setup = FixrecMatchData.init;
+
+end;
--- a/src/HOLCF/Tools/fixrec_package.ML Sun Jun 21 15:45:42 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,435 +0,0 @@
-(* Title: HOLCF/Tools/fixrec.ML
- Author: Amber Telfer and Brian Huffman
-
-Recursive function definition package for HOLCF.
-*)
-
-signature FIXREC =
-sig
- val add_fixrec: bool -> (binding * typ option * mixfix) list
- -> (Attrib.binding * term) list -> local_theory -> local_theory
- val add_fixrec_cmd: bool -> (binding * string option * mixfix) list
- -> (Attrib.binding * string) list -> local_theory -> local_theory
- val add_fixpat: Thm.binding * term list -> theory -> theory
- val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory
- val add_matchers: (string * string) list -> theory -> theory
- val setup: theory -> theory
-end;
-
-structure Fixrec :> FIXREC =
-struct
-
-val def_cont_fix_eq = @{thm def_cont_fix_eq};
-val def_cont_fix_ind = @{thm def_cont_fix_ind};
-
-
-fun fixrec_err s = error ("fixrec definition error:\n" ^ s);
-fun fixrec_eq_err thy s eq =
- fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
-
-(*************************************************************************)
-(***************************** building types ****************************)
-(*************************************************************************)
-
-(* ->> is taken from holcf_logic.ML *)
-fun cfunT (T, U) = Type(@{type_name "->"}, [T, U]);
-
-infixr 6 ->>; val (op ->>) = cfunT;
-
-fun cfunsT (Ts, U) = foldr cfunT U Ts;
-
-fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U)
- | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
-
-fun binder_cfun (Type(@{type_name "->"},[T, U])) = T :: binder_cfun U
- | binder_cfun _ = [];
-
-fun body_cfun (Type(@{type_name "->"},[T, U])) = body_cfun U
- | body_cfun T = T;
-
-fun strip_cfun T : typ list * typ =
- (binder_cfun T, body_cfun T);
-
-fun maybeT T = Type(@{type_name "maybe"}, [T]);
-
-fun dest_maybeT (Type(@{type_name "maybe"}, [T])) = T
- | dest_maybeT T = raise TYPE ("dest_maybeT", [T], []);
-
-fun tupleT [] = HOLogic.unitT
- | tupleT [T] = T
- | tupleT (T :: Ts) = HOLogic.mk_prodT (T, tupleT Ts);
-
-fun matchT (T, U) =
- body_cfun T ->> cfunsT (binder_cfun T, U) ->> U;
-
-
-(*************************************************************************)
-(***************************** building terms ****************************)
-(*************************************************************************)
-
-val mk_trp = HOLogic.mk_Trueprop;
-
-(* splits a cterm into the right and lefthand sides of equality *)
-fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
-
-(* similar to Thm.head_of, but for continuous application *)
-fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f
- | chead_of u = u;
-
-fun capply_const (S, T) =
- Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T));
-
-fun cabs_const (S, T) =
- Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T));
-
-fun mk_cabs t =
- let val T = Term.fastype_of t
- in cabs_const (Term.domain_type T, Term.range_type T) $ t end
-
-fun mk_capply (t, u) =
- let val (S, T) =
- case Term.fastype_of t of
- Type(@{type_name "->"}, [S, T]) => (S, T)
- | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
- in capply_const (S, T) $ t $ u end;
-
-infix 0 ==; val (op ==) = Logic.mk_equals;
-infix 1 ===; val (op ===) = HOLogic.mk_eq;
-infix 9 ` ; val (op `) = mk_capply;
-
-(* builds the expression (LAM v. rhs) *)
-fun big_lambda v rhs =
- cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs;
-
-(* builds the expression (LAM v1 v2 .. vn. rhs) *)
-fun big_lambdas [] rhs = rhs
- | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs);
-
-fun mk_return t =
- let val T = Term.fastype_of t
- in Const(@{const_name Fixrec.return}, T ->> maybeT T) ` t end;
-
-fun mk_bind (t, u) =
- let val (T, mU) = dest_cfunT (Term.fastype_of u);
- val bindT = maybeT T ->> (T ->> mU) ->> mU;
- in Const(@{const_name Fixrec.bind}, bindT) ` t ` u end;
-
-fun mk_mplus (t, u) =
- let val mT = Term.fastype_of t
- in Const(@{const_name Fixrec.mplus}, mT ->> mT ->> mT) ` t ` u end;
-
-fun mk_run t =
- let val mT = Term.fastype_of t
- val T = dest_maybeT mT
- in Const(@{const_name Fixrec.run}, mT ->> T) ` t end;
-
-fun mk_fix t =
- let val (T, _) = dest_cfunT (Term.fastype_of t)
- in Const(@{const_name fix}, (T ->> T) ->> T) ` t end;
-
-fun mk_cont t =
- let val T = Term.fastype_of t
- in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end;
-
-val mk_fst = HOLogic.mk_fst
-val mk_snd = HOLogic.mk_snd
-
-(* builds the expression (v1,v2,..,vn) *)
-fun mk_tuple [] = HOLogic.unit
-| mk_tuple (t::[]) = t
-| mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts);
-
-(* builds the expression (%(v1,v2,..,vn). rhs) *)
-fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs
- | lambda_tuple (v::[]) rhs = Term.lambda v rhs
- | lambda_tuple (v::vs) rhs =
- HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs));
-
-
-(*************************************************************************)
-(************* fixed-point definitions and unfolding theorems ************)
-(*************************************************************************)
-
-fun add_fixdefs
- (fixes : ((binding * typ) * mixfix) list)
- (spec : (Attrib.binding * term) list)
- (lthy : local_theory) =
- let
- val thy = ProofContext.theory_of lthy;
- val names = map (Binding.name_of o fst o fst) fixes;
- val all_names = space_implode "_" names;
- val (lhss,rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
- val functional = lambda_tuple lhss (mk_tuple rhss);
- val fixpoint = mk_fix (mk_cabs functional);
-
- val cont_thm =
- Goal.prove lthy [] [] (mk_trp (mk_cont functional))
- (K (simp_tac (local_simpset_of lthy) 1));
-
- fun one_def (l as Free(n,_)) r =
- let val b = Long_Name.base_name n
- in ((Binding.name (b^"_def"), []), r) end
- | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form";
- fun defs [] _ = []
- | defs (l::[]) r = [one_def l r]
- | defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r);
- val fixdefs = defs lhss fixpoint;
- val define_all = fold_map (LocalTheory.define Thm.definitionK);
- val (fixdef_thms : (term * (string * thm)) list, lthy') = lthy
- |> define_all (map (apfst fst) fixes ~~ fixdefs);
- fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2];
- val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms);
- val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT);
- val predicate = lambda_tuple lhss (list_comb (P, lhss));
- val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm])
- |> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)]
- |> LocalDefs.unfold lthy @{thms split_paired_all split_conv split_strict};
- val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
- |> LocalDefs.unfold lthy' @{thms split_conv};
- fun unfolds [] thm = []
- | unfolds (n::[]) thm = [(n^"_unfold", thm)]
- | unfolds (n::ns) thm = let
- val thmL = thm RS @{thm Pair_eqD1};
- val thmR = thm RS @{thm Pair_eqD2};
- in (n^"_unfold", thmL) :: unfolds ns thmR end;
- val unfold_thms = unfolds names tuple_unfold_thm;
- fun mk_note (n, thm) = ((Binding.name n, []), [thm]);
- val (thmss, lthy'') = lthy'
- |> fold_map (LocalTheory.note Thm.generatedK o mk_note)
- ((all_names ^ "_induct", tuple_induct_thm) :: unfold_thms);
- in
- (lthy'', names, fixdef_thms, map snd unfold_thms)
- end;
-
-(*************************************************************************)
-(*********** monadic notation and pattern matching compilation ***********)
-(*************************************************************************)
-
-structure FixrecMatchData = TheoryDataFun (
- type T = string Symtab.table;
- val empty = Symtab.empty;
- val copy = I;
- val extend = I;
- fun merge _ tabs : T = Symtab.merge (K true) tabs;
-);
-
-(* associate match functions with pattern constants *)
-fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms);
-
-fun taken_names (t : term) : bstring list =
- let
- fun taken (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
- | taken (Free(a,_) , bs) = insert (op =) a bs
- | taken (f $ u , bs) = taken (f, taken (u, bs))
- | taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs)
- | taken (_ , bs) = bs;
- in
- taken (t, [])
- end;
-
-(* builds a monadic term for matching a constructor pattern *)
-fun pre_build match_name pat rhs vs taken =
- case pat of
- Const(@{const_name Rep_CFun},_)$f$(v as Free(n,T)) =>
- pre_build match_name f rhs (v::vs) taken
- | Const(@{const_name Rep_CFun},_)$f$x =>
- let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
- in pre_build match_name f rhs' (v::vs) taken' end
- | Const(c,T) =>
- let
- val n = Name.variant taken "v";
- fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs
- | result_type T _ = T;
- val v = Free(n, result_type T vs);
- val m = Const(match_name c, matchT (T, fastype_of rhs));
- val k = big_lambdas vs rhs;
- in
- (m`v`k, v, n::taken)
- end
- | Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n)
- | _ => fixrec_err "pre_build: invalid pattern";
-
-(* builds a monadic term for matching a function definition pattern *)
-(* returns (name, arity, matcher) *)
-fun building match_name pat rhs vs taken =
- case pat of
- Const(@{const_name Rep_CFun}, _)$f$(v as Free(n,T)) =>
- building match_name f rhs (v::vs) taken
- | Const(@{const_name Rep_CFun}, _)$f$x =>
- let val (rhs', v, taken') = pre_build match_name x rhs [] taken;
- in building match_name f rhs' (v::vs) taken' end
- | Free(_,_) => ((pat, length vs), big_lambdas vs rhs)
- | Const(_,_) => ((pat, length vs), big_lambdas vs rhs)
- | _ => fixrec_err ("function is not declared as constant in theory: "
- ^ ML_Syntax.print_term pat);
-
-fun strip_alls t =
- if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t;
-
-fun match_eq match_name eq =
- let
- val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq));
- in
- building match_name lhs (mk_return rhs) [] (taken_names eq)
- end;
-
-(* returns the sum (using +++) of the terms in ms *)
-(* also applies "run" to the result! *)
-fun fatbar arity ms =
- let
- fun LAM_Ts 0 t = ([], Term.fastype_of t)
- | LAM_Ts n (_ $ Abs(_,T,t)) =
- let val (Ts, U) = LAM_Ts (n-1) t in (T::Ts, U) end
- | LAM_Ts _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
- fun unLAM 0 t = t
- | unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t
- | unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs";
- fun reLAM ([], U) t = t
- | reLAM (T::Ts, U) t = reLAM (Ts, T ->> U) (cabs_const(T,U)$Abs("",T,t));
- val msum = foldr1 mk_mplus (map (unLAM arity) ms);
- val (Ts, U) = LAM_Ts arity (hd ms)
- in
- reLAM (rev Ts, dest_maybeT U) (mk_run msum)
- end;
-
-(* this is the pattern-matching compiler function *)
-fun compile_pats match_name eqs =
- let
- val (((n::names),(a::arities)),mats) =
- apfst ListPair.unzip (ListPair.unzip (map (match_eq match_name) eqs));
- val cname = if forall (fn x => n=x) names then n
- else fixrec_err "all equations in block must define the same function";
- val arity = if forall (fn x => a=x) arities then a
- else fixrec_err "all equations in block must have the same arity";
- val rhs = fatbar arity mats;
- in
- mk_trp (cname === rhs)
- end;
-
-(*************************************************************************)
-(********************** Proving associated theorems **********************)
-(*************************************************************************)
-
-(* proves a block of pattern matching equations as theorems, using unfold *)
-fun make_simps lthy (unfold_thm, eqns : (Attrib.binding * term) list) =
- let
- val tacs =
- [rtac (unfold_thm RS @{thm ssubst_lhs}) 1,
- asm_simp_tac (local_simpset_of lthy) 1];
- fun prove_term t = Goal.prove lthy [] [] t (K (EVERY tacs));
- fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t);
- in
- map prove_eqn eqns
- end;
-
-(*************************************************************************)
-(************************* Main fixrec function **************************)
-(*************************************************************************)
-
-local
-(* code adapted from HOL/Tools/primrec.ML *)
-
-fun gen_fixrec
- (set_group : bool)
- prep_spec
- (strict : bool)
- raw_fixes
- raw_spec
- (lthy : local_theory) =
- let
- val (fixes : ((binding * typ) * mixfix) list,
- spec : (Attrib.binding * term) list) =
- fst (prep_spec raw_fixes raw_spec lthy);
- val chead_of_spec =
- chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd;
- fun name_of (Free (n, _)) = n
- | name_of t = fixrec_err ("unknown term");
- val all_names = map (name_of o chead_of_spec) spec;
- val names = distinct (op =) all_names;
- fun block_of_name n =
- map_filter
- (fn (m,eq) => if m = n then SOME eq else NONE)
- (all_names ~~ spec);
- val blocks = map block_of_name names;
-
- val matcher_tab = FixrecMatchData.get (ProofContext.theory_of lthy);
- fun match_name c =
- case Symtab.lookup matcher_tab c of SOME m => m
- | NONE => fixrec_err ("unknown pattern constructor: " ^ c);
-
- val matches = map (compile_pats match_name) (map (map snd) blocks);
- val spec' = map (pair Attrib.empty_binding) matches;
- val (lthy', cnames, fixdef_thms, unfold_thms) =
- add_fixdefs fixes spec' lthy;
- in
- if strict then let (* only prove simp rules if strict = true *)
- val simps : (Attrib.binding * thm) list list =
- map (make_simps lthy') (unfold_thms ~~ blocks);
- fun mk_bind n : Attrib.binding =
- (Binding.name (n ^ "_simps"),
- [Attrib.internal (K Simplifier.simp_add)]);
- val simps1 : (Attrib.binding * thm list) list =
- map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps);
- val simps2 : (Attrib.binding * thm list) list =
- map (apsnd (fn thm => [thm])) (List.concat simps);
- val (_, lthy'') = lthy'
- |> fold_map (LocalTheory.note Thm.generatedK) (simps1 @ simps2);
- in
- lthy''
- end
- else lthy'
- end;
-
-in
-
-val add_fixrec = gen_fixrec false Specification.check_spec;
-val add_fixrec_cmd = gen_fixrec true Specification.read_spec;
-
-end; (* local *)
-
-(*************************************************************************)
-(******************************** Fixpat *********************************)
-(*************************************************************************)
-
-fun fix_pat thy t =
- let
- val T = fastype_of t;
- val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
- val cname = case chead_of t of Const(c,_) => c | _ =>
- fixrec_err "function is not declared as constant in theory";
- val unfold_thm = PureThy.get_thm thy (cname^"_unfold");
- val simp = Goal.prove_global thy [] [] eq
- (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
- in simp end;
-
-fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
- let
- val atts = map (prep_attrib thy) srcs;
- val ts = map (prep_term thy) strings;
- val simps = map (fix_pat thy) ts;
- in
- (snd o PureThy.add_thmss [((name, simps), atts)]) thy
- end;
-
-val add_fixpat = gen_add_fixpat Sign.cert_term (K I);
-val add_fixpat_cmd = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
-
-
-(*************************************************************************)
-(******************************** Parsers ********************************)
-(*************************************************************************)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl
- ((P.opt_keyword "permissive" >> not) -- P.fixes -- SpecParse.where_alt_specs
- >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
-
-val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
- (SpecParse.specs >> (Toplevel.theory o add_fixpat_cmd));
-
-end;
-
-val setup = FixrecMatchData.init;
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tools/pcpodef.ML Sun Jun 21 15:45:57 2009 +0200
@@ -0,0 +1,201 @@
+(* Title: HOLCF/Tools/pcpodef.ML
+ Author: Brian Huffman
+
+Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
+typedef (see also ~~/src/HOL/Tools/typedef.ML).
+*)
+
+signature PCPODEF =
+sig
+ val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
+ * (binding * binding) option -> theory -> Proof.state
+ val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
+ * (binding * binding) option -> theory -> Proof.state
+ val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
+ * (binding * binding) option -> theory -> Proof.state
+ val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
+ * (binding * binding) option -> theory -> Proof.state
+end;
+
+structure Pcpodef :> PCPODEF =
+struct
+
+(** type definitions **)
+
+(* prepare_cpodef *)
+
+fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
+
+fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
+fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
+
+fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =
+ let
+ val _ = Theory.requires thy "Pcpodef" "pcpodefs";
+ val ctxt = ProofContext.init thy;
+
+ val full = Sign.full_name thy;
+ val full_name = full name;
+ val bname = Binding.name_of name;
+
+ (*rhs*)
+ val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
+ val setT = Term.fastype_of set;
+ val rhs_tfrees = Term.add_tfrees set [];
+ val oldT = HOLogic.dest_setT setT handle TYPE _ =>
+ error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
+
+ (*goal*)
+ val goal_UU_mem = HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
+ val goal_nonempty =
+ HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
+ val goal_admissible =
+ HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
+
+ (*lhs*)
+ val defS = Sign.defaultS thy;
+ val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
+ val lhs_sorts = map snd lhs_tfrees;
+
+ val tname = Binding.map_name (Syntax.type_name mx) t;
+ val full_tname = full tname;
+ val newT = Type (full_tname, map TFree lhs_tfrees);
+
+ val (Rep_name, Abs_name) =
+ (case opt_morphs of
+ NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
+ | SOME morphs => morphs);
+ val RepC = Const (full Rep_name, newT --> oldT);
+ fun belowC T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
+ val below_def = Logic.mk_equals (belowC newT,
+ Abs ("x", newT, Abs ("y", newT, belowC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
+
+ fun make_po tac thy1 =
+ let
+ val ((_, {type_definition, set_def, ...}), thy2) = thy1
+ |> Typedef.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
+ val lthy3 = thy2
+ |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
+ val below_def' = Syntax.check_term lthy3 below_def;
+ val ((_, (_, below_definition')), lthy4) = lthy3
+ |> Specification.definition (NONE,
+ ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def'));
+ val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
+ val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition';
+ val thy5 = lthy4
+ |> Class.prove_instantiation_instance
+ (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
+ |> LocalTheory.exit_global;
+ in ((type_definition, below_definition, set_def), thy5) end;
+
+ fun make_cpo admissible (type_def, below_def, set_def) theory =
+ let
+ val admissible' = fold_rule (the_list set_def) admissible;
+ val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible'];
+ val theory' = theory
+ |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
+ (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
+ val cpo_thms' = map (Thm.transfer theory') cpo_thms;
+ in
+ theory'
+ |> Sign.add_path (Binding.name_of name)
+ |> PureThy.add_thms
+ ([((Binding.prefix_name "adm_" name, admissible'), []),
+ ((Binding.prefix_name "cont_" Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []),
+ ((Binding.prefix_name "cont_" Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []),
+ ((Binding.prefix_name "lub_" name, @{thm typedef_lub} OF cpo_thms'), []),
+ ((Binding.prefix_name "thelub_" name, @{thm typedef_thelub} OF cpo_thms'), []),
+ ((Binding.prefix_name "compact_" name, @{thm typedef_compact} OF cpo_thms'), [])])
+ |> snd
+ |> Sign.parent_path
+ end;
+
+ fun make_pcpo UU_mem (type_def, below_def, set_def) theory =
+ let
+ val UU_mem' = fold_rule (the_list set_def) UU_mem;
+ val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem'];
+ val theory' = theory
+ |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
+ (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
+ val pcpo_thms' = map (Thm.transfer theory') pcpo_thms;
+ in
+ theory'
+ |> Sign.add_path (Binding.name_of name)
+ |> PureThy.add_thms
+ ([((Binding.suffix_name "_strict" Rep_name, @{thm typedef_Rep_strict} OF pcpo_thms'), []),
+ ((Binding.suffix_name "_strict" Abs_name, @{thm typedef_Abs_strict} OF pcpo_thms'), []),
+ ((Binding.suffix_name "_strict_iff" Rep_name, @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
+ ((Binding.suffix_name "_strict_iff" Abs_name, @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
+ ((Binding.suffix_name "_defined" Rep_name, @{thm typedef_Rep_defined} OF pcpo_thms'), []),
+ ((Binding.suffix_name "_defined" Abs_name, @{thm typedef_Abs_defined} OF pcpo_thms'), [])])
+ |> snd
+ |> Sign.parent_path
+ end;
+
+ fun pcpodef_result UU_mem admissible =
+ make_po (Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1)
+ #-> (fn defs => make_cpo admissible defs #> make_pcpo UU_mem defs);
+
+ fun cpodef_result nonempty admissible =
+ make_po (Tactic.rtac nonempty 1)
+ #-> make_cpo admissible;
+ in
+ if pcpo
+ then (goal_UU_mem, goal_admissible, pcpodef_result)
+ else (goal_nonempty, goal_admissible, cpodef_result)
+ end
+ handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
+
+
+(* proof interface *)
+
+local
+
+fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy =
+ let
+ val (goal1, goal2, make_result) =
+ prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
+ fun after_qed [[th1, th2]] = ProofContext.theory (make_result th1 th2);
+ in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end;
+
+in
+
+fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term true x;
+fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term true x;
+
+fun cpodef_proof x = gen_pcpodef_proof Syntax.check_term false x;
+fun cpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term false x;
+
+end;
+
+
+
+(** outer syntax **)
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val typedef_proof_decl =
+ Scan.optional (P.$$$ "(" |--
+ ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
+ --| P.$$$ ")") (true, NONE) --
+ (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
+ Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
+
+fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
+ (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
+ ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs);
+
+val _ =
+ OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
+ (typedef_proof_decl >>
+ (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
+
+val _ =
+ OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
+ (typedef_proof_decl >>
+ (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
+
+end;
+
+end;
--- a/src/HOLCF/Tools/pcpodef_package.ML Sun Jun 21 15:45:42 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,201 +0,0 @@
-(* Title: HOLCF/Tools/pcpodef.ML
- Author: Brian Huffman
-
-Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
-typedef (see also ~~/src/HOL/Tools/typedef.ML).
-*)
-
-signature PCPODEF =
-sig
- val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
- * (binding * binding) option -> theory -> Proof.state
- val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
- * (binding * binding) option -> theory -> Proof.state
- val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
- * (binding * binding) option -> theory -> Proof.state
- val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
- * (binding * binding) option -> theory -> Proof.state
-end;
-
-structure Pcpodef :> PCPODEF =
-struct
-
-(** type definitions **)
-
-(* prepare_cpodef *)
-
-fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
-
-fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
-fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
-
-fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =
- let
- val _ = Theory.requires thy "Pcpodef" "pcpodefs";
- val ctxt = ProofContext.init thy;
-
- val full = Sign.full_name thy;
- val full_name = full name;
- val bname = Binding.name_of name;
-
- (*rhs*)
- val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
- val setT = Term.fastype_of set;
- val rhs_tfrees = Term.add_tfrees set [];
- val oldT = HOLogic.dest_setT setT handle TYPE _ =>
- error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
-
- (*goal*)
- val goal_UU_mem = HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
- val goal_nonempty =
- HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
- val goal_admissible =
- HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
-
- (*lhs*)
- val defS = Sign.defaultS thy;
- val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
- val lhs_sorts = map snd lhs_tfrees;
-
- val tname = Binding.map_name (Syntax.type_name mx) t;
- val full_tname = full tname;
- val newT = Type (full_tname, map TFree lhs_tfrees);
-
- val (Rep_name, Abs_name) =
- (case opt_morphs of
- NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
- | SOME morphs => morphs);
- val RepC = Const (full Rep_name, newT --> oldT);
- fun belowC T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
- val below_def = Logic.mk_equals (belowC newT,
- Abs ("x", newT, Abs ("y", newT, belowC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
-
- fun make_po tac thy1 =
- let
- val ((_, {type_definition, set_def, ...}), thy2) = thy1
- |> Typedef.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
- val lthy3 = thy2
- |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
- val below_def' = Syntax.check_term lthy3 below_def;
- val ((_, (_, below_definition')), lthy4) = lthy3
- |> Specification.definition (NONE,
- ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def'));
- val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
- val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition';
- val thy5 = lthy4
- |> Class.prove_instantiation_instance
- (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
- |> LocalTheory.exit_global;
- in ((type_definition, below_definition, set_def), thy5) end;
-
- fun make_cpo admissible (type_def, below_def, set_def) theory =
- let
- val admissible' = fold_rule (the_list set_def) admissible;
- val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible'];
- val theory' = theory
- |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
- (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
- val cpo_thms' = map (Thm.transfer theory') cpo_thms;
- in
- theory'
- |> Sign.add_path (Binding.name_of name)
- |> PureThy.add_thms
- ([((Binding.prefix_name "adm_" name, admissible'), []),
- ((Binding.prefix_name "cont_" Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []),
- ((Binding.prefix_name "cont_" Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []),
- ((Binding.prefix_name "lub_" name, @{thm typedef_lub} OF cpo_thms'), []),
- ((Binding.prefix_name "thelub_" name, @{thm typedef_thelub} OF cpo_thms'), []),
- ((Binding.prefix_name "compact_" name, @{thm typedef_compact} OF cpo_thms'), [])])
- |> snd
- |> Sign.parent_path
- end;
-
- fun make_pcpo UU_mem (type_def, below_def, set_def) theory =
- let
- val UU_mem' = fold_rule (the_list set_def) UU_mem;
- val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem'];
- val theory' = theory
- |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
- (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
- val pcpo_thms' = map (Thm.transfer theory') pcpo_thms;
- in
- theory'
- |> Sign.add_path (Binding.name_of name)
- |> PureThy.add_thms
- ([((Binding.suffix_name "_strict" Rep_name, @{thm typedef_Rep_strict} OF pcpo_thms'), []),
- ((Binding.suffix_name "_strict" Abs_name, @{thm typedef_Abs_strict} OF pcpo_thms'), []),
- ((Binding.suffix_name "_strict_iff" Rep_name, @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
- ((Binding.suffix_name "_strict_iff" Abs_name, @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
- ((Binding.suffix_name "_defined" Rep_name, @{thm typedef_Rep_defined} OF pcpo_thms'), []),
- ((Binding.suffix_name "_defined" Abs_name, @{thm typedef_Abs_defined} OF pcpo_thms'), [])])
- |> snd
- |> Sign.parent_path
- end;
-
- fun pcpodef_result UU_mem admissible =
- make_po (Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1)
- #-> (fn defs => make_cpo admissible defs #> make_pcpo UU_mem defs);
-
- fun cpodef_result nonempty admissible =
- make_po (Tactic.rtac nonempty 1)
- #-> make_cpo admissible;
- in
- if pcpo
- then (goal_UU_mem, goal_admissible, pcpodef_result)
- else (goal_nonempty, goal_admissible, cpodef_result)
- end
- handle ERROR msg =>
- cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
-
-
-(* proof interface *)
-
-local
-
-fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy =
- let
- val (goal1, goal2, make_result) =
- prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
- fun after_qed [[th1, th2]] = ProofContext.theory (make_result th1 th2);
- in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end;
-
-in
-
-fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term true x;
-fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term true x;
-
-fun cpodef_proof x = gen_pcpodef_proof Syntax.check_term false x;
-fun cpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term false x;
-
-end;
-
-
-
-(** outer syntax **)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val typedef_proof_decl =
- Scan.optional (P.$$$ "(" |--
- ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
- --| P.$$$ ")") (true, NONE) --
- (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
-
-fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
- (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
- ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs);
-
-val _ =
- OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
- (typedef_proof_decl >>
- (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
-
-val _ =
- OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
- (typedef_proof_decl >>
- (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
-
-end;
-
-end;