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

author | urbanc |

Sun, 21 Oct 2007 19:32:19 +0200 | |

changeset 25139 | ffc5054a7274 |

parent 25138 | e453c480d599 |

child 25140 | 273772abbea2 |

tuned

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

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

--- a/src/HOL/Nominal/Examples/Support.thy Sun Oct 21 19:12:05 2007 +0200 +++ b/src/HOL/Nominal/Examples/Support.thy Sun Oct 21 19:32:19 2007 +0200 @@ -5,17 +5,15 @@ begin text {* - An example showing that in general x\<sharp>(A \<union> B) does not imply x\<sharp>A and x\<sharp>B - The example shows that with A set to the set of - even atoms and B to the set of odd even atoms. - Then A \<union> B, that is the set of all atoms, has - empty support. The sets A, respectively B, have - the set of all atoms as support. - + For this we set A to the set of even atoms + and B to the set of odd even atoms. Then A \<union> B, + that is the set of all atoms, has empty support. + The sets A, respectively B, have the set of all atoms + as support. *} atom_decl atom @@ -37,6 +35,7 @@ lemma EVEN_union_ODD: shows "EVEN \<union> ODD = UNIV" + using even_or_odd proof - have "EVEN \<union> ODD = (\<lambda>n. atom n) ` {n. \<exists>i. n = 2*i} \<union> (\<lambda>n. atom n) ` {n. \<exists>i. n = 2*i+1}" by auto also have "\<dots> = (\<lambda>n. atom n) ` ({n. \<exists>i. n = 2*i} \<union> {n. \<exists>i. n = 2*i+1})" by auto @@ -69,7 +68,9 @@ apply(auto simp add: inj_on_def) done -(* A set S that is infinite and coinfinite has all atoms as its support *) +text {* + A set S that is infinite and coinfinite + has all atoms as its support. *} lemma supp_infinite_coinfinite: fixes S::"atom set" assumes a: "infinite S"

--- a/src/HOL/Nominal/Examples/VC_Compatible.thy Sun Oct 21 19:12:05 2007 +0200 +++ b/src/HOL/Nominal/Examples/VC_Compatible.thy Sun Oct 21 19:32:19 2007 +0200 @@ -5,17 +5,15 @@ begin text {* - We show here two examples where using the variable - convention carelessly in rule inductions, we end + We give here two examples that show if we use the variable + convention carelessly in rule inductions, we might 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. + 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. -*} + We define alpha-equated lambda-terms as usual. *} atom_decl name nominal_datatype lam = @@ -27,10 +25,9 @@ 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 + equivalence. However as a relation 'unbind' is ok and a similar relation has been used in our formalisation - of the algorithm W. -*} + of the algorithm W. *} inductive unbind :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _,_" [60,60,60] 60) where @@ -39,10 +36,9 @@ | u_lam: "t\<mapsto>xs,t' \<Longrightarrow> (Lam [x].t) \<mapsto> (x#xs),t'" text {* - We can show that Lam [x]. Lam [x]. Var x unbinds to [x,x],Var x + We can show that Lam [x].Lam [x].Var x unbinds to [x,x],Var x and also to [z,y],Var y (though the proof for the second is a - bit clumsy). -*} + bit clumsy). *} lemma unbind_lambda_lambda1: shows "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)" by (auto intro: unbind.intros) @@ -65,21 +61,21 @@ 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 + requires for rule u_lam to have the binder x being not a free variable in the rule's conclusion. Because this condition is not satisfied, - Isabelle will not derive a strong induction principle for unbind - - that means Isabelle does not allow you to use the variable - convention in induction proofs involving unbind. We can, however, - force Isabelle to derive the strengthening induction principle. -*} + 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 over 'unbind'. We can, however, + force Isabelle to derive the strengthening induction principle + and see what happens. *} + nominal_inductive unbind sorry text {* - To obtain our faulty lemma, we introduce the function 'bind' + To obtain a faulty lemma, we introduce the function 'bind' which takes a list of names and abstracts away these names in - a given lambda-term. -*} + a given lambda-term. *} fun bind :: "name list \<Rightarrow> lam \<Rightarrow> lam" where @@ -88,8 +84,7 @@ text {* Although not necessary for our main argument below, we can - easily prove that bind undoes the unbinding. -*} + easily prove that bind undoes the unbinding. *} lemma bind_unbind: assumes a: "t \<mapsto> xs,t'" shows "t = bind xs t'" @@ -99,8 +94,7 @@ The next lemma shows by induction on xs 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'. -*} + '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" @@ -111,13 +105,12 @@ 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. -*} + variable convention (i.e. our strong induction principle). + 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')" @@ -128,8 +121,8 @@ text {* Obviously the faulty lemma does not hold, for example, in case Lam [x].Lam [x].(Var x) \<mapsto> [x,x],(Var x). Therefore, - we can prove False. -*} + we can prove False. *} + lemma false1: shows "False" proof - @@ -145,8 +138,7 @@ text {* The next example is slightly simpler, but looks more contrived than 'unbind'. This example, caled 'strip' just - strips off the top-most binders from lambdas. -*} + strips off the top-most binders from lambdas. *} inductive strip :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<rightarrow> _" [60,60] 60) @@ -157,8 +149,8 @@ text {* The relation is equivariant but we have to use again - sorry to derive a strong induction principle. -*} + sorry to derive a strong induction principle. *} + equivariance strip nominal_inductive strip @@ -166,8 +158,8 @@ text {* The faulty lemma shows that a variable that is fresh - for a term is also fresh for the term after striping. -*} + for a term is also fresh for the term after striping. *} + lemma faulty2: fixes x::"name" assumes a: "t \<rightarrow> t'" @@ -177,8 +169,8 @@ (auto simp add: abs_fresh) text {* - Obviously Lam [x].Var x is a counter example to this lemma. -*} + Obviously Lam [x].Var x is a counter example to this lemma. *} + lemma false2: shows "False" proof -