corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
--- a/Nominal/Test.thy Thu Mar 18 15:32:49 2010 +0100
+++ b/Nominal/Test.thy Thu Mar 18 16:22:10 2010 +0100
@@ -62,7 +62,7 @@
fixes c::"'a::fs"
assumes a1: "\<And>name c. P c (Vr name)"
and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
- and a3: "\<And>name lm c. \<lbrakk>\<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
+ and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
shows "P c lm"
proof -
have "\<And>p. P c (p \<bullet> lm)"
@@ -87,6 +87,7 @@
apply(simp add: fresh_Pair)
apply(simp)
apply(rule a3)
+ apply(simp add: fresh_Pair)
apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
apply(simp)
apply(simp add: fresh_def)
@@ -99,6 +100,38 @@
qed
+lemma
+ fixes c::"'a::fs"
+ assumes a1: "\<And>name c. P c (Vr name)"
+ and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)"
+ and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)"
+ shows "P c lm"
+proof -
+ have "\<And>p. P c (p \<bullet> lm)"
+ apply(induct lm arbitrary: c rule: lm_induct)
+ apply(simp only: lm_perm)
+ apply(rule a1)
+ apply(simp only: lm_perm)
+ apply(rule a2)
+ apply(blast)[1]
+ apply(assumption)
+ thm at_set_avoiding
+ apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q")
+ apply(erule exE)
+ apply(rule_tac t="p \<bullet> Lm name lm" and
+ s="q \<bullet> p \<bullet> Lm name lm" in subst)
+ defer
+ apply(simp add: lm_perm)
+ apply(rule a3)
+ apply(simp add: eqvts fresh_star_def)
+ apply(drule_tac x="q + p" in meta_spec)
+ apply(simp)
+ sorry
+ then have "P c (0 \<bullet> lm)" by blast
+ then show "P c lm" by simp
+qed
+
+
nominal_datatype lam =
VAR "name"
| APP "lam" "lam"
@@ -418,14 +451,6 @@
ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *}
-lemma supports_subset:
- fixes S1 S2 :: "atom set"
- assumes a: "S1 supports x"
- and b: "S1 \<subseteq> S2"
- shows "S2 supports x"
- using a b
- by (auto simp add: supports_def)
-
lemma finite_fv_t_tyS:
fixes T::"t"
and S::"tyS"
@@ -473,6 +498,10 @@
(* example 1 from Terms.thy *)
+
+
+
+
nominal_datatype trm1 =
Vr1 "name"
| Ap1 "trm1" "trm1"
--- a/Paper/Paper.thy Thu Mar 18 15:32:49 2010 +0100
+++ b/Paper/Paper.thy Thu Mar 18 16:22:10 2010 +0100
@@ -51,19 +51,21 @@
%\end{pspicture}
%\end{center}
-
+ quotient package \cite{Homeier05}
*}
section {* A Short Review of the Nominal Logic Work *}
text {*
At its core, Nominal Isabelle is based on the nominal logic work by Pitts
- \cite{Pitts03}. Two central notions in this work are sorted atoms and
- permutations of atoms. The sorted atoms represent different
- kinds of variables, such as term- and type-variables in Core-Haskell, and it
- is assumed that there is an infinite supply of atoms for each sort.
- However, in order to simplify the description of our work, we shall
- assume in this paper that there is only a single sort of atoms.
+ \cite{Pitts03}. The implementation of this work are described in
+ \cite{HuffmanUrban10}, which we review here briefly to aid the description
+ of what follows in the next sections. Two central notions in the nominal
+ logic work are sorted atoms and permutations of atoms. The sorted atoms
+ represent different kinds of variables, such as term- and type-variables in
+ Core-Haskell, and it is assumed that there is an infinite supply of atoms
+ for each sort. However, in order to simplify the description of our work, we
+ shall assume in this paper that there is only a single sort of atoms.
Permutations are bijective functions from atoms to atoms that are
the identity everywhere except on a finite number of atoms. There is a
@@ -96,38 +98,55 @@
@{thm[display,indent=5] fresh_def[no_vars]}
\noindent
- We also use for sets of atoms the abbreviation @{thm fresh_star_def[no_vars]}.
+ We also use for sets of atoms the abbreviation
+ @{thm (lhs) fresh_star_def[no_vars]} defined as
+ @{thm (rhs) fresh_star_def[no_vars]}.
A striking consequence of these definitions is that we can prove
without knowing anything about the structure of @{term x} that
swapping two fresh atoms, say @{text a} and @{text b}, leave
@{text x} unchanged.
- \begin{Property}
+ \begin{property}
@{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
- \end{Property}
+ \end{property}
- \begin{Property}
+ \noindent
+ For a proof see \cite{HuffmanUrban10}.
+
+ \begin{property}
@{thm[mode=IfThen] at_set_avoiding[no_vars]}
- \end{Property}
+ \end{property}
*}
section {* Abstractions *}
+text {*
+ General notion of alpha-equivalence (depends on a free-variable
+ function and a relation).
+*}
+
section {* Alpha-Equivalence and Free Variables *}
section {* Examples *}
+section {* Adequacy *}
+
+section {* Related Work *}
+
section {* Conclusion *}
text {*
+ TODO: function definitions:
+ \medskip
+
\noindent
{\bf Acknowledgements:} We are very grateful to Andrew Pitts for the
many discussions about Nominal Isabelle. We thank Peter Sewell for
making the informal notes \cite{SewellBestiary} available to us and
- also explaining some of the finer points of the OTT-tool.
+ also for explaining some of the finer points of the OTT-tool.
*}
--- a/Paper/document/root.bib Thu Mar 18 15:32:49 2010 +0100
+++ b/Paper/document/root.bib Thu Mar 18 16:22:10 2010 +0100
@@ -1,7 +1,20 @@
+@InProceedings{Homeier05,
+ author = {P.~Homeier},
+ title = {{A} {D}esign {S}tructure for {H}igher {O}rder {Q}uotients},
+ booktitle = {Proc.~of the 18th International Conference on Theorem
+ Proving in Higher Order Logics (TPHOLs)},
+ pages = {130--146},
+ year = {2005},
+ volume = {3603},
+ series = {LNCS}
+}
+
+
@Unpublished{HuffmanUrban10,
author = {B.~Huffman and C.~Urban},
title = {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle},
- note = {http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf},
+ note = {To appear at ITP 2010},
+ annote = {http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf},
year = {2010}
}
--- a/Paper/document/root.tex Thu Mar 18 15:32:49 2010 +0100
+++ b/Paper/document/root.tex Thu Mar 18 16:22:10 2010 +0100
@@ -20,7 +20,7 @@
%----------------- theorem definitions ----------
-\newtheorem{Property}{Theorem}[section]
+\newtheorem{property}{Property}[section]
\newtheorem{Theorem}{Theorem}[section]
\newtheorem{Definition}[Theorem]{Definition}
\newtheorem{Example}{\it Example}[section]
@@ -38,16 +38,15 @@
\maketitle
\begin{abstract}
-Nominal Isabelle is a definitional extension of the Isabelle/HOL
-theorem prover. It provides a proving infrastructure for
-conveninet reasoning about programming language calculi. In this paper
-we present an extension of Nominal Isabelle for dealing with general binding
-structures. Such structures are ubiquitous in programming language research
-and only very poorly handled by the well-known single abstraction in the
-lambda-calculus. We give definitions for alpha-equivalence and establish
-the reasoning structure for alpha-equated terms. For example we provide
-a strong induction principle that has the variable convention already
-built in.
+Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
+prover. It provides a proving infrastructure for convenient reasoning about
+programming language calculi. In this paper we present an extension of Nominal
+Isabelle for dealing with general binding structures. Such binding structures are
+ubiquitous in programming language research and only very poorly handled by
+single binding from the lambda-calculus. We give in this
+paper novel definitions for alpha-equivalence and establish automatically the
+reasoning structure for alpha-equated terms. For example we provide a strong
+induction principle that has the variable convention already built in.
\end{abstract}