src/HOL/Lambda/Commutation.thy
changeset 23750 a1db5f819d00
parent 23464 bc2563c37b1a
child 23815 73dbab55d283
     1.1 --- a/src/HOL/Lambda/Commutation.thy	Wed Jul 11 11:22:02 2007 +0200
     1.2 +++ b/src/HOL/Lambda/Commutation.thy	Wed Jul 11 11:23:24 2007 +0200
     1.3 @@ -58,9 +58,9 @@
     1.4      "square R S S T ==> square (R^**) S S (T^**)"
     1.5    apply (unfold square_def)
     1.6    apply (intro strip)
     1.7 -  apply (erule rtrancl_induct')
     1.8 +  apply (erule rtranclp_induct)
     1.9     apply blast
    1.10 -  apply (blast intro: rtrancl.rtrancl_into_rtrancl)
    1.11 +  apply (blast intro: rtranclp.rtrancl_into_rtrancl)
    1.12    done
    1.13  
    1.14  lemma square_rtrancl_reflcl_commute:
    1.15 @@ -110,14 +110,14 @@
    1.16  
    1.17  lemma confluent_Un:
    1.18      "[| confluent R; confluent S; commute (R^**) (S^**) |] ==> confluent (sup R S)"
    1.19 -  apply (rule rtrancl_Un_rtrancl' [THEN subst])
    1.20 +  apply (rule rtranclp_sup_rtranclp [THEN subst])
    1.21    apply (blast dest: diamond_Un intro: diamond_confluent)
    1.22    done
    1.23  
    1.24  lemma diamond_to_confluence:
    1.25      "[| diamond R; T \<le> R; R \<le> T^** |] ==> confluent T"
    1.26    apply (force intro: diamond_confluent
    1.27 -    dest: rtrancl_subset' [symmetric])
    1.28 +    dest: rtranclp_subset [symmetric])
    1.29    done
    1.30  
    1.31  
    1.32 @@ -128,12 +128,12 @@
    1.33    apply (tactic {* safe_tac HOL_cs *})
    1.34     apply (tactic {*
    1.35       blast_tac (HOL_cs addIs
    1.36 -       [thm "sup_ge2" RS thm "rtrancl_mono'" RS thm "predicate2D" RS thm "rtrancl_trans'",
    1.37 -        thm "rtrancl_converseI'", thm "conversepI",
    1.38 -        thm "sup_ge1" RS thm "rtrancl_mono'" RS thm "predicate2D"]) 1 *})
    1.39 -  apply (erule rtrancl_induct')
    1.40 +       [thm "sup_ge2" RS thm "rtranclp_mono" RS thm "predicate2D" RS thm "rtranclp_trans",
    1.41 +        thm "rtranclp_converseI", thm "conversepI",
    1.42 +        thm "sup_ge1" RS thm "rtranclp_mono" RS thm "predicate2D"]) 1 *})
    1.43 +  apply (erule rtranclp_induct)
    1.44     apply blast
    1.45 -  apply (blast del: rtrancl.rtrancl_refl intro: rtrancl_trans')
    1.46 +  apply (blast del: rtranclp.rtrancl_refl intro: rtranclp_trans)
    1.47    done
    1.48  
    1.49  
    1.50 @@ -152,7 +152,7 @@
    1.51    case (less x b c)
    1.52    have xc: "R\<^sup>*\<^sup>* x c" by fact
    1.53    have xb: "R\<^sup>*\<^sup>* x b" by fact thus ?case
    1.54 -  proof (rule converse_rtranclE')
    1.55 +  proof (rule converse_rtranclpE)
    1.56      assume "x = b"
    1.57      with xc have "R\<^sup>*\<^sup>* b c" by simp
    1.58      thus ?thesis by iprover
    1.59 @@ -161,7 +161,7 @@
    1.60      assume xy: "R x y"
    1.61      assume yb: "R\<^sup>*\<^sup>* y b"
    1.62      from xc show ?thesis
    1.63 -    proof (rule converse_rtranclE')
    1.64 +    proof (rule converse_rtranclpE)
    1.65        assume "x = c"
    1.66        with xb have "R\<^sup>*\<^sup>* c b" by simp
    1.67        thus ?thesis by iprover
    1.68 @@ -175,11 +175,11 @@
    1.69        from this and yb yu have "\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* u d" by (rule less)
    1.70        then obtain v where bv: "R\<^sup>*\<^sup>* b v" and uv: "R\<^sup>*\<^sup>* u v" by iprover
    1.71        from xy' have "R\<inverse>\<inverse> y' x" ..
    1.72 -      moreover from y'u and uv have "R\<^sup>*\<^sup>* y' v" by (rule rtrancl_trans')
    1.73 +      moreover from y'u and uv have "R\<^sup>*\<^sup>* y' v" by (rule rtranclp_trans)
    1.74        moreover note y'c
    1.75        ultimately have "\<exists>d. R\<^sup>*\<^sup>* v d \<and> R\<^sup>*\<^sup>* c d" by (rule less)
    1.76        then obtain w where vw: "R\<^sup>*\<^sup>* v w" and cw: "R\<^sup>*\<^sup>* c w" by iprover
    1.77 -      from bv vw have "R\<^sup>*\<^sup>* b w" by (rule rtrancl_trans')
    1.78 +      from bv vw have "R\<^sup>*\<^sup>* b w" by (rule rtranclp_trans)
    1.79        with cw show ?thesis by iprover
    1.80      qed
    1.81    qed
    1.82 @@ -206,7 +206,7 @@
    1.83    have xc: "R\<^sup>*\<^sup>* x c" by fact
    1.84    have xb: "R\<^sup>*\<^sup>* x b" by fact
    1.85    thus ?case
    1.86 -  proof (rule converse_rtranclE')
    1.87 +  proof (rule converse_rtranclpE)
    1.88      assume "x = b"
    1.89      with xc have "R\<^sup>*\<^sup>* b c" by simp
    1.90      thus ?thesis by iprover
    1.91 @@ -215,7 +215,7 @@
    1.92      assume xy: "R x y"
    1.93      assume yb: "R\<^sup>*\<^sup>* y b"
    1.94      from xc show ?thesis
    1.95 -    proof (rule converse_rtranclE')
    1.96 +    proof (rule converse_rtranclpE)
    1.97        assume "x = c"
    1.98        with xb have "R\<^sup>*\<^sup>* c b" by simp
    1.99        thus ?thesis by iprover
   1.100 @@ -226,8 +226,8 @@
   1.101        with xy obtain u where u: "R\<^sup>*\<^sup>* y u" "R\<^sup>*\<^sup>* y' u"
   1.102          by (blast dest: lc)
   1.103        from yb u y'c show ?thesis
   1.104 -        by (blast del: rtrancl.rtrancl_refl
   1.105 -            intro: rtrancl_trans'
   1.106 +        by (blast del: rtranclp.rtrancl_refl
   1.107 +            intro: rtranclp_trans
   1.108              dest: IH [OF conversepI, OF xy] IH [OF conversepI, OF xy'])
   1.109      qed
   1.110    qed