author wenzelm Fri, 25 Nov 2011 13:14:58 +0100 changeset 45630 0dd654a01217 parent 45629 ef08425dd2d5 child 45631 6bdf8b926f50
proper intro? declarations -- NB: elim? indexes on major premise, which is too flexible here and easily leads to inefficiences (cf. a0336f8b6558);
```--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Fri Nov 25 10:52:30 2011 +0100
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Fri Nov 25 13:14:58 2011 +0100
@@ -114,8 +114,8 @@
(-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
proof -
assume "a \<in> zOdd"
-  from QRLemma4 [OF this, symmetric] have
-    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" .
+  from QRLemma4 [OF this] have
+    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" ..
moreover have "0 \<le> int(card E)"
by auto
moreover have "0 \<le> setsum (%x. ((x * a) div p)) A"```
```--- a/src/HOL/Predicate.thy	Fri Nov 25 10:52:30 2011 +0100
+++ b/src/HOL/Predicate.thy	Fri Nov 25 13:14:58 2011 +0100
@@ -145,16 +145,16 @@

subsubsection {* Binary union *}

-lemma sup1I1 [elim?]: "A x \<Longrightarrow> (A \<squnion> B) x"
+lemma sup1I1 [intro?]: "A x \<Longrightarrow> (A \<squnion> B) x"
by (simp add: sup_fun_def)

-lemma sup2I1 [elim?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
+lemma sup2I1 [intro?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
by (simp add: sup_fun_def)

-lemma sup1I2 [elim?]: "B x \<Longrightarrow> (A \<squnion> B) x"
+lemma sup1I2 [intro?]: "B x \<Longrightarrow> (A \<squnion> B) x"
by (simp add: sup_fun_def)

-lemma sup2I2 [elim?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
+lemma sup2I2 [intro?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
by (simp add: sup_fun_def)

lemma sup1E [elim!]: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"```