# HG changeset patch # User haftmann # Date 1245591957 -7200 # Node ID 002da20f442e91b7654cf35080c7b717dfba253a # Parent 8155c4d94354661c024e7f7d0ce9d90107716fcc discontinued ancient tradition to suffix certain ML module names with "_package" diff -r 8155c4d94354 -r 002da20f442e src/HOLCF/IOA/meta_theory/ioa.ML --- /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; diff -r 8155c4d94354 -r 002da20f442e src/HOLCF/IOA/meta_theory/ioa_package.ML --- 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; diff -r 8155c4d94354 -r 002da20f442e src/HOLCF/Tools/fixrec.ML --- /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; diff -r 8155c4d94354 -r 002da20f442e src/HOLCF/Tools/fixrec_package.ML --- 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; diff -r 8155c4d94354 -r 002da20f442e src/HOLCF/Tools/pcpodef.ML --- /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; diff -r 8155c4d94354 -r 002da20f442e src/HOLCF/Tools/pcpodef_package.ML --- 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;