# HG changeset patch
# User wenzelm
# Date 1331918482 -3600
# Node ID daf5538144d65f7b7258820acc8c37fe22885287
# Parent  0c8fb96cce73c029a0e485f01a0d2607af9c497d# Parent  5c6955f487e57080131bd1132f5e079690a26446
merged

diff -r 5c6955f487e5 -r daf5538144d6 NEWS
--- a/NEWS	Fri Mar 16 18:20:12 2012 +0100
+++ b/NEWS	Fri Mar 16 18:21:22 2012 +0100
@@ -1727,6 +1727,13 @@
 * All constant names are now qualified internally and use proper
 identifiers, e.g. "IFOL.eq" instead of "op =".  INCOMPATIBILITY.
 
+*** ZF ***
+
+* Greater support for structured proofs involving induction or case analysis.
+
+* Much greater use of special symbols.
+
+* Removal of many ML theorem bindings. INCOMPATIBILITY.
 
 *** ML ***
 
diff -r 5c6955f487e5 -r daf5538144d6 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Mar 16 18:20:12 2012 +0100
+++ b/src/HOL/Word/Word.thy	Fri Mar 16 18:21:22 2012 +0100
@@ -802,8 +802,10 @@
 lemma unats_uints: "unats n = nat ` uints n"
   by (auto simp add : uints_unats image_iff)
 
-lemmas bintr_num = word_ubin.norm_eq_iff [symmetric, folded word_number_of_def]
-lemmas sbintr_num = word_sbin.norm_eq_iff [symmetric, folded word_number_of_def]
+lemmas bintr_num = word_ubin.norm_eq_iff
+  [of "number_of a" "number_of b", symmetric, folded word_number_of_alt] for a b
+lemmas sbintr_num = word_sbin.norm_eq_iff
+  [of "number_of a" "number_of b", symmetric, folded word_number_of_alt] for a b
 
 lemmas num_of_bintr = word_ubin.Abs_norm [folded word_number_of_def]
 lemmas num_of_sbintr = word_sbin.Abs_norm [folded word_number_of_def]
@@ -812,22 +814,25 @@
   may want these in reverse, but loop as simp rules, so use following *)
 
 lemma num_of_bintr':
-  "bintrunc (len_of TYPE('a :: len0)) a = b \<Longrightarrow> 
+  "bintrunc (len_of TYPE('a :: len0)) (number_of a) = (number_of b) \<Longrightarrow> 
     number_of a = (number_of b :: 'a word)"
-  apply safe
-  apply (rule_tac num_of_bintr [symmetric])
-  done
+  unfolding bintr_num by (erule subst, simp)
 
 lemma num_of_sbintr':
-  "sbintrunc (len_of TYPE('a :: len) - 1) a = b \<Longrightarrow> 
+  "sbintrunc (len_of TYPE('a :: len) - 1) (number_of a) = (number_of b) \<Longrightarrow> 
     number_of a = (number_of b :: 'a word)"
-  apply safe
-  apply (rule_tac num_of_sbintr [symmetric])
-  done
-
-lemmas num_abs_bintr = sym [THEN trans, OF num_of_bintr word_number_of_def]
-lemmas num_abs_sbintr = sym [THEN trans, OF num_of_sbintr word_number_of_def]
-  
+  unfolding sbintr_num by (erule subst, simp)
+
+lemma num_abs_bintr:
+  "(number_of x :: 'a word) =
+    word_of_int (bintrunc (len_of TYPE('a::len0)) (number_of x))"
+  by (simp only: word_ubin.Abs_norm word_number_of_alt)
+
+lemma num_abs_sbintr:
+  "(number_of x :: 'a word) =
+    word_of_int (sbintrunc (len_of TYPE('a::len) - 1) (number_of x))"
+  by (simp only: word_sbin.Abs_norm word_number_of_alt)
+
 (** cast - note, no arg for new length, as it's determined by type of result,
   thus in "cast w = w, the type means cast to length of w! **)
 
@@ -2880,16 +2885,16 @@
   by (induct n) (auto simp: shiftl1_2t)
 
 lemma shiftr1_bintr [simp]:
-  "(shiftr1 (number_of w) :: 'a :: len0 word) = 
-    number_of (bin_rest (bintrunc (len_of TYPE ('a)) w))" 
-  unfolding shiftr1_def word_number_of_def
-  by (simp add : word_ubin.eq_norm)
-
-lemma sshiftr1_sbintr [simp] :
-  "(sshiftr1 (number_of w) :: 'a :: len word) = 
-    number_of (bin_rest (sbintrunc (len_of TYPE ('a) - 1) w))" 
-  unfolding sshiftr1_def word_number_of_def
-  by (simp add : word_sbin.eq_norm)
+  "(shiftr1 (number_of w) :: 'a :: len0 word) =
+    word_of_int (bin_rest (bintrunc (len_of TYPE ('a)) (number_of w)))"
+  unfolding shiftr1_def word_number_of_alt
+  by (simp add: word_ubin.eq_norm)
+
+lemma sshiftr1_sbintr [simp]:
+  "(sshiftr1 (number_of w) :: 'a :: len word) =
+    word_of_int (bin_rest (sbintrunc (len_of TYPE ('a) - 1) (number_of w)))"
+  unfolding sshiftr1_def word_number_of_alt
+  by (simp add: word_sbin.eq_norm)
 
 lemma shiftr_no [simp]:
   "(number_of w::'a::len0 word) >> n = word_of_int
@@ -3379,11 +3384,9 @@
 
 lemma word_rsplit_no:
   "(word_rsplit (number_of bin :: 'b :: len0 word) :: 'a word list) = 
-    map number_of (bin_rsplit (len_of TYPE('a :: len)) 
-      (len_of TYPE('b), bintrunc (len_of TYPE('b)) bin))"
-  apply (unfold word_rsplit_def word_no_wi)
-  apply (simp add: word_ubin.eq_norm)
-  done
+    map word_of_int (bin_rsplit (len_of TYPE('a :: len)) 
+      (len_of TYPE('b), bintrunc (len_of TYPE('b)) (number_of bin)))"
+  unfolding word_rsplit_def by (simp add: word_ubin.eq_norm)
 
 lemmas word_rsplit_no_cl [simp] = word_rsplit_no
   [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
diff -r 5c6955f487e5 -r daf5538144d6 src/ZF/Cardinal_AC.thy
--- a/src/ZF/Cardinal_AC.thy	Fri Mar 16 18:20:12 2012 +0100
+++ b/src/ZF/Cardinal_AC.thy	Fri Mar 16 18:21:22 2012 +0100
@@ -134,29 +134,38 @@
 
 (*Kunen's Lemma 10.21*)
 lemma cardinal_UN_le:
-     "[| InfCard(K);  \<forall>i\<in>K. |X(i)| \<le> K |] ==> |\<Union>i\<in>K. X(i)| \<le> K"
-apply (simp add: InfCard_is_Card le_Card_iff)
-apply (rule lepoll_trans)
- prefer 2
- apply (rule InfCard_square_eq [THEN eqpoll_imp_lepoll])
- apply (simp add: InfCard_is_Card Card_cardinal_eq)
-apply (unfold lepoll_def)
-apply (frule InfCard_is_Card [THEN Card_is_Ord])
-apply (erule AC_ball_Pi [THEN exE])
-apply (rule exI)
-(*Lemma needed in both subgoals, for a fixed z*)
-apply (subgoal_tac "\<forall>z\<in>(\<Union>i\<in>K. X (i)). z: X (LEAST i. z:X (i)) &
-                    (LEAST i. z:X (i)) \<in> K")
- prefer 2
- apply (fast intro!: Least_le [THEN lt_trans1, THEN ltD] ltI
-             elim!: LeastI Ord_in_Ord)
-apply (rule_tac c = "%z. <LEAST i. z:X (i), f ` (LEAST i. z:X (i)) ` z>"
-            and d = "%<i,j>. converse (f`i) ` j" in lam_injective)
-(*Instantiate the lemma proved above*)
-by (blast intro: inj_is_fun [THEN apply_type] dest: apply_type, force)
+  assumes K: "InfCard(K)" 
+  shows "(!!i. i\<in>K ==> |X(i)| \<le> K) ==> |\<Union>i\<in>K. X(i)| \<le> K"
+proof (simp add: K InfCard_is_Card le_Card_iff)
+  have [intro]: "Ord(K)" by (blast intro: InfCard_is_Card Card_is_Ord K) 
+  assume "!!i. i\<in>K ==> X(i) \<lesssim> K"
+  hence "!!i. i\<in>K ==> \<exists>f. f \<in> inj(X(i), K)" by (simp add: lepoll_def) 
+  with AC_Pi obtain f where f: "f \<in> (\<Pi> i\<in>K. inj(X(i), K))"
+    apply - apply atomize apply auto done
+  { fix z
+    assume z: "z \<in> (\<Union>i\<in>K. X(i))"
+    then obtain i where i: "i \<in> K" "Ord(i)" "z \<in> X(i)"
+      by (blast intro: Ord_in_Ord [of K]) 
+    hence "(LEAST i. z \<in> X(i)) \<le> i" by (fast intro: Least_le) 
+    hence "(LEAST i. z \<in> X(i)) < K" by (best intro: lt_trans1 ltI i) 
+    hence "(LEAST i. z \<in> X(i)) \<in> K" and "z \<in> X(LEAST i. z \<in> X(i))"  
+      by (auto intro: LeastI ltD i) 
+  } note mems = this
+  have "(\<Union>i\<in>K. X(i)) \<lesssim> K \<times> K" 
+    proof (unfold lepoll_def)
+      show "\<exists>f. f \<in> inj(\<Union>RepFun(K, X), K \<times> K)"
+        apply (rule exI) 
+        apply (rule_tac c = "%z. \<langle>LEAST i. z \<in> X(i), f ` (LEAST i. z \<in> X(i)) ` z\<rangle>"
+                    and d = "%\<langle>i,j\<rangle>. converse (f`i) ` j" in lam_injective) 
+        apply (force intro: f inj_is_fun mems apply_type Perm.left_inverse)+
+        done
+    qed
+  also have "... \<approx> K" 
+    by (simp add: K InfCard_square_eq InfCard_is_Card Card_cardinal_eq)
+  finally show "(\<Union>i\<in>K. X(i)) \<lesssim> K" .
+qed
 
-
-(*The same again, using csucc*)
+text{*The same again, using @{term csucc}*}
 lemma cardinal_UN_lt_csucc:
      "[| InfCard(K);  \<forall>i\<in>K. |X(i)| < csucc(K) |]
       ==> |\<Union>i\<in>K. X(i)| < csucc(K)"
diff -r 5c6955f487e5 -r daf5538144d6 src/ZF/Constructible/Normal.thy
--- a/src/ZF/Constructible/Normal.thy	Fri Mar 16 18:20:12 2012 +0100
+++ b/src/ZF/Constructible/Normal.thy	Fri Mar 16 18:21:22 2012 +0100
@@ -226,7 +226,7 @@
 by (simp add: Normal_def mono_Ord_def cont_Ord_def)
 
 lemma mono_Ord_imp_Ord: "[| Ord(i); mono_Ord(F) |] ==> Ord(F(i))"
-apply (simp add: mono_Ord_def) 
+apply (auto simp add: mono_Ord_def)
 apply (blast intro: lt_Ord) 
 done
 
@@ -242,16 +242,29 @@
 lemma Normal_imp_mono: "[| i<j; Normal(F) |] ==> F(i) < F(j)"
 by (simp add: Normal_def mono_Ord_def)
 
-lemma Normal_increasing: "[| Ord(i); Normal(F) |] ==> i\<le>F(i)"
-apply (induct i rule: trans_induct3)
-  apply (simp add: subset_imp_le)
- apply (subgoal_tac "F(x) < F(succ(x))")
-  apply (force intro: lt_trans1)
- apply (simp add: Normal_def mono_Ord_def)
-apply (subgoal_tac "(\<Union>y<x. y) \<le> (\<Union>y<x. F(y))")
- apply (simp add: Normal_imp_cont Limit_OUN_eq) 
-apply (blast intro: ltD le_implies_OUN_le_OUN)
-done
+lemma Normal_increasing:
+  assumes i: "Ord(i)" and F: "Normal(F)" shows"i \<le> F(i)"
+using i
+proof (induct i rule: trans_induct3)
+  case 0 thus ?case by (simp add: subset_imp_le F)
+next
+  case (succ i) 
+  hence "F(i) < F(succ(i))" using F
+    by (simp add: Normal_def mono_Ord_def)
+  thus ?case using succ.hyps
+    by (blast intro: lt_trans1)
+next
+  case (limit l) 
+  hence "l = (\<Union>y<l. y)" 
+    by (simp add: Limit_OUN_eq)
+  also have "... \<le> (\<Union>y<l. F(y))" using limit
+    by (blast intro: ltD le_implies_OUN_le_OUN)
+  finally have "l \<le> (\<Union>y<l. F(y))" .
+  moreover have "(\<Union>y<l. F(y)) \<le> F(l)" using limit F
+    by (simp add: Normal_imp_cont lt_Ord)
+  ultimately show ?case
+    by (blast intro: le_trans) 
+qed
 
 
 subsubsection{*The class of fixedpoints is closed and unbounded*}
@@ -387,24 +400,32 @@
 apply (simp_all add: ltD def_transrec2 [OF normalize_def])
 done
 
-lemma normalize_lemma [rule_format]:
-     "[| Ord(b); !!x. Ord(x) ==> Ord(F(x)) |] 
-      ==> \<forall>a. a < b \<longrightarrow> normalize(F, a) < normalize(F, b)"
-apply (erule trans_induct3)
-  apply (simp_all add: le_iff def_transrec2 [OF normalize_def])
- apply clarify
-apply (rule Un_upper2_lt) 
-  apply auto
- apply (drule spec, drule mp, assumption) 
- apply (erule leI) 
-apply (drule Limit_has_succ, assumption)
-apply (blast intro!: Ord_normalize intro: OUN_upper_lt ltD lt_Ord)
-done  
-
 lemma normalize_increasing:
-     "[| a < b;  !!x. Ord(x) ==> Ord(F(x)) |] 
-      ==> normalize(F, a) < normalize(F, b)"
-by (blast intro!: normalize_lemma intro: lt_Ord2) 
+  assumes ab: "a < b" and F: "!!x. Ord(x) ==> Ord(F(x))"
+  shows "normalize(F,a) < normalize(F,b)"
+proof -
+  { fix x
+    have "Ord(b)" using ab by (blast intro: lt_Ord2) 
+    hence "x < b \<Longrightarrow> normalize(F,x) < normalize(F,b)"
+    proof (induct b arbitrary: x rule: trans_induct3)
+      case 0 thus ?case by simp
+    next
+      case (succ b)
+      thus ?case
+        by (auto simp add: le_iff def_transrec2 [OF normalize_def] intro: Un_upper2_lt F)
+    next
+      case (limit l)
+      hence sc: "succ(x) < l" 
+        by (blast intro: Limit_has_succ) 
+      hence "normalize(F,x) < normalize(F,succ(x))" 
+        by (blast intro: limit elim: ltE) 
+      hence "normalize(F,x) < (\<Union>j<l. normalize(F,j))"
+        by (blast intro: OUN_upper_lt lt_Ord F sc) 
+      thus ?case using limit
+        by (simp add: def_transrec2 [OF normalize_def])
+    qed
+  } thus ?thesis using ab .
+qed
 
 theorem Normal_normalize:
      "(!!x. Ord(x) ==> Ord(F(x))) ==> Normal(normalize(F))"
@@ -414,14 +435,20 @@
 done
 
 theorem le_normalize:
-     "[| Ord(a); cont_Ord(F); !!x. Ord(x) ==> Ord(F(x)) |] 
-      ==> F(a) \<le> normalize(F,a)"
-apply (erule trans_induct3) 
-apply (simp_all add: def_transrec2 [OF normalize_def])
-apply (simp add: Un_upper1_le) 
-apply (simp add: cont_Ord_def) 
-apply (blast intro: ltD le_implies_OUN_le_OUN)
-done
+  assumes a: "Ord(a)" and coF: "cont_Ord(F)" and F: "!!x. Ord(x) ==> Ord(F(x))"
+  shows "F(a) \<le> normalize(F,a)"
+using a
+proof (induct a rule: trans_induct3)
+  case 0 thus ?case by (simp add: F def_transrec2 [OF normalize_def])
+next
+  case (succ a)
+  thus ?case
+    by (simp add: def_transrec2 [OF normalize_def] Un_upper1_le F )
+next
+  case (limit l) 
+  thus ?case using F coF [unfolded cont_Ord_def]
+    by (simp add: def_transrec2 [OF normalize_def] le_implies_OUN_le_OUN ltD) 
+qed
 
 
 subsection {*The Alephs*}
@@ -442,18 +469,30 @@
                      def_transrec2 [OF Aleph_def])
 done
 
-lemma Aleph_lemma [rule_format]:
-     "Ord(b) ==> \<forall>a. a < b \<longrightarrow> Aleph(a) < Aleph(b)"
-apply (erule trans_induct3) 
-apply (simp_all add: le_iff def_transrec2 [OF Aleph_def])  
-apply (blast intro: lt_trans lt_csucc Card_is_Ord, clarify)
-apply (drule Limit_has_succ, assumption)
-apply (blast intro: Card_is_Ord Card_Aleph OUN_upper_lt ltD lt_Ord)
-done  
-
 lemma Aleph_increasing:
-     "a < b ==> Aleph(a) < Aleph(b)"
-by (blast intro!: Aleph_lemma intro: lt_Ord2) 
+  assumes ab: "a < b" shows "Aleph(a) < Aleph(b)"
+proof -
+  { fix x
+    have "Ord(b)" using ab by (blast intro: lt_Ord2) 
+    hence "x < b \<Longrightarrow> Aleph(x) < Aleph(b)"
+    proof (induct b arbitrary: x rule: trans_induct3)
+      case 0 thus ?case by simp
+    next
+      case (succ b)
+      thus ?case
+        by (force simp add: le_iff def_transrec2 [OF Aleph_def] 
+                  intro: lt_trans lt_csucc Card_is_Ord)
+    next
+      case (limit l)
+      hence sc: "succ(x) < l" 
+        by (blast intro: Limit_has_succ) 
+      hence "\<aleph> x < (\<Union>j<l. \<aleph>j)" using limit
+        by (blast intro: OUN_upper_lt Card_is_Ord ltD lt_Ord)
+      thus ?case using limit
+        by (simp add: def_transrec2 [OF Aleph_def])
+    qed
+  } thus ?thesis using ab .
+qed
 
 theorem Normal_Aleph: "Normal(Aleph)"
 apply (rule NormalI)