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