1.1 --- a/src/HOL/IMP/Compiler.thy Thu Dec 20 17:08:55 2001 +0100
1.2 +++ b/src/HOL/IMP/Compiler.thy Thu Dec 20 18:22:44 2001 +0100
1.3 @@ -135,7 +135,7 @@
1.4 subsection "Compiler correctness"
1.5
1.6 declare rtrancl_into_rtrancl[trans]
1.7 - rtrancl_into_rtrancl2[trans]
1.8 + converse_rtrancl_into_rtrancl[trans]
1.9 rtrancl_trans[trans]
1.10
1.11 text {*
1.12 @@ -232,7 +232,7 @@
1.13 apply(erule_tac x = "a@[?I]" in allE)
1.14 apply(simp)
1.15 (* execute JMPF: *)
1.16 - apply(rule rtrancl_into_rtrancl2)
1.17 + apply(rule converse_rtrancl_into_rtrancl)
1.18 apply(force intro!: JMPFT)
1.19 (* execute compile c0: *)
1.20 apply(rule rtrancl_trans)
1.21 @@ -245,7 +245,7 @@
1.22 apply(intro strip)
1.23 apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE)
1.24 apply(simp add:add_assoc)
1.25 - apply(rule rtrancl_into_rtrancl2)
1.26 + apply(rule converse_rtrancl_into_rtrancl)
1.27 apply(force intro!: JMPFF)
1.28 apply(blast)
1.29 apply(force intro: JMPFF)
1.30 @@ -253,12 +253,12 @@
1.31 apply(erule_tac x = "a@[?I]" in allE)
1.32 apply(erule_tac x = a in allE)
1.33 apply(simp)
1.34 -apply(rule rtrancl_into_rtrancl2)
1.35 +apply(rule converse_rtrancl_into_rtrancl)
1.36 apply(force intro!: JMPFT)
1.37 apply(rule rtrancl_trans)
1.38 apply(erule allE)
1.39 apply assumption
1.40 -apply(rule rtrancl_into_rtrancl2)
1.41 +apply(rule converse_rtrancl_into_rtrancl)
1.42 apply(force intro!: JMPB)
1.43 apply(simp)
1.44 done
2.1 --- a/src/HOL/IMP/Transition.thy Thu Dec 20 17:08:55 2001 +0100
2.2 +++ b/src/HOL/IMP/Transition.thy Thu Dec 20 18:22:44 2001 +0100
2.3 @@ -501,12 +501,12 @@
2.4 apply (fast dest: rtrancl_imp_UN_rel_pow intro: semiI)
2.5
2.6 -- IF
2.7 -apply (fast intro: rtrancl_into_rtrancl2)
2.8 -apply (fast intro: rtrancl_into_rtrancl2)
2.9 +apply (fast intro: converse_rtrancl_into_rtrancl)
2.10 +apply (fast intro: converse_rtrancl_into_rtrancl)
2.11
2.12 -- WHILE
2.13 apply fast
2.14 -apply (fast dest: rtrancl_imp_UN_rel_pow intro: rtrancl_into_rtrancl2 semiI)
2.15 +apply (fast dest: rtrancl_imp_UN_rel_pow intro: converse_rtrancl_into_rtrancl semiI)
2.16
2.17 done
2.18
2.19 @@ -518,7 +518,7 @@
2.20 apply fastsimp
2.21 -- "induction step"
2.22 apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2
2.23 - elim!: rel_pow_imp_rtrancl rtrancl_into_rtrancl2)
2.24 + elim!: rel_pow_imp_rtrancl converse_rtrancl_into_rtrancl)
2.25 done
2.26
2.27 lemma evalc1_impl_evalc [rule_format (no_asm)]:
2.28 @@ -598,7 +598,7 @@
2.29 apply fast
2.30 apply clarify
2.31 apply (case_tac c)
2.32 - apply (auto intro: rtrancl_into_rtrancl2)
2.33 + apply (auto intro: converse_rtrancl_into_rtrancl)
2.34 done
2.35 moreover assume "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle>" "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
2.36 ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" by simp
2.37 @@ -617,12 +617,12 @@
2.38 apply (fast intro: my_lemma1)
2.39
2.40 -- IF
2.41 -apply (fast intro: rtrancl_into_rtrancl2)
2.42 -apply (fast intro: rtrancl_into_rtrancl2)
2.43 +apply (fast intro: converse_rtrancl_into_rtrancl)
2.44 +apply (fast intro: converse_rtrancl_into_rtrancl)
2.45
2.46 -- WHILE
2.47 apply fast
2.48 -apply (fast intro: rtrancl_into_rtrancl2 my_lemma1)
2.49 +apply (fast intro: converse_rtrancl_into_rtrancl my_lemma1)
2.50
2.51 done
2.52
3.1 --- a/src/HOL/Lex/RegExp2NAe.ML Thu Dec 20 17:08:55 2001 +0100
3.2 +++ b/src/HOL/Lex/RegExp2NAe.ML Thu Dec 20 18:22:44 2001 +0100
3.3 @@ -160,7 +160,7 @@
3.4 by (etac rtrancl_induct 1);
3.5 by (Blast_tac 1);
3.6 by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
3.7 -by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
3.8 +by (blast_tac (claset() addIs [converse_rtrancl_into_rtrancl]) 1);
3.9 qed "unfold_rtrancl2";
3.10
3.11 Goal
3.12 @@ -351,7 +351,7 @@
3.13 by (Clarify_tac 1);
3.14 by (rtac (rtrancl_trans) 1);
3.15 by (etac lemma2a 1);
3.16 -by (rtac (rtrancl_into_rtrancl2) 1);
3.17 +by (rtac converse_rtrancl_into_rtrancl 1);
3.18 by (etac True_False_eps_concI 1);
3.19 by (etac lemma2b 1);
3.20 qed "True_epsclosure_conc";
4.1 --- a/src/HOL/MicroJava/BV/Semilat.thy Thu Dec 20 17:08:55 2001 +0100
4.2 +++ b/src/HOL/MicroJava/BV/Semilat.thy Thu Dec 20 18:22:44 2001 +0100
4.3 @@ -198,8 +198,8 @@
4.4 apply (blast elim: converse_rtranclE dest: single_valuedD)
4.5 apply (rule exI)
4.6 apply (rule conjI)
4.7 - apply (blast intro: rtrancl_into_rtrancl2 dest: single_valuedD)
4.8 -apply (blast intro: rtrancl_into_rtrancl rtrancl_into_rtrancl2
4.9 + apply (blast intro: converse_rtrancl_into_rtrancl dest: single_valuedD)
4.10 +apply (blast intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl
4.11 elim: converse_rtranclE dest: single_valuedD)
4.12 done
4.13
4.14 @@ -210,7 +210,7 @@
4.15 apply clarify
4.16 apply (erule converse_rtrancl_induct)
4.17 apply blast
4.18 - apply (blast intro: rtrancl_into_rtrancl2)
4.19 + apply (blast intro: converse_rtrancl_into_rtrancl)
4.20 apply (blast intro: extend_lub)
4.21 done
4.22
4.23 @@ -246,7 +246,7 @@
4.24 apply(subgoal_tac "r \<inter> {a. (x,a) \<in> r\<^sup>*} \<times> {b. (b,y) \<in> r\<^sup>*} =
4.25 insert (x,x') (r \<inter> {a. (x', a) \<in> r\<^sup>*} \<times> {b. (b, y) \<in> r\<^sup>*})")
4.26 apply simp
4.27 -apply(blast intro:rtrancl_into_rtrancl2
4.28 +apply(blast intro:converse_rtrancl_into_rtrancl
4.29 elim:converse_rtranclE dest:single_valuedD)
4.30 done
4.31
5.1 --- a/src/HOL/MicroJava/J/WellForm.thy Thu Dec 20 17:08:55 2001 +0100
5.2 +++ b/src/HOL/MicroJava/J/WellForm.thy Thu Dec 20 18:22:44 2001 +0100
5.3 @@ -178,7 +178,7 @@
5.4 apply( assumption)
5.5 apply( fast)
5.6 apply(auto dest!: wf_cdecl_supD)
5.7 -apply(erule (1) rtrancl_into_rtrancl2)
5.8 +apply(erule (1) converse_rtrancl_into_rtrancl)
5.9 done
5.10
5.11 lemma is_type_rTI: "wf_mhead G sig rT ==> is_type G rT"
6.1 --- a/src/HOL/Transitive_Closure.thy Thu Dec 20 17:08:55 2001 +0100
6.2 +++ b/src/HOL/Transitive_Closure.thy Thu Dec 20 18:22:44 2001 +0100
6.3 @@ -97,9 +97,6 @@
6.4
6.5 (* more about converse rtrancl and trancl, should be merged with main body *)
6.6
6.7 -lemma converse_rtrancl_into_rtrancl: "(a,b) \<in> R \<Longrightarrow> (b,c) \<in> R^* \<Longrightarrow> (a,c) \<in> R^*"
6.8 - by (erule rtrancl_induct) (fast intro: rtrancl_into_rtrancl)+
6.9 -
6.10 lemma r_r_into_trancl: "(a,b) \<in> R \<Longrightarrow> (b,c) \<in> R \<Longrightarrow> (a,c) \<in> R^+"
6.11 by (fast intro: trancl_trans)
6.12
7.1 --- a/src/HOL/Transitive_Closure_lemmas.ML Thu Dec 20 17:08:55 2001 +0100
7.2 +++ b/src/HOL/Transitive_Closure_lemmas.ML Thu Dec 20 18:22:44 2001 +0100
7.3 @@ -68,7 +68,7 @@
7.4 by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
7.5 qed "rtranclE";
7.6
7.7 -bind_thm ("rtrancl_into_rtrancl2", r_into_rtrancl RS rtrancl_trans);
7.8 +bind_thm ("converse_rtrancl_into_rtrancl", r_into_rtrancl RS rtrancl_trans);
7.9
7.10 (*** More r^* equations and inclusions ***)
7.11
7.12 @@ -167,7 +167,7 @@
7.13
7.14 Goal "r O r^* = r^* O r";
7.15 by (blast_tac (claset() addEs [rtranclE, converse_rtranclE]
7.16 - addIs [rtrancl_into_rtrancl, rtrancl_into_rtrancl2]) 1);
7.17 + addIs [rtrancl_into_rtrancl, converse_rtrancl_into_rtrancl]) 1);
7.18 qed "r_comp_rtrancl_eq";
7.19
7.20
8.1 --- a/src/HOL/Wellfounded_Recursion.ML Thu Dec 20 17:08:55 2001 +0100
8.2 +++ b/src/HOL/Wellfounded_Recursion.ML Thu Dec 20 18:22:44 2001 +0100
8.3 @@ -133,7 +133,7 @@
8.4 by (assume_tac 1);
8.5 by (thin_tac "ALL Q. (EX x. x : Q) --> ?P Q" 1); (*essential for speed*)
8.6 (*Blast_tac with new substOccur fails*)
8.7 -by (best_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
8.8 +by (best_tac (claset() addIs [converse_rtrancl_into_rtrancl]) 1);
8.9 qed "wf_insert";
8.10 AddIffs [wf_insert];
8.11