src/HOL/WF_Rel.ML
author paulson
Thu Jan 08 18:10:34 1998 +0100 (1998-01-08)
changeset 4537 4e835bd9fada
parent 4089 96fba19bcbe2
child 4643 1b40fcac5a09
permissions -rw-r--r--
Expressed most Oops rules using Notes instead of Says, and other 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 thy [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 thy [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 thy [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 thy "!!r. 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 thy [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 thy [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 (*----------------------------------------------------------------------------
    63  * Wellfoundedness of lexicographic combinations
    64  *---------------------------------------------------------------------------*)
    65 
    66 val [wfa,wfb] = goalw thy [wf_def,lex_prod_def]
    67  "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
    68 by (EVERY1 [rtac allI,rtac impI]);
    69 by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1);
    70 by (rtac (wfa RS spec RS mp) 1);
    71 by (EVERY1 [rtac allI,rtac impI]);
    72 by (rtac (wfb RS spec RS mp) 1);
    73 by (Blast_tac 1);
    74 qed "wf_lex_prod";
    75 AddSIs [wf_lex_prod];
    76 
    77 (*---------------------------------------------------------------------------
    78  * Transitivity of WF combinators.
    79  *---------------------------------------------------------------------------*)
    80 goalw thy [trans_def, lex_prod_def]
    81     "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 ** R2)";
    82 by (Simp_tac 1);
    83 by (Blast_tac 1);
    84 qed "trans_lex_prod";
    85 AddSIs [trans_lex_prod];
    86 
    87 
    88 (*---------------------------------------------------------------------------
    89  * Wellfoundedness of proper subset on finite sets.
    90  *---------------------------------------------------------------------------*)
    91 goalw thy [finite_psubset_def] "wf(finite_psubset)";
    92 by (rtac (wf_measure RS wf_subset) 1);
    93 by (simp_tac (simpset() addsimps [measure_def, inv_image_def, less_than_def,
    94 				 symmetric less_def])1);
    95 by (fast_tac (claset() addSIs [psubset_card]) 1);
    96 qed "wf_finite_psubset";
    97 
    98 goalw thy [finite_psubset_def, trans_def] "trans finite_psubset";
    99 by (simp_tac (simpset() addsimps [psubset_def]) 1);
   100 by (Blast_tac 1);
   101 qed "trans_finite_psubset";
   102 
   103 (*---------------------------------------------------------------------------
   104  * Wellfoundedness of finite acyclic relations
   105  * Cannot go into WF because it needs Finite
   106  *---------------------------------------------------------------------------*)
   107 
   108 goal thy "!!r. finite r ==> acyclic r --> wf r";
   109 by (etac finite_induct 1);
   110  by (Blast_tac 1);
   111 by (split_all_tac 1);
   112 by (Asm_full_simp_tac 1);
   113 qed_spec_mp "finite_acyclic_wf";
   114 
   115 goal thy "!!r. finite r ==> wf r = acyclic r";
   116 by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1);
   117 qed "wf_iff_acyclic_if_finite";
   118 
   119 
   120 (*---------------------------------------------------------------------------
   121  * A relation is wellfounded iff it has no infinite descending chain
   122  *---------------------------------------------------------------------------*)
   123 
   124 goalw thy [wf_eq_minimal RS eq_reflection]
   125   "wf r = (~(? f. !i. (f(Suc i),f i) : r))";
   126 by (rtac iffI 1);
   127  by (rtac notI 1);
   128  by (etac exE 1);
   129  by (eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1);
   130  by (Blast_tac 1);
   131 by (etac swap 1);
   132 by (Asm_full_simp_tac 1);
   133 by (Clarify_tac 1);
   134 by (subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
   135  by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
   136  by (rtac allI 1);
   137  by (Simp_tac 1);
   138  by (rtac selectI2EX 1);
   139   by (Blast_tac 1);
   140  by (Blast_tac 1);
   141 by (rtac allI 1);
   142 by (induct_tac "n" 1);
   143  by (Asm_simp_tac 1);
   144 by (Simp_tac 1);
   145 by (rtac selectI2EX 1);
   146  by (Blast_tac 1);
   147 by (Blast_tac 1);
   148 qed "wf_iff_no_infinite_down_chain";