author lcp Fri, 11 Nov 1994 10:50:49 +0100 changeset 705 9fb068497df4 parent 704 b71b6be59354 child 706 31b1e4f9af30
removal of HOL_dup_cs rotation of arguments in split, nat_case, sum_case, list_case
--- a/doc-src/Logics/Old_HOL.tex	Fri Nov 11 10:42:55 1994 +0100
+++ b/doc-src/Logics/Old_HOL.tex	Fri Nov 11 10:50:49 1994 +0100
@@ -847,7 +847,7 @@
& & ordered pairs $\langle a,b\rangle$ \\
\cdx{fst}     & $\alpha\times\beta \To \alpha$        & & first projection\\
\cdx{snd}     & $\alpha\times\beta \To \beta$         & & second projection\\
-  \cdx{split}   & $[\alpha\times\beta, [\alpha,\beta]\To\gamma] \To \gamma$
+  \cdx{split}   & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$
& & generalized projection\\
\cdx{Sigma}  &
$[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
@@ -856,14 +856,14 @@
\begin{ttbox}\makeatletter
\tdx{fst_def}      fst(p)     == @a. ? b. p = <a,b>
\tdx{snd_def}      snd(p)     == @b. ? a. p = <a,b>
-\tdx{split_def}    split(p,c) == c(fst(p),snd(p))
+\tdx{split_def}    split(c,p) == c(fst(p),snd(p))
\tdx{Sigma_def}    Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}

\tdx{Pair_inject}  [| <a, b> = <a',b'>;  [| a=a';  b=b' |] ==> R |] ==> R
\tdx{fst_conv}     fst(<a,b>) = a
\tdx{snd_conv}     snd(<a,b>) = b
-\tdx{split}        split(<a,b>, c) = c(a,b)
+\tdx{split}        split(c, <a,b>) = c(a,b)

\tdx{surjective_pairing}  p = <fst(p),snd(p)>

@@ -881,11 +881,11 @@
\it symbol    & \it meta-type &           & \it description \\
\cdx{Inl}     & $\alpha \To \alpha+\beta$    & & first injection\\
\cdx{Inr}     & $\beta \To \alpha+\beta$     & & second injection\\
-  \cdx{sum_case} & $[\alpha+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$
+  \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
& & conditional
\end{constants}
\begin{ttbox}\makeatletter
-\tdx{sum_case_def}   sum_case == (\%p f g. @z. (!x. p=Inl(x) --> z=f(x)) &
+\tdx{sum_case_def}   sum_case == (\%f g p. @z. (!x. p=Inl(x) --> z=f(x)) &
(!y. p=Inr(y) --> z=g(y)))

\tdx{Inl_not_Inr}    ~ Inl(a)=Inr(b)
@@ -895,10 +895,10 @@

\tdx{sumE}           [| !!x::'a. P(Inl(x));  !!y::'b. P(Inr(y)) |] ==> P(s)

-\tdx{sum_case_Inl}   sum_case(Inl(x), f, g) = f(x)
-\tdx{sum_case_Inr}   sum_case(Inr(x), f, g) = g(x)
+\tdx{sum_case_Inl}   sum_case(f, g, Inl(x)) = f(x)
+\tdx{sum_case_Inr}   sum_case(f, g, Inr(x)) = g(x)

-\tdx{surjective_sum} sum_case(s, \%x::'a. f(Inl(x)), \%y::'b. f(Inr(y))) = f(s)
+\tdx{surjective_sum} sum_case(\%x::'a. f(Inl(x)), \%y::'b. f(Inr(y)), s) = f(s)
\end{ttbox}
\caption{Type $\alpha+\beta$}\label{hol-sum}
\end{figure}
@@ -932,7 +932,6 @@
\begin{ttbox}
prop_cs    : claset
HOL_cs     : claset
-HOL_dup_cs : claset
set_cs     : claset
\end{ttbox}
\begin{ttdescription}
@@ -946,13 +945,6 @@
this classical set is incomplete: quantified formulae are used at most
once.

-\item[\ttindexbold{HOL_dup_cs}] extends {\tt prop_cs} with the safe rules
-  {\tt allI} and~{\tt exE} and the unsafe rules \tdx{all_dupE}
-  and~\tdx{exCI}, as well as rules for unique existence.  Search using
-  this is complete --- quantified formulae may be duplicated --- but
-  frequently fails to terminate.  It is generally unsuitable for
-  depth-first search.
-
\item[\ttindexbold{set_cs}] extends {\tt HOL_cs} with rules for the bounded
quantifiers, subsets, comprehensions, unions and intersections,
complements, finite sets, images and ranges.
@@ -994,7 +986,7 @@
\it symbol    & \it meta-type & \it priority & \it description \\
\cdx{0}       & $nat$         & & zero \\
\cdx{Suc}     & $nat \To nat$ & & successor function\\
-  \cdx{nat_case} & $[nat, \alpha, nat\To\alpha] \To\alpha$
+  \cdx{nat_case} & $[\alpha, nat\To\alpha, nat] \To\alpha$
& & conditional\\
\cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
& & primitive recursor\\
@@ -1008,12 +1000,12 @@
\subcaption{Constants and infixes}

\begin{ttbox}\makeatother
-\tdx{nat_case_def}  nat_case == (\%n a f. @z. (n=0 --> z=a) &
+\tdx{nat_case_def}  nat_case == (\%a f n. @z. (n=0 --> z=a) &
(!x. n=Suc(x) --> z=f(x)))
\tdx{pred_nat_def}  pred_nat == \{p. ? n. p = <n, Suc(n)>\}
\tdx{less_def}      m<n      == <m,n>:pred_nat^+
\tdx{nat_rec_def}   nat_rec(n,c,d) ==
-               wfrec(pred_nat, n, \%l g.nat_case(l, c, \%m.d(m,g(m))))
+               wfrec(pred_nat, n, nat_case(\%g.c, \%m g. d(m,g(m))))

\tdx{add_def}   m+n     == nat_rec(m, n, \%u v.Suc(v))
\tdx{diff_def}  m-n     == nat_rec(n, m, \%u v. nat_rec(v, 0, \%x y.x))
@@ -1040,8 +1032,8 @@
\tdx{pred_natE}
[| p : pred_nat;  !!x n. [| p = <n, Suc(n)> |] ==> R |] ==> R

-\tdx{nat_case_0}     nat_case(0, a, f) = a
-\tdx{nat_case_Suc}   nat_case(Suc(k), a, f) = f(k)
+\tdx{nat_case_0}     nat_case(a, f, 0) = a
+\tdx{nat_case_Suc}   nat_case(a, f, Suc(k)) = f(k)

\tdx{wf_pred_nat}    wf(pred_nat)
\tdx{nat_rec_0}      nat_rec(0,c,h) = c
@@ -1164,8 +1156,8 @@
\tdx{list_rec_Nil}    list_rec([],c,h) = c
\tdx{list_rec_Cons}   list_rec(a#l, c, h) = h(a, l, list_rec(l,c,h))

-\tdx{list_case_Nil}   list_case([],c,h) = c
-\tdx{list_case_Cons}  list_case(x#xs, c, h) = h(x, xs)
+\tdx{list_case_Nil}   list_case(c, h, []) = c
+\tdx{list_case_Cons}  list_case(c, h, x#xs) = h(x, xs)

\tdx{map_Nil}         map(f,[]) = []
\tdx{map_Cons}        map(f, x \# xs) = f(x) \# map(f,xs)
@@ -1210,7 +1202,7 @@
"|" & x"\#"xs & " => " b
\end{array}
& \equiv &
-  "list_case"(e, a, \lambda x\;xs.b)
+  "list_case"(a, \lambda x\;xs.b, e)
\end{eqnarray*}}%
The theory includes \cdx{list_rec}, a primitive recursion operator
for lists.  It is derived from well-founded recursion, a general principle