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