--- 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"];
--- 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]