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