equal
deleted
inserted
replaced
|
1 (* Title: HOL/MicroJava/Comp/NatCanonify.thy |
|
2 ID: $Id$ |
|
3 Author: Martin Strecker |
|
4 Copyright GPL 2002 |
|
5 *) |
|
6 |
|
7 theory NatCanonify = Main: |
|
8 |
|
9 (************************************************************************) |
|
10 (* Canonizer for converting nat to int *) |
|
11 (************************************************************************) |
|
12 |
|
13 lemma nat_add_canonify: "(n1::nat) + n2 = nat ((int n1) + (int n2))" |
|
14 by (simp add: nat_add_distrib) |
|
15 |
|
16 lemma nat_mult_canonify: "(n1::nat) * n2 = nat ((int n1) * (int n2))" |
|
17 by (simp add: nat_mult_distrib) |
|
18 |
|
19 lemma nat_diff_canonify: "(n1::nat) - n2 = |
|
20 nat (if (int n1) \<le> (int n2) then 0 else (int n1) - (int n2))" |
|
21 by (simp add: zdiff_int nat_int) |
|
22 |
|
23 lemma nat_le_canonify: "((n1::nat) \<le> n2) = ((int n1) \<le> (int n2))" |
|
24 by arith |
|
25 |
|
26 lemma nat_less_canonify: "((n1::nat) < n2) = ((int n1) < (int n2))" |
|
27 by arith |
|
28 |
|
29 lemma nat_eq_canonify: "((n1::nat) = n2) = ((int n1) = (int n2))" |
|
30 by arith |
|
31 |
|
32 lemma nat_if_canonify: "(if b then (n1::nat) else n2) = |
|
33 nat (if b then (int n1) else (int n2))" |
|
34 by simp |
|
35 |
|
36 lemma int_nat_canonify: "(int (nat n)) = (if 0 \<le> n then n else 0)" |
|
37 by simp |
|
38 |
|
39 lemmas nat_canonify = |
|
40 nat_add_canonify nat_mult_canonify nat_diff_canonify |
|
41 nat_le_canonify nat_less_canonify nat_eq_canonify nat_if_canonify |
|
42 int_nat_canonify nat_int |
|
43 |
|
44 end |