summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/CTT/Arith.thy

changeset 1474 | 3f7d67927fe2 |

parent 0 | a5a9c433f639 |

child 3837 | d7f033c74b38 |

equal
deleted
inserted
replaced

1473:e8d4606e6502 | 1474:3f7d67927fe2 |
---|---|

1 (* Title: CTT/arith |
1 (* Title: CTT/arith |

2 ID: $Id$ |
2 ID: $Id$ |

3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |

4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |

5 |
5 |

6 Arithmetic operators and their definitions |
6 Arithmetic operators and their definitions |

7 |
7 |

8 Proves about elementary arithmetic: addition, multiplication, etc. |
8 Proves about elementary arithmetic: addition, multiplication, etc. |

9 Tests definitions and simplifier. |
9 Tests definitions and simplifier. |

10 *) |
10 *) |

11 |
11 |

12 Arith = CTT + |
12 Arith = CTT + |

13 |
13 |

14 consts "#+","-","|-|" :: "[i,i]=>i" (infixr 65) |
14 consts "#+","-","|-|" :: "[i,i]=>i" (infixr 65) |

15 "#*",div,mod :: "[i,i]=>i" (infixr 70) |
15 "#*",div,mod :: "[i,i]=>i" (infixr 70) |

16 |
16 |

17 rules |
17 rules |

18 add_def "a#+b == rec(a, b, %u v.succ(v))" |
18 add_def "a#+b == rec(a, b, %u v.succ(v))" |

19 diff_def "a-b == rec(b, a, %u v.rec(v, 0, %x y.x))" |
19 diff_def "a-b == rec(b, a, %u v.rec(v, 0, %x y.x))" |

20 absdiff_def "a|-|b == (a-b) #+ (b-a)" |
20 absdiff_def "a|-|b == (a-b) #+ (b-a)" |