src/HOL/Wellfounded.thy
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (22 months ago)
changeset 66924 b4d4027f743b
parent 64632 9df24b8b6c0a
child 66952 80985b62029d
permissions -rw-r--r--
more permissive;
     1 (*  Title:      HOL/Wellfounded.thy
     2     Author:     Tobias Nipkow
     3     Author:     Lawrence C Paulson
     4     Author:     Konrad Slind
     5     Author:     Alexander Krauss
     6     Author:     Andrei Popescu, TU Muenchen
     7 *)
     8 
     9 section \<open>Well-founded Recursion\<close>
    10 
    11 theory Wellfounded
    12   imports Transitive_Closure
    13 begin
    14 
    15 subsection \<open>Basic Definitions\<close>
    16 
    17 definition wf :: "('a \<times> 'a) set \<Rightarrow> bool"
    18   where "wf r \<longleftrightarrow> (\<forall>P. (\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> (\<forall>x. P x))"
    19 
    20 definition wfP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
    21   where "wfP r \<longleftrightarrow> wf {(x, y). r x y}"
    22 
    23 lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
    24   by (simp add: wfP_def)
    25 
    26 lemma wfUNIVI: "(\<And>P x. (\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<Longrightarrow> P x) \<Longrightarrow> wf r"
    27   unfolding wf_def by blast
    28 
    29 lemmas wfPUNIVI = wfUNIVI [to_pred]
    30 
    31 text \<open>Restriction to domain \<open>A\<close> and range \<open>B\<close>.
    32   If \<open>r\<close> is well-founded over their intersection, then \<open>wf r\<close>.\<close>
    33 lemma wfI:
    34   assumes "r \<subseteq> A \<times> B"
    35     and "\<And>x P. \<lbrakk>\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x;  x \<in> A; x \<in> B\<rbrakk> \<Longrightarrow> P x"
    36   shows "wf r"
    37   using assms unfolding wf_def by blast
    38 
    39 lemma wf_induct:
    40   assumes "wf r"
    41     and "\<And>x. \<forall>y. (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x"
    42   shows "P a"
    43   using assms unfolding wf_def by blast
    44 
    45 lemmas wfP_induct = wf_induct [to_pred]
    46 
    47 lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf]
    48 
    49 lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP]
    50 
    51 lemma wf_not_sym: "wf r \<Longrightarrow> (a, x) \<in> r \<Longrightarrow> (x, a) \<notin> r"
    52   by (induct a arbitrary: x set: wf) blast
    53 
    54 lemma wf_asym:
    55   assumes "wf r" "(a, x) \<in> r"
    56   obtains "(x, a) \<notin> r"
    57   by (drule wf_not_sym[OF assms])
    58 
    59 lemma wf_not_refl [simp]: "wf r \<Longrightarrow> (a, a) \<notin> r"
    60   by (blast elim: wf_asym)
    61 
    62 lemma wf_irrefl:
    63   assumes "wf r"
    64   obtains "(a, a) \<notin> r"
    65   by (drule wf_not_refl[OF assms])
    66 
    67 lemma wf_wellorderI:
    68   assumes wf: "wf {(x::'a::ord, y). x < y}"
    69     and lin: "OFCLASS('a::ord, linorder_class)"
    70   shows "OFCLASS('a::ord, wellorder_class)"
    71   using lin
    72   apply (rule wellorder_class.intro)
    73   apply (rule class.wellorder_axioms.intro)
    74   apply (rule wf_induct_rule [OF wf])
    75   apply simp
    76   done
    77 
    78 lemma (in wellorder) wf: "wf {(x, y). x < y}"
    79   unfolding wf_def by (blast intro: less_induct)
    80 
    81 
    82 subsection \<open>Basic Results\<close>
    83 
    84 text \<open>Point-free characterization of well-foundedness\<close>
    85 
    86 lemma wfE_pf:
    87   assumes wf: "wf R"
    88     and a: "A \<subseteq> R `` A"
    89   shows "A = {}"
    90 proof -
    91   from wf have "x \<notin> A" for x
    92   proof induct
    93     fix x assume "\<And>y. (y, x) \<in> R \<Longrightarrow> y \<notin> A"
    94     then have "x \<notin> R `` A" by blast
    95     with a show "x \<notin> A" by blast
    96   qed
    97   then show ?thesis by auto
    98 qed
    99 
   100 lemma wfI_pf:
   101   assumes a: "\<And>A. A \<subseteq> R `` A \<Longrightarrow> A = {}"
   102   shows "wf R"
   103 proof (rule wfUNIVI)
   104   fix P :: "'a \<Rightarrow> bool" and x
   105   let ?A = "{x. \<not> P x}"
   106   assume "\<forall>x. (\<forall>y. (y, x) \<in> R \<longrightarrow> P y) \<longrightarrow> P x"
   107   then have "?A \<subseteq> R `` ?A" by blast
   108   with a show "P x" by blast
   109 qed
   110 
   111 
   112 subsubsection \<open>Minimal-element characterization of well-foundedness\<close>
   113 
   114 lemma wfE_min:
   115   assumes wf: "wf R" and Q: "x \<in> Q"
   116   obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q"
   117   using Q wfE_pf[OF wf, of Q] by blast
   118 
   119 lemma wfE_min':
   120   "wf R \<Longrightarrow> Q \<noteq> {} \<Longrightarrow> (\<And>z. z \<in> Q \<Longrightarrow> (\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q) \<Longrightarrow> thesis) \<Longrightarrow> thesis"
   121   using wfE_min[of R _ Q] by blast
   122 
   123 lemma wfI_min:
   124   assumes a: "\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q"
   125   shows "wf R"
   126 proof (rule wfI_pf)
   127   fix A
   128   assume b: "A \<subseteq> R `` A"
   129   have False if "x \<in> A" for x
   130     using a[OF that] b by blast
   131   then show "A = {}" by blast
   132 qed
   133 
   134 lemma wf_eq_minimal: "wf r \<longleftrightarrow> (\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q))"
   135   apply auto
   136    apply (erule wfE_min)
   137     apply assumption
   138    apply blast
   139   apply (rule wfI_min)
   140   apply auto
   141   done
   142 
   143 lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
   144 
   145 
   146 subsubsection \<open>Well-foundedness of transitive closure\<close>
   147 
   148 lemma wf_trancl:
   149   assumes "wf r"
   150   shows "wf (r\<^sup>+)"
   151 proof -
   152   have "P x" if induct_step: "\<And>x. (\<And>y. (y, x) \<in> r\<^sup>+ \<Longrightarrow> P y) \<Longrightarrow> P x" for P x
   153   proof (rule induct_step)
   154     show "P y" if "(y, x) \<in> r\<^sup>+" for y
   155       using \<open>wf r\<close> and that
   156     proof (induct x arbitrary: y)
   157       case (less x)
   158       note hyp = \<open>\<And>x' y'. (x', x) \<in> r \<Longrightarrow> (y', x') \<in> r\<^sup>+ \<Longrightarrow> P y'\<close>
   159       from \<open>(y, x) \<in> r\<^sup>+\<close> show "P y"
   160       proof cases
   161         case base
   162         show "P y"
   163         proof (rule induct_step)
   164           fix y'
   165           assume "(y', y) \<in> r\<^sup>+"
   166           with \<open>(y, x) \<in> r\<close> show "P y'"
   167             by (rule hyp [of y y'])
   168         qed
   169       next
   170         case step
   171         then obtain x' where "(x', x) \<in> r" and "(y, x') \<in> r\<^sup>+"
   172           by simp
   173         then show "P y" by (rule hyp [of x' y])
   174       qed
   175     qed
   176   qed
   177   then show ?thesis unfolding wf_def by blast
   178 qed
   179 
   180 lemmas wfP_trancl = wf_trancl [to_pred]
   181 
   182 lemma wf_converse_trancl: "wf (r\<inverse>) \<Longrightarrow> wf ((r\<^sup>+)\<inverse>)"
   183   apply (subst trancl_converse [symmetric])
   184   apply (erule wf_trancl)
   185   done
   186 
   187 text \<open>Well-foundedness of subsets\<close>
   188 
   189 lemma wf_subset: "wf r \<Longrightarrow> p \<subseteq> r \<Longrightarrow> wf p"
   190   by (simp add: wf_eq_minimal) fast
   191 
   192 lemmas wfP_subset = wf_subset [to_pred]
   193 
   194 text \<open>Well-foundedness of the empty relation\<close>
   195 
   196 lemma wf_empty [iff]: "wf {}"
   197   by (simp add: wf_def)
   198 
   199 lemma wfP_empty [iff]: "wfP (\<lambda>x y. False)"
   200 proof -
   201   have "wfP bot"
   202     by (fact wf_empty [to_pred bot_empty_eq2])
   203   then show ?thesis
   204     by (simp add: bot_fun_def)
   205 qed
   206 
   207 lemma wf_Int1: "wf r \<Longrightarrow> wf (r \<inter> r')"
   208   by (erule wf_subset) (rule Int_lower1)
   209 
   210 lemma wf_Int2: "wf r \<Longrightarrow> wf (r' \<inter> r)"
   211   by (erule wf_subset) (rule Int_lower2)
   212 
   213 text \<open>Exponentiation.\<close>
   214 lemma wf_exp:
   215   assumes "wf (R ^^ n)"
   216   shows "wf R"
   217 proof (rule wfI_pf)
   218   fix A assume "A \<subseteq> R `` A"
   219   then have "A \<subseteq> (R ^^ n) `` A"
   220     by (induct n) force+
   221   with \<open>wf (R ^^ n)\<close> show "A = {}"
   222     by (rule wfE_pf)
   223 qed
   224 
   225 text \<open>Well-foundedness of \<open>insert\<close>.\<close>
   226 lemma wf_insert [iff]: "wf (insert (y, x) r) \<longleftrightarrow> wf r \<and> (x, y) \<notin> r\<^sup>*"
   227   apply (rule iffI)
   228    apply (blast elim: wf_trancl [THEN wf_irrefl]
   229       intro: rtrancl_into_trancl1 wf_subset rtrancl_mono [THEN [2] rev_subsetD])
   230   apply (simp add: wf_eq_minimal)
   231   apply safe
   232   apply (rule allE)
   233    apply assumption
   234   apply (erule impE)
   235    apply blast
   236   apply (erule bexE)
   237   apply (rename_tac a, case_tac "a = x")
   238    prefer 2
   239    apply blast
   240   apply (case_tac "y \<in> Q")
   241    prefer 2
   242    apply blast
   243   apply (rule_tac x = "{z. z \<in> Q \<and> (z,y) \<in> r\<^sup>*}" in allE)
   244    apply assumption
   245   apply (erule_tac V = "\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> P Q" for P in thin_rl)
   246   (*essential for speed*)
   247   (*blast with new substOccur fails*)
   248   apply (fast intro: converse_rtrancl_into_rtrancl)
   249   done
   250 
   251 
   252 subsubsection \<open>Well-foundedness of image\<close>
   253 
   254 lemma wf_map_prod_image: "wf r \<Longrightarrow> inj f \<Longrightarrow> wf (map_prod f f ` r)"
   255   apply (simp only: wf_eq_minimal)
   256   apply clarify
   257   apply (case_tac "\<exists>p. f p \<in> Q")
   258    apply (erule_tac x = "{p. f p \<in> Q}" in allE)
   259    apply (fast dest: inj_onD)
   260   apply blast
   261   done
   262 
   263 
   264 subsection \<open>Well-Foundedness Results for Unions\<close>
   265 
   266 lemma wf_union_compatible:
   267   assumes "wf R" "wf S"
   268   assumes "R O S \<subseteq> R"
   269   shows "wf (R \<union> S)"
   270 proof (rule wfI_min)
   271   fix x :: 'a and Q
   272   let ?Q' = "{x \<in> Q. \<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> Q}"
   273   assume "x \<in> Q"
   274   obtain a where "a \<in> ?Q'"
   275     by (rule wfE_min [OF \<open>wf R\<close> \<open>x \<in> Q\<close>]) blast
   276   with \<open>wf S\<close> obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'"
   277     by (erule wfE_min)
   278   have "y \<notin> Q" if "(y, z) \<in> S" for y
   279   proof
   280     from that have "y \<notin> ?Q'" by (rule zmin)
   281     assume "y \<in> Q"
   282     with \<open>y \<notin> ?Q'\<close> obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
   283     from \<open>(w, y) \<in> R\<close> \<open>(y, z) \<in> S\<close> have "(w, z) \<in> R O S" by (rule relcompI)
   284     with \<open>R O S \<subseteq> R\<close> have "(w, z) \<in> R" ..
   285     with \<open>z \<in> ?Q'\<close> have "w \<notin> Q" by blast
   286     with \<open>w \<in> Q\<close> show False by contradiction
   287   qed
   288   with \<open>z \<in> ?Q'\<close> show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<union> S \<longrightarrow> y \<notin> Q" by blast
   289 qed
   290 
   291 
   292 text \<open>Well-foundedness of indexed union with disjoint domains and ranges.\<close>
   293 
   294 lemma wf_UN:
   295   assumes "\<forall>i\<in>I. wf (r i)"
   296     and "\<forall>i\<in>I. \<forall>j\<in>I. r i \<noteq> r j \<longrightarrow> Domain (r i) \<inter> Range (r j) = {}"
   297   shows "wf (\<Union>i\<in>I. r i)"
   298   using assms
   299   apply (simp only: wf_eq_minimal)
   300   apply clarify
   301   apply (rename_tac A a, case_tac "\<exists>i\<in>I. \<exists>a\<in>A. \<exists>b\<in>A. (b, a) \<in> r i")
   302    prefer 2
   303    apply force
   304   apply clarify
   305   apply (drule bspec, assumption)
   306   apply (erule_tac x="{a. a \<in> A \<and> (\<exists>b\<in>A. (b, a) \<in> r i) }" in allE)
   307   apply (blast elim!: allE)
   308   done
   309 
   310 lemma wfP_SUP:
   311   "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (Domainp (r i)) (Rangep (r j)) = bot \<Longrightarrow>
   312     wfP (SUPREMUM UNIV r)"
   313   by (rule wf_UN[to_pred]) simp_all
   314 
   315 lemma wf_Union:
   316   assumes "\<forall>r\<in>R. wf r"
   317     and "\<forall>r\<in>R. \<forall>s\<in>R. r \<noteq> s \<longrightarrow> Domain r \<inter> Range s = {}"
   318   shows "wf (\<Union>R)"
   319   using assms wf_UN[of R "\<lambda>i. i"] by simp
   320 
   321 text \<open>
   322   Intuition: We find an \<open>R \<union> S\<close>-min element of a nonempty subset \<open>A\<close> by case distinction.
   323   \<^enum> There is a step \<open>a \<midarrow>R\<rightarrow> b\<close> with \<open>a, b \<in> A\<close>.
   324     Pick an \<open>R\<close>-min element \<open>z\<close> of the (nonempty) set \<open>{a\<in>A | \<exists>b\<in>A. a \<midarrow>R\<rightarrow> b}\<close>.
   325     By definition, there is \<open>z' \<in> A\<close> s.t. \<open>z \<midarrow>R\<rightarrow> z'\<close>. Because \<open>z\<close> is \<open>R\<close>-min in the
   326     subset, \<open>z'\<close> must be \<open>R\<close>-min in \<open>A\<close>. Because \<open>z'\<close> has an \<open>R\<close>-predecessor, it cannot
   327     have an \<open>S\<close>-successor and is thus \<open>S\<close>-min in \<open>A\<close> as well.
   328   \<^enum> There is no such step.
   329     Pick an \<open>S\<close>-min element of \<open>A\<close>. In this case it must be an \<open>R\<close>-min
   330     element of \<open>A\<close> as well.
   331 \<close>
   332 lemma wf_Un: "wf r \<Longrightarrow> wf s \<Longrightarrow> Domain r \<inter> Range s = {} \<Longrightarrow> wf (r \<union> s)"
   333   using wf_union_compatible[of s r]
   334   by (auto simp: Un_ac)
   335 
   336 lemma wf_union_merge: "wf (R \<union> S) = wf (R O R \<union> S O R \<union> S)"
   337   (is "wf ?A = wf ?B")
   338 proof
   339   assume "wf ?A"
   340   with wf_trancl have wfT: "wf (?A\<^sup>+)" .
   341   moreover have "?B \<subseteq> ?A\<^sup>+"
   342     by (subst trancl_unfold, subst trancl_unfold) blast
   343   ultimately show "wf ?B" by (rule wf_subset)
   344 next
   345   assume "wf ?B"
   346   show "wf ?A"
   347   proof (rule wfI_min)
   348     fix Q :: "'a set" and x
   349     assume "x \<in> Q"
   350     with \<open>wf ?B\<close> obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q"
   351       by (erule wfE_min)
   352     then have 1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q"
   353       and 2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q"
   354       and 3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q"
   355       by auto
   356     show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> ?A \<longrightarrow> y \<notin> Q"
   357     proof (cases "\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q")
   358       case True
   359       with \<open>z \<in> Q\<close> 3 show ?thesis by blast
   360     next
   361       case False
   362       then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast
   363       have "\<forall>y. (y, z') \<in> ?A \<longrightarrow> y \<notin> Q"
   364       proof (intro allI impI)
   365         fix y assume "(y, z') \<in> ?A"
   366         then show "y \<notin> Q"
   367         proof
   368           assume "(y, z') \<in> R"
   369           then have "(y, z) \<in> R O R" using \<open>(z', z) \<in> R\<close> ..
   370           with 1 show "y \<notin> Q" .
   371         next
   372           assume "(y, z') \<in> S"
   373           then have "(y, z) \<in> S O R" using  \<open>(z', z) \<in> R\<close> ..
   374           with 2 show "y \<notin> Q" .
   375         qed
   376       qed
   377       with \<open>z' \<in> Q\<close> show ?thesis ..
   378     qed
   379   qed
   380 qed
   381 
   382 lemma wf_comp_self: "wf R \<longleftrightarrow> wf (R O R)"  \<comment> \<open>special case\<close>
   383   by (rule wf_union_merge [where S = "{}", simplified])
   384 
   385 
   386 subsection \<open>Well-Foundedness of Composition\<close>
   387 
   388 text \<open>Bachmair and Dershowitz 1986, Lemma 2. [Provided by Tjark Weber]\<close>
   389 
   390 lemma qc_wf_relto_iff:
   391   assumes "R O S \<subseteq> (R \<union> S)\<^sup>* O R" \<comment> \<open>R quasi-commutes over S\<close>
   392   shows "wf (S\<^sup>* O R O S\<^sup>*) \<longleftrightarrow> wf R"
   393     (is "wf ?S \<longleftrightarrow> _")
   394 proof
   395   show "wf R" if "wf ?S"
   396   proof -
   397     have "R \<subseteq> ?S" by auto
   398     with wf_subset [of ?S] that show "wf R"
   399       by auto
   400   qed
   401 next
   402   show "wf ?S" if "wf R"
   403   proof (rule wfI_pf)
   404     fix A
   405     assume A: "A \<subseteq> ?S `` A"
   406     let ?X = "(R \<union> S)\<^sup>* `` A"
   407     have *: "R O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R"
   408     proof -
   409       have "(x, z) \<in> (R \<union> S)\<^sup>* O R" if "(y, z) \<in> (R \<union> S)\<^sup>*" and "(x, y) \<in> R" for x y z
   410         using that
   411       proof (induct y z)
   412         case rtrancl_refl
   413         then show ?case by auto
   414       next
   415         case (rtrancl_into_rtrancl a b c)
   416         then have "(x, c) \<in> ((R \<union> S)\<^sup>* O (R \<union> S)\<^sup>*) O R"
   417           using assms by blast
   418         then show ?case by simp
   419       qed
   420       then show ?thesis by auto
   421     qed
   422     then have "R O S\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R"
   423       using rtrancl_Un_subset by blast
   424     then have "?S \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R"
   425       by (simp add: relcomp_mono rtrancl_mono)
   426     also have "\<dots> = (R \<union> S)\<^sup>* O R"
   427       by (simp add: O_assoc[symmetric])
   428     finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R O (R \<union> S)\<^sup>*"
   429       by (simp add: O_assoc[symmetric] relcomp_mono)
   430     also have "\<dots> \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R"
   431       using * by (simp add: relcomp_mono)
   432     finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R"
   433       by (simp add: O_assoc[symmetric])
   434     then have "(?S O (R \<union> S)\<^sup>*) `` A \<subseteq> ((R \<union> S)\<^sup>* O R) `` A"
   435       by (simp add: Image_mono)
   436     moreover have "?X \<subseteq> (?S O (R \<union> S)\<^sup>*) `` A"
   437       using A by (auto simp: relcomp_Image)
   438     ultimately have "?X \<subseteq> R `` ?X"
   439       by (auto simp: relcomp_Image)
   440     then have "?X = {}"
   441       using \<open>wf R\<close> by (simp add: wfE_pf)
   442     moreover have "A \<subseteq> ?X" by auto
   443     ultimately show "A = {}" by simp
   444   qed
   445 qed
   446 
   447 corollary wf_relcomp_compatible:
   448   assumes "wf R" and "R O S \<subseteq> S O R"
   449   shows "wf (S O R)"
   450 proof -
   451   have "R O S \<subseteq> (R \<union> S)\<^sup>* O R"
   452     using assms by blast
   453   then have "wf (S\<^sup>* O R O S\<^sup>*)"
   454     by (simp add: assms qc_wf_relto_iff)
   455   then show ?thesis
   456     by (rule Wellfounded.wf_subset) blast
   457 qed
   458 
   459 
   460 subsection \<open>Acyclic relations\<close>
   461 
   462 lemma wf_acyclic: "wf r \<Longrightarrow> acyclic r"
   463   by (simp add: acyclic_def) (blast elim: wf_trancl [THEN wf_irrefl])
   464 
   465 lemmas wfP_acyclicP = wf_acyclic [to_pred]
   466 
   467 
   468 subsubsection \<open>Wellfoundedness of finite acyclic relations\<close>
   469 
   470 lemma finite_acyclic_wf [rule_format]: "finite r \<Longrightarrow> acyclic r \<longrightarrow> wf r"
   471   apply (erule finite_induct)
   472    apply blast
   473   apply (simp add: split_tupled_all)
   474   done
   475 
   476 lemma finite_acyclic_wf_converse: "finite r \<Longrightarrow> acyclic r \<Longrightarrow> wf (r\<inverse>)"
   477   apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])
   478   apply (erule acyclic_converse [THEN iffD2])
   479   done
   480 
   481 text \<open>
   482   Observe that the converse of an irreflexive, transitive,
   483   and finite relation is again well-founded. Thus, we may
   484   employ it for well-founded induction.
   485 \<close>
   486 lemma wf_converse:
   487   assumes "irrefl r" and "trans r" and "finite r"
   488   shows "wf (r\<inverse>)"
   489 proof -
   490   have "acyclic r"
   491     using \<open>irrefl r\<close> and \<open>trans r\<close>
   492     by (simp add: irrefl_def acyclic_irrefl)
   493   with \<open>finite r\<close> show ?thesis
   494     by (rule finite_acyclic_wf_converse)
   495 qed
   496 
   497 lemma wf_iff_acyclic_if_finite: "finite r \<Longrightarrow> wf r = acyclic r"
   498   by (blast intro: finite_acyclic_wf wf_acyclic)
   499 
   500 
   501 subsection \<open>@{typ nat} is well-founded\<close>
   502 
   503 lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+"
   504 proof (rule ext, rule ext, rule iffI)
   505   fix n m :: nat
   506   show "(\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+ m n" if "m < n"
   507     using that
   508   proof (induct n)
   509     case 0
   510     then show ?case by auto
   511   next
   512     case (Suc n)
   513     then show ?case
   514       by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl)
   515   qed
   516   show "m < n" if "(\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+ m n"
   517     using that by (induct n) (simp_all add: less_Suc_eq_le reflexive le_less)
   518 qed
   519 
   520 definition pred_nat :: "(nat \<times> nat) set"
   521   where "pred_nat = {(m, n). n = Suc m}"
   522 
   523 definition less_than :: "(nat \<times> nat) set"
   524   where "less_than = pred_nat\<^sup>+"
   525 
   526 lemma less_eq: "(m, n) \<in> pred_nat\<^sup>+ \<longleftrightarrow> m < n"
   527   unfolding less_nat_rel pred_nat_def trancl_def by simp
   528 
   529 lemma pred_nat_trancl_eq_le: "(m, n) \<in> pred_nat\<^sup>* \<longleftrightarrow> m \<le> n"
   530   unfolding less_eq rtrancl_eq_or_trancl by auto
   531 
   532 lemma wf_pred_nat: "wf pred_nat"
   533   apply (unfold wf_def pred_nat_def)
   534   apply clarify
   535   apply (induct_tac x)
   536    apply 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)
   544 
   545 lemma less_than_iff [iff]: "((x,y) \<in> 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   by (rule Wellfounded.wellorder_class.wf)
   550 
   551 
   552 subsection \<open>Accessible Part\<close>
   553 
   554 text \<open>
   555   Inductive definition of the accessible part \<open>acc r\<close> of a
   556   relation; see also @{cite "paulin-tlca"}.
   557 \<close>
   558 
   559 inductive_set acc :: "('a \<times> 'a) set \<Rightarrow> 'a set" for r :: "('a \<times> 'a) set"
   560   where accI: "(\<And>y. (y, x) \<in> r \<Longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r"
   561 
   562 abbreviation termip :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   563   where "termip r \<equiv> accp (r\<inverse>\<inverse>)"
   564 
   565 abbreviation termi :: "('a \<times> 'a) set \<Rightarrow> 'a set"
   566   where "termi r \<equiv> acc (r\<inverse>)"
   567 
   568 lemmas accpI = accp.accI
   569 
   570 lemma accp_eq_acc [code]: "accp r = (\<lambda>x. x \<in> Wellfounded.acc {(x, y). r x y})"
   571   by (simp add: acc_def)
   572 
   573 
   574 text \<open>Induction rules\<close>
   575 
   576 theorem accp_induct:
   577   assumes major: "accp r a"
   578   assumes hyp: "\<And>x. accp r x \<Longrightarrow> \<forall>y. r y x \<longrightarrow> P y \<Longrightarrow> P x"
   579   shows "P a"
   580   apply (rule major [THEN accp.induct])
   581   apply (rule hyp)
   582    apply (rule accp.accI)
   583    apply fast
   584   apply fast
   585   done
   586 
   587 lemmas accp_induct_rule = accp_induct [rule_format, induct set: accp]
   588 
   589 theorem accp_downward: "accp r b \<Longrightarrow> r a b \<Longrightarrow> accp r a"
   590   by (cases rule: accp.cases)
   591 
   592 lemma not_accp_down:
   593   assumes na: "\<not> accp R x"
   594   obtains z where "R z x" and "\<not> accp R z"
   595 proof -
   596   assume a: "\<And>z. R z x \<Longrightarrow> \<not> accp R z \<Longrightarrow> thesis"
   597   show thesis
   598   proof (cases "\<forall>z. R z x \<longrightarrow> accp R z")
   599     case True
   600     then have "\<And>z. R z x \<Longrightarrow> accp R z" by auto
   601     then have "accp R x" by (rule accp.accI)
   602     with na show thesis ..
   603   next
   604     case False then obtain z where "R z x" and "\<not> accp R z"
   605       by auto
   606     with a show thesis .
   607   qed
   608 qed
   609 
   610 lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r a \<longrightarrow> accp r b"
   611   by (erule rtranclp_induct) (blast dest: accp_downward)+
   612 
   613 theorem accp_downwards: "accp r a \<Longrightarrow> r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r b"
   614   by (blast dest: accp_downwards_aux)
   615 
   616 theorem accp_wfPI: "\<forall>x. accp r x \<Longrightarrow> wfP r"
   617   apply (rule wfPUNIVI)
   618   apply (rule_tac P = P in accp_induct)
   619    apply blast
   620   apply blast
   621   done
   622 
   623 theorem accp_wfPD: "wfP r \<Longrightarrow> accp r x"
   624   apply (erule wfP_induct_rule)
   625   apply (rule accp.accI)
   626   apply blast
   627   done
   628 
   629 theorem wfP_accp_iff: "wfP r = (\<forall>x. accp r x)"
   630   by (blast intro: accp_wfPI dest: accp_wfPD)
   631 
   632 
   633 text \<open>Smaller relations have bigger accessible parts:\<close>
   634 
   635 lemma accp_subset:
   636   assumes "R1 \<le> R2"
   637   shows "accp R2 \<le> accp R1"
   638 proof (rule predicate1I)
   639   fix x
   640   assume "accp R2 x"
   641   then show "accp R1 x"
   642   proof (induct x)
   643     fix x
   644     assume "\<And>y. R2 y x \<Longrightarrow> accp R1 y"
   645     with assms show "accp R1 x"
   646       by (blast intro: accp.accI)
   647   qed
   648 qed
   649 
   650 
   651 text \<open>This is a generalized induction theorem that works on
   652   subsets of the accessible part.\<close>
   653 
   654 lemma accp_subset_induct:
   655   assumes subset: "D \<le> accp R"
   656     and dcl: "\<And>x z. D x \<Longrightarrow> R z x \<Longrightarrow> D z"
   657     and "D x"
   658     and istep: "\<And>x. D x \<Longrightarrow> (\<And>z. R z x \<Longrightarrow> P z) \<Longrightarrow> P x"
   659   shows "P x"
   660 proof -
   661   from subset and \<open>D x\<close>
   662   have "accp R x" ..
   663   then show "P x" using \<open>D x\<close>
   664   proof (induct x)
   665     fix x
   666     assume "D x" and "\<And>y. R y x \<Longrightarrow> D y \<Longrightarrow> P y"
   667     with dcl and istep show "P x" by blast
   668   qed
   669 qed
   670 
   671 
   672 text \<open>Set versions of the above theorems\<close>
   673 
   674 lemmas acc_induct = accp_induct [to_set]
   675 lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc]
   676 lemmas acc_downward = accp_downward [to_set]
   677 lemmas not_acc_down = not_accp_down [to_set]
   678 lemmas acc_downwards_aux = accp_downwards_aux [to_set]
   679 lemmas acc_downwards = accp_downwards [to_set]
   680 lemmas acc_wfI = accp_wfPI [to_set]
   681 lemmas acc_wfD = accp_wfPD [to_set]
   682 lemmas wf_acc_iff = wfP_accp_iff [to_set]
   683 lemmas acc_subset = accp_subset [to_set]
   684 lemmas acc_subset_induct = accp_subset_induct [to_set]
   685 
   686 
   687 subsection \<open>Tools for building wellfounded relations\<close>
   688 
   689 text \<open>Inverse Image\<close>
   690 
   691 lemma wf_inv_image [simp,intro!]: "wf r \<Longrightarrow> wf (inv_image r f)"
   692   for f :: "'a \<Rightarrow> 'b"
   693   apply (simp add: inv_image_def wf_eq_minimal)
   694   apply clarify
   695   apply (subgoal_tac "\<exists>w::'b. w \<in> {w. \<exists>x::'a. x \<in> Q \<and> f x = w}")
   696    prefer 2
   697    apply (blast del: allE)
   698   apply (erule allE)
   699   apply (erule (1) notE impE)
   700   apply blast
   701   done
   702 
   703 text \<open>Measure functions into @{typ nat}\<close>
   704 
   705 definition measure :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set"
   706   where "measure = inv_image less_than"
   707 
   708 lemma in_measure[simp, code_unfold]: "(x, y) \<in> measure f \<longleftrightarrow> f x < f y"
   709   by (simp add:measure_def)
   710 
   711 lemma wf_measure [iff]: "wf (measure f)"
   712   unfolding measure_def by (rule wf_less_than [THEN wf_inv_image])
   713 
   714 lemma wf_if_measure: "(\<And>x. P x \<Longrightarrow> f(g x) < f x) \<Longrightarrow> wf {(y,x). P x \<and> y = g x}"
   715   for f :: "'a \<Rightarrow> nat"
   716   apply (insert wf_measure[of f])
   717   apply (simp only: measure_def inv_image_def less_than_def less_eq)
   718   apply (erule wf_subset)
   719   apply auto
   720   done
   721 
   722 
   723 subsubsection \<open>Lexicographic combinations\<close>
   724 
   725 definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set"
   726     (infixr "<*lex*>" 80)
   727   where "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
   728 
   729 lemma wf_lex_prod [intro!]: "wf ra \<Longrightarrow> wf rb \<Longrightarrow> wf (ra <*lex*> rb)"
   730   apply (unfold wf_def lex_prod_def)
   731   apply (rule allI)
   732   apply (rule impI)
   733   apply (simp only: split_paired_All)
   734   apply (drule spec)
   735   apply (erule mp)
   736   apply (rule allI)
   737   apply (rule impI)
   738   apply (drule spec)
   739   apply (erule mp)
   740   apply blast
   741   done
   742 
   743 lemma in_lex_prod[simp]: "((a, b), (a', b')) \<in> r <*lex*> s \<longleftrightarrow> (a, a') \<in> r \<or> a = a' \<and> (b, b') \<in> s"
   744   by (auto simp:lex_prod_def)
   745 
   746 text \<open>\<open><*lex*>\<close> preserves transitivity\<close>
   747 lemma trans_lex_prod [intro!]: "trans R1 \<Longrightarrow> trans R2 \<Longrightarrow> trans (R1 <*lex*> R2)"
   748   unfolding trans_def lex_prod_def by blast
   749 
   750 
   751 text \<open>lexicographic combinations with measure functions\<close>
   752 
   753 definition mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
   754   where "f <*mlex*> R = inv_image (less_than <*lex*> R) (\<lambda>x. (f x, x))"
   755 
   756 lemma wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)"
   757   by (auto simp: mlex_prod_def)
   758 
   759 lemma mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
   760   by (simp add: mlex_prod_def)
   761 
   762 lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
   763   by (auto simp: mlex_prod_def)
   764 
   765 text \<open>Proper subset relation on finite sets.\<close>
   766 definition finite_psubset :: "('a set \<times> 'a set) set"
   767   where "finite_psubset = {(A, B). A \<subset> B \<and> finite B}"
   768 
   769 lemma wf_finite_psubset[simp]: "wf finite_psubset"
   770   apply (unfold finite_psubset_def)
   771   apply (rule wf_measure [THEN wf_subset])
   772   apply (simp add: measure_def inv_image_def less_than_def less_eq)
   773   apply (fast elim!: psubset_card_mono)
   774   done
   775 
   776 lemma trans_finite_psubset: "trans finite_psubset"
   777   by (auto simp: finite_psubset_def less_le trans_def)
   778 
   779 lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset \<longleftrightarrow> A \<subset> B \<and> finite B"
   780   unfolding finite_psubset_def by auto
   781 
   782 text \<open>max- and min-extension of order to finite sets\<close>
   783 
   784 inductive_set max_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set"
   785   for R :: "('a \<times> 'a) set"
   786   where max_extI[intro]:
   787     "finite X \<Longrightarrow> finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>Y. (x, y) \<in> R) \<Longrightarrow> (X, Y) \<in> max_ext R"
   788 
   789 lemma max_ext_wf:
   790   assumes wf: "wf r"
   791   shows "wf (max_ext r)"
   792 proof (rule acc_wfI, intro allI)
   793   show "M \<in> acc (max_ext r)" (is "_ \<in> ?W") for M
   794   proof (induct M rule: infinite_finite_induct)
   795     case empty
   796     show ?case
   797       by (rule accI) (auto elim: max_ext.cases)
   798   next
   799     case (insert a M)
   800     from wf \<open>M \<in> ?W\<close> \<open>finite M\<close> show "insert a M \<in> ?W"
   801     proof (induct arbitrary: M)
   802       fix M a
   803       assume "M \<in> ?W"
   804       assume [intro]: "finite M"
   805       assume hyp: "\<And>b M. (b, a) \<in> r \<Longrightarrow> M \<in> ?W \<Longrightarrow> finite M \<Longrightarrow> insert b M \<in> ?W"
   806       have add_less: "M \<in> ?W \<Longrightarrow> (\<And>y. y \<in> N \<Longrightarrow> (y, a) \<in> r) \<Longrightarrow> N \<union> M \<in> ?W"
   807         if "finite N" "finite M" for N M :: "'a set"
   808         using that by (induct N arbitrary: M) (auto simp: hyp)
   809       show "insert a M \<in> ?W"
   810       proof (rule accI)
   811         fix N
   812         assume Nless: "(N, insert a M) \<in> max_ext r"
   813         then have *: "\<And>x. x \<in> N \<Longrightarrow> (x, a) \<in> r \<or> (\<exists>y \<in> M. (x, y) \<in> r)"
   814           by (auto elim!: max_ext.cases)
   815 
   816         let ?N1 = "{n \<in> N. (n, a) \<in> r}"
   817         let ?N2 = "{n \<in> N. (n, a) \<notin> r}"
   818         have N: "?N1 \<union> ?N2 = N" by (rule set_eqI) auto
   819         from Nless have "finite N" by (auto elim: max_ext.cases)
   820         then have finites: "finite ?N1" "finite ?N2" by auto
   821 
   822         have "?N2 \<in> ?W"
   823         proof (cases "M = {}")
   824           case [simp]: True
   825           have Mw: "{} \<in> ?W" by (rule accI) (auto elim: max_ext.cases)
   826           from * have "?N2 = {}" by auto
   827           with Mw show "?N2 \<in> ?W" by (simp only:)
   828         next
   829           case False
   830           from * finites have N2: "(?N2, M) \<in> max_ext r"
   831             by (rule_tac max_extI[OF _ _ \<open>M \<noteq> {}\<close>]) auto
   832           with \<open>M \<in> ?W\<close> show "?N2 \<in> ?W" by (rule acc_downward)
   833         qed
   834         with finites have "?N1 \<union> ?N2 \<in> ?W"
   835           by (rule add_less) simp
   836         then show "N \<in> ?W" by (simp only: N)
   837       qed
   838     qed
   839   next
   840     case infinite
   841     show ?case
   842       by (rule accI) (auto elim: max_ext.cases simp: infinite)
   843   qed
   844 qed
   845 
   846 lemma max_ext_additive: "(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow> (A \<union> C, B \<union> D) \<in> max_ext R"
   847   by (force elim!: max_ext.cases)
   848 
   849 
   850 definition min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set"
   851   where "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}"
   852 
   853 lemma min_ext_wf:
   854   assumes "wf r"
   855   shows "wf (min_ext r)"
   856 proof (rule wfI_min)
   857   show "\<exists>m \<in> Q. (\<forall> n. (n, m) \<in> min_ext r \<longrightarrow> n \<notin> Q)" if nonempty: "x \<in> Q"
   858     for Q :: "'a set set" and x
   859   proof (cases "Q = {{}}")
   860     case True
   861     then show ?thesis by (simp add: min_ext_def)
   862   next
   863     case False
   864     with nonempty obtain e x where "x \<in> Q" "e \<in> x" by force
   865     then have eU: "e \<in> \<Union>Q" by auto
   866     with \<open>wf r\<close>
   867     obtain z where z: "z \<in> \<Union>Q" "\<And>y. (y, z) \<in> r \<Longrightarrow> y \<notin> \<Union>Q"
   868       by (erule wfE_min)
   869     from z obtain m where "m \<in> Q" "z \<in> m" by auto
   870     from \<open>m \<in> Q\<close> show ?thesis
   871     proof (intro rev_bexI allI impI)
   872       fix n
   873       assume smaller: "(n, m) \<in> min_ext r"
   874       with \<open>z \<in> m\<close> obtain y where "y \<in> n" "(y, z) \<in> r"
   875         by (auto simp: min_ext_def)
   876       with z(2) show "n \<notin> Q" by auto
   877     qed
   878   qed
   879 qed
   880 
   881 
   882 subsubsection \<open>Bounded increase must terminate\<close>
   883 
   884 lemma wf_bounded_measure:
   885   fixes ub :: "'a \<Rightarrow> nat"
   886     and f :: "'a \<Rightarrow> nat"
   887   assumes "\<And>a b. (b, a) \<in> r \<Longrightarrow> ub b \<le> ub a \<and> ub a \<ge> f b \<and> f b > f a"
   888   shows "wf r"
   889   by (rule wf_subset[OF wf_measure[of "\<lambda>a. ub a - f a"]]) (auto dest: assms)
   890 
   891 lemma wf_bounded_set:
   892   fixes ub :: "'a \<Rightarrow> 'b set"
   893     and f :: "'a \<Rightarrow> 'b set"
   894   assumes "\<And>a b. (b,a) \<in> r \<Longrightarrow> finite (ub a) \<and> ub b \<subseteq> ub a \<and> ub a \<supseteq> f b \<and> f b \<supset> f a"
   895   shows "wf r"
   896   apply (rule wf_bounded_measure[of r "\<lambda>a. card (ub a)" "\<lambda>a. card (f a)"])
   897   apply (drule assms)
   898   apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2])
   899   done
   900 
   901 lemma finite_subset_wf:
   902   assumes "finite A"
   903   shows "wf {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}"
   904 proof (intro finite_acyclic_wf)
   905   have "{(X,Y). X \<subset> Y \<and> Y \<subseteq> A} \<subseteq> Pow A \<times> Pow A"
   906     by blast
   907   then show "finite {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}"
   908     by (rule finite_subset) (auto simp: assms finite_cartesian_product)
   909 next
   910   have "{(X, Y). X \<subset> Y \<and> Y \<subseteq> A}\<^sup>+ = {(X, Y). X \<subset> Y \<and> Y \<subseteq> A}"
   911     by (intro trancl_id transI) blast
   912   also have " \<forall>x. (x, x) \<notin> \<dots>"
   913     by blast
   914   finally show "acyclic {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}"
   915     by (rule acyclicI)
   916 qed
   917 
   918 hide_const (open) acc accp
   919 
   920 end