src/HOL/WF_Rel.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5144 7ac22e5a05d7
child 6803 8273e5a17a43
permissions -rw-r--r--
tidying
paulson@3193
     1
(*  Title: 	HOL/WF_Rel
paulson@3193
     2
    ID:         $Id$
paulson@3193
     3
    Author: 	Konrad Slind
paulson@3193
     4
    Copyright   1996  TU Munich
paulson@3193
     5
paulson@3296
     6
Derived WF relations: inverse image, lexicographic product, measure, ...
paulson@3193
     7
*)
paulson@3193
     8
paulson@3193
     9
open WF_Rel;
paulson@3193
    10
paulson@3193
    11
paulson@3193
    12
(*----------------------------------------------------------------------------
paulson@3237
    13
 * "Less than" on the natural numbers
paulson@3237
    14
 *---------------------------------------------------------------------------*)
paulson@3237
    15
wenzelm@5069
    16
Goalw [less_than_def] "wf less_than"; 
paulson@3237
    17
by (rtac (wf_pred_nat RS wf_trancl) 1);
paulson@3237
    18
qed "wf_less_than";
paulson@3237
    19
AddIffs [wf_less_than];
paulson@3237
    20
wenzelm@5069
    21
Goalw [less_than_def] "trans less_than"; 
paulson@3237
    22
by (rtac trans_trancl 1);
paulson@3237
    23
qed "trans_less_than";
paulson@3237
    24
AddIffs [trans_less_than];
paulson@3237
    25
wenzelm@5069
    26
Goalw [less_than_def, less_def] "((x,y): less_than) = (x<y)"; 
paulson@3237
    27
by (Simp_tac 1);
paulson@3237
    28
qed "less_than_iff";
paulson@3237
    29
AddIffs [less_than_iff];
paulson@3237
    30
paulson@3237
    31
(*----------------------------------------------------------------------------
paulson@3193
    32
 * The inverse image into a wellfounded relation is wellfounded.
paulson@3193
    33
 *---------------------------------------------------------------------------*)
paulson@3193
    34
paulson@5143
    35
Goal "wf(r) ==> wf(inv_image r (f::'a=>'b))"; 
wenzelm@4089
    36
by (full_simp_tac (simpset() addsimps [inv_image_def, wf_eq_minimal]) 1);
paulson@3718
    37
by (Clarify_tac 1);
paulson@3193
    38
by (subgoal_tac "? (w::'b). w : {w. ? (x::'a). x: Q & (f x = w)}" 1);
wenzelm@4089
    39
by (blast_tac (claset() delrules [allE]) 2);
paulson@3193
    40
by (etac allE 1);
paulson@3193
    41
by (mp_tac 1);
paulson@3193
    42
by (Blast_tac 1);
paulson@3193
    43
qed "wf_inv_image";
paulson@3193
    44
AddSIs [wf_inv_image];
paulson@3193
    45
wenzelm@5069
    46
Goalw [trans_def,inv_image_def]
paulson@3237
    47
    "!!r. trans r ==> trans (inv_image r f)";
paulson@3237
    48
by (Simp_tac 1);
paulson@3237
    49
by (Blast_tac 1);
paulson@3237
    50
qed "trans_inv_image";
paulson@3237
    51
paulson@3237
    52
paulson@3193
    53
(*----------------------------------------------------------------------------
paulson@3193
    54
 * All measures are wellfounded.
paulson@3193
    55
 *---------------------------------------------------------------------------*)
paulson@3193
    56
wenzelm@5069
    57
Goalw [measure_def] "wf (measure f)";
paulson@3237
    58
by (rtac (wf_less_than RS wf_inv_image) 1);
paulson@3193
    59
qed "wf_measure";
paulson@3193
    60
AddIffs [wf_measure];
paulson@3193
    61
nipkow@4643
    62
val measure_induct = standard
nipkow@4643
    63
    (asm_full_simplify (simpset() addsimps [measure_def,inv_image_def])
nipkow@4643
    64
      (wf_measure RS wf_induct));
nipkow@4643
    65
store_thm("measure_induct",measure_induct);
nipkow@4643
    66
paulson@3193
    67
(*----------------------------------------------------------------------------
paulson@3193
    68
 * Wellfoundedness of lexicographic combinations
paulson@3193
    69
 *---------------------------------------------------------------------------*)
paulson@3193
    70
paulson@3193
    71
val [wfa,wfb] = goalw thy [wf_def,lex_prod_def]
paulson@3193
    72
 "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
nipkow@3413
    73
by (EVERY1 [rtac allI,rtac impI]);
nipkow@3413
    74
by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1);
paulson@3193
    75
by (rtac (wfa RS spec RS mp) 1);
paulson@3193
    76
by (EVERY1 [rtac allI,rtac impI]);
paulson@3193
    77
by (rtac (wfb RS spec RS mp) 1);
paulson@3193
    78
by (Blast_tac 1);
paulson@3193
    79
qed "wf_lex_prod";
paulson@3193
    80
AddSIs [wf_lex_prod];
paulson@3193
    81
paulson@3193
    82
(*---------------------------------------------------------------------------
paulson@3193
    83
 * Transitivity of WF combinators.
paulson@3193
    84
 *---------------------------------------------------------------------------*)
wenzelm@5069
    85
Goalw [trans_def, lex_prod_def]
paulson@3193
    86
    "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 ** R2)";
paulson@3193
    87
by (Simp_tac 1);
paulson@3193
    88
by (Blast_tac 1);
paulson@3193
    89
qed "trans_lex_prod";
paulson@3193
    90
AddSIs [trans_lex_prod];
paulson@3193
    91
paulson@3193
    92
paulson@3193
    93
(*---------------------------------------------------------------------------
paulson@3193
    94
 * Wellfoundedness of proper subset on finite sets.
paulson@3193
    95
 *---------------------------------------------------------------------------*)
wenzelm@5069
    96
Goalw [finite_psubset_def] "wf(finite_psubset)";
paulson@3193
    97
by (rtac (wf_measure RS wf_subset) 1);
wenzelm@4089
    98
by (simp_tac (simpset() addsimps [measure_def, inv_image_def, less_than_def,
paulson@3237
    99
				 symmetric less_def])1);
wenzelm@4089
   100
by (fast_tac (claset() addSIs [psubset_card]) 1);
paulson@3193
   101
qed "wf_finite_psubset";
paulson@3193
   102
wenzelm@5069
   103
Goalw [finite_psubset_def, trans_def] "trans finite_psubset";
wenzelm@4089
   104
by (simp_tac (simpset() addsimps [psubset_def]) 1);
paulson@3237
   105
by (Blast_tac 1);
paulson@3237
   106
qed "trans_finite_psubset";
paulson@3193
   107
nipkow@3413
   108
(*---------------------------------------------------------------------------
nipkow@3413
   109
 * Wellfoundedness of finite acyclic relations
nipkow@5144
   110
 * Cannot go into WF because it needs Finite.
nipkow@3413
   111
 *---------------------------------------------------------------------------*)
nipkow@3413
   112
paulson@5143
   113
Goal "finite r ==> acyclic r --> wf r";
paulson@3457
   114
by (etac finite_induct 1);
paulson@3457
   115
 by (Blast_tac 1);
paulson@3457
   116
by (split_all_tac 1);
paulson@3457
   117
by (Asm_full_simp_tac 1);
nipkow@3413
   118
qed_spec_mp "finite_acyclic_wf";
nipkow@3413
   119
oheimb@4749
   120
qed_goal "finite_acyclic_wf_converse" thy 
oheimb@4751
   121
 "!!X. [|finite r; acyclic r|] ==> wf (r^-1)" (K [
oheimb@4749
   122
	etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1,
oheimb@4749
   123
	etac (acyclic_converse RS iffD2) 1]);
oheimb@4749
   124
paulson@5143
   125
Goal "finite r ==> wf r = acyclic r";
wenzelm@4089
   126
by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1);
nipkow@3413
   127
qed "wf_iff_acyclic_if_finite";
nipkow@3413
   128
nipkow@3413
   129
nipkow@3413
   130
(*---------------------------------------------------------------------------
nipkow@3413
   131
 * A relation is wellfounded iff it has no infinite descending chain
nipkow@5144
   132
 * Cannot go into WF because it needs type nat.
nipkow@3413
   133
 *---------------------------------------------------------------------------*)
nipkow@3413
   134
wenzelm@5069
   135
Goalw [wf_eq_minimal RS eq_reflection]
nipkow@3413
   136
  "wf r = (~(? f. !i. (f(Suc i),f i) : r))";
paulson@3457
   137
by (rtac iffI 1);
paulson@3457
   138
 by (rtac notI 1);
paulson@3457
   139
 by (etac exE 1);
paulson@3457
   140
 by (eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1);
paulson@3457
   141
 by (Blast_tac 1);
paulson@3457
   142
by (etac swap 1);
paulson@3446
   143
by (Asm_full_simp_tac 1);
paulson@3718
   144
by (Clarify_tac 1);
paulson@3457
   145
by (subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
nipkow@3436
   146
 by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
paulson@3457
   147
 by (rtac allI 1);
paulson@3457
   148
 by (Simp_tac 1);
paulson@3457
   149
 by (rtac selectI2EX 1);
paulson@3457
   150
  by (Blast_tac 1);
paulson@3457
   151
 by (Blast_tac 1);
paulson@3457
   152
by (rtac allI 1);
paulson@3457
   153
by (induct_tac "n" 1);
paulson@3457
   154
 by (Asm_simp_tac 1);
paulson@3457
   155
by (Simp_tac 1);
paulson@3457
   156
by (rtac selectI2EX 1);
paulson@3457
   157
 by (Blast_tac 1);
paulson@3457
   158
by (Blast_tac 1);
nipkow@3413
   159
qed "wf_iff_no_infinite_down_chain";