more lemmas
authorhaftmann
Mon Oct 03 14:34:32 2016 +0200 (2016-10-03)
changeset 64014ca1239a3277b
parent 64013 048b7dbfdfa3
child 64015 c9f3a94cb825
more lemmas
src/HOL/Divides.thy
src/HOL/Int.thy
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/Divides.thy	Mon Oct 03 14:34:31 2016 +0200
     1.2 +++ b/src/HOL/Divides.thy	Mon Oct 03 14:34:32 2016 +0200
     1.3 @@ -542,6 +542,10 @@
     1.4    "even a \<longleftrightarrow> a mod 2 = 0"
     1.5    by (fact dvd_eq_mod_eq_0)
     1.6  
     1.7 +lemma odd_iff_mod_2_eq_one:
     1.8 +  "odd a \<longleftrightarrow> a mod 2 = 1"
     1.9 +  by (auto simp add: even_iff_mod_2_eq_zero)
    1.10 +
    1.11  lemma even_succ_div_two [simp]:
    1.12    "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
    1.13    by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
     2.1 --- a/src/HOL/Int.thy	Mon Oct 03 14:34:31 2016 +0200
     2.2 +++ b/src/HOL/Int.thy	Mon Oct 03 14:34:32 2016 +0200
     2.3 @@ -983,6 +983,20 @@
     2.4  
     2.5  end
     2.6  
     2.7 +lemma transfer_rule_of_int:
     2.8 +  fixes R :: "'a::ring_1 \<Rightarrow> 'b::ring_1 \<Rightarrow> bool"
     2.9 +  assumes [transfer_rule]: "R 0 0" "R 1 1"
    2.10 +    "rel_fun R (rel_fun R R) plus plus"
    2.11 +    "rel_fun R R uminus uminus"
    2.12 +  shows "rel_fun HOL.eq R of_int of_int"
    2.13 +proof -
    2.14 +  note transfer_rule_of_nat [transfer_rule]
    2.15 +  have [transfer_rule]: "rel_fun HOL.eq R of_nat of_nat"
    2.16 +    by transfer_prover
    2.17 +  show ?thesis
    2.18 +    by (unfold of_int_of_nat [abs_def]) transfer_prover
    2.19 +qed
    2.20 +
    2.21  lemma nat_mult_distrib:
    2.22    fixes z z' :: int
    2.23    assumes "0 \<le> z"
     3.1 --- a/src/HOL/Transfer.thy	Mon Oct 03 14:34:31 2016 +0200
     3.2 +++ b/src/HOL/Transfer.thy	Mon Oct 03 14:34:32 2016 +0200
     3.3 @@ -602,4 +602,14 @@
     3.4  
     3.5  end
     3.6  
     3.7 +
     3.8 +subsection \<open>@{const of_nat}\<close>
     3.9 +
    3.10 +lemma transfer_rule_of_nat:
    3.11 +  fixes R :: "'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool"
    3.12 +  assumes [transfer_rule]: "R 0 0" "R 1 1"
    3.13 +    "rel_fun R (rel_fun R R) plus plus"
    3.14 +  shows "rel_fun HOL.eq R of_nat of_nat"
    3.15 +  by (unfold of_nat_def [abs_def]) transfer_prover
    3.16 +
    3.17  end