Function package no longer overwrites theorems.
Some tuning.
--- a/src/HOL/Tools/function_package/context_tree.ML Thu Apr 03 16:03:59 2008 +0200
+++ b/src/HOL/Tools/function_package/context_tree.ML Thu Apr 03 16:34:52 2008 +0200
@@ -81,8 +81,7 @@
fun branch_vars t =
let
val t' = snd (dest_all_all t)
- val assumes = Logic.strip_imp_prems t'
- val concl = Logic.strip_imp_concl t'
+ val (assumes, concl) = Logic.strip_horn t'
in (fold (curry add_term_vars) assumes [], term_vars concl)
end
@@ -104,9 +103,9 @@
fun mk_branch ctx t =
let
val (ctx', fixes, impl) = dest_all_all_ctx ctx t
- val assms = Logic.strip_imp_prems impl
+ val (assms, concl) = Logic.strip_horn impl
in
- (ctx', fixes, assms, rhs_of (Logic.strip_imp_concl impl))
+ (ctx', fixes, assms, rhs_of concl)
end
fun find_cong_rule ctx fvar h ((r,dep)::rs) t =
--- a/src/HOL/Tools/function_package/fundef_common.ML Thu Apr 03 16:03:59 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML Thu Apr 03 16:34:52 2008 +0200
@@ -37,7 +37,6 @@
psimps : thm list,
trsimps : thm list option,
- subset_pinducts : thm list,
simple_pinducts : thm list,
cases : thm,
termination : thm,
@@ -51,7 +50,8 @@
defname : string,
(* contains no logical entities: invariant under morphisms *)
- add_simps : string -> Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+ add_simps : (string -> string) -> string -> Attrib.src list -> thm list
+ -> local_theory -> thm list * local_theory,
case_names : string list,
fs : term list,
@@ -179,9 +179,7 @@
let
fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
val (qs, imp) = open_all_all geq
-
- val gs = Logic.strip_imp_prems imp
- val eq = Logic.strip_imp_concl imp
+ val (gs, eq) = Logic.strip_horn imp
val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
handle TERM _ => error (input_error "Not an equation")
--- a/src/HOL/Tools/function_package/fundef_core.ML Thu Apr 03 16:03:59 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML Thu Apr 03 16:34:52 2008 +0200
@@ -684,7 +684,7 @@
|> forall_intr (cterm_of thy a)
|> forall_intr (cterm_of thy P)
in
- (subset_induct_all, simple_induct_rule)
+ simple_induct_rule
end
@@ -927,7 +927,7 @@
val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
- val (subset_pinduct, simple_pinduct) = PROFILE "Proving partial induction rule"
+ val simple_pinduct = PROFILE "Proving partial induction rule"
(mk_partial_induct_rule newthy globals R complete_thm) xclauses
@@ -940,7 +940,7 @@
in
FundefResult {fs=[f], G=G, R=R, cases=complete_thm,
- psimps=psimps, subset_pinducts=[subset_pinduct], simple_pinducts=[simple_pinduct],
+ psimps=psimps, simple_pinducts=[simple_pinduct],
termination=total_intro, trsimps=trsimps,
domintros=dom_intros}
end
--- a/src/HOL/Tools/function_package/fundef_package.ML Thu Apr 03 16:03:59 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Thu Apr 03 16:34:52 2008 +0200
@@ -40,11 +40,12 @@
fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
-fun add_simps fnames post sort label moreatts simps lthy =
+fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
let
val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts
val spec = post simps
|> map (apfst (apsnd (append atts)))
+ |> map (apfst (apfst extra_qualify))
val (saved_spec_simps, lthy) =
fold_map note_theorem spec lthy
@@ -61,7 +62,7 @@
fun fundef_afterqed config fixes post defname cont sort_cont cnames [[proof]] lthy =
let
- val FundefResult {fs, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} =
+ val FundefResult {fs, R, psimps, trsimps, simple_pinducts, termination, domintros, cases, ...} =
cont (Goal.close_result proof)
val fnames = map (fst o fst) fixes
@@ -70,8 +71,8 @@
val (((psimps', pinducts'), (_, [termination'])), lthy) =
lthy
- |> addsmps "psimps" [] psimps
- ||> fold_option (snd oo addsmps "simps" []) trsimps
+ |> addsmps (NameSpace.qualified "partial") "psimps" [] psimps
+ ||> fold_option (snd oo addsmps I "simps" []) trsimps
||>> note_theorem ((qualify "pinduct",
[Attrib.internal (K (RuleCases.case_names cnames)),
Attrib.internal (K (RuleCases.consumes 1)),
@@ -125,7 +126,7 @@
val qualify = NameSpace.qualified defname;
in
lthy
- |> add_simps "simps" allatts tsimps |> snd
+ |> add_simps I "simps" allatts tsimps |> snd
|> note_theorem ((qualify "induct", [Attrib.internal (K (RuleCases.case_names case_names))]), tinduct) |> snd
end
--- a/src/HOL/Tools/function_package/lexicographic_order.ML Thu Apr 03 16:03:59 2008 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML Thu Apr 03 16:34:52 2008 +0200
@@ -133,8 +133,8 @@
fun dest_term (t : term) =
let
val (vars, prop) = FundefLib.dest_all_all t
- val prems = Logic.strip_imp_prems prop
- val (lhs, rhs) = Logic.strip_imp_concl prop
+ val (prems, concl) = Logic.strip_horn prop
+ val (lhs, rhs) = concl
|> HOLogic.dest_Trueprop
|> HOLogic.dest_mem |> fst
|> HOLogic.dest_prod
--- a/src/HOL/Tools/function_package/mutual.ML Thu Apr 03 16:03:59 2008 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML Thu Apr 03 16:34:52 2008 +0200
@@ -269,7 +269,7 @@
fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
let
val result = inner_cont proof
- val FundefResult {fs=[f], G, R, cases, psimps, trsimps, subset_pinducts=[subset_pinduct],simple_pinducts=[simple_pinduct],
+ val FundefResult {fs=[f], G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
termination,domintros} = result
val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
@@ -290,7 +290,7 @@
val mdomintros = map_option (map (full_simplify rew_ss)) domintros
in
FundefResult { fs=fs, G=G, R=R,
- psimps=mpsimps, subset_pinducts=[subset_pinduct], simple_pinducts=minducts,
+ psimps=mpsimps, simple_pinducts=minducts,
cases=cases, termination=mtermination,
domintros=mdomintros,
trsimps=mtrsimps}