src/CCL/genrec.ML
author paulson
Fri Feb 16 17:24:51 1996 +0100 (1996-02-16)
changeset 1511 09354d37a5ab
parent 1459 d12da312eff4
child 2035 e329b36d9136
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
clasohm@1459
     1
(*  Title:      92/CCL/genrec
clasohm@0
     2
    ID:         $Id$
clasohm@1459
     3
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
*)
clasohm@0
     7
clasohm@0
     8
(*** General Recursive Functions ***)
clasohm@0
     9
clasohm@0
    10
val major::prems = goal Wfd.thy 
clasohm@0
    11
    "[| a : A;  \
clasohm@0
    12
\       !!p g.[| p:A; ALL x:{x: A. <x,p>:wf(R)}. g(x) : D(x) |] ==>\
clasohm@0
    13
\               h(p,g) : D(p) |] ==> \
clasohm@0
    14
\    letrec g x be h(x,g) in g(a) : D(a)";
lcp@642
    15
by (rtac (major RS rev_mp) 1);
lcp@642
    16
by (rtac (wf_wf RS wfd_induct) 1);
lcp@642
    17
by (rtac (letrecB RS ssubst) 1);
lcp@642
    18
by (rtac impI 1);
lcp@642
    19
by (eresolve_tac prems 1);
lcp@642
    20
by (rtac ballI 1);
lcp@642
    21
by (etac (spec RS mp RS mp) 1);
clasohm@0
    22
by (REPEAT (eresolve_tac [SubtypeD1,SubtypeD2] 1));
clasohm@757
    23
qed "letrecT";
clasohm@0
    24
clasohm@0
    25
goalw Wfd.thy [SPLIT_def] "SPLIT(<a,b>,B) = B(a,b)";
lcp@642
    26
by (rtac set_ext 1);
clasohm@0
    27
by (fast_tac ccl_cs 1);
clasohm@757
    28
qed "SPLITB";
clasohm@0
    29
clasohm@0
    30
val prems = goalw Wfd.thy [letrec2_def]
clasohm@0
    31
    "[| a : A;  b : B;  \
clasohm@0
    32
\     !!p q g.[| p:A; q:B; \
clasohm@0
    33
\             ALL x:A.ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==>\
clasohm@0
    34
\               h(p,q,g) : D(p,q) |] ==> \
clasohm@0
    35
\    letrec g x y be h(x,y,g) in g(a,b) : D(a,b)";
lcp@642
    36
by (rtac (SPLITB RS subst) 1);
clasohm@0
    37
by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1));
lcp@642
    38
by (rtac (SPLITB RS ssubst) 1);
clasohm@0
    39
by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1));
lcp@642
    40
by (rtac (SPLITB RS subst) 1);
clasohm@0
    41
by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE 
clasohm@0
    42
            eresolve_tac [bspec,SubtypeE,sym RS subst] 1));
clasohm@757
    43
qed "letrec2T";
clasohm@0
    44
clasohm@0
    45
goal Wfd.thy "SPLIT(<a,<b,c>>,%x xs.SPLIT(xs,%y z.B(x,y,z))) = B(a,b,c)";
lcp@10
    46
by (simp_tac (ccl_ss addsimps [SPLITB]) 1);
clasohm@757
    47
qed "lemma";
clasohm@0
    48
clasohm@0
    49
val prems = goalw Wfd.thy [letrec3_def]
clasohm@0
    50
    "[| a : A;  b : B;  c : C;  \
clasohm@0
    51
\    !!p q r g.[| p:A; q:B; r:C; \
clasohm@0
    52
\      ALL x:A.ALL y:B.ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}. \
clasohm@0
    53
\                                                       g(x,y,z) : D(x,y,z) |] ==>\
clasohm@0
    54
\               h(p,q,r,g) : D(p,q,r) |] ==> \
clasohm@0
    55
\    letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)";
lcp@642
    56
by (rtac (lemma RS subst) 1);
clasohm@0
    57
by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1));
lcp@10
    58
by (simp_tac (ccl_ss addsimps [SPLITB]) 1);
clasohm@0
    59
by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1));
lcp@642
    60
by (rtac (lemma RS subst) 1);
clasohm@0
    61
by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE 
clasohm@0
    62
            eresolve_tac [bspec,SubtypeE,sym RS subst] 1));
clasohm@757
    63
qed "letrec3T";
clasohm@0
    64
clasohm@0
    65
val letrecTs = [letrecT,letrec2T,letrec3T];
clasohm@0
    66
clasohm@0
    67
clasohm@0
    68
(*** Type Checking for Recursive Calls ***)
clasohm@0
    69
clasohm@0
    70
val major::prems = goal Wfd.thy
clasohm@0
    71
    "[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); \
clasohm@0
    72
\       g(a) : D(a) ==> g(a) : E;  a:A;  <a,p>:wf(R) |] ==> \
clasohm@0
    73
\   g(a) : E";
clasohm@0
    74
by (REPEAT (ares_tac ([SubtypeI,major RS bspec,major]@prems) 1));
clasohm@757
    75
qed "rcallT";
clasohm@0
    76
clasohm@0
    77
val major::prems = goal Wfd.thy
clasohm@0
    78
    "[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
clasohm@0
    79
\       g(a,b) : D(a,b) ==> g(a,b) : E;  a:A;  b:B;  <<a,b>,<p,q>>:wf(R) |] ==> \
clasohm@0
    80
\   g(a,b) : E";
clasohm@0
    81
by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec,major]@prems) 1));
clasohm@757
    82
qed "rcall2T";
clasohm@0
    83
clasohm@0
    84
val major::prems = goal Wfd.thy
clasohm@0
    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); \
clasohm@0
    86
\       g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E;  \
clasohm@0
    87
\       a:A;  b:B;  c:C;  <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \
clasohm@0
    88
\   g(a,b,c) : E";
clasohm@0
    89
by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec RS bspec,major]@prems) 1));
clasohm@757
    90
qed "rcall3T";
clasohm@0
    91
clasohm@0
    92
val rcallTs = [rcallT,rcall2T,rcall3T];
clasohm@0
    93
clasohm@0
    94
(*** Instantiating an induction hypothesis with an equality assumption ***)
clasohm@0
    95
clasohm@0
    96
val prems = goal Wfd.thy
clasohm@0
    97
    "[| g(a) = b; ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x);  \
clasohm@0
    98
\       [| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x);  b=g(a);  g(a) : D(a) |] ==> P; \
clasohm@0
    99
\       ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> a:A;  \
clasohm@0
   100
\       ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x) ==> <a,p>:wf(R) |] ==> \
clasohm@0
   101
\   P";
lcp@642
   102
by (resolve_tac (prems RL prems) 1);
lcp@642
   103
by (resolve_tac (prems RL [sym]) 1);
lcp@642
   104
by (rtac rcallT 1);
clasohm@0
   105
by (REPEAT (ares_tac prems 1));
clasohm@0
   106
val hyprcallT = result();
clasohm@0
   107
clasohm@0
   108
val prems = goal Wfd.thy
clasohm@0
   109
    "[| g(a) = b; ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x);\
clasohm@0
   110
\       [| b=g(a);  g(a) : D(a) |] ==> P; a:A;  <a,p>:wf(R) |] ==> \
clasohm@0
   111
\   P";
lcp@642
   112
by (resolve_tac (prems) 1);
lcp@642
   113
by (resolve_tac (prems RL [sym]) 1);
lcp@642
   114
by (rtac rcallT 1);
clasohm@0
   115
by (REPEAT (ares_tac prems 1));
clasohm@757
   116
qed "hyprcallT";
clasohm@0
   117
clasohm@0
   118
val prems = goal Wfd.thy
clasohm@0
   119
    "[| g(a,b) = c; ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
clasohm@0
   120
\       [| c=g(a,b);  g(a,b) : D(a,b) |] ==> P; \
clasohm@0
   121
\       a:A;  b:B;  <<a,b>,<p,q>>:wf(R) |] ==> \
clasohm@0
   122
\   P";
lcp@642
   123
by (resolve_tac (prems) 1);
lcp@642
   124
by (resolve_tac (prems RL [sym]) 1);
lcp@642
   125
by (rtac rcall2T 1);
clasohm@0
   126
by (REPEAT (ares_tac prems 1));
clasohm@757
   127
qed "hyprcall2T";
clasohm@0
   128
clasohm@0
   129
val prems = goal Wfd.thy
clasohm@0
   130
  "[| g(a,b,c) = d; \
clasohm@0
   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); \
clasohm@0
   132
\   [| d=g(a,b,c);  g(a,b,c) : D(a,b,c) |] ==> P; \
clasohm@0
   133
\   a:A;  b:B;  c:C;  <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \
clasohm@0
   134
\   P";
lcp@642
   135
by (resolve_tac (prems) 1);
lcp@642
   136
by (resolve_tac (prems RL [sym]) 1);
lcp@642
   137
by (rtac rcall3T 1);
clasohm@0
   138
by (REPEAT (ares_tac prems 1));
clasohm@757
   139
qed "hyprcall3T";
clasohm@0
   140
clasohm@0
   141
val hyprcallTs = [hyprcallT,hyprcall2T,hyprcall3T];
clasohm@0
   142
clasohm@0
   143
(*** Rules to Remove Induction Hypotheses after Type Checking ***)
clasohm@0
   144
clasohm@0
   145
val prems = goal Wfd.thy
clasohm@0
   146
    "[| ALL x:{x:A.<x,p>:wf(R)}.g(x):D(x); P |] ==> \
clasohm@0
   147
\    P";
clasohm@0
   148
by (REPEAT (ares_tac prems 1));
clasohm@757
   149
qed "rmIH1";
clasohm@0
   150
clasohm@0
   151
val prems = goal Wfd.thy
clasohm@0
   152
    "[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> \
clasohm@0
   153
\    P";
clasohm@0
   154
by (REPEAT (ares_tac prems 1));
clasohm@757
   155
qed "rmIH2";
clasohm@0
   156
clasohm@0
   157
val prems = goal Wfd.thy
clasohm@0
   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); \
clasohm@0
   159
\    P |] ==> \
clasohm@0
   160
\    P";
clasohm@0
   161
by (REPEAT (ares_tac prems 1));
clasohm@757
   162
qed "rmIH3";
clasohm@0
   163
clasohm@0
   164
val rmIHs = [rmIH1,rmIH2,rmIH3];
clasohm@0
   165