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

author | urbanc |

Tue, 01 Jan 2008 07:28:20 +0100 | |

changeset 25751 | a4e69ce247e0 |

parent 25750 | 4e796867ccb5 |

child 25752 | 374446e93558 |

tuned proofs and comments

--- a/src/HOL/Nominal/Examples/Contexts.thy Mon Dec 31 19:36:29 2007 +0100 +++ b/src/HOL/Nominal/Examples/Contexts.thy Tue Jan 01 07:28:20 2008 +0100 @@ -7,12 +7,12 @@ text {* We show here that the Plotkin-style of defining - reductions relation based on congruence rules is + reduction relations (based on congruence rules) is equivalent to the Felleisen-Hieb-style representation - based on contexts. + (based on contexts). - The interesting point is that contexts do not bind - anything. On the other hand the operation of replacing + The interesting point is that contexts do not contain + any binders. On the other hand the operation of filling a term into a context produces an alpha-equivalent term. *} @@ -25,14 +25,17 @@ | App "lam" "lam" | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) -text {* Contexts - the lambda case in contexts does not bind a name *} +text {* + Contexts - the lambda case in contexts does not bind a name + even if we introduce the nomtation [_]._ fro CLam. +*} nominal_datatype ctx = Hole | CAppL "ctx" "lam" | CAppR "lam" "ctx" | CLam "name" "ctx" ("CLam [_]._" [100,100] 100) -text {* Capture-avoiding substitution and three lemmas *} +text {* Capture-avoiding substitution and two lemmas *} consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) @@ -60,13 +63,13 @@ (auto simp add: abs_fresh fresh_prod fresh_atm) text {* - Replace is the operation that fills a term into a hole. While + Filling is the operation that fills a term into a hole. While contexts themselves are not alpha-equivalence classes, the filling operation produces an alpha-equivalent lambda-term. *} consts - replace :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_<_>" [100,100] 100) + filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_<_>" [100,100] 100) nominal_primrec "Hole<t> = t" @@ -75,12 +78,10 @@ "(CLam [x].E)<t> = Lam [x].(E<t>)" by (rule TrueI)+ - lemma alpha_test: shows "(CLam [x].Hole)<Var x> = (CLam [y].Hole)<Var y>" by (auto simp add: alpha lam.inject calc_atm fresh_atm) - lemma replace_eqvt[eqvt]: fixes pi:: "name prm" shows "pi\<bullet>(E<e>) = (pi\<bullet>E)<(pi\<bullet>e)>" @@ -95,7 +96,7 @@ (auto simp add: fresh_prod abs_fresh) -text {* Composition of two contexts *} +text {* The composition of two contexts *} consts ctx_replace :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<circ> _" [100,100] 100) @@ -118,7 +119,7 @@ by (induct E1 rule: ctx.weak_induct) (auto simp add: fresh_prod) -text {* Beta-reduction via contexts *} +text {* Beta-reduction via contexts in the Felleisen-Hieb style. *} inductive ctx_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>x _" [80,80] 80) @@ -130,7 +131,7 @@ nominal_inductive ctx_red by (simp_all add: replace_fresh subst_fresh abs_fresh) -text {* Beta-reduction via congruence rules *} +text {* Beta-reduction via congruence rules in the Plotkin style. *} inductive cong_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>o _" [80,80] 80) @@ -145,7 +146,7 @@ nominal_inductive cong_red by (simp_all add: subst_fresh abs_fresh) -text {* The proof that shows both relations are equal *} +text {* The proof that shows both relations are equal. *} lemma cong_red_ctx: assumes a: "t \<longrightarrow>o t'" @@ -179,7 +180,7 @@ apply(rule ctx_red_hole) apply(rule xbeta) apply(simp) -apply(metis ctx_red_ctx replace.simps)+ (* found by SledgeHammer *) +apply(metis ctx_red_ctx filling.simps)+ (* found by SledgeHammer *) done end

--- a/src/HOL/Nominal/Examples/Height.thy Mon Dec 31 19:36:29 2007 +0100 +++ b/src/HOL/Nominal/Examples/Height.thy Tue Jan 01 07:28:20 2008 +0100 @@ -1,10 +1,13 @@ (* $Id$ *) -(* Simple problem suggested by D. Wang *) +theory Height + imports "../Nominal" +begin -theory Height -imports "../Nominal" -begin +text {* + A trivial problem suggested by D. Wang. It shows how + the height of a lambda-terms behaves under substitution. +*} atom_decl name @@ -13,7 +16,7 @@ | App "lam" "lam" | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) -text {* definition of the height-function on lambda-terms *} +text {* Definition of the height-function on lambda-terms. *} consts height :: "lam \<Rightarrow> int" @@ -28,7 +31,7 @@ apply(fresh_guess add: perm_int_def)+ done -text {* definition of capture-avoiding substitution *} +text {* Definition of capture-avoiding substitution. *} consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) @@ -43,16 +46,16 @@ 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. *} lemma height_ge_one: shows "1 \<le> (height e)" -apply (nominal_induct e rule: lam.induct) -by simp_all +by (nominal_induct e rule: lam.induct) (simp_all) -text {* unlike the proplem suggested by Wang, however, the - theorem is here formulated entirely by using - functions *} +text {* + Unlike the proplem suggested by Wang, however, the + theorem is here formulated entirely by using functions. +*} theorem height_subst: shows "height (e[x::=e']) \<le> (((height e) - 1) + (height e'))"

--- a/src/HOL/Nominal/Examples/Lam_Funs.thy Mon Dec 31 19:36:29 2007 +0100 +++ b/src/HOL/Nominal/Examples/Lam_Funs.thy Tue Jan 01 07:28:20 2008 +0100 @@ -1,9 +1,11 @@ (* $Id$ *) theory Lam_Funs -imports "../Nominal" + imports "../Nominal" begin +text {* Defines some functions over lambda-terms *} + atom_decl name nominal_datatype lam = @@ -11,7 +13,7 @@ | App "lam" "lam" | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) -text {* depth of a lambda-term *} +text {* Depth of a lambda-term *} consts depth :: "lam \<Rightarrow> nat" @@ -26,7 +28,13 @@ apply(fresh_guess)+ done -text {* free variables of a lambda-term *} +text {* + Free variables of a lambda-term. The complication of this + function is the fact that it returns a name set, which is + not automatically a finitely supported type. So we have to + prove the invariant that frees always returns a finite set + of names. +*} consts frees :: "lam \<Rightarrow> name set" @@ -49,8 +57,7 @@ by (nominal_induct t rule: lam.induct) (simp_all add: lam.supp supp_atm abs_supp) -text {* capture-avoiding substitution *} - +text {* Capture-avoiding substitution *} consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) @@ -79,7 +86,7 @@ apply(blast)+ done -text{* parallel substitution *} +text{* Parallel substitution *} consts psubst :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam" ("_<_>" [100,100] 900)

--- a/src/HOL/Nominal/Examples/Support.thy Mon Dec 31 19:36:29 2007 +0100 +++ b/src/HOL/Nominal/Examples/Support.thy Tue Jan 01 07:28:20 2008 +0100 @@ -1,7 +1,7 @@ (* $Id$ *) theory Support -imports "../Nominal" + imports "../Nominal" begin text {* @@ -9,30 +9,33 @@ x\<sharp>(A \<union> B) does not imply x\<sharp>A and x\<sharp>B - 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. + For this we set A to the set of even atoms and B to the + set of odd atoms. Then A \<union> 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 +text {* The set of even atoms. *} abbreviation EVEN :: "atom set" where "EVEN \<equiv> {atom n | n. \<exists>i. n=2*i}" +text {* The set of odd atoms: *} abbreviation ODD :: "atom set" where "ODD \<equiv> {atom n | n. \<exists>i. n=2*i+1}" +text {* An atom is either even or odd. *} lemma even_or_odd: fixes n::"nat" shows "\<exists>i. (n = 2*i) \<or> (n=2*i+1)" by (induct n) (presburger)+ +text {* The union of even and odd atoms is the set of all atoms. *} lemma EVEN_union_ODD: shows "EVEN \<union> ODD = UNIV" using even_or_odd @@ -46,31 +49,41 @@ finally show "EVEN \<union> ODD = UNIV" by simp qed +text {* The sets of even and odd atoms are disjunct. *} lemma EVEN_intersect_ODD: shows "EVEN \<inter> ODD = {}" using even_or_odd by (auto) (presburger) +text {* + The preceeding two lemmas help us to prove + the following two useful equalities: +*} lemma UNIV_subtract: shows "UNIV - EVEN = ODD" and "UNIV - ODD = EVEN" using EVEN_union_ODD EVEN_intersect_ODD by (blast)+ +text {* The sets EVEN and ODD are infinite. *} lemma EVEN_ODD_infinite: shows "infinite EVEN" and "infinite ODD" -apply(simp add: infinite_iff_countable_subset) -apply(rule_tac x="\<lambda>n. atom (2*n)" in exI) -apply(auto simp add: inj_on_def)[1] -apply(simp add: infinite_iff_countable_subset) -apply(rule_tac x="\<lambda>n. atom (2*n+1)" in exI) -apply(auto simp add: inj_on_def) -done +unfolding infinite_iff_countable_subset +proof - + let ?f = "\<lambda>n. atom (2*n)" + have "inj ?f \<and> range ?f \<subseteq> EVEN" by (auto simp add: inj_on_def) + then show "\<exists>f::nat\<Rightarrow>atom. inj f \<and> range f \<subseteq> EVEN" by (rule_tac exI) +next + let ?f = "\<lambda>n. atom (2*n+1)" + have "inj ?f \<and> range ?f \<subseteq> ODD" by (auto simp add: inj_on_def) + then show "\<exists>f::nat\<Rightarrow>atom. inj f \<and> range f \<subseteq> ODD" by (rule_tac exI) +qed text {* - A set S that is infinite and coinfinite - has all atoms as its support. *} + A general fact: a set S that is both infinite and coinfinite + has all atoms as its support. +*} lemma supp_infinite_coinfinite: fixes S::"atom set" assumes a: "infinite S" @@ -100,21 +113,26 @@ then show "(supp S) = (UNIV::atom set)" by auto qed +text {* As a corollary we get that EVEN and ODD have infinite support. *} lemma EVEN_ODD_supp: shows "supp EVEN = (UNIV::atom set)" and "supp ODD = (UNIV::atom set)" using supp_infinite_coinfinite UNIV_subtract EVEN_ODD_infinite by simp_all +text {* + The set of all atoms has empty support, since any swappings leaves + this set unchanged. +*} lemma UNIV_supp: shows "supp (UNIV::atom set) = ({}::atom set)" proof - have "\<forall>(x::atom) (y::atom). [(x,y)]\<bullet>UNIV = (UNIV::atom set)" by (auto simp add: perm_set_def calc_atm) - then show "supp (UNIV::atom set) = ({}::atom set)" - by (simp add: supp_def) + then show "supp (UNIV::atom set) = ({}::atom set)" by (simp add: supp_def) qed +text {* Putting everything together. *} theorem EVEN_ODD_freshness: fixes x::"atom" shows "x\<sharp>(EVEN \<union> ODD)"

--- a/src/HOL/Nominal/Examples/VC_Condition.thy Mon Dec 31 19:36:29 2007 +0100 +++ b/src/HOL/Nominal/Examples/VC_Condition.thy Tue Jan 01 07:28:20 2008 +0100 @@ -9,11 +9,10 @@ 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. + nominal data package one is protected from such bogus reasoning. *} -text {* - We define alpha-equated lambda-terms as usual. *} +text {* We define alpha-equated lambda-terms as usual. *} atom_decl name nominal_datatype lam = @@ -60,21 +59,20 @@ text {* ... but it is not variable-convention compatible (see Urban, - Berghofer, Norrish [2007] for more details). This condition - 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 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. *} + Berghofer, Norrish [2007]). This condition requires for rule u_lam to + have the binder x not being a free variable in this 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 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 a faulty lemma, we introduce the function 'bind' - which takes a list of names and abstracts away these names in + which takes a list of names and abstracts them away in a given lambda-term. *} fun bind :: "name list \<Rightarrow> lam \<Rightarrow> lam" @@ -104,7 +102,7 @@ (auto simp add: fresh_list_cons abs_fresh fresh_atm) text {* - Now comes the faulty lemma. It is derived using the + 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', and x is a free variable in t', then it is also a free @@ -119,10 +117,10 @@ (simp_all add: free_variable) 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. *} - + Obviously this lemma is bogus. For example, in + case Lam [x].Lam [x].(Var x) \<mapsto> [x,x],(Var x). + As a result, we can prove False. +*} lemma false1: shows "False" proof - @@ -137,7 +135,7 @@ text {* The next example is slightly simpler, but looks more - contrived than 'unbind'. This example, caled 'strip' just + contrived than 'unbind'. This example, called 'strip' just strips off the top-most binders from lambdas. *} inductive @@ -149,17 +147,17 @@ 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 sorry text {* - The faulty lemma shows that a variable that is fresh - for a term is also fresh for the term after striping. *} - + The second faulty lemma shows that a variable being fresh + for a term is also fresh for this term after striping. +*} lemma faulty2: fixes x::"name" assumes a: "t \<rightarrow> t'" @@ -168,9 +166,7 @@ by (nominal_induct t t'\<equiv>t' avoiding: t' rule: strip.strong_induct) (auto simp add: abs_fresh) -text {* - Obviously Lam [x].Var x is a counter example to this lemma. *} - +text {* Obviously Lam [x].Var x is a counter example to this lemma. *} lemma false2: shows "False" proof -

--- a/src/HOL/Nominal/Examples/Weakening.thy Mon Dec 31 19:36:29 2007 +0100 +++ b/src/HOL/Nominal/Examples/Weakening.thy Tue Jan 01 07:28:20 2008 +0100 @@ -4,11 +4,11 @@ imports "../Nominal" begin -section {* Weakening Example for the Simply-Typed Lambda-Calculus *} +section {* Weakening Property in the Simply-Typed Lambda-Calculus *} atom_decl name -text {* Terms and types *} +text {* Terms and Types *} nominal_datatype lam = Var "name" | App "lam" "lam" @@ -48,7 +48,7 @@ text {* We derive the strong induction principle for the typing relation (this induction principle has the variable convention - already built in). + already built-in). *} equivariance typing nominal_inductive typing @@ -144,6 +144,7 @@ oops text{* The complete proof without using the variable convention. *} + lemma weakening_with_explicit_renaming: fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list" assumes a: "\<Gamma>1 \<turnstile> t : T" @@ -189,9 +190,9 @@ qed (auto) text {* - Compare the proof with explicit renamings to version1 and version2, - and imagine you are proving something more substantial than the - weakening lemma. + Moral: compare the proof with explicit renamings to version1 and version2, + and imagine you are proving something more substantial than the weakening + lemma. *} end \ No newline at end of file