# HG changeset patch # User wenzelm # Date 1460903315 -7200 # Node ID 637ed69b4d46c19a633e4d7a70aa35476a86da71 # Parent d0dfdd413a7f6a9f281574029cea29353406d8c5 prefer precise names for internal construction; diff -r d0dfdd413a7f -r 637ed69b4d46 src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Sun Apr 17 16:02:44 2016 +0200 +++ b/src/HOL/Tools/Function/function_core.ML Sun Apr 17 16:28:35 2016 +0200 @@ -469,19 +469,17 @@ ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy) end -fun define_graph Gname fvar domT ranT clauses RCss lthy = +fun define_graph (G_name, G_type) fvar clauses RCss lthy = let - val GT = domT --> ranT --> boolT - val (Gvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Gname, GT) - + val G = Free (G_name, G_type) fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs = let fun mk_h_assm (rcfix, rcassm, rcarg) = - HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg)) + HOLogic.mk_Trueprop (G $ rcarg $ (fvar $ rcarg)) |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm |> fold_rev (Logic.all o Free) rcfix in - HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs) + HOLogic.mk_Trueprop (G $ lhs $ rhs) |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs |> fold_rev (curry Logic.mk_implies) gs |> fold_rev Logic.all (fvar :: qs) @@ -489,7 +487,7 @@ val G_intros = map2 mk_GIntro clauses RCss in - inductive_def ((Binding.name n, T), NoSyn) G_intros lthy + inductive_def ((Binding.name G_name, G_type), NoSyn) G_intros lthy end fun define_function fdefname (fname, mixfix) domT ranT G default lthy = @@ -506,13 +504,10 @@ ((Binding.name (function_name fname), mixfix), (def_binding, f_def)) lthy end -fun define_recursion_relation Rname domT qglrs clauses RCss lthy = +fun define_recursion_relation (R_name, R_type) qglrs clauses RCss lthy = let - val RT = domT --> domT --> boolT - val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT) - fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) = - HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs) + HOLogic.mk_Trueprop (Free (R_name, R_type) $ rcarg $ lhs) |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm |> fold_rev (curry Logic.mk_implies) gs |> fold_rev (Logic.all o Free) rcfix @@ -522,7 +517,7 @@ val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss val ((R, RIntro_thms, R_elim, _), lthy) = - inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy + inductive_def ((Binding.name R_name, R_type), NoSyn) (flat R_intross) lthy in ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy) end @@ -855,7 +850,8 @@ val RCss = map find_calls trees val ((G, GIntro_thms, G_elim, G_induct), lthy) = - PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy + PROFILE "def_graph" + (define_graph (graph_name defname, domT --> ranT --> boolT) fvar clauses RCss) lthy val ((f, (_, f_defthm)), lthy) = PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy @@ -864,7 +860,9 @@ val trees = map (Function_Context_Tree.inst_tree 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 + PROFILE "def_rel" + (define_recursion_relation (rel_name defname, domT --> domT --> boolT) + abstract_qglrs clauses RCss) lthy val dom = mk_acc domT R val (_, lthy) =