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