moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
authorblanchet
Mon Jan 20 21:32:41 2014 +0100 (2014-01-20)
changeset 550850e8e4dc55866
parent 55084 8ee9aabb2bca
child 55086 500ef036117b
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
src/HOL/BNF_Def.thy
src/HOL/Divides.thy
src/HOL/FunDef.thy
src/HOL/Fun_Def.thy
src/HOL/Fun_Def_Base.thy
src/HOL/Int.thy
src/HOL/Lifting_Product.thy
src/HOL/Partial_Function.thy
src/HOL/Set_Interval.thy
src/HOL/Tools/Function/context_tree.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/function_core.ML
     1.1 --- a/src/HOL/BNF_Def.thy	Mon Jan 20 20:42:43 2014 +0100
     1.2 +++ b/src/HOL/BNF_Def.thy	Mon Jan 20 21:32:41 2014 +0100
     1.3 @@ -8,9 +8,7 @@
     1.4  header {* Definition of Bounded Natural Functors *}
     1.5  
     1.6  theory BNF_Def
     1.7 -imports BNF_Util
     1.8 -   (*FIXME: register fundef_cong attribute in an interpretation to remove this dependency*)
     1.9 -  FunDef
    1.10 +imports BNF_Util Fun_Def_Base
    1.11  keywords
    1.12    "print_bnfs" :: diag and
    1.13    "bnf" :: thy_goal
     2.1 --- a/src/HOL/Divides.thy	Mon Jan 20 20:42:43 2014 +0100
     2.2 +++ b/src/HOL/Divides.thy	Mon Jan 20 21:32:41 2014 +0100
     2.3 @@ -1062,10 +1062,10 @@
     2.4     \<Longrightarrow> divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
     2.5  by (auto simp add: mult_ac divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
     2.6  
     2.7 -lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
     2.8 +lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
     2.9  by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
    2.10  
    2.11 -lemma mod_mult2_eq: "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"
    2.12 +lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
    2.13  by (auto simp add: mult_commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])
    2.14  
    2.15  
    2.16 @@ -2136,7 +2136,7 @@
    2.17    using mod_div_equality [of m n] by arith
    2.18  
    2.19  
    2.20 -subsubsection {* Proving  @{term "a div (b*c) = (a div b) div c"} *}
    2.21 +subsubsection {* Proving  @{term "a div (b * c) = (a div b) div c"} *}
    2.22  
    2.23  (*The condition c>0 seems necessary.  Consider that 7 div ~6 = ~2 but
    2.24    7 div 2 div ~3 = 3 div ~3 = ~1.  The subcase (a div b) mod c = 0 seems
    2.25 @@ -2144,7 +2144,7 @@
    2.26  
    2.27  text{*first, four lemmas to bound the remainder for the cases b<0 and b>0 *}
    2.28  
    2.29 -lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r \<le> 0 |] ==> b*c < b*(q mod c) + r"
    2.30 +lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r \<le> 0 |] ==> b * c < b * (q mod c) + r"
    2.31  apply (subgoal_tac "b * (c - q mod c) < r * 1")
    2.32   apply (simp add: algebra_simps)
    2.33  apply (rule order_le_less_trans)
     3.1 --- a/src/HOL/FunDef.thy	Mon Jan 20 20:42:43 2014 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,321 +0,0 @@
     3.4 -(*  Title:      HOL/FunDef.thy
     3.5 -    Author:     Alexander Krauss, TU Muenchen
     3.6 -*)
     3.7 -
     3.8 -header {* Function Definitions and Termination Proofs *}
     3.9 -
    3.10 -theory FunDef
    3.11 -imports Partial_Function SAT Wellfounded
    3.12 -keywords "function" "termination" :: thy_goal and "fun" "fun_cases" :: thy_decl
    3.13 -begin
    3.14 -
    3.15 -subsection {* Definitions with default value. *}
    3.16 -
    3.17 -definition
    3.18 -  THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
    3.19 -  "THE_default d P = (if (\<exists>!x. P x) then (THE x. P x) else d)"
    3.20 -
    3.21 -lemma THE_defaultI': "\<exists>!x. P x \<Longrightarrow> P (THE_default d P)"
    3.22 -  by (simp add: theI' THE_default_def)
    3.23 -
    3.24 -lemma THE_default1_equality:
    3.25 -    "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> THE_default d P = a"
    3.26 -  by (simp add: the1_equality THE_default_def)
    3.27 -
    3.28 -lemma THE_default_none:
    3.29 -    "\<not>(\<exists>!x. P x) \<Longrightarrow> THE_default d P = d"
    3.30 -  by (simp add:THE_default_def)
    3.31 -
    3.32 -
    3.33 -lemma fundef_ex1_existence:
    3.34 -  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
    3.35 -  assumes ex1: "\<exists>!y. G x y"
    3.36 -  shows "G x (f x)"
    3.37 -  apply (simp only: f_def)
    3.38 -  apply (rule THE_defaultI')
    3.39 -  apply (rule ex1)
    3.40 -  done
    3.41 -
    3.42 -lemma fundef_ex1_uniqueness:
    3.43 -  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
    3.44 -  assumes ex1: "\<exists>!y. G x y"
    3.45 -  assumes elm: "G x (h x)"
    3.46 -  shows "h x = f x"
    3.47 -  apply (simp only: f_def)
    3.48 -  apply (rule THE_default1_equality [symmetric])
    3.49 -   apply (rule ex1)
    3.50 -  apply (rule elm)
    3.51 -  done
    3.52 -
    3.53 -lemma fundef_ex1_iff:
    3.54 -  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
    3.55 -  assumes ex1: "\<exists>!y. G x y"
    3.56 -  shows "(G x y) = (f x = y)"
    3.57 -  apply (auto simp:ex1 f_def THE_default1_equality)
    3.58 -  apply (rule THE_defaultI')
    3.59 -  apply (rule ex1)
    3.60 -  done
    3.61 -
    3.62 -lemma fundef_default_value:
    3.63 -  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
    3.64 -  assumes graph: "\<And>x y. G x y \<Longrightarrow> D x"
    3.65 -  assumes "\<not> D x"
    3.66 -  shows "f x = d x"
    3.67 -proof -
    3.68 -  have "\<not>(\<exists>y. G x y)"
    3.69 -  proof
    3.70 -    assume "\<exists>y. G x y"
    3.71 -    hence "D x" using graph ..
    3.72 -    with `\<not> D x` show False ..
    3.73 -  qed
    3.74 -  hence "\<not>(\<exists>!y. G x y)" by blast
    3.75 -
    3.76 -  thus ?thesis
    3.77 -    unfolding f_def
    3.78 -    by (rule THE_default_none)
    3.79 -qed
    3.80 -
    3.81 -definition in_rel_def[simp]:
    3.82 -  "in_rel R x y == (x, y) \<in> R"
    3.83 -
    3.84 -lemma wf_in_rel:
    3.85 -  "wf R \<Longrightarrow> wfP (in_rel R)"
    3.86 -  by (simp add: wfP_def)
    3.87 -
    3.88 -ML_file "Tools/Function/function_common.ML"
    3.89 -ML_file "Tools/Function/context_tree.ML"
    3.90 -ML_file "Tools/Function/function_core.ML"
    3.91 -ML_file "Tools/Function/sum_tree.ML"
    3.92 -ML_file "Tools/Function/mutual.ML"
    3.93 -ML_file "Tools/Function/pattern_split.ML"
    3.94 -ML_file "Tools/Function/relation.ML"
    3.95 -ML_file "Tools/Function/function_elims.ML"
    3.96 -
    3.97 -method_setup relation = {*
    3.98 -  Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t))
    3.99 -*} "prove termination using a user-specified wellfounded relation"
   3.100 -
   3.101 -ML_file "Tools/Function/function.ML"
   3.102 -ML_file "Tools/Function/pat_completeness.ML"
   3.103 -
   3.104 -method_setup pat_completeness = {*
   3.105 -  Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
   3.106 -*} "prove completeness of datatype patterns"
   3.107 -
   3.108 -ML_file "Tools/Function/fun.ML"
   3.109 -ML_file "Tools/Function/induction_schema.ML"
   3.110 -
   3.111 -method_setup induction_schema = {*
   3.112 -  Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
   3.113 -*} "prove an induction principle"
   3.114 -
   3.115 -setup {*
   3.116 -  Function.setup
   3.117 -  #> Function_Fun.setup
   3.118 -*}
   3.119 -
   3.120 -subsection {* Measure Functions *}
   3.121 -
   3.122 -inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
   3.123 -where is_measure_trivial: "is_measure f"
   3.124 -
   3.125 -ML_file "Tools/Function/measure_functions.ML"
   3.126 -setup MeasureFunctions.setup
   3.127 -
   3.128 -lemma measure_size[measure_function]: "is_measure size"
   3.129 -by (rule is_measure_trivial)
   3.130 -
   3.131 -lemma measure_fst[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))"
   3.132 -by (rule is_measure_trivial)
   3.133 -lemma measure_snd[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
   3.134 -by (rule is_measure_trivial)
   3.135 -
   3.136 -ML_file "Tools/Function/lexicographic_order.ML"
   3.137 -
   3.138 -method_setup lexicographic_order = {*
   3.139 -  Method.sections clasimp_modifiers >>
   3.140 -  (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))
   3.141 -*} "termination prover for lexicographic orderings"
   3.142 -
   3.143 -setup Lexicographic_Order.setup
   3.144 -
   3.145 -
   3.146 -subsection {* Congruence Rules *}
   3.147 -
   3.148 -lemma let_cong [fundef_cong]:
   3.149 -  "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
   3.150 -  unfolding Let_def by blast
   3.151 -
   3.152 -lemmas [fundef_cong] =
   3.153 -  if_cong image_cong INT_cong UN_cong
   3.154 -  bex_cong ball_cong imp_cong Option.map_cong Option.bind_cong
   3.155 -
   3.156 -lemma split_cong [fundef_cong]:
   3.157 -  "(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q
   3.158 -    \<Longrightarrow> split f p = split g q"
   3.159 -  by (auto simp: split_def)
   3.160 -
   3.161 -lemma comp_cong [fundef_cong]:
   3.162 -  "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
   3.163 -  unfolding o_apply .
   3.164 -
   3.165 -subsection {* Simp rules for termination proofs *}
   3.166 -
   3.167 -lemma termination_basic_simps[termination_simp]:
   3.168 -  "x < (y::nat) \<Longrightarrow> x < y + z"
   3.169 -  "x < z \<Longrightarrow> x < y + z"
   3.170 -  "x \<le> y \<Longrightarrow> x \<le> y + (z::nat)"
   3.171 -  "x \<le> z \<Longrightarrow> x \<le> y + (z::nat)"
   3.172 -  "x < y \<Longrightarrow> x \<le> (y::nat)"
   3.173 -by arith+
   3.174 -
   3.175 -declare le_imp_less_Suc[termination_simp]
   3.176 -
   3.177 -lemma prod_size_simp[termination_simp]:
   3.178 -  "prod_size f g p = f (fst p) + g (snd p) + Suc 0"
   3.179 -by (induct p) auto
   3.180 -
   3.181 -subsection {* Decomposition *}
   3.182 -
   3.183 -lemma less_by_empty:
   3.184 -  "A = {} \<Longrightarrow> A \<subseteq> B"
   3.185 -and  union_comp_emptyL:
   3.186 -  "\<lbrakk> A O C = {}; B O C = {} \<rbrakk> \<Longrightarrow> (A \<union> B) O C = {}"
   3.187 -and union_comp_emptyR:
   3.188 -  "\<lbrakk> A O B = {}; A O C = {} \<rbrakk> \<Longrightarrow> A O (B \<union> C) = {}"
   3.189 -and wf_no_loop:
   3.190 -  "R O R = {} \<Longrightarrow> wf R"
   3.191 -by (auto simp add: wf_comp_self[of R])
   3.192 -
   3.193 -
   3.194 -subsection {* Reduction Pairs *}
   3.195 -
   3.196 -definition
   3.197 -  "reduction_pair P = (wf (fst P) \<and> fst P O snd P \<subseteq> fst P)"
   3.198 -
   3.199 -lemma reduction_pairI[intro]: "wf R \<Longrightarrow> R O S \<subseteq> R \<Longrightarrow> reduction_pair (R, S)"
   3.200 -unfolding reduction_pair_def by auto
   3.201 -
   3.202 -lemma reduction_pair_lemma:
   3.203 -  assumes rp: "reduction_pair P"
   3.204 -  assumes "R \<subseteq> fst P"
   3.205 -  assumes "S \<subseteq> snd P"
   3.206 -  assumes "wf S"
   3.207 -  shows "wf (R \<union> S)"
   3.208 -proof -
   3.209 -  from rp `S \<subseteq> snd P` have "wf (fst P)" "fst P O S \<subseteq> fst P"
   3.210 -    unfolding reduction_pair_def by auto
   3.211 -  with `wf S` have "wf (fst P \<union> S)"
   3.212 -    by (auto intro: wf_union_compatible)
   3.213 -  moreover from `R \<subseteq> fst P` have "R \<union> S \<subseteq> fst P \<union> S" by auto
   3.214 -  ultimately show ?thesis by (rule wf_subset)
   3.215 -qed
   3.216 -
   3.217 -definition
   3.218 -  "rp_inv_image = (\<lambda>(R,S) f. (inv_image R f, inv_image S f))"
   3.219 -
   3.220 -lemma rp_inv_image_rp:
   3.221 -  "reduction_pair P \<Longrightarrow> reduction_pair (rp_inv_image P f)"
   3.222 -  unfolding reduction_pair_def rp_inv_image_def split_def
   3.223 -  by force
   3.224 -
   3.225 -
   3.226 -subsection {* Concrete orders for SCNP termination proofs *}
   3.227 -
   3.228 -definition "pair_less = less_than <*lex*> less_than"
   3.229 -definition "pair_leq = pair_less^="
   3.230 -definition "max_strict = max_ext pair_less"
   3.231 -definition "max_weak = max_ext pair_leq \<union> {({}, {})}"
   3.232 -definition "min_strict = min_ext pair_less"
   3.233 -definition "min_weak = min_ext pair_leq \<union> {({}, {})}"
   3.234 -
   3.235 -lemma wf_pair_less[simp]: "wf pair_less"
   3.236 -  by (auto simp: pair_less_def)
   3.237 -
   3.238 -text {* Introduction rules for @{text pair_less}/@{text pair_leq} *}
   3.239 -lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
   3.240 -  and pair_leqI2: "a \<le> b \<Longrightarrow> s \<le> t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
   3.241 -  and pair_lessI1: "a < b  \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
   3.242 -  and pair_lessI2: "a \<le> b \<Longrightarrow> s < t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
   3.243 -  unfolding pair_leq_def pair_less_def by auto
   3.244 -
   3.245 -text {* Introduction rules for max *}
   3.246 -lemma smax_emptyI:
   3.247 -  "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict"
   3.248 -  and smax_insertI:
   3.249 -  "\<lbrakk>y \<in> Y; (x, y) \<in> pair_less; (X, Y) \<in> max_strict\<rbrakk> \<Longrightarrow> (insert x X, Y) \<in> max_strict"
   3.250 -  and wmax_emptyI:
   3.251 -  "finite X \<Longrightarrow> ({}, X) \<in> max_weak"
   3.252 -  and wmax_insertI:
   3.253 -  "\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak"
   3.254 -unfolding max_strict_def max_weak_def by (auto elim!: max_ext.cases)
   3.255 -
   3.256 -text {* Introduction rules for min *}
   3.257 -lemma smin_emptyI:
   3.258 -  "X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict"
   3.259 -  and smin_insertI:
   3.260 -  "\<lbrakk>x \<in> XS; (x, y) \<in> pair_less; (XS, YS) \<in> min_strict\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_strict"
   3.261 -  and wmin_emptyI:
   3.262 -  "(X, {}) \<in> min_weak"
   3.263 -  and wmin_insertI:
   3.264 -  "\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak"
   3.265 -by (auto simp: min_strict_def min_weak_def min_ext_def)
   3.266 -
   3.267 -text {* Reduction Pairs *}
   3.268 -
   3.269 -lemma max_ext_compat:
   3.270 -  assumes "R O S \<subseteq> R"
   3.271 -  shows "max_ext R O (max_ext S \<union> {({},{})}) \<subseteq> max_ext R"
   3.272 -using assms
   3.273 -apply auto
   3.274 -apply (elim max_ext.cases)
   3.275 -apply rule
   3.276 -apply auto[3]
   3.277 -apply (drule_tac x=xa in meta_spec)
   3.278 -apply simp
   3.279 -apply (erule bexE)
   3.280 -apply (drule_tac x=xb in meta_spec)
   3.281 -by auto
   3.282 -
   3.283 -lemma max_rpair_set: "reduction_pair (max_strict, max_weak)"
   3.284 -  unfolding max_strict_def max_weak_def
   3.285 -apply (intro reduction_pairI max_ext_wf)
   3.286 -apply simp
   3.287 -apply (rule max_ext_compat)
   3.288 -by (auto simp: pair_less_def pair_leq_def)
   3.289 -
   3.290 -lemma min_ext_compat:
   3.291 -  assumes "R O S \<subseteq> R"
   3.292 -  shows "min_ext R O  (min_ext S \<union> {({},{})}) \<subseteq> min_ext R"
   3.293 -using assms
   3.294 -apply (auto simp: min_ext_def)
   3.295 -apply (drule_tac x=ya in bspec, assumption)
   3.296 -apply (erule bexE)
   3.297 -apply (drule_tac x=xc in bspec)
   3.298 -apply assumption
   3.299 -by auto
   3.300 -
   3.301 -lemma min_rpair_set: "reduction_pair (min_strict, min_weak)"
   3.302 -  unfolding min_strict_def min_weak_def
   3.303 -apply (intro reduction_pairI min_ext_wf)
   3.304 -apply simp
   3.305 -apply (rule min_ext_compat)
   3.306 -by (auto simp: pair_less_def pair_leq_def)
   3.307 -
   3.308 -
   3.309 -subsection {* Tool setup *}
   3.310 -
   3.311 -ML_file "Tools/Function/termination.ML"
   3.312 -ML_file "Tools/Function/scnp_solve.ML"
   3.313 -ML_file "Tools/Function/scnp_reconstruct.ML"
   3.314 -ML_file "Tools/Function/fun_cases.ML"
   3.315 -
   3.316 -setup ScnpReconstruct.setup
   3.317 -
   3.318 -ML_val -- "setup inactive"
   3.319 -{*
   3.320 -  Context.theory_map (Function_Common.set_termination_prover
   3.321 -    (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))
   3.322 -*}
   3.323 -
   3.324 -end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Fun_Def.thy	Mon Jan 20 21:32:41 2014 +0100
     4.3 @@ -0,0 +1,319 @@
     4.4 +(*  Title:      HOL/Fun_Def.thy
     4.5 +    Author:     Alexander Krauss, TU Muenchen
     4.6 +*)
     4.7 +
     4.8 +header {* Function Definitions and Termination Proofs *}
     4.9 +
    4.10 +theory Fun_Def
    4.11 +imports Partial_Function SAT
    4.12 +keywords "function" "termination" :: thy_goal and "fun" "fun_cases" :: thy_decl
    4.13 +begin
    4.14 +
    4.15 +subsection {* Definitions with default value *}
    4.16 +
    4.17 +definition
    4.18 +  THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
    4.19 +  "THE_default d P = (if (\<exists>!x. P x) then (THE x. P x) else d)"
    4.20 +
    4.21 +lemma THE_defaultI': "\<exists>!x. P x \<Longrightarrow> P (THE_default d P)"
    4.22 +  by (simp add: theI' THE_default_def)
    4.23 +
    4.24 +lemma THE_default1_equality:
    4.25 +    "\<lbrakk>\<exists>!x. P x; P a\<rbrakk> \<Longrightarrow> THE_default d P = a"
    4.26 +  by (simp add: the1_equality THE_default_def)
    4.27 +
    4.28 +lemma THE_default_none:
    4.29 +    "\<not>(\<exists>!x. P x) \<Longrightarrow> THE_default d P = d"
    4.30 +  by (simp add:THE_default_def)
    4.31 +
    4.32 +
    4.33 +lemma fundef_ex1_existence:
    4.34 +  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
    4.35 +  assumes ex1: "\<exists>!y. G x y"
    4.36 +  shows "G x (f x)"
    4.37 +  apply (simp only: f_def)
    4.38 +  apply (rule THE_defaultI')
    4.39 +  apply (rule ex1)
    4.40 +  done
    4.41 +
    4.42 +lemma fundef_ex1_uniqueness:
    4.43 +  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
    4.44 +  assumes ex1: "\<exists>!y. G x y"
    4.45 +  assumes elm: "G x (h x)"
    4.46 +  shows "h x = f x"
    4.47 +  apply (simp only: f_def)
    4.48 +  apply (rule THE_default1_equality [symmetric])
    4.49 +   apply (rule ex1)
    4.50 +  apply (rule elm)
    4.51 +  done
    4.52 +
    4.53 +lemma fundef_ex1_iff:
    4.54 +  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
    4.55 +  assumes ex1: "\<exists>!y. G x y"
    4.56 +  shows "(G x y) = (f x = y)"
    4.57 +  apply (auto simp:ex1 f_def THE_default1_equality)
    4.58 +  apply (rule THE_defaultI')
    4.59 +  apply (rule ex1)
    4.60 +  done
    4.61 +
    4.62 +lemma fundef_default_value:
    4.63 +  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
    4.64 +  assumes graph: "\<And>x y. G x y \<Longrightarrow> D x"
    4.65 +  assumes "\<not> D x"
    4.66 +  shows "f x = d x"
    4.67 +proof -
    4.68 +  have "\<not>(\<exists>y. G x y)"
    4.69 +  proof
    4.70 +    assume "\<exists>y. G x y"
    4.71 +    hence "D x" using graph ..
    4.72 +    with `\<not> D x` show False ..
    4.73 +  qed
    4.74 +  hence "\<not>(\<exists>!y. G x y)" by blast
    4.75 +
    4.76 +  thus ?thesis
    4.77 +    unfolding f_def
    4.78 +    by (rule THE_default_none)
    4.79 +qed
    4.80 +
    4.81 +definition in_rel_def[simp]:
    4.82 +  "in_rel R x y == (x, y) \<in> R"
    4.83 +
    4.84 +lemma wf_in_rel:
    4.85 +  "wf R \<Longrightarrow> wfP (in_rel R)"
    4.86 +  by (simp add: wfP_def)
    4.87 +
    4.88 +ML_file "Tools/Function/function_core.ML"
    4.89 +ML_file "Tools/Function/sum_tree.ML"
    4.90 +ML_file "Tools/Function/mutual.ML"
    4.91 +ML_file "Tools/Function/pattern_split.ML"
    4.92 +ML_file "Tools/Function/relation.ML"
    4.93 +ML_file "Tools/Function/function_elims.ML"
    4.94 +
    4.95 +method_setup relation = {*
    4.96 +  Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t))
    4.97 +*} "prove termination using a user-specified wellfounded relation"
    4.98 +
    4.99 +ML_file "Tools/Function/function.ML"
   4.100 +ML_file "Tools/Function/pat_completeness.ML"
   4.101 +
   4.102 +method_setup pat_completeness = {*
   4.103 +  Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
   4.104 +*} "prove completeness of datatype patterns"
   4.105 +
   4.106 +ML_file "Tools/Function/fun.ML"
   4.107 +ML_file "Tools/Function/induction_schema.ML"
   4.108 +
   4.109 +method_setup induction_schema = {*
   4.110 +  Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
   4.111 +*} "prove an induction principle"
   4.112 +
   4.113 +setup {*
   4.114 +  Function.setup
   4.115 +  #> Function_Fun.setup
   4.116 +*}
   4.117 +
   4.118 +subsection {* Measure Functions *}
   4.119 +
   4.120 +inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
   4.121 +where is_measure_trivial: "is_measure f"
   4.122 +
   4.123 +ML_file "Tools/Function/measure_functions.ML"
   4.124 +setup MeasureFunctions.setup
   4.125 +
   4.126 +lemma measure_size[measure_function]: "is_measure size"
   4.127 +by (rule is_measure_trivial)
   4.128 +
   4.129 +lemma measure_fst[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))"
   4.130 +by (rule is_measure_trivial)
   4.131 +lemma measure_snd[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
   4.132 +by (rule is_measure_trivial)
   4.133 +
   4.134 +ML_file "Tools/Function/lexicographic_order.ML"
   4.135 +
   4.136 +method_setup lexicographic_order = {*
   4.137 +  Method.sections clasimp_modifiers >>
   4.138 +  (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))
   4.139 +*} "termination prover for lexicographic orderings"
   4.140 +
   4.141 +setup Lexicographic_Order.setup
   4.142 +
   4.143 +
   4.144 +subsection {* Congruence Rules *}
   4.145 +
   4.146 +lemma let_cong [fundef_cong]:
   4.147 +  "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
   4.148 +  unfolding Let_def by blast
   4.149 +
   4.150 +lemmas [fundef_cong] =
   4.151 +  if_cong image_cong INT_cong UN_cong
   4.152 +  bex_cong ball_cong imp_cong Option.map_cong Option.bind_cong
   4.153 +
   4.154 +lemma split_cong [fundef_cong]:
   4.155 +  "(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q
   4.156 +    \<Longrightarrow> split f p = split g q"
   4.157 +  by (auto simp: split_def)
   4.158 +
   4.159 +lemma comp_cong [fundef_cong]:
   4.160 +  "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
   4.161 +  unfolding o_apply .
   4.162 +
   4.163 +subsection {* Simp rules for termination proofs *}
   4.164 +
   4.165 +lemma termination_basic_simps[termination_simp]:
   4.166 +  "x < (y::nat) \<Longrightarrow> x < y + z"
   4.167 +  "x < z \<Longrightarrow> x < y + z"
   4.168 +  "x \<le> y \<Longrightarrow> x \<le> y + (z::nat)"
   4.169 +  "x \<le> z \<Longrightarrow> x \<le> y + (z::nat)"
   4.170 +  "x < y \<Longrightarrow> x \<le> (y::nat)"
   4.171 +by arith+
   4.172 +
   4.173 +declare le_imp_less_Suc[termination_simp]
   4.174 +
   4.175 +lemma prod_size_simp[termination_simp]:
   4.176 +  "prod_size f g p = f (fst p) + g (snd p) + Suc 0"
   4.177 +by (induct p) auto
   4.178 +
   4.179 +subsection {* Decomposition *}
   4.180 +
   4.181 +lemma less_by_empty:
   4.182 +  "A = {} \<Longrightarrow> A \<subseteq> B"
   4.183 +and  union_comp_emptyL:
   4.184 +  "\<lbrakk> A O C = {}; B O C = {} \<rbrakk> \<Longrightarrow> (A \<union> B) O C = {}"
   4.185 +and union_comp_emptyR:
   4.186 +  "\<lbrakk> A O B = {}; A O C = {} \<rbrakk> \<Longrightarrow> A O (B \<union> C) = {}"
   4.187 +and wf_no_loop:
   4.188 +  "R O R = {} \<Longrightarrow> wf R"
   4.189 +by (auto simp add: wf_comp_self[of R])
   4.190 +
   4.191 +
   4.192 +subsection {* Reduction Pairs *}
   4.193 +
   4.194 +definition
   4.195 +  "reduction_pair P = (wf (fst P) \<and> fst P O snd P \<subseteq> fst P)"
   4.196 +
   4.197 +lemma reduction_pairI[intro]: "wf R \<Longrightarrow> R O S \<subseteq> R \<Longrightarrow> reduction_pair (R, S)"
   4.198 +unfolding reduction_pair_def by auto
   4.199 +
   4.200 +lemma reduction_pair_lemma:
   4.201 +  assumes rp: "reduction_pair P"
   4.202 +  assumes "R \<subseteq> fst P"
   4.203 +  assumes "S \<subseteq> snd P"
   4.204 +  assumes "wf S"
   4.205 +  shows "wf (R \<union> S)"
   4.206 +proof -
   4.207 +  from rp `S \<subseteq> snd P` have "wf (fst P)" "fst P O S \<subseteq> fst P"
   4.208 +    unfolding reduction_pair_def by auto
   4.209 +  with `wf S` have "wf (fst P \<union> S)"
   4.210 +    by (auto intro: wf_union_compatible)
   4.211 +  moreover from `R \<subseteq> fst P` have "R \<union> S \<subseteq> fst P \<union> S" by auto
   4.212 +  ultimately show ?thesis by (rule wf_subset)
   4.213 +qed
   4.214 +
   4.215 +definition
   4.216 +  "rp_inv_image = (\<lambda>(R,S) f. (inv_image R f, inv_image S f))"
   4.217 +
   4.218 +lemma rp_inv_image_rp:
   4.219 +  "reduction_pair P \<Longrightarrow> reduction_pair (rp_inv_image P f)"
   4.220 +  unfolding reduction_pair_def rp_inv_image_def split_def
   4.221 +  by force
   4.222 +
   4.223 +
   4.224 +subsection {* Concrete orders for SCNP termination proofs *}
   4.225 +
   4.226 +definition "pair_less = less_than <*lex*> less_than"
   4.227 +definition "pair_leq = pair_less^="
   4.228 +definition "max_strict = max_ext pair_less"
   4.229 +definition "max_weak = max_ext pair_leq \<union> {({}, {})}"
   4.230 +definition "min_strict = min_ext pair_less"
   4.231 +definition "min_weak = min_ext pair_leq \<union> {({}, {})}"
   4.232 +
   4.233 +lemma wf_pair_less[simp]: "wf pair_less"
   4.234 +  by (auto simp: pair_less_def)
   4.235 +
   4.236 +text {* Introduction rules for @{text pair_less}/@{text pair_leq} *}
   4.237 +lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
   4.238 +  and pair_leqI2: "a \<le> b \<Longrightarrow> s \<le> t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
   4.239 +  and pair_lessI1: "a < b  \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
   4.240 +  and pair_lessI2: "a \<le> b \<Longrightarrow> s < t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
   4.241 +  unfolding pair_leq_def pair_less_def by auto
   4.242 +
   4.243 +text {* Introduction rules for max *}
   4.244 +lemma smax_emptyI:
   4.245 +  "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict"
   4.246 +  and smax_insertI:
   4.247 +  "\<lbrakk>y \<in> Y; (x, y) \<in> pair_less; (X, Y) \<in> max_strict\<rbrakk> \<Longrightarrow> (insert x X, Y) \<in> max_strict"
   4.248 +  and wmax_emptyI:
   4.249 +  "finite X \<Longrightarrow> ({}, X) \<in> max_weak"
   4.250 +  and wmax_insertI:
   4.251 +  "\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak"
   4.252 +unfolding max_strict_def max_weak_def by (auto elim!: max_ext.cases)
   4.253 +
   4.254 +text {* Introduction rules for min *}
   4.255 +lemma smin_emptyI:
   4.256 +  "X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict"
   4.257 +  and smin_insertI:
   4.258 +  "\<lbrakk>x \<in> XS; (x, y) \<in> pair_less; (XS, YS) \<in> min_strict\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_strict"
   4.259 +  and wmin_emptyI:
   4.260 +  "(X, {}) \<in> min_weak"
   4.261 +  and wmin_insertI:
   4.262 +  "\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak"
   4.263 +by (auto simp: min_strict_def min_weak_def min_ext_def)
   4.264 +
   4.265 +text {* Reduction Pairs *}
   4.266 +
   4.267 +lemma max_ext_compat:
   4.268 +  assumes "R O S \<subseteq> R"
   4.269 +  shows "max_ext R O (max_ext S \<union> {({},{})}) \<subseteq> max_ext R"
   4.270 +using assms
   4.271 +apply auto
   4.272 +apply (elim max_ext.cases)
   4.273 +apply rule
   4.274 +apply auto[3]
   4.275 +apply (drule_tac x=xa in meta_spec)
   4.276 +apply simp
   4.277 +apply (erule bexE)
   4.278 +apply (drule_tac x=xb in meta_spec)
   4.279 +by auto
   4.280 +
   4.281 +lemma max_rpair_set: "reduction_pair (max_strict, max_weak)"
   4.282 +  unfolding max_strict_def max_weak_def
   4.283 +apply (intro reduction_pairI max_ext_wf)
   4.284 +apply simp
   4.285 +apply (rule max_ext_compat)
   4.286 +by (auto simp: pair_less_def pair_leq_def)
   4.287 +
   4.288 +lemma min_ext_compat:
   4.289 +  assumes "R O S \<subseteq> R"
   4.290 +  shows "min_ext R O  (min_ext S \<union> {({},{})}) \<subseteq> min_ext R"
   4.291 +using assms
   4.292 +apply (auto simp: min_ext_def)
   4.293 +apply (drule_tac x=ya in bspec, assumption)
   4.294 +apply (erule bexE)
   4.295 +apply (drule_tac x=xc in bspec)
   4.296 +apply assumption
   4.297 +by auto
   4.298 +
   4.299 +lemma min_rpair_set: "reduction_pair (min_strict, min_weak)"
   4.300 +  unfolding min_strict_def min_weak_def
   4.301 +apply (intro reduction_pairI min_ext_wf)
   4.302 +apply simp
   4.303 +apply (rule min_ext_compat)
   4.304 +by (auto simp: pair_less_def pair_leq_def)
   4.305 +
   4.306 +
   4.307 +subsection {* Tool setup *}
   4.308 +
   4.309 +ML_file "Tools/Function/termination.ML"
   4.310 +ML_file "Tools/Function/scnp_solve.ML"
   4.311 +ML_file "Tools/Function/scnp_reconstruct.ML"
   4.312 +ML_file "Tools/Function/fun_cases.ML"
   4.313 +
   4.314 +setup ScnpReconstruct.setup
   4.315 +
   4.316 +ML_val -- "setup inactive"
   4.317 +{*
   4.318 +  Context.theory_map (Function_Common.set_termination_prover
   4.319 +    (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))
   4.320 +*}
   4.321 +
   4.322 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Fun_Def_Base.thy	Mon Jan 20 21:32:41 2014 +0100
     5.3 @@ -0,0 +1,16 @@
     5.4 +(*  Title:      HOL/Fun_Def_Base.thy
     5.5 +    Author:     Alexander Krauss, TU Muenchen
     5.6 +*)
     5.7 +
     5.8 +header {* Function Definition Base *}
     5.9 +
    5.10 +theory Fun_Def_Base
    5.11 +imports Ctr_Sugar Set Wellfounded
    5.12 +begin
    5.13 +
    5.14 +ML_file "Tools/Function/function_lib.ML"
    5.15 +ML_file "Tools/Function/function_common.ML"
    5.16 +ML_file "Tools/Function/context_tree.ML"
    5.17 +setup Function_Ctx_Tree.setup
    5.18 +
    5.19 +end
     6.1 --- a/src/HOL/Int.thy	Mon Jan 20 20:42:43 2014 +0100
     6.2 +++ b/src/HOL/Int.thy	Mon Jan 20 21:32:41 2014 +0100
     6.3 @@ -6,7 +6,7 @@
     6.4  header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
     6.5  
     6.6  theory Int
     6.7 -imports Equiv_Relations Wellfounded Quotient FunDef
     6.8 +imports Equiv_Relations Wellfounded Quotient Fun_Def
     6.9  begin
    6.10  
    6.11  subsection {* Definition of integers as a quotient type *}
     7.1 --- a/src/HOL/Lifting_Product.thy	Mon Jan 20 20:42:43 2014 +0100
     7.2 +++ b/src/HOL/Lifting_Product.thy	Mon Jan 20 21:32:41 2014 +0100
     7.3 @@ -17,15 +17,8 @@
     7.4    "prod_pred P1 P2 (a, b) \<longleftrightarrow> P1 a \<and> P2 b"
     7.5    by (simp add: prod_pred_def)
     7.6  
     7.7 -lemma prod_rel_eq [relator_eq]:
     7.8 -  shows "prod_rel (op =) (op =) = (op =)"
     7.9 -  by (simp add: fun_eq_iff)
    7.10 -
    7.11 -lemma prod_rel_mono[relator_mono]:
    7.12 -  assumes "A \<le> C"
    7.13 -  assumes "B \<le> D"
    7.14 -  shows "(prod_rel A B) \<le> (prod_rel C D)"
    7.15 -using assms by (auto simp: prod_rel_def)
    7.16 +lemmas prod_rel_eq[relator_eq] = prod.rel_eq
    7.17 +lemmas prod_rel_mono[relator_mono] = prod.rel_mono
    7.18  
    7.19  lemma prod_rel_OO[relator_distr]:
    7.20    "(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)"
     8.1 --- a/src/HOL/Partial_Function.thy	Mon Jan 20 20:42:43 2014 +0100
     8.2 +++ b/src/HOL/Partial_Function.thy	Mon Jan 20 21:32:41 2014 +0100
     8.3 @@ -5,11 +5,10 @@
     8.4  header {* Partial Function Definitions *}
     8.5  
     8.6  theory Partial_Function
     8.7 -imports Complete_Partial_Order Option
     8.8 +imports Complete_Partial_Order Fun_Def_Base Option
     8.9  keywords "partial_function" :: thy_decl
    8.10  begin
    8.11  
    8.12 -ML_file "Tools/Function/function_lib.ML"
    8.13  ML_file "Tools/Function/partial_function.ML"
    8.14  setup Partial_Function.setup
    8.15  
     9.1 --- a/src/HOL/Set_Interval.thy	Mon Jan 20 20:42:43 2014 +0100
     9.2 +++ b/src/HOL/Set_Interval.thy	Mon Jan 20 21:32:41 2014 +0100
     9.3 @@ -827,8 +827,8 @@
     9.4  subset is exactly that interval. *}
     9.5  
     9.6  lemma subset_card_intvl_is_intvl:
     9.7 -  assumes "A \<subseteq> {k..<k+card A}"
     9.8 -  shows "A = {k..<k+card A}"
     9.9 +  assumes "A \<subseteq> {k..<k + card A}"
    9.10 +  shows "A = {k..<k + card A}"
    9.11  proof (cases "finite A")
    9.12    case True
    9.13    from this and assms show ?thesis
    9.14 @@ -837,7 +837,7 @@
    9.15    next
    9.16      case (insert b A)
    9.17      hence *: "b \<notin> A" by auto
    9.18 -    with insert have "A <= {k..<k+card A}" and "b = k+card A"
    9.19 +    with insert have "A <= {k..<k + card A}" and "b = k + card A"
    9.20        by fastforce+
    9.21      with insert * show ?case by auto
    9.22    qed
    10.1 --- a/src/HOL/Tools/Function/context_tree.ML	Mon Jan 20 20:42:43 2014 +0100
    10.2 +++ b/src/HOL/Tools/Function/context_tree.ML	Mon Jan 20 21:32:41 2014 +0100
    10.3 @@ -35,6 +35,8 @@
    10.4  
    10.5    val rewrite_by_tree : Proof.context -> term -> thm -> (thm * thm) list ->
    10.6      ctx_tree -> thm * (thm * thm) list
    10.7 +
    10.8 +  val setup : theory -> theory
    10.9  end
   10.10  
   10.11  structure Function_Ctx_Tree : FUNCTION_CTXTREE =
   10.12 @@ -286,4 +288,8 @@
   10.13      rewrite_help [] [] x tr
   10.14    end
   10.15  
   10.16 +val setup =
   10.17 +  Attrib.setup @{binding fundef_cong} (Attrib.add_del cong_add cong_del)
   10.18 +    "declaration of congruence rule for function definitions"
   10.19 +
   10.20  end
    11.1 --- a/src/HOL/Tools/Function/function.ML	Mon Jan 20 20:42:43 2014 +0100
    11.2 +++ b/src/HOL/Tools/Function/function.ML	Mon Jan 20 21:32:41 2014 +0100
    11.3 @@ -278,10 +278,7 @@
    11.4  (* setup *)
    11.5  
    11.6  val setup =
    11.7 -  Attrib.setup @{binding fundef_cong}
    11.8 -    (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
    11.9 -    "declaration of congruence rule for function definitions"
   11.10 -  #> setup_case_cong
   11.11 +  setup_case_cong
   11.12    #> Function_Common.Termination_Simps.setup
   11.13  
   11.14  val get_congs = Function_Ctx_Tree.get_function_congs
    12.1 --- a/src/HOL/Tools/Function/function_core.ML	Mon Jan 20 20:42:43 2014 +0100
    12.2 +++ b/src/HOL/Tools/Function/function_core.ML	Mon Jan 20 21:32:41 2014 +0100
    12.3 @@ -81,14 +81,14 @@
    12.4  (* Theory dependencies. *)
    12.5  val acc_induct_rule = @{thm accp_induct_rule}
    12.6  
    12.7 -val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence}
    12.8 -val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness}
    12.9 -val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff}
   12.10 +val ex1_implies_ex = @{thm Fun_Def.fundef_ex1_existence}
   12.11 +val ex1_implies_un = @{thm Fun_Def.fundef_ex1_uniqueness}
   12.12 +val ex1_implies_iff = @{thm Fun_Def.fundef_ex1_iff}
   12.13  
   12.14  val acc_downward = @{thm accp_downward}
   12.15  val accI = @{thm accp.accI}
   12.16  val case_split = @{thm HOL.case_split}
   12.17 -val fundef_default_value = @{thm FunDef.fundef_default_value}
   12.18 +val fundef_default_value = @{thm Fun_Def.fundef_default_value}
   12.19  val not_acc_down = @{thm not_accp_down}
   12.20  
   12.21  
   12.22 @@ -494,7 +494,7 @@
   12.23  fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
   12.24    let
   12.25      val f_def =
   12.26 -      Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT)
   12.27 +      Abs ("x", domT, Const (@{const_name Fun_Def.THE_default}, ranT --> (ranT --> boolT) --> ranT)
   12.28          $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
   12.29        |> Syntax.check_term lthy
   12.30    in
   12.31 @@ -718,8 +718,8 @@
   12.32  (** Termination rule **)
   12.33  
   12.34  val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule}
   12.35 -val wf_in_rel = @{thm FunDef.wf_in_rel}
   12.36 -val in_rel_def = @{thm FunDef.in_rel_def}
   12.37 +val wf_in_rel = @{thm Fun_Def.wf_in_rel}
   12.38 +val in_rel_def = @{thm Fun_Def.in_rel_def}
   12.39  
   12.40  fun mk_nest_term_case ctxt globals R' ihyp clause =
   12.41    let
   12.42 @@ -780,7 +780,7 @@
   12.43      val R' = Free ("R", fastype_of R)
   12.44  
   12.45      val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
   12.46 -    val inrel_R = Const (@{const_name FunDef.in_rel},
   12.47 +    val inrel_R = Const (@{const_name Fun_Def.in_rel},
   12.48        HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
   12.49  
   12.50      val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP},