src/CCL/Type.ML
changeset 0 a5a9c433f639
child 8 c3d2c6dcf3f0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CCL/Type.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,308 @@
     1.4 +(*  Title: 	CCL/types
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Martin Coen, Cambridge University Computer Laboratory
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +For types.thy.
    1.10 +*)
    1.11 +
    1.12 +open Type;
    1.13 +
    1.14 +val simp_type_defs = [Subtype_def,Unit_def,Bool_def,Plus_def,Sigma_def,Pi_def,
    1.15 +                      Lift_def,Tall_def,Tex_def];
    1.16 +val ind_type_defs = [Nat_def,List_def];
    1.17 +
    1.18 +val simp_data_defs = [one_def,inl_def,inr_def];
    1.19 +val ind_data_defs = [zero_def,succ_def,nil_def,cons_def];
    1.20 +
    1.21 +goal Set.thy "A <= B <-> (ALL x.x:A --> x:B)";
    1.22 +by (fast_tac set_cs 1);
    1.23 +val subsetXH = result();
    1.24 +
    1.25 +(*** Exhaustion Rules ***)
    1.26 +
    1.27 +fun mk_XH_tac thy defs rls s = prove_goalw thy defs s (fn _ => [cfast_tac rls 1]);
    1.28 +val XH_tac = mk_XH_tac Type.thy simp_type_defs [];
    1.29 +
    1.30 +val EmptyXH = XH_tac "a : {} <-> False";
    1.31 +val SubtypeXH = XH_tac "a : {x:A.P(x)} <-> (a:A & P(a))";
    1.32 +val UnitXH = XH_tac "a : Unit          <-> a=one";
    1.33 +val BoolXH = XH_tac "a : Bool          <-> a=true | a=false";
    1.34 +val PlusXH = XH_tac "a : A+B           <-> (EX x:A.a=inl(x)) | (EX x:B.a=inr(x))";
    1.35 +val PiXH   = XH_tac "a : PROD x:A.B(x) <-> (EX b.a=lam x.b(x) & (ALL x:A.b(x):B(x)))";
    1.36 +val SgXH   = XH_tac "a : SUM x:A.B(x)  <-> (EX x:A.EX y:B(x).a=<x,y>)";
    1.37 +
    1.38 +val XHs = [EmptyXH,SubtypeXH,UnitXH,BoolXH,PlusXH,PiXH,SgXH];
    1.39 +
    1.40 +val LiftXH = XH_tac "a : [A] <-> (a=bot | a:A)";
    1.41 +val TallXH = XH_tac "a : TALL X.B(X) <-> (ALL X. a:B(X))";
    1.42 +val TexXH  = XH_tac "a : TEX X.B(X) <-> (EX X. a:B(X))";
    1.43 +
    1.44 +val case_rls = XH_to_Es XHs;
    1.45 +
    1.46 +(*** Canonical Type Rules ***)
    1.47 +
    1.48 +fun mk_canT_tac thy xhs s = prove_goal thy s 
    1.49 +                 (fn prems => [fast_tac (set_cs addIs (prems @ (xhs RL [iffD2]))) 1]);
    1.50 +val canT_tac = mk_canT_tac Type.thy XHs;
    1.51 +
    1.52 +val oneT   = canT_tac "one : Unit";
    1.53 +val trueT  = canT_tac "true : Bool";
    1.54 +val falseT = canT_tac "false : Bool";
    1.55 +val lamT   = canT_tac "[| !!x.x:A ==> b(x):B(x) |] ==> lam x.b(x) : Pi(A,B)";
    1.56 +val pairT  = canT_tac "[| a:A; b:B(a) |] ==> <a,b>:Sigma(A,B)";
    1.57 +val inlT   = canT_tac "a:A ==> inl(a) : A+B";
    1.58 +val inrT   = canT_tac "b:B ==> inr(b) : A+B";
    1.59 +
    1.60 +val canTs = [oneT,trueT,falseT,pairT,lamT,inlT,inrT];
    1.61 +
    1.62 +(*** Non-Canonical Type Rules ***)
    1.63 +
    1.64 +local
    1.65 +val lemma = prove_goal Type.thy "[| a:B(u);  u=v |] ==> a : B(v)"
    1.66 +                   (fn prems => [cfast_tac prems 1]);
    1.67 +in
    1.68 +fun mk_ncanT_tac thy defs top_crls crls s = prove_goalw thy defs s 
    1.69 +  (fn major::prems => [(resolve_tac ([major] RL top_crls) 1),
    1.70 +                       (REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))),
    1.71 +                       (ALLGOALS (ASM_SIMP_TAC term_ss)),
    1.72 +                       (ALLGOALS (ares_tac (prems RL [lemma]) ORELSE' 
    1.73 +                                  eresolve_tac [bspec])),
    1.74 +                       (safe_tac (ccl_cs addSIs prems))]);
    1.75 +end;
    1.76 +
    1.77 +val ncanT_tac = mk_ncanT_tac Type.thy [] case_rls case_rls;
    1.78 +
    1.79 +val ifT = ncanT_tac 
    1.80 +     "[| b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) |] ==> \
    1.81 +\     if b then t else u : A(b)";
    1.82 +
    1.83 +val applyT = ncanT_tac 
    1.84 +    "[| f : Pi(A,B);  a:A |] ==> f ` a : B(a)";
    1.85 +
    1.86 +val splitT = ncanT_tac 
    1.87 +    "[| p:Sigma(A,B); !!x y. [| x:A;  y:B(x); p=<x,y>  |] ==> c(x,y):C(<x,y>) |] ==>  \
    1.88 +\     split(p,c):C(p)";
    1.89 +
    1.90 +val whenT = ncanT_tac 
    1.91 +     "[| p:A+B; !!x.[| x:A;  p=inl(x) |] ==> a(x):C(inl(x)); \
    1.92 +\               !!y.[| y:B;  p=inr(y) |] ==> b(y):C(inr(y)) |] ==> \
    1.93 +\     when(p,a,b) : C(p)";
    1.94 +
    1.95 +val ncanTs = [ifT,applyT,splitT,whenT];
    1.96 +
    1.97 +(*** Subtypes ***)
    1.98 +
    1.99 +val SubtypeD1 = standard ((SubtypeXH RS iffD1) RS conjunct1);
   1.100 +val SubtypeD2 = standard ((SubtypeXH RS iffD1) RS conjunct2);
   1.101 +
   1.102 +val prems = goal Type.thy
   1.103 +     "[| a:A;  P(a) |] ==> a : {x:A. P(x)}";
   1.104 +by (REPEAT (resolve_tac (prems@[SubtypeXH RS iffD2,conjI]) 1));
   1.105 +val SubtypeI = result();
   1.106 +
   1.107 +val prems = goal Type.thy
   1.108 +     "[| a : {x:A. P(x)};  [| a:A;  P(a) |] ==> Q |] ==> Q";
   1.109 +by (REPEAT (resolve_tac (prems@[SubtypeD1,SubtypeD2]) 1));
   1.110 +val SubtypeE = result();
   1.111 +
   1.112 +(*** Monotonicity ***)
   1.113 +
   1.114 +goal Type.thy "mono (%X.X)";
   1.115 +by (REPEAT (ares_tac [monoI] 1));
   1.116 +val idM = result();
   1.117 +
   1.118 +goal Type.thy "mono(%X.A)";
   1.119 +by (REPEAT (ares_tac [monoI,subset_refl] 1));
   1.120 +val constM = result();
   1.121 +
   1.122 +val major::prems = goal Type.thy
   1.123 +    "mono(%X.A(X)) ==> mono(%X.[A(X)])";
   1.124 +br (subsetI RS monoI) 1;
   1.125 +bd (LiftXH RS iffD1) 1;
   1.126 +be disjE 1;
   1.127 +be (disjI1 RS (LiftXH RS iffD2)) 1;
   1.128 +br (disjI2 RS (LiftXH RS iffD2)) 1;
   1.129 +be (major RS monoD RS subsetD) 1;
   1.130 +ba 1;
   1.131 +val LiftM = result();
   1.132 +
   1.133 +val prems = goal Type.thy
   1.134 +    "[| mono(%X.A(X)); !!x X. x:A(X) ==> mono(%X.B(X,x)) |] ==> \
   1.135 +\    mono(%X.Sigma(A(X),B(X)))";
   1.136 +by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE
   1.137 +            eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
   1.138 +            (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
   1.139 +            hyp_subst_tac 1));
   1.140 +val SgM = result();
   1.141 +
   1.142 +val prems = goal Type.thy
   1.143 +    "[| !!x. x:A ==> mono(%X.B(X,x)) |] ==> mono(%X.Pi(A,B(X)))";
   1.144 +by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE
   1.145 +            eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
   1.146 +            (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
   1.147 +            hyp_subst_tac 1));
   1.148 +val PiM = result();
   1.149 +
   1.150 +val prems = goal Type.thy
   1.151 +     "[| mono(%X.A(X));  mono(%X.B(X)) |] ==> mono(%X.A(X)+B(X))";
   1.152 +by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE
   1.153 +            eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
   1.154 +            (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
   1.155 +            hyp_subst_tac 1));
   1.156 +val PlusM = result();
   1.157 +
   1.158 +(**************** RECURSIVE TYPES ******************)
   1.159 +
   1.160 +(*** Conversion Rules for Fixed Points via monotonicity and Tarski ***)
   1.161 +
   1.162 +goal Type.thy "mono(%X.Unit+X)";
   1.163 +by (REPEAT (ares_tac [PlusM,constM,idM] 1));
   1.164 +val NatM = result();
   1.165 +val def_NatB = result() RS (Nat_def RS def_lfp_Tarski);
   1.166 +
   1.167 +goal Type.thy "mono(%X.(Unit+Sigma(A,%y.X)))";
   1.168 +by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
   1.169 +val ListM = result();
   1.170 +val def_ListB = result() RS (List_def RS def_lfp_Tarski);
   1.171 +val def_ListsB = result() RS (Lists_def RS def_gfp_Tarski);
   1.172 +
   1.173 +goal Type.thy "mono(%X.({} + Sigma(A,%y.X)))";
   1.174 +by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
   1.175 +val IListsM = result();
   1.176 +val def_IListsB = result() RS (ILists_def RS def_gfp_Tarski);
   1.177 +
   1.178 +val ind_type_eqs = [def_NatB,def_ListB,def_ListsB,def_IListsB];
   1.179 +
   1.180 +(*** Exhaustion Rules ***)
   1.181 +
   1.182 +fun mk_iXH_tac teqs ddefs rls s = prove_goalw Type.thy ddefs s 
   1.183 +           (fn _ => [resolve_tac (teqs RL [XHlemma1]) 1,
   1.184 +                     fast_tac (set_cs addSIs canTs addSEs case_rls) 1]);
   1.185 +
   1.186 +val iXH_tac = mk_iXH_tac ind_type_eqs ind_data_defs [];
   1.187 +
   1.188 +val NatXH  = iXH_tac "a : Nat <-> (a=zero | (EX x:Nat.a=succ(x)))";
   1.189 +val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x.xs))";
   1.190 +val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x.xs))";
   1.191 +val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x.xs)";
   1.192 +
   1.193 +val iXHs = [NatXH,ListXH];
   1.194 +val icase_rls = XH_to_Es iXHs;
   1.195 +
   1.196 +(*** Type Rules ***)
   1.197 +
   1.198 +val icanT_tac = mk_canT_tac Type.thy iXHs;
   1.199 +val incanT_tac = mk_ncanT_tac Type.thy [] icase_rls case_rls;
   1.200 +
   1.201 +val zeroT = icanT_tac "zero : Nat";
   1.202 +val succT = icanT_tac "n:Nat ==> succ(n) : Nat";
   1.203 +val nilT  = icanT_tac "[] : List(A)";
   1.204 +val consT = icanT_tac "[| h:A;  t:List(A) |] ==> h.t : List(A)";
   1.205 +
   1.206 +val icanTs = [zeroT,succT,nilT,consT];
   1.207 +
   1.208 +val ncaseT = incanT_tac 
   1.209 +     "[| n:Nat; n=zero ==> b:C(zero); \
   1.210 +\        !!x.[| x:Nat;  n=succ(x) |] ==> c(x):C(succ(x)) |] ==>  \
   1.211 +\     ncase(n,b,c) : C(n)";
   1.212 +
   1.213 +val lcaseT = incanT_tac
   1.214 +     "[| l:List(A); l=[] ==> b:C([]); \
   1.215 +\        !!h t.[| h:A;  t:List(A); l=h.t |] ==> c(h,t):C(h.t) |] ==> \
   1.216 +\     lcase(l,b,c) : C(l)";
   1.217 +
   1.218 +val incanTs = [ncaseT,lcaseT];
   1.219 +
   1.220 +(*** Induction Rules ***)
   1.221 +
   1.222 +val ind_Ms = [NatM,ListM];
   1.223 +
   1.224 +fun mk_ind_tac ddefs tdefs Ms canTs case_rls s = prove_goalw Type.thy ddefs s 
   1.225 +     (fn major::prems => [resolve_tac (Ms RL ([major] RL (tdefs RL [def_induct]))) 1,
   1.226 +                          fast_tac (set_cs addSIs (prems @ canTs) addSEs case_rls) 1]);
   1.227 +
   1.228 +val ind_tac = mk_ind_tac ind_data_defs ind_type_defs ind_Ms canTs case_rls;
   1.229 +
   1.230 +val Nat_ind = ind_tac
   1.231 +     "[| n:Nat; P(zero); !!x.[| x:Nat; P(x) |] ==> P(succ(x)) |] ==>  \
   1.232 +\     P(n)";
   1.233 +
   1.234 +val List_ind = ind_tac
   1.235 +     "[| l:List(A); P([]); \
   1.236 +\        !!x xs.[| x:A;  xs:List(A); P(xs) |] ==> P(x.xs) |] ==> \
   1.237 +\     P(l)";
   1.238 +
   1.239 +val inds = [Nat_ind,List_ind];
   1.240 +
   1.241 +(*** Primitive Recursive Rules ***)
   1.242 +
   1.243 +fun mk_prec_tac inds s = prove_goal Type.thy s
   1.244 +     (fn major::prems => [resolve_tac ([major] RL inds) 1,
   1.245 +                          ALLGOALS (SIMP_TAC term_ss THEN'
   1.246 +                                    fast_tac (set_cs addSIs prems))]);
   1.247 +val prec_tac = mk_prec_tac inds;
   1.248 +
   1.249 +val nrecT = prec_tac
   1.250 +     "[| n:Nat; b:C(zero); \
   1.251 +\        !!x g.[| x:Nat; g:C(x) |] ==> c(x,g):C(succ(x)) |] ==>  \
   1.252 +\     nrec(n,b,c) : C(n)";
   1.253 +
   1.254 +val lrecT = prec_tac
   1.255 +     "[| l:List(A); b:C([]); \
   1.256 +\        !!x xs g.[| x:A;  xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x.xs) |] ==>  \
   1.257 +\     lrec(l,b,c) : C(l)";
   1.258 +
   1.259 +val precTs = [nrecT,lrecT];
   1.260 +
   1.261 +
   1.262 +(*** Theorem proving ***)
   1.263 +
   1.264 +val [major,minor] = goal Type.thy
   1.265 +    "[| <a,b> : Sigma(A,B);  [| a:A;  b:B(a) |] ==> P   \
   1.266 +\    |] ==> P";
   1.267 +br (major RS (XH_to_E SgXH)) 1;
   1.268 +br minor 1;
   1.269 +by (ALLGOALS (fast_tac term_cs));
   1.270 +val SgE2 = result();
   1.271 +
   1.272 +(* General theorem proving ignores non-canonical term-formers,             *)
   1.273 +(*         - intro rules are type rules for canonical terms                *)
   1.274 +(*         - elim rules are case rules (no non-canonical terms appear)     *)
   1.275 +
   1.276 +val type_cs = term_cs addSIs (SubtypeI::(canTs @ icanTs))
   1.277 +                      addSEs (SubtypeE::(XH_to_Es XHs));
   1.278 +
   1.279 +
   1.280 +(*** Infinite Data Types ***)
   1.281 +
   1.282 +val [mono] = goal Type.thy "mono(f) ==> lfp(f) <= gfp(f)";
   1.283 +br (lfp_lowerbound RS subset_trans) 1;
   1.284 +br (mono RS gfp_lemma3) 1;
   1.285 +br subset_refl 1;
   1.286 +val lfp_subset_gfp = result();
   1.287 +
   1.288 +val prems = goal Type.thy
   1.289 +    "[| a:A;  !!x X.[| x:A;  ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
   1.290 +\    t(a) : gfp(B)";
   1.291 +br coinduct 1;
   1.292 +by (res_inst_tac [("P","%x.EX y:A.x=t(y)")] CollectI 1);
   1.293 +by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
   1.294 +val gfpI = result();
   1.295 +
   1.296 +val rew::prem::prems = goal Type.thy
   1.297 +    "[| C==gfp(B);  a:A;  !!x X.[| x:A;  ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
   1.298 +\    t(a) : C";
   1.299 +by (rewtac rew);
   1.300 +by (REPEAT (ares_tac ((prem RS gfpI)::prems) 1));
   1.301 +val def_gfpI = result();
   1.302 +
   1.303 +(* EG *)
   1.304 +
   1.305 +val prems = goal Type.thy 
   1.306 +    "letrec g x be zero.g(x) in g(bot) : Lists(Nat)";
   1.307 +by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1);
   1.308 +br (letrecB RS ssubst) 1;
   1.309 +bw cons_def;
   1.310 +by (fast_tac type_cs 1);
   1.311 +result();