src/HOL/Bali/Basis.thy
changeset 34915 7894c7dab132
parent 33965 f57c11db4ad4
child 35067 af4c18c30593
     1.1 --- a/src/HOL/Bali/Basis.thy	Sun Jan 10 18:41:07 2010 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Sun Jan 10 18:43:45 2010 +0100
     1.3 @@ -1,7 +1,5 @@
     1.4  (*  Title:      HOL/Bali/Basis.thy
     1.5 -    ID:         $Id$
     1.6      Author:     David von Oheimb
     1.7 -
     1.8  *)
     1.9  header {* Definitions extending HOL as logical basis of Bali *}
    1.10  
    1.11 @@ -66,8 +64,6 @@
    1.12   "\<lbrakk> \<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c; (a,x)\<in>r\<^sup>*; (a,y)\<in>r\<^sup>*\<rbrakk> 
    1.13   \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
    1.14  proof -
    1.15 -  note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1]
    1.16 -  note converse_rtranclE = converse_rtranclE [consumes 1] 
    1.17    assume unique: "\<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c"
    1.18    assume "(a,x)\<in>r\<^sup>*" 
    1.19    then show "(a,y)\<in>r\<^sup>* \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
    1.20 @@ -110,13 +106,6 @@
    1.21  apply (auto dest: rtrancl_into_trancl1)
    1.22  done
    1.23  
    1.24 -(* ### To Transitive_Closure *)
    1.25 -theorems converse_rtrancl_induct 
    1.26 - = converse_rtrancl_induct [consumes 1,case_names Id Step]
    1.27 -
    1.28 -theorems converse_trancl_induct 
    1.29 -         = converse_trancl_induct [consumes 1,case_names Single Step]
    1.30 -
    1.31  (* context (theory "Set") *)
    1.32  lemma Ball_weaken:"\<lbrakk>Ball s P;\<And> x. P x\<longrightarrow>Q x\<rbrakk>\<Longrightarrow>Ball s Q"
    1.33  by auto