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