src/HOL/ex/Transfer_Ex.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 42796 4a8fa4ec0451
child 52360 ac7ac2b242a2
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 
     2 header {* Various examples for transfer procedure *}
     3 
     4 theory Transfer_Ex
     5 imports Main
     6 begin
     7 
     8 lemma ex1: "(x::nat) + y = y + x"
     9   by auto
    10 
    11 lemma "0 \<le> (y\<Colon>int) \<Longrightarrow> 0 \<le> (x\<Colon>int) \<Longrightarrow> x + y = y + x"
    12   by (fact ex1 [transferred])
    13 
    14 lemma ex2: "(a::nat) div b * b + a mod b = a"
    15   by (rule mod_div_equality)
    16 
    17 lemma "0 \<le> (b\<Colon>int) \<Longrightarrow> 0 \<le> (a\<Colon>int) \<Longrightarrow> a div b * b + a mod b = a"
    18   by (fact ex2 [transferred])
    19 
    20 lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
    21   by auto
    22 
    23 lemma "\<forall>x\<ge>0\<Colon>int. \<forall>y\<ge>0. \<exists>z\<ge>0. x + y \<le> z"
    24   by (fact ex3 [transferred nat_int])
    25 
    26 lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
    27   by auto
    28 
    29 lemma "0 \<le> (x\<Colon>int) \<Longrightarrow> 0 \<le> (y\<Colon>int) \<Longrightarrow> y \<le> x \<Longrightarrow> tsub x y + y = x"
    30   by (fact ex4 [transferred])
    31 
    32 lemma ex5: "(2::nat) * \<Sum>{..n} = n * (n + 1)"
    33   by (induct n rule: nat_induct, auto)
    34 
    35 lemma "0 \<le> (n\<Colon>int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
    36   by (fact ex5 [transferred])
    37 
    38 lemma "0 \<le> (n\<Colon>nat) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
    39   by (fact ex5 [transferred, transferred])
    40 
    41 end