1.1 --- a/src/HOL/Nominal/Examples/Contexts.thy Tue Apr 29 19:55:02 2008 +0200
1.2 +++ b/src/HOL/Nominal/Examples/Contexts.thy Fri May 02 02:16:10 2008 +0200
1.3 @@ -7,14 +7,15 @@
1.4 text {*
1.5
1.6 We show here that the Plotkin-style of defining
1.7 - reduction relations (based on congruence rules) is
1.8 + beta-reduction (based on congruence rules) is
1.9 equivalent to the Felleisen-Hieb-style representation
1.10 - (based on contexts), and show cbv-evaluation via a
1.11 - CK-machine described by Roshan James.
1.12 + (based on contexts). We also define cbv-evaluation
1.13 + via a CK-machine described by Roshan James.
1.14
1.15 - The interesting point is that contexts do not contain
1.16 - any binders. On the other hand the operation of filling
1.17 - a term into a context produces an alpha-equivalent term.
1.18 + The interesting point in this theory is that contexts
1.19 + do not contain any binders. On the other hand the operation
1.20 + of filling a term into a context produces an alpha-equivalent
1.21 + term.
1.22
1.23 *}
1.24
1.25 @@ -29,9 +30,10 @@
1.26 | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
1.27
1.28 text {*
1.29 - Contexts - the lambda case in contexts does not bind a name,
1.30 - even if we introduce the notation [_]._ for CLam.
1.31 + Contexts - the lambda case in contexts does not bind
1.32 + a name, even if we introduce the notation [_]._ for CLam.
1.33 *}
1.34 +
1.35 nominal_datatype ctx =
1.36 Hole ("\<box>" 1000)
1.37 | CAppL "ctx" "lam"
1.38 @@ -58,22 +60,23 @@
1.39 *}
1.40
1.41 consts
1.42 - filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_<_>" [100,100] 100)
1.43 + filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100,100] 100)
1.44
1.45 nominal_primrec
1.46 - "\<box><t> = t"
1.47 - "(CAppL E t')<t> = App (E<t>) t'"
1.48 - "(CAppR t' E)<t> = App t' (E<t>)"
1.49 - "(CLam [x].E)<t> = Lam [x].(E<t>)"
1.50 + "\<box>\<lbrakk>t\<rbrakk> = t"
1.51 + "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"
1.52 + "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)"
1.53 + "(CLam [x].E)\<lbrakk>t\<rbrakk> = Lam [x].(E\<lbrakk>t\<rbrakk>)"
1.54 by (rule TrueI)+
1.55
1.56 text {*
1.57 While contexts themselves are not alpha-equivalence classes, the
1.58 filling operation produces an alpha-equivalent lambda-term.
1.59 *}
1.60 +
1.61 lemma alpha_test:
1.62 shows "x\<noteq>y \<Longrightarrow> (CLam [x].\<box>) \<noteq> (CLam [y].\<box>)"
1.63 - and "(CLam [x].\<box>)<Var x> = (CLam [y].\<box>)<Var y>"
1.64 + and "(CLam [x].\<box>)\<lbrakk>Var x\<rbrakk> = (CLam [y].\<box>)\<lbrakk>Var y\<rbrakk>"
1.65 by (auto simp add: alpha ctx.inject lam.inject calc_atm fresh_atm)
1.66
1.67 text {* The composition of two contexts. *}
1.68 @@ -89,7 +92,7 @@
1.69 by (rule TrueI)+
1.70
1.71 lemma ctx_compose:
1.72 - shows "E1<E2<t>> = (E1 \<circ> E2)<t>"
1.73 + shows "(E1 \<circ> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
1.74 by (induct E1 rule: ctx.weak_induct) (auto)
1.75
1.76 text {* Beta-reduction via contexts in the Felleisen-Hieb style. *}
1.77 @@ -97,7 +100,7 @@
1.78 inductive
1.79 ctx_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>x _" [80,80] 80)
1.80 where
1.81 - xbeta[intro]: "E<App (Lam [x].t) t'> \<longrightarrow>x E<t[x::=t']>"
1.82 + xbeta[intro]: "E\<lbrakk>App (Lam [x].t) t'\<rbrakk> \<longrightarrow>x E\<lbrakk>t[x::=t']\<rbrakk>"
1.83
1.84 text {* Beta-reduction via congruence rules in the Plotkin style. *}
1.85
1.86 @@ -113,21 +116,20 @@
1.87
1.88 lemma cong_red_in_ctx:
1.89 assumes a: "t \<longrightarrow>o t'"
1.90 - shows "E<t> \<longrightarrow>o E<t'>"
1.91 + shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>o E\<lbrakk>t'\<rbrakk>"
1.92 using a
1.93 by (induct E rule: ctx.weak_induct) (auto)
1.94
1.95 lemma ctx_red_in_ctx:
1.96 assumes a: "t \<longrightarrow>x t'"
1.97 - shows "E<t> \<longrightarrow>x E<t'>"
1.98 -using a
1.99 -by (induct) (auto simp add: ctx_compose)
1.100 + shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>x E\<lbrakk>t'\<rbrakk>"
1.101 +using a
1.102 +by (induct) (auto simp add: ctx_compose[symmetric])
1.103
1.104 theorem ctx_red_implies_cong_red:
1.105 assumes a: "t \<longrightarrow>x t'"
1.106 shows "t \<longrightarrow>o t'"
1.107 -using a
1.108 -by (induct) (auto intro!: cong_red_in_ctx)
1.109 +using a by (induct) (auto intro: cong_red_in_ctx)
1.110
1.111 theorem cong_red_implies_ctx_red:
1.112 assumes a: "t \<longrightarrow>o t'"
1.113 @@ -135,13 +137,14 @@
1.114 using a
1.115 proof (induct)
1.116 case (obeta x t' t)
1.117 - have "\<box><App (Lam [x].t) t'> \<longrightarrow>x \<box><t[x::=t']>" by (rule xbeta)
1.118 + have "\<box>\<lbrakk>App (Lam [x].t) t'\<rbrakk> \<longrightarrow>x \<box>\<lbrakk>t[x::=t']\<rbrakk>" by (rule xbeta)
1.119 then show "App (Lam [x].t) t' \<longrightarrow>x t[x::=t']" by simp
1.120 qed (metis ctx_red_in_ctx filling.simps)+ (* found by SledgeHammer *)
1.121
1.122 -section {* We now use context in a CBV list machine *}
1.123
1.124 -text {* First the function that composes a list of contexts *}
1.125 +section {* We now use context in a CBV list machine. *}
1.126 +
1.127 +text {* First, a function that composes a list of contexts. *}
1.128
1.129 primrec
1.130 ctx_composes :: "ctx list \<Rightarrow> ctx" ("_\<down>" [80] 80)
1.131 @@ -150,6 +153,7 @@
1.132 | "(E#Es)\<down> = (Es\<down>) \<circ> E"
1.133
1.134 text {* Values *}
1.135 +
1.136 inductive
1.137 val :: "lam\<Rightarrow>bool"
1.138 where
1.139 @@ -157,10 +161,11 @@
1.140 | v_Var[intro]: "val (Var x)"
1.141
1.142 text {* CBV-reduction using contexts *}
1.143 +
1.144 inductive
1.145 cbv :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>cbv _" [80,80] 80)
1.146 where
1.147 - cbv_beta[intro]: "val v \<Longrightarrow> E<App (Lam [x].e) v> \<longrightarrow>cbv E<e[x::=v]>"
1.148 + cbv_beta[intro]: "val v \<Longrightarrow> E\<lbrakk>App (Lam [x].e) v\<rbrakk> \<longrightarrow>cbv E\<lbrakk>e[x::=v]\<rbrakk>"
1.149
1.150 text {* reflexive, transitive closure of CBV reduction *}
1.151 inductive
1.152 @@ -171,6 +176,7 @@
1.153 | cbvs3[intro,trans]: "\<lbrakk>e1\<longrightarrow>cbv* e2; e2 \<longrightarrow>cbv* e3\<rbrakk> \<Longrightarrow> e1 \<longrightarrow>cbv* e3"
1.154
1.155 text {* A little CK-machine, which builds up a list of evaluation contexts. *}
1.156 +
1.157 inductive
1.158 machine :: "lam\<Rightarrow>ctx list\<Rightarrow>lam\<Rightarrow>ctx list\<Rightarrow>bool" ("<_,_> \<mapsto> <_,_>" [60,60,60,60] 60)
1.159 where
1.160 @@ -180,15 +186,13 @@
1.161
1.162 lemma machine_red_implies_cbv_reds_aux:
1.163 assumes a: "<e,Es> \<mapsto> <e',Es'>"
1.164 - shows "(Es\<down>)<e> \<longrightarrow>cbv* (Es'\<down>)<e'>"
1.165 -using a
1.166 -by (induct) (auto simp add: ctx_compose[symmetric])
1.167 + shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
1.168 +using a by (induct) (auto simp add: ctx_compose)
1.169
1.170 lemma machine_execution_implies_cbv_reds:
1.171 assumes a: "<e,[]> \<mapsto> <e',[]>"
1.172 shows "e \<longrightarrow>cbv* e'"
1.173 -using a
1.174 -by (auto dest: machine_red_implies_cbv_reds_aux)
1.175 +using a by (auto dest: machine_red_implies_cbv_reds_aux)
1.176
1.177 text {*
1.178 One would now like to show something about the opposite