1198 text {******************************************************************

  1199   

  1200   The CBV Reduction Relation (Small-Step Semantics) 

  1201   -------------------------------------------------

  1202 

  1203   In order to establish the property that the CK Machine

  1204   calculates a nomrmalform which corresponds to the

  1205   evaluation relation, we introduce the call-by-value

  1206   small-step semantics.

  1207 

  1208 *}

  1209 

  1210 inductive

  1211   cbv :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>cbv _" [60, 60] 60) 

  1212 where

  1213   cbv1: "\<lbrakk>val v; atom x \<sharp> v\<rbrakk> \<Longrightarrow> App (Lam [x].t) v \<longrightarrow>cbv t[x::=v]"

  1214 | cbv2[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> App t t2 \<longrightarrow>cbv App t' t2"

  1215 | cbv3[intro]: "t \<longrightarrow>cbv t' \<Longrightarrow> App t2 t \<longrightarrow>cbv App t2 t'"

  1216 

  1217 equivariance val

  1218 equivariance cbv

  1219 nominal_inductive cbv

  1220   avoids cbv1: "x"

  1221   unfolding fresh_star_def

  1222   by (simp_all add: lam.fresh Abs_fresh_iff fresh_Pair fresh_fact)

  1223 

  1224 text {*

  1225   In order to satisfy the vc-condition we have to formulate

  1226   this relation with the additional freshness constraint

  1227   x\<sharp>v. Though this makes the definition vc-ompatible, it

  1228   makes the definition less useful. We can with some pain

  1229   show that the more restricted rule is equivalent to the

  1230   usual rule. *}

  1231 

  1232 lemma subst_rename: 

  1233   assumes a: "atom y \<sharp> t"

  1234   shows "t[x ::= s] = ((y \<leftrightarrow> x) \<bullet>t)[y ::= s]"

  1235 using a 

  1236 apply (nominal_induct t avoiding: x y s rule: lam.strong_induct)

  1237 apply (auto simp add: lam.fresh fresh_at_base)

  1238 done

  1239 

  1240 thm subst_rename

  1241 

  1242 lemma better_cbv1[intro]: 

  1243   assumes a: "val v" 

  1244   shows "App (Lam [x].t) v \<longrightarrow>cbv t[x::=v]"

  1245 proof -

  1246   obtain y::"name" where fs: "atom y \<sharp> (x, t, v)" by (rule obtain_fresh)

  1247   have "App (Lam [x].t) v = App (Lam [y].((y \<leftrightarrow> x) \<bullet> t)) v" using fs

  1248     by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base)

  1249   also have "\<dots> \<longrightarrow>cbv  ((y \<leftrightarrow> x) \<bullet> t)[y ::= v]" using fs a by (auto intro: cbv1)

  1250   also have "\<dots> = t[x ::= v]" using fs by (simp add: subst_rename[symmetric])

  1251   finally show "App (Lam [x].t) v \<longrightarrow>cbv t[x ::= v]" by simp

  1252 qed

  1253 

  1254 text {*

  1255   The transitive closure of the cbv-reduction relation: *}

  1256 

  1257 inductive 

  1258   "cbvs" :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>cbv* _" [60, 60] 60)

  1259 where

  1260   cbvs1[intro]: "e \<longrightarrow>cbv* e"

  1261 | cbvs2[intro]: "\<lbrakk>e1\<longrightarrow>cbv e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3"

  1262 

  1263 lemma cbvs3[intro]:

  1264   assumes a: "e1 \<longrightarrow>cbv* e2" "e2 \<longrightarrow>cbv* e3"

  1265   shows "e1 \<longrightarrow>cbv* e3"

  1266 using a by (induct) (auto) 

  1267 

  1268 text {******************************************************************

  1269   

  1270   8.) Exercise

  1271   ------------

  1272 

  1273   If more simple exercises are needed, then complete the following proof. 

  1274 

  1275 *}

  1276 

  1277 lemma cbv_in_ctx:

  1278   assumes a: "t \<longrightarrow>cbv t'"

  1279   shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>"

  1280 using a

  1281 proof (induct E)

  1282   case Hole

  1283   have "t \<longrightarrow>cbv t'" by fact

  1284   then show "\<box>\<lbrakk>t\<rbrakk> \<longrightarrow>cbv \<box>\<lbrakk>t'\<rbrakk>" sorry

  1285 next

  1286   case (CAppL E s)

  1287   have ih: "t \<longrightarrow>cbv t' \<Longrightarrow> E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by fact

  1288   have a: "t \<longrightarrow>cbv t'" by fact

  1289   show "(CAppL E s)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppL E s)\<lbrakk>t'\<rbrakk>" sorry

  1290 next

  1291   case (CAppR s E)

  1292   have ih: "t \<longrightarrow>cbv t' \<Longrightarrow> E\<lbrakk>t\<rbrakk> \<longrightarrow>cbv E\<lbrakk>t'\<rbrakk>" by fact

  1293   have a: "t \<longrightarrow>cbv t'" by fact

  1294   show "(CAppR s E)\<lbrakk>t\<rbrakk> \<longrightarrow>cbv (CAppR s E)\<lbrakk>t'\<rbrakk>" sorry

  1295 qed

  1296 

  1297   

  1298 text {******************************************************************

  1299   

  1300   9.) Exercise

  1301   ------------

  1302 

  1303   The point of the cbv-reduction was that we can easily relatively 

  1304   establish the follwoing property:

  1305 

  1306 *}

  1307 

  1308 lemma machine_implies_cbvs_ctx:

  1309   assumes a: "<e, Es> \<mapsto> <e', Es'>"

  1310   shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"

  1311 using a 

  1312 proof (induct)

  1313   case (m1 t1 t2 Es)

  1314 

  1315   show "Es\<down>\<lbrakk>App t1 t2\<rbrakk> \<longrightarrow>cbv* ((CAppL \<box> t2) # Es)\<down>\<lbrakk>t1\<rbrakk>"  sorry

  1316 next

  1317   case (m2 v t2 Es)

  1318   have "val v" by fact

  1319 

  1320   show "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>" sorry

  1321 next

  1322   case (m3 v x t Es)

  1323   have "val v" by fact

  1324  

  1325   show "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" sorry

  1326 qed

  1327 

  1328 text {* 

  1329   It is not difficult to extend the lemma above to

  1330   arbitrary reductions sequences of the CK machine. *}

  1331 

  1332 lemma machines_implies_cbvs_ctx:

  1333   assumes a: "<e, Es> \<mapsto>* <e', Es'>"

  1334   shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"

  1335 using a 

  1336 by (induct) (auto dest: machine_implies_cbvs_ctx)

  1337 

  1338 text {* 

  1339   So whenever we let the CL machine start in an initial

  1340   state and it arrives at a final state, then there exists

  1341   a corresponding cbv-reduction sequence. *}

  1342 

  1343 corollary machines_implies_cbvs:

  1344   assumes a: "<e, []> \<mapsto>* <e', []>"

  1345   shows "e \<longrightarrow>cbv* e'"

  1346 using a by (auto dest: machines_implies_cbvs_ctx)

  1347 

  1348 text {*

  1349   We now want to relate the cbv-reduction to the evaluation

  1350   relation. For this we need two auxiliary lemmas. *}

  1351 

  1352 lemma eval_val:

  1353   assumes a: "val t"

  1354   shows "t \<Down> t"

  1355 using a by (induct) (auto)

  1356 

  1357 lemma e_App_elim:

  1358   assumes a: "App t1 t2 \<Down> v"

  1359   shows "\<exists>x t v'. t1 \<Down> Lam [x].t \<and> t2 \<Down> v' \<and> t[x::=v'] \<Down> v"

  1360 using a by (cases) (auto simp add: lam.eq_iff lam.distinct) 

  1361 

  1362 text {******************************************************************

  1363   

  1364   10.) Exercise

  1365   -------------

  1366 

  1367   Complete the first case in the proof below. 

  1368 

  1369 *}

  1370 

  1371 lemma cbv_eval:

  1372   assumes a: "t1 \<longrightarrow>cbv t2" "t2 \<Down> t3"

  1373   shows "t1 \<Down> t3"

  1374 using a

  1375 proof(induct arbitrary: t3)

  1376   case (cbv1 v x t t3)

  1377   have a1: "val v" by fact

  1378   have a2: "t[x ::= v] \<Down> t3" by fact

  1379 

  1380   show "App (Lam [x].t) v \<Down> t3" sorry

  1381 next

  1382   case (cbv2 t t' t2 t3)

  1383   have ih: "\<And>t3. t' \<Down> t3 \<Longrightarrow> t \<Down> t3" by fact

  1384   have "App t' t2 \<Down> t3" by fact

  1385   then obtain x t'' v' 

  1386     where a1: "t' \<Down> Lam [x].t''" 

  1387       and a2: "t2 \<Down> v'" 

  1388       and a3: "t''[x ::= v'] \<Down> t3" using e_App_elim by blast

  1389   have "t \<Down>  Lam [x].t''" using ih a1 by auto 

  1390   then show "App t t2 \<Down> t3" using a2 a3 by auto

  1391 qed (auto dest!: e_App_elim)

  1392 

  1393 

  1394 text {* 

  1395   Next we extend the lemma above to arbitray initial

  1396   sequences of cbv-reductions. *}

  1397 

  1398 lemma cbvs_eval:

  1399   assumes a: "t1 \<longrightarrow>cbv* t2" "t2 \<Down> t3"

  1400   shows "t1 \<Down> t3"

  1401 using a by (induct) (auto intro: cbv_eval)

  1402 

  1403 text {* 

  1404   Finally, we can show that if from a term t we reach a value 

  1405   by a cbv-reduction sequence, then t evaluates to this value. *}

  1406 

  1407 lemma cbvs_implies_eval:

  1408   assumes a: "t \<longrightarrow>cbv* v" "val v"

  1409   shows "t \<Down> v"

  1410 using a

  1411 by (induct) (auto intro: eval_val cbvs_eval)

  1412 

  1413 text {* 

  1414   All facts tied together give us the desired property about

  1415   K machines. *}

  1416 

  1417 theorem machines_implies_eval:

  1418   assumes a: "<t1, []> \<mapsto>* <t2, []>" 

  1419   and     b: "val t2" 

  1420   shows "t1 \<Down> t2"

  1421 proof -

  1422   have "t1 \<longrightarrow>cbv* t2" using a by (simp add: machines_implies_cbvs)

  1423   then show "t1 \<Down> t2" using b by (simp add: cbvs_implies_eval)

  1424 qed

  1425 

  1426 lemma valid_elim:

  1427   assumes a: "valid ((x, T) # \<Gamma>)"

  1428   shows "atom x \<sharp> \<Gamma> \<and> valid \<Gamma>"

  1429 using a by (cases) (auto)

  1430 

  1431 lemma valid_insert:

  1432   assumes a: "valid (\<Delta> @ [(x, T)] @ \<Gamma>)"

  1433   shows "valid (\<Delta> @ \<Gamma>)" 

  1434 using a

  1435 by (induct \<Delta>)

  1436    (auto simp add: fresh_append fresh_Cons dest!: valid_elim)

  1437 

  1438 lemma fresh_list: 

  1439   shows "atom y \<sharp> xs = (\<forall>x \<in> set xs. atom y \<sharp> x)"

  1440 by (induct xs) (simp_all add: fresh_Nil fresh_Cons)

  1441 

  1442 lemma context_unique:

  1443   assumes a1: "valid \<Gamma>"

  1444   and     a2: "(x, T) \<in> set \<Gamma>"

  1445   and     a3: "(x, U) \<in> set \<Gamma>"

  1446   shows "T = U" 

  1447 using a1 a2 a3

  1448 by (induct) (auto simp add: fresh_list fresh_Pair fresh_at_base)

  1449 

  1450 lemma type_substitution_aux:

  1451   assumes a: "(\<Delta> @ [(x, T')] @ \<Gamma>) \<turnstile> e : T"

  1452   and     b: "\<Gamma> \<turnstile> e' : T'"

  1453   shows "(\<Delta> @ \<Gamma>) \<turnstile> e[x ::= e'] : T" 

  1454 using a b 

  1455 proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, T')] @ \<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)

  1456   case (t_Var y T x e' \<Delta>)

  1457   have a1: "valid (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact

  1458   have a2: "(y,T) \<in> set (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact 

  1459   have a3: "\<Gamma> \<turnstile> e' : T'" by fact

  1460   from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)

  1461   { assume eq: "x = y"

  1462     from a1 a2 have "T = T'" using eq by (auto intro: context_unique)

  1463     with a3 have "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" using eq a4 by (auto intro: weakening)

  1464   }

  1465   moreover

  1466   { assume ineq: "x \<noteq> y"

  1467     from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp

  1468     then have "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" using ineq a4 by auto

  1469   }

  1470   ultimately show "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" by blast

  1471 qed (force simp add: fresh_append fresh_Cons)+

  1472 

  1473 corollary type_substitution:

  1474   assumes a: "(x,T') # \<Gamma> \<turnstile> e : T"

  1475   and     b: "\<Gamma> \<turnstile> e' : T'"

  1476   shows "\<Gamma> \<turnstile> e[x::=e'] : T"

  1477 using a b type_substitution_aux[where \<Delta>="[]"]

  1478 by (auto)

  1479 

  1480 lemma t_App_elim:

  1481   assumes a: "\<Gamma> \<turnstile> App t1 t2 : T"

  1482   shows "\<exists>T'. \<Gamma> \<turnstile> t1 : T' \<rightarrow> T \<and> \<Gamma> \<turnstile> t2 : T'"

  1483 using a

  1484 by (cases) (auto simp add: lam.eq_iff lam.distinct)

  1485 

  1486 lemma t_Lam_elim:

  1487   assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T" 

  1488   and     fc: "atom x \<sharp> \<Gamma>" 

  1489   shows "\<exists>T1 T2. T = T1 \<rightarrow> T2 \<and> (x, T1) # \<Gamma> \<turnstile> t : T2"

  1490 using ty fc

  1491 apply(cases)

  1492 apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff)

  1493 apply(auto simp add: Abs1_eq_iff)

  1494 apply(rule_tac p="(x \<leftrightarrow> xa)" in permute_boolE)

  1495 apply(perm_simp)

  1496 apply(simp add: flip_def swap_fresh_fresh ty_fresh)

  1497 done

  1498 

  1499 theorem cbv_type_preservation:

  1500   assumes a: "t \<longrightarrow>cbv t'"

  1501   and     b: "\<Gamma> \<turnstile> t : T" 

  1502   shows "\<Gamma> \<turnstile> t' : T"

  1503 using a b

  1504 by (nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct)

  1505    (auto dest!: t_Lam_elim t_App_elim simp add: type_substitution ty.eq_iff)

  1506 

  1507 corollary cbvs_type_preservation:

  1508   assumes a: "t \<longrightarrow>cbv* t'"

  1509   and     b: "\<Gamma> \<turnstile> t : T" 

  1510   shows "\<Gamma> \<turnstile> t' : T"

  1511 using a b

  1512 by (induct) (auto intro: cbv_type_preservation)

  1513 

  1514 text {* 

  1515   The Type-Preservation Property for the Machine and Evaluation Relation. *}

  1516 

  1517 theorem machine_type_preservation:

  1518   assumes a: "<t, []> \<mapsto>* <t', []>"

  1519   and     b: "\<Gamma> \<turnstile> t : T" 

  1520   shows "\<Gamma> \<turnstile> t' : T"

  1521 proof -

  1522   from a have "t \<longrightarrow>cbv* t'" by (simp add: machines_implies_cbvs)

  1523   then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: cbvs_type_preservation)

  1524 qed

  1525 

  1526 theorem eval_type_preservation:

  1527   assumes a: "t \<Down> t'"

  1528   and     b: "\<Gamma> \<turnstile> t : T" 

  1529   shows "\<Gamma> \<turnstile> t' : T"

  1530 proof -

  1531   from a have "<t, []> \<mapsto>* <t', []>" by (simp add: eval_implies_machines)

  1532   then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: machine_type_preservation)

  1533 qed

  1534 

  1535 text {* The Progress Property *}

  1536 

  1537 lemma canonical_tArr:

  1538   assumes a: "[] \<turnstile> t : T1 \<rightarrow> T2"

  1539   and     b: "val t"

  1540   shows "\<exists>x t'. t = Lam [x].t'"

  1541 using b a by (induct) (auto) 

  1542 

  1543 theorem progress:

  1544   assumes a: "[] \<turnstile> t : T"

  1545   shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)"

  1546 using a

  1547 by (induct \<Gamma>\<equiv>"[]::ty_ctx" t T)

  1548    (auto intro: cbv.intros dest!: canonical_tArr)

  1549