1 theory IntEx2

     2 imports QuotMain

     3 uses

     4   ("Tools/numeral.ML")

     5   ("Tools/numeral_syntax.ML")

     6   ("Tools/int_arith.ML")

     7 begin

     8 

     9 fun

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

    11 where

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

    13 

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

    15   apply(unfold equivp_def)

    16   apply(auto simp add: mem_def expand_fun_eq)

    17   done

    18 

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

    20 begin

    21 

    22 quotient_def 

    23   zero_qnt::"int"

    24 where

    25   "zero_qnt \<equiv> (0::nat, 0::nat)"

    26 

    27 definition  Zero_int_def[code del]: 

    28   "0 = zero_qnt"

    29 

    30 quotient_def 

    31   one_qnt::"int"

    32 where

    33   "one_qnt \<equiv> (1::nat, 0::nat)"

    34 

    35 definition One_int_def[code del]:

    36   "1 = one_qnt"

    37 

    38 fun

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

    40 where

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

    42 

    43 quotient_def 

    44   plus_qnt::"int \<Rightarrow> int \<Rightarrow> int"

    45 where

    46   "plus_qnt \<equiv> plus_raw"

    47 

    48 definition add_int_def[code del]:

    49   "z + w = plus_qnt z w"

    50 

    51 fun

    52   minus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"

    53 where

    54   "minus_raw (x, y) = (y, x)"

    55 

    56 quotient_def 

    57   minus_qnt::"int \<Rightarrow> int"

    58 where

    59   "minus_qnt \<equiv> minus_raw"

    60 

    61 definition minus_int_def [code del]:

    62     "- z = minus_qnt z"

    63 

    64 definition

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

    66 

    67 fun

    68   mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"

    69 where

    70   "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"

    71 

    72 quotient_def 

    73   mult_qnt::"int \<Rightarrow> int \<Rightarrow> int"

    74 where

    75   "mult_qnt \<equiv> mult_raw"

    76 

    77 definition

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

    79 

    80 fun

    81   le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"

    82 where

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

    84 

    85 quotient_def 

    86   le_qnt :: "int \<Rightarrow> int \<Rightarrow> bool"

    87 where

    88   "le_qnt \<equiv> le_raw"

    89 

    90 definition

    91   le_int_def [code del]:

    92    "z \<le> w \<longleftrightarrow> le_qnt z w"

    93 

    94 definition

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

    96 

    97 definition

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

    99 

   100 definition

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

   102 

   103 instance ..

   104 

   105 end

   106 

   107 thm add_assoc

   108 

   109 lemma plus_raw_rsp[quotient_rsp]:

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

   111 by auto

   112 

   113 lemma mult_raw_rsp[quotient_rsp]:

   114   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"

   115 apply(auto)

   116 apply(simp add: mult algebra_simps)

   117 sorry

   118 

   119 lemma plus_assoc_raw:

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

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

   122 

   123 lemma plus_sym_raw:

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

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

   126 

   127 lemma plus_zero_raw:

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

   129 by (cases i) (simp)

   130 

   131 lemma plus_minus_zero_raw:

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

   133 by (cases i) (simp)

   134 

   135 lemma mult_assoc_raw:

   136   shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"

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

   138    (simp add: mult algebra_simps)

   139 

   140 lemma mult_sym_raw:

   141   shows "mult_raw i j \<approx> mult_raw j i"

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

   143 

   144 lemma mult_one_raw:

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

   146 by (cases i) (simp)

   147 

   148 lemma mult_plus_comm_raw:

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

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

   151    (simp add: mult algebra_simps)

   152 

   153 lemma one_zero_distinct:

   154   shows "(0, 0) \<noteq> ((1::nat), (0::nat))"

   155   by simp

   156   

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

   158 

   159 

   160 ML {* val qty = @{typ "int"} *}

   161 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}

   162 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "int" *}

   163 

   164 instance int :: comm_ring_1

   165 proof

   166   fix i j k :: int

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

   168     unfolding add_int_def

   169     apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} [@{thm int_equivp}] 1 *})

   170     done

   171   show "i + j = j + i" 

   172     unfolding add_int_def

   173     apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} [@{thm int_equivp}] 1 *})

   174     done

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

   176     unfolding add_int_def Zero_int_def 

   177     apply(tactic {* procedure_tac @{context} @{thm plus_zero_raw} 1 *})

   178     apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})

   179     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})

   180     defer

   181     apply(tactic {* clean_tac @{context} 1*})

   182     sorry

   183   show "- i + i = 0"

   184     unfolding add_int_def minus_int_def Zero_int_def 

   185     apply(tactic {* procedure_tac @{context} @{thm plus_minus_zero_raw} 1 *})

   186     apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})

   187     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})

   188     defer

   189     apply(tactic {* clean_tac @{context} 1*})

   190     sorry

   191   show "i - j = i + - j"

   192     by (simp add: diff_int_def)

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

   194     unfolding mult_int_def 

   195     apply(tactic {* procedure_tac @{context} @{thm mult_assoc_raw} 1 *})

   196     apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})

   197     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})

   198     defer

   199     apply(tactic {* clean_tac @{context} 1*})

   200     sorry

   201   show "i * j = j * i"

   202     unfolding mult_int_def 

   203     apply(tactic {* procedure_tac @{context} @{thm mult_sym_raw} 1 *})

   204     apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})

   205     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})

   206     defer

   207     apply(tactic {* clean_tac @{context} 1*})

   208     sorry

   209   show "1 * i = i"

   210     unfolding mult_int_def One_int_def

   211     apply(tactic {* procedure_tac @{context} @{thm mult_one_raw} 1 *})

   212     apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})

   213     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})

   214     defer

   215     apply(tactic {* clean_tac @{context} 1*})

   216     sorry

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

   218     unfolding mult_int_def add_int_def

   219     apply(tactic {* procedure_tac @{context} @{thm mult_plus_comm_raw} 1 *})

   220     apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})

   221     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})

   222     defer

   223     apply(tactic {* clean_tac @{context} 1*})

   224     sorry

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

   226     unfolding Zero_int_def One_int_def

   227     apply(tactic {* procedure_tac @{context} @{thm one_zero_distinct} 1 *})

   228     defer

   229     defer

   230     apply(tactic {* clean_tac @{context} 1*})

   231     sorry

   232 qed

   233