- Renamed inductive2 to inductive
authorberghofe
Wed Jul 11 11:23:24 2007 +0200 (2007-07-11)
changeset 23750a1db5f819d00
parent 23749 ac6d3a8d22b5
child 23751 a7c7edf2c5ad
- Renamed inductive2 to inductive
- Renamed some theorems about transitive closure for predicates
src/HOL/Lambda/Commutation.thy
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/InductTermi.thy
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/ListBeta.thy
src/HOL/Lambda/ListOrder.thy
src/HOL/Lambda/ParRed.thy
src/HOL/Lambda/StrongNorm.thy
src/HOL/Lambda/Type.thy
src/HOL/Lambda/WeakNorm.thy
     1.1 --- a/src/HOL/Lambda/Commutation.thy	Wed Jul 11 11:22:02 2007 +0200
     1.2 +++ b/src/HOL/Lambda/Commutation.thy	Wed Jul 11 11:23:24 2007 +0200
     1.3 @@ -58,9 +58,9 @@
     1.4      "square R S S T ==> square (R^**) S S (T^**)"
     1.5    apply (unfold square_def)
     1.6    apply (intro strip)
     1.7 -  apply (erule rtrancl_induct')
     1.8 +  apply (erule rtranclp_induct)
     1.9     apply blast
    1.10 -  apply (blast intro: rtrancl.rtrancl_into_rtrancl)
    1.11 +  apply (blast intro: rtranclp.rtrancl_into_rtrancl)
    1.12    done
    1.13  
    1.14  lemma square_rtrancl_reflcl_commute:
    1.15 @@ -110,14 +110,14 @@
    1.16  
    1.17  lemma confluent_Un:
    1.18      "[| confluent R; confluent S; commute (R^**) (S^**) |] ==> confluent (sup R S)"
    1.19 -  apply (rule rtrancl_Un_rtrancl' [THEN subst])
    1.20 +  apply (rule rtranclp_sup_rtranclp [THEN subst])
    1.21    apply (blast dest: diamond_Un intro: diamond_confluent)
    1.22    done
    1.23  
    1.24  lemma diamond_to_confluence:
    1.25      "[| diamond R; T \<le> R; R \<le> T^** |] ==> confluent T"
    1.26    apply (force intro: diamond_confluent
    1.27 -    dest: rtrancl_subset' [symmetric])
    1.28 +    dest: rtranclp_subset [symmetric])
    1.29    done
    1.30  
    1.31  
    1.32 @@ -128,12 +128,12 @@
    1.33    apply (tactic {* safe_tac HOL_cs *})
    1.34     apply (tactic {*
    1.35       blast_tac (HOL_cs addIs
    1.36 -       [thm "sup_ge2" RS thm "rtrancl_mono'" RS thm "predicate2D" RS thm "rtrancl_trans'",
    1.37 -        thm "rtrancl_converseI'", thm "conversepI",
    1.38 -        thm "sup_ge1" RS thm "rtrancl_mono'" RS thm "predicate2D"]) 1 *})
    1.39 -  apply (erule rtrancl_induct')
    1.40 +       [thm "sup_ge2" RS thm "rtranclp_mono" RS thm "predicate2D" RS thm "rtranclp_trans",
    1.41 +        thm "rtranclp_converseI", thm "conversepI",
    1.42 +        thm "sup_ge1" RS thm "rtranclp_mono" RS thm "predicate2D"]) 1 *})
    1.43 +  apply (erule rtranclp_induct)
    1.44     apply blast
    1.45 -  apply (blast del: rtrancl.rtrancl_refl intro: rtrancl_trans')
    1.46 +  apply (blast del: rtranclp.rtrancl_refl intro: rtranclp_trans)
    1.47    done
    1.48  
    1.49  
    1.50 @@ -152,7 +152,7 @@
    1.51    case (less x b c)
    1.52    have xc: "R\<^sup>*\<^sup>* x c" by fact
    1.53    have xb: "R\<^sup>*\<^sup>* x b" by fact thus ?case
    1.54 -  proof (rule converse_rtranclE')
    1.55 +  proof (rule converse_rtranclpE)
    1.56      assume "x = b"
    1.57      with xc have "R\<^sup>*\<^sup>* b c" by simp
    1.58      thus ?thesis by iprover
    1.59 @@ -161,7 +161,7 @@
    1.60      assume xy: "R x y"
    1.61      assume yb: "R\<^sup>*\<^sup>* y b"
    1.62      from xc show ?thesis
    1.63 -    proof (rule converse_rtranclE')
    1.64 +    proof (rule converse_rtranclpE)
    1.65        assume "x = c"
    1.66        with xb have "R\<^sup>*\<^sup>* c b" by simp
    1.67        thus ?thesis by iprover
    1.68 @@ -175,11 +175,11 @@
    1.69        from this and yb yu have "\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* u d" by (rule less)
    1.70        then obtain v where bv: "R\<^sup>*\<^sup>* b v" and uv: "R\<^sup>*\<^sup>* u v" by iprover
    1.71        from xy' have "R\<inverse>\<inverse> y' x" ..
    1.72 -      moreover from y'u and uv have "R\<^sup>*\<^sup>* y' v" by (rule rtrancl_trans')
    1.73 +      moreover from y'u and uv have "R\<^sup>*\<^sup>* y' v" by (rule rtranclp_trans)
    1.74        moreover note y'c
    1.75        ultimately have "\<exists>d. R\<^sup>*\<^sup>* v d \<and> R\<^sup>*\<^sup>* c d" by (rule less)
    1.76        then obtain w where vw: "R\<^sup>*\<^sup>* v w" and cw: "R\<^sup>*\<^sup>* c w" by iprover
    1.77 -      from bv vw have "R\<^sup>*\<^sup>* b w" by (rule rtrancl_trans')
    1.78 +      from bv vw have "R\<^sup>*\<^sup>* b w" by (rule rtranclp_trans)
    1.79        with cw show ?thesis by iprover
    1.80      qed
    1.81    qed
    1.82 @@ -206,7 +206,7 @@
    1.83    have xc: "R\<^sup>*\<^sup>* x c" by fact
    1.84    have xb: "R\<^sup>*\<^sup>* x b" by fact
    1.85    thus ?case
    1.86 -  proof (rule converse_rtranclE')
    1.87 +  proof (rule converse_rtranclpE)
    1.88      assume "x = b"
    1.89      with xc have "R\<^sup>*\<^sup>* b c" by simp
    1.90      thus ?thesis by iprover
    1.91 @@ -215,7 +215,7 @@
    1.92      assume xy: "R x y"
    1.93      assume yb: "R\<^sup>*\<^sup>* y b"
    1.94      from xc show ?thesis
    1.95 -    proof (rule converse_rtranclE')
    1.96 +    proof (rule converse_rtranclpE)
    1.97        assume "x = c"
    1.98        with xb have "R\<^sup>*\<^sup>* c b" by simp
    1.99        thus ?thesis by iprover
   1.100 @@ -226,8 +226,8 @@
   1.101        with xy obtain u where u: "R\<^sup>*\<^sup>* y u" "R\<^sup>*\<^sup>* y' u"
   1.102          by (blast dest: lc)
   1.103        from yb u y'c show ?thesis
   1.104 -        by (blast del: rtrancl.rtrancl_refl
   1.105 -            intro: rtrancl_trans'
   1.106 +        by (blast del: rtranclp.rtrancl_refl
   1.107 +            intro: rtranclp_trans
   1.108              dest: IH [OF conversepI, OF xy] IH [OF conversepI, OF xy'])
   1.109      qed
   1.110    qed
     2.1 --- a/src/HOL/Lambda/Eta.thy	Wed Jul 11 11:22:02 2007 +0200
     2.2 +++ b/src/HOL/Lambda/Eta.thy	Wed Jul 11 11:23:24 2007 +0200
     2.3 @@ -18,7 +18,7 @@
     2.4    "free (s \<degree> t) i = (free s i \<or> free t i)"
     2.5    "free (Abs s) i = free s (i + 1)"
     2.6  
     2.7 -inductive2 eta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<eta>" 50)
     2.8 +inductive eta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<eta>" 50)
     2.9    where
    2.10      eta [simp, intro]: "\<not> free s 0 ==> Abs (s \<degree> Var 0) \<rightarrow>\<^sub>\<eta> s[dummy/0]"
    2.11    | appL [simp, intro]: "s \<rightarrow>\<^sub>\<eta> t ==> s \<degree> u \<rightarrow>\<^sub>\<eta> t \<degree> u"
    2.12 @@ -37,7 +37,7 @@
    2.13    eta_reds  (infixl "\<rightarrow>\<^sub>\<eta>\<^sup>*" 50) and
    2.14    eta_red0  (infixl "\<rightarrow>\<^sub>\<eta>\<^sup>=" 50)
    2.15  
    2.16 -inductive_cases2 eta_cases [elim!]:
    2.17 +inductive_cases eta_cases [elim!]:
    2.18    "Abs s \<rightarrow>\<^sub>\<eta> z"
    2.19    "s \<degree> t \<rightarrow>\<^sub>\<eta> u"
    2.20    "Var i \<rightarrow>\<^sub>\<eta> t"
    2.21 @@ -103,19 +103,19 @@
    2.22  subsection "Congruence rules for eta*"
    2.23  
    2.24  lemma rtrancl_eta_Abs: "s \<rightarrow>\<^sub>\<eta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<eta>\<^sup>* Abs s'"
    2.25 -  by (induct set: rtrancl)
    2.26 -    (blast intro: rtrancl.rtrancl_into_rtrancl)+
    2.27 +  by (induct set: rtranclp)
    2.28 +    (blast intro: rtranclp.rtrancl_into_rtrancl)+
    2.29  
    2.30  lemma rtrancl_eta_AppL: "s \<rightarrow>\<^sub>\<eta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<eta>\<^sup>* s' \<degree> t"
    2.31 -  by (induct set: rtrancl)
    2.32 -    (blast intro: rtrancl.rtrancl_into_rtrancl)+
    2.33 +  by (induct set: rtranclp)
    2.34 +    (blast intro: rtranclp.rtrancl_into_rtrancl)+
    2.35  
    2.36  lemma rtrancl_eta_AppR: "t \<rightarrow>\<^sub>\<eta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<eta>\<^sup>* s \<degree> t'"
    2.37 -  by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
    2.38 +  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
    2.39  
    2.40  lemma rtrancl_eta_App:
    2.41      "[| s \<rightarrow>\<^sub>\<eta>\<^sup>* s'; t \<rightarrow>\<^sub>\<eta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<eta>\<^sup>* s' \<degree> t'"
    2.42 -  by (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans')
    2.43 +  by (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtranclp_trans)
    2.44  
    2.45  
    2.46  subsection "Commutation of beta and eta"
    2.47 @@ -149,7 +149,7 @@
    2.48  lemma rtrancl_eta_subst'':
    2.49    assumes eta: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t"
    2.50    shows "u[s/i] \<rightarrow>\<^sub>\<eta>\<^sup>* u[t/i]" using eta
    2.51 -  by induct (iprover intro: rtrancl_eta_subst rtrancl_trans')+
    2.52 +  by induct (iprover intro: rtrancl_eta_subst rtranclp_trans)+
    2.53  
    2.54  lemma square_beta_eta: "square beta eta (eta^**) (beta^==)"
    2.55    apply (unfold square_def)
    2.56 @@ -361,7 +361,7 @@
    2.57      by (auto dest: eta_par_beta)
    2.58    from s' obtain t'' where s: "s => t''" and t'': "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* t'" using 2
    2.59      by blast
    2.60 -  from t'' and t' have "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* s'''" by (rule rtrancl_trans')
    2.61 +  from t'' and t' have "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* s'''" by (rule rtranclp_trans)
    2.62    with s show ?case by iprover
    2.63  qed
    2.64  
    2.65 @@ -381,7 +381,7 @@
    2.66      with t' obtain t'' where st: "t' => t''" and tu: "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* s''"
    2.67        by (auto dest: eta_postponement')
    2.68      from par_beta_subset_beta st have "t' \<rightarrow>\<^sub>\<beta>\<^sup>* t''" ..
    2.69 -    with s have "s \<rightarrow>\<^sub>\<beta>\<^sup>* t''" by (rule rtrancl_trans')
    2.70 +    with s have "s \<rightarrow>\<^sub>\<beta>\<^sup>* t''" by (rule rtranclp_trans)
    2.71      thus ?thesis using tu ..
    2.72    next
    2.73      assume "s' \<rightarrow>\<^sub>\<eta> s''"
     3.1 --- a/src/HOL/Lambda/InductTermi.thy	Wed Jul 11 11:22:02 2007 +0200
     3.2 +++ b/src/HOL/Lambda/InductTermi.thy	Wed Jul 11 11:23:24 2007 +0200
     3.3 @@ -14,7 +14,7 @@
     3.4  
     3.5  subsection {* Terminating lambda terms *}
     3.6  
     3.7 -inductive2 IT :: "dB => bool"
     3.8 +inductive IT :: "dB => bool"
     3.9    where
    3.10      Var [intro]: "listsp IT rs ==> IT (Var n \<degree>\<degree> rs)"
    3.11    | Lambda [intro]: "IT r ==> IT (Abs r)"
    3.12 @@ -24,33 +24,33 @@
    3.13  subsection {* Every term in IT terminates *}
    3.14  
    3.15  lemma double_induction_lemma [rule_format]:
    3.16 -  "termi beta s ==> \<forall>t. termi beta t -->
    3.17 -    (\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> termi beta (Abs r \<degree> s \<degree>\<degree> ss))"
    3.18 -  apply (erule acc_induct)
    3.19 +  "termip beta s ==> \<forall>t. termip beta t -->
    3.20 +    (\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> termip beta (Abs r \<degree> s \<degree>\<degree> ss))"
    3.21 +  apply (erule accp_induct)
    3.22    apply (rule allI)
    3.23    apply (rule impI)
    3.24    apply (erule thin_rl)
    3.25 -  apply (erule acc_induct)
    3.26 +  apply (erule accp_induct)
    3.27    apply clarify
    3.28 -  apply (rule accI)
    3.29 +  apply (rule accp.accI)
    3.30    apply (safe elim!: apps_betasE)
    3.31       apply assumption
    3.32      apply (blast intro: subst_preserves_beta apps_preserves_beta)
    3.33 -   apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI'
    3.34 -     dest: acc_downwards)  (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
    3.35 +   apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtranclp_converseI
    3.36 +     dest: accp_downwards)  (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
    3.37    apply (blast dest: apps_preserves_betas)
    3.38    done
    3.39  
    3.40 -lemma IT_implies_termi: "IT t ==> termi beta t"
    3.41 +lemma IT_implies_termi: "IT t ==> termip beta t"
    3.42    apply (induct set: IT)
    3.43 -    apply (drule rev_predicate1D [OF _ listsp_mono [where B="termi beta"]])
    3.44 +    apply (drule rev_predicate1D [OF _ listsp_mono [where B="termip beta"]])
    3.45      apply fast
    3.46      apply (drule lists_accD)
    3.47 -    apply (erule acc_induct)
    3.48 -    apply (rule accI)
    3.49 +    apply (erule accp_induct)
    3.50 +    apply (rule accp.accI)
    3.51      apply (blast dest: head_Var_reduction)
    3.52 -   apply (erule acc_induct)
    3.53 -   apply (rule accI)
    3.54 +   apply (erule accp_induct)
    3.55 +   apply (rule accp.accI)
    3.56     apply blast
    3.57    apply (blast intro: double_induction_lemma)
    3.58    done
    3.59 @@ -67,13 +67,13 @@
    3.60    "(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')"
    3.61    by (simp add: foldl_Cons [symmetric] del: foldl_Cons)
    3.62  
    3.63 -inductive_cases2 [elim!]:
    3.64 +inductive_cases [elim!]:
    3.65    "IT (Var n \<degree>\<degree> ss)"
    3.66    "IT (Abs t)"
    3.67    "IT (Abs r \<degree> s \<degree>\<degree> ts)"
    3.68  
    3.69 -theorem termi_implies_IT: "termi beta r ==> IT r"
    3.70 -  apply (erule acc_induct)
    3.71 +theorem termi_implies_IT: "termip beta r ==> IT r"
    3.72 +  apply (erule accp_induct)
    3.73    apply (rename_tac r)
    3.74    apply (erule thin_rl)
    3.75    apply (erule rev_mp)
     4.1 --- a/src/HOL/Lambda/Lambda.thy	Wed Jul 11 11:22:02 2007 +0200
     4.2 +++ b/src/HOL/Lambda/Lambda.thy	Wed Jul 11 11:23:24 2007 +0200
     4.3 @@ -53,7 +53,7 @@
     4.4  
     4.5  subsection {* Beta-reduction *}
     4.6  
     4.7 -inductive2 beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
     4.8 +inductive beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
     4.9    where
    4.10      beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
    4.11    | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
    4.12 @@ -67,7 +67,7 @@
    4.13  notation (latex)
    4.14    beta_reds  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
    4.15  
    4.16 -inductive_cases2 beta_cases [elim!]:
    4.17 +inductive_cases beta_cases [elim!]:
    4.18    "Var i \<rightarrow>\<^sub>\<beta> t"
    4.19    "Abs r \<rightarrow>\<^sub>\<beta> s"
    4.20    "s \<degree> t \<rightarrow>\<^sub>\<beta> u"
    4.21 @@ -80,19 +80,19 @@
    4.22  
    4.23  lemma rtrancl_beta_Abs [intro!]:
    4.24      "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'"
    4.25 -  by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
    4.26 +  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
    4.27  
    4.28  lemma rtrancl_beta_AppL:
    4.29      "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t"
    4.30 -  by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
    4.31 +  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
    4.32  
    4.33  lemma rtrancl_beta_AppR:
    4.34      "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree> t'"
    4.35 -  by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
    4.36 +  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
    4.37  
    4.38  lemma rtrancl_beta_App [intro]:
    4.39      "[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
    4.40 -  by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtrancl_trans')
    4.41 +  by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtranclp_trans)
    4.42  
    4.43  
    4.44  subsection {* Substitution-lemmas *}
    4.45 @@ -155,9 +155,9 @@
    4.46    by (induct arbitrary: t i set: beta) (simp_all add: subst_subst [symmetric])
    4.47  
    4.48  theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
    4.49 -  apply (induct set: rtrancl)
    4.50 -   apply (rule rtrancl.rtrancl_refl)
    4.51 -  apply (erule rtrancl.rtrancl_into_rtrancl)
    4.52 +  apply (induct set: rtranclp)
    4.53 +   apply (rule rtranclp.rtrancl_refl)
    4.54 +  apply (erule rtranclp.rtrancl_into_rtrancl)
    4.55    apply (erule subst_preserves_beta)
    4.56    done
    4.57  
    4.58 @@ -166,23 +166,23 @@
    4.59    by (induct arbitrary: i set: beta) auto
    4.60  
    4.61  theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
    4.62 -  apply (induct set: rtrancl)
    4.63 -   apply (rule rtrancl.rtrancl_refl)
    4.64 -  apply (erule rtrancl.rtrancl_into_rtrancl)
    4.65 +  apply (induct set: rtranclp)
    4.66 +   apply (rule rtranclp.rtrancl_refl)
    4.67 +  apply (erule rtranclp.rtrancl_into_rtrancl)
    4.68    apply (erule lift_preserves_beta)
    4.69    done
    4.70  
    4.71  theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
    4.72    apply (induct t arbitrary: r s i)
    4.73 -    apply (simp add: subst_Var r_into_rtrancl')
    4.74 +    apply (simp add: subst_Var r_into_rtranclp)
    4.75     apply (simp add: rtrancl_beta_App)
    4.76    apply (simp add: rtrancl_beta_Abs)
    4.77    done
    4.78  
    4.79  theorem subst_preserves_beta2': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
    4.80 -  apply (induct set: rtrancl)
    4.81 -   apply (rule rtrancl.rtrancl_refl)
    4.82 -  apply (erule rtrancl_trans')
    4.83 +  apply (induct set: rtranclp)
    4.84 +   apply (rule rtranclp.rtrancl_refl)
    4.85 +  apply (erule rtranclp_trans)
    4.86    apply (erule subst_preserves_beta2)
    4.87    done
    4.88  
     5.1 --- a/src/HOL/Lambda/ListBeta.thy	Wed Jul 11 11:22:02 2007 +0200
     5.2 +++ b/src/HOL/Lambda/ListBeta.thy	Wed Jul 11 11:23:24 2007 +0200
     5.3 @@ -71,9 +71,9 @@
     5.4  
     5.5  lemma apps_preserves_beta2 [simp]:
     5.6      "r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss"
     5.7 -  apply (induct set: rtrancl)
     5.8 +  apply (induct set: rtranclp)
     5.9     apply blast
    5.10 -  apply (blast intro: apps_preserves_beta rtrancl.rtrancl_into_rtrancl)
    5.11 +  apply (blast intro: apps_preserves_beta rtranclp.rtrancl_into_rtrancl)
    5.12    done
    5.13  
    5.14  lemma apps_preserves_betas [simp]:
     6.1 --- a/src/HOL/Lambda/ListOrder.thy	Wed Jul 11 11:22:02 2007 +0200
     6.2 +++ b/src/HOL/Lambda/ListOrder.thy	Wed Jul 11 11:23:24 2007 +0200
     6.3 @@ -87,20 +87,20 @@
     6.4    done
     6.5  
     6.6  lemma Cons_acc_step1I [intro!]:
     6.7 -    "acc r x ==> acc (step1 r) xs \<Longrightarrow> acc (step1 r) (x # xs)"
     6.8 -  apply (induct arbitrary: xs set: acc)
     6.9 +    "accp r x ==> accp (step1 r) xs \<Longrightarrow> accp (step1 r) (x # xs)"
    6.10 +  apply (induct arbitrary: xs set: accp)
    6.11    apply (erule thin_rl)
    6.12 -  apply (erule acc_induct)
    6.13 -  apply (rule accI)
    6.14 +  apply (erule accp_induct)
    6.15 +  apply (rule accp.accI)
    6.16    apply blast
    6.17    done
    6.18  
    6.19 -lemma lists_accD: "listsp (acc r) xs ==> acc (step1 r) xs"
    6.20 +lemma lists_accD: "listsp (accp r) xs ==> accp (step1 r) xs"
    6.21    apply (induct set: listsp)
    6.22 -   apply (rule accI)
    6.23 +   apply (rule accp.accI)
    6.24     apply simp
    6.25 -  apply (rule accI)
    6.26 -  apply (fast dest: acc_downward)
    6.27 +  apply (rule accp.accI)
    6.28 +  apply (fast dest: accp_downward)
    6.29    done
    6.30  
    6.31  lemma ex_step1I:
    6.32 @@ -111,10 +111,10 @@
    6.33    apply force
    6.34    done
    6.35  
    6.36 -lemma lists_accI: "acc (step1 r) xs ==> listsp (acc r) xs"
    6.37 -  apply (induct set: acc)
    6.38 +lemma lists_accI: "accp (step1 r) xs ==> listsp (accp r) xs"
    6.39 +  apply (induct set: accp)
    6.40    apply clarify
    6.41 -  apply (rule accI)
    6.42 +  apply (rule accp.accI)
    6.43    apply (drule_tac r=r in ex_step1I, assumption)
    6.44    apply blast
    6.45    done
     7.1 --- a/src/HOL/Lambda/ParRed.thy	Wed Jul 11 11:22:02 2007 +0200
     7.2 +++ b/src/HOL/Lambda/ParRed.thy	Wed Jul 11 11:23:24 2007 +0200
     7.3 @@ -14,14 +14,14 @@
     7.4  
     7.5  subsection {* Parallel reduction *}
     7.6  
     7.7 -inductive2 par_beta :: "[dB, dB] => bool"  (infixl "=>" 50)
     7.8 +inductive par_beta :: "[dB, dB] => bool"  (infixl "=>" 50)
     7.9    where
    7.10      var [simp, intro!]: "Var n => Var n"
    7.11    | abs [simp, intro!]: "s => t ==> Abs s => Abs t"
    7.12    | app [simp, intro!]: "[| s => s'; t => t' |] ==> s \<degree> t => s' \<degree> t'"
    7.13    | beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) \<degree> t => s'[t'/0]"
    7.14  
    7.15 -inductive_cases2 par_beta_cases [elim!]:
    7.16 +inductive_cases par_beta_cases [elim!]:
    7.17    "Var n => t"
    7.18    "Abs s => Abs t"
    7.19    "(Abs s) \<degree> t => u"
    7.20 @@ -50,7 +50,7 @@
    7.21    apply (rule predicate2I)
    7.22    apply (erule par_beta.induct)
    7.23       apply blast
    7.24 -    apply (blast del: rtrancl.rtrancl_refl intro: rtrancl.rtrancl_into_rtrancl)+
    7.25 +    apply (blast del: rtranclp.rtrancl_refl intro: rtranclp.rtrancl_into_rtrancl)+
    7.26        -- {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *}
    7.27    done
    7.28  
     8.1 --- a/src/HOL/Lambda/StrongNorm.thy	Wed Jul 11 11:22:02 2007 +0200
     8.2 +++ b/src/HOL/Lambda/StrongNorm.thy	Wed Jul 11 11:23:24 2007 +0200
     8.3 @@ -277,7 +277,7 @@
     8.4    thus ?case by simp
     8.5  qed
     8.6  
     8.7 -theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> termi beta t"
     8.8 +theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> termip beta t"
     8.9  proof -
    8.10    assume "e \<turnstile> t : T"
    8.11    hence "IT t" by (rule type_implies_IT)
     9.1 --- a/src/HOL/Lambda/Type.thy	Wed Jul 11 11:22:02 2007 +0200
     9.2 +++ b/src/HOL/Lambda/Type.thy	Wed Jul 11 11:23:24 2007 +0200
     9.3 @@ -45,13 +45,13 @@
     9.4      Atom nat
     9.5    | Fun type type    (infixr "\<Rightarrow>" 200)
     9.6  
     9.7 -inductive2 typing :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
     9.8 +inductive typing :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
     9.9    where
    9.10      Var [intro!]: "env x = T \<Longrightarrow> env \<turnstile> Var x : T"
    9.11    | Abs [intro!]: "env\<langle>0:T\<rangle> \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs t : (T \<Rightarrow> U)"
    9.12    | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
    9.13  
    9.14 -inductive_cases2 typing_elims [elim!]:
    9.15 +inductive_cases typing_elims [elim!]:
    9.16    "e \<turnstile> Var i : T"
    9.17    "e \<turnstile> t \<degree> u : T"
    9.18    "e \<turnstile> Abs t : T"
    9.19 @@ -164,7 +164,7 @@
    9.20    apply (erule impE)
    9.21     apply assumption
    9.22    apply (elim exE conjE)
    9.23 -  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
    9.24 +  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
    9.25    apply (rule_tac x = "Ta # Ts" in exI)
    9.26    apply simp
    9.27    done
    9.28 @@ -202,12 +202,12 @@
    9.29    "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U"
    9.30    apply (induct ts arbitrary: T U rule: rev_induct)
    9.31    apply simp
    9.32 -  apply (ind_cases2 "e \<turnstile> Var i : T" for T)
    9.33 -  apply (ind_cases2 "e \<turnstile> Var i : T" for T)
    9.34 +  apply (ind_cases "e \<turnstile> Var i : T" for T)
    9.35 +  apply (ind_cases "e \<turnstile> Var i : T" for T)
    9.36    apply simp
    9.37    apply simp
    9.38 -  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
    9.39 -  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
    9.40 +  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
    9.41 +  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
    9.42    apply atomize
    9.43    apply (erule_tac x="Ta \<Rightarrow> T" in allE)
    9.44    apply (erule_tac x="Tb \<Rightarrow> U" in allE)
    9.45 @@ -230,7 +230,7 @@
    9.46    apply (rule FalseE)
    9.47    apply simp
    9.48    apply (erule list_app_typeE)
    9.49 -  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
    9.50 +  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
    9.51    apply (drule_tac T="Atom nat" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
    9.52    apply assumption
    9.53    apply simp
    9.54 @@ -242,7 +242,7 @@
    9.55    apply (rule types_snoc)
    9.56    apply assumption
    9.57    apply (erule list_app_typeE)
    9.58 -  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
    9.59 +  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
    9.60    apply (drule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
    9.61    apply assumption
    9.62    apply simp
    9.63 @@ -250,7 +250,7 @@
    9.64    apply (rule typing.App)
    9.65    apply assumption
    9.66    apply (erule list_app_typeE)
    9.67 -  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
    9.68 +  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
    9.69    apply (frule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
    9.70    apply assumption
    9.71    apply simp
    9.72 @@ -258,7 +258,7 @@
    9.73    apply (rule_tac x="type1 # Us" in exI)
    9.74    apply simp
    9.75    apply (erule list_app_typeE)
    9.76 -  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
    9.77 +  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
    9.78    apply (frule_tac T="type1 \<Rightarrow> Us \<Rrightarrow> T" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
    9.79    apply assumption
    9.80    apply simp
    9.81 @@ -332,9 +332,9 @@
    9.82      apply blast
    9.83     apply blast
    9.84    apply atomize
    9.85 -  apply (ind_cases2 "s \<degree> t \<rightarrow>\<^sub>\<beta> t'" for s t t')
    9.86 +  apply (ind_cases "s \<degree> t \<rightarrow>\<^sub>\<beta> t'" for s t t')
    9.87      apply hypsubst
    9.88 -    apply (ind_cases2 "env \<turnstile> Abs t : T \<Rightarrow> U" for env t T U)
    9.89 +    apply (ind_cases "env \<turnstile> Abs t : T \<Rightarrow> U" for env t T U)
    9.90      apply (rule subst_lemma)
    9.91        apply assumption
    9.92       apply assumption
    9.93 @@ -344,7 +344,7 @@
    9.94    done
    9.95  
    9.96  theorem subject_reduction': "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<turnstile> t' : T"
    9.97 -  by (induct set: rtrancl) (iprover intro: subject_reduction)+
    9.98 +  by (induct set: rtranclp) (iprover intro: subject_reduction)+
    9.99  
   9.100  
   9.101  subsection {* Alternative induction rule for types *}
    10.1 --- a/src/HOL/Lambda/WeakNorm.thy	Wed Jul 11 11:22:02 2007 +0200
    10.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Wed Jul 11 11:23:24 2007 +0200
    10.3 @@ -75,7 +75,7 @@
    10.4    -- {* Currently needed for strange technical reasons *}
    10.5    by (unfold listall_def) simp
    10.6  
    10.7 -inductive2 NF :: "dB \<Rightarrow> bool"
    10.8 +inductive NF :: "dB \<Rightarrow> bool"
    10.9  where
   10.10    App: "listall NF ts \<Longrightarrow> NF (Var x \<degree>\<degree> ts)"
   10.11  | Abs: "NF t \<Longrightarrow> NF (Abs t)"
   10.12 @@ -138,15 +138,15 @@
   10.13    apply (simplesubst app_last)  --{*Using @{text subst} makes extraction fail*}
   10.14    apply (rule exI)
   10.15    apply (rule conjI)
   10.16 -  apply (rule rtrancl.rtrancl_refl)
   10.17 +  apply (rule rtranclp.rtrancl_refl)
   10.18    apply (rule NF.App)
   10.19    apply (drule listall_conj1)
   10.20    apply (simp add: listall_app)
   10.21    apply (rule Var_NF)
   10.22    apply (rule exI)
   10.23    apply (rule conjI)
   10.24 -  apply (rule rtrancl.rtrancl_into_rtrancl)
   10.25 -  apply (rule rtrancl.rtrancl_refl)
   10.26 +  apply (rule rtranclp.rtrancl_into_rtrancl)
   10.27 +  apply (rule rtranclp.rtrancl_refl)
   10.28    apply (rule beta)
   10.29    apply (erule subst_Var_NF)
   10.30    done
   10.31 @@ -361,7 +361,7 @@
   10.32  
   10.33  
   10.34  -- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}
   10.35 -inductive2 rtyping :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
   10.36 +inductive rtyping :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
   10.37    where
   10.38      Var: "e x = T \<Longrightarrow> e \<turnstile>\<^sub>R Var x : T"
   10.39    | Abs: "e\<langle>0:T\<rangle> \<turnstile>\<^sub>R t : U \<Longrightarrow> e \<turnstile>\<^sub>R Abs t : (T \<Rightarrow> U)"
   10.40 @@ -411,7 +411,7 @@
   10.41    qed
   10.42    then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "NF u" by simp iprover
   10.43    from sred tred have "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'" by (rule rtrancl_beta_App)
   10.44 -  hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtrancl_trans')
   10.45 +  hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtranclp_trans)
   10.46    with unf show ?case by iprover
   10.47  qed
   10.48  
   10.49 @@ -419,21 +419,21 @@
   10.50  subsection {* Extracting the program *}
   10.51  
   10.52  declare NF.induct [ind_realizer]
   10.53 -declare rtrancl.induct [ind_realizer irrelevant]
   10.54 +declare rtranclp.induct [ind_realizer irrelevant]
   10.55  declare rtyping.induct [ind_realizer]
   10.56  lemmas [extraction_expand] = conj_assoc listall_cons_eq
   10.57  
   10.58  extract type_NF
   10.59  
   10.60 -lemma rtranclR_rtrancl_eq: "rtranclR r a b = rtrancl r a b"
   10.61 +lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r\<^sup>*\<^sup>* a b"
   10.62    apply (rule iffI)
   10.63 -  apply (erule rtranclR.induct)
   10.64 -  apply (rule rtrancl.rtrancl_refl)
   10.65 -  apply (erule rtrancl.rtrancl_into_rtrancl)
   10.66 +  apply (erule rtranclpR.induct)
   10.67 +  apply (rule rtranclp.rtrancl_refl)
   10.68 +  apply (erule rtranclp.rtrancl_into_rtrancl)
   10.69    apply assumption
   10.70 -  apply (erule rtrancl.induct)
   10.71 -  apply (rule rtranclR.rtrancl_refl)
   10.72 -  apply (erule rtranclR.rtrancl_into_rtrancl)
   10.73 +  apply (erule rtranclp.induct)
   10.74 +  apply (rule rtranclpR.rtrancl_refl)
   10.75 +  apply (erule rtranclpR.rtrancl_into_rtrancl)
   10.76    apply assumption
   10.77    done
   10.78