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