src/HOL/IMP/Abs_Int3.thy

 theory Abs_Int3
 imports Abs_Int2_ivl
 begin
 
 class widen =
-fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
+fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix \<open>\<nabla>\<close> 65)
 
 class narrow =
-fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
+fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix \<open>\<triangle>\<close> 65)
 
 class wn = widen + narrow + order +
 assumes widen1: "x \<le> x \<nabla> y"
 assumes widen2: "y \<le> x \<nabla> y"
 assumes narrow1: "y \<le> x \<Longrightarrow> y \<le> x \<triangle> y"

 apply(rule_tac x=p in bexI)
  apply (auto simp: vars_acom_def m_o_widen top_on_acom_def)
 done
 
 
-definition n_s :: "'av st \<Rightarrow> vname set \<Rightarrow> nat" ("n\<^sub>s") where
+definition n_s :: "'av st \<Rightarrow> vname set \<Rightarrow> nat" (\<open>n\<^sub>s\<close>) where
 "n\<^sub>s S X = (\<Sum>x\<in>X. n(fun S x))"
 
 lemma n_s_narrow_rep:
 assumes "finite X"  "S1 = S2 on -X"  "\<forall>x. S2 x \<le> S1 x"  "\<forall>x. S1 x \<triangle> S2 x \<le> S1 x"
   "S1 x \<noteq> S1 x \<triangle> S2 x"

 apply(auto simp add: less_st_def n_s_def)
 apply (transfer fixing: n)
 apply(auto simp add: less_eq_st_rep_iff eq_st_def fun_eq_iff n_s_narrow_rep)
 done
 
-definition n_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" ("n\<^sub>o") where
+definition n_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" (\<open>n\<^sub>o\<close>) where
 "n\<^sub>o opt X = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^sub>s S X + 1)"
 
 lemma n_o_narrow:
   "top_on_opt S1 (-X) \<Longrightarrow> top_on_opt S2 (-X) \<Longrightarrow> finite X
   \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1 \<Longrightarrow> n\<^sub>o (S1 \<triangle> S2) X < n\<^sub>o S1 X"
 apply(induction S1 S2 rule: narrow_option.induct)
 apply(auto simp: n_o_def n_s_narrow)
 done
 
 
-definition n_c :: "'av st option acom \<Rightarrow> nat" ("n\<^sub>c") where
+definition n_c :: "'av st option acom \<Rightarrow> nat" (\<open>n\<^sub>c\<close>) where
 "n\<^sub>c C = sum_list (map (\<lambda>a. n\<^sub>o a (vars C)) (annos C))"
 
 lemma less_annos_iff: "(C1 < C2) = (C1 \<le> C2 \<and>
   (\<exists>i<length (annos C1). annos C1 ! i < annos C2 ! i))"
 by(metis (opaque_lifting, no_types) less_le_not_le le_iff_le_annos size_annos_same2)