1theory Contexts
2imports "HOL-Nominal.Nominal"
3begin
4
5text \<open>
6  
7  We show here that the Plotkin-style of defining
8  beta-reduction (based on congruence rules) is
9  equivalent to the Felleisen-Hieb-style representation 
10  (based on contexts). 
11  
12  The interesting point in this theory is that contexts 
13  do not contain any binders. On the other hand the operation 
14  of filling a term into a context produces an alpha-equivalent 
15  term. 
16
17\<close>
18
19atom_decl name
20
21text \<open>
22  Lambda-Terms - the Lam-term constructor binds a name
23\<close>
24
25nominal_datatype lam = 
26    Var "name"
27  | App "lam" "lam"
28  | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
29
30text \<open>
31  Contexts - the lambda case in contexts does not bind 
32  a name, even if we introduce the notation [_]._ for CLam.
33\<close>
34
35nominal_datatype ctx = 
36    Hole ("\<box>" 1000)  
37  | CAppL "ctx" "lam"
38  | CAppR "lam" "ctx" 
39  | CLam "name" "ctx"  ("CLam [_]._" [100,100] 100) 
40
41text \<open>Capture-Avoiding Substitution\<close>
42
43nominal_primrec
44  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
45where
46  "(Var x)[y::=s] = (if x=y then s else (Var x))"
47| "(App t\<^sub>1 t\<^sub>2)[y::=s] = App (t\<^sub>1[y::=s]) (t\<^sub>2[y::=s])"
48| "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
49apply(finite_guess)+
50apply(rule TrueI)+
51apply(simp add: abs_fresh)
52apply(fresh_guess)+
53done
54
55text \<open>
56  Filling is the operation that fills a term into a hole. 
57  This operation is possibly capturing.
58\<close>
59
60nominal_primrec
61  filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100,100] 100)
62where
63  "\<box>\<lbrakk>t\<rbrakk> = t"
64| "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"
65| "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)"
66| "(CLam [x].E)\<lbrakk>t\<rbrakk> = Lam [x].(E\<lbrakk>t\<rbrakk>)" 
67by (rule TrueI)+
68
69text \<open>
70  While contexts themselves are not alpha-equivalence classes, the 
71  filling operation produces an alpha-equivalent lambda-term. 
72\<close>
73
74lemma alpha_test: 
75  shows "x\<noteq>y \<Longrightarrow> (CLam [x].\<box>) \<noteq> (CLam [y].\<box>)"
76  and   "(CLam [x].\<box>)\<lbrakk>Var x\<rbrakk> = (CLam [y].\<box>)\<lbrakk>Var y\<rbrakk>"
77by (auto simp add: alpha ctx.inject lam.inject calc_atm fresh_atm) 
78
79text \<open>The composition of two contexts.\<close>
80
81nominal_primrec
82 ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<circ> _" [100,100] 100)
83where
84  "\<box> \<circ> E' = E'"
85| "(CAppL E t') \<circ> E' = CAppL (E \<circ> E') t'"
86| "(CAppR t' E) \<circ> E' = CAppR t' (E \<circ> E')"
87| "(CLam [x].E) \<circ> E' = CLam [x].(E \<circ> E')"
88by (rule TrueI)+
89  
90lemma ctx_compose:
91  shows "(E1 \<circ> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
92by (induct E1 rule: ctx.induct) (auto)
93
94text \<open>Beta-reduction via contexts in the Felleisen-Hieb style.\<close>
95
96inductive
97  ctx_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>x _" [80,80] 80) 
98where
99  xbeta[intro]: "E\<lbrakk>App (Lam [x].t) t'\<rbrakk> \<longrightarrow>x E\<lbrakk>t[x::=t']\<rbrakk>" 
100
101text \<open>Beta-reduction via congruence rules in the Plotkin style.\<close>
102
103inductive
104  cong_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>o _" [80,80] 80) 
105where
106  obeta[intro]: "App (Lam [x].t) t' \<longrightarrow>o t[x::=t']"
107| oapp1[intro]: "t \<longrightarrow>o t' \<Longrightarrow> App t t2 \<longrightarrow>o App t' t2"
108| oapp2[intro]: "t \<longrightarrow>o t' \<Longrightarrow> App t2 t \<longrightarrow>o App t2 t'"
109| olam[intro]:  "t \<longrightarrow>o t' \<Longrightarrow> Lam [x].t \<longrightarrow>o Lam [x].t'"
110
111text \<open>The proof that shows both relations are equal.\<close>
112
113lemma cong_red_in_ctx:
114  assumes a: "t \<longrightarrow>o t'"
115  shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>o E\<lbrakk>t'\<rbrakk>"
116using a
117by (induct E rule: ctx.induct) (auto)
118
119lemma ctx_red_in_ctx:
120  assumes a: "t \<longrightarrow>x t'"
121  shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>x E\<lbrakk>t'\<rbrakk>"
122using a
123by (induct) (auto simp add: ctx_compose[symmetric])
124
125theorem ctx_red_implies_cong_red:
126  assumes a: "t \<longrightarrow>x t'"
127  shows "t \<longrightarrow>o t'"
128using a by (induct) (auto intro: cong_red_in_ctx)
129
130theorem cong_red_implies_ctx_red:
131  assumes a: "t \<longrightarrow>o t'"
132  shows "t \<longrightarrow>x t'"
133using a
134proof (induct)
135  case (obeta x t' t)
136  have "\<box>\<lbrakk>App (Lam [x].t) t'\<rbrakk> \<longrightarrow>x \<box>\<lbrakk>t[x::=t']\<rbrakk>" by (rule xbeta) 
137  then show  "App (Lam [x].t) t' \<longrightarrow>x t[x::=t']" by simp
138qed (metis ctx_red_in_ctx filling.simps)+ (* found by SledgeHammer *)
139
140
141lemma ctx_existence:
142  assumes a: "t \<longrightarrow>o t'"
143  shows "\<exists>C s s'. t = C\<lbrakk>s\<rbrakk> \<and> t' = C\<lbrakk>s'\<rbrakk> \<and> s \<longrightarrow>o s'"
144using a
145by (induct) (metis cong_red.intros filling.simps)+
146
147end
148