src/HOL/ex/Transfer_Ex.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 52360 ac7ac2b242a2
child 61076 bdc1e2f0a86a
permissions -rw-r--r--
modernized header uniformly as section;
     1 
     2 section {* Various examples for transfer procedure *}
     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\<Colon>int) \<Longrightarrow> 0 \<le> (x\<Colon>int) \<Longrightarrow> x + y = y + x"
    12   by (fact ex1 [transferred])
    13 
    14 (* Using new transfer package *)
    15 lemma "0 \<le> (x\<Colon>int) \<Longrightarrow> 0 \<le> (y\<Colon>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\<Colon>int) \<Longrightarrow> 0 \<le> (a\<Colon>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\<Colon>int) \<Longrightarrow> 0 \<le> (b\<Colon>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\<Colon>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\<Colon>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\<Colon>int) \<Longrightarrow> 0 \<le> (y\<Colon>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\<Colon>int) \<Longrightarrow> 0 \<le> (x\<Colon>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\<Colon>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\<Colon>int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
    56   by (fact ex5 [untransferred])
    57 
    58 lemma "0 \<le> (n\<Colon>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\<Colon>nat) \<Longrightarrow> 2 * \<Sum>{..n} = n * (n + 1)"
    63   by (fact ex5 [untransferred, Transfer.transferred])
    64 
    65 end