# HG changeset patch
# User nipkow
# Date 1047922730 -3600
# Node ID 1fdecd15437fd7a3ae24c901322a891b2ecb31ec
# Parent  b42d7983a8222f544e7978ed0ab51987fcf06369
just a few mods to a few thms

diff -r b42d7983a822 -r 1fdecd15437f src/HOL/Bali/Basis.thy
--- 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^+"
diff -r b42d7983a822 -r 1fdecd15437f src/HOL/Hoare/Separation.thy
--- 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)
diff -r b42d7983a822 -r 1fdecd15437f src/HOL/NanoJava/TypeRel.thy
--- 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']
 
diff -r b42d7983a822 -r 1fdecd15437f src/HOL/Transitive_Closure.thy
--- 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)
diff -r b42d7983a822 -r 1fdecd15437f src/HOL/Wellfounded_Recursion.ML
--- 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);
diff -r b42d7983a822 -r 1fdecd15437f src/HOL/Wellfounded_Relations.ML
--- 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];