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