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