src/CCL/Term.thy
author haftmann
Fri Jun 19 21:08:07 2009 +0200 (2009-06-19)
changeset 31726 ffd2dc631d88
parent 26480 544cef16045b
child 32010 cb1a1c94b4cd
permissions -rw-r--r--
merged
wenzelm@17456
     1
(*  Title:      CCL/Term.thy
clasohm@0
     2
    ID:         $Id$
clasohm@1474
     3
    Author:     Martin Coen
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
*)
clasohm@0
     6
wenzelm@17456
     7
header {* Definitions of usual program constructs in CCL *}
wenzelm@17456
     8
wenzelm@17456
     9
theory Term
wenzelm@17456
    10
imports CCL
wenzelm@17456
    11
begin
clasohm@0
    12
clasohm@0
    13
consts
clasohm@0
    14
lcp@998
    15
  one        :: "i"
clasohm@0
    16
wenzelm@19796
    17
  "if"       :: "[i,i,i]=>i"           ("(3if _/ then _/ else _)" [0,0,60] 60)
clasohm@0
    18
wenzelm@17456
    19
  inl        :: "i=>i"
wenzelm@17456
    20
  inr        :: "i=>i"
wenzelm@17456
    21
  when       :: "[i,i=>i,i=>i]=>i"
clasohm@0
    22
lcp@998
    23
  split      :: "[i,[i,i]=>i]=>i"
wenzelm@17456
    24
  fst        :: "i=>i"
wenzelm@17456
    25
  snd        :: "i=>i"
lcp@998
    26
  thd        :: "i=>i"
clasohm@0
    27
lcp@998
    28
  zero       :: "i"
lcp@998
    29
  succ       :: "i=>i"
lcp@998
    30
  ncase      :: "[i,i,i=>i]=>i"
lcp@998
    31
  nrec       :: "[i,i,[i,i]=>i]=>i"
clasohm@0
    32
lcp@998
    33
  nil        :: "i"                        ("([])")
wenzelm@24825
    34
  cons       :: "[i,i]=>i"                 (infixr "$" 80)
lcp@998
    35
  lcase      :: "[i,i,[i,i]=>i]=>i"
lcp@998
    36
  lrec       :: "[i,i,[i,i,i]=>i]=>i"
lcp@998
    37
wenzelm@17456
    38
  "let"      :: "[i,i=>i]=>i"
lcp@998
    39
  letrec     :: "[[i,i=>i]=>i,(i=>i)=>i]=>i"
lcp@998
    40
  letrec2    :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i"
wenzelm@17456
    41
  letrec3    :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"
clasohm@0
    42
wenzelm@14765
    43
syntax
lcp@998
    44
  "@let"     :: "[idt,i,i]=>i"             ("(3let _ be _/ in _)"
clasohm@1474
    45
                        [0,0,60] 60)
lcp@998
    46
lcp@998
    47
  "@letrec"  :: "[idt,idt,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
clasohm@1474
    48
                        [0,0,0,60] 60)
clasohm@0
    49
lcp@998
    50
  "@letrec2" :: "[idt,idt,idt,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
clasohm@1474
    51
                        [0,0,0,0,60] 60)
clasohm@0
    52
lcp@998
    53
  "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
clasohm@1474
    54
                        [0,0,0,0,0,60] 60)
lcp@998
    55
wenzelm@17456
    56
ML {*
clasohm@0
    57
(** Quantifier translations: variable binding **)
clasohm@0
    58
wenzelm@17781
    59
(* FIXME does not handle "_idtdummy" *)
wenzelm@2709
    60
(* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *)
wenzelm@2709
    61
clasohm@0
    62
fun let_tr [Free(id,T),a,b] = Const("let",dummyT) $ a $ absfree(id,T,b);
clasohm@0
    63
fun let_tr' [a,Abs(id,T,b)] =
clasohm@0
    64
     let val (id',b') = variant_abs(id,T,b)
clasohm@0
    65
     in Const("@let",dummyT) $ Free(id',T) $ a $ b' end;
clasohm@0
    66
wenzelm@17456
    67
fun letrec_tr [Free(f,S),Free(x,T),a,b] =
clasohm@0
    68
      Const("letrec",dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b);
wenzelm@17456
    69
fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] =
clasohm@0
    70
      Const("letrec2",dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b);
wenzelm@17456
    71
fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] =
clasohm@0
    72
      Const("letrec3",dummyT) $ absfree(x,T,absfree(y,U,absfree(z,U,absfree(f,S,a)))) $ absfree(f,S,b);
clasohm@0
    73
clasohm@0
    74
fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
clasohm@0
    75
     let val (f',b')  = variant_abs(ff,SS,b)
clasohm@0
    76
         val (_,a'') = variant_abs(f,S,a)
clasohm@0
    77
         val (x',a')  = variant_abs(x,T,a'')
clasohm@0
    78
     in Const("@letrec",dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
clasohm@0
    79
fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
clasohm@0
    80
     let val (f',b') = variant_abs(ff,SS,b)
clasohm@0
    81
         val ( _,a1) = variant_abs(f,S,a)
clasohm@0
    82
         val (y',a2) = variant_abs(y,U,a1)
clasohm@0
    83
         val (x',a') = variant_abs(x,T,a2)
clasohm@0
    84
     in Const("@letrec2",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
clasohm@0
    85
      end;
clasohm@0
    86
fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
clasohm@0
    87
     let val (f',b') = variant_abs(ff,SS,b)
clasohm@0
    88
         val ( _,a1) = variant_abs(f,S,a)
clasohm@0
    89
         val (z',a2) = variant_abs(z,V,a1)
clasohm@0
    90
         val (y',a3) = variant_abs(y,U,a2)
clasohm@0
    91
         val (x',a') = variant_abs(x,T,a3)
clasohm@0
    92
     in Const("@letrec3",dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
clasohm@0
    93
      end;
clasohm@0
    94
wenzelm@17456
    95
*}
wenzelm@17456
    96
wenzelm@17456
    97
parse_translation {*
wenzelm@17456
    98
  [("@let",       let_tr),
wenzelm@17456
    99
   ("@letrec",    letrec_tr),
wenzelm@17456
   100
   ("@letrec2",   letrec2_tr),
wenzelm@17456
   101
   ("@letrec3",   letrec3_tr)] *}
wenzelm@17456
   102
wenzelm@17456
   103
print_translation {*
wenzelm@17456
   104
  [("let",       let_tr'),
wenzelm@17456
   105
   ("letrec",    letrec_tr'),
wenzelm@17456
   106
   ("letrec2",   letrec2_tr'),
wenzelm@17456
   107
   ("letrec3",   letrec3_tr')] *}
wenzelm@17456
   108
wenzelm@17456
   109
consts
wenzelm@17456
   110
  napply     :: "[i=>i,i,i]=>i"            ("(_ ^ _ ` _)" [56,56,56] 56)
wenzelm@17456
   111
wenzelm@17456
   112
axioms
wenzelm@17456
   113
wenzelm@17456
   114
  one_def:                    "one == true"
wenzelm@17456
   115
  if_def:     "if b then t else u  == case(b,t,u,% x y. bot,%v. bot)"
wenzelm@17456
   116
  inl_def:                 "inl(a) == <true,a>"
wenzelm@17456
   117
  inr_def:                 "inr(b) == <false,b>"
wenzelm@17456
   118
  when_def:           "when(t,f,g) == split(t,%b x. if b then f(x) else g(x))"
wenzelm@17456
   119
  split_def:           "split(t,f) == case(t,bot,bot,f,%u. bot)"
wenzelm@17456
   120
  fst_def:                 "fst(t) == split(t,%x y. x)"
wenzelm@17456
   121
  snd_def:                 "snd(t) == split(t,%x y. y)"
wenzelm@17456
   122
  thd_def:                 "thd(t) == split(t,%x p. split(p,%y z. z))"
wenzelm@17456
   123
  zero_def:                  "zero == inl(one)"
wenzelm@17456
   124
  succ_def:               "succ(n) == inr(n)"
wenzelm@17456
   125
  ncase_def:         "ncase(n,b,c) == when(n,%x. b,%y. c(y))"
wenzelm@17456
   126
  nrec_def:          " nrec(n,b,c) == letrec g x be ncase(x,b,%y. c(y,g(y))) in g(n)"
wenzelm@17456
   127
  nil_def:                     "[] == inl(one)"
wenzelm@17456
   128
  cons_def:                   "h$t == inr(<h,t>)"
wenzelm@17456
   129
  lcase_def:         "lcase(l,b,c) == when(l,%x. b,%y. split(y,c))"
wenzelm@17456
   130
  lrec_def:           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t. c(h,t,g(t))) in g(l)"
wenzelm@17456
   131
wenzelm@17456
   132
  let_def:  "let x be t in f(x) == case(t,f(true),f(false),%x y. f(<x,y>),%u. f(lam x. u(x)))"
wenzelm@17456
   133
  letrec_def:
wenzelm@17456
   134
  "letrec g x be h(x,g) in b(g) == b(%x. fix(%f. lam x. h(x,%y. f`y))`x)"
wenzelm@17456
   135
wenzelm@17456
   136
  letrec2_def:  "letrec g x y be h(x,y,g) in f(g)==
wenzelm@17456
   137
               letrec g' p be split(p,%x y. h(x,y,%u v. g'(<u,v>)))
wenzelm@17456
   138
                          in f(%x y. g'(<x,y>))"
wenzelm@17456
   139
wenzelm@17456
   140
  letrec3_def:  "letrec g x y z be h(x,y,z,g) in f(g) ==
wenzelm@17456
   141
             letrec g' p be split(p,%x xs. split(xs,%y z. h(x,y,z,%u v w. g'(<u,<v,w>>))))
wenzelm@17456
   142
                          in f(%x y z. g'(<x,<y,z>>))"
wenzelm@17456
   143
wenzelm@17456
   144
  napply_def: "f ^n` a == nrec(n,a,%x g. f(g))"
wenzelm@17456
   145
wenzelm@20140
   146
wenzelm@20140
   147
lemmas simp_can_defs = one_def inl_def inr_def
wenzelm@20140
   148
  and simp_ncan_defs = if_def when_def split_def fst_def snd_def thd_def
wenzelm@20140
   149
lemmas simp_defs = simp_can_defs simp_ncan_defs
wenzelm@20140
   150
wenzelm@20140
   151
lemmas ind_can_defs = zero_def succ_def nil_def cons_def
wenzelm@20140
   152
  and ind_ncan_defs = ncase_def nrec_def lcase_def lrec_def
wenzelm@20140
   153
lemmas ind_defs = ind_can_defs ind_ncan_defs
wenzelm@20140
   154
wenzelm@20140
   155
lemmas data_defs = simp_defs ind_defs napply_def
wenzelm@20140
   156
  and genrec_defs = letrec_def letrec2_def letrec3_def
wenzelm@20140
   157
wenzelm@20140
   158
wenzelm@20140
   159
subsection {* Beta Rules, including strictness *}
wenzelm@20140
   160
wenzelm@20140
   161
lemma letB: "~ t=bot ==> let x be t in f(x) = f(t)"
wenzelm@20140
   162
  apply (unfold let_def)
wenzelm@20140
   163
  apply (erule rev_mp)
wenzelm@20140
   164
  apply (rule_tac t = "t" in term_case)
wenzelm@20140
   165
      apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam)
wenzelm@20140
   166
  done
wenzelm@20140
   167
wenzelm@20140
   168
lemma letBabot: "let x be bot in f(x) = bot"
wenzelm@20140
   169
  apply (unfold let_def)
wenzelm@20140
   170
  apply (rule caseBbot)
wenzelm@20140
   171
  done
wenzelm@20140
   172
wenzelm@20140
   173
lemma letBbbot: "let x be t in bot = bot"
wenzelm@20140
   174
  apply (unfold let_def)
wenzelm@20140
   175
  apply (rule_tac t = t in term_case)
wenzelm@20140
   176
      apply (rule caseBbot)
wenzelm@20140
   177
     apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam)
wenzelm@20140
   178
  done
wenzelm@20140
   179
wenzelm@20140
   180
lemma applyB: "(lam x. b(x)) ` a = b(a)"
wenzelm@20140
   181
  apply (unfold apply_def)
wenzelm@20140
   182
  apply (simp add: caseBtrue caseBfalse caseBpair caseBlam)
wenzelm@20140
   183
  done
wenzelm@20140
   184
wenzelm@20140
   185
lemma applyBbot: "bot ` a = bot"
wenzelm@20140
   186
  apply (unfold apply_def)
wenzelm@20140
   187
  apply (rule caseBbot)
wenzelm@20140
   188
  done
wenzelm@20140
   189
wenzelm@20140
   190
lemma fixB: "fix(f) = f(fix(f))"
wenzelm@20140
   191
  apply (unfold fix_def)
wenzelm@20140
   192
  apply (rule applyB [THEN ssubst], rule refl)
wenzelm@20140
   193
  done
wenzelm@20140
   194
wenzelm@20140
   195
lemma letrecB:
wenzelm@20140
   196
    "letrec g x be h(x,g) in g(a) = h(a,%y. letrec g x be h(x,g) in g(y))"
wenzelm@20140
   197
  apply (unfold letrec_def)
wenzelm@20140
   198
  apply (rule fixB [THEN ssubst], rule applyB [THEN ssubst], rule refl)
wenzelm@20140
   199
  done
wenzelm@20140
   200
wenzelm@20140
   201
lemmas rawBs = caseBs applyB applyBbot
wenzelm@20140
   202
wenzelm@20140
   203
ML {*
wenzelm@20140
   204
local
wenzelm@20140
   205
  val letrecB = thm "letrecB"
wenzelm@20140
   206
  val rawBs = thms "rawBs"
wenzelm@20140
   207
  val data_defs = thms "data_defs"
wenzelm@20140
   208
in
wenzelm@20140
   209
wenzelm@20140
   210
fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s
wenzelm@20140
   211
           (fn _ => [stac letrecB 1,
wenzelm@26342
   212
                     simp_tac (@{simpset} addsimps rawBs) 1]);
wenzelm@20140
   213
fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
wenzelm@20140
   214
wenzelm@20140
   215
fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s
wenzelm@26342
   216
           (fn _ => [simp_tac (@{simpset} addsimps rawBs
wenzelm@20140
   217
                               setloop (stac letrecB)) 1]);
wenzelm@20140
   218
fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
wenzelm@17456
   219
wenzelm@17456
   220
end
wenzelm@20140
   221
*}
wenzelm@20140
   222
wenzelm@26480
   223
ML {*
wenzelm@20140
   224
bind_thm ("ifBtrue", mk_beta_rl "if true then t else u = t");
wenzelm@20140
   225
bind_thm ("ifBfalse", mk_beta_rl "if false then t else u = u");
wenzelm@20140
   226
bind_thm ("ifBbot", mk_beta_rl "if bot then t else u = bot");
wenzelm@20140
   227
wenzelm@20140
   228
bind_thm ("whenBinl", mk_beta_rl "when(inl(a),t,u) = t(a)");
wenzelm@20140
   229
bind_thm ("whenBinr", mk_beta_rl "when(inr(a),t,u) = u(a)");
wenzelm@20140
   230
bind_thm ("whenBbot", mk_beta_rl "when(bot,t,u) = bot");
wenzelm@20140
   231
wenzelm@20140
   232
bind_thm ("splitB", mk_beta_rl "split(<a,b>,h) = h(a,b)");
wenzelm@20140
   233
bind_thm ("splitBbot", mk_beta_rl "split(bot,h) = bot");
wenzelm@20140
   234
bind_thm ("fstB", mk_beta_rl "fst(<a,b>) = a");
wenzelm@20140
   235
bind_thm ("fstBbot", mk_beta_rl "fst(bot) = bot");
wenzelm@20140
   236
bind_thm ("sndB", mk_beta_rl "snd(<a,b>) = b");
wenzelm@20140
   237
bind_thm ("sndBbot", mk_beta_rl "snd(bot) = bot");
wenzelm@20140
   238
bind_thm ("thdB", mk_beta_rl "thd(<a,<b,c>>) = c");
wenzelm@20140
   239
bind_thm ("thdBbot", mk_beta_rl "thd(bot) = bot");
wenzelm@20140
   240
wenzelm@20140
   241
bind_thm ("ncaseBzero", mk_beta_rl "ncase(zero,t,u) = t");
wenzelm@20140
   242
bind_thm ("ncaseBsucc", mk_beta_rl "ncase(succ(n),t,u) = u(n)");
wenzelm@20140
   243
bind_thm ("ncaseBbot", mk_beta_rl "ncase(bot,t,u) = bot");
wenzelm@20140
   244
bind_thm ("nrecBzero", mk_beta_rl "nrec(zero,t,u) = t");
wenzelm@20140
   245
bind_thm ("nrecBsucc", mk_beta_rl "nrec(succ(n),t,u) = u(n,nrec(n,t,u))");
wenzelm@20140
   246
bind_thm ("nrecBbot", mk_beta_rl "nrec(bot,t,u) = bot");
wenzelm@20140
   247
wenzelm@20140
   248
bind_thm ("lcaseBnil", mk_beta_rl "lcase([],t,u) = t");
wenzelm@20140
   249
bind_thm ("lcaseBcons", mk_beta_rl "lcase(x$xs,t,u) = u(x,xs)");
wenzelm@20140
   250
bind_thm ("lcaseBbot", mk_beta_rl "lcase(bot,t,u) = bot");
wenzelm@20140
   251
bind_thm ("lrecBnil", mk_beta_rl "lrec([],t,u) = t");
wenzelm@20140
   252
bind_thm ("lrecBcons", mk_beta_rl "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))");
wenzelm@20140
   253
bind_thm ("lrecBbot", mk_beta_rl "lrec(bot,t,u) = bot");
wenzelm@20140
   254
wenzelm@20140
   255
bind_thm ("letrec2B", raw_mk_beta_rl (thms "data_defs" @ [thm "letrec2_def"])
wenzelm@20140
   256
  "letrec g x y be h(x,y,g) in g(p,q) = h(p,q,%u v. letrec g x y be h(x,y,g) in g(u,v))");
wenzelm@20140
   257
wenzelm@20140
   258
bind_thm ("letrec3B", raw_mk_beta_rl (thms "data_defs" @ [thm "letrec3_def"])
wenzelm@20140
   259
  "letrec g x y z be h(x,y,z,g) in g(p,q,r) = h(p,q,r,%u v w. letrec g x y z be h(x,y,z,g) in g(u,v,w))");
wenzelm@20140
   260
wenzelm@20140
   261
bind_thm ("napplyBzero", mk_beta_rl "f^zero`a = a");
wenzelm@20140
   262
bind_thm ("napplyBsucc", mk_beta_rl "f^succ(n)`a = f(f^n`a)");
wenzelm@20140
   263
wenzelm@20140
   264
bind_thms ("termBs", [thm "letB", thm "applyB", thm "applyBbot", splitB,splitBbot,
wenzelm@20140
   265
  fstB,fstBbot,sndB,sndBbot,thdB,thdBbot,
wenzelm@20140
   266
  ifBtrue,ifBfalse,ifBbot,whenBinl,whenBinr,whenBbot,
wenzelm@20140
   267
  ncaseBzero,ncaseBsucc,ncaseBbot,nrecBzero,nrecBsucc,nrecBbot,
wenzelm@20140
   268
  lcaseBnil,lcaseBcons,lcaseBbot,lrecBnil,lrecBcons,lrecBbot,
wenzelm@20140
   269
  napplyBzero,napplyBsucc]);
wenzelm@20140
   270
*}
wenzelm@20140
   271
wenzelm@20140
   272
wenzelm@20140
   273
subsection {* Constructors are injective *}
wenzelm@20140
   274
wenzelm@26480
   275
ML {*
wenzelm@20140
   276
wenzelm@20140
   277
bind_thms ("term_injs", map (mk_inj_rl (the_context ())
wenzelm@20140
   278
  [thm "applyB", thm "splitB", thm "whenBinl", thm "whenBinr", thm "ncaseBsucc", thm "lcaseBcons"])
wenzelm@20140
   279
    ["(inl(a) = inl(a')) <-> (a=a')",
wenzelm@20140
   280
     "(inr(a) = inr(a')) <-> (a=a')",
wenzelm@20140
   281
     "(succ(a) = succ(a')) <-> (a=a')",
wenzelm@20140
   282
     "(a$b = a'$b') <-> (a=a' & b=b')"])
wenzelm@20140
   283
*}
wenzelm@20140
   284
wenzelm@20140
   285
wenzelm@20140
   286
subsection {* Constructors are distinct *}
wenzelm@20140
   287
wenzelm@26480
   288
ML {*
wenzelm@20140
   289
bind_thms ("term_dstncts",
wenzelm@20140
   290
  mkall_dstnct_thms (the_context ()) (thms "data_defs") (thms "ccl_injs" @ thms "term_injs")
wenzelm@24825
   291
    [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
wenzelm@20140
   292
*}
wenzelm@20140
   293
wenzelm@20140
   294
wenzelm@20140
   295
subsection {* Rules for pre-order @{text "[="} *}
wenzelm@20140
   296
wenzelm@26480
   297
ML {*
wenzelm@20140
   298
wenzelm@20140
   299
local
wenzelm@20140
   300
  fun mk_thm s = prove_goalw (the_context ()) (thms "data_defs") s (fn _ =>
wenzelm@26342
   301
    [simp_tac (@{simpset} addsimps (thms "ccl_porews")) 1])
wenzelm@20140
   302
in
wenzelm@20140
   303
  val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
wenzelm@20140
   304
                                "inr(b) [= inr(b') <-> b [= b'",
wenzelm@20140
   305
                                "succ(n) [= succ(n') <-> n [= n'",
wenzelm@20140
   306
                                "x$xs [= x'$xs' <-> x [= x'  & xs [= xs'"]
wenzelm@20140
   307
end;
wenzelm@20140
   308
wenzelm@20140
   309
bind_thms ("term_porews", term_porews);
wenzelm@20140
   310
*}
wenzelm@20140
   311
wenzelm@20140
   312
subsection {* Rewriting and Proving *}
wenzelm@20140
   313
wenzelm@26480
   314
ML {*
wenzelm@24790
   315
  bind_thms ("term_injDs", XH_to_Ds @{thms term_injs});
wenzelm@20140
   316
*}
wenzelm@20140
   317
wenzelm@20917
   318
lemmas term_rews = termBs term_injs term_dstncts ccl_porews term_porews
wenzelm@20917
   319
wenzelm@20140
   320
lemmas [simp] = term_rews
wenzelm@20917
   321
lemmas [elim!] = term_dstncts [THEN notE]
wenzelm@20917
   322
lemmas [dest!] = term_injDs
wenzelm@20140
   323
wenzelm@20140
   324
end