src/CTT/CTT.ML
author obua
Fri, 16 Sep 2005 21:02:15 +0200
changeset 17440 df77edc4f5d0
parent 15570 8d8c70b41bab
child 17441 5b5feca0344a
permissions -rw-r--r--
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9251
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
     1
(*  Title:      CTT/CTT.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1459
d12da312eff4 expanded tabs
clasohm
parents: 1294
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
9251
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
     6
Tactics and derived rules for Constructive Type Theory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
(*Formation rules*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
val form_rls = [NF, ProdF, SumF, PlusF, EqF, FF, TF]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
and formL_rls = [ProdFL, SumFL, PlusFL, EqFL];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
(*Introduction rules
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  OMITTED: EqI, because its premise is an eqelem, not an elem*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
val intr_rls = [NI0, NI_succ, ProdI, SumI, PlusI_inl, PlusI_inr, TI]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
and intrL_rls = [NI_succL, ProdIL, SumIL, PlusI_inlL, PlusI_inrL];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
(*Elimination rules
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
  OMITTED: EqE, because its conclusion is an eqelem,  not an elem
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
           TE, because it does not involve a constructor *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
val elim_rls = [NE, ProdE, SumE, PlusE, FE]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
and elimL_rls = [NEL, ProdEL, SumEL, PlusEL, FEL];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
(*OMITTED: eqC are TC because they make rewriting loop: p = un = un = ... *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
val comp_rls = [NC0, NC_succ, ProdC, SumC, PlusC_inl, PlusC_inr];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
(*rules with conclusion a:A, an elem judgement*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
val element_rls = intr_rls @ elim_rls;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
(*Definitions are (meta)equality axioms*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
val basic_defs = [fst_def,snd_def];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
(*Compare with standard version: B is applied to UNSIMPLIFIED expression! *)
9251
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
    36
Goal "[| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)";
9249
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
    37
by (rtac sym_elem 1);
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
    38
by (rtac SumIL 1);
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
    39
by (ALLGOALS (rtac sym_elem ));
9251
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
    40
by (ALLGOALS assume_tac) ;
9249
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
    41
qed "SumIL2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
val intrL2_rls = [NI_succL, ProdIL, SumIL2, PlusI_inlL, PlusI_inrL];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
(*Exploit p:Prod(A,B) to create the assumption z:B(a).  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
  A more natural form of product elimination. *)
9251
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
    47
val prems = Goal "[| p: Prod(A,B);  a: A;  !!z. z: B(a) ==> c(z): C(z) \
9249
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
    48
\    |] ==> c(p`a): C(p`a)";
9251
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
    49
by (REPEAT (resolve_tac (ProdE::prems) 1)) ;
9249
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
    50
qed "subst_prodE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
(** Tactics for type checking **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
9251
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
    54
fun is_rigid_elem (Const("CTT.Elem",_) $ a $ _) = not(is_Var (head_of a))
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
    55
  | is_rigid_elem (Const("CTT.Eqelem",_) $ a $ _ $ _) = not(is_Var (head_of a))
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
    56
  | is_rigid_elem (Const("CTT.Type",_) $ a) = not(is_Var (head_of a))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
  | is_rigid_elem _ = false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
9251
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
    59
(*Try solving a:A or a=b:A by assumption provided a is rigid!*) 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
val test_assume_tac = SUBGOAL(fn (prem,i) =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
    if is_rigid_elem (Logic.strip_assums_concl prem)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
    then  assume_tac i  else  no_tac);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
fun ASSUME tf i = test_assume_tac i  ORELSE  tf i;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
(*For simplification: type formation and checking,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
  but no equalities between terms*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
val routine_rls = form_rls @ formL_rls @ [refl_type] @ element_rls;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
(*Solve all subgoals "A type" using formation rules. *)
9251
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
    75
val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(form_rls) 1));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
(*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
fun typechk_tac thms =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
  let val tac = filt_resolve_tac (thms @ form_rls @ element_rls) 3
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
  in  REPEAT_FIRST (ASSUME tac)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
(*Solve a:A (a flexible, A rigid) by introduction rules. 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
  Cannot use stringtrees (filt_resolve_tac) since
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
  goals like ?a:SUM(A,B) have a trivial head-string *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
fun intr_tac thms =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
  let val tac = filt_resolve_tac(thms@form_rls@intr_rls) 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
  in  REPEAT_FIRST (ASSUME tac)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
(*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
fun equal_tac thms =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
  let val rls = thms @ form_rls @ element_rls @ intrL_rls @
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
                elimL_rls @ [refl_elem]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
  in  REPEAT_FIRST (ASSUME (filt_resolve_tac rls 3))  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
(*** Simplification ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
(*To simplify the type in a goal*)
9251
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
   101
Goal "[| B = A;  a : A |] ==> a : B";
9249
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
   102
by (rtac equal_types 1);
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
   103
by (rtac sym_type 2);
9251
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
   104
by (ALLGOALS assume_tac) ;
9249
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
   105
qed "replace_type";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
(*Simplify the parameter of a unary type operator.*)
9251
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
   108
val prems = Goal
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
   109
     "[| a=c : A;  !!z. z:A ==> B(z) type |] ==> B(a)=B(c)";
9249
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
   110
by (rtac subst_typeL 1);
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
   111
by (rtac refl_type 2);
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
   112
by (ALLGOALS (resolve_tac prems));
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
   113
by (assume_tac 1) ;
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
   114
qed "subst_eqtyparg";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
(*Make a reduction rule for simplification.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
  A goal a=c becomes b=c, by virtue of a=b *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
fun resolve_trans rl = rl RS trans_elem;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
(*Simplification rules for Constructive Type Theory*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
val reduction_rls = map resolve_trans comp_rls;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
(*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
  Uses other intro rules to avoid changing flexible goals.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac(EqI::intr_rls) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
(** Tactics that instantiate CTT-rules.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
    Vars in the given terms will be incremented! 
1459
d12da312eff4 expanded tabs
clasohm
parents: 1294
diff changeset
   129
    The (rtac EqE i) lets them apply to equality judgements. **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
fun NE_tac (sp: string) i = 
1459
d12da312eff4 expanded tabs
clasohm
parents: 1294
diff changeset
   132
  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
fun SumE_tac (sp: string) i = 
1459
d12da312eff4 expanded tabs
clasohm
parents: 1294
diff changeset
   135
  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
fun PlusE_tac (sp: string) i = 
1459
d12da312eff4 expanded tabs
clasohm
parents: 1294
diff changeset
   138
  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
(** Predicate logic reasoning, WITH THINNING!!  Procedures adapted from NJ. **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
(*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
fun add_mp_tac i = 
1459
d12da312eff4 expanded tabs
clasohm
parents: 1294
diff changeset
   144
    rtac subst_prodE i  THEN  assume_tac i  THEN  assume_tac i;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
1459
d12da312eff4 expanded tabs
clasohm
parents: 1294
diff changeset
   147
fun mp_tac i = etac subst_prodE i  THEN  assume_tac i;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
(*"safe" when regarded as predicate calculus rules*)
4440
9ed4098074bc adapted to new sort function;
wenzelm
parents: 3929
diff changeset
   150
val safe_brls = sort (make_ord lessb)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
    [ (true,FE), (true,asm_rl), 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
      (false,ProdI), (true,SumE), (true,PlusE) ];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
val unsafe_brls =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
    [ (false,PlusI_inl), (false,PlusI_inr), (false,SumI), 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
      (true,subst_prodE) ];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
(*0 subgoals vs 1 or more*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
val (safe0_brls, safep_brls) =
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 9251
diff changeset
   160
    List.partition (apl(0,op=) o subgoals_of_brl) safe_brls;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
fun safestep_tac thms i =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
    form_tac  ORELSE  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
    resolve_tac thms i  ORELSE
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
    biresolve_tac safe0_brls i  ORELSE  mp_tac i  ORELSE
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
    DETERM (biresolve_tac safep_brls i);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i); 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
fun step_tac thms = safestep_tac thms  ORELSE'  biresolve_tac unsafe_brls;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
(*Fails unless it solves the goal!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
(** The elimination rules for fst/snd **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
9251
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
   177
Goalw basic_defs "p : Sum(A,B) ==> fst(p) : A";
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
   178
by (etac SumE 1);
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
   179
by (assume_tac 1);
9249
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
   180
qed "SumE_fst";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
(*The first premise must be p:Sum(A,B) !!*)
9251
bd57acd44fc1 more tidying. also generalized some tactics to prove "Type A" and
paulson
parents: 9249
diff changeset
   183
val major::prems= Goalw basic_defs
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
    "[| p: Sum(A,B);  A type;  !!x. x:A ==> B(x) type \
9249
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
   185
\    |] ==> snd(p) : B(fst(p))";
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
   186
by (rtac (major RS SumE) 1);
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
   187
by (resolve_tac [SumC RS subst_eqtyparg RS replace_type] 1);
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
   188
by (typechk_tac prems) ;
c71db8c28727 removed batch proofs
paulson
parents: 4440
diff changeset
   189
qed "SumE_snd";