equal
deleted
inserted
replaced
23 by (rewtac pred_def); |
23 by (rewtac pred_def); |
24 by (Fast_tac 1); |
24 by (Fast_tac 1); |
25 qed "acc_downward"; |
25 qed "acc_downward"; |
26 |
26 |
27 Goal "(b,a) : r^* ==> a : acc r --> b : acc r"; |
27 Goal "(b,a) : r^* ==> a : acc r --> b : acc r"; |
28 be rtrancl_induct 1; |
28 by (etac rtrancl_induct 1); |
29 by(Blast_tac 1); |
29 by (Blast_tac 1); |
30 by(blast_tac (claset() addDs [acc_downward]) 1); |
30 by (blast_tac (claset() addDs [acc_downward]) 1); |
31 val lemma = result(); |
31 val lemma = result(); |
32 Goal "[| a : acc r; (b,a) : r^* |] ==> b : acc r"; |
32 Goal "[| a : acc r; (b,a) : r^* |] ==> b : acc r"; |
33 by(blast_tac (claset() addDs [lemma]) 1); |
33 by (blast_tac (claset() addDs [lemma]) 1); |
34 qed "acc_downwards"; |
34 qed "acc_downwards"; |
35 |
35 |
36 val [major,indhyp] = goal Acc.thy |
36 val [major,indhyp] = goal Acc.thy |
37 "[| a : acc(r); \ |
37 "[| a : acc(r); \ |
38 \ !!x. [| x: acc(r); ALL y. (y,x):r --> P(y) |] ==> P(x) \ |
38 \ !!x. [| x: acc(r); ALL y. (y,x):r --> P(y) |] ==> P(x) \ |