src/HOL/Wellfounded_Relations.ML
author paulson
Fri, 29 Oct 2004 15:16:02 +0200
changeset 15270 8b3f707a78a7
parent 13867 1fdecd15437f
permissions -rw-r--r--
fixed reference to renamed theorem
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title: 	HOL/Wellfounded_Relations
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     2
    ID:         $Id$
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     3
    Author: 	Konrad Slind
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     4
    Copyright   1996  TU Munich
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     5
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     6
Derived WF relations: inverse image, lexicographic product, measure, ...
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     7
*)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     8
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     9
11142
42181d7cd7b2 moved inv_image to Relation
oheimb
parents: 10996
diff changeset
    10
section "`Less than' on the natural numbers";
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    11
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    12
Goalw [less_than_def] "wf less_than"; 
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    13
by (rtac (wf_pred_nat RS wf_trancl) 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    14
qed "wf_less_than";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    15
AddIffs [wf_less_than];
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    16
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    17
Goalw [less_than_def] "trans less_than"; 
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    18
by (rtac trans_trancl 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    19
qed "trans_less_than";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    20
AddIffs [trans_less_than];
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    21
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    22
Goalw [less_than_def, less_def] "((x,y): less_than) = (x<y)"; 
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    23
by (Simp_tac 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    24
qed "less_than_iff";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    25
AddIffs [less_than_iff];
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    26
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    27
Goal "(!!n. (ALL m. Suc m <= n --> P m) ==> P n) ==> P n";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    28
by (rtac (wf_less_than RS wf_induct) 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    29
by (resolve_tac (premises()) 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    30
by Auto_tac;
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    31
qed_spec_mp "full_nat_induct";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    32
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    33
(*----------------------------------------------------------------------------
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    34
 * The inverse image into a wellfounded relation is wellfounded.
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    35
 *---------------------------------------------------------------------------*)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    36
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    37
Goal "wf(r) ==> wf(inv_image r (f::'a=>'b))"; 
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    38
by (full_simp_tac (simpset() addsimps [inv_image_def, wf_eq_minimal]) 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    39
by (Clarify_tac 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    40
by (subgoal_tac "EX (w::'b). w : {w. EX (x::'a). x: Q & (f x = w)}" 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    41
by (blast_tac (claset() delrules [allE]) 2);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    42
by (etac allE 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    43
by (mp_tac 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    44
by (Blast_tac 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    45
qed "wf_inv_image";
13867
1fdecd15437f just a few mods to a few thms
nipkow
parents: 12524
diff changeset
    46
Addsimps [wf_inv_image];
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    47
AddSIs [wf_inv_image];
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    48
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    49
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    50
(*----------------------------------------------------------------------------
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    51
 * All measures are wellfounded.
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    52
 *---------------------------------------------------------------------------*)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    53
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    54
Goalw [measure_def] "wf (measure f)";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    55
by (rtac (wf_less_than RS wf_inv_image) 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    56
qed "wf_measure";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    57
AddIffs [wf_measure];
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    58
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    59
val measure_induct = standard
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    60
    (asm_full_simplify (simpset() addsimps [measure_def,inv_image_def])
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    61
      (wf_measure RS wf_induct));
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    62
bind_thm ("measure_induct", measure_induct);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    63
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    64
(*----------------------------------------------------------------------------
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    65
 * Wellfoundedness of lexicographic combinations
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    66
 *---------------------------------------------------------------------------*)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    67
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    68
val [wfa,wfb] = goalw (the_context ()) [wf_def,lex_prod_def]
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    69
 "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    70
by (EVERY1 [rtac allI,rtac impI]);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    71
by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    72
by (rtac (wfa RS spec RS mp) 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    73
by (EVERY1 [rtac allI,rtac impI]);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    74
by (rtac (wfb RS spec RS mp) 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    75
by (Blast_tac 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    76
qed "wf_lex_prod";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    77
AddSIs [wf_lex_prod];
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    78
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    79
(*---------------------------------------------------------------------------
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    80
 * Transitivity of WF combinators.
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    81
 *---------------------------------------------------------------------------*)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    82
Goalw [trans_def, lex_prod_def]
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    83
    "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    84
by (Simp_tac 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    85
by (Blast_tac 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    86
qed "trans_lex_prod";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    87
AddSIs [trans_lex_prod];
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    88
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    89
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    90
(*---------------------------------------------------------------------------
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    91
 * Wellfoundedness of proper subset on finite sets.
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    92
 *---------------------------------------------------------------------------*)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    93
Goalw [finite_psubset_def] "wf(finite_psubset)";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    94
by (rtac (wf_measure RS wf_subset) 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    95
by (simp_tac (simpset() addsimps [measure_def, inv_image_def, less_than_def,
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    96
				 symmetric less_def])1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    97
by (fast_tac (claset() addSEs [psubset_card_mono]) 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    98
qed "wf_finite_psubset";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    99
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   100
Goalw [finite_psubset_def, trans_def] "trans finite_psubset";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   101
by (simp_tac (simpset() addsimps [psubset_def]) 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   102
by (Blast_tac 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   103
qed "trans_finite_psubset";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   104
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   105
(*---------------------------------------------------------------------------
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   106
 * Wellfoundedness of finite acyclic relations
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   107
 * Cannot go into WF because it needs Finite.
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   108
 *---------------------------------------------------------------------------*)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   109
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   110
Goal "finite r ==> acyclic r --> wf r";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   111
by (etac finite_induct 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   112
 by (Blast_tac 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   113
by (split_all_tac 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   114
by (Asm_full_simp_tac 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   115
qed_spec_mp "finite_acyclic_wf";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   116
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   117
Goal "[|finite r; acyclic r|] ==> wf (r^-1)";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   118
by (etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   119
by (etac (acyclic_converse RS iffD2) 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   120
qed "finite_acyclic_wf_converse";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   121
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   122
Goal "finite r ==> wf r = acyclic r";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   123
by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   124
qed "wf_iff_acyclic_if_finite";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   125
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   126
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   127
(*----------------------------------------------------------------------------
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   128
 * Weakly decreasing sequences (w.r.t. some well-founded order) stabilize.
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   129
 *---------------------------------------------------------------------------*)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   130
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   131
Goal "[| ALL i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   132
by (induct_tac "k" 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   133
 by (ALLGOALS Simp_tac);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   134
by (blast_tac (claset() addIs [rtrancl_trans]) 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   135
val lemma = result();
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   136
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   137
Goal "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |] \
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   138
\     ==> ALL m. f m = x --> (EX i. ALL k. f (m+i+k) = f (m+i))";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   139
by (etac wf_induct 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   140
by (Clarify_tac 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   141
by (case_tac "EX j. (f (m+j), f m) : r^+" 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   142
 by (Clarify_tac 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   143
 by (subgoal_tac "EX i. ALL k. f ((m+j)+i+k) = f ((m+j)+i)" 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   144
  by (Clarify_tac 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   145
  by (res_inst_tac [("x","j+i")] exI 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   146
  by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   147
 by (Blast_tac 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   148
by (res_inst_tac [("x","0")] exI 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   149
by (Clarsimp_tac 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   150
by (dres_inst_tac [("i","m"), ("k","k")] lemma 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   151
by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   152
val lemma = result();
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   153
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   154
Goal "[| ALL i. (f (Suc i), f i) : r^*; wf (r^+) |] \
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   155
\     ==> EX i. ALL k. f (i+k) = f i";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   156
by (dres_inst_tac [("x","0")] (lemma RS spec) 1);
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   157
by Auto_tac;
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   158
qed "wf_weak_decr_stable";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   159
11454
7514e5e21cb8 Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents: 11340
diff changeset
   160
(* special case of the theorem above: <= *)
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   161
Goal "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   162
by (res_inst_tac [("r","pred_nat")] wf_weak_decr_stable 1);
11454
7514e5e21cb8 Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents: 11340
diff changeset
   163
by (asm_simp_tac (simpset() addsimps [thm "pred_nat_trancl_eq_le"]) 1);
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   164
by (REPEAT (resolve_tac [wf_trancl,wf_pred_nat] 1));
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   165
qed "weak_decr_stable";
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   166
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   167
(*----------------------------------------------------------------------------
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   168
 * Wellfoundedness of same_fst
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   169
 *---------------------------------------------------------------------------*)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   170
11167
2c90a6167b0b added same_fstI
oheimb
parents: 11142
diff changeset
   171
Goalw[same_fst_def] "[| P x; (y',y) : R x |] ==> ((x,y'),(x,y)) : same_fst P R";
2c90a6167b0b added same_fstI
oheimb
parents: 11142
diff changeset
   172
by (Asm_simp_tac 1);
2c90a6167b0b added same_fstI
oheimb
parents: 11142
diff changeset
   173
qed "same_fstI";
11340
34a9a9126c49 added same_fstI as safe intro rule
oheimb
parents: 11167
diff changeset
   174
AddSIs[same_fstI];
11167
2c90a6167b0b added same_fstI
oheimb
parents: 11142
diff changeset
   175
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   176
val prems = goalw thy [same_fst_def]
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   177
  "(!!x. P x ==> wf(R x)) ==> wf(same_fst P R)";
12486
0ed8bdd883e0 isatool expandshort;
wenzelm
parents: 11454
diff changeset
   178
by (full_simp_tac (simpset() delcongs [imp_cong] addsimps [wf_def]) 1);
0ed8bdd883e0 isatool expandshort;
wenzelm
parents: 11454
diff changeset
   179
by (strip_tac 1);
0ed8bdd883e0 isatool expandshort;
wenzelm
parents: 11454
diff changeset
   180
by (rename_tac "a b" 1);
0ed8bdd883e0 isatool expandshort;
wenzelm
parents: 11454
diff changeset
   181
by (case_tac "wf(R a)" 1);
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
   182
 by (eres_inst_tac [("a","b")] wf_induct 1);
12486
0ed8bdd883e0 isatool expandshort;
wenzelm
parents: 11454
diff changeset
   183
 by (Blast_tac 1);
0ed8bdd883e0 isatool expandshort;
wenzelm
parents: 11454
diff changeset
   184
by (blast_tac (claset() addIs prems) 1);
10653
55f33da63366 small mods.
nipkow
parents: 10231
diff changeset
   185
qed "wf_same_fst";