theory IntEx2

imports "../QuotMain" Nat Presburger

(*uses

  ("Tools/numeral.ML")

  ("Tools/numeral_syntax.ML")

  ("Tools/int_arith.ML")*)

begin

fun

  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)

where

  "intrel (x, y) (u, v) = (x + v = u + y)"

quotient int = "nat \<times> nat" / intrel

  unfolding equivp_def

  by (auto simp add: mem_def expand_fun_eq)

instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"

begin

quotient_def

  zero_int::"0 :: int"

where

  "(0::nat, 0::nat)"

quotient_def

  one_int::"1 :: int"

where

  "(1::nat, 0::nat)"

fun

  plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"

where

  "plus_raw (x, y) (u, v) = (x + u, y + v)"

quotient_def

  plus_int::"(op +) :: (int \<Rightarrow> int \<Rightarrow> int)"

where

  "plus_raw"

fun

  uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"

where

  "uminus_raw (x, y) = (y, x)"

quotient_def

  uminus_int::"(uminus :: (int \<Rightarrow> int))"

where

  "uminus_raw"

definition

  minus_int_def [code del]:  "z - w = z + (-w::int)"

fun

  times_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"

where

  "times_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"

quotient_def

  times_int::"(op *) :: (int \<Rightarrow> int \<Rightarrow> int)"

where

  "times_raw"

(* PROBLEM: this should be called le_int and le_raw / or odd *)

fun

  less_eq_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"

where

  "less_eq_raw (x, y) (u, v) = (x+v \<le> u+y)"

quotient_def

  less_eq_int :: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool"

where

  "less_eq_raw"

definition

  less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"

definition

  abs_int_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"

definition

  sgn_int_def: "sgn (i\<Colon>int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"

instance ..

end

lemma plus_raw_rsp[quot_respect]:

  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"

by auto

lemma minus_raw_rsp[quot_respect]:

  shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw"

  by auto

lemma times_raw_fst:

  assumes a: "x \<approx> z"

  shows "times_raw x y \<approx> times_raw z y"

using a

apply(cases x, cases y, cases z)

apply(auto simp add: times_raw.simps intrel.simps)

apply(rename_tac u v w x y z)

apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")

apply(simp add: mult_ac)

apply(simp add: add_mult_distrib [symmetric])

done

lemma times_raw_snd:

  assumes a: "x \<approx> z"

  shows "times_raw y x \<approx> times_raw y z"

using a

apply(cases x, cases y, cases z)

apply(auto simp add: times_raw.simps intrel.simps)

apply(rename_tac u v w x y z)

apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")

apply(simp add: mult_ac)

apply(simp add: add_mult_distrib [symmetric])

done

lemma times_raw_rsp[quot_respect]:

  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_raw times_raw"

apply(simp only: fun_rel.simps)

apply(rule allI | rule impI)+

apply(rule equivp_transp[OF int_equivp])

apply(rule times_raw_fst)

apply(assumption)

apply(rule times_raw_snd)

apply(assumption)

done

lemma less_eq_raw_rsp[quot_respect]:

  shows "(op \<approx> ===> op \<approx> ===> op =) less_eq_raw less_eq_raw"

by auto

lemma plus_assoc_raw:

  shows "plus_raw (plus_raw i j) k \<approx> plus_raw i (plus_raw j k)"

by (cases i, cases j, cases k) (simp)

lemma plus_sym_raw:

  shows "plus_raw i j \<approx> plus_raw j i"

by (cases i, cases j) (simp)

lemma plus_zero_raw:

  shows "plus_raw  (0, 0) i \<approx> i"

by (cases i) (simp)

lemma plus_minus_zero_raw:

  shows "plus_raw (uminus_raw i) i \<approx> (0, 0)"

by (cases i) (simp)

lemma times_assoc_raw:

  shows "times_raw (times_raw i j) k \<approx> times_raw i (times_raw j k)"

by (cases i, cases j, cases k) 

   (simp add: algebra_simps)

lemma times_sym_raw:

  shows "times_raw i j \<approx> times_raw j i"

by (cases i, cases j) (simp add: algebra_simps)

lemma times_one_raw:

  shows "times_raw  (1, 0) i \<approx> i"

by (cases i) (simp)

lemma times_plus_comm_raw:

  shows "times_raw (plus_raw i j) k \<approx> plus_raw (times_raw i k) (times_raw j k)"

by (cases i, cases j, cases k) 

   (simp add: algebra_simps)

lemma one_zero_distinct:

  shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"

  by simp

text{* The integers form a @{text comm_ring_1}*}

ML {* qconsts_lookup @{theory} @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} *}

ML {* dest_Type (snd (dest_Const @{term "0 :: int"})) *}

ML {* @{term "0 :: int"} *}

instance int :: comm_ring_1

proof

  fix i j k :: int

  show "(i + j) + k = i + (j + k)"

    by (lifting plus_assoc_raw)

  show "i + j = j + i" 

    by (lifting plus_sym_raw)

  show "0 + i = (i::int)"

    by (lifting plus_zero_raw)

  show "- i + i = 0"

    by (lifting plus_minus_zero_raw)

  show "i - j = i + - j"

    by (simp add: minus_int_def)

  show "(i * j) * k = i * (j * k)"

    by (lifting times_assoc_raw)

  show "i * j = j * i"

    by (lifting times_sym_raw)

  show "1 * i = i"

    by (lifting times_one_raw)

  show "(i + j) * k = i * k + j * k"

    by (lifting times_plus_comm_raw)

  show "0 \<noteq> (1::int)"

    by (lifting one_zero_distinct)

qed

lemma plus_raw_rsp_aux:

  assumes a: "a \<approx> b" "c \<approx> d"

  shows "plus_raw a c \<approx> plus_raw b d"

using a

by (cases a, cases b, cases c, cases d) 

   (simp)

lemma add:

     "(ABS_int (x,y)) + (ABS_int (u,v)) =

      (ABS_int (x + u, y + v))"

apply(simp add: plus_int_def)

apply(fold plus_raw.simps)

apply(rule Quotient_rel_abs[OF Quotient_int])

apply(rule plus_raw_rsp_aux)

apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])

done

lemma int_def: 

  shows "of_nat m = ABS_int (m, 0)"

by (induct m) (simp_all add: zero_int_def one_int_def add)

lemma le_antisym_raw:

  shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j"

by (cases i, cases j) (simp)

lemma le_refl_raw:

  shows "less_eq_raw i i"

by (cases i) (simp)

lemma le_trans_raw:

  shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j k \<Longrightarrow> less_eq_raw i k"

by (cases i, cases j, cases k) (simp)

lemma le_cases_raw:

  shows "less_eq_raw i j \<or> less_eq_raw j i"

by (cases i, cases j) 

   (simp add: linorder_linear)

instance int :: linorder

proof

  fix i j k :: int

  show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"

    by (lifting le_antisym_raw)

  show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"

    by (auto simp add: less_int_def dest: antisym) 

  show "i \<le> i"

    by (lifting le_refl_raw)

  show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"

    by (lifting le_trans_raw)

  show "i \<le> j \<or> j \<le> i"

    by (lifting le_cases_raw)

qed

instantiation int :: distrib_lattice

begin

definition

  "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"

definition

  "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"

instance

  by intro_classes

    (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)

end

lemma le_plus_raw:

  shows "less_eq_raw i j \<Longrightarrow> less_eq_raw (plus_raw k i) (plus_raw k j)"

by (cases i, cases j, cases k) (simp)

instance int :: pordered_cancel_ab_semigroup_add

proof

  fix i j k :: int

  show "i \<le> j \<Longrightarrow> k + i \<le> k + j"

    by (lifting le_plus_raw)

qed

abbreviation

  "less_raw i j \<equiv> less_eq_raw i j \<and> \<not>(i \<approx> j)"

lemma zmult_zless_mono2_lemma:

  fixes i j::int

  and   k::nat

  shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"

apply(induct "k")

apply(simp)

apply(case_tac "k = 0")

apply(simp_all add: left_distrib add_strict_mono)

done

lemma int_induct_raw:

  assumes a: "P (0::nat, 0)"

  and     b: "\<And>i. P i \<Longrightarrow> P (plus_raw i (1,0))"

  and     c: "\<And>i. P i \<Longrightarrow> P (plus_raw i (minus_raw (1,0)))"

  shows      "P x"

apply(case_tac x) apply(simp)

apply(rule_tac x="b" in spec)

apply(rule_tac Nat.induct)

apply(rule allI)

apply(rule_tac Nat.induct)

using a b c apply(auto)

done

lemma int_induct:

  assumes a: "P (0::int)"

  and     b: "\<And>i. P i \<Longrightarrow> P (i + 1)"

  and     c: "\<And>i. P i \<Longrightarrow> P (i + (- 1))"

  shows      "P x"

using a b c by (lifting int_induct_raw)

lemma zero_le_imp_eq_int: 

  fixes k::int

  shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"

sorry

lemma zmult_zless_mono2: 

  fixes i j k::int

  assumes a: "i < j" "0 < k"

  shows "k * i < k * j"

using a

apply(drule_tac zero_le_imp_eq_int)

apply(auto simp add: zmult_zless_mono2_lemma)

done

text{*The integers form an ordered integral domain*}

instance int :: ordered_idom

proof

  fix i j k :: int

  show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"

    by (rule zmult_zless_mono2)

  show "\<bar>i\<bar> = (if i < 0 then -i else i)"

    by (simp only: abs_int_def)

  show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"

    by (simp only: sgn_int_def)

qed

instance int :: lordered_ring

proof  

  fix k :: int

  show "abs k = sup k (- k)"

    by (auto simp add: sup_int_def abs_int_def less_minus_self_iff [symmetric])

qed

lemmas int_distrib =

  left_distrib [of "z1::int" "z2" "w", standard]

  right_distrib [of "w::int" "z1" "z2", standard]

  left_diff_distrib [of "z1::int" "z2" "w", standard]

  right_diff_distrib [of "w::int" "z1" "z2", standard]

subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}

(*

context ring_1

begin

definition 

  of_int :: "int \<Rightarrow> 'a" 

where

  "of_int 

*)

subsection {* Binary representation *}

text {*

  This formalization defines binary arithmetic in terms of the integers

  rather than using a datatype. This avoids multiple representations (leading

  zeroes, etc.)  See @{text "ZF/Tools/twos-compl.ML"}, function @{text

  int_of_binary}, for the numerical interpretation.

  The representation expects that @{text "(m mod 2)"} is 0 or 1,

  even if m is negative;

  For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus

  @{text "-5 = (-3)*2 + 1"}.

  This two's complement binary representation derives from the paper 

  "An Efficient Representation of Arithmetic for Term Rewriting" by

  Dave Cohen and Phil Watson, Rewriting Techniques and Applications,

  Springer LNCS 488 (240-251), 1991.

*}

subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}

definition

  Pls :: int where

  [code del]: "Pls = 0"

definition

  Min :: int where

  [code del]: "Min = - 1"

definition

  Bit0 :: "int \<Rightarrow> int" where

  [code del]: "Bit0 k = k + k"

definition

  Bit1 :: "int \<Rightarrow> int" where

  [code del]: "Bit1 k = 1 + k + k"

class number = -- {* for numeric types: nat, int, real, \dots *}

  fixes number_of :: "int \<Rightarrow> 'a"

(*use "~~/src/HOL/Tools/numeral.ML"

syntax

  "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")

use "~~/src/HOL/Tools/numeral_syntax.ML"

setup NumeralSyntax.setup

abbreviation

  "Numeral0 \<equiv> number_of Pls"

abbreviation

  "Numeral1 \<equiv> number_of (Bit1 Pls)"

lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"

  -- {* Unfold all @{text let}s involving constants *}

  unfolding Let_def ..

definition

  succ :: "int \<Rightarrow> int" where

  [code del]: "succ k = k + 1"

definition

  pred :: "int \<Rightarrow> int" where

  [code del]: "pred k = k - 1"

lemmas

  max_number_of [simp] = max_def

    [of "number_of u" "number_of v", standard, simp]

and

  min_number_of [simp] = min_def 

    [of "number_of u" "number_of v", standard, simp]

  -- {* unfolding @{text minx} and @{text max} on numerals *}

lemmas numeral_simps = 

  succ_def pred_def Pls_def Min_def Bit0_def Bit1_def

text {* Removal of leading zeroes *}

lemma Bit0_Pls [simp, code_post]:

  "Bit0 Pls = Pls"

  unfolding numeral_simps by simp

lemma Bit1_Min [simp, code_post]:

  "Bit1 Min = Min"

  unfolding numeral_simps by simp

lemmas normalize_bin_simps =

  Bit0_Pls Bit1_Min

*)

end