src/CCL/genrec.ML
author lcp
Tue, 21 Sep 1993 11:16:19 +0200
changeset 10 e37080f41102
parent 0 a5a9c433f639
child 642 0db578095e6a
permissions -rw-r--r--
This commit should not have been necessary. For some reason, the previous commit did not update genrec.ML. There were still occurrences of SIMP_TAC. Was the commit perhaps interrupted??
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	92/CCL/genrec
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Martin Coen, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
(*** General Recursive Functions ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
val major::prems = goal Wfd.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
    "[| a : A;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
\       !!p g.[| p:A; ALL x:{x: A. <x,p>:wf(R)}. g(x) : D(x) |] ==>\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
\               h(p,g) : D(p) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
\    letrec g x be h(x,g) in g(a) : D(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
br (major RS rev_mp) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
br (wf_wf RS wfd_induct) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
br (letrecB RS ssubst) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
br impI 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
bes prems 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
br ballI 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
be (spec RS mp RS mp) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
by (REPEAT (eresolve_tac [SubtypeD1,SubtypeD2] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
val letrecT = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
goalw Wfd.thy [SPLIT_def] "SPLIT(<a,b>,B) = B(a,b)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
br set_ext 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
by (fast_tac ccl_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
val SPLITB = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
val prems = goalw Wfd.thy [letrec2_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
    "[| a : A;  b : B;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
\     !!p q g.[| p:A; q:B; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
\             ALL x:A.ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==>\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
\               h(p,q,g) : D(p,q) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
\    letrec g x y be h(x,y,g) in g(a,b) : D(a,b)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
br (SPLITB RS subst) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
br (SPLITB RS ssubst) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
br (SPLITB RS subst) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
            eresolve_tac [bspec,SubtypeE,sym RS subst] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
val letrec2T = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
goal Wfd.thy "SPLIT(<a,<b,c>>,%x xs.SPLIT(xs,%y z.B(x,y,z))) = B(a,b,c)";
10
e37080f41102 This commit should not have been necessary. For some reason, the previous
lcp
parents: 0
diff changeset
    46
by (simp_tac (ccl_ss addsimps [SPLITB]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
val lemma = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
val prems = goalw Wfd.thy [letrec3_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
    "[| a : A;  b : B;  c : C;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
\    !!p q r g.[| p:A; q:B; r:C; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
\      ALL x:A.ALL y:B.ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}. \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
\                                                       g(x,y,z) : D(x,y,z) |] ==>\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
\               h(p,q,r,g) : D(p,q,r) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
\    letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
br (lemma RS subst) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1));
10
e37080f41102 This commit should not have been necessary. For some reason, the previous
lcp
parents: 0
diff changeset
    58
by (simp_tac (ccl_ss addsimps [SPLITB]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
br (lemma RS subst) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
            eresolve_tac [bspec,SubtypeE,sym RS subst] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
val letrec3T = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
val letrecTs = [letrecT,letrec2T,letrec3T];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
(*** Type Checking for Recursive Calls ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
val major::prems = goal Wfd.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
    "[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
\       g(a) : D(a) ==> g(a) : E;  a:A;  <a,p>:wf(R) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
\   g(a) : E";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
by (REPEAT (ares_tac ([SubtypeI,major RS bspec,major]@prems) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
val rcallT = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
val major::prems = goal Wfd.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
    "[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
\       g(a,b) : D(a,b) ==> g(a,b) : E;  a:A;  b:B;  <<a,b>,<p,q>>:wf(R) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
\   g(a,b) : E";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec,major]@prems) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
val rcall2T = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
val major::prems = goal Wfd.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
    "[| ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z); \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
\       g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
\       a:A;  b:B;  c:C;  <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
\   g(a,b,c) : E";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec RS bspec,major]@prems) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
val rcall3T = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
val rcallTs = [rcallT,rcall2T,rcall3T];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
(*** Instantiating an induction hypothesis with an equality assumption ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
val prems = goal Wfd.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
    "[| g(a) = b; ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
\       [| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x);  b=g(a);  g(a) : D(a) |] ==> P; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
\       ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> a:A;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
\       ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> <a,p>:wf(R) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
\   P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
brs (prems RL prems) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
brs (prems RL [sym]) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
br rcallT 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
by (REPEAT (ares_tac prems 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
val hyprcallT = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
val prems = goal Wfd.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
    "[| g(a) = b; ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x);\
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
\       [| b=g(a);  g(a) : D(a) |] ==> P; a:A;  <a,p>:wf(R) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
\   P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
brs (prems) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
brs (prems RL [sym]) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
br rcallT 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
by (REPEAT (ares_tac prems 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
val hyprcallT = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
val prems = goal Wfd.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
    "[| g(a,b) = c; ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
\       [| c=g(a,b);  g(a,b) : D(a,b) |] ==> P; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
\       a:A;  b:B;  <<a,b>,<p,q>>:wf(R) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
\   P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
brs (prems) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
brs (prems RL [sym]) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
br rcall2T 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
by (REPEAT (ares_tac prems 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
val hyprcall2T = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
val prems = goal Wfd.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
  "[| g(a,b,c) = d; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
\     ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
\   [| d=g(a,b,c);  g(a,b,c) : D(a,b,c) |] ==> P; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
\   a:A;  b:B;  c:C;  <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
\   P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
brs (prems) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
brs (prems RL [sym]) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
br rcall3T 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
by (REPEAT (ares_tac prems 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
val hyprcall3T = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
val hyprcallTs = [hyprcallT,hyprcall2T,hyprcall3T];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
(*** Rules to Remove Induction Hypotheses after Type Checking ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
val prems = goal Wfd.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
    "[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); P |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
\    P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
by (REPEAT (ares_tac prems 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
val rmIH1  = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
val prems = goal Wfd.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
    "[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
\    P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
by (REPEAT (ares_tac prems 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
val rmIH2  = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
val prems = goal Wfd.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
 "[| ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
\    P |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
\    P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
by (REPEAT (ares_tac prems 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
val rmIH3  = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
val rmIHs = [rmIH1,rmIH2,rmIH3];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165