src/HOL/Integ/IntArith.thy
author nipkow
Tue Oct 29 11:32:52 2002 +0100 (2002-10-29)
changeset 13685 0b8fbcf65d73
parent 13575 ecb6ecd9af13
child 13837 8dd150d36c65
permissions -rw-r--r--
added induction thms
wenzelm@12023
     1
wenzelm@12023
     2
header {* Integer arithmetic *}
wenzelm@12023
     3
wenzelm@9436
     4
theory IntArith = Bin
wenzelm@9436
     5
files ("int_arith1.ML") ("int_arith2.ML"):
wenzelm@9436
     6
wenzelm@12023
     7
use "int_arith1.ML"
wenzelm@12023
     8
setup int_arith_setup
wenzelm@12023
     9
use "int_arith2.ML"
wenzelm@12023
    10
declare zabs_split [arith_split]
wenzelm@12023
    11
nipkow@13575
    12
lemma split_nat[arith_split]:
nipkow@13575
    13
  "P(nat(i::int)) = ((ALL n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
nipkow@13575
    14
  (is "?P = (?L & ?R)")
nipkow@13575
    15
proof (cases "i < 0")
nipkow@13575
    16
  case True thus ?thesis by simp
nipkow@13575
    17
next
nipkow@13575
    18
  case False
nipkow@13575
    19
  have "?P = ?L"
nipkow@13575
    20
  proof
nipkow@13575
    21
    assume ?P thus ?L using False by clarsimp
nipkow@13575
    22
  next
nipkow@13575
    23
    assume ?L thus ?P using False by simp
nipkow@13575
    24
  qed
nipkow@13575
    25
  with False show ?thesis by simp
nipkow@13575
    26
qed
nipkow@13575
    27
nipkow@13685
    28
subsubsection "Induction principles for int"
nipkow@13685
    29
nipkow@13685
    30
                     (* `set:int': dummy construction *)
nipkow@13685
    31
theorem int_ge_induct[case_names base step,induct set:int]:
nipkow@13685
    32
  assumes ge: "k \<le> (i::int)" and
nipkow@13685
    33
        base: "P(k)" and
nipkow@13685
    34
        step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
nipkow@13685
    35
  shows "P i"
nipkow@13685
    36
proof -
nipkow@13685
    37
  { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k <= i \<Longrightarrow> P i"
nipkow@13685
    38
    proof (induct n)
nipkow@13685
    39
      case 0
nipkow@13685
    40
      hence "i = k" by arith
nipkow@13685
    41
      thus "P i" using base by simp
nipkow@13685
    42
    next
nipkow@13685
    43
      case (Suc n)
nipkow@13685
    44
      hence "n = nat((i - 1) - k)" by arith
nipkow@13685
    45
      moreover
nipkow@13685
    46
      have ki1: "k \<le> i - 1" using Suc.prems by arith
nipkow@13685
    47
      ultimately
nipkow@13685
    48
      have "P(i - 1)" by(rule Suc.hyps)
nipkow@13685
    49
      from step[OF ki1 this] show ?case by simp
nipkow@13685
    50
    qed
nipkow@13685
    51
  }
nipkow@13685
    52
  from this ge show ?thesis by fast
nipkow@13685
    53
qed
nipkow@13685
    54
nipkow@13685
    55
                     (* `set:int': dummy construction *)
nipkow@13685
    56
theorem int_gr_induct[case_names base step,induct set:int]:
nipkow@13685
    57
  assumes gr: "k < (i::int)" and
nipkow@13685
    58
        base: "P(k+1)" and
nipkow@13685
    59
        step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
nipkow@13685
    60
  shows "P i"
nipkow@13685
    61
apply(rule int_ge_induct[of "k + 1"])
nipkow@13685
    62
  using gr apply arith
nipkow@13685
    63
 apply(rule base)
nipkow@13685
    64
apply(rule step)
nipkow@13685
    65
 apply simp+
nipkow@13685
    66
done
nipkow@13685
    67
nipkow@13685
    68
theorem int_le_induct[consumes 1,case_names base step]:
nipkow@13685
    69
  assumes le: "i \<le> (k::int)" and
nipkow@13685
    70
        base: "P(k)" and
nipkow@13685
    71
        step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
nipkow@13685
    72
  shows "P i"
nipkow@13685
    73
proof -
nipkow@13685
    74
  { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i <= k \<Longrightarrow> P i"
nipkow@13685
    75
    proof (induct n)
nipkow@13685
    76
      case 0
nipkow@13685
    77
      hence "i = k" by arith
nipkow@13685
    78
      thus "P i" using base by simp
nipkow@13685
    79
    next
nipkow@13685
    80
      case (Suc n)
nipkow@13685
    81
      hence "n = nat(k - (i+1))" by arith
nipkow@13685
    82
      moreover
nipkow@13685
    83
      have ki1: "i + 1 \<le> k" using Suc.prems by arith
nipkow@13685
    84
      ultimately
nipkow@13685
    85
      have "P(i+1)" by(rule Suc.hyps)
nipkow@13685
    86
      from step[OF ki1 this] show ?case by simp
nipkow@13685
    87
    qed
nipkow@13685
    88
  }
nipkow@13685
    89
  from this le show ?thesis by fast
nipkow@13685
    90
qed
nipkow@13685
    91
nipkow@13685
    92
theorem int_less_induct[consumes 1,case_names base step]:
nipkow@13685
    93
  assumes less: "(i::int) < k" and
nipkow@13685
    94
        base: "P(k - 1)" and
nipkow@13685
    95
        step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
nipkow@13685
    96
  shows "P i"
nipkow@13685
    97
apply(rule int_le_induct[of _ "k - 1"])
nipkow@13685
    98
  using less apply arith
nipkow@13685
    99
 apply(rule base)
nipkow@13685
   100
apply(rule step)
nipkow@13685
   101
 apply simp+
nipkow@13685
   102
done
nipkow@13685
   103
wenzelm@7707
   104
end