Check-in [556662b818]

Not logged in

 2015-04-15 14:32 Fixed module declarations/imports for the new argument pattern for elaborate. check-in: 207908bad1 user: andy tags: trunk 14:31 Fixed a small logical mistake in a footnote. check-in: 556662b818 user: andy tags: trunk 11:48 Added some extra arguments to the premise/conclusion hooks: index (for antecedants), path, and the actual term itself. check-in: f84190c56c user: andy tags: trunk
 1948 1949 1950 1951 1952 1953 1954 1955 1956 1957 1958 1959 1960 1961 1962 1963 1964  \item $\mathsf{nat}(X) -> \mathsf{add}(X,z,X)$. This will require induction on $\mathsf{nat}(X)$. \item Commutativity of $\mathsf{add}$: $\mathsf{nat}(X) \land \mathsf{nat}(Y) -> \mathsf{add}(X,Y,Z) \land \mathsf{add}(Y,X,Z') \land Z = Z'$. \item Totality of $\mathsf{add}$: $\mathsf{nat}(X) \land \mathsf{nat}(Y) -> \mathsf{add}(X,Y,Z) \land \mathsf{nat}(Z)$.\marginnote{Note that in an intuitionistic logic it is much more difficult to prove that $\mathsf{add}$ is \emph{functional}: i.e., that there exists \emph{exactly one} such $Z$.} \item Transitivity of $>$: $\mathsf{nat}(X) \land \mathsf{nat}(Y) \land \mathsf{nat}(Z) \land X < Y \land Y < Z -> X < Z$. \item Cons is idempotent: \\ $\mathsf{natlist}(L) \land \mathsf{elem}(N,L) \land \mathsf{nat}(N') \land L' = cons(N',L) -> \mathsf{elem}(N,L')$   | < > | >  1948 1949 1950 1951 1952 1953 1954 1955 1956 1957 1958 1959 1960 1961 1962 1963 1964 1965  \item $\mathsf{nat}(X) -> \mathsf{add}(X,z,X)$. This will require induction on $\mathsf{nat}(X)$. \item Commutativity of $\mathsf{add}$: $\mathsf{nat}(X) \land \mathsf{nat}(Y) -> \mathsf{add}(X,Y,Z) \land \mathsf{add}(Y,X,Z') \land Z = Z'$. \item Totality of $\mathsf{add}$: $\mathsf{nat}(X) \land \mathsf{nat}(Y) -> \mathsf{add}(X,Y,Z) \land \mathsf{nat}(Z)$. \item Functionality of $\mathsf{add}$: $\mathsf{nat}(X) \land \mathsf{nat}(Y) \land \mathsf{add}(X,Y,Z_1) \land \mathsf{add}(X,Y,Z_2) -> Z_1 = Z_2$. \item Transitivity of $>$: $\mathsf{nat}(X) \land \mathsf{nat}(Y) \land \mathsf{nat}(Z) \land X < Y \land Y < Z -> X < Z$. \item Cons is idempotent: \\ $\mathsf{natlist}(L) \land \mathsf{elem}(N,L) \land \mathsf{nat}(N') \land L' = cons(N',L) -> \mathsf{elem}(N,L')$