# HG changeset patch # User krauss # Date 1186490998 -7200 # Node ID 86a03a092062c348885fca74f2892e388ca811fe # Parent bd79401b3507be9d0ebc59f7f90881960cf3e13d simplified internal interfaces; cong rules are now handled directly by "context_tree.ML" diff -r bd79401b3507 -r 86a03a092062 src/HOL/Tools/function_package/context_tree.ML --- a/src/HOL/Tools/function_package/context_tree.ML Tue Aug 07 10:03:25 2007 +0200 +++ b/src/HOL/Tools/function_package/context_tree.ML Tue Aug 07 14:49:58 2007 +0200 @@ -13,11 +13,14 @@ type ctx_tree (* FIXME: This interface is a mess and needs to be cleaned up! *) - val cong_deps : thm -> int IntGraph.T - val add_congs : thm list + val get_fundef_congs : Context.generic -> thm list + val add_fundef_cong : thm -> Context.generic -> Context.generic + val map_fundef_congs : (thm list -> thm list) -> Context.generic -> Context.generic - val mk_tree: (thm * depgraph) list -> - (string * typ) -> term -> Proof.context -> term -> ctx_tree + val cong_add: attribute + val cong_del: attribute + + val mk_tree: (string * typ) -> term -> Proof.context -> term -> ctx_tree val inst_tree: theory -> term -> term -> ctx_tree -> ctx_tree @@ -44,6 +47,24 @@ open FundefCommon open FundefLib +structure FundefCongs = GenericDataFun +( + type T = thm list + val empty = [] + val extend = I + fun merge _ = Thm.merge_thms +); + +val map_fundef_congs = FundefCongs.map +val get_fundef_congs = FundefCongs.get +val add_fundef_cong = FundefCongs.map o Thm.add_thm + +(* congruence rules *) + +val cong_add = Thm.declaration_attribute (map_fundef_congs o Thm.add_thm o safe_mk_meta_eq); +val cong_del = Thm.declaration_attribute (map_fundef_congs o Thm.del_thm o safe_mk_meta_eq); + + type depgraph = int IntGraph.T datatype ctx_tree @@ -71,13 +92,13 @@ fun cong_deps crule = let - val branches = map branch_vars (prems_of crule) - val num_branches = (1 upto (length branches)) ~~ branches + val branches = map branch_vars (prems_of crule) + val num_branches = (1 upto (length branches)) ~~ branches in - IntGraph.empty - |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches - |> fold (fn ((i,(c1,_)),(j,(_, t2))) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j)) - (product num_branches num_branches) + IntGraph.empty + |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches + |> fold (fn ((i,(c1,_)),(j,(_, t2))) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j)) + (product num_branches num_branches) end val add_congs = map (fn c => c RS eq_reflection) [cong, ext] @@ -87,11 +108,11 @@ (* Called on the INSTANTIATED branches of the congruence rule *) fun mk_branch ctx t = let - val (ctx', fixes, impl) = dest_all_all_ctx ctx t + val (ctx', fixes, impl) = dest_all_all_ctx ctx t in (ctx', fixes, Logic.strip_imp_prems impl, rhs_of (Logic.strip_imp_concl impl)) end - + fun find_cong_rule ctx fvar h ((r,dep)::rs) t = (let val thy = ProofContext.theory_of ctx @@ -112,18 +133,26 @@ fun matchcall fvar (a $ b) = if a = Free fvar then SOME b else NONE | matchcall fvar _ = NONE -fun mk_tree congs fvar h ctx t = - case matchcall fvar t of - SOME arg => RCall (t, mk_tree congs fvar h ctx arg) - | NONE => - if not (exists_subterm (fn Free v => v = fvar | _ => false) t) then Leaf t - else - let val (r, dep, branches) = find_cong_rule ctx fvar h congs t in - Cong (t, r, dep, - map (fn (ctx', fixes, assumes, st) => - (fixes, map (assume o cterm_of (ProofContext.theory_of ctx)) assumes, - mk_tree congs fvar h ctx' st)) branches) - end +fun mk_tree fvar h ctxt t = + let + val congs = get_fundef_congs (Context.Proof ctxt) + val congs_deps = map (fn c => (c, cong_deps c)) (congs @ add_congs) (* FIXME: Save in theory *) + + fun mk_tree' ctx t = + case matchcall fvar t of + SOME arg => RCall (t, mk_tree' ctx arg) + | NONE => + if not (exists_subterm (fn Free v => v = fvar | _ => false) t) then Leaf t + else + let val (r, dep, branches) = find_cong_rule ctx fvar h congs_deps t in + Cong (t, r, dep, + map (fn (ctx', fixes, assumes, st) => + (fixes, map (assume o cterm_of (ProofContext.theory_of ctx)) assumes, + mk_tree' ctx' st)) branches) + end + in + mk_tree' ctxt t + end fun inst_tree thy fvar f tr = diff -r bd79401b3507 -r 86a03a092062 src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Tue Aug 07 10:03:25 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_common.ML Tue Aug 07 14:49:58 2007 +0200 @@ -84,15 +84,6 @@ ); -structure FundefCongs = GenericDataFun -( - type T = thm list - val empty = [] - val extend = I - fun merge _ = Thm.merge_thms -); - - (* Generally useful?? *) fun lift_morphism thy f = let @@ -126,11 +117,6 @@ val all_fundef_data = NetRules.rules o FundefData.get -val map_fundef_congs = FundefCongs.map -val get_fundef_congs = FundefCongs.get - - - structure TerminationRule = GenericDataFun ( type T = thm list diff -r bd79401b3507 -r 86a03a092062 src/HOL/Tools/function_package/fundef_core.ML --- a/src/HOL/Tools/function_package/fundef_core.ML Tue Aug 07 10:03:25 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_core.ML Tue Aug 07 14:49:58 2007 +0200 @@ -403,7 +403,7 @@ -fun prove_stuff ctxt congs globals G f R clauses complete compat compat_store G_elim f_def = +fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def = let val Globals {h, domT, ranT, x, ...} = globals val thy = ProofContext.theory_of ctxt @@ -868,7 +868,6 @@ val default = singleton (ProofContext.read_termTs lthy) (default_str, fT) - val congs = get_fundef_congs (Context.Proof lthy) val (globals, ctxt') = fix_globals domT ranT fvar lthy val Globals { x, h, ... } = globals @@ -877,10 +876,8 @@ val n = length abstract_qglrs - val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs) (* FIXME: Save in theory *) - fun build_tree (ClauseContext { ctxt, rhs, ...}) = - FundefCtxTree.mk_tree congs_deps (fname, fT) h ctxt rhs + FundefCtxTree.mk_tree (fname, fT) h ctxt rhs val trees = map build_tree clauses val RCss = map find_calls trees @@ -912,7 +909,7 @@ val compat_store = store_compat_thms n compat - val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff lthy congs globals G f R xclauses complete compat compat_store G_elim) f_defthm + val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff lthy globals G f R xclauses complete compat compat_store G_elim) f_defthm val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses diff -r bd79401b3507 -r 86a03a092062 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Tue Aug 07 10:03:25 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Aug 07 14:49:58 2007 +0200 @@ -25,9 +25,6 @@ val setup_termination_proof : string option -> local_theory -> Proof.state - val cong_add: attribute - val cong_del: attribute - val setup : theory -> theory val setup_case_cong_hook : theory -> theory val get_congs : theory -> thm list @@ -169,17 +166,11 @@ val add_fundef_i = gen_add_fundef Specification.cert_specification - -(* congruence rules *) - -val cong_add = Thm.declaration_attribute (map_fundef_congs o Thm.add_thm o safe_mk_meta_eq); -val cong_del = Thm.declaration_attribute (map_fundef_congs o Thm.del_thm o safe_mk_meta_eq); - (* Datatype hook to declare datatype congs as "fundef_congs" *) fun add_case_cong n thy = - Context.theory_map (map_fundef_congs (Thm.add_thm + Context.theory_map (FundefCtxTree.map_fundef_congs (Thm.add_thm (DatatypePackage.get_datatype thy n |> the |> #case_cong |> safe_mk_meta_eq))) @@ -266,14 +257,13 @@ val setup = Attrib.add_attributes - [("fundef_cong", Attrib.add_del_args cong_add cong_del, + [("fundef_cong", Attrib.add_del_args FundefCtxTree.cong_add FundefCtxTree.cong_del, "declaration of congruence rule for function definitions")] #> setup_case_cong_hook #> FundefRelation.setup #> elim_to_cases_setup -val get_congs = FundefCommon.get_fundef_congs o Context.Theory - +val get_congs = FundefCtxTree.get_fundef_congs o Context.Theory (* outer syntax *)