src/HOL/Nominal/Examples/CR.thy

 theory CR
 imports Lam_Funs
 begin
 
-text {* The Church-Rosser proof from Barendregt's book *}
+text \<open>The Church-Rosser proof from Barendregt's book\<close>
 
 lemma forget: 
   assumes asm: "x\<sharp>L"
   shows "L[x::=P] = L"
 using asm

   have "x\<sharp>L" by fact
   show "Var z[x::=N][y::=L] = Var z[y::=L][x::=N[y::=L]]" (is "?LHS = ?RHS")
   proof -
     { (*Case 1.1*)
       assume  "z=x"
-      have "(1)": "?LHS = N[y::=L]" using `z=x` by simp
-      have "(2)": "?RHS = N[y::=L]" using `z=x` `x\<noteq>y` by simp
+      have "(1)": "?LHS = N[y::=L]" using \<open>z=x\<close> by simp
+      have "(2)": "?RHS = N[y::=L]" using \<open>z=x\<close> \<open>x\<noteq>y\<close> by simp
       from "(1)" "(2)" have "?LHS = ?RHS"  by simp
     }
     moreover 
     { (*Case 1.2*)
       assume "z=y" and "z\<noteq>x" 
-      have "(1)": "?LHS = L"               using `z\<noteq>x` `z=y` by simp
-      have "(2)": "?RHS = L[x::=N[y::=L]]" using `z=y` by simp
-      have "(3)": "L[x::=N[y::=L]] = L"    using `x\<sharp>L` by (simp add: forget)
+      have "(1)": "?LHS = L"               using \<open>z\<noteq>x\<close> \<open>z=y\<close> by simp
+      have "(2)": "?RHS = L[x::=N[y::=L]]" using \<open>z=y\<close> by simp
+      have "(3)": "L[x::=N[y::=L]] = L"    using \<open>x\<sharp>L\<close> by (simp add: forget)
       from "(1)" "(2)" "(3)" have "?LHS = ?RHS" by simp
     }
     moreover 
     { (*Case 1.3*)
       assume "z\<noteq>x" and "z\<noteq>y"
-      have "(1)": "?LHS = Var z" using `z\<noteq>x` `z\<noteq>y` by simp
-      have "(2)": "?RHS = Var z" using `z\<noteq>x` `z\<noteq>y` by simp
+      have "(1)": "?LHS = Var z" using \<open>z\<noteq>x\<close> \<open>z\<noteq>y\<close> by simp
+      have "(2)": "?RHS = Var z" using \<open>z\<noteq>x\<close> \<open>z\<noteq>y\<close> by simp
       from "(1)" "(2)" have "?LHS = ?RHS" by simp
     }
     ultimately show "?LHS = ?RHS" by blast
   qed
 next

   have "x\<sharp>L" by fact
   have fs: "z\<sharp>x" "z\<sharp>y" "z\<sharp>N" "z\<sharp>L" by fact+
   hence "z\<sharp>N[y::=L]" by (simp add: fresh_fact)
   show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") 
   proof - 
-    have "?LHS = Lam [z].(M1[x::=N][y::=L])" using `z\<sharp>x` `z\<sharp>y` `z\<sharp>N` `z\<sharp>L` by simp
-    also from ih have "\<dots> = Lam [z].(M1[y::=L][x::=N[y::=L]])" using `x\<noteq>y` `x\<sharp>L` by simp
-    also have "\<dots> = (Lam [z].(M1[y::=L]))[x::=N[y::=L]]" using `z\<sharp>x` `z\<sharp>N[y::=L]` by simp
-    also have "\<dots> = ?RHS" using  `z\<sharp>y` `z\<sharp>L` by simp
+    have "?LHS = Lam [z].(M1[x::=N][y::=L])" using \<open>z\<sharp>x\<close> \<open>z\<sharp>y\<close> \<open>z\<sharp>N\<close> \<open>z\<sharp>L\<close> by simp
+    also from ih have "\<dots> = Lam [z].(M1[y::=L][x::=N[y::=L]])" using \<open>x\<noteq>y\<close> \<open>x\<sharp>L\<close> by simp
+    also have "\<dots> = (Lam [z].(M1[y::=L]))[x::=N[y::=L]]" using \<open>z\<sharp>x\<close> \<open>z\<sharp>N[y::=L]\<close> by simp
+    also have "\<dots> = ?RHS" using  \<open>z\<sharp>y\<close> \<open>z\<sharp>L\<close> by simp
     finally show "?LHS = ?RHS" .
   qed
 next
   case (App M1 M2) (* case 3: applications *)
   thus "(App M1 M2)[x::=N][y::=L] = (App M1 M2)[y::=L][x::=N[y::=L]]" by simp

   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
   using asm 
 by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
    (auto simp add: fresh_fact forget)
 
-section {* Beta Reduction *}
+section \<open>Beta Reduction\<close>
 
 inductive
   "Beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^sub>\<beta> _" [80,80] 80)
 where
     b1[intro]: "s1\<longrightarrow>\<^sub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^sub>\<beta>(App s2 t)"

   and     a2: "M2\<longrightarrow>\<^sub>\<beta>\<^sup>* M3"
   shows "M1 \<longrightarrow>\<^sub>\<beta>\<^sup>* M3"
 using a2 a1
 by (induct) (auto)
 
-section {* One-Reduction *}
+section \<open>One-Reduction\<close>
 
 inductive
   One :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^sub>1 _" [80,80] 80)
 where
     o1[intro!]:      "M\<longrightarrow>\<^sub>1M"

          (\<exists>s1 s2. M = s1[a::=s2] \<and> t1 \<longrightarrow>\<^sub>1 s1 \<and> t2 \<longrightarrow>\<^sub>1 s2)" 
 using a
 by (cases rule: One.strong_cases [where a="a" and aa="a"])
    (auto dest: one_abs simp add: lam.inject abs_fresh alpha fresh_prod)
 
-text {* first case in Lemma 3.2.4*}
+text \<open>first case in Lemma 3.2.4\<close>
 
 lemma one_subst_aux:
   assumes a: "N\<longrightarrow>\<^sub>1N'"
   shows "M[x::=N] \<longrightarrow>\<^sub>1 M[x::=N']"
 using a