1652 \begin{eqnarray} |
1652 \begin{eqnarray} |
1653 \lefteqn{@{text "supp (Abs_lst (bv pat) trm) \<sharp>* \<pi> \<Longrightarrow>"}} \nonumber \\ |
1653 \lefteqn{@{text "supp (Abs_lst (bv pat) trm) \<sharp>* \<pi> \<Longrightarrow>"}} \nonumber \\ |
1654 & & @{text "ACons pat trm al = ACons (\<pi> \<bullet>bv pat) (\<pi> \<bullet> trm) al"} \nonumber |
1654 & & @{text "ACons pat trm al = ACons (\<pi> \<bullet>bv pat) (\<pi> \<bullet> trm) al"} \nonumber |
1655 \end{eqnarray} |
1655 \end{eqnarray} |
1656 |
1656 |
1657 With the Property~\ref{avoiding} we can prove a strong induction principle |
1657 \noindent With the Property~\ref{avoiding} we can prove a strong induction principle |
1658 which we show again only for the interesting constructors in the Core Haskell |
1658 which we show again only for the interesting constructors in the Core Haskell |
1659 example. We first show the weak induction principle for comparison: |
1659 example. We first show the weak induction principle for comparison: |
1660 |
1660 |
1661 \begin{equation}\nonumber |
1661 \begin{equation}\nonumber |
1662 \infer |
1662 \infer |
1663 { |
1663 { |
1664 @{text "P1 tkind \<and> P2 ckind \<and> \<dots> \<and> P12 cvars"} |
1664 \textrm{The properties }@{text "P1, P2, \<dots>, P12"}\textrm{ hold for all }@{text "tkind, ckind, \<dots>"} |
1665 }{ |
1665 }{ |
1666 \begin{tabular}{cp{7cm}} |
1666 \begin{tabular}{cp{7cm}} |
1667 @{text "P1 KStar"}\\ |
1667 %% @{text "P1 KStar"}\\ |
1668 @{text "\<And>tk1 tk2. \<lbrakk>P1 tk1; P1 tk2\<rbrakk> \<Longrightarrow> P1 (KFun tk1 tk2)"}\\ |
1668 %% @{text "\<forall>tk1 tk2. \<^raw:\big(>P1 tk1 \<and> P1 tk2\<^raw:\big)> \<Longrightarrow> P1 (KFun tk1 tk2)"}\\ |
1669 @{text "\<dots>"}\\ |
1669 %% @{text "\<dots>"}\\ |
1670 @{text "\<And>v ty t1 t2. \<lbrakk>P3 ty; P7 t1; P7 t2\<rbrakk> \<Longrightarrow> P7 (Let v ty t1 t2)"}\\ |
1670 @{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)"}\\ |
1671 @{text "\<And>p t al. \<lbrakk>P9 p; P7 t; P8 al\<rbrakk> \<Longrightarrow> P8 (ACons p t al)"}\\ |
1671 @{text "\<forall>p t al. \<^raw:\big(>P9 p \<and> P7 t \<and> P8 al\<^raw:\big)> \<Longrightarrow> P8 (ACons p t al)"}\\ |
1672 @{text "\<dots>"} |
1672 @{text "\<dots>"} |
1673 \end{tabular} |
1673 \end{tabular} |
1674 } |
1674 } |
1675 \end{equation} |
1675 \end{equation} |
1676 |
1676 |
1677 |
1677 |
1678 In comparison, the cases for the same constructors in the derived strong |
1678 \noindent In comparison, the cases for the same constructors in the derived strong |
1679 induction principle are: |
1679 induction principle are: |
1680 |
1680 |
|
1681 %% TODO get rid of the ugly hspaces. |
1681 \begin{equation}\nonumber |
1682 \begin{equation}\nonumber |
1682 \infer |
1683 \infer |
1683 { |
1684 { |
1684 @{text "P1 a tkind \<and> P2 a ckind \<and> \<dots> \<and> P12 a cvars"} |
1685 \begin{tabular}{cp{7cm}} |
|
1686 \textrm{The properties }@{text "P1, P2, \<dots>, P12"}\textrm{ hold for all }@{text "tkind, ckind, \<dots>"}\\ |
|
1687 \textrm{ avoiding any atoms in a given }@{text "y"} |
|
1688 \end{tabular} |
1685 }{ |
1689 }{ |
1686 \begin{tabular}{cp{7cm}} |
1690 \begin{tabular}{cp{7cm}} |
1687 @{text "\<And>b. P1 b KStar"}\\ |
1691 %% @{text "\<forall>b. P1 b KStar"}\\ |
1688 @{text "\<And>tk1 tk2 b. \<lbrakk>\<And>c. P1 c tk1; \<And>c. P1 c tk2\<rbrakk> \<Longrightarrow> P1 b (KFun tk1 tk2)"}\\ |
1692 %% @{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)"}\\ |
1689 @{text "\<dots>"}\\ |
1693 %% @{text "\<dots>"}\\ |
1690 @{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)"}\\ |
1694 @{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>"}\\ |
1691 @{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)"}\\ |
1695 @{text "\<^raw:\hspace{2cm}>\<and> atom var \<sharp> b\<^raw:\big)> \<Longrightarrow> P7 b (Let v ty t1 t2)"}\\ |
|
1696 @{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>"}\\ |
|
1697 @{text "\<^raw:\hspace{2cm}>\<and> set (bv p) \<sharp>* b\<^raw:\big)> \<Longrightarrow> P8 b (ACons p t al)"}\\ |
1692 @{text "\<dots>"} |
1698 @{text "\<dots>"} |
1693 \end{tabular} |
1699 \end{tabular} |
1694 } |
1700 } |
1695 \end{equation} |
1701 \end{equation} |
1696 |
|
1697 |
1702 |
1698 *} |
1703 *} |
1699 |
1704 |
1700 text {* |
1705 text {* |
1701 |
1706 |