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