equal
deleted
inserted
replaced
1119 \hspace{5mm}$\mid$~@{text "Lam x::name t::trm"} |
1119 \hspace{5mm}$\mid$~@{text "Lam x::name t::trm"} |
1120 \;\;\isacommand{binds} @{text x} \isacommand{in} @{text t}\\ |
1120 \;\;\isacommand{binds} @{text x} \isacommand{in} @{text t}\\ |
1121 \hspace{5mm}$\mid$~@{text "Let_pat p::pat trm t::trm"} |
1121 \hspace{5mm}$\mid$~@{text "Let_pat p::pat trm t::trm"} |
1122 \;\;\isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text t}\\ |
1122 \;\;\isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text t}\\ |
1123 \isacommand{and} @{text pat} $=$\\ |
1123 \isacommand{and} @{text pat} $=$\\ |
1124 \hspace{5mm}\phantom{$\mid$}~@{text PNil}\\ |
1124 \hspace{5mm}\phantom{$\mid$}~@{text "PVar name"}\\ |
1125 \hspace{5mm}$\mid$~@{text "PVar name"}\\ |
|
1126 \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\ |
1125 \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\ |
1127 \isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\ |
1126 \isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\ |
1128 \isacommand{where}~@{text "bn(PNil) = []"}\\ |
1127 \isacommand{where}~@{text "bn(PVar x) = [atom x]"}\\ |
1129 \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\ |
|
1130 \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\smallskip\\ |
1128 \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\smallskip\\ |
1131 \end{tabular}} |
1129 \end{tabular}} |
1132 \end{equation}\smallskip |
1130 \end{equation}\smallskip |
1133 |
1131 |
1134 \noindent |
1132 \noindent |
1970 @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. y = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"} |
1968 @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. y = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"} |
1971 \end{array}}\hspace{10mm} |
1969 \end{array}}\hspace{10mm} |
1972 |
1970 |
1973 \infer{@{text "P\<^bsub>pat\<^esub>"}} |
1971 \infer{@{text "P\<^bsub>pat\<^esub>"}} |
1974 {\begin{array}{@ {}l@ {}} |
1972 {\begin{array}{@ {}l@ {}} |
1975 @{text "y = PNil\<^sup>\<alpha> \<Rightarrow> P\<^bsub>pat\<^esub>"}\\ |
|
1976 @{text "\<forall>x. y = PVar\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>pat\<^esub>"}\\ |
1973 @{text "\<forall>x. y = PVar\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>pat\<^esub>"}\\ |
1977 @{text "\<forall>x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub>"} |
1974 @{text "\<forall>x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub>"} |
1978 \end{array}}\medskip\\ |
1975 \end{array}}\medskip\\ |
1979 |
1976 |
1980 \multicolumn{1}{@ {\hspace{-5mm}}l}{induction principle:}\smallskip\\ |
1977 \multicolumn{1}{@ {\hspace{-5mm}}l}{induction principle:}\smallskip\\ |
1983 {\begin{array}{@ {}l@ {}} |
1980 {\begin{array}{@ {}l@ {}} |
1984 @{text "\<forall>x. P\<^bsub>trm\<^esub> (Var\<^sup>\<alpha> x)"}\\ |
1981 @{text "\<forall>x. P\<^bsub>trm\<^esub> (Var\<^sup>\<alpha> x)"}\\ |
1985 @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\ |
1982 @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\ |
1986 @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\ |
1983 @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\ |
1987 @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<and> P\<^bsub>trm\<^esub> x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub> (Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\ |
1984 @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<and> P\<^bsub>trm\<^esub> x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub> (Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\ |
1988 @{text "P\<^bsub>pat\<^esub> (PNil\<^sup>\<alpha>)"}\\ |
|
1989 @{text "\<forall>x. P\<^bsub>pat\<^esub> (PVar\<^sup>\<alpha> x)"}\\ |
1985 @{text "\<forall>x. P\<^bsub>pat\<^esub> (PVar\<^sup>\<alpha> x)"}\\ |
1990 @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>pat\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub> (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"} |
1986 @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>pat\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub> (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"} |
1991 \end{array}} |
1987 \end{array}} |
1992 \end{tabular}} |
1988 \end{tabular}} |
1993 \end{equation}\smallskip |
1989 \end{equation}\smallskip |
2135 @{text "\<forall>x c. P\<^bsub>trm\<^esub> c (Var\<^sup>\<alpha> x)"}\\ |
2131 @{text "\<forall>x c. P\<^bsub>trm\<^esub> c (Var\<^sup>\<alpha> x)"}\\ |
2136 @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\ |
2132 @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\ |
2137 @{text "\<forall>x\<^isub>1 x\<^isub>2 c. atom x\<^isub>1 # c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\ |
2133 @{text "\<forall>x\<^isub>1 x\<^isub>2 c. atom x\<^isub>1 # c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\ |
2138 @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3 c. (set (bn\<^sup>\<alpha> x\<^isub>1)) #\<^sup>* c \<and>"}\\ |
2134 @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3 c. (set (bn\<^sup>\<alpha> x\<^isub>1)) #\<^sup>* c \<and>"}\\ |
2139 \hspace{10mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>3) \<Rightarrow> P\<^bsub>trm\<^esub> c (Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\ |
2135 \hspace{10mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>3) \<Rightarrow> P\<^bsub>trm\<^esub> c (Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\ |
2140 @{text "\<forall>c. P\<^bsub>pat\<^esub> c (PNil\<^sup>\<alpha>)"}\\ |
|
2141 @{text "\<forall>x c. P\<^bsub>pat\<^esub> c (PVar\<^sup>\<alpha> x)"}\\ |
2136 @{text "\<forall>x c. P\<^bsub>pat\<^esub> c (PVar\<^sup>\<alpha> x)"}\\ |
2142 @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>pat\<^esub> c (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"} |
2137 @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>pat\<^esub> c (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"} |
2143 \end{array}} |
2138 \end{array}} |
2144 \end{tabular}} |
2139 \end{tabular}} |
2145 \end{equation}\smallskip |
2140 \end{equation}\smallskip |
2198 @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. set (bn\<^sup>\<alpha> x\<^isub>1) #\<^sup>* c \<and> y = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"} |
2193 @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. set (bn\<^sup>\<alpha> x\<^isub>1) #\<^sup>* c \<and> y = Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub>"} |
2199 \end{array}} & |
2194 \end{array}} & |
2200 |
2195 |
2201 \infer{@{text "P\<^bsub>pat\<^esub>"}} |
2196 \infer{@{text "P\<^bsub>pat\<^esub>"}} |
2202 {\begin{array}{@ {}l@ {}} |
2197 {\begin{array}{@ {}l@ {}} |
2203 @{text "y = PNil\<^sup>\<alpha> \<Rightarrow> P\<^bsub>pat\<^esub>"}\\ |
|
2204 @{text "\<forall>x. y = PVar\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>pat\<^esub>"}\\ |
2198 @{text "\<forall>x. y = PVar\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>pat\<^esub>"}\\ |
2205 @{text "\<forall>x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub>"} |
2199 @{text "\<forall>x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub>"} |
2206 \end{array}} |
2200 \end{array}} |
2207 \end{tabular}} |
2201 \end{tabular}} |
2208 \]\smallskip |
2202 \]\smallskip |