src/HOL/Proofs/Lambda/Commutation.thy

 (*  Title:      HOL/Proofs/Lambda/Commutation.thy
     Author:     Tobias Nipkow
     Copyright   1995  TU Muenchen
 *)
 
-section {* Abstract commutation and confluence notions *}
+section \<open>Abstract commutation and confluence notions\<close>
 
 theory Commutation
 imports Main
 begin
 
 declare [[syntax_ambiguity_warning = false]]
 
 
-subsection {* Basic definitions *}
+subsection \<open>Basic definitions\<close>
 
 definition
   square :: "['a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool, 'a => 'a => bool] => bool" where
   "square R S T U =
     (\<forall>x y. R x y --> (\<forall>z. S x z --> (\<exists>u. T y u \<and> U z u)))"

 abbreviation
   confluent :: "('a => 'a => bool) => bool" where
   "confluent R == diamond (R^**)"
 
 
-subsection {* Basic lemmas *}
-
-subsubsection {* @{text "square"} *}
+subsection \<open>Basic lemmas\<close>
+
+subsubsection \<open>\<open>square\<close>\<close>
 
 lemma square_sym: "square R S T U ==> square S R U T"
   apply (unfold square_def)
   apply blast
   done

   apply (unfold commute_def)
   apply (fastforce dest: square_reflcl square_sym [THEN square_rtrancl])
   done
 
 
-subsubsection {* @{text "commute"} *}
+subsubsection \<open>\<open>commute\<close>\<close>
 
 lemma commute_sym: "commute R S ==> commute S R"
   apply (unfold commute_def)
   apply (blast intro: square_sym)
   done

   apply (unfold commute_def square_def)
   apply blast
   done
 
 
-subsubsection {* @{text "diamond"}, @{text "confluence"}, and @{text "union"} *}
+subsubsection \<open>\<open>diamond\<close>, \<open>confluence\<close>, and \<open>union\<close>\<close>
 
 lemma diamond_Un:
     "[| diamond R; diamond S; commute R S |] ==> diamond (sup R S)"
   apply (unfold diamond_def)
   apply (blast intro: commute_Un commute_sym) 

   apply (force intro: diamond_confluent
     dest: rtranclp_subset [symmetric])
   done
 
 
-subsection {* Church-Rosser *}
+subsection \<open>Church-Rosser\<close>
 
 lemma Church_Rosser_confluent: "Church_Rosser R = confluent R"
   apply (unfold square_def commute_def diamond_def Church_Rosser_def)
-  apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
-   apply (tactic {*
+  apply (tactic \<open>safe_tac (put_claset HOL_cs @{context})\<close>)
+   apply (tactic \<open>
      blast_tac (put_claset HOL_cs @{context} addIs
        [@{thm sup_ge2} RS @{thm rtranclp_mono} RS @{thm predicate2D} RS @{thm rtranclp_trans},
         @{thm rtranclp_converseI}, @{thm conversepI},
-        @{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1 *})
+        @{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1\<close>)
   apply (erule rtranclp_induct)
    apply blast
   apply (blast del: rtranclp.rtrancl_refl intro: rtranclp_trans)
   done
 
 
-subsection {* Newman's lemma *}
-
-text {* Proof by Stefan Berghofer *}
+subsection \<open>Newman's lemma\<close>
+
+text \<open>Proof by Stefan Berghofer\<close>
 
 theorem newman:
   assumes wf: "wfP (R\<inverse>\<inverse>)"
   and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
     \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"

       with cw show ?thesis by iprover
     qed
   qed
 qed
 
-text {*
+text \<open>
   Alternative version.  Partly automated by Tobias
   Nipkow. Takes 2 minutes (2002).
 
-  This is the maximal amount of automation possible using @{text blast}.
-*}
+  This is the maximal amount of automation possible using \<open>blast\<close>.
+\<close>
 
 theorem newman':
   assumes wf: "wfP (R\<inverse>\<inverse>)"
   and lc: "\<And>a b c. R a b \<Longrightarrow> R a c \<Longrightarrow>
     \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
   shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
     \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
   using wf
 proof induct
   case (less x b c)
-  note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
-                     \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d`
+  note IH = \<open>\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
+                     \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d\<close>
   have xc: "R\<^sup>*\<^sup>* x c" by fact
   have xb: "R\<^sup>*\<^sup>* x b" by fact
   thus ?case
   proof (rule converse_rtranclpE)
     assume "x = b"

             dest: IH [OF conversepI, OF xy] IH [OF conversepI, OF xy'])
     qed
   qed
 qed
 
-text {*
+text \<open>
   Using the coherent logic prover, the proof of the induction step
   is completely automatic.
-*}
+\<close>
 
 lemma eq_imp_rtranclp: "x = y \<Longrightarrow> r\<^sup>*\<^sup>* x y"
   by simp
 
 theorem newman'':

   shows "\<And>b c. R\<^sup>*\<^sup>* a b \<Longrightarrow> R\<^sup>*\<^sup>* a c \<Longrightarrow>
     \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d"
   using wf
 proof induct
   case (less x b c)
-  note IH = `\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
-                     \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d`
+  note IH = \<open>\<And>y b c. \<lbrakk>R\<inverse>\<inverse> y x; R\<^sup>*\<^sup>* y b; R\<^sup>*\<^sup>* y c\<rbrakk>
+                     \<Longrightarrow> \<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* c d\<close>
   show ?case
     by (coherent
-      `R\<^sup>*\<^sup>* x c` `R\<^sup>*\<^sup>* x b`
+      \<open>R\<^sup>*\<^sup>* x c\<close> \<open>R\<^sup>*\<^sup>* x b\<close>
       refl [where 'a='a] sym
       eq_imp_rtranclp
       r_into_rtranclp [of R]
       rtranclp_trans
       lc IH [OF conversepI]