1.1 --- a/src/HOL/WF_Rel.ML	Tue May 20 11:39:32 1997 +0200
     1.2 +++ b/src/HOL/WF_Rel.ML	Tue May 20 11:40:28 1997 +0200
     1.3 @@ -10,6 +10,25 @@
     1.4  
     1.5  
     1.6  (*----------------------------------------------------------------------------
     1.7 + * "Less than" on the natural numbers
     1.8 + *---------------------------------------------------------------------------*)
     1.9 +
    1.10 +goalw thy [less_than_def] "wf less_than"; 
    1.11 +by (rtac (wf_pred_nat RS wf_trancl) 1);
    1.12 +qed "wf_less_than";
    1.13 +AddIffs [wf_less_than];
    1.14 +
    1.15 +goalw thy [less_than_def] "trans less_than"; 
    1.16 +by (rtac trans_trancl 1);
    1.17 +qed "trans_less_than";
    1.18 +AddIffs [trans_less_than];
    1.19 +
    1.20 +goalw thy [less_than_def, less_def] "((x,y): less_than) = (x<y)"; 
    1.21 +by (Simp_tac 1);
    1.22 +qed "less_than_iff";
    1.23 +AddIffs [less_than_iff];
    1.24 +
    1.25 +(*----------------------------------------------------------------------------
    1.26   * The inverse image into a wellfounded relation is wellfounded.
    1.27   *---------------------------------------------------------------------------*)
    1.28  
    1.29 @@ -24,14 +43,19 @@
    1.30  qed "wf_inv_image";
    1.31  AddSIs [wf_inv_image];
    1.32  
    1.33 +goalw thy [trans_def,inv_image_def]
    1.34 +    "!!r. trans r ==> trans (inv_image r f)";
    1.35 +by (Simp_tac 1);
    1.36 +by (Blast_tac 1);
    1.37 +qed "trans_inv_image";
    1.38 +
    1.39 +
    1.40  (*----------------------------------------------------------------------------
    1.41   * All measures are wellfounded.
    1.42   *---------------------------------------------------------------------------*)
    1.43  
    1.44  goalw thy [measure_def] "wf (measure f)";
    1.45 -by (rtac wf_inv_image 1);
    1.46 -by (rtac wf_trancl 1);
    1.47 -by (rtac wf_pred_nat 1);
    1.48 +by (rtac (wf_less_than RS wf_inv_image) 1);
    1.49  qed "wf_measure";
    1.50  AddIffs [wf_measure];
    1.51  
    1.52 @@ -111,9 +135,13 @@
    1.53   *---------------------------------------------------------------------------*)
    1.54  goalw thy [finite_psubset_def] "wf(finite_psubset)";
    1.55  by (rtac (wf_measure RS wf_subset) 1);
    1.56 -by (simp_tac (!simpset addsimps[measure_def, inv_image_def,
    1.57 -				symmetric less_def])1);
    1.58 +by (simp_tac (!simpset addsimps [measure_def, inv_image_def, less_than_def,
    1.59 +				 symmetric less_def])1);
    1.60  by (fast_tac (!claset addIs [psubset_card]) 1);
    1.61  qed "wf_finite_psubset";
    1.62  
    1.63 +goalw thy [finite_psubset_def, trans_def] "trans finite_psubset";
    1.64 +by (simp_tac (!simpset addsimps [psubset_def]) 1);
    1.65 +by (Blast_tac 1);
    1.66 +qed "trans_finite_psubset";
    1.67  

     2.1 --- a/src/HOL/WF_Rel.thy	Tue May 20 11:39:32 1997 +0200
     2.2 +++ b/src/HOL/WF_Rel.thy	Tue May 20 11:40:28 1997 +0200
     2.3 @@ -8,16 +8,20 @@
     2.4  
     2.5  WF_Rel = Finite +
     2.6  consts
     2.7 - inv_image  :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
     2.8 - measure    :: "('a => nat) => ('a * 'a)set"
     2.9 -    "**"    :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
    2.10 -   rprod    :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
    2.11 -   finite_psubset  :: "('a set * 'a set) set"
    2.12 +  less_than :: "(nat*nat)set"
    2.13 +  inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
    2.14 +  measure   :: "('a => nat) => ('a * 'a)set"
    2.15 +  "**"      :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
    2.16 +  rprod     :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
    2.17 +  finite_psubset  :: "('a set * 'a set) set"
    2.18 +
    2.19  
    2.20  defs
    2.21 +  less_than_def "less_than == trancl pred_nat"
    2.22 +
    2.23    inv_image_def "inv_image r f == {(x,y). (f(x), f(y)) : r}"
    2.24  
    2.25 -  measure_def   "measure == inv_image (trancl pred_nat)"
    2.26 +  measure_def   "measure == inv_image less_than"
    2.27  
    2.28    lex_prod_def  "ra**rb == {p. ? a a' b b'. 
    2.29                                  p = ((a,b),(a',b')) &