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