equal
deleted
inserted
replaced
30 lemmas wfPUNIVI = wfUNIVI [to_pred] |
30 lemmas wfPUNIVI = wfUNIVI [to_pred] |
31 |
31 |
32 text\<open>Restriction to domain @{term A} and range @{term B}. If @{term r} is |
32 text\<open>Restriction to domain @{term A} and range @{term B}. If @{term r} is |
33 well-founded over their intersection, then @{term "wf r"}\<close> |
33 well-founded over their intersection, then @{term "wf r"}\<close> |
34 lemma wfI: |
34 lemma wfI: |
35 "[| r \<subseteq> A <*> B; |
35 "[| r \<subseteq> A \<times> B; |
36 !!x P. [|\<forall>x. (\<forall>y. (y,x) : r --> P y) --> P x; x : A; x : B |] ==> P x |] |
36 !!x P. [|\<forall>x. (\<forall>y. (y,x) : r --> P y) --> P x; x : A; x : B |] ==> P x |] |
37 ==> wf r" |
37 ==> wf r" |
38 unfolding wf_def by blast |
38 unfolding wf_def by blast |
39 |
39 |
40 lemma wf_induct: |
40 lemma wf_induct: |