src/HOL/Bali/Basis.thy
 changeset 32367 a508148f7c25 parent 32149 ef59550a55d3 child 32376 66b4946d9483
```     1.1 --- a/src/HOL/Bali/Basis.thy	Thu Aug 13 17:19:10 2009 +0100
1.2 +++ b/src/HOL/Bali/Basis.thy	Thu Aug 13 17:19:42 2009 +0100
1.3 @@ -7,8 +7,6 @@
1.4
1.5  theory Basis imports Main begin
1.6
1.7 -declare [[unify_search_bound = 40, unify_trace_bound = 40]]
1.8 -
1.9
1.10  section "misc"
1.11
1.12 @@ -65,36 +63,36 @@
1.13  by (auto intro: r_into_rtrancl rtrancl_trans)
1.14
1.15  lemma triangle_lemma:
1.16 - "\<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.17 - \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
1.18 + "\<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.19 + \<Longrightarrow> (x,y)\<in>r* \<or> (y,x)\<in>r*"
1.20  proof -
1.21    note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1]
1.22    note converse_rtranclE = converse_rtranclE [consumes 1]
1.23    assume unique: "\<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c"
1.24 -  assume "(a,x)\<in>r\<^sup>*"
1.25 -  then show "(a,y)\<in>r\<^sup>* \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
1.26 +  assume "(a,x)\<in>r*"
1.27 +  then show "(a,y)\<in>r* \<Longrightarrow> (x,y)\<in>r* \<or> (y,x)\<in>r*"
1.28    proof (induct rule: converse_rtrancl_induct)
1.29 -    assume "(x,y)\<in>r\<^sup>*"
1.30 +    assume "(x,y)\<in>r*"
1.31      then show ?thesis
1.32        by blast
1.33    next
1.34      fix a v
1.35      assume a_v_r: "(a, v) \<in> r" and
1.36 -          v_x_rt: "(v, x) \<in> r\<^sup>*" and
1.37 -          a_y_rt: "(a, y) \<in> r\<^sup>*"  and
1.38 -             hyp: "(v, y) \<in> r\<^sup>* \<Longrightarrow> (x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
1.39 +          v_x_rt: "(v, x) \<in> r*" and
1.40 +          a_y_rt: "(a, y) \<in> r*"  and
1.41 +             hyp: "(v, y) \<in> r* \<Longrightarrow> (x, y) \<in> r* \<or> (y, x) \<in> r*"
1.42      from a_y_rt
1.43 -    show "(x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
1.44 +    show "(x, y) \<in> r* \<or> (y, x) \<in> r*"
1.45      proof (cases rule: converse_rtranclE)
1.46        assume "a=y"
1.47 -      with a_v_r v_x_rt have "(y,x) \<in> r\<^sup>*"
1.48 +      with a_v_r v_x_rt have "(y,x) \<in> r*"
1.49  	by (auto intro: r_into_rtrancl rtrancl_trans)
1.50        then show ?thesis
1.51  	by blast
1.52      next
1.53        fix w
1.54        assume a_w_r: "(a, w) \<in> r" and
1.55 -            w_y_rt: "(w, y) \<in> r\<^sup>*"
1.56 +            w_y_rt: "(w, y) \<in> r*"
1.57        from a_v_r a_w_r unique
1.58        have "v=w"
1.59  	by auto
1.60 @@ -107,7 +105,7 @@
1.61
1.62
1.63  lemma rtrancl_cases [consumes 1, case_names Refl Trancl]:
1.64 - "\<lbrakk>(a,b)\<in>r\<^sup>*;  a = b \<Longrightarrow> P; (a,b)\<in>r\<^sup>+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
1.65 + "\<lbrakk>(a,b)\<in>r*;  a = b \<Longrightarrow> P; (a,b)\<in>r+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
1.66  apply (erule rtranclE)
1.67  apply (auto dest: rtrancl_into_trancl1)
1.68  done
```