author | paulson |
Thu, 04 Apr 1996 11:45:01 +0200 | |
changeset 1642 | 21db0cf9a1a4 |
parent 1465 | 5d7a7e439cec |
child 1820 | e381e1c51689 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/ex/Acc |
969 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
969 | 4 |
Copyright 1994 University of Cambridge |
5 |
||
6 |
Inductive definition of acc(r) |
|
7 |
||
8 |
See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. |
|
9 |
Research Report 92-49, LIP, ENS Lyon. Dec 1992. |
|
10 |
*) |
|
11 |
||
12 |
open Acc; |
|
13 |
||
14 |
(*The intended introduction rule*) |
|
15 |
val prems = goal Acc.thy |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset
|
16 |
"[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)"; |
969 | 17 |
by (fast_tac (set_cs addIs (prems @ |
1465 | 18 |
map (rewrite_rule [pred_def]) acc.intrs)) 1); |
969 | 19 |
qed "accI"; |
20 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset
|
21 |
goal Acc.thy "!!a b r. [| b: acc(r); (a,b): r |] ==> a: acc(r)"; |
969 | 22 |
by (etac acc.elim 1); |
23 |
by (rewtac pred_def); |
|
24 |
by (fast_tac set_cs 1); |
|
25 |
qed "acc_downward"; |
|
26 |
||
27 |
val [major,indhyp] = goal Acc.thy |
|
1465 | 28 |
"[| a : acc(r); \ |
29 |
\ !!x. [| x: acc(r); ALL y. (y,x):r --> P(y) |] ==> P(x) \ |
|
969 | 30 |
\ |] ==> P(a)"; |
31 |
by (rtac (major RS acc.induct) 1); |
|
32 |
by (rtac indhyp 1); |
|
33 |
by (resolve_tac acc.intrs 1); |
|
34 |
by (rewtac pred_def); |
|
35 |
by (fast_tac set_cs 2); |
|
1046 | 36 |
by (etac (Int_lower1 RS Pow_mono RS subsetD) 1); |
969 | 37 |
qed "acc_induct"; |
38 |
||
39 |
||
1642 | 40 |
val [major] = goal Acc.thy "r <= (acc r) Times (acc r) ==> wf(r)"; |
969 | 41 |
by (rtac (major RS wfI) 1); |
42 |
by (etac acc.induct 1); |
|
43 |
by (rewtac pred_def); |
|
44 |
by (fast_tac set_cs 1); |
|
45 |
qed "acc_wfI"; |
|
46 |
||
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
969
diff
changeset
|
47 |
val [major] = goal Acc.thy "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)"; |
969 | 48 |
by (rtac (major RS wf_induct) 1); |
1046 | 49 |
by (rtac (impI RS allI) 1); |
50 |
by (rtac accI 1); |
|
969 | 51 |
by (fast_tac set_cs 1); |
52 |
qed "acc_wfD_lemma"; |
|
53 |
||
1642 | 54 |
val [major] = goal Acc.thy "wf(r) ==> r <= (acc r) Times (acc r)"; |
969 | 55 |
by (rtac subsetI 1); |
56 |
by (res_inst_tac [("p", "x")] PairE 1); |
|
57 |
by (fast_tac (set_cs addSIs [SigmaI, |
|
1465 | 58 |
major RS acc_wfD_lemma RS spec RS mp]) 1); |
969 | 59 |
qed "acc_wfD"; |
60 |
||
1642 | 61 |
goal Acc.thy "wf(r) = (r <= (acc r) Times (acc r))"; |
969 | 62 |
by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]); |
63 |
qed "wf_acc_iff"; |