# HG changeset patch # User wenzelm # Date 1414586558 -3600 # Node ID aab139c0003fc8248c3c55feb7e849cc4747b4ae # Parent fd3f893a40ea07644dbbca40d6f577ab54f0b7e3 modernized setup; more standard module name; diff -r fd3f893a40ea -r aab139c0003f src/HOL/Fun_Def_Base.thy --- 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 = + \Attrib.add_del Function_Context_Tree.cong_add Function_Context_Tree.cong_del\ + "declaration of congruence rule for function definitions" + ML_file "Tools/Function/sum_tree.ML" end diff -r fd3f893a40ea -r aab139c0003f src/HOL/Tools/Function/context_tree.ML --- 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 diff -r fd3f893a40ea -r aab139c0003f src/HOL/Tools/Function/function.ML --- 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 diff -r fd3f893a40ea -r aab139c0003f src/HOL/Tools/Function/function_context_tree.ML --- /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 diff -r fd3f893a40ea -r aab139c0003f src/HOL/Tools/Function/function_core.ML --- 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