--- a/src/HOL/IMP/Compiler.thy Thu Dec 20 17:08:55 2001 +0100
+++ b/src/HOL/IMP/Compiler.thy Thu Dec 20 18:22:44 2001 +0100
@@ -135,7 +135,7 @@
subsection "Compiler correctness"
declare rtrancl_into_rtrancl[trans]
- rtrancl_into_rtrancl2[trans]
+ converse_rtrancl_into_rtrancl[trans]
rtrancl_trans[trans]
text {*
@@ -232,7 +232,7 @@
apply(erule_tac x = "a@[?I]" in allE)
apply(simp)
(* execute JMPF: *)
- apply(rule rtrancl_into_rtrancl2)
+ apply(rule converse_rtrancl_into_rtrancl)
apply(force intro!: JMPFT)
(* execute compile c0: *)
apply(rule rtrancl_trans)
@@ -245,7 +245,7 @@
apply(intro strip)
apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE)
apply(simp add:add_assoc)
- apply(rule rtrancl_into_rtrancl2)
+ apply(rule converse_rtrancl_into_rtrancl)
apply(force intro!: JMPFF)
apply(blast)
apply(force intro: JMPFF)
@@ -253,12 +253,12 @@
apply(erule_tac x = "a@[?I]" in allE)
apply(erule_tac x = a in allE)
apply(simp)
-apply(rule rtrancl_into_rtrancl2)
+apply(rule converse_rtrancl_into_rtrancl)
apply(force intro!: JMPFT)
apply(rule rtrancl_trans)
apply(erule allE)
apply assumption
-apply(rule rtrancl_into_rtrancl2)
+apply(rule converse_rtrancl_into_rtrancl)
apply(force intro!: JMPB)
apply(simp)
done
--- a/src/HOL/IMP/Transition.thy Thu Dec 20 17:08:55 2001 +0100
+++ b/src/HOL/IMP/Transition.thy Thu Dec 20 18:22:44 2001 +0100
@@ -501,12 +501,12 @@
apply (fast dest: rtrancl_imp_UN_rel_pow intro: semiI)
-- IF
-apply (fast intro: rtrancl_into_rtrancl2)
-apply (fast intro: rtrancl_into_rtrancl2)
+apply (fast intro: converse_rtrancl_into_rtrancl)
+apply (fast intro: converse_rtrancl_into_rtrancl)
-- WHILE
apply fast
-apply (fast dest: rtrancl_imp_UN_rel_pow intro: rtrancl_into_rtrancl2 semiI)
+apply (fast dest: rtrancl_imp_UN_rel_pow intro: converse_rtrancl_into_rtrancl semiI)
done
@@ -518,7 +518,7 @@
apply fastsimp
-- "induction step"
apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2
- elim!: rel_pow_imp_rtrancl rtrancl_into_rtrancl2)
+ elim!: rel_pow_imp_rtrancl converse_rtrancl_into_rtrancl)
done
lemma evalc1_impl_evalc [rule_format (no_asm)]:
@@ -598,7 +598,7 @@
apply fast
apply clarify
apply (case_tac c)
- apply (auto intro: rtrancl_into_rtrancl2)
+ apply (auto intro: converse_rtrancl_into_rtrancl)
done
moreover assume "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle>" "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" by simp
@@ -617,12 +617,12 @@
apply (fast intro: my_lemma1)
-- IF
-apply (fast intro: rtrancl_into_rtrancl2)
-apply (fast intro: rtrancl_into_rtrancl2)
+apply (fast intro: converse_rtrancl_into_rtrancl)
+apply (fast intro: converse_rtrancl_into_rtrancl)
-- WHILE
apply fast
-apply (fast intro: rtrancl_into_rtrancl2 my_lemma1)
+apply (fast intro: converse_rtrancl_into_rtrancl my_lemma1)
done
--- a/src/HOL/Lex/RegExp2NAe.ML Thu Dec 20 17:08:55 2001 +0100
+++ b/src/HOL/Lex/RegExp2NAe.ML Thu Dec 20 18:22:44 2001 +0100
@@ -160,7 +160,7 @@
by (etac rtrancl_induct 1);
by (Blast_tac 1);
by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
-by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
+by (blast_tac (claset() addIs [converse_rtrancl_into_rtrancl]) 1);
qed "unfold_rtrancl2";
Goal
@@ -351,7 +351,7 @@
by (Clarify_tac 1);
by (rtac (rtrancl_trans) 1);
by (etac lemma2a 1);
-by (rtac (rtrancl_into_rtrancl2) 1);
+by (rtac converse_rtrancl_into_rtrancl 1);
by (etac True_False_eps_concI 1);
by (etac lemma2b 1);
qed "True_epsclosure_conc";
--- a/src/HOL/MicroJava/BV/Semilat.thy Thu Dec 20 17:08:55 2001 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy Thu Dec 20 18:22:44 2001 +0100
@@ -198,8 +198,8 @@
apply (blast elim: converse_rtranclE dest: single_valuedD)
apply (rule exI)
apply (rule conjI)
- apply (blast intro: rtrancl_into_rtrancl2 dest: single_valuedD)
-apply (blast intro: rtrancl_into_rtrancl rtrancl_into_rtrancl2
+ apply (blast intro: converse_rtrancl_into_rtrancl dest: single_valuedD)
+apply (blast intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl
elim: converse_rtranclE dest: single_valuedD)
done
@@ -210,7 +210,7 @@
apply clarify
apply (erule converse_rtrancl_induct)
apply blast
- apply (blast intro: rtrancl_into_rtrancl2)
+ apply (blast intro: converse_rtrancl_into_rtrancl)
apply (blast intro: extend_lub)
done
@@ -246,7 +246,7 @@
apply(subgoal_tac "r \<inter> {a. (x,a) \<in> r\<^sup>*} \<times> {b. (b,y) \<in> r\<^sup>*} =
insert (x,x') (r \<inter> {a. (x', a) \<in> r\<^sup>*} \<times> {b. (b, y) \<in> r\<^sup>*})")
apply simp
-apply(blast intro:rtrancl_into_rtrancl2
+apply(blast intro:converse_rtrancl_into_rtrancl
elim:converse_rtranclE dest:single_valuedD)
done
--- a/src/HOL/MicroJava/J/WellForm.thy Thu Dec 20 17:08:55 2001 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy Thu Dec 20 18:22:44 2001 +0100
@@ -178,7 +178,7 @@
apply( assumption)
apply( fast)
apply(auto dest!: wf_cdecl_supD)
-apply(erule (1) rtrancl_into_rtrancl2)
+apply(erule (1) converse_rtrancl_into_rtrancl)
done
lemma is_type_rTI: "wf_mhead G sig rT ==> is_type G rT"
--- a/src/HOL/Transitive_Closure.thy Thu Dec 20 17:08:55 2001 +0100
+++ b/src/HOL/Transitive_Closure.thy Thu Dec 20 18:22:44 2001 +0100
@@ -97,9 +97,6 @@
(* more about converse rtrancl and trancl, should be merged with main body *)
-lemma converse_rtrancl_into_rtrancl: "(a,b) \<in> R \<Longrightarrow> (b,c) \<in> R^* \<Longrightarrow> (a,c) \<in> R^*"
- by (erule rtrancl_induct) (fast intro: rtrancl_into_rtrancl)+
-
lemma r_r_into_trancl: "(a,b) \<in> R \<Longrightarrow> (b,c) \<in> R \<Longrightarrow> (a,c) \<in> R^+"
by (fast intro: trancl_trans)
--- a/src/HOL/Transitive_Closure_lemmas.ML Thu Dec 20 17:08:55 2001 +0100
+++ b/src/HOL/Transitive_Closure_lemmas.ML Thu Dec 20 18:22:44 2001 +0100
@@ -68,7 +68,7 @@
by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
qed "rtranclE";
-bind_thm ("rtrancl_into_rtrancl2", r_into_rtrancl RS rtrancl_trans);
+bind_thm ("converse_rtrancl_into_rtrancl", r_into_rtrancl RS rtrancl_trans);
(*** More r^* equations and inclusions ***)
@@ -167,7 +167,7 @@
Goal "r O r^* = r^* O r";
by (blast_tac (claset() addEs [rtranclE, converse_rtranclE]
- addIs [rtrancl_into_rtrancl, rtrancl_into_rtrancl2]) 1);
+ addIs [rtrancl_into_rtrancl, converse_rtrancl_into_rtrancl]) 1);
qed "r_comp_rtrancl_eq";
--- a/src/HOL/Wellfounded_Recursion.ML Thu Dec 20 17:08:55 2001 +0100
+++ b/src/HOL/Wellfounded_Recursion.ML Thu Dec 20 18:22:44 2001 +0100
@@ -133,7 +133,7 @@
by (assume_tac 1);
by (thin_tac "ALL Q. (EX x. x : Q) --> ?P Q" 1); (*essential for speed*)
(*Blast_tac with new substOccur fails*)
-by (best_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
+by (best_tac (claset() addIs [converse_rtrancl_into_rtrancl]) 1);
qed "wf_insert";
AddIffs [wf_insert];