src/HOL/ex/Transfer_Ex.thy
 author wenzelm Wed Jun 22 10:09:20 2016 +0200 (2016-06-22) changeset 63343 fb5d8a50c641 parent 61343 5b5656a63bd6 child 64242 93c6f0da5c70 permissions -rw-r--r--
bundle lifting_syntax;
```     1
```
```     2 section \<open>Various examples for transfer procedure\<close>
```
```     3
```
```     4 theory Transfer_Ex
```
```     5 imports Main Transfer_Int_Nat
```
```     6 begin
```
```     7
```
```     8 lemma ex1: "(x::nat) + y = y + x"
```
```     9   by auto
```
```    10
```
```    11 lemma "0 \<le> (y::int) \<Longrightarrow> 0 \<le> (x::int) \<Longrightarrow> x + y = y + x"
```
```    12   by (fact ex1 [transferred])
```
```    13
```
```    14 (* Using new transfer package *)
```
```    15 lemma "0 \<le> (x::int) \<Longrightarrow> 0 \<le> (y::int) \<Longrightarrow> x + y = y + x"
```
```    16   by (fact ex1 [untransferred])
```
```    17
```
```    18 lemma ex2: "(a::nat) div b * b + a mod b = a"
```
```    19   by (rule mod_div_equality)
```
```    20
```
```    21 lemma "0 \<le> (b::int) \<Longrightarrow> 0 \<le> (a::int) \<Longrightarrow> a div b * b + a mod b = a"
```
```    22   by (fact ex2 [transferred])
```
```    23
```
```    24 (* Using new transfer package *)
```
```    25 lemma "0 \<le> (a::int) \<Longrightarrow> 0 \<le> (b::int) \<Longrightarrow> a div b * b + a mod b = a"
```
```    26   by (fact ex2 [untransferred])
```
```    27
```
```    28 lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
```
```    29   by auto
```
```    30
```
```    31 lemma "\<forall>x\<ge>0::int. \<forall>y\<ge>0. \<exists>z\<ge>0. x + y \<le> z"
```
```    32   by (fact ex3 [transferred nat_int])
```
```    33
```
```    34 (* Using new transfer package *)
```
```    35 lemma "\<forall>x::int\<in>{0..}. \<forall>y\<in>{0..}. \<exists>z\<in>{0..}. x + y \<le> z"
```
```    36   by (fact ex3 [untransferred])
```
```    37
```
```    38 lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
```
```    39   by auto
```
```    40
```
```    41 lemma "0 \<le> (x::int) \<Longrightarrow> 0 \<le> (y::int) \<Longrightarrow> y \<le> x \<Longrightarrow> tsub x y + y = x"
```
```    42   by (fact ex4 [transferred])
```
```    43
```
```    44 (* Using new transfer package *)
```
```    45 lemma "0 \<le> (y::int) \<Longrightarrow> 0 \<le> (x::int) \<Longrightarrow> y \<le> x \<Longrightarrow> tsub x y + y = x"
```
```    46   by (fact ex4 [untransferred])
```
```    47
```
```    48 lemma ex5: "(2::nat) * \<Sum>{..n} = n * (n + 1)"
```
```    49   by (induct n rule: nat_induct, auto)
```
```    50
```
```    51 lemma "0 \<le> (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
```
```    52   by (fact ex5 [transferred])
```
```    53
```
```    54 (* Using new transfer package *)
```
```    55 lemma "0 \<le> (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
```
```    56   by (fact ex5 [untransferred])
```
```    57
```
```    58 lemma "0 \<le> (n::nat) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
```
```    59   by (fact ex5 [transferred, transferred])
```
```    60
```
```    61 (* Using new transfer package *)
```
```    62 lemma "0 \<le> (n::nat) \<Longrightarrow> 2 * \<Sum>{..n} = n * (n + 1)"
```
```    63   by (fact ex5 [untransferred, Transfer.transferred])
```
```    64
```
```    65 end
```