renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
authornipkow
Thu Dec 20 18:22:44 2001 +0100 (2001-12-20)
changeset 12566fe20540bcf93
parent 12565 9df4b3934487
child 12567 614ef5ca41ed
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
src/HOL/IMP/Compiler.thy
src/HOL/IMP/Transition.thy
src/HOL/Lex/RegExp2NAe.ML
src/HOL/MicroJava/BV/Semilat.thy
src/HOL/MicroJava/J/WellForm.thy
src/HOL/Transitive_Closure.thy
src/HOL/Transitive_Closure_lemmas.ML
src/HOL/Wellfounded_Recursion.ML
     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