src/HOL/WF_Rel.ML
author wenzelm
Thu Jun 22 23:04:34 2000 +0200 (2000-06-22)
changeset 9108 9fff97d29837
parent 9076 108ec332625d
child 9163 4d624e34e19a
permissions -rw-r--r--
bind_thm(s);
     1 (*  Title: 	HOL/WF_Rel
     2     ID:         $Id$
     3     Author: 	Konrad Slind
     4     Copyright   1996  TU Munich
     5 
     6 Derived WF relations: inverse image, lexicographic product, measure, ...
     7 *)
     8 
     9 
    10 (*----------------------------------------------------------------------------
    11  * "Less than" on the natural numbers
    12  *---------------------------------------------------------------------------*)
    13 
    14 Goalw [less_than_def] "wf less_than"; 
    15 by (rtac (wf_pred_nat RS wf_trancl) 1);
    16 qed "wf_less_than";
    17 AddIffs [wf_less_than];
    18 
    19 Goalw [less_than_def] "trans less_than"; 
    20 by (rtac trans_trancl 1);
    21 qed "trans_less_than";
    22 AddIffs [trans_less_than];
    23 
    24 Goalw [less_than_def, less_def] "((x,y): less_than) = (x<y)"; 
    25 by (Simp_tac 1);
    26 qed "less_than_iff";
    27 AddIffs [less_than_iff];
    28 
    29 Goal "(!!n. (!m. Suc m <= n --> P m) ==> P n) ==> P n";
    30 by (rtac (wf_less_than RS wf_induct) 1);
    31 by (resolve_tac (premises()) 1);
    32 by Auto_tac;
    33 qed_spec_mp "full_nat_induct";
    34 
    35 (*----------------------------------------------------------------------------
    36  * The inverse image into a wellfounded relation is wellfounded.
    37  *---------------------------------------------------------------------------*)
    38 
    39 Goal "wf(r) ==> wf(inv_image r (f::'a=>'b))"; 
    40 by (full_simp_tac (simpset() addsimps [inv_image_def, wf_eq_minimal]) 1);
    41 by (Clarify_tac 1);
    42 by (subgoal_tac "? (w::'b). w : {w. ? (x::'a). x: Q & (f x = w)}" 1);
    43 by (blast_tac (claset() delrules [allE]) 2);
    44 by (etac allE 1);
    45 by (mp_tac 1);
    46 by (Blast_tac 1);
    47 qed "wf_inv_image";
    48 AddSIs [wf_inv_image];
    49 
    50 Goalw [trans_def,inv_image_def]
    51     "!!r. trans r ==> trans (inv_image r f)";
    52 by (Simp_tac 1);
    53 by (Blast_tac 1);
    54 qed "trans_inv_image";
    55 
    56 
    57 (*----------------------------------------------------------------------------
    58  * All measures are wellfounded.
    59  *---------------------------------------------------------------------------*)
    60 
    61 Goalw [measure_def] "wf (measure f)";
    62 by (rtac (wf_less_than RS wf_inv_image) 1);
    63 qed "wf_measure";
    64 AddIffs [wf_measure];
    65 
    66 val measure_induct = standard
    67     (asm_full_simplify (simpset() addsimps [measure_def,inv_image_def])
    68       (wf_measure RS wf_induct));
    69 bind_thm ("measure_induct", measure_induct);
    70 
    71 (*----------------------------------------------------------------------------
    72  * Wellfoundedness of lexicographic combinations
    73  *---------------------------------------------------------------------------*)
    74 
    75 val [wfa,wfb] = goalw thy [wf_def,lex_prod_def]
    76  "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)";
    77 by (EVERY1 [rtac allI,rtac impI]);
    78 by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1);
    79 by (rtac (wfa RS spec RS mp) 1);
    80 by (EVERY1 [rtac allI,rtac impI]);
    81 by (rtac (wfb RS spec RS mp) 1);
    82 by (Blast_tac 1);
    83 qed "wf_lex_prod";
    84 AddSIs [wf_lex_prod];
    85 
    86 (*---------------------------------------------------------------------------
    87  * Transitivity of WF combinators.
    88  *---------------------------------------------------------------------------*)
    89 Goalw [trans_def, lex_prod_def]
    90     "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)";
    91 by (Simp_tac 1);
    92 by (Blast_tac 1);
    93 qed "trans_lex_prod";
    94 AddSIs [trans_lex_prod];
    95 
    96 
    97 (*---------------------------------------------------------------------------
    98  * Wellfoundedness of proper subset on finite sets.
    99  *---------------------------------------------------------------------------*)
   100 Goalw [finite_psubset_def] "wf(finite_psubset)";
   101 by (rtac (wf_measure RS wf_subset) 1);
   102 by (simp_tac (simpset() addsimps [measure_def, inv_image_def, less_than_def,
   103 				 symmetric less_def])1);
   104 by (fast_tac (claset() addSEs [psubset_card_mono]) 1);
   105 qed "wf_finite_psubset";
   106 
   107 Goalw [finite_psubset_def, trans_def] "trans finite_psubset";
   108 by (simp_tac (simpset() addsimps [psubset_def]) 1);
   109 by (Blast_tac 1);
   110 qed "trans_finite_psubset";
   111 
   112 (*---------------------------------------------------------------------------
   113  * Wellfoundedness of finite acyclic relations
   114  * Cannot go into WF because it needs Finite.
   115  *---------------------------------------------------------------------------*)
   116 
   117 Goal "finite r ==> acyclic r --> wf r";
   118 by (etac finite_induct 1);
   119  by (Blast_tac 1);
   120 by (split_all_tac 1);
   121 by (Asm_full_simp_tac 1);
   122 qed_spec_mp "finite_acyclic_wf";
   123 
   124 Goal "[|finite r; acyclic r|] ==> wf (r^-1)";
   125 by (etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1);
   126 by (etac (acyclic_converse RS iffD2) 1);
   127 qed "finite_acyclic_wf_converse";
   128 
   129 Goal "finite r ==> wf r = acyclic r";
   130 by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1);
   131 qed "wf_iff_acyclic_if_finite";
   132 
   133 
   134 (*---------------------------------------------------------------------------
   135  * A relation is wellfounded iff it has no infinite descending chain
   136  * Cannot go into WF because it needs type nat.
   137  *---------------------------------------------------------------------------*)
   138 
   139 Goalw [wf_eq_minimal RS eq_reflection]
   140   "wf r = (~(? f. !i. (f(Suc i),f i) : r))";
   141 by (rtac iffI 1);
   142  by (rtac notI 1);
   143  by (etac exE 1);
   144  by (eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1);
   145  by (Blast_tac 1);
   146 by (etac swap 1);
   147 by (Asm_full_simp_tac 1);
   148 by (Clarify_tac 1);
   149 by (subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
   150  by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
   151  by (rtac allI 1);
   152  by (Simp_tac 1);
   153  by (rtac selectI2EX 1);
   154   by (Blast_tac 1);
   155  by (Blast_tac 1);
   156 by (rtac allI 1);
   157 by (induct_tac "n" 1);
   158  by (Asm_simp_tac 1);
   159 by (Simp_tac 1);
   160 by (rtac selectI2EX 1);
   161  by (Blast_tac 1);
   162 by (Blast_tac 1);
   163 qed "wf_iff_no_infinite_down_chain";
   164 
   165 (*----------------------------------------------------------------------------
   166  * Weakly decreasing sequences (w.r.t. some well-founded order) stabilize.
   167  *---------------------------------------------------------------------------*)
   168 
   169 Goal "[| ! i. (f (Suc i), f i) : r^* |] ==> (f (i+k), f i) : r^*";
   170 by (induct_tac "k" 1);
   171  by (ALLGOALS Simp_tac);
   172 by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   173 val lemma = result();
   174 
   175 Goal "[| ! i. (f (Suc i), f i) : r^*; wf (r^+) |] \
   176 \     ==> ! m. f m = x --> (? i. ! k. f (m+i+k) = f (m+i))";
   177 by (etac wf_induct 1);
   178 by (Clarify_tac 1);
   179 by (case_tac "? j. (f (m+j), f m) : r^+" 1);
   180  by (Clarify_tac 1);
   181  by (subgoal_tac "? i. ! k. f ((m+j)+i+k) = f ((m+j)+i)" 1);
   182   by (Clarify_tac 1);
   183   by (res_inst_tac [("x","j+i")] exI 1);
   184   by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
   185  by (Blast_tac 1);
   186 by (res_inst_tac [("x","0")] exI 1);
   187 by (Clarsimp_tac 1);
   188 by (dres_inst_tac [("i","m"), ("k","k")] lemma 1);
   189 by (fast_tac (claset() addDs [rtranclE,rtrancl_into_trancl1]) 1);
   190 val lemma = result();
   191 
   192 Goal "[| ! i. (f (Suc i), f i) : r^*; wf (r^+) |] \
   193 \     ==> ? i. ! k. f (i+k) = f i";
   194 by (dres_inst_tac [("x","0")] (lemma RS spec) 1);
   195 by Auto_tac;
   196 qed "wf_weak_decr_stable";
   197 
   198 (* special case: <= *)
   199 
   200 Goal "(m, n) : pred_nat^* = (m <= n)";
   201 by (simp_tac (simpset() addsimps [less_eq, reflcl_trancl RS sym] 
   202                         delsimps [reflcl_trancl]) 1);
   203 by (arith_tac 1);
   204 qed "le_eq";
   205 
   206 Goal "[| ! i. f (Suc i) <= ((f i)::nat) |] ==> ? i. ! k. f (i+k) = f i";
   207 by (res_inst_tac [("r","pred_nat")] wf_weak_decr_stable 1);
   208 by (asm_simp_tac (simpset() addsimps [le_eq]) 1);
   209 by (REPEAT (resolve_tac [wf_trancl,wf_pred_nat] 1));
   210 qed "weak_decr_stable";