equal
deleted
inserted
replaced
82 subsubsection {*Well-founded relations*} |
82 subsubsection {*Well-founded relations*} |
83 |
83 |
84 lemma (in M_basic) wellfounded_on_iff_wellfounded: |
84 lemma (in M_basic) wellfounded_on_iff_wellfounded: |
85 "wellfounded_on(M,A,r) <-> wellfounded(M, r \<inter> A*A)" |
85 "wellfounded_on(M,A,r) <-> wellfounded(M, r \<inter> A*A)" |
86 apply (simp add: wellfounded_on_def wellfounded_def, safe) |
86 apply (simp add: wellfounded_on_def wellfounded_def, safe) |
87 apply blast |
87 apply force |
88 apply (drule_tac x=x in rspec, assumption, blast) |
88 apply (drule_tac x=x in rspec, assumption, blast) |
89 done |
89 done |
90 |
90 |
91 lemma (in M_basic) wellfounded_on_imp_wellfounded: |
91 lemma (in M_basic) wellfounded_on_imp_wellfounded: |
92 "[|wellfounded_on(M,A,r); r \<subseteq> A*A|] ==> wellfounded(M,r)" |
92 "[|wellfounded_on(M,A,r); r \<subseteq> A*A|] ==> wellfounded(M,r)" |