author haftmann Thu, 26 Apr 2007 13:33:07 +0200 changeset 22802 92026479179e parent 22801 caffcb450ef4 child 22803 5129e02f4df2
replaced recdef by function
 src/HOL/Integ/IntDiv.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Integ/IntDiv.thy	Thu Apr 26 13:33:05 2007 +0200
+++ b/src/HOL/Integ/IntDiv.thy	Thu Apr 26 13:33:07 2007 +0200
@@ -5,11 +5,10 @@

*)

-
header{*The Division Operators div and mod; the Divides Relation dvd*}

theory IntDiv
-imports "../Divides" "../SetInterval" "../Recdef"
+imports IntArith "../Divides" "../FunDef"
uses ("IntDiv_setup.ML")
begin

@@ -28,46 +27,47 @@
else (2*q, r)"

text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
-consts posDivAlg :: "int*int => int*int"
-recdef posDivAlg "measure (%(a,b). nat(a - b + 1))"
-    "posDivAlg (a,b) =
-       (if (a<b | b\<le>0) then (0,a)
-        else adjust b (posDivAlg(a, 2*b)))"
+function
+  posDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int"
+where
+  "posDivAlg a b =
+     (if (a<b | b\<le>0) then (0,a)
+        else adjust b (posDivAlg a (2*b)))"
+by auto
+termination by (relation "measure (%(a,b). nat(a - b + 1))") auto

text{*algorithm for the case @{text "a<0, b>0"}*}
-consts negDivAlg :: "int*int => int*int"
-recdef negDivAlg "measure (%(a,b). nat(- a - b))"
-    "negDivAlg (a,b) =
-       (if (0\<le>a+b | b\<le>0) then (-1,a+b)
-        else adjust b (negDivAlg(a, 2*b)))"
+function
+  negDivAlg :: "int \<Rightarrow> int \<Rightarrow> int \<times> int"
+where
+  "negDivAlg a b  =
+     (if (0\<le>a+b | b\<le>0) then (-1,a+b)
+      else adjust b (negDivAlg a (2*b)))"
+by auto
+termination by (relation "measure (%(a,b). nat(- a - b))") auto

text{*algorithm for the general case @{term "b\<noteq>0"}*}
constdefs
negateSnd :: "int*int => int*int"
[code func]: "negateSnd == %(q,r). (q,-r)"

-  divAlg :: "int*int => int*int"
+definition
+  divAlg :: "int \<times> int \<Rightarrow> int \<times> int"
--{*The full division algorithm considers all possible signs for a, b
including the special case @{text "a=0, b<0"} because
@{term negDivAlg} requires @{term "a<0"}.*}
-    [code func]: "divAlg ==
-       %(a,b). if 0\<le>a then
-                  if 0\<le>b then posDivAlg (a,b)
-                  else if a=0 then (0,0)
-                       else negateSnd (negDivAlg (-a,-b))
+where
+  "divAlg = (\<lambda>(a, b). (if 0\<le>a then
+                  if 0\<le>b then posDivAlg a b
+                  else if a=0 then (0, 0)
+                       else negateSnd (negDivAlg (-a) (-b))
else
-                  if 0<b then negDivAlg (a,b)
-                  else         negateSnd (posDivAlg (-a,-b))"
+                  if 0<b then negDivAlg a b
+                  else negateSnd (posDivAlg (-a) (-b))))"

-instance
-  int :: "Divides.div" ..       --{*avoid clash with 'div' token*}
-
-text{*The operators are defined with reference to the algorithm, which is
-proved to satisfy the specification.*}
-defs
-  div_def [code func]: "a div b == fst (divAlg (a,b))"
-  mod_def [code func]: "a mod b == snd (divAlg (a,b))"
-
+instance int :: Divides.div
+  div_def: "a div b == fst (divAlg (a, b))"
+  mod_def: "a mod b == snd (divAlg (a, b))" ..

text{*
Here is the division algorithm in ML:
@@ -155,18 +155,19 @@
text{*use with a simproc to avoid repeatedly proving the premise*}
lemma posDivAlg_eqn:
"0 < b ==>
-      posDivAlg (a,b) = (if a<b then (0,a) else adjust b (posDivAlg(a, 2*b)))"
+      posDivAlg a b = (if a<b then (0,a) else adjust b (posDivAlg a (2*b)))"
by (rule posDivAlg.simps [THEN trans], simp)

text{*Correctness of @{term posDivAlg}: it computes quotients correctly*}
-theorem posDivAlg_correct [rule_format]:
-     "0 \<le> a --> 0 < b --> quorem ((a, b), posDivAlg (a, b))"
-apply (induct_tac a b rule: posDivAlg.induct, auto)
- (*base case: a<b*)
-(*main argument*)
-apply (subst posDivAlg_eqn, simp_all)
+theorem posDivAlg_correct:
+  assumes "0 \<le> a" and "0 < b"
+  shows "quorem ((a, b), posDivAlg a b)"
+using prems apply (induct a b rule: posDivAlg.induct)
+apply auto
+apply (subst posDivAlg_eqn, simp add: right_distrib)
+apply (case_tac "a < b")
+apply simp_all
apply (erule splitE)
apply (auto simp add: right_distrib Let_def)
done
@@ -181,20 +182,21 @@
text{*use with a simproc to avoid repeatedly proving the premise*}
lemma negDivAlg_eqn:
"0 < b ==>
-      negDivAlg (a,b) =
-       (if 0\<le>a+b then (-1,a+b) else adjust b (negDivAlg(a, 2*b)))"
+      negDivAlg a b =
+       (if 0\<le>a+b then (-1,a+b) else adjust b (negDivAlg a (2*b)))"
by (rule negDivAlg.simps [THEN trans], simp)

(*Correctness of negDivAlg: it computes quotients correctly
It doesn't work if a=0 because the 0/b equals 0, not -1*)
-lemma negDivAlg_correct [rule_format]:
-     "a < 0 --> 0 < b --> quorem ((a, b), negDivAlg (a, b))"
-apply (induct_tac a b rule: negDivAlg.induct, auto)
- (*base case: 0\<le>a+b*)
-(*main argument*)
+lemma negDivAlg_correct:
+  assumes "a < 0" and "b > 0"
+  shows "quorem ((a, b), negDivAlg a b)"
+using prems apply (induct a b rule: negDivAlg.induct)
apply (subst negDivAlg_eqn, assumption)
+apply (case_tac "a + b < (0\<Colon>int)")
+apply simp_all
apply (erule splitE)
apply (auto simp add: right_distrib Let_def)
done
@@ -206,10 +208,10 @@
lemma quorem_0: "b \<noteq> 0 ==> quorem ((0,b), (0,0))"
by (auto simp add: quorem_def linorder_neq_iff)

-lemma posDivAlg_0 [simp]: "posDivAlg (0, b) = (0, 0)"
+lemma posDivAlg_0 [simp]: "posDivAlg 0 b = (0, 0)"
by (subst posDivAlg.simps, auto)

-lemma negDivAlg_minus1 [simp]: "negDivAlg (-1, b) = (-1, b - 1)"
+lemma negDivAlg_minus1 [simp]: "negDivAlg -1 b = (-1, b - 1)"
by (subst negDivAlg.simps, auto)

lemma negateSnd_eq [simp]: "negateSnd(q,r) = (q,-r)"
@@ -218,7 +220,7 @@
lemma quorem_neg: "quorem ((-a,-b), qr) ==> quorem ((a,b), negateSnd qr)"
by (auto simp add: split_ifs quorem_def)

-lemma divAlg_correct: "b \<noteq> 0 ==> quorem ((a,b), divAlg(a,b))"
+lemma divAlg_correct: "b \<noteq> 0 ==> quorem ((a,b), divAlg (a, b))"
by (force simp add: linorder_neq_iff quorem_0 divAlg_def quorem_neg
posDivAlg_correct negDivAlg_correct)

@@ -250,19 +252,16 @@
apply (auto simp add: quorem_def mod_def)
done

-lemmas pos_mod_sign  = pos_mod_conj [THEN conjunct1, standard]
-   and pos_mod_bound = pos_mod_conj [THEN conjunct2, standard]
-
-declare pos_mod_sign[simp] pos_mod_bound[simp]
+lemmas pos_mod_sign  [simp] = pos_mod_conj [THEN conjunct1, standard]
+   and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2, standard]

lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
apply (cut_tac a = a and b = b in divAlg_correct)
apply (auto simp add: quorem_def div_def mod_def)
done

-lemmas neg_mod_sign  = neg_mod_conj [THEN conjunct1, standard]
-   and neg_mod_bound = neg_mod_conj [THEN conjunct2, standard]
-declare neg_mod_sign[simp] neg_mod_bound[simp]
+lemmas neg_mod_sign  [simp] = neg_mod_conj [THEN conjunct1, standard]
+   and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2, standard]

@@ -423,84 +422,73 @@

text{*a positive, b positive *}

-lemma div_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a div b = fst (posDivAlg(a,b))"
+lemma div_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a div b = fst (posDivAlg a b)"

-lemma mod_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a mod b = snd (posDivAlg(a,b))"
+lemma mod_pos_pos: "[| 0 < a;  0 \<le> b |] ==> a mod b = snd (posDivAlg a b)"

text{*a negative, b positive *}

-lemma div_neg_pos: "[| a < 0;  0 < b |] ==> a div b = fst (negDivAlg(a,b))"
+lemma div_neg_pos: "[| a < 0;  0 < b |] ==> a div b = fst (negDivAlg a b)"

-lemma mod_neg_pos: "[| a < 0;  0 < b |] ==> a mod b = snd (negDivAlg(a,b))"
+lemma mod_neg_pos: "[| a < 0;  0 < b |] ==> a mod b = snd (negDivAlg a b)"

text{*a positive, b negative *}

lemma div_pos_neg:
-     "[| 0 < a;  b < 0 |] ==> a div b = fst (negateSnd(negDivAlg(-a,-b)))"
+     "[| 0 < a;  b < 0 |] ==> a div b = fst (negateSnd (negDivAlg (-a) (-b)))"

lemma mod_pos_neg:
-     "[| 0 < a;  b < 0 |] ==> a mod b = snd (negateSnd(negDivAlg(-a,-b)))"
+     "[| 0 < a;  b < 0 |] ==> a mod b = snd (negateSnd (negDivAlg (-a) (-b)))"

text{*a negative, b negative *}

lemma div_neg_neg:
-     "[| a < 0;  b \<le> 0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))"
+     "[| a < 0;  b \<le> 0 |] ==> a div b = fst (negateSnd (posDivAlg (-a) (-b)))"

lemma mod_neg_neg:
-     "[| a < 0;  b \<le> 0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))"
+     "[| a < 0;  b \<le> 0 |] ==> a mod b = snd (negateSnd (posDivAlg (-a) (-b)))"

text {*Simplify expresions in which div and mod combine numerical constants*}

-lemmas div_pos_pos_number_of =
+lemmas div_pos_pos_number_of [simp] =
div_pos_pos [of "number_of v" "number_of w", standard]
-declare div_pos_pos_number_of [simp]

-lemmas div_neg_pos_number_of =
+lemmas div_neg_pos_number_of [simp] =
div_neg_pos [of "number_of v" "number_of w", standard]
-declare div_neg_pos_number_of [simp]

-lemmas div_pos_neg_number_of =
+lemmas div_pos_neg_number_of [simp] =
div_pos_neg [of "number_of v" "number_of w", standard]
-declare div_pos_neg_number_of [simp]

-lemmas div_neg_neg_number_of =
+lemmas div_neg_neg_number_of [simp] =
div_neg_neg [of "number_of v" "number_of w", standard]
-declare div_neg_neg_number_of [simp]

-lemmas mod_pos_pos_number_of =
+lemmas mod_pos_pos_number_of [simp] =
mod_pos_pos [of "number_of v" "number_of w", standard]
-declare mod_pos_pos_number_of [simp]

-lemmas mod_neg_pos_number_of =
+lemmas mod_neg_pos_number_of [simp] =
mod_neg_pos [of "number_of v" "number_of w", standard]
-declare mod_neg_pos_number_of [simp]

-lemmas mod_pos_neg_number_of =
+lemmas mod_pos_neg_number_of [simp] =
mod_pos_neg [of "number_of v" "number_of w", standard]
-declare mod_pos_neg_number_of [simp]

-lemmas mod_neg_neg_number_of =
+lemmas mod_neg_neg_number_of [simp] =
mod_neg_neg [of "number_of v" "number_of w", standard]
-declare mod_neg_neg_number_of [simp]

-lemmas posDivAlg_eqn_number_of =
+lemmas posDivAlg_eqn_number_of [simp] =
posDivAlg_eqn [of "number_of v" "number_of w", standard]
-declare posDivAlg_eqn_number_of [simp]

-lemmas negDivAlg_eqn_number_of =
+lemmas negDivAlg_eqn_number_of [simp] =
negDivAlg_eqn [of "number_of v" "number_of w", standard]
-declare negDivAlg_eqn_number_of [simp]
-

text{*Special-case simplification *}
@@ -526,30 +514,24 @@
(** The last remaining special cases for constant arithmetic:
1 div z and 1 mod z **)

-lemmas div_pos_pos_1_number_of =
+lemmas div_pos_pos_1_number_of [simp] =
div_pos_pos [OF int_0_less_1, of "number_of w", standard]
-declare div_pos_pos_1_number_of [simp]

-lemmas div_pos_neg_1_number_of =
+lemmas div_pos_neg_1_number_of [simp] =
div_pos_neg [OF int_0_less_1, of "number_of w", standard]
-declare div_pos_neg_1_number_of [simp]

-lemmas mod_pos_pos_1_number_of =
+lemmas mod_pos_pos_1_number_of [simp] =
mod_pos_pos [OF int_0_less_1, of "number_of w", standard]
-declare mod_pos_pos_1_number_of [simp]

-lemmas mod_pos_neg_1_number_of =
+lemmas mod_pos_neg_1_number_of [simp] =
mod_pos_neg [OF int_0_less_1, of "number_of w", standard]
-declare mod_pos_neg_1_number_of [simp]

-lemmas posDivAlg_eqn_1_number_of =
+lemmas posDivAlg_eqn_1_number_of [simp] =
posDivAlg_eqn [of concl: 1 "number_of w", standard]
-declare posDivAlg_eqn_1_number_of [simp]

-lemmas negDivAlg_eqn_1_number_of =
+lemmas negDivAlg_eqn_1_number_of [simp] =
negDivAlg_eqn [of concl: 1 "number_of w", standard]
-declare negDivAlg_eqn_1_number_of [simp]

@@ -685,8 +667,7 @@
thus "m mod d = 0" by auto
qed

-lemmas zmod_eq_0D = zmod_eq_0_iff [THEN iffD1]
-declare zmod_eq_0D [dest!]
+lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]

text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}

@@ -1047,11 +1028,9 @@
lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"

-lemmas zdvd_iff_zmod_eq_0_number_of =
+lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]

-declare zdvd_iff_zmod_eq_0_number_of [simp]
-
lemma zdvd_0_right [iff]: "(m::int) dvd 0"

@@ -1380,115 +1359,15 @@
apply simp_all
done

-ML
-{*
-val quorem_def = thm "quorem_def";
+text {* code serializer setup *}
+
+code_modulename SML
+  IntDiv Integer

-val unique_quotient = thm "unique_quotient";
-val unique_remainder = thm "unique_remainder";
-val posDivAlg_eqn = thm "posDivAlg_eqn";
-val posDivAlg_correct = thm "posDivAlg_correct";
-val negDivAlg_eqn = thm "negDivAlg_eqn";
-val negDivAlg_correct = thm "negDivAlg_correct";
-val quorem_0 = thm "quorem_0";
-val posDivAlg_0 = thm "posDivAlg_0";
-val negDivAlg_minus1 = thm "negDivAlg_minus1";
-val negateSnd_eq = thm "negateSnd_eq";
-val quorem_neg = thm "quorem_neg";
-val divAlg_correct = thm "divAlg_correct";
-val DIVISION_BY_ZERO = thm "DIVISION_BY_ZERO";
-val zmod_zdiv_equality = thm "zmod_zdiv_equality";
-val pos_mod_conj = thm "pos_mod_conj";
-val pos_mod_sign = thm "pos_mod_sign";
-val neg_mod_conj = thm "neg_mod_conj";
-val neg_mod_sign = thm "neg_mod_sign";
-val quorem_div_mod = thm "quorem_div_mod";
-val quorem_div = thm "quorem_div";
-val quorem_mod = thm "quorem_mod";
-val div_pos_pos_trivial = thm "div_pos_pos_trivial";
-val div_neg_neg_trivial = thm "div_neg_neg_trivial";
-val div_pos_neg_trivial = thm "div_pos_neg_trivial";
-val mod_pos_pos_trivial = thm "mod_pos_pos_trivial";
-val mod_neg_neg_trivial = thm "mod_neg_neg_trivial";
-val mod_pos_neg_trivial = thm "mod_pos_neg_trivial";
-val zdiv_zminus_zminus = thm "zdiv_zminus_zminus";
-val zmod_zminus_zminus = thm "zmod_zminus_zminus";
-val zdiv_zminus1_eq_if = thm "zdiv_zminus1_eq_if";
-val zmod_zminus1_eq_if = thm "zmod_zminus1_eq_if";
-val zdiv_zminus2 = thm "zdiv_zminus2";
-val zmod_zminus2 = thm "zmod_zminus2";
-val zdiv_zminus2_eq_if = thm "zdiv_zminus2_eq_if";
-val zmod_zminus2_eq_if = thm "zmod_zminus2_eq_if";
-val self_quotient = thm "self_quotient";
-val self_remainder = thm "self_remainder";
-val zdiv_self = thm "zdiv_self";
-val zmod_self = thm "zmod_self";
-val zdiv_zero = thm "zdiv_zero";
-val div_eq_minus1 = thm "div_eq_minus1";
-val zmod_zero = thm "zmod_zero";
-val zdiv_minus1 = thm "zdiv_minus1";
-val zmod_minus1 = thm "zmod_minus1";
-val div_pos_pos = thm "div_pos_pos";
-val mod_pos_pos = thm "mod_pos_pos";
-val div_neg_pos = thm "div_neg_pos";
-val mod_neg_pos = thm "mod_neg_pos";
-val div_pos_neg = thm "div_pos_neg";
-val mod_pos_neg = thm "mod_pos_neg";
-val div_neg_neg = thm "div_neg_neg";
-val mod_neg_neg = thm "mod_neg_neg";
-val zmod_1 = thm "zmod_1";
-val zdiv_1 = thm "zdiv_1";
-val zmod_minus1_right = thm "zmod_minus1_right";
-val zdiv_minus1_right = thm "zdiv_minus1_right";
-val zdiv_mono1 = thm "zdiv_mono1";
-val zdiv_mono1_neg = thm "zdiv_mono1_neg";
-val zdiv_mono2 = thm "zdiv_mono2";
-val zdiv_mono2_neg = thm "zdiv_mono2_neg";
-val zdiv_zmult1_eq = thm "zdiv_zmult1_eq";
-val zmod_zmult1_eq = thm "zmod_zmult1_eq";
-val zmod_zmult1_eq' = thm "zmod_zmult1_eq'";
-val zmod_zmult_distrib = thm "zmod_zmult_distrib";
-val zdiv_zmult_self1 = thm "zdiv_zmult_self1";
-val zdiv_zmult_self2 = thm "zdiv_zmult_self2";
-val zmod_zmult_self1 = thm "zmod_zmult_self1";
-val zmod_zmult_self2 = thm "zmod_zmult_self2";
-val zmod_eq_0_iff = thm "zmod_eq_0_iff";
-val mod_div_trivial = thm "mod_div_trivial";
-val mod_mod_trivial = thm "mod_mod_trivial";
-val zdiv_zmult2_eq = thm "zdiv_zmult2_eq";
-val zmod_zmult2_eq = thm "zmod_zmult2_eq";
-val zdiv_zmult_zmult1 = thm "zdiv_zmult_zmult1";
-val zdiv_zmult_zmult2 = thm "zdiv_zmult_zmult2";
-val zmod_zmult_zmult1 = thm "zmod_zmult_zmult1";
-val zmod_zmult_zmult2 = thm "zmod_zmult_zmult2";
-val pos_zdiv_mult_2 = thm "pos_zdiv_mult_2";
-val neg_zdiv_mult_2 = thm "neg_zdiv_mult_2";
-val zdiv_number_of_BIT = thm "zdiv_number_of_BIT";
-val pos_zmod_mult_2 = thm "pos_zmod_mult_2";
-val neg_zmod_mult_2 = thm "neg_zmod_mult_2";
-val zmod_number_of_BIT = thm "zmod_number_of_BIT";
-val div_neg_pos_less0 = thm "div_neg_pos_less0";
-val div_nonneg_neg_le0 = thm "div_nonneg_neg_le0";
-val pos_imp_zdiv_nonneg_iff = thm "pos_imp_zdiv_nonneg_iff";
-val neg_imp_zdiv_nonneg_iff = thm "neg_imp_zdiv_nonneg_iff";
-val pos_imp_zdiv_neg_iff = thm "pos_imp_zdiv_neg_iff";
-val neg_imp_zdiv_neg_iff = thm "neg_imp_zdiv_neg_iff";
+code_modulename OCaml
+  IntDiv Integer

-val zpower_zmod = thm "zpower_zmod";