# HG changeset patch
# User paulson
# Date 1331745570 0
# Node ID 571ce2bc0b64994555273eee440e939e5479a253
# Parent  89cc3dfb383bcb9750091cd48421b1812c0e97f6# Parent  38ecb2dc3636ca9c4198c4db133e89803ae31ad8
merged

diff -r 89cc3dfb383b -r 571ce2bc0b64 src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Wed Mar 14 17:40:00 2012 +0100
+++ b/src/ZF/Cardinal.thy	Wed Mar 14 17:19:30 2012 +0000
@@ -540,15 +540,21 @@
 done
 
 
-lemma nat_lepoll_imp_le [rule_format]:
-     "m \<in> nat ==> \<forall>n\<in>nat. m \<lesssim> n \<longrightarrow> m \<le> n"
-apply (induct_tac m)
-apply (blast intro!: nat_0_le)
-apply (rule ballI)
-apply (erule_tac n = n in natE)
-apply (simp (no_asm_simp) add: lepoll_def inj_def)
-apply (blast intro!: succ_leI dest!: succ_lepoll_succD)
-done
+lemma nat_lepoll_imp_le:
+     "m \<in> nat ==> n \<in> nat \<Longrightarrow> m \<lesssim> n \<Longrightarrow> m \<le> n"
+proof (induct m arbitrary: n rule: nat_induct)
+  case 0 thus ?case by (blast intro!: nat_0_le)
+next
+  case (succ m)
+  show ?case  using `n \<in> nat`
+    proof (cases rule: natE)
+      case 0 thus ?thesis using succ
+        by (simp add: lepoll_def inj_def)
+    next
+      case (succ n') thus ?thesis using succ.hyps ` succ(m) \<lesssim> n`
+        by (blast intro!: succ_leI dest!: succ_lepoll_succD)
+    qed
+qed
 
 lemma nat_eqpoll_iff: "[| m \<in> nat; n: nat |] ==> m \<approx> n \<longleftrightarrow> m = n"
 apply (rule iffI)
diff -r 89cc3dfb383b -r 571ce2bc0b64 src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Wed Mar 14 17:40:00 2012 +0100
+++ b/src/ZF/CardinalArith.thy	Wed Mar 14 17:19:30 2012 +0000
@@ -628,28 +628,25 @@
   assumes IK: "InfCard(K)" shows "InfCard(K) ==> K \<otimes> K = K"
 proof -
   have  OK: "Ord(K)" using IK by (simp add: Card_is_Ord InfCard_is_Card) 
-  have "InfCard(K) \<longrightarrow> K \<otimes> K = K"
-    proof (rule trans_induct [OF OK], rule impI)
-      fix i
-      assume i: "Ord(i)" "InfCard(i)"
-         and ih: " \<forall>y\<in>i. InfCard(y) \<longrightarrow> y \<otimes> y = y"
-      show "i \<otimes> i = i"
-        proof (rule le_anti_sym)
-          have "|i \<times> i| = |ordertype(i \<times> i, csquare_rel(i))|" 
-            by (rule cardinal_cong, 
-                simp add: i well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll])
-          hence "i \<otimes> i \<le> ordertype(i \<times> i, csquare_rel(i))" using i
-            by (simp add: cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype])
-          moreover
-          have "ordertype(i \<times> i, csquare_rel(i)) \<le> i" using ih i
-            by (simp add: ordertype_csquare_le) 
-          ultimately show "i \<otimes> i \<le> i" by (rule le_trans)
-        next
-          show "i \<le> i \<otimes> i" using i
-            by (blast intro: cmult_square_le InfCard_is_Card) 
-        qed
+  show "InfCard(K) ==> K \<otimes> K = K" using OK
+  proof (induct rule: trans_induct)
+    case (step i)
+    show "i \<otimes> i = i"
+    proof (rule le_anti_sym)
+      have "|i \<times> i| = |ordertype(i \<times> i, csquare_rel(i))|" 
+        by (rule cardinal_cong, 
+          simp add: step.hyps well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll])
+      hence "i \<otimes> i \<le> ordertype(i \<times> i, csquare_rel(i))" 
+        by (simp add: step.hyps cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype])
+      moreover
+      have "ordertype(i \<times> i, csquare_rel(i)) \<le> i" using step
+        by (simp add: ordertype_csquare_le) 
+      ultimately show "i \<otimes> i \<le> i" by (rule le_trans)
+    next
+      show "i \<le> i \<otimes> i" using step
+        by (blast intro: cmult_square_le InfCard_is_Card) 
     qed
-  thus ?thesis using IK ..
+  qed
 qed
 
 (*Corollary for arbitrary well-ordered sets (all sets, assuming AC)*)
@@ -910,10 +907,15 @@
   finally show ?thesis .
 qed
 
-lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i \<subseteq> nat \<longrightarrow> i \<in> nat | i=nat"
-apply (erule trans_induct3, auto)
-apply (blast dest!: nat_le_Limit [THEN le_imp_subset])
-done
+lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i \<subseteq> nat \<Longrightarrow> i \<in> nat | i=nat"
+proof (induct i rule: trans_induct3)
+  case 0 thus ?case by auto
+next
+  case (succ i) thus ?case by auto
+next
+  case (limit l) thus ?case
+    by (blast dest: nat_le_Limit le_imp_subset)
+qed
 
 lemma Ord_nat_subset_into_Card: "[| Ord(i); i \<subseteq> nat |] ==> Card(i)"
 by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card)
diff -r 89cc3dfb383b -r 571ce2bc0b64 src/ZF/Nat_ZF.thy
--- a/src/ZF/Nat_ZF.thy	Wed Mar 14 17:40:00 2012 +0100
+++ b/src/ZF/Nat_ZF.thy	Wed Mar 14 17:19:30 2012 +0000
@@ -87,14 +87,16 @@
 
 (*Mathematical induction*)
 lemma nat_induct [case_names 0 succ, induct set: nat]:
-    "[| n: nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) |] ==> P(n)"
+    "[| n \<in> nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) |] ==> P(n)"
 by (erule def_induct [OF nat_def nat_bnd_mono], blast)
 
 lemma natE:
-    "[| n: nat;  n=0 ==> P;  !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P"
-by (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto)
+ assumes "n \<in> nat"
+ obtains (0) "n=0" | (succ) x where "x \<in> nat" "n=succ(x)" 
+using assms
+by (rule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE]) auto
 
-lemma nat_into_Ord [simp]: "n: nat ==> Ord(n)"
+lemma nat_into_Ord [simp]: "n \<in> nat ==> Ord(n)"
 by (erule nat_induct, auto)
 
 (* @{term"i: nat ==> 0 \<le> i"}; same thing as @{term"0<succ(i)"}  *)
@@ -123,7 +125,7 @@
 lemma succ_natD: "succ(i): nat ==> i: nat"
 by (rule Ord_trans [OF succI1], auto)
 
-lemma nat_succ_iff [iff]: "succ(n): nat \<longleftrightarrow> n: nat"
+lemma nat_succ_iff [iff]: "succ(n): nat \<longleftrightarrow> n \<in> nat"
 by (blast dest!: succ_natD)
 
 lemma nat_le_Limit: "Limit(i) ==> nat \<le> i"
@@ -138,7 +140,7 @@
 (* [| succ(i): k;  k: nat |] ==> i: k *)
 lemmas succ_in_naturalD = Ord_trans [OF succI1 _ nat_into_Ord]
 
-lemma lt_nat_in_nat: "[| m<n;  n: nat |] ==> m: nat"
+lemma lt_nat_in_nat: "[| m<n;  n \<in> nat |] ==> m: nat"
 apply (erule ltE)
 apply (erule Ord_trans, assumption, simp)
 done
@@ -158,7 +160,7 @@
 
 
 lemma nat_induct_from_lemma [rule_format]:
-    "[| n: nat;  m: nat;
+    "[| n \<in> nat;  m: nat;
         !!x. [| x: nat;  m \<le> x;  P(x) |] ==> P(succ(x)) |]
      ==> m \<le> n \<longrightarrow> P(m) \<longrightarrow> P(n)"
 apply (erule nat_induct)
@@ -167,7 +169,7 @@
 
 (*Induction starting from m rather than 0*)
 lemma nat_induct_from:
-    "[| m \<le> n;  m: nat;  n: nat;
+    "[| m \<le> n;  m: nat;  n \<in> nat;
         P(m);
         !!x. [| x: nat;  m \<le> x;  P(x) |] ==> P(succ(x)) |]
      ==> P(n)"
@@ -176,7 +178,7 @@
 
 (*Induction suitable for subtraction and less-than*)
 lemma diff_induct [case_names 0 0_succ succ_succ, consumes 2]:
-    "[| m: nat;  n: nat;
+    "[| m: nat;  n \<in> nat;
         !!x. x: nat ==> P(x,0);
         !!y. y: nat ==> P(0,succ(y));
         !!x y. [| x: nat;  y: nat;  P(x,y) |] ==> P(succ(x),succ(y)) |]
@@ -201,7 +203,7 @@
 done
 
 lemma succ_lt_induct:
-    "[| m<n;  n: nat;
+    "[| m<n;  n \<in> nat;
         P(m,succ(m));
         !!x. [| x: nat;  P(m,x) |] ==> P(m,succ(x)) |]
      ==> P(m,n)"
@@ -241,7 +243,7 @@
 by (simp add: nat_case_def)
 
 lemma nat_case_type [TC]:
-    "[| n: nat;  a: C(0);  !!m. m: nat ==> b(m): C(succ(m)) |]
+    "[| n \<in> nat;  a: C(0);  !!m. m: nat ==> b(m): C(succ(m)) |]
      ==> nat_case(a,b,n) \<in> C(n)";
 by (erule nat_induct, auto)
 
diff -r 89cc3dfb383b -r 571ce2bc0b64 src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Wed Mar 14 17:40:00 2012 +0100
+++ b/src/ZF/Ordinal.thy	Wed Mar 14 17:19:30 2012 +0000
@@ -236,7 +236,7 @@
 done
 
 
-(** Recall that  @{term"i \<le> j"}  abbreviates  @{term"i<succ(j)"} !! **)
+text{* Recall that  @{term"i \<le> j"}  abbreviates  @{term"i<succ(j)"} !! *}
 
 lemma le_iff: "i \<le> j <-> i<j | (i=j & Ord(j))"
 by (unfold lt_def, blast)
@@ -335,12 +335,11 @@
 done
 
 (*Induction over an ordinal*)
-lemmas Ord_induct [consumes 2] = Transset_induct [OF _ Ord_is_Transset]
-lemmas Ord_induct_rule = Ord_induct [rule_format, consumes 2]
+lemmas Ord_induct [consumes 2] = Transset_induct [rule_format, OF _ Ord_is_Transset]
 
 (*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
 
-lemma trans_induct [consumes 1]:
+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)"
@@ -348,10 +347,8 @@
 apply (blast intro: Ord_succ [THEN Ord_in_Ord])
 done
 
-lemmas trans_induct_rule = trans_induct [rule_format, consumes 1]
 
-
-(*** Fundamental properties of the epsilon ordering (< on ordinals) ***)
+section{*Fundamental properties of the epsilon ordering (< on ordinals)*}
 
 
 subsubsection{*Proving That < is a Linear Ordering on the Ordinals*}
@@ -364,23 +361,27 @@
 apply (blast dest: Ord_trans)
 done
 
-(*The trichotomy law for ordinals!*)
+text{*The trichotomy law for ordinals*}
 lemma Ord_linear_lt:
-    "[| Ord(i);  Ord(j);  i<j ==> P;  i=j ==> P;  j<i ==> P |] ==> P"
+ assumes o: "Ord(i)" "Ord(j)"
+ obtains (lt) "i<j" | (eq) "i=j" | (gt) "j<i" 
 apply (simp add: lt_def)
-apply (rule_tac i1=i and j1=j in Ord_linear [THEN disjE], blast+)
+apply (rule_tac i1=i and j1=j in Ord_linear [THEN disjE])
+apply (blast intro: o)+
 done
 
 lemma Ord_linear2:
-    "[| Ord(i);  Ord(j);  i<j ==> P;  j \<le> i ==> P |]  ==> P"
+ assumes o: "Ord(i)" "Ord(j)"
+ obtains (lt) "i<j" | (ge) "j \<le> i" 
 apply (rule_tac i = i and j = j in Ord_linear_lt)
-apply (blast intro: leI le_eqI sym ) +
+apply (blast intro: leI le_eqI sym o) +
 done
 
 lemma Ord_linear_le:
-    "[| Ord(i);  Ord(j);  i \<le> j ==> P;  j \<le> i ==> P |]  ==> P"
+ assumes o: "Ord(i)" "Ord(j)"
+ obtains (le) "i \<le> j" | (ge) "j \<le> i" 
 apply (rule_tac i = i and j = j in Ord_linear_lt)
-apply (blast intro: leI le_eqI ) +
+apply (blast intro: leI le_eqI o) +
 done
 
 lemma le_imp_not_lt: "j \<le> i ==> ~ i<j"
@@ -701,12 +702,9 @@
 by (blast intro!: non_succ_LimitI Ord_0_lt)
 
 lemma Ord_cases:
-    "[| Ord(i);
-        i=0                          ==> P;
-        !!j. [| Ord(j); i=succ(j) |] ==> P;
-        Limit(i)                     ==> P
-     |] ==> P"
-by (drule Ord_cases_disj, blast)
+ assumes i: "Ord(i)"
+ obtains (0) "i=0" | (succ) j where "Ord(j)" "i=succ(j)" | (limit) "Limit(i)" 
+by (insert Ord_cases_disj [OF i], auto)
 
 lemma trans_induct3_raw:
      "[| Ord(i);
diff -r 89cc3dfb383b -r 571ce2bc0b64 src/ZF/ex/LList.thy
--- a/src/ZF/ex/LList.thy	Wed Mar 14 17:40:00 2012 +0100
+++ b/src/ZF/ex/LList.thy	Wed Mar 14 17:19:30 2012 +0000
@@ -106,15 +106,22 @@
 declare qunivD [dest!]
 declare Ord_in_Ord [elim!]
 
-lemma llist_quniv_lemma [rule_format]:
-     "Ord(i) ==> \<forall>l \<in> llist(quniv(A)). l \<inter> Vset(i) \<subseteq> univ(eclose(A))"
-apply (erule trans_induct)
-apply (rule ballI)
-apply (erule llist.cases)
-apply (simp_all add: QInl_def QInr_def llist.con_defs)
-(*LCons case: I simply can't get rid of the deepen_tac*)
-apply (deepen 2 intro: Ord_trans Int_lower1 [THEN subset_trans])
-done
+lemma llist_quniv_lemma:
+     "Ord(i) ==> l \<in> llist(quniv(A)) \<Longrightarrow> l \<inter> Vset(i) \<subseteq> univ(eclose(A))"
+proof (induct i arbitrary: l rule: trans_induct)
+  case (step i l)
+  show ?case using `l \<in> llist(quniv(A))`
+  proof (cases l rule: llist.cases)
+    case LNil thus ?thesis
+      by (simp add: QInl_def QInr_def llist.con_defs)
+  next
+    case (LCons a l) thus ?thesis using step.hyps
+    proof (simp add: QInl_def QInr_def llist.con_defs)
+      show "<1; <a; l>> \<inter> Vset(i) \<subseteq> univ(eclose(A))" using LCons `Ord(i)`
+        by (fast intro: step Ord_trans Int_lower1 [THEN subset_trans])
+    qed
+  qed
+qed
 
 lemma llist_quniv: "llist(quniv(A)) \<subseteq> quniv(A)"
 apply (rule qunivI [THEN subsetI])
@@ -134,14 +141,19 @@
 declare Ord_in_Ord [elim!] 
 
 (*Lemma for proving finality.  Unfold the lazy list; use induction hypothesis*)
-lemma lleq_Int_Vset_subset [rule_format]:
-     "Ord(i) ==> \<forall>l l'. <l,l'> \<in> lleq(A) \<longrightarrow> l \<inter> Vset(i) \<subseteq> l'"
-apply (erule trans_induct)
-apply (intro allI impI)
-apply (erule lleq.cases)
-apply (unfold QInr_def llist.con_defs, safe)
-apply (fast elim!: Ord_trans bspec [elim_format])
-done
+lemma lleq_Int_Vset_subset:
+     "Ord(i) ==> <l,l'> \<in> lleq(A) \<Longrightarrow> l \<inter> Vset(i) \<subseteq> l'"
+proof (induct i arbitrary: l l' rule: trans_induct)
+  case (step i l l')
+  show ?case using `\<langle>l, l'\<rangle> \<in> lleq(A)`
+  proof (cases rule: lleq.cases)
+    case LNil thus ?thesis
+      by (auto simp add: QInr_def llist.con_defs)
+  next
+    case (LCons a l l') thus ?thesis using step.hyps
+      by (auto simp add: QInr_def llist.con_defs intro: Ord_trans)
+  qed
+qed
 
 (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
 lemma lleq_symmetric: "<l,l'> \<in> lleq(A) ==> <l',l> \<in> lleq(A)"
@@ -208,15 +220,22 @@
 
 (*Reasoning borrowed from lleq.ML; a similar proof works for all
   "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
-lemma flip_llist_quniv_lemma [rule_format]:
-     "Ord(i) ==> \<forall>l \<in> llist(bool). flip(l) \<inter> Vset(i) \<subseteq> univ(eclose(bool))"
-apply (erule trans_induct)
-apply (rule ballI)
-apply (erule llist.cases, simp_all)
-apply (simp_all add: QInl_def QInr_def llist.con_defs)
-(*LCons case: I simply can't get rid of the deepen_tac*)
-apply (deepen 2 intro: Ord_trans Int_lower1 [THEN subset_trans])
-done
+lemma flip_llist_quniv_lemma:
+     "Ord(i) ==> l \<in> llist(bool) \<Longrightarrow> flip(l) \<inter> Vset(i) \<subseteq> univ(eclose(bool))"
+proof (induct i arbitrary: l rule: trans_induct)
+  case (step i l)
+  show ?case using `l \<in> llist(bool)`
+  proof (cases l rule: llist.cases)
+    case LNil thus ?thesis
+      by (simp, simp add: QInl_def QInr_def llist.con_defs)
+  next
+    case (LCons a l) thus ?thesis using step.hyps
+    proof (simp, simp add: QInl_def QInr_def llist.con_defs)
+      show "<1; <not(a); flip(l)>> \<inter> Vset(i) \<subseteq> univ(eclose(bool))" using LCons step.hyps
+        by (auto intro: Ord_trans) 
+    qed
+  qed
+qed
 
 lemma flip_in_quniv: "l \<in> llist(bool) ==> flip(l) \<in> quniv(bool)"
 by (rule flip_llist_quniv_lemma [THEN Int_Vset_subset, THEN qunivI], assumption+)