# HG changeset patch # User nipkow # Date 1008868964 -3600 # Node ID fe20540bcf93d971a4c3fd786045631f8ed130d3 # Parent 9df4b3934487452b6f3d4ef25e169d543cfca1bf renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl diff -r 9df4b3934487 -r fe20540bcf93 src/HOL/IMP/Compiler.thy --- 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 diff -r 9df4b3934487 -r fe20540bcf93 src/HOL/IMP/Transition.thy --- 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 "\c1,s1\ \\<^sub>1\<^sup>* \s2\" "\c2,s2\ \\<^sub>1\<^sup>* cs3" ultimately show "\c1;c2,s1\ \\<^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 diff -r 9df4b3934487 -r fe20540bcf93 src/HOL/Lex/RegExp2NAe.ML --- 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"; diff -r 9df4b3934487 -r fe20540bcf93 src/HOL/MicroJava/BV/Semilat.thy --- 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 \ {a. (x,a) \ r\<^sup>*} \ {b. (b,y) \ r\<^sup>*} = insert (x,x') (r \ {a. (x', a) \ r\<^sup>*} \ {b. (b, y) \ r\<^sup>*})") apply simp -apply(blast intro:rtrancl_into_rtrancl2 +apply(blast intro:converse_rtrancl_into_rtrancl elim:converse_rtranclE dest:single_valuedD) done diff -r 9df4b3934487 -r fe20540bcf93 src/HOL/MicroJava/J/WellForm.thy --- 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" diff -r 9df4b3934487 -r fe20540bcf93 src/HOL/Transitive_Closure.thy --- 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) \ R \ (b,c) \ R^* \ (a,c) \ R^*" - by (erule rtrancl_induct) (fast intro: rtrancl_into_rtrancl)+ - lemma r_r_into_trancl: "(a,b) \ R \ (b,c) \ R \ (a,c) \ R^+" by (fast intro: trancl_trans) diff -r 9df4b3934487 -r fe20540bcf93 src/HOL/Transitive_Closure_lemmas.ML --- 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"; diff -r 9df4b3934487 -r fe20540bcf93 src/HOL/Wellfounded_Recursion.ML --- 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];