src/HOL/Nominal/Examples/Standardization.thy

 (*  Title:      HOL/Nominal/Examples/Standardization.thy
     Author:     Stefan Berghofer and Tobias Nipkow
     Copyright   2005, 2008 TU Muenchen
 *)
 
-section {* Standardization *}
+section \<open>Standardization\<close>
 
 theory Standardization
 imports "../Nominal"
 begin
 
-text {*
+text \<open>
 The proof of the standardization theorem, as well as most of the theorems about
-lambda calculus in the following sections, are taken from @{text "HOL/Lambda"}.
-*}
-
-subsection {* Lambda terms *}
+lambda calculus in the following sections, are taken from \<open>HOL/Lambda\<close>.
+\<close>
+
+subsection \<open>Lambda terms\<close>
 
 atom_decl name
 
 nominal_datatype lam =
   Var "name"

 abbreviation
   beta_reds :: "lam \<Rightarrow> lam \<Rightarrow> bool"  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50) where
   "s \<rightarrow>\<^sub>\<beta>\<^sup>* t \<equiv> beta\<^sup>*\<^sup>* s t"
 
 
-subsection {* Application of a term to a list of terms *}
+subsection \<open>Application of a term to a list of terms\<close>
 
 abbreviation
   list_application :: "lam \<Rightarrow> lam list \<Rightarrow> lam"  (infixl "\<degree>\<degree>" 150) where
   "t \<degree>\<degree> ts \<equiv> foldl (op \<degree>) t ts"
 

 
 lemma fresh_apps [simp]: "(x::name) \<sharp> (t \<degree>\<degree> ts) = (x \<sharp> t \<and> x \<sharp> ts)"
   by (induct ts rule: rev_induct)
     (auto simp add: fresh_list_append fresh_list_nil fresh_list_cons)
 
-text {* A customized induction schema for @{text "\<degree>\<degree>"}. *}
+text \<open>A customized induction schema for \<open>\<degree>\<degree>\<close>.\<close>
 
 lemma lem:
   assumes "\<And>n ts (z::'a::fs_name). (\<And>z. \<forall>t \<in> set ts. P z t) \<Longrightarrow> P z (Var n \<degree>\<degree> ts)"
     and "\<And>x u ts z. x \<sharp> z \<Longrightarrow> (\<And>z. P z u) \<Longrightarrow> (\<And>z. \<forall>t \<in> set ts. P z t) \<Longrightarrow> P z ((Lam [x].u) \<degree>\<degree> ts)"
   shows "size t = n \<Longrightarrow> P z t"

     apply (rule refl)
     using assms apply blast+
   done
 
 
-subsection {* Congruence rules *}
+subsection \<open>Congruence rules\<close>
 
 lemma apps_preserves_beta [simp]:
     "r \<rightarrow>\<^sub>\<beta> s \<Longrightarrow> r \<degree>\<degree> ss \<rightarrow>\<^sub>\<beta> s \<degree>\<degree> ss"
   by (induct ss rule: rev_induct) auto
 

 lemma rtrancl_beta_App [intro]:
     "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<Longrightarrow> t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
   by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtranclp_trans)
 
 
-subsection {* Lifting an order to lists of elements *}
+subsection \<open>Lifting an order to lists of elements\<close>
 
 definition
   step1 :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
   "step1 r =
     (\<lambda>ys xs. \<exists>us z z' vs. xs = us @ z # vs \<and> r z' z \<and> ys =

   apply simp
   apply blast
   done
 
 
-subsection {* Lifting beta-reduction to lists *}
+subsection \<open>Lifting beta-reduction to lists\<close>
 
 abbreviation
   list_beta :: "lam list \<Rightarrow> lam list \<Rightarrow> bool"  (infixl "[\<rightarrow>\<^sub>\<beta>]\<^sub>1" 50) where
   "rs [\<rightarrow>\<^sub>\<beta>]\<^sub>1 ss \<equiv> step1 beta rs ss"
 

   apply (drule Snoc_step1_SnocD)
   apply blast
   done
 
 
-subsection {* Standard reduction relation *}
-
-text {*
+subsection \<open>Standard reduction relation\<close>
+
+text \<open>
 Based on lecture notes by Ralph Matthes,
 original proof idea due to Ralph Loader.
-*}
+\<close>
 
 declare listrel_mono [mono_set]
 
 lemma listrelp_eqvt [eqvt]:
   fixes f :: "'a::pt_name \<Rightarrow> 'b::pt_name \<Rightarrow> bool"

 next
   case (Abs x ss ss' r r')
   from Abs(4) 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 "(Lam [x].r) \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s (Lam [x].r') \<degree>\<degree> (ss' @ [s'])"
+  with \<open>r \<rightarrow>\<^sub>s r'\<close> have "(Lam [x].r) \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s (Lam [x].r') \<degree>\<degree> (ss' @ [s'])"
     by (rule better_sred_Abs)
   thus ?case by (simp only: app_last)
 next
   case (Beta x u ss t r)
   hence "r[x::=u] \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s t \<degree> s'" by (simp only: app_last)

     by (cases "y = x") (auto simp add: Var intro: refl_sred)
   ultimately show ?case by simp (rule lemma1')
 next
   case (Abs y ss ss' r r')
   then have "r[x::=s] \<rightarrow>\<^sub>s r'[x::=s']" by fast
-  moreover from Abs(8) `s \<rightarrow>\<^sub>s s'` have "map (\<lambda>t. t[x::=s]) ss [\<rightarrow>\<^sub>s] map (\<lambda>t. t[x::=s']) ss'"
+  moreover from Abs(8) \<open>s \<rightarrow>\<^sub>s s'\<close> have "map (\<lambda>t. t[x::=s]) ss [\<rightarrow>\<^sub>s] map (\<lambda>t. t[x::=s']) ss'"
     by induct (auto intro: listrelp.intros Abs)
-  ultimately show ?case using Abs(6) `y \<sharp> x` `y \<sharp> s` `y \<sharp> s'`
+  ultimately show ?case using Abs(6) \<open>y \<sharp> x\<close> \<open>y \<sharp> s\<close> \<open>y \<sharp> s'\<close>
     by simp (rule better_sred_Abs)
 next
   case (Beta y u ss t r)
   thus ?case by (auto simp add: subst_subst fresh_atm intro: better_sred_Beta)
 qed

   from Var(1) [simplified] 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 x ss ss' r r')
-  from `(Lam [x].r') \<degree>\<degree> ss' \<rightarrow>\<^sub>\<beta> r''` show ?case
+  from \<open>(Lam [x].r') \<degree>\<degree> ss' \<rightarrow>\<^sub>\<beta> r''\<close> show ?case
   proof (cases rule: apps_betasE [where x=x])
     case (appL s)
-    then obtain r''' where s: "s = (Lam [x].r''')" and r''': "r' \<rightarrow>\<^sub>\<beta> r'''" using `x \<sharp> r''`
+    then obtain r''' where s: "s = (Lam [x].r''')" and r''': "r' \<rightarrow>\<^sub>\<beta> r'''" using \<open>x \<sharp> r''\<close>
       by (cases rule: beta.strong_cases) (auto simp add: abs_fresh lam.inject alpha)
     from r''' have "r \<rightarrow>\<^sub>s r'''" by (blast intro: Abs)
     moreover from Abs have "ss [\<rightarrow>\<^sub>s] ss'" by (iprover dest: listrelp_conj1)
     ultimately have "(Lam [x].r) \<degree>\<degree> ss \<rightarrow>\<^sub>s (Lam [x].r''') \<degree>\<degree> ss'" by (rule better_sred_Abs)
     with appL s show "(Lam [x].r) \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by simp
   next
     case (appR rs')
-    from Abs(6) [simplified] `ss' [\<rightarrow>\<^sub>\<beta>]\<^sub>1 rs'`
+    from Abs(6) [simplified] \<open>ss' [\<rightarrow>\<^sub>\<beta>]\<^sub>1 rs'\<close>
     have "ss [\<rightarrow>\<^sub>s] rs'" by (rule lemma4_aux)
-    with `r \<rightarrow>\<^sub>s r'` have "(Lam [x].r) \<degree>\<degree> ss \<rightarrow>\<^sub>s (Lam [x].r') \<degree>\<degree> rs'" by (rule better_sred_Abs)
+    with \<open>r \<rightarrow>\<^sub>s r'\<close> have "(Lam [x].r) \<degree>\<degree> ss \<rightarrow>\<^sub>s (Lam [x].r') \<degree>\<degree> rs'" by (rule better_sred_Abs)
     with appR show "(Lam [x].r) \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by simp
   next
     case (beta t u' us')
     then have Lam_eq: "(Lam [x].r') = (Lam [x].t)" and ss': "ss' = u' # us'"
       and r'': "r'' = t[x::=u'] \<degree>\<degree> us'"
       by (simp_all add: abs_fresh)
     from Abs(6) ss' obtain u us where
       ss: "ss = u # us" and u: "u \<rightarrow>\<^sub>s u'" and us: "us [\<rightarrow>\<^sub>s] us'"
       by cases (auto dest!: listrelp_conj1)
-    have "r[x::=u] \<rightarrow>\<^sub>s r'[x::=u']" using `r \<rightarrow>\<^sub>s r'` and u by (rule lemma3)
+    have "r[x::=u] \<rightarrow>\<^sub>s r'[x::=u']" using \<open>r \<rightarrow>\<^sub>s r'\<close> and u by (rule lemma3)
     with us have "r[x::=u] \<degree>\<degree> us \<rightarrow>\<^sub>s r'[x::=u'] \<degree>\<degree> us'" by (rule lemma1')
     hence "(Lam [x].r) \<degree> u \<degree>\<degree> us \<rightarrow>\<^sub>s r'[x::=u'] \<degree>\<degree> us'" by (rule better_sred_Beta)
     with ss r'' Lam_eq show "(Lam [x].r) \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by (simp add: lam.inject alpha)
   qed
 next

   assumes r: "r \<rightarrow>\<^sub>\<beta>\<^sup>* r'"
   shows "r \<rightarrow>\<^sub>s r'" using r
   by induct (iprover intro: refl_sred lemma4)+
 
 
-subsection {* Terms in normal form *}
+subsection \<open>Terms in normal form\<close>
 
 lemma listsp_eqvt [eqvt]:
   assumes xs: "listsp p (xs::'a::pt_name list)"
   shows "listsp ((pi::name prm) \<bullet> p) (pi \<bullet> xs)" using xs
   apply induct

 next
   case (Abs u)
   thus ?thesis by simp
 qed
 
-text {*
+text \<open>
 @{term NF} characterizes exactly the terms that are in normal form.
-*}
+\<close>
   
 lemma NF_eq: "NF t = (\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t')"
 proof
   assume H: "NF t"
   show "\<forall>t'. \<not> t \<rightarrow>\<^sub>\<beta> t'"

     qed
   qed
 qed
 
 
-subsection {* Leftmost reduction and weakly normalizing terms *}
+subsection \<open>Leftmost reduction and weakly normalizing terms\<close>
 
 inductive
   lred :: "lam \<Rightarrow> lam \<Rightarrow> bool"  (infixl "\<rightarrow>\<^sub>l" 50)
   and lredlist :: "lam list \<Rightarrow> lam 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' x)
-  from `r \<rightarrow>\<^sub>s r'`
+  from \<open>r \<rightarrow>\<^sub>s r'\<close>
   have "(Lam [x].r) \<degree>\<degree> [] \<rightarrow>\<^sub>s (Lam [x].r') \<degree>\<degree> []" using listrelp.Nil
     by (rule better_sred_Abs)
   then show ?case by simp
 next
   case (Beta r x s ss t)
-  from `r[x::=s] \<degree>\<degree> ss \<rightarrow>\<^sub>s t`
+  from \<open>r[x::=s] \<degree>\<degree> ss \<rightarrow>\<^sub>s t\<close>
   show ?case by (rule better_sred_Beta)
 qed
 
 inductive WN :: "lam \<Rightarrow> 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 "listsp NF rs'"
+  from \<open>NF (Var x \<degree>\<degree> rs')\<close> have "listsp 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 x ss ss' r r')
-  from `NF ((Lam [x].r') \<degree>\<degree> ss')`
+  from \<open>NF ((Lam [x].r') \<degree>\<degree> ss')\<close>
   have ss': "ss' = []" by (rule Abs_NF)
   from Abs(4) have ss: "ss = []" using ss'
     by cases simp_all
   from ss' Abs have "NF (Lam [x].r')" by simp
   hence "NF r'" by (cases rule: NF.strong_cases) (auto simp add: abs_fresh lam.inject alpha)