structured case and induct rules
authorpaulson
Wed Mar 14 17:19:08 2012 +0000 (2012-03-14)
changeset 4693538ecb2dc3636
parent 46929 f159e227703a
child 46936 571ce2bc0b64
structured case and induct rules
src/ZF/Cardinal.thy
src/ZF/CardinalArith.thy
src/ZF/Nat_ZF.thy
src/ZF/Ordinal.thy
src/ZF/ex/LList.thy
     1.1 --- a/src/ZF/Cardinal.thy	Wed Mar 14 14:53:48 2012 +0100
     1.2 +++ b/src/ZF/Cardinal.thy	Wed Mar 14 17:19:08 2012 +0000
     1.3 @@ -540,15 +540,21 @@
     1.4  done
     1.5  
     1.6  
     1.7 -lemma nat_lepoll_imp_le [rule_format]:
     1.8 -     "m \<in> nat ==> \<forall>n\<in>nat. m \<lesssim> n \<longrightarrow> m \<le> n"
     1.9 -apply (induct_tac m)
    1.10 -apply (blast intro!: nat_0_le)
    1.11 -apply (rule ballI)
    1.12 -apply (erule_tac n = n in natE)
    1.13 -apply (simp (no_asm_simp) add: lepoll_def inj_def)
    1.14 -apply (blast intro!: succ_leI dest!: succ_lepoll_succD)
    1.15 -done
    1.16 +lemma nat_lepoll_imp_le:
    1.17 +     "m \<in> nat ==> n \<in> nat \<Longrightarrow> m \<lesssim> n \<Longrightarrow> m \<le> n"
    1.18 +proof (induct m arbitrary: n rule: nat_induct)
    1.19 +  case 0 thus ?case by (blast intro!: nat_0_le)
    1.20 +next
    1.21 +  case (succ m)
    1.22 +  show ?case  using `n \<in> nat`
    1.23 +    proof (cases rule: natE)
    1.24 +      case 0 thus ?thesis using succ
    1.25 +        by (simp add: lepoll_def inj_def)
    1.26 +    next
    1.27 +      case (succ n') thus ?thesis using succ.hyps ` succ(m) \<lesssim> n`
    1.28 +        by (blast intro!: succ_leI dest!: succ_lepoll_succD)
    1.29 +    qed
    1.30 +qed
    1.31  
    1.32  lemma nat_eqpoll_iff: "[| m \<in> nat; n: nat |] ==> m \<approx> n \<longleftrightarrow> m = n"
    1.33  apply (rule iffI)
     2.1 --- a/src/ZF/CardinalArith.thy	Wed Mar 14 14:53:48 2012 +0100
     2.2 +++ b/src/ZF/CardinalArith.thy	Wed Mar 14 17:19:08 2012 +0000
     2.3 @@ -628,28 +628,25 @@
     2.4    assumes IK: "InfCard(K)" shows "InfCard(K) ==> K \<otimes> K = K"
     2.5  proof -
     2.6    have  OK: "Ord(K)" using IK by (simp add: Card_is_Ord InfCard_is_Card) 
     2.7 -  have "InfCard(K) \<longrightarrow> K \<otimes> K = K"
     2.8 -    proof (rule trans_induct [OF OK], rule impI)
     2.9 -      fix i
    2.10 -      assume i: "Ord(i)" "InfCard(i)"
    2.11 -         and ih: " \<forall>y\<in>i. InfCard(y) \<longrightarrow> y \<otimes> y = y"
    2.12 -      show "i \<otimes> i = i"
    2.13 -        proof (rule le_anti_sym)
    2.14 -          have "|i \<times> i| = |ordertype(i \<times> i, csquare_rel(i))|" 
    2.15 -            by (rule cardinal_cong, 
    2.16 -                simp add: i well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll])
    2.17 -          hence "i \<otimes> i \<le> ordertype(i \<times> i, csquare_rel(i))" using i
    2.18 -            by (simp add: cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype])
    2.19 -          moreover
    2.20 -          have "ordertype(i \<times> i, csquare_rel(i)) \<le> i" using ih i
    2.21 -            by (simp add: ordertype_csquare_le) 
    2.22 -          ultimately show "i \<otimes> i \<le> i" by (rule le_trans)
    2.23 -        next
    2.24 -          show "i \<le> i \<otimes> i" using i
    2.25 -            by (blast intro: cmult_square_le InfCard_is_Card) 
    2.26 -        qed
    2.27 +  show "InfCard(K) ==> K \<otimes> K = K" using OK
    2.28 +  proof (induct rule: trans_induct)
    2.29 +    case (step i)
    2.30 +    show "i \<otimes> i = i"
    2.31 +    proof (rule le_anti_sym)
    2.32 +      have "|i \<times> i| = |ordertype(i \<times> i, csquare_rel(i))|" 
    2.33 +        by (rule cardinal_cong, 
    2.34 +          simp add: step.hyps well_ord_csquare [THEN ordermap_bij, THEN bij_imp_eqpoll])
    2.35 +      hence "i \<otimes> i \<le> ordertype(i \<times> i, csquare_rel(i))" 
    2.36 +        by (simp add: step.hyps cmult_def Ord_cardinal_le well_ord_csquare [THEN Ord_ordertype])
    2.37 +      moreover
    2.38 +      have "ordertype(i \<times> i, csquare_rel(i)) \<le> i" using step
    2.39 +        by (simp add: ordertype_csquare_le) 
    2.40 +      ultimately show "i \<otimes> i \<le> i" by (rule le_trans)
    2.41 +    next
    2.42 +      show "i \<le> i \<otimes> i" using step
    2.43 +        by (blast intro: cmult_square_le InfCard_is_Card) 
    2.44      qed
    2.45 -  thus ?thesis using IK ..
    2.46 +  qed
    2.47  qed
    2.48  
    2.49  (*Corollary for arbitrary well-ordered sets (all sets, assuming AC)*)
    2.50 @@ -910,10 +907,15 @@
    2.51    finally show ?thesis .
    2.52  qed
    2.53  
    2.54 -lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i \<subseteq> nat \<longrightarrow> i \<in> nat | i=nat"
    2.55 -apply (erule trans_induct3, auto)
    2.56 -apply (blast dest!: nat_le_Limit [THEN le_imp_subset])
    2.57 -done
    2.58 +lemma Ord_subset_natD [rule_format]: "Ord(i) ==> i \<subseteq> nat \<Longrightarrow> i \<in> nat | i=nat"
    2.59 +proof (induct i rule: trans_induct3)
    2.60 +  case 0 thus ?case by auto
    2.61 +next
    2.62 +  case (succ i) thus ?case by auto
    2.63 +next
    2.64 +  case (limit l) thus ?case
    2.65 +    by (blast dest: nat_le_Limit le_imp_subset)
    2.66 +qed
    2.67  
    2.68  lemma Ord_nat_subset_into_Card: "[| Ord(i); i \<subseteq> nat |] ==> Card(i)"
    2.69  by (blast dest: Ord_subset_natD intro: Card_nat nat_into_Card)
     3.1 --- a/src/ZF/Nat_ZF.thy	Wed Mar 14 14:53:48 2012 +0100
     3.2 +++ b/src/ZF/Nat_ZF.thy	Wed Mar 14 17:19:08 2012 +0000
     3.3 @@ -87,14 +87,16 @@
     3.4  
     3.5  (*Mathematical induction*)
     3.6  lemma nat_induct [case_names 0 succ, induct set: nat]:
     3.7 -    "[| n: nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) |] ==> P(n)"
     3.8 +    "[| n \<in> nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) |] ==> P(n)"
     3.9  by (erule def_induct [OF nat_def nat_bnd_mono], blast)
    3.10  
    3.11  lemma natE:
    3.12 -    "[| n: nat;  n=0 ==> P;  !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P"
    3.13 -by (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto)
    3.14 + assumes "n \<in> nat"
    3.15 + obtains (0) "n=0" | (succ) x where "x \<in> nat" "n=succ(x)" 
    3.16 +using assms
    3.17 +by (rule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE]) auto
    3.18  
    3.19 -lemma nat_into_Ord [simp]: "n: nat ==> Ord(n)"
    3.20 +lemma nat_into_Ord [simp]: "n \<in> nat ==> Ord(n)"
    3.21  by (erule nat_induct, auto)
    3.22  
    3.23  (* @{term"i: nat ==> 0 \<le> i"}; same thing as @{term"0<succ(i)"}  *)
    3.24 @@ -123,7 +125,7 @@
    3.25  lemma succ_natD: "succ(i): nat ==> i: nat"
    3.26  by (rule Ord_trans [OF succI1], auto)
    3.27  
    3.28 -lemma nat_succ_iff [iff]: "succ(n): nat \<longleftrightarrow> n: nat"
    3.29 +lemma nat_succ_iff [iff]: "succ(n): nat \<longleftrightarrow> n \<in> nat"
    3.30  by (blast dest!: succ_natD)
    3.31  
    3.32  lemma nat_le_Limit: "Limit(i) ==> nat \<le> i"
    3.33 @@ -138,7 +140,7 @@
    3.34  (* [| succ(i): k;  k: nat |] ==> i: k *)
    3.35  lemmas succ_in_naturalD = Ord_trans [OF succI1 _ nat_into_Ord]
    3.36  
    3.37 -lemma lt_nat_in_nat: "[| m<n;  n: nat |] ==> m: nat"
    3.38 +lemma lt_nat_in_nat: "[| m<n;  n \<in> nat |] ==> m: nat"
    3.39  apply (erule ltE)
    3.40  apply (erule Ord_trans, assumption, simp)
    3.41  done
    3.42 @@ -158,7 +160,7 @@
    3.43  
    3.44  
    3.45  lemma nat_induct_from_lemma [rule_format]:
    3.46 -    "[| n: nat;  m: nat;
    3.47 +    "[| n \<in> nat;  m: nat;
    3.48          !!x. [| x: nat;  m \<le> x;  P(x) |] ==> P(succ(x)) |]
    3.49       ==> m \<le> n \<longrightarrow> P(m) \<longrightarrow> P(n)"
    3.50  apply (erule nat_induct)
    3.51 @@ -167,7 +169,7 @@
    3.52  
    3.53  (*Induction starting from m rather than 0*)
    3.54  lemma nat_induct_from:
    3.55 -    "[| m \<le> n;  m: nat;  n: nat;
    3.56 +    "[| m \<le> n;  m: nat;  n \<in> nat;
    3.57          P(m);
    3.58          !!x. [| x: nat;  m \<le> x;  P(x) |] ==> P(succ(x)) |]
    3.59       ==> P(n)"
    3.60 @@ -176,7 +178,7 @@
    3.61  
    3.62  (*Induction suitable for subtraction and less-than*)
    3.63  lemma diff_induct [case_names 0 0_succ succ_succ, consumes 2]:
    3.64 -    "[| m: nat;  n: nat;
    3.65 +    "[| m: nat;  n \<in> nat;
    3.66          !!x. x: nat ==> P(x,0);
    3.67          !!y. y: nat ==> P(0,succ(y));
    3.68          !!x y. [| x: nat;  y: nat;  P(x,y) |] ==> P(succ(x),succ(y)) |]
    3.69 @@ -201,7 +203,7 @@
    3.70  done
    3.71  
    3.72  lemma succ_lt_induct:
    3.73 -    "[| m<n;  n: nat;
    3.74 +    "[| m<n;  n \<in> nat;
    3.75          P(m,succ(m));
    3.76          !!x. [| x: nat;  P(m,x) |] ==> P(m,succ(x)) |]
    3.77       ==> P(m,n)"
    3.78 @@ -241,7 +243,7 @@
    3.79  by (simp add: nat_case_def)
    3.80  
    3.81  lemma nat_case_type [TC]:
    3.82 -    "[| n: nat;  a: C(0);  !!m. m: nat ==> b(m): C(succ(m)) |]
    3.83 +    "[| n \<in> nat;  a: C(0);  !!m. m: nat ==> b(m): C(succ(m)) |]
    3.84       ==> nat_case(a,b,n) \<in> C(n)";
    3.85  by (erule nat_induct, auto)
    3.86  
     4.1 --- a/src/ZF/Ordinal.thy	Wed Mar 14 14:53:48 2012 +0100
     4.2 +++ b/src/ZF/Ordinal.thy	Wed Mar 14 17:19:08 2012 +0000
     4.3 @@ -236,7 +236,7 @@
     4.4  done
     4.5  
     4.6  
     4.7 -(** Recall that  @{term"i \<le> j"}  abbreviates  @{term"i<succ(j)"} !! **)
     4.8 +text{* Recall that  @{term"i \<le> j"}  abbreviates  @{term"i<succ(j)"} !! *}
     4.9  
    4.10  lemma le_iff: "i \<le> j <-> i<j | (i=j & Ord(j))"
    4.11  by (unfold lt_def, blast)
    4.12 @@ -335,12 +335,11 @@
    4.13  done
    4.14  
    4.15  (*Induction over an ordinal*)
    4.16 -lemmas Ord_induct [consumes 2] = Transset_induct [OF _ Ord_is_Transset]
    4.17 -lemmas Ord_induct_rule = Ord_induct [rule_format, consumes 2]
    4.18 +lemmas Ord_induct [consumes 2] = Transset_induct [rule_format, OF _ Ord_is_Transset]
    4.19  
    4.20  (*Induction over the class of ordinals -- a useful corollary of Ord_induct*)
    4.21  
    4.22 -lemma trans_induct [consumes 1]:
    4.23 +lemma trans_induct [rule_format, consumes 1, case_names step]:
    4.24      "[| Ord(i);
    4.25          !!x.[| Ord(x);  \<forall>y\<in>x. P(y) |] ==> P(x) |]
    4.26       ==>  P(i)"
    4.27 @@ -348,10 +347,8 @@
    4.28  apply (blast intro: Ord_succ [THEN Ord_in_Ord])
    4.29  done
    4.30  
    4.31 -lemmas trans_induct_rule = trans_induct [rule_format, consumes 1]
    4.32  
    4.33 -
    4.34 -(*** Fundamental properties of the epsilon ordering (< on ordinals) ***)
    4.35 +section{*Fundamental properties of the epsilon ordering (< on ordinals)*}
    4.36  
    4.37  
    4.38  subsubsection{*Proving That < is a Linear Ordering on the Ordinals*}
    4.39 @@ -364,23 +361,27 @@
    4.40  apply (blast dest: Ord_trans)
    4.41  done
    4.42  
    4.43 -(*The trichotomy law for ordinals!*)
    4.44 +text{*The trichotomy law for ordinals*}
    4.45  lemma Ord_linear_lt:
    4.46 -    "[| Ord(i);  Ord(j);  i<j ==> P;  i=j ==> P;  j<i ==> P |] ==> P"
    4.47 + assumes o: "Ord(i)" "Ord(j)"
    4.48 + obtains (lt) "i<j" | (eq) "i=j" | (gt) "j<i" 
    4.49  apply (simp add: lt_def)
    4.50 -apply (rule_tac i1=i and j1=j in Ord_linear [THEN disjE], blast+)
    4.51 +apply (rule_tac i1=i and j1=j in Ord_linear [THEN disjE])
    4.52 +apply (blast intro: o)+
    4.53  done
    4.54  
    4.55  lemma Ord_linear2:
    4.56 -    "[| Ord(i);  Ord(j);  i<j ==> P;  j \<le> i ==> P |]  ==> P"
    4.57 + assumes o: "Ord(i)" "Ord(j)"
    4.58 + obtains (lt) "i<j" | (ge) "j \<le> i" 
    4.59  apply (rule_tac i = i and j = j in Ord_linear_lt)
    4.60 -apply (blast intro: leI le_eqI sym ) +
    4.61 +apply (blast intro: leI le_eqI sym o) +
    4.62  done
    4.63  
    4.64  lemma Ord_linear_le:
    4.65 -    "[| Ord(i);  Ord(j);  i \<le> j ==> P;  j \<le> i ==> P |]  ==> P"
    4.66 + assumes o: "Ord(i)" "Ord(j)"
    4.67 + obtains (le) "i \<le> j" | (ge) "j \<le> i" 
    4.68  apply (rule_tac i = i and j = j in Ord_linear_lt)
    4.69 -apply (blast intro: leI le_eqI ) +
    4.70 +apply (blast intro: leI le_eqI o) +
    4.71  done
    4.72  
    4.73  lemma le_imp_not_lt: "j \<le> i ==> ~ i<j"
    4.74 @@ -701,12 +702,9 @@
    4.75  by (blast intro!: non_succ_LimitI Ord_0_lt)
    4.76  
    4.77  lemma Ord_cases:
    4.78 -    "[| Ord(i);
    4.79 -        i=0                          ==> P;
    4.80 -        !!j. [| Ord(j); i=succ(j) |] ==> P;
    4.81 -        Limit(i)                     ==> P
    4.82 -     |] ==> P"
    4.83 -by (drule Ord_cases_disj, blast)
    4.84 + assumes i: "Ord(i)"
    4.85 + obtains (0) "i=0" | (succ) j where "Ord(j)" "i=succ(j)" | (limit) "Limit(i)" 
    4.86 +by (insert Ord_cases_disj [OF i], auto)
    4.87  
    4.88  lemma trans_induct3_raw:
    4.89       "[| Ord(i);
     5.1 --- a/src/ZF/ex/LList.thy	Wed Mar 14 14:53:48 2012 +0100
     5.2 +++ b/src/ZF/ex/LList.thy	Wed Mar 14 17:19:08 2012 +0000
     5.3 @@ -106,15 +106,22 @@
     5.4  declare qunivD [dest!]
     5.5  declare Ord_in_Ord [elim!]
     5.6  
     5.7 -lemma llist_quniv_lemma [rule_format]:
     5.8 -     "Ord(i) ==> \<forall>l \<in> llist(quniv(A)). l \<inter> Vset(i) \<subseteq> univ(eclose(A))"
     5.9 -apply (erule trans_induct)
    5.10 -apply (rule ballI)
    5.11 -apply (erule llist.cases)
    5.12 -apply (simp_all add: QInl_def QInr_def llist.con_defs)
    5.13 -(*LCons case: I simply can't get rid of the deepen_tac*)
    5.14 -apply (deepen 2 intro: Ord_trans Int_lower1 [THEN subset_trans])
    5.15 -done
    5.16 +lemma llist_quniv_lemma:
    5.17 +     "Ord(i) ==> l \<in> llist(quniv(A)) \<Longrightarrow> l \<inter> Vset(i) \<subseteq> univ(eclose(A))"
    5.18 +proof (induct i arbitrary: l rule: trans_induct)
    5.19 +  case (step i l)
    5.20 +  show ?case using `l \<in> llist(quniv(A))`
    5.21 +  proof (cases l rule: llist.cases)
    5.22 +    case LNil thus ?thesis
    5.23 +      by (simp add: QInl_def QInr_def llist.con_defs)
    5.24 +  next
    5.25 +    case (LCons a l) thus ?thesis using step.hyps
    5.26 +    proof (simp add: QInl_def QInr_def llist.con_defs)
    5.27 +      show "<1; <a; l>> \<inter> Vset(i) \<subseteq> univ(eclose(A))" using LCons `Ord(i)`
    5.28 +        by (fast intro: step Ord_trans Int_lower1 [THEN subset_trans])
    5.29 +    qed
    5.30 +  qed
    5.31 +qed
    5.32  
    5.33  lemma llist_quniv: "llist(quniv(A)) \<subseteq> quniv(A)"
    5.34  apply (rule qunivI [THEN subsetI])
    5.35 @@ -134,14 +141,19 @@
    5.36  declare Ord_in_Ord [elim!] 
    5.37  
    5.38  (*Lemma for proving finality.  Unfold the lazy list; use induction hypothesis*)
    5.39 -lemma lleq_Int_Vset_subset [rule_format]:
    5.40 -     "Ord(i) ==> \<forall>l l'. <l,l'> \<in> lleq(A) \<longrightarrow> l \<inter> Vset(i) \<subseteq> l'"
    5.41 -apply (erule trans_induct)
    5.42 -apply (intro allI impI)
    5.43 -apply (erule lleq.cases)
    5.44 -apply (unfold QInr_def llist.con_defs, safe)
    5.45 -apply (fast elim!: Ord_trans bspec [elim_format])
    5.46 -done
    5.47 +lemma lleq_Int_Vset_subset:
    5.48 +     "Ord(i) ==> <l,l'> \<in> lleq(A) \<Longrightarrow> l \<inter> Vset(i) \<subseteq> l'"
    5.49 +proof (induct i arbitrary: l l' rule: trans_induct)
    5.50 +  case (step i l l')
    5.51 +  show ?case using `\<langle>l, l'\<rangle> \<in> lleq(A)`
    5.52 +  proof (cases rule: lleq.cases)
    5.53 +    case LNil thus ?thesis
    5.54 +      by (auto simp add: QInr_def llist.con_defs)
    5.55 +  next
    5.56 +    case (LCons a l l') thus ?thesis using step.hyps
    5.57 +      by (auto simp add: QInr_def llist.con_defs intro: Ord_trans)
    5.58 +  qed
    5.59 +qed
    5.60  
    5.61  (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
    5.62  lemma lleq_symmetric: "<l,l'> \<in> lleq(A) ==> <l',l> \<in> lleq(A)"
    5.63 @@ -208,15 +220,22 @@
    5.64  
    5.65  (*Reasoning borrowed from lleq.ML; a similar proof works for all
    5.66    "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
    5.67 -lemma flip_llist_quniv_lemma [rule_format]:
    5.68 -     "Ord(i) ==> \<forall>l \<in> llist(bool). flip(l) \<inter> Vset(i) \<subseteq> univ(eclose(bool))"
    5.69 -apply (erule trans_induct)
    5.70 -apply (rule ballI)
    5.71 -apply (erule llist.cases, simp_all)
    5.72 -apply (simp_all add: QInl_def QInr_def llist.con_defs)
    5.73 -(*LCons case: I simply can't get rid of the deepen_tac*)
    5.74 -apply (deepen 2 intro: Ord_trans Int_lower1 [THEN subset_trans])
    5.75 -done
    5.76 +lemma flip_llist_quniv_lemma:
    5.77 +     "Ord(i) ==> l \<in> llist(bool) \<Longrightarrow> flip(l) \<inter> Vset(i) \<subseteq> univ(eclose(bool))"
    5.78 +proof (induct i arbitrary: l rule: trans_induct)
    5.79 +  case (step i l)
    5.80 +  show ?case using `l \<in> llist(bool)`
    5.81 +  proof (cases l rule: llist.cases)
    5.82 +    case LNil thus ?thesis
    5.83 +      by (simp, simp add: QInl_def QInr_def llist.con_defs)
    5.84 +  next
    5.85 +    case (LCons a l) thus ?thesis using step.hyps
    5.86 +    proof (simp, simp add: QInl_def QInr_def llist.con_defs)
    5.87 +      show "<1; <not(a); flip(l)>> \<inter> Vset(i) \<subseteq> univ(eclose(bool))" using LCons step.hyps
    5.88 +        by (auto intro: Ord_trans) 
    5.89 +    qed
    5.90 +  qed
    5.91 +qed
    5.92  
    5.93  lemma flip_in_quniv: "l \<in> llist(bool) ==> flip(l) \<in> quniv(bool)"
    5.94  by (rule flip_llist_quniv_lemma [THEN Int_Vset_subset, THEN qunivI], assumption+)