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