src/HOL/MicroJava/Comp/NatCanonify.thy
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 13673 2950128b8206
child 16417 9bc16273c2d4
permissions -rw-r--r--
Merged in license change from Isabelle2004
streckem@13673
     1
(*  Title:      HOL/MicroJava/Comp/NatCanonify.thy
streckem@13673
     2
    ID:         $Id$
streckem@13673
     3
    Author:     Martin Strecker
streckem@13673
     4
*)
streckem@13673
     5
streckem@13673
     6
theory NatCanonify = Main:
streckem@13673
     7
streckem@13673
     8
(************************************************************************)
streckem@13673
     9
  (* Canonizer for converting nat to int *)
streckem@13673
    10
(************************************************************************)
streckem@13673
    11
streckem@13673
    12
lemma nat_add_canonify: "(n1::nat) + n2 = nat ((int n1) + (int n2))"
streckem@13673
    13
by (simp add: nat_add_distrib)
streckem@13673
    14
streckem@13673
    15
lemma nat_mult_canonify: "(n1::nat) * n2 = nat ((int n1) * (int n2))"
streckem@13673
    16
by (simp add: nat_mult_distrib)
streckem@13673
    17
streckem@13673
    18
lemma nat_diff_canonify: "(n1::nat) - n2 = 
streckem@13673
    19
  nat (if (int n1) \<le> (int n2) then 0 else (int n1) - (int n2))"
streckem@13673
    20
by (simp add: zdiff_int nat_int)
streckem@13673
    21
streckem@13673
    22
lemma nat_le_canonify: "((n1::nat) \<le> n2) = ((int n1) \<le> (int n2))"
streckem@13673
    23
by arith
streckem@13673
    24
streckem@13673
    25
lemma nat_less_canonify: "((n1::nat) < n2) = ((int n1) < (int n2))"
streckem@13673
    26
by arith
streckem@13673
    27
streckem@13673
    28
lemma nat_eq_canonify: "((n1::nat) = n2) = ((int n1) = (int n2))"
streckem@13673
    29
by arith
streckem@13673
    30
streckem@13673
    31
lemma nat_if_canonify: "(if b then (n1::nat) else n2) =
streckem@13673
    32
  nat (if b then (int n1) else (int n2))"
streckem@13673
    33
by simp
streckem@13673
    34
streckem@13673
    35
lemma int_nat_canonify: "(int (nat n)) = (if 0 \<le> n then n else 0)"
streckem@13673
    36
by simp
streckem@13673
    37
streckem@13673
    38
lemmas nat_canonify = 
streckem@13673
    39
  nat_add_canonify nat_mult_canonify nat_diff_canonify 
streckem@13673
    40
  nat_le_canonify nat_less_canonify nat_eq_canonify nat_if_canonify 
streckem@13673
    41
  int_nat_canonify nat_int
streckem@13673
    42
streckem@13673
    43
end