# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1270123787 -7200
# Node ID b47c336ba1b7c078104839d0c86552f208acb379
# Parent  24cc3dbd3c4a20e46171fa31c8dd9d85be9f1bfb
Cleaning the strong induction example.

diff -r 24cc3dbd3c4a -r b47c336ba1b7 Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Apr 01 12:19:26 2010 +0200
+++ b/Paper/Paper.thy	Thu Apr 01 14:09:47 2010 +0200
@@ -1654,47 +1654,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:\hspace{2cm}>\<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:\hspace{2cm}>\<and> set (bv p) \<sharp>* b\<^raw:\big)> \<Longrightarrow> P8 b (ACons p t al)"}\\
   @{text "\<dots>"}
   \end{tabular}
 }
 \end{equation}
 
-
 *}
 
 text {*