- Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
authorberghofe
Wed May 07 10:56:52 2008 +0200 (2008-05-07)
changeset 268030af0f674845d
parent 26802 9eede540a5e8
child 26804 e2b1e6868c2f
- Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
to_set and to_pred attributes, because it is no longer applied automatically
- Manually applied predicate1I in proof of accp_subset, because it is no longer
part of the claset
- Replaced psubset_def by less_le
src/HOL/Wellfounded.thy
     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