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