# HG changeset patch
# User paulson
# Date 1331987771 0
# Node ID 7371429c527dbed2ef4dc6f1c81e418ec29524a3
# Parent  bd955d9f464b3c4961c216ba6a7db5ede95615b7
tidying and structured proofs

diff -r bd955d9f464b -r 7371429c527d src/ZF/IntDiv_ZF.thy
--- a/src/ZF/IntDiv_ZF.thy	Sat Mar 17 12:00:11 2012 +0100
+++ b/src/ZF/IntDiv_ZF.thy	Sat Mar 17 12:36:11 2012 +0000
@@ -359,7 +359,7 @@
  apply (erule zle_zless_trans)
  apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls)
  apply (erule zle_zless_trans)
- apply (simp add: );
+ apply simp
 apply (subgoal_tac "b $* q' $< b $* (#1 $+ q)")
  prefer 2
  apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls)
@@ -430,16 +430,18 @@
   assumes prem:
         "!!a b. [| a \<in> int; b \<in> int;
                    ~ (a $< b | b $<= #0) \<longrightarrow> P(<a, #2 $* b>) |] ==> P(<a,b>)"
-  shows "<u,v> \<in> int*int \<longrightarrow> P(<u,v>)"
-apply (rule_tac a = "<u,v>" in wf_induct)
-apply (rule_tac A = "int*int" and f = "%<a,b>.nat_of (a $- b $+ #1)"
-       in wf_measure)
-apply clarify
-apply (rule prem)
-apply (drule_tac [3] x = "<xa, #2 $\<times> y>" in spec)
-apply auto
-apply (simp add: not_zle_iff_zless posDivAlg_termination)
-done
+  shows "<u,v> \<in> int*int \<Longrightarrow> P(<u,v>)"
+using wf_measure [where A = "int*int" and f = "%<a,b>.nat_of (a $- b $+ #1)"]
+proof (induct "<u,v>" arbitrary: u v rule: wf_induct)
+  case (step x)
+  hence uv: "u \<in> int" "v \<in> int" by auto
+  thus ?case
+    apply (rule prem) 
+    apply (rule impI) 
+    apply (rule step) 
+    apply (auto simp add: step uv not_zle_iff_zless posDivAlg_termination)
+    done
+qed
 
 
 lemma posDivAlg_induct [consumes 2]:
@@ -459,26 +461,20 @@
 (*FIXME: use intify in integ_of so that we always have @{term"integ_of w \<in> int"}.
     then this rewrite can work for all constants!!*)
 lemma intify_eq_0_iff_zle: "intify(m) = #0 \<longleftrightarrow> (m $<= #0 & #0 $<= m)"
-apply (simp (no_asm) add: int_eq_iff_zle)
-done
+  by (simp add: int_eq_iff_zle)
 
 
 subsection{* Some convenient biconditionals for products of signs *}
 
 lemma zmult_pos: "[| #0 $< i; #0 $< j |] ==> #0 $< i $* j"
-apply (drule zmult_zless_mono1)
-apply auto
-done
+  by (drule zmult_zless_mono1, auto)
 
 lemma zmult_neg: "[| i $< #0; j $< #0 |] ==> #0 $< i $* j"
-apply (drule zmult_zless_mono1_neg)
-apply auto
-done
+  by (drule zmult_zless_mono1_neg, auto)
 
 lemma zmult_pos_neg: "[| #0 $< i; j $< #0 |] ==> i $* j $< #0"
-apply (drule zmult_zless_mono1_neg)
-apply auto
-done
+  by (drule zmult_zless_mono1_neg, auto)
+
 
 (** Inequality reasoning **)
 
@@ -591,16 +587,18 @@
         "!!a b. [| a \<in> int; b \<in> int;
                    ~ (#0 $<= a $+ b | b $<= #0) \<longrightarrow> P(<a, #2 $* b>) |]
                 ==> P(<a,b>)"
-  shows "<u,v> \<in> int*int \<longrightarrow> P(<u,v>)"
-apply (rule_tac a = "<u,v>" in wf_induct)
-apply (rule_tac A = "int*int" and f = "%<a,b>.nat_of ($- a $- b)"
-       in wf_measure)
-apply clarify
-apply (rule prem)
-apply (drule_tac [3] x = "<xa, #2 $\<times> y>" in spec)
-apply auto
-apply (simp add: not_zle_iff_zless negDivAlg_termination)
-done
+  shows "<u,v> \<in> int*int \<Longrightarrow> P(<u,v>)"
+using wf_measure [where A = "int*int" and f = "%<a,b>.nat_of ($- a $- b)"]
+proof (induct "<u,v>" arbitrary: u v rule: wf_induct)
+  case (step x)
+  hence uv: "u \<in> int" "v \<in> int" by auto
+  thus ?case
+    apply (rule prem) 
+    apply (rule impI) 
+    apply (rule step) 
+    apply (auto simp add: step uv not_zle_iff_zless negDivAlg_termination)
+    done
+qed
 
 lemma negDivAlg_induct [consumes 2]:
   assumes u_int: "u \<in> int"
@@ -729,12 +727,10 @@
 (** intify cancellation **)
 
 lemma zdiv_intify1 [simp]: "intify(x) zdiv y = x zdiv y"
-apply (simp (no_asm) add: zdiv_def)
-done
+  by (simp add: zdiv_def)
 
 lemma zdiv_intify2 [simp]: "x zdiv intify(y) = x zdiv y"
-apply (simp (no_asm) add: zdiv_def)
-done
+  by (simp add: zdiv_def)
 
 lemma zdiv_type [iff,TC]: "z zdiv w \<in> int"
 apply (unfold zdiv_def)
@@ -742,12 +738,10 @@
 done
 
 lemma zmod_intify1 [simp]: "intify(x) zmod y = x zmod y"
-apply (simp (no_asm) add: zmod_def)
-done
+  by (simp add: zmod_def)
 
 lemma zmod_intify2 [simp]: "x zmod intify(y) = x zmod y"
-apply (simp (no_asm) add: zmod_def)
-done
+  by (simp add: zmod_def)
 
 lemma zmod_type [iff,TC]: "z zmod w \<in> int"
 apply (unfold zmod_def)
@@ -760,13 +754,10 @@
     certain equations **)
 
 lemma DIVISION_BY_ZERO_ZDIV: "a zdiv #0 = #0"
-apply (simp (no_asm) add: zdiv_def divAlg_def posDivAlg_zero_divisor)
-done  (*NOT for adding to default simpset*)
+  by (simp add: zdiv_def divAlg_def posDivAlg_zero_divisor)
 
 lemma DIVISION_BY_ZERO_ZMOD: "a zmod #0 = intify(a)"
-apply (simp (no_asm) add: zmod_def divAlg_def posDivAlg_zero_divisor)
-done  (*NOT for adding to default simpset*)
-
+  by (simp add: zmod_def divAlg_def posDivAlg_zero_divisor)
 
 
 (** Basic laws about division and remainder **)
@@ -1021,24 +1012,19 @@
 subsection{* Computation of division and remainder *}
 
 lemma zdiv_zero [simp]: "#0 zdiv b = #0"
-apply (simp (no_asm) add: zdiv_def divAlg_def)
-done
+  by (simp add: zdiv_def divAlg_def)
 
 lemma zdiv_eq_minus1: "#0 $< b ==> #-1 zdiv b = #-1"
-apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
-done
+  by (simp (no_asm_simp) add: zdiv_def divAlg_def)
 
 lemma zmod_zero [simp]: "#0 zmod b = #0"
-apply (simp (no_asm) add: zmod_def divAlg_def)
-done
+  by (simp add: zmod_def divAlg_def)
 
 lemma zdiv_minus1: "#0 $< b ==> #-1 zdiv b = #-1"
-apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
-done
+  by (simp add: zdiv_def divAlg_def)
 
 lemma zmod_minus1: "#0 $< b ==> #-1 zmod b = b $- #1"
-apply (simp (no_asm_simp) add: zmod_def divAlg_def)
-done
+  by (simp add: zmod_def divAlg_def)
 
 (** a positive, b positive **)
 
@@ -1350,20 +1336,16 @@
 done
 
 lemma zdiv_zmult_self1 [simp]: "intify(b) \<noteq> #0 ==> (a$*b) zdiv b = intify(a)"
-apply (simp (no_asm_simp) add: zdiv_zmult1_eq)
-done
+  by (simp add: zdiv_zmult1_eq)
 
 lemma zdiv_zmult_self2 [simp]: "intify(b) \<noteq> #0 ==> (b$*a) zdiv b = intify(a)"
-apply (subst zmult_commute , erule zdiv_zmult_self1)
-done
+  by (simp add: zmult_commute) 
 
 lemma zmod_zmult_self1 [simp]: "(a$*b) zmod b = #0"
-apply (simp (no_asm) add: zmod_zmult1_eq)
-done
+  by (simp add: zmod_zmult1_eq)
 
 lemma zmod_zmult_self2 [simp]: "(b$*a) zmod b = #0"
-apply (simp (no_asm) add: zmult_commute zmod_zmult1_eq)
-done
+  by (simp add: zmult_commute zmod_zmult1_eq)
 
 
 (** proving (a$+b) zdiv c =
diff -r bd955d9f464b -r 7371429c527d src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Sat Mar 17 12:00:11 2012 +0100
+++ b/src/ZF/Ordinal.thy	Sat Mar 17 12:36:11 2012 +0000
@@ -353,13 +353,18 @@
 
 subsubsection{*Proving That < is a Linear Ordering on the Ordinals*}
 
-lemma Ord_linear [rule_format]:
-     "Ord(i) ==> (\<forall>j. Ord(j) \<longrightarrow> i\<in>j | i=j | j\<in>i)"
-apply (erule trans_induct)
-apply (rule impI [THEN allI])
-apply (erule_tac i=j in trans_induct)
-apply (blast dest: Ord_trans)
-done
+lemma Ord_linear:
+     "Ord(i) \<Longrightarrow> Ord(j) \<Longrightarrow> i\<in>j | i=j | j\<in>i"
+proof (induct i arbitrary: j rule: trans_induct)
+  case (step i)
+  note step_i = step
+  show ?case using `Ord(j)`
+    proof (induct j rule: trans_induct)
+      case (step j)
+      thus ?case using step_i
+        by (blast dest: Ord_trans)
+    qed
+qed
 
 text{*The trichotomy law for ordinals*}
 lemma Ord_linear_lt:
diff -r bd955d9f464b -r 7371429c527d src/ZF/WF.thy
--- a/src/ZF/WF.thy	Sat Mar 17 12:00:11 2012 +0100
+++ b/src/ZF/WF.thy	Sat Mar 17 12:36:11 2012 +0000
@@ -57,7 +57,7 @@
 lemma wf_imp_wf_on: "wf(r) ==> wf[A](r)"
 by (unfold wf_def wf_on_def, force)
 
-lemma wf_on_imp_wf: "[|wf[A](r); r \<subseteq> A*A|] ==> wf(r)";
+lemma wf_on_imp_wf: "[|wf[A](r); r \<subseteq> A*A|] ==> wf(r)"
 by (simp add: wf_on_def subset_Int_iff)
 
 lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)"
@@ -105,7 +105,7 @@
 
 text{*Consider the least @{term z} in @{term "domain(r)"} such that
   @{term "P(z)"} does not hold...*}
-lemma wf_induct [induct set: wf]:
+lemma wf_induct_raw:
     "[| wf(r);
         !!x.[| \<forall>y. <y,x>: r \<longrightarrow> P(y) |] ==> P(x) |]
      ==> P(a)"
@@ -114,7 +114,7 @@
 apply blast
 done
 
-lemmas wf_induct_rule = wf_induct [rule_format, induct set: wf]
+lemmas wf_induct = wf_induct_raw [rule_format, consumes 1, case_names step, induct set: wf]
 
 text{*The form of this rule is designed to match @{text wfI}*}
 lemma wf_induct2:
@@ -128,7 +128,7 @@
 lemma field_Int_square: "field(r \<inter> A*A) \<subseteq> A"
 by blast
 
-lemma wf_on_induct [consumes 2, induct set: wf_on]:
+lemma wf_on_induct_raw [consumes 2, induct set: wf_on]:
     "[| wf[A](r);  a \<in> A;
         !!x.[| x \<in> A;  \<forall>y\<in>A. <y,x>: r \<longrightarrow> P(y) |] ==> P(x)
      |]  ==>  P(a)"
@@ -137,8 +137,8 @@
 apply (rule field_Int_square, blast)
 done
 
-lemmas wf_on_induct_rule =
-  wf_on_induct [rule_format, consumes 2, induct set: wf_on]
+lemmas wf_on_induct =
+  wf_on_induct_raw [rule_format, consumes 2, case_names step, induct set: wf_on]
 
 
 text{*If @{term r} allows well-founded induction
@@ -297,6 +297,7 @@
  apply (rule lam_type [THEN restrict_type2])
   apply blast
  apply (blast dest: transD)
+apply atomize
 apply (frule spec [THEN mp], assumption)
 apply (subgoal_tac "<xa,a1> \<in> r")
  apply (drule_tac x1 = xa in spec [THEN mp], assumption)