--- a/src/HOL/Algebra/IntRing.thy Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/Algebra/IntRing.thy Wed Feb 18 13:39:16 2009 +0100
@@ -407,7 +407,7 @@
hence "b mod m = (x * m + a) mod m" by simp
also
- have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq)
+ have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: mod_add_eq)
also
have "\<dots> = a mod m" by simp
finally
--- a/src/HOL/Decision_Procs/cooper_tac.ML Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Wed Feb 18 13:39:16 2009 +0100
@@ -30,7 +30,7 @@
val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
-val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym;
+val int_mod_add_eq = @{thm mod_add_eq} RS sym;
val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
val nat_div_add_eq = @{thm div_add1_eq} RS sym;
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Wed Feb 18 13:39:16 2009 +0100
@@ -34,7 +34,7 @@
val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
-val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym;
+val int_mod_add_eq = @{thm mod_add_eq} RS sym;
val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
val nat_div_add_eq = @{thm div_add1_eq} RS sym;
--- a/src/HOL/Decision_Procs/mir_tac.ML Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Wed Feb 18 13:39:16 2009 +0100
@@ -49,7 +49,7 @@
val nat_mod_add_eq = @{thm "mod_add1_eq"} RS sym;
val nat_mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
val nat_mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
-val int_mod_add_eq = @{thm "zmod_zadd1_eq"} RS sym;
+val int_mod_add_eq = @{thm "mod_add_eq"} RS sym;
val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;
val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;
val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
--- a/src/HOL/Divides.thy Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/Divides.thy Wed Feb 18 13:39:16 2009 +0100
@@ -173,7 +173,7 @@
qed
lemma dvd_imp_mod_0: "a dvd b \<Longrightarrow> b mod a = 0"
-by (unfold dvd_def, auto)
+by (rule dvd_eq_mod_eq_0[THEN iffD1])
lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b"
by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0)
--- a/src/HOL/Induct/Common_Patterns.thy Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/Induct/Common_Patterns.thy Wed Feb 18 13:39:16 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Induct/Common_Patterns.thy
- ID: $Id$
Author: Makarius
*)
--- a/src/HOL/Int.thy Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/Int.thy Wed Feb 18 13:39:16 2009 +0100
@@ -1627,7 +1627,7 @@
context ring_1
begin
-lemma of_int_of_nat:
+lemma of_int_of_nat [nitpick_const_simp]:
"of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
proof (cases "k < 0")
case True then have "0 \<le> - k" by simp
--- a/src/HOL/IntDiv.thy Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/IntDiv.thy Wed Feb 18 13:39:16 2009 +0100
@@ -377,6 +377,11 @@
apply (blast intro: divmod_rel_div_mod [THEN zminus1_lemma, THEN divmod_rel_mod])
done
+lemma zmod_zminus1_not_zero:
+ fixes k l :: int
+ shows "- k mod l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
+ unfolding zmod_zminus1_eq_if by auto
+
lemma zdiv_zminus2: "a div (-b) = (-a::int) div b"
by (cut_tac a = "-a" in zdiv_zminus_zminus, auto)
@@ -393,6 +398,11 @@
"a mod (-b::int) = (if a mod b = 0 then 0 else (a mod b) - b)"
by (simp add: zmod_zminus1_eq_if zmod_zminus2)
+lemma zmod_zminus2_not_zero:
+ fixes k l :: int
+ shows "k mod - l \<noteq> 0 \<Longrightarrow> k mod l \<noteq> 0"
+ unfolding zmod_zminus2_eq_if by auto
+
subsection{*Division of a Number by Itself*}
@@ -441,9 +451,6 @@
lemma zmod_zero [simp]: "(0::int) mod b = 0"
by (simp add: mod_def divmod_def)
-lemma zdiv_minus1: "(0::int) < b ==> -1 div b = -1"
-by (simp add: div_def divmod_def)
-
lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"
by (simp add: mod_def divmod_def)
@@ -719,18 +726,6 @@
apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_mod])
done
-lemma zmod_zmult1_eq': "(a*b) mod (c::int) = ((a mod c) * b) mod c"
-apply (rule trans)
-apply (rule_tac s = "b*a mod c" in trans)
-apply (rule_tac [2] zmod_zmult1_eq)
-apply (simp_all add: mult_commute)
-done
-
-lemma zmod_zmult_distrib: "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c"
-apply (rule zmod_zmult1_eq' [THEN trans])
-apply (rule zmod_zmult1_eq)
-done
-
lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
by (simp add: zdiv_zmult1_eq)
@@ -739,11 +734,6 @@
apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
done
-lemma zmod_zmod_trivial: "(a mod b) mod b = a mod (b::int)"
-apply (case_tac "b = 0", simp)
-apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
-done
-
text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
lemma zadd1_lemma:
@@ -758,11 +748,6 @@
apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_div)
done
-lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
-apply (case_tac "c = 0", simp)
-apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_mod)
-done
-
instance int :: ring_div
proof
fix a b c :: int
@@ -961,7 +946,7 @@
P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
apply (rule iffI, clarify)
apply (erule_tac P="P ?x ?y" in rev_mp)
- apply (subst zmod_zadd1_eq)
+ apply (subst mod_add_eq)
apply (subst zdiv_zadd1_eq)
apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)
txt{*converse direction*}
@@ -974,7 +959,7 @@
P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
apply (rule iffI, clarify)
apply (erule_tac P="P ?x ?y" in rev_mp)
- apply (subst zmod_zadd1_eq)
+ apply (subst mod_add_eq)
apply (subst zdiv_zadd1_eq)
apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)
txt{*converse direction*}
@@ -1047,11 +1032,6 @@
simp)
done
-(*Not clear why this must be proved separately; probably number_of causes
- simplification problems*)
-lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)"
-by auto
-
lemma zdiv_number_of_Bit0 [simp]:
"number_of (Int.Bit0 v) div number_of (Int.Bit0 w) =
number_of v div (number_of w :: int)"
@@ -1078,7 +1058,7 @@
apply (rule_tac [2] mult_left_mono)
apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq
pos_mod_bound)
-apply (subst zmod_zadd1_eq)
+apply (subst mod_add_eq)
apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
apply (rule mod_pos_pos_trivial)
apply (auto simp add: mod_pos_pos_trivial ring_distribs)
@@ -1101,7 +1081,7 @@
(2::int) * (number_of v mod number_of w)"
apply (simp only: number_of_eq numeral_simps)
apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
- not_0_le_lemma neg_zmod_mult_2 add_ac)
+ neg_zmod_mult_2 add_ac)
done
lemma zmod_number_of_Bit1 [simp]:
@@ -1111,7 +1091,7 @@
else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
apply (simp only: number_of_eq numeral_simps)
apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2
- not_0_le_lemma neg_zmod_mult_2 add_ac)
+ neg_zmod_mult_2 add_ac)
done
@@ -1121,7 +1101,7 @@
apply (subgoal_tac "a div b \<le> -1", force)
apply (rule order_trans)
apply (rule_tac a' = "-1" in zdiv_mono1)
-apply (auto simp add: zdiv_minus1)
+apply (auto simp add: div_eq_minus1)
done
lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
@@ -1167,23 +1147,23 @@
lemma zdvd_1_left: "1 dvd (m::int)"
by (rule one_dvd) (* already declared [simp] *)
-lemma zdvd_refl [simp]: "m dvd (m::int)"
- by (rule dvd_refl) (* TODO: declare generic dvd_refl [simp] *)
+lemma zdvd_refl: "m dvd (m::int)"
+ by (rule dvd_refl) (* already declared [simp] *)
lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
by (rule dvd_trans)
-lemma zdvd_zminus_iff[simp]: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
- by (rule dvd_minus_iff)
+lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
+ by (rule dvd_minus_iff) (* already declared [simp] *)
-lemma zdvd_zminus2_iff[simp]: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
- by (rule minus_dvd_iff)
+lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
+ by (rule minus_dvd_iff) (* already declared [simp] *)
-lemma zdvd_abs1[simp]: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
- by (cases "i > 0") (simp_all add: zdvd_zminus2_iff)
+lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
+ by (rule abs_dvd_iff) (* already declared [simp] *)
-lemma zdvd_abs2[simp]: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)"
- by (cases "j > 0") (simp_all add: zdvd_zminus_iff)
+lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)"
+ by (rule dvd_abs_iff) (* already declared [simp] *)
lemma zdvd_anti_sym:
"0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
@@ -1369,7 +1349,7 @@
apply (induct "y", auto)
apply (rule zmod_zmult1_eq [THEN trans])
apply (simp (no_asm_simp))
-apply (rule zmod_zmult_distrib [symmetric])
+apply (rule mod_mult_eq [symmetric])
done
lemma zdiv_int: "int (a div b) = (int a) div (int b)"
@@ -1410,7 +1390,7 @@
IntDiv.zmod_zadd_left_eq [symmetric]
IntDiv.zmod_zadd_right_eq [symmetric]
IntDiv.zmod_zmult1_eq [symmetric]
- IntDiv.zmod_zmult1_eq' [symmetric]
+ mod_mult_left_eq [symmetric]
IntDiv.zpower_zmod
zminus_zmod zdiff_zmod_left zdiff_zmod_right
@@ -1523,6 +1503,40 @@
thus ?lhs by simp
qed
+
+subsection {* Code generation *}
+
+definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
+ "pdivmod k l = (\<bar>k\<bar> div \<bar>l\<bar>, \<bar>k\<bar> mod \<bar>l\<bar>)"
+
+lemma pdivmod_posDivAlg [code]:
+ "pdivmod k l = (if l = 0 then (0, \<bar>k\<bar>) else posDivAlg \<bar>k\<bar> \<bar>l\<bar>)"
+by (subst posDivAlg_div_mod) (simp_all add: pdivmod_def)
+
+lemma divmod_pdivmod: "divmod k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
+ apsnd ((op *) (sgn l)) (if 0 < l \<and> 0 \<le> k \<or> l < 0 \<and> k < 0
+ then pdivmod k l
+ else (let (r, s) = pdivmod k l in
+ if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
+proof -
+ have aux: "\<And>q::int. - k = l * q \<longleftrightarrow> k = l * - q" by auto
+ show ?thesis
+ by (simp add: divmod_mod_div pdivmod_def)
+ (auto simp add: aux not_less not_le zdiv_zminus1_eq_if
+ zmod_zminus1_eq_if zdiv_zminus2_eq_if zmod_zminus2_eq_if)
+qed
+
+lemma divmod_code [code]: "divmod k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else
+ apsnd ((op *) (sgn l)) (if sgn k = sgn l
+ then pdivmod k l
+ else (let (r, s) = pdivmod k l in
+ if s = 0 then (- r, 0) else (- r - 1, \<bar>l\<bar> - s))))"
+proof -
+ 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"
+ by (auto simp add: not_less sgn_if)
+ then show ?thesis by (simp add: divmod_pdivmod)
+qed
+
code_modulename SML
IntDiv Integer
--- a/src/HOL/Library/Code_Integer.thy Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/Library/Code_Integer.thy Wed Feb 18 13:39:16 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Library/Code_Integer.thy
- ID: $Id$
Author: Florian Haftmann, TU Muenchen
*)
@@ -72,6 +71,11 @@
(OCaml "Big'_int.mult'_big'_int")
(Haskell infixl 7 "*")
+code_const pdivmod
+ (SML "(fn k => fn l =>/ IntInf.divMod/ (IntInf.abs k,/ IntInf.abs l))")
+ (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))")
+ (Haskell "(\\k l ->/ divMod/ (abs k)/ (abs l))")
+
code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
(SML "!((_ : IntInf.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
--- a/src/HOL/Library/Efficient_Nat.thy Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy Wed Feb 18 13:39:16 2009 +0100
@@ -105,10 +105,16 @@
This can be accomplished by applying the following transformation rules:
*}
-lemma Suc_if_eq: "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
+lemma Suc_if_eq': "(\<And>n. f (Suc n) = h n) \<Longrightarrow> f 0 = g \<Longrightarrow>
f n = (if n = 0 then g else h (n - 1))"
by (cases n) simp_all
+lemma Suc_if_eq: "(\<And>n. f (Suc n) \<equiv> h n) \<Longrightarrow> f 0 \<equiv> g \<Longrightarrow>
+ f n \<equiv> if n = 0 then g else h (n - 1)"
+ by (rule eq_reflection, rule Suc_if_eq')
+ (rule meta_eq_to_obj_eq, assumption,
+ rule meta_eq_to_obj_eq, assumption)
+
lemma Suc_clause: "(\<And>n. P n (Suc n)) \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> P (n - 1) n"
by (cases n) simp_all
@@ -123,14 +129,14 @@
setup {*
let
-fun remove_suc thy thms =
+fun gen_remove_suc Suc_if_eq dest_judgement thy thms =
let
val vname = Name.variant (map fst
- (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "x";
+ (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "n";
val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT));
fun lhs_of th = snd (Thm.dest_comb
- (fst (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))))));
- fun rhs_of th = snd (Thm.dest_comb (snd (Thm.dest_comb (cprop_of th))));
+ (fst (Thm.dest_comb (dest_judgement (cprop_of th)))));
+ fun rhs_of th = snd (Thm.dest_comb (dest_judgement (cprop_of th)));
fun find_vars ct = (case term_of ct of
(Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))]
| _ $ _ =>
@@ -150,7 +156,7 @@
(Drule.instantiate'
[SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
- @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
+ Suc_if_eq)) (Thm.forall_intr cv' th)
in
case map_filter (fn th'' =>
SOME (th'', singleton
@@ -161,20 +167,26 @@
let val (ths1, ths2) = split_list thps
in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end
end
- in case get_first mk_thms eqs of
- NONE => thms
- | SOME x => remove_suc thy x
+ in get_first mk_thms eqs end;
+
+fun gen_eqn_suc_preproc Suc_if_eq dest_judgement dest_lhs thy thms =
+ let
+ val dest = dest_lhs o prop_of;
+ val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
+ in
+ if forall (can dest) thms andalso exists (contains_suc o dest) thms
+ then perhaps_loop (gen_remove_suc Suc_if_eq dest_judgement thy) thms
+ else NONE
end;
-fun eqn_suc_preproc thy ths =
- let
- val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
- val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc});
- in
- if forall (can dest) ths andalso
- exists (contains_suc o dest) ths
- then remove_suc thy ths else ths
- end;
+fun eqn_suc_preproc thy = map fst
+ #> gen_eqn_suc_preproc
+ @{thm Suc_if_eq} I (fst o Logic.dest_equals) thy
+ #> (Option.map o map) (Code_Unit.mk_eqn thy);
+
+fun eqn_suc_preproc' thy thms = gen_eqn_suc_preproc
+ @{thm Suc_if_eq'} (snd o Thm.dest_comb) (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) thy thms
+ |> the_default thms;
fun remove_suc_clause thy thms =
let
@@ -215,27 +227,11 @@
(map_filter (try dest) (concl_of th :: prems_of th))) ths
then remove_suc_clause thy ths else ths
end;
-
-fun lift f thy eqns1 =
- let
- val eqns2 = burrow_fst Drule.zero_var_indexes_list eqns1;
- val thms3 = try (map fst
- #> map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
- #> f thy
- #> map (fn thm => thm RS @{thm eq_reflection})
- #> map (Conv.fconv_rule Drule.beta_eta_conversion)) eqns2;
- val thms4 = Option.map Drule.zero_var_indexes_list thms3;
- in case thms4
- of NONE => NONE
- | SOME thms4 => if Thm.eq_thms (map fst eqns2, thms4)
- then NONE else SOME (map (apfst (AxClass.overload thy) o Code_Unit.mk_eqn thy) thms4)
- end
-
in
- Codegen.add_preprocessor eqn_suc_preproc
+ Codegen.add_preprocessor eqn_suc_preproc'
#> Codegen.add_preprocessor clause_suc_preproc
- #> Code.add_functrans ("eqn_Suc", lift eqn_suc_preproc)
+ #> Code.add_functrans ("eqn_Suc", eqn_suc_preproc)
end;
*}
--- a/src/HOL/Library/Enum.thy Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/Library/Enum.thy Wed Feb 18 13:39:16 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Library/Enum.thy
- ID: $Id$
Author: Florian Haftmann, TU Muenchen
*)
--- a/src/HOL/NumberTheory/Chinese.thy Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/NumberTheory/Chinese.thy Wed Feb 18 13:39:16 2009 +0100
@@ -101,7 +101,7 @@
apply (induct l)
apply auto
apply (rule trans)
- apply (rule zmod_zadd1_eq)
+ apply (rule mod_add_eq)
apply simp
apply (rule zmod_zadd_right_eq [symmetric])
done
@@ -237,10 +237,10 @@
apply (unfold lincong_sol_def)
apply safe
apply (tactic {* stac (thm "zcong_zmod") 3 *})
- apply (tactic {* stac (thm "zmod_zmult_distrib") 3 *})
+ apply (tactic {* stac (thm "mod_mult_eq") 3 *})
apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *})
apply (tactic {* stac (thm "x_sol_lin") 5 *})
- apply (tactic {* stac (thm "zmod_zmult_distrib" RS sym) 7 *})
+ apply (tactic {* stac (thm "mod_mult_eq" RS sym) 7 *})
apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *})
apply (subgoal_tac [7]
"0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
--- a/src/HOL/NumberTheory/IntPrimes.thy Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.thy Wed Feb 18 13:39:16 2009 +0100
@@ -88,7 +88,7 @@
lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k) n = zgcd m n"
apply (rule zgcd_eq [THEN trans])
- apply (simp add: zmod_zadd1_eq)
+ apply (simp add: mod_add_eq)
apply (rule zgcd_eq [symmetric])
done
--- a/src/HOL/NumberTheory/Residues.thy Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/NumberTheory/Residues.thy Wed Feb 18 13:39:16 2009 +0100
@@ -53,7 +53,7 @@
lemma StandardRes_prop4: "2 < m
==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)"
by (auto simp add: StandardRes_def zcong_zmod_eq
- zmod_zmult_distrib [of x y m])
+ mod_mult_eq [of x y m])
lemma StandardRes_lbound: "0 < p ==> 0 \<le> StandardRes p x"
by (auto simp add: StandardRes_def pos_mod_sign)
--- a/src/HOL/Rational.thy Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/Rational.thy Wed Feb 18 13:39:16 2009 +0100
@@ -886,14 +886,13 @@
finally show ?thesis using assms by simp
qed
-lemma rat_less_eq_code [code]:
- "Fract a b \<le> Fract c d \<longleftrightarrow> (if b = 0
- then sgn c * sgn d \<ge> 0
- else if d = 0
- then sgn a * sgn b \<le> 0
- else a * \<bar>d\<bar> * sgn b \<le> c * \<bar>b\<bar> * sgn d)"
-by (auto simp add: sgn_times mult_le_0_iff zero_le_mult_iff le_rat' eq_rat simp del: le_rat)
- (auto simp add: sgn_times sgn_0_0 le_less sgn_1_pos [symmetric] sgn_1_neg [symmetric])
+lemma (in ordered_idom) sgn_greater [simp]:
+ "0 < sgn a \<longleftrightarrow> 0 < a"
+ unfolding sgn_if by auto
+
+lemma (in ordered_idom) sgn_less [simp]:
+ "sgn a < 0 \<longleftrightarrow> a < 0"
+ unfolding sgn_if by auto
lemma rat_le_eq_code [code]:
"Fract a b < Fract c d \<longleftrightarrow> (if b = 0
@@ -901,9 +900,17 @@
else if d = 0
then sgn a * sgn b < 0
else a * \<bar>d\<bar> * sgn b < c * \<bar>b\<bar> * sgn d)"
-by (auto simp add: sgn_times mult_less_0_iff zero_less_mult_iff less_rat' eq_rat simp del: less_rat)
- (auto simp add: sgn_times sgn_0_0 sgn_1_pos [symmetric] sgn_1_neg [symmetric],
- auto simp add: sgn_1_pos)
+ by (auto simp add: sgn_times mult_less_0_iff zero_less_mult_iff less_rat' eq_rat simp del: less_rat)
+
+lemma rat_less_eq_code [code]:
+ "Fract a b \<le> Fract c d \<longleftrightarrow> (if b = 0
+ then sgn c * sgn d \<ge> 0
+ else if d = 0
+ then sgn a * sgn b \<le> 0
+ else a * \<bar>d\<bar> * sgn b \<le> c * \<bar>b\<bar> * sgn d)"
+ by (auto simp add: sgn_times mult_le_0_iff zero_le_mult_iff le_rat' eq_rat simp del: le_rat)
+ (auto simp add: le_less not_less sgn_0_0)
+
lemma rat_plus_code [code]:
"Fract a b + Fract c d = (if b = 0
--- a/src/HOL/Ring_and_Field.thy Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy Wed Feb 18 13:39:16 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Ring_and_Field.thy
- ID: $Id$
Author: Gertrud Bauer, Steven Obua, Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel,
with contributions by Jeremy Avigad
*)
@@ -1078,6 +1077,14 @@
"sgn a = - 1 \<longleftrightarrow> a < 0"
unfolding sgn_if by (auto simp add: equal_neg_zero)
+lemma sgn_pos [simp]:
+ "0 < a \<Longrightarrow> sgn a = 1"
+unfolding sgn_1_pos .
+
+lemma sgn_neg [simp]:
+ "a < 0 \<Longrightarrow> sgn a = - 1"
+unfolding sgn_1_neg .
+
lemma sgn_times:
"sgn (a * b) = sgn a * sgn b"
by (auto simp add: sgn_if zero_less_mult_iff)
@@ -1085,32 +1092,19 @@
lemma abs_sgn: "abs k = k * sgn k"
unfolding sgn_if abs_if by auto
-(* The int instances are proved, these generic ones are tedious to prove here.
-And not very useful, as int seems to be the only instance.
-If needed, they should be proved later, when metis is available.
-lemma dvd_abs[simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
-proof-
- have "\<forall>k.\<exists>ka. - (m * k) = m * ka"
- by(simp add: mult_minus_right[symmetric] del: mult_minus_right)
- moreover
- have "\<forall>k.\<exists>ka. m * k = - (m * ka)"
- by(auto intro!: minus_minus[symmetric]
- simp add: mult_minus_right[symmetric] simp del: mult_minus_right)
- ultimately show ?thesis by (auto simp: abs_if dvd_def)
-qed
-
-lemma dvd_abs2[simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
-proof-
- have "\<forall>k.\<exists>ka. - (m * k) = m * ka"
- by(simp add: mult_minus_right[symmetric] del: mult_minus_right)
- moreover
- have "\<forall>k.\<exists>ka. - (m * ka) = m * k"
- by(auto intro!: minus_minus
- simp add: mult_minus_right[symmetric] simp del: mult_minus_right)
- ultimately show ?thesis
- by (auto simp add:abs_if dvd_def minus_equation_iff[of k])
-qed
-*)
+lemma sgn_greater [simp]:
+ "0 < sgn a \<longleftrightarrow> 0 < a"
+ unfolding sgn_if by auto
+
+lemma sgn_less [simp]:
+ "sgn a < 0 \<longleftrightarrow> a < 0"
+ unfolding sgn_if by auto
+
+lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
+ by (simp add: abs_if)
+
+lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
+ by (simp add: abs_if)
end
--- a/src/HOL/Tools/Qelim/generated_cooper.ML Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/Tools/Qelim/generated_cooper.ML Wed Feb 18 13:39:16 2009 +0100
@@ -15,13 +15,13 @@
fun divmod n m = (if eqop eq_nat m 0 then (0, n) else IntInf.divMod (n, m));
-fun snd (a, y) = y;
+fun snd (a, b) = b;
fun mod_nat m n = snd (divmod m n);
fun gcd m n = (if eqop eq_nat n 0 then m else gcd n (mod_nat m n));
-fun fst (y, b) = y;
+fun fst (a, b) = a;
fun div_nat m n = fst (divmod m n);
@@ -48,7 +48,7 @@
fun map f [] = []
| map f (x :: xs) = f x :: map f xs;
-fun append [] y = y
+fun append [] ys = ys
| append (x :: xs) ys = x :: append xs ys;
fun disjuncts (Or (p, q)) = append (disjuncts p) (disjuncts q)
@@ -105,53 +105,53 @@
(Le num) = f4 num
| fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19
(Lt num) = f3 num
- | fm_case f1 y f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 F
- = y
- | fm_case y f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 T
- = y;
+ | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 F
+ = f2
+ | fm_case f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 T
+ = f1;
-fun eq_num (Mul (cb, dc)) (Sub (ae, be)) = false
- | eq_num (Mul (cb, dc)) (Add (ae, be)) = false
- | eq_num (Sub (cc, dc)) (Add (ae, be)) = false
- | eq_num (Mul (bd, cc)) (Neg ae) = false
- | eq_num (Sub (be, cc)) (Neg ae) = false
- | eq_num (Add (be, cc)) (Neg ae) = false
- | eq_num (Mul (db, ea)) (Cn (ac, bd, cc)) = false
- | eq_num (Sub (dc, ea)) (Cn (ac, bd, cc)) = false
- | eq_num (Add (dc, ea)) (Cn (ac, bd, cc)) = false
- | eq_num (Neg dc) (Cn (ac, bd, cc)) = false
- | eq_num (Mul (bd, cc)) (Bound ac) = false
- | eq_num (Sub (be, cc)) (Bound ac) = false
- | eq_num (Add (be, cc)) (Bound ac) = false
- | eq_num (Neg be) (Bound ac) = false
- | eq_num (Cn (bc, cb, dc)) (Bound ac) = false
- | eq_num (Mul (bd, cc)) (C ad) = false
- | eq_num (Sub (be, cc)) (C ad) = false
- | eq_num (Add (be, cc)) (C ad) = false
- | eq_num (Neg be) (C ad) = false
- | eq_num (Cn (bc, cb, dc)) (C ad) = false
- | eq_num (Bound bc) (C ad) = false
- | eq_num (Sub (ab, bb)) (Mul (c, da)) = false
- | eq_num (Add (ab, bb)) (Mul (c, da)) = false
- | eq_num (Add (ab, bb)) (Sub (ca, da)) = false
- | eq_num (Neg ab) (Mul (ba, ca)) = false
- | eq_num (Neg ab) (Sub (bb, ca)) = false
- | eq_num (Neg ab) (Add (bb, ca)) = false
- | eq_num (Cn (a, ba, ca)) (Mul (d, e)) = false
- | eq_num (Cn (a, ba, ca)) (Sub (da, e)) = false
- | eq_num (Cn (a, ba, ca)) (Add (da, e)) = false
- | eq_num (Cn (a, ba, ca)) (Neg da) = false
- | eq_num (Bound a) (Mul (ba, ca)) = false
- | eq_num (Bound a) (Sub (bb, ca)) = false
- | eq_num (Bound a) (Add (bb, ca)) = false
- | eq_num (Bound a) (Neg bb) = false
- | eq_num (Bound a) (Cn (b, c, da)) = false
- | eq_num (C aa) (Mul (ba, ca)) = false
- | eq_num (C aa) (Sub (bb, ca)) = false
- | eq_num (C aa) (Add (bb, ca)) = false
- | eq_num (C aa) (Neg bb) = false
- | eq_num (C aa) (Cn (b, c, da)) = false
- | eq_num (C aa) (Bound b) = false
+fun eq_num (Mul (c, d)) (Sub (a, b)) = false
+ | eq_num (Mul (c, d)) (Add (a, b)) = false
+ | eq_num (Sub (c, d)) (Add (a, b)) = false
+ | eq_num (Mul (b, c)) (Neg a) = false
+ | eq_num (Sub (b, c)) (Neg a) = false
+ | eq_num (Add (b, c)) (Neg a) = false
+ | eq_num (Mul (d, e)) (Cn (a, b, c)) = false
+ | eq_num (Sub (d, e)) (Cn (a, b, c)) = false
+ | eq_num (Add (d, e)) (Cn (a, b, c)) = false
+ | eq_num (Neg d) (Cn (a, b, c)) = false
+ | eq_num (Mul (b, c)) (Bound a) = false
+ | eq_num (Sub (b, c)) (Bound a) = false
+ | eq_num (Add (b, c)) (Bound a) = false
+ | eq_num (Neg b) (Bound a) = false
+ | eq_num (Cn (b, c, d)) (Bound a) = false
+ | eq_num (Mul (b, c)) (C a) = false
+ | eq_num (Sub (b, c)) (C a) = false
+ | eq_num (Add (b, c)) (C a) = false
+ | eq_num (Neg b) (C a) = false
+ | eq_num (Cn (b, c, d)) (C a) = false
+ | eq_num (Bound b) (C a) = false
+ | eq_num (Sub (a, b)) (Mul (c, d)) = false
+ | eq_num (Add (a, b)) (Mul (c, d)) = false
+ | eq_num (Add (a, b)) (Sub (c, d)) = false
+ | eq_num (Neg a) (Mul (b, c)) = false
+ | eq_num (Neg a) (Sub (b, c)) = false
+ | eq_num (Neg a) (Add (b, c)) = false
+ | eq_num (Cn (a, b, c)) (Mul (d, e)) = false
+ | eq_num (Cn (a, b, c)) (Sub (d, e)) = false
+ | eq_num (Cn (a, b, c)) (Add (d, e)) = false
+ | eq_num (Cn (a, b, c)) (Neg d) = false
+ | eq_num (Bound a) (Mul (b, c)) = false
+ | eq_num (Bound a) (Sub (b, c)) = false
+ | eq_num (Bound a) (Add (b, c)) = false
+ | eq_num (Bound a) (Neg b) = false
+ | eq_num (Bound a) (Cn (b, c, d)) = false
+ | eq_num (C a) (Mul (b, c)) = false
+ | eq_num (C a) (Sub (b, c)) = false
+ | eq_num (C a) (Add (b, c)) = false
+ | eq_num (C a) (Neg b) = false
+ | eq_num (C a) (Cn (b, c, d)) = false
+ | eq_num (C a) (Bound b) = false
| eq_num (Mul (inta, num)) (Mul (int', num')) =
((inta : IntInf.int) = int') andalso eq_num num num'
| eq_num (Sub (num1, num2)) (Sub (num1', num2')) =
@@ -165,347 +165,347 @@
| eq_num (Bound nat) (Bound nat') = ((nat : IntInf.int) = nat')
| eq_num (C inta) (C int') = ((inta : IntInf.int) = int');
-fun eq_fm (NClosed bd) (Closed ad) = false
- | eq_fm (NClosed bd) (A af) = false
- | eq_fm (Closed bd) (A af) = false
- | eq_fm (NClosed bd) (E af) = false
- | eq_fm (Closed bd) (E af) = false
- | eq_fm (A bf) (E af) = false
- | eq_fm (NClosed cd) (Iff (af, bf)) = false
- | eq_fm (Closed cd) (Iff (af, bf)) = false
- | eq_fm (A cf) (Iff (af, bf)) = false
- | eq_fm (E cf) (Iff (af, bf)) = false
- | eq_fm (NClosed cd) (Imp (af, bf)) = false
- | eq_fm (Closed cd) (Imp (af, bf)) = false
- | eq_fm (A cf) (Imp (af, bf)) = false
- | eq_fm (E cf) (Imp (af, bf)) = false
- | eq_fm (Iff (cf, db)) (Imp (af, bf)) = false
- | eq_fm (NClosed cd) (Or (af, bf)) = false
- | eq_fm (Closed cd) (Or (af, bf)) = false
- | eq_fm (A cf) (Or (af, bf)) = false
- | eq_fm (E cf) (Or (af, bf)) = false
- | eq_fm (Iff (cf, db)) (Or (af, bf)) = false
- | eq_fm (Imp (cf, db)) (Or (af, bf)) = false
- | eq_fm (NClosed cd) (And (af, bf)) = false
- | eq_fm (Closed cd) (And (af, bf)) = false
- | eq_fm (A cf) (And (af, bf)) = false
- | eq_fm (E cf) (And (af, bf)) = false
- | eq_fm (Iff (cf, db)) (And (af, bf)) = false
- | eq_fm (Imp (cf, db)) (And (af, bf)) = false
- | eq_fm (Or (cf, db)) (And (af, bf)) = false
- | eq_fm (NClosed bd) (Not af) = false
- | eq_fm (Closed bd) (Not af) = false
- | eq_fm (A bf) (Not af) = false
- | eq_fm (E bf) (Not af) = false
- | eq_fm (Iff (bf, cf)) (Not af) = false
- | eq_fm (Imp (bf, cf)) (Not af) = false
- | eq_fm (Or (bf, cf)) (Not af) = false
- | eq_fm (And (bf, cf)) (Not af) = false
- | eq_fm (NClosed cd) (NDvd (ae, bg)) = false
- | eq_fm (Closed cd) (NDvd (ae, bg)) = false
- | eq_fm (A cf) (NDvd (ae, bg)) = false
- | eq_fm (E cf) (NDvd (ae, bg)) = false
- | eq_fm (Iff (cf, db)) (NDvd (ae, bg)) = false
- | eq_fm (Imp (cf, db)) (NDvd (ae, bg)) = false
- | eq_fm (Or (cf, db)) (NDvd (ae, bg)) = false
- | eq_fm (And (cf, db)) (NDvd (ae, bg)) = false
- | eq_fm (Not cf) (NDvd (ae, bg)) = false
- | eq_fm (NClosed cd) (Dvd (ae, bg)) = false
- | eq_fm (Closed cd) (Dvd (ae, bg)) = false
- | eq_fm (A cf) (Dvd (ae, bg)) = false
- | eq_fm (E cf) (Dvd (ae, bg)) = false
- | eq_fm (Iff (cf, db)) (Dvd (ae, bg)) = false
- | eq_fm (Imp (cf, db)) (Dvd (ae, bg)) = false
- | eq_fm (Or (cf, db)) (Dvd (ae, bg)) = false
- | eq_fm (And (cf, db)) (Dvd (ae, bg)) = false
- | eq_fm (Not cf) (Dvd (ae, bg)) = false
- | eq_fm (NDvd (ce, dc)) (Dvd (ae, bg)) = false
- | eq_fm (NClosed bd) (NEq ag) = false
- | eq_fm (Closed bd) (NEq ag) = false
- | eq_fm (A bf) (NEq ag) = false
- | eq_fm (E bf) (NEq ag) = false
- | eq_fm (Iff (bf, cf)) (NEq ag) = false
- | eq_fm (Imp (bf, cf)) (NEq ag) = false
- | eq_fm (Or (bf, cf)) (NEq ag) = false
- | eq_fm (And (bf, cf)) (NEq ag) = false
- | eq_fm (Not bf) (NEq ag) = false
- | eq_fm (NDvd (be, cg)) (NEq ag) = false
- | eq_fm (Dvd (be, cg)) (NEq ag) = false
- | eq_fm (NClosed bd) (Eq ag) = false
- | eq_fm (Closed bd) (Eq ag) = false
- | eq_fm (A bf) (Eq ag) = false
- | eq_fm (E bf) (Eq ag) = false
- | eq_fm (Iff (bf, cf)) (Eq ag) = false
- | eq_fm (Imp (bf, cf)) (Eq ag) = false
- | eq_fm (Or (bf, cf)) (Eq ag) = false
- | eq_fm (And (bf, cf)) (Eq ag) = false
- | eq_fm (Not bf) (Eq ag) = false
- | eq_fm (NDvd (be, cg)) (Eq ag) = false
- | eq_fm (Dvd (be, cg)) (Eq ag) = false
- | eq_fm (NEq bg) (Eq ag) = false
- | eq_fm (NClosed bd) (Ge ag) = false
- | eq_fm (Closed bd) (Ge ag) = false
- | eq_fm (A bf) (Ge ag) = false
- | eq_fm (E bf) (Ge ag) = false
- | eq_fm (Iff (bf, cf)) (Ge ag) = false
- | eq_fm (Imp (bf, cf)) (Ge ag) = false
- | eq_fm (Or (bf, cf)) (Ge ag) = false
- | eq_fm (And (bf, cf)) (Ge ag) = false
- | eq_fm (Not bf) (Ge ag) = false
- | eq_fm (NDvd (be, cg)) (Ge ag) = false
- | eq_fm (Dvd (be, cg)) (Ge ag) = false
- | eq_fm (NEq bg) (Ge ag) = false
- | eq_fm (Eq bg) (Ge ag) = false
- | eq_fm (NClosed bd) (Gt ag) = false
- | eq_fm (Closed bd) (Gt ag) = false
- | eq_fm (A bf) (Gt ag) = false
- | eq_fm (E bf) (Gt ag) = false
- | eq_fm (Iff (bf, cf)) (Gt ag) = false
- | eq_fm (Imp (bf, cf)) (Gt ag) = false
- | eq_fm (Or (bf, cf)) (Gt ag) = false
- | eq_fm (And (bf, cf)) (Gt ag) = false
- | eq_fm (Not bf) (Gt ag) = false
- | eq_fm (NDvd (be, cg)) (Gt ag) = false
- | eq_fm (Dvd (be, cg)) (Gt ag) = false
- | eq_fm (NEq bg) (Gt ag) = false
- | eq_fm (Eq bg) (Gt ag) = false
- | eq_fm (Ge bg) (Gt ag) = false
- | eq_fm (NClosed bd) (Le ag) = false
- | eq_fm (Closed bd) (Le ag) = false
- | eq_fm (A bf) (Le ag) = false
- | eq_fm (E bf) (Le ag) = false
- | eq_fm (Iff (bf, cf)) (Le ag) = false
- | eq_fm (Imp (bf, cf)) (Le ag) = false
- | eq_fm (Or (bf, cf)) (Le ag) = false
- | eq_fm (And (bf, cf)) (Le ag) = false
- | eq_fm (Not bf) (Le ag) = false
- | eq_fm (NDvd (be, cg)) (Le ag) = false
- | eq_fm (Dvd (be, cg)) (Le ag) = false
- | eq_fm (NEq bg) (Le ag) = false
- | eq_fm (Eq bg) (Le ag) = false
- | eq_fm (Ge bg) (Le ag) = false
- | eq_fm (Gt bg) (Le ag) = false
- | eq_fm (NClosed bd) (Lt ag) = false
- | eq_fm (Closed bd) (Lt ag) = false
- | eq_fm (A bf) (Lt ag) = false
- | eq_fm (E bf) (Lt ag) = false
- | eq_fm (Iff (bf, cf)) (Lt ag) = false
- | eq_fm (Imp (bf, cf)) (Lt ag) = false
- | eq_fm (Or (bf, cf)) (Lt ag) = false
- | eq_fm (And (bf, cf)) (Lt ag) = false
- | eq_fm (Not bf) (Lt ag) = false
- | eq_fm (NDvd (be, cg)) (Lt ag) = false
- | eq_fm (Dvd (be, cg)) (Lt ag) = false
- | eq_fm (NEq bg) (Lt ag) = false
- | eq_fm (Eq bg) (Lt ag) = false
- | eq_fm (Ge bg) (Lt ag) = false
- | eq_fm (Gt bg) (Lt ag) = false
- | eq_fm (Le bg) (Lt ag) = false
- | eq_fm (NClosed ad) F = false
- | eq_fm (Closed ad) F = false
- | eq_fm (A af) F = false
- | eq_fm (E af) F = false
- | eq_fm (Iff (af, bf)) F = false
- | eq_fm (Imp (af, bf)) F = false
- | eq_fm (Or (af, bf)) F = false
- | eq_fm (And (af, bf)) F = false
- | eq_fm (Not af) F = false
- | eq_fm (NDvd (ae, bg)) F = false
- | eq_fm (Dvd (ae, bg)) F = false
- | eq_fm (NEq ag) F = false
- | eq_fm (Eq ag) F = false
- | eq_fm (Ge ag) F = false
- | eq_fm (Gt ag) F = false
- | eq_fm (Le ag) F = false
- | eq_fm (Lt ag) F = false
- | eq_fm (NClosed ad) T = false
- | eq_fm (Closed ad) T = false
- | eq_fm (A af) T = false
- | eq_fm (E af) T = false
- | eq_fm (Iff (af, bf)) T = false
- | eq_fm (Imp (af, bf)) T = false
- | eq_fm (Or (af, bf)) T = false
- | eq_fm (And (af, bf)) T = false
- | eq_fm (Not af) T = false
- | eq_fm (NDvd (ae, bg)) T = false
- | eq_fm (Dvd (ae, bg)) T = false
- | eq_fm (NEq ag) T = false
- | eq_fm (Eq ag) T = false
- | eq_fm (Ge ag) T = false
- | eq_fm (Gt ag) T = false
- | eq_fm (Le ag) T = false
- | eq_fm (Lt ag) T = false
+fun eq_fm (NClosed b) (Closed a) = false
+ | eq_fm (NClosed b) (A a) = false
+ | eq_fm (Closed b) (A a) = false
+ | eq_fm (NClosed b) (E a) = false
+ | eq_fm (Closed b) (E a) = false
+ | eq_fm (A b) (E a) = false
+ | eq_fm (NClosed c) (Iff (a, b)) = false
+ | eq_fm (Closed c) (Iff (a, b)) = false
+ | eq_fm (A c) (Iff (a, b)) = false
+ | eq_fm (E c) (Iff (a, b)) = false
+ | eq_fm (NClosed c) (Imp (a, b)) = false
+ | eq_fm (Closed c) (Imp (a, b)) = false
+ | eq_fm (A c) (Imp (a, b)) = false
+ | eq_fm (E c) (Imp (a, b)) = false
+ | eq_fm (Iff (c, d)) (Imp (a, b)) = false
+ | eq_fm (NClosed c) (Or (a, b)) = false
+ | eq_fm (Closed c) (Or (a, b)) = false
+ | eq_fm (A c) (Or (a, b)) = false
+ | eq_fm (E c) (Or (a, b)) = false
+ | eq_fm (Iff (c, d)) (Or (a, b)) = false
+ | eq_fm (Imp (c, d)) (Or (a, b)) = false
+ | eq_fm (NClosed c) (And (a, b)) = false
+ | eq_fm (Closed c) (And (a, b)) = false
+ | eq_fm (A c) (And (a, b)) = false
+ | eq_fm (E c) (And (a, b)) = false
+ | eq_fm (Iff (c, d)) (And (a, b)) = false
+ | eq_fm (Imp (c, d)) (And (a, b)) = false
+ | eq_fm (Or (c, d)) (And (a, b)) = false
+ | eq_fm (NClosed b) (Not a) = false
+ | eq_fm (Closed b) (Not a) = false
+ | eq_fm (A b) (Not a) = false
+ | eq_fm (E b) (Not a) = false
+ | eq_fm (Iff (b, c)) (Not a) = false
+ | eq_fm (Imp (b, c)) (Not a) = false
+ | eq_fm (Or (b, c)) (Not a) = false
+ | eq_fm (And (b, c)) (Not a) = false
+ | eq_fm (NClosed c) (NDvd (a, b)) = false
+ | eq_fm (Closed c) (NDvd (a, b)) = false
+ | eq_fm (A c) (NDvd (a, b)) = false
+ | eq_fm (E c) (NDvd (a, b)) = false
+ | eq_fm (Iff (c, d)) (NDvd (a, b)) = false
+ | eq_fm (Imp (c, d)) (NDvd (a, b)) = false
+ | eq_fm (Or (c, d)) (NDvd (a, b)) = false
+ | eq_fm (And (c, d)) (NDvd (a, b)) = false
+ | eq_fm (Not c) (NDvd (a, b)) = false
+ | eq_fm (NClosed c) (Dvd (a, b)) = false
+ | eq_fm (Closed c) (Dvd (a, b)) = false
+ | eq_fm (A c) (Dvd (a, b)) = false
+ | eq_fm (E c) (Dvd (a, b)) = false
+ | eq_fm (Iff (c, d)) (Dvd (a, b)) = false
+ | eq_fm (Imp (c, d)) (Dvd (a, b)) = false
+ | eq_fm (Or (c, d)) (Dvd (a, b)) = false
+ | eq_fm (And (c, d)) (Dvd (a, b)) = false
+ | eq_fm (Not c) (Dvd (a, b)) = false
+ | eq_fm (NDvd (c, d)) (Dvd (a, b)) = false
+ | eq_fm (NClosed b) (NEq a) = false
+ | eq_fm (Closed b) (NEq a) = false
+ | eq_fm (A b) (NEq a) = false
+ | eq_fm (E b) (NEq a) = false
+ | eq_fm (Iff (b, c)) (NEq a) = false
+ | eq_fm (Imp (b, c)) (NEq a) = false
+ | eq_fm (Or (b, c)) (NEq a) = false
+ | eq_fm (And (b, c)) (NEq a) = false
+ | eq_fm (Not b) (NEq a) = false
+ | eq_fm (NDvd (b, c)) (NEq a) = false
+ | eq_fm (Dvd (b, c)) (NEq a) = false
+ | eq_fm (NClosed b) (Eq a) = false
+ | eq_fm (Closed b) (Eq a) = false
+ | eq_fm (A b) (Eq a) = false
+ | eq_fm (E b) (Eq a) = false
+ | eq_fm (Iff (b, c)) (Eq a) = false
+ | eq_fm (Imp (b, c)) (Eq a) = false
+ | eq_fm (Or (b, c)) (Eq a) = false
+ | eq_fm (And (b, c)) (Eq a) = false
+ | eq_fm (Not b) (Eq a) = false
+ | eq_fm (NDvd (b, c)) (Eq a) = false
+ | eq_fm (Dvd (b, c)) (Eq a) = false
+ | eq_fm (NEq b) (Eq a) = false
+ | eq_fm (NClosed b) (Ge a) = false
+ | eq_fm (Closed b) (Ge a) = false
+ | eq_fm (A b) (Ge a) = false
+ | eq_fm (E b) (Ge a) = false
+ | eq_fm (Iff (b, c)) (Ge a) = false
+ | eq_fm (Imp (b, c)) (Ge a) = false
+ | eq_fm (Or (b, c)) (Ge a) = false
+ | eq_fm (And (b, c)) (Ge a) = false
+ | eq_fm (Not b) (Ge a) = false
+ | eq_fm (NDvd (b, c)) (Ge a) = false
+ | eq_fm (Dvd (b, c)) (Ge a) = false
+ | eq_fm (NEq b) (Ge a) = false
+ | eq_fm (Eq b) (Ge a) = false
+ | eq_fm (NClosed b) (Gt a) = false
+ | eq_fm (Closed b) (Gt a) = false
+ | eq_fm (A b) (Gt a) = false
+ | eq_fm (E b) (Gt a) = false
+ | eq_fm (Iff (b, c)) (Gt a) = false
+ | eq_fm (Imp (b, c)) (Gt a) = false
+ | eq_fm (Or (b, c)) (Gt a) = false
+ | eq_fm (And (b, c)) (Gt a) = false
+ | eq_fm (Not b) (Gt a) = false
+ | eq_fm (NDvd (b, c)) (Gt a) = false
+ | eq_fm (Dvd (b, c)) (Gt a) = false
+ | eq_fm (NEq b) (Gt a) = false
+ | eq_fm (Eq b) (Gt a) = false
+ | eq_fm (Ge b) (Gt a) = false
+ | eq_fm (NClosed b) (Le a) = false
+ | eq_fm (Closed b) (Le a) = false
+ | eq_fm (A b) (Le a) = false
+ | eq_fm (E b) (Le a) = false
+ | eq_fm (Iff (b, c)) (Le a) = false
+ | eq_fm (Imp (b, c)) (Le a) = false
+ | eq_fm (Or (b, c)) (Le a) = false
+ | eq_fm (And (b, c)) (Le a) = false
+ | eq_fm (Not b) (Le a) = false
+ | eq_fm (NDvd (b, c)) (Le a) = false
+ | eq_fm (Dvd (b, c)) (Le a) = false
+ | eq_fm (NEq b) (Le a) = false
+ | eq_fm (Eq b) (Le a) = false
+ | eq_fm (Ge b) (Le a) = false
+ | eq_fm (Gt b) (Le a) = false
+ | eq_fm (NClosed b) (Lt a) = false
+ | eq_fm (Closed b) (Lt a) = false
+ | eq_fm (A b) (Lt a) = false
+ | eq_fm (E b) (Lt a) = false
+ | eq_fm (Iff (b, c)) (Lt a) = false
+ | eq_fm (Imp (b, c)) (Lt a) = false
+ | eq_fm (Or (b, c)) (Lt a) = false
+ | eq_fm (And (b, c)) (Lt a) = false
+ | eq_fm (Not b) (Lt a) = false
+ | eq_fm (NDvd (b, c)) (Lt a) = false
+ | eq_fm (Dvd (b, c)) (Lt a) = false
+ | eq_fm (NEq b) (Lt a) = false
+ | eq_fm (Eq b) (Lt a) = false
+ | eq_fm (Ge b) (Lt a) = false
+ | eq_fm (Gt b) (Lt a) = false
+ | eq_fm (Le b) (Lt a) = false
+ | eq_fm (NClosed a) F = false
+ | eq_fm (Closed a) F = false
+ | eq_fm (A a) F = false
+ | eq_fm (E a) F = false
+ | eq_fm (Iff (a, b)) F = false
+ | eq_fm (Imp (a, b)) F = false
+ | eq_fm (Or (a, b)) F = false
+ | eq_fm (And (a, b)) F = false
+ | eq_fm (Not a) F = false
+ | eq_fm (NDvd (a, b)) F = false
+ | eq_fm (Dvd (a, b)) F = false
+ | eq_fm (NEq a) F = false
+ | eq_fm (Eq a) F = false
+ | eq_fm (Ge a) F = false
+ | eq_fm (Gt a) F = false
+ | eq_fm (Le a) F = false
+ | eq_fm (Lt a) F = false
+ | eq_fm (NClosed a) T = false
+ | eq_fm (Closed a) T = false
+ | eq_fm (A a) T = false
+ | eq_fm (E a) T = false
+ | eq_fm (Iff (a, b)) T = false
+ | eq_fm (Imp (a, b)) T = false
+ | eq_fm (Or (a, b)) T = false
+ | eq_fm (And (a, b)) T = false
+ | eq_fm (Not a) T = false
+ | eq_fm (NDvd (a, b)) T = false
+ | eq_fm (Dvd (a, b)) T = false
+ | eq_fm (NEq a) T = false
+ | eq_fm (Eq a) T = false
+ | eq_fm (Ge a) T = false
+ | eq_fm (Gt a) T = false
+ | eq_fm (Le a) T = false
+ | eq_fm (Lt a) T = false
| eq_fm F T = false
| eq_fm (Closed a) (NClosed b) = false
- | eq_fm (A ab) (NClosed b) = false
- | eq_fm (A ab) (Closed b) = false
- | eq_fm (E ab) (NClosed b) = false
- | eq_fm (E ab) (Closed b) = false
- | eq_fm (E ab) (A bb) = false
- | eq_fm (Iff (ab, bb)) (NClosed c) = false
- | eq_fm (Iff (ab, bb)) (Closed c) = false
- | eq_fm (Iff (ab, bb)) (A cb) = false
- | eq_fm (Iff (ab, bb)) (E cb) = false
- | eq_fm (Imp (ab, bb)) (NClosed c) = false
- | eq_fm (Imp (ab, bb)) (Closed c) = false
- | eq_fm (Imp (ab, bb)) (A cb) = false
- | eq_fm (Imp (ab, bb)) (E cb) = false
- | eq_fm (Imp (ab, bb)) (Iff (cb, d)) = false
- | eq_fm (Or (ab, bb)) (NClosed c) = false
- | eq_fm (Or (ab, bb)) (Closed c) = false
- | eq_fm (Or (ab, bb)) (A cb) = false
- | eq_fm (Or (ab, bb)) (E cb) = false
- | eq_fm (Or (ab, bb)) (Iff (cb, d)) = false
- | eq_fm (Or (ab, bb)) (Imp (cb, d)) = false
- | eq_fm (And (ab, bb)) (NClosed c) = false
- | eq_fm (And (ab, bb)) (Closed c) = false
- | eq_fm (And (ab, bb)) (A cb) = false
- | eq_fm (And (ab, bb)) (E cb) = false
- | eq_fm (And (ab, bb)) (Iff (cb, d)) = false
- | eq_fm (And (ab, bb)) (Imp (cb, d)) = false
- | eq_fm (And (ab, bb)) (Or (cb, d)) = false
- | eq_fm (Not ab) (NClosed b) = false
- | eq_fm (Not ab) (Closed b) = false
- | eq_fm (Not ab) (A bb) = false
- | eq_fm (Not ab) (E bb) = false
- | eq_fm (Not ab) (Iff (bb, cb)) = false
- | eq_fm (Not ab) (Imp (bb, cb)) = false
- | eq_fm (Not ab) (Or (bb, cb)) = false
- | eq_fm (Not ab) (And (bb, cb)) = false
- | eq_fm (NDvd (aa, bc)) (NClosed c) = false
- | eq_fm (NDvd (aa, bc)) (Closed c) = false
- | eq_fm (NDvd (aa, bc)) (A cb) = false
- | eq_fm (NDvd (aa, bc)) (E cb) = false
- | eq_fm (NDvd (aa, bc)) (Iff (cb, d)) = false
- | eq_fm (NDvd (aa, bc)) (Imp (cb, d)) = false
- | eq_fm (NDvd (aa, bc)) (Or (cb, d)) = false
- | eq_fm (NDvd (aa, bc)) (And (cb, d)) = false
- | eq_fm (NDvd (aa, bc)) (Not cb) = false
- | eq_fm (Dvd (aa, bc)) (NClosed c) = false
- | eq_fm (Dvd (aa, bc)) (Closed c) = false
- | eq_fm (Dvd (aa, bc)) (A cb) = false
- | eq_fm (Dvd (aa, bc)) (E cb) = false
- | eq_fm (Dvd (aa, bc)) (Iff (cb, d)) = false
- | eq_fm (Dvd (aa, bc)) (Imp (cb, d)) = false
- | eq_fm (Dvd (aa, bc)) (Or (cb, d)) = false
- | eq_fm (Dvd (aa, bc)) (And (cb, d)) = false
- | eq_fm (Dvd (aa, bc)) (Not cb) = false
- | eq_fm (Dvd (aa, bc)) (NDvd (ca, da)) = false
- | eq_fm (NEq ac) (NClosed b) = false
- | eq_fm (NEq ac) (Closed b) = false
- | eq_fm (NEq ac) (A bb) = false
- | eq_fm (NEq ac) (E bb) = false
- | eq_fm (NEq ac) (Iff (bb, cb)) = false
- | eq_fm (NEq ac) (Imp (bb, cb)) = false
- | eq_fm (NEq ac) (Or (bb, cb)) = false
- | eq_fm (NEq ac) (And (bb, cb)) = false
- | eq_fm (NEq ac) (Not bb) = false
- | eq_fm (NEq ac) (NDvd (ba, cc)) = false
- | eq_fm (NEq ac) (Dvd (ba, cc)) = false
- | eq_fm (Eq ac) (NClosed b) = false
- | eq_fm (Eq ac) (Closed b) = false
- | eq_fm (Eq ac) (A bb) = false
- | eq_fm (Eq ac) (E bb) = false
- | eq_fm (Eq ac) (Iff (bb, cb)) = false
- | eq_fm (Eq ac) (Imp (bb, cb)) = false
- | eq_fm (Eq ac) (Or (bb, cb)) = false
- | eq_fm (Eq ac) (And (bb, cb)) = false
- | eq_fm (Eq ac) (Not bb) = false
- | eq_fm (Eq ac) (NDvd (ba, cc)) = false
- | eq_fm (Eq ac) (Dvd (ba, cc)) = false
- | eq_fm (Eq ac) (NEq bc) = false
- | eq_fm (Ge ac) (NClosed b) = false
- | eq_fm (Ge ac) (Closed b) = false
- | eq_fm (Ge ac) (A bb) = false
- | eq_fm (Ge ac) (E bb) = false
- | eq_fm (Ge ac) (Iff (bb, cb)) = false
- | eq_fm (Ge ac) (Imp (bb, cb)) = false
- | eq_fm (Ge ac) (Or (bb, cb)) = false
- | eq_fm (Ge ac) (And (bb, cb)) = false
- | eq_fm (Ge ac) (Not bb) = false
- | eq_fm (Ge ac) (NDvd (ba, cc)) = false
- | eq_fm (Ge ac) (Dvd (ba, cc)) = false
- | eq_fm (Ge ac) (NEq bc) = false
- | eq_fm (Ge ac) (Eq bc) = false
- | eq_fm (Gt ac) (NClosed b) = false
- | eq_fm (Gt ac) (Closed b) = false
- | eq_fm (Gt ac) (A bb) = false
- | eq_fm (Gt ac) (E bb) = false
- | eq_fm (Gt ac) (Iff (bb, cb)) = false
- | eq_fm (Gt ac) (Imp (bb, cb)) = false
- | eq_fm (Gt ac) (Or (bb, cb)) = false
- | eq_fm (Gt ac) (And (bb, cb)) = false
- | eq_fm (Gt ac) (Not bb) = false
- | eq_fm (Gt ac) (NDvd (ba, cc)) = false
- | eq_fm (Gt ac) (Dvd (ba, cc)) = false
- | eq_fm (Gt ac) (NEq bc) = false
- | eq_fm (Gt ac) (Eq bc) = false
- | eq_fm (Gt ac) (Ge bc) = false
- | eq_fm (Le ac) (NClosed b) = false
- | eq_fm (Le ac) (Closed b) = false
- | eq_fm (Le ac) (A bb) = false
- | eq_fm (Le ac) (E bb) = false
- | eq_fm (Le ac) (Iff (bb, cb)) = false
- | eq_fm (Le ac) (Imp (bb, cb)) = false
- | eq_fm (Le ac) (Or (bb, cb)) = false
- | eq_fm (Le ac) (And (bb, cb)) = false
- | eq_fm (Le ac) (Not bb) = false
- | eq_fm (Le ac) (NDvd (ba, cc)) = false
- | eq_fm (Le ac) (Dvd (ba, cc)) = false
- | eq_fm (Le ac) (NEq bc) = false
- | eq_fm (Le ac) (Eq bc) = false
- | eq_fm (Le ac) (Ge bc) = false
- | eq_fm (Le ac) (Gt bc) = false
- | eq_fm (Lt ac) (NClosed b) = false
- | eq_fm (Lt ac) (Closed b) = false
- | eq_fm (Lt ac) (A bb) = false
- | eq_fm (Lt ac) (E bb) = false
- | eq_fm (Lt ac) (Iff (bb, cb)) = false
- | eq_fm (Lt ac) (Imp (bb, cb)) = false
- | eq_fm (Lt ac) (Or (bb, cb)) = false
- | eq_fm (Lt ac) (And (bb, cb)) = false
- | eq_fm (Lt ac) (Not bb) = false
- | eq_fm (Lt ac) (NDvd (ba, cc)) = false
- | eq_fm (Lt ac) (Dvd (ba, cc)) = false
- | eq_fm (Lt ac) (NEq bc) = false
- | eq_fm (Lt ac) (Eq bc) = false
- | eq_fm (Lt ac) (Ge bc) = false
- | eq_fm (Lt ac) (Gt bc) = false
- | eq_fm (Lt ac) (Le bc) = false
+ | eq_fm (A a) (NClosed b) = false
+ | eq_fm (A a) (Closed b) = false
+ | eq_fm (E a) (NClosed b) = false
+ | eq_fm (E a) (Closed b) = false
+ | eq_fm (E a) (A b) = false
+ | eq_fm (Iff (a, b)) (NClosed c) = false
+ | eq_fm (Iff (a, b)) (Closed c) = false
+ | eq_fm (Iff (a, b)) (A c) = false
+ | eq_fm (Iff (a, b)) (E c) = false
+ | eq_fm (Imp (a, b)) (NClosed c) = false
+ | eq_fm (Imp (a, b)) (Closed c) = false
+ | eq_fm (Imp (a, b)) (A c) = false
+ | eq_fm (Imp (a, b)) (E c) = false
+ | eq_fm (Imp (a, b)) (Iff (c, d)) = false
+ | eq_fm (Or (a, b)) (NClosed c) = false
+ | eq_fm (Or (a, b)) (Closed c) = false
+ | eq_fm (Or (a, b)) (A c) = false
+ | eq_fm (Or (a, b)) (E c) = false
+ | eq_fm (Or (a, b)) (Iff (c, d)) = false
+ | eq_fm (Or (a, b)) (Imp (c, d)) = false
+ | eq_fm (And (a, b)) (NClosed c) = false
+ | eq_fm (And (a, b)) (Closed c) = false
+ | eq_fm (And (a, b)) (A c) = false
+ | eq_fm (And (a, b)) (E c) = false
+ | eq_fm (And (a, b)) (Iff (c, d)) = false
+ | eq_fm (And (a, b)) (Imp (c, d)) = false
+ | eq_fm (And (a, b)) (Or (c, d)) = false
+ | eq_fm (Not a) (NClosed b) = false
+ | eq_fm (Not a) (Closed b) = false
+ | eq_fm (Not a) (A b) = false
+ | eq_fm (Not a) (E b) = false
+ | eq_fm (Not a) (Iff (b, c)) = false
+ | eq_fm (Not a) (Imp (b, c)) = false
+ | eq_fm (Not a) (Or (b, c)) = false
+ | eq_fm (Not a) (And (b, c)) = false
+ | eq_fm (NDvd (a, b)) (NClosed c) = false
+ | eq_fm (NDvd (a, b)) (Closed c) = false
+ | eq_fm (NDvd (a, b)) (A c) = false
+ | eq_fm (NDvd (a, b)) (E c) = false
+ | eq_fm (NDvd (a, b)) (Iff (c, d)) = false
+ | eq_fm (NDvd (a, b)) (Imp (c, d)) = false
+ | eq_fm (NDvd (a, b)) (Or (c, d)) = false
+ | eq_fm (NDvd (a, b)) (And (c, d)) = false
+ | eq_fm (NDvd (a, b)) (Not c) = false
+ | eq_fm (Dvd (a, b)) (NClosed c) = false
+ | eq_fm (Dvd (a, b)) (Closed c) = false
+ | eq_fm (Dvd (a, b)) (A c) = false
+ | eq_fm (Dvd (a, b)) (E c) = false
+ | eq_fm (Dvd (a, b)) (Iff (c, d)) = false
+ | eq_fm (Dvd (a, b)) (Imp (c, d)) = false
+ | eq_fm (Dvd (a, b)) (Or (c, d)) = false
+ | eq_fm (Dvd (a, b)) (And (c, d)) = false
+ | eq_fm (Dvd (a, b)) (Not c) = false
+ | eq_fm (Dvd (a, b)) (NDvd (c, d)) = false
+ | eq_fm (NEq a) (NClosed b) = false
+ | eq_fm (NEq a) (Closed b) = false
+ | eq_fm (NEq a) (A b) = false
+ | eq_fm (NEq a) (E b) = false
+ | eq_fm (NEq a) (Iff (b, c)) = false
+ | eq_fm (NEq a) (Imp (b, c)) = false
+ | eq_fm (NEq a) (Or (b, c)) = false
+ | eq_fm (NEq a) (And (b, c)) = false
+ | eq_fm (NEq a) (Not b) = false
+ | eq_fm (NEq a) (NDvd (b, c)) = false
+ | eq_fm (NEq a) (Dvd (b, c)) = false
+ | eq_fm (Eq a) (NClosed b) = false
+ | eq_fm (Eq a) (Closed b) = false
+ | eq_fm (Eq a) (A b) = false
+ | eq_fm (Eq a) (E b) = false
+ | eq_fm (Eq a) (Iff (b, c)) = false
+ | eq_fm (Eq a) (Imp (b, c)) = false
+ | eq_fm (Eq a) (Or (b, c)) = false
+ | eq_fm (Eq a) (And (b, c)) = false
+ | eq_fm (Eq a) (Not b) = false
+ | eq_fm (Eq a) (NDvd (b, c)) = false
+ | eq_fm (Eq a) (Dvd (b, c)) = false
+ | eq_fm (Eq a) (NEq b) = false
+ | eq_fm (Ge a) (NClosed b) = false
+ | eq_fm (Ge a) (Closed b) = false
+ | eq_fm (Ge a) (A b) = false
+ | eq_fm (Ge a) (E b) = false
+ | eq_fm (Ge a) (Iff (b, c)) = false
+ | eq_fm (Ge a) (Imp (b, c)) = false
+ | eq_fm (Ge a) (Or (b, c)) = false
+ | eq_fm (Ge a) (And (b, c)) = false
+ | eq_fm (Ge a) (Not b) = false
+ | eq_fm (Ge a) (NDvd (b, c)) = false
+ | eq_fm (Ge a) (Dvd (b, c)) = false
+ | eq_fm (Ge a) (NEq b) = false
+ | eq_fm (Ge a) (Eq b) = false
+ | eq_fm (Gt a) (NClosed b) = false
+ | eq_fm (Gt a) (Closed b) = false
+ | eq_fm (Gt a) (A b) = false
+ | eq_fm (Gt a) (E b) = false
+ | eq_fm (Gt a) (Iff (b, c)) = false
+ | eq_fm (Gt a) (Imp (b, c)) = false
+ | eq_fm (Gt a) (Or (b, c)) = false
+ | eq_fm (Gt a) (And (b, c)) = false
+ | eq_fm (Gt a) (Not b) = false
+ | eq_fm (Gt a) (NDvd (b, c)) = false
+ | eq_fm (Gt a) (Dvd (b, c)) = false
+ | eq_fm (Gt a) (NEq b) = false
+ | eq_fm (Gt a) (Eq b) = false
+ | eq_fm (Gt a) (Ge b) = false
+ | eq_fm (Le a) (NClosed b) = false
+ | eq_fm (Le a) (Closed b) = false
+ | eq_fm (Le a) (A b) = false
+ | eq_fm (Le a) (E b) = false
+ | eq_fm (Le a) (Iff (b, c)) = false
+ | eq_fm (Le a) (Imp (b, c)) = false
+ | eq_fm (Le a) (Or (b, c)) = false
+ | eq_fm (Le a) (And (b, c)) = false
+ | eq_fm (Le a) (Not b) = false
+ | eq_fm (Le a) (NDvd (b, c)) = false
+ | eq_fm (Le a) (Dvd (b, c)) = false
+ | eq_fm (Le a) (NEq b) = false
+ | eq_fm (Le a) (Eq b) = false
+ | eq_fm (Le a) (Ge b) = false
+ | eq_fm (Le a) (Gt b) = false
+ | eq_fm (Lt a) (NClosed b) = false
+ | eq_fm (Lt a) (Closed b) = false
+ | eq_fm (Lt a) (A b) = false
+ | eq_fm (Lt a) (E b) = false
+ | eq_fm (Lt a) (Iff (b, c)) = false
+ | eq_fm (Lt a) (Imp (b, c)) = false
+ | eq_fm (Lt a) (Or (b, c)) = false
+ | eq_fm (Lt a) (And (b, c)) = false
+ | eq_fm (Lt a) (Not b) = false
+ | eq_fm (Lt a) (NDvd (b, c)) = false
+ | eq_fm (Lt a) (Dvd (b, c)) = false
+ | eq_fm (Lt a) (NEq b) = false
+ | eq_fm (Lt a) (Eq b) = false
+ | eq_fm (Lt a) (Ge b) = false
+ | eq_fm (Lt a) (Gt b) = false
+ | eq_fm (Lt a) (Le b) = false
| eq_fm F (NClosed a) = false
| eq_fm F (Closed a) = false
- | eq_fm F (A ab) = false
- | eq_fm F (E ab) = false
- | eq_fm F (Iff (ab, bb)) = false
- | eq_fm F (Imp (ab, bb)) = false
- | eq_fm F (Or (ab, bb)) = false
- | eq_fm F (And (ab, bb)) = false
- | eq_fm F (Not ab) = false
- | eq_fm F (NDvd (aa, bc)) = false
- | eq_fm F (Dvd (aa, bc)) = false
- | eq_fm F (NEq ac) = false
- | eq_fm F (Eq ac) = false
- | eq_fm F (Ge ac) = false
- | eq_fm F (Gt ac) = false
- | eq_fm F (Le ac) = false
- | eq_fm F (Lt ac) = false
+ | eq_fm F (A a) = false
+ | eq_fm F (E a) = false
+ | eq_fm F (Iff (a, b)) = false
+ | eq_fm F (Imp (a, b)) = false
+ | eq_fm F (Or (a, b)) = false
+ | eq_fm F (And (a, b)) = false
+ | eq_fm F (Not a) = false
+ | eq_fm F (NDvd (a, b)) = false
+ | eq_fm F (Dvd (a, b)) = false
+ | eq_fm F (NEq a) = false
+ | eq_fm F (Eq a) = false
+ | eq_fm F (Ge a) = false
+ | eq_fm F (Gt a) = false
+ | eq_fm F (Le a) = false
+ | eq_fm F (Lt a) = false
| eq_fm T (NClosed a) = false
| eq_fm T (Closed a) = false
- | eq_fm T (A ab) = false
- | eq_fm T (E ab) = false
- | eq_fm T (Iff (ab, bb)) = false
- | eq_fm T (Imp (ab, bb)) = false
- | eq_fm T (Or (ab, bb)) = false
- | eq_fm T (And (ab, bb)) = false
- | eq_fm T (Not ab) = false
- | eq_fm T (NDvd (aa, bc)) = false
- | eq_fm T (Dvd (aa, bc)) = false
- | eq_fm T (NEq ac) = false
- | eq_fm T (Eq ac) = false
- | eq_fm T (Ge ac) = false
- | eq_fm T (Gt ac) = false
- | eq_fm T (Le ac) = false
- | eq_fm T (Lt ac) = false
+ | eq_fm T (A a) = false
+ | eq_fm T (E a) = false
+ | eq_fm T (Iff (a, b)) = false
+ | eq_fm T (Imp (a, b)) = false
+ | eq_fm T (Or (a, b)) = false
+ | eq_fm T (And (a, b)) = false
+ | eq_fm T (Not a) = false
+ | eq_fm T (NDvd (a, b)) = false
+ | eq_fm T (Dvd (a, b)) = false
+ | eq_fm T (NEq a) = false
+ | eq_fm T (Eq a) = false
+ | eq_fm T (Ge a) = false
+ | eq_fm T (Gt a) = false
+ | eq_fm T (Le a) = false
+ | eq_fm T (Lt a) = false
| eq_fm T F = false
| eq_fm (NClosed nat) (NClosed nat') = ((nat : IntInf.int) = nat')
| eq_fm (Closed nat) (Closed nat') = ((nat : IntInf.int) = nat')
@@ -554,7 +554,7 @@
| NClosed nat => Or (f p, q))
end));
-fun foldr f [] y = y
+fun foldr f [] a = a
| foldr f (x :: xs) a = f x (foldr f xs a);
fun evaldjf f ps = foldr (djf f) ps F;
@@ -607,9 +607,9 @@
| numsubst0 t (Add (a, b)) = Add (numsubst0 t a, numsubst0 t b)
| numsubst0 t (Sub (a, b)) = Sub (numsubst0 t a, numsubst0 t b)
| numsubst0 t (Mul (i, a)) = Mul (i, numsubst0 t a)
- | numsubst0 ta (Cn (v, ia, aa)) =
- (if eqop eq_nat v 0 then Add (Mul (ia, ta), numsubst0 ta aa)
- else Cn (suc (minus_nat v 1), ia, numsubst0 ta aa));
+ | numsubst0 t (Cn (v, i, a)) =
+ (if eqop eq_nat v 0 then Add (Mul (i, t), numsubst0 t a)
+ else Cn (suc (minus_nat v 1), i, numsubst0 t a));
fun subst0 t T = T
| subst0 t F = F
@@ -691,36 +691,35 @@
| minusinf (NEq (Cn (hm, c, e))) =
(if eqop eq_nat hm 0 then T else NEq (Cn (suc (minus_nat hm 1), c, e)));
-fun adjust b =
- (fn a as (q, r) =>
- (if IntInf.<= ((0 : IntInf.int), IntInf.- (r, b))
- then (IntInf.+ (IntInf.* ((2 : IntInf.int), q), (1 : IntInf.int)),
- IntInf.- (r, b))
- else (IntInf.* ((2 : IntInf.int), q), r)));
+val eq_int = {eq = (fn a => fn b => ((a : IntInf.int) = b))} : IntInf.int eq;
-fun negDivAlg a b =
- (if IntInf.<= ((0 : IntInf.int), IntInf.+ (a, b)) orelse
- IntInf.<= (b, (0 : IntInf.int))
- then ((~1 : IntInf.int), IntInf.+ (a, b))
- else adjust b (negDivAlg a (IntInf.* ((2 : IntInf.int), b))));
+fun sgn_int i =
+ (if eqop eq_int i (0 : IntInf.int) then (0 : IntInf.int)
+ else (if IntInf.< ((0 : IntInf.int), i) then (1 : IntInf.int)
+ else IntInf.~ (1 : IntInf.int)));
fun apsnd f (x, y) = (x, f y);
-val eq_int = {eq = (fn a => fn b => ((a : IntInf.int) = b))} : IntInf.int eq;
-
-fun posDivAlg a b =
- (if IntInf.< (a, b) orelse IntInf.<= (b, (0 : IntInf.int))
- then ((0 : IntInf.int), a)
- else adjust b (posDivAlg a (IntInf.* ((2 : IntInf.int), b))));
-
-fun divmoda a b =
- (if IntInf.<= ((0 : IntInf.int), a)
- then (if IntInf.<= ((0 : IntInf.int), b) then posDivAlg a b
- else (if eqop eq_int a (0 : IntInf.int)
- then ((0 : IntInf.int), (0 : IntInf.int))
- else apsnd IntInf.~ (negDivAlg (IntInf.~ a) (IntInf.~ b))))
- else (if IntInf.< ((0 : IntInf.int), b) then negDivAlg a b
- else apsnd IntInf.~ (posDivAlg (IntInf.~ a) (IntInf.~ b))));
+fun divmoda k l =
+ (if eqop eq_int k (0 : IntInf.int) then ((0 : IntInf.int), (0 : IntInf.int))
+ else (if eqop eq_int l (0 : IntInf.int) then ((0 : IntInf.int), k)
+ else apsnd (fn a => IntInf.* (sgn_int l, a))
+ (if eqop eq_int (sgn_int k) (sgn_int l)
+ then (fn k => fn l => IntInf.divMod (IntInf.abs k,
+ IntInf.abs l))
+ k l
+ else let
+ val a =
+ (fn k => fn l => IntInf.divMod (IntInf.abs k,
+ IntInf.abs l))
+ k l;
+ val (r, s) = a;
+ in
+ (if eqop eq_int s (0 : IntInf.int)
+ then (IntInf.~ r, (0 : IntInf.int))
+ else (IntInf.- (IntInf.~ r, (1 : IntInf.int)),
+ IntInf.- (abs_int l, s)))
+ end)));
fun mod_int a b = snd (divmoda a b);
@@ -823,23 +822,23 @@
else nummul i (simpnum t))
| simpnum (Cn (v, va, vb)) = Cn (v, va, vb);
-fun nota (Not y) = y
+fun nota (Not p) = p
| nota T = F
| nota F = T
- | nota (Lt vc) = Not (Lt vc)
- | nota (Le vc) = Not (Le vc)
- | nota (Gt vc) = Not (Gt vc)
- | nota (Ge vc) = Not (Ge vc)
- | nota (Eq vc) = Not (Eq vc)
- | nota (NEq vc) = Not (NEq vc)
- | nota (Dvd (va, vab)) = Not (Dvd (va, vab))
- | nota (NDvd (va, vab)) = Not (NDvd (va, vab))
- | nota (And (vb, vaa)) = Not (And (vb, vaa))
- | nota (Or (vb, vaa)) = Not (Or (vb, vaa))
- | nota (Imp (vb, vaa)) = Not (Imp (vb, vaa))
- | nota (Iff (vb, vaa)) = Not (Iff (vb, vaa))
- | nota (E vb) = Not (E vb)
- | nota (A vb) = Not (A vb)
+ | nota (Lt v) = Not (Lt v)
+ | nota (Le v) = Not (Le v)
+ | nota (Gt v) = Not (Gt v)
+ | nota (Ge v) = Not (Ge v)
+ | nota (Eq v) = Not (Eq v)
+ | nota (NEq v) = Not (NEq v)
+ | nota (Dvd (v, va)) = Not (Dvd (v, va))
+ | nota (NDvd (v, va)) = Not (NDvd (v, va))
+ | nota (And (v, va)) = Not (And (v, va))
+ | nota (Or (v, va)) = Not (Or (v, va))
+ | nota (Imp (v, va)) = Not (Imp (v, va))
+ | nota (Iff (v, va)) = Not (Iff (v, va))
+ | nota (E v) = Not (E v)
+ | nota (A v) = Not (A v)
| nota (Closed v) = Not (Closed v)
| nota (NClosed v) = Not (NClosed v);
@@ -1184,7 +1183,7 @@
| delta (Le v) = (1 : IntInf.int)
| delta (Gt w) = (1 : IntInf.int)
| delta (Ge x) = (1 : IntInf.int)
- | delta (Eq ya) = (1 : IntInf.int)
+ | delta (Eq y) = (1 : IntInf.int)
| delta (NEq z) = (1 : IntInf.int)
| delta (Dvd (aa, C bo)) = (1 : IntInf.int)
| delta (Dvd (aa, Bound bp)) = (1 : IntInf.int)
@@ -1205,10 +1204,10 @@
| delta (A ao) = (1 : IntInf.int)
| delta (Closed ap) = (1 : IntInf.int)
| delta (NClosed aq) = (1 : IntInf.int)
- | delta (Dvd (b, Cn (cm, c, e))) =
- (if eqop eq_nat cm 0 then b else (1 : IntInf.int))
- | delta (NDvd (b, Cn (dm, c, e))) =
- (if eqop eq_nat dm 0 then b else (1 : IntInf.int));
+ | delta (Dvd (i, Cn (cm, c, e))) =
+ (if eqop eq_nat cm 0 then i else (1 : IntInf.int))
+ | delta (NDvd (i, Cn (dm, c, e))) =
+ (if eqop eq_nat dm 0 then i else (1 : IntInf.int));
fun div_int a b = fst (divmoda a b);
@@ -1367,22 +1366,22 @@
| zeta (A ao) = (1 : IntInf.int)
| zeta (Closed ap) = (1 : IntInf.int)
| zeta (NClosed aq) = (1 : IntInf.int)
- | zeta (Lt (Cn (cm, b, e))) =
- (if eqop eq_nat cm 0 then b else (1 : IntInf.int))
- | zeta (Le (Cn (dm, b, e))) =
- (if eqop eq_nat dm 0 then b else (1 : IntInf.int))
- | zeta (Gt (Cn (em, b, e))) =
- (if eqop eq_nat em 0 then b else (1 : IntInf.int))
- | zeta (Ge (Cn (fm, b, e))) =
- (if eqop eq_nat fm 0 then b else (1 : IntInf.int))
- | zeta (Eq (Cn (gm, b, e))) =
- (if eqop eq_nat gm 0 then b else (1 : IntInf.int))
- | zeta (NEq (Cn (hm, b, e))) =
- (if eqop eq_nat hm 0 then b else (1 : IntInf.int))
- | zeta (Dvd (i, Cn (im, b, e))) =
- (if eqop eq_nat im 0 then b else (1 : IntInf.int))
- | zeta (NDvd (i, Cn (jm, b, e))) =
- (if eqop eq_nat jm 0 then b else (1 : IntInf.int));
+ | zeta (Lt (Cn (cm, c, e))) =
+ (if eqop eq_nat cm 0 then c else (1 : IntInf.int))
+ | zeta (Le (Cn (dm, c, e))) =
+ (if eqop eq_nat dm 0 then c else (1 : IntInf.int))
+ | zeta (Gt (Cn (em, c, e))) =
+ (if eqop eq_nat em 0 then c else (1 : IntInf.int))
+ | zeta (Ge (Cn (fm, c, e))) =
+ (if eqop eq_nat fm 0 then c else (1 : IntInf.int))
+ | zeta (Eq (Cn (gm, c, e))) =
+ (if eqop eq_nat gm 0 then c else (1 : IntInf.int))
+ | zeta (NEq (Cn (hm, c, e))) =
+ (if eqop eq_nat hm 0 then c else (1 : IntInf.int))
+ | zeta (Dvd (i, Cn (im, c, e))) =
+ (if eqop eq_nat im 0 then c else (1 : IntInf.int))
+ | zeta (NDvd (i, Cn (jm, c, e))) =
+ (if eqop eq_nat jm 0 then c else (1 : IntInf.int));
fun zsplit0 (C c) = ((0 : IntInf.int), C c)
| zsplit0 (Bound n) =
@@ -1691,4 +1690,16 @@
(if IntInf.<= (i, (0 : IntInf.int)) then n
else nat_aux (IntInf.- (i, (1 : IntInf.int))) (suc n));
+fun adjust b =
+ (fn a as (q, r) =>
+ (if IntInf.<= ((0 : IntInf.int), IntInf.- (r, b))
+ then (IntInf.+ (IntInf.* ((2 : IntInf.int), q), (1 : IntInf.int)),
+ IntInf.- (r, b))
+ else (IntInf.* ((2 : IntInf.int), q), r)));
+
+fun posDivAlg a b =
+ (if IntInf.< (a, b) orelse IntInf.<= (b, (0 : IntInf.int))
+ then ((0 : IntInf.int), a)
+ else adjust b (posDivAlg a (IntInf.* ((2 : IntInf.int), b))));
+
end; (*struct GeneratedCooper*)
--- a/src/HOL/Tools/Qelim/presburger.ML Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML Wed Feb 18 13:39:16 2009 +0100
@@ -124,7 +124,7 @@
@ map (symmetric o mk_meta_eq)
[@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, @{thm "mod_add1_eq"},
@{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"},
- @{thm "zmod_zadd1_eq"}, @{thm "zmod_zadd_left_eq"},
+ @{thm "mod_add_eq"}, @{thm "zmod_zadd_left_eq"},
@{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
@ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"},
@{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1,
--- a/src/HOL/Tools/refute.ML Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/Tools/refute.ML Wed Feb 18 13:39:16 2009 +0100
@@ -2662,6 +2662,34 @@
(* theory -> model -> arguments -> Term.term ->
(interpretation * model * arguments) option *)
+ fun set_interpreter thy model args t =
+ let
+ val (typs, terms) = model
+ in
+ case AList.lookup (op =) terms t of
+ SOME intr =>
+ (* return an existing interpretation *)
+ SOME (intr, model, args)
+ | NONE =>
+ (case t of
+ (* 'Collect' == identity *)
+ Const (@{const_name Collect}, _) $ t1 =>
+ SOME (interpret thy model args t1)
+ | Const (@{const_name Collect}, _) =>
+ SOME (interpret thy model args (eta_expand t 1))
+ (* 'op :' == application *)
+ | Const (@{const_name "op :"}, _) $ t1 $ t2 =>
+ SOME (interpret thy model args (t2 $ t1))
+ | Const (@{const_name "op :"}, _) $ t1 =>
+ SOME (interpret thy model args (eta_expand t 1))
+ | Const (@{const_name "op :"}, _) =>
+ SOME (interpret thy model args (eta_expand t 2))
+ | _ => NONE)
+ end;
+
+ (* theory -> model -> arguments -> Term.term ->
+ (interpretation * model * arguments) option *)
+
(* only an optimization: 'card' could in principle be interpreted with *)
(* interpreters available already (using its definition), but the code *)
(* below is more efficient *)
@@ -3271,6 +3299,7 @@
add_interpreter "stlc" stlc_interpreter #>
add_interpreter "Pure" Pure_interpreter #>
add_interpreter "HOLogic" HOLogic_interpreter #>
+ add_interpreter "set" set_interpreter #>
add_interpreter "IDT" IDT_interpreter #>
add_interpreter "IDT_constructor" IDT_constructor_interpreter #>
add_interpreter "IDT_recursion" IDT_recursion_interpreter #>
--- a/src/HOL/Word/Num_Lemmas.thy Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/Word/Num_Lemmas.thy Wed Feb 18 13:39:16 2009 +0100
@@ -121,8 +121,8 @@
lemma zmod_zsub_distrib: "((a::int) - b) mod c = (a mod c - b mod c) mod c"
apply (unfold diff_int_def)
- apply (rule trans [OF _ zmod_zadd1_eq [symmetric]])
- apply (simp add: zmod_uminus zmod_zadd1_eq [symmetric])
+ apply (rule trans [OF _ mod_add_eq [symmetric]])
+ apply (simp add: zmod_uminus mod_add_eq [symmetric])
done
lemma zmod_zsub_right_eq: "((a::int) - b) mod c = (a - b mod c) mod c"
@@ -162,8 +162,8 @@
lemmas nat_minus_mod_plus_right = trans [OF nat_minus_mod mod_0 [symmetric],
THEN mod_plus_right [THEN iffD2], standard, simplified]
-lemmas push_mods' = zmod_zadd1_eq [standard]
- zmod_zmult_distrib [standard] zmod_zsub_distrib [standard]
+lemmas push_mods' = mod_add_eq [standard]
+ mod_mult_eq [standard] zmod_zsub_distrib [standard]
zmod_uminus [symmetric, standard]
lemmas push_mods = push_mods' [THEN eq_reflection, standard]
--- a/src/HOL/Word/WordGenLib.thy Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/Word/WordGenLib.thy Wed Feb 18 13:39:16 2009 +0100
@@ -293,9 +293,9 @@
shows "(x + y) mod b = z' mod b'"
proof -
from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
- by (simp add: zmod_zadd1_eq[symmetric])
+ by (simp add: mod_add_eq[symmetric])
also have "\<dots> = (x' + y') mod b'"
- by (simp add: zmod_zadd1_eq[symmetric])
+ by (simp add: mod_add_eq[symmetric])
finally show ?thesis by (simp add: 4)
qed
--- a/src/HOL/ex/Efficient_Nat_examples.thy Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/ex/Efficient_Nat_examples.thy Wed Feb 18 13:39:16 2009 +0100
@@ -1,12 +1,11 @@
(* Title: HOL/ex/Efficient_Nat_examples.thy
- ID: $Id$
Author: Florian Haftmann, TU Muenchen
*)
header {* Simple examples for Efficient\_Nat theory. *}
theory Efficient_Nat_examples
-imports Main "~~/src/HOL/Real/RealDef" Efficient_Nat
+imports Complex_Main Efficient_Nat
begin
fun to_n :: "nat \<Rightarrow> nat list" where
--- a/src/HOL/ex/Numeral.thy Wed Feb 18 13:39:05 2009 +0100
+++ b/src/HOL/ex/Numeral.thy Wed Feb 18 13:39:16 2009 +0100
@@ -1,8 +1,8 @@
(* Title: HOL/ex/Numeral.thy
Author: Florian Haftmann
+*)
-An experimental alternative numeral representation.
-*)
+header {* An experimental alternative numeral representation. *}
theory Numeral
imports Int Inductive
@@ -10,70 +10,103 @@
subsection {* The @{text num} type *}
+datatype num = One | Dig0 num | Dig1 num
+
+text {* Increment function for type @{typ num} *}
+
+primrec
+ inc :: "num \<Rightarrow> num"
+where
+ "inc One = Dig0 One"
+| "inc (Dig0 x) = Dig1 x"
+| "inc (Dig1 x) = Dig0 (inc x)"
+
+text {* Converting between type @{typ num} and type @{typ nat} *}
+
+primrec
+ nat_of_num :: "num \<Rightarrow> nat"
+where
+ "nat_of_num One = Suc 0"
+| "nat_of_num (Dig0 x) = nat_of_num x + nat_of_num x"
+| "nat_of_num (Dig1 x) = Suc (nat_of_num x + nat_of_num x)"
+
+primrec
+ num_of_nat :: "nat \<Rightarrow> num"
+where
+ "num_of_nat 0 = One"
+| "num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)"
+
+lemma nat_of_num_pos: "0 < nat_of_num x"
+ by (induct x) simp_all
+
+lemma nat_of_num_neq_0: " nat_of_num x \<noteq> 0"
+ by (induct x) simp_all
+
+lemma nat_of_num_inc: "nat_of_num (inc x) = Suc (nat_of_num x)"
+ by (induct x) simp_all
+
+lemma num_of_nat_double:
+ "0 < n \<Longrightarrow> num_of_nat (n + n) = Dig0 (num_of_nat n)"
+ by (induct n) simp_all
+
text {*
- We construct @{text num} as a copy of strictly positive
+ Type @{typ num} is isomorphic to the strictly positive
natural numbers.
*}
-typedef (open) num = "\<lambda>n\<Colon>nat. n > 0"
- morphisms nat_of_num num_of_nat_abs
- by (auto simp add: mem_def)
-
-text {*
- A totalized abstraction function. It is not entirely clear
- whether this is really useful.
-*}
-
-definition num_of_nat :: "nat \<Rightarrow> num" where
- "num_of_nat n = (if n = 0 then num_of_nat_abs 1 else num_of_nat_abs n)"
+lemma nat_of_num_inverse: "num_of_nat (nat_of_num x) = x"
+ by (induct x) (simp_all add: num_of_nat_double nat_of_num_pos)
-lemma num_cases [case_names nat, cases type: num]:
- assumes "(\<And>n\<Colon>nat. m = num_of_nat n \<Longrightarrow> 0 < n \<Longrightarrow> P)"
- shows P
-apply (rule num_of_nat_abs_cases)
-apply (unfold mem_def)
-using assms unfolding num_of_nat_def
-apply auto
-done
+lemma num_of_nat_inverse: "0 < n \<Longrightarrow> nat_of_num (num_of_nat n) = n"
+ by (induct n) (simp_all add: nat_of_num_inc)
-lemma num_of_nat_zero: "num_of_nat 0 = num_of_nat 1"
- by (simp add: num_of_nat_def)
-
-lemma num_of_nat_inverse: "nat_of_num (num_of_nat n) = (if n = 0 then 1 else n)"
- apply (simp add: num_of_nat_def)
- apply (subst num_of_nat_abs_inverse)
- apply (auto simp add: mem_def num_of_nat_abs_inverse)
+lemma num_eq_iff: "x = y \<longleftrightarrow> nat_of_num x = nat_of_num y"
+ apply safe
+ apply (drule arg_cong [where f=num_of_nat])
+ apply (simp add: nat_of_num_inverse)
done
-lemma num_of_nat_inject:
- "num_of_nat m = num_of_nat n \<longleftrightarrow> m = n \<or> (m = 0 \<or> m = 1) \<and> (n = 0 \<or> n = 1)"
-by (auto simp add: num_of_nat_def num_of_nat_abs_inject [unfolded mem_def])
-
-lemma split_num_all:
- "(\<And>m. PROP P m) \<equiv> (\<And>n. PROP P (num_of_nat n))"
-proof
- fix n
- assume "\<And>m\<Colon>num. PROP P m"
- then show "PROP P (num_of_nat n)" .
-next
- fix m
- have nat_of_num: "\<And>m. nat_of_num m \<noteq> 0"
- using nat_of_num by (auto simp add: mem_def)
- have nat_of_num_inverse: "\<And>m. num_of_nat (nat_of_num m) = m"
- by (auto simp add: num_of_nat_def nat_of_num_inverse nat_of_num)
- assume "\<And>n. PROP P (num_of_nat n)"
- then have "PROP P (num_of_nat (nat_of_num m))" .
- then show "PROP P m" unfolding nat_of_num_inverse .
+lemma num_induct [case_names One inc]:
+ fixes P :: "num \<Rightarrow> bool"
+ assumes One: "P One"
+ and inc: "\<And>x. P x \<Longrightarrow> P (inc x)"
+ shows "P x"
+proof -
+ obtain n where n: "Suc n = nat_of_num x"
+ by (cases "nat_of_num x", simp_all add: nat_of_num_neq_0)
+ have "P (num_of_nat (Suc n))"
+ proof (induct n)
+ case 0 show ?case using One by simp
+ next
+ case (Suc n)
+ then have "P (inc (num_of_nat (Suc n)))" by (rule inc)
+ then show "P (num_of_nat (Suc (Suc n)))" by simp
+ qed
+ with n show "P x"
+ by (simp add: nat_of_num_inverse)
qed
+text {*
+ From now on, there are two possible models for @{typ num}:
+ as positive naturals (rule @{text "num_induct"})
+ and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}).
-subsection {* Digit representation for @{typ num} *}
+ It is not entirely clear in which context it is better to use
+ the one or the other, or whether the construction should be reversed.
+*}
+
-instantiation num :: "{semiring, monoid_mult}"
-begin
+subsection {* Numeral operations *}
-definition one_num :: num where
- [code del]: "1 = num_of_nat 1"
+ML {*
+structure DigSimps =
+ NamedThmsFun(val name = "numeral"; val description = "Simplification rules for numerals")
+*}
+
+setup DigSimps.setup
+
+instantiation num :: "{plus,times,ord}"
+begin
definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where
[code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
@@ -81,167 +114,114 @@
definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where
[code del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
-definition Dig0 :: "num \<Rightarrow> num" where
- [code del]: "Dig0 n = n + n"
+definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
+ [code del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
-definition Dig1 :: "num \<Rightarrow> num" where
- [code del]: "Dig1 n = n + n + 1"
+definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
+ [code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
-instance proof
-qed (simp_all add: one_num_def plus_num_def times_num_def
- split_num_all num_of_nat_inverse num_of_nat_zero add_ac mult_ac nat_distrib)
+instance ..
end
-text {*
- The following proofs seem horribly complicated.
- Any room for simplification!?
-*}
+lemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y"
+ unfolding plus_num_def
+ by (intro num_of_nat_inverse add_pos_pos nat_of_num_pos)
+
+lemma nat_of_num_mult: "nat_of_num (x * y) = nat_of_num x * nat_of_num y"
+ unfolding times_num_def
+ by (intro num_of_nat_inverse mult_pos_pos nat_of_num_pos)
+
+lemma Dig_plus [numeral, simp, code]:
+ "One + One = Dig0 One"
+ "One + Dig0 m = Dig1 m"
+ "One + Dig1 m = Dig0 (m + One)"
+ "Dig0 n + One = Dig1 n"
+ "Dig0 n + Dig0 m = Dig0 (n + m)"
+ "Dig0 n + Dig1 m = Dig1 (n + m)"
+ "Dig1 n + One = Dig0 (n + One)"
+ "Dig1 n + Dig0 m = Dig1 (n + m)"
+ "Dig1 n + Dig1 m = Dig0 (n + m + One)"
+ by (simp_all add: num_eq_iff nat_of_num_add)
-lemma nat_dig_cases [case_names 0 1 dig0 dig1]:
- fixes n :: nat
- assumes "n = 0 \<Longrightarrow> P"
- and "n = 1 \<Longrightarrow> P"
- and "\<And>m. m > 0 \<Longrightarrow> n = m + m \<Longrightarrow> P"
- and "\<And>m. m > 0 \<Longrightarrow> n = Suc (m + m) \<Longrightarrow> P"
- shows P
-using assms proof (induct n)
- case 0 then show ?case by simp
-next
- case (Suc n)
- show P proof (rule Suc.hyps)
- assume "n = 0"
- then have "Suc n = 1" by simp
- then show P by (rule Suc.prems(2))
- next
- assume "n = 1"
- have "1 > (0\<Colon>nat)" by simp
- moreover from `n = 1` have "Suc n = 1 + 1" by simp
- ultimately show P by (rule Suc.prems(3))
- next
- fix m
- assume "0 < m" and "n = m + m"
- note `0 < m`
- moreover from `n = m + m` have "Suc n = Suc (m + m)" by simp
- ultimately show P by (rule Suc.prems(4))
- next
- fix m
- assume "0 < m" and "n = Suc (m + m)"
- have "0 < Suc m" by simp
- moreover from `n = Suc (m + m)` have "Suc n = Suc m + Suc m" by simp
- ultimately show P by (rule Suc.prems(3))
- qed
-qed
+lemma Dig_times [numeral, simp, code]:
+ "One * One = One"
+ "One * Dig0 n = Dig0 n"
+ "One * Dig1 n = Dig1 n"
+ "Dig0 n * One = Dig0 n"
+ "Dig0 n * Dig0 m = Dig0 (n * Dig0 m)"
+ "Dig0 n * Dig1 m = Dig0 (n * Dig1 m)"
+ "Dig1 n * One = Dig1 n"
+ "Dig1 n * Dig0 m = Dig0 (n * Dig0 m + m)"
+ "Dig1 n * Dig1 m = Dig1 (n * Dig1 m + m)"
+ by (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult
+ left_distrib right_distrib)
-lemma num_induct_raw:
- fixes n :: nat
- assumes not0: "n > 0"
- assumes "P 1"
- and "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (n + n)"
- and "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc (n + n))"
- shows "P n"
-using not0 proof (induct n rule: less_induct)
- case (less n)
- show "P n" proof (cases n rule: nat_dig_cases)
- case 0 then show ?thesis using less by simp
- next
- case 1 then show ?thesis using assms by simp
- next
- case (dig0 m)
- then show ?thesis apply simp
- apply (rule assms(3)) apply assumption
- apply (rule less)
- apply simp_all
- done
- next
- case (dig1 m)
- then show ?thesis apply simp
- apply (rule assms(4)) apply assumption
- apply (rule less)
- apply simp_all
- done
- qed
-qed
-
-lemma num_of_nat_Suc: "num_of_nat (Suc n) = (if n = 0 then 1 else num_of_nat n + 1)"
- by (cases n) (auto simp add: one_num_def plus_num_def num_of_nat_inverse)
+lemma less_eq_num_code [numeral, simp, code]:
+ "One \<le> n \<longleftrightarrow> True"
+ "Dig0 m \<le> One \<longleftrightarrow> False"
+ "Dig1 m \<le> One \<longleftrightarrow> False"
+ "Dig0 m \<le> Dig0 n \<longleftrightarrow> m \<le> n"
+ "Dig0 m \<le> Dig1 n \<longleftrightarrow> m \<le> n"
+ "Dig1 m \<le> Dig1 n \<longleftrightarrow> m \<le> n"
+ "Dig1 m \<le> Dig0 n \<longleftrightarrow> m < n"
+ using nat_of_num_pos [of n] nat_of_num_pos [of m]
+ by (auto simp add: less_eq_num_def less_num_def)
-lemma num_induct [case_names 1 Suc, induct type: num]:
- fixes P :: "num \<Rightarrow> bool"
- assumes 1: "P 1"
- and Suc: "\<And>n. P n \<Longrightarrow> P (n + 1)"
- shows "P n"
-proof (cases n)
- case (nat m) then show ?thesis by (induct m arbitrary: n)
- (auto simp: num_of_nat_Suc intro: 1 Suc split: split_if_asm)
-qed
+lemma less_num_code [numeral, simp, code]:
+ "m < One \<longleftrightarrow> False"
+ "One < One \<longleftrightarrow> False"
+ "One < Dig0 n \<longleftrightarrow> True"
+ "One < Dig1 n \<longleftrightarrow> True"
+ "Dig0 m < Dig0 n \<longleftrightarrow> m < n"
+ "Dig0 m < Dig1 n \<longleftrightarrow> m \<le> n"
+ "Dig1 m < Dig1 n \<longleftrightarrow> m < n"
+ "Dig1 m < Dig0 n \<longleftrightarrow> m < n"
+ using nat_of_num_pos [of n] nat_of_num_pos [of m]
+ by (auto simp add: less_eq_num_def less_num_def)
+
+text {* Rules using @{text One} and @{text inc} as constructors *}
+
+lemma add_One: "x + One = inc x"
+ by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc)
+
+lemma add_inc: "x + inc y = inc (x + y)"
+ by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc)
+
+lemma mult_One: "x * One = x"
+ by (simp add: num_eq_iff nat_of_num_mult)
+
+lemma mult_inc: "x * inc y = x * y + x"
+ by (simp add: num_eq_iff nat_of_num_mult nat_of_num_add nat_of_num_inc)
-rep_datatype "1::num" Dig0 Dig1 proof -
- fix P m
- assume 1: "P 1"
- and Dig0: "\<And>m. P m \<Longrightarrow> P (Dig0 m)"
- and Dig1: "\<And>m. P m \<Longrightarrow> P (Dig1 m)"
- obtain n where "0 < n" and m: "m = num_of_nat n"
- by (cases m) auto
- from `0 < n` have "P (num_of_nat n)" proof (induct n rule: num_induct_raw)
- case 1 from `0 < n` show ?case .
- next
- case 2 with 1 show ?case by (simp add: one_num_def)
- next
- case (3 n) then have "P (num_of_nat n)" by auto
- then have "P (Dig0 (num_of_nat n))" by (rule Dig0)
- with 3 show ?case by (simp add: Dig0_def plus_num_def num_of_nat_inverse)
- next
- case (4 n) then have "P (num_of_nat n)" by auto
- then have "P (Dig1 (num_of_nat n))" by (rule Dig1)
- with 4 show ?case by (simp add: Dig1_def one_num_def plus_num_def num_of_nat_inverse)
- qed
- with m show "P m" by simp
-next
- fix m n
- show "Dig0 m = Dig0 n \<longleftrightarrow> m = n"
- apply (cases m) apply (cases n)
- by (auto simp add: Dig0_def plus_num_def num_of_nat_inverse num_of_nat_inject)
-next
- fix m n
- show "Dig1 m = Dig1 n \<longleftrightarrow> m = n"
- apply (cases m) apply (cases n)
- by (auto simp add: Dig1_def plus_num_def num_of_nat_inverse num_of_nat_inject)
-next
- fix n
- show "1 \<noteq> Dig0 n"
- apply (cases n)
- by (auto simp add: Dig0_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)
-next
- fix n
- show "1 \<noteq> Dig1 n"
- apply (cases n)
- by (auto simp add: Dig1_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)
-next
- fix m n
- have "\<And>n m. n + n \<noteq> Suc (m + m)"
- proof -
- fix n m
- show "n + n \<noteq> Suc (m + m)"
- proof (induct m arbitrary: n)
- case 0 then show ?case by (cases n) simp_all
- next
- case (Suc m) then show ?case by (cases n) simp_all
- qed
- qed
- then show "Dig0 n \<noteq> Dig1 m"
- apply (cases n) apply (cases m)
- by (auto simp add: Dig0_def Dig1_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)
-qed
+text {* A double-and-decrement function *}
+
+primrec DigM :: "num \<Rightarrow> num" where
+ "DigM One = One"
+ | "DigM (Dig0 n) = Dig1 (DigM n)"
+ | "DigM (Dig1 n) = Dig1 (Dig0 n)"
+
+lemma DigM_plus_one: "DigM n + One = Dig0 n"
+ by (induct n) simp_all
+
+lemma add_One_commute: "One + n = n + One"
+ by (induct n) simp_all
-text {*
- From now on, there are two possible models for @{typ num}:
- as positive naturals (rules @{text "num_induct"}, @{text "num_cases"})
- and as digit representation (rules @{text "num.induct"}, @{text "num.cases"}).
+lemma one_plus_DigM: "One + DigM n = Dig0 n"
+ unfolding add_One_commute DigM_plus_one ..
+
+text {* Squaring and exponentiation *}
- It is not entirely clear in which context it is better to use
- the one or the other, or whether the construction should be reversed.
-*}
+primrec square :: "num \<Rightarrow> num" where
+ "square One = One"
+| "square (Dig0 n) = Dig0 (Dig0 (square n))"
+| "square (Dig1 n) = Dig1 (Dig0 (square n + n))"
+
+primrec pow :: "num \<Rightarrow> num \<Rightarrow> num"
+where
+ "pow x One = x"
+| "pow x (Dig0 y) = square (pow x y)"
+| "pow x (Dig1 y) = x * square (pow x y)"
subsection {* Binary numerals *}
@@ -251,21 +231,17 @@
structure using @{text of_num}.
*}
-ML {*
-structure DigSimps =
- NamedThmsFun(val name = "numeral"; val description = "Simplification rules for numerals")
-*}
-
-setup DigSimps.setup
-
class semiring_numeral = semiring + monoid_mult
begin
primrec of_num :: "num \<Rightarrow> 'a" where
- of_num_one [numeral]: "of_num 1 = 1"
+ of_num_one [numeral]: "of_num One = 1"
| "of_num (Dig0 n) = of_num n + of_num n"
| "of_num (Dig1 n) = of_num n + of_num n + 1"
+lemma of_num_inc: "of_num (inc x) = of_num x + 1"
+ by (induct x) (simp_all add: add_ac)
+
declare of_num.simps [simp del]
end
@@ -275,14 +251,14 @@
*}
ML {*
-fun mk_num 1 = @{term "1::num"}
+fun mk_num 1 = @{term One}
| mk_num k =
let
val (l, b) = Integer.div_mod k 2;
val bit = (if b = 0 then @{term Dig0} else @{term Dig1});
in bit $ (mk_num l) end;
-fun dest_num @{term "1::num"} = 1
+fun dest_num @{term One} = 1
| dest_num (@{term Dig0} $ n) = 2 * dest_num n
| dest_num (@{term Dig1} $ n) = 2 * dest_num n + 1;
@@ -301,7 +277,7 @@
parse_translation {*
let
fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)
- of (0, 1) => Const (@{const_name HOL.one}, dummyT)
+ of (0, 1) => Const (@{const_name One}, dummyT)
| (n, 0) => Const (@{const_name Dig0}, dummyT) $ num_of_int n
| (n, 1) => Const (@{const_name Dig1}, dummyT) $ num_of_int n
else raise Match;
@@ -322,7 +298,7 @@
dig 0 (int_of_num' n)
| int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =
dig 1 (int_of_num' n)
- | int_of_num' (Const (@{const_syntax HOL.one}, _)) = 1;
+ | int_of_num' (Const (@{const_syntax One}, _)) = 1;
fun num_tr' show_sorts T [n] =
let
val k = int_of_num' n;
@@ -336,45 +312,18 @@
in [(@{const_syntax of_num}, num_tr')] end
*}
-
-subsection {* Numeral operations *}
-
-text {*
- First, addition and multiplication on digits.
-*}
-
-lemma Dig_plus [numeral, simp, code]:
- "1 + 1 = Dig0 1"
- "1 + Dig0 m = Dig1 m"
- "1 + Dig1 m = Dig0 (m + 1)"
- "Dig0 n + 1 = Dig1 n"
- "Dig0 n + Dig0 m = Dig0 (n + m)"
- "Dig0 n + Dig1 m = Dig1 (n + m)"
- "Dig1 n + 1 = Dig0 (n + 1)"
- "Dig1 n + Dig0 m = Dig1 (n + m)"
- "Dig1 n + Dig1 m = Dig0 (n + m + 1)"
- by (simp_all add: add_ac Dig0_def Dig1_def)
-
-lemma Dig_times [numeral, simp, code]:
- "1 * 1 = (1::num)"
- "1 * Dig0 n = Dig0 n"
- "1 * Dig1 n = Dig1 n"
- "Dig0 n * 1 = Dig0 n"
- "Dig0 n * Dig0 m = Dig0 (n * Dig0 m)"
- "Dig0 n * Dig1 m = Dig0 (n * Dig1 m)"
- "Dig1 n * 1 = Dig1 n"
- "Dig1 n * Dig0 m = Dig0 (n * Dig0 m + m)"
- "Dig1 n * Dig1 m = Dig1 (n * Dig1 m + m)"
- by (simp_all add: left_distrib right_distrib add_ac Dig0_def Dig1_def)
+subsection {* Class-specific numeral rules *}
text {*
@{const of_num} is a morphism.
*}
+subsubsection {* Class @{text semiring_numeral} *}
+
context semiring_numeral
begin
-abbreviation "Num1 \<equiv> of_num 1"
+abbreviation "Num1 \<equiv> of_num One"
text {*
Alas, there is still the duplication of @{term 1},
@@ -386,18 +335,17 @@
*}
lemma of_num_plus_one [numeral]:
- "of_num n + 1 = of_num (n + 1)"
- by (rule sym, induct n) (simp_all add: Dig_plus of_num.simps add_ac)
+ "of_num n + 1 = of_num (n + One)"
+ by (rule sym, induct n) (simp_all add: of_num.simps add_ac)
lemma of_num_one_plus [numeral]:
- "1 + of_num n = of_num (n + 1)"
+ "1 + of_num n = of_num (n + One)"
unfolding of_num_plus_one [symmetric] add_commute ..
lemma of_num_plus [numeral]:
"of_num m + of_num n = of_num (m + n)"
by (induct n rule: num_induct)
- (simp_all add: Dig_plus of_num_one semigroup_add_class.add_assoc [symmetric, of m]
- add_ac of_num_plus_one [symmetric])
+ (simp_all add: add_One add_inc of_num_one of_num_inc add_ac)
lemma of_num_times_one [numeral]:
"of_num n * 1 = of_num n"
@@ -410,13 +358,13 @@
lemma of_num_times [numeral]:
"of_num m * of_num n = of_num (m * n)"
by (induct n rule: num_induct)
- (simp_all add: of_num_plus [symmetric]
- semiring_class.right_distrib right_distrib of_num_one)
+ (simp_all add: of_num_plus [symmetric] mult_One mult_inc
+ semiring_class.right_distrib right_distrib of_num_one of_num_inc)
end
-text {*
- Structures with a @{term 0}.
+subsubsection {*
+ Structures with a zero: class @{text semiring_1}
*}
context semiring_1
@@ -449,16 +397,13 @@
lemma nat_of_num_of_num: "nat_of_num = of_num"
proof
fix n
- have "of_num n = nat_of_num n" apply (induct n)
- apply (simp_all add: of_num.simps)
- using nat_of_num
- apply (simp_all add: one_num_def plus_num_def Dig0_def Dig1_def num_of_nat_inverse mem_def)
- done
+ have "of_num n = nat_of_num n"
+ by (induct n) (simp_all add: of_num.simps)
then show "nat_of_num n = of_num n" by simp
qed
-text {*
- Equality.
+subsubsection {*
+ Equality: class @{text semiring_char_0}
*}
context semiring_char_0
@@ -467,25 +412,27 @@
lemma of_num_eq_iff [numeral]:
"of_num m = of_num n \<longleftrightarrow> m = n"
unfolding of_nat_of_num [symmetric] nat_of_num_of_num [symmetric]
- of_nat_eq_iff nat_of_num_inject ..
+ of_nat_eq_iff num_eq_iff ..
lemma of_num_eq_one_iff [numeral]:
- "of_num n = 1 \<longleftrightarrow> n = 1"
+ "of_num n = 1 \<longleftrightarrow> n = One"
proof -
- have "of_num n = of_num 1 \<longleftrightarrow> n = 1" unfolding of_num_eq_iff ..
+ have "of_num n = of_num One \<longleftrightarrow> n = One" unfolding of_num_eq_iff ..
then show ?thesis by (simp add: of_num_one)
qed
lemma one_eq_of_num_iff [numeral]:
- "1 = of_num n \<longleftrightarrow> n = 1"
+ "1 = of_num n \<longleftrightarrow> n = One"
unfolding of_num_eq_one_iff [symmetric] by auto
end
-text {*
- Comparisons. Could be perhaps more general than here.
+subsubsection {*
+ Comparisons: class @{text ordered_semidom}
*}
+text {* Could be perhaps more general than here. *}
+
lemma (in ordered_semidom) of_num_pos: "0 < of_num n"
proof -
have "(0::nat) < of_num n"
@@ -498,44 +445,6 @@
ultimately show ?thesis by (simp add: of_nat_of_num)
qed
-instantiation num :: linorder
-begin
-
-definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
- [code del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
-
-definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
- [code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
-
-instance proof
-qed (auto simp add: less_eq_num_def less_num_def
- split_num_all num_of_nat_inverse num_of_nat_inject split: split_if_asm)
-
-end
-
-lemma less_eq_num_code [numeral, simp, code]:
- "(1::num) \<le> n \<longleftrightarrow> True"
- "Dig0 m \<le> 1 \<longleftrightarrow> False"
- "Dig1 m \<le> 1 \<longleftrightarrow> False"
- "Dig0 m \<le> Dig0 n \<longleftrightarrow> m \<le> n"
- "Dig0 m \<le> Dig1 n \<longleftrightarrow> m \<le> n"
- "Dig1 m \<le> Dig1 n \<longleftrightarrow> m \<le> n"
- "Dig1 m \<le> Dig0 n \<longleftrightarrow> m < n"
- using of_num_pos [of n, where ?'a = nat] of_num_pos [of m, where ?'a = nat]
- by (auto simp add: less_eq_num_def less_num_def nat_of_num_of_num of_num.simps)
-
-lemma less_num_code [numeral, simp, code]:
- "m < (1::num) \<longleftrightarrow> False"
- "(1::num) < 1 \<longleftrightarrow> False"
- "1 < Dig0 n \<longleftrightarrow> True"
- "1 < Dig1 n \<longleftrightarrow> True"
- "Dig0 m < Dig0 n \<longleftrightarrow> m < n"
- "Dig0 m < Dig1 n \<longleftrightarrow> m \<le> n"
- "Dig1 m < Dig1 n \<longleftrightarrow> m < n"
- "Dig1 m < Dig0 n \<longleftrightarrow> m < n"
- using of_num_pos [of n, where ?'a = nat] of_num_pos [of m, where ?'a = nat]
- by (auto simp add: less_eq_num_def less_num_def nat_of_num_of_num of_num.simps)
-
context ordered_semidom
begin
@@ -546,16 +455,16 @@
then show ?thesis by (simp add: of_nat_of_num)
qed
-lemma of_num_less_eq_one_iff [numeral]: "of_num n \<le> 1 \<longleftrightarrow> n = 1"
+lemma of_num_less_eq_one_iff [numeral]: "of_num n \<le> 1 \<longleftrightarrow> n = One"
proof -
- have "of_num n \<le> of_num 1 \<longleftrightarrow> n = 1"
+ have "of_num n \<le> of_num One \<longleftrightarrow> n = One"
by (cases n) (simp_all add: of_num_less_eq_iff)
then show ?thesis by (simp add: of_num_one)
qed
lemma one_less_eq_of_num_iff [numeral]: "1 \<le> of_num n"
proof -
- have "of_num 1 \<le> of_num n"
+ have "of_num One \<le> of_num n"
by (cases n) (simp_all add: of_num_less_eq_iff)
then show ?thesis by (simp add: of_num_one)
qed
@@ -569,51 +478,24 @@
lemma of_num_less_one_iff [numeral]: "\<not> of_num n < 1"
proof -
- have "\<not> of_num n < of_num 1"
+ have "\<not> of_num n < of_num One"
by (cases n) (simp_all add: of_num_less_iff)
then show ?thesis by (simp add: of_num_one)
qed
-lemma one_less_of_num_iff [numeral]: "1 < of_num n \<longleftrightarrow> n \<noteq> 1"
+lemma one_less_of_num_iff [numeral]: "1 < of_num n \<longleftrightarrow> n \<noteq> One"
proof -
- have "of_num 1 < of_num n \<longleftrightarrow> n \<noteq> 1"
+ have "of_num One < of_num n \<longleftrightarrow> n \<noteq> One"
by (cases n) (simp_all add: of_num_less_iff)
then show ?thesis by (simp add: of_num_one)
qed
end
-text {*
- Structures with subtraction @{term "op -"}.
+subsubsection {*
+ Structures with subtraction: class @{text semiring_1_minus}
*}
-text {* A decrement function *}
-
-primrec dec :: "num \<Rightarrow> num" where
- "dec 1 = 1"
- | "dec (Dig0 n) = (case n of 1 \<Rightarrow> 1 | _ \<Rightarrow> Dig1 (dec n))"
- | "dec (Dig1 n) = Dig0 n"
-
-declare dec.simps [simp del, code del]
-
-lemma Dig_dec [numeral, simp, code]:
- "dec 1 = 1"
- "dec (Dig0 1) = 1"
- "dec (Dig0 (Dig0 n)) = Dig1 (dec (Dig0 n))"
- "dec (Dig0 (Dig1 n)) = Dig1 (Dig0 n)"
- "dec (Dig1 n) = Dig0 n"
- by (simp_all add: dec.simps)
-
-lemma Dig_dec_plus_one:
- "dec n + 1 = (if n = 1 then Dig0 1 else n)"
- by (induct n)
- (auto simp add: Dig_plus dec.simps,
- auto simp add: Dig_plus split: num.splits)
-
-lemma Dig_one_plus_dec:
- "1 + dec n = (if n = 1 then Dig0 1 else n)"
- unfolding add_commute [of 1] Dig_dec_plus_one ..
-
class semiring_minus = semiring + minus + zero +
assumes minus_inverts_plus1: "a + b = c \<Longrightarrow> c - b = a"
assumes minus_minus_zero_inverts_plus1: "a + b = c \<Longrightarrow> b - c = 0 - a"
@@ -645,7 +527,7 @@
by (rule minus_minus_zero_inverts_plus1) (simp add: of_num_plus assms)
lemmas Dig_plus_eval =
- of_num_plus of_num_eq_iff Dig_plus refl [of "1::num", THEN eqTrueI] num.inject
+ of_num_plus of_num_eq_iff Dig_plus refl [of One, THEN eqTrueI] num.inject
simproc_setup numeral_minus ("of_num m - of_num n") = {*
let
@@ -683,17 +565,21 @@
by (simp add: minus_inverts_plus1)
lemma Dig_of_num_minus_one [numeral]:
- "of_num (Dig0 n) - 1 = of_num (dec (Dig0 n))"
+ "of_num (Dig0 n) - 1 = of_num (DigM n)"
"of_num (Dig1 n) - 1 = of_num (Dig0 n)"
- by (auto intro: minus_inverts_plus1 simp add: Dig_dec_plus_one of_num.simps of_num_plus_one)
+ by (auto intro: minus_inverts_plus1 simp add: DigM_plus_one of_num.simps of_num_plus_one)
lemma Dig_one_minus_of_num [numeral]:
- "1 - of_num (Dig0 n) = 0 - of_num (dec (Dig0 n))"
+ "1 - of_num (Dig0 n) = 0 - of_num (DigM n)"
"1 - of_num (Dig1 n) = 0 - of_num (Dig0 n)"
- by (auto intro: minus_minus_zero_inverts_plus1 simp add: Dig_dec_plus_one of_num.simps of_num_plus_one)
+ by (auto intro: minus_minus_zero_inverts_plus1 simp add: DigM_plus_one of_num.simps of_num_plus_one)
end
+subsubsection {*
+ Structures with negation: class @{text ring_1}
+*}
+
context ring_1
begin
@@ -735,21 +621,63 @@
end
-text {*
+subsubsection {*
+ Structures with exponentiation
+*}
+
+lemma of_num_square: "of_num (square x) = of_num x * of_num x"
+by (induct x)
+ (simp_all add: of_num.simps of_num_plus [symmetric] algebra_simps)
+
+lemma of_num_pow:
+ "(of_num (pow x y)::'a::{semiring_numeral,recpower}) = of_num x ^ of_num y"
+by (induct y)
+ (simp_all add: of_num.simps of_num_square of_num_times [symmetric]
+ power_Suc power_add)
+
+lemma power_of_num [numeral]:
+ "of_num x ^ of_num y = (of_num (pow x y)::'a::{semiring_numeral,recpower})"
+ by (rule of_num_pow [symmetric])
+
+lemma power_zero_of_num [numeral]:
+ "0 ^ of_num n = (0::'a::{semiring_0,recpower})"
+ using of_num_pos [where n=n and ?'a=nat]
+ by (simp add: power_0_left)
+
+lemma power_minus_one_double:
+ "(- 1) ^ (n + n) = (1::'a::{ring_1,recpower})"
+ by (induct n) (simp_all add: power_Suc)
+
+lemma power_minus_Dig0 [numeral]:
+ fixes x :: "'a::{ring_1,recpower}"
+ shows "(- x) ^ of_num (Dig0 n) = x ^ of_num (Dig0 n)"
+ by (subst power_minus)
+ (simp add: of_num.simps power_minus_one_double)
+
+lemma power_minus_Dig1 [numeral]:
+ fixes x :: "'a::{ring_1,recpower}"
+ shows "(- x) ^ of_num (Dig1 n) = - (x ^ of_num (Dig1 n))"
+ by (subst power_minus)
+ (simp add: of_num.simps power_Suc power_minus_one_double)
+
+declare power_one [numeral]
+
+
+subsubsection {*
Greetings to @{typ nat}.
*}
instance nat :: semiring_1_minus proof qed simp_all
-lemma Suc_of_num [numeral]: "Suc (of_num n) = of_num (n + 1)"
+lemma Suc_of_num [numeral]: "Suc (of_num n) = of_num (n + One)"
unfolding of_num_plus_one [symmetric] by simp
lemma nat_number:
"1 = Suc 0"
- "of_num 1 = Suc 0"
- "of_num (Dig0 n) = Suc (of_num (dec (Dig0 n)))"
+ "of_num One = Suc 0"
+ "of_num (Dig0 n) = Suc (of_num (DigM n))"
"of_num (Dig1 n) = Suc (of_num (Dig0 n))"
- by (simp_all add: of_num.simps Dig_dec_plus_one Suc_of_num)
+ by (simp_all add: of_num.simps DigM_plus_one Suc_of_num)
declare diff_0_eq_0 [numeral]
@@ -773,17 +701,17 @@
[code del]: "dup k = 2 * k"
lemma Dig_sub [code]:
- "sub 1 1 = 0"
- "sub (Dig0 m) 1 = of_num (dec (Dig0 m))"
- "sub (Dig1 m) 1 = of_num (Dig0 m)"
- "sub 1 (Dig0 n) = - of_num (dec (Dig0 n))"
- "sub 1 (Dig1 n) = - of_num (Dig0 n)"
+ "sub One One = 0"
+ "sub (Dig0 m) One = of_num (DigM m)"
+ "sub (Dig1 m) One = of_num (Dig0 m)"
+ "sub One (Dig0 n) = - of_num (DigM n)"
+ "sub One (Dig1 n) = - of_num (Dig0 n)"
"sub (Dig0 m) (Dig0 n) = dup (sub m n)"
"sub (Dig1 m) (Dig1 n) = dup (sub m n)"
"sub (Dig1 m) (Dig0 n) = dup (sub m n) + 1"
"sub (Dig0 m) (Dig1 n) = dup (sub m n) - 1"
apply (simp_all add: dup_def algebra_simps)
- apply (simp_all add: of_num_plus Dig_one_plus_dec)[4]
+ apply (simp_all add: of_num_plus one_plus_DigM)[4]
apply (simp_all add: of_num.simps)
done
@@ -805,7 +733,7 @@
by rule+
lemma one_int_code [code]:
- "1 = Pls 1"
+ "1 = Pls One"
by (simp add: of_num_one)
lemma plus_int_code [code]:
--- a/src/Tools/code/code_funcgr.ML Wed Feb 18 13:39:05 2009 +0100
+++ b/src/Tools/code/code_funcgr.ML Wed Feb 18 13:39:16 2009 +0100
@@ -1,8 +1,7 @@
(* Title: Tools/code/code_funcgr.ML
- ID: $Id$
Author: Florian Haftmann, TU Muenchen
-Retrieving, normalizing and structuring defining equations in graph
+Retrieving, normalizing and structuring code equations in graph
with explicit dependencies.
*)
--- a/src/Tools/code/code_funcgr_new.ML Wed Feb 18 13:39:05 2009 +0100
+++ b/src/Tools/code/code_funcgr_new.ML Wed Feb 18 13:39:16 2009 +0100
@@ -1,9 +1,8 @@
(* Title: Tools/code/code_funcgr.ML
- ID: $Id$
Author: Florian Haftmann, TU Muenchen
-Retrieving, well-sorting and structuring defining equations in graph
-with explicit dependencies.
+Retrieving, well-sorting and structuring code equations in graph
+with explicit dependencies -- the waisenhaus algorithm.
*)
signature CODE_FUNCGR =
@@ -28,12 +27,8 @@
type T = (((string * sort) list * typ) * (thm * bool) list) Graph.T;
-fun eqns funcgr =
- these o Option.map snd o try (Graph.get_node funcgr);
-
-fun typ funcgr =
- fst o Graph.get_node funcgr;
-
+fun eqns funcgr = these o Option.map snd o try (Graph.get_node funcgr);
+fun typ funcgr = fst o Graph.get_node funcgr;
fun all funcgr = Graph.keys funcgr;
fun pretty thy funcgr =
@@ -48,23 +43,22 @@
|> Pretty.chunks;
-(** generic combinators **)
-
-fun fold_consts f thms =
- thms
- |> maps (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of)
- |> (fold o fold_aterms) (fn Const c => f c | _ => I);
-
-fun consts_of (const, []) = []
- | consts_of (const, thms as _ :: _) =
- let
- fun the_const (c, _) = if c = const then I else insert (op =) c
- in fold_consts the_const (map fst thms) [] end;
-
-
(** graph algorithm **)
-(* some nonsense -- FIXME *)
+(* generic *)
+
+fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
+
+fun complete_proper_sort thy =
+ Sign.complete_sort thy #> filter (can (AxClass.get_info thy));
+
+fun inst_params thy tyco class =
+ map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
+ ((#params o AxClass.get_info thy) class);
+
+fun consts_of thy eqns = [] |> (fold o fold o fold_aterms)
+ (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
+ (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns);
fun lhs_rhss_of thy c =
let
@@ -73,33 +67,9 @@
|> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var);
val (lhs, _) = case eqns of [] => Code.default_typscheme thy c
| ((thm, _) :: _) => (snd o Code_Unit.head_eqn thy) thm;
- val rhss = fold_consts (fn (c, ty) =>
- insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty))) (map fst eqns) [];
+ val rhss = consts_of thy eqns;
in (lhs, rhss) end;
-fun inst_params thy tyco class =
- map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
- ((#params o AxClass.get_info thy) class);
-
-fun complete_proper_sort thy sort =
- Sign.complete_sort thy sort |> filter (can (AxClass.get_info thy));
-
-fun minimal_proper_sort thy sort =
- complete_proper_sort thy sort |> Sign.minimize_sort thy;
-
-fun dicts_of thy algebra (T, sort) =
- let
- fun class_relation (x, _) _ = x;
- fun type_constructor tyco xs class =
- inst_params thy tyco class @ (maps o maps) fst xs;
- fun type_variable (TFree (_, sort)) = map (pair []) sort;
- in
- flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
- { class_relation = class_relation, type_constructor = type_constructor,
- type_variable = type_variable } (T, minimal_proper_sort thy sort)
- handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
- end;
-
(* data structures *)
@@ -179,6 +149,7 @@
val classess = map (complete_proper_sort thy)
(Sign.arity_sorts thy tyco [class]);
val inst_params = inst_params thy tyco class;
+ (*FIXME also consider existing things here*)
in
vardeps
|> fold (fn superclass => assert thy (Inst (superclass, tyco))) superclasses
@@ -199,6 +170,7 @@
let
val _ = tracing "add_const";
val (lhs, rhss) = lhs_rhss_of thy c;
+ (*FIXME build lhs_rhss_of such that it points to existing graph if possible*)
fun styp_of (Type (tyco, tys)) = Tyco (tyco, map styp_of tys)
| styp_of (TFree (v, _)) = Var (Fun c, find_index (fn (v', _) => v = v') lhs);
val rhss' = (map o apsnd o map) styp_of rhss;
@@ -220,33 +192,62 @@
(* applying instantiations *)
+fun dicts_of thy (proj_sort, algebra) (T, sort) =
+ let
+ fun class_relation (x, _) _ = x;
+ fun type_constructor tyco xs class =
+ inst_params thy tyco class @ (maps o maps) fst xs;
+ fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
+ in
+ flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
+ { class_relation = class_relation, type_constructor = type_constructor,
+ type_variable = type_variable } (T, proj_sort sort)
+ handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
+ end;
+
+fun instances_of (*FIXME move to sorts.ML*) algebra =
+ let
+ val { classes, arities } = Sorts.rep_algebra algebra;
+ val sort_classes = fn cs => filter (member (op = o apsnd fst) cs)
+ (flat (rev (Graph.strong_conn classes)));
+ in
+ Symtab.fold (fn (a, cs) => append ((map (pair a) o sort_classes) cs))
+ arities []
+ end;
+
fun algebra_of thy vardeps =
let
val pp = Syntax.pp_global thy;
val thy_algebra = Sign.classes_of thy;
val is_proper = can (AxClass.get_info thy);
- val arities = Vargraph.fold (fn ((Fun _, _), _) => I
+ val classrels = Sorts.classrels_of thy_algebra
+ |> filter (is_proper o fst)
+ |> (map o apsnd) (filter is_proper);
+ val instances = instances_of thy_algebra
+ |> filter (is_proper o snd);
+ fun add_class (class, superclasses) algebra =
+ Sorts.add_class pp (class, Sorts.minimize_sort algebra superclasses) algebra;
+ val arity_constraints = Vargraph.fold (fn ((Fun _, _), _) => I
| ((Inst (class, tyco), k), ((_, classes), _)) =>
AList.map_default (op =)
((tyco, class), replicate (Sign.arity_number thy tyco) [])
(nth_map k (K classes))) vardeps [];
- val classrels = Sorts.classrels_of thy_algebra
- |> filter (is_proper o fst)
- |> (map o apsnd) (filter is_proper);
- fun add_arity (tyco, class) = case AList.lookup (op =) arities (tyco, class)
- of SOME sorts => Sorts.add_arities pp (tyco, [(class, sorts)])
- | NONE => if Sign.arity_number thy tyco = 0
- then (tracing (tyco ^ "::" ^ class); Sorts.add_arities pp (tyco, [(class, [])]))
- else I;
- val instances = Sorts.instances_of thy_algebra
- |> filter (is_proper o snd)
+ fun add_arity (tyco, class) algebra =
+ case AList.lookup (op =) arity_constraints (tyco, class)
+ of SOME sorts => (tracing (Pretty.output (Syntax.pretty_arity (ProofContext.init thy)
+ (tyco, sorts, [class])));
+ Sorts.add_arities pp
+ (tyco, [(class, map (Sorts.minimize_sort algebra) sorts)]) algebra)
+ | NONE => if Sign.arity_number thy tyco = 0
+ then Sorts.add_arities pp (tyco, [(class, [])]) algebra
+ else algebra;
in
Sorts.empty_algebra
- |> fold (Sorts.add_class pp) classrels
+ |> fold add_class classrels
|> fold add_arity instances
end;
-fun add_eqs thy algebra vardeps c gr =
+fun add_eqs thy (proj_sort, algebra) vardeps c gr =
let
val eqns = Code.these_eqns thy c
|> burrow_fst (Code_Unit.norm_args thy)
@@ -260,28 +261,27 @@
val tyscm = case eqns' of [] => Code.default_typscheme thy c
| ((thm, _) :: _) => (snd o Code_Unit.head_eqn thy) thm;
val _ = tracing ("tyscm " ^ makestring (map snd (fst tyscm)));
- val rhss = fold_consts (fn (c, ty) =>
- insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty))) (map fst eqns') [];
+ val rhss = consts_of thy eqns';
in
gr
|> Graph.new_node (c, (tyscm, eqns'))
- |> fold (fn (c', Ts) => ensure_eqs_dep thy algebra vardeps c c'
+ |> fold (fn (c', Ts) => ensure_eqs_dep thy (proj_sort, algebra) vardeps c c'
#-> (fn (vs, _) =>
- fold2 (ensure_match thy algebra vardeps c) Ts (map snd vs))) rhss
+ fold2 (ensure_match thy (proj_sort, algebra) vardeps c) Ts (map snd vs))) rhss
|> pair tyscm
end
-and ensure_match thy algebra vardeps c T sort gr =
+and ensure_match thy (proj_sort, algebra) vardeps c T sort gr =
gr
- |> fold (fn c' => ensure_eqs_dep thy algebra vardeps c c' #> snd)
- (dicts_of thy algebra (T, sort))
-and ensure_eqs_dep thy algebra vardeps c c' gr =
+ |> fold (fn c' => ensure_eqs_dep thy (proj_sort, algebra) vardeps c c' #> snd)
+ (dicts_of thy (proj_sort, algebra) (T, proj_sort sort))
+and ensure_eqs_dep thy (proj_sort, algebra) vardeps c c' gr =
gr
- |> ensure_eqs thy algebra vardeps c'
+ |> ensure_eqs thy (proj_sort, algebra) vardeps c'
||> Graph.add_edge (c, c')
-and ensure_eqs thy algebra vardeps c gr =
+and ensure_eqs thy (proj_sort, algebra) vardeps c gr =
case try (Graph.get_node gr) c
of SOME (tyscm, _) => (tyscm, gr)
- | NONE => add_eqs thy algebra vardeps c gr;
+ | NONE => add_eqs thy (proj_sort, algebra) vardeps c gr;
fun extend_graph thy cs gr =
let
@@ -291,13 +291,10 @@
val _ = tracing "obtaining algebra";
val algebra = algebra_of thy vardeps;
val _ = tracing "obtaining equations";
- val (_, gr) = fold_map (ensure_eqs thy algebra vardeps) cs gr;
+ val proj_sort = complete_proper_sort thy #> Sorts.minimize_sort algebra;
+ val (_, gr') = fold_map (ensure_eqs thy (proj_sort, algebra) vardeps) cs gr;
val _ = tracing "sort projection";
- val minimal_proper_sort = fn sort => sort
- |> Sorts.complete_sort (Sign.classes_of thy)
- |> filter (can (AxClass.get_info thy))
- |> Sorts.minimize_sort algebra;
- in ((minimal_proper_sort, algebra), gr) end;
+ in ((proj_sort, algebra), gr') end;
(** retrieval interfaces **)
@@ -320,7 +317,7 @@
insert (op =) (Sign.const_typargs thy (c, Logic.unvarifyT ty), c)) consts' [];
val typ_matches = maps (fn (tys, c) => tys ~~ map snd (fst (fst (Graph.get_node funcgr' c))))
const_matches;
- val dicts = maps (dicts_of thy (snd algebra')) typ_matches;
+ val dicts = maps (dicts_of thy algebra') typ_matches;
val (algebra'', funcgr'') = extend_graph thy dicts funcgr';
in (evaluator_lift (evaluator_funcgr algebra'') thm funcgr'', funcgr'') end;
--- a/src/Tools/code/code_haskell.ML Wed Feb 18 13:39:05 2009 +0100
+++ b/src/Tools/code/code_haskell.ML Wed Feb 18 13:39:16 2009 +0100
@@ -101,7 +101,7 @@
and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
let
- val (binds, t) = Code_Thingol.unfold_let (ICase cases);
+ val (binds, body) = Code_Thingol.unfold_let (ICase cases);
fun pr ((pat, ty), t) vars =
vars
|> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
@@ -110,20 +110,20 @@
in
Pretty.block_enclose (
str "let {",
- concat [str "}", str "in", pr_term tyvars thm vars' NOBR t]
+ concat [str "}", str "in", pr_term tyvars thm vars' NOBR body]
) ps
end
- | pr_case tyvars thm vars fxy (((td, ty), bs as _ :: _), _) =
+ | pr_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) =
let
- fun pr (pat, t) =
+ fun pr (pat, body) =
let
val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
- in semicolon [p, str "->", pr_term tyvars thm vars' NOBR t] end;
+ in semicolon [p, str "->", pr_term tyvars thm vars' NOBR body] end;
in
Pretty.block_enclose (
- concat [str "(case", pr_term tyvars thm vars NOBR td, str "of", str "{"],
+ concat [str "(case", pr_term tyvars thm vars NOBR t, str "of", str "{"],
str "})"
- ) (map pr bs)
+ ) (map pr clauses)
end
| pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) =
--- a/src/Tools/code/code_ml.ML Wed Feb 18 13:39:05 2009 +0100
+++ b/src/Tools/code/code_ml.ML Wed Feb 18 13:39:16 2009 +0100
@@ -130,7 +130,7 @@
and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
let
- val (binds, t') = Code_Thingol.unfold_let (ICase cases);
+ val (binds, body) = Code_Thingol.unfold_let (ICase cases);
fun pr ((pat, ty), t) vars =
vars
|> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty)
@@ -139,24 +139,24 @@
in
Pretty.chunks [
[str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
- [str ("in"), Pretty.fbrk, pr_term is_closure thm vars' NOBR t'] |> Pretty.block,
+ [str ("in"), Pretty.fbrk, pr_term is_closure thm vars' NOBR body] |> Pretty.block,
str ("end")
]
end
- | pr_case is_closure thm vars fxy (((td, ty), b::bs), _) =
+ | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) =
let
- fun pr delim (pat, t) =
+ fun pr delim (pat, body) =
let
val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
in
- concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR t]
+ concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
end;
in
(Pretty.enclose "(" ")" o single o brackify fxy) (
str "case"
- :: pr_term is_closure thm vars NOBR td
- :: pr "of" b
- :: map (pr "|") bs
+ :: pr_term is_closure thm vars NOBR t
+ :: pr "of" clause
+ :: map (pr "|") clauses
)
end
| pr_case is_closure thm vars fxy ((_, []), _) = str "raise Fail \"empty case\"";
@@ -434,26 +434,26 @@
and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
let
- val (binds, t') = Code_Thingol.unfold_let (ICase cases);
+ val (binds, body) = Code_Thingol.unfold_let (ICase cases);
fun pr ((pat, ty), t) vars =
vars
|> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty)
|>> (fn p => concat
[str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
val (ps, vars') = fold_map pr binds vars;
- in Pretty.chunks (ps @| pr_term is_closure thm vars' NOBR t') end
- | pr_case is_closure thm vars fxy (((td, ty), b::bs), _) =
+ in Pretty.chunks (ps @| pr_term is_closure thm vars' NOBR body) end
+ | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) =
let
- fun pr delim (pat, t) =
+ fun pr delim (pat, body) =
let
val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
- in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR t] end;
+ in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
in
(Pretty.enclose "(" ")" o single o brackify fxy) (
str "match"
- :: pr_term is_closure thm vars NOBR td
- :: pr "with" b
- :: map (pr "|") bs
+ :: pr_term is_closure thm vars NOBR t
+ :: pr "with" clause
+ :: map (pr "|") clauses
)
end
| pr_case is_closure thm vars fxy ((_, []), _) = str "failwith \"empty case\"";
--- a/src/Tools/code/code_thingol.ML Wed Feb 18 13:39:05 2009 +0100
+++ b/src/Tools/code/code_thingol.ML Wed Feb 18 13:39:16 2009 +0100
@@ -109,7 +109,7 @@
let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
-(** language core - types, patterns, expressions **)
+(** language core - types, terms **)
type vname = string;
@@ -131,31 +131,6 @@
| ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
(*see also signature*)
-(*
- variable naming conventions
-
- bare names:
- variable names v
- class names class
- type constructor names tyco
- datatype names dtco
- const names (general) c (const)
- constructor names co
- class parameter names classparam
- arbitrary name s
-
- v, c, co, classparam also annotated with types etc.
-
- constructs:
- sort sort
- type parameters vs
- type ty
- type schemes tysm
- term t
- (term as pattern) p
- instance (class, tyco) inst
- *)
-
val op `$$ = Library.foldl (op `$);
val op `|--> = Library.foldr (op `|->);
@@ -486,6 +461,12 @@
(* translation *)
+(*FIXME move to code(_unit).ML*)
+fun get_case_scheme thy c = case Code.get_case_data thy c
+ of SOME (proto_case_scheme as (_, case_pats)) =>
+ SOME (1 + (if null case_pats then 1 else length case_pats), proto_case_scheme)
+ | NONE => NONE
+
fun ensure_class thy (algbr as (_, algebra)) funcgr class =
let
val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
@@ -537,16 +518,8 @@
Global ((class, tyco), yss)
| class_relation (Local (classrels, v), subclass) superclass =
Local ((subclass, superclass) :: classrels, v);
- fun norm_typargs ys =
- let
- val raw_sort = map snd ys;
- val sort = Sorts.minimize_sort algebra raw_sort;
- in
- map_filter (fn (y, class) =>
- if member (op =) sort class then SOME y else NONE) ys
- end;
fun type_constructor tyco yss class =
- Global ((class, tyco), map norm_typargs yss);
+ Global ((class, tyco), (map o map) fst yss);
fun type_variable (TFree (v, sort)) =
let
val sort' = proj_sort sort;
@@ -669,58 +642,72 @@
translate_const thy algbr funcgr thm c_ty
##>> fold_map (translate_term thy algbr funcgr thm) ts
#>> (fn (t, ts) => t `$$ ts)
-and translate_case thy algbr funcgr thm n cases (app as ((c, ty), ts)) =
+and translate_case thy algbr funcgr thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
let
- val (tys, _) =
- (chop (1 + (if null cases then 1 else length cases)) o fst o strip_type) ty;
- val dt = nth ts n;
- val dty = nth tys n;
- fun is_undefined (Const (c, _)) = Code.is_undefined thy c
- | is_undefined _ = false;
- fun mk_case (co, n) t =
+ val (tys, _) = (chop num_args o fst o strip_type o snd) c_ty;
+ val t = nth ts t_pos;
+ val ty = nth tys t_pos;
+ val ts_clause = nth_drop t_pos ts;
+ fun mk_clause (co, num_co_args) t =
let
val _ = if (is_some o Code.get_datatype_of_constr thy) co then ()
else error ("Non-constructor " ^ quote co
^ " encountered in case pattern"
^ (case thm of NONE => ""
| SOME thm => ", in equation\n" ^ Display.string_of_thm thm))
- val (vs, body) = Term.strip_abs_eta n t;
- val selector = list_comb (Const (co, map snd vs ---> dty), map Free vs);
- in if is_undefined body then NONE else SOME (selector, body) end;
- fun mk_ds [] =
+ val (vs, body) = Term.strip_abs_eta num_co_args t;
+ val not_undefined = case body
+ of (Const (c, _)) => not (Code.is_undefined thy c)
+ | _ => true;
+ val pat = list_comb (Const (co, map snd vs ---> ty), map Free vs);
+ in (not_undefined, (pat, body)) end;
+ val clauses = if null case_pats then let val ([v_ty], body) =
+ Term.strip_abs_eta 1 (the_single ts_clause)
+ in [(true, (Free v_ty, body))] end
+ else map (uncurry mk_clause)
+ (AList.make (Code_Unit.no_args thy) case_pats ~~ ts_clause);
+ fun retermify ty (_, (IVar x, body)) =
+ (x, ty) `|-> body
+ | retermify _ (_, (pat, body)) =
let
- val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts))
- in [(Free v_ty, body)] end
- | mk_ds cases = map_filter (uncurry mk_case)
- (AList.make (Code_Unit.no_args thy) cases ~~ nth_drop n ts);
+ val (IConst (_, (_, tys)), ts) = unfold_app pat;
+ val vs = map2 (fn IVar x => fn ty => (x, ty)) ts tys;
+ in vs `|--> body end;
+ fun mk_icase const t ty clauses =
+ let
+ val (ts1, ts2) = chop t_pos (map (retermify ty) clauses);
+ in
+ ICase (((t, ty), map_filter (fn (b, d) => if b then SOME d else NONE) clauses),
+ const `$$ (ts1 @ t :: ts2))
+ end;
in
- translate_term thy algbr funcgr thm dt
- ##>> translate_typ thy algbr funcgr dty
- ##>> fold_map (fn (pat, body) => translate_term thy algbr funcgr thm pat
- ##>> translate_term thy algbr funcgr thm body) (mk_ds cases)
- ##>> translate_app_default thy algbr funcgr thm app
- #>> (fn (((dt, dty), ds), t0) => ICase (((dt, dty), ds), t0))
+ translate_const thy algbr funcgr thm c_ty
+ ##>> translate_term thy algbr funcgr thm t
+ ##>> translate_typ thy algbr funcgr ty
+ ##>> fold_map (fn (b, (pat, body)) => translate_term thy algbr funcgr thm pat
+ ##>> translate_term thy algbr funcgr thm body
+ #>> pair b) clauses
+ #>> (fn (((const, t), ty), ds) => mk_icase const t ty ds)
end
-and translate_app thy algbr funcgr thm ((c, ty), ts) = case Code.get_case_data thy c
- of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in
- if length ts < i then
+and translate_app thy algbr funcgr thm ((c, ty), ts) = case get_case_scheme thy c
+ of SOME (case_scheme as (num_args, _)) =>
+ if length ts < num_args then
let
val k = length ts;
- val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
+ val tys = (curry Library.take (num_args - k) o curry Library.drop k o fst o strip_type) ty;
val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
val vs = Name.names ctxt "a" tys;
in
fold_map (translate_typ thy algbr funcgr) tys
- ##>> translate_case thy algbr funcgr thm n cases ((c, ty), ts @ map Free vs)
+ ##>> translate_case thy algbr funcgr thm case_scheme ((c, ty), ts @ map Free vs)
#>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
end
- else if length ts > i then
- translate_case thy algbr funcgr thm n cases ((c, ty), Library.take (i, ts))
- ##>> fold_map (translate_term thy algbr funcgr thm) (Library.drop (i, ts))
+ else if length ts > num_args then
+ translate_case thy algbr funcgr thm case_scheme ((c, ty), Library.take (num_args, ts))
+ ##>> fold_map (translate_term thy algbr funcgr thm) (Library.drop (num_args, ts))
#>> (fn (t, ts) => t `$$ ts)
else
- translate_case thy algbr funcgr thm n cases ((c, ty), ts)
- end
+ translate_case thy algbr funcgr thm case_scheme ((c, ty), ts)
| NONE => translate_app_default thy algbr funcgr thm ((c, ty), ts);