src/HOL/Wellfounded.thy
author krauss
Fri May 23 17:19:24 2008 +0200 (2008-05-23)
changeset 26976 cf147f69b3df
parent 26803 0af0f674845d
child 27823 52971512d1a2
permissions -rw-r--r--
rearranged subsections
     1 (*  ID:         $Id$
     2     Author:     Tobias Nipkow
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Author:     Konrad Slind, Alexander Krauss
     5     Copyright   1992-2008  University of Cambridge and TU Muenchen
     6 *)
     7 
     8 header {*Well-founded Recursion*}
     9 
    10 theory Wellfounded
    11 imports Finite_Set Nat
    12 uses ("Tools/function_package/size.ML")
    13 begin
    14 
    15 subsection {* Basic Definitions *}
    16 
    17 inductive
    18   wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
    19   for R :: "('a * 'a) set"
    20   and F :: "('a => 'b) => 'a => 'b"
    21 where
    22   wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
    23             wfrec_rel R F x (F g x)"
    24 
    25 constdefs
    26   wf         :: "('a * 'a)set => bool"
    27   "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
    28 
    29   wfP :: "('a => 'a => bool) => bool"
    30   "wfP r == wf {(x, y). r x y}"
    31 
    32   acyclic :: "('a*'a)set => bool"
    33   "acyclic r == !x. (x,x) ~: r^+"
    34 
    35   cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
    36   "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
    37 
    38   adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
    39   "adm_wf R F == ALL f g x.
    40      (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
    41 
    42   wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
    43   [code func del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
    44 
    45 abbreviation acyclicP :: "('a => 'a => bool) => bool" where
    46   "acyclicP r == acyclic {(x, y). r x y}"
    47 
    48 class wellorder = linorder +
    49   assumes wf: "wf {(x, y). x < y}"
    50 
    51 
    52 lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
    53   by (simp add: wfP_def)
    54 
    55 lemma wfUNIVI: 
    56    "(!!P x. (ALL x. (ALL y. (y,x) : r --> P(y)) --> P(x)) ==> P(x)) ==> wf(r)"
    57   unfolding wf_def by blast
    58 
    59 lemmas wfPUNIVI = wfUNIVI [to_pred]
    60 
    61 text{*Restriction to domain @{term A} and range @{term B}.  If @{term r} is
    62     well-founded over their intersection, then @{term "wf r"}*}
    63 lemma wfI: 
    64  "[| r \<subseteq> A <*> B; 
    65      !!x P. [|\<forall>x. (\<forall>y. (y,x) : r --> P y) --> P x;  x : A; x : B |] ==> P x |]
    66   ==>  wf r"
    67   unfolding wf_def by blast
    68 
    69 lemma wf_induct: 
    70     "[| wf(r);           
    71         !!x.[| ALL y. (y,x): r --> P(y) |] ==> P(x)  
    72      |]  ==>  P(a)"
    73   unfolding wf_def by blast
    74 
    75 lemmas wfP_induct = wf_induct [to_pred]
    76 
    77 lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf]
    78 
    79 lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP]
    80 
    81 lemma wf_not_sym: "wf r ==> (a, x) : r ==> (x, a) ~: r"
    82   by (induct a arbitrary: x set: wf) blast
    83 
    84 (* [| wf r;  ~Z ==> (a,x) : r;  (x,a) ~: r ==> Z |] ==> Z *)
    85 lemmas wf_asym = wf_not_sym [elim_format]
    86 
    87 lemma wf_not_refl [simp]: "wf r ==> (a, a) ~: r"
    88   by (blast elim: wf_asym)
    89 
    90 (* [| wf r;  (a,a) ~: r ==> PROP W |] ==> PROP W *)
    91 lemmas wf_irrefl = wf_not_refl [elim_format]
    92 
    93 subsection {* Basic Results *}
    94 
    95 text{*transitive closure of a well-founded relation is well-founded! *}
    96 lemma wf_trancl:
    97   assumes "wf r"
    98   shows "wf (r^+)"
    99 proof -
   100   {
   101     fix P and x
   102     assume induct_step: "!!x. (!!y. (y, x) : r^+ ==> P y) ==> P x"
   103     have "P x"
   104     proof (rule induct_step)
   105       fix y assume "(y, x) : r^+"
   106       with `wf r` show "P y"
   107       proof (induct x arbitrary: y)
   108 	case (less x)
   109 	note hyp = `\<And>x' y'. (x', x) : r ==> (y', x') : r^+ ==> P y'`
   110 	from `(y, x) : r^+` show "P y"
   111 	proof cases
   112 	  case base
   113 	  show "P y"
   114 	  proof (rule induct_step)
   115 	    fix y' assume "(y', y) : r^+"
   116 	    with `(y, x) : r` show "P y'" by (rule hyp [of y y'])
   117 	  qed
   118 	next
   119 	  case step
   120 	  then obtain x' where "(x', x) : r" and "(y, x') : r^+" by simp
   121 	  then show "P y" by (rule hyp [of x' y])
   122 	qed
   123       qed
   124     qed
   125   } then show ?thesis unfolding wf_def by blast
   126 qed
   127 
   128 lemmas wfP_trancl = wf_trancl [to_pred]
   129 
   130 lemma wf_converse_trancl: "wf (r^-1) ==> wf ((r^+)^-1)"
   131   apply (subst trancl_converse [symmetric])
   132   apply (erule wf_trancl)
   133   done
   134 
   135 
   136 text{*Minimal-element characterization of well-foundedness*}
   137 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))"
   138 proof (intro iffI strip)
   139   fix Q :: "'a set" and x
   140   assume "wf r" and "x \<in> Q"
   141   then show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q"
   142     unfolding wf_def
   143     by (blast dest: spec [of _ "%x. x\<in>Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y,z) \<in> r \<longrightarrow> y\<notin>Q)"]) 
   144 next
   145   assume 1: "\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)"
   146   show "wf r"
   147   proof (rule wfUNIVI)
   148     fix P :: "'a \<Rightarrow> bool" and x
   149     assume 2: "\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x"
   150     let ?Q = "{x. \<not> P x}"
   151     have "x \<in> ?Q \<longrightarrow> (\<exists>z \<in> ?Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> ?Q)"
   152       by (rule 1 [THEN spec, THEN spec])
   153     then have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> (\<forall>y. (y, z) \<in> r \<longrightarrow> P y))" by simp
   154     with 2 have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> P z)" by fast
   155     then show "P x" by simp
   156   qed
   157 qed
   158 
   159 lemma wfE_min: 
   160   assumes "wf R" "x \<in> Q"
   161   obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q"
   162   using assms unfolding wf_eq_minimal by blast
   163 
   164 lemma wfI_min:
   165   "(\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q)
   166   \<Longrightarrow> wf R"
   167   unfolding wf_eq_minimal by blast
   168 
   169 lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
   170 
   171 text {* Well-foundedness of subsets *}
   172 lemma wf_subset: "[| wf(r);  p<=r |] ==> wf(p)"
   173   apply (simp (no_asm_use) add: wf_eq_minimal)
   174   apply fast
   175   done
   176 
   177 lemmas wfP_subset = wf_subset [to_pred]
   178 
   179 text {* Well-foundedness of the empty relation *}
   180 lemma wf_empty [iff]: "wf({})"
   181   by (simp add: wf_def)
   182 
   183 lemmas wfP_empty [iff] =
   184   wf_empty [to_pred bot_empty_eq2, simplified bot_fun_eq bot_bool_eq]
   185 
   186 lemma wf_Int1: "wf r ==> wf (r Int r')"
   187   apply (erule wf_subset)
   188   apply (rule Int_lower1)
   189   done
   190 
   191 lemma wf_Int2: "wf r ==> wf (r' Int r)"
   192   apply (erule wf_subset)
   193   apply (rule Int_lower2)
   194   done  
   195 
   196 text{*Well-foundedness of insert*}
   197 lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"
   198 apply (rule iffI)
   199  apply (blast elim: wf_trancl [THEN wf_irrefl]
   200               intro: rtrancl_into_trancl1 wf_subset 
   201                      rtrancl_mono [THEN [2] rev_subsetD])
   202 apply (simp add: wf_eq_minimal, safe)
   203 apply (rule allE, assumption, erule impE, blast) 
   204 apply (erule bexE)
   205 apply (rename_tac "a", case_tac "a = x")
   206  prefer 2
   207 apply blast 
   208 apply (case_tac "y:Q")
   209  prefer 2 apply blast
   210 apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE)
   211  apply assumption
   212 apply (erule_tac V = "ALL Q. (EX x. x : Q) --> ?P Q" in thin_rl) 
   213   --{*essential for speed*}
   214 txt{*Blast with new substOccur fails*}
   215 apply (fast intro: converse_rtrancl_into_rtrancl)
   216 done
   217 
   218 text{*Well-foundedness of image*}
   219 lemma wf_prod_fun_image: "[| wf r; inj f |] ==> wf(prod_fun f f ` r)"
   220 apply (simp only: wf_eq_minimal, clarify)
   221 apply (case_tac "EX p. f p : Q")
   222 apply (erule_tac x = "{p. f p : Q}" in allE)
   223 apply (fast dest: inj_onD, blast)
   224 done
   225 
   226 
   227 subsection {* Well-Foundedness Results for Unions *}
   228 
   229 lemma wf_union_compatible:
   230   assumes "wf R" "wf S"
   231   assumes "S O R \<subseteq> R"
   232   shows "wf (R \<union> S)"
   233 proof (rule wfI_min)
   234   fix x :: 'a and Q 
   235   let ?Q' = "{x \<in> Q. \<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> Q}"
   236   assume "x \<in> Q"
   237   obtain a where "a \<in> ?Q'"
   238     by (rule wfE_min [OF `wf R` `x \<in> Q`]) blast
   239   with `wf S`
   240   obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'" by (erule wfE_min)
   241   { 
   242     fix y assume "(y, z) \<in> S"
   243     then have "y \<notin> ?Q'" by (rule zmin)
   244 
   245     have "y \<notin> Q"
   246     proof 
   247       assume "y \<in> Q"
   248       with `y \<notin> ?Q'` 
   249       obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
   250       from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> S O R" by (rule rel_compI)
   251       with `S O R \<subseteq> R` have "(w, z) \<in> R" ..
   252       with `z \<in> ?Q'` have "w \<notin> Q" by blast 
   253       with `w \<in> Q` show False by contradiction
   254     qed
   255   }
   256   with `z \<in> ?Q'` show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<union> S \<longrightarrow> y \<notin> Q" by blast
   257 qed
   258 
   259 
   260 text {* Well-foundedness of indexed union with disjoint domains and ranges *}
   261 
   262 lemma wf_UN: "[| ALL i:I. wf(r i);  
   263          ALL i:I. ALL j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {}  
   264       |] ==> wf(UN i:I. r i)"
   265 apply (simp only: wf_eq_minimal, clarify)
   266 apply (rename_tac A a, case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i")
   267  prefer 2
   268  apply force 
   269 apply clarify
   270 apply (drule bspec, assumption)  
   271 apply (erule_tac x="{a. a:A & (EX b:A. (b,a) : r i) }" in allE)
   272 apply (blast elim!: allE)  
   273 done
   274 
   275 lemmas wfP_SUP = wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}",
   276   to_pred SUP_UN_eq2 bot_empty_eq pred_equals_eq, simplified, standard]
   277 
   278 lemma wf_Union: 
   279  "[| ALL r:R. wf r;  
   280      ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}  
   281   |] ==> wf(Union R)"
   282 apply (simp add: Union_def)
   283 apply (blast intro: wf_UN)
   284 done
   285 
   286 (*Intuition: we find an (R u S)-min element of a nonempty subset A
   287              by case distinction.
   288   1. There is a step a -R-> b with a,b : A.
   289      Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}.
   290      By definition, there is z':A s.t. z -R-> z'. Because z is R-min in the
   291      subset, z' must be R-min in A. Because z' has an R-predecessor, it cannot
   292      have an S-successor and is thus S-min in A as well.
   293   2. There is no such step.
   294      Pick an S-min element of A. In this case it must be an R-min
   295      element of A as well.
   296 
   297 *)
   298 lemma wf_Un:
   299      "[| wf r; wf s; Domain r Int Range s = {} |] ==> wf(r Un s)"
   300   using wf_union_compatible[of s r] 
   301   by (auto simp: Un_ac)
   302 
   303 lemma wf_union_merge: 
   304   "wf (R \<union> S) = wf (R O R \<union> R O S \<union> S)" (is "wf ?A = wf ?B")
   305 proof
   306   assume "wf ?A"
   307   with wf_trancl have wfT: "wf (?A^+)" .
   308   moreover have "?B \<subseteq> ?A^+"
   309     by (subst trancl_unfold, subst trancl_unfold) blast
   310   ultimately show "wf ?B" by (rule wf_subset)
   311 next
   312   assume "wf ?B"
   313 
   314   show "wf ?A"
   315   proof (rule wfI_min)
   316     fix Q :: "'a set" and x 
   317     assume "x \<in> Q"
   318 
   319     with `wf ?B`
   320     obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" 
   321       by (erule wfE_min)
   322     then have A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q"
   323       and A2: "\<And>y. (y, z) \<in> R O S \<Longrightarrow> y \<notin> Q"
   324       and A3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q"
   325       by auto
   326     
   327     show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> ?A \<longrightarrow> y \<notin> Q"
   328     proof (cases "\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q")
   329       case True
   330       with `z \<in> Q` A3 show ?thesis by blast
   331     next
   332       case False 
   333       then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast
   334 
   335       have "\<forall>y. (y, z') \<in> ?A \<longrightarrow> y \<notin> Q"
   336       proof (intro allI impI)
   337         fix y assume "(y, z') \<in> ?A"
   338         then show "y \<notin> Q"
   339         proof
   340           assume "(y, z') \<in> R" 
   341           then have "(y, z) \<in> R O R" using `(z', z) \<in> R` ..
   342           with A1 show "y \<notin> Q" .
   343         next
   344           assume "(y, z') \<in> S" 
   345           then have "(y, z) \<in> R O S" using  `(z', z) \<in> R` ..
   346           with A2 show "y \<notin> Q" .
   347         qed
   348       qed
   349       with `z' \<in> Q` show ?thesis ..
   350     qed
   351   qed
   352 qed
   353 
   354 lemma wf_comp_self: "wf R = wf (R O R)"  -- {* special case *}
   355   by (rule wf_union_merge [where S = "{}", simplified])
   356 
   357 
   358 subsubsection {* acyclic *}
   359 
   360 lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
   361   by (simp add: acyclic_def)
   362 
   363 lemma wf_acyclic: "wf r ==> acyclic r"
   364 apply (simp add: acyclic_def)
   365 apply (blast elim: wf_trancl [THEN wf_irrefl])
   366 done
   367 
   368 lemmas wfP_acyclicP = wf_acyclic [to_pred]
   369 
   370 lemma acyclic_insert [iff]:
   371      "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"
   372 apply (simp add: acyclic_def trancl_insert)
   373 apply (blast intro: rtrancl_trans)
   374 done
   375 
   376 lemma acyclic_converse [iff]: "acyclic(r^-1) = acyclic r"
   377 by (simp add: acyclic_def trancl_converse)
   378 
   379 lemmas acyclicP_converse [iff] = acyclic_converse [to_pred]
   380 
   381 lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)"
   382 apply (simp add: acyclic_def antisym_def)
   383 apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)
   384 done
   385 
   386 (* Other direction:
   387 acyclic = no loops
   388 antisym = only self loops
   389 Goalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r - Id)
   390 ==> antisym( r^* ) = acyclic(r - Id)";
   391 *)
   392 
   393 lemma acyclic_subset: "[| acyclic s; r <= s |] ==> acyclic r"
   394 apply (simp add: acyclic_def)
   395 apply (blast intro: trancl_mono)
   396 done
   397 
   398 text{* Wellfoundedness of finite acyclic relations*}
   399 
   400 lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r"
   401 apply (erule finite_induct, blast)
   402 apply (simp (no_asm_simp) only: split_tupled_all)
   403 apply simp
   404 done
   405 
   406 lemma finite_acyclic_wf_converse: "[|finite r; acyclic r|] ==> wf (r^-1)"
   407 apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])
   408 apply (erule acyclic_converse [THEN iffD2])
   409 done
   410 
   411 lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r"
   412 by (blast intro: finite_acyclic_wf wf_acyclic)
   413 
   414 
   415 subsection{*Well-Founded Recursion*}
   416 
   417 text{*cut*}
   418 
   419 lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
   420 by (simp add: expand_fun_eq cut_def)
   421 
   422 lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
   423 by (simp add: cut_def)
   424 
   425 text{*Inductive characterization of wfrec combinator; for details see:  
   426 John Harrison, "Inductive definitions: automation and application"*}
   427 
   428 lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
   429 apply (simp add: adm_wf_def)
   430 apply (erule_tac a=x in wf_induct) 
   431 apply (rule ex1I)
   432 apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
   433 apply (fast dest!: theI')
   434 apply (erule wfrec_rel.cases, simp)
   435 apply (erule allE, erule allE, erule allE, erule mp)
   436 apply (fast intro: the_equality [symmetric])
   437 done
   438 
   439 lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
   440 apply (simp add: adm_wf_def)
   441 apply (intro strip)
   442 apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
   443 apply (rule refl)
   444 done
   445 
   446 lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
   447 apply (simp add: wfrec_def)
   448 apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
   449 apply (rule wfrec_rel.wfrecI)
   450 apply (intro strip)
   451 apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
   452 done
   453 
   454 subsection {* Code generator setup *}
   455 
   456 consts_code
   457   "wfrec"   ("\<module>wfrec?")
   458 attach {*
   459 fun wfrec f x = f (wfrec f) x;
   460 *}
   461 
   462 
   463 subsection {*LEAST and wellorderings*}
   464 
   465 text{* See also @{text wf_linord_ex_has_least} and its consequences in
   466  @{text Wellfounded_Relations.ML}*}
   467 
   468 lemma wellorder_Least_lemma [rule_format]:
   469      "P (k::'a::wellorder) --> P (LEAST x. P(x)) & (LEAST x. P(x)) <= k"
   470 apply (rule_tac a = k in wf [THEN wf_induct])
   471 apply (rule impI)
   472 apply (rule classical)
   473 apply (rule_tac s = x in Least_equality [THEN ssubst], auto)
   474 apply (auto simp add: linorder_not_less [symmetric])
   475 done
   476 
   477 lemmas LeastI   = wellorder_Least_lemma [THEN conjunct1, standard]
   478 lemmas Least_le = wellorder_Least_lemma [THEN conjunct2, standard]
   479 
   480 -- "The following 3 lemmas are due to Brian Huffman"
   481 lemma LeastI_ex: "EX x::'a::wellorder. P x ==> P (Least P)"
   482 apply (erule exE)
   483 apply (erule LeastI)
   484 done
   485 
   486 lemma LeastI2:
   487   "[| P (a::'a::wellorder); !!x. P x ==> Q x |] ==> Q (Least P)"
   488 by (blast intro: LeastI)
   489 
   490 lemma LeastI2_ex:
   491   "[| EX a::'a::wellorder. P a; !!x. P x ==> Q x |] ==> Q (Least P)"
   492 by (blast intro: LeastI_ex)
   493 
   494 lemma not_less_Least: "[| k < (LEAST x. P x) |] ==> ~P (k::'a::wellorder)"
   495 apply (simp (no_asm_use) add: linorder_not_le [symmetric])
   496 apply (erule contrapos_nn)
   497 apply (erule Least_le)
   498 done
   499 
   500 subsection {* @{typ nat} is well-founded *}
   501 
   502 lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++"
   503 proof (rule ext, rule ext, rule iffI)
   504   fix n m :: nat
   505   assume "m < n"
   506   then show "(\<lambda>m n. n = Suc m)^++ m n"
   507   proof (induct n)
   508     case 0 then show ?case by auto
   509   next
   510     case (Suc n) then show ?case
   511       by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl)
   512   qed
   513 next
   514   fix n m :: nat
   515   assume "(\<lambda>m n. n = Suc m)^++ m n"
   516   then show "m < n"
   517     by (induct n)
   518       (simp_all add: less_Suc_eq_le reflexive le_less)
   519 qed
   520 
   521 definition
   522   pred_nat :: "(nat * nat) set" where
   523   "pred_nat = {(m, n). n = Suc m}"
   524 
   525 definition
   526   less_than :: "(nat * nat) set" where
   527   "less_than = pred_nat^+"
   528 
   529 lemma less_eq: "(m, n) \<in> pred_nat^+ \<longleftrightarrow> m < n"
   530   unfolding less_nat_rel pred_nat_def trancl_def by simp
   531 
   532 lemma pred_nat_trancl_eq_le:
   533   "(m, n) \<in> pred_nat^* \<longleftrightarrow> m \<le> n"
   534   unfolding less_eq rtrancl_eq_or_trancl by auto
   535 
   536 lemma wf_pred_nat: "wf pred_nat"
   537   apply (unfold wf_def pred_nat_def, clarify)
   538   apply (induct_tac x, blast+)
   539   done
   540 
   541 lemma wf_less_than [iff]: "wf less_than"
   542   by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])
   543 
   544 lemma trans_less_than [iff]: "trans less_than"
   545   by (simp add: less_than_def trans_trancl)
   546 
   547 lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)"
   548   by (simp add: less_than_def less_eq)
   549 
   550 lemma wf_less: "wf {(x, y::nat). x < y}"
   551   using wf_less_than by (simp add: less_than_def less_eq [symmetric])
   552 
   553 text {* Type @{typ nat} is a wellfounded order *}
   554 
   555 instance nat :: wellorder
   556   by intro_classes
   557     (assumption |
   558       rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+
   559 
   560 text {* @{text LEAST} theorems for type @{typ nat}*}
   561 
   562 lemma Least_Suc:
   563      "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
   564   apply (case_tac "n", auto)
   565   apply (frule LeastI)
   566   apply (drule_tac P = "%x. P (Suc x) " in LeastI)
   567   apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
   568   apply (erule_tac [2] Least_le)
   569   apply (case_tac "LEAST x. P x", auto)
   570   apply (drule_tac P = "%x. P (Suc x) " in Least_le)
   571   apply (blast intro: order_antisym)
   572   done
   573 
   574 lemma Least_Suc2:
   575    "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
   576   apply (erule (1) Least_Suc [THEN ssubst])
   577   apply simp
   578   done
   579 
   580 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)"
   581   apply (cases n)
   582    apply blast
   583   apply (rule_tac x="LEAST k. P(k)" in exI)
   584   apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
   585   done
   586 
   587 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)"
   588   apply (cases n)
   589    apply blast
   590   apply (frule (1) ex_least_nat_le)
   591   apply (erule exE)
   592   apply (case_tac k)
   593    apply simp
   594   apply (rename_tac k1)
   595   apply (rule_tac x=k1 in exI)
   596   apply fastsimp
   597   done
   598 
   599 
   600 subsection {* Accessible Part *}
   601 
   602 text {*
   603  Inductive definition of the accessible part @{term "acc r"} of a
   604  relation; see also \cite{paulin-tlca}.
   605 *}
   606 
   607 inductive_set
   608   acc :: "('a * 'a) set => 'a set"
   609   for r :: "('a * 'a) set"
   610   where
   611     accI: "(!!y. (y, x) : r ==> y : acc r) ==> x : acc r"
   612 
   613 abbreviation
   614   termip :: "('a => 'a => bool) => 'a => bool" where
   615   "termip r == accp (r\<inverse>\<inverse>)"
   616 
   617 abbreviation
   618   termi :: "('a * 'a) set => 'a set" where
   619   "termi r == acc (r\<inverse>)"
   620 
   621 lemmas accpI = accp.accI
   622 
   623 text {* Induction rules *}
   624 
   625 theorem accp_induct:
   626   assumes major: "accp r a"
   627   assumes hyp: "!!x. accp r x ==> \<forall>y. r y x --> P y ==> P x"
   628   shows "P a"
   629   apply (rule major [THEN accp.induct])
   630   apply (rule hyp)
   631    apply (rule accp.accI)
   632    apply fast
   633   apply fast
   634   done
   635 
   636 theorems accp_induct_rule = accp_induct [rule_format, induct set: accp]
   637 
   638 theorem accp_downward: "accp r b ==> r a b ==> accp r a"
   639   apply (erule accp.cases)
   640   apply fast
   641   done
   642 
   643 lemma not_accp_down:
   644   assumes na: "\<not> accp R x"
   645   obtains z where "R z x" and "\<not> accp R z"
   646 proof -
   647   assume a: "\<And>z. \<lbrakk>R z x; \<not> accp R z\<rbrakk> \<Longrightarrow> thesis"
   648 
   649   show thesis
   650   proof (cases "\<forall>z. R z x \<longrightarrow> accp R z")
   651     case True
   652     hence "\<And>z. R z x \<Longrightarrow> accp R z" by auto
   653     hence "accp R x"
   654       by (rule accp.accI)
   655     with na show thesis ..
   656   next
   657     case False then obtain z where "R z x" and "\<not> accp R z"
   658       by auto
   659     with a show thesis .
   660   qed
   661 qed
   662 
   663 lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a ==> accp r a --> accp r b"
   664   apply (erule rtranclp_induct)
   665    apply blast
   666   apply (blast dest: accp_downward)
   667   done
   668 
   669 theorem accp_downwards: "accp r a ==> r\<^sup>*\<^sup>* b a ==> accp r b"
   670   apply (blast dest: accp_downwards_aux)
   671   done
   672 
   673 theorem accp_wfPI: "\<forall>x. accp r x ==> wfP r"
   674   apply (rule wfPUNIVI)
   675   apply (induct_tac P x rule: accp_induct)
   676    apply blast
   677   apply blast
   678   done
   679 
   680 theorem accp_wfPD: "wfP r ==> accp r x"
   681   apply (erule wfP_induct_rule)
   682   apply (rule accp.accI)
   683   apply blast
   684   done
   685 
   686 theorem wfP_accp_iff: "wfP r = (\<forall>x. accp r x)"
   687   apply (blast intro: accp_wfPI dest: accp_wfPD)
   688   done
   689 
   690 
   691 text {* Smaller relations have bigger accessible parts: *}
   692 
   693 lemma accp_subset:
   694   assumes sub: "R1 \<le> R2"
   695   shows "accp R2 \<le> accp R1"
   696 proof (rule predicate1I)
   697   fix x assume "accp R2 x"
   698   then show "accp R1 x"
   699   proof (induct x)
   700     fix x
   701     assume ih: "\<And>y. R2 y x \<Longrightarrow> accp R1 y"
   702     with sub show "accp R1 x"
   703       by (blast intro: accp.accI)
   704   qed
   705 qed
   706 
   707 
   708 text {* This is a generalized induction theorem that works on
   709   subsets of the accessible part. *}
   710 
   711 lemma accp_subset_induct:
   712   assumes subset: "D \<le> accp R"
   713     and dcl: "\<And>x z. \<lbrakk>D x; R z x\<rbrakk> \<Longrightarrow> D z"
   714     and "D x"
   715     and istep: "\<And>x. \<lbrakk>D x; (\<And>z. R z x \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
   716   shows "P x"
   717 proof -
   718   from subset and `D x`
   719   have "accp R x" ..
   720   then show "P x" using `D x`
   721   proof (induct x)
   722     fix x
   723     assume "D x"
   724       and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y"
   725     with dcl and istep show "P x" by blast
   726   qed
   727 qed
   728 
   729 
   730 text {* Set versions of the above theorems *}
   731 
   732 lemmas acc_induct = accp_induct [to_set]
   733 
   734 lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc]
   735 
   736 lemmas acc_downward = accp_downward [to_set]
   737 
   738 lemmas not_acc_down = not_accp_down [to_set]
   739 
   740 lemmas acc_downwards_aux = accp_downwards_aux [to_set]
   741 
   742 lemmas acc_downwards = accp_downwards [to_set]
   743 
   744 lemmas acc_wfI = accp_wfPI [to_set]
   745 
   746 lemmas acc_wfD = accp_wfPD [to_set]
   747 
   748 lemmas wf_acc_iff = wfP_accp_iff [to_set]
   749 
   750 lemmas acc_subset = accp_subset [to_set pred_subset_eq]
   751 
   752 lemmas acc_subset_induct = accp_subset_induct [to_set pred_subset_eq]
   753 
   754 
   755 subsection {* Tools for building wellfounded relations *}
   756 
   757 text {* Inverse Image *}
   758 
   759 lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))"
   760 apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal)
   761 apply clarify
   762 apply (subgoal_tac "EX (w::'b) . w : {w. EX (x::'a) . x: Q & (f x = w) }")
   763 prefer 2 apply (blast del: allE)
   764 apply (erule allE)
   765 apply (erule (1) notE impE)
   766 apply blast
   767 done
   768 
   769 lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
   770   by (auto simp:inv_image_def)
   771 
   772 text {* Measure functions into @{typ nat} *}
   773 
   774 definition measure :: "('a => nat) => ('a * 'a)set"
   775 where "measure == inv_image less_than"
   776 
   777 lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)"
   778   by (simp add:measure_def)
   779 
   780 lemma wf_measure [iff]: "wf (measure f)"
   781 apply (unfold measure_def)
   782 apply (rule wf_less_than [THEN wf_inv_image])
   783 done
   784 
   785 text{* Lexicographic combinations *}
   786 
   787 definition
   788  lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
   789                (infixr "<*lex*>" 80)
   790 where
   791     "ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
   792 
   793 lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
   794 apply (unfold wf_def lex_prod_def) 
   795 apply (rule allI, rule impI)
   796 apply (simp (no_asm_use) only: split_paired_All)
   797 apply (drule spec, erule mp) 
   798 apply (rule allI, rule impI)
   799 apply (drule spec, erule mp, blast) 
   800 done
   801 
   802 lemma in_lex_prod[simp]: 
   803   "(((a,b),(a',b')): r <*lex*> s) = ((a,a'): r \<or> (a = a' \<and> (b, b') : s))"
   804   by (auto simp:lex_prod_def)
   805 
   806 text{* @{term "op <*lex*>"} preserves transitivity *}
   807 
   808 lemma trans_lex_prod [intro!]: 
   809     "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
   810 by (unfold trans_def lex_prod_def, blast) 
   811 
   812 text {* lexicographic combinations with measure functions *}
   813 
   814 definition 
   815   mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
   816 where
   817   "f <*mlex*> R = inv_image (less_than <*lex*> R) (%x. (f x, x))"
   818 
   819 lemma wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)"
   820 unfolding mlex_prod_def
   821 by auto
   822 
   823 lemma mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
   824 unfolding mlex_prod_def by simp
   825 
   826 lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
   827 unfolding mlex_prod_def by auto
   828 
   829 text {* proper subset relation on finite sets *}
   830 
   831 definition finite_psubset  :: "('a set * 'a set) set"
   832 where "finite_psubset == {(A,B). A < B & finite B}"
   833 
   834 lemma wf_finite_psubset: "wf(finite_psubset)"
   835 apply (unfold finite_psubset_def)
   836 apply (rule wf_measure [THEN wf_subset])
   837 apply (simp add: measure_def inv_image_def less_than_def less_eq)
   838 apply (fast elim!: psubset_card_mono)
   839 done
   840 
   841 lemma trans_finite_psubset: "trans finite_psubset"
   842 by (simp add: finite_psubset_def less_le trans_def, blast)
   843 
   844 
   845 
   846 
   847 text {*Wellfoundedness of @{text same_fst}*}
   848 
   849 definition
   850  same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
   851 where
   852     "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
   853    --{*For @{text rec_def} declarations where the first n parameters
   854        stay unchanged in the recursive call. 
   855        See @{text "Library/While_Combinator.thy"} for an application.*}
   856 
   857 lemma same_fstI [intro!]:
   858      "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
   859 by (simp add: same_fst_def)
   860 
   861 lemma wf_same_fst:
   862   assumes prem: "(!!x. P x ==> wf(R x))"
   863   shows "wf(same_fst P R)"
   864 apply (simp cong del: imp_cong add: wf_def same_fst_def)
   865 apply (intro strip)
   866 apply (rename_tac a b)
   867 apply (case_tac "wf (R a)")
   868  apply (erule_tac a = b in wf_induct, blast)
   869 apply (blast intro: prem)
   870 done
   871 
   872 
   873 subsection{*Weakly decreasing sequences (w.r.t. some well-founded order) 
   874    stabilize.*}
   875 
   876 text{*This material does not appear to be used any longer.*}
   877 
   878 lemma lemma1: "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*"
   879 apply (induct_tac "k", simp_all)
   880 apply (blast intro: rtrancl_trans)
   881 done
   882 
   883 lemma lemma2: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
   884       ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))"
   885 apply (erule wf_induct, clarify)
   886 apply (case_tac "EX j. (f (m+j), f m) : r^+")
   887  apply clarify
   888  apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ")
   889   apply clarify
   890   apply (rule_tac x = "j+i" in exI)
   891   apply (simp add: add_ac, blast)
   892 apply (rule_tac x = 0 in exI, clarsimp)
   893 apply (drule_tac i = m and k = k in lemma1)
   894 apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
   895 done
   896 
   897 lemma wf_weak_decr_stable: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
   898       ==> EX i. ALL k. f (i+k) = f i"
   899 apply (drule_tac x = 0 in lemma2 [THEN spec], auto)
   900 done
   901 
   902 (* special case of the theorem above: <= *)
   903 lemma weak_decr_stable:
   904      "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i"
   905 apply (rule_tac r = pred_nat in wf_weak_decr_stable)
   906 apply (simp add: pred_nat_trancl_eq_le)
   907 apply (intro wf_trancl wf_pred_nat)
   908 done
   909 
   910 
   911 subsection {* size of a datatype value *}
   912 
   913 use "Tools/function_package/size.ML"
   914 
   915 setup Size.setup
   916 
   917 lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
   918   by (induct n) simp_all
   919 
   920 
   921 end