+
−
header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}+
−
+
−
theory LarryInt +
−
imports Nat "../QuotMain"+
−
begin+
−
+
−
fun+
−
  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" +
−
where+
−
  "intrel (x, y) (u, v) = (x + v = u + y)"+
−
+
−
quotient_type int = "nat \<times> nat" / intrel+
−
  by (auto simp add: equivp_def expand_fun_eq)+
−
+
−
instantiation int :: "{zero, one, plus, uminus, minus, times, ord}"+
−
begin+
−
+
−
quotient_definition +
−
  Zero_int_def: "0::int" as "(0::nat, 0::nat)"+
−
+
−
quotient_definition+
−
  One_int_def: "1::int" as "(1::nat, 0::nat)"+
−
+
−
definition+
−
  "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"+
−
+
−
quotient_definition+
−
  "(op +) :: int \<Rightarrow> int \<Rightarrow> int" +
−
as +
−
  "add_raw"+
−
+
−
definition+
−
  "uminus_raw \<equiv> \<lambda>(x::nat, y::nat). (y, x)"+
−
+
−
quotient_definition+
−
  "uminus :: int \<Rightarrow> int" +
−
as +
−
  "uminus_raw"+
−
+
−
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_definition+
−
  "(op *) :: int \<Rightarrow> int \<Rightarrow> int" +
−
as +
−
  "mult_raw"+
−
+
−
definition+
−
  "le_raw \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"+
−
+
−
quotient_definition +
−
  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" +
−
as +
−
  "le_raw"+
−
+
−
definition+
−
  less_int_def: "z < (w::int) \<equiv> (z \<le> w & z \<noteq> w)"+
−
+
−
definition+
−
  diff_int_def:  "z - (w::int) \<equiv> z + (-w)"+
−
+
−
instance ..+
−
+
−
end+
−
+
−
subsection{*Construction of the Integers*}+
−
+
−
lemma zminus_zminus_raw:+
−
  "uminus_raw (uminus_raw z) = z"+
−
  by (cases z) (simp add: uminus_raw_def)+
−
+
−
lemma [quot_respect]:+
−
  shows "(intrel ===> intrel) uminus_raw uminus_raw"+
−
  by (simp add: uminus_raw_def)+
−
  +
−
lemma zminus_zminus: +
−
  shows "- (- z) = (z::int)"+
−
apply(lifting zminus_zminus_raw)+
−
done+
−
+
−
lemma zminus_0_raw:+
−
  shows "uminus_raw (0, 0) = (0, 0::nat)"+
−
by (simp add: uminus_raw_def)+
−
+
−
lemma zminus_0: "- 0 = (0::int)"+
−
apply(lifting zminus_0_raw)+
−
done+
−
+
−
subsection{*Integer Addition*}+
−
+
−
lemma zminus_zadd_distrib_raw:+
−
  shows "uminus_raw (add_raw z w) = add_raw (uminus_raw z) (uminus_raw w)"+
−
by (cases z, cases w)+
−
   (auto simp add: add_raw_def uminus_raw_def)+
−
+
−
lemma [quot_respect]:+
−
  shows "(intrel ===> intrel ===> intrel) add_raw add_raw"+
−
by (simp add: add_raw_def)+
−
+
−
lemma zminus_zadd_distrib: +
−
  shows "- (z + w) = (- z) + (- w::int)"+
−
apply(lifting zminus_zadd_distrib_raw)+
−
done+
−
+
−
lemma zadd_commute_raw:+
−
  shows "add_raw z w = add_raw w z"+
−
by (cases z, cases w)+
−
   (simp add: add_raw_def)+
−
+
−
lemma zadd_commute:+
−
  shows "(z::int) + w = w + z"+
−
apply(lifting zadd_commute_raw)+
−
done+
−
+
−
lemma zadd_assoc_raw:+
−
  shows "add_raw (add_raw z1 z2) z3 = add_raw z1 (add_raw z2 z3)"+
−
by (cases z1, cases z2, cases z3) (simp add: add_raw_def)+
−
+
−
lemma zadd_assoc: "((z1::int) + z2) + z3 = z1 + (z2 + z3)"+
−
apply(lifting zadd_assoc_raw)+
−
done+
−
+
−
lemma zadd_0_raw:+
−
  fixes z::"nat \<times> nat"+
−
  shows "add_raw (0, 0) z = z"+
−
by (simp add: add_raw_def)+
−
+
−
+
−
(*also for the instance declaration int :: plus_ac0*)+
−
lemma zadd_0: "(0::int) + z = z"+
−
apply(lifting zadd_0_raw)+
−
done+
−
+
−
lemma zadd_zminus_inverse_raw:+
−
  shows "intrel (add_raw (uminus_raw z) z) (0, 0)"+
−
by (cases z) (simp add: add_raw_def uminus_raw_def)+
−
+
−
lemma zadd_zminus_inverse2: "(- z) + z = (0::int)"+
−
apply(lifting zadd_zminus_inverse_raw)+
−
done+
−
+
−
subsection{*Integer Multiplication*}+
−
+
−
lemma zmult_zminus_raw:+
−
  shows "mult_raw (uminus_raw z) w = uminus_raw (mult_raw z w)"+
−
apply(cases z, cases w)+
−
apply(simp add:uminus_raw_def)+
−
done+
−
+
−
lemma mult_raw_fst:+
−
  assumes a: "intrel x z"+
−
  shows "intrel (mult_raw x y) (mult_raw z y)"+
−
using a+
−
apply(cases x, cases y, cases z)+
−
apply(auto simp add: mult_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 mult_raw_snd:+
−
  assumes a: "intrel x z"+
−
  shows "intrel (mult_raw y x) (mult_raw y z)"+
−
using a+
−
apply(cases x, cases y, cases z)+
−
apply(auto simp add: mult_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 [quot_respect]:+
−
  shows "(intrel ===> intrel ===> intrel) mult_raw mult_raw"+
−
apply(simp only: fun_rel.simps)+
−
apply(rule allI | rule impI)++
−
apply(rule equivp_transp[OF int_equivp])+
−
apply(rule mult_raw_fst)+
−
apply(assumption)+
−
apply(rule mult_raw_snd)+
−
apply(assumption)+
−
done+
−
+
−
lemma zmult_zminus: "(- z) * w = - (z * (w::int))"+
−
apply(lifting zmult_zminus_raw)+
−
done+
−
+
−
lemma zmult_commute_raw: +
−
  shows "mult_raw z w = mult_raw w z"+
−
apply(cases z, cases w)+
−
apply(simp add: add_ac mult_ac)+
−
done+
−
+
−
lemma zmult_commute: "(z::int) * w = w * z"+
−
by (lifting zmult_commute_raw)+
−
+
−
lemma zmult_assoc_raw:+
−
  shows "mult_raw (mult_raw z1 z2) z3 = mult_raw z1 (mult_raw z2 z3)"+
−
apply(cases z1, cases z2, cases z3)+
−
apply(simp add: add_mult_distrib2 mult_ac)+
−
done+
−
+
−
lemma zmult_assoc: "((z1::int) * z2) * z3 = z1 * (z2 * z3)"+
−
by (lifting zmult_assoc_raw)+
−
+
−
lemma zadd_mult_distrib_raw:+
−
  shows "mult_raw (add_raw z1 z2) w = add_raw (mult_raw z1 w) (mult_raw z2 w)"+
−
apply(cases z1, cases z2, cases w)+
−
apply(simp add: add_mult_distrib2 mult_ac add_raw_def)+
−
done+
−
+
−
lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"+
−
apply(lifting zadd_mult_distrib_raw)+
−
done+
−
+
−
lemma zadd_zmult_distrib2: "(w::int) * (z1 + z2) = (w * z1) + (w * z2)"+
−
by (simp add: zmult_commute [of w] zadd_zmult_distrib)+
−
+
−
lemma zdiff_zmult_distrib: "((z1::int) - z2) * w = (z1 * w) - (z2 * w)"+
−
by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus)+
−
+
−
lemma zdiff_zmult_distrib2: "(w::int) * (z1 - z2) = (w * z1) - (w * z2)"+
−
by (simp add: zmult_commute [of w] zdiff_zmult_distrib)+
−
+
−
lemmas int_distrib =+
−
  zadd_zmult_distrib zadd_zmult_distrib2+
−
  zdiff_zmult_distrib zdiff_zmult_distrib2+
−
+
−
lemma zmult_1_raw:+
−
  shows "mult_raw (1, 0) z = z"+
−
apply(cases z)+
−
apply(auto)+
−
done+
−
+
−
lemma zmult_1: "(1::int) * z = z"+
−
apply(lifting zmult_1_raw)+
−
done+
−
+
−
lemma zmult_1_right: "z * (1::int) = z"+
−
by (rule trans [OF zmult_commute zmult_1])+
−
+
−
lemma zero_not_one:+
−
  shows "\<not>(intrel (0, 0) (1::nat, 0::nat))"+
−
by auto+
−
+
−
text{*The Integers Form A Ring*}+
−
instance int :: comm_ring_1+
−
proof+
−
  fix i j k :: int+
−
  show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)+
−
  show "i + j = j + i" by (simp add: zadd_commute)+
−
  show "0 + i = i" by (rule zadd_0)+
−
  show "- i + i = 0" by (rule zadd_zminus_inverse2)+
−
  show "i - j = i + (-j)" by (simp add: diff_int_def)+
−
  show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)+
−
  show "i * j = j * i" by (rule zmult_commute)+
−
  show "1 * i = i" by (rule zmult_1) +
−
  show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)+
−
  show "0 \<noteq> (1::int)" by (lifting zero_not_one)+
−
qed+
−
+
−
+
−
subsection{*The @{text "\<le>"} Ordering*}+
−
+
−
lemma zle_refl_raw:+
−
  "le_raw w w"+
−
apply(cases w)+
−
apply(simp add: le_raw_def)+
−
done+
−
+
−
lemma [quot_respect]:+
−
  shows "(intrel ===> intrel ===> op =) le_raw le_raw"+
−
by (auto) (simp_all add: le_raw_def)+
−
+
−
lemma zle_refl: "w \<le> (w::int)"+
−
apply(lifting zle_refl_raw)+
−
done+
−
+
−
lemma zle_trans_raw:+
−
  shows "\<lbrakk>le_raw i j; le_raw j k\<rbrakk> \<Longrightarrow> le_raw i k"+
−
apply(cases i, cases j, cases k)+
−
apply(auto)+
−
apply(simp add:le_raw_def)+
−
done+
−
+
−
lemma zle_trans: "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> (k::int)"+
−
apply(lifting zle_trans_raw)+
−
done+
−
+
−
lemma zle_anti_sym_raw:+
−
  shows "\<lbrakk>le_raw z w; le_raw w z\<rbrakk> \<Longrightarrow> intrel z w"+
−
apply(cases z, cases w)+
−
apply(auto iff: le_raw_def)+
−
done+
−
+
−
lemma zle_anti_sym: "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = (w::int)"+
−
apply(lifting zle_anti_sym_raw)+
−
done+
−
+
−
(* Axiom 'order_less_le' of class 'order': *)+
−
lemma zless_le: "((w::int) < z) = (w \<le> z & w \<noteq> z)"+
−
by (simp add: less_int_def)+
−
+
−
instance int :: order+
−
apply(intro_classes)+
−
apply(auto intro: zle_refl zle_trans zle_anti_sym zless_le simp add: less_int_def)+
−
done+
−
+
−
(* Axiom 'linorder_linear' of class 'linorder': *)+
−
+
−
lemma zle_linear_raw:+
−
  "le_raw z w \<or> le_raw w z"+
−
apply(cases w, cases z)+
−
apply(auto iff: le_raw_def)+
−
done+
−
+
−
+
−
lemma zle_linear: "(z::int) \<le> w \<or> w \<le> z"+
−
apply(lifting zle_linear_raw)+
−
done+
−
+
−
instance int :: linorder+
−
proof qed (rule zle_linear)+
−
+
−
lemma zadd_left_mono_raw:+
−
  shows "le_raw i j \<Longrightarrow> le_raw (add_raw k i) (add_raw k j)"+
−
apply(cases k)+
−
apply(auto simp add: add_raw_def le_raw_def)+
−
done+
−
+
−
lemma zadd_left_mono: "i \<le> j \<Longrightarrow> k + i \<le> k + (j::int)"+
−
apply(lifting zadd_left_mono_raw)+
−
done+
−
+
−
+
−
+
−
subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}+
−
+
−
definition+
−
  "nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"+
−
+
−
quotient_definition+
−
  "nat2::int\<Rightarrow>nat"+
−
as+
−
  "nat_raw"+
−
+
−
abbreviation+
−
  "less_raw x y \<equiv> (le_raw x y \<and> \<not>(x = y))"+
−
+
−
lemma nat_le_eq_zle_raw:+
−
  shows "less_raw (0, 0) w \<or> le_raw (0, 0) z \<Longrightarrow> (nat_raw w \<le> nat_raw z) = (le_raw w z)"+
−
apply(auto)+
−
sorry+
−
+
−
lemma [quot_respect]:+
−
  shows "(intrel ===> op =) nat_raw nat_raw"+
−
apply(auto iff: nat_raw_def)+
−
done+
−
+
−
ML {*+
−
  let+
−
   val parser = Args.context -- Scan.lift Args.name_source+
−
   fun term_pat (ctxt, str) =+
−
      str |> ProofContext.read_term_pattern ctxt+
−
          |> ML_Syntax.print_term+
−
          |> ML_Syntax.atomic+
−
in+
−
   ML_Antiquote.inline "term_pat" (parser >> term_pat)+
−
end+
−
+
−
*}+
−
+
−
consts test::"'b \<Rightarrow> 'b \<Rightarrow> 'b"+
−
+
−
+
−
lemma nat_le_eq_zle: "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"+
−
unfolding less_int_def+
−
apply(lifting nat_le_eq_zle_raw)+
−
done+
−
+
−
end+
−