src/HOL/ex/Transfer_Ex.thy
author hoelzl
Thu Jan 31 11:31:27 2013 +0100 (2013-01-31)
changeset 50999 3de230ed0547
parent 42796 4a8fa4ec0451
child 52360 ac7ac2b242a2
permissions -rw-r--r--
introduce order topology
haftmann@32556
     1
haftmann@32556
     2
header {* Various examples for transfer procedure *}
haftmann@32556
     3
haftmann@32556
     4
theory Transfer_Ex
haftmann@35685
     5
imports Main
haftmann@32556
     6
begin
haftmann@32556
     7
haftmann@32556
     8
lemma ex1: "(x::nat) + y = y + x"
haftmann@32556
     9
  by auto
haftmann@32556
    10
krauss@42796
    11
lemma "0 \<le> (y\<Colon>int) \<Longrightarrow> 0 \<le> (x\<Colon>int) \<Longrightarrow> x + y = y + x"
haftmann@35685
    12
  by (fact ex1 [transferred])
haftmann@32556
    13
haftmann@32556
    14
lemma ex2: "(a::nat) div b * b + a mod b = a"
haftmann@32556
    15
  by (rule mod_div_equality)
haftmann@32556
    16
krauss@42796
    17
lemma "0 \<le> (b\<Colon>int) \<Longrightarrow> 0 \<le> (a\<Colon>int) \<Longrightarrow> a div b * b + a mod b = a"
haftmann@35685
    18
  by (fact ex2 [transferred])
haftmann@32556
    19
haftmann@32556
    20
lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
haftmann@32556
    21
  by auto
haftmann@32556
    22
krauss@42796
    23
lemma "\<forall>x\<ge>0\<Colon>int. \<forall>y\<ge>0. \<exists>z\<ge>0. x + y \<le> z"
haftmann@35685
    24
  by (fact ex3 [transferred nat_int])
haftmann@32556
    25
haftmann@32556
    26
lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
haftmann@32556
    27
  by auto
haftmann@32556
    28
krauss@42796
    29
lemma "0 \<le> (x\<Colon>int) \<Longrightarrow> 0 \<le> (y\<Colon>int) \<Longrightarrow> y \<le> x \<Longrightarrow> tsub x y + y = x"
haftmann@35685
    30
  by (fact ex4 [transferred])
haftmann@32556
    31
haftmann@35685
    32
lemma ex5: "(2::nat) * \<Sum>{..n} = n * (n + 1)"
haftmann@32556
    33
  by (induct n rule: nat_induct, auto)
haftmann@32556
    34
krauss@42796
    35
lemma "0 \<le> (n\<Colon>int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
haftmann@35685
    36
  by (fact ex5 [transferred])
haftmann@35685
    37
krauss@42796
    38
lemma "0 \<le> (n\<Colon>nat) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
haftmann@35685
    39
  by (fact ex5 [transferred, transferred])
haftmann@32556
    40
haftmann@32556
    41
end