src/HOL/WF_Rel.ML
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 8703 816d8f6513be
child 9076 108ec332625d
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     1
(*  Title: 	HOL/WF_Rel
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     2
    ID:         $Id$
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     3
    Author: 	Konrad Slind
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     4
    Copyright   1996  TU Munich
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     5
3296
2ee6c397003d Deleted rprod: lex_prod is (usually?) enough
paulson
parents: 3237
diff changeset
     6
Derived WF relations: inverse image, lexicographic product, measure, ...
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     7
*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     8
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     9
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    10
(*----------------------------------------------------------------------------
3237
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    11
 * "Less than" on the natural numbers
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    12
 *---------------------------------------------------------------------------*)
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    13
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4751
diff changeset
    14
Goalw [less_than_def] "wf less_than"; 
3237
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    15
by (rtac (wf_pred_nat RS wf_trancl) 1);
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    16
qed "wf_less_than";
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    17
AddIffs [wf_less_than];
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    18
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4751
diff changeset
    19
Goalw [less_than_def] "trans less_than"; 
3237
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    20
by (rtac trans_trancl 1);
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    21
qed "trans_less_than";
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    22
AddIffs [trans_less_than];
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    23
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4751
diff changeset
    24
Goalw [less_than_def, less_def] "((x,y): less_than) = (x<y)"; 
3237
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    25
by (Simp_tac 1);
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    26
qed "less_than_iff";
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    27
AddIffs [less_than_iff];
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    28
8158
b4700243eb9c added full_nat_induct
oheimb
parents: 7031
diff changeset
    29
Goal "(!!n. (!m. Suc m <= n --> P m) ==> P n) ==> P n";
8254
84a5fe44520f expandshort
paulson
parents: 8158
diff changeset
    30
by (rtac (wf_less_than RS wf_induct) 1);
8158
b4700243eb9c added full_nat_induct
oheimb
parents: 7031
diff changeset
    31
by (resolve_tac (premises()) 1);
b4700243eb9c added full_nat_induct
oheimb
parents: 7031
diff changeset
    32
by Auto_tac;
b4700243eb9c added full_nat_induct
oheimb
parents: 7031
diff changeset
    33
qed_spec_mp "full_nat_induct";
b4700243eb9c added full_nat_induct
oheimb
parents: 7031
diff changeset
    34
3237
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    35
(*----------------------------------------------------------------------------
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    36
 * The inverse image into a wellfounded relation is wellfounded.
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    37
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    38
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    39
Goal "wf(r) ==> wf(inv_image r (f::'a=>'b))"; 
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3718
diff changeset
    40
by (full_simp_tac (simpset() addsimps [inv_image_def, wf_eq_minimal]) 1);
3718
d78cf498a88c Minor tidying to use Clarify_tac, etc.
paulson
parents: 3484
diff changeset
    41
by (Clarify_tac 1);
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    42
by (subgoal_tac "? (w::'b). w : {w. ? (x::'a). x: Q & (f x = w)}" 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3718
diff changeset
    43
by (blast_tac (claset() delrules [allE]) 2);
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    44
by (etac allE 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    45
by (mp_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    46
by (Blast_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    47
qed "wf_inv_image";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    48
AddSIs [wf_inv_image];
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    49
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4751
diff changeset
    50
Goalw [trans_def,inv_image_def]
3237
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    51
    "!!r. trans r ==> trans (inv_image r f)";
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    52
by (Simp_tac 1);
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    53
by (Blast_tac 1);
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    54
qed "trans_inv_image";
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    55
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    56
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    57
(*----------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    58
 * All measures are wellfounded.
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    59
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    60
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4751
diff changeset
    61
Goalw [measure_def] "wf (measure f)";
3237
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    62
by (rtac (wf_less_than RS wf_inv_image) 1);
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    63
qed "wf_measure";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    64
AddIffs [wf_measure];
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    65
4643
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4089
diff changeset
    66
val measure_induct = standard
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4089
diff changeset
    67
    (asm_full_simplify (simpset() addsimps [measure_def,inv_image_def])
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4089
diff changeset
    68
      (wf_measure RS wf_induct));
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4089
diff changeset
    69
store_thm("measure_induct",measure_induct);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4089
diff changeset
    70
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    71
(*----------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    72
 * Wellfoundedness of lexicographic combinations
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    73
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    74
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    75
val [wfa,wfb] = goalw thy [wf_def,lex_prod_def]
8703
816d8f6513be Times -> <*>
nipkow
parents: 8556
diff changeset
    76
 "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)";
3413
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3296
diff changeset
    77
by (EVERY1 [rtac allI,rtac impI]);
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3296
diff changeset
    78
by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1);
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    79
by (rtac (wfa RS spec RS mp) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    80
by (EVERY1 [rtac allI,rtac impI]);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    81
by (rtac (wfb RS spec RS mp) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    82
by (Blast_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    83
qed "wf_lex_prod";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    84
AddSIs [wf_lex_prod];
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    85
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    86
(*---------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    87
 * Transitivity of WF combinators.
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    88
 *---------------------------------------------------------------------------*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4751
diff changeset
    89
Goalw [trans_def, lex_prod_def]
8703
816d8f6513be Times -> <*>
nipkow
parents: 8556
diff changeset
    90
    "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)";
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    91
by (Simp_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    92
by (Blast_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    93
qed "trans_lex_prod";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    94
AddSIs [trans_lex_prod];
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    95
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    96
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    97
(*---------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    98
 * Wellfoundedness of proper subset on finite sets.
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    99
 *---------------------------------------------------------------------------*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4751
diff changeset
   100
Goalw [finite_psubset_def] "wf(finite_psubset)";
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   101
by (rtac (wf_measure RS wf_subset) 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3718
diff changeset
   102
by (simp_tac (simpset() addsimps [measure_def, inv_image_def, less_than_def,
3237
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
   103
				 symmetric less_def])1);
8556
52ef986bd0a6 made a proof more robust (did not like Suc_less_eq)
paulson
parents: 8254
diff changeset
   104
by (fast_tac (claset() addSEs [psubset_card]) 1);
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   105
qed "wf_finite_psubset";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   106
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4751
diff changeset
   107
Goalw [finite_psubset_def, trans_def] "trans finite_psubset";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3718
diff changeset
   108
by (simp_tac (simpset() addsimps [psubset_def]) 1);
3237
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
   109
by (Blast_tac 1);
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
   110
qed "trans_finite_psubset";
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   111
3413
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3296
diff changeset
   112
(*---------------------------------------------------------------------------
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3296
diff changeset
   113
 * Wellfoundedness of finite acyclic relations
5144
7ac22e5a05d7 Minor tidying up.
nipkow
parents: 5143
diff changeset
   114
 * Cannot go into WF because it needs Finite.
3413
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3296
diff changeset
   115
 *---------------------------------------------------------------------------*)
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3296
diff changeset
   116
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   117
Goal "finite r ==> acyclic r --> wf r";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   118
by (etac finite_induct 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   119
 by (Blast_tac 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   120
by (split_all_tac 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   121
by (Asm_full_simp_tac 1);
3413
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3296
diff changeset
   122
qed_spec_mp "finite_acyclic_wf";
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3296
diff changeset
   123
7031
972b5f62f476 getting rid of qed_goal
paulson
parents: 6803
diff changeset
   124
Goal "[|finite r; acyclic r|] ==> wf (r^-1)";
972b5f62f476 getting rid of qed_goal
paulson
parents: 6803
diff changeset
   125
by (etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 6803
diff changeset
   126
by (etac (acyclic_converse RS iffD2) 1);
972b5f62f476 getting rid of qed_goal
paulson
parents: 6803
diff changeset
   127
qed "finite_acyclic_wf_converse";
4749
35b47e36e615 added finite_acyclic_wf_converse
oheimb
parents: 4643
diff changeset
   128
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   129
Goal "finite r ==> wf r = acyclic r";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3718
diff changeset
   130
by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1);
3413
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3296
diff changeset
   131
qed "wf_iff_acyclic_if_finite";
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3296
diff changeset
   132
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3296
diff changeset
   133
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3296
diff changeset
   134
(*---------------------------------------------------------------------------
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3296
diff changeset
   135
 * A relation is wellfounded iff it has no infinite descending chain
5144
7ac22e5a05d7 Minor tidying up.
nipkow
parents: 5143
diff changeset
   136
 * Cannot go into WF because it needs type nat.
3413
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3296
diff changeset
   137
 *---------------------------------------------------------------------------*)
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3296
diff changeset
   138
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4751
diff changeset
   139
Goalw [wf_eq_minimal RS eq_reflection]
3413
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3296
diff changeset
   140
  "wf r = (~(? f. !i. (f(Suc i),f i) : r))";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   141
by (rtac iffI 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   142
 by (rtac notI 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   143
 by (etac exE 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   144
 by (eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   145
 by (Blast_tac 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   146
by (etac swap 1);
3446
a14e5451f613 Addition of not_imp (which pushes negation into implication) as a default
paulson
parents: 3436
diff changeset
   147
by (Asm_full_simp_tac 1);
3718
d78cf498a88c Minor tidying to use Clarify_tac, etc.
paulson
parents: 3484
diff changeset
   148
by (Clarify_tac 1);
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   149
by (subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
3436
d68dbb8f22d3 Tuned wf_iff_no_infinite_down_chain proof, based on Konrads ideas.
nipkow
parents: 3413
diff changeset
   150
 by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   151
 by (rtac allI 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   152
 by (Simp_tac 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   153
 by (rtac selectI2EX 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   154
  by (Blast_tac 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   155
 by (Blast_tac 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   156
by (rtac allI 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   157
by (induct_tac "n" 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   158
 by (Asm_simp_tac 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   159
by (Simp_tac 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   160
by (rtac selectI2EX 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   161
 by (Blast_tac 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3446
diff changeset
   162
by (Blast_tac 1);
3413
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents: 3296
diff changeset
   163
qed "wf_iff_no_infinite_down_chain";
6803
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   164
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   165
(*----------------------------------------------------------------------------
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   166
 * Weakly decreasing sequences (w.r.t. some well-founded order) stabilize.
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   167
 *---------------------------------------------------------------------------*)
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   168
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   169
Goal "[| ! i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*";
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   170
by (induct_tac "k" 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   171
 by (ALLGOALS Simp_tac);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   172
by (blast_tac (claset() addIs [rtrancl_trans]) 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   173
val lemma = result();
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   174
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   175
Goal "[| ! i. (f (Suc i), f i) : r^*; wf (r^+) |] \
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   176
\     ==> ! m. f m = x --> (? i. ! k. f (m+i+k) = f (m+i))";
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   177
by (etac wf_induct 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   178
by (Clarify_tac 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   179
by (case_tac "? j. (f (m+j), f m) : r^+" 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   180
 by (Clarify_tac 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   181
 by (subgoal_tac "? i. ! k. f ((m+j)+i+k) = f ((m+j)+i)" 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   182
  by (Clarify_tac 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   183
  by (res_inst_tac [("x","j+i")] exI 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   184
  by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   185
 by (Blast_tac 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   186
by (res_inst_tac [("x","0")] exI 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   187
by (Clarsimp_tac 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   188
by (dres_inst_tac [("i","m"), ("k","k")] lemma 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   189
by (fast_tac (claset() addDs [rtranclE,rtrancl_into_trancl1]) 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   190
val lemma = result();
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   191
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   192
Goal "[| ! i. (f (Suc i), f i) : r^*; wf (r^+) |] \
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   193
\     ==> ? i. ! k. f (i+k) = f i";
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   194
by (dres_inst_tac [("x","0")] (lemma RS spec) 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   195
by Auto_tac;
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   196
qed "wf_weak_decr_stable";
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   197
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   198
(* special case: <= *)
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   199
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   200
Goal "(m, n) : pred_nat^* = (m <= n)";
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   201
by (simp_tac (simpset() addsimps [less_eq, reflcl_trancl RS sym] 
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   202
                        delsimps [reflcl_trancl]) 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   203
by (arith_tac 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   204
qed "le_eq";
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   205
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   206
Goal "[| ! i. f (Suc i) <= ((f i)::nat) |] ==> ? i. ! k. f (i+k) = f i";
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   207
by (res_inst_tac [("r","pred_nat")] wf_weak_decr_stable 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   208
by (asm_simp_tac (simpset() addsimps [le_eq]) 1);
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   209
by (REPEAT (resolve_tac [wf_trancl,wf_pred_nat] 1));
8273e5a17a43 Stefan Merz's lemmas.
nipkow
parents: 5144
diff changeset
   210
qed "weak_decr_stable";