src/CCL/Type.ML
author wenzelm
Fri Oct 10 17:10:12 1997 +0200 (1997-10-10)
changeset 3837 d7f033c74b38
parent 2035 e329b36d9136
child 5062 fbdb0b541314
permissions -rw-r--r--
fixed dots;
     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 qed "subsetXH";
    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                                   etac 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 qed "SubtypeI";
   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 qed "SubtypeE";
   108 
   109 (*** Monotonicity ***)
   110 
   111 goal Type.thy "mono (%X. X)";
   112 by (REPEAT (ares_tac [monoI] 1));
   113 qed "idM";
   114 
   115 goal Type.thy "mono(%X. A)";
   116 by (REPEAT (ares_tac [monoI,subset_refl] 1));
   117 qed "constM";
   118 
   119 val major::prems = goal Type.thy
   120     "mono(%X. A(X)) ==> mono(%X.[A(X)])";
   121 by (rtac (subsetI RS monoI) 1);
   122 by (dtac (LiftXH RS iffD1) 1);
   123 by (etac disjE 1);
   124 by (etac (disjI1 RS (LiftXH RS iffD2)) 1);
   125 by (rtac (disjI2 RS (LiftXH RS iffD2)) 1);
   126 by (etac (major RS monoD RS subsetD) 1);
   127 by (assume_tac 1);
   128 qed "LiftM";
   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 qed "SgM";
   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 qed "PiM";
   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 qed "PlusM";
   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 qed "NatM";
   162 bind_thm("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 qed "ListM";
   167 bind_thm("def_ListB", result() RS (List_def RS def_lfp_Tarski));
   168 bind_thm("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 qed "IListsM";
   173 bind_thm("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 by (rtac (major RS (XH_to_E SgXH)) 1);
   265 by (rtac minor 1);
   266 by (ALLGOALS (fast_tac term_cs));
   267 qed "SgE2";
   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 by (rtac (lfp_lowerbound RS subset_trans) 1);
   281 by (rtac (mono RS gfp_lemma3) 1);
   282 by (rtac subset_refl 1);
   283 qed "lfp_subset_gfp";
   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 by (rtac 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 qed "gfpI";
   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 qed "def_gfpI";
   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 by (stac letrecB 1);
   306 by (rewtac cons_def);
   307 by (fast_tac type_cs 1);
   308 result();