src/HOL/Wellfounded_Relations.thy
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 26072 f65a7fa2da6c
permissions -rw-r--r--
avoid rebinding of existing facts;
paulson@15346
     1
(*  ID:   $Id$
nipkow@10213
     2
    Author:     Konrad Slind
nipkow@10213
     3
    Copyright   1995 TU Munich
nipkow@10213
     4
*)
nipkow@10213
     5
paulson@15346
     6
header {*Well-founded Relations*}
paulson@15346
     7
paulson@15346
     8
theory Wellfounded_Relations
haftmann@25517
     9
imports Finite_Set FunDef
haftmann@25517
    10
uses
haftmann@25517
    11
  ("Tools/function_package/lexicographic_order.ML")
haftmann@25517
    12
  ("Tools/function_package/fundef_datatype.ML")
paulson@15346
    13
begin
paulson@15346
    14
paulson@15346
    15
text{*Derived WF relations such as inverse image, lexicographic product and
paulson@15346
    16
measure. The simple relational product, in which @{term "(x',y')"} precedes
paulson@15346
    17
@{term "(x,y)"} if @{term "x'<x"} and @{term "y'<y"}, is a subset of the
paulson@15346
    18
lexicographic product, and therefore does not need to be defined separately.*}
nipkow@10213
    19
nipkow@10213
    20
constdefs
nipkow@10213
    21
 measure   :: "('a => nat) => ('a * 'a)set"
paulson@15346
    22
    "measure == inv_image less_than"
nipkow@10213
    23
nipkow@10213
    24
 lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
nipkow@10213
    25
               (infixr "<*lex*>" 80)
paulson@15346
    26
    "ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
paulson@15346
    27
paulson@15346
    28
 finite_psubset  :: "('a set * 'a set) set"
paulson@15346
    29
   --{* finite proper subset*}
paulson@15346
    30
    "finite_psubset == {(A,B). A < B & finite B}"
paulson@15346
    31
paulson@15346
    32
 same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
paulson@15346
    33
    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
paulson@15346
    34
   --{*For @{text rec_def} declarations where the first n parameters
paulson@15346
    35
       stay unchanged in the recursive call. 
paulson@15346
    36
       See @{text "Library/While_Combinator.thy"} for an application.*}
paulson@15346
    37
paulson@15346
    38
paulson@15346
    39
subsection{*Measure Functions make Wellfounded Relations*}
paulson@15346
    40
paulson@15346
    41
subsubsection{*`Less than' on the natural numbers*}
paulson@15346
    42
paulson@15346
    43
lemma full_nat_induct:
paulson@15346
    44
  assumes ih: "(!!n. (ALL m. Suc m <= n --> P m) ==> P n)"
paulson@15346
    45
  shows "P n"
paulson@15346
    46
apply (rule wf_less_than [THEN wf_induct])
paulson@15346
    47
apply (rule ih, auto)
paulson@15346
    48
done
paulson@15346
    49
paulson@15346
    50
subsubsection{*The Inverse Image into a Wellfounded Relation is Wellfounded.*}
paulson@15346
    51
paulson@15346
    52
lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))"
paulson@15346
    53
apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal)
paulson@15346
    54
apply clarify
paulson@15346
    55
apply (subgoal_tac "EX (w::'b) . w : {w. EX (x::'a) . x: Q & (f x = w) }")
paulson@15346
    56
prefer 2 apply (blast del: allE)
paulson@15346
    57
apply (erule allE)
paulson@15346
    58
apply (erule (1) notE impE)
paulson@15346
    59
apply blast
paulson@15346
    60
done
nipkow@10213
    61
krauss@19769
    62
lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
krauss@19769
    63
  by (auto simp:inv_image_def)
paulson@15346
    64
paulson@15346
    65
subsubsection{*Finally, All Measures are Wellfounded.*}
paulson@15346
    66
nipkow@19623
    67
lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)"
krauss@19769
    68
  by (simp add:measure_def)
nipkow@19623
    69
paulson@15346
    70
lemma wf_measure [iff]: "wf (measure f)"
paulson@15346
    71
apply (unfold measure_def)
paulson@15346
    72
apply (rule wf_less_than [THEN wf_inv_image])
paulson@15346
    73
done
paulson@15346
    74
wenzelm@18277
    75
lemma measure_induct_rule [case_names less]:
wenzelm@18277
    76
  fixes f :: "'a \<Rightarrow> nat"
wenzelm@18277
    77
  assumes step: "\<And>x. (\<And>y. f y < f x \<Longrightarrow> P y) \<Longrightarrow> P x"
wenzelm@18277
    78
  shows "P a"
wenzelm@18277
    79
proof -
wenzelm@18277
    80
  have "wf (measure f)" ..
wenzelm@18277
    81
  then show ?thesis
wenzelm@18277
    82
  proof induct
wenzelm@18277
    83
    case (less x)
wenzelm@18277
    84
    show ?case
wenzelm@18277
    85
    proof (rule step)
wenzelm@18277
    86
      fix y
wenzelm@18277
    87
      assume "f y < f x"
nipkow@19623
    88
      hence "(y, x) \<in> measure f" by simp
nipkow@19623
    89
      thus "P y" by (rule less)
wenzelm@18277
    90
    qed
wenzelm@18277
    91
  qed
wenzelm@18277
    92
qed
wenzelm@18277
    93
wenzelm@18277
    94
lemma measure_induct:
wenzelm@18277
    95
  fixes f :: "'a \<Rightarrow> nat"
wenzelm@18277
    96
  shows "(\<And>x. \<forall>y. f y < f x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
wenzelm@18277
    97
  by (rule measure_induct_rule [of f P a]) iprover
paulson@15346
    98
nipkow@24853
    99
(* Should go into Finite_Set, but needs measure.
nipkow@24853
   100
   Maybe move Wf_Rel before Finite_Set and finite_psubset to Finite_set?
nipkow@24853
   101
*)
nipkow@24853
   102
lemma (in linorder)
nipkow@24853
   103
  finite_linorder_induct[consumes 1, case_names empty insert]:
nipkow@24853
   104
 "finite A \<Longrightarrow> P {} \<Longrightarrow>
haftmann@25062
   105
  (!!A b. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A))
nipkow@24853
   106
  \<Longrightarrow> P A"
nipkow@24853
   107
proof (induct A rule: measure_induct[where f=card])
nipkow@24853
   108
  fix A :: "'a set"
nipkow@24853
   109
  assume IH: "ALL B. card B < card A \<longrightarrow> finite B \<longrightarrow> P {} \<longrightarrow>
haftmann@25062
   110
                 (\<forall>A b. finite A \<longrightarrow> (\<forall>a\<in>A. a<b) \<longrightarrow> P A \<longrightarrow> P (insert b A))
nipkow@24853
   111
                  \<longrightarrow> P B"
nipkow@24853
   112
  and "finite A" and "P {}"
haftmann@25062
   113
  and step: "!!A b. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)"
nipkow@24853
   114
  show "P A"
nipkow@24853
   115
  proof cases
nipkow@24853
   116
    assume "A = {}" thus "P A" using `P {}` by simp
nipkow@24853
   117
  next
nipkow@24853
   118
    let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B"
nipkow@24853
   119
    assume "A \<noteq> {}"
nipkow@24853
   120
    with `finite A` have "Max A : A" by auto
nipkow@24853
   121
    hence A: "?A = A" using insert_Diff_single insert_absorb by auto
nipkow@24853
   122
    note card_Diff1_less[OF `finite A` `Max A : A`]
nipkow@24853
   123
    moreover have "finite ?B" using `finite A` by simp
nipkow@24853
   124
    ultimately have "P ?B" using `P {}` step IH by blast
haftmann@25062
   125
    moreover have "\<forall>a\<in>?B. a < Max A"
nipkow@24853
   126
      using Max_ge[OF `finite A` `A \<noteq> {}`] by fastsimp
nipkow@24853
   127
    ultimately show "P A"
nipkow@24853
   128
      using A insert_Diff_single step[OF `finite ?B`] by fastsimp
nipkow@24853
   129
  qed
nipkow@24853
   130
qed
nipkow@24853
   131
paulson@15346
   132
paulson@15346
   133
subsection{*Other Ways of Constructing Wellfounded Relations*}
paulson@15346
   134
paulson@15346
   135
text{*Wellfoundedness of lexicographic combinations*}
paulson@15346
   136
lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
paulson@15346
   137
apply (unfold wf_def lex_prod_def) 
paulson@15346
   138
apply (rule allI, rule impI)
paulson@15346
   139
apply (simp (no_asm_use) only: split_paired_All)
paulson@15346
   140
apply (drule spec, erule mp) 
paulson@15346
   141
apply (rule allI, rule impI)
paulson@15346
   142
apply (drule spec, erule mp, blast) 
paulson@15346
   143
done
paulson@15346
   144
krauss@19769
   145
lemma in_lex_prod[simp]: 
krauss@19769
   146
  "(((a,b),(a',b')): r <*lex*> s) = ((a,a'): r \<or> (a = a' \<and> (b, b') : s))"
krauss@19769
   147
  by (auto simp:lex_prod_def)
krauss@19769
   148
krauss@24575
   149
text {* lexicographic combinations with measure functions *}
krauss@24575
   150
krauss@24575
   151
definition 
krauss@24575
   152
  mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
krauss@24575
   153
where
krauss@24575
   154
  "f <*mlex*> R = inv_image (less_than <*lex*> R) (%x. (f x, x))"
krauss@24575
   155
krauss@24575
   156
lemma wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)"
krauss@24575
   157
unfolding mlex_prod_def
krauss@24575
   158
by auto
krauss@24575
   159
krauss@24575
   160
lemma mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
krauss@24575
   161
unfolding mlex_prod_def by simp
krauss@24575
   162
krauss@24575
   163
lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
krauss@24575
   164
unfolding mlex_prod_def by auto
krauss@24575
   165
krauss@24575
   166
paulson@15346
   167
text{*Transitivity of WF combinators.*}
paulson@15346
   168
lemma trans_lex_prod [intro!]: 
paulson@15346
   169
    "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
paulson@15346
   170
by (unfold trans_def lex_prod_def, blast) 
paulson@15346
   171
paulson@15346
   172
subsubsection{*Wellfoundedness of proper subset on finite sets.*}
paulson@15346
   173
lemma wf_finite_psubset: "wf(finite_psubset)"
paulson@15346
   174
apply (unfold finite_psubset_def)
paulson@15346
   175
apply (rule wf_measure [THEN wf_subset])
haftmann@26072
   176
apply (simp add: measure_def inv_image_def less_than_def less_eq)
paulson@15346
   177
apply (fast elim!: psubset_card_mono)
paulson@15346
   178
done
paulson@15346
   179
paulson@15346
   180
lemma trans_finite_psubset: "trans finite_psubset"
paulson@15346
   181
by (simp add: finite_psubset_def psubset_def trans_def, blast)
paulson@15346
   182
paulson@15346
   183
paulson@15346
   184
subsubsection{*Wellfoundedness of finite acyclic relations*}
paulson@15346
   185
paulson@15346
   186
text{*This proof belongs in this theory because it needs Finite.*}
nipkow@10213
   187
paulson@15346
   188
lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r"
paulson@15346
   189
apply (erule finite_induct, blast)
paulson@15346
   190
apply (simp (no_asm_simp) only: split_tupled_all)
paulson@15346
   191
apply simp
paulson@15346
   192
done
paulson@15346
   193
paulson@15346
   194
lemma finite_acyclic_wf_converse: "[|finite r; acyclic r|] ==> wf (r^-1)"
paulson@15346
   195
apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])
paulson@15346
   196
apply (erule acyclic_converse [THEN iffD2])
paulson@15346
   197
done
paulson@15346
   198
paulson@15346
   199
lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r"
paulson@15346
   200
by (blast intro: finite_acyclic_wf wf_acyclic)
paulson@15346
   201
paulson@15346
   202
paulson@15352
   203
subsubsection{*Wellfoundedness of @{term same_fst}*}
paulson@15346
   204
paulson@15346
   205
lemma same_fstI [intro!]:
paulson@15346
   206
     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
paulson@15346
   207
by (simp add: same_fst_def)
paulson@15346
   208
paulson@15346
   209
lemma wf_same_fst:
paulson@15346
   210
  assumes prem: "(!!x. P x ==> wf(R x))"
paulson@15346
   211
  shows "wf(same_fst P R)"
paulson@15346
   212
apply (simp cong del: imp_cong add: wf_def same_fst_def)
paulson@15346
   213
apply (intro strip)
paulson@15346
   214
apply (rename_tac a b)
paulson@15346
   215
apply (case_tac "wf (R a)")
paulson@15346
   216
 apply (erule_tac a = b in wf_induct, blast)
paulson@15346
   217
apply (blast intro: prem)
paulson@15346
   218
done
paulson@15346
   219
paulson@15346
   220
paulson@15346
   221
subsection{*Weakly decreasing sequences (w.r.t. some well-founded order) 
paulson@15346
   222
   stabilize.*}
paulson@15346
   223
paulson@15346
   224
text{*This material does not appear to be used any longer.*}
paulson@15346
   225
paulson@15346
   226
lemma lemma1: "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*"
paulson@15346
   227
apply (induct_tac "k", simp_all)
paulson@15346
   228
apply (blast intro: rtrancl_trans)
paulson@15346
   229
done
paulson@15346
   230
paulson@15346
   231
lemma lemma2: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
paulson@15346
   232
      ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))"
paulson@15346
   233
apply (erule wf_induct, clarify)
paulson@15346
   234
apply (case_tac "EX j. (f (m+j), f m) : r^+")
paulson@15346
   235
 apply clarify
paulson@15346
   236
 apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ")
paulson@15346
   237
  apply clarify
paulson@15346
   238
  apply (rule_tac x = "j+i" in exI)
paulson@15346
   239
  apply (simp add: add_ac, blast)
paulson@15346
   240
apply (rule_tac x = 0 in exI, clarsimp)
paulson@15346
   241
apply (drule_tac i = m and k = k in lemma1)
paulson@15346
   242
apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
paulson@15346
   243
done
paulson@15346
   244
paulson@15346
   245
lemma wf_weak_decr_stable: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
paulson@15346
   246
      ==> EX i. ALL k. f (i+k) = f i"
paulson@15346
   247
apply (drule_tac x = 0 in lemma2 [THEN spec], auto)
paulson@15346
   248
done
paulson@15346
   249
paulson@15346
   250
(* special case of the theorem above: <= *)
paulson@15346
   251
lemma weak_decr_stable:
paulson@15346
   252
     "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i"
paulson@15346
   253
apply (rule_tac r = pred_nat in wf_weak_decr_stable)
paulson@15346
   254
apply (simp add: pred_nat_trancl_eq_le)
paulson@15346
   255
apply (intro wf_trancl wf_pred_nat)
paulson@15346
   256
done
paulson@15346
   257
haftmann@25517
   258
haftmann@25517
   259
text {*
haftmann@25517
   260
  Setup of @{text lexicographic_order} method
haftmann@25517
   261
  and @{text fun} command
haftmann@25517
   262
*}
haftmann@25517
   263
haftmann@25517
   264
use "Tools/function_package/lexicographic_order.ML"
haftmann@25517
   265
use "Tools/function_package/fundef_datatype.ML"
haftmann@25517
   266
haftmann@25517
   267
setup "LexicographicOrder.setup #> FundefDatatype.setup"
haftmann@25517
   268
nipkow@10213
   269
end