--- a/src/HOL/Fun_Def_Base.thy Wed Oct 29 11:41:54 2014 +0100
+++ b/src/HOL/Fun_Def_Base.thy Wed Oct 29 13:42:38 2014 +0100
@@ -11,8 +11,12 @@
ML_file "Tools/Function/function_lib.ML"
named_theorems termination_simp "simplification rules for termination proofs"
ML_file "Tools/Function/function_common.ML"
-ML_file "Tools/Function/context_tree.ML"
-setup Function_Ctx_Tree.setup
+ML_file "Tools/Function/function_context_tree.ML"
+
+attribute_setup fundef_cong =
+ \<open>Attrib.add_del Function_Context_Tree.cong_add Function_Context_Tree.cong_del\<close>
+ "declaration of congruence rule for function definitions"
+
ML_file "Tools/Function/sum_tree.ML"
end
--- a/src/HOL/Tools/Function/context_tree.ML Wed Oct 29 11:41:54 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,295 +0,0 @@
-(* Title: HOL/Tools/Function/context_tree.ML
- Author: Alexander Krauss, TU Muenchen
-
-Construction and traversal of trees of nested contexts along a term.
-*)
-
-signature FUNCTION_CTXTREE =
-sig
- (* poor man's contexts: fixes + assumes *)
- type ctxt = (string * typ) list * thm list
- type ctx_tree
-
- (* FIXME: This interface is a mess and needs to be cleaned up! *)
- val get_function_congs : Proof.context -> thm list
- val add_function_cong : thm -> Context.generic -> Context.generic
- val map_function_congs : (thm list -> thm list) -> Context.generic -> Context.generic
-
- 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
-
- val export_term : ctxt -> term -> term
- val export_thm : theory -> ctxt -> thm -> thm
- val import_thm : theory -> ctxt -> thm -> thm
-
- val traverse_tree :
- (ctxt -> term ->
- (ctxt * thm) list ->
- (ctxt * thm) list * 'b ->
- (ctxt * thm) list * 'b)
- -> ctx_tree -> 'b -> 'b
-
- val rewrite_by_tree : Proof.context -> term -> thm -> (thm * thm) list ->
- ctx_tree -> thm * (thm * thm) list
-
- val setup : theory -> theory
-end
-
-structure Function_Ctx_Tree : FUNCTION_CTXTREE =
-struct
-
-type ctxt = (string * typ) list * thm list
-
-open Function_Common
-open Function_Lib
-
-structure FunctionCongs = Generic_Data
-(
- type T = thm list
- val empty = []
- val extend = I
- val merge = Thm.merge_thms
-);
-
-val get_function_congs = FunctionCongs.get o Context.Proof
-val map_function_congs = FunctionCongs.map
-val add_function_cong = FunctionCongs.map o Thm.add_thm
-
-(* congruence rules *)
-
-val cong_add = Thm.declaration_attribute (map_function_congs o Thm.add_thm o safe_mk_meta_eq);
-val cong_del = Thm.declaration_attribute (map_function_congs o Thm.del_thm o safe_mk_meta_eq);
-
-
-type depgraph = int Int_Graph.T
-
-datatype ctx_tree =
- Leaf of term
- | Cong of (thm * depgraph * (ctxt * ctx_tree) list)
- | RCall of (term * ctx_tree)
-
-
-(* Maps "Trueprop A = B" to "A" *)
-val rhs_of = snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
-
-
-(*** Dependency analysis for congruence rules ***)
-
-fun branch_vars t =
- let
- val t' = snd (dest_all_all t)
- val (assumes, concl) = Logic.strip_horn t'
- in
- (fold Term.add_vars assumes [], Term.add_vars concl [])
- end
-
-fun cong_deps crule =
- let
- val num_branches = map_index (apsnd branch_vars) (prems_of crule)
- in
- Int_Graph.empty
- |> fold (fn (i,_)=> Int_Graph.new_node (i,i)) num_branches
- |> fold_product (fn (i, (c1, _)) => fn (j, (_, t2)) =>
- if i = j orelse null (inter (op =) c1 t2)
- then I else Int_Graph.add_edge_acyclic (i,j))
- num_branches num_branches
- end
-
-val default_congs =
- map (fn c => c RS eq_reflection) [@{thm "cong"}, @{thm "ext"}]
-
-(* Called on the INSTANTIATED branches of the congruence rule *)
-fun mk_branch ctxt t =
- let
- val ((params, impl), ctxt') = Variable.focus t ctxt
- val (assms, concl) = Logic.strip_horn impl
- in
- (ctxt', map #2 params, assms, rhs_of concl)
- end
-
-fun find_cong_rule ctxt fvar h ((r,dep)::rs) t =
- (let
- val thy = Proof_Context.theory_of ctxt
-
- val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(Free fvar, h)] [] t, t)
- val (c, subs) = (concl_of r, prems_of r)
-
- val subst =
- Pattern.match (Proof_Context.theory_of ctxt) (c, tt') (Vartab.empty, Vartab.empty)
- val branches = map (mk_branch ctxt o Envir.beta_norm o Envir.subst_term subst) subs
- val inst = map (fn v =>
- (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v))))
- (Term.add_vars c [])
- in
- (cterm_instantiate inst r, dep, branches)
- end
- handle Pattern.MATCH => find_cong_rule ctxt fvar h rs t)
- | find_cong_rule _ _ _ [] _ = raise General.Fail "No cong rule found!"
-
-
-fun mk_tree fvar h ctxt t =
- let
- val congs = get_function_congs ctxt
-
- (* FIXME: Save in theory: *)
- val congs_deps = map (fn c => (c, cong_deps c)) (congs @ default_congs)
-
- fun matchcall (a $ b) = if a = Free fvar then SOME b else NONE
- | matchcall _ = NONE
-
- fun mk_tree' ctxt t =
- case matchcall t of
- SOME arg => RCall (t, mk_tree' ctxt 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 ctxt fvar h congs_deps t
- fun subtree (ctxt', fixes, assumes, st) =
- ((fixes,
- map (Thm.assume o cterm_of (Proof_Context.theory_of ctxt)) assumes),
- mk_tree' ctxt' st)
- in
- Cong (r, dep, map subtree branches)
- end
- in
- mk_tree' ctxt t
- end
-
-fun inst_tree thy fvar f tr =
- let
- val cfvar = cterm_of thy fvar
- val cf = cterm_of thy f
-
- fun inst_term t =
- subst_bound(f, abstract_over (fvar, t))
-
- val inst_thm = Thm.forall_elim cf o Thm.forall_intr cfvar
-
- fun inst_tree_aux (Leaf t) = Leaf t
- | inst_tree_aux (Cong (crule, deps, branches)) =
- Cong (inst_thm crule, deps, map inst_branch branches)
- | inst_tree_aux (RCall (t, str)) =
- RCall (inst_term t, inst_tree_aux str)
- and inst_branch ((fxs, assms), str) =
- ((fxs, map (Thm.assume o cterm_of thy o inst_term o prop_of) assms),
- inst_tree_aux str)
- in
- inst_tree_aux tr
- end
-
-
-(* Poor man's contexts: Only fixes and assumes *)
-fun compose (fs1, as1) (fs2, as2) = (fs1 @ fs2, as1 @ as2)
-
-fun export_term (fixes, assumes) =
- fold_rev (curry Logic.mk_implies o prop_of) assumes
- #> fold_rev (Logic.all o Free) fixes
-
-fun export_thm thy (fixes, assumes) =
- fold_rev (Thm.implies_intr o cprop_of) assumes
- #> fold_rev (Thm.forall_intr o cterm_of thy o Free) fixes
-
-fun import_thm thy (fixes, athms) =
- fold (Thm.forall_elim o cterm_of thy o Free) fixes
- #> fold Thm.elim_implies athms
-
-
-(* folds in the order of the dependencies of a graph. *)
-fun fold_deps G f x =
- let
- fun fill_table i (T, x) =
- case Inttab.lookup T i of
- SOME _ => (T, x)
- | NONE =>
- let
- val (T', x') = Int_Graph.Keys.fold fill_table (Int_Graph.imm_succs G i) (T, x)
- val (v, x'') = f (the o Inttab.lookup T') i x'
- in
- (Inttab.update (i, v) T', x'')
- end
-
- val (T, x) = fold fill_table (Int_Graph.keys G) (Inttab.empty, x)
- in
- (Inttab.fold (cons o snd) T [], x)
- end
-
-fun traverse_tree rcOp tr =
- let
- fun traverse_help ctxt (Leaf _) _ x = ([], x)
- | traverse_help ctxt (RCall (t, st)) u x =
- rcOp ctxt t u (traverse_help ctxt st u x)
- | traverse_help ctxt (Cong (_, deps, branches)) u x =
- let
- fun sub_step lu i x =
- let
- val (ctxt', subtree) = nth branches i
- val used = Int_Graph.Keys.fold_rev (append o lu) (Int_Graph.imm_succs deps i) u
- val (subs, x') = traverse_help (compose ctxt ctxt') subtree used x
- val exported_subs = map (apfst (compose ctxt')) subs (* FIXME: Right order of composition? *)
- in
- (exported_subs, x')
- end
- in
- fold_deps deps sub_step x
- |> apfst flat
- end
- in
- snd o traverse_help ([], []) tr []
- end
-
-fun rewrite_by_tree ctxt h ih x tr =
- let
- val thy = Proof_Context.theory_of ctxt
- fun rewrite_help _ _ x (Leaf t) = (Thm.reflexive (cterm_of thy t), x)
- | rewrite_help fix h_as x (RCall (_ $ arg, st)) =
- let
- val (inner, (lRi,ha)::x') = rewrite_help fix h_as x st (* "a' = a" *)
-
- val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
- |> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner))))
- (* (a, h a) : G *)
- val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
- val eq = Thm.implies_elim (Thm.implies_elim inst_ih lRi) iha (* h a = f a *)
-
- val h_a'_eq_h_a = Thm.combination (Thm.reflexive (cterm_of thy h)) inner
- val h_a_eq_f_a = eq RS eq_reflection
- val result = Thm.transitive h_a'_eq_h_a h_a_eq_f_a
- in
- (result, x')
- end
- | rewrite_help fix h_as x (Cong (crule, deps, branches)) =
- let
- fun sub_step lu i x =
- let
- val ((fixes, assumes), st) = nth branches i
- val used = map lu (Int_Graph.immediate_succs deps i)
- |> map (fn u_eq => (u_eq RS sym) RS eq_reflection)
- |> filter_out Thm.is_reflexive
-
- val assumes' = map (simplify (put_simpset HOL_basic_ss ctxt addsimps used)) assumes
-
- val (subeq, x') =
- rewrite_help (fix @ fixes) (h_as @ assumes') x st
- val subeq_exp =
- export_thm thy (fixes, assumes) (subeq RS meta_eq_to_obj_eq)
- in
- (subeq_exp, x')
- end
- val (subthms, x') = fold_deps deps sub_step x
- in
- (fold_rev (curry op COMP) subthms crule, x')
- end
- in
- rewrite_help [] [] x tr
- end
-
-val setup =
- Attrib.setup @{binding fundef_cong} (Attrib.add_del cong_add cong_del)
- "declaration of congruence rule for function definitions"
-
-end
--- a/src/HOL/Tools/Function/function.ML Wed Oct 29 11:41:54 2014 +0100
+++ b/src/HOL/Tools/Function/function.ML Wed Oct 29 13:42:38 2014 +0100
@@ -271,7 +271,7 @@
|> safe_mk_meta_eq
in
Context.theory_map
- (Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy
+ (Function_Context_Tree.map_function_congs (Thm.add_thm cong)) thy
end
val setup_case_cong = Old_Datatype_Data.interpretation (K (fold add_case_cong))
@@ -281,7 +281,7 @@
val setup = setup_case_cong
-val get_congs = Function_Ctx_Tree.get_function_congs
+val get_congs = Function_Context_Tree.get_function_congs
fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t
|> the_single |> snd
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Function/function_context_tree.ML Wed Oct 29 13:42:38 2014 +0100
@@ -0,0 +1,289 @@
+(* Title: HOL/Tools/Function/function_context_tree.ML
+ Author: Alexander Krauss, TU Muenchen
+
+Construction and traversal of trees of nested contexts along a term.
+*)
+
+signature FUNCTION_CONTEXT_TREE =
+sig
+ (* poor man's contexts: fixes + assumes *)
+ type ctxt = (string * typ) list * thm list
+ type ctx_tree
+
+ (* FIXME: This interface is a mess and needs to be cleaned up! *)
+ val get_function_congs : Proof.context -> thm list
+ val add_function_cong : thm -> Context.generic -> Context.generic
+ val map_function_congs : (thm list -> thm list) -> Context.generic -> Context.generic
+
+ 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
+
+ val export_term : ctxt -> term -> term
+ val export_thm : theory -> ctxt -> thm -> thm
+ val import_thm : theory -> ctxt -> thm -> thm
+
+ val traverse_tree :
+ (ctxt -> term ->
+ (ctxt * thm) list ->
+ (ctxt * thm) list * 'b ->
+ (ctxt * thm) list * 'b)
+ -> ctx_tree -> 'b -> 'b
+
+ val rewrite_by_tree : Proof.context -> term -> thm -> (thm * thm) list ->
+ ctx_tree -> thm * (thm * thm) list
+end
+
+structure Function_Context_Tree : FUNCTION_CONTEXT_TREE =
+struct
+
+type ctxt = (string * typ) list * thm list
+
+open Function_Common
+open Function_Lib
+
+structure FunctionCongs = Generic_Data
+(
+ type T = thm list
+ val empty = []
+ val extend = I
+ val merge = Thm.merge_thms
+);
+
+val get_function_congs = FunctionCongs.get o Context.Proof
+val map_function_congs = FunctionCongs.map
+val add_function_cong = FunctionCongs.map o Thm.add_thm
+
+(* congruence rules *)
+
+val cong_add = Thm.declaration_attribute (map_function_congs o Thm.add_thm o safe_mk_meta_eq);
+val cong_del = Thm.declaration_attribute (map_function_congs o Thm.del_thm o safe_mk_meta_eq);
+
+
+type depgraph = int Int_Graph.T
+
+datatype ctx_tree =
+ Leaf of term
+ | Cong of (thm * depgraph * (ctxt * ctx_tree) list)
+ | RCall of (term * ctx_tree)
+
+
+(* Maps "Trueprop A = B" to "A" *)
+val rhs_of = snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
+
+
+(*** Dependency analysis for congruence rules ***)
+
+fun branch_vars t =
+ let
+ val t' = snd (dest_all_all t)
+ val (assumes, concl) = Logic.strip_horn t'
+ in
+ (fold Term.add_vars assumes [], Term.add_vars concl [])
+ end
+
+fun cong_deps crule =
+ let
+ val num_branches = map_index (apsnd branch_vars) (prems_of crule)
+ in
+ Int_Graph.empty
+ |> fold (fn (i,_)=> Int_Graph.new_node (i,i)) num_branches
+ |> fold_product (fn (i, (c1, _)) => fn (j, (_, t2)) =>
+ if i = j orelse null (inter (op =) c1 t2)
+ then I else Int_Graph.add_edge_acyclic (i,j))
+ num_branches num_branches
+ end
+
+val default_congs =
+ map (fn c => c RS eq_reflection) [@{thm "cong"}, @{thm "ext"}]
+
+(* Called on the INSTANTIATED branches of the congruence rule *)
+fun mk_branch ctxt t =
+ let
+ val ((params, impl), ctxt') = Variable.focus t ctxt
+ val (assms, concl) = Logic.strip_horn impl
+ in
+ (ctxt', map #2 params, assms, rhs_of concl)
+ end
+
+fun find_cong_rule ctxt fvar h ((r,dep)::rs) t =
+ (let
+ val thy = Proof_Context.theory_of ctxt
+
+ val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(Free fvar, h)] [] t, t)
+ val (c, subs) = (concl_of r, prems_of r)
+
+ val subst =
+ Pattern.match (Proof_Context.theory_of ctxt) (c, tt') (Vartab.empty, Vartab.empty)
+ val branches = map (mk_branch ctxt o Envir.beta_norm o Envir.subst_term subst) subs
+ val inst = map (fn v =>
+ (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v))))
+ (Term.add_vars c [])
+ in
+ (cterm_instantiate inst r, dep, branches)
+ end
+ handle Pattern.MATCH => find_cong_rule ctxt fvar h rs t)
+ | find_cong_rule _ _ _ [] _ = raise General.Fail "No cong rule found!"
+
+
+fun mk_tree fvar h ctxt t =
+ let
+ val congs = get_function_congs ctxt
+
+ (* FIXME: Save in theory: *)
+ val congs_deps = map (fn c => (c, cong_deps c)) (congs @ default_congs)
+
+ fun matchcall (a $ b) = if a = Free fvar then SOME b else NONE
+ | matchcall _ = NONE
+
+ fun mk_tree' ctxt t =
+ case matchcall t of
+ SOME arg => RCall (t, mk_tree' ctxt 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 ctxt fvar h congs_deps t
+ fun subtree (ctxt', fixes, assumes, st) =
+ ((fixes,
+ map (Thm.assume o cterm_of (Proof_Context.theory_of ctxt)) assumes),
+ mk_tree' ctxt' st)
+ in
+ Cong (r, dep, map subtree branches)
+ end
+ in
+ mk_tree' ctxt t
+ end
+
+fun inst_tree thy fvar f tr =
+ let
+ val cfvar = cterm_of thy fvar
+ val cf = cterm_of thy f
+
+ fun inst_term t =
+ subst_bound(f, abstract_over (fvar, t))
+
+ val inst_thm = Thm.forall_elim cf o Thm.forall_intr cfvar
+
+ fun inst_tree_aux (Leaf t) = Leaf t
+ | inst_tree_aux (Cong (crule, deps, branches)) =
+ Cong (inst_thm crule, deps, map inst_branch branches)
+ | inst_tree_aux (RCall (t, str)) =
+ RCall (inst_term t, inst_tree_aux str)
+ and inst_branch ((fxs, assms), str) =
+ ((fxs, map (Thm.assume o cterm_of thy o inst_term o prop_of) assms),
+ inst_tree_aux str)
+ in
+ inst_tree_aux tr
+ end
+
+
+(* Poor man's contexts: Only fixes and assumes *)
+fun compose (fs1, as1) (fs2, as2) = (fs1 @ fs2, as1 @ as2)
+
+fun export_term (fixes, assumes) =
+ fold_rev (curry Logic.mk_implies o prop_of) assumes
+ #> fold_rev (Logic.all o Free) fixes
+
+fun export_thm thy (fixes, assumes) =
+ fold_rev (Thm.implies_intr o cprop_of) assumes
+ #> fold_rev (Thm.forall_intr o cterm_of thy o Free) fixes
+
+fun import_thm thy (fixes, athms) =
+ fold (Thm.forall_elim o cterm_of thy o Free) fixes
+ #> fold Thm.elim_implies athms
+
+
+(* folds in the order of the dependencies of a graph. *)
+fun fold_deps G f x =
+ let
+ fun fill_table i (T, x) =
+ case Inttab.lookup T i of
+ SOME _ => (T, x)
+ | NONE =>
+ let
+ val (T', x') = Int_Graph.Keys.fold fill_table (Int_Graph.imm_succs G i) (T, x)
+ val (v, x'') = f (the o Inttab.lookup T') i x'
+ in
+ (Inttab.update (i, v) T', x'')
+ end
+
+ val (T, x) = fold fill_table (Int_Graph.keys G) (Inttab.empty, x)
+ in
+ (Inttab.fold (cons o snd) T [], x)
+ end
+
+fun traverse_tree rcOp tr =
+ let
+ fun traverse_help ctxt (Leaf _) _ x = ([], x)
+ | traverse_help ctxt (RCall (t, st)) u x =
+ rcOp ctxt t u (traverse_help ctxt st u x)
+ | traverse_help ctxt (Cong (_, deps, branches)) u x =
+ let
+ fun sub_step lu i x =
+ let
+ val (ctxt', subtree) = nth branches i
+ val used = Int_Graph.Keys.fold_rev (append o lu) (Int_Graph.imm_succs deps i) u
+ val (subs, x') = traverse_help (compose ctxt ctxt') subtree used x
+ val exported_subs = map (apfst (compose ctxt')) subs (* FIXME: Right order of composition? *)
+ in
+ (exported_subs, x')
+ end
+ in
+ fold_deps deps sub_step x
+ |> apfst flat
+ end
+ in
+ snd o traverse_help ([], []) tr []
+ end
+
+fun rewrite_by_tree ctxt h ih x tr =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ fun rewrite_help _ _ x (Leaf t) = (Thm.reflexive (cterm_of thy t), x)
+ | rewrite_help fix h_as x (RCall (_ $ arg, st)) =
+ let
+ val (inner, (lRi,ha)::x') = rewrite_help fix h_as x st (* "a' = a" *)
+
+ val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
+ |> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner))))
+ (* (a, h a) : G *)
+ val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
+ val eq = Thm.implies_elim (Thm.implies_elim inst_ih lRi) iha (* h a = f a *)
+
+ val h_a'_eq_h_a = Thm.combination (Thm.reflexive (cterm_of thy h)) inner
+ val h_a_eq_f_a = eq RS eq_reflection
+ val result = Thm.transitive h_a'_eq_h_a h_a_eq_f_a
+ in
+ (result, x')
+ end
+ | rewrite_help fix h_as x (Cong (crule, deps, branches)) =
+ let
+ fun sub_step lu i x =
+ let
+ val ((fixes, assumes), st) = nth branches i
+ val used = map lu (Int_Graph.immediate_succs deps i)
+ |> map (fn u_eq => (u_eq RS sym) RS eq_reflection)
+ |> filter_out Thm.is_reflexive
+
+ val assumes' = map (simplify (put_simpset HOL_basic_ss ctxt addsimps used)) assumes
+
+ val (subeq, x') =
+ rewrite_help (fix @ fixes) (h_as @ assumes') x st
+ val subeq_exp =
+ export_thm thy (fixes, assumes) (subeq RS meta_eq_to_obj_eq)
+ in
+ (subeq_exp, x')
+ end
+ val (subthms, x') = fold_deps deps sub_step x
+ in
+ (fold_rev (curry op COMP) subthms crule, x')
+ end
+ in
+ rewrite_help [] [] x tr
+ end
+
+end
--- a/src/HOL/Tools/Function/function_core.ML Wed Oct 29 11:41:54 2014 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Wed Oct 29 13:42:38 2014 +0100
@@ -73,7 +73,7 @@
{no: int,
qglr : ((string * typ) list * term list * term * term),
cdata : clause_context,
- tree: Function_Ctx_Tree.ctx_tree,
+ tree: Function_Context_Tree.ctx_tree,
lGI: thm,
RCs: rec_call_info list}
@@ -99,7 +99,7 @@
([], (fixes, assumes, arg) :: xs)
| add_Ri _ _ _ _ = raise Match
in
- rev (Function_Ctx_Tree.traverse_tree add_Ri tree [])
+ rev (Function_Context_Tree.traverse_tree add_Ri tree [])
end
@@ -277,7 +277,7 @@
Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
val (eql, _) =
- Function_Ctx_Tree.rewrite_by_tree ctxt h ih_elim_case (Ris ~~ h_assums) tree
+ Function_Context_Tree.rewrite_by_tree ctxt h ih_elim_case (Ris ~~ h_assums) tree
val replace_lemma = (eql RS meta_eq_to_obj_eq)
|> Thm.implies_intr (cprop_of case_hyp)
@@ -733,11 +733,11 @@
fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
let
val used = (u @ sub)
- |> map (fn (ctxt, thm) => Function_Ctx_Tree.export_thm thy ctxt thm)
+ |> map (fn (ctxt, thm) => Function_Context_Tree.export_thm thy ctxt thm)
val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
|> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
- |> Function_Ctx_Tree.export_term (fixes, assumes)
+ |> Function_Context_Tree.export_term (fixes, assumes)
|> fold_rev (curry Logic.mk_implies o prop_of) ags
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
|> cterm_of thy
@@ -745,7 +745,7 @@
val thm = Thm.assume hyp
|> fold Thm.forall_elim cqs
|> fold Thm.elim_implies ags
- |> Function_Ctx_Tree.import_thm thy (fixes, assumes)
+ |> Function_Context_Tree.import_thm thy (fixes, assumes)
|> fold Thm.elim_implies used (* "(arg, lhs) : R'" *)
val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg))
@@ -757,7 +757,7 @@
(Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection)))))
val ethm = z_acc_local
- |> Function_Ctx_Tree.export_thm thy (fixes,
+ |> Function_Context_Tree.export_thm thy (fixes,
z_eq_arg :: case_hyp :: ags @ assumes)
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
@@ -767,7 +767,7 @@
end
| step _ _ _ _ = raise Match
in
- Function_Ctx_Tree.traverse_tree step tree
+ Function_Context_Tree.traverse_tree step tree
end
@@ -846,7 +846,7 @@
val n = length abstract_qglrs
fun build_tree (ClauseContext { ctxt, rhs, ...}) =
- Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs
+ Function_Context_Tree.mk_tree (fname, fT) h ctxt rhs
val trees = map build_tree clauses
val RCss = map find_calls trees
@@ -858,7 +858,7 @@
PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
val RCss = map (map (inst_RC (Proof_Context.theory_of lthy) fvar f)) RCss
- val trees = map (Function_Ctx_Tree.inst_tree (Proof_Context.theory_of lthy) fvar f) trees
+ val trees = map (Function_Context_Tree.inst_tree (Proof_Context.theory_of lthy) fvar f) trees
val ((R, RIntro_thmss, R_elim), lthy) =
PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy