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;
haftmann@32556
     1
wenzelm@61343
     2
section \<open>Various examples for transfer procedure\<close>
haftmann@32556
     3
haftmann@32556
     4
theory Transfer_Ex
huffman@52360
     5
imports Main Transfer_Int_Nat
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
wenzelm@61076
    11
lemma "0 \<le> (y::int) \<Longrightarrow> 0 \<le> (x::int) \<Longrightarrow> x + y = y + x"
haftmann@35685
    12
  by (fact ex1 [transferred])
haftmann@32556
    13
huffman@52360
    14
(* Using new transfer package *)
wenzelm@61076
    15
lemma "0 \<le> (x::int) \<Longrightarrow> 0 \<le> (y::int) \<Longrightarrow> x + y = y + x"
huffman@52360
    16
  by (fact ex1 [untransferred])
huffman@52360
    17
haftmann@32556
    18
lemma ex2: "(a::nat) div b * b + a mod b = a"
haftmann@32556
    19
  by (rule mod_div_equality)
haftmann@32556
    20
wenzelm@61076
    21
lemma "0 \<le> (b::int) \<Longrightarrow> 0 \<le> (a::int) \<Longrightarrow> a div b * b + a mod b = a"
haftmann@35685
    22
  by (fact ex2 [transferred])
haftmann@32556
    23
huffman@52360
    24
(* Using new transfer package *)
wenzelm@61076
    25
lemma "0 \<le> (a::int) \<Longrightarrow> 0 \<le> (b::int) \<Longrightarrow> a div b * b + a mod b = a"
huffman@52360
    26
  by (fact ex2 [untransferred])
huffman@52360
    27
haftmann@32556
    28
lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
haftmann@32556
    29
  by auto
haftmann@32556
    30
wenzelm@61076
    31
lemma "\<forall>x\<ge>0::int. \<forall>y\<ge>0. \<exists>z\<ge>0. x + y \<le> z"
haftmann@35685
    32
  by (fact ex3 [transferred nat_int])
haftmann@32556
    33
huffman@52360
    34
(* Using new transfer package *)
wenzelm@61076
    35
lemma "\<forall>x::int\<in>{0..}. \<forall>y\<in>{0..}. \<exists>z\<in>{0..}. x + y \<le> z"
huffman@52360
    36
  by (fact ex3 [untransferred])
huffman@52360
    37
haftmann@32556
    38
lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
haftmann@32556
    39
  by auto
haftmann@32556
    40
wenzelm@61076
    41
lemma "0 \<le> (x::int) \<Longrightarrow> 0 \<le> (y::int) \<Longrightarrow> y \<le> x \<Longrightarrow> tsub x y + y = x"
haftmann@35685
    42
  by (fact ex4 [transferred])
haftmann@32556
    43
huffman@52360
    44
(* Using new transfer package *)
wenzelm@61076
    45
lemma "0 \<le> (y::int) \<Longrightarrow> 0 \<le> (x::int) \<Longrightarrow> y \<le> x \<Longrightarrow> tsub x y + y = x"
huffman@52360
    46
  by (fact ex4 [untransferred])
huffman@52360
    47
haftmann@35685
    48
lemma ex5: "(2::nat) * \<Sum>{..n} = n * (n + 1)"
haftmann@32556
    49
  by (induct n rule: nat_induct, auto)
haftmann@32556
    50
wenzelm@61076
    51
lemma "0 \<le> (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
haftmann@35685
    52
  by (fact ex5 [transferred])
haftmann@35685
    53
huffman@52360
    54
(* Using new transfer package *)
wenzelm@61076
    55
lemma "0 \<le> (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
huffman@52360
    56
  by (fact ex5 [untransferred])
huffman@52360
    57
wenzelm@61076
    58
lemma "0 \<le> (n::nat) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
haftmann@35685
    59
  by (fact ex5 [transferred, transferred])
haftmann@32556
    60
huffman@52360
    61
(* Using new transfer package *)
wenzelm@61076
    62
lemma "0 \<le> (n::nat) \<Longrightarrow> 2 * \<Sum>{..n} = n * (n + 1)"
huffman@52360
    63
  by (fact ex5 [untransferred, Transfer.transferred])
huffman@52360
    64
huffman@52360
    65
end