author | paulson |
Fri, 31 Jul 1998 10:48:42 +0200 | |
changeset 5223 | 4cb05273f764 |
parent 5168 | adafef6eb295 |
child 5580 | 354f4914811f |
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 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
12 |
(*The intended introduction rule*) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
13 |
val prems = goal Acc.thy |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
14 |
"[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)"; |
4089 | 15 |
by (fast_tac (claset() addIs (prems @ |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
16 |
map (rewrite_rule [pred_def]) acc.intrs)) 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
17 |
qed "accI"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
18 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
19 |
Goal "[| b: acc(r); (a,b): r |] ==> a: acc(r)"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
20 |
by (etac acc.elim 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
21 |
by (rewtac pred_def); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
22 |
by (Fast_tac 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
23 |
qed "acc_downward"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
24 |
|
5163 | 25 |
Goal "(b,a) : r^* ==> a : acc r --> b : acc r"; |
5168 | 26 |
by (etac rtrancl_induct 1); |
27 |
by (Blast_tac 1); |
|
28 |
by (blast_tac (claset() addDs [acc_downward]) 1); |
|
5163 | 29 |
val lemma = result(); |
30 |
Goal "[| a : acc r; (b,a) : r^* |] ==> b : acc r"; |
|
5168 | 31 |
by (blast_tac (claset() addDs [lemma]) 1); |
5163 | 32 |
qed "acc_downwards"; |
33 |
||
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
34 |
val [major,indhyp] = goal Acc.thy |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
35 |
"[| a : acc(r); \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
36 |
\ !!x. [| x: acc(r); ALL y. (y,x):r --> P(y) |] ==> P(x) \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
37 |
\ |] ==> P(a)"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
38 |
by (rtac (major RS acc.induct) 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
39 |
by (rtac indhyp 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
40 |
by (resolve_tac acc.intrs 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
41 |
by (rewtac pred_def); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
42 |
by (Fast_tac 2); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
43 |
by (etac (Int_lower1 RS Pow_mono RS subsetD) 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
44 |
qed "acc_induct"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
45 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
46 |
|
5223
4cb05273f764
Removal of obsolete "open" commands from heads of .ML files
paulson
parents:
5168
diff
changeset
|
47 |
Goal "r <= (acc r) Times (acc r) ==> wf(r)"; |
4cb05273f764
Removal of obsolete "open" commands from heads of .ML files
paulson
parents:
5168
diff
changeset
|
48 |
by (etac wfI 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
49 |
by (etac acc.induct 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
50 |
by (rewtac pred_def); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
51 |
by (Fast_tac 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
52 |
qed "acc_wfI"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
53 |
|
5223
4cb05273f764
Removal of obsolete "open" commands from heads of .ML files
paulson
parents:
5168
diff
changeset
|
54 |
Goal "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)"; |
4cb05273f764
Removal of obsolete "open" commands from heads of .ML files
paulson
parents:
5168
diff
changeset
|
55 |
by (etac wf_induct 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
56 |
by (rtac (impI RS allI) 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
57 |
by (rtac accI 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
58 |
by (Fast_tac 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
59 |
qed "acc_wfD_lemma"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
60 |
|
5223
4cb05273f764
Removal of obsolete "open" commands from heads of .ML files
paulson
parents:
5168
diff
changeset
|
61 |
Goal "wf(r) ==> r <= (acc r) Times (acc r)"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
62 |
by (rtac subsetI 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
63 |
by (res_inst_tac [("p", "x")] PairE 1); |
4089 | 64 |
by (fast_tac (claset() addSIs [SigmaI, |
5223
4cb05273f764
Removal of obsolete "open" commands from heads of .ML files
paulson
parents:
5168
diff
changeset
|
65 |
acc_wfD_lemma RS spec RS mp]) 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
66 |
qed "acc_wfD"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
67 |
|
5069 | 68 |
Goal "wf(r) = (r <= (acc r) Times (acc r))"; |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
69 |
by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
70 |
qed "wf_acc_iff"; |