src/CCL/Term.thy
author wenzelm
Sat May 15 22:15:57 2010 +0200 (2010-05-15)
changeset 36948 d2cdad45fd14
parent 35113 1a0c129bb2e0
child 42051 dbdd4790da34
permissions -rw-r--r--
renamed Outer_Parse to Parse (in Scala);
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@35113
    43
  "_let"     :: "[idt,i,i]=>i"             ("(3let _ be _/ in _)"
clasohm@1474
    44
                        [0,0,60] 60)
lcp@998
    45
wenzelm@35113
    46
  "_letrec"  :: "[idt,idt,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
clasohm@1474
    47
                        [0,0,0,60] 60)
clasohm@0
    48
wenzelm@35113
    49
  "_letrec2" :: "[idt,idt,idt,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
clasohm@1474
    50
                        [0,0,0,0,60] 60)
clasohm@0
    51
wenzelm@35113
    52
  "_letrec3" :: "[idt,idt,idt,idt,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@2709
    59
(* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *)
wenzelm@2709
    60
wenzelm@35113
    61
fun let_tr [Free(id,T),a,b] = Const(@{const_syntax let},dummyT) $ a $ absfree(id,T,b);
clasohm@0
    62
fun let_tr' [a,Abs(id,T,b)] =
clasohm@0
    63
     let val (id',b') = variant_abs(id,T,b)
wenzelm@35113
    64
     in Const(@{syntax_const "_let"},dummyT) $ Free(id',T) $ a $ b' end;
clasohm@0
    65
wenzelm@17456
    66
fun letrec_tr [Free(f,S),Free(x,T),a,b] =
wenzelm@35113
    67
      Const(@{const_syntax letrec},dummyT) $ absfree(x,T,absfree(f,S,a)) $ absfree(f,S,b);
wenzelm@17456
    68
fun letrec2_tr [Free(f,S),Free(x,T),Free(y,U),a,b] =
wenzelm@35113
    69
      Const(@{const_syntax letrec2},dummyT) $ absfree(x,T,absfree(y,U,absfree(f,S,a))) $ absfree(f,S,b);
wenzelm@17456
    70
fun letrec3_tr [Free(f,S),Free(x,T),Free(y,U),Free(z,V),a,b] =
wenzelm@35113
    71
      Const(@{const_syntax letrec3},dummyT) $
wenzelm@35113
    72
        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'')
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)] =
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)
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)] =
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)
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@35113
    98
 [(@{syntax_const "_let"}, let_tr),
wenzelm@35113
    99
  (@{syntax_const "_letrec"}, letrec_tr),
wenzelm@35113
   100
  (@{syntax_const "_letrec2"}, letrec2_tr),
wenzelm@35113
   101
  (@{syntax_const "_letrec3"}, letrec3_tr)]
wenzelm@35113
   102
*}
wenzelm@17456
   103
wenzelm@17456
   104
print_translation {*
wenzelm@35113
   105
 [(@{const_syntax let}, let_tr'),
wenzelm@35113
   106
  (@{const_syntax letrec}, letrec_tr'),
wenzelm@35113
   107
  (@{const_syntax letrec2}, letrec2_tr'),
wenzelm@35113
   108
  (@{const_syntax letrec3}, 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@17456
   114
axioms
wenzelm@17456
   115
wenzelm@17456
   116
  one_def:                    "one == true"
wenzelm@17456
   117
  if_def:     "if b then t else u  == case(b,t,u,% x y. bot,%v. bot)"
wenzelm@17456
   118
  inl_def:                 "inl(a) == <true,a>"
wenzelm@17456
   119
  inr_def:                 "inr(b) == <false,b>"
wenzelm@17456
   120
  when_def:           "when(t,f,g) == split(t,%b x. if b then f(x) else g(x))"
wenzelm@17456
   121
  split_def:           "split(t,f) == case(t,bot,bot,f,%u. bot)"
wenzelm@17456
   122
  fst_def:                 "fst(t) == split(t,%x y. x)"
wenzelm@17456
   123
  snd_def:                 "snd(t) == split(t,%x y. y)"
wenzelm@17456
   124
  thd_def:                 "thd(t) == split(t,%x p. split(p,%y z. z))"
wenzelm@17456
   125
  zero_def:                  "zero == inl(one)"
wenzelm@17456
   126
  succ_def:               "succ(n) == inr(n)"
wenzelm@17456
   127
  ncase_def:         "ncase(n,b,c) == when(n,%x. b,%y. c(y))"
wenzelm@17456
   128
  nrec_def:          " nrec(n,b,c) == letrec g x be ncase(x,b,%y. c(y,g(y))) in g(n)"
wenzelm@17456
   129
  nil_def:                     "[] == inl(one)"
wenzelm@17456
   130
  cons_def:                   "h$t == inr(<h,t>)"
wenzelm@17456
   131
  lcase_def:         "lcase(l,b,c) == when(l,%x. b,%y. split(y,c))"
wenzelm@17456
   132
  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
   133
wenzelm@17456
   134
  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
   135
  letrec_def:
wenzelm@17456
   136
  "letrec g x be h(x,g) in b(g) == b(%x. fix(%f. lam x. h(x,%y. f`y))`x)"
wenzelm@17456
   137
wenzelm@17456
   138
  letrec2_def:  "letrec g x y be h(x,y,g) in f(g)==
wenzelm@17456
   139
               letrec g' p be split(p,%x y. h(x,y,%u v. g'(<u,v>)))
wenzelm@17456
   140
                          in f(%x y. g'(<x,y>))"
wenzelm@17456
   141
wenzelm@17456
   142
  letrec3_def:  "letrec g x y z be h(x,y,z,g) in f(g) ==
wenzelm@17456
   143
             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
   144
                          in f(%x y z. g'(<x,<y,z>>))"
wenzelm@17456
   145
wenzelm@17456
   146
  napply_def: "f ^n` a == nrec(n,a,%x g. f(g))"
wenzelm@17456
   147
wenzelm@20140
   148
wenzelm@20140
   149
lemmas simp_can_defs = one_def inl_def inr_def
wenzelm@20140
   150
  and simp_ncan_defs = if_def when_def split_def fst_def snd_def thd_def
wenzelm@20140
   151
lemmas simp_defs = simp_can_defs simp_ncan_defs
wenzelm@20140
   152
wenzelm@20140
   153
lemmas ind_can_defs = zero_def succ_def nil_def cons_def
wenzelm@20140
   154
  and ind_ncan_defs = ncase_def nrec_def lcase_def lrec_def
wenzelm@20140
   155
lemmas ind_defs = ind_can_defs ind_ncan_defs
wenzelm@20140
   156
wenzelm@20140
   157
lemmas data_defs = simp_defs ind_defs napply_def
wenzelm@20140
   158
  and genrec_defs = letrec_def letrec2_def letrec3_def
wenzelm@20140
   159
wenzelm@20140
   160
wenzelm@20140
   161
subsection {* Beta Rules, including strictness *}
wenzelm@20140
   162
wenzelm@20140
   163
lemma letB: "~ t=bot ==> let x be t in f(x) = f(t)"
wenzelm@20140
   164
  apply (unfold let_def)
wenzelm@20140
   165
  apply (erule rev_mp)
wenzelm@20140
   166
  apply (rule_tac t = "t" in term_case)
wenzelm@20140
   167
      apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam)
wenzelm@20140
   168
  done
wenzelm@20140
   169
wenzelm@20140
   170
lemma letBabot: "let x be bot in f(x) = bot"
wenzelm@20140
   171
  apply (unfold let_def)
wenzelm@20140
   172
  apply (rule caseBbot)
wenzelm@20140
   173
  done
wenzelm@20140
   174
wenzelm@20140
   175
lemma letBbbot: "let x be t in bot = bot"
wenzelm@20140
   176
  apply (unfold let_def)
wenzelm@20140
   177
  apply (rule_tac t = t in term_case)
wenzelm@20140
   178
      apply (rule caseBbot)
wenzelm@20140
   179
     apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam)
wenzelm@20140
   180
  done
wenzelm@20140
   181
wenzelm@20140
   182
lemma applyB: "(lam x. b(x)) ` a = b(a)"
wenzelm@20140
   183
  apply (unfold apply_def)
wenzelm@20140
   184
  apply (simp add: caseBtrue caseBfalse caseBpair caseBlam)
wenzelm@20140
   185
  done
wenzelm@20140
   186
wenzelm@20140
   187
lemma applyBbot: "bot ` a = bot"
wenzelm@20140
   188
  apply (unfold apply_def)
wenzelm@20140
   189
  apply (rule caseBbot)
wenzelm@20140
   190
  done
wenzelm@20140
   191
wenzelm@20140
   192
lemma fixB: "fix(f) = f(fix(f))"
wenzelm@20140
   193
  apply (unfold fix_def)
wenzelm@20140
   194
  apply (rule applyB [THEN ssubst], rule refl)
wenzelm@20140
   195
  done
wenzelm@20140
   196
wenzelm@20140
   197
lemma letrecB:
wenzelm@20140
   198
    "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
   199
  apply (unfold letrec_def)
wenzelm@20140
   200
  apply (rule fixB [THEN ssubst], rule applyB [THEN ssubst], rule refl)
wenzelm@20140
   201
  done
wenzelm@20140
   202
wenzelm@20140
   203
lemmas rawBs = caseBs applyB applyBbot
wenzelm@20140
   204
wenzelm@32153
   205
method_setup beta_rl = {*
wenzelm@32153
   206
  Scan.succeed (fn ctxt =>
wenzelm@32153
   207
    SIMPLE_METHOD' (CHANGED o
wenzelm@32153
   208
      simp_tac (simpset_of ctxt addsimps @{thms rawBs} setloop (stac @{thm letrecB}))))
wenzelm@32153
   209
*} ""
wenzelm@20140
   210
wenzelm@32153
   211
lemma ifBtrue: "if true then t else u = t"
wenzelm@32153
   212
  and ifBfalse: "if false then t else u = u"
wenzelm@32153
   213
  and ifBbot: "if bot then t else u = bot"
wenzelm@32153
   214
  unfolding data_defs by beta_rl+
wenzelm@32153
   215
wenzelm@32153
   216
lemma whenBinl: "when(inl(a),t,u) = t(a)"
wenzelm@32153
   217
  and whenBinr: "when(inr(a),t,u) = u(a)"
wenzelm@32153
   218
  and whenBbot: "when(bot,t,u) = bot"
wenzelm@32153
   219
  unfolding data_defs by beta_rl+
wenzelm@20140
   220
wenzelm@32153
   221
lemma splitB: "split(<a,b>,h) = h(a,b)"
wenzelm@32153
   222
  and splitBbot: "split(bot,h) = bot"
wenzelm@32153
   223
  unfolding data_defs by beta_rl+
wenzelm@17456
   224
wenzelm@32153
   225
lemma fstB: "fst(<a,b>) = a"
wenzelm@32153
   226
  and fstBbot: "fst(bot) = bot"
wenzelm@32153
   227
  unfolding data_defs by beta_rl+
wenzelm@20140
   228
wenzelm@32153
   229
lemma sndB: "snd(<a,b>) = b"
wenzelm@32153
   230
  and sndBbot: "snd(bot) = bot"
wenzelm@32153
   231
  unfolding data_defs by beta_rl+
wenzelm@20140
   232
wenzelm@32153
   233
lemma thdB: "thd(<a,<b,c>>) = c"
wenzelm@32153
   234
  and thdBbot: "thd(bot) = bot"
wenzelm@32153
   235
  unfolding data_defs by beta_rl+
wenzelm@20140
   236
wenzelm@32153
   237
lemma ncaseBzero: "ncase(zero,t,u) = t"
wenzelm@32153
   238
  and ncaseBsucc: "ncase(succ(n),t,u) = u(n)"
wenzelm@32153
   239
  and ncaseBbot: "ncase(bot,t,u) = bot"
wenzelm@32153
   240
  unfolding data_defs by beta_rl+
wenzelm@20140
   241
wenzelm@32153
   242
lemma nrecBzero: "nrec(zero,t,u) = t"
wenzelm@32153
   243
  and nrecBsucc: "nrec(succ(n),t,u) = u(n,nrec(n,t,u))"
wenzelm@32153
   244
  and nrecBbot: "nrec(bot,t,u) = bot"
wenzelm@32153
   245
  unfolding data_defs by beta_rl+
wenzelm@32153
   246
wenzelm@32153
   247
lemma lcaseBnil: "lcase([],t,u) = t"
wenzelm@32153
   248
  and lcaseBcons: "lcase(x$xs,t,u) = u(x,xs)"
wenzelm@32153
   249
  and lcaseBbot: "lcase(bot,t,u) = bot"
wenzelm@32153
   250
  unfolding data_defs by beta_rl+
wenzelm@20140
   251
wenzelm@32153
   252
lemma lrecBnil: "lrec([],t,u) = t"
wenzelm@32153
   253
  and lrecBcons: "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))"
wenzelm@32153
   254
  and lrecBbot: "lrec(bot,t,u) = bot"
wenzelm@32153
   255
  unfolding data_defs by beta_rl+
wenzelm@20140
   256
wenzelm@32153
   257
lemma letrec2B:
wenzelm@32153
   258
  "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
   259
  unfolding data_defs letrec2_def by beta_rl+
wenzelm@20140
   260
wenzelm@32153
   261
lemma letrec3B:
wenzelm@32153
   262
  "letrec g x y z be h(x,y,z,g) in g(p,q,r) =
wenzelm@32153
   263
    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
   264
  unfolding data_defs letrec3_def by beta_rl+
wenzelm@20140
   265
wenzelm@32153
   266
lemma napplyBzero: "f^zero`a = a"
wenzelm@32153
   267
  and napplyBsucc: "f^succ(n)`a = f(f^n`a)"
wenzelm@32153
   268
  unfolding data_defs by beta_rl+
wenzelm@32153
   269
wenzelm@32153
   270
lemmas termBs = letB applyB applyBbot splitB splitBbot fstB fstBbot
wenzelm@32153
   271
  sndB sndBbot thdB thdBbot ifBtrue ifBfalse ifBbot whenBinl whenBinr
wenzelm@32153
   272
  whenBbot ncaseBzero ncaseBsucc ncaseBbot nrecBzero nrecBsucc
wenzelm@32153
   273
  nrecBbot lcaseBnil lcaseBcons lcaseBbot lrecBnil lrecBcons lrecBbot
wenzelm@32153
   274
  napplyBzero napplyBsucc
wenzelm@20140
   275
wenzelm@20140
   276
wenzelm@20140
   277
subsection {* Constructors are injective *}
wenzelm@20140
   278
wenzelm@32154
   279
lemma term_injs:
wenzelm@32154
   280
  "(inl(a) = inl(a')) <-> (a=a')"
wenzelm@32154
   281
  "(inr(a) = inr(a')) <-> (a=a')"
wenzelm@32154
   282
  "(succ(a) = succ(a')) <-> (a=a')"
wenzelm@32154
   283
  "(a$b = a'$b') <-> (a=a' & b=b')"
wenzelm@32154
   284
  by (inj_rl applyB splitB whenBinl whenBinr ncaseBsucc lcaseBcons)
wenzelm@20140
   285
wenzelm@20140
   286
wenzelm@20140
   287
subsection {* Constructors are distinct *}
wenzelm@20140
   288
wenzelm@26480
   289
ML {*
wenzelm@20140
   290
bind_thms ("term_dstncts",
wenzelm@32010
   291
  mkall_dstnct_thms @{theory} @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs})
wenzelm@24825
   292
    [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
wenzelm@20140
   293
*}
wenzelm@20140
   294
wenzelm@20140
   295
wenzelm@20140
   296
subsection {* Rules for pre-order @{text "[="} *}
wenzelm@20140
   297
wenzelm@32154
   298
lemma term_porews:
wenzelm@32154
   299
  "inl(a) [= inl(a') <-> a [= a'"
wenzelm@32154
   300
  "inr(b) [= inr(b') <-> b [= b'"
wenzelm@32154
   301
  "succ(n) [= succ(n') <-> n [= n'"
wenzelm@32154
   302
  "x$xs [= x'$xs' <-> x [= x'  & xs [= xs'"
wenzelm@32154
   303
  by (simp_all add: data_defs ccl_porews)
wenzelm@20140
   304
wenzelm@20140
   305
wenzelm@20140
   306
subsection {* Rewriting and Proving *}
wenzelm@20140
   307
wenzelm@26480
   308
ML {*
wenzelm@24790
   309
  bind_thms ("term_injDs", XH_to_Ds @{thms term_injs});
wenzelm@20140
   310
*}
wenzelm@20140
   311
wenzelm@20917
   312
lemmas term_rews = termBs term_injs term_dstncts ccl_porews term_porews
wenzelm@20917
   313
wenzelm@20140
   314
lemmas [simp] = term_rews
wenzelm@20917
   315
lemmas [elim!] = term_dstncts [THEN notE]
wenzelm@20917
   316
lemmas [dest!] = term_injDs
wenzelm@20140
   317
wenzelm@20140
   318
end