--- a/src/ZF/Nat.thy Thu Nov 07 16:03:26 2019 +0100
+++ b/src/ZF/Nat.thy Fri Nov 08 12:07:39 2019 +0100
@@ -155,26 +155,21 @@
lemmas complete_induct = Ord_induct [OF _ Ord_nat, case_names less, consumes 1]
-lemmas complete_induct_rule =
- complete_induct [rule_format, case_names less, consumes 1]
-
-
-lemma nat_induct_from_lemma [rule_format]:
- "[| n \<in> nat; m \<in> nat;
- !!x. [| x \<in> nat; m \<le> x; P(x) |] ==> P(succ(x)) |]
- ==> m \<le> n \<longrightarrow> P(m) \<longrightarrow> P(n)"
-apply (erule nat_induct)
-apply (simp_all add: distrib_simps le0_iff le_succ_iff)
-done
+lemma complete_induct_rule [case_names less, consumes 1]:
+ "i \<in> nat \<Longrightarrow> (\<And>x. x \<in> nat \<Longrightarrow> (\<And>y. y \<in> x \<Longrightarrow> P(y)) \<Longrightarrow> P(x)) \<Longrightarrow> P(i)"
+ using complete_induct [of i P] by simp
(*Induction starting from m rather than 0*)
lemma nat_induct_from:
- "[| m \<le> n; m \<in> nat; n \<in> nat;
- P(m);
- !!x. [| x \<in> nat; m \<le> x; P(x) |] ==> P(succ(x)) |]
- ==> P(n)"
-apply (blast intro: nat_induct_from_lemma)
-done
+ assumes "m \<le> n" "m \<in> nat" "n \<in> nat"
+ and "P(m)"
+ and "!!x. [| x \<in> nat; m \<le> x; P(x) |] ==> P(succ(x))"
+ shows "P(n)"
+proof -
+ from assms(3) have "m \<le> n \<longrightarrow> P(m) \<longrightarrow> P(n)"
+ by (rule nat_induct) (use assms(5) in \<open>simp_all add: distrib_simps le_succ_iff\<close>)
+ with assms(1,2,4) show ?thesis by blast
+qed
(*Induction suitable for subtraction and less-than*)
lemma diff_induct [case_names 0 0_succ succ_succ, consumes 2]:
--- a/src/ZF/Ordinal.thy Thu Nov 07 16:03:26 2019 +0100
+++ b/src/ZF/Ordinal.thy Fri Nov 08 12:07:39 2019 +0100
@@ -329,17 +329,16 @@
done
(*Induction over an ordinal*)
-lemmas Ord_induct [consumes 2] = Transset_induct [rule_format, OF _ Ord_is_Transset]
+lemma Ord_induct [consumes 2]:
+ "i \<in> k \<Longrightarrow> Ord(k) \<Longrightarrow> (\<And>x. x \<in> k \<Longrightarrow> (\<And>y. y \<in> x \<Longrightarrow> P(y)) \<Longrightarrow> P(x)) \<Longrightarrow> P(i)"
+ using Transset_induct [OF _ Ord_is_Transset, of i k P] by simp
(*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
-
-lemma trans_induct [rule_format, consumes 1, case_names step]:
- "[| Ord(i);
- !!x.[| Ord(x); \<forall>y\<in>x. P(y) |] ==> P(x) |]
- ==> P(i)"
-apply (rule Ord_succ [THEN succI1 [THEN Ord_induct]], assumption)
-apply (blast intro: Ord_succ [THEN Ord_in_Ord])
-done
+lemma trans_induct [consumes 1, case_names step]:
+ "Ord(i) \<Longrightarrow> (\<And>x. Ord(x) \<Longrightarrow> (\<And>y. y \<in> x \<Longrightarrow> P(y)) \<Longrightarrow> P(x)) \<Longrightarrow> P(i)"
+ apply (rule Ord_succ [THEN succI1 [THEN Ord_induct]], assumption)
+ apply (blast intro: Ord_succ [THEN Ord_in_Ord])
+ done
section\<open>Fundamental properties of the epsilon ordering (< on ordinals)\<close>
@@ -716,7 +715,9 @@
apply (erule Ord_cases, blast+)
done
-lemmas trans_induct3 = trans_induct3_raw [rule_format, case_names 0 succ limit, consumes 1]
+lemma trans_induct3 [case_names 0 succ limit, consumes 1]:
+ "Ord(i) \<Longrightarrow> P(0) \<Longrightarrow> (\<And>x. Ord(x) \<Longrightarrow> P(x) \<Longrightarrow> P(succ(x))) \<Longrightarrow> (\<And>x. Limit(x) \<Longrightarrow> (\<And>y. y \<in> x \<Longrightarrow> P(y)) \<Longrightarrow> P(x)) \<Longrightarrow> P(i)"
+ using trans_induct3_raw [of i P] by simp
text\<open>A set of ordinals is either empty, contains its own union, or its
union is a limit ordinal.\<close>
@@ -756,7 +757,7 @@
lemma Ord_Union_eq_succD: "[|\<forall>x\<in>X. Ord(x); \<Union>X = succ(j)|] ==> succ(j) \<in> X"
by (drule Ord_set_cases, auto)
-lemma Limit_Union [rule_format]: "[| I \<noteq> 0; \<forall>i\<in>I. Limit(i) |] ==> Limit(\<Union>I)"
+lemma Limit_Union [rule_format]: "[| I \<noteq> 0; (\<And>i. i\<in>I \<Longrightarrow> Limit(i)) |] ==> Limit(\<Union>I)"
apply (simp add: Limit_def lt_def)
apply (blast intro!: equalityI)
done
--- a/src/ZF/WF.thy Thu Nov 07 16:03:26 2019 +0100
+++ b/src/ZF/WF.thy Fri Nov 08 12:07:39 2019 +0100
@@ -137,9 +137,9 @@
apply (rule field_Int_square, blast)
done
-lemmas wf_on_induct =
- wf_on_induct_raw [rule_format, consumes 2, case_names step, induct set: wf_on]
-
+lemma wf_on_induct [consumes 2, case_names step, induct set: wf_on]:
+ "wf[A](r) \<Longrightarrow> a \<in> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> (\<And>y. y \<in> A \<Longrightarrow> \<langle>y, x\<rangle> \<in> r \<Longrightarrow> P(y)) \<Longrightarrow> P(x)) \<Longrightarrow> P(a)"
+ using wf_on_induct_raw [of A r a P] by simp
text\<open>If \<^term>\<open>r\<close> allows well-founded induction
then we have \<^term>\<open>wf(r)\<close>.\<close>
@@ -169,8 +169,9 @@
lemma wf_on_not_refl: "[| wf[A](r); a \<in> A |] ==> <a,a> \<notin> r"
by (erule_tac a=a in wf_on_induct, assumption, blast)
-lemma wf_on_not_sym [rule_format]:
- "[| wf[A](r); a \<in> A |] ==> \<forall>b\<in>A. <a,b>:r \<longrightarrow> <b,a>\<notin>r"
+lemma wf_on_not_sym:
+ "[| wf[A](r); a \<in> A |] ==> (\<And>b. b\<in>A \<Longrightarrow> <a,b>:r \<Longrightarrow> <b,a>\<notin>r)"
+apply (atomize (full), intro impI)
apply (erule_tac a=a in wf_on_induct, assumption, blast)
done
--- a/src/ZF/equalities.thy Thu Nov 07 16:03:26 2019 +0100
+++ b/src/ZF/equalities.thy Fri Nov 08 12:07:39 2019 +0100
@@ -105,7 +105,7 @@
lemma Diff_cons_eq: "cons(a,B) - C = (if a\<in>C then B-C else cons(a,B-C))"
by auto
-lemma equal_singleton [rule_format]: "[| a: C; \<forall>y\<in>C. y=b |] ==> C = {b}"
+lemma equal_singleton: "[| a: C; \<And>y. y \<in>C \<Longrightarrow> y=b |] ==> C = {b}"
by blast
lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)"
--- a/src/ZF/func.thy Thu Nov 07 16:03:26 2019 +0100
+++ b/src/ZF/func.thy Fri Nov 08 12:07:39 2019 +0100
@@ -356,8 +356,8 @@
apply (blast intro!: rel_Union function_Union)
done
-lemma gen_relation_Union [rule_format]:
- "\<forall>f\<in>F. relation(f) \<Longrightarrow> relation(\<Union>(F))"
+lemma gen_relation_Union:
+ "(\<And>f. f\<in>F \<Longrightarrow> relation(f)) \<Longrightarrow> relation(\<Union>(F))"
by (simp add: relation_def)