more instances
authorhaftmann
Tue Feb 11 19:03:57 2020 +0100 (2 weeks ago ago)
changeset 71654d45495e897f4
parent 71653 4e66867fd63f
child 71655 ff6394cfc05c
more instances
src/HOL/ex/Bit_Operations.thy
     1.1 --- a/src/HOL/ex/Bit_Operations.thy	Tue Feb 11 19:03:56 2020 +0100
     1.2 +++ b/src/HOL/ex/Bit_Operations.thy	Tue Feb 11 19:03:57 2020 +0100
     1.3 @@ -530,4 +530,84 @@
     1.4  
     1.5  end
     1.6  
     1.7 +
     1.8 +subsubsection \<open>Instances for \<^typ>\<open>integer\<close> and \<^typ>\<open>natural\<close>\<close>
     1.9 +
    1.10 +unbundle integer.lifting natural.lifting
    1.11 +
    1.12 +context
    1.13 +  includes lifting_syntax
    1.14 +begin
    1.15 +
    1.16 +lemma transfer_rule_bit_integer [transfer_rule]:
    1.17 +  \<open>((pcr_integer :: int \<Rightarrow> integer \<Rightarrow> bool) ===> (=)) bit bit\<close>
    1.18 +  by (unfold bit_def) transfer_prover
    1.19 +
    1.20 +lemma transfer_rule_bit_natural [transfer_rule]:
    1.21 +  \<open>((pcr_natural :: nat \<Rightarrow> natural \<Rightarrow> bool) ===> (=)) bit bit\<close>
    1.22 +  by (unfold bit_def) transfer_prover
    1.23 +
    1.24  end
    1.25 +
    1.26 +instantiation integer :: ring_bit_operations
    1.27 +begin
    1.28 +
    1.29 +lift_definition not_integer :: \<open>integer \<Rightarrow> integer\<close>
    1.30 +  is not .
    1.31 +
    1.32 +lift_definition and_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
    1.33 +  is \<open>and\<close> .
    1.34 +
    1.35 +lift_definition or_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
    1.36 +  is or .
    1.37 +
    1.38 +lift_definition xor_integer ::  \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
    1.39 +  is xor .
    1.40 +
    1.41 +instance proof
    1.42 +  fix k l :: \<open>integer\<close> and n :: nat
    1.43 +  show \<open>- k = NOT (k - 1)\<close>
    1.44 +    by transfer (simp add: minus_eq_not_minus_1)
    1.45 +  show \<open>bit (NOT k) n \<longleftrightarrow> (2 :: integer) ^ n \<noteq> 0 \<and> \<not> bit k n\<close>
    1.46 +    by transfer (fact bit_not_iff)
    1.47 +  show \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close>
    1.48 +    by transfer (fact and_int.bit_eq_iff)
    1.49 +  show \<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close>
    1.50 +    by transfer (fact or_int.bit_eq_iff)
    1.51 +  show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close>
    1.52 +    by transfer (fact xor_int.bit_eq_iff)
    1.53 +qed
    1.54 +
    1.55 +end
    1.56 +
    1.57 +instantiation natural :: semiring_bit_operations
    1.58 +begin
    1.59 +
    1.60 +lift_definition and_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
    1.61 +  is \<open>and\<close> .
    1.62 +
    1.63 +lift_definition or_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
    1.64 +  is or .
    1.65 +
    1.66 +lift_definition xor_natural ::  \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
    1.67 +  is xor .
    1.68 +
    1.69 +instance proof
    1.70 +  fix m n :: \<open>natural\<close> and q :: nat
    1.71 +  show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
    1.72 +    by transfer (fact and_nat.bit_eq_iff)
    1.73 +  show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
    1.74 +    by transfer (fact or_nat.bit_eq_iff)
    1.75 +  show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
    1.76 +    by transfer (fact xor_nat.bit_eq_iff)
    1.77 +qed
    1.78 +
    1.79 +end
    1.80 +
    1.81 +lifting_update integer.lifting
    1.82 +lifting_forget integer.lifting
    1.83 +
    1.84 +lifting_update natural.lifting
    1.85 +lifting_forget natural.lifting
    1.86 +
    1.87 +end