src/CCL/Term.thy
author blanchet
Tue, 15 Nov 2011 22:13:39 +0100
changeset 45509 624872fc47bf
parent 44241 7943b69f0188
child 49660 de49d9b4d7bc
permissions -rw-r--r--
use consts, not frees, for lambda-lifting
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
     1
(*  Title:      CCL/Term.thy
1474
3f7d67927fe2 expanded tabs
clasohm
parents: 1149
diff changeset
     2
    Author:     Martin Coen
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
     6
header {* Definitions of usual program constructs in CCL *}
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
     7
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
     8
theory Term
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
     9
imports CCL
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    10
begin
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
consts
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    14
  one        :: "i"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
19796
d86e7b1fc472 quoted "if";
wenzelm
parents: 17781
diff changeset
    16
  "if"       :: "[i,i,i]=>i"           ("(3if _/ then _/ else _)" [0,0,60] 60)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    18
  inl        :: "i=>i"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    19
  inr        :: "i=>i"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    20
  when       :: "[i,i=>i,i=>i]=>i"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    22
  split      :: "[i,[i,i]=>i]=>i"
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    23
  fst        :: "i=>i"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    24
  snd        :: "i=>i"
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    25
  thd        :: "i=>i"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    27
  zero       :: "i"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    28
  succ       :: "i=>i"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    29
  ncase      :: "[i,i,i=>i]=>i"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    30
  nrec       :: "[i,i,[i,i]=>i]=>i"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    32
  nil        :: "i"                        ("([])")
24825
c4f13ab78f9d avoid unnamed infixes;
wenzelm
parents: 24790
diff changeset
    33
  cons       :: "[i,i]=>i"                 (infixr "$" 80)
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    34
  lcase      :: "[i,i,[i,i]=>i]=>i"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    35
  lrec       :: "[i,i,[i,i,i]=>i]=>i"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    36
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    37
  "let"      :: "[i,i=>i]=>i"
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    38
  letrec     :: "[[i,i=>i]=>i,(i=>i)=>i]=>i"
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    39
  letrec2    :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i"
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    40
  letrec3    :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
14765
bafb24c150c1 proper use of 'syntax';
wenzelm
parents: 3837
diff changeset
    42
syntax
42051
dbdd4790da34 let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
wenzelm
parents: 35113
diff changeset
    43
  "_let"     :: "[id,i,i]=>i"             ("(3let _ be _/ in _)"
1474
3f7d67927fe2 expanded tabs
clasohm
parents: 1149
diff changeset
    44
                        [0,0,60] 60)
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    45
42051
dbdd4790da34 let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
wenzelm
parents: 35113
diff changeset
    46
  "_letrec"  :: "[id,id,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
1474
3f7d67927fe2 expanded tabs
clasohm
parents: 1149
diff changeset
    47
                        [0,0,0,60] 60)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
42051
dbdd4790da34 let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
wenzelm
parents: 35113
diff changeset
    49
  "_letrec2" :: "[id,id,id,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
1474
3f7d67927fe2 expanded tabs
clasohm
parents: 1149
diff changeset
    50
                        [0,0,0,0,60] 60)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
42051
dbdd4790da34 let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);
wenzelm
parents: 35113
diff changeset
    52
  "_letrec3" :: "[id,id,id,id,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
1474
3f7d67927fe2 expanded tabs
clasohm
parents: 1149
diff changeset
    53
                        [0,0,0,0,0,60] 60)
998
91d09e262799 Gave tighter priorities to if, napply and the let-forms to
lcp
parents: 610
diff changeset
    54
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    55
ML {*
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
(** Quantifier translations: variable binding **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
17781
32bb237158a5 print_translation: does not handle _idtdummy;
wenzelm
parents: 17456
diff changeset
    58
(* FIXME does not handle "_idtdummy" *)
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42156
diff changeset
    59
(* FIXME should use Syntax_Trans.mark_bound(T), Syntax_Trans.variant_abs' *)
2709
241fffc25284 added comment;
wenzelm
parents: 1474
diff changeset
    60
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 42814
diff changeset
    61
fun let_tr [Free x, a, b] = Const(@{const_syntax let},dummyT) $ a $ absfree x b;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
fun let_tr' [a,Abs(id,T,b)] =
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42156
diff changeset
    63
     let val (id',b') = Syntax_Trans.variant_abs(id,T,b)
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 32154
diff changeset
    64
     in Const(@{syntax_const "_let"},dummyT) $ Free(id',T) $ a $ b' end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 42814
diff changeset
    66
fun letrec_tr [Free f, Free x, a, b] =
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 42814
diff changeset
    67
      Const(@{const_syntax letrec}, dummyT) $ absfree x (absfree f a) $ absfree f b;
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 42814
diff changeset
    68
fun letrec2_tr [Free f, Free x, Free y, a, b] =
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 42814
diff changeset
    69
      Const(@{const_syntax letrec2}, dummyT) $ absfree x (absfree y (absfree f a)) $ absfree f b;
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 42814
diff changeset
    70
fun letrec3_tr [Free f, Free x, Free y, Free z, a, b] =
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 42814
diff changeset
    71
      Const(@{const_syntax letrec3}, dummyT) $
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 42814
diff changeset
    72
        absfree x (absfree y (absfree z (absfree f a))) $ absfree f b;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42156
diff changeset
    75
     let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42156
diff changeset
    76
         val (_,a'') = Syntax_Trans.variant_abs(f,S,a)
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42156
diff changeset
    77
         val (x',a') = Syntax_Trans.variant_abs(x,T,a'')
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 32154
diff changeset
    78
     in Const(@{syntax_const "_letrec"},dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42156
diff changeset
    80
     let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42156
diff changeset
    81
         val ( _,a1) = Syntax_Trans.variant_abs(f,S,a)
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42156
diff changeset
    82
         val (y',a2) = Syntax_Trans.variant_abs(y,U,a1)
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42156
diff changeset
    83
         val (x',a') = Syntax_Trans.variant_abs(x,T,a2)
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 32154
diff changeset
    84
     in Const(@{syntax_const "_letrec2"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
      end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42156
diff changeset
    87
     let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42156
diff changeset
    88
         val ( _,a1) = Syntax_Trans.variant_abs(f,S,a)
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42156
diff changeset
    89
         val (z',a2) = Syntax_Trans.variant_abs(z,V,a1)
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42156
diff changeset
    90
         val (y',a3) = Syntax_Trans.variant_abs(y,U,a2)
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42156
diff changeset
    91
         val (x',a') = Syntax_Trans.variant_abs(x,T,a3)
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 32154
diff changeset
    92
     in Const(@{syntax_const "_letrec3"},dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
      end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    95
*}
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    96
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
    97
parse_translation {*
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 32154
diff changeset
    98
 [(@{syntax_const "_let"}, let_tr),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 32154
diff changeset
    99
  (@{syntax_const "_letrec"}, letrec_tr),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 32154
diff changeset
   100
  (@{syntax_const "_letrec2"}, letrec2_tr),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 32154
diff changeset
   101
  (@{syntax_const "_letrec3"}, letrec3_tr)]
1a0c129bb2e0 modernized translations;
wenzelm
parents: 32154
diff changeset
   102
*}
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   103
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   104
print_translation {*
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 32154
diff changeset
   105
 [(@{const_syntax let}, let_tr'),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 32154
diff changeset
   106
  (@{const_syntax letrec}, letrec_tr'),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 32154
diff changeset
   107
  (@{const_syntax letrec2}, letrec2_tr'),
1a0c129bb2e0 modernized translations;
wenzelm
parents: 32154
diff changeset
   108
  (@{const_syntax letrec3}, letrec3_tr')]
1a0c129bb2e0 modernized translations;
wenzelm
parents: 32154
diff changeset
   109
*}
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   110
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   111
consts
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   112
  napply     :: "[i=>i,i,i]=>i"            ("(_ ^ _ ` _)" [56,56,56] 56)
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   113
42156
df219e736a5d modernized specifications -- less axioms;
wenzelm
parents: 42051
diff changeset
   114
defs
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   115
  one_def:                    "one == true"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   116
  if_def:     "if b then t else u  == case(b,t,u,% x y. bot,%v. bot)"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   117
  inl_def:                 "inl(a) == <true,a>"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   118
  inr_def:                 "inr(b) == <false,b>"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   119
  when_def:           "when(t,f,g) == split(t,%b x. if b then f(x) else g(x))"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   120
  split_def:           "split(t,f) == case(t,bot,bot,f,%u. bot)"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   121
  fst_def:                 "fst(t) == split(t,%x y. x)"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   122
  snd_def:                 "snd(t) == split(t,%x y. y)"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   123
  thd_def:                 "thd(t) == split(t,%x p. split(p,%y z. z))"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   124
  zero_def:                  "zero == inl(one)"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   125
  succ_def:               "succ(n) == inr(n)"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   126
  ncase_def:         "ncase(n,b,c) == when(n,%x. b,%y. c(y))"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   127
  nrec_def:          " nrec(n,b,c) == letrec g x be ncase(x,b,%y. c(y,g(y))) in g(n)"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   128
  nil_def:                     "[] == inl(one)"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   129
  cons_def:                   "h$t == inr(<h,t>)"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   130
  lcase_def:         "lcase(l,b,c) == when(l,%x. b,%y. split(y,c))"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   131
  lrec_def:           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t. c(h,t,g(t))) in g(l)"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   132
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   133
  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)))"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   134
  letrec_def:
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   135
  "letrec g x be h(x,g) in b(g) == b(%x. fix(%f. lam x. h(x,%y. f`y))`x)"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   136
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   137
  letrec2_def:  "letrec g x y be h(x,y,g) in f(g)==
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   138
               letrec g' p be split(p,%x y. h(x,y,%u v. g'(<u,v>)))
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   139
                          in f(%x y. g'(<x,y>))"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   140
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   141
  letrec3_def:  "letrec g x y z be h(x,y,z,g) in f(g) ==
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   142
             letrec g' p be split(p,%x xs. split(xs,%y z. h(x,y,z,%u v w. g'(<u,<v,w>>))))
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   143
                          in f(%x y z. g'(<x,<y,z>>))"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   144
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   145
  napply_def: "f ^n` a == nrec(n,a,%x g. f(g))"
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   146
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   147
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   148
lemmas simp_can_defs = one_def inl_def inr_def
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   149
  and simp_ncan_defs = if_def when_def split_def fst_def snd_def thd_def
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   150
lemmas simp_defs = simp_can_defs simp_ncan_defs
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   151
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   152
lemmas ind_can_defs = zero_def succ_def nil_def cons_def
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   153
  and ind_ncan_defs = ncase_def nrec_def lcase_def lrec_def
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   154
lemmas ind_defs = ind_can_defs ind_ncan_defs
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   155
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   156
lemmas data_defs = simp_defs ind_defs napply_def
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   157
  and genrec_defs = letrec_def letrec2_def letrec3_def
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   158
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   159
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   160
subsection {* Beta Rules, including strictness *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   161
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   162
lemma letB: "~ t=bot ==> let x be t in f(x) = f(t)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   163
  apply (unfold let_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   164
  apply (erule rev_mp)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   165
  apply (rule_tac t = "t" in term_case)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   166
      apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   167
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   168
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   169
lemma letBabot: "let x be bot in f(x) = bot"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   170
  apply (unfold let_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   171
  apply (rule caseBbot)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   172
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   173
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   174
lemma letBbbot: "let x be t in bot = bot"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   175
  apply (unfold let_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   176
  apply (rule_tac t = t in term_case)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   177
      apply (rule caseBbot)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   178
     apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   179
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   180
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   181
lemma applyB: "(lam x. b(x)) ` a = b(a)"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   182
  apply (unfold apply_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   183
  apply (simp add: caseBtrue caseBfalse caseBpair caseBlam)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   184
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   185
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   186
lemma applyBbot: "bot ` a = bot"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   187
  apply (unfold apply_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   188
  apply (rule caseBbot)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   189
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   190
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   191
lemma fixB: "fix(f) = f(fix(f))"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   192
  apply (unfold fix_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   193
  apply (rule applyB [THEN ssubst], rule refl)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   194
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   195
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   196
lemma letrecB:
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   197
    "letrec g x be h(x,g) in g(a) = h(a,%y. letrec g x be h(x,g) in g(y))"
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   198
  apply (unfold letrec_def)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   199
  apply (rule fixB [THEN ssubst], rule applyB [THEN ssubst], rule refl)
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   200
  done
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   201
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   202
lemmas rawBs = caseBs applyB applyBbot
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   203
32153
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   204
method_setup beta_rl = {*
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   205
  Scan.succeed (fn ctxt =>
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   206
    SIMPLE_METHOD' (CHANGED o
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   207
      simp_tac (simpset_of ctxt addsimps @{thms rawBs} setloop (stac @{thm letrecB}))))
42814
5af15f1e2ef6 simplified/unified method_setup/attribute_setup;
wenzelm
parents: 42284
diff changeset
   208
*}
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   209
32153
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   210
lemma ifBtrue: "if true then t else u = t"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   211
  and ifBfalse: "if false then t else u = u"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   212
  and ifBbot: "if bot then t else u = bot"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   213
  unfolding data_defs by beta_rl+
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   214
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   215
lemma whenBinl: "when(inl(a),t,u) = t(a)"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   216
  and whenBinr: "when(inr(a),t,u) = u(a)"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   217
  and whenBbot: "when(bot,t,u) = bot"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   218
  unfolding data_defs by beta_rl+
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   219
32153
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   220
lemma splitB: "split(<a,b>,h) = h(a,b)"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   221
  and splitBbot: "split(bot,h) = bot"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   222
  unfolding data_defs by beta_rl+
17456
bcf7544875b2 converted to Isar theory format;
wenzelm
parents: 14765
diff changeset
   223
32153
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   224
lemma fstB: "fst(<a,b>) = a"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   225
  and fstBbot: "fst(bot) = bot"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   226
  unfolding data_defs by beta_rl+
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   227
32153
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   228
lemma sndB: "snd(<a,b>) = b"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   229
  and sndBbot: "snd(bot) = bot"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   230
  unfolding data_defs by beta_rl+
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   231
32153
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   232
lemma thdB: "thd(<a,<b,c>>) = c"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   233
  and thdBbot: "thd(bot) = bot"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   234
  unfolding data_defs by beta_rl+
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   235
32153
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   236
lemma ncaseBzero: "ncase(zero,t,u) = t"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   237
  and ncaseBsucc: "ncase(succ(n),t,u) = u(n)"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   238
  and ncaseBbot: "ncase(bot,t,u) = bot"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   239
  unfolding data_defs by beta_rl+
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   240
32153
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   241
lemma nrecBzero: "nrec(zero,t,u) = t"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   242
  and nrecBsucc: "nrec(succ(n),t,u) = u(n,nrec(n,t,u))"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   243
  and nrecBbot: "nrec(bot,t,u) = bot"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   244
  unfolding data_defs by beta_rl+
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   245
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   246
lemma lcaseBnil: "lcase([],t,u) = t"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   247
  and lcaseBcons: "lcase(x$xs,t,u) = u(x,xs)"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   248
  and lcaseBbot: "lcase(bot,t,u) = bot"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   249
  unfolding data_defs by beta_rl+
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   250
32153
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   251
lemma lrecBnil: "lrec([],t,u) = t"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   252
  and lrecBcons: "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   253
  and lrecBbot: "lrec(bot,t,u) = bot"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   254
  unfolding data_defs by beta_rl+
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   255
32153
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   256
lemma letrec2B:
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   257
  "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))"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   258
  unfolding data_defs letrec2_def by beta_rl+
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   259
32153
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   260
lemma letrec3B:
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   261
  "letrec g x y z be h(x,y,z,g) in g(p,q,r) =
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   262
    h(p,q,r,%u v w. letrec g x y z be h(x,y,z,g) in g(u,v,w))"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   263
  unfolding data_defs letrec3_def by beta_rl+
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   264
32153
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   265
lemma napplyBzero: "f^zero`a = a"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   266
  and napplyBsucc: "f^succ(n)`a = f(f^n`a)"
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   267
  unfolding data_defs by beta_rl+
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   268
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   269
lemmas termBs = letB applyB applyBbot splitB splitBbot fstB fstBbot
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   270
  sndB sndBbot thdB thdBbot ifBtrue ifBfalse ifBbot whenBinl whenBinr
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   271
  whenBbot ncaseBzero ncaseBsucc ncaseBbot nrecBzero nrecBsucc
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   272
  nrecBbot lcaseBnil lcaseBcons lcaseBbot lrecBnil lrecBcons lrecBbot
a0e57fb1b930 misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents: 32010
diff changeset
   273
  napplyBzero napplyBsucc
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   274
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   275
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   276
subsection {* Constructors are injective *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   277
32154
9721e8e4d48c eliminated adhoc ML code;
wenzelm
parents: 32153
diff changeset
   278
lemma term_injs:
9721e8e4d48c eliminated adhoc ML code;
wenzelm
parents: 32153
diff changeset
   279
  "(inl(a) = inl(a')) <-> (a=a')"
9721e8e4d48c eliminated adhoc ML code;
wenzelm
parents: 32153
diff changeset
   280
  "(inr(a) = inr(a')) <-> (a=a')"
9721e8e4d48c eliminated adhoc ML code;
wenzelm
parents: 32153
diff changeset
   281
  "(succ(a) = succ(a')) <-> (a=a')"
9721e8e4d48c eliminated adhoc ML code;
wenzelm
parents: 32153
diff changeset
   282
  "(a$b = a'$b') <-> (a=a' & b=b')"
9721e8e4d48c eliminated adhoc ML code;
wenzelm
parents: 32153
diff changeset
   283
  by (inj_rl applyB splitB whenBinl whenBinr ncaseBsucc lcaseBcons)
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   284
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   285
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   286
subsection {* Constructors are distinct *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   287
26480
544cef16045b replaced 'ML_setup' by 'ML';
wenzelm
parents: 26342
diff changeset
   288
ML {*
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   289
bind_thms ("term_dstncts",
32010
cb1a1c94b4cd more antiquotations;
wenzelm
parents: 26480
diff changeset
   290
  mkall_dstnct_thms @{theory} @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs})
24825
c4f13ab78f9d avoid unnamed infixes;
wenzelm
parents: 24790
diff changeset
   291
    [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   292
*}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   293
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   294
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   295
subsection {* Rules for pre-order @{text "[="} *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   296
32154
9721e8e4d48c eliminated adhoc ML code;
wenzelm
parents: 32153
diff changeset
   297
lemma term_porews:
9721e8e4d48c eliminated adhoc ML code;
wenzelm
parents: 32153
diff changeset
   298
  "inl(a) [= inl(a') <-> a [= a'"
9721e8e4d48c eliminated adhoc ML code;
wenzelm
parents: 32153
diff changeset
   299
  "inr(b) [= inr(b') <-> b [= b'"
9721e8e4d48c eliminated adhoc ML code;
wenzelm
parents: 32153
diff changeset
   300
  "succ(n) [= succ(n') <-> n [= n'"
9721e8e4d48c eliminated adhoc ML code;
wenzelm
parents: 32153
diff changeset
   301
  "x$xs [= x'$xs' <-> x [= x'  & xs [= xs'"
9721e8e4d48c eliminated adhoc ML code;
wenzelm
parents: 32153
diff changeset
   302
  by (simp_all add: data_defs ccl_porews)
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   303
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   304
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   305
subsection {* Rewriting and Proving *}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   306
26480
544cef16045b replaced 'ML_setup' by 'ML';
wenzelm
parents: 26342
diff changeset
   307
ML {*
24790
3be1580de4cc ML_setup for bind_thms;
wenzelm
parents: 20917
diff changeset
   308
  bind_thms ("term_injDs", XH_to_Ds @{thms term_injs});
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   309
*}
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   310
20917
803c94363ccc reorderd ML/lemmas (Why!?);
wenzelm
parents: 20140
diff changeset
   311
lemmas term_rews = termBs term_injs term_dstncts ccl_porews term_porews
803c94363ccc reorderd ML/lemmas (Why!?);
wenzelm
parents: 20140
diff changeset
   312
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   313
lemmas [simp] = term_rews
20917
803c94363ccc reorderd ML/lemmas (Why!?);
wenzelm
parents: 20140
diff changeset
   314
lemmas [elim!] = term_dstncts [THEN notE]
803c94363ccc reorderd ML/lemmas (Why!?);
wenzelm
parents: 20140
diff changeset
   315
lemmas [dest!] = term_injDs
20140
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   316
98acc6d0fab6 removed obsolete ML files;
wenzelm
parents: 19796
diff changeset
   317
end