# HG changeset patch # User Christian Urban # Date 1268925730 -3600 # Node ID 62d6f7acc110b4fff4fe971d40198807a4b16333 # Parent e3a82a3529cebe8b87f9baabbe81c7b68c310856 corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant diff -r e3a82a3529ce -r 62d6f7acc110 Nominal/Test.thy --- 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: "\name c. P c (Vr name)" and a2: "\lm1 lm2 c. \\d. P d lm1; \d. P d lm2\ \ P c (Ap lm1 lm2)" - and a3: "\name lm c. \\d. P d lm\ \ P c (Lm name lm)" + and a3: "\name lm c. \atom name \ c; \d. P d lm\ \ P c (Lm name lm)" shows "P c lm" proof - have "\p. P c (p \ 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 \ name) \ new) + p" in meta_spec) apply(simp) apply(simp add: fresh_def) @@ -99,6 +100,38 @@ qed +lemma + fixes c::"'a::fs" + assumes a1: "\name c. P c (Vr name)" + and a2: "\lm1 lm2 c. \\d. P d lm1; \d. P d lm2\ \ P c (Ap lm1 lm2)" + and a3: "\name lm c. \atom name \ c; \d. P d lm\ \ P c (Lm name lm)" + shows "P c lm" +proof - + have "\p. P c (p \ 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 "\q. (q \ {p \ atom name}) \* c \ supp (p \ Lm name lm) \* q") + apply(erule exE) + apply(rule_tac t="p \ Lm name lm" and + s="q \ p \ 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 \ 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 \ 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" diff -r e3a82a3529ce -r 62d6f7acc110 Paper/Paper.thy --- 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. *} diff -r e3a82a3529ce -r 62d6f7acc110 Paper/document/root.bib --- 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} } diff -r e3a82a3529ce -r 62d6f7acc110 Paper/document/root.tex --- 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}