# HG changeset patch
# User wenzelm
# Date 1245929806 -7200
# Node ID b97b34e7c853711f4cca1c56918c8a21f0cb444a
# Parent  477f2abf90a4940c67b704dc22ad0f2ec853fc0d# Parent  203d5e61e3bcc9cbe924eb123d325106958cb33b
merged

diff -r 203d5e61e3bc -r b97b34e7c853 src/HOL/GCD.thy
--- 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)"
diff -r 203d5e61e3bc -r b97b34e7c853 src/HOL/NewNumberTheory/Residues.thy
--- a/src/HOL/NewNumberTheory/Residues.thy	Thu Jun 25 13:25:35 2009 +0200
+++ b/src/HOL/NewNumberTheory/Residues.thy	Thu Jun 25 13:36:46 2009 +0200
@@ -202,9 +202,6 @@
   apply (subgoal_tac "a mod m ~= 0")
   apply arith
   apply auto
-  apply (subst (asm) int_gcd_commute)
-  apply (subst (asm) int_gcd_mult)
-  apply auto
   apply (subst (asm) int_gcd_red)
   apply (subst int_gcd_commute, assumption)
 done
diff -r 203d5e61e3bc -r b97b34e7c853 src/HOL/Tools/res_hol_clause.ML
--- 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)