1.1 --- a/src/HOL/Algebra/IntRing.thy Wed Feb 18 13:39:05 2009 +0100
1.2 +++ b/src/HOL/Algebra/IntRing.thy Wed Feb 18 13:39:16 2009 +0100
1.3 @@ -407,7 +407,7 @@
1.4
1.5 hence "b mod m = (x * m + a) mod m" by simp
1.6 also
1.7 - have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq)
1.8 + have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: mod_add_eq)
1.9 also
1.10 have "\<dots> = a mod m" by simp
1.11 finally
2.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML Wed Feb 18 13:39:05 2009 +0100
2.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Wed Feb 18 13:39:16 2009 +0100
2.3 @@ -30,7 +30,7 @@
2.4 val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
2.5 val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
2.6 val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
2.7 -val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym;
2.8 +val int_mod_add_eq = @{thm mod_add_eq} RS sym;
2.9 val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
2.10 val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
2.11 val nat_div_add_eq = @{thm div_add1_eq} RS sym;
3.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML Wed Feb 18 13:39:05 2009 +0100
3.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Wed Feb 18 13:39:16 2009 +0100
3.3 @@ -34,7 +34,7 @@
3.4 val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
3.5 val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
3.6 val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
3.7 -val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym;
3.8 +val int_mod_add_eq = @{thm mod_add_eq} RS sym;
3.9 val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
3.10 val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
3.11 val nat_div_add_eq = @{thm div_add1_eq} RS sym;
4.1 --- a/src/HOL/Decision_Procs/mir_tac.ML Wed Feb 18 13:39:05 2009 +0100
4.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML Wed Feb 18 13:39:16 2009 +0100
4.3 @@ -49,7 +49,7 @@
4.4 val nat_mod_add_eq = @{thm "mod_add1_eq"} RS sym;
4.5 val nat_mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
4.6 val nat_mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
4.7 -val int_mod_add_eq = @{thm "zmod_zadd1_eq"} RS sym;
4.8 +val int_mod_add_eq = @{thm "mod_add_eq"} RS sym;
4.9 val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;
4.10 val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;
4.11 val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
5.1 --- a/src/HOL/Divides.thy Wed Feb 18 13:39:05 2009 +0100
5.2 +++ b/src/HOL/Divides.thy Wed Feb 18 13:39:16 2009 +0100
5.3 @@ -173,7 +173,7 @@
5.4 qed
5.5
5.6 lemma dvd_imp_mod_0: "a dvd b \<Longrightarrow> b mod a = 0"
5.7 -by (unfold dvd_def, auto)
5.8 +by (rule dvd_eq_mod_eq_0[THEN iffD1])
5.9
5.10 lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b"
5.11 by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0)
6.1 --- a/src/HOL/Induct/Common_Patterns.thy Wed Feb 18 13:39:05 2009 +0100
6.2 +++ b/src/HOL/Induct/Common_Patterns.thy Wed Feb 18 13:39:16 2009 +0100
6.3 @@ -1,5 +1,4 @@
6.4 (* Title: HOL/Induct/Common_Patterns.thy
6.5 - ID: $Id$
6.6 Author: Makarius
6.7 *)
6.8
7.1 --- a/src/HOL/Int.thy Wed Feb 18 13:39:05 2009 +0100
7.2 +++ b/src/HOL/Int.thy Wed Feb 18 13:39:16 2009 +0100
7.3 @@ -1627,7 +1627,7 @@
7.4 context ring_1
7.5 begin
7.6
7.7 -lemma of_int_of_nat:
7.8 +lemma of_int_of_nat [nitpick_const_simp]:
7.9 "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
7.10 proof (cases "k < 0")
7.11 case True then have "0 \<le> - k" by simp
8.1 --- a/src/HOL/IntDiv.thy Wed Feb 18 13:39:05 2009 +0100
8.2 +++ b/src/HOL/IntDiv.thy Wed Feb 18 13:39:16 2009 +0100
8.3 @@ -377,6 +377,11 @@
8.4 apply (blast intro: divmod_rel_div_mod [THEN zminus1_lemma, THEN divmod_rel_mod])
8.5 done
8.6
8.7 +lemma zmod_zminus1_not_zero:
8.8 + fixes k l :: int
8.9 + shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
8.10 + unfolding zmod_zminus1_eq_if by auto
8.11 +
8.12 lemma zdiv_zminus2: "a div (-b) = (-a::int) div b"
8.13 by (cut_tac a = "-a" in zdiv_zminus_zminus, auto)
8.14
8.15 @@ -393,6 +398,11 @@
8.16 "a mod (-b::int) = (if a mod b = 0 then 0 else (a mod b) - b)"
8.17 by (simp add: zmod_zminus1_eq_if zmod_zminus2)
8.18
8.19 +lemma zmod_zminus2_not_zero:
8.20 + fixes k l :: int
8.21 + shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
8.22 + unfolding zmod_zminus2_eq_if by auto
8.23 +
8.24
8.25 subsection{*Division of a Number by Itself*}
8.26
8.27 @@ -441,9 +451,6 @@
8.28 lemma zmod_zero [simp]: "(0::int) mod b = 0"
8.29 by (simp add: mod_def divmod_def)
8.30
8.31 -lemma zdiv_minus1: "(0::int) < b ==> -1 div b = -1"
8.32 -by (simp add: div_def divmod_def)
8.33 -
8.34 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
8.35 by (simp add: mod_def divmod_def)
8.36
8.37 @@ -719,18 +726,6 @@
8.38 apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_mod])
8.39 done
8.40
8.41 -lemma zmod_zmult1_eq': "(a*b) mod (c::int) = ((a mod c) * b) mod c"
8.42 -apply (rule trans)
8.43 -apply (rule_tac s = "b*a mod c" in trans)
8.44 -apply (rule_tac [2] zmod_zmult1_eq)
8.45 -apply (simp_all add: mult_commute)
8.46 -done
8.47 -
8.48 -lemma zmod_zmult_distrib: "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c"
8.49 -apply (rule zmod_zmult1_eq' [THEN trans])
8.50 -apply (rule zmod_zmult1_eq)
8.51 -done
8.52 -
8.53 lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
8.54 by (simp add: zdiv_zmult1_eq)
8.55
8.56 @@ -739,11 +734,6 @@
8.57 apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
8.58 done
8.59
8.60 -lemma zmod_zmod_trivial: "(a mod b) mod b = a mod (b::int)"
8.61 -apply (case_tac "b = 0", simp)
8.62 -apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
8.63 -done
8.64 -
8.65 text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
8.66
8.67 lemma zadd1_lemma:
8.68 @@ -758,11 +748,6 @@
8.69 apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_div)
8.70 done
8.71
8.72 -lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
8.73 -apply (case_tac "c = 0", simp)
8.74 -apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_mod)
8.75 -done
8.76 -
8.77 instance int :: ring_div
8.78 proof
8.79 fix a b c :: int
8.80 @@ -961,7 +946,7 @@
8.81 P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
8.82 apply (rule iffI, clarify)
8.83 apply (erule_tac P="P ?x ?y" in rev_mp)
8.84 - apply (subst zmod_zadd1_eq)
8.85 + apply (subst mod_add_eq)
8.86 apply (subst zdiv_zadd1_eq)
8.87 apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
8.88 txt{*converse direction*}
8.89 @@ -974,7 +959,7 @@
8.90 P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
8.91 apply (rule iffI, clarify)
8.92 apply (erule_tac P="P ?x ?y" in rev_mp)
8.93 - apply (subst zmod_zadd1_eq)
8.94 + apply (subst mod_add_eq)
8.95 apply (subst zdiv_zadd1_eq)
8.96 apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
8.97 txt{*converse direction*}
8.98 @@ -1047,11 +1032,6 @@
8.99 simp)
8.100 done
8.101
8.102 -(*Not clear why this must be proved separately; probably number_of causes
8.103 - simplification problems*)
8.104 -lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)"
8.105 -by auto
8.106 -
8.107 lemma zdiv_number_of_Bit0 [simp]:
8.108 "number_of (Int.Bit0 v) div number_of (Int.Bit0 w) =
8.109 number_of v div (number_of w :: int)"
8.110 @@ -1078,7 +1058,7 @@
8.111 apply (rule_tac [2] mult_left_mono)
8.112 apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq
8.113 pos_mod_bound)
8.114 -apply (subst zmod_zadd1_eq)
8.115 +apply (subst mod_add_eq)
8.116 apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
8.117 apply (rule mod_pos_pos_trivial)
8.118 apply (auto simp add: mod_pos_pos_trivial ring_distribs)
8.119 @@ -1101,7 +1081,7 @@
8.120 (2::int) * (number_of v mod number_of w)"
8.121 apply (simp only: number_of_eq numeral_simps)
8.122 apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
8.123 - not_0_le_lemma neg_zmod_mult_2 add_ac)
8.124 + neg_zmod_mult_2 add_ac)
8.125 done
8.126
8.127 lemma zmod_number_of_Bit1 [simp]:
8.128 @@ -1111,7 +1091,7 @@
8.129 else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
8.130 apply (simp only: number_of_eq numeral_simps)
8.131 apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
8.132 - not_0_le_lemma neg_zmod_mult_2 add_ac)
8.133 + neg_zmod_mult_2 add_ac)
8.134 done
8.135
8.136
8.137 @@ -1121,7 +1101,7 @@
8.138 apply (subgoal_tac "a div b \<le> -1", force)
8.139 apply (rule order_trans)
8.140 apply (rule_tac a' = "-1" in zdiv_mono1)
8.141 -apply (auto simp add: zdiv_minus1)
8.142 +apply (auto simp add: div_eq_minus1)
8.143 done
8.144
8.145 lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
8.146 @@ -1167,23 +1147,23 @@
8.147 lemma zdvd_1_left: "1 dvd (m::int)"
8.148 by (rule one_dvd) (* already declared [simp] *)
8.149
8.150 -lemma zdvd_refl [simp]: "m dvd (m::int)"
8.151 - by (rule dvd_refl) (* TODO: declare generic dvd_refl [simp] *)
8.152 +lemma zdvd_refl: "m dvd (m::int)"
8.153 + by (rule dvd_refl) (* already declared [simp] *)
8.154
8.155 lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
8.156 by (rule dvd_trans)
8.157
8.158 -lemma zdvd_zminus_iff[simp]: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
8.159 - by (rule dvd_minus_iff)
8.160 +lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
8.161 + by (rule dvd_minus_iff) (* already declared [simp] *)
8.162
8.163 -lemma zdvd_zminus2_iff[simp]: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
8.164 - by (rule minus_dvd_iff)
8.165 +lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
8.166 + by (rule minus_dvd_iff) (* already declared [simp] *)
8.167
8.168 -lemma zdvd_abs1[simp]: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
8.169 - by (cases "i > 0") (simp_all add: zdvd_zminus2_iff)
8.170 +lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
8.171 + by (rule abs_dvd_iff) (* already declared [simp] *)
8.172
8.173 -lemma zdvd_abs2[simp]: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)"
8.174 - by (cases "j > 0") (simp_all add: zdvd_zminus_iff)
8.175 +lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)"
8.176 + by (rule dvd_abs_iff) (* already declared [simp] *)
8.177
8.178 lemma zdvd_anti_sym:
8.179 "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
8.180 @@ -1369,7 +1349,7 @@
8.181 apply (induct "y", auto)
8.182 apply (rule zmod_zmult1_eq [THEN trans])
8.183 apply (simp (no_asm_simp))
8.184 -apply (rule zmod_zmult_distrib [symmetric])
8.185 +apply (rule mod_mult_eq [symmetric])
8.186 done
8.187
8.188 lemma zdiv_int: "int (a div b) = (int a) div (int b)"
8.189 @@ -1410,7 +1390,7 @@
8.190 IntDiv.zmod_zadd_left_eq [symmetric]
8.191 IntDiv.zmod_zadd_right_eq [symmetric]
8.192 IntDiv.zmod_zmult1_eq [symmetric]
8.193 - IntDiv.zmod_zmult1_eq' [symmetric]
8.194 + mod_mult_left_eq [symmetric]
8.195 IntDiv.zpower_zmod
8.196 zminus_zmod zdiff_zmod_left zdiff_zmod_right
8.197
8.198 @@ -1523,6 +1503,40 @@
8.199 thus ?lhs by simp
8.200 qed
8.201
8.202 +
8.203 +subsection {* Code generation *}
8.204 +
8.205 +definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
8.206 + "pdivmod k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"
8.207 +
8.208 +lemma pdivmod_posDivAlg [code]:
8.209 + "pdivmod k l = (if l = 0 then (0, \<bar>k\<bar>) else posDivAlg \<bar>k\<bar> \<bar>l\<bar>)"
8.210 +by (subst posDivAlg_div_mod) (simp_all add: pdivmod_def)
8.211 +
8.212 +lemma divmod_pdivmod: "divmod k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
8.213 + apsnd ((op *) (sgn l)) (if 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0
8.214 + then pdivmod k l
8.215 + else (let (r, s) = pdivmod k l in
8.216 + if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
8.217 +proof -
8.218 + have aux: "\<And>q::int. - k = l * q \<longleftrightarrow> k = l * - q" by auto
8.219 + show ?thesis
8.220 + by (simp add: divmod_mod_div pdivmod_def)
8.221 + (auto simp add: aux not_less not_le zdiv_zminus1_eq_if
8.222 + zmod_zminus1_eq_if zdiv_zminus2_eq_if zmod_zminus2_eq_if)
8.223 +qed
8.224 +
8.225 +lemma divmod_code [code]: "divmod k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
8.226 + apsnd ((op *) (sgn l)) (if sgn k = sgn l
8.227 + then pdivmod k l
8.228 + else (let (r, s) = pdivmod k l in
8.229 + if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
8.230 +proof -
8.231 + have "k \<noteq> 0 \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0 \<longleftrightarrow> sgn k = sgn l"
8.232 + by (auto simp add: not_less sgn_if)
8.233 + then show ?thesis by (simp add: divmod_pdivmod)
8.234 +qed
8.235 +
8.236 code_modulename SML
8.237 IntDiv Integer
8.238
9.1 --- a/src/HOL/Library/Code_Integer.thy Wed Feb 18 13:39:05 2009 +0100
9.2 +++ b/src/HOL/Library/Code_Integer.thy Wed Feb 18 13:39:16 2009 +0100
9.3 @@ -1,5 +1,4 @@
9.4 (* Title: HOL/Library/Code_Integer.thy
9.5 - ID: $Id$
9.6 Author: Florian Haftmann, TU Muenchen
9.7 *)
9.8
9.9 @@ -72,6 +71,11 @@
9.10 (OCaml "Big'_int.mult'_big'_int")
9.11 (Haskell infixl 7 "*")
9.12
9.13 +code_const pdivmod
9.14 + (SML "(fn k => fn l =>/ IntInf.divMod/ (IntInf.abs k,/ IntInf.abs l))")
9.15 + (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))")
9.16 + (Haskell "(\\k l ->/ divMod/ (abs k)/ (abs l))")
9.17 +
9.18 code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
9.19 (SML "!((_ : IntInf.int) = _)")
9.20 (OCaml "Big'_int.eq'_big'_int")
10.1 --- a/src/HOL/Library/Efficient_Nat.thy Wed Feb 18 13:39:05 2009 +0100
10.2 +++ b/src/HOL/Library/Efficient_Nat.thy Wed Feb 18 13:39:16 2009 +0100
10.3 @@ -105,10 +105,16 @@
10.4 This can be accomplished by applying the following transformation rules:
10.5 *}
10.6
10.7 -lemma Suc_if_eq: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
10.8 +lemma Suc_if_eq': "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
10.9 f n = (if n = 0 then g else h (n - 1))"
10.10 by (cases n) simp_all
10.11
10.12 +lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow>
10.13 + f n \<equiv> if n = 0 then g else h (n - 1)"
10.14 + by (rule eq_reflection, rule Suc_if_eq')
10.15 + (rule meta_eq_to_obj_eq, assumption,
10.16 + rule meta_eq_to_obj_eq, assumption)
10.17 +
10.18 lemma Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
10.19 by (cases n) simp_all
10.20
10.21 @@ -123,14 +129,14 @@
10.22 setup {*
10.23 let
10.24
10.25 -fun remove_suc thy thms =
10.26 +fun gen_remove_suc Suc_if_eq dest_judgement thy thms =
10.27 let
10.28 val vname = Name.variant (map fst
10.29 - (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
10.30 + (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "n";
10.31 val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
10.32 fun lhs_of th = snd (Thm.dest_comb
10.33 - (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
10.34 - fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
10.35 + (fst (Thm.dest_comb (dest_judgement (cprop_of th)))));
10.36 + fun rhs_of th = snd (Thm.dest_comb (dest_judgement (cprop_of th)));
10.37 fun find_vars ct = (case term_of ct of
10.38 (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
10.39 | _ $ _ =>
10.40 @@ -150,7 +156,7 @@
10.41 (Drule.instantiate'
10.42 [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
10.43 SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
10.44 - @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
10.45 + Suc_if_eq)) (Thm.forall_intr cv' th)
10.46 in
10.47 case map_filter (fn th'' =>
10.48 SOME (th'', singleton
10.49 @@ -161,20 +167,26 @@
10.50 let val (ths1, ths2) = split_list thps
10.51 in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
10.52 end
10.53 - in case get_first mk_thms eqs of
10.54 - NONE => thms
10.55 - | SOME x => remove_suc thy x
10.56 + in get_first mk_thms eqs end;
10.57 +
10.58 +fun gen_eqn_suc_preproc Suc_if_eq dest_judgement dest_lhs thy thms =
10.59 + let
10.60 + val dest = dest_lhs o prop_of;
10.61 + val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
10.62 + in
10.63 + if forall (can dest) thms andalso exists (contains_suc o dest) thms
10.64 + then perhaps_loop (gen_remove_suc Suc_if_eq dest_judgement thy) thms
10.65 + else NONE
10.66 end;
10.67
10.68 -fun eqn_suc_preproc thy ths =
10.69 - let
10.70 - val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
10.71 - val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
10.72 - in
10.73 - if forall (can dest) ths andalso
10.74 - exists (contains_suc o dest) ths
10.75 - then remove_suc thy ths else ths
10.76 - end;
10.77 +fun eqn_suc_preproc thy = map fst
10.78 + #> gen_eqn_suc_preproc
10.79 + @{thm Suc_if_eq} I (fst o Logic.dest_equals) thy
10.80 + #> (Option.map o map) (Code_Unit.mk_eqn thy);
10.81 +
10.82 +fun eqn_suc_preproc' thy thms = gen_eqn_suc_preproc
10.83 + @{thm Suc_if_eq'} (snd o Thm.dest_comb) (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) thy thms
10.84 + |> the_default thms;
10.85
10.86 fun remove_suc_clause thy thms =
10.87 let
10.88 @@ -215,27 +227,11 @@
10.89 (map_filter (try dest) (concl_of th :: prems_of th))) ths
10.90 then remove_suc_clause thy ths else ths
10.91 end;
10.92 -
10.93 -fun lift f thy eqns1 =
10.94 - let
10.95 - val eqns2 = burrow_fst Drule.zero_var_indexes_list eqns1;
10.96 - val thms3 = try (map fst
10.97 - #> map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
10.98 - #> f thy
10.99 - #> map (fn thm => thm RS @{thm eq_reflection})
10.100 - #> map (Conv.fconv_rule Drule.beta_eta_conversion)) eqns2;
10.101 - val thms4 = Option.map Drule.zero_var_indexes_list thms3;
10.102 - in case thms4
10.103 - of NONE => NONE
10.104 - | SOME thms4 => if Thm.eq_thms (map fst eqns2, thms4)
10.105 - then NONE else SOME (map (apfst (AxClass.overload thy) o Code_Unit.mk_eqn thy) thms4)
10.106 - end
10.107 -
10.108 in
10.109
10.110 - Codegen.add_preprocessor eqn_suc_preproc
10.111 + Codegen.add_preprocessor eqn_suc_preproc'
10.112 #> Codegen.add_preprocessor clause_suc_preproc
10.113 - #> Code.add_functrans ("eqn_Suc", lift eqn_suc_preproc)
10.114 + #> Code.add_functrans ("eqn_Suc", eqn_suc_preproc)
10.115
10.116 end;
10.117 *}
11.1 --- a/src/HOL/Library/Enum.thy Wed Feb 18 13:39:05 2009 +0100
11.2 +++ b/src/HOL/Library/Enum.thy Wed Feb 18 13:39:16 2009 +0100
11.3 @@ -1,5 +1,4 @@
11.4 (* Title: HOL/Library/Enum.thy
11.5 - ID: $Id$
11.6 Author: Florian Haftmann, TU Muenchen
11.7 *)
11.8
12.1 --- a/src/HOL/NumberTheory/Chinese.thy Wed Feb 18 13:39:05 2009 +0100
12.2 +++ b/src/HOL/NumberTheory/Chinese.thy Wed Feb 18 13:39:16 2009 +0100
12.3 @@ -101,7 +101,7 @@
12.4 apply (induct l)
12.5 apply auto
12.6 apply (rule trans)
12.7 - apply (rule zmod_zadd1_eq)
12.8 + apply (rule mod_add_eq)
12.9 apply simp
12.10 apply (rule zmod_zadd_right_eq [symmetric])
12.11 done
12.12 @@ -237,10 +237,10 @@
12.13 apply (unfold lincong_sol_def)
12.14 apply safe
12.15 apply (tactic {* stac (thm "zcong_zmod") 3 *})
12.16 - apply (tactic {* stac (thm "zmod_zmult_distrib") 3 *})
12.17 + apply (tactic {* stac (thm "mod_mult_eq") 3 *})
12.18 apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *})
12.19 apply (tactic {* stac (thm "x_sol_lin") 5 *})
12.20 - apply (tactic {* stac (thm "zmod_zmult_distrib" RS sym) 7 *})
12.21 + apply (tactic {* stac (thm "mod_mult_eq" RS sym) 7 *})
12.22 apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *})
12.23 apply (subgoal_tac [7]
12.24 "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
13.1 --- a/src/HOL/NumberTheory/IntPrimes.thy Wed Feb 18 13:39:05 2009 +0100
13.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy Wed Feb 18 13:39:16 2009 +0100
13.3 @@ -88,7 +88,7 @@
13.4
13.5 lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k) n = zgcd m n"
13.6 apply (rule zgcd_eq [THEN trans])
13.7 - apply (simp add: zmod_zadd1_eq)
13.8 + apply (simp add: mod_add_eq)
13.9 apply (rule zgcd_eq [symmetric])
13.10 done
13.11
14.1 --- a/src/HOL/NumberTheory/Residues.thy Wed Feb 18 13:39:05 2009 +0100
14.2 +++ b/src/HOL/NumberTheory/Residues.thy Wed Feb 18 13:39:16 2009 +0100
14.3 @@ -53,7 +53,7 @@
14.4 lemma StandardRes_prop4: "2 < m
14.5 ==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)"
14.6 by (auto simp add: StandardRes_def zcong_zmod_eq
14.7 - zmod_zmult_distrib [of x y m])
14.8 + mod_mult_eq [of x y m])
14.9
14.10 lemma StandardRes_lbound: "0 < p ==> 0 \<le> StandardRes p x"
14.11 by (auto simp add: StandardRes_def pos_mod_sign)
15.1 --- a/src/HOL/Rational.thy Wed Feb 18 13:39:05 2009 +0100
15.2 +++ b/src/HOL/Rational.thy Wed Feb 18 13:39:16 2009 +0100
15.3 @@ -886,14 +886,13 @@
15.4 finally show ?thesis using assms by simp
15.5 qed
15.6
15.7 -lemma rat_less_eq_code [code]:
15.8 - "Fract a b \<le> Fract c d \<longleftrightarrow> (if b = 0
15.9 - then sgn c * sgn d \<ge> 0
15.10 - else if d = 0
15.11 - then sgn a * sgn b \<le> 0
15.12 - else a * \<bar>d\<bar> * sgn b \<le> c * \<bar>b\<bar> * sgn d)"
15.13 -by (auto simp add: sgn_times mult_le_0_iff zero_le_mult_iff le_rat' eq_rat simp del: le_rat)
15.14 - (auto simp add: sgn_times sgn_0_0 le_less sgn_1_pos [symmetric] sgn_1_neg [symmetric])
15.15 +lemma (in ordered_idom) sgn_greater [simp]:
15.16 + "0 < sgn a \<longleftrightarrow> 0 < a"
15.17 + unfolding sgn_if by auto
15.18 +
15.19 +lemma (in ordered_idom) sgn_less [simp]:
15.20 + "sgn a < 0 \<longleftrightarrow> a < 0"
15.21 + unfolding sgn_if by auto
15.22
15.23 lemma rat_le_eq_code [code]:
15.24 "Fract a b < Fract c d \<longleftrightarrow> (if b = 0
15.25 @@ -901,9 +900,17 @@
15.26 else if d = 0
15.27 then sgn a * sgn b < 0
15.28 else a * \<bar>d\<bar> * sgn b < c * \<bar>b\<bar> * sgn d)"
15.29 -by (auto simp add: sgn_times mult_less_0_iff zero_less_mult_iff less_rat' eq_rat simp del: less_rat)
15.30 - (auto simp add: sgn_times sgn_0_0 sgn_1_pos [symmetric] sgn_1_neg [symmetric],
15.31 - auto simp add: sgn_1_pos)
15.32 + by (auto simp add: sgn_times mult_less_0_iff zero_less_mult_iff less_rat' eq_rat simp del: less_rat)
15.33 +
15.34 +lemma rat_less_eq_code [code]:
15.35 + "Fract a b \<le> Fract c d \<longleftrightarrow> (if b = 0
15.36 + then sgn c * sgn d \<ge> 0
15.37 + else if d = 0
15.38 + then sgn a * sgn b \<le> 0
15.39 + else a * \<bar>d\<bar> * sgn b \<le> c * \<bar>b\<bar> * sgn d)"
15.40 + by (auto simp add: sgn_times mult_le_0_iff zero_le_mult_iff le_rat' eq_rat simp del: le_rat)
15.41 + (auto simp add: le_less not_less sgn_0_0)
15.42 +
15.43
15.44 lemma rat_plus_code [code]:
15.45 "Fract a b + Fract c d = (if b = 0
16.1 --- a/src/HOL/Ring_and_Field.thy Wed Feb 18 13:39:05 2009 +0100
16.2 +++ b/src/HOL/Ring_and_Field.thy Wed Feb 18 13:39:16 2009 +0100
16.3 @@ -1,5 +1,4 @@
16.4 (* Title: HOL/Ring_and_Field.thy
16.5 - ID: $Id$
16.6 Author: Gertrud Bauer, Steven Obua, Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel,
16.7 with contributions by Jeremy Avigad
16.8 *)
16.9 @@ -1078,6 +1077,14 @@
16.10 "sgn a = - 1 \<longleftrightarrow> a < 0"
16.11 unfolding sgn_if by (auto simp add: equal_neg_zero)
16.12
16.13 +lemma sgn_pos [simp]:
16.14 + "0 < a \<Longrightarrow> sgn a = 1"
16.15 +unfolding sgn_1_pos .
16.16 +
16.17 +lemma sgn_neg [simp]:
16.18 + "a < 0 \<Longrightarrow> sgn a = - 1"
16.19 +unfolding sgn_1_neg .
16.20 +
16.21 lemma sgn_times:
16.22 "sgn (a * b) = sgn a * sgn b"
16.23 by (auto simp add: sgn_if zero_less_mult_iff)
16.24 @@ -1085,32 +1092,19 @@
16.25 lemma abs_sgn: "abs k = k * sgn k"
16.26 unfolding sgn_if abs_if by auto
16.27
16.28 -(* The int instances are proved, these generic ones are tedious to prove here.
16.29 -And not very useful, as int seems to be the only instance.
16.30 -If needed, they should be proved later, when metis is available.
16.31 -lemma dvd_abs[simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
16.32 -proof-
16.33 - have "\<forall>k.\<exists>ka. - (m * k) = m * ka"
16.34 - by(simp add: mult_minus_right[symmetric] del: mult_minus_right)
16.35 - moreover
16.36 - have "\<forall>k.\<exists>ka. m * k = - (m * ka)"
16.37 - by(auto intro!: minus_minus[symmetric]
16.38 - simp add: mult_minus_right[symmetric] simp del: mult_minus_right)
16.39 - ultimately show ?thesis by (auto simp: abs_if dvd_def)
16.40 -qed
16.41 -
16.42 -lemma dvd_abs2[simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
16.43 -proof-
16.44 - have "\<forall>k.\<exists>ka. - (m * k) = m * ka"
16.45 - by(simp add: mult_minus_right[symmetric] del: mult_minus_right)
16.46 - moreover
16.47 - have "\<forall>k.\<exists>ka. - (m * ka) = m * k"
16.48 - by(auto intro!: minus_minus
16.49 - simp add: mult_minus_right[symmetric] simp del: mult_minus_right)
16.50 - ultimately show ?thesis
16.51 - by (auto simp add:abs_if dvd_def minus_equation_iff[of k])
16.52 -qed
16.53 -*)
16.54 +lemma sgn_greater [simp]:
16.55 + "0 < sgn a \<longleftrightarrow> 0 < a"
16.56 + unfolding sgn_if by auto
16.57 +
16.58 +lemma sgn_less [simp]:
16.59 + "sgn a < 0 \<longleftrightarrow> a < 0"
16.60 + unfolding sgn_if by auto
16.61 +
16.62 +lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
16.63 + by (simp add: abs_if)
16.64 +
16.65 +lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
16.66 + by (simp add: abs_if)
16.67
16.68 end
16.69
17.1 --- a/src/HOL/Tools/Qelim/generated_cooper.ML Wed Feb 18 13:39:05 2009 +0100
17.2 +++ b/src/HOL/Tools/Qelim/generated_cooper.ML Wed Feb 18 13:39:16 2009 +0100
17.3 @@ -15,13 +15,13 @@
17.4
17.5 fun divmod n m = (if eqop eq_nat m 0 then (0, n) else IntInf.divMod (n, m));
17.6
17.7 -fun snd (a, y) = y;
17.8 +fun snd (a, b) = b;
17.9
17.10 fun mod_nat m n = snd (divmod m n);
17.11
17.12 fun gcd m n = (if eqop eq_nat n 0 then m else gcd n (mod_nat m n));
17.13
17.14 -fun fst (y, b) = y;
17.15 +fun fst (a, b) = a;
17.16
17.17 fun div_nat m n = fst (divmod m n);
17.18
17.19 @@ -48,7 +48,7 @@
17.20 fun map f [] = []
17.21 | map f (x :: xs) = f x :: map f xs;
17.22
17.23 -fun append [] y = y
17.24 +fun append [] ys = ys
17.25 | append (x :: xs) ys = x :: append xs ys;
17.26
17.27 fun disjuncts (Or (p, q)) = append (disjuncts p) (disjuncts q)
17.28 @@ -105,53 +105,53 @@
17.29 (Le num) = f4 num
17.30 | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19
17.31 (Lt num) = f3 num
17.32 - | fm_case f1 y f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 F
17.33 - = y
17.34 - | fm_case y f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 T
17.35 - = y;
17.36 + | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 F
17.37 + = f2
17.38 + | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 T
17.39 + = f1;
17.40
17.41 -fun eq_num (Mul (cb, dc)) (Sub (ae, be)) = false
17.42 - | eq_num (Mul (cb, dc)) (Add (ae, be)) = false
17.43 - | eq_num (Sub (cc, dc)) (Add (ae, be)) = false
17.44 - | eq_num (Mul (bd, cc)) (Neg ae) = false
17.45 - | eq_num (Sub (be, cc)) (Neg ae) = false
17.46 - | eq_num (Add (be, cc)) (Neg ae) = false
17.47 - | eq_num (Mul (db, ea)) (Cn (ac, bd, cc)) = false
17.48 - | eq_num (Sub (dc, ea)) (Cn (ac, bd, cc)) = false
17.49 - | eq_num (Add (dc, ea)) (Cn (ac, bd, cc)) = false
17.50 - | eq_num (Neg dc) (Cn (ac, bd, cc)) = false
17.51 - | eq_num (Mul (bd, cc)) (Bound ac) = false
17.52 - | eq_num (Sub (be, cc)) (Bound ac) = false
17.53 - | eq_num (Add (be, cc)) (Bound ac) = false
17.54 - | eq_num (Neg be) (Bound ac) = false
17.55 - | eq_num (Cn (bc, cb, dc)) (Bound ac) = false
17.56 - | eq_num (Mul (bd, cc)) (C ad) = false
17.57 - | eq_num (Sub (be, cc)) (C ad) = false
17.58 - | eq_num (Add (be, cc)) (C ad) = false
17.59 - | eq_num (Neg be) (C ad) = false
17.60 - | eq_num (Cn (bc, cb, dc)) (C ad) = false
17.61 - | eq_num (Bound bc) (C ad) = false
17.62 - | eq_num (Sub (ab, bb)) (Mul (c, da)) = false
17.63 - | eq_num (Add (ab, bb)) (Mul (c, da)) = false
17.64 - | eq_num (Add (ab, bb)) (Sub (ca, da)) = false
17.65 - | eq_num (Neg ab) (Mul (ba, ca)) = false
17.66 - | eq_num (Neg ab) (Sub (bb, ca)) = false
17.67 - | eq_num (Neg ab) (Add (bb, ca)) = false
17.68 - | eq_num (Cn (a, ba, ca)) (Mul (d, e)) = false
17.69 - | eq_num (Cn (a, ba, ca)) (Sub (da, e)) = false
17.70 - | eq_num (Cn (a, ba, ca)) (Add (da, e)) = false
17.71 - | eq_num (Cn (a, ba, ca)) (Neg da) = false
17.72 - | eq_num (Bound a) (Mul (ba, ca)) = false
17.73 - | eq_num (Bound a) (Sub (bb, ca)) = false
17.74 - | eq_num (Bound a) (Add (bb, ca)) = false
17.75 - | eq_num (Bound a) (Neg bb) = false
17.76 - | eq_num (Bound a) (Cn (b, c, da)) = false
17.77 - | eq_num (C aa) (Mul (ba, ca)) = false
17.78 - | eq_num (C aa) (Sub (bb, ca)) = false
17.79 - | eq_num (C aa) (Add (bb, ca)) = false
17.80 - | eq_num (C aa) (Neg bb) = false
17.81 - | eq_num (C aa) (Cn (b, c, da)) = false
17.82 - | eq_num (C aa) (Bound b) = false
17.83 +fun eq_num (Mul (c, d)) (Sub (a, b)) = false
17.84 + | eq_num (Mul (c, d)) (Add (a, b)) = false
17.85 + | eq_num (Sub (c, d)) (Add (a, b)) = false
17.86 + | eq_num (Mul (b, c)) (Neg a) = false
17.87 + | eq_num (Sub (b, c)) (Neg a) = false
17.88 + | eq_num (Add (b, c)) (Neg a) = false
17.89 + | eq_num (Mul (d, e)) (Cn (a, b, c)) = false
17.90 + | eq_num (Sub (d, e)) (Cn (a, b, c)) = false
17.91 + | eq_num (Add (d, e)) (Cn (a, b, c)) = false
17.92 + | eq_num (Neg d) (Cn (a, b, c)) = false
17.93 + | eq_num (Mul (b, c)) (Bound a) = false
17.94 + | eq_num (Sub (b, c)) (Bound a) = false
17.95 + | eq_num (Add (b, c)) (Bound a) = false
17.96 + | eq_num (Neg b) (Bound a) = false
17.97 + | eq_num (Cn (b, c, d)) (Bound a) = false
17.98 + | eq_num (Mul (b, c)) (C a) = false
17.99 + | eq_num (Sub (b, c)) (C a) = false
17.100 + | eq_num (Add (b, c)) (C a) = false
17.101 + | eq_num (Neg b) (C a) = false
17.102 + | eq_num (Cn (b, c, d)) (C a) = false
17.103 + | eq_num (Bound b) (C a) = false
17.104 + | eq_num (Sub (a, b)) (Mul (c, d)) = false
17.105 + | eq_num (Add (a, b)) (Mul (c, d)) = false
17.106 + | eq_num (Add (a, b)) (Sub (c, d)) = false
17.107 + | eq_num (Neg a) (Mul (b, c)) = false
17.108 + | eq_num (Neg a) (Sub (b, c)) = false
17.109 + | eq_num (Neg a) (Add (b, c)) = false
17.110 + | eq_num (Cn (a, b, c)) (Mul (d, e)) = false
17.111 + | eq_num (Cn (a, b, c)) (Sub (d, e)) = false
17.112 + | eq_num (Cn (a, b, c)) (Add (d, e)) = false
17.113 + | eq_num (Cn (a, b, c)) (Neg d) = false
17.114 + | eq_num (Bound a) (Mul (b, c)) = false
17.115 + | eq_num (Bound a) (Sub (b, c)) = false
17.116 + | eq_num (Bound a) (Add (b, c)) = false
17.117 + | eq_num (Bound a) (Neg b) = false
17.118 + | eq_num (Bound a) (Cn (b, c, d)) = false
17.119 + | eq_num (C a) (Mul (b, c)) = false
17.120 + | eq_num (C a) (Sub (b, c)) = false
17.121 + | eq_num (C a) (Add (b, c)) = false
17.122 + | eq_num (C a) (Neg b) = false
17.123 + | eq_num (C a) (Cn (b, c, d)) = false
17.124 + | eq_num (C a) (Bound b) = false
17.125 | eq_num (Mul (inta, num)) (Mul (int', num')) =
17.126 ((inta : IntInf.int) = int') andalso eq_num num num'
17.127 | eq_num (Sub (num1, num2)) (Sub (num1', num2')) =
17.128 @@ -165,347 +165,347 @@
17.129 | eq_num (Bound nat) (Bound nat') = ((nat : IntInf.int) = nat')
17.130 | eq_num (C inta) (C int') = ((inta : IntInf.int) = int');
17.131
17.132 -fun eq_fm (NClosed bd) (Closed ad) = false
17.133 - | eq_fm (NClosed bd) (A af) = false
17.134 - | eq_fm (Closed bd) (A af) = false
17.135 - | eq_fm (NClosed bd) (E af) = false
17.136 - | eq_fm (Closed bd) (E af) = false
17.137 - | eq_fm (A bf) (E af) = false
17.138 - | eq_fm (NClosed cd) (Iff (af, bf)) = false
17.139 - | eq_fm (Closed cd) (Iff (af, bf)) = false
17.140 - | eq_fm (A cf) (Iff (af, bf)) = false
17.141 - | eq_fm (E cf) (Iff (af, bf)) = false
17.142 - | eq_fm (NClosed cd) (Imp (af, bf)) = false
17.143 - | eq_fm (Closed cd) (Imp (af, bf)) = false
17.144 - | eq_fm (A cf) (Imp (af, bf)) = false
17.145 - | eq_fm (E cf) (Imp (af, bf)) = false
17.146 - | eq_fm (Iff (cf, db)) (Imp (af, bf)) = false
17.147 - | eq_fm (NClosed cd) (Or (af, bf)) = false
17.148 - | eq_fm (Closed cd) (Or (af, bf)) = false
17.149 - | eq_fm (A cf) (Or (af, bf)) = false
17.150 - | eq_fm (E cf) (Or (af, bf)) = false
17.151 - | eq_fm (Iff (cf, db)) (Or (af, bf)) = false
17.152 - | eq_fm (Imp (cf, db)) (Or (af, bf)) = false
17.153 - | eq_fm (NClosed cd) (And (af, bf)) = false
17.154 - | eq_fm (Closed cd) (And (af, bf)) = false
17.155 - | eq_fm (A cf) (And (af, bf)) = false
17.156 - | eq_fm (E cf) (And (af, bf)) = false
17.157 - | eq_fm (Iff (cf, db)) (And (af, bf)) = false
17.158 - | eq_fm (Imp (cf, db)) (And (af, bf)) = false
17.159 - | eq_fm (Or (cf, db)) (And (af, bf)) = false
17.160 - | eq_fm (NClosed bd) (Not af) = false
17.161 - | eq_fm (Closed bd) (Not af) = false
17.162 - | eq_fm (A bf) (Not af) = false
17.163 - | eq_fm (E bf) (Not af) = false
17.164 - | eq_fm (Iff (bf, cf)) (Not af) = false
17.165 - | eq_fm (Imp (bf, cf)) (Not af) = false
17.166 - | eq_fm (Or (bf, cf)) (Not af) = false
17.167 - | eq_fm (And (bf, cf)) (Not af) = false
17.168 - | eq_fm (NClosed cd) (NDvd (ae, bg)) = false
17.169 - | eq_fm (Closed cd) (NDvd (ae, bg)) = false
17.170 - | eq_fm (A cf) (NDvd (ae, bg)) = false
17.171 - | eq_fm (E cf) (NDvd (ae, bg)) = false
17.172 - | eq_fm (Iff (cf, db)) (NDvd (ae, bg)) = false
17.173 - | eq_fm (Imp (cf, db)) (NDvd (ae, bg)) = false
17.174 - | eq_fm (Or (cf, db)) (NDvd (ae, bg)) = false
17.175 - | eq_fm (And (cf, db)) (NDvd (ae, bg)) = false
17.176 - | eq_fm (Not cf) (NDvd (ae, bg)) = false
17.177 - | eq_fm (NClosed cd) (Dvd (ae, bg)) = false
17.178 - | eq_fm (Closed cd) (Dvd (ae, bg)) = false
17.179 - | eq_fm (A cf) (Dvd (ae, bg)) = false
17.180 - | eq_fm (E cf) (Dvd (ae, bg)) = false
17.181 - | eq_fm (Iff (cf, db)) (Dvd (ae, bg)) = false
17.182 - | eq_fm (Imp (cf, db)) (Dvd (ae, bg)) = false
17.183 - | eq_fm (Or (cf, db)) (Dvd (ae, bg)) = false
17.184 - | eq_fm (And (cf, db)) (Dvd (ae, bg)) = false
17.185 - | eq_fm (Not cf) (Dvd (ae, bg)) = false
17.186 - | eq_fm (NDvd (ce, dc)) (Dvd (ae, bg)) = false
17.187 - | eq_fm (NClosed bd) (NEq ag) = false
17.188 - | eq_fm (Closed bd) (NEq ag) = false
17.189 - | eq_fm (A bf) (NEq ag) = false
17.190 - | eq_fm (E bf) (NEq ag) = false
17.191 - | eq_fm (Iff (bf, cf)) (NEq ag) = false
17.192 - | eq_fm (Imp (bf, cf)) (NEq ag) = false
17.193 - | eq_fm (Or (bf, cf)) (NEq ag) = false
17.194 - | eq_fm (And (bf, cf)) (NEq ag) = false
17.195 - | eq_fm (Not bf) (NEq ag) = false
17.196 - | eq_fm (NDvd (be, cg)) (NEq ag) = false
17.197 - | eq_fm (Dvd (be, cg)) (NEq ag) = false
17.198 - | eq_fm (NClosed bd) (Eq ag) = false
17.199 - | eq_fm (Closed bd) (Eq ag) = false
17.200 - | eq_fm (A bf) (Eq ag) = false
17.201 - | eq_fm (E bf) (Eq ag) = false
17.202 - | eq_fm (Iff (bf, cf)) (Eq ag) = false
17.203 - | eq_fm (Imp (bf, cf)) (Eq ag) = false
17.204 - | eq_fm (Or (bf, cf)) (Eq ag) = false
17.205 - | eq_fm (And (bf, cf)) (Eq ag) = false
17.206 - | eq_fm (Not bf) (Eq ag) = false
17.207 - | eq_fm (NDvd (be, cg)) (Eq ag) = false
17.208 - | eq_fm (Dvd (be, cg)) (Eq ag) = false
17.209 - | eq_fm (NEq bg) (Eq ag) = false
17.210 - | eq_fm (NClosed bd) (Ge ag) = false
17.211 - | eq_fm (Closed bd) (Ge ag) = false
17.212 - | eq_fm (A bf) (Ge ag) = false
17.213 - | eq_fm (E bf) (Ge ag) = false
17.214 - | eq_fm (Iff (bf, cf)) (Ge ag) = false
17.215 - | eq_fm (Imp (bf, cf)) (Ge ag) = false
17.216 - | eq_fm (Or (bf, cf)) (Ge ag) = false
17.217 - | eq_fm (And (bf, cf)) (Ge ag) = false
17.218 - | eq_fm (Not bf) (Ge ag) = false
17.219 - | eq_fm (NDvd (be, cg)) (Ge ag) = false
17.220 - | eq_fm (Dvd (be, cg)) (Ge ag) = false
17.221 - | eq_fm (NEq bg) (Ge ag) = false
17.222 - | eq_fm (Eq bg) (Ge ag) = false
17.223 - | eq_fm (NClosed bd) (Gt ag) = false
17.224 - | eq_fm (Closed bd) (Gt ag) = false
17.225 - | eq_fm (A bf) (Gt ag) = false
17.226 - | eq_fm (E bf) (Gt ag) = false
17.227 - | eq_fm (Iff (bf, cf)) (Gt ag) = false
17.228 - | eq_fm (Imp (bf, cf)) (Gt ag) = false
17.229 - | eq_fm (Or (bf, cf)) (Gt ag) = false
17.230 - | eq_fm (And (bf, cf)) (Gt ag) = false
17.231 - | eq_fm (Not bf) (Gt ag) = false
17.232 - | eq_fm (NDvd (be, cg)) (Gt ag) = false
17.233 - | eq_fm (Dvd (be, cg)) (Gt ag) = false
17.234 - | eq_fm (NEq bg) (Gt ag) = false
17.235 - | eq_fm (Eq bg) (Gt ag) = false
17.236 - | eq_fm (Ge bg) (Gt ag) = false
17.237 - | eq_fm (NClosed bd) (Le ag) = false
17.238 - | eq_fm (Closed bd) (Le ag) = false
17.239 - | eq_fm (A bf) (Le ag) = false
17.240 - | eq_fm (E bf) (Le ag) = false
17.241 - | eq_fm (Iff (bf, cf)) (Le ag) = false
17.242 - | eq_fm (Imp (bf, cf)) (Le ag) = false
17.243 - | eq_fm (Or (bf, cf)) (Le ag) = false
17.244 - | eq_fm (And (bf, cf)) (Le ag) = false
17.245 - | eq_fm (Not bf) (Le ag) = false
17.246 - | eq_fm (NDvd (be, cg)) (Le ag) = false
17.247 - | eq_fm (Dvd (be, cg)) (Le ag) = false
17.248 - | eq_fm (NEq bg) (Le ag) = false
17.249 - | eq_fm (Eq bg) (Le ag) = false
17.250 - | eq_fm (Ge bg) (Le ag) = false
17.251 - | eq_fm (Gt bg) (Le ag) = false
17.252 - | eq_fm (NClosed bd) (Lt ag) = false
17.253 - | eq_fm (Closed bd) (Lt ag) = false
17.254 - | eq_fm (A bf) (Lt ag) = false
17.255 - | eq_fm (E bf) (Lt ag) = false
17.256 - | eq_fm (Iff (bf, cf)) (Lt ag) = false
17.257 - | eq_fm (Imp (bf, cf)) (Lt ag) = false
17.258 - | eq_fm (Or (bf, cf)) (Lt ag) = false
17.259 - | eq_fm (And (bf, cf)) (Lt ag) = false
17.260 - | eq_fm (Not bf) (Lt ag) = false
17.261 - | eq_fm (NDvd (be, cg)) (Lt ag) = false
17.262 - | eq_fm (Dvd (be, cg)) (Lt ag) = false
17.263 - | eq_fm (NEq bg) (Lt ag) = false
17.264 - | eq_fm (Eq bg) (Lt ag) = false
17.265 - | eq_fm (Ge bg) (Lt ag) = false
17.266 - | eq_fm (Gt bg) (Lt ag) = false
17.267 - | eq_fm (Le bg) (Lt ag) = false
17.268 - | eq_fm (NClosed ad) F = false
17.269 - | eq_fm (Closed ad) F = false
17.270 - | eq_fm (A af) F = false
17.271 - | eq_fm (E af) F = false
17.272 - | eq_fm (Iff (af, bf)) F = false
17.273 - | eq_fm (Imp (af, bf)) F = false
17.274 - | eq_fm (Or (af, bf)) F = false
17.275 - | eq_fm (And (af, bf)) F = false
17.276 - | eq_fm (Not af) F = false
17.277 - | eq_fm (NDvd (ae, bg)) F = false
17.278 - | eq_fm (Dvd (ae, bg)) F = false
17.279 - | eq_fm (NEq ag) F = false
17.280 - | eq_fm (Eq ag) F = false
17.281 - | eq_fm (Ge ag) F = false
17.282 - | eq_fm (Gt ag) F = false
17.283 - | eq_fm (Le ag) F = false
17.284 - | eq_fm (Lt ag) F = false
17.285 - | eq_fm (NClosed ad) T = false
17.286 - | eq_fm (Closed ad) T = false
17.287 - | eq_fm (A af) T = false
17.288 - | eq_fm (E af) T = false
17.289 - | eq_fm (Iff (af, bf)) T = false
17.290 - | eq_fm (Imp (af, bf)) T = false
17.291 - | eq_fm (Or (af, bf)) T = false
17.292 - | eq_fm (And (af, bf)) T = false
17.293 - | eq_fm (Not af) T = false
17.294 - | eq_fm (NDvd (ae, bg)) T = false
17.295 - | eq_fm (Dvd (ae, bg)) T = false
17.296 - | eq_fm (NEq ag) T = false
17.297 - | eq_fm (Eq ag) T = false
17.298 - | eq_fm (Ge ag) T = false
17.299 - | eq_fm (Gt ag) T = false
17.300 - | eq_fm (Le ag) T = false
17.301 - | eq_fm (Lt ag) T = false
17.302 +fun eq_fm (NClosed b) (Closed a) = false
17.303 + | eq_fm (NClosed b) (A a) = false
17.304 + | eq_fm (Closed b) (A a) = false
17.305 + | eq_fm (NClosed b) (E a) = false
17.306 + | eq_fm (Closed b) (E a) = false
17.307 + | eq_fm (A b) (E a) = false
17.308 + | eq_fm (NClosed c) (Iff (a, b)) = false
17.309 + | eq_fm (Closed c) (Iff (a, b)) = false
17.310 + | eq_fm (A c) (Iff (a, b)) = false
17.311 + | eq_fm (E c) (Iff (a, b)) = false
17.312 + | eq_fm (NClosed c) (Imp (a, b)) = false
17.313 + | eq_fm (Closed c) (Imp (a, b)) = false
17.314 + | eq_fm (A c) (Imp (a, b)) = false
17.315 + | eq_fm (E c) (Imp (a, b)) = false
17.316 + | eq_fm (Iff (c, d)) (Imp (a, b)) = false
17.317 + | eq_fm (NClosed c) (Or (a, b)) = false
17.318 + | eq_fm (Closed c) (Or (a, b)) = false
17.319 + | eq_fm (A c) (Or (a, b)) = false
17.320 + | eq_fm (E c) (Or (a, b)) = false
17.321 + | eq_fm (Iff (c, d)) (Or (a, b)) = false
17.322 + | eq_fm (Imp (c, d)) (Or (a, b)) = false
17.323 + | eq_fm (NClosed c) (And (a, b)) = false
17.324 + | eq_fm (Closed c) (And (a, b)) = false
17.325 + | eq_fm (A c) (And (a, b)) = false
17.326 + | eq_fm (E c) (And (a, b)) = false
17.327 + | eq_fm (Iff (c, d)) (And (a, b)) = false
17.328 + | eq_fm (Imp (c, d)) (And (a, b)) = false
17.329 + | eq_fm (Or (c, d)) (And (a, b)) = false
17.330 + | eq_fm (NClosed b) (Not a) = false
17.331 + | eq_fm (Closed b) (Not a) = false
17.332 + | eq_fm (A b) (Not a) = false
17.333 + | eq_fm (E b) (Not a) = false
17.334 + | eq_fm (Iff (b, c)) (Not a) = false
17.335 + | eq_fm (Imp (b, c)) (Not a) = false
17.336 + | eq_fm (Or (b, c)) (Not a) = false
17.337 + | eq_fm (And (b, c)) (Not a) = false
17.338 + | eq_fm (NClosed c) (NDvd (a, b)) = false
17.339 + | eq_fm (Closed c) (NDvd (a, b)) = false
17.340 + | eq_fm (A c) (NDvd (a, b)) = false
17.341 + | eq_fm (E c) (NDvd (a, b)) = false
17.342 + | eq_fm (Iff (c, d)) (NDvd (a, b)) = false
17.343 + | eq_fm (Imp (c, d)) (NDvd (a, b)) = false
17.344 + | eq_fm (Or (c, d)) (NDvd (a, b)) = false
17.345 + | eq_fm (And (c, d)) (NDvd (a, b)) = false
17.346 + | eq_fm (Not c) (NDvd (a, b)) = false
17.347 + | eq_fm (NClosed c) (Dvd (a, b)) = false
17.348 + | eq_fm (Closed c) (Dvd (a, b)) = false
17.349 + | eq_fm (A c) (Dvd (a, b)) = false
17.350 + | eq_fm (E c) (Dvd (a, b)) = false
17.351 + | eq_fm (Iff (c, d)) (Dvd (a, b)) = false
17.352 + | eq_fm (Imp (c, d)) (Dvd (a, b)) = false
17.353 + | eq_fm (Or (c, d)) (Dvd (a, b)) = false
17.354 + | eq_fm (And (c, d)) (Dvd (a, b)) = false
17.355 + | eq_fm (Not c) (Dvd (a, b)) = false
17.356 + | eq_fm (NDvd (c, d)) (Dvd (a, b)) = false
17.357 + | eq_fm (NClosed b) (NEq a) = false
17.358 + | eq_fm (Closed b) (NEq a) = false
17.359 + | eq_fm (A b) (NEq a) = false
17.360 + | eq_fm (E b) (NEq a) = false
17.361 + | eq_fm (Iff (b, c)) (NEq a) = false
17.362 + | eq_fm (Imp (b, c)) (NEq a) = false
17.363 + | eq_fm (Or (b, c)) (NEq a) = false
17.364 + | eq_fm (And (b, c)) (NEq a) = false
17.365 + | eq_fm (Not b) (NEq a) = false
17.366 + | eq_fm (NDvd (b, c)) (NEq a) = false
17.367 + | eq_fm (Dvd (b, c)) (NEq a) = false
17.368 + | eq_fm (NClosed b) (Eq a) = false
17.369 + | eq_fm (Closed b) (Eq a) = false
17.370 + | eq_fm (A b) (Eq a) = false
17.371 + | eq_fm (E b) (Eq a) = false
17.372 + | eq_fm (Iff (b, c)) (Eq a) = false
17.373 + | eq_fm (Imp (b, c)) (Eq a) = false
17.374 + | eq_fm (Or (b, c)) (Eq a) = false
17.375 + | eq_fm (And (b, c)) (Eq a) = false
17.376 + | eq_fm (Not b) (Eq a) = false
17.377 + | eq_fm (NDvd (b, c)) (Eq a) = false
17.378 + | eq_fm (Dvd (b, c)) (Eq a) = false
17.379 + | eq_fm (NEq b) (Eq a) = false
17.380 + | eq_fm (NClosed b) (Ge a) = false
17.381 + | eq_fm (Closed b) (Ge a) = false
17.382 + | eq_fm (A b) (Ge a) = false
17.383 + | eq_fm (E b) (Ge a) = false
17.384 + | eq_fm (Iff (b, c)) (Ge a) = false
17.385 + | eq_fm (Imp (b, c)) (Ge a) = false
17.386 + | eq_fm (Or (b, c)) (Ge a) = false
17.387 + | eq_fm (And (b, c)) (Ge a) = false
17.388 + | eq_fm (Not b) (Ge a) = false
17.389 + | eq_fm (NDvd (b, c)) (Ge a) = false
17.390 + | eq_fm (Dvd (b, c)) (Ge a) = false
17.391 + | eq_fm (NEq b) (Ge a) = false
17.392 + | eq_fm (Eq b) (Ge a) = false
17.393 + | eq_fm (NClosed b) (Gt a) = false
17.394 + | eq_fm (Closed b) (Gt a) = false
17.395 + | eq_fm (A b) (Gt a) = false
17.396 + | eq_fm (E b) (Gt a) = false
17.397 + | eq_fm (Iff (b, c)) (Gt a) = false
17.398 + | eq_fm (Imp (b, c)) (Gt a) = false
17.399 + | eq_fm (Or (b, c)) (Gt a) = false
17.400 + | eq_fm (And (b, c)) (Gt a) = false
17.401 + | eq_fm (Not b) (Gt a) = false
17.402 + | eq_fm (NDvd (b, c)) (Gt a) = false
17.403 + | eq_fm (Dvd (b, c)) (Gt a) = false
17.404 + | eq_fm (NEq b) (Gt a) = false
17.405 + | eq_fm (Eq b) (Gt a) = false
17.406 + | eq_fm (Ge b) (Gt a) = false
17.407 + | eq_fm (NClosed b) (Le a) = false
17.408 + | eq_fm (Closed b) (Le a) = false
17.409 + | eq_fm (A b) (Le a) = false
17.410 + | eq_fm (E b) (Le a) = false
17.411 + | eq_fm (Iff (b, c)) (Le a) = false
17.412 + | eq_fm (Imp (b, c)) (Le a) = false
17.413 + | eq_fm (Or (b, c)) (Le a) = false
17.414 + | eq_fm (And (b, c)) (Le a) = false
17.415 + | eq_fm (Not b) (Le a) = false
17.416 + | eq_fm (NDvd (b, c)) (Le a) = false
17.417 + | eq_fm (Dvd (b, c)) (Le a) = false
17.418 + | eq_fm (NEq b) (Le a) = false
17.419 + | eq_fm (Eq b) (Le a) = false
17.420 + | eq_fm (Ge b) (Le a) = false
17.421 + | eq_fm (Gt b) (Le a) = false
17.422 + | eq_fm (NClosed b) (Lt a) = false
17.423 + | eq_fm (Closed b) (Lt a) = false
17.424 + | eq_fm (A b) (Lt a) = false
17.425 + | eq_fm (E b) (Lt a) = false
17.426 + | eq_fm (Iff (b, c)) (Lt a) = false
17.427 + | eq_fm (Imp (b, c)) (Lt a) = false
17.428 + | eq_fm (Or (b, c)) (Lt a) = false
17.429 + | eq_fm (And (b, c)) (Lt a) = false
17.430 + | eq_fm (Not b) (Lt a) = false
17.431 + | eq_fm (NDvd (b, c)) (Lt a) = false
17.432 + | eq_fm (Dvd (b, c)) (Lt a) = false
17.433 + | eq_fm (NEq b) (Lt a) = false
17.434 + | eq_fm (Eq b) (Lt a) = false
17.435 + | eq_fm (Ge b) (Lt a) = false
17.436 + | eq_fm (Gt b) (Lt a) = false
17.437 + | eq_fm (Le b) (Lt a) = false
17.438 + | eq_fm (NClosed a) F = false
17.439 + | eq_fm (Closed a) F = false
17.440 + | eq_fm (A a) F = false
17.441 + | eq_fm (E a) F = false
17.442 + | eq_fm (Iff (a, b)) F = false
17.443 + | eq_fm (Imp (a, b)) F = false
17.444 + | eq_fm (Or (a, b)) F = false
17.445 + | eq_fm (And (a, b)) F = false
17.446 + | eq_fm (Not a) F = false
17.447 + | eq_fm (NDvd (a, b)) F = false
17.448 + | eq_fm (Dvd (a, b)) F = false
17.449 + | eq_fm (NEq a) F = false
17.450 + | eq_fm (Eq a) F = false
17.451 + | eq_fm (Ge a) F = false
17.452 + | eq_fm (Gt a) F = false
17.453 + | eq_fm (Le a) F = false
17.454 + | eq_fm (Lt a) F = false
17.455 + | eq_fm (NClosed a) T = false
17.456 + | eq_fm (Closed a) T = false
17.457 + | eq_fm (A a) T = false
17.458 + | eq_fm (E a) T = false
17.459 + | eq_fm (Iff (a, b)) T = false
17.460 + | eq_fm (Imp (a, b)) T = false
17.461 + | eq_fm (Or (a, b)) T = false
17.462 + | eq_fm (And (a, b)) T = false
17.463 + | eq_fm (Not a) T = false
17.464 + | eq_fm (NDvd (a, b)) T = false
17.465 + | eq_fm (Dvd (a, b)) T = false
17.466 + | eq_fm (NEq a) T = false
17.467 + | eq_fm (Eq a) T = false
17.468 + | eq_fm (Ge a) T = false
17.469 + | eq_fm (Gt a) T = false
17.470 + | eq_fm (Le a) T = false
17.471 + | eq_fm (Lt a) T = false
17.472 | eq_fm F T = false
17.473 | eq_fm (Closed a) (NClosed b) = false
17.474 - | eq_fm (A ab) (NClosed b) = false
17.475 - | eq_fm (A ab) (Closed b) = false
17.476 - | eq_fm (E ab) (NClosed b) = false
17.477 - | eq_fm (E ab) (Closed b) = false
17.478 - | eq_fm (E ab) (A bb) = false
17.479 - | eq_fm (Iff (ab, bb)) (NClosed c) = false
17.480 - | eq_fm (Iff (ab, bb)) (Closed c) = false
17.481 - | eq_fm (Iff (ab, bb)) (A cb) = false
17.482 - | eq_fm (Iff (ab, bb)) (E cb) = false
17.483 - | eq_fm (Imp (ab, bb)) (NClosed c) = false
17.484 - | eq_fm (Imp (ab, bb)) (Closed c) = false
17.485 - | eq_fm (Imp (ab, bb)) (A cb) = false
17.486 - | eq_fm (Imp (ab, bb)) (E cb) = false
17.487 - | eq_fm (Imp (ab, bb)) (Iff (cb, d)) = false
17.488 - | eq_fm (Or (ab, bb)) (NClosed c) = false
17.489 - | eq_fm (Or (ab, bb)) (Closed c) = false
17.490 - | eq_fm (Or (ab, bb)) (A cb) = false
17.491 - | eq_fm (Or (ab, bb)) (E cb) = false
17.492 - | eq_fm (Or (ab, bb)) (Iff (cb, d)) = false
17.493 - | eq_fm (Or (ab, bb)) (Imp (cb, d)) = false
17.494 - | eq_fm (And (ab, bb)) (NClosed c) = false
17.495 - | eq_fm (And (ab, bb)) (Closed c) = false
17.496 - | eq_fm (And (ab, bb)) (A cb) = false
17.497 - | eq_fm (And (ab, bb)) (E cb) = false
17.498 - | eq_fm (And (ab, bb)) (Iff (cb, d)) = false
17.499 - | eq_fm (And (ab, bb)) (Imp (cb, d)) = false
17.500 - | eq_fm (And (ab, bb)) (Or (cb, d)) = false
17.501 - | eq_fm (Not ab) (NClosed b) = false
17.502 - | eq_fm (Not ab) (Closed b) = false
17.503 - | eq_fm (Not ab) (A bb) = false
17.504 - | eq_fm (Not ab) (E bb) = false
17.505 - | eq_fm (Not ab) (Iff (bb, cb)) = false
17.506 - | eq_fm (Not ab) (Imp (bb, cb)) = false
17.507 - | eq_fm (Not ab) (Or (bb, cb)) = false
17.508 - | eq_fm (Not ab) (And (bb, cb)) = false
17.509 - | eq_fm (NDvd (aa, bc)) (NClosed c) = false
17.510 - | eq_fm (NDvd (aa, bc)) (Closed c) = false
17.511 - | eq_fm (NDvd (aa, bc)) (A cb) = false
17.512 - | eq_fm (NDvd (aa, bc)) (E cb) = false
17.513 - | eq_fm (NDvd (aa, bc)) (Iff (cb, d)) = false
17.514 - | eq_fm (NDvd (aa, bc)) (Imp (cb, d)) = false
17.515 - | eq_fm (NDvd (aa, bc)) (Or (cb, d)) = false
17.516 - | eq_fm (NDvd (aa, bc)) (And (cb, d)) = false
17.517 - | eq_fm (NDvd (aa, bc)) (Not cb) = false
17.518 - | eq_fm (Dvd (aa, bc)) (NClosed c) = false
17.519 - | eq_fm (Dvd (aa, bc)) (Closed c) = false
17.520 - | eq_fm (Dvd (aa, bc)) (A cb) = false
17.521 - | eq_fm (Dvd (aa, bc)) (E cb) = false
17.522 - | eq_fm (Dvd (aa, bc)) (Iff (cb, d)) = false
17.523 - | eq_fm (Dvd (aa, bc)) (Imp (cb, d)) = false
17.524 - | eq_fm (Dvd (aa, bc)) (Or (cb, d)) = false
17.525 - | eq_fm (Dvd (aa, bc)) (And (cb, d)) = false
17.526 - | eq_fm (Dvd (aa, bc)) (Not cb) = false
17.527 - | eq_fm (Dvd (aa, bc)) (NDvd (ca, da)) = false
17.528 - | eq_fm (NEq ac) (NClosed b) = false
17.529 - | eq_fm (NEq ac) (Closed b) = false
17.530 - | eq_fm (NEq ac) (A bb) = false
17.531 - | eq_fm (NEq ac) (E bb) = false
17.532 - | eq_fm (NEq ac) (Iff (bb, cb)) = false
17.533 - | eq_fm (NEq ac) (Imp (bb, cb)) = false
17.534 - | eq_fm (NEq ac) (Or (bb, cb)) = false
17.535 - | eq_fm (NEq ac) (And (bb, cb)) = false
17.536 - | eq_fm (NEq ac) (Not bb) = false
17.537 - | eq_fm (NEq ac) (NDvd (ba, cc)) = false
17.538 - | eq_fm (NEq ac) (Dvd (ba, cc)) = false
17.539 - | eq_fm (Eq ac) (NClosed b) = false
17.540 - | eq_fm (Eq ac) (Closed b) = false
17.541 - | eq_fm (Eq ac) (A bb) = false
17.542 - | eq_fm (Eq ac) (E bb) = false
17.543 - | eq_fm (Eq ac) (Iff (bb, cb)) = false
17.544 - | eq_fm (Eq ac) (Imp (bb, cb)) = false
17.545 - | eq_fm (Eq ac) (Or (bb, cb)) = false
17.546 - | eq_fm (Eq ac) (And (bb, cb)) = false
17.547 - | eq_fm (Eq ac) (Not bb) = false
17.548 - | eq_fm (Eq ac) (NDvd (ba, cc)) = false
17.549 - | eq_fm (Eq ac) (Dvd (ba, cc)) = false
17.550 - | eq_fm (Eq ac) (NEq bc) = false
17.551 - | eq_fm (Ge ac) (NClosed b) = false
17.552 - | eq_fm (Ge ac) (Closed b) = false
17.553 - | eq_fm (Ge ac) (A bb) = false
17.554 - | eq_fm (Ge ac) (E bb) = false
17.555 - | eq_fm (Ge ac) (Iff (bb, cb)) = false
17.556 - | eq_fm (Ge ac) (Imp (bb, cb)) = false
17.557 - | eq_fm (Ge ac) (Or (bb, cb)) = false
17.558 - | eq_fm (Ge ac) (And (bb, cb)) = false
17.559 - | eq_fm (Ge ac) (Not bb) = false
17.560 - | eq_fm (Ge ac) (NDvd (ba, cc)) = false
17.561 - | eq_fm (Ge ac) (Dvd (ba, cc)) = false
17.562 - | eq_fm (Ge ac) (NEq bc) = false
17.563 - | eq_fm (Ge ac) (Eq bc) = false
17.564 - | eq_fm (Gt ac) (NClosed b) = false
17.565 - | eq_fm (Gt ac) (Closed b) = false
17.566 - | eq_fm (Gt ac) (A bb) = false
17.567 - | eq_fm (Gt ac) (E bb) = false
17.568 - | eq_fm (Gt ac) (Iff (bb, cb)) = false
17.569 - | eq_fm (Gt ac) (Imp (bb, cb)) = false
17.570 - | eq_fm (Gt ac) (Or (bb, cb)) = false
17.571 - | eq_fm (Gt ac) (And (bb, cb)) = false
17.572 - | eq_fm (Gt ac) (Not bb) = false
17.573 - | eq_fm (Gt ac) (NDvd (ba, cc)) = false
17.574 - | eq_fm (Gt ac) (Dvd (ba, cc)) = false
17.575 - | eq_fm (Gt ac) (NEq bc) = false
17.576 - | eq_fm (Gt ac) (Eq bc) = false
17.577 - | eq_fm (Gt ac) (Ge bc) = false
17.578 - | eq_fm (Le ac) (NClosed b) = false
17.579 - | eq_fm (Le ac) (Closed b) = false
17.580 - | eq_fm (Le ac) (A bb) = false
17.581 - | eq_fm (Le ac) (E bb) = false
17.582 - | eq_fm (Le ac) (Iff (bb, cb)) = false
17.583 - | eq_fm (Le ac) (Imp (bb, cb)) = false
17.584 - | eq_fm (Le ac) (Or (bb, cb)) = false
17.585 - | eq_fm (Le ac) (And (bb, cb)) = false
17.586 - | eq_fm (Le ac) (Not bb) = false
17.587 - | eq_fm (Le ac) (NDvd (ba, cc)) = false
17.588 - | eq_fm (Le ac) (Dvd (ba, cc)) = false
17.589 - | eq_fm (Le ac) (NEq bc) = false
17.590 - | eq_fm (Le ac) (Eq bc) = false
17.591 - | eq_fm (Le ac) (Ge bc) = false
17.592 - | eq_fm (Le ac) (Gt bc) = false
17.593 - | eq_fm (Lt ac) (NClosed b) = false
17.594 - | eq_fm (Lt ac) (Closed b) = false
17.595 - | eq_fm (Lt ac) (A bb) = false
17.596 - | eq_fm (Lt ac) (E bb) = false
17.597 - | eq_fm (Lt ac) (Iff (bb, cb)) = false
17.598 - | eq_fm (Lt ac) (Imp (bb, cb)) = false
17.599 - | eq_fm (Lt ac) (Or (bb, cb)) = false
17.600 - | eq_fm (Lt ac) (And (bb, cb)) = false
17.601 - | eq_fm (Lt ac) (Not bb) = false
17.602 - | eq_fm (Lt ac) (NDvd (ba, cc)) = false
17.603 - | eq_fm (Lt ac) (Dvd (ba, cc)) = false
17.604 - | eq_fm (Lt ac) (NEq bc) = false
17.605 - | eq_fm (Lt ac) (Eq bc) = false
17.606 - | eq_fm (Lt ac) (Ge bc) = false
17.607 - | eq_fm (Lt ac) (Gt bc) = false
17.608 - | eq_fm (Lt ac) (Le bc) = false
17.609 + | eq_fm (A a) (NClosed b) = false
17.610 + | eq_fm (A a) (Closed b) = false
17.611 + | eq_fm (E a) (NClosed b) = false
17.612 + | eq_fm (E a) (Closed b) = false
17.613 + | eq_fm (E a) (A b) = false
17.614 + | eq_fm (Iff (a, b)) (NClosed c) = false
17.615 + | eq_fm (Iff (a, b)) (Closed c) = false
17.616 + | eq_fm (Iff (a, b)) (A c) = false
17.617 + | eq_fm (Iff (a, b)) (E c) = false
17.618 + | eq_fm (Imp (a, b)) (NClosed c) = false
17.619 + | eq_fm (Imp (a, b)) (Closed c) = false
17.620 + | eq_fm (Imp (a, b)) (A c) = false
17.621 + | eq_fm (Imp (a, b)) (E c) = false
17.622 + | eq_fm (Imp (a, b)) (Iff (c, d)) = false
17.623 + | eq_fm (Or (a, b)) (NClosed c) = false
17.624 + | eq_fm (Or (a, b)) (Closed c) = false
17.625 + | eq_fm (Or (a, b)) (A c) = false
17.626 + | eq_fm (Or (a, b)) (E c) = false
17.627 + | eq_fm (Or (a, b)) (Iff (c, d)) = false
17.628 + | eq_fm (Or (a, b)) (Imp (c, d)) = false
17.629 + | eq_fm (And (a, b)) (NClosed c) = false
17.630 + | eq_fm (And (a, b)) (Closed c) = false
17.631 + | eq_fm (And (a, b)) (A c) = false
17.632 + | eq_fm (And (a, b)) (E c) = false
17.633 + | eq_fm (And (a, b)) (Iff (c, d)) = false
17.634 + | eq_fm (And (a, b)) (Imp (c, d)) = false
17.635 + | eq_fm (And (a, b)) (Or (c, d)) = false
17.636 + | eq_fm (Not a) (NClosed b) = false
17.637 + | eq_fm (Not a) (Closed b) = false
17.638 + | eq_fm (Not a) (A b) = false
17.639 + | eq_fm (Not a) (E b) = false
17.640 + | eq_fm (Not a) (Iff (b, c)) = false
17.641 + | eq_fm (Not a) (Imp (b, c)) = false
17.642 + | eq_fm (Not a) (Or (b, c)) = false
17.643 + | eq_fm (Not a) (And (b, c)) = false
17.644 + | eq_fm (NDvd (a, b)) (NClosed c) = false
17.645 + | eq_fm (NDvd (a, b)) (Closed c) = false
17.646 + | eq_fm (NDvd (a, b)) (A c) = false
17.647 + | eq_fm (NDvd (a, b)) (E c) = false
17.648 + | eq_fm (NDvd (a, b)) (Iff (c, d)) = false
17.649 + | eq_fm (NDvd (a, b)) (Imp (c, d)) = false
17.650 + | eq_fm (NDvd (a, b)) (Or (c, d)) = false
17.651 + | eq_fm (NDvd (a, b)) (And (c, d)) = false
17.652 + | eq_fm (NDvd (a, b)) (Not c) = false
17.653 + | eq_fm (Dvd (a, b)) (NClosed c) = false
17.654 + | eq_fm (Dvd (a, b)) (Closed c) = false
17.655 + | eq_fm (Dvd (a, b)) (A c) = false
17.656 + | eq_fm (Dvd (a, b)) (E c) = false
17.657 + | eq_fm (Dvd (a, b)) (Iff (c, d)) = false
17.658 + | eq_fm (Dvd (a, b)) (Imp (c, d)) = false
17.659 + | eq_fm (Dvd (a, b)) (Or (c, d)) = false
17.660 + | eq_fm (Dvd (a, b)) (And (c, d)) = false
17.661 + | eq_fm (Dvd (a, b)) (Not c) = false
17.662 + | eq_fm (Dvd (a, b)) (NDvd (c, d)) = false
17.663 + | eq_fm (NEq a) (NClosed b) = false
17.664 + | eq_fm (NEq a) (Closed b) = false
17.665 + | eq_fm (NEq a) (A b) = false
17.666 + | eq_fm (NEq a) (E b) = false
17.667 + | eq_fm (NEq a) (Iff (b, c)) = false
17.668 + | eq_fm (NEq a) (Imp (b, c)) = false
17.669 + | eq_fm (NEq a) (Or (b, c)) = false
17.670 + | eq_fm (NEq a) (And (b, c)) = false
17.671 + | eq_fm (NEq a) (Not b) = false
17.672 + | eq_fm (NEq a) (NDvd (b, c)) = false
17.673 + | eq_fm (NEq a) (Dvd (b, c)) = false
17.674 + | eq_fm (Eq a) (NClosed b) = false
17.675 + | eq_fm (Eq a) (Closed b) = false
17.676 + | eq_fm (Eq a) (A b) = false
17.677 + | eq_fm (Eq a) (E b) = false
17.678 + | eq_fm (Eq a) (Iff (b, c)) = false
17.679 + | eq_fm (Eq a) (Imp (b, c)) = false
17.680 + | eq_fm (Eq a) (Or (b, c)) = false
17.681 + | eq_fm (Eq a) (And (b, c)) = false
17.682 + | eq_fm (Eq a) (Not b) = false
17.683 + | eq_fm (Eq a) (NDvd (b, c)) = false
17.684 + | eq_fm (Eq a) (Dvd (b, c)) = false
17.685 + | eq_fm (Eq a) (NEq b) = false
17.686 + | eq_fm (Ge a) (NClosed b) = false
17.687 + | eq_fm (Ge a) (Closed b) = false
17.688 + | eq_fm (Ge a) (A b) = false
17.689 + | eq_fm (Ge a) (E b) = false
17.690 + | eq_fm (Ge a) (Iff (b, c)) = false
17.691 + | eq_fm (Ge a) (Imp (b, c)) = false
17.692 + | eq_fm (Ge a) (Or (b, c)) = false
17.693 + | eq_fm (Ge a) (And (b, c)) = false
17.694 + | eq_fm (Ge a) (Not b) = false
17.695 + | eq_fm (Ge a) (NDvd (b, c)) = false
17.696 + | eq_fm (Ge a) (Dvd (b, c)) = false
17.697 + | eq_fm (Ge a) (NEq b) = false
17.698 + | eq_fm (Ge a) (Eq b) = false
17.699 + | eq_fm (Gt a) (NClosed b) = false
17.700 + | eq_fm (Gt a) (Closed b) = false
17.701 + | eq_fm (Gt a) (A b) = false
17.702 + | eq_fm (Gt a) (E b) = false
17.703 + | eq_fm (Gt a) (Iff (b, c)) = false
17.704 + | eq_fm (Gt a) (Imp (b, c)) = false
17.705 + | eq_fm (Gt a) (Or (b, c)) = false
17.706 + | eq_fm (Gt a) (And (b, c)) = false
17.707 + | eq_fm (Gt a) (Not b) = false
17.708 + | eq_fm (Gt a) (NDvd (b, c)) = false
17.709 + | eq_fm (Gt a) (Dvd (b, c)) = false
17.710 + | eq_fm (Gt a) (NEq b) = false
17.711 + | eq_fm (Gt a) (Eq b) = false
17.712 + | eq_fm (Gt a) (Ge b) = false
17.713 + | eq_fm (Le a) (NClosed b) = false
17.714 + | eq_fm (Le a) (Closed b) = false
17.715 + | eq_fm (Le a) (A b) = false
17.716 + | eq_fm (Le a) (E b) = false
17.717 + | eq_fm (Le a) (Iff (b, c)) = false
17.718 + | eq_fm (Le a) (Imp (b, c)) = false
17.719 + | eq_fm (Le a) (Or (b, c)) = false
17.720 + | eq_fm (Le a) (And (b, c)) = false
17.721 + | eq_fm (Le a) (Not b) = false
17.722 + | eq_fm (Le a) (NDvd (b, c)) = false
17.723 + | eq_fm (Le a) (Dvd (b, c)) = false
17.724 + | eq_fm (Le a) (NEq b) = false
17.725 + | eq_fm (Le a) (Eq b) = false
17.726 + | eq_fm (Le a) (Ge b) = false
17.727 + | eq_fm (Le a) (Gt b) = false
17.728 + | eq_fm (Lt a) (NClosed b) = false
17.729 + | eq_fm (Lt a) (Closed b) = false
17.730 + | eq_fm (Lt a) (A b) = false
17.731 + | eq_fm (Lt a) (E b) = false
17.732 + | eq_fm (Lt a) (Iff (b, c)) = false
17.733 + | eq_fm (Lt a) (Imp (b, c)) = false
17.734 + | eq_fm (Lt a) (Or (b, c)) = false
17.735 + | eq_fm (Lt a) (And (b, c)) = false
17.736 + | eq_fm (Lt a) (Not b) = false
17.737 + | eq_fm (Lt a) (NDvd (b, c)) = false
17.738 + | eq_fm (Lt a) (Dvd (b, c)) = false
17.739 + | eq_fm (Lt a) (NEq b) = false
17.740 + | eq_fm (Lt a) (Eq b) = false
17.741 + | eq_fm (Lt a) (Ge b) = false
17.742 + | eq_fm (Lt a) (Gt b) = false
17.743 + | eq_fm (Lt a) (Le b) = false
17.744 | eq_fm F (NClosed a) = false
17.745 | eq_fm F (Closed a) = false
17.746 - | eq_fm F (A ab) = false
17.747 - | eq_fm F (E ab) = false
17.748 - | eq_fm F (Iff (ab, bb)) = false
17.749 - | eq_fm F (Imp (ab, bb)) = false
17.750 - | eq_fm F (Or (ab, bb)) = false
17.751 - | eq_fm F (And (ab, bb)) = false
17.752 - | eq_fm F (Not ab) = false
17.753 - | eq_fm F (NDvd (aa, bc)) = false
17.754 - | eq_fm F (Dvd (aa, bc)) = false
17.755 - | eq_fm F (NEq ac) = false
17.756 - | eq_fm F (Eq ac) = false
17.757 - | eq_fm F (Ge ac) = false
17.758 - | eq_fm F (Gt ac) = false
17.759 - | eq_fm F (Le ac) = false
17.760 - | eq_fm F (Lt ac) = false
17.761 + | eq_fm F (A a) = false
17.762 + | eq_fm F (E a) = false
17.763 + | eq_fm F (Iff (a, b)) = false
17.764 + | eq_fm F (Imp (a, b)) = false
17.765 + | eq_fm F (Or (a, b)) = false
17.766 + | eq_fm F (And (a, b)) = false
17.767 + | eq_fm F (Not a) = false
17.768 + | eq_fm F (NDvd (a, b)) = false
17.769 + | eq_fm F (Dvd (a, b)) = false
17.770 + | eq_fm F (NEq a) = false
17.771 + | eq_fm F (Eq a) = false
17.772 + | eq_fm F (Ge a) = false
17.773 + | eq_fm F (Gt a) = false
17.774 + | eq_fm F (Le a) = false
17.775 + | eq_fm F (Lt a) = false
17.776 | eq_fm T (NClosed a) = false
17.777 | eq_fm T (Closed a) = false
17.778 - | eq_fm T (A ab) = false
17.779 - | eq_fm T (E ab) = false
17.780 - | eq_fm T (Iff (ab, bb)) = false
17.781 - | eq_fm T (Imp (ab, bb)) = false
17.782 - | eq_fm T (Or (ab, bb)) = false
17.783 - | eq_fm T (And (ab, bb)) = false
17.784 - | eq_fm T (Not ab) = false
17.785 - | eq_fm T (NDvd (aa, bc)) = false
17.786 - | eq_fm T (Dvd (aa, bc)) = false
17.787 - | eq_fm T (NEq ac) = false
17.788 - | eq_fm T (Eq ac) = false
17.789 - | eq_fm T (Ge ac) = false
17.790 - | eq_fm T (Gt ac) = false
17.791 - | eq_fm T (Le ac) = false
17.792 - | eq_fm T (Lt ac) = false
17.793 + | eq_fm T (A a) = false
17.794 + | eq_fm T (E a) = false
17.795 + | eq_fm T (Iff (a, b)) = false
17.796 + | eq_fm T (Imp (a, b)) = false
17.797 + | eq_fm T (Or (a, b)) = false
17.798 + | eq_fm T (And (a, b)) = false
17.799 + | eq_fm T (Not a) = false
17.800 + | eq_fm T (NDvd (a, b)) = false
17.801 + | eq_fm T (Dvd (a, b)) = false
17.802 + | eq_fm T (NEq a) = false
17.803 + | eq_fm T (Eq a) = false
17.804 + | eq_fm T (Ge a) = false
17.805 + | eq_fm T (Gt a) = false
17.806 + | eq_fm T (Le a) = false
17.807 + | eq_fm T (Lt a) = false
17.808 | eq_fm T F = false
17.809 | eq_fm (NClosed nat) (NClosed nat') = ((nat : IntInf.int) = nat')
17.810 | eq_fm (Closed nat) (Closed nat') = ((nat : IntInf.int) = nat')
17.811 @@ -554,7 +554,7 @@
17.812 | NClosed nat => Or (f p, q))
17.813 end));
17.814
17.815 -fun foldr f [] y = y
17.816 +fun foldr f [] a = a
17.817 | foldr f (x :: xs) a = f x (foldr f xs a);
17.818
17.819 fun evaldjf f ps = foldr (djf f) ps F;
17.820 @@ -607,9 +607,9 @@
17.821 | numsubst0 t (Add (a, b)) = Add (numsubst0 t a, numsubst0 t b)
17.822 | numsubst0 t (Sub (a, b)) = Sub (numsubst0 t a, numsubst0 t b)
17.823 | numsubst0 t (Mul (i, a)) = Mul (i, numsubst0 t a)
17.824 - | numsubst0 ta (Cn (v, ia, aa)) =
17.825 - (if eqop eq_nat v 0 then Add (Mul (ia, ta), numsubst0 ta aa)
17.826 - else Cn (suc (minus_nat v 1), ia, numsubst0 ta aa));
17.827 + | numsubst0 t (Cn (v, i, a)) =
17.828 + (if eqop eq_nat v 0 then Add (Mul (i, t), numsubst0 t a)
17.829 + else Cn (suc (minus_nat v 1), i, numsubst0 t a));
17.830
17.831 fun subst0 t T = T
17.832 | subst0 t F = F
17.833 @@ -691,36 +691,35 @@
17.834 | minusinf (NEq (Cn (hm, c, e))) =
17.835 (if eqop eq_nat hm 0 then T else NEq (Cn (suc (minus_nat hm 1), c, e)));
17.836
17.837 -fun adjust b =
17.838 - (fn a as (q, r) =>
17.839 - (if IntInf.<= ((0 : IntInf.int), IntInf.- (r, b))
17.840 - then (IntInf.+ (IntInf.* ((2 : IntInf.int), q), (1 : IntInf.int)),
17.841 - IntInf.- (r, b))
17.842 - else (IntInf.* ((2 : IntInf.int), q), r)));
17.843 +val eq_int = {eq = (fn a => fn b => ((a : IntInf.int) = b))} : IntInf.int eq;
17.844
17.845 -fun negDivAlg a b =
17.846 - (if IntInf.<= ((0 : IntInf.int), IntInf.+ (a, b)) orelse
17.847 - IntInf.<= (b, (0 : IntInf.int))
17.848 - then ((~1 : IntInf.int), IntInf.+ (a, b))
17.849 - else adjust b (negDivAlg a (IntInf.* ((2 : IntInf.int), b))));
17.850 +fun sgn_int i =
17.851 + (if eqop eq_int i (0 : IntInf.int) then (0 : IntInf.int)
17.852 + else (if IntInf.< ((0 : IntInf.int), i) then (1 : IntInf.int)
17.853 + else IntInf.~ (1 : IntInf.int)));
17.854
17.855 fun apsnd f (x, y) = (x, f y);
17.856
17.857 -val eq_int = {eq = (fn a => fn b => ((a : IntInf.int) = b))} : IntInf.int eq;
17.858 -
17.859 -fun posDivAlg a b =
17.860 - (if IntInf.< (a, b) orelse IntInf.<= (b, (0 : IntInf.int))
17.861 - then ((0 : IntInf.int), a)
17.862 - else adjust b (posDivAlg a (IntInf.* ((2 : IntInf.int), b))));
17.863 -
17.864 -fun divmoda a b =
17.865 - (if IntInf.<= ((0 : IntInf.int), a)
17.866 - then (if IntInf.<= ((0 : IntInf.int), b) then posDivAlg a b
17.867 - else (if eqop eq_int a (0 : IntInf.int)
17.868 - then ((0 : IntInf.int), (0 : IntInf.int))
17.869 - else apsnd IntInf.~ (negDivAlg (IntInf.~ a) (IntInf.~ b))))
17.870 - else (if IntInf.< ((0 : IntInf.int), b) then negDivAlg a b
17.871 - else apsnd IntInf.~ (posDivAlg (IntInf.~ a) (IntInf.~ b))));
17.872 +fun divmoda k l =
17.873 + (if eqop eq_int k (0 : IntInf.int) then ((0 : IntInf.int), (0 : IntInf.int))
17.874 + else (if eqop eq_int l (0 : IntInf.int) then ((0 : IntInf.int), k)
17.875 + else apsnd (fn a => IntInf.* (sgn_int l, a))
17.876 + (if eqop eq_int (sgn_int k) (sgn_int l)
17.877 + then (fn k => fn l => IntInf.divMod (IntInf.abs k,
17.878 + IntInf.abs l))
17.879 + k l
17.880 + else let
17.881 + val a =
17.882 + (fn k => fn l => IntInf.divMod (IntInf.abs k,
17.883 + IntInf.abs l))
17.884 + k l;
17.885 + val (r, s) = a;
17.886 + in
17.887 + (if eqop eq_int s (0 : IntInf.int)
17.888 + then (IntInf.~ r, (0 : IntInf.int))
17.889 + else (IntInf.- (IntInf.~ r, (1 : IntInf.int)),
17.890 + IntInf.- (abs_int l, s)))
17.891 + end)));
17.892
17.893 fun mod_int a b = snd (divmoda a b);
17.894
17.895 @@ -823,23 +822,23 @@
17.896 else nummul i (simpnum t))
17.897 | simpnum (Cn (v, va, vb)) = Cn (v, va, vb);
17.898
17.899 -fun nota (Not y) = y
17.900 +fun nota (Not p) = p
17.901 | nota T = F
17.902 | nota F = T
17.903 - | nota (Lt vc) = Not (Lt vc)
17.904 - | nota (Le vc) = Not (Le vc)
17.905 - | nota (Gt vc) = Not (Gt vc)
17.906 - | nota (Ge vc) = Not (Ge vc)
17.907 - | nota (Eq vc) = Not (Eq vc)
17.908 - | nota (NEq vc) = Not (NEq vc)
17.909 - | nota (Dvd (va, vab)) = Not (Dvd (va, vab))
17.910 - | nota (NDvd (va, vab)) = Not (NDvd (va, vab))
17.911 - | nota (And (vb, vaa)) = Not (And (vb, vaa))
17.912 - | nota (Or (vb, vaa)) = Not (Or (vb, vaa))
17.913 - | nota (Imp (vb, vaa)) = Not (Imp (vb, vaa))
17.914 - | nota (Iff (vb, vaa)) = Not (Iff (vb, vaa))
17.915 - | nota (E vb) = Not (E vb)
17.916 - | nota (A vb) = Not (A vb)
17.917 + | nota (Lt v) = Not (Lt v)
17.918 + | nota (Le v) = Not (Le v)
17.919 + | nota (Gt v) = Not (Gt v)
17.920 + | nota (Ge v) = Not (Ge v)
17.921 + | nota (Eq v) = Not (Eq v)
17.922 + | nota (NEq v) = Not (NEq v)
17.923 + | nota (Dvd (v, va)) = Not (Dvd (v, va))
17.924 + | nota (NDvd (v, va)) = Not (NDvd (v, va))
17.925 + | nota (And (v, va)) = Not (And (v, va))
17.926 + | nota (Or (v, va)) = Not (Or (v, va))
17.927 + | nota (Imp (v, va)) = Not (Imp (v, va))
17.928 + | nota (Iff (v, va)) = Not (Iff (v, va))
17.929 + | nota (E v) = Not (E v)
17.930 + | nota (A v) = Not (A v)
17.931 | nota (Closed v) = Not (Closed v)
17.932 | nota (NClosed v) = Not (NClosed v);
17.933
17.934 @@ -1184,7 +1183,7 @@
17.935 | delta (Le v) = (1 : IntInf.int)
17.936 | delta (Gt w) = (1 : IntInf.int)
17.937 | delta (Ge x) = (1 : IntInf.int)
17.938 - | delta (Eq ya) = (1 : IntInf.int)
17.939 + | delta (Eq y) = (1 : IntInf.int)
17.940 | delta (NEq z) = (1 : IntInf.int)
17.941 | delta (Dvd (aa, C bo)) = (1 : IntInf.int)
17.942 | delta (Dvd (aa, Bound bp)) = (1 : IntInf.int)
17.943 @@ -1205,10 +1204,10 @@
17.944 | delta (A ao) = (1 : IntInf.int)
17.945 | delta (Closed ap) = (1 : IntInf.int)
17.946 | delta (NClosed aq) = (1 : IntInf.int)
17.947 - | delta (Dvd (b, Cn (cm, c, e))) =
17.948 - (if eqop eq_nat cm 0 then b else (1 : IntInf.int))
17.949 - | delta (NDvd (b, Cn (dm, c, e))) =
17.950 - (if eqop eq_nat dm 0 then b else (1 : IntInf.int));
17.951 + | delta (Dvd (i, Cn (cm, c, e))) =
17.952 + (if eqop eq_nat cm 0 then i else (1 : IntInf.int))
17.953 + | delta (NDvd (i, Cn (dm, c, e))) =
17.954 + (if eqop eq_nat dm 0 then i else (1 : IntInf.int));
17.955
17.956 fun div_int a b = fst (divmoda a b);
17.957
17.958 @@ -1367,22 +1366,22 @@
17.959 | zeta (A ao) = (1 : IntInf.int)
17.960 | zeta (Closed ap) = (1 : IntInf.int)
17.961 | zeta (NClosed aq) = (1 : IntInf.int)
17.962 - | zeta (Lt (Cn (cm, b, e))) =
17.963 - (if eqop eq_nat cm 0 then b else (1 : IntInf.int))
17.964 - | zeta (Le (Cn (dm, b, e))) =
17.965 - (if eqop eq_nat dm 0 then b else (1 : IntInf.int))
17.966 - | zeta (Gt (Cn (em, b, e))) =
17.967 - (if eqop eq_nat em 0 then b else (1 : IntInf.int))
17.968 - | zeta (Ge (Cn (fm, b, e))) =
17.969 - (if eqop eq_nat fm 0 then b else (1 : IntInf.int))
17.970 - | zeta (Eq (Cn (gm, b, e))) =
17.971 - (if eqop eq_nat gm 0 then b else (1 : IntInf.int))
17.972 - | zeta (NEq (Cn (hm, b, e))) =
17.973 - (if eqop eq_nat hm 0 then b else (1 : IntInf.int))
17.974 - | zeta (Dvd (i, Cn (im, b, e))) =
17.975 - (if eqop eq_nat im 0 then b else (1 : IntInf.int))
17.976 - | zeta (NDvd (i, Cn (jm, b, e))) =
17.977 - (if eqop eq_nat jm 0 then b else (1 : IntInf.int));
17.978 + | zeta (Lt (Cn (cm, c, e))) =
17.979 + (if eqop eq_nat cm 0 then c else (1 : IntInf.int))
17.980 + | zeta (Le (Cn (dm, c, e))) =
17.981 + (if eqop eq_nat dm 0 then c else (1 : IntInf.int))
17.982 + | zeta (Gt (Cn (em, c, e))) =
17.983 + (if eqop eq_nat em 0 then c else (1 : IntInf.int))
17.984 + | zeta (Ge (Cn (fm, c, e))) =
17.985 + (if eqop eq_nat fm 0 then c else (1 : IntInf.int))
17.986 + | zeta (Eq (Cn (gm, c, e))) =
17.987 + (if eqop eq_nat gm 0 then c else (1 : IntInf.int))
17.988 + | zeta (NEq (Cn (hm, c, e))) =
17.989 + (if eqop eq_nat hm 0 then c else (1 : IntInf.int))
17.990 + | zeta (Dvd (i, Cn (im, c, e))) =
17.991 + (if eqop eq_nat im 0 then c else (1 : IntInf.int))
17.992 + | zeta (NDvd (i, Cn (jm, c, e))) =
17.993 + (if eqop eq_nat jm 0 then c else (1 : IntInf.int));
17.994
17.995 fun zsplit0 (C c) = ((0 : IntInf.int), C c)
17.996 | zsplit0 (Bound n) =
17.997 @@ -1691,4 +1690,16 @@
17.998 (if IntInf.<= (i, (0 : IntInf.int)) then n
17.999 else nat_aux (IntInf.- (i, (1 : IntInf.int))) (suc n));
17.1000
17.1001 +fun adjust b =
17.1002 + (fn a as (q, r) =>
17.1003 + (if IntInf.<= ((0 : IntInf.int), IntInf.- (r, b))
17.1004 + then (IntInf.+ (IntInf.* ((2 : IntInf.int), q), (1 : IntInf.int)),
17.1005 + IntInf.- (r, b))
17.1006 + else (IntInf.* ((2 : IntInf.int), q), r)));
17.1007 +
17.1008 +fun posDivAlg a b =
17.1009 + (if IntInf.< (a, b) orelse IntInf.<= (b, (0 : IntInf.int))
17.1010 + then ((0 : IntInf.int), a)
17.1011 + else adjust b (posDivAlg a (IntInf.* ((2 : IntInf.int), b))));
17.1012 +
17.1013 end; (*struct GeneratedCooper*)
18.1 --- a/src/HOL/Tools/Qelim/presburger.ML Wed Feb 18 13:39:05 2009 +0100
18.2 +++ b/src/HOL/Tools/Qelim/presburger.ML Wed Feb 18 13:39:16 2009 +0100
18.3 @@ -124,7 +124,7 @@
18.4 @ map (symmetric o mk_meta_eq)
18.5 [@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, @{thm "mod_add1_eq"},
18.6 @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"},
18.7 - @{thm "zmod_zadd1_eq"}, @{thm "zmod_zadd_left_eq"},
18.8 + @{thm "mod_add_eq"}, @{thm "zmod_zadd_left_eq"},
18.9 @{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
18.10 @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"},
18.11 @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1,
19.1 --- a/src/HOL/Tools/refute.ML Wed Feb 18 13:39:05 2009 +0100
19.2 +++ b/src/HOL/Tools/refute.ML Wed Feb 18 13:39:16 2009 +0100
19.3 @@ -2662,6 +2662,34 @@
19.4 (* theory -> model -> arguments -> Term.term ->
19.5 (interpretation * model * arguments) option *)
19.6
19.7 + fun set_interpreter thy model args t =
19.8 + let
19.9 + val (typs, terms) = model
19.10 + in
19.11 + case AList.lookup (op =) terms t of
19.12 + SOME intr =>
19.13 + (* return an existing interpretation *)
19.14 + SOME (intr, model, args)
19.15 + | NONE =>
19.16 + (case t of
19.17 + (* 'Collect' == identity *)
19.18 + Const (@{const_name Collect}, _) $ t1 =>
19.19 + SOME (interpret thy model args t1)
19.20 + | Const (@{const_name Collect}, _) =>
19.21 + SOME (interpret thy model args (eta_expand t 1))
19.22 + (* 'op :' == application *)
19.23 + | Const (@{const_name "op :"}, _) $ t1 $ t2 =>
19.24 + SOME (interpret thy model args (t2 $ t1))
19.25 + | Const (@{const_name "op :"}, _) $ t1 =>
19.26 + SOME (interpret thy model args (eta_expand t 1))
19.27 + | Const (@{const_name "op :"}, _) =>
19.28 + SOME (interpret thy model args (eta_expand t 2))
19.29 + | _ => NONE)
19.30 + end;
19.31 +
19.32 + (* theory -> model -> arguments -> Term.term ->
19.33 + (interpretation * model * arguments) option *)
19.34 +
19.35 (* only an optimization: 'card' could in principle be interpreted with *)
19.36 (* interpreters available already (using its definition), but the code *)
19.37 (* below is more efficient *)
19.38 @@ -3271,6 +3299,7 @@
19.39 add_interpreter "stlc" stlc_interpreter #>
19.40 add_interpreter "Pure" Pure_interpreter #>
19.41 add_interpreter "HOLogic" HOLogic_interpreter #>
19.42 + add_interpreter "set" set_interpreter #>
19.43 add_interpreter "IDT" IDT_interpreter #>
19.44 add_interpreter "IDT_constructor" IDT_constructor_interpreter #>
19.45 add_interpreter "IDT_recursion" IDT_recursion_interpreter #>
20.1 --- a/src/HOL/Word/Num_Lemmas.thy Wed Feb 18 13:39:05 2009 +0100
20.2 +++ b/src/HOL/Word/Num_Lemmas.thy Wed Feb 18 13:39:16 2009 +0100
20.3 @@ -121,8 +121,8 @@
20.4
20.5 lemma zmod_zsub_distrib: "((a::int) - b) mod c = (a mod c - b mod c) mod c"
20.6 apply (unfold diff_int_def)
20.7 - apply (rule trans [OF _ zmod_zadd1_eq [symmetric]])
20.8 - apply (simp add: zmod_uminus zmod_zadd1_eq [symmetric])
20.9 + apply (rule trans [OF _ mod_add_eq [symmetric]])
20.10 + apply (simp add: zmod_uminus mod_add_eq [symmetric])
20.11 done
20.12
20.13 lemma zmod_zsub_right_eq: "((a::int) - b) mod c = (a - b mod c) mod c"
20.14 @@ -162,8 +162,8 @@
20.15 lemmas nat_minus_mod_plus_right = trans [OF nat_minus_mod mod_0 [symmetric],
20.16 THEN mod_plus_right [THEN iffD2], standard, simplified]
20.17
20.18 -lemmas push_mods' = zmod_zadd1_eq [standard]
20.19 - zmod_zmult_distrib [standard] zmod_zsub_distrib [standard]
20.20 +lemmas push_mods' = mod_add_eq [standard]
20.21 + mod_mult_eq [standard] zmod_zsub_distrib [standard]
20.22 zmod_uminus [symmetric, standard]
20.23
20.24 lemmas push_mods = push_mods' [THEN eq_reflection, standard]
21.1 --- a/src/HOL/Word/WordGenLib.thy Wed Feb 18 13:39:05 2009 +0100
21.2 +++ b/src/HOL/Word/WordGenLib.thy Wed Feb 18 13:39:16 2009 +0100
21.3 @@ -293,9 +293,9 @@
21.4 shows "(x + y) mod b = z' mod b'"
21.5 proof -
21.6 from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
21.7 - by (simp add: zmod_zadd1_eq[symmetric])
21.8 + by (simp add: mod_add_eq[symmetric])
21.9 also have "\<dots> = (x' + y') mod b'"
21.10 - by (simp add: zmod_zadd1_eq[symmetric])
21.11 + by (simp add: mod_add_eq[symmetric])
21.12 finally show ?thesis by (simp add: 4)
21.13 qed
21.14
22.1 --- a/src/HOL/ex/Efficient_Nat_examples.thy Wed Feb 18 13:39:05 2009 +0100
22.2 +++ b/src/HOL/ex/Efficient_Nat_examples.thy Wed Feb 18 13:39:16 2009 +0100
22.3 @@ -1,12 +1,11 @@
22.4 (* Title: HOL/ex/Efficient_Nat_examples.thy
22.5 - ID: $Id$
22.6 Author: Florian Haftmann, TU Muenchen
22.7 *)
22.8
22.9 header {* Simple examples for Efficient\_Nat theory. *}
22.10
22.11 theory Efficient_Nat_examples
22.12 -imports Main "~~/src/HOL/Real/RealDef" Efficient_Nat
22.13 +imports Complex_Main Efficient_Nat
22.14 begin
22.15
22.16 fun to_n :: "nat \<Rightarrow> nat list" where
23.1 --- a/src/HOL/ex/Numeral.thy Wed Feb 18 13:39:05 2009 +0100
23.2 +++ b/src/HOL/ex/Numeral.thy Wed Feb 18 13:39:16 2009 +0100
23.3 @@ -1,8 +1,8 @@
23.4 (* Title: HOL/ex/Numeral.thy
23.5 Author: Florian Haftmann
23.6 +*)
23.7
23.8 -An experimental alternative numeral representation.
23.9 -*)
23.10 +header {* An experimental alternative numeral representation. *}
23.11
23.12 theory Numeral
23.13 imports Int Inductive
23.14 @@ -10,238 +10,218 @@
23.15
23.16 subsection {* The @{text num} type *}
23.17
23.18 +datatype num = One | Dig0 num | Dig1 num
23.19 +
23.20 +text {* Increment function for type @{typ num} *}
23.21 +
23.22 +primrec
23.23 + inc :: "num \<Rightarrow> num"
23.24 +where
23.25 + "inc One = Dig0 One"
23.26 +| "inc (Dig0 x) = Dig1 x"
23.27 +| "inc (Dig1 x) = Dig0 (inc x)"
23.28 +
23.29 +text {* Converting between type @{typ num} and type @{typ nat} *}
23.30 +
23.31 +primrec
23.32 + nat_of_num :: "num \<Rightarrow> nat"
23.33 +where
23.34 + "nat_of_num One = Suc 0"
23.35 +| "nat_of_num (Dig0 x) = nat_of_num x + nat_of_num x"
23.36 +| "nat_of_num (Dig1 x) = Suc (nat_of_num x + nat_of_num x)"
23.37 +
23.38 +primrec
23.39 + num_of_nat :: "nat \<Rightarrow> num"
23.40 +where
23.41 + "num_of_nat 0 = One"
23.42 +| "num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)"
23.43 +
23.44 +lemma nat_of_num_pos: "0 < nat_of_num x"
23.45 + by (induct x) simp_all
23.46 +
23.47 +lemma nat_of_num_neq_0: " nat_of_num x \<noteq> 0"
23.48 + by (induct x) simp_all
23.49 +
23.50 +lemma nat_of_num_inc: "nat_of_num (inc x) = Suc (nat_of_num x)"
23.51 + by (induct x) simp_all
23.52 +
23.53 +lemma num_of_nat_double:
23.54 + "0 < n \<Longrightarrow> num_of_nat (n + n) = Dig0 (num_of_nat n)"
23.55 + by (induct n) simp_all
23.56 +
23.57 text {*
23.58 - We construct @{text num} as a copy of strictly positive
23.59 + Type @{typ num} is isomorphic to the strictly positive
23.60 natural numbers.
23.61 *}
23.62
23.63 -typedef (open) num = "\<lambda>n\<Colon>nat. n > 0"
23.64 - morphisms nat_of_num num_of_nat_abs
23.65 - by (auto simp add: mem_def)
23.66 +lemma nat_of_num_inverse: "num_of_nat (nat_of_num x) = x"
23.67 + by (induct x) (simp_all add: num_of_nat_double nat_of_num_pos)
23.68 +
23.69 +lemma num_of_nat_inverse: "0 < n \<Longrightarrow> nat_of_num (num_of_nat n) = n"
23.70 + by (induct n) (simp_all add: nat_of_num_inc)
23.71 +
23.72 +lemma num_eq_iff: "x = y \<longleftrightarrow> nat_of_num x = nat_of_num y"
23.73 + apply safe
23.74 + apply (drule arg_cong [where f=num_of_nat])
23.75 + apply (simp add: nat_of_num_inverse)
23.76 + done
23.77 +
23.78 +lemma num_induct [case_names One inc]:
23.79 + fixes P :: "num \<Rightarrow> bool"
23.80 + assumes One: "P One"
23.81 + and inc: "\<And>x. P x \<Longrightarrow> P (inc x)"
23.82 + shows "P x"
23.83 +proof -
23.84 + obtain n where n: "Suc n = nat_of_num x"
23.85 + by (cases "nat_of_num x", simp_all add: nat_of_num_neq_0)
23.86 + have "P (num_of_nat (Suc n))"
23.87 + proof (induct n)
23.88 + case 0 show ?case using One by simp
23.89 + next
23.90 + case (Suc n)
23.91 + then have "P (inc (num_of_nat (Suc n)))" by (rule inc)
23.92 + then show "P (num_of_nat (Suc (Suc n)))" by simp
23.93 + qed
23.94 + with n show "P x"
23.95 + by (simp add: nat_of_num_inverse)
23.96 +qed
23.97
23.98 text {*
23.99 - A totalized abstraction function. It is not entirely clear
23.100 - whether this is really useful.
23.101 + From now on, there are two possible models for @{typ num}:
23.102 + as positive naturals (rule @{text "num_induct"})
23.103 + and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}).
23.104 +
23.105 + It is not entirely clear in which context it is better to use
23.106 + the one or the other, or whether the construction should be reversed.
23.107 *}
23.108
23.109 -definition num_of_nat :: "nat \<Rightarrow> num" where
23.110 - "num_of_nat n = (if n = 0 then num_of_nat_abs 1 else num_of_nat_abs n)"
23.111
23.112 -lemma num_cases [case_names nat, cases type: num]:
23.113 - assumes "(\<And>n\<Colon>nat. m = num_of_nat n \<Longrightarrow> 0 < n \<Longrightarrow> P)"
23.114 - shows P
23.115 -apply (rule num_of_nat_abs_cases)
23.116 -apply (unfold mem_def)
23.117 -using assms unfolding num_of_nat_def
23.118 -apply auto
23.119 -done
23.120 +subsection {* Numeral operations *}
23.121
23.122 -lemma num_of_nat_zero: "num_of_nat 0 = num_of_nat 1"
23.123 - by (simp add: num_of_nat_def)
23.124 +ML {*
23.125 +structure DigSimps =
23.126 + NamedThmsFun(val name = "numeral"; val description = "Simplification rules for numerals")
23.127 +*}
23.128
23.129 -lemma num_of_nat_inverse: "nat_of_num (num_of_nat n) = (if n = 0 then 1 else n)"
23.130 - apply (simp add: num_of_nat_def)
23.131 - apply (subst num_of_nat_abs_inverse)
23.132 - apply (auto simp add: mem_def num_of_nat_abs_inverse)
23.133 - done
23.134 +setup DigSimps.setup
23.135
23.136 -lemma num_of_nat_inject:
23.137 - "num_of_nat m = num_of_nat n \<longleftrightarrow> m = n \<or> (m = 0 \<or> m = 1) \<and> (n = 0 \<or> n = 1)"
23.138 -by (auto simp add: num_of_nat_def num_of_nat_abs_inject [unfolded mem_def])
23.139 -
23.140 -lemma split_num_all:
23.141 - "(\<And>m. PROP P m) \<equiv> (\<And>n. PROP P (num_of_nat n))"
23.142 -proof
23.143 - fix n
23.144 - assume "\<And>m\<Colon>num. PROP P m"
23.145 - then show "PROP P (num_of_nat n)" .
23.146 -next
23.147 - fix m
23.148 - have nat_of_num: "\<And>m. nat_of_num m \<noteq> 0"
23.149 - using nat_of_num by (auto simp add: mem_def)
23.150 - have nat_of_num_inverse: "\<And>m. num_of_nat (nat_of_num m) = m"
23.151 - by (auto simp add: num_of_nat_def nat_of_num_inverse nat_of_num)
23.152 - assume "\<And>n. PROP P (num_of_nat n)"
23.153 - then have "PROP P (num_of_nat (nat_of_num m))" .
23.154 - then show "PROP P m" unfolding nat_of_num_inverse .
23.155 -qed
23.156 -
23.157 -
23.158 -subsection {* Digit representation for @{typ num} *}
23.159 -
23.160 -instantiation num :: "{semiring, monoid_mult}"
23.161 +instantiation num :: "{plus,times,ord}"
23.162 begin
23.163
23.164 -definition one_num :: num where
23.165 - [code del]: "1 = num_of_nat 1"
23.166 -
23.167 definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where
23.168 [code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
23.169
23.170 definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where
23.171 [code del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
23.172
23.173 -definition Dig0 :: "num \<Rightarrow> num" where
23.174 - [code del]: "Dig0 n = n + n"
23.175 +definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
23.176 + [code del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
23.177
23.178 -definition Dig1 :: "num \<Rightarrow> num" where
23.179 - [code del]: "Dig1 n = n + n + 1"
23.180 +definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
23.181 + [code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
23.182
23.183 -instance proof
23.184 -qed (simp_all add: one_num_def plus_num_def times_num_def
23.185 - split_num_all num_of_nat_inverse num_of_nat_zero add_ac mult_ac nat_distrib)
23.186 +instance ..
23.187
23.188 end
23.189
23.190 -text {*
23.191 - The following proofs seem horribly complicated.
23.192 - Any room for simplification!?
23.193 -*}
23.194 +lemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y"
23.195 + unfolding plus_num_def
23.196 + by (intro num_of_nat_inverse add_pos_pos nat_of_num_pos)
23.197
23.198 -lemma nat_dig_cases [case_names 0 1 dig0 dig1]:
23.199 - fixes n :: nat
23.200 - assumes "n = 0 \<Longrightarrow> P"
23.201 - and "n = 1 \<Longrightarrow> P"
23.202 - and "\<And>m. m > 0 \<Longrightarrow> n = m + m \<Longrightarrow> P"
23.203 - and "\<And>m. m > 0 \<Longrightarrow> n = Suc (m + m) \<Longrightarrow> P"
23.204 - shows P
23.205 -using assms proof (induct n)
23.206 - case 0 then show ?case by simp
23.207 -next
23.208 - case (Suc n)
23.209 - show P proof (rule Suc.hyps)
23.210 - assume "n = 0"
23.211 - then have "Suc n = 1" by simp
23.212 - then show P by (rule Suc.prems(2))
23.213 - next
23.214 - assume "n = 1"
23.215 - have "1 > (0\<Colon>nat)" by simp
23.216 - moreover from `n = 1` have "Suc n = 1 + 1" by simp
23.217 - ultimately show P by (rule Suc.prems(3))
23.218 - next
23.219 - fix m
23.220 - assume "0 < m" and "n = m + m"
23.221 - note `0 < m`
23.222 - moreover from `n = m + m` have "Suc n = Suc (m + m)" by simp
23.223 - ultimately show P by (rule Suc.prems(4))
23.224 - next
23.225 - fix m
23.226 - assume "0 < m" and "n = Suc (m + m)"
23.227 - have "0 < Suc m" by simp
23.228 - moreover from `n = Suc (m + m)` have "Suc n = Suc m + Suc m" by simp
23.229 - ultimately show P by (rule Suc.prems(3))
23.230 - qed
23.231 -qed
23.232 +lemma nat_of_num_mult: "nat_of_num (x * y) = nat_of_num x * nat_of_num y"
23.233 + unfolding times_num_def
23.234 + by (intro num_of_nat_inverse mult_pos_pos nat_of_num_pos)
23.235
23.236 -lemma num_induct_raw:
23.237 - fixes n :: nat
23.238 - assumes not0: "n > 0"
23.239 - assumes "P 1"
23.240 - and "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (n + n)"
23.241 - and "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc (n + n))"
23.242 - shows "P n"
23.243 -using not0 proof (induct n rule: less_induct)
23.244 - case (less n)
23.245 - show "P n" proof (cases n rule: nat_dig_cases)
23.246 - case 0 then show ?thesis using less by simp
23.247 - next
23.248 - case 1 then show ?thesis using assms by simp
23.249 - next
23.250 - case (dig0 m)
23.251 - then show ?thesis apply simp
23.252 - apply (rule assms(3)) apply assumption
23.253 - apply (rule less)
23.254 - apply simp_all
23.255 - done
23.256 - next
23.257 - case (dig1 m)
23.258 - then show ?thesis apply simp
23.259 - apply (rule assms(4)) apply assumption
23.260 - apply (rule less)
23.261 - apply simp_all
23.262 - done
23.263 - qed
23.264 -qed
23.265 +lemma Dig_plus [numeral, simp, code]:
23.266 + "One + One = Dig0 One"
23.267 + "One + Dig0 m = Dig1 m"
23.268 + "One + Dig1 m = Dig0 (m + One)"
23.269 + "Dig0 n + One = Dig1 n"
23.270 + "Dig0 n + Dig0 m = Dig0 (n + m)"
23.271 + "Dig0 n + Dig1 m = Dig1 (n + m)"
23.272 + "Dig1 n + One = Dig0 (n + One)"
23.273 + "Dig1 n + Dig0 m = Dig1 (n + m)"
23.274 + "Dig1 n + Dig1 m = Dig0 (n + m + One)"
23.275 + by (simp_all add: num_eq_iff nat_of_num_add)
23.276
23.277 -lemma num_of_nat_Suc: "num_of_nat (Suc n) = (if n = 0 then 1 else num_of_nat n + 1)"
23.278 - by (cases n) (auto simp add: one_num_def plus_num_def num_of_nat_inverse)
23.279 +lemma Dig_times [numeral, simp, code]:
23.280 + "One * One = One"
23.281 + "One * Dig0 n = Dig0 n"
23.282 + "One * Dig1 n = Dig1 n"
23.283 + "Dig0 n * One = Dig0 n"
23.284 + "Dig0 n * Dig0 m = Dig0 (n * Dig0 m)"
23.285 + "Dig0 n * Dig1 m = Dig0 (n * Dig1 m)"
23.286 + "Dig1 n * One = Dig1 n"
23.287 + "Dig1 n * Dig0 m = Dig0 (n * Dig0 m + m)"
23.288 + "Dig1 n * Dig1 m = Dig1 (n * Dig1 m + m)"
23.289 + by (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult
23.290 + left_distrib right_distrib)
23.291
23.292 -lemma num_induct [case_names 1 Suc, induct type: num]:
23.293 - fixes P :: "num \<Rightarrow> bool"
23.294 - assumes 1: "P 1"
23.295 - and Suc: "\<And>n. P n \<Longrightarrow> P (n + 1)"
23.296 - shows "P n"
23.297 -proof (cases n)
23.298 - case (nat m) then show ?thesis by (induct m arbitrary: n)
23.299 - (auto simp: num_of_nat_Suc intro: 1 Suc split: split_if_asm)
23.300 -qed
23.301 +lemma less_eq_num_code [numeral, simp, code]:
23.302 + "One \<le> n \<longleftrightarrow> True"
23.303 + "Dig0 m \<le> One \<longleftrightarrow> False"
23.304 + "Dig1 m \<le> One \<longleftrightarrow> False"
23.305 + "Dig0 m \<le> Dig0 n \<longleftrightarrow> m \<le> n"
23.306 + "Dig0 m \<le> Dig1 n \<longleftrightarrow> m \<le> n"
23.307 + "Dig1 m \<le> Dig1 n \<longleftrightarrow> m \<le> n"
23.308 + "Dig1 m \<le> Dig0 n \<longleftrightarrow> m < n"
23.309 + using nat_of_num_pos [of n] nat_of_num_pos [of m]
23.310 + by (auto simp add: less_eq_num_def less_num_def)
23.311
23.312 -rep_datatype "1::num" Dig0 Dig1 proof -
23.313 - fix P m
23.314 - assume 1: "P 1"
23.315 - and Dig0: "\<And>m. P m \<Longrightarrow> P (Dig0 m)"
23.316 - and Dig1: "\<And>m. P m \<Longrightarrow> P (Dig1 m)"
23.317 - obtain n where "0 < n" and m: "m = num_of_nat n"
23.318 - by (cases m) auto
23.319 - from `0 < n` have "P (num_of_nat n)" proof (induct n rule: num_induct_raw)
23.320 - case 1 from `0 < n` show ?case .
23.321 - next
23.322 - case 2 with 1 show ?case by (simp add: one_num_def)
23.323 - next
23.324 - case (3 n) then have "P (num_of_nat n)" by auto
23.325 - then have "P (Dig0 (num_of_nat n))" by (rule Dig0)
23.326 - with 3 show ?case by (simp add: Dig0_def plus_num_def num_of_nat_inverse)
23.327 - next
23.328 - case (4 n) then have "P (num_of_nat n)" by auto
23.329 - then have "P (Dig1 (num_of_nat n))" by (rule Dig1)
23.330 - with 4 show ?case by (simp add: Dig1_def one_num_def plus_num_def num_of_nat_inverse)
23.331 - qed
23.332 - with m show "P m" by simp
23.333 -next
23.334 - fix m n
23.335 - show "Dig0 m = Dig0 n \<longleftrightarrow> m = n"
23.336 - apply (cases m) apply (cases n)
23.337 - by (auto simp add: Dig0_def plus_num_def num_of_nat_inverse num_of_nat_inject)
23.338 -next
23.339 - fix m n
23.340 - show "Dig1 m = Dig1 n \<longleftrightarrow> m = n"
23.341 - apply (cases m) apply (cases n)
23.342 - by (auto simp add: Dig1_def plus_num_def num_of_nat_inverse num_of_nat_inject)
23.343 -next
23.344 - fix n
23.345 - show "1 \<noteq> Dig0 n"
23.346 - apply (cases n)
23.347 - by (auto simp add: Dig0_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)
23.348 -next
23.349 - fix n
23.350 - show "1 \<noteq> Dig1 n"
23.351 - apply (cases n)
23.352 - by (auto simp add: Dig1_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)
23.353 -next
23.354 - fix m n
23.355 - have "\<And>n m. n + n \<noteq> Suc (m + m)"
23.356 - proof -
23.357 - fix n m
23.358 - show "n + n \<noteq> Suc (m + m)"
23.359 - proof (induct m arbitrary: n)
23.360 - case 0 then show ?case by (cases n) simp_all
23.361 - next
23.362 - case (Suc m) then show ?case by (cases n) simp_all
23.363 - qed
23.364 - qed
23.365 - then show "Dig0 n \<noteq> Dig1 m"
23.366 - apply (cases n) apply (cases m)
23.367 - by (auto simp add: Dig0_def Dig1_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)
23.368 -qed
23.369 +lemma less_num_code [numeral, simp, code]:
23.370 + "m < One \<longleftrightarrow> False"
23.371 + "One < One \<longleftrightarrow> False"
23.372 + "One < Dig0 n \<longleftrightarrow> True"
23.373 + "One < Dig1 n \<longleftrightarrow> True"
23.374 + "Dig0 m < Dig0 n \<longleftrightarrow> m < n"
23.375 + "Dig0 m < Dig1 n \<longleftrightarrow> m \<le> n"
23.376 + "Dig1 m < Dig1 n \<longleftrightarrow> m < n"
23.377 + "Dig1 m < Dig0 n \<longleftrightarrow> m < n"
23.378 + using nat_of_num_pos [of n] nat_of_num_pos [of m]
23.379 + by (auto simp add: less_eq_num_def less_num_def)
23.380
23.381 -text {*
23.382 - From now on, there are two possible models for @{typ num}:
23.383 - as positive naturals (rules @{text "num_induct"}, @{text "num_cases"})
23.384 - and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}).
23.385 +text {* Rules using @{text One} and @{text inc} as constructors *}
23.386
23.387 - It is not entirely clear in which context it is better to use
23.388 - the one or the other, or whether the construction should be reversed.
23.389 -*}
23.390 +lemma add_One: "x + One = inc x"
23.391 + by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc)
23.392 +
23.393 +lemma add_inc: "x + inc y = inc (x + y)"
23.394 + by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc)
23.395 +
23.396 +lemma mult_One: "x * One = x"
23.397 + by (simp add: num_eq_iff nat_of_num_mult)
23.398 +
23.399 +lemma mult_inc: "x * inc y = x * y + x"
23.400 + by (simp add: num_eq_iff nat_of_num_mult nat_of_num_add nat_of_num_inc)
23.401 +
23.402 +text {* A double-and-decrement function *}
23.403 +
23.404 +primrec DigM :: "num \<Rightarrow> num" where
23.405 + "DigM One = One"
23.406 + | "DigM (Dig0 n) = Dig1 (DigM n)"
23.407 + | "DigM (Dig1 n) = Dig1 (Dig0 n)"
23.408 +
23.409 +lemma DigM_plus_one: "DigM n + One = Dig0 n"
23.410 + by (induct n) simp_all
23.411 +
23.412 +lemma add_One_commute: "One + n = n + One"
23.413 + by (induct n) simp_all
23.414 +
23.415 +lemma one_plus_DigM: "One + DigM n = Dig0 n"
23.416 + unfolding add_One_commute DigM_plus_one ..
23.417 +
23.418 +text {* Squaring and exponentiation *}
23.419 +
23.420 +primrec square :: "num \<Rightarrow> num" where
23.421 + "square One = One"
23.422 +| "square (Dig0 n) = Dig0 (Dig0 (square n))"
23.423 +| "square (Dig1 n) = Dig1 (Dig0 (square n + n))"
23.424 +
23.425 +primrec pow :: "num \<Rightarrow> num \<Rightarrow> num"
23.426 +where
23.427 + "pow x One = x"
23.428 +| "pow x (Dig0 y) = square (pow x y)"
23.429 +| "pow x (Dig1 y) = x * square (pow x y)"
23.430
23.431
23.432 subsection {* Binary numerals *}
23.433 @@ -251,21 +231,17 @@
23.434 structure using @{text of_num}.
23.435 *}
23.436
23.437 -ML {*
23.438 -structure DigSimps =
23.439 - NamedThmsFun(val name = "numeral"; val description = "Simplification rules for numerals")
23.440 -*}
23.441 -
23.442 -setup DigSimps.setup
23.443 -
23.444 class semiring_numeral = semiring + monoid_mult
23.445 begin
23.446
23.447 primrec of_num :: "num \<Rightarrow> 'a" where
23.448 - of_num_one [numeral]: "of_num 1 = 1"
23.449 + of_num_one [numeral]: "of_num One = 1"
23.450 | "of_num (Dig0 n) = of_num n + of_num n"
23.451 | "of_num (Dig1 n) = of_num n + of_num n + 1"
23.452
23.453 +lemma of_num_inc: "of_num (inc x) = of_num x + 1"
23.454 + by (induct x) (simp_all add: add_ac)
23.455 +
23.456 declare of_num.simps [simp del]
23.457
23.458 end
23.459 @@ -275,14 +251,14 @@
23.460 *}
23.461
23.462 ML {*
23.463 -fun mk_num 1 = @{term "1::num"}
23.464 +fun mk_num 1 = @{term One}
23.465 | mk_num k =
23.466 let
23.467 val (l, b) = Integer.div_mod k 2;
23.468 val bit = (if b = 0 then @{term Dig0} else @{term Dig1});
23.469 in bit $ (mk_num l) end;
23.470
23.471 -fun dest_num @{term "1::num"} = 1
23.472 +fun dest_num @{term One} = 1
23.473 | dest_num (@{term Dig0} $ n) = 2 * dest_num n
23.474 | dest_num (@{term Dig1} $ n) = 2 * dest_num n + 1;
23.475
23.476 @@ -301,7 +277,7 @@
23.477 parse_translation {*
23.478 let
23.479 fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)
23.480 - of (0, 1) => Const (@{const_name HOL.one}, dummyT)
23.481 + of (0, 1) => Const (@{const_name One}, dummyT)
23.482 | (n, 0) => Const (@{const_name Dig0}, dummyT) $ num_of_int n
23.483 | (n, 1) => Const (@{const_name Dig1}, dummyT) $ num_of_int n
23.484 else raise Match;
23.485 @@ -322,7 +298,7 @@
23.486 dig 0 (int_of_num' n)
23.487 | int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =
23.488 dig 1 (int_of_num' n)
23.489 - | int_of_num' (Const (@{const_syntax HOL.one}, _)) = 1;
23.490 + | int_of_num' (Const (@{const_syntax One}, _)) = 1;
23.491 fun num_tr' show_sorts T [n] =
23.492 let
23.493 val k = int_of_num' n;
23.494 @@ -336,45 +312,18 @@
23.495 in [(@{const_syntax of_num}, num_tr')] end
23.496 *}
23.497
23.498 -
23.499 -subsection {* Numeral operations *}
23.500 -
23.501 -text {*
23.502 - First, addition and multiplication on digits.
23.503 -*}
23.504 -
23.505 -lemma Dig_plus [numeral, simp, code]:
23.506 - "1 + 1 = Dig0 1"
23.507 - "1 + Dig0 m = Dig1 m"
23.508 - "1 + Dig1 m = Dig0 (m + 1)"
23.509 - "Dig0 n + 1 = Dig1 n"
23.510 - "Dig0 n + Dig0 m = Dig0 (n + m)"
23.511 - "Dig0 n + Dig1 m = Dig1 (n + m)"
23.512 - "Dig1 n + 1 = Dig0 (n + 1)"
23.513 - "Dig1 n + Dig0 m = Dig1 (n + m)"
23.514 - "Dig1 n + Dig1 m = Dig0 (n + m + 1)"
23.515 - by (simp_all add: add_ac Dig0_def Dig1_def)
23.516 -
23.517 -lemma Dig_times [numeral, simp, code]:
23.518 - "1 * 1 = (1::num)"
23.519 - "1 * Dig0 n = Dig0 n"
23.520 - "1 * Dig1 n = Dig1 n"
23.521 - "Dig0 n * 1 = Dig0 n"
23.522 - "Dig0 n * Dig0 m = Dig0 (n * Dig0 m)"
23.523 - "Dig0 n * Dig1 m = Dig0 (n * Dig1 m)"
23.524 - "Dig1 n * 1 = Dig1 n"
23.525 - "Dig1 n * Dig0 m = Dig0 (n * Dig0 m + m)"
23.526 - "Dig1 n * Dig1 m = Dig1 (n * Dig1 m + m)"
23.527 - by (simp_all add: left_distrib right_distrib add_ac Dig0_def Dig1_def)
23.528 +subsection {* Class-specific numeral rules *}
23.529
23.530 text {*
23.531 @{const of_num} is a morphism.
23.532 *}
23.533
23.534 +subsubsection {* Class @{text semiring_numeral} *}
23.535 +
23.536 context semiring_numeral
23.537 begin
23.538
23.539 -abbreviation "Num1 \<equiv> of_num 1"
23.540 +abbreviation "Num1 \<equiv> of_num One"
23.541
23.542 text {*
23.543 Alas, there is still the duplication of @{term 1},
23.544 @@ -386,18 +335,17 @@
23.545 *}
23.546
23.547 lemma of_num_plus_one [numeral]:
23.548 - "of_num n + 1 = of_num (n + 1)"
23.549 - by (rule sym, induct n) (simp_all add: Dig_plus of_num.simps add_ac)
23.550 + "of_num n + 1 = of_num (n + One)"
23.551 + by (rule sym, induct n) (simp_all add: of_num.simps add_ac)
23.552
23.553 lemma of_num_one_plus [numeral]:
23.554 - "1 + of_num n = of_num (n + 1)"
23.555 + "1 + of_num n = of_num (n + One)"
23.556 unfolding of_num_plus_one [symmetric] add_commute ..
23.557
23.558 lemma of_num_plus [numeral]:
23.559 "of_num m + of_num n = of_num (m + n)"
23.560 by (induct n rule: num_induct)
23.561 - (simp_all add: Dig_plus of_num_one semigroup_add_class.add_assoc [symmetric, of m]
23.562 - add_ac of_num_plus_one [symmetric])
23.563 + (simp_all add: add_One add_inc of_num_one of_num_inc add_ac)
23.564
23.565 lemma of_num_times_one [numeral]:
23.566 "of_num n * 1 = of_num n"
23.567 @@ -410,13 +358,13 @@
23.568 lemma of_num_times [numeral]:
23.569 "of_num m * of_num n = of_num (m * n)"
23.570 by (induct n rule: num_induct)
23.571 - (simp_all add: of_num_plus [symmetric]
23.572 - semiring_class.right_distrib right_distrib of_num_one)
23.573 + (simp_all add: of_num_plus [symmetric] mult_One mult_inc
23.574 + semiring_class.right_distrib right_distrib of_num_one of_num_inc)
23.575
23.576 end
23.577
23.578 -text {*
23.579 - Structures with a @{term 0}.
23.580 +subsubsection {*
23.581 + Structures with a zero: class @{text semiring_1}
23.582 *}
23.583
23.584 context semiring_1
23.585 @@ -449,16 +397,13 @@
23.586 lemma nat_of_num_of_num: "nat_of_num = of_num"
23.587 proof
23.588 fix n
23.589 - have "of_num n = nat_of_num n" apply (induct n)
23.590 - apply (simp_all add: of_num.simps)
23.591 - using nat_of_num
23.592 - apply (simp_all add: one_num_def plus_num_def Dig0_def Dig1_def num_of_nat_inverse mem_def)
23.593 - done
23.594 + have "of_num n = nat_of_num n"
23.595 + by (induct n) (simp_all add: of_num.simps)
23.596 then show "nat_of_num n = of_num n" by simp
23.597 qed
23.598
23.599 -text {*
23.600 - Equality.
23.601 +subsubsection {*
23.602 + Equality: class @{text semiring_char_0}
23.603 *}
23.604
23.605 context semiring_char_0
23.606 @@ -467,25 +412,27 @@
23.607 lemma of_num_eq_iff [numeral]:
23.608 "of_num m = of_num n \<longleftrightarrow> m = n"
23.609 unfolding of_nat_of_num [symmetric] nat_of_num_of_num [symmetric]
23.610 - of_nat_eq_iff nat_of_num_inject ..
23.611 + of_nat_eq_iff num_eq_iff ..
23.612
23.613 lemma of_num_eq_one_iff [numeral]:
23.614 - "of_num n = 1 \<longleftrightarrow> n = 1"
23.615 + "of_num n = 1 \<longleftrightarrow> n = One"
23.616 proof -
23.617 - have "of_num n = of_num 1 \<longleftrightarrow> n = 1" unfolding of_num_eq_iff ..
23.618 + have "of_num n = of_num One \<longleftrightarrow> n = One" unfolding of_num_eq_iff ..
23.619 then show ?thesis by (simp add: of_num_one)
23.620 qed
23.621
23.622 lemma one_eq_of_num_iff [numeral]:
23.623 - "1 = of_num n \<longleftrightarrow> n = 1"
23.624 + "1 = of_num n \<longleftrightarrow> n = One"
23.625 unfolding of_num_eq_one_iff [symmetric] by auto
23.626
23.627 end
23.628
23.629 -text {*
23.630 - Comparisons. Could be perhaps more general than here.
23.631 +subsubsection {*
23.632 + Comparisons: class @{text ordered_semidom}
23.633 *}
23.634
23.635 +text {* Could be perhaps more general than here. *}
23.636 +
23.637 lemma (in ordered_semidom) of_num_pos: "0 < of_num n"
23.638 proof -
23.639 have "(0::nat) < of_num n"
23.640 @@ -498,44 +445,6 @@
23.641 ultimately show ?thesis by (simp add: of_nat_of_num)
23.642 qed
23.643
23.644 -instantiation num :: linorder
23.645 -begin
23.646 -
23.647 -definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
23.648 - [code del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
23.649 -
23.650 -definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
23.651 - [code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
23.652 -
23.653 -instance proof
23.654 -qed (auto simp add: less_eq_num_def less_num_def
23.655 - split_num_all num_of_nat_inverse num_of_nat_inject split: split_if_asm)
23.656 -
23.657 -end
23.658 -
23.659 -lemma less_eq_num_code [numeral, simp, code]:
23.660 - "(1::num) \<le> n \<longleftrightarrow> True"
23.661 - "Dig0 m \<le> 1 \<longleftrightarrow> False"
23.662 - "Dig1 m \<le> 1 \<longleftrightarrow> False"
23.663 - "Dig0 m \<le> Dig0 n \<longleftrightarrow> m \<le> n"
23.664 - "Dig0 m \<le> Dig1 n \<longleftrightarrow> m \<le> n"
23.665 - "Dig1 m \<le> Dig1 n \<longleftrightarrow> m \<le> n"
23.666 - "Dig1 m \<le> Dig0 n \<longleftrightarrow> m < n"
23.667 - using of_num_pos [of n, where ?'a = nat] of_num_pos [of m, where ?'a = nat]
23.668 - by (auto simp add: less_eq_num_def less_num_def nat_of_num_of_num of_num.simps)
23.669 -
23.670 -lemma less_num_code [numeral, simp, code]:
23.671 - "m < (1::num) \<longleftrightarrow> False"
23.672 - "(1::num) < 1 \<longleftrightarrow> False"
23.673 - "1 < Dig0 n \<longleftrightarrow> True"
23.674 - "1 < Dig1 n \<longleftrightarrow> True"
23.675 - "Dig0 m < Dig0 n \<longleftrightarrow> m < n"
23.676 - "Dig0 m < Dig1 n \<longleftrightarrow> m \<le> n"
23.677 - "Dig1 m < Dig1 n \<longleftrightarrow> m < n"
23.678 - "Dig1 m < Dig0 n \<longleftrightarrow> m < n"
23.679 - using of_num_pos [of n, where ?'a = nat] of_num_pos [of m, where ?'a = nat]
23.680 - by (auto simp add: less_eq_num_def less_num_def nat_of_num_of_num of_num.simps)
23.681 -
23.682 context ordered_semidom
23.683 begin
23.684
23.685 @@ -546,16 +455,16 @@
23.686 then show ?thesis by (simp add: of_nat_of_num)
23.687 qed
23.688
23.689 -lemma of_num_less_eq_one_iff [numeral]: "of_num n \<le> 1 \<longleftrightarrow> n = 1"
23.690 +lemma of_num_less_eq_one_iff [numeral]: "of_num n \<le> 1 \<longleftrightarrow> n = One"
23.691 proof -
23.692 - have "of_num n \<le> of_num 1 \<longleftrightarrow> n = 1"
23.693 + have "of_num n \<le> of_num One \<longleftrightarrow> n = One"
23.694 by (cases n) (simp_all add: of_num_less_eq_iff)
23.695 then show ?thesis by (simp add: of_num_one)
23.696 qed
23.697
23.698 lemma one_less_eq_of_num_iff [numeral]: "1 \<le> of_num n"
23.699 proof -
23.700 - have "of_num 1 \<le> of_num n"
23.701 + have "of_num One \<le> of_num n"
23.702 by (cases n) (simp_all add: of_num_less_eq_iff)
23.703 then show ?thesis by (simp add: of_num_one)
23.704 qed
23.705 @@ -569,51 +478,24 @@
23.706
23.707 lemma of_num_less_one_iff [numeral]: "\<not> of_num n < 1"
23.708 proof -
23.709 - have "\<not> of_num n < of_num 1"
23.710 + have "\<not> of_num n < of_num One"
23.711 by (cases n) (simp_all add: of_num_less_iff)
23.712 then show ?thesis by (simp add: of_num_one)
23.713 qed
23.714
23.715 -lemma one_less_of_num_iff [numeral]: "1 < of_num n \<longleftrightarrow> n \<noteq> 1"
23.716 +lemma one_less_of_num_iff [numeral]: "1 < of_num n \<longleftrightarrow> n \<noteq> One"
23.717 proof -
23.718 - have "of_num 1 < of_num n \<longleftrightarrow> n \<noteq> 1"
23.719 + have "of_num One < of_num n \<longleftrightarrow> n \<noteq> One"
23.720 by (cases n) (simp_all add: of_num_less_iff)
23.721 then show ?thesis by (simp add: of_num_one)
23.722 qed
23.723
23.724 end
23.725
23.726 -text {*
23.727 - Structures with subtraction @{term "op -"}.
23.728 +subsubsection {*
23.729 + Structures with subtraction: class @{text semiring_1_minus}
23.730 *}
23.731
23.732 -text {* A decrement function *}
23.733 -
23.734 -primrec dec :: "num \<Rightarrow> num" where
23.735 - "dec 1 = 1"
23.736 - | "dec (Dig0 n) = (case n of 1 \<Rightarrow> 1 | _ \<Rightarrow> Dig1 (dec n))"
23.737 - | "dec (Dig1 n) = Dig0 n"
23.738 -
23.739 -declare dec.simps [simp del, code del]
23.740 -
23.741 -lemma Dig_dec [numeral, simp, code]:
23.742 - "dec 1 = 1"
23.743 - "dec (Dig0 1) = 1"
23.744 - "dec (Dig0 (Dig0 n)) = Dig1 (dec (Dig0 n))"
23.745 - "dec (Dig0 (Dig1 n)) = Dig1 (Dig0 n)"
23.746 - "dec (Dig1 n) = Dig0 n"
23.747 - by (simp_all add: dec.simps)
23.748 -
23.749 -lemma Dig_dec_plus_one:
23.750 - "dec n + 1 = (if n = 1 then Dig0 1 else n)"
23.751 - by (induct n)
23.752 - (auto simp add: Dig_plus dec.simps,
23.753 - auto simp add: Dig_plus split: num.splits)
23.754 -
23.755 -lemma Dig_one_plus_dec:
23.756 - "1 + dec n = (if n = 1 then Dig0 1 else n)"
23.757 - unfolding add_commute [of 1] Dig_dec_plus_one ..
23.758 -
23.759 class semiring_minus = semiring + minus + zero +
23.760 assumes minus_inverts_plus1: "a + b = c \<Longrightarrow> c - b = a"
23.761 assumes minus_minus_zero_inverts_plus1: "a + b = c \<Longrightarrow> b - c = 0 - a"
23.762 @@ -645,7 +527,7 @@
23.763 by (rule minus_minus_zero_inverts_plus1) (simp add: of_num_plus assms)
23.764
23.765 lemmas Dig_plus_eval =
23.766 - of_num_plus of_num_eq_iff Dig_plus refl [of "1::num", THEN eqTrueI] num.inject
23.767 + of_num_plus of_num_eq_iff Dig_plus refl [of One, THEN eqTrueI] num.inject
23.768
23.769 simproc_setup numeral_minus ("of_num m - of_num n") = {*
23.770 let
23.771 @@ -683,17 +565,21 @@
23.772 by (simp add: minus_inverts_plus1)
23.773
23.774 lemma Dig_of_num_minus_one [numeral]:
23.775 - "of_num (Dig0 n) - 1 = of_num (dec (Dig0 n))"
23.776 + "of_num (Dig0 n) - 1 = of_num (DigM n)"
23.777 "of_num (Dig1 n) - 1 = of_num (Dig0 n)"
23.778 - by (auto intro: minus_inverts_plus1 simp add: Dig_dec_plus_one of_num.simps of_num_plus_one)
23.779 + by (auto intro: minus_inverts_plus1 simp add: DigM_plus_one of_num.simps of_num_plus_one)
23.780
23.781 lemma Dig_one_minus_of_num [numeral]:
23.782 - "1 - of_num (Dig0 n) = 0 - of_num (dec (Dig0 n))"
23.783 + "1 - of_num (Dig0 n) = 0 - of_num (DigM n)"
23.784 "1 - of_num (Dig1 n) = 0 - of_num (Dig0 n)"
23.785 - by (auto intro: minus_minus_zero_inverts_plus1 simp add: Dig_dec_plus_one of_num.simps of_num_plus_one)
23.786 + by (auto intro: minus_minus_zero_inverts_plus1 simp add: DigM_plus_one of_num.simps of_num_plus_one)
23.787
23.788 end
23.789
23.790 +subsubsection {*
23.791 + Structures with negation: class @{text ring_1}
23.792 +*}
23.793 +
23.794 context ring_1
23.795 begin
23.796
23.797 @@ -735,21 +621,63 @@
23.798
23.799 end
23.800
23.801 -text {*
23.802 +subsubsection {*
23.803 + Structures with exponentiation
23.804 +*}
23.805 +
23.806 +lemma of_num_square: "of_num (square x) = of_num x * of_num x"
23.807 +by (induct x)
23.808 + (simp_all add: of_num.simps of_num_plus [symmetric] algebra_simps)
23.809 +
23.810 +lemma of_num_pow:
23.811 + "(of_num (pow x y)::'a::{semiring_numeral,recpower}) = of_num x ^ of_num y"
23.812 +by (induct y)
23.813 + (simp_all add: of_num.simps of_num_square of_num_times [symmetric]
23.814 + power_Suc power_add)
23.815 +
23.816 +lemma power_of_num [numeral]:
23.817 + "of_num x ^ of_num y = (of_num (pow x y)::'a::{semiring_numeral,recpower})"
23.818 + by (rule of_num_pow [symmetric])
23.819 +
23.820 +lemma power_zero_of_num [numeral]:
23.821 + "0 ^ of_num n = (0::'a::{semiring_0,recpower})"
23.822 + using of_num_pos [where n=n and ?'a=nat]
23.823 + by (simp add: power_0_left)
23.824 +
23.825 +lemma power_minus_one_double:
23.826 + "(- 1) ^ (n + n) = (1::'a::{ring_1,recpower})"
23.827 + by (induct n) (simp_all add: power_Suc)
23.828 +
23.829 +lemma power_minus_Dig0 [numeral]:
23.830 + fixes x :: "'a::{ring_1,recpower}"
23.831 + shows "(- x) ^ of_num (Dig0 n) = x ^ of_num (Dig0 n)"
23.832 + by (subst power_minus)
23.833 + (simp add: of_num.simps power_minus_one_double)
23.834 +
23.835 +lemma power_minus_Dig1 [numeral]:
23.836 + fixes x :: "'a::{ring_1,recpower}"
23.837 + shows "(- x) ^ of_num (Dig1 n) = - (x ^ of_num (Dig1 n))"
23.838 + by (subst power_minus)
23.839 + (simp add: of_num.simps power_Suc power_minus_one_double)
23.840 +
23.841 +declare power_one [numeral]
23.842 +
23.843 +
23.844 +subsubsection {*
23.845 Greetings to @{typ nat}.
23.846 *}
23.847
23.848 instance nat :: semiring_1_minus proof qed simp_all
23.849
23.850 -lemma Suc_of_num [numeral]: "Suc (of_num n) = of_num (n + 1)"
23.851 +lemma Suc_of_num [numeral]: "Suc (of_num n) = of_num (n + One)"
23.852 unfolding of_num_plus_one [symmetric] by simp
23.853
23.854 lemma nat_number:
23.855 "1 = Suc 0"
23.856 - "of_num 1 = Suc 0"
23.857 - "of_num (Dig0 n) = Suc (of_num (dec (Dig0 n)))"
23.858 + "of_num One = Suc 0"
23.859 + "of_num (Dig0 n) = Suc (of_num (DigM n))"
23.860 "of_num (Dig1 n) = Suc (of_num (Dig0 n))"
23.861 - by (simp_all add: of_num.simps Dig_dec_plus_one Suc_of_num)
23.862 + by (simp_all add: of_num.simps DigM_plus_one Suc_of_num)
23.863
23.864 declare diff_0_eq_0 [numeral]
23.865
23.866 @@ -773,17 +701,17 @@
23.867 [code del]: "dup k = 2 * k"
23.868
23.869 lemma Dig_sub [code]:
23.870 - "sub 1 1 = 0"
23.871 - "sub (Dig0 m) 1 = of_num (dec (Dig0 m))"
23.872 - "sub (Dig1 m) 1 = of_num (Dig0 m)"
23.873 - "sub 1 (Dig0 n) = - of_num (dec (Dig0 n))"
23.874 - "sub 1 (Dig1 n) = - of_num (Dig0 n)"
23.875 + "sub One One = 0"
23.876 + "sub (Dig0 m) One = of_num (DigM m)"
23.877 + "sub (Dig1 m) One = of_num (Dig0 m)"
23.878 + "sub One (Dig0 n) = - of_num (DigM n)"
23.879 + "sub One (Dig1 n) = - of_num (Dig0 n)"
23.880 "sub (Dig0 m) (Dig0 n) = dup (sub m n)"
23.881 "sub (Dig1 m) (Dig1 n) = dup (sub m n)"
23.882 "sub (Dig1 m) (Dig0 n) = dup (sub m n) + 1"
23.883 "sub (Dig0 m) (Dig1 n) = dup (sub m n) - 1"
23.884 apply (simp_all add: dup_def algebra_simps)
23.885 - apply (simp_all add: of_num_plus Dig_one_plus_dec)[4]
23.886 + apply (simp_all add: of_num_plus one_plus_DigM)[4]
23.887 apply (simp_all add: of_num.simps)
23.888 done
23.889
23.890 @@ -805,7 +733,7 @@
23.891 by rule+
23.892
23.893 lemma one_int_code [code]:
23.894 - "1 = Pls 1"
23.895 + "1 = Pls One"
23.896 by (simp add: of_num_one)
23.897
23.898 lemma plus_int_code [code]:
24.1 --- a/src/Tools/code/code_funcgr.ML Wed Feb 18 13:39:05 2009 +0100
24.2 +++ b/src/Tools/code/code_funcgr.ML Wed Feb 18 13:39:16 2009 +0100
24.3 @@ -1,8 +1,7 @@
24.4 (* Title: Tools/code/code_funcgr.ML
24.5 - ID: $Id$
24.6 Author: Florian Haftmann, TU Muenchen
24.7
24.8 -Retrieving, normalizing and structuring defining equations in graph
24.9 +Retrieving, normalizing and structuring code equations in graph
24.10 with explicit dependencies.
24.11 *)
24.12
25.1 --- a/src/Tools/code/code_funcgr_new.ML Wed Feb 18 13:39:05 2009 +0100
25.2 +++ b/src/Tools/code/code_funcgr_new.ML Wed Feb 18 13:39:16 2009 +0100
25.3 @@ -1,9 +1,8 @@
25.4 (* Title: Tools/code/code_funcgr.ML
25.5 - ID: $Id$
25.6 Author: Florian Haftmann, TU Muenchen
25.7
25.8 -Retrieving, well-sorting and structuring defining equations in graph
25.9 -with explicit dependencies.
25.10 +Retrieving, well-sorting and structuring code equations in graph
25.11 +with explicit dependencies -- the waisenhaus algorithm.
25.12 *)
25.13
25.14 signature CODE_FUNCGR =
25.15 @@ -28,12 +27,8 @@
25.16
25.17 type T = (((string * sort) list * typ) * (thm * bool) list) Graph.T;
25.18
25.19 -fun eqns funcgr =
25.20 - these o Option.map snd o try (Graph.get_node funcgr);
25.21 -
25.22 -fun typ funcgr =
25.23 - fst o Graph.get_node funcgr;
25.24 -
25.25 +fun eqns funcgr = these o Option.map snd o try (Graph.get_node funcgr);
25.26 +fun typ funcgr = fst o Graph.get_node funcgr;
25.27 fun all funcgr = Graph.keys funcgr;
25.28
25.29 fun pretty thy funcgr =
25.30 @@ -48,23 +43,22 @@
25.31 |> Pretty.chunks;
25.32
25.33
25.34 -(** generic combinators **)
25.35 -
25.36 -fun fold_consts f thms =
25.37 - thms
25.38 - |> maps (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of)
25.39 - |> (fold o fold_aterms) (fn Const c => f c | _ => I);
25.40 -
25.41 -fun consts_of (const, []) = []
25.42 - | consts_of (const, thms as _ :: _) =
25.43 - let
25.44 - fun the_const (c, _) = if c = const then I else insert (op =) c
25.45 - in fold_consts the_const (map fst thms) [] end;
25.46 -
25.47 -
25.48 (** graph algorithm **)
25.49
25.50 -(* some nonsense -- FIXME *)
25.51 +(* generic *)
25.52 +
25.53 +fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
25.54 +
25.55 +fun complete_proper_sort thy =
25.56 + Sign.complete_sort thy #> filter (can (AxClass.get_info thy));
25.57 +
25.58 +fun inst_params thy tyco class =
25.59 + map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
25.60 + ((#params o AxClass.get_info thy) class);
25.61 +
25.62 +fun consts_of thy eqns = [] |> (fold o fold o fold_aterms)
25.63 + (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
25.64 + (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns);
25.65
25.66 fun lhs_rhss_of thy c =
25.67 let
25.68 @@ -73,33 +67,9 @@
25.69 |> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var);
25.70 val (lhs, _) = case eqns of [] => Code.default_typscheme thy c
25.71 | ((thm, _) :: _) => (snd o Code_Unit.head_eqn thy) thm;
25.72 - val rhss = fold_consts (fn (c, ty) =>
25.73 - insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty))) (map fst eqns) [];
25.74 + val rhss = consts_of thy eqns;
25.75 in (lhs, rhss) end;
25.76
25.77 -fun inst_params thy tyco class =
25.78 - map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
25.79 - ((#params o AxClass.get_info thy) class);
25.80 -
25.81 -fun complete_proper_sort thy sort =
25.82 - Sign.complete_sort thy sort |> filter (can (AxClass.get_info thy));
25.83 -
25.84 -fun minimal_proper_sort thy sort =
25.85 - complete_proper_sort thy sort |> Sign.minimize_sort thy;
25.86 -
25.87 -fun dicts_of thy algebra (T, sort) =
25.88 - let
25.89 - fun class_relation (x, _) _ = x;
25.90 - fun type_constructor tyco xs class =
25.91 - inst_params thy tyco class @ (maps o maps) fst xs;
25.92 - fun type_variable (TFree (_, sort)) = map (pair []) sort;
25.93 - in
25.94 - flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
25.95 - { class_relation = class_relation, type_constructor = type_constructor,
25.96 - type_variable = type_variable } (T, minimal_proper_sort thy sort)
25.97 - handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
25.98 - end;
25.99 -
25.100
25.101 (* data structures *)
25.102
25.103 @@ -179,6 +149,7 @@
25.104 val classess = map (complete_proper_sort thy)
25.105 (Sign.arity_sorts thy tyco [class]);
25.106 val inst_params = inst_params thy tyco class;
25.107 + (*FIXME also consider existing things here*)
25.108 in
25.109 vardeps
25.110 |> fold (fn superclass => assert thy (Inst (superclass, tyco))) superclasses
25.111 @@ -199,6 +170,7 @@
25.112 let
25.113 val _ = tracing "add_const";
25.114 val (lhs, rhss) = lhs_rhss_of thy c;
25.115 + (*FIXME build lhs_rhss_of such that it points to existing graph if possible*)
25.116 fun styp_of (Type (tyco, tys)) = Tyco (tyco, map styp_of tys)
25.117 | styp_of (TFree (v, _)) = Var (Fun c, find_index (fn (v', _) => v = v') lhs);
25.118 val rhss' = (map o apsnd o map) styp_of rhss;
25.119 @@ -220,33 +192,62 @@
25.120
25.121 (* applying instantiations *)
25.122
25.123 +fun dicts_of thy (proj_sort, algebra) (T, sort) =
25.124 + let
25.125 + fun class_relation (x, _) _ = x;
25.126 + fun type_constructor tyco xs class =
25.127 + inst_params thy tyco class @ (maps o maps) fst xs;
25.128 + fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
25.129 + in
25.130 + flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
25.131 + { class_relation = class_relation, type_constructor = type_constructor,
25.132 + type_variable = type_variable } (T, proj_sort sort)
25.133 + handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
25.134 + end;
25.135 +
25.136 +fun instances_of (*FIXME move to sorts.ML*) algebra =
25.137 + let
25.138 + val { classes, arities } = Sorts.rep_algebra algebra;
25.139 + val sort_classes = fn cs => filter (member (op = o apsnd fst) cs)
25.140 + (flat (rev (Graph.strong_conn classes)));
25.141 + in
25.142 + Symtab.fold (fn (a, cs) => append ((map (pair a) o sort_classes) cs))
25.143 + arities []
25.144 + end;
25.145 +
25.146 fun algebra_of thy vardeps =
25.147 let
25.148 val pp = Syntax.pp_global thy;
25.149 val thy_algebra = Sign.classes_of thy;
25.150 val is_proper = can (AxClass.get_info thy);
25.151 - val arities = Vargraph.fold (fn ((Fun _, _), _) => I
25.152 + val classrels = Sorts.classrels_of thy_algebra
25.153 + |> filter (is_proper o fst)
25.154 + |> (map o apsnd) (filter is_proper);
25.155 + val instances = instances_of thy_algebra
25.156 + |> filter (is_proper o snd);
25.157 + fun add_class (class, superclasses) algebra =
25.158 + Sorts.add_class pp (class, Sorts.minimize_sort algebra superclasses) algebra;
25.159 + val arity_constraints = Vargraph.fold (fn ((Fun _, _), _) => I
25.160 | ((Inst (class, tyco), k), ((_, classes), _)) =>
25.161 AList.map_default (op =)
25.162 ((tyco, class), replicate (Sign.arity_number thy tyco) [])
25.163 (nth_map k (K classes))) vardeps [];
25.164 - val classrels = Sorts.classrels_of thy_algebra
25.165 - |> filter (is_proper o fst)
25.166 - |> (map o apsnd) (filter is_proper);
25.167 - fun add_arity (tyco, class) = case AList.lookup (op =) arities (tyco, class)
25.168 - of SOME sorts => Sorts.add_arities pp (tyco, [(class, sorts)])
25.169 - | NONE => if Sign.arity_number thy tyco = 0
25.170 - then (tracing (tyco ^ "::" ^ class); Sorts.add_arities pp (tyco, [(class, [])]))
25.171 - else I;
25.172 - val instances = Sorts.instances_of thy_algebra
25.173 - |> filter (is_proper o snd)
25.174 + fun add_arity (tyco, class) algebra =
25.175 + case AList.lookup (op =) arity_constraints (tyco, class)
25.176 + of SOME sorts => (tracing (Pretty.output (Syntax.pretty_arity (ProofContext.init thy)
25.177 + (tyco, sorts, [class])));
25.178 + Sorts.add_arities pp
25.179 + (tyco, [(class, map (Sorts.minimize_sort algebra) sorts)]) algebra)
25.180 + | NONE => if Sign.arity_number thy tyco = 0
25.181 + then Sorts.add_arities pp (tyco, [(class, [])]) algebra
25.182 + else algebra;
25.183 in
25.184 Sorts.empty_algebra
25.185 - |> fold (Sorts.add_class pp) classrels
25.186 + |> fold add_class classrels
25.187 |> fold add_arity instances
25.188 end;
25.189
25.190 -fun add_eqs thy algebra vardeps c gr =
25.191 +fun add_eqs thy (proj_sort, algebra) vardeps c gr =
25.192 let
25.193 val eqns = Code.these_eqns thy c
25.194 |> burrow_fst (Code_Unit.norm_args thy)
25.195 @@ -260,28 +261,27 @@
25.196 val tyscm = case eqns' of [] => Code.default_typscheme thy c
25.197 | ((thm, _) :: _) => (snd o Code_Unit.head_eqn thy) thm;
25.198 val _ = tracing ("tyscm " ^ makestring (map snd (fst tyscm)));
25.199 - val rhss = fold_consts (fn (c, ty) =>
25.200 - insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty))) (map fst eqns') [];
25.201 + val rhss = consts_of thy eqns';
25.202 in
25.203 gr
25.204 |> Graph.new_node (c, (tyscm, eqns'))
25.205 - |> fold (fn (c', Ts) => ensure_eqs_dep thy algebra vardeps c c'
25.206 + |> fold (fn (c', Ts) => ensure_eqs_dep thy (proj_sort, algebra) vardeps c c'
25.207 #-> (fn (vs, _) =>
25.208 - fold2 (ensure_match thy algebra vardeps c) Ts (map snd vs))) rhss
25.209 + fold2 (ensure_match thy (proj_sort, algebra) vardeps c) Ts (map snd vs))) rhss
25.210 |> pair tyscm
25.211 end
25.212 -and ensure_match thy algebra vardeps c T sort gr =
25.213 +and ensure_match thy (proj_sort, algebra) vardeps c T sort gr =
25.214 gr
25.215 - |> fold (fn c' => ensure_eqs_dep thy algebra vardeps c c' #> snd)
25.216 - (dicts_of thy algebra (T, sort))
25.217 -and ensure_eqs_dep thy algebra vardeps c c' gr =
25.218 + |> fold (fn c' => ensure_eqs_dep thy (proj_sort, algebra) vardeps c c' #> snd)
25.219 + (dicts_of thy (proj_sort, algebra) (T, proj_sort sort))
25.220 +and ensure_eqs_dep thy (proj_sort, algebra) vardeps c c' gr =
25.221 gr
25.222 - |> ensure_eqs thy algebra vardeps c'
25.223 + |> ensure_eqs thy (proj_sort, algebra) vardeps c'
25.224 ||> Graph.add_edge (c, c')
25.225 -and ensure_eqs thy algebra vardeps c gr =
25.226 +and ensure_eqs thy (proj_sort, algebra) vardeps c gr =
25.227 case try (Graph.get_node gr) c
25.228 of SOME (tyscm, _) => (tyscm, gr)
25.229 - | NONE => add_eqs thy algebra vardeps c gr;
25.230 + | NONE => add_eqs thy (proj_sort, algebra) vardeps c gr;
25.231
25.232 fun extend_graph thy cs gr =
25.233 let
25.234 @@ -291,13 +291,10 @@
25.235 val _ = tracing "obtaining algebra";
25.236 val algebra = algebra_of thy vardeps;
25.237 val _ = tracing "obtaining equations";
25.238 - val (_, gr) = fold_map (ensure_eqs thy algebra vardeps) cs gr;
25.239 + val proj_sort = complete_proper_sort thy #> Sorts.minimize_sort algebra;
25.240 + val (_, gr') = fold_map (ensure_eqs thy (proj_sort, algebra) vardeps) cs gr;
25.241 val _ = tracing "sort projection";
25.242 - val minimal_proper_sort = fn sort => sort
25.243 - |> Sorts.complete_sort (Sign.classes_of thy)
25.244 - |> filter (can (AxClass.get_info thy))
25.245 - |> Sorts.minimize_sort algebra;
25.246 - in ((minimal_proper_sort, algebra), gr) end;
25.247 + in ((proj_sort, algebra), gr') end;
25.248
25.249
25.250 (** retrieval interfaces **)
25.251 @@ -320,7 +317,7 @@
25.252 insert (op =) (Sign.const_typargs thy (c, Logic.unvarifyT ty), c)) consts' [];
25.253 val typ_matches = maps (fn (tys, c) => tys ~~ map snd (fst (fst (Graph.get_node funcgr' c))))
25.254 const_matches;
25.255 - val dicts = maps (dicts_of thy (snd algebra')) typ_matches;
25.256 + val dicts = maps (dicts_of thy algebra') typ_matches;
25.257 val (algebra'', funcgr'') = extend_graph thy dicts funcgr';
25.258 in (evaluator_lift (evaluator_funcgr algebra'') thm funcgr'', funcgr'') end;
25.259
26.1 --- a/src/Tools/code/code_haskell.ML Wed Feb 18 13:39:05 2009 +0100
26.2 +++ b/src/Tools/code/code_haskell.ML Wed Feb 18 13:39:16 2009 +0100
26.3 @@ -101,7 +101,7 @@
26.4 and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
26.5 and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
26.6 let
26.7 - val (binds, t) = Code_Thingol.unfold_let (ICase cases);
26.8 + val (binds, body) = Code_Thingol.unfold_let (ICase cases);
26.9 fun pr ((pat, ty), t) vars =
26.10 vars
26.11 |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
26.12 @@ -110,20 +110,20 @@
26.13 in
26.14 Pretty.block_enclose (
26.15 str "let {",
26.16 - concat [str "}", str "in", pr_term tyvars thm vars' NOBR t]
26.17 + concat [str "}", str "in", pr_term tyvars thm vars' NOBR body]
26.18 ) ps
26.19 end
26.20 - | pr_case tyvars thm vars fxy (((td, ty), bs as _ :: _), _) =
26.21 + | pr_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) =
26.22 let
26.23 - fun pr (pat, t) =
26.24 + fun pr (pat, body) =
26.25 let
26.26 val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
26.27 - in semicolon [p, str "->", pr_term tyvars thm vars' NOBR t] end;
26.28 + in semicolon [p, str "->", pr_term tyvars thm vars' NOBR body] end;
26.29 in
26.30 Pretty.block_enclose (
26.31 - concat [str "(case", pr_term tyvars thm vars NOBR td, str "of", str "{"],
26.32 + concat [str "(case", pr_term tyvars thm vars NOBR t, str "of", str "{"],
26.33 str "})"
26.34 - ) (map pr bs)
26.35 + ) (map pr clauses)
26.36 end
26.37 | pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
26.38 fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) =
27.1 --- a/src/Tools/code/code_ml.ML Wed Feb 18 13:39:05 2009 +0100
27.2 +++ b/src/Tools/code/code_ml.ML Wed Feb 18 13:39:16 2009 +0100
27.3 @@ -130,7 +130,7 @@
27.4 and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
27.5 and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
27.6 let
27.7 - val (binds, t') = Code_Thingol.unfold_let (ICase cases);
27.8 + val (binds, body) = Code_Thingol.unfold_let (ICase cases);
27.9 fun pr ((pat, ty), t) vars =
27.10 vars
27.11 |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty)
27.12 @@ -139,24 +139,24 @@
27.13 in
27.14 Pretty.chunks [
27.15 [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
27.16 - [str ("in"), Pretty.fbrk, pr_term is_closure thm vars' NOBR t'] |> Pretty.block,
27.17 + [str ("in"), Pretty.fbrk, pr_term is_closure thm vars' NOBR body] |> Pretty.block,
27.18 str ("end")
27.19 ]
27.20 end
27.21 - | pr_case is_closure thm vars fxy (((td, ty), b::bs), _) =
27.22 + | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) =
27.23 let
27.24 - fun pr delim (pat, t) =
27.25 + fun pr delim (pat, body) =
27.26 let
27.27 val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
27.28 in
27.29 - concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR t]
27.30 + concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
27.31 end;
27.32 in
27.33 (Pretty.enclose "(" ")" o single o brackify fxy) (
27.34 str "case"
27.35 - :: pr_term is_closure thm vars NOBR td
27.36 - :: pr "of" b
27.37 - :: map (pr "|") bs
27.38 + :: pr_term is_closure thm vars NOBR t
27.39 + :: pr "of" clause
27.40 + :: map (pr "|") clauses
27.41 )
27.42 end
27.43 | pr_case is_closure thm vars fxy ((_, []), _) = str "raise Fail \"empty case\"";
27.44 @@ -434,26 +434,26 @@
27.45 and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
27.46 and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
27.47 let
27.48 - val (binds, t') = Code_Thingol.unfold_let (ICase cases);
27.49 + val (binds, body) = Code_Thingol.unfold_let (ICase cases);
27.50 fun pr ((pat, ty), t) vars =
27.51 vars
27.52 |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty)
27.53 |>> (fn p => concat
27.54 [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
27.55 val (ps, vars') = fold_map pr binds vars;
27.56 - in Pretty.chunks (ps @| pr_term is_closure thm vars' NOBR t') end
27.57 - | pr_case is_closure thm vars fxy (((td, ty), b::bs), _) =
27.58 + in Pretty.chunks (ps @| pr_term is_closure thm vars' NOBR body) end
27.59 + | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) =
27.60 let
27.61 - fun pr delim (pat, t) =
27.62 + fun pr delim (pat, body) =
27.63 let
27.64 val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
27.65 - in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR t] end;
27.66 + in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
27.67 in
27.68 (Pretty.enclose "(" ")" o single o brackify fxy) (
27.69 str "match"
27.70 - :: pr_term is_closure thm vars NOBR td
27.71 - :: pr "with" b
27.72 - :: map (pr "|") bs
27.73 + :: pr_term is_closure thm vars NOBR t
27.74 + :: pr "with" clause
27.75 + :: map (pr "|") clauses
27.76 )
27.77 end
27.78 | pr_case is_closure thm vars fxy ((_, []), _) = str "failwith \"empty case\"";
28.1 --- a/src/Tools/code/code_thingol.ML Wed Feb 18 13:39:05 2009 +0100
28.2 +++ b/src/Tools/code/code_thingol.ML Wed Feb 18 13:39:16 2009 +0100
28.3 @@ -109,7 +109,7 @@
28.4 let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
28.5
28.6
28.7 -(** language core - types, patterns, expressions **)
28.8 +(** language core - types, terms **)
28.9
28.10 type vname = string;
28.11
28.12 @@ -131,31 +131,6 @@
28.13 | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
28.14 (*see also signature*)
28.15
28.16 -(*
28.17 - variable naming conventions
28.18 -
28.19 - bare names:
28.20 - variable names v
28.21 - class names class
28.22 - type constructor names tyco
28.23 - datatype names dtco
28.24 - const names (general) c (const)
28.25 - constructor names co
28.26 - class parameter names classparam
28.27 - arbitrary name s
28.28 -
28.29 - v, c, co, classparam also annotated with types etc.
28.30 -
28.31 - constructs:
28.32 - sort sort
28.33 - type parameters vs
28.34 - type ty
28.35 - type schemes tysm
28.36 - term t
28.37 - (term as pattern) p
28.38 - instance (class, tyco) inst
28.39 - *)
28.40 -
28.41 val op `$$ = Library.foldl (op `$);
28.42 val op `|--> = Library.foldr (op `|->);
28.43
28.44 @@ -486,6 +461,12 @@
28.45
28.46 (* translation *)
28.47
28.48 +(*FIXME move to code(_unit).ML*)
28.49 +fun get_case_scheme thy c = case Code.get_case_data thy c
28.50 + of SOME (proto_case_scheme as (_, case_pats)) =>
28.51 + SOME (1 + (if null case_pats then 1 else length case_pats), proto_case_scheme)
28.52 + | NONE => NONE
28.53 +
28.54 fun ensure_class thy (algbr as (_, algebra)) funcgr class =
28.55 let
28.56 val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
28.57 @@ -537,16 +518,8 @@
28.58 Global ((class, tyco), yss)
28.59 | class_relation (Local (classrels, v), subclass) superclass =
28.60 Local ((subclass, superclass) :: classrels, v);
28.61 - fun norm_typargs ys =
28.62 - let
28.63 - val raw_sort = map snd ys;
28.64 - val sort = Sorts.minimize_sort algebra raw_sort;
28.65 - in
28.66 - map_filter (fn (y, class) =>
28.67 - if member (op =) sort class then SOME y else NONE) ys
28.68 - end;
28.69 fun type_constructor tyco yss class =
28.70 - Global ((class, tyco), map norm_typargs yss);
28.71 + Global ((class, tyco), (map o map) fst yss);
28.72 fun type_variable (TFree (v, sort)) =
28.73 let
28.74 val sort' = proj_sort sort;
28.75 @@ -669,58 +642,72 @@
28.76 translate_const thy algbr funcgr thm c_ty
28.77 ##>> fold_map (translate_term thy algbr funcgr thm) ts
28.78 #>> (fn (t, ts) => t `$$ ts)
28.79 -and translate_case thy algbr funcgr thm n cases (app as ((c, ty), ts)) =
28.80 +and translate_case thy algbr funcgr thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
28.81 let
28.82 - val (tys, _) =
28.83 - (chop (1 + (if null cases then 1 else length cases)) o fst o strip_type) ty;
28.84 - val dt = nth ts n;
28.85 - val dty = nth tys n;
28.86 - fun is_undefined (Const (c, _)) = Code.is_undefined thy c
28.87 - | is_undefined _ = false;
28.88 - fun mk_case (co, n) t =
28.89 + val (tys, _) = (chop num_args o fst o strip_type o snd) c_ty;
28.90 + val t = nth ts t_pos;
28.91 + val ty = nth tys t_pos;
28.92 + val ts_clause = nth_drop t_pos ts;
28.93 + fun mk_clause (co, num_co_args) t =
28.94 let
28.95 val _ = if (is_some o Code.get_datatype_of_constr thy) co then ()
28.96 else error ("Non-constructor " ^ quote co
28.97 ^ " encountered in case pattern"
28.98 ^ (case thm of NONE => ""
28.99 | SOME thm => ", in equation\n" ^ Display.string_of_thm thm))
28.100 - val (vs, body) = Term.strip_abs_eta n t;
28.101 - val selector = list_comb (Const (co, map snd vs ---> dty), map Free vs);
28.102 - in if is_undefined body then NONE else SOME (selector, body) end;
28.103 - fun mk_ds [] =
28.104 + val (vs, body) = Term.strip_abs_eta num_co_args t;
28.105 + val not_undefined = case body
28.106 + of (Const (c, _)) => not (Code.is_undefined thy c)
28.107 + | _ => true;
28.108 + val pat = list_comb (Const (co, map snd vs ---> ty), map Free vs);
28.109 + in (not_undefined, (pat, body)) end;
28.110 + val clauses = if null case_pats then let val ([v_ty], body) =
28.111 + Term.strip_abs_eta 1 (the_single ts_clause)
28.112 + in [(true, (Free v_ty, body))] end
28.113 + else map (uncurry mk_clause)
28.114 + (AList.make (Code_Unit.no_args thy) case_pats ~~ ts_clause);
28.115 + fun retermify ty (_, (IVar x, body)) =
28.116 + (x, ty) `|-> body
28.117 + | retermify _ (_, (pat, body)) =
28.118 let
28.119 - val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts))
28.120 - in [(Free v_ty, body)] end
28.121 - | mk_ds cases = map_filter (uncurry mk_case)
28.122 - (AList.make (Code_Unit.no_args thy) cases ~~ nth_drop n ts);
28.123 + val (IConst (_, (_, tys)), ts) = unfold_app pat;
28.124 + val vs = map2 (fn IVar x => fn ty => (x, ty)) ts tys;
28.125 + in vs `|--> body end;
28.126 + fun mk_icase const t ty clauses =
28.127 + let
28.128 + val (ts1, ts2) = chop t_pos (map (retermify ty) clauses);
28.129 + in
28.130 + ICase (((t, ty), map_filter (fn (b, d) => if b then SOME d else NONE) clauses),
28.131 + const `$$ (ts1 @ t :: ts2))
28.132 + end;
28.133 in
28.134 - translate_term thy algbr funcgr thm dt
28.135 - ##>> translate_typ thy algbr funcgr dty
28.136 - ##>> fold_map (fn (pat, body) => translate_term thy algbr funcgr thm pat
28.137 - ##>> translate_term thy algbr funcgr thm body) (mk_ds cases)
28.138 - ##>> translate_app_default thy algbr funcgr thm app
28.139 - #>> (fn (((dt, dty), ds), t0) => ICase (((dt, dty), ds), t0))
28.140 + translate_const thy algbr funcgr thm c_ty
28.141 + ##>> translate_term thy algbr funcgr thm t
28.142 + ##>> translate_typ thy algbr funcgr ty
28.143 + ##>> fold_map (fn (b, (pat, body)) => translate_term thy algbr funcgr thm pat
28.144 + ##>> translate_term thy algbr funcgr thm body
28.145 + #>> pair b) clauses
28.146 + #>> (fn (((const, t), ty), ds) => mk_icase const t ty ds)
28.147 end
28.148 -and translate_app thy algbr funcgr thm ((c, ty), ts) = case Code.get_case_data thy c
28.149 - of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in
28.150 - if length ts < i then
28.151 +and translate_app thy algbr funcgr thm ((c, ty), ts) = case get_case_scheme thy c
28.152 + of SOME (case_scheme as (num_args, _)) =>
28.153 + if length ts < num_args then
28.154 let
28.155 val k = length ts;
28.156 - val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
28.157 + val tys = (curry Library.take (num_args - k) o curry Library.drop k o fst o strip_type) ty;
28.158 val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
28.159 val vs = Name.names ctxt "a" tys;
28.160 in
28.161 fold_map (translate_typ thy algbr funcgr) tys
28.162 - ##>> translate_case thy algbr funcgr thm n cases ((c, ty), ts @ map Free vs)
28.163 + ##>> translate_case thy algbr funcgr thm case_scheme ((c, ty), ts @ map Free vs)
28.164 #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
28.165 end
28.166 - else if length ts > i then
28.167 - translate_case thy algbr funcgr thm n cases ((c, ty), Library.take (i, ts))
28.168 - ##>> fold_map (translate_term thy algbr funcgr thm) (Library.drop (i, ts))
28.169 + else if length ts > num_args then
28.170 + translate_case thy algbr funcgr thm case_scheme ((c, ty), Library.take (num_args, ts))
28.171 + ##>> fold_map (translate_term thy algbr funcgr thm) (Library.drop (num_args, ts))
28.172 #>> (fn (t, ts) => t `$$ ts)
28.173 else
28.174 - translate_case thy algbr funcgr thm n cases ((c, ty), ts)
28.175 - end
28.176 + translate_case thy algbr funcgr thm case_scheme ((c, ty), ts)
28.177 | NONE => translate_app_default thy algbr funcgr thm ((c, ty), ts);
28.178
28.179