Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/Tools/ComputeNumeral.thy
changeset 25919 8b1c0d434824
parent 23664 9c486517354a
child 26075 815f3ccc0b45
equal deleted inserted replaced
25918:82dd239e0f65 25919:8b1c0d434824 
     4 
     4 
     5 (* normalization of bit strings *)
 
     5 (* normalization of bit strings *)
 
     6 lemmas bitnorm = Pls_0_eq Min_1_eq
 
     6 lemmas bitnorm = Pls_0_eq Min_1_eq
 
     7 
     7 
     8 (* neg for bit strings *)
 
     8 (* neg for bit strings *)
 
     9 lemma neg1: "neg Numeral.Pls = False" by (simp add: Numeral.Pls_def)
 
     9 lemma neg1: "neg Int.Pls = False" by (simp add: Int.Pls_def)
 
    10 lemma neg2: "neg Numeral.Min = True" apply (subst Numeral.Min_def) by auto
 
    10 lemma neg2: "neg Int.Min = True" apply (subst Int.Min_def) by auto
 
    11 lemma neg3: "neg (x BIT Numeral.B0) = neg x" apply (simp add: neg_def) apply (subst Bit_def) by auto
 
    11 lemma neg3: "neg (x BIT Int.B0) = neg x" apply (simp add: neg_def) apply (subst Bit_def) by auto
 
    12 lemma neg4: "neg (x BIT Numeral.B1) = neg x" apply (simp add: neg_def) apply (subst Bit_def) by auto  
    12 lemma neg4: "neg (x BIT Int.B1) = neg x" apply (simp add: neg_def) apply (subst Bit_def) by auto  
    13 lemmas bitneg = neg1 neg2 neg3 neg4
 
    13 lemmas bitneg = neg1 neg2 neg3 neg4
 
    14 
    14 
    15 (* iszero for bit strings *)
 
    15 (* iszero for bit strings *)
 
    16 lemma iszero1: "iszero Numeral.Pls = True" by (simp add: Numeral.Pls_def iszero_def)
 
    16 lemma iszero1: "iszero Int.Pls = True" by (simp add: Int.Pls_def iszero_def)
 
    17 lemma iszero2: "iszero Numeral.Min = False" apply (subst Numeral.Min_def) apply (subst iszero_def) by simp
 
    17 lemma iszero2: "iszero Int.Min = False" apply (subst Int.Min_def) apply (subst iszero_def) by simp
 
    18 lemma iszero3: "iszero (x BIT Numeral.B0) = iszero x" apply (subst Numeral.Bit_def) apply (subst iszero_def)+ by auto
 
    18 lemma iszero3: "iszero (x BIT Int.B0) = iszero x" apply (subst Int.Bit_def) apply (subst iszero_def)+ by auto
 
    19 lemma iszero4: "iszero (x BIT Numeral.B1) = False" apply (subst Numeral.Bit_def) apply (subst iszero_def)+  apply simp by arith
 
    19 lemma iszero4: "iszero (x BIT Int.B1) = False" apply (subst Int.Bit_def) apply (subst iszero_def)+  apply simp by arith
 
    20 lemmas bitiszero = iszero1 iszero2 iszero3 iszero4
 
    20 lemmas bitiszero = iszero1 iszero2 iszero3 iszero4
 
    21 
    21 
    22 (* lezero for bit strings *)
 
    22 (* lezero for bit strings *)
 
    23 constdefs
 
    23 constdefs
 
    24   "lezero x == (x \<le> 0)"
 
    24   "lezero x == (x \<le> 0)"
 
    25 lemma lezero1: "lezero Numeral.Pls = True" unfolding Numeral.Pls_def lezero_def by auto
 
    25 lemma lezero1: "lezero Int.Pls = True" unfolding Int.Pls_def lezero_def by auto
 
    26 lemma lezero2: "lezero Numeral.Min = True" unfolding Numeral.Min_def lezero_def by auto
 
    26 lemma lezero2: "lezero Int.Min = True" unfolding Int.Min_def lezero_def by auto
 
    27 lemma lezero3: "lezero (x BIT Numeral.B0) = lezero x" unfolding Numeral.Bit_def lezero_def by auto
 
    27 lemma lezero3: "lezero (x BIT Int.B0) = lezero x" unfolding Int.Bit_def lezero_def by auto
 
    28 lemma lezero4: "lezero (x BIT Numeral.B1) = neg x" unfolding Numeral.Bit_def lezero_def neg_def by auto
 
    28 lemma lezero4: "lezero (x BIT Int.B1) = neg x" unfolding Int.Bit_def lezero_def neg_def by auto
 
    29 lemmas bitlezero = lezero1 lezero2 lezero3 lezero4
 
    29 lemmas bitlezero = lezero1 lezero2 lezero3 lezero4
 
    30 
    30 
    31 (* equality for bit strings *)
 
    31 (* equality for bit strings *)
 
    32 lemma biteq1: "(Numeral.Pls = Numeral.Pls) = True" by auto
 
    32 lemma biteq1: "(Int.Pls = Int.Pls) = True" by auto
 
    33 lemma biteq2: "(Numeral.Min = Numeral.Min) = True" by auto
 
    33 lemma biteq2: "(Int.Min = Int.Min) = True" by auto
 
    34 lemma biteq3: "(Numeral.Pls = Numeral.Min) = False" unfolding Pls_def Min_def by auto
 
    34 lemma biteq3: "(Int.Pls = Int.Min) = False" unfolding Pls_def Min_def by auto
 
    35 lemma biteq4: "(Numeral.Min = Numeral.Pls) = False" unfolding Pls_def Min_def by auto
 
    35 lemma biteq4: "(Int.Min = Int.Pls) = False" unfolding Pls_def Min_def by auto
 
    36 lemma biteq5: "(x BIT Numeral.B0 = y BIT Numeral.B0) = (x = y)" unfolding Bit_def by auto
 
    36 lemma biteq5: "(x BIT Int.B0 = y BIT Int.B0) = (x = y)" unfolding Bit_def by auto
 
    37 lemma biteq6: "(x BIT Numeral.B1 = y BIT Numeral.B1) = (x = y)" unfolding Bit_def by auto
 
    37 lemma biteq6: "(x BIT Int.B1 = y BIT Int.B1) = (x = y)" unfolding Bit_def by auto
 
    38 lemma biteq7: "(x BIT Numeral.B0 = y BIT Numeral.B1) = False" unfolding Bit_def by (simp, arith) 
    38 lemma biteq7: "(x BIT Int.B0 = y BIT Int.B1) = False" unfolding Bit_def by (simp, arith) 
    39 lemma biteq8: "(x BIT Numeral.B1 = y BIT Numeral.B0) = False" unfolding Bit_def by (simp, arith)
 
    39 lemma biteq8: "(x BIT Int.B1 = y BIT Int.B0) = False" unfolding Bit_def by (simp, arith)
 
    40 lemma biteq9: "(Numeral.Pls = x BIT Numeral.B0) = (Numeral.Pls = x)" unfolding Bit_def Pls_def by auto
 
    40 lemma biteq9: "(Int.Pls = x BIT Int.B0) = (Int.Pls = x)" unfolding Bit_def Pls_def by auto
 
    41 lemma biteq10: "(Numeral.Pls = x BIT Numeral.B1) = False" unfolding Bit_def Pls_def by (simp, arith) 
    41 lemma biteq10: "(Int.Pls = x BIT Int.B1) = False" unfolding Bit_def Pls_def by (simp, arith) 
    42 lemma biteq11: "(Numeral.Min = x BIT Numeral.B0) = False" unfolding Bit_def Min_def by (simp, arith)
 
    42 lemma biteq11: "(Int.Min = x BIT Int.B0) = False" unfolding Bit_def Min_def by (simp, arith)
 
    43 lemma biteq12: "(Numeral.Min = x BIT Numeral.B1) = (Numeral.Min = x)" unfolding Bit_def Min_def by auto
 
    43 lemma biteq12: "(Int.Min = x BIT Int.B1) = (Int.Min = x)" unfolding Bit_def Min_def by auto
 
    44 lemma biteq13: "(x BIT Numeral.B0 = Numeral.Pls) = (x = Numeral.Pls)" unfolding Bit_def Pls_def by auto
 
    44 lemma biteq13: "(x BIT Int.B0 = Int.Pls) = (x = Int.Pls)" unfolding Bit_def Pls_def by auto
 
    45 lemma biteq14: "(x BIT Numeral.B1 = Numeral.Pls) = False" unfolding Bit_def Pls_def by (simp, arith)
 
    45 lemma biteq14: "(x BIT Int.B1 = Int.Pls) = False" unfolding Bit_def Pls_def by (simp, arith)
 
    46 lemma biteq15: "(x BIT Numeral.B0 = Numeral.Min) = False" unfolding Bit_def Pls_def Min_def by (simp, arith)
 
    46 lemma biteq15: "(x BIT Int.B0 = Int.Min) = False" unfolding Bit_def Pls_def Min_def by (simp, arith)
 
    47 lemma biteq16: "(x BIT Numeral.B1 = Numeral.Min) = (x = Numeral.Min)" unfolding Bit_def Min_def by (simp, arith)
 
    47 lemma biteq16: "(x BIT Int.B1 = Int.Min) = (x = Int.Min)" unfolding Bit_def Min_def by (simp, arith)
 
    48 lemmas biteq = biteq1 biteq2 biteq3 biteq4 biteq5 biteq6 biteq7 biteq8 biteq9 biteq10 biteq11 biteq12 biteq13 biteq14 biteq15 biteq16
 
    48 lemmas biteq = biteq1 biteq2 biteq3 biteq4 biteq5 biteq6 biteq7 biteq8 biteq9 biteq10 biteq11 biteq12 biteq13 biteq14 biteq15 biteq16
 
    49 
    49 
    50 (* x < y for bit strings *)
 
    50 (* x < y for bit strings *)
 
    51 lemma bitless1: "(Numeral.Pls < Numeral.Min) = False" unfolding Pls_def Min_def by auto
 
    51 lemma bitless1: "(Int.Pls < Int.Min) = False" unfolding Pls_def Min_def by auto
 
    52 lemma bitless2: "(Numeral.Pls < Numeral.Pls) = False" by auto
 
    52 lemma bitless2: "(Int.Pls < Int.Pls) = False" by auto
 
    53 lemma bitless3: "(Numeral.Min < Numeral.Pls) = True" unfolding Pls_def Min_def by auto
 
    53 lemma bitless3: "(Int.Min < Int.Pls) = True" unfolding Pls_def Min_def by auto
 
    54 lemma bitless4: "(Numeral.Min < Numeral.Min) = False" unfolding Pls_def Min_def by auto
 
    54 lemma bitless4: "(Int.Min < Int.Min) = False" unfolding Pls_def Min_def by auto
 
    55 lemma bitless5: "(x BIT Numeral.B0 < y BIT Numeral.B0) = (x < y)" unfolding Bit_def by auto
 
    55 lemma bitless5: "(x BIT Int.B0 < y BIT Int.B0) = (x < y)" unfolding Bit_def by auto
 
    56 lemma bitless6: "(x BIT Numeral.B1 < y BIT Numeral.B1) = (x < y)" unfolding Bit_def by auto
 
    56 lemma bitless6: "(x BIT Int.B1 < y BIT Int.B1) = (x < y)" unfolding Bit_def by auto
 
    57 lemma bitless7: "(x BIT Numeral.B0 < y BIT Numeral.B1) = (x \<le> y)" unfolding Bit_def by auto
 
    57 lemma bitless7: "(x BIT Int.B0 < y BIT Int.B1) = (x \<le> y)" unfolding Bit_def by auto
 
    58 lemma bitless8: "(x BIT Numeral.B1 < y BIT Numeral.B0) = (x < y)" unfolding Bit_def by auto
 
    58 lemma bitless8: "(x BIT Int.B1 < y BIT Int.B0) = (x < y)" unfolding Bit_def by auto
 
    59 lemma bitless9: "(Numeral.Pls < x BIT Numeral.B0) = (Numeral.Pls < x)" unfolding Bit_def Pls_def by auto
 
    59 lemma bitless9: "(Int.Pls < x BIT Int.B0) = (Int.Pls < x)" unfolding Bit_def Pls_def by auto
 
    60 lemma bitless10: "(Numeral.Pls < x BIT Numeral.B1) = (Numeral.Pls \<le> x)" unfolding Bit_def Pls_def by auto
 
    60 lemma bitless10: "(Int.Pls < x BIT Int.B1) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def by auto
 
    61 lemma bitless11: "(Numeral.Min < x BIT Numeral.B0) = (Numeral.Pls \<le> x)" unfolding Bit_def Pls_def Min_def by auto
 
    61 lemma bitless11: "(Int.Min < x BIT Int.B0) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def Min_def by auto
 
    62 lemma bitless12: "(Numeral.Min < x BIT Numeral.B1) = (Numeral.Min < x)" unfolding Bit_def Min_def by auto
 
    62 lemma bitless12: "(Int.Min < x BIT Int.B1) = (Int.Min < x)" unfolding Bit_def Min_def by auto
 
    63 lemma bitless13: "(x BIT Numeral.B0 < Numeral.Pls) = (x < Numeral.Pls)" unfolding Bit_def Pls_def by auto
 
    63 lemma bitless13: "(x BIT Int.B0 < Int.Pls) = (x < Int.Pls)" unfolding Bit_def Pls_def by auto
 
    64 lemma bitless14: "(x BIT Numeral.B1 < Numeral.Pls) = (x < Numeral.Pls)" unfolding Bit_def Pls_def by auto
 
    64 lemma bitless14: "(x BIT Int.B1 < Int.Pls) = (x < Int.Pls)" unfolding Bit_def Pls_def by auto
 
    65 lemma bitless15: "(x BIT Numeral.B0 < Numeral.Min) = (x < Numeral.Pls)" unfolding Bit_def Pls_def Min_def by auto
 
    65 lemma bitless15: "(x BIT Int.B0 < Int.Min) = (x < Int.Pls)" unfolding Bit_def Pls_def Min_def by auto
 
    66 lemma bitless16: "(x BIT Numeral.B1 < Numeral.Min) = (x < Numeral.Min)" unfolding Bit_def Min_def by auto
 
    66 lemma bitless16: "(x BIT Int.B1 < Int.Min) = (x < Int.Min)" unfolding Bit_def Min_def by auto
 
    67 lemmas bitless = bitless1 bitless2 bitless3 bitless4 bitless5 bitless6 bitless7 bitless8 
    67 lemmas bitless = bitless1 bitless2 bitless3 bitless4 bitless5 bitless6 bitless7 bitless8 
    68                  bitless9 bitless10 bitless11 bitless12 bitless13 bitless14 bitless15 bitless16
 
    68                  bitless9 bitless10 bitless11 bitless12 bitless13 bitless14 bitless15 bitless16
 
    69 
    69 
    70 (* x \<le> y for bit strings *)
 
    70 (* x \<le> y for bit strings *)
 
    71 lemma bitle1: "(Numeral.Pls \<le> Numeral.Min) = False" unfolding Pls_def Min_def by auto
 
    71 lemma bitle1: "(Int.Pls \<le> Int.Min) = False" unfolding Pls_def Min_def by auto
 
    72 lemma bitle2: "(Numeral.Pls \<le> Numeral.Pls) = True" by auto
 
    72 lemma bitle2: "(Int.Pls \<le> Int.Pls) = True" by auto
 
    73 lemma bitle3: "(Numeral.Min \<le> Numeral.Pls) = True" unfolding Pls_def Min_def by auto
 
    73 lemma bitle3: "(Int.Min \<le> Int.Pls) = True" unfolding Pls_def Min_def by auto
 
    74 lemma bitle4: "(Numeral.Min \<le> Numeral.Min) = True" unfolding Pls_def Min_def by auto
 
    74 lemma bitle4: "(Int.Min \<le> Int.Min) = True" unfolding Pls_def Min_def by auto
 
    75 lemma bitle5: "(x BIT Numeral.B0 \<le> y BIT Numeral.B0) = (x \<le> y)" unfolding Bit_def by auto
 
    75 lemma bitle5: "(x BIT Int.B0 \<le> y BIT Int.B0) = (x \<le> y)" unfolding Bit_def by auto
 
    76 lemma bitle6: "(x BIT Numeral.B1 \<le> y BIT Numeral.B1) = (x \<le> y)" unfolding Bit_def by auto
 
    76 lemma bitle6: "(x BIT Int.B1 \<le> y BIT Int.B1) = (x \<le> y)" unfolding Bit_def by auto
 
    77 lemma bitle7: "(x BIT Numeral.B0 \<le> y BIT Numeral.B1) = (x \<le> y)" unfolding Bit_def by auto
 
    77 lemma bitle7: "(x BIT Int.B0 \<le> y BIT Int.B1) = (x \<le> y)" unfolding Bit_def by auto
 
    78 lemma bitle8: "(x BIT Numeral.B1 \<le> y BIT Numeral.B0) = (x < y)" unfolding Bit_def by auto
 
    78 lemma bitle8: "(x BIT Int.B1 \<le> y BIT Int.B0) = (x < y)" unfolding Bit_def by auto
 
    79 lemma bitle9: "(Numeral.Pls \<le> x BIT Numeral.B0) = (Numeral.Pls \<le> x)" unfolding Bit_def Pls_def by auto
 
    79 lemma bitle9: "(Int.Pls \<le> x BIT Int.B0) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def by auto
 
    80 lemma bitle10: "(Numeral.Pls \<le> x BIT Numeral.B1) = (Numeral.Pls \<le> x)" unfolding Bit_def Pls_def by auto
 
    80 lemma bitle10: "(Int.Pls \<le> x BIT Int.B1) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def by auto
 
    81 lemma bitle11: "(Numeral.Min \<le> x BIT Numeral.B0) = (Numeral.Pls \<le> x)" unfolding Bit_def Pls_def Min_def by auto
 
    81 lemma bitle11: "(Int.Min \<le> x BIT Int.B0) = (Int.Pls \<le> x)" unfolding Bit_def Pls_def Min_def by auto
 
    82 lemma bitle12: "(Numeral.Min \<le> x BIT Numeral.B1) = (Numeral.Min \<le> x)" unfolding Bit_def Min_def by auto
 
    82 lemma bitle12: "(Int.Min \<le> x BIT Int.B1) = (Int.Min \<le> x)" unfolding Bit_def Min_def by auto
 
    83 lemma bitle13: "(x BIT Numeral.B0 \<le> Numeral.Pls) = (x \<le> Numeral.Pls)" unfolding Bit_def Pls_def by auto
 
    83 lemma bitle13: "(x BIT Int.B0 \<le> Int.Pls) = (x \<le> Int.Pls)" unfolding Bit_def Pls_def by auto
 
    84 lemma bitle14: "(x BIT Numeral.B1 \<le> Numeral.Pls) = (x < Numeral.Pls)" unfolding Bit_def Pls_def by auto
 
    84 lemma bitle14: "(x BIT Int.B1 \<le> Int.Pls) = (x < Int.Pls)" unfolding Bit_def Pls_def by auto
 
    85 lemma bitle15: "(x BIT Numeral.B0 \<le> Numeral.Min) = (x < Numeral.Pls)" unfolding Bit_def Pls_def Min_def by auto
 
    85 lemma bitle15: "(x BIT Int.B0 \<le> Int.Min) = (x < Int.Pls)" unfolding Bit_def Pls_def Min_def by auto
 
    86 lemma bitle16: "(x BIT Numeral.B1 \<le> Numeral.Min) = (x \<le> Numeral.Min)" unfolding Bit_def Min_def by auto
 
    86 lemma bitle16: "(x BIT Int.B1 \<le> Int.Min) = (x \<le> Int.Min)" unfolding Bit_def Min_def by auto
 
    87 lemmas bitle = bitle1 bitle2 bitle3 bitle4 bitle5 bitle6 bitle7 bitle8 
    87 lemmas bitle = bitle1 bitle2 bitle3 bitle4 bitle5 bitle6 bitle7 bitle8 
    88                  bitle9 bitle10 bitle11 bitle12 bitle13 bitle14 bitle15 bitle16
 
    88                  bitle9 bitle10 bitle11 bitle12 bitle13 bitle14 bitle15 bitle16
 
    89 
    89 
    90 (* succ for bit strings *)
 
    90 (* succ for bit strings *)
 
    91 lemmas bitsucc = succ_Pls succ_Min succ_1 succ_0
 
    91 lemmas bitsucc = succ_Pls succ_Min succ_1 succ_0
 
    95 
    95 
    96 (* unary minus for bit strings *)
 
    96 (* unary minus for bit strings *)
 
    97 lemmas bituminus = minus_Pls minus_Min minus_1 minus_0 
    97 lemmas bituminus = minus_Pls minus_Min minus_1 minus_0 
    98 
    98 
    99 (* addition for bit strings *)
 
    99 (* addition for bit strings *)
 
   100 lemmas bitadd = add_Pls add_Pls_right add_Min add_Min_right add_BIT_11 add_BIT_10 add_BIT_0[where b="Numeral.B0"] add_BIT_0[where b="Numeral.B1"]
 
   100 lemmas bitadd = add_Pls add_Pls_right add_Min add_Min_right add_BIT_11 add_BIT_10 add_BIT_0[where b="Int.B0"] add_BIT_0[where b="Int.B1"]
 
   101 
   101 
   102 (* multiplication for bit strings *) 
   102 (* multiplication for bit strings *) 
   103 lemma mult_Pls_right: "x * Numeral.Pls = Numeral.Pls" by (simp add: Pls_def)
 
   103 lemma mult_Pls_right: "x * Int.Pls = Int.Pls" by (simp add: Pls_def)
 
   104 lemma mult_Min_right: "x * Numeral.Min = - x" by (subst mult_commute, simp add: mult_Min)
 
   104 lemma mult_Min_right: "x * Int.Min = - x" by (subst mult_commute, simp add: mult_Min)
 
   105 lemma multb0x: "(x BIT Numeral.B0) * y = (x * y) BIT Numeral.B0" unfolding Bit_def by simp
 
   105 lemma multb0x: "(x BIT Int.B0) * y = (x * y) BIT Int.B0" unfolding Bit_def by simp
 
   106 lemma multxb0: "x * (y BIT Numeral.B0) = (x * y) BIT Numeral.B0" unfolding Bit_def by simp
 
   106 lemma multxb0: "x * (y BIT Int.B0) = (x * y) BIT Int.B0" unfolding Bit_def by simp
 
   107 lemma multb1: "(x BIT Numeral.B1) * (y BIT Numeral.B1) = (((x * y) BIT Numeral.B0) + x + y) BIT Numeral.B1"
 
   107 lemma multb1: "(x BIT Int.B1) * (y BIT Int.B1) = (((x * y) BIT Int.B0) + x + y) BIT Int.B1"
 
   108   unfolding Bit_def by (simp add: ring_simps)
 
   108   unfolding Bit_def by (simp add: ring_simps)
 
   109 lemmas bitmul = mult_Pls mult_Min mult_Pls_right mult_Min_right multb0x multxb0 multb1
 
   109 lemmas bitmul = mult_Pls mult_Min mult_Pls_right mult_Min_right multb0x multxb0 multb1
 
   110 
   110 
   111 lemmas bitarith = bitnorm bitiszero bitneg bitlezero biteq bitless bitle bitsucc bitpred bituminus bitadd bitmul 
   111 lemmas bitarith = bitnorm bitiszero bitneg bitlezero biteq bitless bitle bitsucc bitpred bituminus bitadd bitmul 
   112 
   112 
   118   unfolding lezero_def iszero_def neg_def
 
   118   unfolding lezero_def iszero_def neg_def
 
   119   apply (simp add: number_of_is_id)
 
   119   apply (simp add: number_of_is_id)
 
   120   done
 
   120   done
 
   121 
   121 
   122 (* Normalization of nat literals *)
 
   122 (* Normalization of nat literals *)
 
   123 lemma natnorm0: "(0::nat) = number_of (Numeral.Pls)" by auto
 
   123 lemma natnorm0: "(0::nat) = number_of (Int.Pls)" by auto
 
   124 lemma natnorm1: "(1 :: nat) = number_of (Numeral.Pls BIT Numeral.B1)"  by auto 
   124 lemma natnorm1: "(1 :: nat) = number_of (Int.Pls BIT Int.B1)"  by auto 
   125 lemmas natnorm = natnorm0 natnorm1 nat_norm_number_of
 
   125 lemmas natnorm = natnorm0 natnorm1 nat_norm_number_of
 
   126 
   126 
   127 (* Suc *)
 
   127 (* Suc *)
 
   128 lemma natsuc: "Suc (number_of x) = (if neg x then 1 else number_of (Numeral.succ x))" by (auto simp add: number_of_is_id)
 
   128 lemma natsuc: "Suc (number_of x) = (if neg x then 1 else number_of (Int.succ x))" by (auto simp add: number_of_is_id)
 
   129 
   129 
   130 (* Addition for nat *)
 
   130 (* Addition for nat *)
 
   131 lemma natadd: "number_of x + ((number_of y)::nat) = (if neg x then (number_of y) else (if neg y then number_of x else (number_of (x + y))))"
 
   131 lemma natadd: "number_of x + ((number_of y)::nat) = (if neg x then (number_of y) else (if neg y then number_of x else (number_of (x + y))))"
 
   132   by (auto simp add: number_of_is_id)
 
   132   by (auto simp add: number_of_is_id)
 
   133 
   133 
   218 
   218 
   219 
   219 
   220 
   220 
   221 (* collecting all the theorems *)
 
   221 (* collecting all the theorems *)
 
   222 
   222 
   223 lemma even_Pls: "even (Numeral.Pls) = True"
 
   223 lemma even_Pls: "even (Int.Pls) = True"
 
   224   apply (unfold Pls_def even_def)
 
   224   apply (unfold Pls_def even_def)
 
   225   by simp
 
   225   by simp
 
   226 
   226 
   227 lemma even_Min: "even (Numeral.Min) = False"
 
   227 lemma even_Min: "even (Int.Min) = False"
 
   228   apply (unfold Min_def even_def)
 
   228   apply (unfold Min_def even_def)
 
   229   by simp
 
   229   by simp
 
   230 
   230 
   231 lemma even_B0: "even (x BIT Numeral.B0) = True"
 
   231 lemma even_B0: "even (x BIT Int.B0) = True"
 
   232   apply (unfold Bit_def)
 
   232   apply (unfold Bit_def)
 
   233   by simp
 
   233   by simp
 
   234 
   234 
   235 lemma even_B1: "even (x BIT Numeral.B1) = False"
 
   235 lemma even_B1: "even (x BIT Int.B1) = False"
 
   236   apply (unfold Bit_def)
 
   236   apply (unfold Bit_def)
 
   237   by simp
 
   237   by simp
 
   238 
   238 
   239 lemma even_number_of: "even ((number_of w)::int) = even w"
 
   239 lemma even_number_of: "even ((number_of w)::int) = even w"
 
   240   by (simp only: number_of_is_id)
 
   240   by (simp only: number_of_is_id)
wneuper/isa