src/HOL/Nominal/Examples/Class1.thy

 theory Class1
 imports "../Nominal" 
 begin
 
-section {* Term-Calculus from Urban's PhD *}
+section \<open>Term-Calculus from Urban's PhD\<close>
 
 atom_decl name coname
 
-text {* types *}
+text \<open>types\<close>
 
 nominal_datatype ty =
     PR "string"
   | NOT  "ty"
   | AND  "ty" "ty"   ("_ AND _" [100,100] 100)

   and   T::"ty"
   shows "a\<sharp>T" and "x\<sharp>T"
 by (nominal_induct T rule: ty.strong_induct)
    (auto simp add: fresh_string)
 
-text {* terms *}
+text \<open>terms\<close>
 
 nominal_datatype trm = 
     Ax   "name" "coname"
   | Cut  "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm"            ("Cut <_>._ (_)._" [100,100,100,100] 100)
   | NotR "\<guillemotleft>name\<guillemotright>trm" "coname"                 ("NotR (_)._ _" [100,100,100] 100)

   | OrR2 "\<guillemotleft>coname\<guillemotright>trm" "coname"               ("OrR2 <_>._ _" [100,100,100] 100)
   | OrL "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"        ("OrL (_)._ (_)._ _" [100,100,100,100,100] 100)
   | ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname"       ("ImpR (_).<_>._ _" [100,100,100,100] 100)
   | ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"     ("ImpL <_>._ (_)._ _" [100,100,100,100,100] 100)
 
-text {* named terms *}
+text \<open>named terms\<close>
 
 nominal_datatype ntrm = Na "\<guillemotleft>name\<guillemotright>trm" ("((_):_)" [100,100] 100)
 
-text {* conamed terms *}
+text \<open>conamed terms\<close>
 
 nominal_datatype ctrm = Co "\<guillemotleft>coname\<guillemotright>trm" ("(<_>:_)" [100,100] 100)
 
-text {* renaming functions *}
+text \<open>renaming functions\<close>
 
 nominal_primrec (freshness_context: "(d::coname,e::coname)") 
   crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,100,100] 100) 
 where
   "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" 

 using a
 apply(nominal_induct M avoiding: x y z a rule: trm.strong_induct)
 apply(simp_all add: trm.inject split: if_splits)
 done
 
-text {* substitution functions *}
+text \<open>substitution functions\<close>
 
 lemma fresh_perm_coname:
   fixes c::"coname"
   and   pi::"coname prm"
   and   M::"trm"

 lemmas subst_comm = substn_crename_comm substc_crename_comm
                     substn_nrename_comm substc_nrename_comm
 lemmas subst_comm' = substn_crename_comm' substc_crename_comm'
                      substn_nrename_comm' substc_nrename_comm'
 
-text {* typing contexts *}
+text \<open>typing contexts\<close>
 
 type_synonym ctxtn = "(name\<times>ty) list"
 type_synonym ctxtc = "(coname\<times>ty) list"
 
 inductive

   show "a\<sharp>\<Gamma>" by (induct \<Gamma>) (auto simp add: fresh_list_nil fresh_list_cons fresh_prod fresh_atm fresh_ty)
 next
   show "x\<sharp>\<Delta>" by (induct \<Delta>) (auto simp add: fresh_list_nil fresh_list_cons fresh_prod fresh_atm fresh_ty)
 qed
 
-text {* cut-reductions *}
+text \<open>cut-reductions\<close>
 
 declare abs_perm[eqvt]
 
 inductive
   fin :: "trm \<Rightarrow> name \<Rightarrow> bool"

   also have "\<dots> = ImpR (x).<a>.M' b" 
     using fs2 red by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
   finally show ?thesis by simp
 qed
 
-text {* axioms do not reduce *}
+text \<open>axioms do not reduce\<close>
 
 lemma ax_do_not_l_reduce:
   shows "Ax x a \<longrightarrow>\<^sub>l M \<Longrightarrow> False"
 by (erule_tac l_redu.cases) (simp_all add: trm.inject)
  

 apply(rule trans)
 apply(rule perm_compose)
 apply(simp add: calc_atm perm_swap)
 done
 
-text {* Transitive Closure*}
+text \<open>Transitive Closure\<close>
 
 abbreviation
  a_star_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longrightarrow>\<^sub>a* _" [100,100] 100)
 where
   "M \<longrightarrow>\<^sub>a* M' \<equiv> (a_redu)^** M M'"

   and     a2: "M2\<longrightarrow>\<^sub>a* M3"
   shows "M1 \<longrightarrow>\<^sub>a* M3"
 using a2 a1
 by (induct) (auto)
 
-text {* congruence rules for \<open>\<longrightarrow>\<^sub>a*\<close> *}
+text \<open>congruence rules for \<open>\<longrightarrow>\<^sub>a*\<close>\<close>
 
 lemma ax_do_not_a_star_reduce:
   shows "Ax x a \<longrightarrow>\<^sub>a* M \<Longrightarrow> M = Ax x a"
 apply(induct set: rtranclp)
 apply(auto)

 apply(auto)
 apply(drule a_redu_ImpL_elim)
 apply(auto simp add: alpha trm.inject)
 done
 
-text {* Substitution *}
+text \<open>Substitution\<close>
 
 lemma subst_not_fin1:
   shows "\<not>fin(M{x:=<c>.P}) x"
 apply(nominal_induct M avoiding: x c P rule: trm.strong_induct)
 apply(auto)

 apply(drule fic_elims, simp)
 apply(rule exists_fresh'(1)[OF fs_name1])
 apply(drule fic_elims, simp)
 done
 
-text {* Reductions *}
+text \<open>Reductions\<close>
 
 lemma fin_l_reduce:
   assumes  a: "fin M x"
   and      b: "M \<longrightarrow>\<^sub>l M'"
   shows "fin M' x"

 using b a
 apply(induct set: rtranclp)
 apply(auto simp add: fic_a_reduce)
 done
 
-text {* substitution properties *}
+text \<open>substitution properties\<close>
 
 lemma subst_with_ax1:
   shows "M{x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* M[x\<turnstile>n>y]"
 proof(nominal_induct M avoiding: x a y rule: trm.strong_induct)
   case (Ax z b x a y)

     using ih1 ih2 by (auto intro: a_star_congs)
   finally show "(ImpL <c>.M (u).N v){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (ImpL <c>.M (u).N v)[b\<turnstile>c>a]" 
     using fs by simp
 qed
 
-text {* substitution lemmas *}
+text \<open>substitution lemmas\<close>
 
 lemma not_Ax1:
   shows "\<not>(b\<sharp>M) \<Longrightarrow> M{b:=(y).Q} \<noteq> Ax x a"
 apply(nominal_induct M avoiding: b y Q x a rule: trm.strong_induct)
 apply(auto simp add: fresh_atm abs_fresh abs_supp fin_supp)