author | wenzelm |
Thu, 16 Mar 2000 00:35:27 +0100 | |
changeset 8490 | 6e0f23304061 |
parent 7721 | cb353d802ade |
child 9802 | adda1dc18bb8 |
permissions | -rw-r--r-- |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/ex/Acc |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
4 |
Copyright 1994 University of Cambridge |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
5 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
6 |
Inductive definition of acc(r) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
7 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
8 |
See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
9 |
Research Report 92-49, LIP, ENS Lyon. Dec 1992. |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
10 |
*) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
11 |
|
7721 | 12 |
val accI = thm "acc.accI"; |
13 |
||
14 |
val [major,indhyp] = Goal |
|
15 |
"[| a : acc(r); \ |
|
16 |
\ !!x. [| x: acc(r); ALL y. (y,x):r --> P(y) |] ==> P(x) \ |
|
17 |
\ |] ==> P(a)"; |
|
18 |
by (rtac (major RS thm "acc.induct") 1); |
|
19 |
by (rtac indhyp 1); |
|
20 |
by (rtac accI 1); |
|
21 |
by (ALLGOALS Fast_tac); |
|
22 |
qed "acc_induct"; |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
23 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
24 |
Goal "[| b: acc(r); (a,b): r |] ==> a: acc(r)"; |
7721 | 25 |
by (etac (thm "acc.elims") 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
26 |
by (Fast_tac 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
27 |
qed "acc_downward"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
28 |
|
5163 | 29 |
Goal "(b,a) : r^* ==> a : acc r --> b : acc r"; |
5168 | 30 |
by (etac rtrancl_induct 1); |
31 |
by (Blast_tac 1); |
|
32 |
by (blast_tac (claset() addDs [acc_downward]) 1); |
|
7681 | 33 |
no_qed(); |
5163 | 34 |
val lemma = result(); |
7453 | 35 |
|
5163 | 36 |
Goal "[| a : acc r; (b,a) : r^* |] ==> b : acc r"; |
5168 | 37 |
by (blast_tac (claset() addDs [lemma]) 1); |
5163 | 38 |
qed "acc_downwards"; |
39 |
||
5580 | 40 |
Goal "!x. x : acc(r) ==> wf(r)"; |
41 |
by (rtac wfUNIVI 1); |
|
6301 | 42 |
by (deepen_tac (claset() addEs [acc_induct]) 1 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
43 |
qed "acc_wfI"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
44 |
|
5580 | 45 |
Goal "wf(r) ==> x : acc(r)"; |
5223
4cb05273f764
Removal of obsolete "open" commands from heads of .ML files
paulson
parents:
5168
diff
changeset
|
46 |
by (etac wf_induct 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
47 |
by (rtac accI 1); |
5580 | 48 |
by (Blast_tac 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
49 |
qed "acc_wfD"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
50 |
|
5580 | 51 |
Goal "wf(r) = (!x. x : acc(r))"; |
52 |
by (blast_tac (claset() addIs [acc_wfI] addDs [acc_wfD]) 1); |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
53 |
qed "wf_acc_iff"; |