# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1269668654 -3600
# Node ID 2922b04d9545710f08ffafa897113eb1b95ae9e0
# Parent  d00dd828f7affcf5d4d402338b85d2c8f9e450af
more on the paper

diff -r d00dd828f7af -r 2922b04d9545 Nominal/ExCoreHaskell.thy
--- a/Nominal/ExCoreHaskell.thy	Fri Mar 26 22:23:22 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Sat Mar 27 06:44:14 2010 +0100
@@ -312,7 +312,7 @@
 apply (simp)
 oops
 
-lemma 
+lemma strong_inudction_principle:
   assumes a01: "\<And>b. P1 b KStar"
   and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
   and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)"
diff -r d00dd828f7af -r 2922b04d9545 Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Mar 26 22:23:22 2010 +0100
+++ b/Paper/Paper.thy	Sat Mar 27 06:44:14 2010 +0100
@@ -78,7 +78,7 @@
   we would like to regard the following two type-schemes as alpha-equivalent
   %
   \begin{equation}\label{ex1}
-  @{text "\<forall>{x,y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y,x}. y \<rightarrow> x"} 
+  @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. y \<rightarrow> x"} 
   \end{equation}
 
   \noindent
@@ -86,7 +86,7 @@
   the following two should \emph{not} be alpha-equivalent
   %
   \begin{equation}\label{ex2}
-  @{text "\<forall>{x,y}. x \<rightarrow> y  \<notapprox>\<^isub>\<alpha>  \<forall>{z}. z \<rightarrow> z"} 
+  @{text "\<forall>{x, y}. x \<rightarrow> y  \<notapprox>\<^isub>\<alpha>  \<forall>{z}. z \<rightarrow> z"} 
   \end{equation}
 
   \noindent
@@ -94,7 +94,7 @@
   only on \emph{vacuous} binders, such as
   %
   \begin{equation}\label{ex3}
-  @{text "\<forall>{x}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{x,z}. x \<rightarrow> y"}
+  @{text "\<forall>{x}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{x, z}. x \<rightarrow> y"}
   \end{equation}
 
   \noindent
@@ -170,7 +170,7 @@
   \noindent
   where the notation @{text "[_]._"} indicates that the @{text "x\<^isub>i"}
   become bound in @{text s}. In this representation the term 
-  \mbox{@{text "\<LET> [x].s [t\<^isub>1,t\<^isub>2]"}} would be a perfectly legal
+  \mbox{@{text "\<LET> [x].s [t\<^isub>1, t\<^isub>2]"}} would be a perfectly legal
   instance. To exclude such terms, additional predicates about well-formed
   terms are needed in order to ensure that the two lists are of equal
   length. This can result into very messy reasoning (see for
@@ -230,7 +230,7 @@
   two type-schemes (with $x$, $y$ and $z$ being distinct)
 
   \begin{center}
-  @{text "\<forall>{x}. x \<rightarrow> y  = \<forall>{x,z}. x \<rightarrow> y"} 
+  @{text "\<forall>{x}. x \<rightarrow> y  = \<forall>{x, z}. x \<rightarrow> y"} 
   \end{center}
   
   \noindent
@@ -253,7 +253,7 @@
   specification we will need to construct a type containing as elements the
   alpha-equated terms. To do so, we use the standard HOL-technique of defining
   a new type by identifying a non-empty subset of an existing type.  The
-  construction we perform in HOL can be illustrated by the following picture:
+  construction we perform in Isabelle/HOL can be illustrated by the following picture:
 
   \begin{center}
   \begin{tikzpicture}
@@ -326,12 +326,22 @@
   and lambda are lifted to the quotient level.)  This construction, of course,
   only works if alpha-equivalence is indeed an equivalence relation, and the lifted
   definitions and theorems are respectful w.r.t.~alpha-equivalence.  Accordingly, we
-  will not be able to lift a bound-variable function to alpha-equated terms
+  will not be able to lift a bound-variable function, which can be defined for
+  raw terms, to alpha-equated terms
   (since it does not respect alpha-equivalence). To sum up, every lifting of
   theorems to the quotient level needs proofs of some respectfulness
   properties. In the paper we show that we are able to automate these
   proofs and therefore can establish a reasoning infrastructure for
-  alpha-equated terms.\medskip
+  alpha-equated terms.
+
+  The examples we have in mind where our reasoning infrastructure will be
+  immeasurably helpful is what is often referred to as Core-Haskell (see
+  Figure~\ref{corehas}). There terms include patterns which include a list of
+  type- and term- variables (the arguments of constructors) all of which are
+  bound in case expressions. One difficulty is that each of these variables
+  come with a kind or type annotation. Representing such binders with single
+  binders and reasoning about them in a theorem prover would be a major pain.
+  \medskip
 
 
   \noindent
@@ -343,6 +353,11 @@
   conditions for alpha-equated terms. We are also able to derive, at the moment 
   only manually, strong induction principles that 
   have the variable convention already built in.
+
+  \begin{figure}
+
+  \caption{Core Haskell.\label{corehas}}
+  \end{figure}
 *}
 
 section {* A Short Review of the Nominal Logic Work *}