--- 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