author | paulson |
Thu, 10 Oct 1996 11:09:03 +0200 | |
changeset 2085 | bcc9cbed10b1 |
parent 2031 | 03a843f0f447 |
child 2637 | e9b203f854ae |
permissions | -rw-r--r-- |
1475 | 1 |
(* Title: HOL/wf.ML |
923 | 2 |
ID: $Id$ |
1475 | 3 |
Author: Tobias Nipkow, with minor changes by Konrad Slind |
4 |
Copyright 1992 University of Cambridge/1995 TU Munich |
|
923 | 5 |
|
1475 | 6 |
For WF.thy. Wellfoundedness, induction, and recursion |
923 | 7 |
*) |
8 |
||
9 |
open WF; |
|
10 |
||
950 | 11 |
val H_cong = read_instantiate [("f","H")] (standard(refl RS cong RS cong)); |
923 | 12 |
val H_cong1 = refl RS H_cong; |
13 |
||
14 |
(*Restriction to domain A. If r is well-founded over A then wf(r)*) |
|
15 |
val [prem1,prem2] = goalw WF.thy [wf_def] |
|
1642 | 16 |
"[| r <= A Times A; \ |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
17 |
\ !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x); x:A |] ==> P(x) |] \ |
923 | 18 |
\ ==> wf(r)"; |
19 |
by (strip_tac 1); |
|
20 |
by (rtac allE 1); |
|
21 |
by (assume_tac 1); |
|
1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1771
diff
changeset
|
22 |
by (best_tac (!claset addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1); |
923 | 23 |
qed "wfI"; |
24 |
||
25 |
val major::prems = goalw WF.thy [wf_def] |
|
26 |
"[| wf(r); \ |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
27 |
\ !!x.[| ! y. (y,x): r --> P(y) |] ==> P(x) \ |
923 | 28 |
\ |] ==> P(a)"; |
29 |
by (rtac (major RS spec RS mp RS spec) 1); |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1642
diff
changeset
|
30 |
by (fast_tac (!claset addEs prems) 1); |
923 | 31 |
qed "wf_induct"; |
32 |
||
33 |
(*Perform induction on i, then prove the wf(r) subgoal using prems. *) |
|
34 |
fun wf_ind_tac a prems i = |
|
35 |
EVERY [res_inst_tac [("a",a)] wf_induct i, |
|
1465 | 36 |
rename_last_tac a ["1"] (i+1), |
37 |
ares_tac prems i]; |
|
923 | 38 |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
39 |
val prems = goal WF.thy "[| wf(r); (a,x):r; (x,a):r |] ==> P"; |
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
40 |
by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1); |
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1642
diff
changeset
|
41 |
by (fast_tac (!claset addIs prems) 1); |
923 | 42 |
by (wf_ind_tac "a" prems 1); |
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1642
diff
changeset
|
43 |
by (Fast_tac 1); |
923 | 44 |
qed "wf_asym"; |
45 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
46 |
val prems = goal WF.thy "[| wf(r); (a,a): r |] ==> P"; |
923 | 47 |
by (rtac wf_asym 1); |
48 |
by (REPEAT (resolve_tac prems 1)); |
|
1618 | 49 |
qed "wf_irrefl"; |
923 | 50 |
|
1475 | 51 |
(*transitive closure of a wf relation is wf! *) |
923 | 52 |
val [prem] = goal WF.thy "wf(r) ==> wf(r^+)"; |
53 |
by (rewtac wf_def); |
|
54 |
by (strip_tac 1); |
|
55 |
(*must retain the universal formula for later use!*) |
|
56 |
by (rtac allE 1 THEN assume_tac 1); |
|
57 |
by (etac mp 1); |
|
58 |
by (res_inst_tac [("a","x")] (prem RS wf_induct) 1); |
|
59 |
by (rtac (impI RS allI) 1); |
|
60 |
by (etac tranclE 1); |
|
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1642
diff
changeset
|
61 |
by (Fast_tac 1); |
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1642
diff
changeset
|
62 |
by (Fast_tac 1); |
923 | 63 |
qed "wf_trancl"; |
64 |
||
65 |
||
66 |
(** cut **) |
|
67 |
||
68 |
(*This rewrite rule works upon formulae; thus it requires explicit use of |
|
69 |
H_cong to expose the equality*) |
|
70 |
goalw WF.thy [cut_def] |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
71 |
"(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))"; |
1552 | 72 |
by (simp_tac (HOL_ss addsimps [expand_fun_eq] |
1475 | 73 |
setloop (split_tac [expand_if])) 1); |
74 |
qed "cuts_eq"; |
|
923 | 75 |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
950
diff
changeset
|
76 |
goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)"; |
1552 | 77 |
by (asm_simp_tac HOL_ss 1); |
923 | 78 |
qed "cut_apply"; |
79 |
||
80 |
(*** is_recfun ***) |
|
81 |
||
82 |
goalw WF.thy [is_recfun_def,cut_def] |
|
1475 |