simplified internal interfaces; cong rules are now handled directly by "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 =
--- 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
--- 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
--- 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 *)