src/CCL/Type.ML
author lcp
Wed, 19 Oct 1994 09:23:56 +0100
changeset 642 0db578095e6a
parent 289 78541329ff35
child 757 2ca12511676d
permissions -rw-r--r--
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification CCL/CCL, Fix, Gfp, Hered, Set, Term, Trancl, Type, Wfd: expanded shorthands
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' 
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 289
diff changeset
    70
                                  etac bspec )),
0
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)])";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 289
diff changeset
   121
by (rtac (subsetI RS monoI) 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 289
diff changeset
   122
by (dtac (LiftXH RS iffD1) 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 289
diff changeset
   123
by (etac disjE 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 289
diff changeset
   124
by (etac (disjI1 RS (LiftXH RS iffD2)) 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 289
diff changeset
   125
by (rtac (disjI2 RS (LiftXH RS iffD2)) 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 289
diff changeset
   126
by (etac (major RS monoD RS subsetD) 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 289
diff changeset
   127
by (assume_tac 1);
0
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)))";
289
78541329ff35 changed "." to "$" to eliminate ambiguity
clasohm
parents: 8
diff changeset
   186
val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x$xs))";
78541329ff35 changed "." to "$" to eliminate ambiguity
clasohm
parents: 8
diff changeset
   187
val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x$xs))";
78541329ff35 changed "." to "$" to eliminate ambiguity
clasohm
parents: 8
diff changeset
   188
val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x$xs)";
0
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)";
289
78541329ff35 changed "." to "$" to eliminate ambiguity
clasohm
parents: 8
diff changeset
   201
val consT = icanT_tac "[| h:A;  t:List(A) |] ==> h$t : List(A)";
0
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([]); \
289
78541329ff35 changed "." to "$" to eliminate ambiguity
clasohm
parents: 8
diff changeset
   212
\        !!h t.[| h:A;  t:List(A); l=h$t |] ==> c(h,t):C(h$t) |] ==> \
0
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([]); \
289
78541329ff35 changed "." to "$" to eliminate ambiguity
clasohm
parents: 8
diff changeset
   233
\        !!x xs.[| x:A;  xs:List(A); P(xs) |] ==> P(x$xs) |] ==> \
0
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([]); \
289
78541329ff35 changed "." to "$" to eliminate ambiguity
clasohm
parents: 8
diff changeset
   253
\        !!x xs g.[| x:A;  xs:List(A); g:C(xs) |] ==> c(x,xs,g):C(x$xs) |] ==>  \
0
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";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 289
diff changeset
   264
by (rtac (major RS (XH_to_E SgXH)) 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 289
diff changeset
   265
by (rtac minor 1);
0
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)";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 289
diff changeset
   280
by (rtac (lfp_lowerbound RS subset_trans) 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 289
diff changeset
   281
by (rtac (mono RS gfp_lemma3) 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 289
diff changeset
   282
by (rtac subset_refl 1);
0
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)";
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 289
diff changeset
   288
by (rtac coinduct 1);
0
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 
289
78541329ff35 changed "." to "$" to eliminate ambiguity
clasohm
parents: 8
diff changeset
   303
    "letrec g x be zero$g(x) in g(bot) : Lists(Nat)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
by (rtac (refl RS (XH_to_I UnitXH) RS (Lists_def RS def_gfpI)) 1);
642
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 289
diff changeset
   305
by (rtac (letrecB RS ssubst) 1);
0db578095e6a CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
lcp
parents: 289
diff changeset
   306
by (rewtac cons_def);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
by (fast_tac type_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   308
result();