src/HOL/Induct/Acc.ML
author paulson
Wed Mar 03 11:15:18 1999 +0100 (1999-03-03)
changeset 6301 08245f5a436d
parent 5618 721671c68324
child 7453 18df56953792
permissions -rw-r--r--
expandshort
paulson@3120
     1
(*  Title:      HOL/ex/Acc
paulson@3120
     2
    ID:         $Id$
paulson@3120
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3120
     4
    Copyright   1994  University of Cambridge
paulson@3120
     5
paulson@3120
     6
Inductive definition of acc(r)
paulson@3120
     7
paulson@3120
     8
See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
paulson@3120
     9
Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
paulson@3120
    10
*)
paulson@3120
    11
paulson@3120
    12
(*The intended introduction rule*)
paulson@3120
    13
val prems = goal Acc.thy
paulson@3120
    14
    "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)";
paulson@5618
    15
by (fast_tac (claset() addIs prems @ 
paulson@5618
    16
                             map (rewrite_rule [pred_def]) acc.intrs) 1);
paulson@3120
    17
qed "accI";
paulson@3120
    18
paulson@5143
    19
Goal "[| b: acc(r);  (a,b): r |] ==> a: acc(r)";
paulson@3120
    20
by (etac acc.elim 1);
paulson@3120
    21
by (rewtac pred_def);
paulson@3120
    22
by (Fast_tac 1);
paulson@3120
    23
qed "acc_downward";
paulson@3120
    24
nipkow@5163
    25
Goal "(b,a) : r^* ==> a : acc r --> b : acc r";
wenzelm@5168
    26
by (etac rtrancl_induct 1);
wenzelm@5168
    27
by (Blast_tac 1);
wenzelm@5168
    28
 by (blast_tac (claset() addDs [acc_downward]) 1);
nipkow@5163
    29
val lemma = result();
nipkow@5163
    30
Goal "[| a : acc r; (b,a) : r^* |] ==> b : acc r";
wenzelm@5168
    31
by (blast_tac (claset() addDs [lemma]) 1);
nipkow@5163
    32
qed "acc_downwards";
nipkow@5163
    33
paulson@3120
    34
val [major,indhyp] = goal Acc.thy
paulson@3120
    35
    "[| a : acc(r);                                             \
paulson@3120
    36
\       !!x. [| x: acc(r);  ALL y. (y,x):r --> P(y) |] ==> P(x) \
paulson@3120
    37
\    |] ==> P(a)";
paulson@3120
    38
by (rtac (major RS acc.induct) 1);
paulson@3120
    39
by (rtac indhyp 1);
paulson@3120
    40
by (resolve_tac acc.intrs 1);
paulson@3120
    41
by (rewtac pred_def);
paulson@3120
    42
by (Fast_tac 2);
paulson@3120
    43
by (etac (Int_lower1 RS Pow_mono RS subsetD) 1);
paulson@3120
    44
qed "acc_induct";
paulson@3120
    45
nipkow@5580
    46
Goal "!x. x : acc(r) ==> wf(r)";
nipkow@5580
    47
by (rtac wfUNIVI 1);
paulson@6301
    48
by (deepen_tac (claset() addEs [acc_induct]) 1 1);
paulson@3120
    49
qed "acc_wfI";
paulson@3120
    50
nipkow@5580
    51
Goal "wf(r) ==> x : acc(r)";
paulson@5223
    52
by (etac wf_induct 1);
paulson@3120
    53
by (rtac accI 1);
nipkow@5580
    54
by (Blast_tac 1);
paulson@3120
    55
qed "acc_wfD";
paulson@3120
    56
nipkow@5580
    57
Goal "wf(r)  =  (!x. x : acc(r))";
nipkow@5580
    58
by (blast_tac (claset() addIs [acc_wfI] addDs [acc_wfD]) 1);
paulson@3120
    59
qed "wf_acc_iff";