Theory Transfer_Ex

theory Transfer_Ex
imports Transfer_Int_Nat
header {* Various examples for transfer procedure *}

theory Transfer_Ex
imports Main Transfer_Int_Nat
begin

lemma ex1: "(x::nat) + y = y + x"
  by auto

lemma "0 ≤ (y::int) ==> 0 ≤ (x::int) ==> x + y = y + x"
  by (fact ex1 [transferred])

(* Using new transfer package *)
lemma "0 ≤ (x::int) ==> 0 ≤ (y::int) ==> x + y = y + x"
  by (fact ex1 [untransferred])

lemma ex2: "(a::nat) div b * b + a mod b = a"
  by (rule mod_div_equality)

lemma "0 ≤ (b::int) ==> 0 ≤ (a::int) ==> a div b * b + a mod b = a"
  by (fact ex2 [transferred])

(* Using new transfer package *)
lemma "0 ≤ (a::int) ==> 0 ≤ (b::int) ==> a div b * b + a mod b = a"
  by (fact ex2 [untransferred])

lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
  by auto

lemma "∀x≥0::int. ∀y≥0. ∃z≥0. x + y ≤ z"
  by (fact ex3 [transferred nat_int])

(* Using new transfer package *)
lemma "∀x::int∈{0..}. ∀y∈{0..}. ∃z∈{0..}. x + y ≤ z"
  by (fact ex3 [untransferred])

lemma ex4: "(x::nat) >= y ==> (x - y) + y = x"
  by auto

lemma "0 ≤ (x::int) ==> 0 ≤ (y::int) ==> y ≤ x ==> tsub x y + y = x"
  by (fact ex4 [transferred])

(* Using new transfer package *)
lemma "0 ≤ (y::int) ==> 0 ≤ (x::int) ==> y ≤ x ==> tsub x y + y = x"
  by (fact ex4 [untransferred])

lemma ex5: "(2::nat) * ∑{..n} = n * (n + 1)"
  by (induct n rule: nat_induct, auto)

lemma "0 ≤ (n::int) ==> 2 * ∑{0..n} = n * (n + 1)"
  by (fact ex5 [transferred])

(* Using new transfer package *)
lemma "0 ≤ (n::int) ==> 2 * ∑{0..n} = n * (n + 1)"
  by (fact ex5 [untransferred])

lemma "0 ≤ (n::nat) ==> 2 * ∑{0..n} = n * (n + 1)"
  by (fact ex5 [transferred, transferred])

(* Using new transfer package *)
lemma "0 ≤ (n::nat) ==> 2 * ∑{..n} = n * (n + 1)"
  by (fact ex5 [untransferred, Transfer.transferred])

end