Quot/Examples/IntEx2.thy
changeset 675 94d6d29459c9
parent 674 bb276771d85c
child 676 0668d218bfa5
child 677 35fbace8d48d
equal deleted inserted replaced
674:bb276771d85c 675:94d6d29459c9
   178 
   178 
   179 instance int :: comm_ring_1
   179 instance int :: comm_ring_1
   180 proof
   180 proof
   181   fix i j k :: int
   181   fix i j k :: int
   182   show "(i + j) + k = i + (j + k)"
   182   show "(i + j) + k = i + (j + k)"
   183      by (lifting plus_assoc_raw)
   183     by (lifting plus_assoc_raw)
   184   show "i + j = j + i" 
   184   show "i + j = j + i" 
   185     by (lifting plus_sym_raw)
   185     by (lifting plus_sym_raw)
   186   show "0 + i = (i::int)"
   186   show "0 + i = (i::int)"
   187     by (lifting plus_zero_raw)
   187     by (lifting plus_zero_raw)
   188   show "- i + i = 0"
   188   show "- i + i = 0"
   199     by (lifting times_plus_comm_raw)
   199     by (lifting times_plus_comm_raw)
   200   show "0 \<noteq> (1::int)"
   200   show "0 \<noteq> (1::int)"
   201     by (lifting one_zero_distinct)
   201     by (lifting one_zero_distinct)
   202 qed
   202 qed
   203 
   203 
   204 
   204 lemma plus_raw_rsp_aux:
   205 lemma plus_raw_rsp_lo:
   205   assumes a: "a \<approx> b" "c \<approx> d"
   206   "\<And>a b c d. a \<approx> b \<Longrightarrow> c \<approx> d \<Longrightarrow> plus_raw a c \<approx> plus_raw b d"
   206   shows "plus_raw a c \<approx> plus_raw b d"
   207 by auto
   207 using a
       
   208 by (cases a, cases b, cases c, cases d) 
       
   209    (simp)
   208 
   210 
   209 lemma add:
   211 lemma add:
   210      "(ABS_int (x,y)) + (ABS_int (u,v)) =
   212      "(ABS_int (x,y)) + (ABS_int (u,v)) =
   211       (ABS_int (x+u, y+v))"
   213       (ABS_int (x + u, y + v))"
   212 apply(simp add: plus_int_def)
   214 apply(simp add: plus_int_def)
   213 apply(fold plus_raw.simps)
   215 apply(fold plus_raw.simps)
   214 apply(rule Quotient_rel_abs[OF Quotient_int])
   216 apply(rule Quotient_rel_abs[OF Quotient_int])
   215 apply(rule plus_raw_rsp_lo)
   217 apply(rule plus_raw_rsp_aux)
   216 apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
   218 apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
   217 done
   219 done
   218 
   220 
   219 lemma int_def: "of_nat m = ABS_int (m, 0)"
   221 lemma int_def: 
   220 apply(induct m)
   222   shows "of_nat m = ABS_int (m, 0)"
   221 apply(simp add: zero_int_def)
   223 by (induct m) (simp_all add: zero_int_def one_int_def add)
   222 apply(simp add: one_int_def add)
       
   223 done
       
   224 
   224 
   225 lemma le_antisym_raw:
   225 lemma le_antisym_raw:
   226   shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j"
   226   shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j"
   227 by (cases i, cases j) (simp)
   227 by (cases i, cases j) (simp)
   228 
   228 
   282 qed
   282 qed
   283 
   283 
   284 abbreviation
   284 abbreviation
   285   "less_raw i j \<equiv> less_eq_raw i j \<and> \<not>(i \<approx> j)"
   285   "less_raw i j \<equiv> less_eq_raw i j \<and> \<not>(i \<approx> j)"
   286 
   286 
   287 
   287 lemma zmult_zless_mono2_lemma:
   288 lemma test:
   288   fixes i j::int
   289   "\<lbrakk>less_raw i j; less_raw (0, 0) k\<rbrakk>
   289   and   k::nat
   290     \<Longrightarrow> less_raw (times_raw k i) (times_raw k j)"
   290   shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
   291 apply(cases i, cases j, cases k)
   291 apply(induct "k")
   292 apply(simp only: less_eq_raw.simps times_raw.simps)
       
   293 apply(simp)
   292 apply(simp)
   294 apply(rename_tac u v w x y z)
   293 apply(case_tac "k = 0")
   295 apply(rule conjI)
   294 apply(simp_all add: left_distrib add_strict_mono)
   296 apply(subgoal_tac "y*u + y*x \<le> y*w + y*v  &  z*v \<le> y*v")
   295 done
   297 apply(simp add: )
   296 
       
   297 lemma zero_le_imp_eq_int: 
       
   298   fixes k::int
       
   299   shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
   298 sorry
   300 sorry
   299 
   301 
       
   302 lemma zmult_zless_mono2: 
       
   303   fixes i j k::int
       
   304   assumes a: "i < j" "0 < k"
       
   305   shows "k * i < k * j"
       
   306 using a
       
   307 apply(drule_tac zero_le_imp_eq_int)
       
   308 apply(auto simp add: zmult_zless_mono2_lemma)
       
   309 done
   300 
   310 
   301 text{*The integers form an ordered integral domain*}
   311 text{*The integers form an ordered integral domain*}
   302 instance int :: ordered_idom
   312 instance int :: ordered_idom
   303 proof
   313 proof
   304   fix i j k :: int
   314   fix i j k :: int
   305   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
   315   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
   306     unfolding less_int_def by (lifting test)
   316     by (rule zmult_zless_mono2)
   307   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
   317   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
   308     by (simp only: abs_int_def)
   318     by (simp only: abs_int_def)
   309   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
   319   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
   310     by (simp only: sgn_int_def)
   320     by (simp only: sgn_int_def)
   311 qed
   321 qed