summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | urbanc |

Mon, 08 Oct 2007 07:05:54 +0200 | |

changeset 24897 | b0a93a6d6ab9 |

parent 24896 | 70f238757695 |

child 24898 | 799ca514244f |

changed file name

src/HOL/Nominal/Examples/ROOT.ML | file | annotate | diff | comparison | revisions | |

src/HOL/Nominal/Examples/VC-Compatible.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Nominal/Examples/VC_Compatible.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Nominal/Examples/ROOT.ML Mon Oct 08 05:27:52 2007 +0200 +++ b/src/HOL/Nominal/Examples/ROOT.ML Mon Oct 08 07:05:54 2007 +0200 @@ -17,8 +17,8 @@ "Weakening", "Crary", "SOS", - "LocalWeakening" + "LocalWeakening", "Support" ]; -setmp quick_and_dirty true use_thy "VC-Compatible"; \ No newline at end of file +setmp quick_and_dirty true use_thy "VC_Compatible"; \ No newline at end of file

--- a/src/HOL/Nominal/Examples/VC-Compatible.thy Mon Oct 08 05:27:52 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,190 +0,0 @@ -(* $Id$ *) - -theory VC_NonCompatible -imports "../Nominal" -begin - -text {* - We show here two examples where using the variable - convention carelessly in rule inductions, we end - up with faulty lemmas. The point is that the examples - are not variable-convention compatible and therefore - in the nominal package one is protected from such - bogus reasoning. -*} - -text {* - We define alpha-equated lambda-terms as usual. -*} -atom_decl name - -nominal_datatype lam = - Var "name" - | App "lam" "lam" - | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) - -text {* - The inductive relation "unbind" unbinds the top-most - binders of a lambda-term; this relation is obviously - not a function, since it does not respect alpha- - equivalence. However as a relation unbind is ok and - a similar relation has been used in our formalisation - of the algorithm W. -*} -inductive - unbind :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _,_" [60,60,60] 60) -where - u_var: "(Var a) \<mapsto> [],(Var a)" -| u_app: "(App t1 t2) \<mapsto> [],(App t1 t2)" -| u_lam: "t\<mapsto>xs,t' \<Longrightarrow> (Lam [x].t) \<mapsto> (x#xs),t'" - -text {* Unbind is equivariant ...*} -equivariance unbind - -text {* - ... but it is not variable-convention compatible (see Urban, - Berghofer, Norrish [2007] for more details). This condition - requires for rule u_lam, that the binder x is not a free variable - in the rule's conclusion. Beacuse this condition is not satisfied, - Isabelle will not derive a strong induction principle for unbind - - that means Isabelle does not allow us to use the variable - convention in induction proofs involving unbind. We can, however, - force Isabelle to derive the strengthening induction principle. -*} -nominal_inductive unbind - sorry - -text {* - We can show that %x.%x. x unbinds to [x,x],x and - also to [z,y],y (though the proof for the second - is a bit clumsy). -*} -lemma unbind_lambda_lambda1: - shows "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)" -by (auto intro: unbind.intros) - -lemma unbind_lambda_lambda2: - shows "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)" -proof - - have "Lam [x].Lam [x].(Var x) = Lam [y].Lam [z].(Var z)" - by (auto simp add: lam.inject alpha calc_atm abs_fresh fresh_atm) - moreover - have "Lam [y].Lam [z].(Var z) \<mapsto> [y,z],(Var z)" - by (auto intro: unbind.intros) - ultimately - show "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)" by simp -qed - -text {* - The function 'bind' takes a list of names and abstracts - away these names in a given lambda-term. -*} -fun - bind :: "name list \<Rightarrow> lam \<Rightarrow> lam" -where - "bind [] t = t" -| "bind (x#xs) t = Lam [x].(bind xs t)" - -text {* - Although not necessary for our main argument below, we can - easily prove that bind undoes the unbinding. -*} -lemma bind_unbind: - assumes a: "t \<mapsto> xs,t'" - shows "t = bind xs t'" -using a by (induct) (auto) - -text {* - The next lemma shows that if x is a free variable in t - and x does not occur in xs, then x is a free variable - in bind xs t. In the nominal tradition we formulate - 'is a free variable in' as 'is not fresh for'. -*} -lemma free_variable: - fixes x::"name" - assumes a: "\<not>(x\<sharp>t)" and b: "x\<sharp>xs" - shows "\<not>(x\<sharp>bind xs t)" -using a b -by (induct xs) - (auto simp add: fresh_list_cons abs_fresh fresh_atm) - -text {* - Now comes the faulty lemma. It is derived using the - variable convention, that means using the strong induction - principle we 'proved' above by using sorry. This faulty - lemma states that if t unbinds to x::xs and t', and x is a - free variable in t', then it is also a free variable in - bind xs t'. We show this lemma by assuming that the binder - x is fresh w.r.t. to the xs unbound previously. -*} -lemma faulty1: - assumes a: "t\<mapsto>(x#xs),t'" - shows "\<not>(x\<sharp>t') \<Longrightarrow> \<not>(x\<sharp>bind xs t')" -using a -by (nominal_induct t xs'\<equiv>"x#xs" t' avoiding: xs rule: unbind.strong_induct) - (simp_all add: free_variable) - -text {* - Obviously the faulty lemma does not hold for the case - Lam [x].Lam [x].(Var x) \<mapsto> [x,x],(Var x). -*} -lemma false1: - shows "False" -proof - - have "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)" - and "\<not>(x\<sharp>Var x)" by (simp_all add: unbind_lambda_lambda1 fresh_atm) - then have "\<not>(x\<sharp>(bind [x] (Var x)))" by (rule faulty1) - moreover - have "x\<sharp>(bind [x] (Var x))" by (simp add: abs_fresh) - ultimately - show "False" by simp -qed - -text {* - The next example is slightly simpler, but looks more - contrived than unbind. This example just strips off - the top-most binders from lambdas. -*} - -inductive - strip :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<rightarrow> _" [60,60] 60) -where - s_var: "(Var a) \<rightarrow> (Var a)" -| s_app: "(App t1 t2) \<rightarrow> (App t1 t2)" -| s_lam: "t \<rightarrow> t' \<Longrightarrow> (Lam [x].t) \<rightarrow> t'" - -text {* - The relation is equivariant but we have to use again - sorry to derive a strong induction principle. -*} -equivariance strip - -nominal_inductive strip - sorry - -text {* - The faulty lemma shows that a variable that is fresh - for a term is also fresh for the term after striping. -*} -lemma faulty2: - fixes x::"name" - assumes a: "t \<rightarrow> t'" - shows "x\<sharp>t \<Longrightarrow> x\<sharp>t'" -using a -by (nominal_induct t t'\<equiv>t' avoiding: t' rule: strip.strong_induct) - (auto simp add: abs_fresh) - -text {* - Obviously %x.x is an counter example to this lemma. -*} -lemma false2: - shows "False" -proof - - have "Lam [x].(Var x) \<rightarrow> (Var x)" by (auto intro: strip.intros) - moreover - have "x\<sharp>Lam [x].(Var x)" by (simp add: abs_fresh) - ultimately have "x\<sharp>(Var x)" by (simp only: faulty2) - then show "False" by (simp add: fresh_atm) -qed - -end \ No newline at end of file

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nominal/Examples/VC_Compatible.thy Mon Oct 08 07:05:54 2007 +0200 @@ -0,0 +1,190 @@ +(* $Id$ *) + +theory VC_Compatible +imports "../Nominal" +begin + +text {* + We show here two examples where using the variable + convention carelessly in rule inductions, we end + up with faulty lemmas. The point is that the examples + are not variable-convention compatible and therefore + in the nominal package one is protected from such + bogus reasoning. +*} + +text {* + We define alpha-equated lambda-terms as usual. +*} +atom_decl name + +nominal_datatype lam = + Var "name" + | App "lam" "lam" + | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) + +text {* + The inductive relation "unbind" unbinds the top-most + binders of a lambda-term; this relation is obviously + not a function, since it does not respect alpha- + equivalence. However as a relation unbind is ok and + a similar relation has been used in our formalisation + of the algorithm W. +*} +inductive + unbind :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _,_" [60,60,60] 60) +where + u_var: "(Var a) \<mapsto> [],(Var a)" +| u_app: "(App t1 t2) \<mapsto> [],(App t1 t2)" +| u_lam: "t\<mapsto>xs,t' \<Longrightarrow> (Lam [x].t) \<mapsto> (x#xs),t'" + +text {* Unbind is equivariant ...*} +equivariance unbind + +text {* + ... but it is not variable-convention compatible (see Urban, + Berghofer, Norrish [2007] for more details). This condition + requires for rule u_lam, that the binder x is not a free variable + in the rule's conclusion. Beacuse this condition is not satisfied, + Isabelle will not derive a strong induction principle for unbind + - that means Isabelle does not allow us to use the variable + convention in induction proofs involving unbind. We can, however, + force Isabelle to derive the strengthening induction principle. +*} +nominal_inductive unbind + sorry + +text {* + We can show that %x.%x. x unbinds to [x,x],x and + also to [z,y],y (though the proof for the second + is a bit clumsy). +*} +lemma unbind_lambda_lambda1: + shows "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)" +by (auto intro: unbind.intros) + +lemma unbind_lambda_lambda2: + shows "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)" +proof - + have "Lam [x].Lam [x].(Var x) = Lam [y].Lam [z].(Var z)" + by (auto simp add: lam.inject alpha calc_atm abs_fresh fresh_atm) + moreover + have "Lam [y].Lam [z].(Var z) \<mapsto> [y,z],(Var z)" + by (auto intro: unbind.intros) + ultimately + show "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)" by simp +qed + +text {* + The function 'bind' takes a list of names and abstracts + away these names in a given lambda-term. +*} +fun + bind :: "name list \<Rightarrow> lam \<Rightarrow> lam" +where + "bind [] t = t" +| "bind (x#xs) t = Lam [x].(bind xs t)" + +text {* + Although not necessary for our main argument below, we can + easily prove that bind undoes the unbinding. +*} +lemma bind_unbind: + assumes a: "t \<mapsto> xs,t'" + shows "t = bind xs t'" +using a by (induct) (auto) + +text {* + The next lemma shows that if x is a free variable in t + and x does not occur in xs, then x is a free variable + in bind xs t. In the nominal tradition we formulate + 'is a free variable in' as 'is not fresh for'. +*} +lemma free_variable: + fixes x::"name" + assumes a: "\<not>(x\<sharp>t)" and b: "x\<sharp>xs" + shows "\<not>(x\<sharp>bind xs t)" +using a b +by (induct xs) + (auto simp add: fresh_list_cons abs_fresh fresh_atm) + +text {* + Now comes the faulty lemma. It is derived using the + variable convention, that means using the strong induction + principle we 'proved' above by using sorry. This faulty + lemma states that if t unbinds to x::xs and t', and x is a + free variable in t', then it is also a free variable in + bind xs t'. We show this lemma by assuming that the binder + x is fresh w.r.t. to the xs unbound previously. +*} +lemma faulty1: + assumes a: "t\<mapsto>(x#xs),t'" + shows "\<not>(x\<sharp>t') \<Longrightarrow> \<not>(x\<sharp>bind xs t')" +using a +by (nominal_induct t xs'\<equiv>"x#xs" t' avoiding: xs rule: unbind.strong_induct) + (simp_all add: free_variable) + +text {* + Obviously the faulty lemma does not hold for the case + Lam [x].Lam [x].(Var x) \<mapsto> [x,x],(Var x). +*} +lemma false1: + shows "False" +proof - + have "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)" + and "\<not>(x\<sharp>Var x)" by (simp_all add: unbind_lambda_lambda1 fresh_atm) + then have "\<not>(x\<sharp>(bind [x] (Var x)))" by (rule faulty1) + moreover + have "x\<sharp>(bind [x] (Var x))" by (simp add: abs_fresh) + ultimately + show "False" by simp +qed + +text {* + The next example is slightly simpler, but looks more + contrived than unbind. This example just strips off + the top-most binders from lambdas. +*} + +inductive + strip :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<rightarrow> _" [60,60] 60) +where + s_var: "(Var a) \<rightarrow> (Var a)" +| s_app: "(App t1 t2) \<rightarrow> (App t1 t2)" +| s_lam: "t \<rightarrow> t' \<Longrightarrow> (Lam [x].t) \<rightarrow> t'" + +text {* + The relation is equivariant but we have to use again + sorry to derive a strong induction principle. +*} +equivariance strip + +nominal_inductive strip + sorry + +text {* + The faulty lemma shows that a variable that is fresh + for a term is also fresh for the term after striping. +*} +lemma faulty2: + fixes x::"name" + assumes a: "t \<rightarrow> t'" + shows "x\<sharp>t \<Longrightarrow> x\<sharp>t'" +using a +by (nominal_induct t t'\<equiv>t' avoiding: t' rule: strip.strong_induct) + (auto simp add: abs_fresh) + +text {* + Obviously %x.x is an counter example to this lemma. +*} +lemma false2: + shows "False" +proof - + have "Lam [x].(Var x) \<rightarrow> (Var x)" by (auto intro: strip.intros) + moreover + have "x\<sharp>Lam [x].(Var x)" by (simp add: abs_fresh) + ultimately have "x\<sharp>(Var x)" by (simp only: faulty2) + then show "False" by (simp add: fresh_atm) +qed + +end \ No newline at end of file