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