src/HOL/MicroJava/J/WellForm.thy

   apply (erule_tac x = x in allE)
   apply clarify
   apply (auto intro!: map_of_SomeI)
   done
 
-lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; ws_prog G|] ==> D \<noteq> C \<and> \<not>(D,C)\<in>(subcls1 G)^+"
-apply( frule r_into_trancl)
+lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; ws_prog G|] ==> D \<noteq> C \<and> \<not> (subcls1 G)^++ D C"
+apply( frule trancl.r_into_trancl [where r="subcls1 G"])
 apply( drule subcls1D)
 apply(clarify)
 apply( drule (1) class_wf_struct)
 apply( unfold ws_cdecl_def)
-apply(force simp add: reflcl_trancl [THEN sym] simp del: reflcl_trancl)
+apply(force simp add: reflcl_trancl' [THEN sym] simp del: reflcl_trancl')
 done
 
 lemma wf_cdecl_supD: 
 "!!r. \<lbrakk>ws_cdecl G (C,D,r); C \<noteq> Object\<rbrakk> \<Longrightarrow> is_class G D"
 apply (unfold ws_cdecl_def)
 apply (auto split add: option.split_asm)
 done
 
-lemma subcls_asym: "[|ws_prog G; (C,D)\<in>(subcls1 G)^+|] ==> \<not>(D,C)\<in>(subcls1 G)^+"
-apply(erule tranclE)
+lemma subcls_asym: "[|ws_prog G; (subcls1 G)^++ C D|] ==> \<not> (subcls1 G)^++ D C"
+apply(erule trancl.cases)
 apply(fast dest!: subcls1_wfD )
-apply(fast dest!: subcls1_wfD intro: trancl_trans)
-done
-
-lemma subcls_irrefl: "[|ws_prog G; (C,D)\<in>(subcls1 G)^+|] ==> C \<noteq> D"
-apply (erule trancl_trans_induct)
+apply(fast dest!: subcls1_wfD intro: trancl_trans')
+done
+
+lemma subcls_irrefl: "[|ws_prog G; (subcls1 G)^++ C D|] ==> C \<noteq> D"
+apply (erule trancl_trans_induct')
 apply  (auto dest: subcls1_wfD subcls_asym)
 done
 
-lemma acyclic_subcls1: "ws_prog G ==> acyclic (subcls1 G)"
-apply (unfold acyclic_def)
+lemma acyclic_subcls1: "ws_prog G ==> acyclicP (subcls1 G)"
+apply (simp add: acyclic_def [to_pred])
 apply (fast dest: subcls_irrefl)
 done
 
-lemma wf_subcls1: "ws_prog G ==> wf ((subcls1 G)^-1)"
-apply (rule finite_acyclic_wf)
-apply ( subst finite_converse)
+lemma wf_subcls1: "ws_prog G ==> wfP ((subcls1 G)^--1)"
+apply (rule finite_acyclic_wf [to_pred])
+apply ( subst finite_converse [to_pred])
 apply ( rule finite_subcls1)
-apply (subst acyclic_converse)
+apply (subst acyclic_converse [to_pred])
 apply (erule acyclic_subcls1)
 done
 
 
 lemma subcls_induct: 
-"[|wf_prog wf_mb G; !!C. \<forall>D. (C,D)\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C"
+"[|wf_prog wf_mb G; !!C. \<forall>D. (subcls1 G)^++ C D --> P D ==> P C|] ==> P C"
 (is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
 proof -
   assume p: "PROP ?P"
   assume ?A thus ?thesis apply -
 apply (drule wf_prog_ws_prog)
 apply(drule wf_subcls1)
-apply(drule wf_trancl)
-apply(simp only: trancl_converse)
-apply(erule_tac a = C in wf_induct)
+apply(drule wfP_trancl)
+apply(simp only: trancl_converse')
+apply(erule_tac a = C in wfP_induct)
 apply(rule p)
 apply(auto)
 done
 qed
 

 apply auto
 done
 qed
 
 lemma subcls_induct_struct: 
-"[|ws_prog G; !!C. \<forall>D. (C,D)\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C"
+"[|ws_prog G; !!C. \<forall>D. (subcls1 G)^++ C D --> P D ==> P C|] ==> P C"
 (is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
 proof -
   assume p: "PROP ?P"
   assume ?A thus ?thesis apply -
 apply(drule wf_subcls1)
-apply(drule wf_trancl)
-apply(simp only: trancl_converse)
-apply(erule_tac a = C in wf_induct)
+apply(drule wfP_trancl)
+apply(simp only: trancl_converse')
+apply(erule_tac a = C in wfP_induct)
 apply(rule p)
 apply(auto)
 done
 qed
 

 apply( rule ballI)
 apply( simp (no_asm_simp) only: split_tupled_all)
 apply( simp (no_asm))
 apply( erule UnE)
 apply(  force)
-apply( erule r_into_rtrancl [THEN rtrancl_trans])
+apply( erule r_into_rtrancl' [THEN rtrancl_trans'])
 apply auto
 done
 
 lemma widen_fields_defpl: 
   "[|((fn,fd),fT) \<in> set (fields (G,C)); ws_prog G; is_class G C|] ==>  

 apply(  simp)
 apply(auto dest!: widen_fields_defpl)
 done
 
 lemma fields_mono_lemma [rule_format (no_asm)]: 
-  "[|ws_prog G; (C',C)\<in>(subcls1 G)^*|] ==>  
+  "[|ws_prog G; (subcls1 G)^** C' C|] ==>  
   x \<in> set (fields (G,C)) --> x \<in> set (fields (G,C'))"
-apply(erule converse_rtrancl_induct)
+apply(erule converse_rtrancl_induct')
 apply( safe dest!: subcls1D)
 apply(subst fields_rec)
 apply(  auto)
 done
 

 
 lemma widen_cfs_fields: 
 "[|field (G,C) fn = Some (fd, fT); G\<turnstile>D\<preceq>C C; ws_prog G|]==>  
   map_of (fields (G,D)) (fn, fd) = Some fT"
 apply (drule field_fields)
-apply (drule rtranclD)
+apply (drule rtranclD')
 apply safe
 apply (frule subcls_is_class)
-apply (drule trancl_into_rtrancl)
+apply (drule trancl_into_rtrancl')
 apply (fast dest: fields_mono)
 done
 
 lemma method_wf_mdecl [rule_format (no_asm)]: 
   "wf_prog wf_mb G ==> is_class G C \<Longrightarrow>   

 apply( erule disjE)
 apply(  erule_tac V = "?P --> ?Q" in thin_rl)
 apply (frule map_of_SomeD)
 apply (clarsimp simp add: wf_cdecl_def)
 apply( clarify)
-apply( rule rtrancl_trans)
-prefer 2
-apply(  assumption)
-apply( rule r_into_rtrancl)
+apply( rule rtrancl_trans')
+prefer 2
+apply(  assumption)
+apply( rule r_into_rtrancl')
 apply( fast intro: subcls1I)
 done
 
 
 lemma method_wf_mhead [rule_format (no_asm)]: 

 apply(  erule_tac V = "?P --> ?Q" in thin_rl)
 apply (frule map_of_SomeD)
 apply (clarsimp simp add: ws_cdecl_def)
 apply blast
 apply clarify
-apply( rule rtrancl_trans)
-prefer 2
-apply(  assumption)
-apply( rule r_into_rtrancl)
+apply( rule rtrancl_trans')
+prefer 2
+apply(  assumption)
+apply( rule r_into_rtrancl')
 apply( fast intro: subcls1I)
 done
 
 lemma subcls_widen_methd [rule_format (no_asm)]: 
   "[|G\<turnstile>T'\<preceq>C T; wf_prog wf_mb G|] ==>  
    \<forall>D rT b. method (G,T) sig = Some (D,rT ,b) --> 
   (\<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)"
-apply( drule rtranclD)
+apply( drule rtranclD')
 apply( erule disjE)
 apply(  fast)
 apply( erule conjE)
-apply( erule trancl_trans_induct)
+apply( erule trancl_trans_induct')
 prefer 2
 apply(  clarify)
 apply(  drule spec, drule spec, drule spec, erule (1) impE)
-apply(  fast elim: widen_trans rtrancl_trans)
+apply(  fast elim: widen_trans rtrancl_trans')
 apply( clarify)
 apply( drule subcls1D)
 apply( clarify)
 apply( subst method_rec)
 apply(  assumption)

 apply( frule (1) class_wf)
 apply( simp (no_asm_simp) only: split_tupled_all)
 apply( unfold wf_cdecl_def)
 apply( drule map_of_SomeD)
 apply (auto simp add: wf_mrT_def)
-apply (rule rtrancl_trans)
+apply (rule rtrancl_trans')
 defer
 apply (rule method_wf_mhead [THEN conjunct1])
 apply (simp only: wf_prog_def)
 apply (simp add: is_class_def)
 apply assumption