equal
deleted
inserted
replaced
11 val H_cong = read_instantiate [("f","H")] (standard(refl RS cong RS cong)); |
11 val H_cong = read_instantiate [("f","H")] (standard(refl RS cong RS cong)); |
12 val H_cong1 = refl RS H_cong; |
12 val H_cong1 = refl RS H_cong; |
13 |
13 |
14 (*Restriction to domain A. If r is well-founded over A then wf(r)*) |
14 (*Restriction to domain A. If r is well-founded over A then wf(r)*) |
15 val [prem1,prem2] = goalw WF.thy [wf_def] |
15 val [prem1,prem2] = goalw WF.thy [wf_def] |
16 "[| r <= Sigma A (%u.A); \ |
16 "[| r <= A Times A; \ |
17 \ !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x); x:A |] ==> P(x) |] \ |
17 \ !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x); x:A |] ==> P(x) |] \ |
18 \ ==> wf(r)"; |
18 \ ==> wf(r)"; |
19 by (strip_tac 1); |
19 by (strip_tac 1); |
20 by (rtac allE 1); |
20 by (rtac allE 1); |
21 by (assume_tac 1); |
21 by (assume_tac 1); |