# HG changeset patch # User haftmann # Date 1242826522 -7200 # Node ID 052fddd640066736c65f4d6bf41762eefecf07bf # Parent b67179528acddfd2e1a9dc9b409d8cb9c6fe6523# Parent 3dde56615750825b2ab64aad024ec8c1417ba418 merged diff -r b67179528acd -r 052fddd64006 src/HOL/Bali/Example.thy --- a/src/HOL/Bali/Example.thy Wed May 20 15:35:13 2009 +0200 +++ b/src/HOL/Bali/Example.thy Wed May 20 15:35:22 2009 +0200 @@ -1075,7 +1075,7 @@ lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \name=foo,parTs=[NT]\ = {((ClassT Base, \access=Public,static=False,pars=[z],resT=Class Base\) , [Class Base])}" -by (simp (no_asm) add: max_spec_def appl_methds_Base_foo) +by (simp add: max_spec_def appl_methds_Base_foo Collect_conv_if) section "well-typedness" diff -r b67179528acd -r 052fddd64006 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Wed May 20 15:35:13 2009 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Wed May 20 15:35:22 2009 +0200 @@ -2102,6 +2102,80 @@ ultimately show ?thesis by (cases n, auto) qed +lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)" + by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_negf[symmetric]) + +lemma fps_compose_sub_distrib: + shows "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)" + unfolding diff_minus fps_compose_uminus fps_compose_add_distrib .. + +lemma X_fps_compose:"X oo a = Abs_fps (\n. if n = 0 then (0::'a::comm_ring_1) else a$n)" + by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta power_Suc) + +lemma fps_inverse_compose: + assumes b0: "(b$0 :: 'a::field) = 0" and a0: "a$0 \ 0" + shows "inverse a oo b = inverse (a oo b)" +proof- + let ?ia = "inverse a" + let ?ab = "a oo b" + let ?iab = "inverse ?ab" + +from a0 have ia0: "?ia $ 0 \ 0" by (simp ) +from a0 have ab0: "?ab $ 0 \ 0" by (simp add: fps_compose_def) +thm inverse_mult_eq_1[OF ab0] +have "(?ia oo b) * (a oo b) = 1" +unfolding fps_compose_mult_distrib[OF b0, symmetric] +unfolding inverse_mult_eq_1[OF a0] +fps_compose_1 .. + +then have "(?ia oo b) * (a oo b) * ?iab = 1 * ?iab" by simp +then have "(?ia oo b) * (?iab * (a oo b)) = ?iab" by simp +then show ?thesis + unfolding inverse_mult_eq_1[OF ab0] by simp +qed + +lemma fps_divide_compose: + assumes c0: "(c$0 :: 'a::field) = 0" and b0: "b$0 \ 0" + shows "(a/b) oo c = (a oo c) / (b oo c)" + unfolding fps_divide_def fps_compose_mult_distrib[OF c0] + fps_inverse_compose[OF c0 b0] .. + +lemma gp: assumes a0: "a$0 = (0::'a::field)" + shows "(Abs_fps (\n. 1)) oo a = 1/(1 - a)" (is "?one oo a = _") +proof- + have o0: "?one $ 0 \ 0" by simp + have th0: "(1 - X) $ 0 \ (0::'a)" by simp + from fps_inverse_gp[where ?'a = 'a] + have "inverse ?one = 1 - X" by (simp add: fps_eq_iff) + hence "inverse (inverse ?one) = inverse (1 - X)" by simp + hence th: "?one = 1/(1 - X)" unfolding fps_inverse_idempotent[OF o0] + by (simp add: fps_divide_def) + show ?thesis unfolding th + unfolding fps_divide_compose[OF a0 th0] + fps_compose_1 fps_compose_sub_distrib X_fps_compose_startby0[OF a0] .. +qed + +lemma fps_const_power[simp]: "fps_const (c::'a::ring_1) ^ n = fps_const (c^n)" +by (induct n, auto) + +lemma fps_compose_radical: + assumes b0: "b$0 = (0::'a::{field, ring_char_0})" + and ra0: "r (Suc k) (a$0) ^ Suc k = a$0" + and a0: "a$0 \ 0" + shows "fps_radical r (Suc k) a oo b = fps_radical r (Suc k) (a oo b)" +proof- + let ?r = "fps_radical r (Suc k)" + let ?ab = "a oo b" + have ab0: "?ab $ 0 = a$0" by (simp add: fps_compose_def) + from ab0 a0 ra0 have rab0: "?ab $ 0 \ 0" "r (Suc k) (?ab $ 0) ^ Suc k = ?ab $ 0" by simp_all + have th00: "r (Suc k) ((a oo b) $ 0) = (fps_radical r (Suc k) a oo b) $ 0" + by (simp add: ab0 fps_compose_def) + have th0: "(?r a oo b) ^ (Suc k) = a oo b" + unfolding fps_compose_power[OF b0] + unfolding iffD1[OF power_radical[of a r k], OF a0 ra0] .. + from iffD1[OF radical_unique[where r=r and k=k and b= ?ab and a = "?r a oo b", OF rab0(2) th00 rab0(1)], OF th0] show ?thesis . +qed + lemma fps_const_mult_apply_left: "fps_const c * (a oo b) = (fps_const c * a) oo b" by (simp add: fps_eq_iff fps_compose_nth setsum_right_distrib mult_assoc) @@ -2249,15 +2323,6 @@ lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::{field, ring_char_0})) = (fps_const a)^n * (E a)" by (induct n, auto simp add: power_Suc) -lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)" - by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_negf[symmetric]) - -lemma fps_compose_sub_distrib: - shows "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)" - unfolding diff_minus fps_compose_uminus fps_compose_add_distrib .. - -lemma X_fps_compose:"X oo a = Abs_fps (\n. if n = 0 then (0::'a::comm_ring_1) else a$n)" - by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta power_Suc) lemma X_compose_E[simp]: "X oo E (a::'a::{field}) = E a - 1" by (simp add: fps_eq_iff X_fps_compose) @@ -2301,6 +2366,7 @@ unfolding inverse_one_plus_X by (simp add: L_def fps_eq_iff power_Suc del: of_nat_Suc) + lemma L_nth: "L $ n = (- 1) ^ Suc n / of_nat n" by (simp add: L_def) diff -r b67179528acd -r 052fddd64006 src/HOL/Library/Pocklington.thy --- a/src/HOL/Library/Pocklington.thy Wed May 20 15:35:13 2009 +0200 +++ b/src/HOL/Library/Pocklington.thy Wed May 20 15:35:22 2009 +0200 @@ -382,8 +382,9 @@ (* Euler totient function. *) definition phi_def: "\ n = card { m. 0 < m \ m <= n \ coprime m n }" + lemma phi_0[simp]: "\ 0 = 0" - unfolding phi_def by (auto simp add: card_eq_0_iff) + unfolding phi_def by auto lemma phi_finite[simp]: "finite ({ m. 0 < m \ m <= n \ coprime m n })" proof- diff -r b67179528acd -r 052fddd64006 src/HOL/List.thy --- a/src/HOL/List.thy Wed May 20 15:35:13 2009 +0200 +++ b/src/HOL/List.thy Wed May 20 15:35:22 2009 +0200 @@ -2913,6 +2913,10 @@ "sorted (xs@ys) = (sorted xs & sorted ys & (\x \ set xs. \y \ set ys. x\y))" by (induct xs) (auto simp add:sorted_Cons) +lemma sorted_nth_mono: + "sorted xs \ i <= j \ j < length xs \ xs!i <= xs!j" +by (induct xs arbitrary: i j) (auto simp:nth_Cons' sorted_Cons) + lemma set_insort: "set(insort x xs) = insert x (set xs)" by (induct xs) auto diff -r b67179528acd -r 052fddd64006 src/HOL/MicroJava/BV/BVExample.thy --- a/src/HOL/MicroJava/BV/BVExample.thy Wed May 20 15:35:13 2009 +0200 +++ b/src/HOL/MicroJava/BV/BVExample.thy Wed May 20 15:35:22 2009 +0200 @@ -69,9 +69,9 @@ lemma subcls1: "subcls1 E = (\C D. (C, D) \ {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object), (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)})" -apply (simp add: subcls1_def2 del:singleton_conj_conv2) +apply (simp add: subcls1_def2) apply (simp add: name_defs class_defs system_defs E_def class_def) -apply (auto simp: expand_fun_eq split: split_if_asm) +apply (auto simp: expand_fun_eq) done text {* The subclass relation is acyclic; hence its converse is well founded: *} diff -r b67179528acd -r 052fddd64006 src/HOL/Set.thy --- a/src/HOL/Set.thy Wed May 20 15:35:13 2009 +0200 +++ b/src/HOL/Set.thy Wed May 20 15:35:22 2009 +0200 @@ -1036,11 +1036,16 @@ text{* Elimination of @{text"{x. \ & x=t & \}"}. *} -lemma singleton_conj_conv[simp]: "{x. x=a & P x} = (if P a then {a} else {})" +lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})" +by auto + +lemma Collect_conv_if2: "{x. a=x & P x} = (if P a then {a} else {})" by auto -lemma singleton_conj_conv2[simp]: "{x. a=x & P x} = (if P a then {a} else {})" -by auto +text {* +Simproc for pulling @{text "x=t"} in @{text "{x. \ & x=t & \}"} +to the front (and similarly for @{text "t=x"}): +*} ML{* local @@ -1054,7 +1059,6 @@ end; Addsimprocs [defColl_regroup]; - *} text {* diff -r b67179528acd -r 052fddd64006 src/Provers/quantifier1.ML --- a/src/Provers/quantifier1.ML Wed May 20 15:35:13 2009 +0200 +++ b/src/Provers/quantifier1.ML Wed May 20 15:35:22 2009 +0200 @@ -90,7 +90,7 @@ fun extract_conj fst xs t = case dest_conj t of NONE => NONE | SOME(conj,P,Q) => - (if not fst andalso def xs P then SOME(xs,P,Q) else + (if def xs P then (if fst then NONE else SOME(xs,P,Q)) else if def xs Q then SOME(xs,Q,P) else (case extract_conj false xs P of SOME(xs,eq,P') => SOME(xs,eq, conj $ P' $ Q) @@ -99,7 +99,7 @@ | NONE => NONE))); fun extract_imp fst xs t = case dest_imp t of NONE => NONE - | SOME(imp,P,Q) => if not fst andalso def xs P then SOME(xs,P,Q) + | SOME(imp,P,Q) => if def xs P then (if fst then NONE else SOME(xs,P,Q)) else (case extract_conj false xs P of SOME(xs,eq,P') => SOME(xs, eq, imp $ P' $ Q) | NONE => (case extract_imp false xs Q of