--- 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 *)
--- 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
--- 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 \<and>"]}) 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: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q p) \<Longrightarrow> \<exists>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 {*
--- 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
--- 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}
*}
--- /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