clasohm@1474: (* Title: CTT/arith clasohm@0: ID: \$Id\$ clasohm@1474: Author: Lawrence C Paulson, Cambridge University Computer Laboratory clasohm@0: Copyright 1991 University of Cambridge clasohm@0: clasohm@0: Arithmetic operators and their definitions clasohm@0: clasohm@0: Proves about elementary arithmetic: addition, multiplication, etc. clasohm@0: Tests definitions and simplifier. clasohm@0: *) clasohm@0: clasohm@0: Arith = CTT + clasohm@0: clasohm@1474: consts "#+","-","|-|" :: "[i,i]=>i" (infixr 65) clasohm@1474: "#*",div,mod :: "[i,i]=>i" (infixr 70) clasohm@0: wenzelm@12110: syntax (xsymbols) paulson@10467: "op #*" :: [i, i] => i (infixr "#\\" 70) paulson@10467: paulson@10467: syntax (HTML output) paulson@10467: "op #*" :: [i, i] => i (infixr "#\\" 70) paulson@10467: clasohm@0: rules wenzelm@3837: add_def "a#+b == rec(a, b, %u v. succ(v))" wenzelm@3837: diff_def "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))" clasohm@0: absdiff_def "a|-|b == (a-b) #+ (b-a)" clasohm@0: mult_def "a#*b == rec(a, 0, %u v. b #+ v)" wenzelm@3837: mod_def "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))" wenzelm@3837: div_def "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))" clasohm@0: end