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