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