theory IntEx2
imports QuotMain
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
  apply(unfold equivp_def)
  apply(auto simp add: mem_def expand_fun_eq)
  done

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

quotient_def 
  zero_qnt::"int"
where
  "zero_qnt \<equiv> (0::nat, 0::nat)"

definition  Zero_int_def[code del]: 
  "0 = zero_qnt"

quotient_def 
  one_qnt::"int"
where
  "one_qnt \<equiv> (1::nat, 0::nat)"

definition One_int_def[code del]:
  "1 = one_qnt"

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_qnt::"int \<Rightarrow> int \<Rightarrow> int"
where
  "plus_qnt \<equiv> plus_raw"

definition add_int_def[code del]:
  "z + w = plus_qnt z w"

fun
  minus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
where
  "minus_raw (x, y) = (y, x)"

quotient_def
  minus_qnt::"int \<Rightarrow> int"
where
  "minus_qnt \<equiv> minus_raw"

definition minus_int_def [code del]:
    "- z = minus_qnt z"

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

fun
  mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
where
  "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"

quotient_def 
  mult_qnt::"int \<Rightarrow> int \<Rightarrow> int"
where
  "mult_qnt \<equiv> mult_raw"

definition
  mult_int_def [code del]: "z * w = mult_qnt z w"

fun
  le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
where
  "le_raw (x, y) (u, v) = (x+v \<le> u+y)"

quotient_def 
  le_qnt :: "int \<Rightarrow> int \<Rightarrow> bool"
where
  "le_qnt \<equiv> le_raw"

definition
  le_int_def [code del]:
   "z \<le> w = le_qnt z w"

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

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

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

instance ..

end

thm add_assoc

lemma plus_raw_rsp[quotient_rsp]:
  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
by auto

lemma minus_raw_rsp[quotient_rsp]:
  shows "(op \<approx> ===> op \<approx>) minus_raw minus_raw"
  by auto

lemma mult_raw_rsp[quotient_rsp]:
  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
apply(auto)
apply(simp add: mult algebra_simps)
sorry

lemma le_raw_rsp[quotient_rsp]:
  shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_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 (minus_raw i) i \<approx> (0, 0)"
by (cases i) (simp)

lemma mult_assoc_raw:
  shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"
by (cases i, cases j, cases k) 
   (simp add: mult algebra_simps)

lemma mult_sym_raw:
  shows "mult_raw i j \<approx> mult_raw j i"
by (cases i, cases j) (simp)

lemma mult_one_raw:
  shows "mult_raw  (1, 0) i \<approx> i"
by (cases i) (simp)

lemma mult_plus_comm_raw:
  shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
by (cases i, cases j, cases k) 
   (simp add: mult 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 {* val qty = @{typ "int"} *}
ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "int" *}

instance int :: comm_ring_1
proof
  fix i j k :: int
  show "(i + j) + k = i + (j + k)"
    unfolding add_int_def
    apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} [@{thm int_equivp}] 1 *})
    done
  show "i + j = j + i" 
    unfolding add_int_def
    apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} [@{thm int_equivp}] 1 *})
    done
  show "0 + i = (i::int)"
    unfolding add_int_def Zero_int_def 
    apply(tactic {* lift_tac @{context} @{thm plus_zero_raw} [@{thm int_equivp}] 1 *})
    done
  show "- i + i = 0"
    unfolding add_int_def minus_int_def Zero_int_def 
    apply(tactic {* lift_tac @{context} @{thm plus_minus_zero_raw} [@{thm int_equivp}] 1 *})
    done
  show "i - j = i + - j"
    by (simp add: diff_int_def)
  show "(i * j) * k = i * (j * k)"
    unfolding mult_int_def 
    apply(tactic {* lift_tac @{context} @{thm mult_assoc_raw} [@{thm int_equivp}] 1 *})
    done
  show "i * j = j * i"
    unfolding mult_int_def 
    apply(tactic {* lift_tac @{context} @{thm mult_sym_raw} [@{thm int_equivp}] 1 *})
    done
  show "1 * i = i"
    unfolding mult_int_def One_int_def
    apply(tactic {* lift_tac @{context} @{thm mult_one_raw} [@{thm int_equivp}] 1 *})
    done
  show "(i + j) * k = i * k + j * k"
    unfolding mult_int_def add_int_def
    apply(tactic {* lift_tac @{context} @{thm mult_plus_comm_raw} [@{thm int_equivp}] 1 *})
    done
  show "0 \<noteq> (1::int)"
    unfolding Zero_int_def One_int_def
    apply(tactic {* lift_tac @{context} @{thm one_zero_distinct} [@{thm int_equivp}] 1 *})
    done
qed

term of_nat
thm of_nat_def

lemma int_def: "of_nat m = ABS_int (m, 0)"
apply(induct m) 
apply(simp add: Zero_int_def zero_qnt_def)
apply(simp)
apply(simp add: add_int_def One_int_def)
apply(simp add: plus_qnt_def one_qnt_def)
oops

lemma le_antisym_raw:
  shows "le_raw i j \<Longrightarrow> le_raw j i \<Longrightarrow> i \<approx> j"
by (cases i, cases j) (simp)

lemma le_refl_raw:
  shows "le_raw i i"
by (cases i) (simp)

lemma le_trans_raw:
  shows "le_raw i j \<Longrightarrow> le_raw j k \<Longrightarrow> le_raw i k"
by (cases i, cases j, cases k) (simp)

lemma le_cases_raw:
  shows "le_raw i j \<or> le_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"
    unfolding le_int_def
    apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} [@{thm int_equivp}] 1 *})
    done
  show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
    by (auto simp add: less_int_def dest: antisym) 
  show "i \<le> i"
    unfolding le_int_def
    apply(tactic {* lift_tac @{context} @{thm le_refl_raw} [@{thm int_equivp}] 1 *})
    done
  show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
    unfolding le_int_def
    apply(tactic {* lift_tac @{context} @{thm le_trans_raw} [@{thm int_equivp}] 1 *})
    done
  show "i \<le> j \<or> j \<le> i"
    unfolding le_int_def
    apply(tactic {* lift_tac @{context} @{thm le_cases_raw} [@{thm int_equivp}] 1 *})
    done
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 "le_raw i j \<Longrightarrow> le_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"
    unfolding le_int_def add_int_def
    apply(tactic {* lift_tac @{context} @{thm le_plus_raw} [@{thm int_equivp}] 1 *})
    done
qed

lemma test:
  "\<lbrakk>le_raw i j \<and> \<not>i \<approx> j; le_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk>
    \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> \<not>mult_raw k i \<approx> mult_raw k j"
apply(cases i, cases j, cases k)
apply(auto simp add: mult algebra_simps)
sorry


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"
    unfolding mult_int_def le_int_def less_int_def Zero_int_def
    apply(tactic {* lift_tac @{context} @{thm test} [@{thm int_equivp}] 1 *})
    done
  show "\<bar>i\<bar> = (if i < 0 then -i else i)"
    by (simp only: zabs_def)
  show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
    by (simp only: zsgn_def)
qed

instance int :: lordered_ring
proof  
  fix k :: int
  show "abs k = sup k (- k)"
    by (auto simp add: sup_int_def zabs_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