# HG changeset patch # User ballarin # Date 1038477042 -3600 # Node ID 7de9342aca7a2cecb4cfafb166afcb5d624523bf # Parent 50dcee1c509ecdde702936ee25437b751d3bc79e HOL-Algebra partially ported to Isar. diff -r 50dcee1c509e -r 7de9342aca7a NEWS --- a/NEWS Wed Nov 27 17:25:41 2002 +0100 +++ b/NEWS Thu Nov 28 10:50:42 2002 +0100 @@ -6,6 +6,9 @@ *** General *** +* Provers/linorder: New generic prover for transitivity reasoning over +linear orders. Note: this prover is not efficient! + * Provers/simplifier: - Completely reimplemented Asm_full_simp_tac: @@ -87,6 +90,10 @@ *** HOL *** +* New tactic "trans_tac" and method "trans" instantiate +Provers/linorder.ML for axclasses "order" and "linorder" (predicates +"<=", "<" and "="). + * function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp"; diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/abstract/Factor.ML --- a/src/HOL/Algebra/abstract/Factor.ML Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/Algebra/abstract/Factor.ML Thu Nov 28 10:50:42 2002 +0100 @@ -4,29 +4,29 @@ Author: Clemens Ballarin, started 25 November 1997 *) -goalw Ring.thy [assoc_def] "!! c::'a::factorial. \ +Goalw [thm "assoc_def"] "!! c::'a::factorial. \ \ [| irred c; irred a; irred b; c dvd a*b |] ==> c assoc a | c assoc b"; -by (ftac factorial_prime 1); -by (rewrite_goals_tac [irred_def, prime_def]); +by (ftac (thm "factorial_prime") 1); +by (rewrite_goals_tac [thm "irred_def", thm "prime_def"]); by (Blast_tac 1); qed "irred_dvd_lemma"; -goalw Ring.thy [assoc_def] "!! c::'a::factorial. \ -\ [| irred c; a dvd <1> |] ==> \ +Goalw [thm "assoc_def"] "!! c::'a::factorial. \ +\ [| irred c; a dvd 1 |] ==> \ \ (ALL b : set factors. irred b) & c dvd foldr op* factors a --> \ \ (EX d. c assoc d & d : set factors)"; by (induct_tac "factors" 1); (* Base case: c dvd a contradicts irred c *) -by (full_simp_tac (simpset() addsimps [irred_def]) 1); +by (full_simp_tac (simpset() addsimps [thm "irred_def"]) 1); by (blast_tac (claset() addIs [dvd_trans_ring]) 1); (* Induction step *) -by (ftac factorial_prime 1); -by (full_simp_tac (simpset() addsimps [irred_def, prime_def]) 1); +by (ftac (thm "factorial_prime") 1); +by (full_simp_tac (simpset() addsimps [thm "irred_def", thm "prime_def"]) 1); by (Blast_tac 1); qed "irred_dvd_list_lemma"; -goal Ring.thy "!! c::'a::factorial. \ -\ [| irred c; ALL b : set factors. irred b; a dvd <1>; \ +Goal "!! c::'a::factorial. \ +\ [| irred c; ALL b : set factors. irred b; a dvd 1; \ \ c dvd foldr op* factors a |] ==> \ \ EX d. c assoc d & d : set factors"; by (rtac (irred_dvd_list_lemma RS mp) 1); diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/abstract/Factor.thy --- a/src/HOL/Algebra/abstract/Factor.thy Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/Algebra/abstract/Factor.thy Thu Nov 28 10:50:42 2002 +0100 @@ -7,12 +7,12 @@ Factor = Ring + consts - Factorisation :: ['a::ringS, 'a list, 'a] => bool + Factorisation :: ['a::ring, 'a list, 'a] => bool (* factorisation of x into a list of irred factors and a unit u *) defs Factorisation_def "Factorisation x factors u == x = foldr op* factors u & - (ALL a : set factors. irred a) & u dvd <1>" + (ALL a : set factors. irred a) & u dvd 1" end diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/abstract/Ideal.ML --- a/src/HOL/Algebra/abstract/Ideal.ML Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/Algebra/abstract/Ideal.ML Thu Nov 28 10:50:42 2002 +0100 @@ -51,7 +51,11 @@ Goal "is_ideal {x::'a::ring. EX u v. x = a * u + b * v}"; by (rtac is_idealI 1); -by Auto_tac; +(* by Auto_tac; FIXME: makes Zumkeller's order fail (raises exn Domain) *) +by (Clarify_tac 1); +by (Clarify_tac 2); +by (Clarify_tac 3); +by (Clarify_tac 4); by (res_inst_tac [("x", "u+ua")] exI 1); by (res_inst_tac [("x", "v+va")] exI 1); by (res_inst_tac [("x", "-u")] exI 2); @@ -60,7 +64,7 @@ by (res_inst_tac [("x", "0")] exI 3); by (res_inst_tac [("x", "u * r")] exI 4); by (res_inst_tac [("x", "v * r")] exI 4); -by (REPEAT (simp_tac (simpset() addsimps [r_distr, l_distr, r_minus, minus_add, m_assoc]@a_ac) 1)); +by (REPEAT (Simp_tac 1)); qed "is_ideal_2"; (* ideal_of *) @@ -73,9 +77,10 @@ by Auto_tac; qed "generator_in_ideal"; -Goalw [ideal_of_def] "ideal_of {<1>::'a::ring} = UNIV"; -by (force_tac (claset() addDs [is_ideal_mult], simpset()) 1); - (* loops if is_ideal_mult is added as non-safe rule *) +Goalw [ideal_of_def] "ideal_of {1::'a::ring} = UNIV"; +by (force_tac (claset() addDs [is_ideal_mult], + simpset() addsimps [l_one] delsimprocs [ring_simproc]) 1); + (* FIXME: Zumkeller's order raises Domain exn *) qed "ideal_of_one_eq"; Goalw [ideal_of_def] "ideal_of {} = {0::'a::ring}"; @@ -101,11 +106,13 @@ by (rtac subsetI 1); by (dtac InterD 1); by (assume_tac 2); -by (auto_tac (claset() addIs [is_ideal_2], simpset())); -by (res_inst_tac [("x", "<1>")] exI 1); +by (auto_tac (claset() addIs [is_ideal_2], + simpset() delsimprocs [ring_simproc])); +(* FIXME: Zumkeller's order *) +by (res_inst_tac [("x", "1")] exI 1); by (res_inst_tac [("x", "0")] exI 1); by (res_inst_tac [("x", "0")] exI 2); -by (res_inst_tac [("x", "<1>")] exI 2); +by (res_inst_tac [("x", "1")] exI 2); by (Simp_tac 1); by (Simp_tac 1); qed "ideal_of_2_structure"; @@ -204,18 +211,18 @@ by (rtac in_pideal_imp_dvd 1); by (Asm_simp_tac 1); by (res_inst_tac [("x", "0")] exI 1); -by (res_inst_tac [("x", "<1>")] exI 1); +by (res_inst_tac [("x", "1")] exI 1); by (Simp_tac 1); qed "not_dvd_psubideal"; -Goalw [irred_def] +Goalw [thm "irred_def"] "[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I"; by (dtac is_pidealD 1); by (etac exE 1); by (Clarify_tac 1); by (eres_inst_tac [("x", "aa")] allE 1); by (Clarify_tac 1); -by (dres_inst_tac [("a", "<1>")] dvd_imp_subideal 1); +by (dres_inst_tac [("a", "1")] dvd_imp_subideal 1); by (auto_tac (claset(), simpset() addsimps [ideal_of_one_eq])); qed "irred_imp_max_ideal"; @@ -271,20 +278,21 @@ (* Primeness condition *) -Goalw [prime_def] "irred a ==> prime (a::'a::pid)"; +Goalw [thm "prime_def"] "irred a ==> prime (a::'a::pid)"; by (rtac conjI 1); by (rtac conjI 2); by (Clarify_tac 3); -by (dres_inst_tac [("I", "ideal_of {a, b}"), ("x", "<1>")] +by (dres_inst_tac [("I", "ideal_of {a, b}"), ("x", "1")] irred_imp_max_ideal 3); by (auto_tac (claset() addIs [ideal_of_is_ideal, pid_ax], - simpset() addsimps [irred_def, not_dvd_psubideal, pid_ax])); + simpset() addsimps [thm "irred_def", not_dvd_psubideal, pid_ax])); by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1); by (Clarify_tac 1); by (dres_inst_tac [("f", "op* aa")] arg_cong 1); by (full_simp_tac (simpset() addsimps [r_distr]) 1); -by (etac ssubst 1); -by (asm_simp_tac (simpset() addsimps [m_assoc RS sym]) 1); +by (etac subst 1); +by (asm_simp_tac (simpset() addsimps [m_assoc RS sym] + delsimprocs [ring_simproc]) 1); qed "pid_irred_imp_prime"; (* Fields are Pid *) @@ -294,7 +302,7 @@ by (Simp_tac 1); by (rtac subset_trans 1); by (rtac dvd_imp_subideal 2); -by (rtac field_ax 2); +by (rtac (thm "field_ax") 2); by (assume_tac 2); by (simp_tac (simpset() addsimps [ideal_of_one_eq]) 1); qed "field_pideal_univ"; diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/abstract/Ideal.thy --- a/src/HOL/Algebra/abstract/Ideal.thy Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/Algebra/abstract/Ideal.thy Thu Nov 28 10:50:42 2002 +0100 @@ -7,9 +7,9 @@ Ideal = Ring + consts - ideal_of :: ('a::ringS) set => 'a set - is_ideal :: ('a::ringS) set => bool - is_pideal :: ('a::ringS) set => bool + ideal_of :: ('a::ring) set => 'a set + is_ideal :: ('a::ring) set => bool + is_pideal :: ('a::ring) set => bool defs is_ideal_def "is_ideal I == (ALL a: I. ALL b: I. a + b : I) & diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/abstract/NatSum.ML --- a/src/HOL/Algebra/abstract/NatSum.ML Wed Nov 27 17:25:41 2002 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,215 +0,0 @@ -(* - Sums with naturals as index domain - $Id$ - Author: Clemens Ballarin, started 12 December 1996 -*) - -section "Basic Properties"; - -Goal "setsum f {..0::nat} = (f 0::'a::ring)"; -by (Asm_simp_tac 1); -qed "SUM_0"; - -Goal "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::ring)"; -by (simp_tac (simpset() addsimps [atMost_Suc]) 1); -qed "SUM_Suc"; - -Addsimps [SUM_0, SUM_Suc]; - -Goal - "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::ring)"; -by (induct_tac "n" 1); -(* Base case *) -by (Simp_tac 1); -(* Induction step *) -by (asm_full_simp_tac (simpset() addsimps [a_assoc]) 1); -qed "SUM_Suc2"; - -(* Congruence rules *) - -Goal "ALL j'::nat. j=j' --> (ALL i. i<=j' --> f i = (f' i :: 'a :: ring)) \ -\ --> setsum f {..j} = setsum f' {..j'}"; -by (induct_tac "j" 1); -by Auto_tac; -bind_thm ("SUM_cong", (impI RS allI) RSN (2, result() RS spec RS mp RS mp)); -Addcongs [SUM_cong]; - -(* Results needed for the development of polynomials *) - -section "Ring Properties"; - -Goal "setsum (%i. 0) {..n::nat} = (0::'a::ring)"; -by (induct_tac "n" 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -qed "SUM_zero"; - -Addsimps [SUM_zero]; - -Goal - "!!f::nat=>'a::ring. \ -\ setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}"; -by (induct_tac "n" 1); -(* Base case *) -by (Simp_tac 1); -(* Induction step *) -by (asm_simp_tac (simpset() addsimps a_ac) 1); -qed "SUM_add"; - -Goal - "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"; -by (induct_tac "n" 1); -(* Base case *) -by (Simp_tac 1); -(* Induction step *) -by (asm_simp_tac (simpset() addsimps [l_distr]) 1); -qed "SUM_ldistr"; - -Goal - "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}"; -by (induct_tac "n" 1); -(* Base case *) -by (Simp_tac 1); -(* Induction step *) -by (asm_simp_tac (simpset() addsimps [r_distr]) 1); -qed "SUM_rdistr"; - -section "Results for the Construction of Polynomials"; - -Goal - "!!a::nat=>'a::ring. k <= n --> \ -\ setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} = \ -\ setsum (%j. a j * setsum (%i. b i * c (n-j-i)) {..k-j}) {..k}"; -by (induct_tac "k" 1); -(* Base case *) -by (simp_tac (simpset() addsimps [m_assoc]) 1); -(* Induction step *) -by (rtac impI 1); -by (etac impE 1); -by (arith_tac 1); -by (asm_simp_tac - (simpset() addsimps a_ac@ - [Suc_diff_le, l_distr, r_distr, m_assoc, SUM_add]) 1); -by (asm_simp_tac (simpset() addsimps a_ac@ [SUM_ldistr, m_assoc]) 1); -qed_spec_mp "poly_assoc_lemma1"; - -Goal - "!!a::nat=>'a::ring. \ -\ setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..n} = \ -\ setsum (%j. a j * setsum (%i. b i * c (n-(j+i))) {..n-j}) {..n}"; -by (asm_simp_tac (simpset() addsimps [poly_assoc_lemma1]) 1); -qed "poly_assoc_lemma"; - -Goal - "!! a::nat=>'a::ring. j <= n --> \ -\ setsum (%i. a i * b (n-i)) {..j} = \ -\ setsum (%i. a (n-i-(n-j)) * b (i+(n-j))) {..j}"; -by (Simp_tac 1); -by (induct_tac "j" 1); -(* Base case *) -by (Simp_tac 1); -(* Induction step *) -by (stac SUM_Suc2 1); -by (asm_simp_tac (simpset() addsimps [a_comm]) 1); -qed "poly_comm_lemma1"; - -Goal - "!!a::nat=>'a::ring. \ -\ setsum (%i. a i * b (n-i)) {..n} = \ -\ setsum (%i. a (n-i) * b i) {..n}"; -by (cut_inst_tac [("j", "n"), ("n", "n")] poly_comm_lemma1 1); -by (Asm_full_simp_tac 1); -qed "poly_comm_lemma"; - -section "Changing the Range of Summation"; - -Goal - "!! f::(nat=>'a::ring). \ -\ setsum (%i. if i = x then f i else 0) {..n} = (if x <= n then f x else 0)"; -by (induct_tac "n" 1); -(* Base case *) -by (Simp_tac 1); -(* Induction step *) -by (Asm_simp_tac 1); -by (Clarify_tac 1); -by (res_inst_tac [("f", "f")] arg_cong 1); -by (arith_tac 1); -qed "SUM_if_singleton"; - -Goal - "!! f::(nat=>'a::ring). \ -\ m <= n & (ALL i. m < i & i <= n --> f i = 0) --> \ -\ setsum f {..m} = setsum f {..n}"; -by (induct_tac "n" 1); -(* Base case *) -by (Simp_tac 1); -(* Induction step *) -by (case_tac "m <= n" 1); -by Auto_tac; -by (subgoal_tac "m = Suc n" 1); -by (Asm_simp_tac 1); -by (fast_arith_tac 1); -val SUM_shrink_lemma = result(); - -Goal - "!! f::(nat=>'a::ring). \ -\ [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..n}) |] \ -\ ==> P (setsum f {..m})"; -by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1); -by (Asm_full_simp_tac 1); -qed "SUM_shrink"; - -Goal - "!! f::(nat=>'a::ring). \ -\ [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..m}) |] \ -\ ==> P (setsum f {..n})"; -by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1); -by (Asm_full_simp_tac 1); -qed "SUM_extend"; - -Goal - "!! f::(nat=>'a::ring). \ -\ (ALL i. i < m --> f i = 0) --> \ -\ setsum (%i. f (i+m)) {..d} = setsum f {..m+d}"; -by (induct_tac "d" 1); -(* Base case *) -by (induct_tac "m" 1); -by (Simp_tac 1); -by (Force_tac 1); -(* Induction step *) -by (asm_simp_tac (simpset() addsimps add_ac) 1); -val SUM_shrink_below_lemma = result(); - -Goal - "!! f::(nat=>'a::ring). \ -\ [| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |] \ -\ ==> P (setsum f {..n})"; -by (asm_full_simp_tac - (simpset() addsimps [SUM_shrink_below_lemma, add_diff_inverse, leD]) 1); -qed "SUM_extend_below"; - -section "Result for the Univeral Property of Polynomials"; - -Goal - "!!f::nat=>'a::ring. j <= n + m --> \ -\ setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..j} = \ -\ setsum (%k. setsum (%i. f k * g i) {..j - k}) {..j}"; -by (induct_tac "j" 1); -(* Base case *) -by (Simp_tac 1); -(* Induction step *) -by (simp_tac (simpset() addsimps [Suc_diff_le, SUM_add]) 1); -by (asm_simp_tac (simpset() addsimps a_ac) 1); -val DiagSum_lemma = result(); - -Goal - "!!f::nat=>'a::ring. \ -\ setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..n + m} = \ -\ setsum (%k. setsum (%i. f k * g i) {..n + m - k}) {..n + m}"; -by (rtac (DiagSum_lemma RS mp) 1); -by (rtac le_refl 1); -qed "DiagSum"; - - - - diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/abstract/NatSum.thy --- a/src/HOL/Algebra/abstract/NatSum.thy Wed Nov 27 17:25:41 2002 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ -(* - Sums with naturals as index domain - $Id$ - Author: Clemens Ballarin, started 12 December 1996 -*) - -NatSum = Ring + - -instance - ring < plus_ac0 (a_assoc, a_comm, l_zero) - -end diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/abstract/Ring.ML --- a/src/HOL/Algebra/abstract/Ring.ML Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/Algebra/abstract/Ring.ML Thu Nov 28 10:50:42 2002 +0100 @@ -4,6 +4,7 @@ Author: Clemens Ballarin, started 9 December 1996 *) +(* val a_assoc = thm "plus_ac0.assoc"; val l_zero = thm "plus_ac0.zero"; val a_comm = thm "plus_ac0.commute"; @@ -78,7 +79,7 @@ val m_ac = [m_assoc, m_comm, m_lcomm]; -Goal "!!a::'a::ring. a * <1> = a"; +Goal "!!a::'a::ring. a * 1 = a"; by (rtac (m_comm RS trans) 1); by (rtac l_one 1); qed "r_one"; @@ -161,19 +162,21 @@ Goal "!!a::'a::ring. (a = b) = (a -- b = 0)"; *) +*) + (* Power *) -Goal "!!a::'a::ring. a ^ 0 = <1>"; -by (simp_tac (simpset() addsimps [power_ax]) 1); +Goal "!!a::'a::ring. a ^ 0 = 1"; +by (simp_tac (simpset() addsimps [power_def]) 1); qed "power_0"; Goal "!!a::'a::ring. a ^ Suc n = a ^ n * a"; -by (simp_tac (simpset() addsimps [power_ax]) 1); +by (simp_tac (simpset() addsimps [power_def]) 1); qed "power_Suc"; Addsimps [power_0, power_Suc]; -Goal "<1> ^ n = (<1>::'a::ring)"; +Goal "1 ^ n = (1::'a::ring)"; by (induct_tac "n" 1); by Auto_tac; qed "power_one"; @@ -189,7 +192,7 @@ Goal "!! a::'a::ring. a ^ m * a ^ n = a ^ (m + n)"; by (induct_tac "m" 1); by (Simp_tac 1); -by (asm_simp_tac (simpset() addsimps m_ac) 1); +by (Asm_simp_tac 1); qed "power_mult"; (* Divisibility *) @@ -205,26 +208,26 @@ qed "dvd_zero_left"; Goalw [dvd_def] "!! a::'a::ring. a dvd a"; -by (res_inst_tac [("x", "<1>")] exI 1); +by (res_inst_tac [("x", "1")] exI 1); by (Simp_tac 1); qed "dvd_refl_ring"; Goalw [dvd_def] "!! a::'a::ring. [| a dvd b; b dvd c |] ==> a dvd c"; by (Step_tac 1); by (res_inst_tac [("x", "k * ka")] exI 1); -by (simp_tac (simpset() addsimps m_ac) 1); +by (Asm_simp_tac 1); qed "dvd_trans_ring"; Addsimps [dvd_zero_right, dvd_refl_ring]; Goalw [dvd_def] - "!!a::'a::ring. [| a dvd <1>; b dvd <1> |] ==> a * b dvd <1>"; + "!!a::'a::ring. [| a dvd 1; b dvd 1 |] ==> a * b dvd 1"; by (Clarify_tac 1); by (res_inst_tac [("x", "k * ka")] exI 1); -by (asm_full_simp_tac (simpset() addsimps m_ac) 1); +by (Asm_full_simp_tac 1); qed "unit_mult"; -Goal "!!a::'a::ring. a dvd <1> ==> a^n dvd <1>"; +Goal "!!a::'a::ring. a dvd 1 ==> a^n dvd 1"; by (induct_tac "n" 1); by (Simp_tac 1); by (asm_simp_tac (simpset() addsimps [unit_mult]) 1); @@ -248,14 +251,14 @@ "!! a::'a::ring. a dvd b ==> a dvd c*b"; by (Clarify_tac 1); by (res_inst_tac [("x", "c * k")] exI 1); -by (simp_tac (simpset() addsimps m_ac) 1); +by (Simp_tac 1); qed "dvd_l_mult_right"; Goalw [dvd_def] "!! a::'a::ring. a dvd b ==> a dvd b*c"; by (Clarify_tac 1); by (res_inst_tac [("x", "k * c")] exI 1); -by (simp_tac (simpset() addsimps m_ac) 1); +by (Simp_tac 1); qed "dvd_r_mult_right"; Addsimps [dvd_add_right, dvd_uminus_right, dvd_l_mult_right, dvd_r_mult_right]; @@ -264,34 +267,37 @@ section "inverse"; -Goal "!! a::'a::ring. [| a * x = <1>; a * y = <1> |] ==> x = y"; +Goal "!! a::'a::ring. [| a * x = 1; a * y = 1 |] ==> x = y"; by (res_inst_tac [("a", "(a*y)*x"), ("b", "y*(a*x)")] box_equals 1); -by (simp_tac (simpset() addsimps m_ac) 1); +by (Simp_tac 1); by Auto_tac; qed "inverse_unique"; -Goal "!! a::'a::ring. a dvd <1> ==> a * inverse a = <1>"; -by (asm_full_simp_tac (simpset () addsimps [inverse_ax, dvd_def]) 1); +Goal "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1"; +by (asm_full_simp_tac (simpset () addsimps [inverse_def, dvd_def]) 1); by (Clarify_tac 1); -by (rtac someI 1); -by (rtac sym 1); -by (assume_tac 1); +by (rtac theI 1); +by (atac 1); +by (rtac inverse_unique 1); +by (atac 1); +by (atac 1); qed "r_inverse_ring"; -Goal "!! a::'a::ring. a dvd <1> ==> inverse a * a= <1>"; -by (asm_simp_tac (simpset() addsimps r_inverse_ring::m_ac) 1); +Goal "!! a::'a::ring. a dvd 1 ==> inverse a * a= 1"; +by (asm_simp_tac (simpset() addsimps [r_inverse_ring]) 1); qed "l_inverse_ring"; (* Integral domain *) +(* section "Integral domains"; -Goal "0 ~= (<1>::'a::domain)"; +Goal "0 ~= (1::'a::domain)"; by (rtac not_sym 1); by (rtac one_not_zero 1); qed "zero_not_one"; -Goal "!! a::'a::domain. a dvd <1> ==> a ~= 0"; +Goal "!! a::'a::domain. a dvd 1 ==> a ~= 0"; by (auto_tac (claset() addDs [dvd_zero_left], simpset() addsimps [one_not_zero] )); qed "unit_imp_nonzero"; @@ -312,16 +318,16 @@ Addsimps [not_integral, one_not_zero, zero_not_one]; -Goal "!! a::'a::domain. [| a * x = x; x ~= 0 |] ==> a = <1>"; -by (res_inst_tac [("a", "- <1>")] a_lcancel 1); +Goal "!! a::'a::domain. [| a * x = x; x ~= 0 |] ==> a = 1"; +by (res_inst_tac [("a", "- 1")] a_lcancel 1); by (Simp_tac 1); by (rtac l_integral 1); by (assume_tac 2); by (asm_simp_tac (simpset() addsimps [l_distr, l_minus]) 1); qed "l_one_integral"; -Goal "!! a::'a::domain. [| x * a = x; x ~= 0 |] ==> a = <1>"; -by (res_inst_tac [("a", "- <1>")] a_rcancel 1); +Goal "!! a::'a::domain. [| x * a = x; x ~= 0 |] ==> a = 1"; +by (res_inst_tac [("a", "- 1")] a_rcancel 1); by (Simp_tac 1); by (rtac r_integral 1); by (assume_tac 2); @@ -340,7 +346,7 @@ Goal "!! a::'a::domain. [| a ~= 0; b * a = c * a |] ==> b = c"; by (rtac m_lcancel 1); by (assume_tac 1); -by (asm_full_simp_tac (simpset() addsimps m_ac) 1); +by (Asm_full_simp_tac 1); qed "m_rcancel"; Goal "!! a::'a::domain. a ~= 0 ==> (a * b = a * c) = (b = c)"; @@ -352,23 +358,28 @@ qed "m_rcancel_eq"; Addsimps [m_lcancel_eq, m_rcancel_eq]; +*) (* Fields *) section "Fields"; -Goal "!! a::'a::field. (a dvd <1>) = (a ~= 0)"; -by (auto_tac (claset() addDs [field_ax, dvd_zero_left], - simpset() addsimps [field_one_not_zero])); +Goal "!! a::'a::field. (a dvd 1) = (a ~= 0)"; +by (auto_tac (claset() addDs [thm "field_ax", dvd_zero_left], + simpset() addsimps [thm "field_one_not_zero"])); qed "field_unit"; +(* required for instantiation of field < domain in file Field.thy *) + Addsimps [field_unit]; -Goal "!! a::'a::field. a ~= 0 ==> a * inverse a = <1>"; +val field_one_not_zero = thm "field_one_not_zero"; + +Goal "!! a::'a::field. a ~= 0 ==> a * inverse a = 1"; by (asm_full_simp_tac (simpset() addsimps [r_inverse_ring]) 1); qed "r_inverse"; -Goal "!! a::'a::field. a ~= 0 ==> inverse a * a= <1>"; +Goal "!! a::'a::field. a ~= 0 ==> inverse a * a= 1"; by (asm_full_simp_tac (simpset() addsimps [l_inverse_ring]) 1); qed "l_inverse"; @@ -380,12 +391,13 @@ by (Step_tac 1); by (res_inst_tac [("a", "(a*b)*inverse b")] box_equals 1); by (rtac refl 3); -by (simp_tac (simpset() addsimps m_ac) 2); +by (Simp_tac 2); by Auto_tac; qed "field_integral"; (* fields are factorial domains *) -Goalw [prime_def, irred_def] "!! a::'a::field. irred a ==> prime a"; -by (blast_tac (claset() addIs [field_ax]) 1); +Goalw [thm "prime_def", thm "irred_def"] + "!! a::'a::field. irred a ==> prime a"; +by (blast_tac (claset() addIs [thm "field_ax"]) 1); qed "field_fact_prime"; diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/abstract/Ring.thy --- a/src/HOL/Algebra/abstract/Ring.thy Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/Algebra/abstract/Ring.thy Thu Nov 28 10:50:42 2002 +0100 @@ -1,89 +1,86 @@ (* - Abstract class ring (commutative, with 1) - $Id$ - Author: Clemens Ballarin, started 9 December 1996 + Title: The algebraic hierarchy of rings as axiomatic classes + Id: $Id$ + Author: Clemens Ballarin, started 9 December 1996 + Copyright: Clemens Ballarin *) -Ring = Main + +header {* The algebraic hierarchy of rings as axiomatic classes *} -(* Syntactic class ring *) +theory Ring = Main +files ("order.ML"): -axclass - ringS < zero, plus, minus, times, power, inverse +section {* Constants *} + +text {* Most constants are already declared by HOL. *} consts - (* Basic rings *) - "<1>" :: 'a::ringS ("<1>") - "--" :: ['a, 'a] => 'a::ringS (infixl 65) + assoc :: "['a::times, 'a] => bool" (infixl 50) + irred :: "'a::{zero, one, times} => bool" + prime :: "'a::{zero, one, times} => bool" + +section {* Axioms *} + +subsection {* Ring axioms *} + +axclass ring < zero, one, plus, minus, times, inverse, power + + a_assoc: "(a + b) + c = a + (b + c)" + l_zero: "0 + a = a" + l_neg: "(-a) + a = 0" + a_comm: "a + b = b + a" + + m_assoc: "(a * b) * c = a * (b * c)" + l_one: "1 * a = a" - (* Divisibility *) - assoc :: ['a::times, 'a] => bool (infixl 50) - irred :: 'a::ringS => bool - prime :: 'a::ringS => bool + l_distr: "(a + b) * c = a * c + b * c" + + m_comm: "a * b = b * a" + + -- {* Definition of derived operations *} -translations - "a -- b" == "a + (-b)" + minus_def: "a - b = a + (-b)" + inverse_def: "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)" + divide_def: "a / b = a * inverse b" + power_def: "a ^ n = nat_rec 1 (%u b. b * a) n" -(* Class ring and ring axioms *) +defs + assoc_def: "a assoc b == a dvd b & b dvd a" + irred_def: "irred a == a ~= 0 & ~ a dvd 1 + & (ALL d. d dvd a --> d dvd 1 | a dvd d)" + prime_def: "prime p == p ~= 0 & ~ p dvd 1 + & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)" + +subsection {* Integral domains *} axclass - ring < ringS, plus_ac0 - -(*a_assoc "(a + b) + c = a + (b + c)"*) -(*l_zero "0 + a = a"*) - l_neg "(-a) + a = 0" -(*a_comm "a + b = b + a"*) - - m_assoc "(a * b) * c = a * (b * c)" - l_one "<1> * a = a" - - l_distr "(a + b) * c = a * c + b * c" - - m_comm "a * b = b * a" + "domain" < ring - (* Definition of derived operations *) - - inverse_ax "inverse a = (if a dvd <1> then @x. a*x = <1> else 0)" - divide_ax "a / b = a * inverse b" - power_ax "a ^ n = nat_rec <1> (%u b. b * a) n" + one_not_zero: "1 ~= 0" + integral: "a * b = 0 ==> a = 0 | b = 0" -defs - assoc_def "a assoc b == a dvd b & b dvd a" - irred_def "irred a == a ~= 0 & ~ a dvd <1> - & (ALL d. d dvd a --> d dvd <1> | a dvd d)" - prime_def "prime p == p ~= 0 & ~ p dvd <1> - & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)" - -(* Integral domains *) +subsection {* Factorial domains *} axclass - domain < ring - - one_not_zero "<1> ~= 0" - integral "a * b = 0 ==> a = 0 | b = 0" - -(* Factorial domains *) - -axclass - factorial < domain + factorial < "domain" (* Proper definition using divisor chain condition currently not supported. - factorial_divisor "wf {(a, b). a dvd b & ~ (b dvd a)}" + factorial_divisor: "wf {(a, b). a dvd b & ~ (b dvd a)}" *) - factorial_divisor "True" - factorial_prime "irred a ==> prime a" + factorial_divisor: "True" + factorial_prime: "irred a ==> prime a" -(* Euclidean domains *) +subsection {* Euclidean domains *} (* axclass - euclidean < domain + euclidean < "domain" - euclidean_ax "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat). + euclidean_ax: "b ~= 0 ==> Ex (% (q, r, e_size::('a::ringS)=>nat). a = b * q + r & e_size r < e_size b)" - Nothing has been proved about euclidean domains, yet. + Nothing has been proved about Euclidean domains, yet. Design question: Fix quo, rem and e_size as constants that are axiomatised with euclidean_ax? @@ -95,14 +92,147 @@ definitions of quo and rem. *) -(* Fields *) +subsection {* Fields *} axclass field < ring - field_one_not_zero "<1> ~= 0" - (* Avoid a common superclass as the first thing we will - prove about fields is that they are domains. *) - field_ax "a ~= 0 ==> a dvd <1>" + field_one_not_zero: "1 ~= 0" + (* Avoid a common superclass as the first thing we will + prove about fields is that they are domains. *) + field_ax: "a ~= 0 ==> a dvd 1" + +section {* Basic facts *} + +subsection {* Normaliser for rings *} + +use "order.ML" + +method_setup ring = + {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (full_simp_tac ring_ss)) *} + {* computes distributive normal form in rings *} + + +subsection {* Rings and the summation operator *} + +(* Basic facts --- move to HOL!!! *) + +lemma natsum_0 [simp]: "setsum f {..(0::nat)} = (f 0::'a::plus_ac0)" +by simp + +lemma natsum_Suc [simp]: + "setsum f {..Suc n} = (f (Suc n) + setsum f {..n}::'a::plus_ac0)" +by (simp add: atMost_Suc) + +lemma natsum_Suc2: + "setsum f {..Suc n} = (setsum (%i. f (Suc i)) {..n} + f 0::'a::plus_ac0)" +proof (induct n) + case 0 show ?case by simp +next + case Suc thus ?case by (simp add: assoc) +qed + +lemma natsum_cong [cong]: + "!!k. [| j = k; !!i::nat. i <= k ==> f i = (g i::'a::plus_ac0) |] ==> + setsum f {..j} = setsum g {..k}" +by (induct j) auto + +lemma natsum_zero [simp]: "setsum (%i. 0) {..n::nat} = (0::'a::plus_ac0)" +by (induct n) simp_all + +lemma natsum_add [simp]: + "!!f::nat=>'a::plus_ac0. + setsum (%i. f i + g i) {..n::nat} = setsum f {..n} + setsum g {..n}" +by (induct n) (simp_all add: plus_ac0) + +(* Facts specific to rings *) + +instance ring < plus_ac0 +proof + fix x y z + show "(x::'a::ring) + y = y + x" by (rule a_comm) + show "((x::'a::ring) + y) + z = x + (y + z)" by (rule a_assoc) + show "0 + (x::'a::ring) = x" by (rule l_zero) +qed + +ML {* + local + val lhss = + [read_cterm (sign_of (the_context ())) + ("?t + ?u::'a::ring", TVar (("'z", 0), [])), + read_cterm (sign_of (the_context ())) + ("?t - ?u::'a::ring", TVar (("'z", 0), [])), + read_cterm (sign_of (the_context ())) + ("?t * ?u::'a::ring", TVar (("'z", 0), [])), + read_cterm (sign_of (the_context ())) + ("- ?t::'a::ring", TVar (("'z", 0), [])) + ]; + fun proc sg _ t = + let val rew = Tactic.prove sg [] [] + (HOLogic.mk_Trueprop + (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t)))) + (fn _ => simp_tac ring_ss 1) + |> mk_meta_eq; + val (t', u) = Logic.dest_equals (Thm.prop_of rew); + in if t' aconv u + then None + else Some rew + end; + in + val ring_simproc = mk_simproc "ring" lhss proc; + end; +*} + +ML_setup {* Addsimprocs [ring_simproc] *} + +lemma natsum_ldistr: + "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}" +by (induct n) simp_all + +lemma natsum_rdistr: + "!!a::'a::ring. a * setsum f {..n::nat} = setsum (%i. a * f i) {..n}" +by (induct n) simp_all + +subsection {* Integral Domains *} + +declare one_not_zero [simp] + +lemma zero_not_one [simp]: + "0 ~= (1::'a::domain)" +by (rule not_sym) simp + +lemma integral_iff: (* not by default a simp rule! *) + "(a * b = (0::'a::domain)) = (a = 0 | b = 0)" +proof + assume "a * b = 0" then show "a = 0 | b = 0" by (simp add: integral) +next + assume "a = 0 | b = 0" then show "a * b = 0" by auto +qed + +(* +lemma "(a::'a::ring) - (a - b) = b" apply simp +simproc seems to fail on this example +*) + +lemma bug: "(b::'a::ring) - (b - a) = a" by simp + (* simproc for rings cannot prove "(a::'a::ring) - (a - b) = b" *) + +lemma m_lcancel: + assumes prem: "(a::'a::domain) ~= 0" shows conc: "(a * b = a * c) = (b = c)" +proof + assume eq: "a * b = a * c" + then have "a * (b - c) = 0" by simp + then have "a = 0 | (b - c) = 0" by (simp only: integral_iff) + with prem have "b - c = 0" by auto + then have "b = b - (b - c)" by simp + also have "b - (b - c) = c" by (rule bug) + finally show "b = c" . +next + assume "b = c" then show "a * b = a * c" by simp +qed + +lemma m_rcancel: + "(a::'a::domain) ~= 0 ==> (b * a = c * a) = (b = c)" +by (simp add: m_lcancel) end diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/abstract/RingHomo.ML --- a/src/HOL/Algebra/abstract/RingHomo.ML Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/Algebra/abstract/RingHomo.ML Thu Nov 28 10:50:42 2002 +0100 @@ -8,7 +8,7 @@ Goalw [homo_def] "!! f. [| !! a b. f (a + b) = f a + f b; !! a b. f (a * b) = f a * f b; \ -\ f <1> = <1> |] ==> homo f"; +\ f 1 = 1 |] ==> homo f"; by Auto_tac; qed "homoI"; @@ -20,7 +20,7 @@ by (Fast_tac 1); qed "homo_mult"; -Goalw [homo_def] "!! f. homo f ==> f <1> = <1>"; +Goalw [homo_def] "!! f. homo f ==> f 1 = 1"; by (Fast_tac 1); qed "homo_one"; @@ -41,7 +41,7 @@ by (dtac homo_one 1); by (Asm_simp_tac 1); by (dres_inst_tac [("a", "a^n"), ("b", "a")] homo_mult 1); -by (Asm_simp_tac 1); +by (Asm_full_simp_tac 1); qed "homo_power"; Goal diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/abstract/RingHomo.thy --- a/src/HOL/Algebra/abstract/RingHomo.thy Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/Algebra/abstract/RingHomo.thy Thu Nov 28 10:50:42 2002 +0100 @@ -4,14 +4,14 @@ Author: Clemens Ballarin, started 15 April 1997 *) -RingHomo = NatSum + +RingHomo = Ring + consts - homo :: ('a::ringS => 'b::ringS) => bool + homo :: ('a::ring => 'b::ring) => bool defs homo_def "homo f == (ALL a b. f (a + b) = f a + f b & f (a * b) = f a * f b) & - f <1> = <1>" + f 1 = 1" end diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/abstract/order.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Algebra/abstract/order.ML Thu Nov 28 10:50:42 2002 +0100 @@ -0,0 +1,250 @@ +(* + Title: Term order, needed for normal forms in rings + Id: $Id$ + Author: Clemens Ballarin and Roland Zumkeller + Copyright: TU Muenchen +*) + +local + +(* +An order is a value of type + ('a -> bool, 'a * 'a -> bool). + +The two parts are: + 1) a unary predicate denoting the order's domain + 2) a binary predicate with the semanitcs "greater than" + +If (d, ord) is an order then ord (a,b) is defined if both d a and d b. +*) + +(* +Combines two orders with disjoint domains and returns +another one. +When the compared values are from the same domain, the corresponding +order is used. If not the ones from the first domain are considerer +greater. (If a value is in neither of the two domains, exception +"Domain" is raised.) +*) + +fun combineOrd ((d1, ord1), (d2, ord2)) = + (fn x => d1 x orelse d2 x, + fn (a, b) => + if d1 a andalso d1 b then ord1 (a, b) else + if d1 a andalso d2 b then true else + if d2 a andalso d2 b then ord2 (a, b) else + if d2 a andalso d1 b then false else raise Domain) + + +(* Counts the number of function applications + 1. *) +(* ### is there a standard Isabelle function for this? *) + +fun tsize (a $ b) = tsize a + tsize b + | tsize _ = 1; + +(* foldl on non-empty lists *) + +fun foldl2 f (x::xs) = foldl f (x,xs) + + +(* Compares two terms, ignoring type information. *) +infix e; +fun Const (s1, _) e Const (s2, _) = s1 = s2 + | Free (s1, _) e Free (s2, _) = s1 = s2 + | Var (ix1, _) e Var (ix2, _) = ix1 = ix2 + | Bound i1 e Bound i2 = i1 = i2 + | Abs (s1, _, t1) e Abs (s2, _, t2) = s1 = s2 andalso t1 = t2 + | (s1 $ s2) e (t1 $ t2) = s1 = t1 andalso s2 = t2 + | _ e _ = false + + + +(* Curried lexicographich path order induced by an order on function symbols. +Its feature include: +- compatibility with Epsilon-operations +- closure under substitutions +- well-foundedness +- subterm-property +- termination +- defined on all terms (not only on ground terms) +- linearity + +The order ignores types. +*) + +infix g; +fun clpo (d, ord) (s,t) = + let val (op g) = clpo (d, ord) in + (s <> t) andalso + if tsize s < tsize t then not (t g s) else + (* improves performance. allowed because clpo is total. *) + #2 (foldl2 combineOrd [ + (fn _ $ _ => true | Abs _ => true | _ => false, + fn (Abs (_, _, s'), t) => s' e t orelse s' g t orelse + (case t of + Abs (_, _, t') => s' g t' + | t1 $ t2 => s g t1 andalso s g t2 + ) + | (s1 $ s2, t) => s1 e t orelse s2 e t orelse + s1 g t orelse s2 g t orelse + (case t of + t1 $ t2 => (s1 e t1 andalso s2 g t2) orelse + (s1 g t1 andalso s g t2) + | _ => false + ) + ), + (fn Free _ => true | _ => false, fn (Free (a,_), Free (b,_)) => a > b), + (fn Bound _ => true | _ => false, fn (Bound a, Bound b) => a > b), + (fn Const (c, _) => not (d c) | _ => false, fn (Const (a, _), Const (b, _)) => a > b), + (fn Const (c, _) => d c | _ => false, fn (Const (a, _), Const (b, _)) => ord (a,b)) + ]) (s,t) + end; + +(* +Open Issues: +- scheme variables have to be ordered (should be simple) +*) + +(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *) + +(* Returns the position of an element in a list. If the +element doesn't occur in the list, a MatchException is raised. *) +fun pos (x::xs) i = if x = i then 0 else 1 + pos xs i; + +(* Generates a finite linear order from a list. +[a, b, c] results in the order "a > b > c". *) +fun linOrd l = fn (a,b) => pos l a < pos l b; + +(* Determines whether an element is contained in a list. *) +fun contains (x::xs) i = (x = i) orelse (contains xs i) | + contains [] i = false; + +in + +(* Term order for commutative rings *) + +fun termless_ring (a, b) = + let + val S = ["op *", "op -", "uminus", "op +", "0"]; + (* Order (decending from left to right) on the constant symbols *) + val baseOrd = (contains S, linOrd S); + in clpo baseOrd (b, a) + end; + +(*** Rewrite rules ***) + +val a_assoc = thm "ring.a_assoc"; +val l_zero = thm "ring.l_zero"; +val l_neg = thm "ring.l_neg"; +val a_comm = thm "ring.a_comm"; +val m_assoc = thm "ring.m_assoc"; +val l_one = thm "ring.l_one"; +val l_distr = thm "ring.l_distr"; +val m_comm = thm "ring.m_comm"; +val minus_def = thm "ring.minus_def"; +val inverse_def = thm "ring.inverse_def"; +val divide_def = thm "ring.divide_def"; +val power_def = thm "ring.power_def"; + +(* These are the following axioms: + + a_assoc: "(a + b) + c = a + (b + c)" + l_zero: "0 + a = a" + l_neg: "(-a) + a = 0" + a_comm: "a + b = b + a" + + m_assoc: "(a * b) * c = a * (b * c)" + l_one: "1 * a = a" + + l_distr: "(a + b) * c = a * c + b * c" + + m_comm: "a * b = b * a" + + -- {* Definition of derived operations *} + + minus_def: "a - b = a + (-b)" + inverse_def: "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)" + divide_def: "a / b = a * inverse b" + power_def: "a ^ n = nat_rec 1 (%u b. b * a) n" +*) + +(* These lemmas are needed in the proofs *) +val trans = thm "trans"; +val sym = thm "sym"; +val subst = thm "subst"; +val box_equals = thm "box_equals"; +val arg_cong = thm "arg_cong"; +(* current theory *) +val thy = the_context (); + +(* derived rewrite rules *) +val a_lcomm = prove_goal thy "(a::'a::ring)+(b+c) = b+(a+c)" + (fn _ => [rtac (a_comm RS trans) 1, rtac (a_assoc RS trans) 1, + rtac (a_comm RS arg_cong) 1]); +val r_zero = prove_goal thy "(a::'a::ring) + 0 = a" + (fn _ => [rtac (a_comm RS trans) 1, rtac l_zero 1]); +val r_neg = prove_goal thy "(a::'a::ring) + (-a) = 0" + (fn _ => [rtac (a_comm RS trans) 1, rtac l_neg 1]); +val r_neg2 = prove_goal thy "(a::'a::ring) + (-a + b) = b" + (fn _ => [rtac (a_assoc RS sym RS trans) 1, + simp_tac (simpset() addsimps [r_neg, l_zero]) 1]); +val r_neg1 = prove_goal thy "-(a::'a::ring) + (a + b) = b" + (fn _ => [rtac (a_assoc RS sym RS trans) 1, + simp_tac (simpset() addsimps [l_neg, l_zero]) 1]); +(* auxiliary *) +val a_lcancel = prove_goal thy "!! a::'a::ring. a + b = a + c ==> b = c" + (fn _ => [rtac box_equals 1, rtac l_zero 2, rtac l_zero 2, + res_inst_tac [("a1", "a")] (l_neg RS subst) 1, + asm_simp_tac (simpset() addsimps [a_assoc]) 1]); +val minus_add = prove_goal thy "-((a::'a::ring) + b) = (-a) + (-b)" + (fn _ => [res_inst_tac [("a", "a+b")] a_lcancel 1, + simp_tac (simpset() addsimps [r_neg, l_neg, l_zero, + a_assoc, a_comm, a_lcomm]) 1]); +val minus_minus = prove_goal thy "-(-(a::'a::ring)) = a" + (fn _ => [rtac a_lcancel 1, rtac (r_neg RS trans) 1, rtac (l_neg RS sym) 1]); +val minus0 = prove_goal thy "- 0 = (0::'a::ring)" + (fn _ => [rtac a_lcancel 1, rtac (r_neg RS trans) 1, + rtac (l_zero RS sym) 1]); + +(* derived rules for multiplication *) +val m_lcomm = prove_goal thy "(a::'a::ring)*(b*c) = b*(a*c)" + (fn _ => [rtac (m_comm RS trans) 1, rtac (m_assoc RS trans) 1, + rtac (m_comm RS arg_cong) 1]); +val r_one = prove_goal thy "(a::'a::ring) * 1 = a" + (fn _ => [rtac (m_comm RS trans) 1, rtac l_one 1]); +val r_distr = prove_goal thy "(a::'a::ring) * (b + c) = a * b + a * c" + (fn _ => [rtac (m_comm RS trans) 1, rtac (l_distr RS trans) 1, + simp_tac (simpset() addsimps [m_comm]) 1]); +(* the following proof is from Jacobson, Basic Algebra I, pp. 88-89 *) +val l_null = prove_goal thy "0 * (a::'a::ring) = 0" + (fn _ => [rtac a_lcancel 1, rtac (l_distr RS sym RS trans) 1, + simp_tac (simpset() addsimps [r_zero]) 1]); +val r_null = prove_goal thy "(a::'a::ring) * 0 = 0" + (fn _ => [rtac (m_comm RS trans) 1, rtac l_null 1]); +val l_minus = prove_goal thy "(-(a::'a::ring)) * b = - (a * b)" + (fn _ => [rtac a_lcancel 1, rtac (r_neg RS sym RSN (2, trans)) 1, + rtac (l_distr RS sym RS trans) 1, + simp_tac (simpset() addsimps [l_null, r_neg]) 1]); +val r_minus = prove_goal thy "(a::'a::ring) * (-b) = - (a * b)" + (fn _ => [rtac a_lcancel 1, rtac (r_neg RS sym RSN (2, trans)) 1, + rtac (r_distr RS sym RS trans) 1, + simp_tac (simpset() addsimps [r_null, r_neg]) 1]); + +val ring_ss = HOL_basic_ss settermless termless_ring addsimps + [a_assoc, l_zero, l_neg, a_comm, m_assoc, l_one, l_distr, m_comm, minus_def, + r_zero, r_neg, r_neg2, r_neg1, minus_add, minus_minus, minus0, + a_lcomm, m_lcomm, r_distr, l_null, r_null, l_minus, r_minus]; + +val x = bind_thms ("ring_simps", [l_zero, r_zero, l_neg, r_neg, + minus_minus, minus0, + l_one, r_one, l_null, r_null, l_minus, r_minus]); + +(* note: r_one added to ring_simp but not ring_ss *) + +(* note: not added (and not proved): + a_lcancel_eq, a_rcancel_eq, power_one, power_Suc, power_zero, power_one, + m_lcancel_eq, m_rcancel_eq, + thms involving dvd, integral domains, fields +*) + +end; \ No newline at end of file diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/poly/Degree.ML --- a/src/HOL/Algebra/poly/Degree.ML Wed Nov 27 17:25:41 2002 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,358 +0,0 @@ -(* - Degree of polynomials - $Id$ - written by Clemens Ballarin, started 22 January 1997 -*) - -(* Relating degree and bound *) - -Goal "[| bound m f; f n ~= 0 |] ==> n <= m"; -by (force_tac (claset() addDs [inst "m" "n" boundD], - simpset()) 1); -qed "below_bound"; - -goal UnivPoly.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)"; -by (rtac exE 1); -by (rtac LeastI 2); -by (assume_tac 2); -by (res_inst_tac [("a", "Rep_UP p")] CollectD 1); -by (rtac (rewrite_rule [UP_def] Rep_UP) 1); -qed "Least_is_bound"; - -Goalw [coeff_def, deg_def] - "!! p. ALL m. n < m --> coeff m p = 0 ==> deg p <= n"; -by (rtac Least_le 1); -by (Fast_tac 1); -qed "deg_aboveI"; - -Goalw [coeff_def, deg_def] - "(n ~= 0 --> coeff n p ~= 0) ==> n <= deg p"; -by (case_tac "n = 0" 1); -(* Case n=0 *) -by (Asm_simp_tac 1); -(* Case n~=0 *) -by (rotate_tac 1 1); -by (Asm_full_simp_tac 1); -by (rtac below_bound 1); -by (assume_tac 2); -by (rtac Least_is_bound 1); -qed "deg_belowI"; - -Goalw [coeff_def, deg_def] - "deg p < m ==> coeff m p = 0"; -by (rtac exE 1); (* create !! x. *) -by (rtac boundD 2); -by (assume_tac 3); -by (rtac LeastI 2); -by (assume_tac 2); -by (res_inst_tac [("a", "Rep_UP p")] CollectD 1); -by (rtac (rewrite_rule [UP_def] Rep_UP) 1); -qed "deg_aboveD"; - -Goalw [deg_def] - "deg p = Suc y ==> ~ bound y (Rep_UP p)"; -by (rtac not_less_Least 1); -by (Asm_simp_tac 1); -val lemma1 = result(); - -Goalw [deg_def, coeff_def] - "deg p = Suc y ==> coeff (deg p) p ~= 0"; -by (rtac ccontr 1); -by (dtac notnotD 1); -by (cut_inst_tac [("p", "p")] Least_is_bound 1); -by (subgoal_tac "bound y (Rep_UP p)" 1); -(* prove subgoal *) -by (rtac boundI 2); -by (case_tac "Suc y < m" 2); -(* first case *) -by (rtac boundD 2); -by (assume_tac 2); -by (Asm_simp_tac 2); -(* second case *) -by (dtac leI 2); -by (dtac Suc_leI 2); -by (dtac le_anti_sym 2); -by (assume_tac 2); -by (Asm_full_simp_tac 2); -(* end prove subgoal *) -by (fold_goals_tac [deg_def]); -by (dtac lemma1 1); -by (etac notE 1); -by (assume_tac 1); -val lemma2 = result(); - -Goal "deg p ~= 0 ==> coeff (deg p) p ~= 0"; -by (rtac lemma2 1); -by (Full_simp_tac 1); -by (dtac Suc_pred 1); -by (rtac sym 1); -by (Asm_simp_tac 1); -qed "deg_lcoeff"; - -Goal "p ~= 0 ==> coeff (deg p) p ~= 0"; -by (etac contrapos_np 1); -by (case_tac "deg p = 0" 1); -by (blast_tac (claset() addSDs [deg_lcoeff]) 2); -by (rtac up_eqI 1); -by (case_tac "n=0" 1); -by (rotate_tac ~2 1); -by (Asm_full_simp_tac 1); -by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1); -qed "nonzero_lcoeff"; - -Goal "(deg p <= n) = bound n (Rep_UP p)"; -by (rtac iffI 1); -(* ==> *) -by (rtac boundI 1); -by (fold_goals_tac [coeff_def]); -by (rtac deg_aboveD 1); -by (fast_arith_tac 1); -(* <== *) -by (rtac deg_aboveI 1); -by (rewtac coeff_def); -by (Fast_tac 1); -qed "deg_above_is_bound"; - -(* Lemmas on the degree function *) - -Goalw [max_def] - "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)"; -by (case_tac "deg p <= deg q" 1); -(* case deg p <= deg q *) -by (rtac deg_aboveI 1); -by (Asm_simp_tac 1); -by (strip_tac 1); -by (dtac le_less_trans 1); -by (assume_tac 1); -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); -(* case deg p > deg q *) -by (rtac deg_aboveI 1); -by (Asm_simp_tac 1); -by (dtac not_leE 1); -by (strip_tac 1); -by (dtac less_trans 1); -by (assume_tac 1); -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); -qed "deg_add"; - -Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q"; -by (rtac order_antisym 1); -by (rtac le_trans 1); -by (rtac deg_add 1); -by (Asm_simp_tac 1); -by (rtac deg_belowI 1); -by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1); -qed "deg_add_equal"; - -Goal "deg (monom m::'a::ring up) <= m"; -by (asm_simp_tac - (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1); -qed "deg_monom_ring"; - -Goal "deg (monom m::'a::domain up) = m"; -by (rtac le_anti_sym 1); -(* <= *) -by (rtac deg_monom_ring 1); -(* >= *) -by (asm_simp_tac - (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1); -qed "deg_monom"; - -Goal "!! a::'a::ring. deg (const a) = 0"; -by (rtac le_anti_sym 1); -by (rtac deg_aboveI 1); -by (simp_tac (simpset() addsimps [less_not_refl2]) 1); -by (rtac deg_belowI 1); -by (simp_tac (simpset() addsimps [less_not_refl2]) 1); -qed "deg_const"; - -Goal "deg (0::'a::ringS up) = 0"; -by (rtac le_anti_sym 1); -by (rtac deg_aboveI 1); -by (Simp_tac 1); -by (rtac deg_belowI 1); -by (Simp_tac 1); -qed "deg_zero"; - -Goal "deg (<1>::'a::ring up) = 0"; -by (rtac le_anti_sym 1); -by (rtac deg_aboveI 1); -by (simp_tac (simpset() addsimps [less_not_refl2]) 1); -by (rtac deg_belowI 1); -by (Simp_tac 1); -qed "deg_one"; - -Goal "!!p::('a::ring) up. deg (-p) = deg p"; -by (rtac le_anti_sym 1); -(* <= *) -by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1); -by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1); -qed "deg_uminus"; - -Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus]; - -Goal - "!! a::'a::ring. deg (a *s p) <= (if a = 0 then 0 else deg p)"; -by (case_tac "a = 0" 1); -by (REPEAT (asm_simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1)); -qed "deg_smult_ring"; - -Goal - "!! a::'a::domain. deg (a *s p) = (if a = 0 then 0 else deg p)"; -by (rtac le_anti_sym 1); -by (rtac deg_smult_ring 1); -by (case_tac "a = 0" 1); -by (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1)); -qed "deg_smult"; - -Goal - "!! p::'a::ring up. [| deg p + deg q < k |] ==> \ -\ coeff i p * coeff (k - i) q = 0"; -by (simp_tac (simpset() addsimps [coeff_def]) 1); -by (rtac bound_mult_zero 1); -by (assume_tac 3); -by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1); -by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1); -qed "deg_above_mult_zero"; - -Goal - "!! p::'a::ring up. deg (p * q) <= deg p + deg q"; -by (rtac deg_aboveI 1); -by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1); -qed "deg_mult_ring"; - -goal Main.thy - "!!k::nat. k < n ==> m < n + m - k"; -by (arith_tac 1); -qed "less_add_diff"; - -Goal "!!p. coeff n p ~= 0 ==> n <= deg p"; -(* More general than deg_belowI, and simplifies the next proof! *) -by (rtac deg_belowI 1); -by (Fast_tac 1); -qed "deg_below2I"; - -Goal - "!! p::'a::domain up. \ -\ [| p ~= 0; q ~= 0 |] ==> deg (p * q) = deg p + deg q"; -by (rtac le_anti_sym 1); -by (rtac deg_mult_ring 1); -(* deg p + deg q <= deg (p * q) *) -by (rtac deg_below2I 1); -by (Simp_tac 1); -(* -by (rtac conjI 1); -by (rtac impI 1); -*) -by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1); -by (rtac le_add1 1); -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); -by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1); -by (rtac le_refl 1); -by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1); -by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1); -(* -by (rtac impI 1); -by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1); -by (rtac le_add1 1); -by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1); -by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1); -by (rtac le_refl 1); -by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1); -by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1); -*) -qed "deg_mult"; - -Addsimps [deg_smult, deg_mult]; - -(* Representation theorems about polynomials *) - -goal PolyRing.thy - "!! p::nat=>'a::ring up. \ -\ coeff k (setsum p {..n}) = setsum (%i. coeff k (p i)) {..n}"; -by (induct_tac "n" 1); -by Auto_tac; -qed "coeff_SUM"; - -goal UnivPoly.thy - "!! f::(nat=>'a::ring). \ -\ bound n f ==> setsum (%i. if i = x then f i else 0) {..n} = f x"; -by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1); -by (auto_tac - (claset() addDs [not_leE], - simpset())); -qed "bound_SUM_if"; - -Goal - "!! p::'a::ring up. deg p <= n ==> \ -\ setsum (%i. coeff i p *s monom i) {..n} = p"; -by (rtac up_eqI 1); -by (simp_tac (simpset() addsimps [coeff_SUM]) 1); -by (rtac trans 1); -by (res_inst_tac [("x", "na")] bound_SUM_if 2); -by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2); -by (rtac SUM_cong 1); -by (rtac refl 1); -by (Asm_simp_tac 1); -qed "up_repr"; - -Goal - "!! p::'a::ring up. [| deg p <= n; P p |] ==> \ -\ P (setsum (%i. coeff i p *s monom i) {..n})"; -by (asm_simp_tac (simpset() addsimps [up_repr]) 1); -qed "up_reprD"; - -Goal - "!! p::'a::ring up. \ -\ [| deg p <= n; P (setsum (%i. coeff i p *s monom i) {..n}) |] \ -\ ==> P p"; -by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1); -qed "up_repr2D"; - -(* -Goal - "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \ -\ (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \ -\ = (coeff k f = coeff k g) -... -qed "up_unique"; -*) - -(* Polynomials over integral domains are again integral domains *) - -Goal "!!p::'a::domain up. p * q = 0 ==> p = 0 | q = 0"; -by (rtac classical 1); -by (subgoal_tac "deg p = 0 & deg q = 0" 1); -by (res_inst_tac [("p", "p"), ("n", "0")] up_repr2D 1); -by (Asm_simp_tac 1); -by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1); -by (Asm_simp_tac 1); -by (subgoal_tac "coeff 0 p = 0 | coeff 0 q = 0" 1); -by (force_tac (claset() addIs [up_eqI], simpset()) 1); -by (rtac integral 1); -by (subgoal_tac "coeff 0 (p * q) = 0" 1); -by (Asm_simp_tac 2); -by (Full_simp_tac 1); -by (dres_inst_tac [("f", "deg")] arg_cong 1); -by (Asm_full_simp_tac 1); -qed "up_integral"; - -Goal "!! a::'a::domain. a *s p = 0 ==> a = 0 | p = 0"; -by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1); -by (dtac up_integral 1); -by Auto_tac; -by (rtac (const_inj RS injD) 1); -by (Simp_tac 1); -qed "smult_integral"; - -(* Divisibility and degree *) - -Goalw [dvd_def] - "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q"; -by (etac exE 1); -by (hyp_subst_tac 1); -by (case_tac "p = 0" 1); -by (Asm_simp_tac 1); -by (dtac r_nullD 1); -by (asm_simp_tac (simpset() addsimps [le_add1]) 1); -qed "dvd_imp_deg"; diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/poly/Degree.thy --- a/src/HOL/Algebra/poly/Degree.thy Wed Nov 27 17:25:41 2002 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -(* - Degree of polynomials - $Id$ - written by Clemens Ballarin, started 22. 1. 1997 -*) - -Degree = PolyRing + - -consts - deg :: ('a::ringS) up => nat - -defs - deg_def "deg p == LEAST n. bound n (Rep_UP p)" - -end diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/poly/LongDiv.ML --- a/src/HOL/Algebra/poly/LongDiv.ML Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/Algebra/poly/LongDiv.ML Thu Nov 28 10:50:42 2002 +0100 @@ -4,10 +4,55 @@ Author: Clemens Ballarin, started 23 June 1999 *) +(* legacy bindings and theorems *) + +val deg_aboveI = thm "deg_aboveI"; +val smult_l_minus = thm "smult_l_minus"; +val deg_monom_ring = thm "deg_monom_ring"; +val deg_smult_ring = thm "deg_smult_ring"; +val smult_l_distr = thm "smult_l_distr"; +val smult_r_distr = thm "smult_r_distr"; +val smult_r_minus = thm "smult_r_minus"; +val smult_assoc2 = thm "smult_assoc2"; +val smult_assoc1 = thm "smult_assoc1"; +val monom_mult_smult = thm "monom_mult_smult"; +val field_ax = thm "field_ax"; +val lcoeff_nonzero = thm "lcoeff_nonzero"; + +Goal + "!! f::(nat=>'a::ring). \ +\ (ALL i. i < m --> f i = 0) --> \ +\ setsum (%i. f (i+m)) {..d} = setsum f {..m+d}"; +by (induct_tac "d" 1); +(* Base case *) +by (induct_tac "m" 1); +by (Simp_tac 1); +by (Force_tac 1); +(* Induction step *) +by (asm_simp_tac (simpset() addsimps add_ac) 1); +val SUM_shrink_below_lemma = result(); + +Goal + "!! f::(nat=>'a::ring). \ +\ [| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |] \ +\ ==> P (setsum f {..n})"; +by (asm_full_simp_tac + (simpset() addsimps [SUM_shrink_below_lemma, add_diff_inverse, leD]) 1); +qed "SUM_extend_below"; + +Goal + "!! p::'a::ring up. \ +\ [| deg p <= n; P (setsum (%i. monom (coeff p i) i) {..n}) |] \ +\ ==> P p"; +by (asm_full_simp_tac (simpset() addsimps [thm "up_repr_le"]) 1); +qed "up_repr2D"; + +(* Start of LongDiv *) + Goal "!!p::('a::ring up). \ \ [| deg p <= deg r; deg q <= deg r; \ -\ coeff (deg r) p = - (coeff (deg r) q); deg r ~= 0 |] ==> \ +\ coeff p (deg r) = - (coeff q (deg r)); deg r ~= 0 |] ==> \ \ deg (p + q) < deg r"; by (res_inst_tac [("j", "deg r - 1")] le_less_trans 1); by (arith_tac 2); @@ -25,7 +70,7 @@ Goal "!!p::('a::ring up). \ \ [| deg p <= deg r; deg q <= deg r; \ -\ p ~= -q; coeff (deg r) p = - (coeff (deg r) q) |] ==> \ +\ p ~= -q; coeff p (deg r) = - (coeff q (deg r)) |] ==> \ \ deg (p + q) < deg r"; by (rtac deg_lcoeff_cancel 1); by (REPEAT (atac 1)); @@ -51,7 +96,7 @@ by (res_inst_tac [("x", "(0, x, 0)")] exI 1); by (Asm_simp_tac 1); (* case "eucl_size x >= eucl_size g" *) -by (dres_inst_tac [("x", "lcoeff g *s x -- (lcoeff x *s monom (deg x - deg g)) * g")] spec 1); +by (dres_inst_tac [("x", "lcoeff g *s x - (monom (lcoeff x) (deg x - deg g)) * g")] spec 1); by (etac impE 1); by (full_simp_tac (simpset() addsimps [inv_image_def, measure_def, lcoeff_def]) 1); by (case_tac "x = 0" 1); @@ -71,14 +116,35 @@ by (rtac le_trans 1); by (rtac deg_mult_ring 1); by (rtac le_trans 1); +(**) + by (rtac add_le_mono 1); by (rtac le_refl 1); + (* term order forces to use this instead of add_le_mono1 *) + by (rtac deg_monom_ring 1); + by (Asm_simp_tac 1); +(**) +(* by (rtac add_le_mono1 1); by (rtac deg_smult_ring 1); (* by (asm_simp_tac (simpset() addsimps [leI]) 1); *) by (Asm_simp_tac 1); by (cut_inst_tac [("m", "deg x - deg g"), ("'a", "'a")] deg_monom_ring 1); by (arith_tac 1); +*) by (Force_tac 1); by (Simp_tac 1); +(**) + (* This change is probably caused by application of commutativity *) +by (res_inst_tac [("m", "deg g"), ("n", "deg x")] SUM_extend 1); +by (Simp_tac 1); +by (Asm_simp_tac 1); +by (arith_tac 1); +by (res_inst_tac [("m", "deg g"), ("n", "deg g")] SUM_extend_below 1); +by (rtac le_refl 1); +by (Asm_simp_tac 1); +by (arith_tac 1); +by (Simp_tac 1); +(**) +(* by (res_inst_tac [("m", "deg x - deg g"), ("n", "deg x")] SUM_extend 1); by (Simp_tac 1); by (asm_simp_tac (simpset() addsimps [less_not_refl2 RS not_sym]) 1); @@ -87,14 +153,19 @@ by (rtac le_refl 1); by (asm_simp_tac (simpset() addsimps [less_not_refl2]) 1); by (asm_simp_tac (simpset() addsimps [diff_diff_right, leI, m_comm]) 1); +*) (* end of subproof deg f1 < deg f *) by (etac exE 1); -by (res_inst_tac [("x", "((%(q,r,k). ((lcoeff g ^ k * lcoeff x) *s monom (deg x - deg g) + q)) xa, (%(q,r,k). r) xa, (%(q,r,k). Suc k) xa)")] exI 1); +by (res_inst_tac [("x", "((%(q,r,k). (monom (lcoeff g ^ k * lcoeff x) (deg x - deg g) + q)) xa, (%(q,r,k). r) xa, (%(q,r,k). Suc k) xa)")] exI 1); by (Clarify_tac 1); by (dtac sym 1); -by (simp_tac (simpset() addsimps [l_distr, a_assoc]) 1); -by (Asm_simp_tac 1); -by (simp_tac (simpset() addsimps a_ac@[smult_l_distr, smult_r_distr, smult_r_minus, smult_assoc2, smult_assoc1]) 1); +by (simp_tac (simpset() addsimps [l_distr, a_assoc] + delsimprocs [ring_simproc]) 1); +by (asm_simp_tac (simpset() delsimprocs [ring_simproc]) 1); +by (simp_tac (simpset() addsimps [minus_def, smult_r_distr, smult_r_minus, + monom_mult_smult, smult_assoc1, smult_assoc2] + delsimprocs [ring_simproc]) 1); +by (Simp_tac 1); qed "long_div_eucl_size"; Goal @@ -102,8 +173,9 @@ \ Ex (% (q, r, k). \ \ (lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))"; by (forw_inst_tac [("f", "f")] - (simplify (simpset() addsimps [eucl_size_def]) long_div_eucl_size) 1); -by Auto_tac; + (simplify (simpset() addsimps [eucl_size_def] + delsimprocs [ring_simproc]) long_div_eucl_size) 1); +by (auto_tac (claset(), simpset() delsimprocs [ring_simproc])); by (case_tac "aa = 0" 1); by (Blast_tac 1); (* case "aa ~= 0 *) @@ -111,18 +183,20 @@ by Auto_tac; qed "long_div_ring"; +(* Next one fails *) Goal - "!!g::('a::ring up). [| g ~= 0; (lcoeff g) dvd <1> |] ==> \ + "!!g::('a::ring up). [| g ~= 0; (lcoeff g) dvd 1 |] ==> \ \ Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))"; by (forw_inst_tac [("f", "f")] long_div_ring 1); by (etac exE 1); by (res_inst_tac [("x", "((%(q,r,k). (inverse(lcoeff g ^k) *s q)) x, \ \ (%(q,r,k). inverse(lcoeff g ^k) *s r) x)")] exI 1); by (Clarify_tac 1); -by (Simp_tac 1); +(* by (Simp_tac 1); *) by (rtac conjI 1); by (dtac sym 1); -by (asm_simp_tac (simpset() addsimps [smult_r_distr RS sym, smult_assoc2]) 1); +by (asm_simp_tac (simpset() addsimps [smult_r_distr RS sym, smult_assoc2] + delsimprocs [ring_simproc]) 1); by (asm_simp_tac (simpset() addsimps [l_inverse_ring, unit_power, smult_assoc1 RS sym]) 1); (* degree property *) by (etac disjE 1); @@ -138,14 +212,28 @@ \ Ex (% (q, r). f = q * g + r & (r = 0 | deg r < deg g))"; by (rtac long_div_unit 1); by (assume_tac 1); -by (asm_simp_tac (simpset() addsimps [lcoeff_def, nonzero_lcoeff, field_ax]) 1); +by (asm_simp_tac (simpset() addsimps [lcoeff_def, lcoeff_nonzero, field_ax]) 1); qed "long_div_theorem"; +Goal "- (0::'a::ring) = 0"; +by (Simp_tac 1); +val uminus_zero = result(); + +Goal "!!a::'a::ring. a - b = 0 ==> a = b"; +br trans 1; +by (res_inst_tac [("b", "a")] (thm "bug") 2); +by (Asm_simp_tac 1); +val diff_zero_imp_eq = result(); + +Goal "!!a::'a::ring. a = b ==> a + (-b) = 0"; +by (Asm_simp_tac 1); +val eq_imp_diff_zero = result(); + Goal "!!g::('a::field up). [| g ~= 0; \ \ f = q1 * g + r1; (r1 = 0 | deg r1 < deg g); \ \ f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> q1 = q2"; -by (subgoal_tac "(q1 -- q2) * g = r2 -- r1" 1); (* 1 *) +by (subgoal_tac "(q1 - q2) * g = r2 - r1" 1); (* 1 *) by (thin_tac "f = ?x" 1); by (thin_tac "f = ?x" 1); by (rtac diff_zero_imp_eq 1); @@ -154,18 +242,23 @@ (* r1 = 0 *) by (etac disjE 1); (* r2 = 0 *) -by (force_tac (claset() addDs [integral], simpset()) 1); +by (asm_full_simp_tac (simpset() + addsimps [thm "integral_iff", minus_def, l_zero, uminus_zero] + delsimprocs [ring_simproc]) 1); (* r2 ~= 0 *) -by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1); -by (Force_tac 1); +by (dres_inst_tac [("f", "deg"), ("y", "r2 - r1")] arg_cong 1); +by (asm_full_simp_tac (simpset() addsimps [minus_def, l_zero, uminus_zero] + delsimprocs [ring_simproc]) 1); (* r1 ~=0 *) by (etac disjE 1); (* r2 = 0 *) -by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1); -by (Force_tac 1); +by (dres_inst_tac [("f", "deg"), ("y", "r2 - r1")] arg_cong 1); +by (asm_full_simp_tac (simpset() addsimps [minus_def, l_zero, uminus_zero] + delsimprocs [ring_simproc]) 1); (* r2 ~= 0 *) -by (dres_inst_tac [("f", "deg"), ("y", "r2 -- r1")] arg_cong 1); -by (Asm_full_simp_tac 1); +by (dres_inst_tac [("f", "deg"), ("y", "r2 - r1")] arg_cong 1); +by (asm_full_simp_tac (simpset() addsimps [minus_def] + delsimprocs [ring_simproc]) 1); by (dtac (order_eq_refl RS add_leD2) 1); by (dtac leD 1); by (etac notE 1 THEN rtac (deg_add RS le_less_trans) 1); @@ -174,7 +267,7 @@ by (rtac diff_zero_imp_eq 1); by (hyp_subst_tac 1); by (dres_inst_tac [("a", "?x+?y")] eq_imp_diff_zero 1); -by (asm_full_simp_tac (simpset() addsimps (l_distr::minus_add::l_minus::a_ac)) 1); +by (Asm_full_simp_tac 1); qed "long_div_quo_unique"; Goal @@ -183,7 +276,11 @@ \ f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> r1 = r2"; by (subgoal_tac "q1 = q2" 1); by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [a_lcancel_eq]) 1); +by (res_inst_tac [("a", "q2 * g + r1 - q2 * g"), ("b", "q2 * g + r2 - q2 * g")] + box_equals 1); +by (Asm_full_simp_tac 1); +by (Simp_tac 1); +by (Simp_tac 1); by (rtac long_div_quo_unique 1); by (REPEAT (atac 1)); qed "long_div_rem_unique"; diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/poly/LongDiv.thy --- a/src/HOL/Algebra/poly/LongDiv.thy Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/Algebra/poly/LongDiv.thy Thu Nov 28 10:50:42 2002 +0100 @@ -7,11 +7,11 @@ LongDiv = PolyHomo + consts - lcoeff :: "'a::ringS up => 'a" - eucl_size :: 'a::ringS => nat + lcoeff :: "'a::ring up => 'a" + eucl_size :: 'a::ring => nat defs - lcoeff_def "lcoeff p == coeff (deg p) p" + lcoeff_def "lcoeff p == coeff p (deg p)" eucl_size_def "eucl_size p == if p = 0 then 0 else deg p+1" end diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/poly/PolyHomo.ML --- a/src/HOL/Algebra/poly/PolyHomo.ML Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/Algebra/poly/PolyHomo.ML Thu Nov 28 10:50:42 2002 +0100 @@ -4,8 +4,85 @@ Author: Clemens Ballarin, started 16 April 1997 *) +(* Summation result for tactic-style proofs *) + +val natsum_add = thm "natsum_add"; +val natsum_ldistr = thm "natsum_ldistr"; +val natsum_rdistr = thm "natsum_rdistr"; + +Goal + "!! f::(nat=>'a::ring). \ +\ m <= n & (ALL i. m < i & i <= n --> f i = 0) --> \ +\ setsum f {..m} = setsum f {..n}"; +by (induct_tac "n" 1); +(* Base case *) +by (Simp_tac 1); +(* Induction step *) +by (case_tac "m <= n" 1); +by Auto_tac; +by (subgoal_tac "m = Suc n" 1); +by (Asm_simp_tac 1); +by (fast_arith_tac 1); +val SUM_shrink_lemma = result(); + +Goal + "!! f::(nat=>'a::ring). \ +\ [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..n}) |] \ +\ ==> P (setsum f {..m})"; +by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1); +by (Asm_full_simp_tac 1); +qed "SUM_shrink"; + +Goal + "!! f::(nat=>'a::ring). \ +\ [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..m}) |] \ +\ ==> P (setsum f {..n})"; +by (cut_inst_tac [("m", "m"), ("n", "n"), ("f", "f")] SUM_shrink_lemma 1); +by (Asm_full_simp_tac 1); +qed "SUM_extend"; + +Goal + "!!f::nat=>'a::ring. j <= n + m --> \ +\ setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..j} = \ +\ setsum (%k. setsum (%i. f k * g i) {..j - k}) {..j}"; +by (induct_tac "j" 1); +(* Base case *) +by (Simp_tac 1); +(* Induction step *) +by (simp_tac (simpset() addsimps [Suc_diff_le, natsum_add]) 1); +(* +by (asm_simp_tac (simpset() addsimps a_ac) 1); +*) +by (Asm_simp_tac 1); +val DiagSum_lemma = result(); + +Goal + "!!f::nat=>'a::ring. \ +\ setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..n + m} = \ +\ setsum (%k. setsum (%i. f k * g i) {..n + m - k}) {..n + m}"; +by (rtac (DiagSum_lemma RS mp) 1); +by (rtac le_refl 1); +qed "DiagSum"; + +Goal + "!! f::nat=>'a::ring. [| bound n f; bound m g|] ==> \ +\ setsum (%k. setsum (%i. f i * g (k-i)) {..k}) {..n + m} = \ +\ setsum f {..n} * setsum g {..m}"; +by (simp_tac (simpset() addsimps [natsum_ldistr, DiagSum]) 1); +(* SUM_rdistr must be applied after SUM_ldistr ! *) +by (simp_tac (simpset() addsimps [natsum_rdistr]) 1); +by (res_inst_tac [("m", "n"), ("n", "n+m")] SUM_extend 1); +by (rtac le_add1 1); +by (Force_tac 1); +by (rtac (thm "natsum_cong") 1); +by (rtac refl 1); +by (res_inst_tac [("m", "m"), ("n", "n+m-i")] SUM_shrink 1); +by (asm_simp_tac (simpset() addsimps [le_add_diff]) 1); +by Auto_tac; +qed "CauchySum"; + (* Ring homomorphisms and polynomials *) - +(* Goal "homo (const::'a::ring=>'a up)"; by (auto_tac (claset() addSIs [homoI], simpset())); qed "const_homo"; @@ -19,6 +96,15 @@ qed "homo_smult"; Addsimps [homo_smult]; +*) + +val deg_add = thm "deg_add"; +val deg_mult_ring = thm "deg_mult_ring"; +val deg_aboveD = thm "deg_aboveD"; +val coeff_add = thm "coeff_add"; +val coeff_mult = thm "coeff_mult"; +val boundI = thm "boundI"; +val monom_mult_is_smult = thm "monom_mult_is_smult"; (* Evaluation homomorphism *) @@ -42,7 +128,7 @@ by (rtac le_maxI2 1); by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); (* actual homom property + *) -by (asm_simp_tac (simpset() addsimps [l_distr, SUM_add]) 1); +by (asm_simp_tac (simpset() addsimps [l_distr, natsum_add]) 1); (* * commutes *) by (res_inst_tac [("m", "deg (aa * b)"), ("n", "deg aa + deg b")] @@ -53,34 +139,33 @@ by (rtac CauchySum 2); by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2); by (asm_simp_tac (simpset() addsimps [boundI, deg_aboveD]) 2); -(* getting a^i and a^(k-i) together is difficult, so we do is manually *) +(* getting a^i and a^(k-i) together is difficult, so we do it manually *) by (res_inst_tac [("s", " setsum \ \ (%k. setsum \ -\ (%i. phi (coeff i aa) * (phi (coeff (k - i) b) * \ +\ (%i. phi (coeff aa i) * (phi (coeff b (k - i)) * \ \ (a ^ i * a ^ (k - i)))) {..k}) \ \ {..deg aa + deg b}")] trans 1); by (asm_simp_tac (simpset() - addsimps [power_mult, leD RS add_diff_inverse, SUM_ldistr]) 1); -by (simp_tac (simpset() addsimps m_ac) 1); -by (simp_tac (simpset() addsimps m_ac) 1); -(* <1> commutes *) + addsimps [power_mult, leD RS add_diff_inverse, natsum_ldistr]) 1); +by (Simp_tac 1); +(* 1 commutes *) by (Asm_simp_tac 1); qed "EVAL2_homo"; Goalw [EVAL2_def] - "!! phi::'a::ring=>'b::ring. EVAL2 phi a (const b) = phi b"; + "!! phi::'a::ring=>'b::ring. EVAL2 phi a (monom b 0) = phi b"; by (Simp_tac 1); qed "EVAL2_const"; Goalw [EVAL2_def] - "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1) = a"; -(* Must be able to distinguish 0 from <1>, hence 'a::domain *) + "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 1) = a"; +(* Must be able to distinguish 0 from 1, hence 'a::domain *) by (Asm_simp_tac 1); qed "EVAL2_monom1"; Goalw [EVAL2_def] - "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom n) = a ^ n"; + "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 n) = a ^ n"; by (Simp_tac 1); by (case_tac "n" 1); by Auto_tac; @@ -89,19 +174,35 @@ Goal "!! phi::'a::ring=>'b::ring. \ \ homo phi ==> EVAL2 phi a (b *s p) = phi b * EVAL2 phi a p"; -by (asm_simp_tac - (simpset() addsimps [const_mult_is_smult RS sym, EVAL2_homo, EVAL2_const]) 1); +by (asm_simp_tac (simpset() + addsimps [monom_mult_is_smult RS sym, EVAL2_homo, EVAL2_const]) 1); qed "EVAL2_smult"; +val up_eqI = thm "up_eqI"; + +Goal "monom (a::'a::ring) n = monom a 0 * monom 1 n"; +by (simp_tac (simpset() addsimps [monom_mult_is_smult]) 1); +by (rtac up_eqI 1); +by (Simp_tac 1); +qed "monom_decomp"; + +Goal + "!! phi::'a::domain=>'b::ring. \ +\ homo phi ==> EVAL2 phi a (monom b n) = phi b * a ^ n"; +by (stac monom_decomp 1); +by (asm_simp_tac (simpset() + addsimps [EVAL2_homo, EVAL2_const, EVAL2_monom]) 1); +qed "EVAL2_monom_n"; + Goalw [EVAL_def] "!! a::'a::ring. homo (EVAL a)"; -by (asm_simp_tac (simpset() addsimps [EVAL2_homo, id_homo]) 1); +by (asm_simp_tac (simpset() addsimps [EVAL2_homo]) 1); qed "EVAL_homo"; -Goalw [EVAL_def] "!! a::'a::ring. EVAL a (const b) = b"; +Goalw [EVAL_def] "!! a::'a::ring. EVAL a (monom b 0) = b"; by (asm_simp_tac (simpset() addsimps [EVAL2_const]) 1); qed "EVAL_const"; -Goalw [EVAL_def] "!! a::'a::domain. EVAL a (monom n) = a ^ n"; +Goalw [EVAL_def] "!! a::'a::domain. EVAL a (monom 1 n) = a ^ n"; by (asm_simp_tac (simpset() addsimps [EVAL2_monom]) 1); qed "EVAL_monom"; @@ -109,19 +210,23 @@ by (asm_simp_tac (simpset() addsimps [EVAL2_smult]) 1); qed "EVAL_smult"; +Goalw [EVAL_def] "!! a::'a::domain. EVAL a (monom b n) = b * a ^ n"; +by (asm_simp_tac (simpset() addsimps [EVAL2_monom_n]) 1); +qed "EVAL_monom_n"; + (* Examples *) Goal "EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c"; by (asm_simp_tac (simpset() delsimps [power_Suc] - addsimps [EVAL_homo, EVAL_monom, EVAL_smult]) 1); + addsimps [EVAL_homo, EVAL_monom, EVAL_monom_n]) 1); result(); Goal "EVAL (y::'a::domain) \ -\ (EVAL (const x) (monom 1 + const (a*X^2 + b*X^1 + c*X^0))) = \ +\ (EVAL (monom x 0) (monom 1 1 + monom (a*X^2 + b*X^1 + c*X^0) 0)) = \ \ x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)"; by (asm_simp_tac (simpset() delsimps [power_Suc] - addsimps [EVAL_homo, EVAL_monom, EVAL_smult, EVAL_const]) 1); + addsimps [EVAL_homo, EVAL_monom, EVAL_monom_n, EVAL_const]) 1); result(); diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/poly/PolyHomo.thy --- a/src/HOL/Algebra/poly/PolyHomo.thy Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/Algebra/poly/PolyHomo.thy Thu Nov 28 10:50:42 2002 +0100 @@ -4,20 +4,15 @@ Author: Clemens Ballarin, started 15 April 1997 *) -PolyHomo = Degree + - -(* Instantiate result from Degree.ML *) - -instance - up :: (domain) domain (up_one_not_zero, up_integral) +PolyHomo = UnivPoly + consts - EVAL2 :: "('a::ring => 'b) => 'b => 'a up => 'b::ring" - EVAL :: "'a::ring => 'a up => 'a" + EVAL2 :: "['a::ring => 'b, 'b, 'a up] => 'b::ring" + EVAL :: "['a::ring, 'a up] => 'a" defs EVAL2_def "EVAL2 phi a p == - setsum (%i. phi (coeff i p) * a ^ i) {..deg p}" + setsum (%i. phi (coeff p i) * a ^ i) {..deg p}" EVAL_def "EVAL == EVAL2 (%x. x)" end diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/poly/PolyRing.ML --- a/src/HOL/Algebra/poly/PolyRing.ML Wed Nov 27 17:25:41 2002 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,68 +0,0 @@ -(* - Instantiate polynomials to form a ring and prove further properties - $Id$ - Author: Clemens Ballarin, started 22 January 1997 -*) - -(* Properties of *s: - Polynomials form a module *) - -goal UnivPoly.thy "!!a::'a::ring. (a + b) *s p = a *s p + b *s p"; -by (rtac up_eqI 1); -by (simp_tac (simpset() addsimps [l_distr]) 1); -qed "smult_l_distr"; - -goal UnivPoly.thy "!!a::'a::ring. a *s (p + q) = a *s p + a *s q"; -by (rtac up_eqI 1); -by (simp_tac (simpset() addsimps [r_distr]) 1); -qed "smult_r_distr"; - -goal UnivPoly.thy "!!a::'a::ring. (a * b) *s p = a *s (b *s p)"; -by (rtac up_eqI 1); -by (simp_tac (simpset() addsimps [m_assoc]) 1); -qed "smult_assoc1"; - -goal UnivPoly.thy "(<1>::'a::ring) *s p = p"; -by (rtac up_eqI 1); -by (Simp_tac 1); -qed "smult_one"; - -(* Polynomials form an algebra *) - -goal UnivPoly.thy "!!a::'a::ring. (a *s p) * q = a *s (p * q)"; -by (rtac up_eqI 1); -by (simp_tac (simpset() addsimps [SUM_rdistr, m_assoc]) 1); -qed "smult_assoc2"; - -(* the following can be derived from the above ones, - for generality reasons, it is therefore done *) - -Goal "(0::'a::ring) *s p = 0"; -by (rtac a_lcancel 1); -by (rtac (smult_l_distr RS sym RS trans) 1); -by (Simp_tac 1); -qed "smult_l_null"; - -Goal "!!a::'a::ring. a *s 0 = 0"; -by (rtac a_lcancel 1); -by (rtac (smult_r_distr RS sym RS trans) 1); -by (Simp_tac 1); -qed "smult_r_null"; - -Goal "!!a::'a::ring. (-a) *s p = - (a *s p)"; -by (rtac a_lcancel 1); -by (rtac (r_neg RS sym RSN (2, trans)) 1); -by (rtac (smult_l_distr RS sym RS trans) 1); -by (simp_tac (simpset() addsimps [smult_l_null, r_neg]) 1); -qed "smult_l_minus"; - -Goal "!!a::'a::ring. a *s (-p) = - (a *s p)"; -by (rtac a_lcancel 1); -by (rtac (r_neg RS sym RSN (2, trans)) 1); -by (rtac (smult_r_distr RS sym RS trans) 1); -by (simp_tac (simpset() addsimps [smult_r_null, r_neg]) 1); -qed "smult_r_minus"; - -val smult_minus = [smult_l_minus, smult_r_minus]; - -Addsimps [smult_one, smult_l_null, smult_r_null]; diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/poly/PolyRing.thy --- a/src/HOL/Algebra/poly/PolyRing.thy Wed Nov 27 17:25:41 2002 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -(* - Instantiate polynomials to form a ring and prove further properties - $Id$ - Author: Clemens Ballarin, started 20 January 1997 -*) - -PolyRing = UnivPoly + - -instance - up :: (ring) ring - (up_a_assoc, up_l_zero, up_l_neg, up_a_comm, - up_m_assoc, up_l_one, up_l_distr, up_m_comm, - up_inverse_def, up_divide_def, up_power_def) {| ALLGOALS (rtac refl) |} - -end diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/poly/ProtoPoly.ML --- a/src/HOL/Algebra/poly/ProtoPoly.ML Wed Nov 27 17:25:41 2002 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,30 +0,0 @@ -(* - Prepearing definitions for polynomials - $Id$ - Author: Clemens Ballarin, started 9 December 1996 -*) - -(* Rules for bound *) - -val prem = goalw ProtoPoly.thy [bound_def] - "[| !! m. n < m ==> f m = 0 |] ==> bound n f"; -by (fast_tac (claset() addIs prem) 1); -qed "boundI"; - -Goalw [bound_def] - "!! f. [| bound n f; n < m |] ==> f m = 0"; -by (Fast_tac 1); -qed "boundD"; - -Goalw [bound_def] - "!! f. [| bound n f; n <= m |] ==> bound m f"; -by (fast_tac (set_cs addIs [le_less_trans]) 1); -(* Need set_cs, otherwise starts reasoning about naturals *) -qed "le_bound"; - -AddSIs [boundI]; -AddDs [boundD]; - -Goal "(%x. 0) : {f. EX n. bound n f}"; -by (Blast_tac 1); -qed "UP_witness"; diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/poly/ProtoPoly.thy --- a/src/HOL/Algebra/poly/ProtoPoly.thy Wed Nov 27 17:25:41 2002 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -(* - Prepearing definitions for polynomials - $Id$ - Author: Clemens Ballarin, started 9 December 1996 -*) - -ProtoPoly = Abstract + - -consts - bound :: [nat, nat => 'a::ringS] => bool - -defs - bound_def "bound n f == ALL i. n f i = 0" - -end diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/poly/UnivPoly.ML --- a/src/HOL/Algebra/poly/UnivPoly.ML Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/Algebra/poly/UnivPoly.ML Thu Nov 28 10:50:42 2002 +0100 @@ -1,242 +1,359 @@ (* - Univariate Polynomials + Degree of polynomials $Id$ - Author: Clemens Ballarin, started 9 December 1996 -TODO: monom is *mono*morphism (probably induction needed) + written by Clemens Ballarin, started 22 January 1997 *) -(* Closure of UP under +, *s, monom, const and * *) +(* +(* Relating degree and bound *) + +Goal "[| bound m f; f n ~= 0 |] ==> n <= m"; +by (force_tac (claset() addDs [inst "m" "n" boundD], + simpset()) 1); +qed "below_bound"; + +goal UnivPoly.thy "bound (LEAST n. bound n (Rep_UP p)) (Rep_UP p)"; +by (rtac exE 1); +by (rtac LeastI 2); +by (assume_tac 2); +by (res_inst_tac [("a", "Rep_UP p")] CollectD 1); +by (rtac (rewrite_rule [UP_def] Rep_UP) 1); +qed "Least_is_bound"; + +Goalw [coeff_def, deg_def] + "!! p. ALL m. n < m --> coeff m p = 0 ==> deg p <= n"; +by (rtac Least_le 1); +by (Fast_tac 1); +qed "deg_aboveI"; + +Goalw [coeff_def, deg_def] + "(n ~= 0 --> coeff n p ~= 0) ==> n <= deg p"; +by (case_tac "n = 0" 1); +(* Case n=0 *) +by (Asm_simp_tac 1); +(* Case n~=0 *) +by (rotate_tac 1 1); +by (Asm_full_simp_tac 1); +by (rtac below_bound 1); +by (assume_tac 2); +by (rtac Least_is_bound 1); +qed "deg_belowI"; + +Goalw [coeff_def, deg_def] + "deg p < m ==> coeff m p = 0"; +by (rtac exE 1); (* create !! x. *) +by (rtac boundD 2); +by (assume_tac 3); +by (rtac LeastI 2); +by (assume_tac 2); +by (res_inst_tac [("a", "Rep_UP p")] CollectD 1); +by (rtac (rewrite_rule [UP_def] Rep_UP) 1); +qed "deg_aboveD"; + +Goalw [deg_def] + "deg p = Suc y ==> ~ bound y (Rep_UP p)"; +by (rtac not_less_Least 1); +by (Asm_simp_tac 1); +val lemma1 = result(); + +Goalw [deg_def, coeff_def] + "deg p = Suc y ==> coeff (deg p) p ~= 0"; +by (rtac ccontr 1); +by (dtac notnotD 1); +by (cut_inst_tac [("p", "p")] Least_is_bound 1); +by (subgoal_tac "bound y (Rep_UP p)" 1); +(* prove subgoal *) +by (rtac boundI 2); +by (case_tac "Suc y < m" 2); +(* first case *) +by (rtac boundD 2); +by (assume_tac 2); +by (Asm_simp_tac 2); +(* second case *) +by (dtac leI 2); +by (dtac Suc_leI 2); +by (dtac le_anti_sym 2); +by (assume_tac 2); +by (Asm_full_simp_tac 2); +(* end prove subgoal *) +by (fold_goals_tac [deg_def]); +by (dtac lemma1 1); +by (etac notE 1); +by (assume_tac 1); +val lemma2 = result(); + +Goal "deg p ~= 0 ==> coeff (deg p) p ~= 0"; +by (rtac lemma2 1); +by (Full_simp_tac 1); +by (dtac Suc_pred 1); +by (rtac sym 1); +by (Asm_simp_tac 1); +qed "deg_lcoeff"; -Goalw [UP_def] - "[| f : UP; g : UP |] ==> (%n. (f n + g n::'a::ring)) : UP"; -by Auto_tac; -(* instantiate bound for the sum and do case split *) -by (res_inst_tac [("x", "if n<=na then na else n")] exI 1); -by Auto_tac; -(* first case, bound of g higher *) -by (dtac le_bound 1 THEN assume_tac 1); -by (Force_tac 1); -(* second case is identical, - apart from we have to massage the inequality *) -by (dtac (not_leE RS less_imp_le) 1); -by (dtac le_bound 1 THEN assume_tac 1); -by (Force_tac 1); -qed "UP_closed_add"; +Goal "p ~= 0 ==> coeff (deg p) p ~= 0"; +by (etac contrapos_np 1); +by (case_tac "deg p = 0" 1); +by (blast_tac (claset() addSDs [deg_lcoeff]) 2); +by (rtac up_eqI 1); +by (case_tac "n=0" 1); +by (rotate_tac ~2 1); +by (Asm_full_simp_tac 1); +by (asm_full_simp_tac (simpset() addsimps [deg_aboveD]) 1); +qed "nonzero_lcoeff"; + +Goal "(deg p <= n) = bound n (Rep_UP p)"; +by (rtac iffI 1); +(* ==> *) +by (rtac boundI 1); +by (fold_goals_tac [coeff_def]); +by (rtac deg_aboveD 1); +by (fast_arith_tac 1); +(* <== *) +by (rtac deg_aboveI 1); +by (rewtac coeff_def); +by (Fast_tac 1); +qed "deg_above_is_bound"; + +(* Lemmas on the degree function *) + +Goalw [max_def] + "!! p::'a::ring up. deg (p + q) <= max (deg p) (deg q)"; +by (case_tac "deg p <= deg q" 1); +(* case deg p <= deg q *) +by (rtac deg_aboveI 1); +by (Asm_simp_tac 1); +by (strip_tac 1); +by (dtac le_less_trans 1); +by (assume_tac 1); +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); +(* case deg p > deg q *) +by (rtac deg_aboveI 1); +by (Asm_simp_tac 1); +by (dtac not_leE 1); +by (strip_tac 1); +by (dtac less_trans 1); +by (assume_tac 1); +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); +qed "deg_add"; -Goalw [UP_def] - "f : UP ==> (%n. (a * f n::'a::ring)) : UP"; -by (Force_tac 1); -qed "UP_closed_smult"; +Goal "!!p::('a::ring up). deg p < deg q ==> deg (p + q) = deg q"; +by (rtac order_antisym 1); +by (rtac le_trans 1); +by (rtac deg_add 1); +by (Asm_simp_tac 1); +by (rtac deg_belowI 1); +by (asm_simp_tac (simpset() addsimps [deg_aboveD, deg_lcoeff]) 1); +qed "deg_add_equal"; + +Goal "deg (monom m::'a::ring up) <= m"; +by (asm_simp_tac + (simpset() addsimps [deg_aboveI, less_not_refl2 RS not_sym]) 1); +qed "deg_monom_ring"; + +Goal "deg (monom m::'a::domain up) = m"; +by (rtac le_anti_sym 1); +(* <= *) +by (rtac deg_monom_ring 1); +(* >= *) +by (asm_simp_tac + (simpset() addsimps [deg_belowI, less_not_refl2 RS not_sym]) 1); +qed "deg_monom"; -Goalw [UP_def] - "(%n. if m = n then <1> else 0) : UP"; -by Auto_tac; -qed "UP_closed_monom"; +Goal "!! a::'a::ring. deg (const a) = 0"; +by (rtac le_anti_sym 1); +by (rtac deg_aboveI 1); +by (simp_tac (simpset() addsimps [less_not_refl2]) 1); +by (rtac deg_belowI 1); +by (simp_tac (simpset() addsimps [less_not_refl2]) 1); +qed "deg_const"; + +Goal "deg (0::'a::ringS up) = 0"; +by (rtac le_anti_sym 1); +by (rtac deg_aboveI 1); +by (Simp_tac 1); +by (rtac deg_belowI 1); +by (Simp_tac 1); +qed "deg_zero"; -Goalw [UP_def] "(%n. if n = 0 then a else 0) : UP"; -by Auto_tac; -qed "UP_closed_const"; +Goal "deg (<1>::'a::ring up) = 0"; +by (rtac le_anti_sym 1); +by (rtac deg_aboveI 1); +by (simp_tac (simpset() addsimps [less_not_refl2]) 1); +by (rtac deg_belowI 1); +by (Simp_tac 1); +qed "deg_one"; + +Goal "!!p::('a::ring) up. deg (-p) = deg p"; +by (rtac le_anti_sym 1); +(* <= *) +by (simp_tac (simpset() addsimps [deg_aboveI, deg_aboveD]) 1); +by (simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff, uminus_monom_neq]) 1); +qed "deg_uminus"; + +Addsimps [deg_monom, deg_const, deg_zero, deg_one, deg_uminus]; Goal - "!! f::nat=>'a::ring. \ -\ [| bound n f; bound m g; n + m < k |] ==> f i * g (k - i) = 0"; -(* Case split: either f i or g (k - i) is zero *) -by (case_tac "n \ -\ (%n. (setsum (%i. f i * g (n-i)) {..n}::'a::ring)) : UP"; -by (Step_tac 1); -(* Instantiate bound for the product, and remove bound in goal *) -by (res_inst_tac [("x", "n + na")] exI 1); -by (Step_tac 1); -(* Show that the sum is 0 *) -by (asm_simp_tac (simpset() addsimps [bound_mult_zero]) 1); -qed "UP_closed_mult"; +Goal + "!! a::'a::domain. deg (a *s p) = (if a = 0 then 0 else deg p)"; +by (rtac le_anti_sym 1); +by (rtac deg_smult_ring 1); +by (case_tac "a = 0" 1); +by (REPEAT (asm_simp_tac (simpset() addsimps [deg_belowI, deg_lcoeff]) 1)); +qed "deg_smult"; -(* %x. 0 represents a polynomial *) - -Goalw [UP_def] "(%x. 0) : UP"; -by (Fast_tac 1); -qed "UP_zero"; - -(* Effect of +, *s, monom, * and the other operations on the coefficients *) +Goal + "!! p::'a::ring up. [| deg p + deg q < k |] ==> \ +\ coeff i p * coeff (k - i) q = 0"; +by (simp_tac (simpset() addsimps [coeff_def]) 1); +by (rtac bound_mult_zero 1); +by (assume_tac 3); +by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1); +by (simp_tac (simpset() addsimps [deg_above_is_bound RS sym]) 1); +qed "deg_above_mult_zero"; -Goalw [coeff_def, up_add_def] - "coeff n (p+q) = (coeff n p + coeff n q::'a::ring)"; -by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_add, Rep_UP]) 1); -qed "coeff_add"; +Goal + "!! p::'a::ring up. deg (p * q) <= deg p + deg q"; +by (rtac deg_aboveI 1); +by (asm_simp_tac (simpset() addsimps [deg_above_mult_zero]) 1); +qed "deg_mult_ring"; -Goalw [coeff_def, up_smult_def] - "!!a::'a::ring. coeff n (a *s p) = a * coeff n p"; -by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_smult, Rep_UP]) 1); -qed "coeff_smult"; +goal Main.thy + "!!k::nat. k < n ==> m < n + m - k"; +by (arith_tac 1); +qed "less_add_diff"; -Goalw [coeff_def, monom_def] - "coeff n (monom m) = (if m=n then <1> else 0)"; -by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_monom, Rep_UP]) 1); -qed "coeff_monom"; +Goal "!!p. coeff n p ~= 0 ==> n <= deg p"; +(* More general than deg_belowI, and simplifies the next proof! *) +by (rtac deg_belowI 1); +by (Fast_tac 1); +qed "deg_below2I"; -Goalw [coeff_def, const_def] - "coeff n (const a) = (if n=0 then a else 0)"; -by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_const, Rep_UP]) 1); -qed "coeff_const"; - -Goalw [coeff_def, up_mult_def] - "coeff n (p * q) = (setsum (%i. coeff i p * coeff (n-i) q) {..n}::'a::ring)"; -by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_mult, Rep_UP]) 1); -qed "coeff_mult"; - -Goalw [coeff_def, up_zero_def] "coeff n 0 = 0"; -by (asm_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_zero, Rep_UP]) 1); -qed "coeff_zero"; - -Addsimps [coeff_add, coeff_smult, coeff_monom, coeff_const, - coeff_mult, coeff_zero]; - -Goalw [up_one_def] - "coeff n <1> = (if n=0 then <1> else 0)"; +Goal + "!! p::'a::domain up. \ +\ [| p ~= 0; q ~= 0 |] ==> deg (p * q) = deg p + deg q"; +by (rtac le_anti_sym 1); +by (rtac deg_mult_ring 1); +(* deg p + deg q <= deg (p * q) *) +by (rtac deg_below2I 1); by (Simp_tac 1); -qed "coeff_one"; +(* +by (rtac conjI 1); +by (rtac impI 1); +*) +by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1); +by (rtac le_add1 1); +by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1); +by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1); +by (rtac le_refl 1); +by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1); +by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1); +(* +by (rtac impI 1); +by (res_inst_tac [("m", "deg p"), ("n", "deg p + deg q")] SUM_extend 1); +by (rtac le_add1 1); +by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1); +by (res_inst_tac [("m", "deg p"), ("n", "deg p")] SUM_extend_below 1); +by (rtac le_refl 1); +by (asm_simp_tac (simpset() addsimps [deg_aboveD, less_add_diff]) 1); +by (asm_simp_tac (simpset() addsimps [nonzero_lcoeff]) 1); +*) +qed "deg_mult"; -Goalw [up_uminus_def] "coeff n (-p) = (-coeff n p::'a::ring)"; -by (simp_tac (simpset() addsimps m_minus) 1); -qed "coeff_uminus"; +Addsimps [deg_smult, deg_mult]; + +(* Representation theorems about polynomials *) -Addsimps [coeff_one, coeff_uminus]; - -(* Polynomials form a ring *) +goal PolyRing.thy + "!! p::nat=>'a::ring up. \ +\ coeff k (setsum p {..n}) = setsum (%i. coeff k (p i)) {..n}"; +by (induct_tac "n" 1); +by Auto_tac; +qed "coeff_SUM"; -val prems = Goalw [coeff_def] - "(!! n. coeff n p = coeff n q) ==> p = q"; -by (res_inst_tac [("t", "p")] (Rep_UP_inverse RS subst) 1); -by (res_inst_tac [("t", "q")] (Rep_UP_inverse RS subst) 1); -by (asm_simp_tac (simpset() addsimps prems) 1); -qed "up_eqI"; +goal UnivPoly.thy + "!! f::(nat=>'a::ring). \ +\ bound n f ==> setsum (%i. if i = x then f i else 0) {..n} = f x"; +by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1); +by (auto_tac + (claset() addDs [not_leE], + simpset())); +qed "bound_SUM_if"; -Goalw [coeff_def] - "coeff n p ~= coeff n q ==> p ~= q"; -by Auto_tac; -qed "up_neqI"; - -Goal "!! a::('a::ring) up. (a + b) + c = a + (b + c)"; -by (rtac up_eqI 1); -by (Simp_tac 1); -by (rtac a_assoc 1); -qed "up_a_assoc"; - -Goal "!! a::('a::ring) up. 0 + a = a"; +Goal + "!! p::'a::ring up. deg p <= n ==> \ +\ setsum (%i. coeff i p *s monom i) {..n} = p"; by (rtac up_eqI 1); -by (Simp_tac 1); -qed "up_l_zero"; - -Goal "!! a::('a::ring) up. (-a) + a = 0"; -by (rtac up_eqI 1); -by (Simp_tac 1); -qed "up_l_neg"; - -Goal "!! a::('a::ring) up. a + b = b + a"; -by (rtac up_eqI 1); -by (Simp_tac 1); -by (rtac a_comm 1); -qed "up_a_comm"; - -Goal "!! a::('a::ring) up. (a * b) * c = a * (b * c)"; -by (rtac up_eqI 1); -by (Simp_tac 1); -by (rtac poly_assoc_lemma 1); -qed "up_m_assoc"; - -Goal "!! a::('a::ring) up. <1> * a = a"; -by (rtac up_eqI 1); -by (Simp_tac 1); -by (case_tac "n" 1); -(* 0 case *) -by (Asm_simp_tac 1); -(* Suc case *) -by (asm_simp_tac (simpset() delsimps [SUM_Suc] addsimps [SUM_Suc2]) 1); -qed "up_l_one"; - -Goal "!! a::('a::ring) up. (a + b) * c = a * c + b * c"; -by (rtac up_eqI 1); -by (simp_tac (simpset() addsimps [l_distr, SUM_add]) 1); -qed "up_l_distr"; - -Goal "!! a::('a::ring) up. a * b = b * a"; -by (rtac up_eqI 1); -by (cut_inst_tac [("a", "%i. coeff i a"), ("b", "%i. coeff i b")] - poly_comm_lemma 1); -by (asm_full_simp_tac (simpset() addsimps [m_comm]) 1); -qed "up_m_comm"; - -(* Further algebraic rules *) - -Goal "!! a::'a::ring. const a * p = a *s p"; -by (rtac up_eqI 1); -by (case_tac "n" 1); -by (Asm_simp_tac 1); -by (asm_simp_tac (simpset() delsimps [SUM_Suc] addsimps [SUM_Suc2]) 1); -qed "const_mult_is_smult"; - -Goal "!! a::'a::ring. const (a + b) = const a + const b"; -by (rtac up_eqI 1); -by (Simp_tac 1); -qed "const_add"; - -Goal "!! a::'a::ring. const (a * b) = const a * const b"; -by (simp_tac (simpset() addsimps [const_mult_is_smult]) 1); -by (rtac up_eqI 1); -by (Simp_tac 1); -qed "const_mult"; - -Goal "const (<1>::'a::ring) = <1>"; -by (rtac up_eqI 1); -by (Simp_tac 1); -qed "const_one"; - -Goal "const (0::'a::ring) = 0"; -by (rtac up_eqI 1); -by (Simp_tac 1); -qed "const_zero"; - -Addsimps [const_add, const_mult, const_one, const_zero]; - -Goalw [inj_on_def, UNIV_def, const_def] "inj const"; -by (Simp_tac 1); -by (strip_tac 1); -by (dres_inst_tac [("f", "Rep_UP")] arg_cong 1); -by (full_simp_tac (simpset() addsimps [Abs_UP_inverse, UP_closed_const, - expand_fun_eq]) 1); -by (dres_inst_tac [("x", "0")] spec 1); -by (Full_simp_tac 1); -qed "const_inj"; - -(*Lemma used in PolyHomo*) -Goal - "!! f::nat=>'a::ring. [| bound n f; bound m g|] ==> \ -\ setsum (%k. setsum (%i. f i * g (k-i)) {..k}) {..n + m} = \ -\ setsum f {..n} * setsum g {..m}"; -by (simp_tac (simpset() addsimps [SUM_ldistr, DiagSum]) 1); -(* SUM_rdistr must be applied after SUM_ldistr ! *) -by (simp_tac (simpset() addsimps [SUM_rdistr]) 1); -by (res_inst_tac [("m", "n"), ("n", "n+m")] SUM_extend 1); -by (rtac le_add1 1); -by (Force_tac 1); +by (simp_tac (simpset() addsimps [coeff_SUM]) 1); +by (rtac trans 1); +by (res_inst_tac [("x", "na")] bound_SUM_if 2); +by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2); by (rtac SUM_cong 1); by (rtac refl 1); -by (res_inst_tac [("m", "m"), ("n", "n+m-i")] SUM_shrink 1); -by (asm_simp_tac (simpset() addsimps [le_add_diff]) 1); -by Auto_tac; -qed "CauchySum"; +by (Asm_simp_tac 1); +qed "up_repr"; + +Goal + "!! p::'a::ring up. [| deg p <= n; P p |] ==> \ +\ P (setsum (%i. coeff i p *s monom i) {..n})"; +by (asm_simp_tac (simpset() addsimps [up_repr]) 1); +qed "up_reprD"; + +Goal + "!! p::'a::ring up. \ +\ [| deg p <= n; P (setsum (%i. coeff i p *s monom i) {..n}) |] \ +\ ==> P p"; +by (asm_full_simp_tac (simpset() addsimps [up_repr]) 1); +qed "up_repr2D"; + +(* +Goal + "!! p::'a::ring up. [| deg p <= n; deg q <= m |] ==> \ +\ (SUM n (%i. coeff i p *s monom i) = SUM m (%i. coeff i q *s monom i)) \ +\ = (coeff k f = coeff k g) +... +qed "up_unique"; +*) + +(* Polynomials over integral domains are again integral domains *) -Goal "<1> ~= (0::('a::domain) up)"; -by (res_inst_tac [("n", "0")] up_neqI 1); +Goal "!!p::'a::domain up. p * q = 0 ==> p = 0 | q = 0"; +by (rtac classical 1); +by (subgoal_tac "deg p = 0 & deg q = 0" 1); +by (res_inst_tac [("p", "p"), ("n", "0")] up_repr2D 1); +by (Asm_simp_tac 1); +by (res_inst_tac [("p", "q"), ("n", "0")] up_repr2D 1); +by (Asm_simp_tac 1); +by (subgoal_tac "coeff 0 p = 0 | coeff 0 q = 0" 1); +by (force_tac (claset() addIs [up_eqI], simpset()) 1); +by (rtac integral 1); +by (subgoal_tac "coeff 0 (p * q) = 0" 1); +by (Asm_simp_tac 2); +by (Full_simp_tac 1); +by (dres_inst_tac [("f", "deg")] arg_cong 1); +by (Asm_full_simp_tac 1); +qed "up_integral"; + +Goal "!! a::'a::domain. a *s p = 0 ==> a = 0 | p = 0"; +by (full_simp_tac (simpset() addsimps [const_mult_is_smult RS sym]) 1); +by (dtac up_integral 1); +by Auto_tac; +by (rtac (const_inj RS injD) 1); by (Simp_tac 1); -qed "up_one_not_zero"; +qed "smult_integral"; +*) + +(* Divisibility and degree *) + +Goalw [dvd_def] + "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q"; +by (etac exE 1); +by (hyp_subst_tac 1); +by (case_tac "p = 0" 1); +by (case_tac "k = 0" 2); +by Auto_tac; +qed "dvd_imp_deg"; diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Algebra/poly/UnivPoly.thy --- a/src/HOL/Algebra/poly/UnivPoly.thy Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/Algebra/poly/UnivPoly.thy Thu Nov 28 10:50:42 2002 +0100 @@ -1,44 +1,748 @@ (* - Univariate Polynomials - $Id$ - Author: Clemens Ballarin, started 9 December 1996 + Title: Univariate Polynomials + Id: $Id$ + Author: Clemens Ballarin, started 9 December 1996 + Copyright: Clemens Ballarin +*) + +header {* Univariate Polynomials *} + +theory UnivPoly = Abstract: + +(* already proved in Finite_Set.thy + +lemma setsum_cong: + "[| A = B; !!i. i : B ==> f i = g i |] ==> setsum f A = setsum g B" +proof - + assume prems: "A = B" "!!i. i : B ==> f i = g i" + show ?thesis + proof (cases "finite B") + case True + then have "!!A. [| A = B; !!i. i : B ==> f i = g i |] ==> + setsum f A = setsum g B" + proof induct + case empty thus ?case by simp + next + case insert thus ?case by simp + qed + with prems show ?thesis by simp + next + case False with prems show ?thesis by (simp add: setsum_def) + qed +qed *) -UnivPoly = ProtoPoly + +(* Instruct simplifier to simplify assumptions introduced by congs. + This makes setsum_cong more convenient to use, because assumptions + like i:{m..n} get simplified (to m <= i & i <= n). *) + +ML_setup {* + +Addcongs [thm "setsum_cong"]; +Context.>> (fn thy => (simpset_ref_of thy := + simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *} + +section {* Definition of type up *} + +constdefs + bound :: "[nat, nat => 'a::zero] => bool" + "bound n f == (ALL i. n < i --> f i = 0)" + +lemma boundI [intro!]: "[| !! m. n < m ==> f m = 0 |] ==> bound n f" +proof (unfold bound_def) +qed fast + +lemma boundE [elim?]: "[| bound n f; (!! m. n < m ==> f m = 0) ==> P |] ==> P" +proof (unfold bound_def) +qed fast + +lemma boundD [dest]: "[| bound n f; n < m |] ==> f m = 0" +proof (unfold bound_def) +qed fast + +lemma bound_below: + assumes bound: "bound m f" and nonzero: "f n ~= 0" shows "n <= m" +proof (rule classical) + assume "~ ?thesis" + then have "m < n" by arith + with bound have "f n = 0" .. + with nonzero show ?thesis by contradiction +qed typedef (UP) - ('a) up = "{f :: nat => 'a::ringS. EX n. bound n f}" (UP_witness) + ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}" +by (rule+) (* Question: what does trace_rule show??? *) -instance - up :: (ringS) ringS +section {* Constants *} consts - coeff :: [nat, 'a up] => 'a::ringS - "*s" :: ['a::ringS, 'a up] => 'a up (infixl 70) - monom :: nat => ('a::ringS) up - const :: 'a::ringS => 'a up + coeff :: "['a up, nat] => ('a::zero)" + monom :: "['a::zero, nat] => 'a up" ("(3_*X^/_)" [71, 71] 70) + "*s" :: "['a::{zero, times}, 'a up] => 'a up" (infixl 70) + +defs + coeff_def: "coeff p n == Rep_UP p n" + monom_def: "monom a n == Abs_UP (%i. if i=n then a else 0)" + smult_def: "a *s p == Abs_UP (%i. a * Rep_UP p i)" - "*X^" :: ['a, nat] => 'a up ("(3_*X^/_)" [71, 71] 70) +lemma coeff_bound_ex: "EX n. bound n (coeff p)" +proof - + have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP) + then obtain n where "bound n (coeff p)" by (unfold UP_def) fast + then show ?thesis .. +qed + +lemma bound_coeff_obtain: + assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P" +proof - + have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP) + then obtain n where "bound n (coeff p)" by (unfold UP_def) fast + with prem show P . +qed -translations - "a *X^ n" == "a *s monom n" - (* this translation is only nice for non-nested polynomials *) +text {* Ring operations *} + +instance up :: (zero) zero .. +instance up :: (one) one .. +instance up :: (plus) plus .. +instance up :: (minus) minus .. +instance up :: (times) times .. +instance up :: (inverse) inverse .. +instance up :: (power) power .. defs - coeff_def "coeff n p == Rep_UP p n" - up_add_def "p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)" - up_smult_def "a *s p == Abs_UP (%n. a * Rep_UP p n)" - monom_def "monom m == Abs_UP (%n. if m=n then <1> else 0)" - const_def "const a == Abs_UP (%n. if n=0 then a else 0)" - up_mult_def "p * q == Abs_UP (%n::nat. setsum + up_add_def: "p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)" + up_mult_def: "p * q == Abs_UP (%n::nat. setsum (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})" + up_zero_def: "0 == monom 0 0" + up_one_def: "1 == monom 1 0" + up_uminus_def:"- p == (- 1) *s p" + (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *) + (* note: - 1 is different from -1; latter is of class number *) + + up_minus_def: "(a::'a::{plus, minus} up) - b == a + (-b)" + up_inverse_def: "inverse (a::'a::{zero, one, times, inverse} up) == + (if a dvd 1 then THE x. a*x = 1 else 0)" + up_divide_def: "(a::'a::{times, inverse} up) / b == a * inverse b" + up_power_def: "(a::'a::{one, times, power} up) ^ n == + nat_rec 1 (%u b. b * a) n" + +subsection {* Effect of operations on coefficients *} + +lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)" +proof - + have "(%n. if n = m then a else 0) : UP" + using UP_def by force + from this show ?thesis + by (simp add: coeff_def monom_def Abs_UP_inverse Rep_UP) +qed + +lemma coeff_zero [simp]: "coeff 0 n = 0" +proof (unfold up_zero_def) +qed simp + +lemma coeff_one [simp]: "coeff 1 n = (if n=0 then 1 else 0)" +proof (unfold up_one_def) +qed simp + +lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n" +proof - + have "!!f. f : UP ==> (%n. a * f n) : UP" + by (unfold UP_def) (force simp add: ring_simps) + (* this force step is slow *) + then show ?thesis + by (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP) +qed + +lemma coeff_add [simp]: "coeff (p+q) n = (coeff p n + coeff q n::'a::ring)" +proof - + { + fix f g + assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP" + have "(%i. f i + g i) : UP" + proof - + from fup obtain n where boundn: "bound n f" + by (unfold UP_def) fast + from gup obtain m where boundm: "bound m g" + by (unfold UP_def) fast + have "bound (max n m) (%i. (f i + g i))" + proof + fix i + assume "max n m < i" + with boundn and boundm show "f i + g i = 0" + by (fastsimp simp add: ring_simps) + qed + then show "(%i. (f i + g i)) : UP" + by (unfold UP_def) fast + qed + } + then show ?thesis + by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP) +qed + +lemma coeff_mult [simp]: + "coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)" +proof - + { + fix f g + assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP" + have "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP" + proof - + from fup obtain n where "bound n f" + by (unfold UP_def) fast + from gup obtain m where "bound m g" + by (unfold UP_def) fast + have "bound (n + m) (%n. setsum (%i. f i * g (n-i)) {..n})" + proof + fix k + assume bound: "n + m < k" + { + fix i + have "f i * g (k-i) = 0" + proof cases + assume "n < i" + show ?thesis by (auto! simp add: ring_simps) + next + assume "~ (n < i)" + with bound have "m < k-i" by arith + then show ?thesis by (auto! simp add: ring_simps) + qed + } + then show "setsum (%i. f i * g (k-i)) {..k} = 0" + by (simp add: ring_simps) + qed + then show "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP" + by (unfold UP_def) fast + qed + } + then show ?thesis + by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP) +qed + +lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)" +by (unfold up_uminus_def) (simp add: ring_simps) + +(* Other lemmas *) + +lemma up_eqI: assumes prem: "(!! n. coeff p n = coeff q n)" shows "p = q" +proof - + have "p = Abs_UP (%u. Rep_UP p u)" by (simp add: Rep_UP_inverse) + also from prem have "... = Abs_UP (Rep_UP q)" by (simp only: coeff_def) + also have "... = q" by (simp add: Rep_UP_inverse) + finally show ?thesis . +qed + +(* ML_setup {* Addsimprocs [ring_simproc] *} *) + +instance up :: (ring) ring +proof + fix p q r :: "'a::ring up" + fix n + show "(p + q) + r = p + (q + r)" + by (rule up_eqI) simp + show "0 + p = p" + by (rule up_eqI) simp + show "(-p) + p = 0" + by (rule up_eqI) simp + show "p + q = q + p" + by (rule up_eqI) simp + show "(p * q) * r = p * (q * r)" + proof (rule up_eqI) + fix n + { + fix k and a b c :: "nat=>'a::ring" + have "k <= n ==> + setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} = + setsum (%j. a j * setsum (%i. b i * c (n-j-i)) {..k-j}) {..k}" + (is "_ ==> ?eq k") + proof (induct k) + case 0 show ?case by simp + next + case (Suc k) + then have "k <= n" by arith + then have "?eq k" by (rule Suc) + then show ?case + by (simp add: Suc_diff_le natsum_ldistr) + qed + } + then show "coeff ((p * q) * r) n = coeff (p * (q * r)) n" + by simp + qed + show "1 * p = p" + proof (rule up_eqI) + fix n + show "coeff (1 * p) n = coeff p n" + proof (cases n) + case 0 then show ?thesis by simp + next + case Suc then show ?thesis by (simp del: natsum_Suc add: natsum_Suc2) + qed + qed + show "(p + q) * r = p * r + q * r" + by (rule up_eqI) simp + show "p * q = q * p" + proof (rule up_eqI) + fix n + { + fix k + fix a b :: "nat=>'a::ring" + have "k <= n ==> + setsum (%i. a i * b (n-i)) {..k} = + setsum (%i. a (k-i) * b (i+n-k)) {..k}" + (is "_ ==> ?eq k") + proof (induct k) + case 0 show ?case by simp + next + case (Suc k) then show ?case by (subst natsum_Suc2) simp + qed + } + then show "coeff (p * q) n = coeff (q * p) n" + by simp + qed + + show "p - q = p + (-q)" + by (simp add: up_minus_def) + show "inverse p = (if p dvd 1 then THE x. p*x = 1 else 0)" + by (simp add: up_inverse_def) + show "p / q = p * inverse q" + by (simp add: up_divide_def) + show "p ^ n = nat_rec 1 (%u b. b * p) n" + by (simp add: up_power_def) + qed + +(* Further properties of monom *) + +lemma monom_zero [simp]: + "monom 0 n = 0" + by (simp add: monom_def up_zero_def) + +lemma monom_mult_is_smult: + "monom (a::'a::ring) 0 * p = a *s p" +proof (rule up_eqI) + fix k + show "coeff (monom a 0 * p) k = coeff (a *s p) k" + proof (cases k) + case 0 then show ?thesis by simp + next + case Suc then show ?thesis by simp + qed +qed + +lemma monom_add [simp]: + "monom (a + b) n = monom (a::'a::ring) n + monom b n" +by (rule up_eqI) simp + +lemma monom_mult_smult: + "monom (a * b) n = a *s monom (b::'a::ring) n" +by (rule up_eqI) simp + +lemma monom_uminus [simp]: + "monom (-a) n = - monom (a::'a::ring) n" +by (rule up_eqI) simp + +lemma monom_one [simp]: + "monom 1 0 = 1" +by (simp add: up_one_def) + +lemma monom_inj: + "(monom a n = monom b n) = (a = b)" +proof + assume "monom a n = monom b n" + then have "coeff (monom a n) n = coeff (monom b n) n" by simp + then show "a = b" by simp +next + assume "a = b" then show "monom a n = monom b n" by simp +qed + +(* Properties of *s: + Polynomials form a module *) + +lemma smult_l_distr: + "(a + b::'a::ring) *s p = a *s p + b *s p" +by (rule up_eqI) simp + +lemma smult_r_distr: + "(a::'a::ring) *s (p + q) = a *s p + a *s q" +by (rule up_eqI) simp + +lemma smult_assoc1: + "(a * b::'a::ring) *s p = a *s (b *s p)" +by (rule up_eqI) simp + +lemma smult_one [simp]: + "(1::'a::ring) *s p = p" +by (rule up_eqI) simp + +(* Polynomials form an algebra *) + +ML_setup {* Delsimprocs [ring_simproc] *} + +lemma smult_assoc2: + "(a *s p) * q = (a::'a::ring) *s (p * q)" +by (rule up_eqI) (simp add: natsum_rdistr m_assoc) +(* Simproc fails. *) + +ML_setup {* Addsimprocs [ring_simproc] *} + +(* the following can be derived from the above ones, + for generality reasons, it is therefore done *) + +lemma smult_l_null [simp]: + "(0::'a::ring) *s p = 0" +proof - + fix a + have "0 *s p = (0 *s p + a *s p) + - (a *s p)" by simp + also have "... = (0 + a) *s p + - (a *s p)" by (simp only: smult_l_distr) + also have "... = 0" by simp + finally show ?thesis . +qed + +lemma smult_r_null [simp]: + "(a::'a::ring) *s 0 = 0"; +proof - + fix p + have "a *s 0 = (a *s 0 + a *s p) + - (a *s p)" by simp + also have "... = a *s (0 + p) + - (a *s p)" by (simp only: smult_r_distr) + also have "... = 0" by simp + finally show ?thesis . +qed + +lemma smult_l_minus: + "(-a::'a::ring) *s p = - (a *s p)" +proof - + have "(-a) *s p = (-a *s p + a *s p) + -(a *s p)" by simp + also have "... = (-a + a) *s p + -(a *s p)" by (simp only: smult_l_distr) + also have "... = -(a *s p)" by simp + finally show ?thesis . +qed + +lemma smult_r_minus: + "(a::'a::ring) *s (-p) = - (a *s p)" +proof - + have "a *s (-p) = (a *s -p + a *s p) + -(a *s p)" by simp + also have "... = a *s (-p + p) + -(a *s p)" by (simp only: smult_r_distr) + also have "... = -(a *s p)" by simp + finally show ?thesis . +qed + +section {* The degree function *} - up_zero_def "0 == Abs_UP (%x. 0)" - up_one_def "<1> == monom 0" - up_uminus_def "- p == (-<1>) *s p" - up_inverse_def "inverse (a::'a::ringS up) == (if a dvd <1> then @x. a*x = <1> else 0)" - up_divide_def "(a::'a::ringS up) / b == a * inverse b" - up_power_def "a ^ n == nat_rec (<1>::('a::ringS) up) (%u b. b * a) n" -end +constdefs + deg :: "('a::zero) up => nat" + "deg p == LEAST n. bound n (coeff p)" + +lemma deg_aboveI: + "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n" +by (unfold deg_def) (fast intro: Least_le) + +lemma deg_aboveD: + assumes prem: "deg p < m" shows "coeff p m = 0" +proof - + obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain) + then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI) + then show "coeff p m = 0" by (rule boundD) +qed + +lemma deg_belowI: + assumes prem: "n ~= 0 ==> coeff p n ~= 0" shows "n <= deg p" +(* logically, this is a slightly stronger version of deg_aboveD *) +proof (cases "n=0") + case True then show ?thesis by simp +next + case False then have "coeff p n ~= 0" by (rule prem) + then have "~ deg p < n" by (fast dest: deg_aboveD) + then show ?thesis by arith +qed + +lemma lcoeff_nonzero_deg: + assumes deg: "deg p ~= 0" shows "coeff p (deg p) ~= 0" +proof - + obtain m where "deg p <= m" and m_coeff: "coeff p m ~= 0" + proof - + have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)" + by arith (* make public?, why does proof not work with "1" *) + from deg have "deg p - 1 < (LEAST n. bound n (coeff p))" + by (unfold deg_def) arith + then have "~ bound (deg p - 1) (coeff p)" by (rule not_less_Least) + then have "EX m. deg p - 1 < m & coeff p m ~= 0" + by (unfold bound_def) fast + then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus) + then show ?thesis by auto + qed + with deg_belowI have "deg p = m" by fastsimp + with m_coeff show ?thesis by simp +qed + +lemma lcoeff_nonzero_nonzero: + assumes deg: "deg p = 0" and nonzero: "p ~= 0" shows "coeff p 0 ~= 0" +proof - + have "EX m. coeff p m ~= 0" + proof (rule classical) + assume "~ ?thesis" + then have "p = 0" by (auto intro: up_eqI) + with nonzero show ?thesis by contradiction + qed + then obtain m where coeff: "coeff p m ~= 0" .. + then have "m <= deg p" by (rule deg_belowI) + then have "m = 0" by (simp add: deg) + with coeff show ?thesis by simp +qed + +lemma lcoeff_nonzero: + "p ~= 0 ==> coeff p (deg p) ~= 0" +proof (cases "deg p = 0") + case True + assume "p ~= 0" + with True show ?thesis by (simp add: lcoeff_nonzero_nonzero) +next + case False + assume "p ~= 0" + with False show ?thesis by (simp add: lcoeff_nonzero_deg) +qed + +lemma deg_eqI: + "[| !!m. n < m ==> coeff p m = 0; + !!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n" +by (fast intro: le_anti_sym deg_aboveI deg_belowI) + +(* Degree and polynomial operations *) + +lemma deg_add [simp]: + "deg ((p::'a::ring up) + q) <= max (deg p) (deg q)" +proof (cases "deg p <= deg q") + case True show ?thesis by (rule deg_aboveI) (simp add: True deg_aboveD) +next + case False show ?thesis by (rule deg_aboveI) (simp add: False deg_aboveD) +qed + +lemma deg_monom_ring: + "deg (monom a n::'a::ring up) <= n" +by (rule deg_aboveI) simp + +lemma deg_monom [simp]: + "a ~= 0 ==> deg (monom a n::'a::ring up) = n" +by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI) + +lemma deg_const [simp]: + "deg (monom (a::'a::ring) 0) = 0" +proof (rule le_anti_sym) + show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp +next + show "0 <= deg (monom a 0)" by (rule deg_belowI) simp +qed + +lemma deg_zero [simp]: + "deg 0 = 0" +proof (rule le_anti_sym) + show "deg 0 <= 0" by (rule deg_aboveI) simp +next + show "0 <= deg 0" by (rule deg_belowI) simp +qed + +lemma deg_one [simp]: + "deg 1 = 0" +proof (rule le_anti_sym) + show "deg 1 <= 0" by (rule deg_aboveI) simp +next + show "0 <= deg 1" by (rule deg_belowI) simp +qed + +lemma uminus_monom: + "!!a::'a::ring. (-a = 0) = (a = 0)" +proof + fix a::"'a::ring" + assume "a = 0" + then show "-a = 0" by simp +next + fix a::"'a::ring" + assume "- a = 0" + then have "-(- a) = 0" by simp + then show "a = 0" by simp +qed + +lemma deg_uminus [simp]: + "deg (-p::('a::ring) up) = deg p" +proof (rule le_anti_sym) + show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD) +next + show "deg p <= deg (- p)" + by (simp add: deg_belowI lcoeff_nonzero_deg uminus_monom) +qed + +lemma deg_smult_ring: + "deg ((a::'a::ring) *s p) <= (if a = 0 then 0 else deg p)" +proof (cases "a = 0") +qed (simp add: deg_aboveI deg_aboveD)+ + +lemma deg_smult [simp]: + "deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)" +proof (rule le_anti_sym) + show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring) +next + show "(if a = 0 then 0 else deg p) <= deg (a *s p)" + proof (cases "a = 0") + qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff) +qed +lemma deg_mult_ring: + "deg (p * q::'a::ring up) <= deg p + deg q" +proof (rule deg_aboveI) + fix m + assume boundm: "deg p + deg q < m" + { + fix k i + assume boundk: "deg p + deg q < k" + then have "coeff p i * coeff q (k - i) = 0" + proof (cases "deg p < i") + case True then show ?thesis by (simp add: deg_aboveD) + next + case False with boundk have "deg q < k - i" by arith + then show ?thesis by (simp add: deg_aboveD) + qed + } + (* This is similar to bound_mult_zero and deg_above_mult_zero in the old + proofs. *) + with boundm show "coeff (p * q) m = 0" by simp +qed +lemma deg_mult [simp]: + "[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q" +proof (rule le_anti_sym) + show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring) +next + let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))" + assume nz: "p ~= 0" "q ~= 0" + have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith + show "deg p + deg q <= deg (p * q)" + proof (rule deg_belowI, simp) + have "setsum ?s {.. deg p + deg q} + = setsum ?s ({.. deg p(} Un {deg p .. deg p + deg q})" + by (simp only: ivl_disj_un_one) + also have "... = setsum ?s {deg p .. deg p + deg q}" + by (simp add: setsum_Un_disjoint ivl_disj_int_one + setsum_0 deg_aboveD less_add_diff) + also have "... = setsum ?s ({deg p} Un {)deg p .. deg p + deg q})" + by (simp only: ivl_disj_un_singleton) + also have "... = coeff p (deg p) * coeff q (deg q)" + by (simp add: setsum_Un_disjoint ivl_disj_int_singleton + setsum_0 deg_aboveD) + finally have "setsum ?s {.. deg p + deg q} + = coeff p (deg p) * coeff q (deg q)" . + with nz show "setsum ?s {.. deg p + deg q} ~= 0" + by (simp add: integral_iff lcoeff_nonzero) + qed + qed + +lemma coeff_natsum: + "((coeff (setsum p A) k)::'a::ring) = + setsum (%i. coeff (p i) k) A" +proof (cases "finite A") + case True then show ?thesis by induct auto +next + case False then show ?thesis by (simp add: setsum_def) +qed +(* Instance of a more general result!!! *) + +(* +lemma coeff_natsum: + "((coeff (setsum p {..n::nat}) k)::'a::ring) = + setsum (%i. coeff (p i) k) {..n}" +by (induct n) auto +*) + +lemma up_repr: + "setsum (%i. monom (coeff p i) i) {..deg (p::'a::ring up)} = p" +proof (rule up_eqI) + let ?s = "(%i. monom (coeff p i) i)" + fix k + show "coeff (setsum ?s {..deg p}) k = coeff p k" + proof (cases "k <= deg p") + case True + hence "coeff (setsum ?s {..deg p}) k = + coeff (setsum ?s ({..k} Un {)k..deg p})) k" + by (simp only: ivl_disj_un_one) + also from True + have "... = coeff (setsum ?s {..k}) k" + by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2 + setsum_0 coeff_natsum ) + also + have "... = coeff (setsum ?s ({..k(} Un {k})) k" + by (simp only: ivl_disj_un_singleton) + also have "... = coeff p k" + by (simp add: setsum_Un_disjoint ivl_disj_int_singleton + setsum_0 coeff_natsum deg_aboveD) + finally show ?thesis . + next + case False + hence "coeff (setsum ?s {..deg p}) k = + coeff (setsum ?s ({..deg p(} Un {deg p})) k" + by (simp only: ivl_disj_un_singleton) + also from False have "... = coeff p k" + by (simp add: setsum_Un_disjoint ivl_disj_int_singleton + setsum_0 coeff_natsum deg_aboveD) + finally show ?thesis . + qed +qed + +lemma up_repr_le: + "deg (p::'a::ring up) <= n ==> setsum (%i. monom (coeff p i) i) {..n} = p" +proof - + let ?s = "(%i. monom (coeff p i) i)" + assume "deg p <= n" + then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {)deg p..n})" + by (simp only: ivl_disj_un_one) + also have "... = setsum ?s {..deg p}" + by (simp add: setsum_Un_disjoint ivl_disj_int_one + setsum_0 deg_aboveD) + also have "... = p" by (rule up_repr) + finally show ?thesis . +qed + +instance up :: ("domain") "domain" +proof + show "1 ~= (0::'a up)" + proof (* notI is applied here *) + assume "1 = (0::'a up)" + hence "coeff 1 0 = (coeff 0 0::'a)" by simp + hence "1 = (0::'a)" by simp + with one_not_zero show "False" by contradiction + qed +next + fix p q :: "'a::domain up" + assume pq: "p * q = 0" + show "p = 0 | q = 0" + proof (rule classical) + assume c: "~ (p = 0 | q = 0)" + then have "deg p + deg q = deg (p * q)" by simp + also from pq have "... = 0" by simp + finally have "deg p + deg q = 0" . + then have f1: "deg p = 0 & deg q = 0" by simp + from f1 have "p = setsum (%i. (monom (coeff p i) i)) {..0}" + by (simp only: up_repr_le) + also have "... = monom (coeff p 0) 0" by simp + finally have p: "p = monom (coeff p 0) 0" . + from f1 have "q = setsum (%i. (monom (coeff q i) i)) {..0}" + by (simp only: up_repr_le) + also have "... = monom (coeff q 0) 0" by simp + finally have q: "q = monom (coeff q 0) 0" . + have "coeff p 0 * coeff q 0 = coeff (p * q) 0" by simp + also from pq have "... = 0" by simp + finally have "coeff p 0 * coeff q 0 = 0" . + then have "coeff p 0 = 0 | coeff q 0 = 0" by (simp only: integral_iff) + with p q show "p = 0 | q = 0" by fastsimp + qed +qed + +lemma monom_inj_zero: + "(monom a n = 0) = (a = 0)" +proof - + have "(monom a n = 0) = (monom a n = monom 0 n)" by simp + also have "... = (a = 0)" by (simp add: monom_inj del: monom_zero) + finally show ?thesis . +qed + +lemma smult_integral: + "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0" +by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) fast + +end \ No newline at end of file diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/Finite_Set.thy Thu Nov 28 10:50:42 2002 +0100 @@ -273,6 +273,22 @@ lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}" by (induct k) (simp_all add: atMost_Suc) +lemma finite_greaterThanLessThan [iff]: + fixes l :: nat shows "finite {)l..u(}" +by (simp add: greaterThanLessThan_def) + +lemma finite_atLeastLessThan [iff]: + fixes l :: nat shows "finite {l..u(}" +by (simp add: atLeastLessThan_def) + +lemma finite_greaterThanAtMost [iff]: + fixes l :: nat shows "finite {)l..u}" +by (simp add: greaterThanAtMost_def) + +lemma finite_atLeastAtMost [iff]: + fixes l :: nat shows "finite {l..u}" +by (simp add: atLeastAtMost_def) + lemma bounded_nat_set_is_finite: "(ALL i:N. i < (n::nat)) ==> finite N" -- {* A bounded set of natural numbers is finite. *} diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/IsaMakefile Thu Nov 28 10:50:42 2002 +0100 @@ -78,7 +78,8 @@ $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/induct_method.ML \ $(SRC)/Provers/make_elim.ML $(SRC)/Provers/simplifier.ML \ - $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \ + $(SRC)/Provers/splitter.ML $(SRC)/Provers/linorder.ML \ + $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \ $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \ $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \ Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides_lemmas.ML \ @@ -341,16 +342,13 @@ Algebra/abstract/Factor.ML Algebra/abstract/Factor.thy \ Algebra/abstract/Field.thy \ Algebra/abstract/Ideal.ML Algebra/abstract/Ideal.thy \ - Algebra/abstract/NatSum.ML Algebra/abstract/NatSum.thy \ Algebra/abstract/PID.thy \ Algebra/abstract/Ring.ML Algebra/abstract/Ring.thy \ Algebra/abstract/RingHomo.ML Algebra/abstract/RingHomo.thy\ - Algebra/poly/Degree.ML Algebra/poly/Degree.thy \ + Algebra/abstract/order.ML \ Algebra/poly/LongDiv.ML Algebra/poly/LongDiv.thy \ Algebra/poly/PolyHomo.ML Algebra/poly/PolyHomo.thy \ - Algebra/poly/PolyRing.ML Algebra/poly/PolyRing.thy \ Algebra/poly/Polynomial.thy \ - Algebra/poly/ProtoPoly.ML Algebra/poly/ProtoPoly.thy \ Algebra/poly/UnivPoly.ML Algebra/poly/UnivPoly.thy @$(ISATOOL) usedir $(OUT)/HOL Algebra diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/ROOT.ML --- a/src/HOL/ROOT.ML Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/ROOT.ML Thu Nov 28 10:50:42 2002 +0100 @@ -35,6 +35,7 @@ use "~~/src/Provers/Arith/cancel_numeral_factor.ML"; use "~~/src/Provers/Arith/extract_common_term.ML"; use "~~/src/Provers/Arith/cancel_div_mod.ML"; +use "~~/src/Provers/linorder.ML"; with_path "Integ" use_thy "Main"; diff -r 50dcee1c509e -r 7de9342aca7a src/HOL/SetInterval.ML --- a/src/HOL/SetInterval.ML Wed Nov 27 17:25:41 2002 +0100 +++ b/src/HOL/SetInterval.ML Thu Nov 28 10:50:42 2002 +0100 @@ -1,137 +1,51 @@ (* Title: HOL/SetInterval.ML ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TU Muenchen - -Set Intervals: lessThan, greaterThan, atLeast, atMost + Author: Clemens Ballarin + Copyright 2002 TU Muenchen *) - -(*** lessThan ***) - -Goalw [lessThan_def] "(i: lessThan k) = (i 'a set" ("(1{.._'(})") @@ -21,4 +21,320 @@ atLeast :: "('a::ord) => 'a set" ("(1{_..})") "{l..} == {x. l<=x}" + greaterThanLessThan :: "['a::ord, 'a] => 'a set" ("(1{')_.._'(})") + "{)l..u(} == {)l..} Int {..u(}" + + atLeastLessThan :: "['a::ord, 'a] => 'a set" ("(1{_.._'(})") + "{l..u(} == {l..} Int {..u(}" + + greaterThanAtMost :: "['a::ord, 'a] => 'a set" ("(1{')_.._})") + "{)l..u} == {)l..} Int {..u}" + + atLeastAtMost :: "['a::ord, 'a] => 'a set" ("(1{_.._})") + "{l..u} == {l..} Int {..u}" + +(* Setup of transitivity reasoner *) + +ML {* + +structure Trans_Tac = Trans_Tac_Fun ( + struct + val less_reflE = thm "order_less_irrefl" RS thm "notE"; + val le_refl = thm "order_refl"; + val less_imp_le = thm "order_less_imp_le"; + val not_lessI = thm "linorder_not_less" RS thm "iffD2"; + val not_leI = thm "linorder_not_less" RS thm "iffD2"; + val not_lessD = thm "linorder_not_less" RS thm "iffD1"; + val not_leD = thm "linorder_not_le" RS thm "iffD1"; + val eqI = thm "order_antisym"; + val eqD1 = thm "order_eq_refl"; + val eqD2 = thm "sym" RS thm "order_eq_refl"; + val less_trans = thm "order_less_trans"; + val less_le_trans = thm "order_less_le_trans"; + val le_less_trans = thm "order_le_less_trans"; + val le_trans = thm "order_trans"; + fun decomp (Trueprop $ t) = + let fun dec (Const ("Not", _) $ t) = ( + case dec t of + None => None + | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2)) + | dec (Const (rel, _) $ t1 $ t2) = + Some (t1, implode (drop (3, explode rel)), t2) + | dec _ = None + in dec t end + | decomp _ = None + end); + +val trans_tac = Trans_Tac.trans_tac; + +*} + +method_setup trans = + {* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (trans_tac)) *} + {* simple transitivity reasoner *} + +(*** lessThan ***) + +lemma lessThan_iff: "(i: lessThan k) = (i {l} Un {)l..u(} = {l..u(}" + "(l::'a::linorder) < u ==> {)l..u(} Un {u} = {)l..u}" + "(l::'a::linorder) <= u ==> {l} Un {)l..u} = {l..u}" + "(l::'a::linorder) <= u ==> {l..u(} Un {u} = {l..u}" +by auto (elim linorder_neqE | trans+)+ + +(* One- and two-sided intervals *) + +lemma ivl_disj_un_one: + "(l::'a::linorder) < u ==> {..l} Un {)l..u(} = {..u(}" + "(l::'a::linorder) <= u ==> {..l(} Un {l..u(} = {..u(}" + "(l::'a::linorder) <= u ==> {..l} Un {)l..u} = {..u}" + "(l::'a::linorder) <= u ==> {..l(} Un {l..u} = {..u}" + "(l::'a::linorder) <= u ==> {)l..u} Un {)u..} = {)l..}" + "(l::'a::linorder) < u ==> {)l..u(} Un {u..} = {)l..}" + "(l::'a::linorder) <= u ==> {l..u} Un {)u..} = {l..}" + "(l::'a::linorder) <= u ==> {l..u(} Un {u..} = {l..}" +by auto trans+ + +(* Two- and two-sided intervals *) + +lemma ivl_disj_un_two: + "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u(} = {)l..u(}" + "[| (l::'a::linorder) <= m; m < u |] ==> {)l..m} Un {)m..u(} = {)l..u(}" + "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u(} = {l..u(}" + "[| (l::'a::linorder) <= m; m < u |] ==> {l..m} Un {)m..u(} = {l..u(}" + "[| (l::'a::linorder) < m; m <= u |] ==> {)l..m(} Un {m..u} = {)l..u}" + "[| (l::'a::linorder) <= m; m <= u |] ==> {)l..m} Un {)m..u} = {)l..u}" + "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m(} Un {m..u} = {l..u}" + "[| (l::'a::linorder) <= m; m <= u |] ==> {l..m} Un {)m..u} = {l..u}" +by auto trans+ + +lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two + +(** Disjoint Intersections **) + +(* Singletons and open intervals *) + +lemma ivl_disj_int_singleton: + "{l::'a::order} Int {)l..} = {}" + "{..u(} Int {u} = {}" + "{l} Int {)l..u(} = {}" + "{)l..u(} Int {u} = {}" + "{l} Int {)l..u} = {}" + "{l..u(} Int {u} = {}" + by simp+ + +(* One- and two-sided intervals *) + +lemma ivl_disj_int_one: + "{..l::'a::order} Int {)l..u(} = {}" + "{..l(} Int {l..u(} = {}" + "{..l} Int {)l..u} = {}" + "{..l(} Int {l..u} = {}" + "{)l..u} Int {)u..} = {}" + "{)l..u(} Int {u..} = {}" + "{l..u} Int {)u..} = {}" + "{l..u(} Int {u..} = {}" + by auto trans+ + +(* Two- and two-sided intervals *) + +lemma ivl_disj_int_two: + "{)l::'a::order..m(} Int {m..u(} = {}" + "{)l..m} Int {)m..u(} = {}" + "{l..m(} Int {m..u(} = {}" + "{l..m} Int {)m..u(} = {}" + "{)l..m(} Int {m..u} = {}" + "{)l..m} Int {)m..u} = {}" + "{l..m(} Int {m..u} = {}" + "{l..m} Int {)m..u} = {}" + by auto trans+ + +lemmas ivl_disj_int = ivl_disj_int_singleton ivl_disj_int_one ivl_disj_int_two + end diff -r 50dcee1c509e -r 7de9342aca7a src/Provers/README --- a/src/Provers/README Wed Nov 27 17:25:41 2002 +0100 +++ b/src/Provers/README Thu Nov 28 10:50:42 2002 +0100 @@ -16,6 +16,7 @@ simplifier.ML fast simplifier split_paired_all.ML turn surjective pairing into split rule splitter.ML performs case splits for simplifier.ML + trans.ML transitivity reasoner for linear (total) orders typedsimp.ML basic simplifier for explicitly typed logics directory Arith: diff -r 50dcee1c509e -r 7de9342aca7a src/Provers/linorder.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Provers/linorder.ML Thu Nov 28 10:50:42 2002 +0100 @@ -0,0 +1,214 @@ +(* + Title: Transitivity reasoner for linear orders + Id: $Id$ + Author: Clemens Ballarin, started 8 November 2002 + Copyright: TU Muenchen +*) + +(*** +This is a very simple package for transitivity reasoning over linear orders. +Simple means exponential time (and space) in the number of premises. +Should be replaced by a graph-theoretic algorithm. + +The package provides a tactic trans_tac that uses all premises of the form + + t = u, t < u, t <= u, ~(t < u) and ~(t <= u) + +to +1. either derive a contradiction, + in which case the conclusion can be any term, +2. or prove the conclusion, which must be of the same form as the premises. + +To get rid of ~= in the premises, it is advisable to use an elimination +rule of the form + + [| t ~= u; t < u ==> P; u < t ==> P |] ==> P. + +The package is implemented as an ML functor and thus not limited to the +relation <= and friends. It can be instantiated to any total order --- +for example, the divisibility relation "dvd". +***) + +(*** Credits *** + +This package is closely based on a (no longer used) transitivity reasoner for +the natural numbers, which was written by Tobias Nipkow. + +****************) + +signature LESS_ARITH = +sig + val less_reflE: thm (* x < x ==> P *) + val le_refl: thm (* x <= x *) + val less_imp_le: thm (* x <= y ==> x < y *) + val not_lessI: thm (* y <= x ==> ~(x < y) *) + val not_leI: thm (* y < x ==> ~(x <= y) *) + val not_lessD: thm (* ~(x < y) ==> y <= x *) + val not_leD: thm (* ~(x <= y) ==> y < x *) + val eqI: thm (* [| x <= y; y <= x |] ==> x = y *) + val eqD1: thm (* x = y ==> x <= y *) + val eqD2: thm (* x = y ==> y <= x *) + val less_trans: thm (* [| x <= y; y <= z |] ==> x <= z *) + val less_le_trans: thm (* [| x <= y; y < z |] ==> x < z *) + val le_less_trans: thm (* [| x < y; y <= z |] ==> x < z *) + val le_trans: thm (* [| x < y; y < z |] ==> x < z *) + val decomp: term -> (term * string * term) option + (* decomp (`x Rel y') should yield (x, Rel, y) + where Rel is one of "<", "<=", "~<", "~<=", "=" and "~=" + other relation symbols are ignored *) +end; + +signature TRANS_TAC = +sig + val trans_tac: int -> tactic +end; + +functor Trans_Tac_Fun (Less: LESS_ARITH): TRANS_TAC = +struct + +(*** Proof objects ***) + +datatype proof + = Asm of int + | Thm of proof list * thm; + +(* Turn proof objects into theorems *) + +fun prove asms = + let fun pr (Asm i) = nth_elem (i, asms) + | pr (Thm (prfs, thm)) = (map pr prfs) MRS thm + in pr end; + +(*** Exceptions ***) + +exception Contr of proof; (* Raised when contradiction is found *) + +exception Cannot; (* Raised when goal cannot be proved *) + +(*** Internal representation of inequalities ***) + +datatype less + = Less of term * term * proof + | Le of term * term * proof; + +fun lower (Less (x, _, _)) = x + | lower (Le (x, _, _)) = x; + +fun upper (Less (_, y, _)) = y + | upper (Le (_, y, _)) = y; + +infix subsumes; + +fun (Less (x, y, _)) subsumes (Le (x', y', _)) = (x = x' andalso y = y') + | (Less (x, y, _)) subsumes (Less (x', y', _)) = (x = x' andalso y = y') + | (Le (x, y, _)) subsumes (Le (x', y', _)) = (x = x' andalso y = y') + | _ subsumes _ = false; + +fun trivial (Le (x, x', _)) = (x = x') + | trivial _ = false; + +(*** Transitive closure ***) + +fun add new = + let fun adds([], news) = new::news + | adds(old::olds, news) = if new subsumes old then adds(olds, news) + else adds(olds, old::news) + in adds end; + +fun ctest (less as Less (x, x', p)) = + if x = x' then raise Contr (Thm ([p], Less.less_reflE)) + else less + | ctest less = less; + +fun mktrans (Less (x, _, p), Less (_, z, q)) = + Less (x, z, Thm([p, q], Less.less_trans)) + | mktrans (Less (x, _, p), Le (_, z, q)) = + Less (x, z, Thm([p, q], Less.less_le_trans)) + | mktrans (Le (x, _, p), Less (_, z, q)) = + Less (x, z, Thm([p, q], Less.le_less_trans)) + | mktrans (Le (x, _, p), Le (_, z, q)) = + Le (x, z, Thm([p, q], Less.le_trans)); + +fun trans new olds = + let fun tr (news, old) = + if upper old = lower new then mktrans (old, new)::news + else if upper new = lower old then mktrans (new, old)::news + else news + in foldl tr ([], olds) end; + +fun close1 olds new = + if trivial new orelse exists (fn old => old subsumes new) olds then olds + else let val news = trans new olds + in close (add new (olds, [])) news end +and close olds [] = olds + | close olds (new::news) = close (close1 olds (ctest new)) news; + +(*** Solving and proving goals ***) + +(* Recognise and solve trivial goal *) + +fun triv_sol (Le (x, x', _)) = + if x = x' then Some (Thm ([], Less.le_refl)) + else None + | triv_sol _ = None; + +(* Solve less starting from facts *) + +fun solve facts less = + case triv_sol less of + None => (case (Library.find_first (fn fact => fact subsumes less) facts, less) of + (None, _) => raise Cannot + | (Some (Less (_, _, p)), Less _) => p + | (Some (Le (_, _, p)), Less _) => + error "trans_tac/solve: internal error: le cannot subsume less" + | (Some (Less (_, _, p)), Le _) => Thm ([p], Less.less_imp_le) + | (Some (Le (_, _, p)), Le _) => p) + | Some prf => prf; + +(* Turn term t into Less or Le; n is position of t in list of assumptions *) + +fun mkasm (t, n) = + case Less.decomp t of + Some (x, rel, y) => (case rel of + "<" => [Less (x, y, Asm n)] + | "~<" => [Le (y, x, Thm ([Asm n], Less.not_lessD))] + | "<=" => [Le (x, y, Asm n)] + | "~<=" => [Less (y, x, Thm ([Asm n], Less.not_leD))] + | "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)), + Le (x, y, Thm ([Asm n], Less.eqD1))] + | "~=" => [] + | _ => error ("trans_tac/mkasm: unknown relation " ^ rel)) + | None => []; + +(* Turn goal t into a pair (goals, proof) where goals is a list of + Le/Less-subgoals to solve, and proof the validation that proves the concl t + Asm ~1 is dummy (denotes a goal) +*) + +fun mkconcl t = + case Less.decomp t of + Some (x, rel, y) => (case rel of + "<" => ([Less (x, y, Asm ~1)], Asm 0) + | "~<" => ([Le (y, x, Asm ~1)], Thm ([Asm 0], Less.not_lessI)) + | "<=" => ([Le (x, y, Asm ~1)], Asm 0) + | "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], Less.not_leI)) + | "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)], + Thm ([Asm 0, Asm 1], Less.eqI)) + | _ => raise Cannot) + | None => raise Cannot; + +val trans_tac = SUBGOAL (fn (A, n) => + let val Hs = Logic.strip_assums_hyp A + val C = Logic.strip_assums_concl A + val lesss = flat (ListPair.map mkasm (Hs, 0 upto (length Hs - 1))) + val clesss = close [] lesss + val (subgoals, prf) = mkconcl C + val prfs = map (solve clesss) subgoals + in METAHYPS (fn asms => + let val thms = map (prove asms) prfs + in rtac (prove thms prf) 1 end) n + end + handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n + | Cannot => no_tac); + +end;