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