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 \<longleftrightarrow> le_qnt z w"

definition
  less_int_def [code del]: "(z\<Colon>int) < w \<longleftrightarrow> 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 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 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 "(0, 0) \<noteq> ((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 {* procedure_tac @{context} @{thm plus_zero_raw} 1 *})
    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
    defer
    apply(tactic {* clean_tac @{context} 1*})
    sorry
  show "- i + i = 0"
    unfolding add_int_def minus_int_def Zero_int_def 
    apply(tactic {* procedure_tac @{context} @{thm plus_minus_zero_raw} 1 *})
    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
    defer
    apply(tactic {* clean_tac @{context} 1*})
    sorry
  show "i - j = i + - j"
    by (simp add: diff_int_def)
  show "(i * j) * k = i * (j * k)"
    unfolding mult_int_def 
    apply(tactic {* procedure_tac @{context} @{thm mult_assoc_raw} 1 *})
    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
    defer
    apply(tactic {* clean_tac @{context} 1*})
    sorry
  show "i * j = j * i"
    unfolding mult_int_def 
    apply(tactic {* procedure_tac @{context} @{thm mult_sym_raw} 1 *})
    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
    defer
    apply(tactic {* clean_tac @{context} 1*})
    sorry
  show "1 * i = i"
    unfolding mult_int_def One_int_def
    apply(tactic {* procedure_tac @{context} @{thm mult_one_raw} 1 *})
    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
    defer
    apply(tactic {* clean_tac @{context} 1*})
    sorry
  show "(i + j) * k = i * k + j * k"
    unfolding mult_int_def add_int_def
    apply(tactic {* procedure_tac @{context} @{thm mult_plus_comm_raw} 1 *})
    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
    defer
    apply(tactic {* clean_tac @{context} 1*})
    sorry
  show "0 \<noteq> (1::int)"
    unfolding Zero_int_def One_int_def
    apply(tactic {* procedure_tac @{context} @{thm one_zero_distinct} 1 *})
    defer
    defer
    apply(tactic {* clean_tac @{context} 1*})
    sorry
qed