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
```     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`