equal
deleted
inserted
replaced
53 lemma wf_induct: |
53 lemma wf_induct: |
54 "[| wf(r); |
54 "[| wf(r); |
55 !!x.[| ALL y. (y,x): r --> P(y) |] ==> P(x) |
55 !!x.[| ALL y. (y,x): r --> P(y) |] ==> P(x) |
56 |] ==> P(a)" |
56 |] ==> P(a)" |
57 by (unfold wf_def, blast) |
57 by (unfold wf_def, blast) |
|
58 |
|
59 lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf] |
58 |
60 |
59 lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. (a,x):r --> (x,a)~:r" |
61 lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. (a,x):r --> (x,a)~:r" |
60 by (erule_tac a=a in wf_induct, blast) |
62 by (erule_tac a=a in wf_induct, blast) |
61 |
63 |
62 (* [| wf r; ~Z ==> (a,x) : r; (x,a) ~: r ==> Z |] ==> Z *) |
64 (* [| wf r; ~Z ==> (a,x) : r; (x,a) ~: r ==> Z |] ==> Z *) |