# HG changeset patch # User krauss # Date 1149574874 -7200 # Node ID c62720b20e9afe3e5659919fa3f59f1235b3116e # Parent dce2168b0ea480c34afebcb93194b1d8d55b0eb8 HOL/Tools/function_package: More cleanup diff -r dce2168b0ea4 -r c62720b20e9a src/HOL/Tools/function_package/context_tree.ML --- a/src/HOL/Tools/function_package/context_tree.ML Mon Jun 05 21:54:26 2006 +0200 +++ b/src/HOL/Tools/function_package/context_tree.ML Tue Jun 06 08:21:14 2006 +0200 @@ -82,7 +82,6 @@ -exception CTREE_INTERNAL of string fun find_cong_rule thy ((r,dep)::rs) t = (let @@ -95,7 +94,7 @@ (r, dep, branches) end handle Pattern.MATCH => find_cong_rule thy rs t) - | find_cong_rule thy [] _ = raise CTREE_INTERNAL "No cong rule found!" (* Should never happen *) + | find_cong_rule thy [] _ = sys_error "function_package/context_tree.ML: No cong rule found!" fun matchcall f (a $ b) = if a = f then SOME b else NONE diff -r dce2168b0ea4 -r c62720b20e9a src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Mon Jun 05 21:54:26 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_common.ML Tue Jun 06 08:21:14 2006 +0200 @@ -40,17 +40,17 @@ datatype rec_call_info = - RCInfo - of { - RI: thm, - RIvs: (string * typ) list, - lRI: thm, - lRIq: thm, - Gh: thm, - Gh': thm, - GmAs: term list, - rcarg: term -} + RCInfo of + { + RI: thm, + RIvs: (string * typ) list, + lRI: thm, + lRIq: thm, + Gh: thm, + Gh': thm, + GmAs: term list, + rcarg: term + } datatype clause_info = ClauseInfo of @@ -80,10 +80,6 @@ case_hyp: thm } - -datatype curry_info = - Curry of { argTs: typ list, curry_ss: simpset } - type inj_proj = ((term -> term) * (term -> term)) type qgar = (string * typ) list * term list * term list * term diff -r dce2168b0ea4 -r c62720b20e9a src/HOL/Tools/function_package/fundef_prep.ML --- a/src/HOL/Tools/function_package/fundef_prep.ML Mon Jun 05 21:54:26 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_prep.ML Tue Jun 06 08:21:14 2006 +0200 @@ -46,29 +46,6 @@ end -fun analyze_eqs eqs = - let - fun dest_geq geq = - let - val qs = add_term_frees (geq, []) - in - case dest_implies_list geq of - (gs, Const ("Trueprop", _) $ (Const ("op =", _) $ (f $ lhs) $ rhs)) => - (f, (qs, gs, lhs, rhs)) - | _ => raise ERROR "Not a guarded equation" - end - - val (fs, glrs) = split_list (map dest_geq eqs) - - val f = (hd fs) (* should be equal and a constant... check! *) - - val used = fold (curry add_term_names) eqs [] (* all names in the eqs *) - (* Must check for recursive calls in guards and new vars in rhss *) - in - (f, glrs, used) - end - - (* maps (qs,gs,lhs,ths) to (qs',gs',lhs',rhs') with primed variables *) fun mk_primed_vars thy glrs = let @@ -162,8 +139,8 @@ val trees = map (build_tree thy f congs) glrs val allused = fold FundefCtxTree.add_context_varnames trees used - val Const (f_proper_name, fT) = f - val fxname = Sign.extern_const thy f_proper_name + val Const (f_fullname, fT) = f + val fname = Sign.base_name f_fullname val domT = domain_type fT val ranT = range_type fT @@ -188,15 +165,15 @@ val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy - val G = Const (Sign.intern_const thy G_name, GT) - val R = Const (Sign.intern_const thy R_name, RT) + val G = Const (Sign.full_name thy G_name, GT) + val R = Const (Sign.full_name thy R_name, RT) val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R val f_eq = Logic.mk_equals (f $ x, Const ("The", (ranT --> boolT) --> ranT) $ Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G)) - val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", f_eq), [])] thy + val ([f_def], thy) = PureThy.add_defs_i false [((fname ^ "_def", f_eq), [])] thy in (Names {f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, used=allused, trees=trees}, thy) end @@ -262,7 +239,7 @@ fun extract_conditions thy names trees congs = let - val Names {f, G, R, acc_R, domT, ranT, f_def, x, z, fvarname, glrs, glrs', ...} = names + val Names {f, R, glrs, glrs', ...} = names val (vRiss, preRiss, Riss) = split_list3 (map2 (extract_Ris thy congs f R) trees glrs) val Gis = map2 (mk_GIntro thy names) glrs preRiss diff -r dce2168b0ea4 -r c62720b20e9a src/HOL/Tools/function_package/fundef_proof.ML --- a/src/HOL/Tools/function_package/fundef_proof.ML Mon Jun 05 21:54:26 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_proof.ML Tue Jun 06 08:21:14 2006 +0200 @@ -350,9 +350,9 @@ val goal = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs,acc_R))) in Goal.init goal - |> (SINGLE (resolve_tac [accI] 1)) |> print |> the - |> (SINGLE (eresolve_tac [R_cases] 1)) |> print |> the - |> (SINGLE (CLASIMPSET auto_tac)) |> print |> the + |> (SINGLE (resolve_tac [accI] 1)) |> the + |> (SINGLE (eresolve_tac [R_cases] 1)) |> the + |> (SINGLE (CLASIMPSET auto_tac)) |> the |> Goal.conclude end diff -r dce2168b0ea4 -r c62720b20e9a src/HOL/Tools/function_package/mutual.ML --- a/src/HOL/Tools/function_package/mutual.ML Mon Jun 05 21:54:26 2006 +0200 +++ b/src/HOL/Tools/function_package/mutual.ML Tue Jun 06 08:21:14 2006 +0200 @@ -83,11 +83,11 @@ val sfun_type = ST --> RST val thy = Sign.add_consts_i [(sfun_xname, sfun_type, NoSyn)] thy (* Add the sum function *) - val sfun = Const (Sign.intern_const thy sfun_xname, sfun_type) + val sfun = Const (Sign.full_name thy sfun_xname, sfun_type) fun define (((((n, T), _), caTs), (pthA, pthR)), qgars) (thy, rews) = let - val fxname = Sign.extern_const thy n + val fxname = Sign.base_name n val f = Const (n, T) val vars = map_index (fn (i,T) => Free ("x" ^ string_of_int i, T)) caTs @@ -100,9 +100,6 @@ (MutualPart {f_name=fxname, const=(n, T),cargTs=caTs,pthA=pthA,pthR=pthR,qgars=qgars,f_def=f_def}, (thy, rews')) end - val _ = print pthsA - val _ = print pthsR - val (parts, (thy, rews)) = fold_map define (((consts ~~ caTss)~~ (pthsA ~~ pthsR)) ~~ qgarss) (thy, []) fun mk_qglrss (MutualPart {qgars, pthA, pthR, ...}) =