# HG changeset patch
# User wenzelm
# Date 1573211259 -3600
# Node ID 950e1cfe0fe46e4c5c69311df46db2eeed1fcd55
# Parent  995fe5877d53550f8bd74c906746d7c129ccefd3
tuned proofs -- more stable proof terms without [rule_format];

diff -r 995fe5877d53 -r 950e1cfe0fe4 src/ZF/Nat.thy
--- 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]:
diff -r 995fe5877d53 -r 950e1cfe0fe4 src/ZF/Ordinal.thy
--- 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
diff -r 995fe5877d53 -r 950e1cfe0fe4 src/ZF/WF.thy
--- 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
 
diff -r 995fe5877d53 -r 950e1cfe0fe4 src/ZF/equalities.thy
--- 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)"
diff -r 995fe5877d53 -r 950e1cfe0fe4 src/ZF/func.thy
--- 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)