1theory VC_Condition
2imports "HOL-Nominal.Nominal" 
3begin
4
5text \<open>
6  We give here two examples showing that if we use the variable  
7  convention carelessly in rule inductions, we might end 
8  up with faulty lemmas. The point is that the examples
9  are not variable-convention compatible and therefore in the 
10  nominal data package one is protected from such bogus reasoning.
11\<close>
12
13text \<open>We define alpha-equated lambda-terms as usual.\<close>
14atom_decl name 
15
16nominal_datatype lam = 
17    Var "name"
18  | App "lam" "lam"
19  | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
20
21text \<open>
22  The inductive relation 'unbind' unbinds the top-most  
23  binders of a lambda-term; this relation is obviously  
24  not a function, since it does not respect alpha-      
25  equivalence. However as a relation 'unbind' is ok and     
26  a similar relation has been used in our formalisation 
27  of the algorithm W.\<close>
28
29inductive
30  unbind :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _,_" [60,60,60] 60)
31where
32  u_var: "(Var a) \<mapsto> [],(Var a)"
33| u_app: "(App t1 t2) \<mapsto> [],(App t1 t2)"
34| u_lam: "t\<mapsto>xs,t' \<Longrightarrow> (Lam [x].t) \<mapsto> (x#xs),t'"
35
36text \<open>
37  We can show that Lam [x].Lam [x].Var x unbinds to [x,x],Var x 
38  and also to [z,y],Var y (though the proof for the second is a 
39  bit clumsy).\<close> 
40
41lemma unbind_lambda_lambda1: 
42  shows "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)"
43by (auto intro: unbind.intros)
44
45lemma unbind_lambda_lambda2: 
46  shows "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)"
47proof -
48  have "Lam [x].Lam [x].(Var x) = Lam [y].Lam [z].(Var z)" 
49    by (auto simp add: lam.inject alpha calc_atm abs_fresh fresh_atm)
50  moreover
51  have "Lam [y].Lam [z].(Var z) \<mapsto> [y,z],(Var z)"
52    by (auto intro: unbind.intros)
53  ultimately 
54  show "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)" by simp
55qed
56
57text \<open>Unbind is equivariant ...\<close>
58equivariance unbind
59
60text \<open>
61  ... but it is not variable-convention compatible (see Urban, 
62  Berghofer, Norrish [2007]). This condition requires for rule u_lam to 
63  have the binder x not being a free variable in this rule's conclusion. 
64  Because this condition is not satisfied, Isabelle will not derive a 
65  strong induction principle for 'unbind' - that means Isabelle does not 
66  allow us to use the variable convention in induction proofs over 'unbind'. 
67  We can, however, force Isabelle to derive the strengthening induction 
68  principle and see what happens.\<close>
69
70nominal_inductive unbind
71  sorry
72
73text \<open>
74  To obtain a faulty lemma, we introduce the function 'bind'
75  which takes a list of names and abstracts them away in 
76  a given lambda-term.\<close>
77
78fun 
79  bind :: "name list \<Rightarrow> lam \<Rightarrow> lam"
80where
81  "bind [] t = t"
82| "bind (x#xs) t = Lam [x].(bind xs t)"
83
84text \<open>
85  Although not necessary for our main argument below, we can 
86  easily prove that bind undoes the unbinding.\<close>
87
88lemma bind_unbind:
89  assumes a: "t \<mapsto> xs,t'"
90  shows "t = bind xs t'"
91using a by (induct) (auto)
92
93text \<open>
94  The next lemma shows by induction on xs that if x is a free 
95  variable in t, and x does not occur in xs, then x is a free 
96  variable in bind xs t. In the nominal tradition we formulate    
97  'is a free variable in' as 'is not fresh for'.\<close>
98
99lemma free_variable:
100  fixes x::"name"
101  assumes a: "\<not>(x\<sharp>t)" and b: "x\<sharp>xs"
102  shows "\<not>(x\<sharp>bind xs t)"
103using a b
104by (induct xs)
105   (auto simp add: fresh_list_cons abs_fresh fresh_atm)
106
107text \<open>
108  Now comes the first faulty lemma. It is derived using the     
109  variable convention (i.e. our strong induction principle). 
110  This faulty lemma states that if t unbinds to x#xs and t', 
111  and x is a free variable in t', then it is also a free 
112  variable in bind xs t'. We show this lemma by assuming that 
113  the binder x is fresh w.r.t. to the xs unbound previously.\<close>   
114
115lemma faulty1:
116  assumes a: "t\<mapsto>(x#xs),t'"
117  shows "\<not>(x\<sharp>t') \<Longrightarrow> \<not>(x\<sharp>bind xs t')"
118using a
119by (nominal_induct t xs'\<equiv>"x#xs" t' avoiding: xs rule: unbind.strong_induct)
120   (simp_all add: free_variable)
121
122text \<open>
123  Obviously this lemma is bogus. For example, in 
124  case Lam [x].Lam [x].(Var x) \<mapsto> [x,x],(Var x). 
125  As a result, we can prove False.\<close>
126
127lemma false1:
128  shows "False"
129proof -
130  fix x
131  have "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)" 
132  and  "\<not>(x\<sharp>Var x)" by (simp_all add: unbind_lambda_lambda1 fresh_atm)
133  then have "\<not>(x\<sharp>(bind [x] (Var x)))" by (rule faulty1)
134  moreover 
135  have "x\<sharp>(bind [x] (Var x))" by (simp add: abs_fresh)
136  ultimately
137  show "False" by simp
138qed
139   
140text \<open>
141  The next example is slightly simpler, but looks more
142  contrived than 'unbind'. This example, called 'strip' just 
143  strips off the top-most binders from lambdas.\<close>
144
145inductive
146  strip :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<rightarrow> _" [60,60] 60)
147where
148  s_var: "(Var a) \<rightarrow> (Var a)"
149| s_app: "(App t1 t2) \<rightarrow> (App t1 t2)"
150| s_lam: "t \<rightarrow> t' \<Longrightarrow> (Lam [x].t) \<rightarrow> t'"
151
152text \<open>
153  The relation is equivariant but we have to use again 
154  sorry to derive a strong induction principle.\<close>
155
156equivariance strip
157
158nominal_inductive strip
159  sorry
160
161text \<open>
162  The second faulty lemma shows that a variable being fresh
163  for a term is also fresh for this term after striping.\<close>
164
165lemma faulty2:
166  fixes x::"name"
167  assumes a: "t \<rightarrow> t'"
168  shows "x\<sharp>t \<Longrightarrow> x\<sharp>t'"
169using a
170by (nominal_induct t t'\<equiv>t' avoiding: t' rule: strip.strong_induct)
171   (auto simp add: abs_fresh)
172
173text \<open>Obviously Lam [x].Var x is a counter example to this lemma.\<close>
174
175lemma false2:
176  shows "False"
177proof -
178  fix x
179  have "Lam [x].(Var x) \<rightarrow> (Var x)" by (auto intro: strip.intros)
180  moreover
181  have "x\<sharp>Lam [x].(Var x)" by (simp add: abs_fresh)
182  ultimately have "x\<sharp>(Var x)" by (simp only: faulty2)
183  then show "False" by (simp add: fresh_atm)
184qed 
185
186text \<open>A similar effect can be achieved by using naive inversion 
187  on rules.\<close>
188
189lemma false3: 
190  shows "False"
191proof -
192  fix x
193  have "Lam [x].(Var x) \<rightarrow> (Var x)" by (auto intro: strip.intros)
194  moreover obtain y::"name" where fc: "y\<sharp>x" by (rule exists_fresh) (rule fin_supp)
195  then have "Lam [x].(Var x) = Lam [y].(Var y)"
196    by (simp add: lam.inject alpha calc_atm fresh_atm)
197  ultimately have "Lam [y].(Var y) \<rightarrow> (Var x)" by simp
198  then have "Var y \<rightarrow> Var x" using fc
199    by (cases rule: strip.strong_cases[where x=y])
200       (simp_all add: lam.inject alpha abs_fresh)
201  then show "False" using fc
202    by (cases) (simp_all add: lam.inject fresh_atm)
203qed
204
205text \<open>
206  Moral: Who would have thought that the variable convention 
207  is in general an unsound reasoning principle.
208\<close>
209
210end
211