src/HOL/Wellfounded_Relations.thy
author wenzelm
Mon, 28 Nov 2005 10:58:40 +0100
changeset 18277 6c2b039b4847
parent 15352 cba05842bd7a
child 19404 9bf2cdc9e8e8
permissions -rw-r--r--
added proof of measure_induct_rule;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15346
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
     1
(*  ID:   $Id$
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     2
    Author:     Konrad Slind
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     3
    Copyright   1995 TU Munich
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     4
*)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     5
15346
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
     6
header {*Well-founded Relations*}
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
     7
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
     8
theory Wellfounded_Relations
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
     9
imports Finite_Set
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    10
begin
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    11
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    12
text{*Derived WF relations such as inverse image, lexicographic product and
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    13
measure. The simple relational product, in which @{term "(x',y')"} precedes
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    14
@{term "(x,y)"} if @{term "x'<x"} and @{term "y'<y"}, is a subset of the
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    15
lexicographic product, and therefore does not need to be defined separately.*}
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    16
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    17
constdefs
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    18
 less_than :: "(nat*nat)set"
15346
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    19
    "less_than == trancl pred_nat"
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    20
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    21
 measure   :: "('a => nat) => ('a * 'a)set"
15346
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    22
    "measure == inv_image less_than"
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    23
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    24
 lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    25
               (infixr "<*lex*>" 80)
15346
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    26
    "ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    27
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    28
 finite_psubset  :: "('a set * 'a set) set"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    29
   --{* finite proper subset*}
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    30
    "finite_psubset == {(A,B). A < B & finite B}"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    31
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    32
 same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    33
    "same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    34
   --{*For @{text rec_def} declarations where the first n parameters
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    35
       stay unchanged in the recursive call. 
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    36
       See @{text "Library/While_Combinator.thy"} for an application.*}
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    37
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    38
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    39
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    40
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    41
subsection{*Measure Functions make Wellfounded Relations*}
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    42
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    43
subsubsection{*`Less than' on the natural numbers*}
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    44
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    45
lemma wf_less_than [iff]: "wf less_than"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    46
by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    47
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    48
lemma trans_less_than [iff]: "trans less_than"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    49
by (simp add: less_than_def trans_trancl)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    50
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    51
lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    52
by (simp add: less_than_def less_def)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    53
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    54
lemma full_nat_induct:
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    55
  assumes ih: "(!!n. (ALL m. Suc m <= n --> P m) ==> P n)"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    56
  shows "P n"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    57
apply (rule wf_less_than [THEN wf_induct])
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    58
apply (rule ih, auto)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    59
done
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    60
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    61
subsubsection{*The Inverse Image into a Wellfounded Relation is Wellfounded.*}
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    62
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    63
lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    64
apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    65
apply clarify
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    66
apply (subgoal_tac "EX (w::'b) . w : {w. EX (x::'a) . x: Q & (f x = w) }")
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    67
prefer 2 apply (blast del: allE)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    68
apply (erule allE)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    69
apply (erule (1) notE impE)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    70
apply blast
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    71
done
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    72
15346
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    73
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    74
subsubsection{*Finally, All Measures are Wellfounded.*}
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    75
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    76
lemma wf_measure [iff]: "wf (measure f)"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    77
apply (unfold measure_def)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    78
apply (rule wf_less_than [THEN wf_inv_image])
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    79
done
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
    80
18277
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    81
lemma measure_induct_rule [case_names less]:
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    82
  fixes f :: "'a \<Rightarrow> nat"
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    83
  assumes step: "\<And>x. (\<And>y. f y < f x \<Longrightarrow> P y) \<Longrightarrow> P x"
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    84
  shows "P a"
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    85
proof -
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    86
  have "wf (measure f)" ..
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    87
  then show ?thesis
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    88
  proof induct
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    89
    case (less x)
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    90
    show ?case
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    91
    proof (rule step)
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    92
      fix y
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    93
      assume "f y < f x"
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    94
      then have "(y, x) \<in> measure f"
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    95
        by (simp add: measure_def inv_image_def)
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    96
      then show "P y" by (rule less)
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    97
    qed
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    98
  qed
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
    99
qed
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
   100
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
   101
lemma measure_induct:
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
   102
  fixes f :: "'a \<Rightarrow> nat"
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
   103
  shows "(\<And>x. \<forall>y. f y < f x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
6c2b039b4847 added proof of measure_induct_rule;
wenzelm
parents: 15352
diff changeset
   104
  by (rule measure_induct_rule [of f P a]) iprover
15346
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   105
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   106
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   107
subsection{*Other Ways of Constructing Wellfounded Relations*}
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   108
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   109
text{*Wellfoundedness of lexicographic combinations*}
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   110
lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   111
apply (unfold wf_def lex_prod_def) 
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   112
apply (rule allI, rule impI)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   113
apply (simp (no_asm_use) only: split_paired_All)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   114
apply (drule spec, erule mp) 
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   115
apply (rule allI, rule impI)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   116
apply (drule spec, erule mp, blast) 
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   117
done
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   118
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   119
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   120
text{*Transitivity of WF combinators.*}
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   121
lemma trans_lex_prod [intro!]: 
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   122
    "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   123
by (unfold trans_def lex_prod_def, blast) 
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   124
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   125
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   126
subsubsection{*Wellfoundedness of proper subset on finite sets.*}
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   127
lemma wf_finite_psubset: "wf(finite_psubset)"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   128
apply (unfold finite_psubset_def)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   129
apply (rule wf_measure [THEN wf_subset])
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   130
apply (simp add: measure_def inv_image_def less_than_def less_def [symmetric])
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   131
apply (fast elim!: psubset_card_mono)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   132
done
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   133
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   134
lemma trans_finite_psubset: "trans finite_psubset"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   135
by (simp add: finite_psubset_def psubset_def trans_def, blast)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   136
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   137
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   138
subsubsection{*Wellfoundedness of finite acyclic relations*}
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   139
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   140
text{*This proof belongs in this theory because it needs Finite.*}
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   141
15346
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   142
lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   143
apply (erule finite_induct, blast)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   144
apply (simp (no_asm_simp) only: split_tupled_all)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   145
apply simp
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   146
done
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   147
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   148
lemma finite_acyclic_wf_converse: "[|finite r; acyclic r|] ==> wf (r^-1)"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   149
apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   150
apply (erule acyclic_converse [THEN iffD2])
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   151
done
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   152
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   153
lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   154
by (blast intro: finite_acyclic_wf wf_acyclic)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   155
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   156
15352
cba05842bd7a fixed presentation
paulson
parents: 15348
diff changeset
   157
subsubsection{*Wellfoundedness of @{term same_fst}*}
15346
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   158
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   159
lemma same_fstI [intro!]:
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   160
     "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   161
by (simp add: same_fst_def)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   162
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   163
lemma wf_same_fst:
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   164
  assumes prem: "(!!x. P x ==> wf(R x))"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   165
  shows "wf(same_fst P R)"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   166
apply (simp cong del: imp_cong add: wf_def same_fst_def)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   167
apply (intro strip)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   168
apply (rename_tac a b)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   169
apply (case_tac "wf (R a)")
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   170
 apply (erule_tac a = b in wf_induct, blast)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   171
apply (blast intro: prem)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   172
done
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   173
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   174
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   175
subsection{*Weakly decreasing sequences (w.r.t. some well-founded order) 
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   176
   stabilize.*}
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   177
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   178
text{*This material does not appear to be used any longer.*}
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   179
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   180
lemma lemma1: "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   181
apply (induct_tac "k", simp_all)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   182
apply (blast intro: rtrancl_trans)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   183
done
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   184
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   185
lemma lemma2: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   186
      ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   187
apply (erule wf_induct, clarify)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   188
apply (case_tac "EX j. (f (m+j), f m) : r^+")
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   189
 apply clarify
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   190
 apply (subgoal_tac "EX i. ALL k. f ((m+j) +i+k) = f ( (m+j) +i) ")
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   191
  apply clarify
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   192
  apply (rule_tac x = "j+i" in exI)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   193
  apply (simp add: add_ac, blast)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   194
apply (rule_tac x = 0 in exI, clarsimp)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   195
apply (drule_tac i = m and k = k in lemma1)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   196
apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   197
done
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   198
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   199
lemma wf_weak_decr_stable: "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |]  
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   200
      ==> EX i. ALL k. f (i+k) = f i"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   201
apply (drule_tac x = 0 in lemma2 [THEN spec], auto)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   202
done
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   203
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   204
(* special case of the theorem above: <= *)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   205
lemma weak_decr_stable:
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   206
     "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i"
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   207
apply (rule_tac r = pred_nat in wf_weak_decr_stable)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   208
apply (simp add: pred_nat_trancl_eq_le)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   209
apply (intro wf_trancl wf_pred_nat)
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   210
done
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   211
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   212
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   213
ML
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   214
{*
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   215
val less_than_def = thm "less_than_def";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   216
val measure_def = thm "measure_def";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   217
val lex_prod_def = thm "lex_prod_def";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   218
val finite_psubset_def = thm "finite_psubset_def";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   219
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   220
val wf_less_than = thm "wf_less_than";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   221
val trans_less_than = thm "trans_less_than";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   222
val less_than_iff = thm "less_than_iff";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   223
val full_nat_induct = thm "full_nat_induct";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   224
val wf_inv_image = thm "wf_inv_image";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   225
val wf_measure = thm "wf_measure";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   226
val measure_induct = thm "measure_induct";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   227
val wf_lex_prod = thm "wf_lex_prod";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   228
val trans_lex_prod = thm "trans_lex_prod";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   229
val wf_finite_psubset = thm "wf_finite_psubset";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   230
val trans_finite_psubset = thm "trans_finite_psubset";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   231
val finite_acyclic_wf = thm "finite_acyclic_wf";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   232
val finite_acyclic_wf_converse = thm "finite_acyclic_wf_converse";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   233
val wf_iff_acyclic_if_finite = thm "wf_iff_acyclic_if_finite";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   234
val wf_weak_decr_stable = thm "wf_weak_decr_stable";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   235
val weak_decr_stable = thm "weak_decr_stable";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   236
val same_fstI = thm "same_fstI";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   237
val wf_same_fst = thm "wf_same_fst";
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   238
*}
ac272926fb77 converted Wellfounded_Relations to Isar script
paulson
parents: 12398
diff changeset
   239
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   240
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   241
end