25727
|
1 |
theory VC_Condition
|
25722
|
2 |
imports "../Nominal"
|
|
3 |
begin
|
|
4 |
|
|
5 |
text {*
|
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.
|
25722
|
11 |
*}
|
|
12 |
|
25751
|
13 |
text {* We define alpha-equated lambda-terms as usual. *}
|
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 |
|
|
21 |
text {*
|
|
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. *}
|
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 |
|
|
36 |
text {*
|
|
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). *}
|
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 |
|
|
57 |
text {* Unbind is equivariant ...*}
|
|
58 |
equivariance unbind
|
|
59 |
|
|
60 |
text {*
|
|
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
|
|
68 |
principle and see what happens. *}
|
25722
|
69 |
|
|
70 |
nominal_inductive unbind
|
|
71 |
sorry
|
|
72 |
|
|
73 |
text {*
|
|
74 |
To obtain a faulty lemma, we introduce the function 'bind'
|
25751
|
75 |
which takes a list of names and abstracts them away in
|
25722
|
76 |
a given lambda-term. *}
|
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 |
|
|
84 |
text {*
|
|
85 |
Although not necessary for our main argument below, we can
|
|
86 |
easily prove that bind undoes the unbinding. *}
|
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 |
|
|
93 |
text {*
|
|
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
|
|
97 |
'is a free variable in' as 'is not fresh for'. *}
|
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 |
|
|
107 |
text {*
|
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
|
|
113 |
the binder x is fresh w.r.t. to the xs unbound previously. *}
|
|
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 |
|
|
122 |
text {*
|
25751
|
123 |
Obviously this lemma is bogus. For example, in
|
|
124 |
case Lam [x].Lam [x].(Var x) \<mapsto> [x,x],(Var x).
|
26055
|
125 |
As a result, we can prove False. *}
|
|
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 |
|
|
140 |
text {*
|
|
141 |
The next example is slightly simpler, but looks more
|
25751
|
142 |
contrived than 'unbind'. This example, called 'strip' just
|
25722
|
143 |
strips off the top-most binders from lambdas. *}
|
|
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 |
|
|
152 |
text {*
|
|
153 |
The relation is equivariant but we have to use again
|
26055
|
154 |
sorry to derive a strong induction principle. *}
|
|
155 |
|
25722
|
156 |
equivariance strip
|
|
157 |
|
|
158 |
nominal_inductive strip
|
|
159 |
sorry
|
|
160 |
|
|
161 |
text {*
|
25751
|
162 |
The second faulty lemma shows that a variable being fresh
|
26055
|
163 |
for a term is also fresh for this term after striping. *}
|
|
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 |
|
25751
|
173 |
text {* Obviously Lam [x].Var x is a counter example to this lemma. *}
|
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 |
|
26262
|
186 |
text {* A similar effect can be achieved by using naive inversion
|
|
187 |
on rules. *}
|
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 |
|
26262
|
205 |
text {*
|
|
206 |
Moral: Who would have thought that the variable convention
|
|
207 |
is in general an unsound reasoning principle.
|
|
208 |
*}
|
|
209 |
|
62390
|
210 |
end
|