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