equal
deleted
inserted
replaced
69 |
69 |
70 lemmas wfP_induct = wf_induct [to_pred] |
70 lemmas wfP_induct = wf_induct [to_pred] |
71 |
71 |
72 lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf] |
72 lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf] |
73 |
73 |
74 lemmas wfP_induct_rule = |
74 lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP] |
75 wf_induct_rule [to_pred, consumes 1, case_names less, induct set: wfP] |
|
76 |
75 |
77 lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. (a,x):r --> (x,a)~:r" |
76 lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. (a,x):r --> (x,a)~:r" |
78 by (erule_tac a=a in wf_induct, blast) |
77 by (erule_tac a=a in wf_induct, blast) |
79 |
78 |
80 (* [| wf r; ~Z ==> (a,x) : r; (x,a) ~: r ==> Z |] ==> Z *) |
79 (* [| wf r; ~Z ==> (a,x) : r; (x,a) ~: r ==> Z |] ==> Z *) |