--- a/Nominal/Ex/CoreHaskell.thy Sun Jun 06 13:16:27 2010 +0200
+++ b/Nominal/Ex/CoreHaskell.thy Mon Jun 07 11:33:00 2010 +0200
@@ -84,7 +84,9 @@
| "bv_tvs TvsNil = []"
| "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t"
| "bv_cvs CvsNil = []"
-| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
+| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
+
+
lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
--- a/Nominal/Ex/SingleLet.thy Sun Jun 06 13:16:27 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy Mon Jun 07 11:33:00 2010 +0200
@@ -8,7 +8,8 @@
Var "name"
| App "trm" "trm"
| Lam x::"name" t::"trm" bind_set x in t
-| Let a::"assg" t::"trm" bind_set "bn a" in t
+| Let a::"assg" t1::"trm" t2::"trm" bind_set "bn a" in t1 t2
+
and assg =
As "name" "trm"
binder
--- a/Nominal/NewFv.thy Sun Jun 06 13:16:27 2010 +0200
+++ b/Nominal/NewFv.thy Mon Jun 07 11:33:00 2010 +0200
@@ -265,6 +265,8 @@
val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
+ val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) (flat fv_bn_eqs)))
+
fun pat_completeness_auto ctxt =
Pat_Completeness.pat_completeness_tac ctxt 1
THEN auto_tac (clasimpset_of ctxt)
--- a/Quotient-Paper/Paper.thy Sun Jun 06 13:16:27 2010 +0200
+++ b/Quotient-Paper/Paper.thy Mon Jun 07 11:33:00 2010 +0200
@@ -46,7 +46,7 @@
\begin{flushright}
{\em ``Not using a [quotient] package has its advantages: we do not have to\\
collect all the theorems we shall ever want into one giant list;''}\\
- Paulson \cite{Paulson06}
+ Larry Paulson \cite{Paulson06}
\end{flushright}\smallskip
\noindent
@@ -58,7 +58,8 @@
mechanisms for extending the logic: one is the definition of new constants
in terms of existing ones; the other is the introduction of new types
by identifying non-empty subsets in existing types. It is well understood
- to use both mechanism for dealing with quotient constructions in HOL (cite Larry).
+ to use both mechanisms for dealing with quotient constructions in HOL (see for example
+ \cite{Paulson06}).
For example the integers in Isabelle/HOL are constructed by a quotient construction over
the type @{typ "nat \<times> nat"} and the equivalence relation
--- a/Quotient-Paper/document/root.tex Sun Jun 06 13:16:27 2010 +0200
+++ b/Quotient-Paper/document/root.tex Mon Jun 07 11:33:00 2010 +0200
@@ -12,6 +12,10 @@
\isabellestyle{it}
\renewcommand{\isastyle}{\isastyleminor}
+\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\renewcommand{\isasymequiv}{$\dn$}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+
\begin{document}
\title{Quotients Revisited for Isabelle/HOL}
@@ -20,16 +24,18 @@
\maketitle
\begin{abstract}
-Higher-order logic (HOL) is based on a small logic kernel, whose
-only mechanism for extension is the introduction of definitions
-and types. Both extensions are often performed by
-quotient constructions, for example finite sets are constructed by quotienting
+Higher-order logic (HOL), used in several theorem provers, is based on a
+small logic kernel, whose only mechanism for extension is the introduction
+of safe definitions and non-empty types. Both extensions are often performed by
+quotient constructions; for example finite sets are constructed by quotienting
lists, or integers by quotienting pairs of natural numbers. To ease the work
involved with quotient constructions, we re-implemented in Isabelle/HOL
the quotient package by Homeier. In doing so we extended his work
in order to deal with compositions of quotients. Also, we designed
our quotient package so that every step in a quotient construction
-can be performed separately.
+can be performed separately. The importance to programming language research
+is that many properties of programming languages are more convenient to verify
+over $\alpha$-quotient terms, than over raw terms.
\end{abstract}
% generated text of all theories