equal
deleted
inserted
replaced
15 lemma lemma_complex_mult_inverse_squared [simp]: |
15 lemma lemma_complex_mult_inverse_squared [simp]: |
16 "x \<noteq> (0::complex) \<Longrightarrow> (x * inverse(x) ^ 2) = inverse x" |
16 "x \<noteq> (0::complex) \<Longrightarrow> (x * inverse(x) ^ 2) = inverse x" |
17 by (simp add: numeral_2_eq_2) |
17 by (simp add: numeral_2_eq_2) |
18 |
18 |
19 text{*Changing the quantified variable. Install earlier?*} |
19 text{*Changing the quantified variable. Install earlier?*} |
20 lemma all_shift: "(\<forall>x::'a::ring. P x) = (\<forall>x. P (x-a))"; |
20 lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))"; |
21 apply auto |
21 apply auto |
22 apply (drule_tac x="x+a" in spec) |
22 apply (drule_tac x="x+a" in spec) |
23 apply (simp add: diff_minus add_assoc) |
23 apply (simp add: diff_minus add_assoc) |
24 done |
24 done |
25 |
25 |