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