src/CCL/Type.ML
author lcp
Mon Sep 20 17:02:11 1993 +0200 (1993-09-20)
changeset 8 c3d2c6dcf3f0
parent 0 a5a9c433f639
child 289 78541329ff35
permissions -rw-r--r--
Installation of new simplfier. Previously appeared to set up the old
simplifier to rewrite with the partial ordering [=, something not possible
with the new simplifier. But such rewriting appears not to have actually
been used, and there were few complications. In terms.ML setloop was used
to avoid infinite rewriting with the letrec rule. Congruence rules were
deleted, and an occasional SIMP_TAC had to become asm_simp_tac.
     1 (*  Title: 	CCL/types
     2     ID:         $Id$
     3     Author: 	Martin Coen, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 For types.thy.
     7 *)
     8 
     9 open Type;
    10 
    11 val simp_type_defs = [Subtype_def,Unit_def,Bool_def,Plus_def,Sigma_def,Pi_def,
    12                       Lift_def,Tall_def,Tex_def];
    13 val ind_type_defs = [Nat_def,List_def];
    14 
    15 val simp_data_defs = [one_def,inl_def,inr_def];
    16 val ind_data_defs = [zero_def,succ_def,nil_def,cons_def];
    17 
    18 goal Set.thy "A <= B <-> (ALL x.x:A --> x:B)";
    19 by (fast_tac set_cs 1);
    20 val subsetXH = result();
    21 
    22 (*** Exhaustion Rules ***)
    23 
    24 fun mk_XH_tac thy defs rls s = prove_goalw thy defs s (fn _ => [cfast_tac rls 1]);
    25 val XH_tac = mk_XH_tac Type.thy simp_type_defs [];
    26 
    27 val EmptyXH = XH_tac "a : {} <-> False";
    28 val SubtypeXH = XH_tac "a : {x:A.P(x)} <-> (a:A & P(a))";
    29 val UnitXH = XH_tac "a : Unit          <-> a=one";
    30 val BoolXH = XH_tac "a : Bool          <-> a=true | a=false";
    31 val PlusXH = XH_tac "a : A+B           <-> (EX x:A.a=inl(x)) | (EX x:B.a=inr(x))";
    32 val PiXH   = XH_tac "a : PROD x:A.B(x) <-> (EX b.a=lam x.b(x) & (ALL x:A.b(x):B(x)))";
    33 val SgXH   = XH_tac "a : SUM x:A.B(x)  <-> (EX x:A.EX y:B(x).a=<x,y>)";
    34 
    35 val XHs = [EmptyXH,SubtypeXH,UnitXH,BoolXH,PlusXH,PiXH,SgXH];
    36 
    37 val LiftXH = XH_tac "a : [A] <-> (a=bot | a:A)";
    38 val TallXH = XH_tac "a : TALL X.B(X) <-> (ALL X. a:B(X))";
    39 val TexXH  = XH_tac "a : TEX X.B(X) <-> (EX X. a:B(X))";
    40 
    41 val case_rls = XH_to_Es XHs;
    42 
    43 (*** Canonical Type Rules ***)
    44 
    45 fun mk_canT_tac thy xhs s = prove_goal thy s 
    46                  (fn prems => [fast_tac (set_cs addIs (prems @ (xhs RL [iffD2]))) 1]);
    47 val canT_tac = mk_canT_tac Type.thy XHs;
    48 
    49 val oneT   = canT_tac "one : Unit";
    50 val trueT  = canT_tac "true : Bool";
    51 val falseT = canT_tac "false : Bool";
    52 val lamT   = canT_tac "[| !!x.x:A ==> b(x):B(x) |] ==> lam x.b(x) : Pi(A,B)";
    53 val pairT  = canT_tac "[| a:A; b:B(a) |] ==> <a,b>:Sigma(A,B)";
    54 val inlT   = canT_tac "a:A ==> inl(a) : A+B";
    55 val inrT   = canT_tac "b:B ==> inr(b) : A+B";
    56 
    57 val canTs = [oneT,trueT,falseT,pairT,lamT,inlT,inrT];
    58 
    59 (*** Non-Canonical Type Rules ***)
    60 
    61 local
    62 val lemma = prove_goal Type.thy "[| a:B(u);  u=v |] ==> a : B(v)"
    63                    (fn prems => [cfast_tac prems 1]);
    64 in
    65 fun mk_ncanT_tac thy defs top_crls crls s = prove_goalw thy defs s 
    66   (fn major::prems => [(resolve_tac ([major] RL top_crls) 1),
    67                        (REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))),
    68                        (ALLGOALS (asm_simp_tac term_ss)),
    69                        (ALLGOALS (ares_tac (prems RL [lemma]) ORELSE' 
    70                                   eresolve_tac [bspec])),
    71                        (safe_tac (ccl_cs addSIs prems))]);
    72 end;
    73 
    74 val ncanT_tac = mk_ncanT_tac Type.thy [] case_rls case_rls;
    75 
    76 val ifT = ncanT_tac 
    77      "[| b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) |] ==> \
    78 \     if b then t else u : A(b)";
    79 
    80 val applyT = ncanT_tac 
    81     "[| f : Pi(A,B);  a:A |] ==> f ` a : B(a)";
    82 
    83 val splitT = ncanT_tac 
    84     "[| p:Sigma(A,B); !!x y. [| x:A;  y:B(x); p=<x,y>  |] ==> c(x,y):C(<x,y>) |] ==>  \
    85 \     split(p,c):C(p)";
    86 
    87 val whenT = ncanT_tac 
    88      "[| p:A+B; !!x.[| x:A;  p=inl(x) |] ==> a(x):C(inl(x)); \
    89 \               !!y.[| y:B;  p=inr(y) |] ==> b(y):C(inr(y)) |] ==> \
    90 \     when(p,a,b) : C(p)";
    91 
    92 val ncanTs = [ifT,applyT,splitT,whenT];
    93 
    94 (*** Subtypes ***)
    95 
    96 val SubtypeD1 = standard ((SubtypeXH RS iffD1) RS conjunct1);
    97 val SubtypeD2 = standard ((SubtypeXH RS iffD1) RS conjunct2);
    98 
    99 val prems = goal Type.thy
   100      "[| a:A;  P(a) |] ==> a : {x:A. P(x)}";
   101 by (REPEAT (resolve_tac (prems@[SubtypeXH RS iffD2,conjI]) 1));
   102 val SubtypeI = result();
   103 
   104 val prems = goal Type.thy
   105      "[| a : {x:A. P(x)};  [| a:A;  P(a) |] ==> Q |] ==> Q";
   106 by (REPEAT (resolve_tac (prems@[SubtypeD1,SubtypeD2]) 1));
   107 val SubtypeE = result();
   108 
   109 (*** Monotonicity ***)
   110 
   111 goal Type.thy "mono (%X.X)";
   112 by (REPEAT (ares_tac [monoI] 1));
   113 val idM = result();
   114 
   115 goal Type.thy "mono(%X.A)";
   116 by (REPEAT (ares_tac [monoI,subset_refl] 1));
   117 val constM = result();
   118 
   119 val major::prems = goal Type.thy
   120     "mono(%X.A(X)) ==> mono(%X.[A(X)])";
   121 br (subsetI RS monoI) 1;
   122 bd (LiftXH RS iffD1) 1;
   123 be disjE 1;
   124 be (disjI1 RS (LiftXH RS iffD2)) 1;
   125 br (disjI2 RS (LiftXH RS iffD2)) 1;
   126 be (major RS monoD RS subsetD) 1;
   127 ba 1;
   128 val LiftM = result();
   129 
   130 val prems = goal Type.thy
   131     "[| mono(%X.A(X)); !!x X. x:A(X) ==> mono(%X.B(X,x)) |] ==> \
   132 \    mono(%X.Sigma(A(X),B(X)))";
   133 by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE
   134             eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
   135             (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
   136             hyp_subst_tac 1));
   137 val SgM = result();
   138 
   139 val prems = goal Type.thy
   140     "[| !!x. x:A ==> mono(%X.B(X,x)) |] ==> mono(%X.Pi(A,B(X)))";
   141 by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE
   142             eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
   143             (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
   144             hyp_subst_tac 1));
   145 val PiM = result();
   146 
   147 val prems = goal Type.thy
   148      "[| mono(%X.A(X));  mono(%X.B(X)) |] ==> mono(%X.A(X)+B(X))";
   149 by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE
   150             eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
   151             (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
   152             hyp_subst_tac 1));
   153 val PlusM = result();
   154 
   155 (**************** RECURSIVE TYPES ******************)
   156 
   157 (*** Conversion Rules for Fixed Points via monotonicity and Tarski ***)
   158 
   159 goal Type.thy "mono(%X.Unit+X)";
   160 by (REPEAT (ares_tac [PlusM,constM,idM] 1));
   161 val NatM = result();
   162 val def_NatB = result() RS (Nat_def RS def_lfp_Tarski);
   163 
   164 goal Type.thy "mono(%X.(Unit+Sigma(A,%y.X)))";
   165 by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
   166 val ListM = result();
   167 val def_ListB = result() RS (List_def RS def_lfp_Tarski);
   168 val def_ListsB = result() RS (Lists_def RS def_gfp_Tarski);
   169 
   170 goal Type.thy "mono(%X.({} + Sigma(A,%y.X)))";
   171 by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
   172 val IListsM = result();
   173 val def_IListsB = result() RS (ILists_def RS def_gfp_Tarski);
   174 
   175 val ind_type_eqs = [def_NatB,def_ListB,def_ListsB,def_IListsB];
   176 
   177 (*** Exhaustion Rules ***)
   178 
   179 fun mk_iXH_tac teqs ddefs rls s = prove_goalw Type.thy ddefs s 
   180            (fn _ => [resolve_tac (teqs RL [XHlemma1]) 1,
   181                      fast_tac (set_cs addSIs canTs addSEs case_rls) 1]);
   182 
   183 val iXH_tac = mk_iXH_tac ind_type_eqs ind_data_defs [];
   184 
   185 val NatXH  = iXH_tac "a : Nat <-> (a=zero | (EX x:Nat.a=succ(x)))";
   186 val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x.xs))";
   187 val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x.xs))";
   188 val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x.xs)";
   189 
   190 val iXHs = [NatXH,ListXH];
   191 val icase_rls = XH_to_Es iXHs;
   192 
   193 (*** Type Rules ***)
   194 
   195 val icanT_tac = mk_canT_tac Type.thy iXHs;
   196 val incanT_tac = mk_ncanT_tac Type.thy [] icase_rls case_rls;
   197 
   198 val zeroT = icanT_tac "zero : Nat";
   199 val succT = icanT_tac "n:Nat ==> succ(n) : Nat";
   200 val nilT  = icanT_tac "[] : List(A)";
   201 val consT = icanT_tac "[| h:A;  t:List(A) |] ==> h.t : List(A)";
   202 
   203 val icanTs = [zeroT,succT,nilT,consT];
   204 
   205 val ncaseT = incanT_tac 
   206      "[| n:Nat; n=zero ==> b:C(zero); \
   207 \        !!x.[| x:Nat;  n=succ(x) |] ==> c(x):C(succ(x)) |] ==>  \
   208 \     ncase(n,b,c) : C(n)";
   209 
   210 val lcaseT = incanT_tac
   211      "[| l:List(A); l=[] ==> b:C([]); \
   212 \        !!h t.[| h:A;  t:List(A); l=h.t |] ==> c(h,t):C(h.t) |] ==> \
   213 \     lcase(l,b,c) : C(l)";
   214 
   215 val incanTs = [ncaseT,lcaseT];
   216 
   217 (*** Induction Rules ***)
   218 
   219 val ind_Ms = [NatM,ListM];
   220 
   221 fun mk_ind_tac ddefs tdefs Ms canTs case_rls s = prove_goalw Type.thy ddefs s 
   222      (fn major::prems => [resolve_tac (Ms RL ([major] RL (tdefs RL [def_induct]))) 1,
   223                           fast_tac (set_cs addSIs (prems @ canTs) addSEs case_rls) 1]);
   224 
   225 val ind_tac = mk_ind_tac ind_data_defs ind_type_defs ind_Ms canTs case_rls;
   226 
   227 val Nat_ind = ind_tac
   228      "[| n:Nat; P(zero); !!x.[| x:Nat; P(x) |] ==> P(succ(x)) |] ==>  \
   229 \     P(n)";
   230 
   231 val List_ind = ind_tac
   232      "[| l:List(A); P([]); \
   233 \        !!x xs.[| x:A;  xs:List(A); P(xs) |] ==> P(x.xs) |] ==> \
   234 \     P(l)";
   235 
   236 val inds = [Nat_ind,List_ind];
   237 
   238 (*** Primitive Recursive Rules ***)
   239 
   240 fun mk_prec_tac inds s = prove_goal Type.thy s
   241      (fn major::prems => [resolve_tac ([major] RL inds) 1,
   242                           ALLGOALS (simp_tac term_ss THEN'
   243                                     fast_tac (set_cs addSIs prems))]);
   244 val prec_tac = mk_prec_tac inds;
   245 
   246 val nrecT = prec_tac
   247      "[| n:Nat; b:C(zero); \
   248 \        !!x g.[| x:Nat; g:C(x) |] ==> c(x,g):C(succ(x)) |] ==>  \
   249 \     nrec(n,b,c) : C(n)";
   250 
   251 val lrecT = prec_tac
   252      "[| l:List(A); b:C([]); \
   253 \        !!x xs g.[| x:A;  xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x.xs) |] ==>  \
   254 \     lrec(l,b,c) : C(l)";
   255 
   256 val precTs = [nrecT,lrecT];
   257 
   258 
   259 (*** Theorem proving ***)
   260 
   261 val [major,minor] = goal Type.thy
   262     "[| <a,b> : Sigma(A,B);  [| a:A;  b:B(a) |] ==> P   \
   263 \    |] ==> P";
   264 br (major RS (XH_to_E SgXH)) 1;
   265 br minor 1;
   266 by (ALLGOALS (fast_tac term_cs));
   267 val SgE2 = result();
   268 
   269 (* General theorem proving ignores non-canonical term-formers,             *)
   270 (*         - intro rules are type rules for canonical terms                *)
   271 (*         - elim rules are case rules (no non-canonical terms appear)     *)
   272 
   273 val type_cs = term_cs addSIs (SubtypeI::(canTs @ icanTs))
   274                       addSEs (SubtypeE::(XH_to_Es XHs));
   275 
   276 
   277 (*** Infinite Data Types ***)
   278 
   279 val [mono] = goal Type.thy "mono(f) ==> lfp(f) <= gfp(f)";
   280 br (lfp_lowerbound RS subset_trans) 1;
   281 br (mono RS gfp_lemma3) 1;
   282 br subset_refl 1;
   283 val lfp_subset_gfp = result();
   284 
   285 val prems = goal Type.thy
   286     "[| a:A;  !!x X.[| x:A;  ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
   287 \    t(a) : gfp(B)";
   288 br coinduct 1;
   289 by (res_inst_tac [("P","%x.EX y:A.x=t(y)")] CollectI 1);
   290 by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
   291 val gfpI = result();
   292 
   293 val rew::prem::prems = goal Type.thy
   294     "[| C==gfp(B);  a:A;  !!x X.[| x:A;  ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
   295 \    t(a) : C";
   296 by (rewtac rew);
   297 by (REPEAT (ares_tac ((prem RS gfpI)::prems) 1));
   298 val def_gfpI = result();
   299 
   300 (* EG *)
   301 
   302 val prems = goal Type.thy 
   303     "letrec g x be zero.g(x) in g(bot) : Lists(Nat)";
   304 by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1);
   305 br (letrecB RS ssubst) 1;
   306 bw cons_def;
   307 by (fast_tac type_cs 1);
   308 result();