just a few mods to a few thms
authornipkow
Mon Mar 17 18:38:50 2003 +0100 (2003-03-17)
changeset 138671fdecd15437f
parent 13866 b42d7983a822
child 13868 01b516b64233
just a few mods to a few thms
src/HOL/Bali/Basis.thy
src/HOL/Hoare/Separation.thy
src/HOL/NanoJava/TypeRel.thy
src/HOL/Transitive_Closure.thy
src/HOL/Wellfounded_Recursion.ML
src/HOL/Wellfounded_Relations.ML
     1.1 --- a/src/HOL/Bali/Basis.thy	Mon Mar 17 17:37:48 2003 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Mon Mar 17 18:38:50 2003 +0100
     1.3 @@ -62,11 +62,10 @@
     1.4  apply auto
     1.5  done
     1.6  
     1.7 -(* context (theory "Transitive_Closure") *)
     1.8 +(* irrefl_tranclI in Transitive_Closure.thy is more general *)
     1.9  lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+"
    1.10 -apply (rule allI)
    1.11 -apply (erule irrefl_tranclI)
    1.12 -done
    1.13 +by(blast elim: tranclE dest: trancl_into_rtrancl)
    1.14 +
    1.15  
    1.16  lemma trancl_rtrancl_trancl:
    1.17  "\<lbrakk>(x,y)\<in>r^+; (y,z)\<in>r^*\<rbrakk> \<Longrightarrow> (x,z)\<in>r^+"
     2.1 --- a/src/HOL/Hoare/Separation.thy	Mon Mar 17 17:37:48 2003 +0100
     2.2 +++ b/src/HOL/Hoare/Separation.thy	Mon Mar 17 18:38:50 2003 +0100
     2.3 @@ -64,7 +64,7 @@
     2.4  
     2.5  lemma "VARS H x y z w
     2.6   {[x\<mapsto>y] ** [z\<mapsto>w]}
     2.7 - SKIP
     2.8 + y := w
     2.9   {x \<noteq> z}"
    2.10  apply vcg
    2.11  apply(auto simp:star_def R_def singl_def)
     3.1 --- a/src/HOL/NanoJava/TypeRel.thy	Mon Mar 17 17:37:48 2003 +0100
     3.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Mon Mar 17 18:38:50 2003 +0100
     3.3 @@ -83,11 +83,10 @@
     3.4  lemma subcls1_irrefl_lemma1: "ws_prog \<Longrightarrow> subcls1^-1 \<inter> subcls1^+ = {}"
     3.5  by (fast dest: subcls1D ws_progD)
     3.6  
     3.7 -(* context (theory "Transitive_Closure") *)
     3.8 +(* irrefl_tranclI in Transitive_Closure.thy is more general *)
     3.9  lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+"
    3.10 -apply (rule allI)
    3.11 -apply (erule irrefl_tranclI)
    3.12 -done
    3.13 +by(blast elim: tranclE dest: trancl_into_rtrancl)
    3.14 +
    3.15  
    3.16  lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI']
    3.17  
     4.1 --- a/src/HOL/Transitive_Closure.thy	Mon Mar 17 17:37:48 2003 +0100
     4.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Mar 17 18:38:50 2003 +0100
     4.3 @@ -341,13 +341,8 @@
     4.4    apply (blast intro: rtrancl_trans)
     4.5    done
     4.6  
     4.7 -lemma irrefl_tranclI: "r^-1 \<inter> r^+ = {} ==> (x, x) \<notin> r^+"
     4.8 -  apply (subgoal_tac "ALL y. (x, y) : r^+ --> x \<noteq> y")
     4.9 -   apply fast
    4.10 -  apply (intro strip)
    4.11 -  apply (erule trancl_induct)
    4.12 -   apply (auto intro: r_into_trancl)
    4.13 -  done
    4.14 +lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+"
    4.15 +by(blast elim: tranclE dest: trancl_into_rtrancl)
    4.16  
    4.17  lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y"
    4.18    by (blast dest: r_into_trancl)
     5.1 --- a/src/HOL/Wellfounded_Recursion.ML	Mon Mar 17 17:37:48 2003 +0100
     5.2 +++ b/src/HOL/Wellfounded_Recursion.ML	Mon Mar 17 18:38:50 2003 +0100
     5.3 @@ -52,6 +52,7 @@
     5.4  Goal "wf(r) ==> (a,a) ~: r";
     5.5  by (blast_tac (claset() addEs [wf_asym]) 1);
     5.6  qed "wf_not_refl";
     5.7 +Addsimps [wf_not_refl];
     5.8  
     5.9  (* [| wf r;  (a,a) ~: r ==> PROP W |] ==> PROP W *)
    5.10  bind_thm ("wf_irrefl", make_elim wf_not_refl);
     6.1 --- a/src/HOL/Wellfounded_Relations.ML	Mon Mar 17 17:37:48 2003 +0100
     6.2 +++ b/src/HOL/Wellfounded_Relations.ML	Mon Mar 17 18:38:50 2003 +0100
     6.3 @@ -43,6 +43,7 @@
     6.4  by (mp_tac 1);
     6.5  by (Blast_tac 1);
     6.6  qed "wf_inv_image";
     6.7 +Addsimps [wf_inv_image];
     6.8  AddSIs [wf_inv_image];
     6.9  
    6.10