--- a/src/HOL/GCD.thy Thu Jun 25 13:25:35 2009 +0200
+++ b/src/HOL/GCD.thy Thu Jun 25 13:36:46 2009 +0200
@@ -1,6 +1,6 @@
(* Title: GCD.thy
Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
- Thomas M. Rasmussen, Jeremy Avigad
+ Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow
This file deals with the functions gcd and lcm, and properties of
@@ -20,6 +20,7 @@
the congruence relations on the integers. The notion was extended to
the natural numbers by Chiaeb.
+Tobias Nipkow cleaned up a lot.
*)
@@ -247,11 +248,11 @@
lemma int_gcd_1 [simp]: "gcd (m::int) 1 = 1"
by (simp add: gcd_int_def)
-lemma nat_gcd_self [simp]: "gcd (x::nat) x = x"
- by simp
+lemma nat_gcd_idem: "gcd (x::nat) x = x"
+by simp
-lemma int_gcd_def [simp]: "gcd (x::int) x = abs x"
- by (subst int_gcd_abs, auto simp add: gcd_int_def)
+lemma int_gcd_idem: "gcd (x::int) x = abs x"
+by (subst int_gcd_abs, auto simp add: gcd_int_def)
declare gcd_nat.simps [simp del]
@@ -267,8 +268,6 @@
apply (blast dest: dvd_mod_imp_dvd)
done
-thm nat_gcd_dvd1 [transferred]
-
lemma int_gcd_dvd1 [iff]: "gcd (x::int) y dvd x"
apply (subst int_gcd_abs)
apply (rule dvd_trans)
@@ -308,7 +307,7 @@
by (rule zdvd_imp_le, auto)
lemma nat_gcd_greatest: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
- by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod)
+by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod)
lemma int_gcd_greatest:
assumes "(k::int) dvd m" and "k dvd n"
@@ -364,15 +363,6 @@
lemmas int_gcd_ac = int_gcd_assoc int_gcd_commute int_gcd_left_commute
-lemma nat_gcd_1_left [simp]: "gcd (1::nat) m = 1"
- by (subst nat_gcd_commute, simp)
-
-lemma nat_gcd_Suc_0_left [simp]: "gcd (Suc 0) m = Suc 0"
- by (subst nat_gcd_commute, simp add: One_nat_def)
-
-lemma int_gcd_1_left [simp]: "gcd (1::int) m = 1"
- by (subst int_gcd_commute, simp)
-
lemma nat_gcd_unique: "(d::nat) dvd a \<and> d dvd b \<and>
(\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
apply auto
@@ -395,6 +385,19 @@
apply (auto intro: int_gcd_greatest)
done
+lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
+by (metis dvd.eq_iff nat_gcd_unique)
+
+lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
+by (metis dvd.eq_iff nat_gcd_unique)
+
+lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
+by (metis abs_dvd_iff abs_eq_0 int_gcd_0_left int_gcd_abs int_gcd_unique)
+
+lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
+by (metis gcd_proj1_if_dvd_int int_gcd_commute)
+
+
text {*
\medskip Multiplication laws
*}
@@ -414,12 +417,6 @@
apply auto
done
-lemma nat_gcd_mult [simp]: "gcd (k::nat) (k * n) = k"
- by (rule nat_gcd_mult_distrib [of k 1 n, simplified, symmetric])
-
-lemma int_gcd_mult [simp]: "gcd (k::int) (k * n) = abs k"
- by (rule int_gcd_mult_distrib [of k 1 n, simplified, symmetric])
-
lemma nat_coprime_dvd_mult: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
apply (insert nat_gcd_mult_distrib [of m k n])
apply simp
@@ -517,42 +514,22 @@
done
lemma int_gcd_add1 [simp]: "gcd ((m::int) + n) n = gcd m n"
- apply (case_tac "n = 0", force)
- apply (subst (1 2) int_gcd_red)
- apply auto
-done
+by (metis int_gcd_red mod_add_self1 zadd_commute)
lemma int_gcd_add2 [simp]: "gcd m ((m::int) + n) = gcd m n"
- apply (subst int_gcd_commute)
- apply (subst add_commute)
- apply (subst int_gcd_add1)
- apply (subst int_gcd_commute)
- apply (rule refl)
-done
+by (metis int_gcd_add1 int_gcd_commute zadd_commute)
lemma nat_gcd_add_mult: "gcd (m::nat) (k * m + n) = gcd m n"
- by (induct k, simp_all add: ring_simps)
+by (metis mod_mult_self3 nat_gcd_commute nat_gcd_red)
lemma int_gcd_add_mult: "gcd (m::int) (k * m + n) = gcd m n"
- apply (subgoal_tac "ALL s. ALL m. ALL n.
- gcd m (int (s::nat) * m + n) = gcd m n")
- apply (case_tac "k >= 0")
- apply (drule_tac x = "nat k" in spec, force)
- apply (subst (1 2) int_gcd_neg2 [symmetric])
- apply (drule_tac x = "nat (- k)" in spec)
- apply (drule_tac x = "m" in spec)
- apply (drule_tac x = "-n" in spec)
- apply auto
- apply (rule nat_induct)
- apply auto
- apply (auto simp add: left_distrib)
- apply (subst add_assoc)
- apply simp
-done
+by (metis int_gcd_commute int_gcd_red mod_mult_self1 zadd_commute)
+
(* to do: differences, and all variations of addition rules
as simplification rules for nat and int *)
+(* FIXME remove iff *)
lemma nat_gcd_dvd_prod [iff]: "gcd (m::nat) n dvd k * n"
using mult_dvd_mono [of 1] by auto
@@ -714,20 +691,20 @@
qed
lemma int_coprime_lmult:
- assumes dab: "coprime (d::int) (a * b)" shows "coprime d a"
+ assumes "coprime (d::int) (a * b)" shows "coprime d a"
proof -
have "gcd d a dvd gcd d (a * b)"
by (rule int_gcd_greatest, auto)
- with dab show ?thesis
+ with assms show ?thesis
by auto
qed
lemma nat_coprime_rmult:
- assumes dab: "coprime (d::nat) (a * b)" shows "coprime d b"
+ assumes "coprime (d::nat) (a * b)" shows "coprime d b"
proof -
have "gcd d b dvd gcd d (a * b)"
by (rule nat_gcd_greatest, auto intro: dvd_mult)
- with dab show ?thesis
+ with assms show ?thesis
by auto
qed
@@ -937,6 +914,7 @@
ultimately show ?thesis by blast
qed
+(* FIXME move to Divides(?) *)
lemma nat_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
by (auto intro: nat_pow_divides_pow dvd_power_same)
@@ -1316,30 +1294,12 @@
lemma int_lcm_0 [simp]: "lcm (m::int) 0 = 0"
unfolding lcm_int_def by simp
-lemma nat_lcm_1 [simp]: "lcm (m::nat) 1 = m"
- unfolding lcm_nat_def by simp
-
-lemma nat_lcm_Suc_0 [simp]: "lcm (m::nat) (Suc 0) = m"
- unfolding lcm_nat_def by (simp add: One_nat_def)
-
-lemma int_lcm_1 [simp]: "lcm (m::int) 1 = abs m"
- unfolding lcm_int_def by simp
-
lemma nat_lcm_0_left [simp]: "lcm (0::nat) n = 0"
unfolding lcm_nat_def by simp
lemma int_lcm_0_left [simp]: "lcm (0::int) n = 0"
unfolding lcm_int_def by simp
-lemma nat_lcm_1_left [simp]: "lcm (1::nat) m = m"
- unfolding lcm_nat_def by simp
-
-lemma nat_lcm_Suc_0_left [simp]: "lcm (Suc 0) m = m"
- unfolding lcm_nat_def by (simp add: One_nat_def)
-
-lemma int_lcm_1_left [simp]: "lcm (1::int) m = abs m"
- unfolding lcm_int_def by simp
-
lemma nat_lcm_commute: "lcm (m::nat) n = lcm n m"
unfolding lcm_nat_def by (simp add: nat_gcd_commute ring_simps)
@@ -1348,34 +1308,14 @@
lemma nat_lcm_pos:
- assumes mpos: "(m::nat) > 0"
- and npos: "n>0"
- shows "lcm m n > 0"
-proof(rule ccontr, simp add: lcm_nat_def nat_gcd_zero)
- assume h:"m*n div gcd m n = 0"
- from mpos npos have "gcd m n \<noteq> 0" using nat_gcd_zero by simp
- hence gcdp: "gcd m n > 0" by simp
- with h
- have "m*n < gcd m n"
- by (cases "m * n < gcd m n")
- (auto simp add: div_if[OF gcdp, where m="m*n"])
- moreover
- have "gcd m n dvd m" by simp
- with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
- with npos have t1:"gcd m n*n \<le> m*n" by simp
- have "gcd m n \<le> gcd m n*n" using npos by simp
- with t1 have "gcd m n \<le> m*n" by arith
- ultimately show "False" by simp
-qed
+ "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
+by (metis gr0I mult_is_0 nat_prod_gcd_lcm)
lemma int_lcm_pos:
- assumes mneq0: "(m::int) ~= 0"
- and npos: "n ~= 0"
- shows "lcm m n > 0"
-
+ "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
apply (subst int_lcm_abs)
apply (rule nat_lcm_pos [transferred])
- using prems apply auto
+ apply auto
done
lemma nat_dvd_pos:
@@ -1417,13 +1357,11 @@
qed
lemma int_lcm_least:
- assumes "(m::int) dvd k" and "n dvd k"
- shows "lcm m n dvd k"
-
- apply (subst int_lcm_abs)
- apply (rule dvd_trans)
- apply (rule nat_lcm_least [transferred, of _ "abs k" _])
- using prems apply auto
+ "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
+apply (subst int_lcm_abs)
+apply (rule dvd_trans)
+apply (rule nat_lcm_least [transferred, of _ "abs k" _])
+apply auto
done
lemma nat_lcm_dvd1: "(m::nat) dvd lcm m n"
@@ -1481,23 +1419,23 @@
(\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
by (auto intro: dvd_anti_sym [transferred] int_lcm_least)
-lemma nat_lcm_dvd_eq [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
+lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
apply (rule sym)
apply (subst nat_lcm_unique [symmetric])
apply auto
done
-lemma int_lcm_dvd_eq [simp]: "0 <= y \<Longrightarrow> (x::int) dvd y \<Longrightarrow> lcm x y = y"
+lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = abs y"
apply (rule sym)
apply (subst int_lcm_unique [symmetric])
apply auto
done
-lemma nat_lcm_dvd_eq' [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
- by (subst nat_lcm_commute, erule nat_lcm_dvd_eq)
+lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
+by (subst nat_lcm_commute, erule lcm_proj2_if_dvd_nat)
-lemma int_lcm_dvd_eq' [simp]: "y >= 0 \<Longrightarrow> (x::int) dvd y \<Longrightarrow> lcm y x = y"
- by (subst int_lcm_commute, erule (1) int_lcm_dvd_eq)
+lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
+by (subst int_lcm_commute, erule lcm_proj2_if_dvd_int)
lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
--- a/src/HOL/Tools/res_hol_clause.ML Thu Jun 25 13:25:35 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML Thu Jun 25 13:36:46 2009 +0200
@@ -12,8 +12,6 @@
val comb_B: thm
val comb_C: thm
val comb_S: thm
- datatype type_level = T_FULL | T_CONST
- val typ_level: type_level
val minimize_applies: bool
type axiom_name = string
type polarity = bool
@@ -59,10 +57,8 @@
val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal";
-(*The different translations of types*)
-datatype type_level = T_FULL | T_CONST;
-
-val typ_level = T_CONST;
+(* Parameter t_full below indicates that full type information is to be
+exported *)
(*If true, each function will be directly applied to as many arguments as possible, avoiding
use of the "apply" operator. Use of hBOOL is also minimized.*)
@@ -260,26 +256,26 @@
fun wrap_type_if t_full cnh (head, s, tp) =
if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s;
-fun string_of_combterm t_full cma cnh t =
+fun string_of_combterm (params as (t_full, cma, cnh)) t =
let val (head, args) = strip_comb t
in wrap_type_if t_full cnh (head,
- string_of_applic t_full cma (head, map (string_of_combterm t_full cma cnh) args),
+ string_of_applic t_full cma (head, map (string_of_combterm (params)) args),
type_of_combterm t)
end;
(*Boolean-valued terms are here converted to literals.*)
-fun boolify t_full cma cnh t =
- "hBOOL" ^ RC.paren_pack [string_of_combterm t_full cma cnh t];
+fun boolify params t =
+ "hBOOL" ^ RC.paren_pack [string_of_combterm params t];
-fun string_of_predicate t_full cma cnh t =
+fun string_of_predicate (params as (_,_,cnh)) t =
case t of
(CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
(*DFG only: new TPTP prefers infix equality*)
- ("equal" ^ RC.paren_pack [string_of_combterm t_full cma cnh t1, string_of_combterm t_full cma cnh t2])
+ ("equal" ^ RC.paren_pack [string_of_combterm params t1, string_of_combterm params t2])
| _ =>
case #1 (strip_comb t) of
- CombConst(c,_,_) => if needs_hBOOL cnh c then boolify t_full cma cnh t else string_of_combterm t_full cma cnh t
- | _ => boolify t_full cma cnh t;
+ CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t
+ | _ => boolify params t;
fun string_of_clausename (cls_id,ax_name) =
RC.clause_prefix ^ RC.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
@@ -290,23 +286,23 @@
(*** tptp format ***)
-fun tptp_of_equality t_full cma cnh pol (t1,t2) =
+fun tptp_of_equality params pol (t1,t2) =
let val eqop = if pol then " = " else " != "
- in string_of_combterm t_full cma cnh t1 ^ eqop ^ string_of_combterm t_full cma cnh t2 end;
+ in string_of_combterm params t1 ^ eqop ^ string_of_combterm params t2 end;
-fun tptp_literal t_full cma cnh (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
- tptp_of_equality t_full cma cnh pol (t1,t2)
- | tptp_literal t_full cma cnh (Literal(pol,pred)) =
- RC.tptp_sign pol (string_of_predicate t_full cma cnh pred);
+fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
+ tptp_of_equality params pol (t1,t2)
+ | tptp_literal params (Literal(pol,pred)) =
+ RC.tptp_sign pol (string_of_predicate params pred);
(*Given a clause, returns its literals paired with a list of literals concerning TFrees;
the latter should only occur in conjecture clauses.*)
-fun tptp_type_lits t_full cma cnh pos (Clause{literals, ctypes_sorts, ...}) =
- (map (tptp_literal t_full cma cnh) literals,
+fun tptp_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
+ (map (tptp_literal params) literals,
map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts));
-fun clause2tptp (t_full, cma, cnh) (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
- let val (lits,tylits) = tptp_type_lits t_full cma cnh (kind = RC.Conjecture) cls
+fun clause2tptp params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
+ let val (lits,tylits) = tptp_type_lits params (kind = RC.Conjecture) cls
in
(RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
end;
@@ -314,10 +310,10 @@
(*** dfg format ***)
-fun dfg_literal t_full cma cnh (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate t_full cma cnh pred);
+fun dfg_literal params (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate params pred);
-fun dfg_type_lits t_full cma cnh pos (Clause{literals, ctypes_sorts, ...}) =
- (map (dfg_literal t_full cma cnh) literals,
+fun dfg_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
+ (map (dfg_literal params) literals,
map (RC.dfg_of_typeLit pos) (RC.add_typs ctypes_sorts));
fun get_uvars (CombConst _) vars = vars
@@ -328,8 +324,8 @@
fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
-fun clause2dfg (t_full, cma, cnh) (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
- let val (lits,tylits) = dfg_type_lits t_full cma cnh (kind = RC.Conjecture) cls
+fun clause2dfg params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
+ let val (lits,tylits) = dfg_type_lits params (kind = RC.Conjecture) cls
val vars = dfg_vars cls
val tvars = RC.get_tvar_strs ctypes_sorts
in
@@ -341,7 +337,7 @@
fun addtypes tvars tab = List.foldl RC.add_foltype_funcs tab tvars;
-fun add_decls t_full cma cnh (CombConst(c,tp,tvars), (funcs,preds)) =
+fun add_decls (t_full, cma, cnh) (CombConst(c,tp,tvars), (funcs,preds)) =
if c = "equal" then (addtypes tvars funcs, preds)
else
let val arity = min_arity_of cma c
@@ -351,20 +347,20 @@
if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds)
else (addtypes tvars funcs, addit preds)
end
- | add_decls _ _ _ (CombVar(_,ctp), (funcs,preds)) =
+ | add_decls _ (CombVar(_,ctp), (funcs,preds)) =
(RC.add_foltype_funcs (ctp,funcs), preds)
- | add_decls t_full cma cnh (CombApp(P,Q),decls) = add_decls t_full cma cnh (P,add_decls t_full cma cnh (Q,decls));
+ | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls));
-fun add_literal_decls t_full cma cnh (Literal(_,c), decls) = add_decls t_full cma cnh (c,decls);
+fun add_literal_decls params (Literal(_,c), decls) = add_decls params (c,decls);
-fun add_clause_decls t_full cma cnh (Clause {literals, ...}, decls) =
- List.foldl (add_literal_decls t_full cma cnh) decls literals
+fun add_clause_decls params (Clause {literals, ...}, decls) =
+ List.foldl (add_literal_decls params) decls literals
handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
-fun decls_of_clauses (t_full, cma, cnh) clauses arity_clauses =
+fun decls_of_clauses params clauses arity_clauses =
let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab)
val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
- val (functab,predtab) = (List.foldl (add_clause_decls t_full cma cnh) (init_functab, init_predtab) clauses)
+ val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses)
in
(Symtab.dest (List.foldl RC.add_arityClause_funcs functab arity_clauses),
Symtab.dest predtab)