src/HOL/Lambda/Commutation.thy
 changeset 18241 afdba6b3e383 parent 17589 58eeffd73be1 child 18513 791b53bf4073
```     1.1 --- a/src/HOL/Lambda/Commutation.thy	Wed Nov 23 22:23:52 2005 +0100
1.2 +++ b/src/HOL/Lambda/Commutation.thy	Wed Nov 23 22:26:13 2005 +0100
1.3 @@ -197,11 +197,11 @@
1.4      \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
1.5    shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
1.6                 \<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
1.7 -using wf
1.8 +  using wf
1.9  proof induct
1.10    case (less x b c)
1.11 -  have IH: "\<And>y b c. \<lbrakk>(y,x) \<in> R\<inverse>; (y,b) \<in> R\<^sup>*; (y,c) \<in> R\<^sup>*\<rbrakk>
1.12 -                     \<Longrightarrow> \<exists>d. (b,d) \<in> R\<^sup>* \<and> (c,d) \<in> R\<^sup>*" by(rule less)
1.13 +  note IH = `\<And>y b c. \<lbrakk>(y,x) \<in> R\<inverse>; (y,b) \<in> R\<^sup>*; (y,c) \<in> R\<^sup>*\<rbrakk>
1.14 +                     \<Longrightarrow> \<exists>d. (b,d) \<in> R\<^sup>* \<and> (c,d) \<in> R\<^sup>*`
1.15    have xc: "(x, c) \<in> R\<^sup>*" .
1.16    have xb: "(x, b) \<in> R\<^sup>*" .
1.17    thus ?case
1.18 @@ -223,11 +223,11 @@
1.19        assume y'c: "(y', c) \<in> R\<^sup>*"
1.20        assume xy': "(x, y') \<in> R"
1.21        with xy obtain u where u: "(y, u) \<in> R\<^sup>*" "(y', u) \<in> R\<^sup>*"
1.22 -	by (blast dest:lc)
1.23 +        by (blast dest: lc)
1.24        from yb u y'c show ?thesis
1.25 -	by(blast del: rtrancl_refl
1.26 -		 intro:rtrancl_trans
1.27 -                 dest:IH[OF xy[symmetric]] IH[OF xy'[symmetric]])
1.28 +        by (blast del: rtrancl_refl
1.29 +            intro: rtrancl_trans
1.30 +            dest: IH [OF xy [symmetric]] IH [OF xy' [symmetric]])
1.31      qed
1.32    qed
1.33  qed
```