# HG changeset patch # User wenzelm # Date 1126642759 -7200 # Node ID c05f72cff36896710f1d5a8410a00e173851251e # Parent 7cff05c90a0e27171768cedbd6d6985bdb5ce506 tuned IsarThy.theorem_i; diff -r 7cff05c90a0e -r c05f72cff368 src/HOL/Tools/recdef_package.ML --- a/src/HOL/Tools/recdef_package.ML Tue Sep 13 17:05:59 2005 +0200 +++ b/src/HOL/Tools/recdef_package.ML Tue Sep 13 22:19:19 2005 +0200 @@ -35,10 +35,9 @@ -> theory -> theory * {induct_rules: thm} val defer_recdef_i: xstring -> term list -> (thm list * theory attribute list) list -> theory -> theory * {induct_rules: thm} - val recdef_tc: bstring * Attrib.src list -> xstring -> int option - -> bool -> theory -> ProofHistory.T + val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> theory -> Proof.state val recdef_tc_i: bstring * theory attribute list -> string -> int option - -> bool -> theory -> ProofHistory.T + -> theory -> Proof.state val setup: (theory -> theory) list end; @@ -302,7 +301,7 @@ (** recdef_tc(_i) **) -fun gen_recdef_tc prep_att prep_name (bname, raw_atts) raw_name opt_i int thy = +fun gen_recdef_tc prep_att prep_name (bname, raw_atts) raw_name opt_i thy = let val name = prep_name thy raw_name; val atts = map (prep_att thy) raw_atts; @@ -314,10 +313,7 @@ val tc = List.nth (tcs, i - 1) handle Subscript => error ("No termination condition #" ^ string_of_int i ^ " in recdef definition of " ^ quote name); - in - thy - |> IsarThy.theorem_i Drule.internalK ((bname, atts), (HOLogic.mk_Trueprop tc, ([], []))) int - end; + in IsarThy.theorem_i Drule.internalK (bname, atts) (HOLogic.mk_Trueprop tc, ([], [])) thy end; val recdef_tc = gen_recdef_tc Attrib.global_attribute Sign.intern_const; val recdef_tc_i = gen_recdef_tc (K I) (K I); @@ -362,15 +358,11 @@ OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl (defer_recdef_decl >> Toplevel.theory); - -val recdef_tc_decl = - P.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")"); - -fun mk_recdef_tc ((thm_name, name), i) = recdef_tc thm_name name i; - val recdef_tcP = OuterSyntax.command "recdef_tc" "recommence proof of termination condition (TFL)" K.thy_goal - (recdef_tc_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_recdef_tc))); + (P.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") + >> (fn ((thm_name, name), i) => + Toplevel.print o Toplevel.theory_to_proof (recdef_tc thm_name name i))); val _ = OuterSyntax.add_keywords ["permissive", "congs", "hints"]; diff -r 7cff05c90a0e -r c05f72cff368 src/HOL/Tools/specification_package.ML --- a/src/HOL/Tools/specification_package.ML Tue Sep 13 17:05:59 2005 +0200 +++ b/src/HOL/Tools/specification_package.ML Tue Sep 13 22:19:19 2005 +0200 @@ -7,9 +7,9 @@ signature SPECIFICATION_PACKAGE = sig - val quiet_mode: bool ref - val add_specification_i: string option -> (bstring * xstring * bool) list - -> theory * thm -> theory * thm + val quiet_mode: bool ref + val add_specification_i: string option -> (bstring * xstring * bool) list -> + theory attribute end structure SpecificationPackage : SPECIFICATION_PACKAGE = @@ -34,64 +34,64 @@ local fun mk_definitional [] arg = arg | mk_definitional ((thname,cname,covld)::cos) (thy,thm) = - case HOLogic.dest_Trueprop (concl_of thm) of - Const("Ex",_) $ P => - let - val ctype = domain_type (type_of P) - val cname_full = Sign.intern_const (sign_of thy) cname - val cdefname = if thname = "" - then Thm.def_name (Sign.base_name cname) - else thname - val def_eq = Logic.mk_equals (Const(cname_full,ctype), - HOLogic.choice_const ctype $ P) - val (thy',thms) = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy - val thm' = [thm,hd thms] MRS helper - in - mk_definitional cos (thy',thm') - end - | _ => raise THM ("Internal error: Bad specification theorem",0,[thm]) + case HOLogic.dest_Trueprop (concl_of thm) of + Const("Ex",_) $ P => + let + val ctype = domain_type (type_of P) + val cname_full = Sign.intern_const (sign_of thy) cname + val cdefname = if thname = "" + then Thm.def_name (Sign.base_name cname) + else thname + val def_eq = Logic.mk_equals (Const(cname_full,ctype), + HOLogic.choice_const ctype $ P) + val (thy',thms) = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy + val thm' = [thm,hd thms] MRS helper + in + mk_definitional cos (thy',thm') + end + | _ => raise THM ("Internal error: Bad specification theorem",0,[thm]) fun mk_axiomatic axname cos arg = - let - fun process [] (thy,tm) = - let - val (thy',thms) = PureThy.add_axioms_i [((axname,HOLogic.mk_Trueprop tm),[])] thy - in - (thy',hd thms) - end - | process ((thname,cname,covld)::cos) (thy,tm) = - case tm of - Const("Ex",_) $ P => - let - val ctype = domain_type (type_of P) - val cname_full = Sign.intern_const (sign_of thy) cname - val cdefname = if thname = "" - then Thm.def_name (Sign.base_name cname) - else thname - val co = Const(cname_full,ctype) - val thy' = Theory.add_finals_i covld [co] thy - val tm' = case P of - Abs(_, _, bodt) => subst_bound (co, bodt) - | _ => P $ co - in - process cos (thy',tm') - end - | _ => raise TERM ("Internal error: Bad specification theorem",[tm]) - in - process cos arg - end + let + fun process [] (thy,tm) = + let + val (thy',thms) = PureThy.add_axioms_i [((axname,HOLogic.mk_Trueprop tm),[])] thy + in + (thy',hd thms) + end + | process ((thname,cname,covld)::cos) (thy,tm) = + case tm of + Const("Ex",_) $ P => + let + val ctype = domain_type (type_of P) + val cname_full = Sign.intern_const (sign_of thy) cname + val cdefname = if thname = "" + then Thm.def_name (Sign.base_name cname) + else thname + val co = Const(cname_full,ctype) + val thy' = Theory.add_finals_i covld [co] thy + val tm' = case P of + Abs(_, _, bodt) => subst_bound (co, bodt) + | _ => P $ co + in + process cos (thy',tm') + end + | _ => raise TERM ("Internal error: Bad specification theorem",[tm]) + in + process cos arg + end in fun proc_exprop axiomatic cos arg = case axiomatic of - SOME axname => mk_axiomatic axname cos (apsnd (HOLogic.dest_Trueprop o concl_of) arg) + SOME axname => mk_axiomatic axname cos (apsnd (HOLogic.dest_Trueprop o concl_of) arg) | NONE => mk_definitional cos arg end fun add_specification_i axiomatic cos arg = arg |> apsnd freezeT - |> proc_exprop axiomatic cos - |> apsnd standard + |> proc_exprop axiomatic cos + |> apsnd standard (* Collect all intances of constants in term *) @@ -104,169 +104,167 @@ fun unvarify t fmap = let - val fmap' = map Library.swap fmap - fun unthaw (f as (a,S)) = - (case assoc (fmap',a) of - NONE => TVar f - | SOME (b, _) => TFree (b,S)) + val fmap' = map Library.swap fmap + fun unthaw (f as (a,S)) = + (case assoc (fmap',a) of + NONE => TVar f + | SOME (b, _) => TFree (b,S)) in - map_term_types (map_type_tvar unthaw) t + map_term_types (map_type_tvar unthaw) t end (* The syntactic meddling needed to setup add_specification for work *) -fun process_spec axiomatic cos alt_props int thy = +fun process_spec axiomatic cos alt_props thy = let - fun zip3 [] [] [] = [] - | zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs - | zip3 _ _ _ = error "SpecificationPackage.process_spec internal error" + fun zip3 [] [] [] = [] + | zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs + | zip3 _ _ _ = error "SpecificationPackage.process_spec internal error" - fun myfoldr f [x] = x - | myfoldr f (x::xs) = f (x,myfoldr f xs) - | myfoldr f [] = error "SpecificationPackage.process_spec internal error" + fun myfoldr f [x] = x + | myfoldr f (x::xs) = f (x,myfoldr f xs) + | myfoldr f [] = error "SpecificationPackage.process_spec internal error" - val sg = sign_of thy - fun typ_equiv t u = Sign.typ_instance sg (t,u) andalso Sign.typ_instance sg (u,t); + val sg = sign_of thy + fun typ_equiv t u = Sign.typ_instance sg (t,u) andalso Sign.typ_instance sg (u,t); - val cprops = map (Thm.read_cterm sg o rpair Term.propT o snd) alt_props - val ss = empty_ss setmksimps single addsimps [thm "HOL.atomize_imp",thm "HOL.atomize_all"] - val rew_imps = map (Simplifier.full_rewrite ss) cprops - val props' = map (HOLogic.dest_Trueprop o term_of o snd o dest_equals o cprop_of) rew_imps + val cprops = map (Thm.read_cterm sg o rpair Term.propT o snd) alt_props + val ss = empty_ss setmksimps single addsimps [thm "HOL.atomize_imp",thm "HOL.atomize_all"] + val rew_imps = map (Simplifier.full_rewrite ss) cprops + val props' = map (HOLogic.dest_Trueprop o term_of o snd o dest_equals o cprop_of) rew_imps - fun proc_single prop = - let - val frees = Term.term_frees prop - val tsig = Sign.tsig_of (sign_of thy) - val _ = assert (forall (fn v => Type.of_sort tsig (type_of v,HOLogic.typeS)) frees) - "Specificaton: Only free variables of sort 'type' allowed" - val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees) - in - (prop_closed,frees) - end + fun proc_single prop = + let + val frees = Term.term_frees prop + val tsig = Sign.tsig_of (sign_of thy) + val _ = assert (forall (fn v => Type.of_sort tsig (type_of v,HOLogic.typeS)) frees) + "Specificaton: Only free variables of sort 'type' allowed" + val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees) + in + (prop_closed,frees) + end - val props'' = map proc_single props' - val frees = map snd props'' - val prop = myfoldr HOLogic.mk_conj (map fst props'') - val cprop = cterm_of sg (HOLogic.mk_Trueprop prop) + val props'' = map proc_single props' + val frees = map snd props'' + val prop = myfoldr HOLogic.mk_conj (map fst props'') + val cprop = cterm_of sg (HOLogic.mk_Trueprop prop) - val (prop_thawed,vmap) = Type.varify (prop,[]) - val thawed_prop_consts = collect_consts (prop_thawed,[]) - val (altcos,overloaded) = Library.split_list cos - val (names,sconsts) = Library.split_list altcos - val consts = map (term_of o Thm.read_cterm sg o rpair TypeInfer.logicT) sconsts - val _ = assert (not (Library.exists (not o Term.is_Const) consts)) - "Specification: Non-constant found as parameter" + val (prop_thawed,vmap) = Type.varify (prop,[]) + val thawed_prop_consts = collect_consts (prop_thawed,[]) + val (altcos,overloaded) = Library.split_list cos + val (names,sconsts) = Library.split_list altcos + val consts = map (term_of o Thm.read_cterm sg o rpair TypeInfer.logicT) sconsts + val _ = assert (not (Library.exists (not o Term.is_Const) consts)) + "Specification: Non-constant found as parameter" - fun proc_const c = - let - val c' = fst (Type.varify (c,[])) - val (cname,ctyp) = dest_Const c' - in - case List.filter (fn t => let val (name,typ) = dest_Const t - in name = cname andalso typ_equiv typ ctyp - end) thawed_prop_consts of - [] => error ("Specification: No suitable instances of constant \"" ^ (Sign.string_of_term sg c) ^ "\" found") - | [cf] => unvarify cf vmap - | _ => error ("Specification: Several variations of \"" ^ (Sign.string_of_term sg c) ^ "\" found (try applying explicit type constraints)") - end - val proc_consts = map proc_const consts - fun mk_exist (c,prop) = - let - val T = type_of c - val cname = Sign.base_name (fst (dest_Const c)) - val vname = if Syntax.is_identifier cname - then cname - else "x" - in - HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c,prop)) - end - val ex_prop = foldr mk_exist prop proc_consts - val cnames = map (fst o dest_Const) proc_consts - fun post_process (arg as (thy,thm)) = - let - fun inst_all sg (thm,v) = - let - val cv = cterm_of sg v - val cT = ctyp_of_term cv - val spec' = instantiate' [SOME cT] [NONE,SOME cv] spec - in - thm RS spec' - end - fun remove_alls frees thm = Library.foldl (inst_all (sign_of_thm thm)) (thm,frees) - fun process_single ((name,atts),rew_imp,frees) args = - let - fun undo_imps thm = - equal_elim (symmetric rew_imp) thm + fun proc_const c = + let + val c' = fst (Type.varify (c,[])) + val (cname,ctyp) = dest_Const c' + in + case List.filter (fn t => let val (name,typ) = dest_Const t + in name = cname andalso typ_equiv typ ctyp + end) thawed_prop_consts of + [] => error ("Specification: No suitable instances of constant \"" ^ (Sign.string_of_term sg c) ^ "\" found") + | [cf] => unvarify cf vmap + | _ => error ("Specification: Several variations of \"" ^ (Sign.string_of_term sg c) ^ "\" found (try applying explicit type constraints)") + end + val proc_consts = map proc_const consts + fun mk_exist (c,prop) = + let + val T = type_of c + val cname = Sign.base_name (fst (dest_Const c)) + val vname = if Syntax.is_identifier cname + then cname + else "x" + in + HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c,prop)) + end + val ex_prop = foldr mk_exist prop proc_consts + val cnames = map (fst o dest_Const) proc_consts + fun post_process (arg as (thy,thm)) = + let + fun inst_all sg (thm,v) = + let + val cv = cterm_of sg v + val cT = ctyp_of_term cv + val spec' = instantiate' [SOME cT] [NONE,SOME cv] spec + in + thm RS spec' + end + fun remove_alls frees thm = Library.foldl (inst_all (sign_of_thm thm)) (thm,frees) + fun process_single ((name,atts),rew_imp,frees) args = + let + fun undo_imps thm = + equal_elim (symmetric rew_imp) thm - fun apply_atts arg = Thm.apply_attributes (arg,map (Attrib.global_attribute thy) atts) - fun add_final (arg as (thy,thm)) = - if name = "" - then arg - else (writeln (" " ^ name ^ ": " ^ (string_of_thm thm)); - PureThy.store_thm((name,thm),[]) thy) - in - args |> apsnd (remove_alls frees) - |> apsnd undo_imps - |> apsnd standard - |> apply_atts - |> add_final - end + fun apply_atts arg = Thm.apply_attributes (arg,map (Attrib.global_attribute thy) atts) + fun add_final (arg as (thy,thm)) = + if name = "" + then arg + else (writeln (" " ^ name ^ ": " ^ (string_of_thm thm)); + PureThy.store_thm((name,thm),[]) thy) + in + args |> apsnd (remove_alls frees) + |> apsnd undo_imps + |> apsnd standard + |> apply_atts + |> add_final + end - fun process_all [proc_arg] args = - process_single proc_arg args - | process_all (proc_arg::rest) (thy,thm) = - let - val single_th = thm RS conjunct1 - val rest_th = thm RS conjunct2 - val (thy',_) = process_single proc_arg (thy,single_th) - in - process_all rest (thy',rest_th) - end - | process_all [] _ = error "SpecificationPackage.process_spec internal error" - val alt_names = map fst alt_props - val _ = if exists (fn(name,_) => not (name = "")) alt_names - then writeln "specification" - else () - in - arg |> apsnd freezeT - |> process_all (zip3 alt_names rew_imps frees) - end + fun process_all [proc_arg] args = + process_single proc_arg args + | process_all (proc_arg::rest) (thy,thm) = + let + val single_th = thm RS conjunct1 + val rest_th = thm RS conjunct2 + val (thy',_) = process_single proc_arg (thy,single_th) + in + process_all rest (thy',rest_th) + end + | process_all [] _ = error "SpecificationPackage.process_spec internal error" + val alt_names = map fst alt_props + val _ = if exists (fn(name,_) => not (name = "")) alt_names + then writeln "specification" + else () + in + arg |> apsnd freezeT + |> process_all (zip3 alt_names rew_imps frees) + end in - IsarThy.theorem_i Drule.internalK - (("",[add_specification_i axiomatic (zip3 names cnames overloaded),post_process]), - (HOLogic.mk_Trueprop ex_prop,([],[]))) int thy + IsarThy.theorem_i Drule.internalK + ("", [add_specification_i axiomatic (zip3 names cnames overloaded), post_process]) + (HOLogic.mk_Trueprop ex_prop, ([], [])) thy end + (* outer syntax *) local structure P = OuterParse and K = OuterKeyword in -(* taken from ~~/Pure/Isar/isar_syn.ML *) -val opt_overloaded = - Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "overloaded" >> K true) --| P.$$$ ")")) false - val opt_name = Scan.optional (P.name --| P.$$$ ":") "" +val opt_overloaded = P.opt_keyword "overloaded"; val specification_decl = - P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" -- - Scan.repeat1 (P.opt_thm_name ":" -- P.prop) + P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" -- + Scan.repeat1 (P.opt_thm_name ":" -- P.prop) val specificationP = OuterSyntax.command "specification" "define constants by specification" K.thy_goal (specification_decl >> (fn (cos,alt_props) => - Toplevel.print o (Toplevel.theory_to_proof - (process_spec NONE cos alt_props)))) + Toplevel.print o (Toplevel.theory_to_proof + (process_spec NONE cos alt_props)))) val ax_specification_decl = P.name -- (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" -- - Scan.repeat1 (P.opt_thm_name ":" -- P.prop)) + Scan.repeat1 (P.opt_thm_name ":" -- P.prop)) val ax_specificationP = OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal (ax_specification_decl >> (fn (axname,(cos,alt_props)) => - Toplevel.print o (Toplevel.theory_to_proof - (process_spec (SOME axname) cos alt_props)))) + Toplevel.print o (Toplevel.theory_to_proof + (process_spec (SOME axname) cos alt_props)))) val _ = OuterSyntax.add_parsers [specificationP,ax_specificationP] diff -r 7cff05c90a0e -r c05f72cff368 src/HOLCF/pcpodef_package.ML --- a/src/HOLCF/pcpodef_package.ML Tue Sep 13 17:05:59 2005 +0200 +++ b/src/HOLCF/pcpodef_package.ML Tue Sep 13 22:19:19 2005 +0200 @@ -9,13 +9,13 @@ sig val quiet_mode: bool ref val pcpodef_proof: (bool * string) * (bstring * string list * mixfix) * string - * (string * string) option -> bool -> theory -> ProofHistory.T + * (string * string) option -> theory -> Proof.state val pcpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term - * (string * string) option -> bool -> theory -> ProofHistory.T + * (string * string) option -> theory -> Proof.state val cpodef_proof: (bool * string) * (bstring * string list * mixfix) * string - * (string * string) option -> bool -> theory -> ProofHistory.T + * (string * string) option -> theory -> Proof.state val cpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term - * (string * string) option -> bool -> theory -> ProofHistory.T + * (string * string) option -> theory -> Proof.state end; structure PcpodefPackage: PCPODEF_PACKAGE = @@ -170,11 +170,11 @@ (* cpodef_proof interface *) -fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) int thy = +fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy = let val (goal, att) = gen_prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy; - in thy |> IsarThy.theorem_i Drule.internalK (("", [att]), (goal, ([], []))) int end; + in IsarThy.theorem_i Drule.internalK ("", [att]) (goal, ([], [])) thy end; val pcpodef_proof = gen_pcpodef_proof read_term true; val pcpodef_proof_i = gen_pcpodef_proof cert_term true;