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