src/HOL/Wellfounded.thy
changeset 26803 0af0f674845d
parent 26748 4d51ddd6aa5c
child 26976 cf147f69b3df
     1.1 --- a/src/HOL/Wellfounded.thy	Wed May 07 10:56:50 2008 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Wed May 07 10:56:52 2008 +0200
     1.3 @@ -271,7 +271,7 @@
     1.4  done
     1.5  
     1.6  lemmas wfP_SUP = wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}",
     1.7 -  to_pred SUP_UN_eq2 bot_empty_eq, simplified, standard]
     1.8 +  to_pred SUP_UN_eq2 bot_empty_eq pred_equals_eq, simplified, standard]
     1.9  
    1.10  lemma wf_Union: 
    1.11   "[| ALL r:R. wf r;  
    1.12 @@ -691,7 +691,7 @@
    1.13  lemma accp_subset:
    1.14    assumes sub: "R1 \<le> R2"
    1.15    shows "accp R2 \<le> accp R1"
    1.16 -proof
    1.17 +proof (rule predicate1I)
    1.18    fix x assume "accp R2 x"
    1.19    then show "accp R1 x"
    1.20    proof (induct x)
    1.21 @@ -745,9 +745,9 @@
    1.22  
    1.23  lemmas wf_acc_iff = wfP_accp_iff [to_set]
    1.24  
    1.25 -lemmas acc_subset = accp_subset [to_set]
    1.26 +lemmas acc_subset = accp_subset [to_set pred_subset_eq]
    1.27  
    1.28 -lemmas acc_subset_induct = accp_subset_induct [to_set]
    1.29 +lemmas acc_subset_induct = accp_subset_induct [to_set pred_subset_eq]
    1.30  
    1.31  
    1.32  subsection {* Tools for building wellfounded relations *}
    1.33 @@ -837,7 +837,7 @@
    1.34  done
    1.35  
    1.36  lemma trans_finite_psubset: "trans finite_psubset"
    1.37 -by (simp add: finite_psubset_def psubset_def trans_def, blast)
    1.38 +by (simp add: finite_psubset_def less_le trans_def, blast)
    1.39  
    1.40  
    1.41