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