src/HOL/Induct/Acc.ML
author paulson
Wed, 07 May 1997 12:50:26 +0200
changeset 3120 c58423c20740
child 4089 96fba19bcbe2
permissions -rw-r--r--
New directory to contain examples of (co)inductive definitions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
open Acc;
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    13
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    14
(*The intended introduction rule*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    15
val prems = goal Acc.thy
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    16
    "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    17
by (fast_tac (!claset addIs (prems @ 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    18
                            map (rewrite_rule [pred_def]) acc.intrs)) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    19
qed "accI";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    20
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    21
goal Acc.thy "!!a b r. [| b: acc(r);  (a,b): r |] ==> a: acc(r)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    22
by (etac acc.elim 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    23
by (rewtac pred_def);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    24
by (Fast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    25
qed "acc_downward";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    26
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    27
val [major,indhyp] = goal Acc.thy
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    28
    "[| a : acc(r);                                             \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    29
\       !!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
    30
\    |] ==> P(a)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    31
by (rtac (major RS acc.induct) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    32
by (rtac indhyp 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    33
by (resolve_tac acc.intrs 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    34
by (rewtac pred_def);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    35
by (Fast_tac 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    36
by (etac (Int_lower1 RS Pow_mono RS subsetD) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    37
qed "acc_induct";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    38
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    39
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    40
val [major] = goal Acc.thy "r <= (acc r) Times (acc r) ==> wf(r)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    41
by (rtac (major RS wfI) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    42
by (etac acc.induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    43
by (rewtac pred_def);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    44
by (Fast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    45
qed "acc_wfI";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    46
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    47
val [major] = goal Acc.thy "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    48
by (rtac (major RS wf_induct) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    49
by (rtac (impI RS allI) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    50
by (rtac accI 1);
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_wfD_lemma";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    53
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    54
val [major] = goal Acc.thy "wf(r) ==> r <= (acc r) Times (acc r)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    55
by (rtac subsetI 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    56
by (res_inst_tac [("p", "x")] PairE 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    57
by (fast_tac (!claset addSIs [SigmaI,
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    58
                             major RS acc_wfD_lemma RS spec RS mp]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    59
qed "acc_wfD";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    60
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    61
goal Acc.thy "wf(r)  =  (r <= (acc r) Times (acc r))";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    62
by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    63
qed "wf_acc_iff";