- Renamed inductive2 to inductive
authorberghofe
Wed Jul 11 11:32:02 2007 +0200 (2007-07-11)
changeset 23757087b0a241557
parent 23756 14008ce7df96
child 23758 705f25072f5c
- Renamed inductive2 to inductive
- Renamed some theorems about transitive closure for predicates
src/HOL/MicroJava/BV/BVExample.thy
src/HOL/MicroJava/BV/JType.thy
src/HOL/MicroJava/BV/Listn.thy
src/HOL/MicroJava/BV/Semilat.thy
src/HOL/MicroJava/Comp/CorrComp.thy
src/HOL/MicroJava/Comp/LemmasComp.thy
src/HOL/MicroJava/J/Eval.thy
src/HOL/MicroJava/J/Example.thy
src/HOL/MicroJava/J/JTypeSafe.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/J/WellForm.thy
src/HOL/MicroJava/J/WellType.thy
src/HOL/Nominal/Examples/Class.thy
     1.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Wed Jul 11 11:29:44 2007 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Wed Jul 11 11:32:02 2007 +0200
     1.3 @@ -67,28 +67,28 @@
     1.4  
     1.5  text {* The subclass releation spelled out: *}
     1.6  lemma subcls1:
     1.7 -  "subcls1 E = member2 {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
     1.8 -                (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}"
     1.9 +  "subcls1 E = (\<lambda>C D. (C, D) \<in> {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
    1.10 +                (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)})"
    1.11    apply (simp add: subcls1_def2)
    1.12    apply (simp add: name_defs class_defs system_defs E_def class_def)
    1.13 -  apply (auto simp: member2_inject split: split_if_asm)
    1.14 +  apply (auto simp: expand_fun_eq split: split_if_asm)
    1.15    done
    1.16  
    1.17  text {* The subclass relation is acyclic; hence its converse is well founded: *}
    1.18  lemma notin_rtrancl:
    1.19    "r\<^sup>*\<^sup>* a b \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. \<not> r a y) \<Longrightarrow> False"
    1.20 -  by (auto elim: converse_rtranclE')
    1.21 +  by (auto elim: converse_rtranclpE)
    1.22  
    1.23  lemma acyclic_subcls1_E: "acyclicP (subcls1 E)"
    1.24    apply (rule acyclicI [to_pred])
    1.25    apply (simp add: subcls1)
    1.26 -  apply (auto dest!: tranclD')
    1.27 +  apply (auto dest!: tranclpD)
    1.28    apply (auto elim!: notin_rtrancl simp add: name_defs distinct_classes)
    1.29    done
    1.30  
    1.31  lemma wf_subcls1_E: "wfP ((subcls1 E)\<inverse>\<inverse>)"
    1.32    apply (rule finite_acyclic_wf_converse [to_pred])
    1.33 -  apply (simp add: subcls1)
    1.34 +  apply (simp add: subcls1 del: insert_iff)
    1.35    apply (rule acyclic_subcls1_E)
    1.36    done  
    1.37  
    1.38 @@ -464,7 +464,7 @@
    1.39    meta_eq_to_obj_eq [OF JType.sup_def [unfolded exec_lub_def]]
    1.40    meta_eq_to_obj_eq [OF JVM_le_unfold]
    1.41  
    1.42 -lemmas [code ind] = rtrancl.rtrancl_refl converse_rtrancl_into_rtrancl'
    1.43 +lemmas [code ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
    1.44  
    1.45  code_module BV
    1.46  contains
     2.1 --- a/src/HOL/MicroJava/BV/JType.thy	Wed Jul 11 11:29:44 2007 +0200
     2.2 +++ b/src/HOL/MicroJava/BV/JType.thy	Wed Jul 11 11:32:02 2007 +0200
     2.3 @@ -78,7 +78,7 @@
     2.4      have "R \<noteq> ClassT Object \<Longrightarrow> ?thesis"
     2.5       by (auto simp add: is_ty_def is_class_def split_tupled_all
     2.6                 elim!: subcls1.cases
     2.7 -               elim: converse_rtranclE'
     2.8 +               elim: converse_rtranclpE
     2.9                 split: ref_ty.splits)
    2.10      ultimately    
    2.11      show ?thesis by blast
    2.12 @@ -146,16 +146,16 @@
    2.13  apply (case_tac t)
    2.14   apply simp
    2.15  apply simp
    2.16 -apply (insert rtrancl_r_diff_Id' [symmetric, standard, of "subcls1 G"])
    2.17 +apply (insert rtranclp_r_diff_Id [symmetric, standard, of "subcls1 G"])
    2.18  apply simp
    2.19 -apply (erule rtrancl.cases)
    2.20 +apply (erule rtranclp.cases)
    2.21   apply blast
    2.22 -apply (drule rtrancl_converseI')
    2.23 +apply (drule rtranclp_converseI)
    2.24  apply (subgoal_tac "(inf (subcls1 G) op \<noteq>)^--1 = (inf ((subcls1 G)^--1) op \<noteq>)")
    2.25   prefer 2
    2.26   apply (simp add: converse_meet)
    2.27  apply simp
    2.28 -apply (blast intro: rtrancl_into_trancl2')
    2.29 +apply (blast intro: rtranclp_into_tranclp2)
    2.30  done 
    2.31  
    2.32  lemma closed_err_types:
     3.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Wed Jul 11 11:29:44 2007 +0200
     3.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Wed Jul 11 11:32:02 2007 +0200
     3.3 @@ -330,7 +330,7 @@
     3.4   apply (rename_tac m n)
     3.5   apply (case_tac "m=n")
     3.6    apply simp
     3.7 - apply (fast intro!: equals0I [to_pred] dest: not_sym)
     3.8 + apply (fast intro!: equals0I [to_pred bot_empty_eq] dest: not_sym)
     3.9  apply clarify
    3.10  apply (rename_tac n)
    3.11  apply (induct_tac n)
     4.1 --- a/src/HOL/MicroJava/BV/Semilat.thy	Wed Jul 11 11:29:44 2007 +0200
     4.2 +++ b/src/HOL/MicroJava/BV/Semilat.thy	Wed Jul 11 11:32:02 2007 +0200
     4.3 @@ -272,22 +272,22 @@
     4.4  apply (case_tac "r^** y x")
     4.5   apply (case_tac "r^** y x'")
     4.6    apply blast
     4.7 - apply (blast elim: converse_rtranclE' dest: single_valuedD)
     4.8 + apply (blast elim: converse_rtranclpE dest: single_valuedD)
     4.9  apply (rule exI)
    4.10  apply (rule conjI)
    4.11 - apply (blast intro: converse_rtrancl_into_rtrancl' dest: single_valuedD)
    4.12 -apply (blast intro: rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl'
    4.13 -             elim: converse_rtranclE' dest: single_valuedD)
    4.14 + apply (blast intro: converse_rtranclp_into_rtranclp dest: single_valuedD)
    4.15 +apply (blast intro: rtranclp.rtrancl_into_rtrancl converse_rtranclp_into_rtranclp
    4.16 +             elim: converse_rtranclpE dest: single_valuedD)
    4.17  done
    4.18  
    4.19  lemma single_valued_has_lubs [rule_format]:
    4.20    "\<lbrakk> single_valuedP r; r^** x u \<rbrakk> \<Longrightarrow> (!y. r^** y u \<longrightarrow> 
    4.21    (EX z. is_lub (r^** ) x y z))"
    4.22 -apply (erule converse_rtrancl_induct')
    4.23 +apply (erule converse_rtranclp_induct)
    4.24   apply clarify
    4.25 - apply (erule converse_rtrancl_induct')
    4.26 + apply (erule converse_rtranclp_induct)
    4.27    apply blast
    4.28 - apply (blast intro: converse_rtrancl_into_rtrancl')
    4.29 + apply (blast intro: converse_rtranclp_into_rtranclp)
    4.30  apply (blast intro: extend_lub)
    4.31  done
    4.32  
    4.33 @@ -313,18 +313,18 @@
    4.34  
    4.35  lemma acyclic_single_valued_finite:
    4.36   "\<lbrakk>acyclicP r; single_valuedP r; r\<^sup>*\<^sup>* x y \<rbrakk>
    4.37 -  \<Longrightarrow> finite (Collect2 r \<inter> {a. r\<^sup>*\<^sup>* x a} \<times> {b. r\<^sup>*\<^sup>* b y})"
    4.38 -apply(erule converse_rtrancl_induct')
    4.39 +  \<Longrightarrow> finite ({(x, y). r x y} \<inter> {a. r\<^sup>*\<^sup>* x a} \<times> {b. r\<^sup>*\<^sup>* b y})"
    4.40 +apply(erule converse_rtranclp_induct)
    4.41   apply(rule_tac B = "{}" in finite_subset)
    4.42    apply(simp only:acyclic_def [to_pred])
    4.43 -  apply(blast intro:rtrancl_into_trancl2' rtrancl_trancl_trancl')
    4.44 +  apply(blast intro:rtranclp_into_tranclp2 rtranclp_tranclp_tranclp)
    4.45   apply simp
    4.46  apply(rename_tac x x')
    4.47 -apply(subgoal_tac "Collect2 r \<inter> {a. r\<^sup>*\<^sup>* x a} \<times> {b. r\<^sup>*\<^sup>* b y} =
    4.48 -                   insert (x,x') (Collect2 r \<inter> {a. r\<^sup>*\<^sup>* x' a} \<times> {b. r\<^sup>*\<^sup>* b y})")
    4.49 +apply(subgoal_tac "{(x, y). r x y} \<inter> {a. r\<^sup>*\<^sup>* x a} \<times> {b. r\<^sup>*\<^sup>* b y} =
    4.50 +                   insert (x,x') ({(x, y). r x y} \<inter> {a. r\<^sup>*\<^sup>* x' a} \<times> {b. r\<^sup>*\<^sup>* b y})")
    4.51   apply simp
    4.52 -apply(blast intro:converse_rtrancl_into_rtrancl'
    4.53 -            elim:converse_rtranclE' dest:single_valuedD)
    4.54 +apply(blast intro:converse_rtranclp_into_rtranclp
    4.55 +            elim:converse_rtranclpE dest:single_valuedD)
    4.56  done
    4.57  
    4.58  
    4.59 @@ -333,21 +333,21 @@
    4.60    exec_lub r f x y = u";
    4.61  apply(unfold exec_lub_def)
    4.62  apply(rule_tac P = "\<lambda>z. r\<^sup>*\<^sup>* y z \<and> r\<^sup>*\<^sup>* z u" and
    4.63 -               r = "(Collect2 r \<inter> {(a,b). r\<^sup>*\<^sup>* y a \<and> r\<^sup>*\<^sup>* b u})^-1" in while_rule)
    4.64 +               r = "({(x, y). r x y} \<inter> {(a,b). r\<^sup>*\<^sup>* y a \<and> r\<^sup>*\<^sup>* b u})^-1" in while_rule)
    4.65      apply(blast dest: is_lubD is_ubD)
    4.66     apply(erule conjE)
    4.67 -   apply(erule_tac z = u in converse_rtranclE')
    4.68 +   apply(erule_tac z = u in converse_rtranclpE)
    4.69      apply(blast dest: is_lubD is_ubD)
    4.70 -   apply(blast dest: rtrancl.rtrancl_into_rtrancl)
    4.71 +   apply(blast dest: rtranclp.rtrancl_into_rtrancl)
    4.72    apply(rename_tac s)
    4.73    apply(subgoal_tac "is_ub (r\<^sup>*\<^sup>*) x y s")
    4.74     prefer 2; apply(simp add:is_ub_def)
    4.75    apply(subgoal_tac "r\<^sup>*\<^sup>* u s")
    4.76     prefer 2; apply(blast dest:is_lubD)
    4.77 -  apply(erule converse_rtranclE')
    4.78 +  apply(erule converse_rtranclpE)
    4.79     apply blast
    4.80    apply(simp only:acyclic_def [to_pred])
    4.81 -  apply(blast intro:rtrancl_into_trancl2' rtrancl_trancl_trancl')
    4.82 +  apply(blast intro:rtranclp_into_tranclp2 rtranclp_tranclp_tranclp)
    4.83   apply(rule finite_acyclic_wf)
    4.84    apply simp
    4.85    apply(erule acyclic_single_valued_finite)
    4.86 @@ -358,7 +358,7 @@
    4.87   apply blast
    4.88  apply simp
    4.89  apply(erule conjE)
    4.90 -apply(erule_tac z = u in converse_rtranclE')
    4.91 +apply(erule_tac z = u in converse_rtranclpE)
    4.92   apply(blast dest: is_lubD is_ubD)
    4.93  apply blast
    4.94  done
     5.1 --- a/src/HOL/MicroJava/Comp/CorrComp.thy	Wed Jul 11 11:29:44 2007 +0200
     5.2 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Wed Jul 11 11:32:02 2007 +0200
     5.3 @@ -404,7 +404,7 @@
     5.4         E\<turnstile>ps[::]pTs & max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')})"
     5.5  apply (simp only: wtpd_expr_def wtpd_exprs_def)
     5.6  apply (erule exE)
     5.7 -apply (ind_cases2 "E \<turnstile> {C}a..mn( {pTs'}ps) :: T" for T)
     5.8 +apply (ind_cases "E \<turnstile> {C}a..mn( {pTs'}ps) :: T" for T)
     5.9  apply (auto simp: max_spec_preserves_length)
    5.10  done
    5.11  
    5.12 @@ -618,13 +618,13 @@
    5.13  apply simp
    5.14  apply (rule allI)
    5.15  apply (rule iffI)
    5.16 -  apply (ind_cases2 "E \<turnstile> [] [::] Ts" for Ts, assumption)
    5.17 +  apply (ind_cases "E \<turnstile> [] [::] Ts" for Ts, assumption)
    5.18    apply simp apply (rule WellType.Nil)
    5.19  apply (simp add: list_all2_Cons1)
    5.20  apply (rule allI)
    5.21  apply (rule iffI)
    5.22    apply (rename_tac a exs Ts)
    5.23 -  apply (ind_cases2 "E \<turnstile> a # exs  [::] Ts" for a exs Ts) apply blast
    5.24 +  apply (ind_cases "E \<turnstile> a # exs  [::] Ts" for a exs Ts) apply blast
    5.25    apply (auto intro: WellType.Cons)
    5.26  done
    5.27  
     6.1 --- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Wed Jul 11 11:29:44 2007 +0200
     6.2 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Wed Jul 11 11:32:02 2007 +0200
     6.3 @@ -111,7 +111,7 @@
     6.4  by (case_tac "class G C", auto simp: is_class_def dest: comp_class_imp)
     6.5  
     6.6  lemma comp_subcls1: "subcls1 (comp G) = subcls1 G"
     6.7 -by (auto simp add: subcls1_def2 comp_classname comp_is_class member2_inject)
     6.8 +by (auto simp add: subcls1_def2 comp_classname comp_is_class expand_fun_eq)
     6.9  
    6.10  lemma comp_widen: "widen (comp G) = widen G"
    6.11    apply (simp add: expand_fun_eq)
    6.12 @@ -193,7 +193,8 @@
    6.13  apply (erule disjE)
    6.14  
    6.15    (* case class G x = None *)
    6.16 -apply (simp (no_asm_simp) add: class_rec_def comp_subcls1 wfrec [to_pred] cut_apply)
    6.17 +apply (simp (no_asm_simp) add: class_rec_def comp_subcls1
    6.18 +  wfrec [to_pred, where r="(subcls1 G)^--1", simplified])
    6.19  apply (simp add: comp_class_None)
    6.20  
    6.21    (* case \<exists> D fs ms. (class G x = Some (D, fs, ms)) *)
     7.1 --- a/src/HOL/MicroJava/J/Eval.thy	Wed Jul 11 11:29:44 2007 +0200
     7.2 +++ b/src/HOL/MicroJava/J/Eval.thy	Wed Jul 11 11:32:02 2007 +0200
     7.3 @@ -32,7 +32,7 @@
     7.4  
     7.5    -- "Evaluation relations"
     7.6  
     7.7 -inductive2
     7.8 +inductive
     7.9    eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
    7.10            ("_ \<turnstile> _ -_\<succ>_-> _" [51,82,60,82,82] 81)
    7.11    and evals :: "[java_mb prog,xstate,expr list,
     8.1 --- a/src/HOL/MicroJava/J/Example.thy	Wed Jul 11 11:29:44 2007 +0200
     8.2 +++ b/src/HOL/MicroJava/J/Example.thy	Wed Jul 11 11:32:02 2007 +0200
     8.3 @@ -173,18 +173,18 @@
     8.4  done
     8.5  
     8.6  lemma not_Object_subcls [elim!]: "(subcls1 tprg)^++ Object C ==> R"
     8.7 -apply (auto dest!: tranclD' subcls1D)
     8.8 +apply (auto dest!: tranclpD subcls1D)
     8.9  done
    8.10  
    8.11  lemma subcls_ObjectD [dest!]: "tprg\<turnstile>Object\<preceq>C C ==> C = Object"
    8.12 -apply (erule rtrancl_induct')
    8.13 +apply (erule rtranclp_induct)
    8.14  apply  auto
    8.15  apply (drule subcls1D)
    8.16  apply auto
    8.17  done
    8.18  
    8.19  lemma not_Base_subcls_Ext [elim!]: "(subcls1 tprg)^++ Base Ext ==> R"
    8.20 -apply (auto dest!: tranclD' subcls1D)
    8.21 +apply (auto dest!: tranclpD subcls1D)
    8.22  done
    8.23  
    8.24  lemma class_tprgD: 
    8.25 @@ -194,10 +194,10 @@
    8.26  done
    8.27  
    8.28  lemma not_class_subcls_class [elim!]: "(subcls1 tprg)^++ C C ==> R"
    8.29 -apply (auto dest!: tranclD' subcls1D)
    8.30 +apply (auto dest!: tranclpD subcls1D)
    8.31  apply (frule class_tprgD)
    8.32  apply (auto dest!:)
    8.33 -apply (drule rtranclD')
    8.34 +apply (drule rtranclpD)
    8.35  apply auto
    8.36  done
    8.37  
    8.38 @@ -205,7 +205,7 @@
    8.39  apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def)
    8.40  done
    8.41  
    8.42 -lemmas subcls_direct = subcls1I [THEN r_into_rtrancl' [where r="subcls1 G"], standard]
    8.43 +lemmas subcls_direct = subcls1I [THEN r_into_rtranclp [where r="subcls1 G"], standard]
    8.44  
    8.45  lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base"
    8.46  apply (rule subcls_direct)
    8.47 @@ -345,7 +345,7 @@
    8.48  apply (fold ExtC_def)
    8.49  apply (rule mp) defer apply (rule wf_foo_Ext)
    8.50  apply (auto simp add: wf_mdecl_def)
    8.51 -apply (drule rtranclD')
    8.52 +apply (drule rtranclpD)
    8.53  apply auto
    8.54  done
    8.55  
     9.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Jul 11 11:29:44 2007 +0200
     9.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Jul 11 11:32:02 2007 +0200
     9.3 @@ -27,7 +27,7 @@
     9.4  apply (case_tac "ref_ty")
     9.5  apply (clarsimp simp add: conf_def)
     9.6  apply simp
     9.7 -apply (ind_cases2 "G \<turnstile> Class cname \<preceq>? Class D" for cname, simp)
     9.8 +apply (ind_cases "G \<turnstile> Class cname \<preceq>? Class D" for cname, simp)
     9.9  apply (rule conf_widen, assumption+) apply (erule widen.subcls)
    9.10  
    9.11  apply (unfold cast_ok_def)
    9.12 @@ -222,7 +222,7 @@
    9.13  apply( rule conjI)
    9.14  apply(  force elim!: NewC_conforms)
    9.15  apply( rule conf_obj_AddrI)
    9.16 -apply(  rule_tac [2] rtrancl.rtrancl_refl)
    9.17 +apply(  rule_tac [2] rtranclp.rtrancl_refl)
    9.18  apply( simp (no_asm))
    9.19  
    9.20  -- "for Cast"
    10.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Jul 11 11:29:44 2007 +0200
    10.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Jul 11 11:32:02 2007 +0200
    10.3 @@ -9,7 +9,7 @@
    10.4  theory TypeRel imports Decl begin
    10.5  
    10.6  -- "direct subclass, cf. 8.1.3"
    10.7 -inductive2
    10.8 +inductive
    10.9    subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
   10.10    for G :: "'c prog"
   10.11  where
   10.12 @@ -26,12 +26,12 @@
   10.13  done
   10.14  
   10.15  lemma subcls1_def2: 
   10.16 -  "subcls1 G = member2
   10.17 -     (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
   10.18 +  "subcls1 G = (\<lambda>C D. (C, D) \<in>
   10.19 +     (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D}))"
   10.20    by (auto simp add: is_class_def expand_fun_eq dest: subcls1D intro: subcls1I)
   10.21  
   10.22 -lemma finite_subcls1: "finite (Collect2 (subcls1 G))"
   10.23 -apply(simp add: subcls1_def2)
   10.24 +lemma finite_subcls1: "finite {(C, D). subcls1 G C D}"
   10.25 +apply(simp add: subcls1_def2 del: mem_Sigma_iff)
   10.26  apply(rule finite_SigmaI [OF finite_is_class])
   10.27  apply(rule_tac B = "{fst (the (class G C))}" in finite_subset)
   10.28  apply  auto
   10.29 @@ -39,14 +39,14 @@
   10.30  
   10.31  lemma subcls_is_class: "(subcls1 G)^++ C D ==> is_class G C"
   10.32  apply (unfold is_class_def)
   10.33 -apply(erule trancl_trans_induct')
   10.34 +apply(erule tranclp_trans_induct)
   10.35  apply (auto dest!: subcls1D)
   10.36  done
   10.37  
   10.38  lemma subcls_is_class2 [rule_format (no_asm)]: 
   10.39    "G\<turnstile>C\<preceq>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C"
   10.40  apply (unfold is_class_def)
   10.41 -apply (erule rtrancl_induct')
   10.42 +apply (erule rtranclp_induct)
   10.43  apply  (drule_tac [2] subcls1D)
   10.44  apply  auto
   10.45  done
   10.46 @@ -54,7 +54,7 @@
   10.47  constdefs
   10.48    class_rec :: "'c prog \<Rightarrow> cname \<Rightarrow> 'a \<Rightarrow>
   10.49      (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
   10.50 -  "class_rec G == wfrec (Collect2 ((subcls1 G)^--1))
   10.51 +  "class_rec G == wfrec {(C, D). (subcls1 G)^--1 C D}
   10.52      (\<lambda>r C t f. case class G C of
   10.53           None \<Rightarrow> arbitrary
   10.54         | Some (D,fs,ms) \<Rightarrow> 
   10.55 @@ -62,8 +62,8 @@
   10.56  
   10.57  lemma class_rec_lemma: "wfP ((subcls1 G)^--1) \<Longrightarrow> class G C = Some (D,fs,ms) \<Longrightarrow>
   10.58   class_rec G C t f = f C fs ms (if C=Object then t else class_rec G D t f)"
   10.59 -  by (simp add: class_rec_def wfrec [to_pred]
   10.60 -    cut_apply [OF Collect2I [where P="(subcls1 G)^--1"], OF conversepI, OF subcls1I])
   10.61 +  by (simp add: class_rec_def wfrec [to_pred, where r="(subcls1 G)^--1", simplified]
   10.62 +    cut_apply [where r="{(C, D). subcls1 G D C}", simplified, OF subcls1I])
   10.63  
   10.64  definition
   10.65    "wf_class G = wfP ((subcls1 G)^--1)"
   10.66 @@ -84,8 +84,8 @@
   10.67    proof (cases "class G C")
   10.68      case None
   10.69      with wf show ?thesis
   10.70 -      by (simp add: class_rec_def wfrec [to_pred]
   10.71 -        cut_apply [OF Collect2I [where P="(subcls1 G)^--1"], OF conversepI, OF subcls1I])
   10.72 +      by (simp add: class_rec_def wfrec [to_pred, where r="(subcls1 G)^--1", simplified]
   10.73 +        cut_apply [where r="{(C, D).subcls1 G D C}", simplified, OF subcls1I])
   10.74    next
   10.75      case (Some x) show ?thesis
   10.76      proof (cases x)
   10.77 @@ -142,7 +142,7 @@
   10.78  
   10.79  
   10.80  -- "widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping"
   10.81 -inductive2
   10.82 +inductive
   10.83    widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _"   [71,71,71] 70)
   10.84    for G :: "'c prog"
   10.85  where
   10.86 @@ -154,7 +154,7 @@
   10.87  
   10.88  -- "casting conversion, cf. 5.5 / 5.1.5"
   10.89  -- "left out casts on primitve types"
   10.90 -inductive2
   10.91 +inductive
   10.92    cast    :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq>? _"  [71,71,71] 70)
   10.93    for G :: "'c prog"
   10.94  where
   10.95 @@ -168,34 +168,34 @@
   10.96  done
   10.97  
   10.98  lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T ==> \<exists>t. T=RefT t"
   10.99 -apply (ind_cases2 "G\<turnstile>RefT R\<preceq>T")
  10.100 +apply (ind_cases "G\<turnstile>RefT R\<preceq>T")
  10.101  apply auto
  10.102  done
  10.103  
  10.104  lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R ==> \<exists>t. S=RefT t"
  10.105 -apply (ind_cases2 "G\<turnstile>S\<preceq>RefT R")
  10.106 +apply (ind_cases "G\<turnstile>S\<preceq>RefT R")
  10.107  apply auto
  10.108  done
  10.109  
  10.110  lemma widen_Class: "G\<turnstile>Class C\<preceq>T ==> \<exists>D. T=Class D"
  10.111 -apply (ind_cases2 "G\<turnstile>Class C\<preceq>T")
  10.112 +apply (ind_cases "G\<turnstile>Class C\<preceq>T")
  10.113  apply auto
  10.114  done
  10.115  
  10.116  lemma widen_Class_NullT [iff]: "(G\<turnstile>Class C\<preceq>NT) = False"
  10.117  apply (rule iffI)
  10.118 -apply (ind_cases2 "G\<turnstile>Class C\<preceq>NT")
  10.119 +apply (ind_cases "G\<turnstile>Class C\<preceq>NT")
  10.120  apply auto
  10.121  done
  10.122  
  10.123  lemma widen_Class_Class [iff]: "(G\<turnstile>Class C\<preceq> Class D) = (G\<turnstile>C\<preceq>C D)"
  10.124  apply (rule iffI)
  10.125 -apply (ind_cases2 "G\<turnstile>Class C \<preceq> Class D")
  10.126 +apply (ind_cases "G\<turnstile>Class C \<preceq> Class D")
  10.127  apply (auto elim: widen.subcls)
  10.128  done
  10.129  
  10.130  lemma widen_NT_Class [simp]: "G \<turnstile> T \<preceq> NT \<Longrightarrow> G \<turnstile> T \<preceq> Class D"
  10.131 -by (ind_cases2 "G \<turnstile> T \<preceq> NT",  auto)
  10.132 +by (ind_cases "G \<turnstile> T \<preceq> NT",  auto)
  10.133  
  10.134  lemma cast_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>? RefT rT) = False"
  10.135  apply (rule iffI)
    11.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Wed Jul 11 11:29:44 2007 +0200
    11.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Jul 11 11:32:02 2007 +0200
    11.3 @@ -135,12 +135,12 @@
    11.4    done
    11.5  
    11.6  lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; ws_prog G|] ==> D \<noteq> C \<and> \<not> (subcls1 G)^++ D C"
    11.7 -apply( frule trancl.r_into_trancl [where r="subcls1 G"])
    11.8 +apply( frule tranclp.r_into_trancl [where r="subcls1 G"])
    11.9  apply( drule subcls1D)
   11.10  apply(clarify)
   11.11  apply( drule (1) class_wf_struct)
   11.12  apply( unfold ws_cdecl_def)
   11.13 -apply(force simp add: reflcl_trancl' [THEN sym] simp del: reflcl_trancl')
   11.14 +apply(force simp add: reflcl_tranclp [THEN sym] simp del: reflcl_tranclp)
   11.15  done
   11.16  
   11.17  lemma wf_cdecl_supD: 
   11.18 @@ -150,13 +150,13 @@
   11.19  done
   11.20  
   11.21  lemma subcls_asym: "[|ws_prog G; (subcls1 G)^++ C D|] ==> \<not> (subcls1 G)^++ D C"
   11.22 -apply(erule trancl.cases)
   11.23 +apply(erule tranclp.cases)
   11.24  apply(fast dest!: subcls1_wfD )
   11.25 -apply(fast dest!: subcls1_wfD intro: trancl_trans')
   11.26 +apply(fast dest!: subcls1_wfD intro: tranclp_trans)
   11.27  done
   11.28  
   11.29  lemma subcls_irrefl: "[|ws_prog G; (subcls1 G)^++ C D|] ==> C \<noteq> D"
   11.30 -apply (erule trancl_trans_induct')
   11.31 +apply (erule tranclp_trans_induct)
   11.32  apply  (auto dest: subcls1_wfD subcls_asym)
   11.33  done
   11.34  
   11.35 @@ -183,7 +183,7 @@
   11.36  apply (drule wf_prog_ws_prog)
   11.37  apply(drule wf_subcls1)
   11.38  apply(drule wfP_trancl)
   11.39 -apply(simp only: trancl_converse')
   11.40 +apply(simp only: tranclp_converse)
   11.41  apply(erule_tac a = C in wfP_induct)
   11.42  apply(rule p)
   11.43  apply(auto)
   11.44 @@ -232,7 +232,7 @@
   11.45    assume ?A thus ?thesis apply -
   11.46  apply(drule wf_subcls1)
   11.47  apply(drule wfP_trancl)
   11.48 -apply(simp only: trancl_converse')
   11.49 +apply(simp only: tranclp_converse)
   11.50  apply(erule_tac a = C in wfP_induct)
   11.51  apply(rule p)
   11.52  apply(auto)
   11.53 @@ -339,7 +339,7 @@
   11.54  apply( simp (no_asm))
   11.55  apply( erule UnE)
   11.56  apply(  force)
   11.57 -apply( erule r_into_rtrancl' [THEN rtrancl_trans'])
   11.58 +apply( erule r_into_rtranclp [THEN rtranclp_trans])
   11.59  apply auto
   11.60  done
   11.61  
   11.62 @@ -383,7 +383,7 @@
   11.63  lemma fields_mono_lemma [rule_format (no_asm)]: 
   11.64    "[|ws_prog G; (subcls1 G)^** C' C|] ==>  
   11.65    x \<in> set (fields (G,C)) --> x \<in> set (fields (G,C'))"
   11.66 -apply(erule converse_rtrancl_induct')
   11.67 +apply(erule converse_rtranclp_induct)
   11.68  apply( safe dest!: subcls1D)
   11.69  apply(subst fields_rec)
   11.70  apply(  auto)
   11.71 @@ -402,10 +402,10 @@
   11.72  "[|field (G,C) fn = Some (fd, fT); G\<turnstile>D\<preceq>C C; ws_prog G|]==>  
   11.73    map_of (fields (G,D)) (fn, fd) = Some fT"
   11.74  apply (drule field_fields)
   11.75 -apply (drule rtranclD')
   11.76 +apply (drule rtranclpD)
   11.77  apply safe
   11.78  apply (frule subcls_is_class)
   11.79 -apply (drule trancl_into_rtrancl')
   11.80 +apply (drule tranclp_into_rtranclp)
   11.81  apply (fast dest: fields_mono)
   11.82  done
   11.83  
   11.84 @@ -437,10 +437,10 @@
   11.85  apply (frule map_of_SomeD)
   11.86  apply (clarsimp simp add: wf_cdecl_def)
   11.87  apply( clarify)
   11.88 -apply( rule rtrancl_trans')
   11.89 +apply( rule rtranclp_trans)
   11.90  prefer 2
   11.91  apply(  assumption)
   11.92 -apply( rule r_into_rtrancl')
   11.93 +apply( rule r_into_rtranclp)
   11.94  apply( fast intro: subcls1I)
   11.95  done
   11.96  
   11.97 @@ -473,10 +473,10 @@
   11.98  apply (clarsimp simp add: ws_cdecl_def)
   11.99  apply blast
  11.100  apply clarify
  11.101 -apply( rule rtrancl_trans')
  11.102 +apply( rule rtranclp_trans)
  11.103  prefer 2
  11.104  apply(  assumption)
  11.105 -apply( rule r_into_rtrancl')
  11.106 +apply( rule r_into_rtranclp)
  11.107  apply( fast intro: subcls1I)
  11.108  done
  11.109  
  11.110 @@ -484,15 +484,15 @@
  11.111    "[|G\<turnstile>T'\<preceq>C T; wf_prog wf_mb G|] ==>  
  11.112     \<forall>D rT b. method (G,T) sig = Some (D,rT ,b) --> 
  11.113    (\<exists>D' rT' b'. method (G,T') sig = Some (D',rT',b') \<and> G\<turnstile>D'\<preceq>C D \<and> G\<turnstile>rT'\<preceq>rT)"
  11.114 -apply( drule rtranclD')
  11.115 +apply( drule rtranclpD)
  11.116  apply( erule disjE)
  11.117  apply(  fast)
  11.118  apply( erule conjE)
  11.119 -apply( erule trancl_trans_induct')
  11.120 +apply( erule tranclp_trans_induct)
  11.121  prefer 2
  11.122  apply(  clarify)
  11.123  apply(  drule spec, drule spec, drule spec, erule (1) impE)
  11.124 -apply(  fast elim: widen_trans rtrancl_trans')
  11.125 +apply(  fast elim: widen_trans rtranclp_trans)
  11.126  apply( clarify)
  11.127  apply( drule subcls1D)
  11.128  apply( clarify)
  11.129 @@ -512,7 +512,7 @@
  11.130  apply( unfold wf_cdecl_def)
  11.131  apply( drule map_of_SomeD)
  11.132  apply (auto simp add: wf_mrT_def)
  11.133 -apply (rule rtrancl_trans')
  11.134 +apply (rule rtranclp_trans)
  11.135  defer
  11.136  apply (rule method_wf_mhead [THEN conjunct1])
  11.137  apply (simp only: wf_prog_def)
    12.1 --- a/src/HOL/MicroJava/J/WellType.thy	Wed Jul 11 11:29:44 2007 +0200
    12.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Wed Jul 11 11:32:02 2007 +0200
    12.3 @@ -107,7 +107,7 @@
    12.4  -- "method body with parameter names, local variables, block, result expression."
    12.5  -- "local variables might include This, which is hidden anyway"
    12.6    
    12.7 -inductive2
    12.8 +inductive
    12.9    ty_expr :: "'c env => expr => ty => bool" ("_ \<turnstile> _ :: _" [51, 51, 51] 50)
   12.10    and ty_exprs :: "'c env => expr list => ty list => bool" ("_ \<turnstile> _ [::] _" [51, 51, 51] 50)
   12.11    and wt_stmt :: "'c env => stmt => bool" ("_ \<turnstile> _ \<surd>" [51, 51] 50)
    13.1 --- a/src/HOL/Nominal/Examples/Class.thy	Wed Jul 11 11:29:44 2007 +0200
    13.2 +++ b/src/HOL/Nominal/Examples/Class.thy	Wed Jul 11 11:32:02 2007 +0200
    13.3 @@ -2912,7 +2912,7 @@
    13.4    ctxtn = "(name\<times>ty) list"
    13.5    ctxtc = "(coname\<times>ty) list"
    13.6  
    13.7 -inductive2
    13.8 +inductive
    13.9    validc :: "ctxtc \<Rightarrow> bool"
   13.10  where
   13.11    vc1[intro]: "validc []"
   13.12 @@ -2920,7 +2920,7 @@
   13.13  
   13.14  equivariance validc
   13.15  
   13.16 -inductive2
   13.17 +inductive
   13.18    validn :: "ctxtn \<Rightarrow> bool"
   13.19  where
   13.20    vn1[intro]: "validn []"
   13.21 @@ -2944,7 +2944,7 @@
   13.22  
   13.23  declare abs_perm[eqvt]
   13.24  
   13.25 -inductive2
   13.26 +inductive
   13.27    fin :: "trm \<Rightarrow> name \<Rightarrow> bool"
   13.28  where
   13.29    [intro]: "fin (Ax x a) x"
   13.30 @@ -3367,7 +3367,7 @@
   13.31  apply(rule fin_supp)
   13.32  done
   13.33  
   13.34 -inductive2
   13.35 +inductive
   13.36    fic :: "trm \<Rightarrow> coname \<Rightarrow> bool"
   13.37  where
   13.38    [intro]: "fic (Ax x a) a"
   13.39 @@ -3766,7 +3766,7 @@
   13.40  apply(simp)
   13.41  done
   13.42  
   13.43 -inductive2
   13.44 +inductive
   13.45    l_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longrightarrow>\<^isub>l _" [100,100] 100)
   13.46  where
   13.47    LAxR:  "\<lbrakk>x\<sharp>M; a\<sharp>b; fic M a\<rbrakk> \<Longrightarrow> Cut <a>.M (x).(Ax x b) \<longrightarrow>\<^isub>l M[a\<turnstile>c>b]"
   13.48 @@ -4467,7 +4467,7 @@
   13.49  apply(perm_simp)+
   13.50  done
   13.51  
   13.52 -inductive2
   13.53 +inductive
   13.54    c_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longrightarrow>\<^isub>c _" [100,100] 100)
   13.55  where
   13.56    left[intro]:  "\<lbrakk>\<not>fic M a; a\<sharp>N; x\<sharp>M\<rbrakk> \<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^isub>c M{a:=(x).N}"
   13.57 @@ -4532,7 +4532,7 @@
   13.58  apply(auto simp add: abs_fresh rename_fresh subst_fresh)
   13.59  done
   13.60  
   13.61 -inductive2
   13.62 +inductive
   13.63    a_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longrightarrow>\<^isub>a _" [100,100] 100)
   13.64  where
   13.65    al_redu[intro]: "M\<longrightarrow>\<^isub>l M' \<Longrightarrow> M \<longrightarrow>\<^isub>a M'"
   13.66 @@ -5269,7 +5269,7 @@
   13.67  
   13.68  lemma ax_do_not_a_star_reduce:
   13.69    shows "Ax x a \<longrightarrow>\<^isub>a* M \<Longrightarrow> M = Ax x a"
   13.70 -apply(induct set: rtrancl)
   13.71 +apply(induct set: rtranclp)
   13.72  apply(auto)
   13.73  apply(drule  ax_do_not_a_reduce)
   13.74  apply(simp)
   13.75 @@ -5278,79 +5278,79 @@
   13.76  
   13.77  lemma a_star_CutL:
   13.78      "M \<longrightarrow>\<^isub>a* M' \<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^isub>a* Cut <a>.M' (x).N"
   13.79 -by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
   13.80 +by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
   13.81  
   13.82  lemma a_star_CutR:
   13.83      "N \<longrightarrow>\<^isub>a* N'\<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^isub>a* Cut <a>.M (x).N'"
   13.84 -by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
   13.85 +by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
   13.86  
   13.87  lemma a_star_Cut:
   13.88      "\<lbrakk>M \<longrightarrow>\<^isub>a* M'; N \<longrightarrow>\<^isub>a* N'\<rbrakk> \<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^isub>a* Cut <a>.M' (x).N'"
   13.89 -by (blast intro!: a_star_CutL a_star_CutR intro: rtrancl_trans')
   13.90 +by (blast intro!: a_star_CutL a_star_CutR intro: rtranclp_trans)
   13.91  
   13.92  lemma a_star_NotR:
   13.93      "M \<longrightarrow>\<^isub>a* M' \<Longrightarrow> NotR (x).M a \<longrightarrow>\<^isub>a* NotR (x).M' a"
   13.94 -by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
   13.95 +by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
   13.96  
   13.97  lemma a_star_NotL:
   13.98      "M \<longrightarrow>\<^isub>a* M' \<Longrightarrow> NotL <a>.M x \<longrightarrow>\<^isub>a* NotL <a>.M' x"
   13.99 -by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
  13.100 +by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
  13.101  
  13.102  lemma a_star_AndRL:
  13.103      "M \<longrightarrow>\<^isub>a* M'\<Longrightarrow> AndR <a>.M <b>.N c \<longrightarrow>\<^isub>a* AndR <a>.M' <b>.N c"
  13.104 -by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
  13.105 +by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
  13.106  
  13.107  lemma a_star_AndRR:
  13.108      "N \<longrightarrow>\<^isub>a* N'\<Longrightarrow> AndR <a>.M <b>.N c \<longrightarrow>\<^isub>a* AndR <a>.M <b>.N' c"
  13.109 -by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
  13.110 +by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
  13.111  
  13.112  lemma a_star_AndR:
  13.113      "\<lbrakk>M \<longrightarrow>\<^isub>a* M'; N \<longrightarrow>\<^isub>a* N'\<rbrakk> \<Longrightarrow> AndR <a>.M <b>.N c \<longrightarrow>\<^isub>a* AndR <a>.M' <b>.N' c"
  13.114 -by (blast intro!: a_star_AndRL a_star_AndRR intro: rtrancl_trans')
  13.115 +by (blast intro!: a_star_AndRL a_star_AndRR intro: rtranclp_trans)
  13.116  
  13.117  lemma a_star_AndL1:
  13.118      "M \<longrightarrow>\<^isub>a* M' \<Longrightarrow> AndL1 (x).M y \<longrightarrow>\<^isub>a* AndL1 (x).M' y"
  13.119 -by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
  13.120 +by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
  13.121  
  13.122  lemma a_star_AndL2:
  13.123      "M \<longrightarrow>\<^isub>a* M' \<Longrightarrow> AndL2 (x).M y \<longrightarrow>\<^isub>a* AndL2 (x).M' y"
  13.124 -by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
  13.125 +by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
  13.126  
  13.127  lemma a_star_OrLL:
  13.128      "M \<longrightarrow>\<^isub>a* M'\<Longrightarrow> OrL (x).M (y).N z \<longrightarrow>\<^isub>a* OrL (x).M' (y).N z"
  13.129 -by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
  13.130 +by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
  13.131  
  13.132  lemma a_star_OrLR:
  13.133      "N \<longrightarrow>\<^isub>a* N'\<Longrightarrow> OrL (x).M (y).N z \<longrightarrow>\<^isub>a* OrL (x).M (y).N' z"
  13.134 -by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
  13.135 +by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
  13.136  
  13.137  lemma a_star_OrL:
  13.138      "\<lbrakk>M \<longrightarrow>\<^isub>a* M'; N \<longrightarrow>\<^isub>a* N'\<rbrakk> \<Longrightarrow> OrL (x).M (y).N z \<longrightarrow>\<^isub>a* OrL (x).M' (y).N' z"
  13.139 -by (blast intro!: a_star_OrLL a_star_OrLR intro: rtrancl_trans')
  13.140 +by (blast intro!: a_star_OrLL a_star_OrLR intro: rtranclp_trans)
  13.141  
  13.142  lemma a_star_OrR1:
  13.143      "M \<longrightarrow>\<^isub>a* M' \<Longrightarrow> OrR1 <a>.M b \<longrightarrow>\<^isub>a* OrR1 <a>.M' b"
  13.144 -by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
  13.145 +by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
  13.146  
  13.147  lemma a_star_OrR2:
  13.148      "M \<longrightarrow>\<^isub>a* M' \<Longrightarrow> OrR2 <a>.M b \<longrightarrow>\<^isub>a* OrR2 <a>.M' b"
  13.149 -by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
  13.150 +by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
  13.151  
  13.152  lemma a_star_ImpLL:
  13.153      "M \<longrightarrow>\<^isub>a* M'\<Longrightarrow> ImpL <a>.M (y).N z \<longrightarrow>\<^isub>a* ImpL <a>.M' (y).N z"
  13.154 -by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
  13.155 +by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
  13.156  
  13.157  lemma a_star_ImpLR:
  13.158      "N \<longrightarrow>\<^isub>a* N'\<Longrightarrow> ImpL <a>.M (y).N z \<longrightarrow>\<^isub>a* ImpL <a>.M (y).N' z"
  13.159 -by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
  13.160 +by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
  13.161  
  13.162  lemma a_star_ImpL:
  13.163      "\<lbrakk>M \<longrightarrow>\<^isub>a* M'; N \<longrightarrow>\<^isub>a* N'\<rbrakk> \<Longrightarrow> ImpL <a>.M (y).N z \<longrightarrow>\<^isub>a* ImpL <a>.M' (y).N' z"
  13.164 -by (blast intro!: a_star_ImpLL a_star_ImpLR intro: rtrancl_trans')
  13.165 +by (blast intro!: a_star_ImpLL a_star_ImpLR intro: rtranclp_trans)
  13.166  
  13.167  lemma a_star_ImpR:
  13.168      "M \<longrightarrow>\<^isub>a* M' \<Longrightarrow> ImpR (x).<a>.M b \<longrightarrow>\<^isub>a* ImpR (x).<a>.M' b"
  13.169 -by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
  13.170 +by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
  13.171  
  13.172  lemmas a_star_congs = a_star_Cut a_star_NotR a_star_NotL a_star_AndR a_star_AndL1 a_star_AndL2
  13.173                        a_star_OrL a_star_OrR1 a_star_OrR2 a_star_ImpL a_star_ImpR
  13.174 @@ -5359,7 +5359,7 @@
  13.175    assumes a: "NotL <a>.M x \<longrightarrow>\<^isub>a* R"
  13.176    shows "\<exists>M'. R = NotL <a>.M' x \<and> M \<longrightarrow>\<^isub>a* M'"
  13.177  using a
  13.178 -apply(induct set: rtrancl)
  13.179 +apply(induct set: rtranclp)
  13.180  apply(auto)
  13.181  apply(drule a_redu_NotL_elim)
  13.182  apply(auto)
  13.183 @@ -5369,7 +5369,7 @@
  13.184    assumes a: "NotR (x).M a \<longrightarrow>\<^isub>a* R"
  13.185    shows "\<exists>M'. R = NotR (x).M' a \<and> M \<longrightarrow>\<^isub>a* M'"
  13.186  using a
  13.187 -apply(induct set: rtrancl)
  13.188 +apply(induct set: rtranclp)
  13.189  apply(auto)
  13.190  apply(drule a_redu_NotR_elim)
  13.191  apply(auto)
  13.192 @@ -5379,7 +5379,7 @@
  13.193    assumes a: "AndR <a>.M <b>.N c\<longrightarrow>\<^isub>a* R"
  13.194    shows "(\<exists>M' N'. R = AndR <a>.M' <b>.N' c \<and> M \<longrightarrow>\<^isub>a* M' \<and> N \<longrightarrow>\<^isub>a* N')"
  13.195  using a
  13.196 -apply(induct set: rtrancl)
  13.197 +apply(induct set: rtranclp)
  13.198  apply(auto)
  13.199  apply(drule a_redu_AndR_elim)
  13.200  apply(auto simp add: alpha trm.inject)
  13.201 @@ -5389,7 +5389,7 @@
  13.202    assumes a: "AndL1 (x).M y \<longrightarrow>\<^isub>a* R"
  13.203    shows "\<exists>M'. R = AndL1 (x).M' y \<and> M \<longrightarrow>\<^isub>a* M'"
  13.204  using a
  13.205 -apply(induct set: rtrancl)
  13.206 +apply(induct set: rtranclp)
  13.207  apply(auto)
  13.208  apply(drule a_redu_AndL1_elim)
  13.209  apply(auto simp add: alpha trm.inject)
  13.210 @@ -5399,7 +5399,7 @@
  13.211    assumes a: "AndL2 (x).M y \<longrightarrow>\<^isub>a* R"
  13.212    shows "\<exists>M'. R = AndL2 (x).M' y \<and> M \<longrightarrow>\<^isub>a* M'"
  13.213  using a
  13.214 -apply(induct set: rtrancl)
  13.215 +apply(induct set: rtranclp)
  13.216  apply(auto)
  13.217  apply(drule a_redu_AndL2_elim)
  13.218  apply(auto simp add: alpha trm.inject)
  13.219 @@ -5409,7 +5409,7 @@
  13.220    assumes a: "OrL (x).M (y).N z \<longrightarrow>\<^isub>a* R"
  13.221    shows "(\<exists>M' N'. R = OrL (x).M' (y).N' z \<and> M \<longrightarrow>\<^isub>a* M' \<and> N \<longrightarrow>\<^isub>a* N')"
  13.222  using a
  13.223 -apply(induct set: rtrancl)
  13.224 +apply(induct set: rtranclp)
  13.225  apply(auto)
  13.226  apply(drule a_redu_OrL_elim)
  13.227  apply(auto simp add: alpha trm.inject)
  13.228 @@ -5419,7 +5419,7 @@
  13.229    assumes a: "OrR1 <a>.M y \<longrightarrow>\<^isub>a* R"
  13.230    shows "\<exists>M'. R = OrR1 <a>.M' y \<and> M \<longrightarrow>\<^isub>a* M'"
  13.231  using a
  13.232 -apply(induct set: rtrancl)
  13.233 +apply(induct set: rtranclp)
  13.234  apply(auto)
  13.235  apply(drule a_redu_OrR1_elim)
  13.236  apply(auto simp add: alpha trm.inject)
  13.237 @@ -5429,7 +5429,7 @@
  13.238    assumes a: "OrR2 <a>.M y \<longrightarrow>\<^isub>a* R"
  13.239    shows "\<exists>M'. R = OrR2 <a>.M' y \<and> M \<longrightarrow>\<^isub>a* M'"
  13.240  using a
  13.241 -apply(induct set: rtrancl)
  13.242 +apply(induct set: rtranclp)
  13.243  apply(auto)
  13.244  apply(drule a_redu_OrR2_elim)
  13.245  apply(auto simp add: alpha trm.inject)
  13.246 @@ -5439,7 +5439,7 @@
  13.247    assumes a: "ImpR (x).<a>.M y \<longrightarrow>\<^isub>a* R"
  13.248    shows "\<exists>M'. R = ImpR (x).<a>.M' y \<and> M \<longrightarrow>\<^isub>a* M'"
  13.249  using a
  13.250 -apply(induct set: rtrancl)
  13.251 +apply(induct set: rtranclp)
  13.252  apply(auto)
  13.253  apply(drule a_redu_ImpR_elim)
  13.254  apply(auto simp add: alpha trm.inject)
  13.255 @@ -5449,7 +5449,7 @@
  13.256    assumes a: "ImpL <a>.M (y).N z \<longrightarrow>\<^isub>a* R"
  13.257    shows "(\<exists>M' N'. R = ImpL <a>.M' (y).N' z \<and> M \<longrightarrow>\<^isub>a* M' \<and> N \<longrightarrow>\<^isub>a* N')"
  13.258  using a
  13.259 -apply(induct set: rtrancl)
  13.260 +apply(induct set: rtranclp)
  13.261  apply(auto)
  13.262  apply(drule a_redu_ImpL_elim)
  13.263  apply(auto simp add: alpha trm.inject)
  13.264 @@ -5788,7 +5788,7 @@
  13.265    and      b: "M \<longrightarrow>\<^isub>a* M'"
  13.266    shows "fin M' x"
  13.267  using b a
  13.268 -apply(induct set: rtrancl)
  13.269 +apply(induct set: rtranclp)
  13.270  apply(auto simp add: fin_a_reduce)
  13.271  done
  13.272  
  13.273 @@ -5854,7 +5854,7 @@
  13.274    and      b: "M \<longrightarrow>\<^isub>a* M'"
  13.275    shows "fic M' x"
  13.276  using b a
  13.277 -apply(induct set: rtrancl)
  13.278 +apply(induct set: rtranclp)
  13.279  apply(auto simp add: fic_a_reduce)
  13.280  done
  13.281  
  13.282 @@ -10021,7 +10021,7 @@
  13.283  
  13.284  text {* SNa *}
  13.285  
  13.286 -inductive2 
  13.287 +inductive 
  13.288    SNa :: "trm \<Rightarrow> bool"
  13.289  where
  13.290    SNaI: "(\<And>M'. M \<longrightarrow>\<^isub>a M' \<Longrightarrow> SNa M') \<Longrightarrow> SNa M"
  13.291 @@ -19224,7 +19224,7 @@
  13.292  
  13.293  text {* typing relation *}
  13.294  
  13.295 -inductive2
  13.296 +inductive
  13.297     typing :: "ctxtn \<Rightarrow> trm \<Rightarrow> ctxtc \<Rightarrow> bool" ("_ \<turnstile> _ \<turnstile> _" [100,100,100] 100)
  13.298  where
  13.299    TAx:    "\<lbrakk>validn \<Gamma>;validc \<Delta>; (x,B)\<in>set \<Gamma>; (a,B)\<in>set \<Delta>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Ax x a \<turnstile> \<Delta>"