src/HOL/Wellfounded.thy
changeset 26748 4d51ddd6aa5c
child 26803 0af0f674845d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Wellfounded.thy	Fri Apr 25 15:30:33 2008 +0200
     1.3 @@ -0,0 +1,919 @@
     1.4 +(*  ID:         $Id$
     1.5 +    Author:     Tobias Nipkow
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Author:     Konrad Slind, Alexander Krauss
     1.8 +    Copyright   1992-2008  University of Cambridge and TU Muenchen
     1.9 +*)
    1.10 +
    1.11 +header {*Well-founded Recursion*}
    1.12 +
    1.13 +theory Wellfounded
    1.14 +imports Finite_Set Nat
    1.15 +uses ("Tools/function_package/size.ML")
    1.16 +begin
    1.17 +
    1.18 +inductive
    1.19 +  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
    1.20 +  for R :: "('a * 'a) set"
    1.21 +  and F :: "('a => 'b) => 'a => 'b"
    1.22 +where
    1.23 +  wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
    1.24 +            wfrec_rel R F x (F g x)"
    1.25 +
    1.26 +constdefs
    1.27 +  wf         :: "('a * 'a)set => bool"
    1.28 +  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
    1.29 +
    1.30 +  wfP :: "('a => 'a => bool) => bool"
    1.31 +  "wfP r == wf {(x, y). r x y}"
    1.32 +
    1.33 +  acyclic :: "('a*'a)set => bool"
    1.34 +  "acyclic r == !x. (x,x) ~: r^+"
    1.35 +
    1.36 +  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
    1.37 +  "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
    1.38 +
    1.39 +  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
    1.40 +  "adm_wf R F == ALL f g x.
    1.41 +     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
    1.42 +
    1.43 +  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
    1.44 +  [code func del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    1.45 +
    1.46 +abbreviation acyclicP :: "('a => 'a => bool) => bool" where
    1.47 +  "acyclicP r == acyclic {(x, y). r x y}"
    1.48 +
    1.49 +class wellorder = linorder +
    1.50 +  assumes wf: "wf {(x, y). x < y}"
    1.51 +
    1.52 +
    1.53 +lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
    1.54 +  by (simp add: wfP_def)
    1.55 +
    1.56 +lemma wfUNIVI: 
    1.57 +   "(!!P x. (ALL x. (ALL y. (y,x) : r --> P(y)) --> P(x)) ==> P(x)) ==> wf(r)"
    1.58 +  unfolding wf_def by blast
    1.59 +
    1.60 +lemmas wfPUNIVI = wfUNIVI [to_pred]
    1.61 +
    1.62 +text{*Restriction to domain @{term A} and range @{term B}.  If @{term r} is
    1.63 +    well-founded over their intersection, then @{term "wf r"}*}
    1.64 +lemma wfI: 
    1.65 + "[| r \<subseteq> A <*> B; 
    1.66 +     !!x P. [|\<forall>x. (\<forall>y. (y,x) : r --> P y) --> P x;  x : A; x : B |] ==> P x |]
    1.67 +  ==>  wf r"
    1.68 +  unfolding wf_def by blast
    1.69 +
    1.70 +lemma wf_induct: 
    1.71 +    "[| wf(r);           
    1.72 +        !!x.[| ALL y. (y,x): r --> P(y) |] ==> P(x)  
    1.73 +     |]  ==>  P(a)"
    1.74 +  unfolding wf_def by blast
    1.75 +
    1.76 +lemmas wfP_induct = wf_induct [to_pred]
    1.77 +
    1.78 +lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf]
    1.79 +
    1.80 +lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP]
    1.81 +
    1.82 +lemma wf_not_sym: "wf r ==> (a, x) : r ==> (x, a) ~: r"
    1.83 +  by (induct a arbitrary: x set: wf) blast
    1.84 +
    1.85 +(* [| wf r;  ~Z ==> (a,x) : r;  (x,a) ~: r ==> Z |] ==> Z *)
    1.86 +lemmas wf_asym = wf_not_sym [elim_format]
    1.87 +
    1.88 +lemma wf_not_refl [simp]: "wf r ==> (a, a) ~: r"
    1.89 +  by (blast elim: wf_asym)
    1.90 +
    1.91 +(* [| wf r;  (a,a) ~: r ==> PROP W |] ==> PROP W *)
    1.92 +lemmas wf_irrefl = wf_not_refl [elim_format]
    1.93 +
    1.94 +text{*transitive closure of a well-founded relation is well-founded! *}
    1.95 +lemma wf_trancl:
    1.96 +  assumes "wf r"
    1.97 +  shows "wf (r^+)"
    1.98 +proof -
    1.99 +  {
   1.100 +    fix P and x
   1.101 +    assume induct_step: "!!x. (!!y. (y, x) : r^+ ==> P y) ==> P x"
   1.102 +    have "P x"
   1.103 +    proof (rule induct_step)
   1.104 +      fix y assume "(y, x) : r^+"
   1.105 +      with `wf r` show "P y"
   1.106 +      proof (induct x arbitrary: y)
   1.107 +	case (less x)
   1.108 +	note hyp = `\<And>x' y'. (x', x) : r ==> (y', x') : r^+ ==> P y'`
   1.109 +	from `(y, x) : r^+` show "P y"
   1.110 +	proof cases
   1.111 +	  case base
   1.112 +	  show "P y"
   1.113 +	  proof (rule induct_step)
   1.114 +	    fix y' assume "(y', y) : r^+"
   1.115 +	    with `(y, x) : r` show "P y'" by (rule hyp [of y y'])
   1.116 +	  qed
   1.117 +	next
   1.118 +	  case step
   1.119 +	  then obtain x' where "(x', x) : r" and "(y, x') : r^+" by simp
   1.120 +	  then show "P y" by (rule hyp [of x' y])
   1.121 +	qed
   1.122 +      qed
   1.123 +    qed
   1.124 +  } then show ?thesis unfolding wf_def by blast
   1.125 +qed
   1.126 +
   1.127 +lemmas wfP_trancl = wf_trancl [to_pred]
   1.128 +
   1.129 +lemma wf_converse_trancl: "wf (r^-1) ==> wf ((r^+)^-1)"
   1.130 +  apply (subst trancl_converse [symmetric])
   1.131 +  apply (erule wf_trancl)
   1.132 +  done
   1.133 +
   1.134 +
   1.135 +subsubsection {* Other simple well-foundedness results *}
   1.136 +
   1.137 +text{*Minimal-element characterization of well-foundedness*}
   1.138 +lemma wf_eq_minimal: "wf r = (\<forall>Q x. x\<in>Q --> (\<exists>z\<in>Q. \<forall>y. (y,z)\<in>r --> y\<notin>Q))"
   1.139 +proof (intro iffI strip)
   1.140 +  fix Q :: "'a set" and x
   1.141 +  assume "wf r" and "x \<in> Q"
   1.142 +  then show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q"
   1.143 +    unfolding wf_def
   1.144 +    by (blast dest: spec [of _ "%x. x\<in>Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y,z) \<in> r \<longrightarrow> y\<notin>Q)"]) 
   1.145 +next
   1.146 +  assume 1: "\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)"
   1.147 +  show "wf r"
   1.148 +  proof (rule wfUNIVI)
   1.149 +    fix P :: "'a \<Rightarrow> bool" and x
   1.150 +    assume 2: "\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x"
   1.151 +    let ?Q = "{x. \<not> P x}"
   1.152 +    have "x \<in> ?Q \<longrightarrow> (\<exists>z \<in> ?Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> ?Q)"
   1.153 +      by (rule 1 [THEN spec, THEN spec])
   1.154 +    then have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> (\<forall>y. (y, z) \<in> r \<longrightarrow> P y))" by simp
   1.155 +    with 2 have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> P z)" by fast
   1.156 +    then show "P x" by simp
   1.157 +  qed
   1.158 +qed
   1.159 +
   1.160 +lemma wfE_min: 
   1.161 +  assumes "wf R" "x \<in> Q"
   1.162 +  obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q"
   1.163 +  using assms unfolding wf_eq_minimal by blast
   1.164 +
   1.165 +lemma wfI_min:
   1.166 +  "(\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q)
   1.167 +  \<Longrightarrow> wf R"
   1.168 +  unfolding wf_eq_minimal by blast
   1.169 +
   1.170 +lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
   1.171 +
   1.172 +text {* Well-foundedness of subsets *}
   1.173 +lemma wf_subset: "[| wf(r);  p<=r |] ==> wf(p)"
   1.174 +  apply (simp (no_asm_use) add: wf_eq_minimal)
   1.175 +  apply fast
   1.176 +  done
   1.177 +
   1.178 +lemmas wfP_subset = wf_subset [to_pred]
   1.179 +
   1.180 +text {* Well-foundedness of the empty relation *}
   1.181 +lemma wf_empty [iff]: "wf({})"
   1.182 +  by (simp add: wf_def)
   1.183 +
   1.184 +lemmas wfP_empty [iff] =
   1.185 +  wf_empty [to_pred bot_empty_eq2, simplified bot_fun_eq bot_bool_eq]
   1.186 +
   1.187 +lemma wf_Int1: "wf r ==> wf (r Int r')"
   1.188 +  apply (erule wf_subset)
   1.189 +  apply (rule Int_lower1)
   1.190 +  done
   1.191 +
   1.192 +lemma wf_Int2: "wf r ==> wf (r' Int r)"
   1.193 +  apply (erule wf_subset)
   1.194 +  apply (rule Int_lower2)
   1.195 +  done  
   1.196 +
   1.197 +text{*Well-foundedness of insert*}
   1.198 +lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"
   1.199 +apply (rule iffI)
   1.200 + apply (blast elim: wf_trancl [THEN wf_irrefl]
   1.201 +              intro: rtrancl_into_trancl1 wf_subset 
   1.202 +                     rtrancl_mono [THEN [2] rev_subsetD])
   1.203 +apply (simp add: wf_eq_minimal, safe)
   1.204 +apply (rule allE, assumption, erule impE, blast) 
   1.205 +apply (erule bexE)
   1.206 +apply (rename_tac "a", case_tac "a = x")
   1.207 + prefer 2
   1.208 +apply blast 
   1.209 +apply (case_tac "y:Q")
   1.210 + prefer 2 apply blast
   1.211 +apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE)
   1.212 + apply assumption
   1.213 +apply (erule_tac V = "ALL Q. (EX x. x : Q) --> ?P Q" in thin_rl) 
   1.214 +  --{*essential for speed*}
   1.215 +txt{*Blast with new substOccur fails*}
   1.216 +apply (fast intro: converse_rtrancl_into_rtrancl)
   1.217 +done
   1.218 +
   1.219 +text{*Well-foundedness of image*}
   1.220 +lemma wf_prod_fun_image: "[| wf r; inj f |] ==> wf(prod_fun f f ` r)"
   1.221 +apply (simp only: wf_eq_minimal, clarify)
   1.222 +apply (case_tac "EX p. f p : Q")
   1.223 +apply (erule_tac x = "{p. f p : Q}" in allE)
   1.224 +apply (fast dest: inj_onD, blast)
   1.225 +done
   1.226 +
   1.227 +
   1.228 +subsubsection {* Well-Foundedness Results for Unions *}
   1.229 +
   1.230 +lemma wf_union_compatible:
   1.231 +  assumes "wf R" "wf S"
   1.232 +  assumes "S O R \<subseteq> R"
   1.233 +  shows "wf (R \<union> S)"
   1.234 +proof (rule wfI_min)
   1.235 +  fix x :: 'a and Q 
   1.236 +  let ?Q' = "{x \<in> Q. \<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> Q}"
   1.237 +  assume "x \<in> Q"
   1.238 +  obtain a where "a \<in> ?Q'"
   1.239 +    by (rule wfE_min [OF `wf R` `x \<in> Q`]) blast
   1.240 +  with `wf S`
   1.241 +  obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'" by (erule wfE_min)
   1.242 +  { 
   1.243 +    fix y assume "(y, z) \<in> S"
   1.244 +    then have "y \<notin> ?Q'" by (rule zmin)
   1.245 +
   1.246 +    have "y \<notin> Q"
   1.247 +    proof 
   1.248 +      assume "y \<in> Q"
   1.249 +      with `y \<notin> ?Q'` 
   1.250 +      obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
   1.251 +      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> S O R" by (rule rel_compI)
   1.252 +      with `S O R \<subseteq> R` have "(w, z) \<in> R" ..
   1.253 +      with `z \<in> ?Q'` have "w \<notin> Q" by blast 
   1.254 +      with `w \<in> Q` show False by contradiction
   1.255 +    qed
   1.256 +  }
   1.257 +  with `z \<in> ?Q'` show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<union> S \<longrightarrow> y \<notin> Q" by blast
   1.258 +qed
   1.259 +
   1.260 +
   1.261 +text {* Well-foundedness of indexed union with disjoint domains and ranges *}
   1.262 +
   1.263 +lemma wf_UN: "[| ALL i:I. wf(r i);  
   1.264 +         ALL i:I. ALL j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {}  
   1.265 +      |] ==> wf(UN i:I. r i)"
   1.266 +apply (simp only: wf_eq_minimal, clarify)
   1.267 +apply (rename_tac A a, case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i")
   1.268 + prefer 2
   1.269 + apply force 
   1.270 +apply clarify
   1.271 +apply (drule bspec, assumption)  
   1.272 +apply (erule_tac x="{a. a:A & (EX b:A. (b,a) : r i) }" in allE)
   1.273 +apply (blast elim!: allE)  
   1.274 +done
   1.275 +
   1.276 +lemmas wfP_SUP = wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}",
   1.277 +  to_pred SUP_UN_eq2 bot_empty_eq, simplified, standard]
   1.278 +
   1.279 +lemma wf_Union: 
   1.280 + "[| ALL r:R. wf r;  
   1.281 +     ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}  
   1.282 +  |] ==> wf(Union R)"
   1.283 +apply (simp add: Union_def)
   1.284 +apply (blast intro: wf_UN)
   1.285 +done
   1.286 +
   1.287 +(*Intuition: we find an (R u S)-min element of a nonempty subset A
   1.288 +             by case distinction.
   1.289 +  1. There is a step a -R-> b with a,b : A.
   1.290 +     Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}.
   1.291 +     By definition, there is z':A s.t. z -R-> z'. Because z is R-min in the
   1.292 +     subset, z' must be R-min in A. Because z' has an R-predecessor, it cannot
   1.293 +     have an S-successor and is thus S-min in A as well.
   1.294 +  2. There is no such step.
   1.295 +     Pick an S-min element of A. In this case it must be an R-min
   1.296 +     element of A as well.
   1.297 +
   1.298 +*)
   1.299 +lemma wf_Un:
   1.300 +     "[| wf r; wf s; Domain r Int Range s = {} |] ==> wf(r Un s)"
   1.301 +  using wf_union_compatible[of s r] 
   1.302 +  by (auto simp: Un_ac)
   1.303 +
   1.304 +lemma wf_union_merge: 
   1.305 +  "wf (R \<union> S) = wf (R O R \<union> R O S \<union> S)" (is "wf ?A = wf ?B")
   1.306 +proof
   1.307 +  assume "wf ?A"
   1.308 +  with wf_trancl have wfT: "wf (?A^+)" .
   1.309 +  moreover have "?B \<subseteq> ?A^+"
   1.310 +    by (subst trancl_unfold, subst trancl_unfold) blast
   1.311 +  ultimately show "wf ?B" by (rule wf_subset)
   1.312 +next
   1.313 +  assume "wf ?B"
   1.314 +
   1.315 +  show "wf ?A"
   1.316 +  proof (rule wfI_min)
   1.317 +    fix Q :: "'a set" and x 
   1.318 +    assume "x \<in> Q"
   1.319 +
   1.320 +    with `wf ?B`
   1.321 +    obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" 
   1.322 +      by (erule wfE_min)
   1.323 +    then have A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q"
   1.324 +      and A2: "\<And>y. (y, z) \<in> R O S \<Longrightarrow> y \<notin> Q"
   1.325 +      and A3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q"
   1.326 +      by auto
   1.327 +    
   1.328 +    show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> ?A \<longrightarrow> y \<notin> Q"
   1.329 +    proof (cases "\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q")
   1.330 +      case True
   1.331 +      with `z \<in> Q` A3 show ?thesis by blast
   1.332 +    next
   1.333 +      case False 
   1.334 +      then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast
   1.335 +
   1.336 +      have "\<forall>y. (y, z') \<in> ?A \<longrightarrow> y \<notin> Q"
   1.337 +      proof (intro allI impI)
   1.338 +        fix y assume "(y, z') \<in> ?A"
   1.339 +        then show "y \<notin> Q"
   1.340 +        proof
   1.341 +          assume "(y, z') \<in> R" 
   1.342 +          then have "(y, z) \<in> R O R" using `(z', z) \<in> R` ..
   1.343 +          with A1 show "y \<notin> Q" .
   1.344 +        next
   1.345 +          assume "(y, z') \<in> S" 
   1.346 +          then have "(y, z) \<in> R O S" using  `(z', z) \<in> R` ..
   1.347 +          with A2 show "y \<notin> Q" .
   1.348 +        qed
   1.349 +      qed
   1.350 +      with `z' \<in> Q` show ?thesis ..
   1.351 +    qed
   1.352 +  qed
   1.353 +qed
   1.354 +
   1.355 +lemma wf_comp_self: "wf R = wf (R O R)"  -- {* special case *}
   1.356 +  by (rule wf_union_merge [where S = "{}", simplified])
   1.357 +
   1.358 +
   1.359 +subsubsection {* acyclic *}
   1.360 +
   1.361 +lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
   1.362 +  by (simp add: acyclic_def)
   1.363 +
   1.364 +lemma wf_acyclic: "wf r ==> acyclic r"
   1.365 +apply (simp add: acyclic_def)
   1.366 +apply (blast elim: wf_trancl [THEN wf_irrefl])
   1.367 +done
   1.368 +
   1.369 +lemmas wfP_acyclicP = wf_acyclic [to_pred]
   1.370 +
   1.371 +lemma acyclic_insert [iff]:
   1.372 +     "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"
   1.373 +apply (simp add: acyclic_def trancl_insert)
   1.374 +apply (blast intro: rtrancl_trans)
   1.375 +done
   1.376 +
   1.377 +lemma acyclic_converse [iff]: "acyclic(r^-1) = acyclic r"
   1.378 +by (simp add: acyclic_def trancl_converse)
   1.379 +
   1.380 +lemmas acyclicP_converse [iff] = acyclic_converse [to_pred]
   1.381 +
   1.382 +lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)"
   1.383 +apply (simp add: acyclic_def antisym_def)
   1.384 +apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)
   1.385 +done
   1.386 +
   1.387 +(* Other direction:
   1.388 +acyclic = no loops
   1.389 +antisym = only self loops
   1.390 +Goalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r - Id)
   1.391 +==> antisym( r^* ) = acyclic(r - Id)";
   1.392 +*)
   1.393 +
   1.394 +lemma acyclic_subset: "[| acyclic s; r <= s |] ==> acyclic r"
   1.395 +apply (simp add: acyclic_def)
   1.396 +apply (blast intro: trancl_mono)
   1.397 +done
   1.398 +
   1.399 +text{* Wellfoundedness of finite acyclic relations*}
   1.400 +
   1.401 +lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r"
   1.402 +apply (erule finite_induct, blast)
   1.403 +apply (simp (no_asm_simp) only: split_tupled_all)
   1.404 +apply simp
   1.405 +done
   1.406 +
   1.407 +lemma finite_acyclic_wf_converse: "[|finite r; acyclic r|] ==> wf (r^-1)"
   1.408 +apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])
   1.409 +apply (erule acyclic_converse [THEN iffD2])
   1.410 +done
   1.411 +
   1.412 +lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r"
   1.413 +by (blast intro: finite_acyclic_wf wf_acyclic)
   1.414 +
   1.415 +
   1.416 +subsection{*Well-Founded Recursion*}
   1.417 +
   1.418 +text{*cut*}
   1.419 +
   1.420 +lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
   1.421 +by (simp add: expand_fun_eq cut_def)
   1.422 +
   1.423 +lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
   1.424 +by (simp add: cut_def)
   1.425 +
   1.426 +text{*Inductive characterization of wfrec combinator; for details see:  
   1.427 +John Harrison, "Inductive definitions: automation and application"*}
   1.428 +
   1.429 +lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
   1.430 +apply (simp add: adm_wf_def)
   1.431 +apply (erule_tac a=x in wf_induct) 
   1.432 +apply (rule ex1I)
   1.433 +apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
   1.434 +apply (fast dest!: theI')
   1.435 +apply (erule wfrec_rel.cases, simp)
   1.436 +apply (erule allE, erule allE, erule allE, erule mp)
   1.437 +apply (fast intro: the_equality [symmetric])
   1.438 +done
   1.439 +
   1.440 +lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
   1.441 +apply (simp add: adm_wf_def)
   1.442 +apply (intro strip)
   1.443 +apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
   1.444 +apply (rule refl)
   1.445 +done
   1.446 +
   1.447 +lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
   1.448 +apply (simp add: wfrec_def)
   1.449 +apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
   1.450 +apply (rule wfrec_rel.wfrecI)
   1.451 +apply (intro strip)
   1.452 +apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
   1.453 +done
   1.454 +
   1.455 +subsection {* Code generator setup *}
   1.456 +
   1.457 +consts_code
   1.458 +  "wfrec"   ("\<module>wfrec?")
   1.459 +attach {*
   1.460 +fun wfrec f x = f (wfrec f) x;
   1.461 +*}
   1.462 +
   1.463 +
   1.464 +subsection {*LEAST and wellorderings*}
   1.465 +
   1.466 +text{* See also @{text wf_linord_ex_has_least} and its consequences in
   1.467 + @{text Wellfounded_Relations.ML}*}
   1.468 +
   1.469 +lemma wellorder_Least_lemma [rule_format]:
   1.470 +     "P (k::'a::wellorder) --> P (LEAST x. P(x)) & (LEAST x. P(x)) <= k"
   1.471 +apply (rule_tac a = k in wf [THEN wf_induct])
   1.472 +apply (rule impI)
   1.473 +apply (rule classical)
   1.474 +apply (rule_tac s = x in Least_equality [THEN ssubst], auto)
   1.475 +apply (auto simp add: linorder_not_less [symmetric])
   1.476 +done
   1.477 +
   1.478 +lemmas LeastI   = wellorder_Least_lemma [THEN conjunct1, standard]
   1.479 +lemmas Least_le = wellorder_Least_lemma [THEN conjunct2, standard]
   1.480 +
   1.481 +-- "The following 3 lemmas are due to Brian Huffman"
   1.482 +lemma LeastI_ex: "EX x::'a::wellorder. P x ==> P (Least P)"
   1.483 +apply (erule exE)
   1.484 +apply (erule LeastI)
   1.485 +done
   1.486 +
   1.487 +lemma LeastI2:
   1.488 +  "[| P (a::'a::wellorder); !!x. P x ==> Q x |] ==> Q (Least P)"
   1.489 +by (blast intro: LeastI)
   1.490 +
   1.491 +lemma LeastI2_ex:
   1.492 +  "[| EX a::'a::wellorder. P a; !!x. P x ==> Q x |] ==> Q (Least P)"
   1.493 +by (blast intro: LeastI_ex)
   1.494 +
   1.495 +lemma not_less_Least: "[| k < (LEAST x. P x) |] ==> ~P (k::'a::wellorder)"
   1.496 +apply (simp (no_asm_use) add: linorder_not_le [symmetric])
   1.497 +apply (erule contrapos_nn)
   1.498 +apply (erule Least_le)
   1.499 +done
   1.500 +
   1.501 +subsection {* @{typ nat} is well-founded *}
   1.502 +
   1.503 +lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++"
   1.504 +proof (rule ext, rule ext, rule iffI)
   1.505 +  fix n m :: nat
   1.506 +  assume "m < n"
   1.507 +  then show "(\<lambda>m n. n = Suc m)^++ m n"
   1.508 +  proof (induct n)
   1.509 +    case 0 then show ?case by auto
   1.510 +  next
   1.511 +    case (Suc n) then show ?case
   1.512 +      by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl)
   1.513 +  qed
   1.514 +next
   1.515 +  fix n m :: nat
   1.516 +  assume "(\<lambda>m n. n = Suc m)^++ m n"
   1.517 +  then show "m < n"
   1.518 +    by (induct n)
   1.519 +      (simp_all add: less_Suc_eq_le reflexive le_less)
   1.520 +qed
   1.521 +
   1.522 +definition
   1.523 +  pred_nat :: "(nat * nat) set" where
   1.524 +  "pred_nat = {(m, n). n = Suc m}"
   1.525 +
   1.526 +definition
   1.527 +  less_than :: "(nat * nat) set" where
   1.528 +  "less_than = pred_nat^+"
   1.529 +
   1.530 +lemma less_eq: "(m, n) \<in> pred_nat^+ \<longleftrightarrow> m < n"
   1.531 +  unfolding less_nat_rel pred_nat_def trancl_def by simp
   1.532 +
   1.533 +lemma pred_nat_trancl_eq_le:
   1.534 +  "(m, n) \<in> pred_nat^* \<longleftrightarrow> m \<le> n"
   1.535 +  unfolding less_eq rtrancl_eq_or_trancl by auto
   1.536 +
   1.537 +lemma wf_pred_nat: "wf pred_nat"
   1.538 +  apply (unfold wf_def pred_nat_def, clarify)
   1.539 +  apply (induct_tac x, blast+)
   1.540 +  done
   1.541 +
   1.542 +lemma wf_less_than [iff]: "wf less_than"
   1.543 +  by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])
   1.544 +
   1.545 +lemma trans_less_than [iff]: "trans less_than"
   1.546 +  by (simp add: less_than_def trans_trancl)
   1.547 +
   1.548 +lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)"
   1.549 +  by (simp add: less_than_def less_eq)
   1.550 +
   1.551 +lemma wf_less: "wf {(x, y::nat). x < y}"
   1.552 +  using wf_less_than by (simp add: less_than_def less_eq [symmetric])
   1.553 +
   1.554 +text {* Type @{typ nat} is a wellfounded order *}
   1.555 +
   1.556 +instance nat :: wellorder
   1.557 +  by intro_classes
   1.558 +    (assumption |
   1.559 +      rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+
   1.560 +
   1.561 +text {* @{text LEAST} theorems for type @{typ nat}*}
   1.562 +
   1.563 +lemma Least_Suc:
   1.564 +     "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
   1.565 +  apply (case_tac "n", auto)
   1.566 +  apply (frule LeastI)
   1.567 +  apply (drule_tac P = "%x. P (Suc x) " in LeastI)
   1.568 +  apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
   1.569 +  apply (erule_tac [2] Least_le)
   1.570 +  apply (case_tac "LEAST x. P x", auto)
   1.571 +  apply (drule_tac P = "%x. P (Suc x) " in Least_le)
   1.572 +  apply (blast intro: order_antisym)
   1.573 +  done
   1.574 +
   1.575 +lemma Least_Suc2:
   1.576 +   "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
   1.577 +  apply (erule (1) Least_Suc [THEN ssubst])
   1.578 +  apply simp
   1.579 +  done
   1.580 +
   1.581 +lemma ex_least_nat_le: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not>P i) & P(k)"
   1.582 +  apply (cases n)
   1.583 +   apply blast
   1.584 +  apply (rule_tac x="LEAST k. P(k)" in exI)
   1.585 +  apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
   1.586 +  done
   1.587 +
   1.588 +lemma ex_least_nat_less: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not>P i) & P(k+1)"
   1.589 +  apply (cases n)
   1.590 +   apply blast
   1.591 +  apply (frule (1) ex_least_nat_le)
   1.592 +  apply (erule exE)
   1.593 +  apply (case_tac k)
   1.594 +   apply simp
   1.595 +  apply (rename_tac k1)
   1.596 +  apply (rule_tac x=k1 in exI)
   1.597 +  apply fastsimp
   1.598 +  done
   1.599 +
   1.600 +
   1.601 +subsection {* Accessible Part *}
   1.602 +
   1.603 +text {*
   1.604 + Inductive definition of the accessible part @{term "acc r"} of a
   1.605 + relation; see also \cite{paulin-tlca}.
   1.606 +*}
   1.607 +
   1.608 +inductive_set
   1.609 +  acc :: "('a * 'a) set => 'a set"
   1.610 +  for r :: "('a * 'a) set"
   1.611 +  where
   1.612 +    accI: "(!!y. (y, x) : r ==> y : acc r) ==> x : acc r"
   1.613 +
   1.614 +abbreviation
   1.615 +  termip :: "('a => 'a => bool) => 'a => bool" where
   1.616 +  "termip r == accp (r\<inverse>\<inverse>)"
   1.617 +
   1.618 +abbreviation
   1.619 +  termi :: "('a * 'a) set => 'a set" where
   1.620 +  "termi r == acc (r\<inverse>)"
   1.621 +
   1.622 +lemmas accpI = accp.accI
   1.623 +
   1.624 +text {* Induction rules *}
   1.625 +
   1.626 +theorem accp_induct:
   1.627 +  assumes major: "accp r a"
   1.628 +  assumes hyp: "!!x. accp r x ==> \<forall>y. r y x --> P y ==> P x"
   1.629 +  shows "P a"
   1.630 +  apply (rule major [THEN accp.induct])
   1.631 +  apply (rule hyp)
   1.632 +   apply (rule accp.accI)
   1.633 +   apply fast
   1.634 +  apply fast
   1.635 +  done
   1.636 +
   1.637 +theorems accp_induct_rule = accp_induct [rule_format, induct set: accp]
   1.638 +
   1.639 +theorem accp_downward: "accp r b ==> r a b ==> accp r a"
   1.640 +  apply (erule accp.cases)
   1.641 +  apply fast
   1.642 +  done
   1.643 +
   1.644 +lemma not_accp_down:
   1.645 +  assumes na: "\<not> accp R x"
   1.646 +  obtains z where "R z x" and "\<not> accp R z"
   1.647 +proof -
   1.648 +  assume a: "\<And>z. \<lbrakk>R z x; \<not> accp R z\<rbrakk> \<Longrightarrow> thesis"
   1.649 +
   1.650 +  show thesis
   1.651 +  proof (cases "\<forall>z. R z x \<longrightarrow> accp R z")
   1.652 +    case True
   1.653 +    hence "\<And>z. R z x \<Longrightarrow> accp R z" by auto
   1.654 +    hence "accp R x"
   1.655 +      by (rule accp.accI)
   1.656 +    with na show thesis ..
   1.657 +  next
   1.658 +    case False then obtain z where "R z x" and "\<not> accp R z"
   1.659 +      by auto
   1.660 +    with a show thesis .
   1.661 +  qed
   1.662 +qed
   1.663 +
   1.664 +lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a ==> accp r a --> accp r b"
   1.665 +  apply (erule rtranclp_induct)
   1.666 +   apply blast
   1.667 +  apply (blast dest: accp_downward)
   1.668 +  done
   1.669 +
   1.670 +theorem accp_downwards: "accp r a ==> r\<^sup>*\<^sup>* b a ==> accp r b"
   1.671 +  apply (blast dest: accp_downwards_aux)
   1.672 +  done
   1.673 +
   1.674 +theorem accp_wfPI: "\<forall>x. accp r x ==> wfP r"
   1.675 +  apply (rule wfPUNIVI)
   1.676 +  apply (induct_tac P x rule: accp_induct)
   1.677 +   apply blast
   1.678 +  apply blast
   1.679 +  done
   1.680 +
   1.681 +theorem accp_wfPD: "wfP r ==> accp r x"
   1.682 +  apply (erule wfP_induct_rule)
   1.683 +  apply (rule accp.accI)
   1.684 +  apply blast
   1.685 +  done
   1.686 +
   1.687 +theorem wfP_accp_iff: "wfP r = (\<forall>x. accp r x)"
   1.688 +  apply (blast intro: accp_wfPI dest: accp_wfPD)
   1.689 +  done
   1.690 +
   1.691 +
   1.692 +text {* Smaller relations have bigger accessible parts: *}
   1.693 +
   1.694 +lemma accp_subset:
   1.695 +  assumes sub: "R1 \<le> R2"
   1.696 +  shows "accp R2 \<le> accp R1"
   1.697 +proof
   1.698 +  fix x assume "accp R2 x"
   1.699 +  then show "accp R1 x"
   1.700 +  proof (induct x)
   1.701 +    fix x
   1.702 +    assume ih: "\<And>y. R2 y x \<Longrightarrow> accp R1 y"
   1.703 +    with sub show "accp R1 x"
   1.704 +      by (blast intro: accp.accI)
   1.705 +  qed
   1.706 +qed
   1.707 +
   1.708 +
   1.709 +text {* This is a generalized induction theorem that works on
   1.710 +  subsets of the accessible part. *}
   1.711 +
   1.712 +lemma accp_subset_induct:
   1.713 +  assumes subset: "D \<le> accp R"
   1.714 +    and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z"
   1.715 +    and "D x"
   1.716 +    and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
   1.717 +  shows "P x"
   1.718 +proof -
   1.719 +  from subset and `D x`
   1.720 +  have "accp R x" ..
   1.721 +  then show "P x" using `D x`
   1.722 +  proof (induct x)
   1.723 +    fix x
   1.724 +    assume "D x"
   1.725 +      and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y"
   1.726 +    with dcl and istep show "P x" by blast
   1.727 +  qed
   1.728 +qed
   1.729 +
   1.730 +
   1.731 +text {* Set versions of the above theorems *}
   1.732 +
   1.733 +lemmas acc_induct = accp_induct [to_set]
   1.734 +
   1.735 +lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc]
   1.736 +
   1.737 +lemmas acc_downward = accp_downward [to_set]
   1.738 +
   1.739 +lemmas not_acc_down = not_accp_down [to_set]
   1.740 +
   1.741 +lemmas acc_downwards_aux = accp_downwards_aux [to_set]
   1.742 +
   1.743 +lemmas acc_downwards = accp_downwards [to_set]
   1.744 +
   1.745 +lemmas acc_wfI = accp_wfPI [to_set]
   1.746 +
   1.747 +lemmas acc_wfD = accp_wfPD [to_set]
   1.748 +
   1.749 +lemmas wf_acc_iff = wfP_accp_iff [to_set]
   1.750 +
   1.751 +lemmas acc_subset = accp_subset [to_set]
   1.752 +
   1.753 +lemmas acc_subset_induct = accp_subset_induct [to_set]
   1.754 +
   1.755 +
   1.756 +subsection {* Tools for building wellfounded relations *}
   1.757 +
   1.758 +text {* Inverse Image *}
   1.759 +
   1.760 +lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))"
   1.761 +apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal)
   1.762 +apply clarify
   1.763 +apply (subgoal_tac "EX (w::'b) . w : {w. EX (x::'a) . x: Q & (f x = w) }")
   1.764 +prefer 2 apply (blast del: allE)
   1.765 +apply (erule allE)
   1.766 +apply (erule (1) notE impE)
   1.767 +apply blast
   1.768 +done
   1.769 +
   1.770 +lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
   1.771 +  by (auto simp:inv_image_def)
   1.772 +
   1.773 +text {* Measure functions into @{typ nat} *}
   1.774 +
   1.775 +definition measure :: "('a => nat) => ('a * 'a)set"
   1.776 +where "measure == inv_image less_than"
   1.777 +
   1.778 +lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)"
   1.779 +  by (simp add:measure_def)
   1.780 +
   1.781 +lemma wf_measure [iff]: "wf (measure f)"
   1.782 +apply (unfold measure_def)
   1.783 +apply (rule wf_less_than [THEN wf_inv_image])
   1.784 +done
   1.785 +
   1.786 +text{* Lexicographic combinations *}
   1.787 +
   1.788 +definition
   1.789 + lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
   1.790 +               (infixr "<*lex*>" 80)
   1.791 +where
   1.792 +    "ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
   1.793 +
   1.794 +lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
   1.795 +apply (unfold wf_def lex_prod_def) 
   1.796 +apply (rule allI, rule impI)
   1.797 +apply (simp (no_asm_use) only: split_paired_All)
   1.798 +apply (drule spec, erule mp) 
   1.799 +apply (rule allI, rule impI)
   1.800 +apply (drule spec, erule mp, blast) 
   1.801 +done
   1.802 +
   1.803 +lemma in_lex_prod[simp]: 
   1.804 +  "(((a,b),(a',b')): r <*lex*> s) = ((a,a'): r \<or> (a = a' \<and> (b, b') : s))"
   1.805 +  by (auto simp:lex_prod_def)
   1.806 +
   1.807 +text{* @{term "op <*lex*>"} preserves transitivity *}
   1.808 +
   1.809 +lemma trans_lex_prod [intro!]: 
   1.810 +    "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
   1.811 +by (unfold trans_def lex_prod_def, blast) 
   1.812 +
   1.813 +text {* lexicographic combinations with measure functions *}
   1.814 +
   1.815 +definition 
   1.816 +  mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
   1.817 +where
   1.818 +  "f <*mlex*> R = inv_image (less_than <*lex*> R) (%x. (f x, x))"
   1.819 +
   1.820 +lemma wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)"
   1.821 +unfolding mlex_prod_def
   1.822 +by auto
   1.823 +
   1.824 +lemma mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
   1.825 +unfolding mlex_prod_def by simp
   1.826 +
   1.827 +lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
   1.828 +unfolding mlex_prod_def by auto
   1.829 +
   1.830 +text {* proper subset relation on finite sets *}
   1.831 +
   1.832 +definition finite_psubset  :: "('a set * 'a set) set"
   1.833 +where "finite_psubset == {(A,B). A < B & finite B}"
   1.834 +
   1.835 +lemma wf_finite_psubset: "wf(finite_psubset)"
   1.836 +apply (unfold finite_psubset_def)
   1.837 +apply (rule wf_measure [THEN wf_subset])
   1.838 +apply (simp add: measure_def inv_image_def less_than_def less_eq)
   1.839 +apply (fast elim!: psubset_card_mono)
   1.840 +done
   1.841 +
   1.842 +lemma trans_finite_psubset: "trans finite_psubset"
   1.843 +by (simp add: finite_psubset_def psubset_def trans_def, blast)
   1.844 +
   1.845 +
   1.846 +
   1.847 +
   1.848 +text {*Wellfoundedness of @{text same_fst}*}
   1.849 +
   1.850 +definition
   1.851 + same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
   1.852 +where
   1.853 +    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
   1.854 +   --{*For @{text rec_def} declarations where the first n parameters
   1.855 +       stay unchanged in the recursive call. 
   1.856 +       See @{text "Library/While_Combinator.thy"} for an application.*}
   1.857 +
   1.858 +lemma same_fstI [intro!]:
   1.859 +     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
   1.860 +by (simp add: same_fst_def)
   1.861 +
   1.862 +lemma wf_same_fst:
   1.863 +  assumes prem: "(!!x. P x ==> wf(R x))"
   1.864 +  shows "wf(same_fst P R)"
   1.865 +apply (simp cong del: imp_cong add: wf_def same_fst_def)
   1.866 +apply (intro strip)
   1.867 +apply (rename_tac a b)
   1.868 +apply (case_tac "wf (R a)")
   1.869 + apply (erule_tac a = b in wf_induct, blast)
   1.870 +apply (blast intro: prem)
   1.871 +done
   1.872 +
   1.873 +
   1.874 +subsection{*Weakly decreasing sequences (w.r.t. some well-founded order) 
   1.875 +   stabilize.*}
   1.876 +
   1.877 +text{*This material does not appear to be used any longer.*}
   1.878 +
   1.879 +lemma lemma1: "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*"
   1.880 +apply (induct_tac "k", simp_all)
   1.881 +apply (blast intro: rtrancl_trans)
   1.882 +done
   1.883 +
   1.884 +lemma lemma2: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
   1.885 +      ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))"
   1.886 +apply (erule wf_induct, clarify)
   1.887 +apply (case_tac "EX j. (f (m+j), f m) : r^+")
   1.888 + apply clarify
   1.889 + apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ")
   1.890 +  apply clarify
   1.891 +  apply (rule_tac x = "j+i" in exI)
   1.892 +  apply (simp add: add_ac, blast)
   1.893 +apply (rule_tac x = 0 in exI, clarsimp)
   1.894 +apply (drule_tac i = m and k = k in lemma1)
   1.895 +apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
   1.896 +done
   1.897 +
   1.898 +lemma wf_weak_decr_stable: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
   1.899 +      ==> EX i. ALL k. f (i+k) = f i"
   1.900 +apply (drule_tac x = 0 in lemma2 [THEN spec], auto)
   1.901 +done
   1.902 +
   1.903 +(* special case of the theorem above: <= *)
   1.904 +lemma weak_decr_stable:
   1.905 +     "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i"
   1.906 +apply (rule_tac r = pred_nat in wf_weak_decr_stable)
   1.907 +apply (simp add: pred_nat_trancl_eq_le)
   1.908 +apply (intro wf_trancl wf_pred_nat)
   1.909 +done
   1.910 +
   1.911 +
   1.912 +subsection {* size of a datatype value *}
   1.913 +
   1.914 +use "Tools/function_package/size.ML"
   1.915 +
   1.916 +setup Size.setup
   1.917 +
   1.918 +lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
   1.919 +  by (induct n) simp_all
   1.920 +
   1.921 +
   1.922 +end