# HG changeset patch # User Cezary Kaliszyk # Date 1274431627 -7200 # Node ID 687369ae8f8122f2b645221b44b31b6da6d985d6 # Parent fe84fcfab46f1b2cf8a660c24bab0cf87bf6be63# Parent e838f7d90f811c565c26e2de4260a29349c71059 merge (non-trival) diff -r e838f7d90f81 -r 687369ae8f81 Nominal-General/nominal_permeq.ML --- a/Nominal-General/nominal_permeq.ML Fri May 21 10:44:07 2010 +0200 +++ b/Nominal-General/nominal_permeq.ML Fri May 21 10:47:07 2010 +0200 @@ -127,10 +127,10 @@ val post_thms = map safe_mk_equiv @{thms permute_pure} in first_conv_wrapper - [ More_Conv.rewrs_conv pre_thms, + [ Conv.rewrs_conv pre_thms, eqvt_apply_conv, eqvt_lambda_conv, - More_Conv.rewrs_conv post_thms, + Conv.rewrs_conv post_thms, progress_info_conv ctxt strict_flag excluded ] ctrm end @@ -141,12 +141,12 @@ (* raises an error if some permutations cannot be eliminated *) fun eqvt_strict_tac ctxt user_thms excluded = - CONVERSION (More_Conv.top_conv + CONVERSION (Conv.top_conv (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms excluded)) ctxt) (* prints a warning message if some permutations cannot be eliminated *) fun eqvt_tac ctxt user_thms excluded = - CONVERSION (More_Conv.top_conv + CONVERSION (Conv.top_conv (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms excluded)) ctxt) (* setup of the configuration value *) diff -r e838f7d90f81 -r 687369ae8f81 Nominal/Ex/Lambda.thy diff -r e838f7d90f81 -r 687369ae8f81 Nominal/Ex/Term8.thy --- a/Nominal/Ex/Term8.thy Fri May 21 10:44:07 2010 +0200 +++ b/Nominal/Ex/Term8.thy Fri May 21 10:47:07 2010 +0200 @@ -6,9 +6,7 @@ atom_decl name -(* this should work but gives an error at the moment: - in alpha_bn_rsp proof. -*) +ML {* val _ = cheat_alpha_bn_rsp := true *} nominal_datatype foo = Foo0 "name" @@ -22,6 +20,7 @@ "bv (Bar0 x) = {}" | "bv (Bar1 v x b) = {atom v}" +thm foo_bar.supp end diff -r e838f7d90f81 -r 687369ae8f81 Nominal/Rsp.thy --- a/Nominal/Rsp.thy Fri May 21 10:44:07 2010 +0200 +++ b/Nominal/Rsp.thy Fri May 21 10:47:07 2010 +0200 @@ -145,10 +145,10 @@ fun alpha_bn_rsp_tac simps res exhausts a ctxt = rtac allI THEN_ALL_NEW case_rules_tac ctxt a exhausts THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW + asm_full_simp_tac (HOL_ss addsimps simps addsimps @{thms alphas}) THEN_ALL_NEW TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \"]}) THEN_ALL_NEW TRY o eresolve_tac res THEN_ALL_NEW - asm_full_simp_tac (HOL_ss addsimps simps); + asm_full_simp_tac (HOL_ss addsimps simps) *} @@ -186,10 +186,15 @@ end *} +lemma exi_same: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q p) \ \pi. Q pi" + by auto + ML {* fun prove_alpha_alphabn alphas ind simps alpha_bns ctxt = prove_by_rel_induct alphas build_alpha_alpha_bn_gl ind - (fn _ => asm_full_simp_tac (HOL_ss addsimps simps)) alpha_bns ctxt + (fn _ => asm_full_simp_tac (HOL_ss addsimps simps addsimps @{thms alphas}) + THEN_ALL_NEW split_conj_tac THEN_ALL_NEW (TRY o etac @{thm exi_same}) + THEN_ALL_NEW asm_full_simp_tac HOL_ss) alpha_bns ctxt *} ML {* diff -r e838f7d90f81 -r 687369ae8f81 Paper/Paper.thy --- a/Paper/Paper.thy Fri May 21 10:44:07 2010 +0200 +++ b/Paper/Paper.thy Fri May 21 10:47:07 2010 +0200 @@ -922,30 +922,33 @@ ``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to Ott, we allow multiple labels in binders and bodies. For example - we have binding clauses of the form: + we allow binding clauses of the form: \begin{center} - \begin{tabular}{ll} - @{text "Foo x::name y::name t::lam s::lam"} & - \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"} + \begin{tabular}{@ {}ll@ {}} + @{text "Foo\<^isub>1 x::name y::name t::lam s::lam"} & + \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\ + @{text "Foo\<^isub>2 x::name y::name t::lam s::lam"} & + \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t"}, + \isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\ \end{tabular} \end{center} \noindent - Similarly for the other binding modes. + Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set} + and \isacommand{bind\_res} the binding clauses will make a difference in + terms of the corresponding alpha-equivalence. We will show this later with an example. - - There are a few restrictions we need to impose: First, a body can only occur in - \emph{one} binding clause of a term constructor. - For binders we distinguish between \emph{shallow} and \emph{deep} binders. - Shallow binders are just labels. The - restriction we need to impose on them is that in case of - \isacommand{bind\_set} and \isacommand{bind\_res} the labels must - either refer to atom types or to sets of atom types; in case of - \isacommand{bind} the labels must refer to atom types or lists of atom types. - Two examples for the use of shallow binders are the specification of - lambda-terms, where a single name is bound, and type-schemes, where a finite - set of names is bound: + There are some restrictions we need to impose: First, a body can only occur + in \emph{one} binding clause of a term constructor. For binders we + distinguish between \emph{shallow} and \emph{deep} binders. Shallow binders + are just labels. The restriction we need to impose on them is that in case + of \isacommand{bind\_set} and \isacommand{bind\_res} the labels must either + refer to atom types or to sets of atom types; in case of \isacommand{bind} + the labels must refer to atom types or lists of atom types. Two examples for + the use of shallow binders are the specification of lambda-terms, where a + single name is bound, and type-schemes, where a finite set of names is + bound: \begin{center} \begin{tabular}{@ {}cc@ {}} @@ -967,23 +970,25 @@ \end{center} \noindent - Note that for @{text lam} it does not matter which binding mode we use. The reason is that - we bind only a single @{text name}. However, having \isacommand{bind\_set} or - \isacommand{bind} in the second - case changes the semantics of the specification. - Note also that in these specifications @{text "name"} refers to an atom type, and - @{text "fset"} to the type of finite sets. + Note that for @{text lam} it does not matter which binding mode we use. The + reason is that we bind only a single @{text name}. However, having + \isacommand{bind\_set} or \isacommand{bind} in the second case again makes a + difference to the underlying notion of alpha-equivalence. Note also that in + these specifications @{text "name"} refers to an atom type, and @{text + "fset"} to the type of finite sets. + A \emph{deep} binder uses an auxiliary binding function that ``picks'' out - the atoms in one argument of the term-constructor, which can be bound in - other arguments and also in the same argument (we will - call such binders \emph{recursive}, see below). - The corresponding binding functions are expected to return either a set of atoms - (for \isacommand{bind\_set} and \isacommand{bind\_res}) or a list of atoms - (for \isacommand{bind}). They can be defined by primitive recursion over the - corresponding type; the equations must be given in the binding function part of - the scheme shown in \eqref{scheme}. For example a term-calculus containing @{text "Let"}s - with tuple patterns might be specified as: + the atoms in one argument of the term-constructor, which can be bound in + other arguments and also in the same argument (we will call such binders + \emph{recursive}, see below). The corresponding binding functions are + expected to return either a set of atoms (for \isacommand{bind\_set} and + \isacommand{bind\_res}) or a list of atoms (for \isacommand{bind}). They can + be defined by primitive recursion over the corresponding type; the equations + must be given in the binding function part of the scheme shown in + \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with + tuple patterns might be specified as: + % \begin{equation}\label{letpat} \mbox{% @@ -1065,9 +1070,7 @@ \noindent The reason why we must exclude such specifications is that they cannot be - represented by the general binders described in Section - \ref{sec:binders}. Unlike shallow binders, we restrict deep binders to occur - in only one binding clause. + represented by the general binders described in Section~\ref{sec:binders}. We also need to restrict the form of the binding functions. As will shortly become clear, we cannot return an atom in a binding function that is also @@ -1084,7 +1087,7 @@ (case @{text PTup}). This restriction will simplify some automatic proofs later on. - In order to simplify later definitions, we shall assume specifications + In order to simplify our definitions, we shall assume specifications of term-calculi are \emph{completed}. By this we mean that for every argument of a term-constructor that is \emph{not} already part of a binding clause, we add implicitly a special \emph{empty} binding diff -r e838f7d90f81 -r 687369ae8f81 Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Fri May 21 10:44:07 2010 +0200 +++ b/Quotient-Paper/Paper.thy Fri May 21 10:47:07 2010 +0200 @@ -134,7 +134,7 @@ Example of non-regularizable theorem ($0 = 1$). -New regularization lemmas: +Separtion of regularization from injection thanks to the following 2 lemmas: \begin{lemma} If @{term R2} is an equivalence relation, then: \begin{eqnarray} @@ -159,20 +159,23 @@ text {* \begin{itemize} - \item Peter Homeier's package (and related work from there), John - Harrison's one. + \item Peter Homeier's package~\cite{Homeier05} (and related work from there) + \item John Harrison's one~\cite{harrison-thesis} is the first one to lift theorems + but only first order. - \item Manually defined quotients in Isabelle/HOL Library (Larry's - quotients, Markus's Quotient\_Type, Dixon's FSet, \ldots) + \item PVS~\cite{PVS:Interpretations} + \item MetaPRL~\cite{Nogin02} + \item Manually defined quotients in Isabelle/HOL Library (Markus's Quotient\_Type, + Dixon's FSet, \ldots) \item Oscar Slotosch defines quotient-type automatically but no - lifting. + lifting~\cite{Slotosch97}. \item PER. And how to avoid it. - \item Necessity of Hilbert Choice op. + \item Necessity of Hilbert Choice op and Larry's quotients~\cite{Paulson06} - \item Setoids in Coq + \item Setoids in Coq and \cite{ChicliPS02} \end{itemize} *} diff -r e838f7d90f81 -r 687369ae8f81 Quotient-Paper/document/root.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quotient-Paper/document/root.bib Fri May 21 10:47:07 2010 +0200 @@ -0,0 +1,131 @@ +@inproceedings{Nogin02, + author = {Aleksey Nogin}, + title = {Quotient Types: A Modular Approach}, + booktitle = {TPHOLs}, + year = {2002}, + pages = {263-280}, + ee = {http://link.springer.de/link/service/series/0558/bibs/2410/24100263.htm}, + crossref = {DBLP:conf/tphol/2002}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} +@proceedings{DBLP:conf/tphol/2002, + editor = {Victor Carre{\~n}o and + C{\'e}sar Mu{\~n}oz and + Sofi{\`e}ne Tahar}, + title = {Theorem Proving in Higher Order Logics, 15th International + Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, + 2002, Proceedings}, + booktitle = {TPHOLs}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = {2410}, + year = {2002}, + isbn = {3-540-44039-9}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@techreport{PVS:Interpretations, + Author= {S. Owre and N. Shankar}, + Title= {Theory Interpretations in PVS}, + Number= {SRI-CSL-01-01}, + Institution= {Computer Science Laboratory, SRI International}, + Address= {Menlo Park, CA}, + Month= {April}, + Year= {2001}} + +@inproceedings{ChicliPS02, + author = {Laurent Chicli and + Loic Pottier and + Carlos Simpson}, + title = {Mathematical Quotients and Quotient Types in Coq}, + booktitle = {TYPES}, + year = {2002}, + pages = {95-107}, + ee = {http://link.springer.de/link/service/series/0558/bibs/2646/26460095.htm}, + crossref = {DBLP:conf/types/2002}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@proceedings{DBLP:conf/types/2002, + editor = {Herman Geuvers and + Freek Wiedijk}, + title = {Types for Proofs and Programs, Second International Workshop, + TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, + Selected Papers}, + booktitle = {TYPES}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = {2646}, + year = {2003}, + isbn = {3-540-14031-X}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@article{Paulson06, + author = {Lawrence C. Paulson}, + title = {Defining functions on equivalence classes}, + journal = {ACM Trans. Comput. Log.}, + volume = {7}, + number = {4}, + year = {2006}, + pages = {658-675}, + ee = {http://doi.acm.org/10.1145/1183278.1183280}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@inproceedings{Slotosch97, + author = {Oscar Slotosch}, + title = {Higher Order Quotients and their Implementation in Isabelle + HOL}, + booktitle = {TPHOLs}, + year = {1997}, + pages = {291-306}, + ee = {http://dx.doi.org/10.1007/BFb0028401}, + crossref = {DBLP:conf/tphol/1997}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} +@proceedings{DBLP:conf/tphol/1997, + editor = {Elsa L. Gunter and + Amy P. Felty}, + title = {Theorem Proving in Higher Order Logics, 10th International + Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, + 1997, Proceedings}, + booktitle = {TPHOLs}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = {1275}, + year = {1997}, + isbn = {3-540-63379-0}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@inproceedings{Homeier05, + author = {Peter V. Homeier}, + title = {A Design Structure for Higher Order Quotients}, + booktitle = {TPHOLs}, + year = {2005}, + pages = {130-146}, + ee = {http://dx.doi.org/10.1007/11541868_9}, + crossref = {DBLP:conf/tphol/2005}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} +@proceedings{DBLP:conf/tphol/2005, + editor = {Joe Hurd and + Thomas F. Melham}, + title = {Theorem Proving in Higher Order Logics, 18th International + Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, + Proceedings}, + booktitle = {TPHOLs}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = {3603}, + year = {2005}, + isbn = {3-540-28372-2}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + +@BOOK{harrison-thesis, + author = "John Harrison", + title = "Theorem Proving with the Real Numbers", + publisher = "Springer-Verlag", + year = 1998} \ No newline at end of file