Theory Bits

theory Bits
imports IntMod BitRing
begin

typedef (open) 'a bits = "{0::int..<2 ^ nat_of_type TYPE('a::numeral1)}"
by (rule_tac x=0 in exI, simp add: zero_less_power)

lemma one_less_power: -- "belongs in Power.thy"
  "[|1 < (a::'a::{ordered_semidom,recpower}); 0 < n|] ==> 1 < a ^ n"
by (cases n, simp, simp add: power_gt1)

constdefs
  Abs_bits' :: "int => 'a::numeral1 bits"
  "Abs_bits' x ≡ Abs_bits (x mod (2 ^ nat_of_type TYPE('a)))"

instance bits :: (numeral1) "{zero,one,plus,times,minus,power,bit}" ..

defs (overloaded)
  zero_bits_def: "0 ≡ Abs_bits 0"
  one_bits_def:  "1 ≡ Abs_bits 1"
  add_bits_def:  "x + y ≡ Abs_bits' (Rep_bits x + Rep_bits y)"
  mult_bits_def: "x * y ≡ Abs_bits' (Rep_bits x * Rep_bits y)"
  diff_bits_def: "x - y ≡ Abs_bits' (Rep_bits x - Rep_bits y)"
  minus_bits_def: "- x ≡ Abs_bits' (- Rep_bits x)"
  power_bits_def: "x ^ n ≡ Abs_bits' (Rep_bits x ^ n)"
  NOT_bits_def: "NOT x ≡ Abs_bits' (NOT Rep_bits x)"
  AND_bits_def: "x AND y ≡ Abs_bits' (Rep_bits x AND Rep_bits y)"
  OR_bits_def: "x OR y ≡ Abs_bits' (Rep_bits x OR Rep_bits y)"
  XOR_bits_def: "x XOR y ≡ Abs_bits' (Rep_bits x XOR Rep_bits y)"

interpretation bits:
  mod_type ["2 ^ nat_of_type TYPE('a::numeral1)"
            "Rep_bits::'a::numeral1 bits => int"
            "Abs_bits::int => 'a::numeral1 bits"]
apply (rule mod_type.intro)
apply (rule type_definition_bits)
apply (rule one_less_power, simp)
apply (rule zero_less_nat_of_type)
apply (rule zero_bits_def)
apply (rule one_bits_def)
apply (rule add_bits_def [unfolded Abs_bits'_def])
apply (rule mult_bits_def [unfolded Abs_bits'_def])
apply (rule diff_bits_def [unfolded Abs_bits'_def])
apply (rule minus_bits_def [unfolded Abs_bits'_def])
apply (rule power_bits_def [unfolded Abs_bits'_def])
done

instance bits :: (numeral1) comm_ring_1
by (rule bits.comm_ring_1)

instance bits :: (numeral1) recpower
by (rule bits.recpower)

instance bits :: (numeral1) number ..

defs (overloaded)
  number_bits_def: "number_of w::_ bits ≡ of_int w"

instance bits :: (numeral1) number_ring
by intro_classes (simp add: number_bits_def)

interpretation bits:
  mod_ring ["2 ^ nat_of_type TYPE('a::numeral1)"
            "Rep_bits::'a::numeral1 bits => int"
            "Abs_bits::int => 'a::numeral1 bits"] .

lemma bits_iszero_number_of [unfolded nat_of_type_def, simp]:
  "iszero (number_of w::'a::numeral1 bits) =
   (number_of w mod 2 ^ nat_of_type TYPE('a) = (0::int))"
by (rule bits.iszero_number_of)

subsection {* @{text bit_ring} instance *}

lemmas bits_bit_defs = 
  NOT_bits_def AND_bits_def OR_bits_def XOR_bits_def

instance bits :: (numeral1) bit_ring
apply (intro_classes)
apply (unfold bits_bit_defs Abs_bits'_def)
apply (simp_all add: bits.Rep_inject_sym bits.of_int_eq
                     bits.Rep_Abs_mod bits.Rep_0 bits.Rep_number_of)
apply (simp_all add: zmod_bit_simps AND_ac OR_ac XOR_def bits.Rep_mod)
apply (simp add: AND_OR_distrib)
apply (simp add: OR_AND_distrib)
done

end