diff -r b1281a0051ae -r b611aee9f8e7 Attic/Quot/Examples/IntEx2.thy
--- a/Attic/Quot/Examples/IntEx2.thy	Thu Apr 29 09:13:18 2010 +0200
+++ b/Attic/Quot/Examples/IntEx2.thy	Thu Apr 29 09:14:16 2010 +0200
@@ -1,361 +1,7 @@
 theory IntEx2
-imports "../Quotient" "../Quotient_Product" Nat
-(*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_type int = "nat \<times> nat" / intrel
-  unfolding equivp_def
-  by (auto simp add: mem_def expand_fun_eq)
-
-instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
+imports "Quotient_Int"
 begin
 
-ML {* @{term "0 \<Colon> int"} *}
-
-quotient_definition
-  "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)"
-
-quotient_definition
-  "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)"
-
-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_definition
-  "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_raw"
-
-fun
-  uminus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
-where
-  "uminus_raw (x, y) = (y, x)"
-
-quotient_definition
-  "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_raw"
-
-definition
-  minus_int_def [code del]:  "z - w = z + (-w\<Colon>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_definition
-  mult_int_def: "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "mult_raw"
-
-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_definition
-  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_raw"
-
-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
-
-lemma plus_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
-  by auto
-
-lemma uminus_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw"
-  by auto
-
-lemma mult_raw_fst:
-  assumes a: "x \<approx> z"
-  shows "mult_raw x y \<approx> 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: "x \<approx> z"
-  shows "mult_raw y x \<approx> 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 mult_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
-  apply(simp only: fun_rel_def)
-  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 le_raw_rsp[quot_respect]:
-  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 (uminus_raw i) i \<approx> (0, 0)"
-  by (cases i) (simp)
-
-lemma times_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: algebra_simps)
-
-lemma times_sym_raw:
-  shows "mult_raw i j \<approx> mult_raw j i"
-  by (cases i, cases j) (simp add: algebra_simps)
-
-lemma times_one_raw:
-  shows "mult_raw  (1, 0) i \<approx> i"
-  by (cases i) (simp)
-
-lemma times_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: 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}*}
-
-instance int :: comm_ring_1
-proof
-  fix i j k :: int
-  show "(i + j) + k = i + (j + k)"
-    by (lifting plus_assoc_raw)
-  show "i + j = j + i" 
-    by (lifting plus_sym_raw)
-  show "0 + i = (i::int)"
-    by (lifting plus_zero_raw)
-  show "- i + i = 0"
-    by (lifting plus_minus_zero_raw)
-  show "i - j = i + - j"
-    by (simp add: minus_int_def)
-  show "(i * j) * k = i * (j * k)"
-    by (lifting times_assoc_raw)
-  show "i * j = j * i"
-    by (lifting times_sym_raw)
-  show "1 * i = i"
-    by (lifting times_one_raw)
-  show "(i + j) * k = i * k + j * k"
-    by (lifting times_plus_comm_raw)
-  show "0 \<noteq> (1::int)"
-    by (lifting one_zero_distinct)
-qed
-
-lemma plus_raw_rsp_aux:
-  assumes a: "a \<approx> b" "c \<approx> d"
-  shows "plus_raw a c \<approx> plus_raw b d"
-  using a
-  by (cases a, cases b, cases c, cases d)
-     (simp)
-
-lemma add:
-  "(abs_int (x,y)) + (abs_int (u,v)) =
-   (abs_int (x + u, y + v))"
-  apply(simp add: plus_int_def id_simps)
-  apply(fold plus_raw.simps)
-  apply(rule Quotient_rel_abs[OF Quotient_int])
-  apply(rule plus_raw_rsp_aux)
-  apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
-  done
-
-definition int_of_nat_raw: 
-  "int_of_nat_raw m = (m :: nat, 0 :: nat)"
-
-quotient_definition
-  "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"
-
-lemma[quot_respect]: 
-  shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
-  by (simp add: equivp_reflp[OF int_equivp])
-
-lemma int_of_nat:
-  shows "of_nat m = int_of_nat m"
-  by (induct m)
-    (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add)
-
-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"
-    by (lifting le_antisym_raw)
-  show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
-    by (auto simp add: less_int_def dest: antisym) 
-  show "i \<le> i"
-    by (lifting le_refl_raw)
-  show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
-    by (lifting le_trans_raw)
-  show "i \<le> j \<or> j \<le> i"
-    by (lifting le_cases_raw)
-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 :: ordered_cancel_ab_semigroup_add
-proof
-  fix i j k :: int
-  show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
-    by (lifting le_plus_raw)
-qed
-
-abbreviation
-  "less_raw i j \<equiv> le_raw i j \<and> \<not>(i \<approx> j)"
-
-lemma zmult_zless_mono2_lemma:
-  fixes i j::int
-  and   k::nat
-  shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
-  apply(induct "k")
-  apply(simp)
-  apply(case_tac "k = 0")
-  apply(simp_all add: left_distrib add_strict_mono)
-  done
-
-lemma zero_le_imp_eq_int_raw:
-  fixes k::"(nat \<times> nat)"
-  shows "less_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
-  apply(cases k)
-  apply(simp add:int_of_nat_raw)
-  apply(auto)
-  apply(rule_tac i="b" and j="a" in less_Suc_induct)
-  apply(auto)
-  done
-
-lemma zero_le_imp_eq_int:
-  fixes k::int
-  shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
-  unfolding less_int_def int_of_nat
-  by (lifting zero_le_imp_eq_int_raw)
-
-lemma zmult_zless_mono2: 
-  fixes i j k::int
-  assumes a: "i < j" "0 < k"
-  shows "k * i < k * j"
-  using a
-  by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
-
-text{*The integers form an ordered integral domain*}
-instance int :: linordered_idom
-proof
-  fix i j k :: int
-  show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
-    by (rule zmult_zless_mono2)
-  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
-
-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]
-
-lemma int_induct_raw:
-  assumes a: "P (0::nat, 0)"
-  and     b: "\<And>i. P i \<Longrightarrow> P (plus_raw i (1, 0))"
-  and     c: "\<And>i. P i \<Longrightarrow> P (plus_raw i (uminus_raw (1, 0)))"
-  shows      "P x"
-proof (cases x, clarify)
-  fix a b
-  show "P (a, b)"
-  proof (induct a arbitrary: b rule: Nat.induct)
-    case zero
-    show "P (0, b)" using assms by (induct b) auto
-  next
-    case (Suc n)
-    then show ?case using assms by auto
-  qed
-qed
-
-lemma int_induct:
-  fixes x :: int
-  assumes a: "P 0"
-  and     b: "\<And>i. P i \<Longrightarrow> P (i + 1)"
-  and     c: "\<And>i. P i \<Longrightarrow> P (i - 1)"
-  shows      "P x"
-  using a b c unfolding minus_int_def
-  by (lifting int_induct_raw)
-
 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
 
 (*