# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1270126394 -7200
# Node ID 7440bfcdf84972e54f83bcb0542e5acf394a19cb
# Parent  9e09253c80cf0861ad14f1475e91c2bd5e91e877# Parent  6d6c36f7dd1e4ce13e9e5ca998161078929ea338
merged

diff -r 9e09253c80cf -r 7440bfcdf849 Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Apr 01 14:49:01 2010 +0200
+++ b/Paper/Paper.thy	Thu Apr 01 14:53:14 2010 +0200
@@ -1652,47 +1652,52 @@
   & & @{text "ACons pat trm al = ACons (\<pi> \<bullet>bv pat) (\<pi> \<bullet> trm) al"} \nonumber
   \end{eqnarray}
 
-  With the Property~\ref{avoiding} we can prove a strong induction principle
+  \noindent With the Property~\ref{avoiding} we can prove a strong induction principle
   which we show again only for the interesting constructors in the Core Haskell
   example. We first show the weak induction principle for comparison:
 
 \begin{equation}\nonumber
 \infer
 {
-  @{text "P1 tkind \<and> P2 ckind \<and> \<dots> \<and> P12 cvars"}
+  \textrm{The properties }@{text "P1, P2, \<dots>, P12"}\textrm{ hold for all }@{text "tkind, ckind, \<dots>"}
 }{
   \begin{tabular}{cp{7cm}}
-  @{text "P1 KStar"}\\
-  @{text "\<And>tk1 tk2. \<lbrakk>P1 tk1; P1 tk2\<rbrakk> \<Longrightarrow> P1 (KFun tk1 tk2)"}\\
-  @{text "\<dots>"}\\
-  @{text "\<And>v ty t1 t2. \<lbrakk>P3 ty; P7 t1; P7 t2\<rbrakk> \<Longrightarrow> P7 (Let v ty t1 t2)"}\\
-  @{text "\<And>p t al. \<lbrakk>P9 p; P7 t; P8 al\<rbrakk> \<Longrightarrow> P8 (ACons p t al)"}\\
+%%  @{text "P1 KStar"}\\
+%%  @{text "\<forall>tk1 tk2. \<^raw:\big(>P1 tk1 \<and> P1 tk2\<^raw:\big)> \<Longrightarrow> P1 (KFun tk1 tk2)"}\\
+%%  @{text "\<dots>"}\\
+  @{text "\<forall>v ty t1 t2. \<^raw:\big(>P3 ty \<and> P7 t1 \<and> P7 t2\<^raw:\big)> \<Longrightarrow> P7 (Let v ty t1 t2)"}\\
+  @{text "\<forall>p t al. \<^raw:\big(>P9 p \<and> P7 t \<and> P8 al\<^raw:\big)> \<Longrightarrow> P8 (ACons p t al)"}\\
   @{text "\<dots>"}
   \end{tabular}
 }
 \end{equation}
 
 
-In comparison, the cases for the same constructors in the derived strong
-induction principle are:
+  \noindent In comparison, the cases for the same constructors in the derived strong
+  induction principle are:
 
+%% TODO get rid of the ugly hspaces.
 \begin{equation}\nonumber
 \infer
 {
-  @{text "P1 a tkind \<and> P2 a ckind \<and> \<dots> \<and> P12 a cvars"}
+  \begin{tabular}{cp{7cm}}
+  \textrm{The properties }@{text "P1, P2, \<dots>, P12"}\textrm{ hold for all }@{text "tkind, ckind, \<dots>"}\\
+  \textrm{ avoiding any atoms in a given }@{text "y"}
+  \end{tabular}
 }{
   \begin{tabular}{cp{7cm}}
-  @{text "\<And>b. P1 b KStar"}\\
-  @{text "\<And>tk1 tk2 b. \<lbrakk>\<And>c. P1 c tk1; \<And>c. P1 c tk2\<rbrakk> \<Longrightarrow> P1 b (KFun tk1 tk2)"}\\
-  @{text "\<dots>"}\\
-  @{text "\<And>v ty t1 t2 b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c t1; \<And>c. P7 c t2; atom var \<sharp> b\<rbrakk> \<Longrightarrow> P7 b (Let v ty t1 t2)"}\\
-  @{text "\<And>p t al b. \<lbrakk>\<And>c. P9 c p; \<And>c. P7 c t; \<And>c. P8 c al; set (bv p) \<sharp>* b\<rbrakk> \<Longrightarrow> P8 b (ACons p t al)"}\\
+%%  @{text "\<forall>b. P1 b KStar"}\\
+%%  @{text "\<forall>tk1 tk2 b. \<^raw:\big(>\<forall>c. P1 c tk1 \<and> \<forall>c. P1 c tk2\<^raw:\big)> \<Longrightarrow> P1 b (KFun tk1 tk2)"}\\
+%%  @{text "\<dots>"}\\
+  @{text "\<forall>v ty t1 t2 b. \<^raw:\big(>\<forall>c. P3 c ty \<and> \<forall>c. P7 c t1 \<and> \<forall>c. P7 c t2 \<and>"}\\
+  @{text "\<^raw:\hfill>\<and> atom var \<sharp> b\<^raw:\big)> \<Longrightarrow> P7 b (Let v ty t1 t2)"}\\
+  @{text "\<forall>p t al b. \<^raw:\big(>\<forall>c. P9 c p \<and> \<forall>c. P7 c t \<and> \<forall>c. P8 c al \<and>"}\\
+  @{text "\<^raw:\hfill>\<and> set (bv p) \<sharp>* b\<^raw:\big)> \<Longrightarrow> P8 b (ACons p t al)"}\\
   @{text "\<dots>"}
   \end{tabular}
 }
 \end{equation}
 
-
 *}
 
 text {*