author | wenzelm |
Fri, 18 Aug 2017 20:47:47 +0200 | |
changeset 66453 | cc19f7ca2ed6 |
parent 63167 | 0909deb8059b |
permissions | -rw-r--r-- |
25727 | 1 |
theory VC_Condition |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63167
diff
changeset
|
2 |
imports "HOL-Nominal.Nominal" |
25722 | 3 |
begin |
4 |
||
63167 | 5 |
text \<open> |
26262 | 6 |
We give here two examples showing that if we use the variable |
25722 | 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 |
|
25751 | 10 |
nominal data package one is protected from such bogus reasoning. |
63167 | 11 |
\<close> |
25722 | 12 |
|
63167 | 13 |
text \<open>We define alpha-equated lambda-terms as usual.\<close> |
25722 | 14 |
atom_decl name |
15 |
||
16 |
nominal_datatype lam = |
|
17 |
Var "name" |
|
18 |
| App "lam" "lam" |
|
19 |
| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
|
20 |
||
63167 | 21 |
text \<open> |
25722 | 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 |
|
63167 | 27 |
of the algorithm W.\<close> |
26055 | 28 |
|
25722 | 29 |
inductive |
30 |
unbind :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _,_" [60,60,60] 60) |
|
31 |
where |
|
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 |
||
63167 | 36 |
text \<open> |
25722 | 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 |
|
63167 | 39 |
bit clumsy).\<close> |
26055 | 40 |
|
25722 | 41 |
lemma unbind_lambda_lambda1: |
42 |
shows "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)" |
|
43 |
by (auto intro: unbind.intros) |
|
44 |
||
45 |
lemma unbind_lambda_lambda2: |
|
46 |
shows "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)" |
|
47 |
proof - |
|
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 |
|
55 |
qed |
|
56 |
||
63167 | 57 |
text \<open>Unbind is equivariant ...\<close> |
25722 | 58 |
equivariance unbind |
59 |
||
63167 | 60 |
text \<open> |
25722 | 61 |
... but it is not variable-convention compatible (see Urban, |
25751 | 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 |
|
63167 | 68 |
principle and see what happens.\<close> |
25722 | 69 |
|
70 |
nominal_inductive unbind |
|
71 |
sorry |
|
72 |
||
63167 | 73 |
text \<open> |
25722 | 74 |
To obtain a faulty lemma, we introduce the function 'bind' |
25751 | 75 |
which takes a list of names and abstracts them away in |
63167 | 76 |
a given lambda-term.\<close> |
26055 | 77 |
|
25722 | 78 |
fun |
79 |
bind :: "name list \<Rightarrow> lam \<Rightarrow> lam" |
|
80 |
where |
|
81 |
"bind [] t = t" |
|
82 |
| "bind (x#xs) t = Lam [x].(bind xs t)" |
|
83 |
||
63167 | 84 |
text \<open> |
25722 | 85 |
Although not necessary for our main argument below, we can |
63167 | 86 |
easily prove that bind undoes the unbinding.\<close> |
26055 | 87 |
|
25722 | 88 |
lemma bind_unbind: |
89 |
assumes a: "t \<mapsto> xs,t'" |
|
90 |
shows "t = bind xs t'" |
|
91 |
using a by (induct) (auto) |
|
92 |
||
63167 | 93 |
text \<open> |
25722 | 94 |
The next lemma shows by induction on xs that if x is a free |
25867 | 95 |
variable in t, and x does not occur in xs, then x is a free |
25722 | 96 |
variable in bind xs t. In the nominal tradition we formulate |
63167 | 97 |
'is a free variable in' as 'is not fresh for'.\<close> |
26055 | 98 |
|
25722 | 99 |
lemma 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)" |
|
103 |
using a b |
|
104 |
by (induct xs) |
|
105 |
(auto simp add: fresh_list_cons abs_fresh fresh_atm) |
|
106 |
||
63167 | 107 |
text \<open> |
25751 | 108 |
Now comes the first faulty lemma. It is derived using the |
25722 | 109 |
variable convention (i.e. our strong induction principle). |
26262 | 110 |
This faulty lemma states that if t unbinds to x#xs and t', |
25722 | 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 |
|
63167 | 113 |
the binder x is fresh w.r.t. to the xs unbound previously.\<close> |
25722 | 114 |
|
115 |
lemma faulty1: |
|
116 |
assumes a: "t\<mapsto>(x#xs),t'" |
|
117 |
shows "\<not>(x\<sharp>t') \<Longrightarrow> \<not>(x\<sharp>bind xs t')" |
|
118 |
using a |
|
119 |
by (nominal_induct t xs'\<equiv>"x#xs" t' avoiding: xs rule: unbind.strong_induct) |
|
120 |
(simp_all add: free_variable) |
|
121 |
||
63167 | 122 |
text \<open> |
25751 | 123 |
Obviously this lemma is bogus. For example, in |
124 |
case Lam [x].Lam [x].(Var x) \<mapsto> [x,x],(Var x). |
|
63167 | 125 |
As a result, we can prove False.\<close> |
26055 | 126 |
|
25722 | 127 |
lemma false1: |
128 |
shows "False" |
|
129 |
proof - |
|
26932 | 130 |
fix x |
25722 | 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 |
|
138 |
qed |
|
139 |
||
63167 | 140 |
text \<open> |
25722 | 141 |
The next example is slightly simpler, but looks more |
25751 | 142 |
contrived than 'unbind'. This example, called 'strip' just |
63167 | 143 |
strips off the top-most binders from lambdas.\<close> |
25722 | 144 |
|
145 |
inductive |
|
146 |
strip :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<rightarrow> _" [60,60] 60) |
|
147 |
where |
|
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 |
||
63167 | 152 |
text \<open> |
25722 | 153 |
The relation is equivariant but we have to use again |
63167 | 154 |
sorry to derive a strong induction principle.\<close> |
26055 | 155 |
|
25722 | 156 |
equivariance strip |
157 |
||
158 |
nominal_inductive strip |
|
159 |
sorry |
|
160 |
||
63167 | 161 |
text \<open> |
25751 | 162 |
The second faulty lemma shows that a variable being fresh |
63167 | 163 |
for a term is also fresh for this term after striping.\<close> |
26055 | 164 |
|
25722 | 165 |
lemma faulty2: |
166 |
fixes x::"name" |
|
167 |
assumes a: "t \<rightarrow> t'" |
|
168 |
shows "x\<sharp>t \<Longrightarrow> x\<sharp>t'" |
|
169 |
using a |
|
170 |
by (nominal_induct t t'\<equiv>t' avoiding: t' rule: strip.strong_induct) |
|
171 |
(auto simp add: abs_fresh) |
|
172 |
||
63167 | 173 |
text \<open>Obviously Lam [x].Var x is a counter example to this lemma.\<close> |
26055 | 174 |
|
25722 | 175 |
lemma false2: |
176 |
shows "False" |
|
177 |
proof - |
|
26932 | 178 |
fix x |
25722 | 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) |
|
184 |
qed |
|
26055 | 185 |
|
63167 | 186 |
text \<open>A similar effect can be achieved by using naive inversion |
187 |
on rules.\<close> |
|
26095 | 188 |
|
189 |
lemma false3: |
|
190 |
shows "False" |
|
191 |
proof - |
|
26932 | 192 |
fix x |
26095 | 193 |
have "Lam [x].(Var x) \<rightarrow> (Var x)" by (auto intro: strip.intros) |
26262 | 194 |
moreover obtain y::"name" where fc: "y\<sharp>x" by (rule exists_fresh) (rule fin_supp) |
26095 | 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 |
|
26262 | 198 |
then have "Var y \<rightarrow> Var x" using fc |
199 |
by (cases rule: strip.strong_cases[where x=y]) |
|
26095 | 200 |
(simp_all add: lam.inject alpha abs_fresh) |
26262 | 201 |
then show "False" using fc |
26095 | 202 |
by (cases) (simp_all add: lam.inject fresh_atm) |
203 |
qed |
|
204 |
||
63167 | 205 |
text \<open> |
26262 | 206 |
Moral: Who would have thought that the variable convention |
207 |
is in general an unsound reasoning principle. |
|
63167 | 208 |
\<close> |
26262 | 209 |
|
62390 | 210 |
end |