--- a/src/HOL/Nominal/Examples/CR_Takahashi.thy Sun Feb 10 20:49:48 2008 +0100
+++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy Mon Feb 11 15:19:17 2008 +0100
@@ -45,13 +45,13 @@
by (nominal_induct t avoiding: x s rule: lam.induct)
(auto simp add: abs_fresh fresh_atm)
-lemma fresh_fact:
+lemma fresh_fact1:
fixes z::"name"
shows "z\<sharp>(t,s) \<Longrightarrow> z\<sharp>t[y::=s]"
by (nominal_induct t avoiding: z y s rule: lam.induct)
(auto simp add: abs_fresh fresh_prod fresh_atm)
-lemma fresh_fact':
+lemma fresh_fact2:
fixes x::"name"
shows "x\<sharp>s \<Longrightarrow> x\<sharp>t[x::=s]"
by (nominal_induct t avoiding: x s rule: lam.induct)
@@ -61,7 +61,7 @@
assumes a: "x\<noteq>y" "x\<sharp>u"
shows "t[x::=s][y::=u] = t[y::=u][x::=s[y::=u]]"
using a by (nominal_induct t avoiding: x y s u rule: lam.induct)
- (auto simp add: fresh_fact forget)
+ (auto simp add: fresh_fact1 forget)
lemma subst_rename:
assumes a: "y\<sharp>t"
@@ -100,7 +100,7 @@
equivariance One
nominal_inductive One
- by (simp_all add: abs_fresh fresh_fact')
+ by (simp_all add: abs_fresh fresh_fact2)
lemma One_refl:
shows "t \<longrightarrow>\<^isub>1 t"
@@ -110,7 +110,7 @@
assumes a: "t1 \<longrightarrow>\<^isub>1 t2" "s1 \<longrightarrow>\<^isub>1 s2"
shows "t1[x::=s1] \<longrightarrow>\<^isub>1 t2[x::=s2]"
using a by (nominal_induct t1 t2 avoiding: s1 s2 x rule: One.strong_induct)
- (auto simp add: substitution_lemma fresh_atm fresh_fact)
+ (auto simp add: substitution_lemma fresh_atm fresh_fact1)
lemma better_o4_intro:
assumes a: "t1 \<longrightarrow>\<^isub>1 t2" "s1 \<longrightarrow>\<^isub>1 s2"
@@ -127,27 +127,27 @@
lemma One_Var:
assumes a: "Var x \<longrightarrow>\<^isub>1 M"
shows "M = Var x"
-using a by (erule_tac One.cases) (simp_all)
+using a by (cases rule: One.cases) (simp_all)
lemma One_Lam:
assumes a: "Lam [x].t \<longrightarrow>\<^isub>1 s" "x\<sharp>s"
shows "\<exists>t'. s = Lam [x].t' \<and> t \<longrightarrow>\<^isub>1 t'"
using a
-by (cases rule: One.strong_cases[where x="x" and xa="x"])
+by (cases rule: One.strong_cases)
(auto simp add: lam.inject abs_fresh alpha)
lemma One_App:
assumes a: "App t s \<longrightarrow>\<^isub>1 r"
shows "(\<exists>t' s'. r = App t' s' \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s') \<or>
(\<exists>x p p' s'. r = p'[x::=s'] \<and> t = Lam [x].p \<and> p \<longrightarrow>\<^isub>1 p' \<and> s \<longrightarrow>\<^isub>1 s' \<and> x\<sharp>(s,s'))"
-using a by (erule_tac One.cases) (auto simp add: lam.inject)
+using a by (cases rule: One.cases) (auto simp add: lam.inject)
lemma One_Redex:
assumes a: "App (Lam [x].t) s \<longrightarrow>\<^isub>1 r" "x\<sharp>(s,r)"
shows "(\<exists>t' s'. r = App (Lam [x].t') s' \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s') \<or>
(\<exists>t' s'. r = t'[x::=s'] \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s')"
using a
-by (cases rule: One.strong_cases [where x="x" and xa="x"])
+by (cases rule: One.strong_cases)
(auto dest: One_Lam simp add: lam.inject abs_fresh alpha fresh_prod)
section {* Transitive Closure of One *}
@@ -171,7 +171,7 @@
equivariance Dev
nominal_inductive Dev
- by (simp_all add: abs_fresh fresh_fact')
+ by (simp_all add: abs_fresh fresh_fact2)
lemma better_d4_intro:
assumes a: "t1 \<longrightarrow>\<^isub>d t2" "s1 \<longrightarrow>\<^isub>d s2"
@@ -189,8 +189,8 @@
fixes x::"name"
assumes a: "M\<longrightarrow>\<^isub>d N"
shows "x\<sharp>M \<Longrightarrow> x\<sharp>N"
-using a
-by (induct) (auto simp add: abs_fresh fresh_fact fresh_fact')
+using a
+by (induct) (auto simp add: abs_fresh fresh_fact1 fresh_fact2)
lemma Dev_Lam:
assumes a: "Lam [x].M \<longrightarrow>\<^isub>d N"
@@ -198,8 +198,8 @@
proof -
from a have "x\<sharp>Lam [x].M" by (simp add: abs_fresh)
with a have "x\<sharp>N" by (simp add: Dev_preserves_fresh)
- with a show ?thesis
- by (cases rule: Dev.strong_cases [where x="x" and xa="x"])
+ with a show "\<exists>N'. N = Lam [x].N' \<and> M \<longrightarrow>\<^isub>d N'"
+ by (cases rule: Dev.strong_cases)
(auto simp add: lam.inject abs_fresh alpha)
qed
@@ -213,10 +213,8 @@
shows "t2 \<longrightarrow>\<^isub>1 t1"
using a
apply(nominal_induct avoiding: t2 rule: Dev.strong_induct)
-apply(auto dest!: One_Var)[1]
-apply(auto dest!: One_Lam)[1]
-apply(auto dest!: One_App)[1]
-apply(auto dest!: One_Redex intro: One_subst)[1]
+apply(auto dest!: One_Var One_Lam One_App)[3]
+apply(auto dest!: One_Redex intro: One_subst)
done
lemma Diamond_for_One:
@@ -245,20 +243,16 @@
shows "Lam [x].t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam [x].t2"
using a by (induct) (blast)+
-lemma Beta_App_congL:
+lemma Beta_App_cong_aux:
assumes a: "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2"
shows "App t1 s\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s"
-using a by (induct) (blast)+
-
-lemma Beta_App_congR:
- assumes a: "s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* s2"
- shows "App t s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t s2"
+ and "App s t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App s t2"
using a by (induct) (blast)+
lemma Beta_App_cong:
assumes a: "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" "s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* s2"
shows "App t1 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2"
-using a by (blast intro: Beta_App_congL Beta_App_congR)
+using a by (blast intro: Beta_App_cong_aux)
lemmas Beta_congs = Beta_Lam_cong Beta_App_cong
@@ -272,17 +266,13 @@
shows "Lam [x].t1 \<longrightarrow>\<^isub>1\<^sup>* Lam [x].t2"
using a by (induct) (auto)
-lemma One_star_App_congL:
+lemma One_star_App_cong:
assumes a: "t1 \<longrightarrow>\<^isub>1\<^sup>* t2"
- shows "App t1 s\<longrightarrow>\<^isub>1\<^sup>* App t2 s"
+ shows "App t1 s \<longrightarrow>\<^isub>1\<^sup>* App t2 s"
+ and "App s t1 \<longrightarrow>\<^isub>1\<^sup>* App s t2"
using a by (induct) (auto intro: One_refl)
-lemma One_star_App_congR:
- assumes a: "s1 \<longrightarrow>\<^isub>1\<^sup>* s2"
- shows "App t s1 \<longrightarrow>\<^isub>1\<^sup>* App t s2"
-using a by (induct) (auto intro: One_refl)
-
-lemmas One_congs = One_star_App_congL One_star_App_congR One_star_Lam_cong
+lemmas One_congs = One_star_App_cong One_star_Lam_cong
lemma Beta_implies_One_star:
assumes a: "t1 \<longrightarrow>\<^isub>\<beta> t2"
@@ -305,9 +295,9 @@
assumes a: "t \<longrightarrow>\<^isub>\<beta>\<^sup>* t1" "t\<longrightarrow>\<^isub>\<beta>\<^sup>* t2"
shows "\<exists>t3. t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3 \<and> t2 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3"
proof -
- from a have "t \<longrightarrow>\<^isub>1\<^sup>* t1" and "t\<longrightarrow>\<^isub>1\<^sup>* t2" by (simp_all only: Beta_star_equals_One_star)
- then have "\<exists>t3. t1 \<longrightarrow>\<^isub>1\<^sup>* t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by (rule_tac CR_for_One_star)
- then show "\<exists>t3. t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3 \<and> t2 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3" by (simp only: Beta_star_equals_One_star)
+ from a have "t \<longrightarrow>\<^isub>1\<^sup>* t1" and "t\<longrightarrow>\<^isub>1\<^sup>* t2" by (simp_all add: Beta_star_equals_One_star)
+ then have "\<exists>t3. t1 \<longrightarrow>\<^isub>1\<^sup>* t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by (simp add: CR_for_One_star)
+ then show "\<exists>t3. t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3 \<and> t2 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3" by (simp add: Beta_star_equals_One_star)
qed
end
--- a/src/HOL/Nominal/Examples/Support.thy Sun Feb 10 20:49:48 2008 +0100
+++ b/src/HOL/Nominal/Examples/Support.thy Mon Feb 11 15:19:17 2008 +0100
@@ -9,10 +9,11 @@
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 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.
+ 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 \<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
@@ -35,7 +36,9 @@
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. *}
+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. *}
lemma EVEN_union_ODD:
shows "EVEN \<union> ODD = UNIV"
using even_or_odd
@@ -57,8 +60,8 @@
text {*
The preceeding two lemmas help us to prove
- the following two useful equalities:
-*}
+ the following two useful equalities: *}
+
lemma UNIV_subtract:
shows "UNIV - EVEN = ODD"
and "UNIV - ODD = EVEN"
@@ -81,9 +84,10 @@
qed
text {*
- A general fact: a set S that is both infinite and coinfinite
- has all atoms as its support.
-*}
+ A general fact about a set S of names that is both infinite and
+ coinfinite. Then S has all atoms as its support. Steve Zdancewick
+ helped with proving this fact. *}
+
lemma supp_infinite_coinfinite:
fixes S::"atom set"
assumes asm1: "infinite S"
@@ -122,8 +126,8 @@
text {*
The set of all atoms has empty support, since any swappings leaves
- this set unchanged.
-*}
+ this set unchanged. *}
+
lemma UNIV_supp:
shows "supp (UNIV::atom set) = ({}::atom set)"
proof -
@@ -140,4 +144,6 @@
and "\<not>x\<sharp>ODD"
by (auto simp only: fresh_def EVEN_union_ODD EVEN_ODD_supp UNIV_supp)
+text {* Moral: support is a sublte notion. *}
+
end
\ No newline at end of file
--- a/src/HOL/Nominal/Examples/VC_Condition.thy Sun Feb 10 20:49:48 2008 +0100
+++ b/src/HOL/Nominal/Examples/VC_Condition.thy Mon Feb 11 15:19:17 2008 +0100
@@ -27,6 +27,7 @@
equivalence. However as a relation 'unbind' is ok and
a similar relation has been used in our formalisation
of the algorithm W. *}
+
inductive
unbind :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _,_" [60,60,60] 60)
where
@@ -38,6 +39,7 @@
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). *}
+
lemma unbind_lambda_lambda1:
shows "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)"
by (auto intro: unbind.intros)
@@ -74,6 +76,7 @@
To obtain a faulty lemma, we introduce the function 'bind'
which takes a list of names and abstracts them away in
a given lambda-term. *}
+
fun
bind :: "name list \<Rightarrow> lam \<Rightarrow> lam"
where
@@ -83,6 +86,7 @@
text {*
Although not necessary for our main argument below, we can
easily prove that bind undoes the unbinding. *}
+
lemma bind_unbind:
assumes a: "t \<mapsto> xs,t'"
shows "t = bind xs t'"
@@ -93,6 +97,7 @@
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'. *}
+
lemma free_variable:
fixes x::"name"
assumes a: "\<not>(x\<sharp>t)" and b: "x\<sharp>xs"
@@ -119,8 +124,8 @@
text {*
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.
-*}
+ As a result, we can prove False. *}
+
lemma false1:
shows "False"
proof -
@@ -147,8 +152,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
@@ -156,8 +161,8 @@
text {*
The second faulty lemma shows that a variable being fresh
- for a term is also fresh for this term after striping.
-*}
+ for a term is also fresh for this term after striping. *}
+
lemma faulty2:
fixes x::"name"
assumes a: "t \<rightarrow> t'"
@@ -167,6 +172,7 @@
(auto simp add: abs_fresh)
text {* Obviously Lam [x].Var x is a counter example to this lemma. *}
+
lemma false2:
shows "False"
proof -
@@ -176,5 +182,11 @@
ultimately have "x\<sharp>(Var x)" by (simp only: faulty2)
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.
+ *}
+
end
\ No newline at end of file
--- a/src/HOL/Nominal/Examples/Weakening.thy Sun Feb 10 20:49:48 2008 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy Mon Feb 11 15:19:17 2008 +0100
@@ -4,11 +4,15 @@
imports "../Nominal"
begin
-section {* Weakening Property in the Simply-Typed Lambda-Calculus *}
+text {*
+ A simple proof of the Weakening Property in the simply-typed
+ lambda-calculus. The proof is simple, because we can make use
+ of the variable convention. *}
atom_decl name
text {* Terms and Types *}
+
nominal_datatype lam =
Var "name"
| App "lam" "lam"
@@ -27,8 +31,8 @@
text {*
Valid contexts (at the moment we have no type for finite
- sets yet; therefore typing-contexts are lists).
- *}
+ sets yet, therefore typing-contexts are lists). *}
+
inductive
valid :: "(name\<times>ty) list \<Rightarrow> bool"
where
@@ -38,6 +42,7 @@
equivariance valid
text{* Typing judgements *}
+
inductive
typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60)
where
@@ -48,13 +53,14 @@
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
by (simp_all add: abs_fresh ty_fresh)
text {* Abbreviation for the notion of subcontexts. *}
+
abbreviation
"sub_context" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60)
where
@@ -62,10 +68,10 @@
text {* Now it comes: The Weakening Lemma *}
-text {*
+text {*
The first version is, after setting up the induction,
- completely automatic except for use of atomize.
- *}
+ completely automatic except for use of atomize. *}
+
lemma weakening_version1:
fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
assumes a: "\<Gamma>1 \<turnstile> t : T"
@@ -77,9 +83,9 @@
(auto | atomize)+
text {*
- The second version gives all details for the variable
- and lambda case.
- *}
+ The second version gives the details for the variable
+ and lambda case. *}
+
lemma weakening_version2:
fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
and t ::"lam"
@@ -113,8 +119,8 @@
text{*
The original induction principle for the typing relation
is not strong enough - even this simple lemma fails to be
- simple ;o)
- *}
+ simple ;o) *}
+
lemma weakening_not_straigh_forward:
fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
assumes a: "\<Gamma>1 \<turnstile> t : T"
@@ -143,7 +149,11 @@
have "valid ((x,T1)#\<Gamma>2)" using v2 (* fails *)
oops
-text{* The complete proof without using the variable convention. *}
+text{*
+ To show that the proof is not simple, here proof without using
+ the variable convention.
+
+*}
lemma weakening_with_explicit_renaming:
fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
@@ -190,9 +200,8 @@
qed (auto)
text {*
- Moral: 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 weakening_version1
+ and weakening_version2, and imagine you are proving something more substantial
+ than the weakening lemma. *}
end
\ No newline at end of file