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