src/HOL/Proofs/Lambda/Standardization.thy

 (*  Title:      HOL/Proofs/Lambda/Standardization.thy
     Author:     Stefan Berghofer
     Copyright   2005 TU Muenchen
 *)
 
-section {* Standardization *}
+section \<open>Standardization\<close>
 
 theory Standardization
 imports NormalForm
 begin
 
-text {*
+text \<open>
 Based on lecture notes by Ralph Matthes @{cite "Matthes-ESSLLI2000"},
 original proof idea due to Ralph Loader @{cite Loader1998}.
-*}
-
-
-subsection {* Standard reduction relation *}
+\<close>
+
+
+subsection \<open>Standard reduction relation\<close>
 
 declare listrel_mono [mono_set]
 
 inductive
   sred :: "dB \<Rightarrow> dB \<Rightarrow> bool"  (infixl "\<rightarrow>\<^sub>s" 50)

 next
   case (Abs r r' ss ss')
   from Abs(3) have "ss [\<rightarrow>\<^sub>s] ss'" by (rule listrelp_conj1)
   moreover have "[s] [\<rightarrow>\<^sub>s] [s']" by (iprover intro: s listrelp.intros)
   ultimately have "ss @ [s] [\<rightarrow>\<^sub>s] ss' @ [s']" by (rule listrelp_app)
-  with `r \<rightarrow>\<^sub>s r'` have "Abs r \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> (ss' @ [s'])"
+  with \<open>r \<rightarrow>\<^sub>s r'\<close> have "Abs r \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> (ss' @ [s'])"
     by (rule sred.Abs)
   thus ?case by (simp only: app_last)
 next
   case (Beta r u ss t)
   hence "r[u/0] \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s t \<degree> s'" by (simp only: app_last)

   from Var(1) rs have "rs [\<rightarrow>\<^sub>s] ss" by (rule lemma4_aux)
   hence "Var x \<degree>\<degree> rs \<rightarrow>\<^sub>s Var x \<degree>\<degree> ss" by (rule sred.Var)
   with r'' show ?case by simp
 next
   case (Abs r r' ss ss')
-  from `Abs r' \<degree>\<degree> ss' \<rightarrow>\<^sub>\<beta> r''` show ?case
+  from \<open>Abs r' \<degree>\<degree> ss' \<rightarrow>\<^sub>\<beta> r''\<close> show ?case
   proof
     fix s
     assume r'': "r'' = s \<degree>\<degree> ss'"
     assume "Abs r' \<rightarrow>\<^sub>\<beta> s"
     then obtain r''' where s: "s = Abs r'''" and r''': "r' \<rightarrow>\<^sub>\<beta> r'''" by cases auto

     with r'' s show "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by simp
   next
     fix rs'
     assume "ss' => rs'"
     with Abs(3) have "ss [\<rightarrow>\<^sub>s] rs'" by (rule lemma4_aux)
-    with `r \<rightarrow>\<^sub>s r'` have "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> rs'" by (rule sred.Abs)
+    with \<open>r \<rightarrow>\<^sub>s r'\<close> have "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> rs'" by (rule sred.Abs)
     moreover assume "r'' = Abs r' \<degree>\<degree> rs'"
     ultimately show "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by simp
   next
     fix t u' us'
     assume "ss' = u' # us'"

   assumes r: "r \<rightarrow>\<^sub>\<beta>\<^sup>* r'"
   shows "r \<rightarrow>\<^sub>s r'" using r
   by induct (iprover intro: refl_sred lemma4)+
 
 
-subsection {* Leftmost reduction and weakly normalizing terms *}
+subsection \<open>Leftmost reduction and weakly normalizing terms\<close>
 
 inductive
   lred :: "dB \<Rightarrow> dB \<Rightarrow> bool"  (infixl "\<rightarrow>\<^sub>l" 50)
   and lredlist :: "dB list \<Rightarrow> dB list \<Rightarrow> bool"  (infixl "[\<rightarrow>\<^sub>l]" 50)
 where

   then have "rs [\<rightarrow>\<^sub>s] rs'"
     by induct (iprover intro: listrelp.intros)+
   then show ?case by (rule sred.Var)
 next
   case (Abs r r')
-  from `r \<rightarrow>\<^sub>s r'`
+  from \<open>r \<rightarrow>\<^sub>s r'\<close>
   have "Abs r \<degree>\<degree> [] \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> []" using listrelp.Nil
     by (rule sred.Abs)
   then show ?case by simp
 next
   case (Beta r s ss t)
-  from `r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>s t`
+  from \<open>r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>s t\<close>
   show ?case by (rule sred.Beta)
 qed
 
 inductive WN :: "dB => bool"
   where

 lemma lemma7:
   assumes r: "r \<rightarrow>\<^sub>s r'"
   shows "NF r' \<Longrightarrow> r \<rightarrow>\<^sub>l r'" using r
 proof induct
   case (Var rs rs' x)
-  from `NF (Var x \<degree>\<degree> rs')` have "listall NF rs'"
+  from \<open>NF (Var x \<degree>\<degree> rs')\<close> have "listall NF rs'"
     by cases simp_all
   with Var(1) have "rs [\<rightarrow>\<^sub>l] rs'"
   proof induct
     case Nil
     show ?case by (rule listrelp.Nil)

     thus ?case by (rule listrelp.Cons)
   qed
   thus ?case by (rule lred.Var)
 next
   case (Abs r r' ss ss')
-  from `NF (Abs r' \<degree>\<degree> ss')`
+  from \<open>NF (Abs r' \<degree>\<degree> ss')\<close>
   have ss': "ss' = []" by (rule Abs_NF)
   from Abs(3) have ss: "ss = []" using ss'
     by cases simp_all
   from ss' Abs have "NF (Abs r')" by simp
   hence "NF r'" by cases simp_all