src/HOL/Wellfounded_Recursion.thy
 author wenzelm Fri Mar 28 19:43:54 2008 +0100 (2008-03-28) changeset 26462 dac4e2bce00d parent 26235 96b804999ca7 permissions -rw-r--r--
avoid rebinding of existing facts;
     1 (*  ID:         $Id$

     2     Author:     Tobias Nipkow

     3     Copyright   1992  University of Cambridge

     4 *)

     5

     6 header {*Well-founded Recursion*}

     7

     8 theory Wellfounded_Recursion

     9 imports Transitive_Closure Nat

    10 uses ("Tools/function_package/size.ML")

    11 begin

    12

    13 inductive

    14   wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"

    15   for R :: "('a * 'a) set"

    16   and F :: "('a => 'b) => 'a => 'b"

    17 where

    18   wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>

    19             wfrec_rel R F x (F g x)"

    20

    21 constdefs

    22   wf         :: "('a * 'a)set => bool"

    23   "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"

    24

    25   wfP :: "('a => 'a => bool) => bool"

    26   "wfP r == wf {(x, y). r x y}"

    27

    28   acyclic :: "('a*'a)set => bool"

    29   "acyclic r == !x. (x,x) ~: r^+"

    30

    31   cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"

    32   "cut f r x == (%y. if (y,x):r then f y else arbitrary)"

    33

    34   adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"

    35   "adm_wf R F == ALL f g x.

    36      (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"

    37

    38   wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"

    39   [code func del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"

    40

    41 abbreviation acyclicP :: "('a => 'a => bool) => bool" where

    42   "acyclicP r == acyclic {(x, y). r x y}"

    43

    44 class wellorder = linorder +

    45   assumes wf: "wf {(x, y). x < y}"

    46

    47

    48 lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"

    49   by (simp add: wfP_def)

    50

    51 lemma wfUNIVI:

    52    "(!!P x. (ALL x. (ALL y. (y,x) : r --> P(y)) --> P(x)) ==> P(x)) ==> wf(r)"

    53   unfolding wf_def by blast

    54

    55 lemmas wfPUNIVI = wfUNIVI [to_pred]

    56

    57 text{*Restriction to domain @{term A} and range @{term B}.  If @{term r} is

    58     well-founded over their intersection, then @{term "wf r"}*}

    59 lemma wfI:

    60  "[| r \<subseteq> A <*> B;

    61      !!x P. [|\<forall>x. (\<forall>y. (y,x) : r --> P y) --> P x;  x : A; x : B |] ==> P x |]

    62   ==>  wf r"

    63   unfolding wf_def by blast

    64

    65 lemma wf_induct:

    66     "[| wf(r);

    67         !!x.[| ALL y. (y,x): r --> P(y) |] ==> P(x)

    68      |]  ==>  P(a)"

    69   unfolding wf_def by blast

    70

    71 lemmas wfP_induct = wf_induct [to_pred]

    72

    73 lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf]

    74

    75 lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP]

    76

    77 lemma wf_not_sym: "wf r ==> (a, x) : r ==> (x, a) ~: r"

    78   by (induct a arbitrary: x set: wf) blast

    79

    80 (* [| wf r;  ~Z ==> (a,x) : r;  (x,a) ~: r ==> Z |] ==> Z *)

    81 lemmas wf_asym = wf_not_sym [elim_format]

    82

    83 lemma wf_not_refl [simp]: "wf r ==> (a, a) ~: r"

    84   by (blast elim: wf_asym)

    85

    86 (* [| wf r;  (a,a) ~: r ==> PROP W |] ==> PROP W *)

    87 lemmas wf_irrefl = wf_not_refl [elim_format]

    88

    89 text{*transitive closure of a well-founded relation is well-founded! *}

    90 lemma wf_trancl:

    91   assumes "wf r"

    92   shows "wf (r^+)"

    93 proof -

    94   {

    95     fix P and x

    96     assume induct_step: "!!x. (!!y. (y, x) : r^+ ==> P y) ==> P x"

    97     have "P x"

    98     proof (rule induct_step)

    99       fix y assume "(y, x) : r^+"

   100       with wf r show "P y"

   101       proof (induct x arbitrary: y)

   102 	case (less x)

   103 	note hyp = \<And>x' y'. (x', x) : r ==> (y', x') : r^+ ==> P y'

   104 	from (y, x) : r^+ show "P y"

   105 	proof cases

   106 	  case base

   107 	  show "P y"

   108 	  proof (rule induct_step)

   109 	    fix y' assume "(y', y) : r^+"

   110 	    with (y, x) : r show "P y'" by (rule hyp [of y y'])

   111 	  qed

   112 	next

   113 	  case step

   114 	  then obtain x' where "(x', x) : r" and "(y, x') : r^+" by simp

   115 	  then show "P y" by (rule hyp [of x' y])

   116 	qed

   117       qed

   118     qed

   119   } then show ?thesis unfolding wf_def by blast

   120 qed

   121

   122 lemmas wfP_trancl = wf_trancl [to_pred]

   123

   124 lemma wf_converse_trancl: "wf (r^-1) ==> wf ((r^+)^-1)"

   125   apply (subst trancl_converse [symmetric])

   126   apply (erule wf_trancl)

   127   done

   128

   129

   130 subsubsection {* Other simple well-foundedness results *}

   131

   132 text{*Minimal-element characterization of well-foundedness*}

   133 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))"

   134 proof (intro iffI strip)

   135   fix Q :: "'a set" and x

   136   assume "wf r" and "x \<in> Q"

   137   then show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q"

   138     unfolding wf_def

   139     by (blast dest: spec [of _ "%x. x\<in>Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y,z) \<in> r \<longrightarrow> y\<notin>Q)"])

   140 next

   141   assume 1: "\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)"

   142   show "wf r"

   143   proof (rule wfUNIVI)

   144     fix P :: "'a \<Rightarrow> bool" and x

   145     assume 2: "\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x"

   146     let ?Q = "{x. \<not> P x}"

   147     have "x \<in> ?Q \<longrightarrow> (\<exists>z \<in> ?Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> ?Q)"

   148       by (rule 1 [THEN spec, THEN spec])

   149     then have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> (\<forall>y. (y, z) \<in> r \<longrightarrow> P y))" by simp

   150     with 2 have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> P z)" by fast

   151     then show "P x" by simp

   152   qed

   153 qed

   154

   155 lemma wfE_min:

   156   assumes "wf R" "x \<in> Q"

   157   obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q"

   158   using assms unfolding wf_eq_minimal by blast

   159

   160 lemma wfI_min:

   161   "(\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q)

   162   \<Longrightarrow> wf R"

   163   unfolding wf_eq_minimal by blast

   164

   165 lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]

   166

   167 text {* Well-foundedness of subsets *}

   168 lemma wf_subset: "[| wf(r);  p<=r |] ==> wf(p)"

   169   apply (simp (no_asm_use) add: wf_eq_minimal)

   170   apply fast

   171   done

   172

   173 lemmas wfP_subset = wf_subset [to_pred]

   174

   175 text {* Well-foundedness of the empty relation *}

   176 lemma wf_empty [iff]: "wf({})"

   177   by (simp add: wf_def)

   178

   179 lemmas wfP_empty [iff] =

   180   wf_empty [to_pred bot_empty_eq2, simplified bot_fun_eq bot_bool_eq]

   181

   182 lemma wf_Int1: "wf r ==> wf (r Int r')"

   183   apply (erule wf_subset)

   184   apply (rule Int_lower1)

   185   done

   186

   187 lemma wf_Int2: "wf r ==> wf (r' Int r)"

   188   apply (erule wf_subset)

   189   apply (rule Int_lower2)

   190   done

   191

   192 text{*Well-foundedness of insert*}

   193 lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"

   194 apply (rule iffI)

   195  apply (blast elim: wf_trancl [THEN wf_irrefl]

   196               intro: rtrancl_into_trancl1 wf_subset

   197                      rtrancl_mono [THEN [2] rev_subsetD])

   198 apply (simp add: wf_eq_minimal, safe)

   199 apply (rule allE, assumption, erule impE, blast)

   200 apply (erule bexE)

   201 apply (rename_tac "a", case_tac "a = x")

   202  prefer 2

   203 apply blast

   204 apply (case_tac "y:Q")

   205  prefer 2 apply blast

   206 apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE)

   207  apply assumption

   208 apply (erule_tac V = "ALL Q. (EX x. x : Q) --> ?P Q" in thin_rl)

   209   --{*essential for speed*}

   210 txt{*Blast with new substOccur fails*}

   211 apply (fast intro: converse_rtrancl_into_rtrancl)

   212 done

   213

   214 text{*Well-foundedness of image*}

   215 lemma wf_prod_fun_image: "[| wf r; inj f |] ==> wf(prod_fun f f  r)"

   216 apply (simp only: wf_eq_minimal, clarify)

   217 apply (case_tac "EX p. f p : Q")

   218 apply (erule_tac x = "{p. f p : Q}" in allE)

   219 apply (fast dest: inj_onD, blast)

   220 done

   221

   222

   223 subsubsection {* Well-Foundedness Results for Unions *}

   224

   225 lemma wf_union_compatible:

   226   assumes "wf R" "wf S"

   227   assumes "S O R \<subseteq> R"

   228   shows "wf (R \<union> S)"

   229 proof (rule wfI_min)

   230   fix x :: 'a and Q

   231   let ?Q' = "{x \<in> Q. \<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> Q}"

   232   assume "x \<in> Q"

   233   obtain a where "a \<in> ?Q'"

   234     by (rule wfE_min [OF wf R x \<in> Q]) blast

   235   with wf S

   236   obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'" by (erule wfE_min)

   237   {

   238     fix y assume "(y, z) \<in> S"

   239     then have "y \<notin> ?Q'" by (rule zmin)

   240

   241     have "y \<notin> Q"

   242     proof

   243       assume "y \<in> Q"

   244       with y \<notin> ?Q'

   245       obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto

   246       from (w, y) \<in> R (y, z) \<in> S have "(w, z) \<in> S O R" by (rule rel_compI)

   247       with S O R \<subseteq> R have "(w, z) \<in> R" ..

   248       with z \<in> ?Q' have "w \<notin> Q" by blast

   249       with w \<in> Q show False by contradiction

   250     qed

   251   }

   252   with z \<in> ?Q' show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<union> S \<longrightarrow> y \<notin> Q" by blast

   253 qed

   254

   255

   256 text {* Well-foundedness of indexed union with disjoint domains and ranges *}

   257

   258 lemma wf_UN: "[| ALL i:I. wf(r i);

   259          ALL i:I. ALL j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {}

   260       |] ==> wf(UN i:I. r i)"

   261 apply (simp only: wf_eq_minimal, clarify)

   262 apply (rename_tac A a, case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i")

   263  prefer 2

   264  apply force

   265 apply clarify

   266 apply (drule bspec, assumption)

   267 apply (erule_tac x="{a. a:A & (EX b:A. (b,a) : r i) }" in allE)

   268 apply (blast elim!: allE)

   269 done

   270

   271 lemmas wfP_SUP = wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}",

   272   to_pred SUP_UN_eq2 bot_empty_eq, simplified, standard]

   273

   274 lemma wf_Union:

   275  "[| ALL r:R. wf r;

   276      ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}

   277   |] ==> wf(Union R)"

   278 apply (simp add: Union_def)

   279 apply (blast intro: wf_UN)

   280 done

   281

   282 (*Intuition: we find an (R u S)-min element of a nonempty subset A

   283              by case distinction.

   284   1. There is a step a -R-> b with a,b : A.

   285      Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}.

   286      By definition, there is z':A s.t. z -R-> z'. Because z is R-min in the

   287      subset, z' must be R-min in A. Because z' has an R-predecessor, it cannot

   288      have an S-successor and is thus S-min in A as well.

   289   2. There is no such step.

   290      Pick an S-min element of A. In this case it must be an R-min

   291      element of A as well.

   292

   293 *)

   294 lemma wf_Un:

   295      "[| wf r; wf s; Domain r Int Range s = {} |] ==> wf(r Un s)"

   296   using wf_union_compatible[of s r]

   297   by (auto simp: Un_ac)

   298

   299 lemma wf_union_merge:

   300   "wf (R \<union> S) = wf (R O R \<union> R O S \<union> S)" (is "wf ?A = wf ?B")

   301 proof

   302   assume "wf ?A"

   303   with wf_trancl have wfT: "wf (?A^+)" .

   304   moreover have "?B \<subseteq> ?A^+"

   305     by (subst trancl_unfold, subst trancl_unfold) blast

   306   ultimately show "wf ?B" by (rule wf_subset)

   307 next

   308   assume "wf ?B"

   309

   310   show "wf ?A"

   311   proof (rule wfI_min)

   312     fix Q :: "'a set" and x

   313     assume "x \<in> Q"

   314

   315     with wf ?B

   316     obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q"

   317       by (erule wfE_min)

   318     then have A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q"

   319       and A2: "\<And>y. (y, z) \<in> R O S \<Longrightarrow> y \<notin> Q"

   320       and A3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q"

   321       by auto

   322

   323     show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> ?A \<longrightarrow> y \<notin> Q"

   324     proof (cases "\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q")

   325       case True

   326       with z \<in> Q A3 show ?thesis by blast

   327     next

   328       case False

   329       then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast

   330

   331       have "\<forall>y. (y, z') \<in> ?A \<longrightarrow> y \<notin> Q"

   332       proof (intro allI impI)

   333         fix y assume "(y, z') \<in> ?A"

   334         then show "y \<notin> Q"

   335         proof

   336           assume "(y, z') \<in> R"

   337           then have "(y, z) \<in> R O R" using (z', z) \<in> R ..

   338           with A1 show "y \<notin> Q" .

   339         next

   340           assume "(y, z') \<in> S"

   341           then have "(y, z) \<in> R O S" using  (z', z) \<in> R ..

   342           with A2 show "y \<notin> Q" .

   343         qed

   344       qed

   345       with z' \<in> Q show ?thesis ..

   346     qed

   347   qed

   348 qed

   349

   350 lemma wf_comp_self: "wf R = wf (R O R)"  -- {* special case *}

   351   by (rule wf_union_merge [where S = "{}", simplified])

   352

   353

   354 subsubsection {* acyclic *}

   355

   356 lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"

   357   by (simp add: acyclic_def)

   358

   359 lemma wf_acyclic: "wf r ==> acyclic r"

   360 apply (simp add: acyclic_def)

   361 apply (blast elim: wf_trancl [THEN wf_irrefl])

   362 done

   363

   364 lemmas wfP_acyclicP = wf_acyclic [to_pred]

   365

   366 lemma acyclic_insert [iff]:

   367      "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"

   368 apply (simp add: acyclic_def trancl_insert)

   369 apply (blast intro: rtrancl_trans)

   370 done

   371

   372 lemma acyclic_converse [iff]: "acyclic(r^-1) = acyclic r"

   373 by (simp add: acyclic_def trancl_converse)

   374

   375 lemmas acyclicP_converse [iff] = acyclic_converse [to_pred]

   376

   377 lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)"

   378 apply (simp add: acyclic_def antisym_def)

   379 apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)

   380 done

   381

   382 (* Other direction:

   383 acyclic = no loops

   384 antisym = only self loops

   385 Goalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r - Id)

   386 ==> antisym( r^* ) = acyclic(r - Id)";

   387 *)

   388

   389 lemma acyclic_subset: "[| acyclic s; r <= s |] ==> acyclic r"

   390 apply (simp add: acyclic_def)

   391 apply (blast intro: trancl_mono)

   392 done

   393

   394

   395 subsection{*Well-Founded Recursion*}

   396

   397 text{*cut*}

   398

   399 lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"

   400 by (simp add: expand_fun_eq cut_def)

   401

   402 lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"

   403 by (simp add: cut_def)

   404

   405 text{*Inductive characterization of wfrec combinator; for details see:

   406 John Harrison, "Inductive definitions: automation and application"*}

   407

   408 lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"

   409 apply (simp add: adm_wf_def)

   410 apply (erule_tac a=x in wf_induct)

   411 apply (rule ex1I)

   412 apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)

   413 apply (fast dest!: theI')

   414 apply (erule wfrec_rel.cases, simp)

   415 apply (erule allE, erule allE, erule allE, erule mp)

   416 apply (fast intro: the_equality [symmetric])

   417 done

   418

   419 lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"

   420 apply (simp add: adm_wf_def)

   421 apply (intro strip)

   422 apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)

   423 apply (rule refl)

   424 done

   425

   426 lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"

   427 apply (simp add: wfrec_def)

   428 apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)

   429 apply (rule wfrec_rel.wfrecI)

   430 apply (intro strip)

   431 apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])

   432 done

   433

   434

   435 text{** This form avoids giant explosions in proofs.  NOTE USE OF ==*}

   436 lemma def_wfrec: "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a"

   437 apply auto

   438 apply (blast intro: wfrec)

   439 done

   440

   441

   442 subsection {* Code generator setup *}

   443

   444 consts_code

   445   "wfrec"   ("\<module>wfrec?")

   446 attach {*

   447 fun wfrec f x = f (wfrec f) x;

   448 *}

   449

   450

   451 subsection{*Variants for TFL: the Recdef Package*}

   452

   453 lemma tfl_wf_induct: "ALL R. wf R -->

   454        (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"

   455 apply clarify

   456 apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)

   457 done

   458

   459 lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)"

   460 apply clarify

   461 apply (rule cut_apply, assumption)

   462 done

   463

   464 lemma tfl_wfrec:

   465      "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)"

   466 apply clarify

   467 apply (erule wfrec)

   468 done

   469

   470 subsection {*LEAST and wellorderings*}

   471

   472 text{* See also @{text wf_linord_ex_has_least} and its consequences in

   473  @{text Wellfounded_Relations.ML}*}

   474

   475 lemma wellorder_Least_lemma [rule_format]:

   476      "P (k::'a::wellorder) --> P (LEAST x. P(x)) & (LEAST x. P(x)) <= k"

   477 apply (rule_tac a = k in wf [THEN wf_induct])

   478 apply (rule impI)

   479 apply (rule classical)

   480 apply (rule_tac s = x in Least_equality [THEN ssubst], auto)

   481 apply (auto simp add: linorder_not_less [symmetric])

   482 done

   483

   484 lemmas LeastI   = wellorder_Least_lemma [THEN conjunct1, standard]

   485 lemmas Least_le = wellorder_Least_lemma [THEN conjunct2, standard]

   486

   487 -- "The following 3 lemmas are due to Brian Huffman"

   488 lemma LeastI_ex: "EX x::'a::wellorder. P x ==> P (Least P)"

   489 apply (erule exE)

   490 apply (erule LeastI)

   491 done

   492

   493 lemma LeastI2:

   494   "[| P (a::'a::wellorder); !!x. P x ==> Q x |] ==> Q (Least P)"

   495 by (blast intro: LeastI)

   496

   497 lemma LeastI2_ex:

   498   "[| EX a::'a::wellorder. P a; !!x. P x ==> Q x |] ==> Q (Least P)"

   499 by (blast intro: LeastI_ex)

   500

   501 lemma not_less_Least: "[| k < (LEAST x. P x) |] ==> ~P (k::'a::wellorder)"

   502 apply (simp (no_asm_use) add: linorder_not_le [symmetric])

   503 apply (erule contrapos_nn)

   504 apply (erule Least_le)

   505 done

   506

   507 subsection {* @{typ nat} is well-founded *}

   508

   509 lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++"

   510 proof (rule ext, rule ext, rule iffI)

   511   fix n m :: nat

   512   assume "m < n"

   513   then show "(\<lambda>m n. n = Suc m)^++ m n"

   514   proof (induct n)

   515     case 0 then show ?case by auto

   516   next

   517     case (Suc n) then show ?case

   518       by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl)

   519   qed

   520 next

   521   fix n m :: nat

   522   assume "(\<lambda>m n. n = Suc m)^++ m n"

   523   then show "m < n"

   524     by (induct n)

   525       (simp_all add: less_Suc_eq_le reflexive le_less)

   526 qed

   527

   528 definition

   529   pred_nat :: "(nat * nat) set" where

   530   "pred_nat = {(m, n). n = Suc m}"

   531

   532 definition

   533   less_than :: "(nat * nat) set" where

   534   "less_than = pred_nat^+"

   535

   536 lemma less_eq: "(m, n) \<in> pred_nat^+ \<longleftrightarrow> m < n"

   537   unfolding less_nat_rel pred_nat_def trancl_def by simp

   538

   539 lemma pred_nat_trancl_eq_le:

   540   "(m, n) \<in> pred_nat^* \<longleftrightarrow> m \<le> n"

   541   unfolding less_eq rtrancl_eq_or_trancl by auto

   542

   543 lemma wf_pred_nat: "wf pred_nat"

   544   apply (unfold wf_def pred_nat_def, clarify)

   545   apply (induct_tac x, blast+)

   546   done

   547

   548 lemma wf_less_than [iff]: "wf less_than"

   549   by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])

   550

   551 lemma trans_less_than [iff]: "trans less_than"

   552   by (simp add: less_than_def trans_trancl)

   553

   554 lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)"

   555   by (simp add: less_than_def less_eq)

   556

   557 lemma wf_less: "wf {(x, y::nat). x < y}"

   558   using wf_less_than by (simp add: less_than_def less_eq [symmetric])

   559

   560 text {* Complete induction, aka course-of-values induction *}

   561 lemma nat_less_induct:

   562   assumes "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n"

   563   apply (induct n rule: wf_induct [OF wf_pred_nat [THEN wf_trancl]])

   564   apply (rule assms)

   565   apply (unfold less_eq [symmetric], assumption)

   566   done

   567

   568 lemmas less_induct = nat_less_induct [rule_format, case_names less]

   569

   570 text {* Type @{typ nat} is a wellfounded order *}

   571

   572 instance nat :: wellorder

   573   by intro_classes

   574     (assumption |

   575       rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+

   576

   577 lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n"

   578   apply (rule nat_less_induct)

   579   apply (case_tac n)

   580   apply (case_tac [2] nat)

   581   apply (blast intro: less_trans)+

   582   done

   583

   584 text {* The method of infinite descent, frequently used in number theory.

   585 Provided by Roelof Oosterhuis.

   586 $P(n)$ is true for all $n\in\mathbb{N}$ if

   587 \begin{itemize}

   588   \item case 0'': given $n=0$ prove $P(n)$,

   589   \item case smaller'': given $n>0$ and $\neg P(n)$ prove there exists

   590         a smaller integer $m$ such that $\neg P(m)$.

   591 \end{itemize} *}

   592

   593 lemma infinite_descent0[case_names 0 smaller]:

   594   "\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n"

   595 by (induct n rule: less_induct, case_tac "n>0", auto)

   596

   597 text{* A compact version without explicit base case: *}

   598 lemma infinite_descent:

   599   "\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow>  \<exists>m<n. \<not>  P m \<rbrakk> \<Longrightarrow>  P n"

   600 by (induct n rule: less_induct, auto)

   601

   602 text {*

   603 Infinite descent using a mapping to $\mathbb{N}$:

   604 $P(x)$ is true for all $x\in D$ if there exists a $V: D \to \mathbb{N}$ and

   605 \begin{itemize}

   606 \item case 0'': given $V(x)=0$ prove $P(x)$,

   607 \item case smaller'': given $V(x)>0$ and $\neg P(x)$ prove there exists a $y \in D$ such that $V(y)<V(x)$ and $~\neg P(y)$.

   608 \end{itemize}

   609 NB: the proof also shows how to use the previous lemma. *}

   610

   611 corollary infinite_descent0_measure [case_names 0 smaller]:

   612   assumes A0: "!!x. V x = (0::nat) \<Longrightarrow> P x"

   613     and   A1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)"

   614   shows "P x"

   615 proof -

   616   obtain n where "n = V x" by auto

   617   moreover have "\<And>x. V x = n \<Longrightarrow> P x"

   618   proof (induct n rule: infinite_descent0)

   619     case 0 -- "i.e. $V(x) = 0$"

   620     with A0 show "P x" by auto

   621   next -- "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$"

   622     case (smaller n)

   623     then obtain x where vxn: "V x = n " and "V x > 0 \<and> \<not> P x" by auto

   624     with A1 obtain y where "V y < V x \<and> \<not> P y" by auto

   625     with vxn obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto

   626     then show ?case by auto

   627   qed

   628   ultimately show "P x" by auto

   629 qed

   630

   631 text{* Again, without explicit base case: *}

   632 lemma infinite_descent_measure:

   633 assumes "!!x. \<not> P x \<Longrightarrow> \<exists>y. (V::'a\<Rightarrow>nat) y < V x \<and> \<not> P y" shows "P x"

   634 proof -

   635   from assms obtain n where "n = V x" by auto

   636   moreover have "!!x. V x = n \<Longrightarrow> P x"

   637   proof (induct n rule: infinite_descent, auto)

   638     fix x assume "\<not> P x"

   639     with assms show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" by auto

   640   qed

   641   ultimately show "P x" by auto

   642 qed

   643

   644 text {* @{text LEAST} theorems for type @{typ nat}*}

   645

   646 lemma Least_Suc:

   647      "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"

   648   apply (case_tac "n", auto)

   649   apply (frule LeastI)

   650   apply (drule_tac P = "%x. P (Suc x) " in LeastI)

   651   apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")

   652   apply (erule_tac [2] Least_le)

   653   apply (case_tac "LEAST x. P x", auto)

   654   apply (drule_tac P = "%x. P (Suc x) " in Least_le)

   655   apply (blast intro: order_antisym)

   656   done

   657

   658 lemma Least_Suc2:

   659    "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"

   660   apply (erule (1) Least_Suc [THEN ssubst])

   661   apply simp

   662   done

   663

   664 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)"

   665   apply (cases n)

   666    apply blast

   667   apply (rule_tac x="LEAST k. P(k)" in exI)

   668   apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)

   669   done

   670

   671 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)"

   672   apply (cases n)

   673    apply blast

   674   apply (frule (1) ex_least_nat_le)

   675   apply (erule exE)

   676   apply (case_tac k)

   677    apply simp

   678   apply (rename_tac k1)

   679   apply (rule_tac x=k1 in exI)

   680   apply fastsimp

   681   done

   682

   683

   684 subsection {* size of a datatype value *}

   685

   686 use "Tools/function_package/size.ML"

   687

   688 setup Size.setup

   689

   690 lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"

   691   by (induct n) simp_all

   692

   693 end
`