|
1 (* Title: HOL/ex/Acc |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
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 |
|
16 "[| !!b. <b,a>:r ==> b: acc(r) |] ==> a: acc(r)"; |
|
17 by (fast_tac (set_cs addIs (prems @ |
|
18 map (rewrite_rule [pred_def]) acc.intrs)) 1); |
|
19 val accI = result(); |
|
20 |
|
21 goal Acc.thy "!!a b r. [| b: acc(r); <a,b>: r |] ==> a: acc(r)"; |
|
22 by (etac acc.elim 1); |
|
23 by (rewtac pred_def); |
|
24 by (fast_tac set_cs 1); |
|
25 val acc_downward = result(); |
|
26 |
|
27 val [major,indhyp] = goal Acc.thy |
|
28 "[| a : acc(r); \ |
|
29 \ !!x. [| x: acc(r); ALL y. <y,x>:r --> P(y) |] ==> P(x) \ |
|
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); |
|
36 be (Int_lower1 RS Pow_mono RS subsetD) 1; |
|
37 val acc_induct = result(); |
|
38 |
|
39 |
|
40 val [major] = goal Acc.thy "r <= Sigma(acc(r), %u. acc(r)) ==> wf(r)"; |
|
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 val acc_wfI = result(); |
|
46 |
|
47 val [major] = goal Acc.thy "wf(r) ==> ALL x. <x,y>: r | <y,x>:r --> y: acc(r)"; |
|
48 by (rtac (major RS wf_induct) 1); |
|
49 br (impI RS allI) 1; |
|
50 br accI 1; |
|
51 by (fast_tac set_cs 1); |
|
52 val acc_wfD_lemma = result(); |
|
53 |
|
54 val [major] = goal Acc.thy "wf(r) ==> r <= Sigma(acc(r), %u. acc(r))"; |
|
55 by (rtac subsetI 1); |
|
56 by (res_inst_tac [("p", "x")] PairE 1); |
|
57 by (fast_tac (set_cs addSIs [SigmaI, |
|
58 major RS acc_wfD_lemma RS spec RS mp]) 1); |
|
59 val acc_wfD = result(); |
|
60 |
|
61 goal Acc.thy "wf(r) = (r <= Sigma(acc(r), %u. acc(r)))"; |
|
62 by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]); |
|
63 val wf_acc_iff = result(); |