reverted accidential corruption of superscripts introduced in a508148f7c25
authorkrauss
Fri Aug 14 21:28:58 2009 +0200 (2009-08-14)
changeset 3237666b4946d9483
parent 32375 d33f5a96df0b
child 32377 99dc5b7b4687
reverted accidential corruption of superscripts introduced in a508148f7c25
src/HOL/Bali/Basis.thy
     1.1 --- a/src/HOL/Bali/Basis.thy	Fri Aug 14 17:27:34 2009 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Fri Aug 14 21:28:58 2009 +0200
     1.3 @@ -63,36 +63,36 @@
     1.4  by (auto intro: r_into_rtrancl rtrancl_trans)
     1.5  
     1.6  lemma triangle_lemma:
     1.7 - "\<lbrakk> \<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c; (a,x)\<in>r*; (a,y)\<in>r*\<rbrakk> 
     1.8 - \<Longrightarrow> (x,y)\<in>r* \<or> (y,x)\<in>r*"
     1.9 + "\<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.10 + \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
    1.11  proof -
    1.12    note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1]
    1.13    note converse_rtranclE = converse_rtranclE [consumes 1] 
    1.14    assume unique: "\<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c"
    1.15 -  assume "(a,x)\<in>r*" 
    1.16 -  then show "(a,y)\<in>r* \<Longrightarrow> (x,y)\<in>r* \<or> (y,x)\<in>r*"
    1.17 +  assume "(a,x)\<in>r\<^sup>*" 
    1.18 +  then show "(a,y)\<in>r\<^sup>* \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
    1.19    proof (induct rule: converse_rtrancl_induct)
    1.20 -    assume "(x,y)\<in>r*"
    1.21 +    assume "(x,y)\<in>r\<^sup>*"
    1.22      then show ?thesis 
    1.23        by blast
    1.24    next
    1.25      fix a v
    1.26      assume a_v_r: "(a, v) \<in> r" and
    1.27 -          v_x_rt: "(v, x) \<in> r*" and
    1.28 -          a_y_rt: "(a, y) \<in> r*"  and
    1.29 -             hyp: "(v, y) \<in> r* \<Longrightarrow> (x, y) \<in> r* \<or> (y, x) \<in> r*"
    1.30 +          v_x_rt: "(v, x) \<in> r\<^sup>*" and
    1.31 +          a_y_rt: "(a, y) \<in> r\<^sup>*"  and
    1.32 +             hyp: "(v, y) \<in> r\<^sup>* \<Longrightarrow> (x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
    1.33      from a_y_rt 
    1.34 -    show "(x, y) \<in> r* \<or> (y, x) \<in> r*"
    1.35 +    show "(x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
    1.36      proof (cases rule: converse_rtranclE)
    1.37        assume "a=y"
    1.38 -      with a_v_r v_x_rt have "(y,x) \<in> r*"
    1.39 +      with a_v_r v_x_rt have "(y,x) \<in> r\<^sup>*"
    1.40  	by (auto intro: r_into_rtrancl rtrancl_trans)
    1.41        then show ?thesis 
    1.42  	by blast
    1.43      next
    1.44        fix w 
    1.45        assume a_w_r: "(a, w) \<in> r" and
    1.46 -            w_y_rt: "(w, y) \<in> r*"
    1.47 +            w_y_rt: "(w, y) \<in> r\<^sup>*"
    1.48        from a_v_r a_w_r unique 
    1.49        have "v=w" 
    1.50  	by auto
    1.51 @@ -105,7 +105,7 @@
    1.52  
    1.53  
    1.54  lemma rtrancl_cases [consumes 1, case_names Refl Trancl]:
    1.55 - "\<lbrakk>(a,b)\<in>r*;  a = b \<Longrightarrow> P; (a,b)\<in>r+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.56 + "\<lbrakk>(a,b)\<in>r\<^sup>*;  a = b \<Longrightarrow> P; (a,b)\<in>r\<^sup>+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.57  apply (erule rtranclE)
    1.58  apply (auto dest: rtrancl_into_trancl1)
    1.59  done