# HG changeset patch # User urbanc # Date 1199168900 -3600 # Node ID a4e69ce247e0d5e748816bfcb2b098b74ea76aa4 # Parent 4e796867ccb5fabdb8f82f9d42ec4e0322ba9833 tuned proofs and comments diff -r 4e796867ccb5 -r a4e69ce247e0 src/HOL/Nominal/Examples/Contexts.thy --- 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 "\name\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 \ name \ lam \ 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 \ lam \ lam" ("_<_>" [100,100] 100) + filling :: "ctx \ lam \ lam" ("_<_>" [100,100] 100) nominal_primrec "Hole = t" @@ -75,12 +78,10 @@ "(CLam [x].E) = Lam [x].(E)" by (rule TrueI)+ - lemma alpha_test: shows "(CLam [x].Hole) = (CLam [y].Hole)" by (auto simp add: alpha lam.inject calc_atm fresh_atm) - lemma replace_eqvt[eqvt]: fixes pi:: "name prm" shows "pi\(E) = (pi\E)<(pi\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 \ ctx \ ctx" ("_ \ _" [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\lam\bool" ("_ \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\lam\bool" ("_ \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 \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 diff -r 4e796867ccb5 -r a4e69ce247e0 src/HOL/Nominal/Examples/Height.thy --- 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 "\name\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 \ 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 \ name \ lam \ 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 \ (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']) \ (((height e) - 1) + (height e'))" diff -r 4e796867ccb5 -r a4e69ce247e0 src/HOL/Nominal/Examples/Lam_Funs.thy --- 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 "\name\lam" ("Lam [_]._" [100,100] 100) -text {* depth of a lambda-term *} +text {* Depth of a lambda-term *} consts depth :: "lam \ 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 \ 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 \ name \ lam \ lam" ("_[_::=_]" [100,100,100] 100) @@ -79,7 +86,7 @@ apply(blast)+ done -text{* parallel substitution *} +text{* Parallel substitution *} consts psubst :: "(name\lam) list \ lam \ lam" ("_<_>" [100,100] 900) diff -r 4e796867ccb5 -r a4e69ce247e0 src/HOL/Nominal/Examples/Support.thy --- 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\(A \ B) does not imply x\A and x\B - For this we set A to the set of even atoms - and B to the set of odd even atoms. Then A \ 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 \ 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 \ {atom n | n. \i. n=2*i}" +text {* The set of odd atoms: *} abbreviation ODD :: "atom set" where "ODD \ {atom n | n. \i. n=2*i+1}" +text {* An atom is either even or odd. *} lemma even_or_odd: fixes n::"nat" shows "\i. (n = 2*i) \ (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 \ ODD = UNIV" using even_or_odd @@ -46,31 +49,41 @@ finally show "EVEN \ ODD = UNIV" by simp qed +text {* The sets of even and odd atoms are disjunct. *} lemma EVEN_intersect_ODD: shows "EVEN \ 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="\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="\n. atom (2*n+1)" in exI) -apply(auto simp add: inj_on_def) -done +unfolding infinite_iff_countable_subset +proof - + let ?f = "\n. atom (2*n)" + have "inj ?f \ range ?f \ EVEN" by (auto simp add: inj_on_def) + then show "\f::nat\atom. inj f \ range f \ EVEN" by (rule_tac exI) +next + let ?f = "\n. atom (2*n+1)" + have "inj ?f \ range ?f \ ODD" by (auto simp add: inj_on_def) + then show "\f::nat\atom. inj f \ range f \ 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 "\(x::atom) (y::atom). [(x,y)]\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\(EVEN \ ODD)" diff -r 4e796867ccb5 -r a4e69ce247e0 src/HOL/Nominal/Examples/VC_Condition.thy --- 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 \ lam \ 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) \ [x,x],(Var x). Therefore, - we can prove False. *} - + Obviously this lemma is bogus. For example, in + case Lam [x].Lam [x].(Var x) \ [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 \ t'" @@ -168,9 +166,7 @@ by (nominal_induct t t'\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 - diff -r 4e796867ccb5 -r a4e69ce247e0 src/HOL/Nominal/Examples/Weakening.thy --- 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 \1 \2::"(name\ty) list" assumes a: "\1 \ 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