equal
deleted
inserted
replaced
4 Copyright 1992 University of Cambridge/1995 TU Munich |
4 Copyright 1992 University of Cambridge/1995 TU Munich |
5 |
5 |
6 Wellfoundedness, induction, and recursion |
6 Wellfoundedness, induction, and recursion |
7 *) |
7 *) |
8 |
8 |
9 open WF; |
|
10 |
|
11 val H_cong = read_instantiate [("f","H")] (standard(refl RS cong RS cong)); |
9 val H_cong = read_instantiate [("f","H")] (standard(refl RS cong RS cong)); |
12 val H_cong1 = refl RS H_cong; |
10 val H_cong1 = refl RS H_cong; |
|
11 |
|
12 val [prem] = Goalw [wf_def] |
|
13 "[| !!P x. [| !x. (!y. (y,x) : r --> P(y)) --> P(x) |] ==> P(x) |] ==> wf(r)"; |
|
14 by (Clarify_tac 1); |
|
15 by (rtac prem 1); |
|
16 by (assume_tac 1); |
|
17 qed "wfUNIVI"; |
13 |
18 |
14 (*Restriction to domain A. If r is well-founded over A then wf(r)*) |
19 (*Restriction to domain A. If r is well-founded over A then wf(r)*) |
15 val [prem1,prem2] = Goalw [wf_def] |
20 val [prem1,prem2] = Goalw [wf_def] |
16 "[| r <= A Times A; \ |
21 "[| r <= A Times A; \ |
17 \ !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x); x:A |] ==> P(x) |] \ |
22 \ !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x); x:A |] ==> P(x) |] \ |