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