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