--- a/src/HOL/Bali/Basis.thy Mon Mar 17 17:37:48 2003 +0100
+++ b/src/HOL/Bali/Basis.thy Mon Mar 17 18:38:50 2003 +0100
@@ -62,11 +62,10 @@
apply auto
done
-(* context (theory "Transitive_Closure") *)
+(* irrefl_tranclI in Transitive_Closure.thy is more general *)
lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+"
-apply (rule allI)
-apply (erule irrefl_tranclI)
-done
+by(blast elim: tranclE dest: trancl_into_rtrancl)
+
lemma trancl_rtrancl_trancl:
"\<lbrakk>(x,y)\<in>r^+; (y,z)\<in>r^*\<rbrakk> \<Longrightarrow> (x,z)\<in>r^+"
--- a/src/HOL/Hoare/Separation.thy Mon Mar 17 17:37:48 2003 +0100
+++ b/src/HOL/Hoare/Separation.thy Mon Mar 17 18:38:50 2003 +0100
@@ -64,7 +64,7 @@
lemma "VARS H x y z w
{[x\<mapsto>y] ** [z\<mapsto>w]}
- SKIP
+ y := w
{x \<noteq> z}"
apply vcg
apply(auto simp:star_def R_def singl_def)
--- a/src/HOL/NanoJava/TypeRel.thy Mon Mar 17 17:37:48 2003 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy Mon Mar 17 18:38:50 2003 +0100
@@ -83,11 +83,10 @@
lemma subcls1_irrefl_lemma1: "ws_prog \<Longrightarrow> subcls1^-1 \<inter> subcls1^+ = {}"
by (fast dest: subcls1D ws_progD)
-(* context (theory "Transitive_Closure") *)
+(* irrefl_tranclI in Transitive_Closure.thy is more general *)
lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+"
-apply (rule allI)
-apply (erule irrefl_tranclI)
-done
+by(blast elim: tranclE dest: trancl_into_rtrancl)
+
lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI']
--- a/src/HOL/Transitive_Closure.thy Mon Mar 17 17:37:48 2003 +0100
+++ b/src/HOL/Transitive_Closure.thy Mon Mar 17 18:38:50 2003 +0100
@@ -341,13 +341,8 @@
apply (blast intro: rtrancl_trans)
done
-lemma irrefl_tranclI: "r^-1 \<inter> r^+ = {} ==> (x, x) \<notin> r^+"
- apply (subgoal_tac "ALL y. (x, y) : r^+ --> x \<noteq> y")
- apply fast
- apply (intro strip)
- apply (erule trancl_induct)
- apply (auto intro: r_into_trancl)
- done
+lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+"
+by(blast elim: tranclE dest: trancl_into_rtrancl)
lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y"
by (blast dest: r_into_trancl)
--- a/src/HOL/Wellfounded_Recursion.ML Mon Mar 17 17:37:48 2003 +0100
+++ b/src/HOL/Wellfounded_Recursion.ML Mon Mar 17 18:38:50 2003 +0100
@@ -52,6 +52,7 @@
Goal "wf(r) ==> (a,a) ~: r";
by (blast_tac (claset() addEs [wf_asym]) 1);
qed "wf_not_refl";
+Addsimps [wf_not_refl];
(* [| wf r; (a,a) ~: r ==> PROP W |] ==> PROP W *)
bind_thm ("wf_irrefl", make_elim wf_not_refl);
--- a/src/HOL/Wellfounded_Relations.ML Mon Mar 17 17:37:48 2003 +0100
+++ b/src/HOL/Wellfounded_Relations.ML Mon Mar 17 18:38:50 2003 +0100
@@ -43,6 +43,7 @@
by (mp_tac 1);
by (Blast_tac 1);
qed "wf_inv_image";
+Addsimps [wf_inv_image];
AddSIs [wf_inv_image];