src/HOL/Wellfounded_Relations.thy
author paulson
Wed Dec 01 12:53:49 2004 +0100 (2004-12-01)
changeset 15352 cba05842bd7a
parent 15348 0a60f15c2d7a
child 18277 6c2b039b4847
permissions -rw-r--r--
fixed presentation
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
paulson@15346
     9
imports Finite_Set
paulson@15346
    10
begin
paulson@15346
    11
paulson@15346
    12
text{*Derived WF relations such as inverse image, lexicographic product and
paulson@15346
    13
measure. The simple relational product, in which @{term "(x',y')"} precedes
paulson@15346
    14
@{term "(x,y)"} if @{term "x'<x"} and @{term "y'<y"}, is a subset of the
paulson@15346
    15
lexicographic product, and therefore does not need to be defined separately.*}
nipkow@10213
    16
nipkow@10213
    17
constdefs
nipkow@10213
    18
 less_than :: "(nat*nat)set"
paulson@15346
    19
    "less_than == trancl pred_nat"
nipkow@10213
    20
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
paulson@15346
    40
paulson@15346
    41
subsection{*Measure Functions make Wellfounded Relations*}
paulson@15346
    42
paulson@15346
    43
subsubsection{*`Less than' on the natural numbers*}
paulson@15346
    44
paulson@15346
    45
lemma wf_less_than [iff]: "wf less_than"
paulson@15346
    46
by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])
paulson@15346
    47
paulson@15346
    48
lemma trans_less_than [iff]: "trans less_than"
paulson@15346
    49
by (simp add: less_than_def trans_trancl)
paulson@15346
    50
paulson@15346
    51
lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)"
paulson@15346
    52
by (simp add: less_than_def less_def)
paulson@15346
    53
paulson@15346
    54
lemma full_nat_induct:
paulson@15346
    55
  assumes ih: "(!!n. (ALL m. Suc m <= n --> P m) ==> P n)"
paulson@15346
    56
  shows "P n"
paulson@15346
    57
apply (rule wf_less_than [THEN wf_induct])
paulson@15346
    58
apply (rule ih, auto)
paulson@15346
    59
done
paulson@15346
    60
paulson@15346
    61
subsubsection{*The Inverse Image into a Wellfounded Relation is Wellfounded.*}
paulson@15346
    62
paulson@15346
    63
lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))"
paulson@15346
    64
apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal)
paulson@15346
    65
apply clarify
paulson@15346
    66
apply (subgoal_tac "EX (w::'b) . w : {w. EX (x::'a) . x: Q & (f x = w) }")
paulson@15346
    67
prefer 2 apply (blast del: allE)
paulson@15346
    68
apply (erule allE)
paulson@15346
    69
apply (erule (1) notE impE)
paulson@15346
    70
apply blast
paulson@15346
    71
done
nipkow@10213
    72
paulson@15346
    73
paulson@15346
    74
subsubsection{*Finally, All Measures are Wellfounded.*}
paulson@15346
    75
paulson@15346
    76
lemma wf_measure [iff]: "wf (measure f)"
paulson@15346
    77
apply (unfold measure_def)
paulson@15346
    78
apply (rule wf_less_than [THEN wf_inv_image])
paulson@15346
    79
done
paulson@15346
    80
paulson@15346
    81
lemmas measure_induct =
paulson@15346
    82
    wf_measure [THEN wf_induct, unfolded measure_def inv_image_def, 
paulson@15346
    83
                simplified, standard]
paulson@15346
    84
paulson@15346
    85
paulson@15346
    86
subsection{*Other Ways of Constructing Wellfounded Relations*}
paulson@15346
    87
paulson@15346
    88
text{*Wellfoundedness of lexicographic combinations*}
paulson@15346
    89
lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
paulson@15346
    90
apply (unfold wf_def lex_prod_def) 
paulson@15346
    91
apply (rule allI, rule impI)
paulson@15346
    92
apply (simp (no_asm_use) only: split_paired_All)
paulson@15346
    93
apply (drule spec, erule mp) 
paulson@15346
    94
apply (rule allI, rule impI)
paulson@15346
    95
apply (drule spec, erule mp, blast) 
paulson@15346
    96
done
paulson@15346
    97
paulson@15346
    98
paulson@15346
    99
text{*Transitivity of WF combinators.*}
paulson@15346
   100
lemma trans_lex_prod [intro!]: 
paulson@15346
   101
    "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
paulson@15346
   102
by (unfold trans_def lex_prod_def, blast) 
paulson@15346
   103
paulson@15346
   104
paulson@15346
   105
subsubsection{*Wellfoundedness of proper subset on finite sets.*}
paulson@15346
   106
lemma wf_finite_psubset: "wf(finite_psubset)"
paulson@15346
   107
apply (unfold finite_psubset_def)
paulson@15346
   108
apply (rule wf_measure [THEN wf_subset])
paulson@15346
   109
apply (simp add: measure_def inv_image_def less_than_def less_def [symmetric])
paulson@15346
   110
apply (fast elim!: psubset_card_mono)
paulson@15346
   111
done
paulson@15346
   112
paulson@15346
   113
lemma trans_finite_psubset: "trans finite_psubset"
paulson@15346
   114
by (simp add: finite_psubset_def psubset_def trans_def, blast)
paulson@15346
   115
paulson@15346
   116
paulson@15346
   117
subsubsection{*Wellfoundedness of finite acyclic relations*}
paulson@15346
   118
paulson@15346
   119
text{*This proof belongs in this theory because it needs Finite.*}
nipkow@10213
   120
paulson@15346
   121
lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r"
paulson@15346
   122
apply (erule finite_induct, blast)
paulson@15346
   123
apply (simp (no_asm_simp) only: split_tupled_all)
paulson@15346
   124
apply simp
paulson@15346
   125
done
paulson@15346
   126
paulson@15346
   127
lemma finite_acyclic_wf_converse: "[|finite r; acyclic r|] ==> wf (r^-1)"
paulson@15346
   128
apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])
paulson@15346
   129
apply (erule acyclic_converse [THEN iffD2])
paulson@15346
   130
done
paulson@15346
   131
paulson@15346
   132
lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r"
paulson@15346
   133
by (blast intro: finite_acyclic_wf wf_acyclic)
paulson@15346
   134
paulson@15346
   135
paulson@15352
   136
subsubsection{*Wellfoundedness of @{term same_fst}*}
paulson@15346
   137
paulson@15346
   138
lemma same_fstI [intro!]:
paulson@15346
   139
     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
paulson@15346
   140
by (simp add: same_fst_def)
paulson@15346
   141
paulson@15346
   142
lemma wf_same_fst:
paulson@15346
   143
  assumes prem: "(!!x. P x ==> wf(R x))"
paulson@15346
   144
  shows "wf(same_fst P R)"
paulson@15346
   145
apply (simp cong del: imp_cong add: wf_def same_fst_def)
paulson@15346
   146
apply (intro strip)
paulson@15346
   147
apply (rename_tac a b)
paulson@15346
   148
apply (case_tac "wf (R a)")
paulson@15346
   149
 apply (erule_tac a = b in wf_induct, blast)
paulson@15346
   150
apply (blast intro: prem)
paulson@15346
   151
done
paulson@15346
   152
paulson@15346
   153
paulson@15346
   154
subsection{*Weakly decreasing sequences (w.r.t. some well-founded order) 
paulson@15346
   155
   stabilize.*}
paulson@15346
   156
paulson@15346
   157
text{*This material does not appear to be used any longer.*}
paulson@15346
   158
paulson@15346
   159
lemma lemma1: "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*"
paulson@15346
   160
apply (induct_tac "k", simp_all)
paulson@15346
   161
apply (blast intro: rtrancl_trans)
paulson@15346
   162
done
paulson@15346
   163
paulson@15346
   164
lemma lemma2: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
paulson@15346
   165
      ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))"
paulson@15346
   166
apply (erule wf_induct, clarify)
paulson@15346
   167
apply (case_tac "EX j. (f (m+j), f m) : r^+")
paulson@15346
   168
 apply clarify
paulson@15346
   169
 apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ")
paulson@15346
   170
  apply clarify
paulson@15346
   171
  apply (rule_tac x = "j+i" in exI)
paulson@15346
   172
  apply (simp add: add_ac, blast)
paulson@15346
   173
apply (rule_tac x = 0 in exI, clarsimp)
paulson@15346
   174
apply (drule_tac i = m and k = k in lemma1)
paulson@15346
   175
apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
paulson@15346
   176
done
paulson@15346
   177
paulson@15346
   178
lemma wf_weak_decr_stable: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
paulson@15346
   179
      ==> EX i. ALL k. f (i+k) = f i"
paulson@15346
   180
apply (drule_tac x = 0 in lemma2 [THEN spec], auto)
paulson@15346
   181
done
paulson@15346
   182
paulson@15346
   183
(* special case of the theorem above: <= *)
paulson@15346
   184
lemma weak_decr_stable:
paulson@15346
   185
     "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i"
paulson@15346
   186
apply (rule_tac r = pred_nat in wf_weak_decr_stable)
paulson@15346
   187
apply (simp add: pred_nat_trancl_eq_le)
paulson@15346
   188
apply (intro wf_trancl wf_pred_nat)
paulson@15346
   189
done
paulson@15346
   190
paulson@15346
   191
paulson@15346
   192
ML
paulson@15346
   193
{*
paulson@15346
   194
val less_than_def = thm "less_than_def";
paulson@15346
   195
val measure_def = thm "measure_def";
paulson@15346
   196
val lex_prod_def = thm "lex_prod_def";
paulson@15346
   197
val finite_psubset_def = thm "finite_psubset_def";
paulson@15346
   198
paulson@15346
   199
val wf_less_than = thm "wf_less_than";
paulson@15346
   200
val trans_less_than = thm "trans_less_than";
paulson@15346
   201
val less_than_iff = thm "less_than_iff";
paulson@15346
   202
val full_nat_induct = thm "full_nat_induct";
paulson@15346
   203
val wf_inv_image = thm "wf_inv_image";
paulson@15346
   204
val wf_measure = thm "wf_measure";
paulson@15346
   205
val measure_induct = thm "measure_induct";
paulson@15346
   206
val wf_lex_prod = thm "wf_lex_prod";
paulson@15346
   207
val trans_lex_prod = thm "trans_lex_prod";
paulson@15346
   208
val wf_finite_psubset = thm "wf_finite_psubset";
paulson@15346
   209
val trans_finite_psubset = thm "trans_finite_psubset";
paulson@15346
   210
val finite_acyclic_wf = thm "finite_acyclic_wf";
paulson@15346
   211
val finite_acyclic_wf_converse = thm "finite_acyclic_wf_converse";
paulson@15346
   212
val wf_iff_acyclic_if_finite = thm "wf_iff_acyclic_if_finite";
paulson@15346
   213
val wf_weak_decr_stable = thm "wf_weak_decr_stable";
paulson@15346
   214
val weak_decr_stable = thm "weak_decr_stable";
paulson@15346
   215
val same_fstI = thm "same_fstI";
paulson@15346
   216
val wf_same_fst = thm "wf_same_fst";
paulson@15346
   217
*}
paulson@15346
   218
nipkow@10213
   219
nipkow@10213
   220
end