nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:e6a5651a1d81
+:375e15002efc
 proof.
 \end{proof}
 \noindent
 To sum up this section, we established a reasoning infrastructure
-for the types @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}
+for the types @{text "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}
 by first lifting definitions from the raw level to the quotient level and
 then establish facts about these lifted definitions. All necessary proofs
-are generated automatically by custom ML-code. This code can deal with
+are generated automatically by custom ML-code we implemented. This code can deal with
-specifications as shown in Figure~\ref{nominalcorehas} for Core-Haskell.
+specifications like the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.
 \begin{figure}[t!]
 \begin{boxedminipage}{\linewidth}
 \small
 \begin{tabular}{l}
 @{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}
 \end{equation}
 \noindent
 where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}.
-The problem with this implication is that in general it is not easy to establish.
+The problem with this implication is that in general it is not easy to establish this
+implication
 The reason is we cannot make any assumption about the binders in @{text "C\<^sup>\<alpha>"}
 (for example we cannot assume the variable convention).
 In \cite{UrbanTasson05} we introduced a method for automatically
 strengthening weak induction principles for terms containing single
-binders. These stronger induction principles allow us to make additional
+binders. These stronger induction principles allow the user to make additional
-assumptions about binders. These additional assumptions amount to a formal
+assumptions about binders when proving the induction hypotheses.
-version of the usual variable convention for binders. A natural question is
+These additional assumptions amount to a formal
-whether we can also strengthen the weak induction principles in the presence
+version of the informal variable convention for binders. A natural question is
+whether we can also strengthen the weak induction principles involving
 general binders. We will indeed be able to so, but for this we need an
 additional notion of permuting deep binders.
-Given a binding function @{text "bn"} we need to define an auxiliary permutation
+Given a binding function @{text "bn"} we define an auxiliary permutation
 operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder.
 Given a clause of @{text bn} is defined as @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then
 %
 \begin{center}
 @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C y\<^isub>1 \<dots> y\<^isub>n"}
 $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise
 \end{tabular}
 \end{center}
 \noindent
-Using the quotient package we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to alpha
+Using the quotient package again we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to
-equated terms. We can then prove
+alpha-equated terms. We can then prove:
-\begin{lemma} Given a binding function @{text "bn\<^sup>\<alpha>"}. Then
+\begin{lemma} Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p}
 {\it i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<^bsub>bn\<^sup>\<alpha>\<^esub> x)"} and {\it ii)}
-for all permutations @{text p},  @{text "fv_bn\<^isup>\<alpha> x = fv_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^sup>\<alpha>\<^esub> x)"}.
+@{text "fv_bn\<^isup>\<alpha> x = fv_bn\<^isup>\<alpha> (p \<bullet>\<^bsub>bn\<^sup>\<alpha>\<^esub> x)"}.
 \end{lemma}
 \begin{proof}
 By induction on @{text x}. The equation follow by simple unfolding
 of the definitions.
 \end{proof}
-This allows is to strengthen the induction principles. We will explain
+The first property states that a permutation applied to a binding function is
-the details with the @{text "Let"} term-constructor from \eqref{letpat}.
+equivalent to first permuting the binders and then calculating the bound
+variables. The second amounts to the fact that permuting the binders has no
+effect on the free-variable function.
+This notion allows is to strengthen the induction principles. We will explain
+the details with the @{text "Let"} term-constructor from the example shown
+in \eqref{letpat}.
 Instead of establishing the implication
 \begin{center}
 @{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"}
 \end{center}
 \noindent
-from the weak induction principle, we will show that it is sufficient
+for the weak induction principle, we will show that it is sufficient
 to establish
 \begin{center}
 \begin{tabular}{l}
 @{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\
 \hspace{5mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\
 \hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"}
 \end{tabular}
 \end{center}
+\noindent
+While this implication contains additional arguments (i.e.~@{text c}) and
+additional universal quantifications, it is usually easier to establish.
+The reason is that in the case of @{text "Let"} we can make the freshness
+assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, wherby @{text c} can be arbitrarily
+chosen as long as it has finite support.
 With the help of @{text "\<bullet>bn"} functions defined in the previous section
 we can show that binders can be substituted in term constructors. We show
 this only for the specification from Figure~\ref{nominalcorehas}. The only
 constructor with a complicated binding structure is @{text "ACons"}. For this

changeset 1768	375e15002efc
parent 1767	e6a5651a1d81
child 1769	6ca795b1cd76