src/HOL/Quotient_Examples/Quotient_Int.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47308 9caab698dbe4
child 49962 a8cc904a6820
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     1
(*  Title:      HOL/Quotient_Examples/Quotient_Int.thy
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     2
    Author:     Cezary Kaliszyk
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     3
    Author:     Christian Urban
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     4
41467
8fc17c5e11c0 tuned headers;
wenzelm
parents: 41413
diff changeset
     5
Integers based on Quotients, based on an older version by Larry
8fc17c5e11c0 tuned headers;
wenzelm
parents: 41413
diff changeset
     6
Paulson.
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     7
*)
41467
8fc17c5e11c0 tuned headers;
wenzelm
parents: 41413
diff changeset
     8
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     9
theory Quotient_Int
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 40928
diff changeset
    10
imports "~~/src/HOL/Library/Quotient_Product" Nat
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    11
begin
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    12
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    13
fun
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    14
  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    15
where
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    16
  "intrel (x, y) (u, v) = (x + v = u + y)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    17
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    18
quotient_type int = "nat \<times> nat" / intrel
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
    19
  by (auto simp add: equivp_def fun_eq_iff)
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    20
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    21
instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    22
begin
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    23
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    24
quotient_definition
47092
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    25
  "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)" done
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    26
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    27
quotient_definition
47092
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    28
  "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)" done
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    29
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    30
fun
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    31
  plus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    32
where
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    33
  "plus_int_raw (x, y) (u, v) = (x + u, y + v)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    34
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    35
quotient_definition
47092
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    36
  "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw" by auto
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    37
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    38
fun
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    39
  uminus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    40
where
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    41
  "uminus_int_raw (x, y) = (y, x)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    42
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    43
quotient_definition
47092
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    44
  "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw" by auto
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    45
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    46
definition
37767
a2b7a20d6ea3 dropped superfluous [code del]s
haftmann
parents: 37594
diff changeset
    47
  minus_int_def:  "z - w = z + (-w\<Colon>int)"
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    48
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    49
fun
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    50
  times_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    51
where
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    52
  "times_int_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    53
47092
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    54
lemma times_int_raw_fst:
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    55
  assumes a: "x \<approx> z"
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    56
  shows "times_int_raw x y \<approx> times_int_raw z y"
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    57
  using a
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    58
  apply(cases x, cases y, cases z)
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    59
  apply(auto simp add: times_int_raw.simps intrel.simps)
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    60
  apply(rename_tac u v w x y z)
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    61
  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    62
  apply(simp add: mult_ac)
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    63
  apply(simp add: add_mult_distrib [symmetric])
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    64
done
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    65
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    66
lemma times_int_raw_snd:
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    67
  assumes a: "x \<approx> z"
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    68
  shows "times_int_raw y x \<approx> times_int_raw y z"
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    69
  using a
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    70
  apply(cases x, cases y, cases z)
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    71
  apply(auto simp add: times_int_raw.simps intrel.simps)
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    72
  apply(rename_tac u v w x y z)
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    73
  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    74
  apply(simp add: mult_ac)
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    75
  apply(simp add: add_mult_distrib [symmetric])
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    76
done
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    77
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    78
quotient_definition
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    79
  "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
47092
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    80
  apply(rule equivp_transp[OF int_equivp])
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    81
  apply(rule times_int_raw_fst)
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    82
  apply(assumption)
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    83
  apply(rule times_int_raw_snd)
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    84
  apply(assumption)
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    85
done
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    86
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    87
fun
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    88
  le_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    89
where
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    90
  "le_int_raw (x, y) (u, v) = (x+v \<le> u+y)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    91
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    92
quotient_definition
47092
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
    93
  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw" by auto
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    94
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    95
definition
37767
a2b7a20d6ea3 dropped superfluous [code del]s
haftmann
parents: 37594
diff changeset
    96
  less_int_def: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    97
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    98
definition
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    99
  zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   100
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   101
definition
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   102
  zsgn_def: "sgn (i\<Colon>int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   103
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   104
instance ..
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   105
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   106
end
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   107
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   108
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   109
text{* The integers form a @{text comm_ring_1}*}
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   110
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   111
instance int :: comm_ring_1
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   112
proof
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   113
  fix i j k :: int
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   114
  show "(i + j) + k = i + (j + k)"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   115
    by (descending) (auto)
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   116
  show "i + j = j + i"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   117
    by (descending) (auto)
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   118
  show "0 + i = (i::int)"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   119
    by (descending) (auto)
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   120
  show "- i + i = 0"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   121
    by (descending) (auto)
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   122
  show "i - j = i + - j"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   123
    by (simp add: minus_int_def)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   124
  show "(i * j) * k = i * (j * k)"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   125
    by (descending) (auto simp add: algebra_simps)
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   126
  show "i * j = j * i"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   127
    by (descending) (auto)
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   128
  show "1 * i = i"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   129
    by (descending) (auto)
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   130
  show "(i + j) * k = i * k + j * k"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   131
    by (descending) (auto simp add: algebra_simps)
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   132
  show "0 \<noteq> (1::int)"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   133
    by (descending) (auto)
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   134
qed
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   135
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   136
lemma plus_int_raw_rsp_aux:
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   137
  assumes a: "a \<approx> b" "c \<approx> d"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   138
  shows "plus_int_raw a c \<approx> plus_int_raw b d"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   139
  using a
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   140
  by (cases a, cases b, cases c, cases d)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   141
     (simp)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   142
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   143
lemma add_abs_int:
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   144
  "(abs_int (x,y)) + (abs_int (u,v)) =
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   145
   (abs_int (x + u, y + v))"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   146
  apply(simp add: plus_int_def id_simps)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   147
  apply(fold plus_int_raw.simps)
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47304
diff changeset
   148
  apply(rule Quotient3_rel_abs[OF Quotient3_int])
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   149
  apply(rule plus_int_raw_rsp_aux)
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47304
diff changeset
   150
  apply(simp_all add: rep_abs_rsp_left[OF Quotient3_int])
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   151
  done
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   152
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   153
definition int_of_nat_raw:
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   154
  "int_of_nat_raw m = (m :: nat, 0 :: nat)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   155
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   156
quotient_definition
47092
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45605
diff changeset
   157
  "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw" done
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   158
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   159
lemma int_of_nat:
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   160
  shows "of_nat m = int_of_nat m"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   161
  by (induct m)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   162
     (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add_abs_int)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   163
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   164
instance int :: linorder
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   165
proof
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   166
  fix i j k :: int
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   167
  show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   168
    by (descending) (auto)
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   169
  show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   170
    by (auto simp add: less_int_def dest: antisym)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   171
  show "i \<le> i"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   172
    by (descending) (auto)
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   173
  show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   174
    by (descending) (auto)
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   175
  show "i \<le> j \<or> j \<le> i"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   176
    by (descending) (auto)
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   177
qed
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   178
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   179
instantiation int :: distrib_lattice
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   180
begin
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   181
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   182
definition
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   183
  "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   184
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   185
definition
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   186
  "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   187
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   188
instance
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   189
  by default
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   190
     (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   191
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   192
end
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   193
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   194
instance int :: ordered_cancel_ab_semigroup_add
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   195
proof
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   196
  fix i j k :: int
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   197
  show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   198
    by (descending) (auto)
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   199
qed
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   200
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   201
abbreviation
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   202
  "less_int_raw i j \<equiv> le_int_raw i j \<and> \<not>(i \<approx> j)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   203
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   204
lemma zmult_zless_mono2_lemma:
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   205
  fixes i j::int
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   206
  and   k::nat
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   207
  shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   208
  apply(induct "k")
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   209
  apply(simp)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   210
  apply(case_tac "k = 0")
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   211
  apply(simp_all add: left_distrib add_strict_mono)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   212
  done
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   213
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   214
lemma zero_le_imp_eq_int_raw:
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   215
  fixes k::"(nat \<times> nat)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   216
  shows "less_int_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   217
  apply(cases k)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   218
  apply(simp add:int_of_nat_raw)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   219
  apply(auto)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   220
  apply(rule_tac i="b" and j="a" in less_Suc_induct)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   221
  apply(auto)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   222
  done
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   223
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   224
lemma zero_le_imp_eq_int:
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   225
  fixes k::int
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   226
  shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   227
  unfolding less_int_def int_of_nat
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   228
  by (descending) (rule zero_le_imp_eq_int_raw)
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   229
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   230
lemma zmult_zless_mono2:
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   231
  fixes i j k::int
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   232
  assumes a: "i < j" "0 < k"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   233
  shows "k * i < k * j"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   234
  using a
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   235
  by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   236
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   237
text{*The integers form an ordered integral domain*}
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   238
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   239
instance int :: linordered_idom
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   240
proof
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   241
  fix i j k :: int
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   242
  show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   243
    by (rule zmult_zless_mono2)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   244
  show "\<bar>i\<bar> = (if i < 0 then -i else i)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   245
    by (simp only: zabs_def)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   246
  show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   247
    by (simp only: zsgn_def)
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   248
qed
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   249
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   250
lemmas int_distrib =
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 41467
diff changeset
   251
  left_distrib [of z1 z2 w]
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 41467
diff changeset
   252
  right_distrib [of w z1 z2]
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 41467
diff changeset
   253
  left_diff_distrib [of z1 z2 w]
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 41467
diff changeset
   254
  right_diff_distrib [of w z1 z2]
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 41467
diff changeset
   255
  minus_add_distrib[of z1 z2]
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 41467
diff changeset
   256
  for z1 z2 w :: int
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   257
47304
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   258
lemma int_induct2:
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   259
  assumes "P 0 0"
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   260
  and     "\<And>n m. P n m \<Longrightarrow> P (Suc n) m"
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   261
  and     "\<And>n m. P n m \<Longrightarrow> P n (Suc m)"
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   262
  shows   "P n m"
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   263
using assms
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   264
by (induction_schema) (pat_completeness, lexicographic_order)
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   265
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   266
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   267
lemma int_induct:
47304
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   268
  fixes j :: int
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   269
  assumes a: "P 0"
47304
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   270
  and     b: "\<And>i::int. P i \<Longrightarrow> P (i + 1)"
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   271
  and     c: "\<And>i::int. P i \<Longrightarrow> P (i - 1)"
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   272
  shows      "P j"
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   273
using a b c 
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   274
unfolding minus_int_def
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   275
by (descending) (auto intro: int_induct2)
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   276
  
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   277
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   278
text {* Magnitide of an Integer, as a Natural Number: @{term nat} *}
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   279
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   280
definition
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   281
  "int_to_nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   282
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   283
quotient_definition
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   284
  "int_to_nat::int \<Rightarrow> nat"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   285
is
47304
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   286
  "int_to_nat_raw" 
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   287
unfolding int_to_nat_raw_def by auto 
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   288
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   289
lemma nat_le_eq_zle:
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   290
  fixes w z::"int"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   291
  shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (int_to_nat w \<le> int_to_nat z) = (w \<le> z)"
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   292
  unfolding less_int_def
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   293
  by (descending) (auto simp add: int_to_nat_raw_def)
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   294
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   295
end