src/HOL/Nominal/Examples/Class2.thy

 theory Class2
 imports Class1
 begin
 
-text {* Reduction *}
+text \<open>Reduction\<close>
 
 lemma fin_not_Cut:
   assumes a: "fin M x"
   shows "\<not>(\<exists>a M' x N'. M = Cut <a>.M' (x).N')"
 using a

 apply(blast)
 apply(drule_tac y="y" and c="c" and P="P" in a_redu_subst2)
 apply(auto)
 done
 
-text {* Candidates and SN *}
-
-text {* SNa *}
+text \<open>Candidates and SN\<close>
+
+text \<open>SNa\<close>
 
 inductive 
   SNa :: "trm \<Rightarrow> bool"
 where
   SNaI: "(\<And>M'. M \<longrightarrow>\<^sub>a M' \<Longrightarrow> SNa M') \<Longrightarrow> SNa M"

 apply(rotate_tac 1)
 apply(drule_tac x="(rev pi2)\<bullet>M'" in meta_spec)
 apply(perm_simp)
 done
 
-text {* set operators *}
+text \<open>set operators\<close>
 
 definition AXIOMSn :: "ty \<Rightarrow> ntrm set" where
   "AXIOMSn B \<equiv> { (x):(Ax y b) | x y b. True }"
 
 definition AXIOMSc::"ty \<Rightarrow> ctrm set" where

 termination
 apply(relation "measure (case_sum (size\<circ>fst) (size\<circ>fst))")
 apply(simp_all)
 done
 
-text {* Candidates *}
+text \<open>Candidates\<close>
 
 lemma test1:
   shows "x\<in>(X\<union>Y) = (x\<in>X \<or> x\<in>Y)"
 by blast
 

       by (simp only: NEGc_simps union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname 
                      IMPRIGHT_eqvt_coname IMPLEFT_eqvt_coname ih1 ih2 ih3 ih4 g)
   }
 qed
 
-text {* Elimination rules for the set-operators *}
+text \<open>Elimination rules for the set-operators\<close>
 
 lemma BINDINGc_elim:
   assumes a: "<a>:M \<in> BINDINGc B (\<parallel>(B)\<parallel>)"
   shows "\<forall>x P. ((x):P)\<in>(\<parallel>(B)\<parallel>) \<longrightarrow> SNa (M{a:=(x).P})"
 using a

 apply(simp add: CAND_eqvt_name CAND_eqvt_coname)
 apply(drule_tac pi="[(x,ca)]" and X="\<parallel><ty2>\<parallel>" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
 apply(perm_simp add: CAND_eqvt_name CAND_eqvt_coname csubst_eqvt nsubst_eqvt)
 done
 
-text {* Main lemma 1 *}
+text \<open>Main lemma 1\<close>
 
 lemma AXIOMS_imply_SNa:
   shows "<a>:M \<in> AXIOMSc B \<Longrightarrow> SNa M"
   and   "(x):M \<in> AXIOMSn B \<Longrightarrow> SNa M"
 apply -

     }
     ultimately show "SNa M" by blast
   }
 qed 
 
-text {* Main lemma 2 *}
+text \<open>Main lemma 2\<close>
 
 lemma AXIOMS_preserved:
   shows "<a>:M \<in> AXIOMSc B \<Longrightarrow> M \<longrightarrow>\<^sub>a* M' \<Longrightarrow> <a>:M' \<in> AXIOMSc B"
   and   "(x):M \<in> AXIOMSn B \<Longrightarrow> M \<longrightarrow>\<^sub>a* M' \<Longrightarrow> (x):M' \<in> AXIOMSn B"
   apply(simp_all add: AXIOMSc_def AXIOMSn_def)