# HG changeset patch # User urbanc # Date 1205319432 -3600 # Node ID f5cb9602145f71548a6598ee1986d202f1d78041 # Parent b6a103ace4db1a9cd3e37cd6ccaa5124fcc50caf tuned diff -r b6a103ace4db -r f5cb9602145f src/HOL/Nominal/Examples/Height.thy --- a/src/HOL/Nominal/Examples/Height.thy Wed Mar 12 08:47:37 2008 +0100 +++ b/src/HOL/Nominal/Examples/Height.thy Wed Mar 12 11:57:12 2008 +0100 @@ -5,7 +5,7 @@ begin text {* - A trivial problem suggested by D. Wang. It shows how + A small problem suggested by D. Wang. It shows how the height of a lambda-terms behaves under substitution. *} @@ -17,7 +17,6 @@ | Lam "\name\lam" ("Lam [_]._" [100,100] 100) text {* Definition of the height-function on lambda-terms. *} - consts height :: "lam \ int" @@ -46,7 +45,7 @@ apply(fresh_guess)+ done -text{* The next lemma is needed in the Var-case of the theorem. *} +text{* The next lemma is needed in the Var-case of the theorem below. *} lemma height_ge_one: shows "1 \ (height e)" @@ -54,26 +53,46 @@ text {* Unlike the proplem suggested by Wang, however, the - theorem is here formulated entirely by using functions. + theorem is here formulated entirely by using functions. *} theorem height_subst: - shows "height (e[x::=e']) \ (((height e) - 1) + (height e'))" + shows "height (e[x::=e']) \ ((height e) - 1) + (height e')" proof (nominal_induct e avoiding: x e' rule: lam.induct) case (Var y) have "1 \ height e'" by (rule height_ge_one) then show "height (Var y[x::=e']) \ height (Var y) - 1 + height e'" by simp next case (Lam y e1) - hence ih: "height (e1[x::=e']) \ (((height e1) - 1) + (height e'))" by simp + hence ih: "height (e1[x::=e']) \ ((height e1) - 1) + (height e')" by simp moreover have vc: "y\x" "y\e'" by fact+ (* usual variable convention *) ultimately show "height ((Lam [y].e1)[x::=e']) \ height (Lam [y].e1) - 1 + height e'" by simp next case (App e1 e2) - hence ih1: "height (e1[x::=e']) \ (((height e1) - 1) + (height e'))" - and ih2: "height (e2[x::=e']) \ (((height e2) - 1) + (height e'))" by simp_all + hence ih1: "height (e1[x::=e']) \ ((height e1) - 1) + (height e')" + and ih2: "height (e2[x::=e']) \ ((height e2) - 1) + (height e')" by simp_all then show "height ((App e1 e2)[x::=e']) \ height (App e1 e2) - 1 + height e'" by simp qed +theorem height_subst: + shows "height (e[x::=e']) \ ((height e) - 1) + (height e')" +proof (nominal_induct e avoiding: x e' rule: lam.induct) + case (Var y) + have "1 \ height e'" by (rule height_ge_one) + then show "height (Var y[x::=e']) \ height (Var y) - 1 + height e'" by simp +next + case (Lam y e1) + hence ih: "height (e1[x::=e']) \ ((height e1) - 1) + (height e')" by simp + moreover + have vc: "y\x" "y\e'" by fact+ (* usual variable convention *) + ultimately show "height ((Lam [y].e1)[x::=e']) \ height (Lam [y].e1) - 1 + height e'" by simp +next + case (App e1 e2) + hence ih1: "height (e1[x::=e']) \ ((height e1) - 1) + (height e')" + and ih2: "height (e2[x::=e']) \ ((height e2) - 1) + (height e')" by simp_all + then show "height ((App e1 e2)[x::=e']) \ height (App e1 e2) - 1 + height e'" by simp +qed + + end diff -r b6a103ace4db -r f5cb9602145f src/HOL/Nominal/Examples/Support.thy --- a/src/HOL/Nominal/Examples/Support.thy Wed Mar 12 08:47:37 2008 +0100 +++ b/src/HOL/Nominal/Examples/Support.thy Wed Mar 12 11:57:12 2008 +0100 @@ -9,11 +9,10 @@ x\(A \ B) does not imply x\A and x\B - with A and B being sets. For this we set A to the set of - even atoms and B to the set of odd atoms. Then A \ B, that - is the set of all atoms, has empty support. The sets A, - respectively B, however have the set of all atoms as - their support. + For this we set A to the set of even atoms and B to + the set of odd atoms. Then A \ B, that is the set of + all atoms, has empty support. The sets A, respectively B, + however have the set of all atoms as their support. *} atom_decl atom @@ -38,7 +37,7 @@ text {* The union of even and odd atoms is the set of all atoms. - Unfortunately I do not know a simpler proof of this fact. *} + (Unfortunately I do not know a simpler proof of this fact.) *} lemma EVEN_union_ODD: shows "EVEN \ ODD = UNIV" using even_or_odd @@ -84,7 +83,7 @@ qed text {* - A general fact about a set S of names that is both infinite and + A general fact about a set S of atoms that is both infinite and coinfinite. Then S has all atoms as its support. Steve Zdancewick helped with proving this fact. *} diff -r b6a103ace4db -r f5cb9602145f src/HOL/Nominal/Examples/VC_Condition.thy --- a/src/HOL/Nominal/Examples/VC_Condition.thy Wed Mar 12 08:47:37 2008 +0100 +++ b/src/HOL/Nominal/Examples/VC_Condition.thy Wed Mar 12 11:57:12 2008 +0100 @@ -5,7 +5,7 @@ begin text {* - We give here two examples that show if we use the variable + We give here two examples showing that 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 @@ -109,7 +109,7 @@ text {* Now comes the first faulty lemma. It is derived using the variable convention (i.e. our strong induction principle). - This faulty lemma states that if t unbinds to x::xs and t', + 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. *} @@ -183,30 +183,27 @@ then show "False" by (simp add: fresh_atm) qed -text {* - Moral: Who would have thought that the variable convention - is in general an unsound reasoning principle. - *} - - -text - {* BTW: A similar effect can be achieved by using naive (that - is strong) inversion rules. *} +text {* A similar effect can be achieved by using naive inversion + on rules. *} lemma false3: shows "False" proof - have "Lam [x].(Var x) \ (Var x)" by (auto intro: strip.intros) - moreover obtain y::name where y: "y\x" - by (rule exists_fresh) (rule fin_supp) + moreover obtain y::"name" where fc: "y\x" by (rule exists_fresh) (rule fin_supp) then have "Lam [x].(Var x) = Lam [y].(Var y)" by (simp add: lam.inject alpha calc_atm fresh_atm) ultimately have "Lam [y].(Var y) \ (Var x)" by simp - then have "Var y \ Var x" using y - by (cases rule: strip.strong_cases [where x=y]) + then have "Var y \ Var x" using fc + by (cases rule: strip.strong_cases[where x=y]) (simp_all add: lam.inject alpha abs_fresh) - then show "False" using y + then show "False" using fc by (cases) (simp_all add: lam.inject fresh_atm) qed +text {* + Moral: Who would have thought that the variable convention + is in general an unsound reasoning principle. + *} + end \ No newline at end of file diff -r b6a103ace4db -r f5cb9602145f src/HOL/Nominal/Examples/Weakening.thy --- a/src/HOL/Nominal/Examples/Weakening.thy Wed Mar 12 08:47:37 2008 +0100 +++ b/src/HOL/Nominal/Examples/Weakening.thy Wed Mar 12 11:57:12 2008 +0100 @@ -150,8 +150,10 @@ oops text{* - To show that the proof is not simple, here proof without using - the variable convention. + To show that the proof with explicit renaming is not simple, + here is the proof without using the variable convention. It + crucially depends on the equivariance property of the typing + relation. *} @@ -197,7 +199,7 @@ then show "\2 \ Lam [c].([(c,x)]\t) : T1 \ T2" using fc1 by auto qed ultimately show "\2 \ Lam [x].t : T1 \ T2" by simp -qed (auto) +qed (auto) (* var and app cases *) text {* Moral: compare the proof with explicit renamings to weakening_version1