src/HOL/Library/FinFun.thy
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 60565 b7ee41f72add
     1.1 --- a/src/HOL/Library/FinFun.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/FinFun.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -1,12 +1,12 @@
     1.4  (* Author: Andreas Lochbihler, Uni Karlsruhe *)
     1.5  
     1.6 -section {* Almost everywhere constant functions *}
     1.7 +section \<open>Almost everywhere constant functions\<close>
     1.8  
     1.9  theory FinFun
    1.10  imports Cardinality
    1.11  begin
    1.12  
    1.13 -text {*
    1.14 +text \<open>
    1.15    This theory defines functions which are constant except for finitely
    1.16    many points (FinFun) and introduces a type finfin along with a
    1.17    number of operators for them. The code generator is set up such that
    1.18 @@ -14,10 +14,10 @@
    1.19    all operators are executable.
    1.20  
    1.21    For details, see Formalising FinFuns - Generating Code for Functions as Data by A. Lochbihler in TPHOLs 2009.
    1.22 -*}
    1.23 +\<close>
    1.24  
    1.25  
    1.26 -subsection {* The @{text "map_default"} operation *}
    1.27 +subsection \<open>The @{text "map_default"} operation\<close>
    1.28  
    1.29  definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.30  where "map_default b f a \<equiv> case f a of None \<Rightarrow> b | Some b' \<Rightarrow> b'"
    1.31 @@ -72,7 +72,7 @@
    1.32    qed
    1.33  qed
    1.34  
    1.35 -subsection {* The finfun type *}
    1.36 +subsection \<open>The finfun type\<close>
    1.37  
    1.38  definition "finfun = {f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
    1.39  
    1.40 @@ -122,8 +122,8 @@
    1.41      thus ?case by(simp)
    1.42    next
    1.43      case (insert x F)
    1.44 -    note IH = `\<And>y. F = {a. y a \<noteq> b} \<Longrightarrow> finite {c. g (y c) \<noteq> g b}`
    1.45 -    from `insert x F = {a. y a \<noteq> b}` `x \<notin> F`
    1.46 +    note IH = \<open>\<And>y. F = {a. y a \<noteq> b} \<Longrightarrow> finite {c. g (y c) \<noteq> g b}\<close>
    1.47 +    from \<open>insert x F = {a. y a \<noteq> b}\<close> \<open>x \<notin> F\<close>
    1.48      have F: "F = {a. (y(x := b)) a \<noteq> b}" by(auto)
    1.49      show ?case
    1.50      proof(cases "g (y x) = g b")
    1.51 @@ -269,7 +269,7 @@
    1.52  qed
    1.53  
    1.54  
    1.55 -subsection {* Kernel functions for type @{typ "'a \<Rightarrow>f 'b"} *}
    1.56 +subsection \<open>Kernel functions for type @{typ "'a \<Rightarrow>f 'b"}\<close>
    1.57  
    1.58  lift_definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>f 'b" ("K$/ _" [0] 1)
    1.59  is "\<lambda> b x. b" by (rule const_finfun)
    1.60 @@ -287,7 +287,7 @@
    1.61  lemma finfun_update_const_same: "(K$ b)(a $:= b) = (K$ b)"
    1.62  by transfer (simp add: fun_eq_iff)
    1.63  
    1.64 -subsection {* Code generator setup *}
    1.65 +subsection \<open>Code generator setup\<close>
    1.66  
    1.67  definition finfun_update_code :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>f 'b"
    1.68  where [simp, code del]: "finfun_update_code = finfun_update"
    1.69 @@ -303,11 +303,11 @@
    1.70  by(simp add: finfun_update_twist)
    1.71  
    1.72  
    1.73 -subsection {* Setup for quickcheck *}
    1.74 +subsection \<open>Setup for quickcheck\<close>
    1.75  
    1.76  quickcheck_generator finfun constructors: finfun_update_code, "finfun_const :: 'b \<Rightarrow> 'a \<Rightarrow>f 'b"
    1.77  
    1.78 -subsection {* @{text "finfun_update"} as instance of @{text "comp_fun_commute"} *}
    1.79 +subsection \<open>@{text "finfun_update"} as instance of @{text "comp_fun_commute"}\<close>
    1.80  
    1.81  interpretation finfun_update: comp_fun_commute "\<lambda>a f. f(a :: 'a $:= b')"
    1.82    including finfun
    1.83 @@ -343,7 +343,7 @@
    1.84  qed
    1.85  
    1.86  
    1.87 -subsection {* Default value for FinFuns *}
    1.88 +subsection \<open>Default value for FinFuns\<close>
    1.89  
    1.90  definition finfun_default_aux :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"
    1.91  where [code del]: "finfun_default_aux f = (if finite (UNIV :: 'a set) then undefined else THE b. finite {a. f a \<noteq> b})"
    1.92 @@ -431,7 +431,7 @@
    1.93    "finfun_default (finfun_update_code f a b) = finfun_default f"
    1.94  by(simp add: finfun_default_update_const)
    1.95  
    1.96 -subsection {* Recursion combinator and well-formedness conditions *}
    1.97 +subsection \<open>Recursion combinator and well-formedness conditions\<close>
    1.98  
    1.99  definition finfun_rec :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow>f 'b) \<Rightarrow> 'c"
   1.100  where [code del]:
   1.101 @@ -469,13 +469,13 @@
   1.102    from fin anf fg show ?thesis
   1.103    proof(induct "dom f" arbitrary: f)
   1.104      case empty
   1.105 -    from `{} = dom f` have "f = empty" by(auto simp add: dom_def)
   1.106 +    from \<open>{} = dom f\<close> have "f = empty" by(auto simp add: dom_def)
   1.107      thus ?case by(simp add: finfun_const_def upd_const_same)
   1.108    next
   1.109      case (insert a' A)
   1.110 -    note IH = `\<And>f.  \<lbrakk> A = dom f; a \<notin> dom f; f \<subseteq>\<^sub>m g \<rbrakk> \<Longrightarrow> upd a d (?fr (dom f)) = ?fr (dom f)`
   1.111 -    note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
   1.112 -    note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
   1.113 +    note IH = \<open>\<And>f.  \<lbrakk> A = dom f; a \<notin> dom f; f \<subseteq>\<^sub>m g \<rbrakk> \<Longrightarrow> upd a d (?fr (dom f)) = ?fr (dom f)\<close>
   1.114 +    note fin = \<open>finite A\<close> note anf = \<open>a \<notin> dom f\<close> note a'nA = \<open>a' \<notin> A\<close>
   1.115 +    note domf = \<open>insert a' A = dom f\<close> note fg = \<open>f \<subseteq>\<^sub>m g\<close>
   1.116      
   1.117      from domf obtain b where b: "f a' = Some b" by auto
   1.118      let ?f' = "f(a' := None)"
   1.119 @@ -485,7 +485,7 @@
   1.120      hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
   1.121      also from anf domf have "a \<noteq> a'" by auto note upd_commute[OF this]
   1.122      also from domf a'nA anf fg have "a \<notin> dom ?f'" "?f' \<subseteq>\<^sub>m g" and A: "A = dom ?f'" by(auto simp add: ran_def map_le_def)
   1.123 -    note A also note IH[OF A `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g`]
   1.124 +    note A also note IH[OF A \<open>a \<notin> dom ?f'\<close> \<open>?f' \<subseteq>\<^sub>m g\<close>]
   1.125      also have "upd a' (map_default d f a') (?fr (dom (f(a' := None)))) = ?fr (dom f)"
   1.126        unfolding domf[symmetric] gwf.fold_insert[OF fin a'nA] ga' unfolding A ..
   1.127      also have "insert a' (dom ?f') = dom f" using domf by auto
   1.128 @@ -507,13 +507,13 @@
   1.129    from fin anf fg show ?thesis
   1.130    proof(induct "dom f" arbitrary: f)
   1.131      case empty
   1.132 -    from `{} = dom f` have "f = empty" by(auto simp add: dom_def)
   1.133 +    from \<open>{} = dom f\<close> have "f = empty" by(auto simp add: dom_def)
   1.134      thus ?case by(auto simp add: finfun_const_def finfun_update_def upd_upd_twice)
   1.135    next
   1.136      case (insert a' A)
   1.137 -    note IH = `\<And>f. \<lbrakk>A = dom f; a \<notin> dom f; f \<subseteq>\<^sub>m g\<rbrakk> \<Longrightarrow> upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (?fr (dom f))`
   1.138 -    note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
   1.139 -    note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
   1.140 +    note IH = \<open>\<And>f. \<lbrakk>A = dom f; a \<notin> dom f; f \<subseteq>\<^sub>m g\<rbrakk> \<Longrightarrow> upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (?fr (dom f))\<close>
   1.141 +    note fin = \<open>finite A\<close> note anf = \<open>a \<notin> dom f\<close> note a'nA = \<open>a' \<notin> A\<close>
   1.142 +    note domf = \<open>insert a' A = dom f\<close> note fg = \<open>f \<subseteq>\<^sub>m g\<close>
   1.143      
   1.144      from domf obtain b where b: "f a' = Some b" by auto
   1.145      let ?f' = "f(a' := None)"
   1.146 @@ -525,7 +525,7 @@
   1.147      also from anf domf have ana': "a \<noteq> a'" by auto note upd_commute[OF this]
   1.148      also note upd_commute[OF ana']
   1.149      also from domf a'nA anf fg have "a \<notin> dom ?f'" "?f' \<subseteq>\<^sub>m g" and A: "A = dom ?f'" by(auto simp add: ran_def map_le_def)
   1.150 -    note A also note IH[OF A `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g`]
   1.151 +    note A also note IH[OF A \<open>a \<notin> dom ?f'\<close> \<open>?f' \<subseteq>\<^sub>m g\<close>]
   1.152      also note upd_commute[OF ana'[symmetric]] also note ga'[symmetric] also note A[symmetric]
   1.153      also note gwf.fold_insert[symmetric, OF fin a'nA] also note domf
   1.154      finally show ?case .
   1.155 @@ -551,8 +551,8 @@
   1.156        case empty thus ?case by simp
   1.157      next
   1.158        case (insert a B)
   1.159 -      note finB = `finite B` note anB = `a \<notin> B` note sub = `insert a B \<subseteq> A`
   1.160 -      note IH = `B \<subseteq> A \<Longrightarrow> Finite_Set.fold f z B = Finite_Set.fold g z B`
   1.161 +      note finB = \<open>finite B\<close> note anB = \<open>a \<notin> B\<close> note sub = \<open>insert a B \<subseteq> A\<close>
   1.162 +      note IH = \<open>B \<subseteq> A \<Longrightarrow> Finite_Set.fold f z B = Finite_Set.fold g z B\<close>
   1.163        from sub anB have BpsubA: "B \<subset> A" and BsubA: "B \<subseteq> A" and aA: "a \<in> A" by auto
   1.164        from IH[OF BsubA] eq[OF aA] finB anB
   1.165        show ?case by(auto)
   1.166 @@ -770,7 +770,7 @@
   1.167        with True show "g' = empty"
   1.168          by -(rule map_default_inject(2)[OF _ fin g], auto)
   1.169      qed
   1.170 -    show ?thesis unfolding finfun_rec_def using `finite UNIV` True
   1.171 +    show ?thesis unfolding finfun_rec_def using \<open>finite UNIV\<close> True
   1.172        unfolding Let_def the default by(simp)
   1.173    next
   1.174      case False
   1.175 @@ -797,7 +797,7 @@
   1.176  
   1.177  end
   1.178  
   1.179 -subsection {* Weak induction rule and case analysis for FinFuns *}
   1.180 +subsection \<open>Weak induction rule and case analysis for FinFuns\<close>
   1.181  
   1.182  lemma finfun_weak_induct [consumes 0, case_names const update]:
   1.183    assumes const: "\<And>b. P (K$ b)"
   1.184 @@ -807,7 +807,7 @@
   1.185  proof(induct x rule: Abs_finfun_induct)
   1.186    case (Abs_finfun y)
   1.187    then obtain b where "finite {a. y a \<noteq> b}" unfolding finfun_def by blast
   1.188 -  thus ?case using `y \<in> finfun`
   1.189 +  thus ?case using \<open>y \<in> finfun\<close>
   1.190    proof(induct "{a. y a \<noteq> b}" arbitrary: y rule: finite_induct)
   1.191      case empty
   1.192      hence "\<And>a. y a = b" by blast
   1.193 @@ -816,9 +816,9 @@
   1.194      thus ?case by(simp add: const)
   1.195    next
   1.196      case (insert a A)
   1.197 -    note IH = `\<And>y. \<lbrakk> A = {a. y a \<noteq> b}; y \<in> finfun  \<rbrakk> \<Longrightarrow> P (Abs_finfun y)`
   1.198 -    note y = `y \<in> finfun`
   1.199 -    with `insert a A = {a. y a \<noteq> b}` `a \<notin> A`
   1.200 +    note IH = \<open>\<And>y. \<lbrakk> A = {a. y a \<noteq> b}; y \<in> finfun  \<rbrakk> \<Longrightarrow> P (Abs_finfun y)\<close>
   1.201 +    note y = \<open>y \<in> finfun\<close>
   1.202 +    with \<open>insert a A = {a. y a \<noteq> b}\<close> \<open>a \<notin> A\<close>
   1.203      have "A = {a'. (y(a := b)) a' \<noteq> b}" "y(a := b) \<in> finfun" by auto
   1.204      from IH[OF this] have "P (finfun_update (Abs_finfun (y(a := b))) a (y a))" by(rule update)
   1.205      thus ?case using y unfolding finfun_update_def by simp
   1.206 @@ -847,7 +847,7 @@
   1.207  qed
   1.208  
   1.209  
   1.210 -subsection {* Function application *}
   1.211 +subsection \<open>Function application\<close>
   1.212  
   1.213  notation finfun_apply (infixl "$" 999)
   1.214  
   1.215 @@ -905,7 +905,7 @@
   1.216    "((K$ b) = f(a $:= b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f $ a' = b))"
   1.217  by(auto simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
   1.218  
   1.219 -subsection {* Function composition *}
   1.220 +subsection \<open>Function composition\<close>
   1.221  
   1.222  definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>f 'a \<Rightarrow> 'c \<Rightarrow>f 'b" (infixr "o$" 55)
   1.223  where [code del]: "g o$ f  = finfun_rec (\<lambda>b. (K$ g b)) (\<lambda>a b c. c(a $:= g b)) f"
   1.224 @@ -991,7 +991,7 @@
   1.225    with False show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def)
   1.226  qed
   1.227  
   1.228 -subsection {* Universal quantification *}
   1.229 +subsection \<open>Universal quantification\<close>
   1.230  
   1.231  definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>f bool \<Rightarrow> bool"
   1.232  where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P $ a"
   1.233 @@ -1035,7 +1035,7 @@
   1.234  by(simp add: finfun_Ex_def)
   1.235  
   1.236  
   1.237 -subsection {* A diagonal operator for FinFuns *}
   1.238 +subsection \<open>A diagonal operator for FinFuns\<close>
   1.239  
   1.240  definition finfun_Diag :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow>f 'c \<Rightarrow> 'a \<Rightarrow>f ('b \<times> 'c)" ("(1'($_,/ _$'))" [0, 0] 1000)
   1.241  where [code del]: "($f, g$) = finfun_rec (\<lambda>b. Pair b \<circ>$ g) (\<lambda>a b c. c(a $:= (b, g $ a))) f"
   1.242 @@ -1061,9 +1061,9 @@
   1.243  lemma finfun_Diag_const1: "($K$ b, g$) = Pair b \<circ>$ g"
   1.244  by(simp add: finfun_Diag_def)
   1.245  
   1.246 -text {*
   1.247 +text \<open>
   1.248    Do not use @{thm finfun_Diag_const1} for the code generator because @{term "Pair b"} is injective, i.e. if @{term g} is free of redundant updates, there is no need to check for redundant updates as is done for @{term "op \<circ>$"}.
   1.249 -*}
   1.250 +\<close>
   1.251  
   1.252  lemma finfun_Diag_const_code [code]:
   1.253    "($K$ b, K$ c$) = (K$ (b, c))"
   1.254 @@ -1161,7 +1161,7 @@
   1.255  lemma finfun_Diag_collapse [simp]: "($finfun_fst f, finfun_snd f$) = f"
   1.256  by(induct f rule: finfun_weak_induct)(simp_all add: finfun_fst_const finfun_snd_const finfun_fst_update finfun_snd_update finfun_Diag_update_update)
   1.257  
   1.258 -subsection {* Currying for FinFuns *}
   1.259 +subsection \<open>Currying for FinFuns\<close>
   1.260  
   1.261  definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>f 'c \<Rightarrow> 'a \<Rightarrow>f 'b \<Rightarrow>f 'c"
   1.262  where [code del]: "finfun_curry = finfun_rec (finfun_const \<circ> finfun_const) (\<lambda>(a, b) c f. f(a $:= (f $ a)(b $:= c)))"
   1.263 @@ -1234,7 +1234,7 @@
   1.264    thus ?thesis by(auto simp add: fun_eq_iff)
   1.265  qed
   1.266  
   1.267 -subsection {* Executable equality for FinFuns *}
   1.268 +subsection \<open>Executable equality for FinFuns\<close>
   1.269  
   1.270  lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>$ ($f, g$))"
   1.271  by(simp add: expand_finfun_eq fun_eq_iff finfun_All_All o_def)
   1.272 @@ -1248,7 +1248,7 @@
   1.273    "HOL.equal (f :: _ \<Rightarrow>f _) f \<longleftrightarrow> True"
   1.274    by (fact equal_refl)
   1.275  
   1.276 -subsection {* An operator that explicitly removes all redundant updates in the generated representations *}
   1.277 +subsection \<open>An operator that explicitly removes all redundant updates in the generated representations\<close>
   1.278  
   1.279  definition finfun_clearjunk :: "'a \<Rightarrow>f 'b \<Rightarrow> 'a \<Rightarrow>f 'b"
   1.280  where [simp, code del]: "finfun_clearjunk = id"
   1.281 @@ -1260,7 +1260,7 @@
   1.282    "finfun_clearjunk (finfun_update_code f a b) = f(a $:= b)"
   1.283  by simp
   1.284  
   1.285 -subsection {* The domain of a FinFun as a FinFun *}
   1.286 +subsection \<open>The domain of a FinFun as a FinFun\<close>
   1.287  
   1.288  definition finfun_dom :: "('a \<Rightarrow>f 'b) \<Rightarrow> ('a \<Rightarrow>f bool)"
   1.289  where [code del]: "finfun_dom f = Abs_finfun (\<lambda>a. f $ a \<noteq> finfun_default f)"
   1.290 @@ -1270,10 +1270,10 @@
   1.291  unfolding finfun_dom_def finfun_default_const
   1.292  by(auto)(simp_all add: finfun_const_def)
   1.293  
   1.294 -text {*
   1.295 +text \<open>
   1.296    @{term "finfun_dom" } raises an exception when called on a FinFun whose domain is a finite type. 
   1.297    For such FinFuns, the default value (and as such the domain) is undefined.
   1.298 -*}
   1.299 +\<close>
   1.300  
   1.301  lemma finfun_dom_const_code [code]:
   1.302    "finfun_dom ((K$ c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = 
   1.303 @@ -1311,7 +1311,7 @@
   1.304  qed
   1.305  
   1.306  
   1.307 -subsection {* The domain of a FinFun as a sorted list *}
   1.308 +subsection \<open>The domain of a FinFun as a sorted list\<close>
   1.309  
   1.310  definition finfun_to_list :: "('a :: linorder) \<Rightarrow>f 'b \<Rightarrow> 'a list"
   1.311  where
   1.312 @@ -1422,7 +1422,7 @@
   1.313          assume "set xs' = {x. finfun_dom f $ x} \<and> sorted xs' \<and> distinct xs'"
   1.314          thus "xs' = remove1 a xs" using 1 by(blast intro: sorted_distinct_set_unique)
   1.315        qed
   1.316 -      thus ?thesis using False eq `b \<noteq> finfun_default f` 
   1.317 +      thus ?thesis using False eq \<open>b \<noteq> finfun_default f\<close> 
   1.318          by (simp add: insort_insert_insort insort_remove1)
   1.319      qed
   1.320    qed
   1.321 @@ -1433,7 +1433,7 @@
   1.322    (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
   1.323  by(simp add: finfun_to_list_update)
   1.324  
   1.325 -text {* More type class instantiations *}
   1.326 +text \<open>More type class instantiations\<close>
   1.327  
   1.328  lemma card_eq_1_iff: "card A = 1 \<longleftrightarrow> A \<noteq> {} \<and> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)"
   1.329    (is "?lhs \<longleftrightarrow> ?rhs")
   1.330 @@ -1442,11 +1442,11 @@
   1.331    moreover {
   1.332      fix x y
   1.333      assume A: "x \<in> A" "y \<in> A" and neq: "x \<noteq> y"
   1.334 -    have "finite A" using `?lhs` by(simp add: card_ge_0_finite)
   1.335 +    have "finite A" using \<open>?lhs\<close> by(simp add: card_ge_0_finite)
   1.336      from neq have "2 = card {x, y}" by simp
   1.337 -    also have "\<dots> \<le> card A" using A `finite A`
   1.338 +    also have "\<dots> \<le> card A" using A \<open>finite A\<close>
   1.339        by(auto intro: card_mono)
   1.340 -    finally have False using `?lhs` by simp }
   1.341 +    finally have False using \<open>?lhs\<close> by simp }
   1.342    ultimately show ?rhs by auto
   1.343  next
   1.344    assume ?rhs
   1.345 @@ -1486,9 +1486,9 @@
   1.346        unfolding type_definition.Abs_image[OF type_definition_finfun, symmetric] F_def
   1.347        by(rule finite_imageD)(auto intro: inj_onI simp add: Abs_finfun_inject)
   1.348      hence "finite (range ?f)" 
   1.349 -      by(rule finite_subset[rotated 1])(auto simp add: F_def finfun_def `b1 \<noteq> b2` intro!: exI[where x=b2])
   1.350 +      by(rule finite_subset[rotated 1])(auto simp add: F_def finfun_def \<open>b1 \<noteq> b2\<close> intro!: exI[where x=b2])
   1.351      thus "finite (UNIV :: 'a set)"
   1.352 -      by(rule finite_imageD)(auto intro: inj_onI simp add: fun_eq_iff `b1 \<noteq> b2` split: split_if_asm)
   1.353 +      by(rule finite_imageD)(auto intro: inj_onI simp add: fun_eq_iff \<open>b1 \<noteq> b2\<close> split: split_if_asm)
   1.354      
   1.355      from finite have "finite (range (\<lambda>b. ((K$ b) :: 'a \<Rightarrow>f 'b)))"
   1.356        by(rule finite_subset[rotated 1]) simp
   1.357 @@ -1526,7 +1526,7 @@
   1.358  instance by intro_classes (simp add: card_UNIV_finfun_def card_UNIV Let_def card_UNIV_finfun)
   1.359  end
   1.360  
   1.361 -text {* Deactivate syntax again. Import theory @{text FinFun_Syntax} to reactivate it again *}
   1.362 +text \<open>Deactivate syntax again. Import theory @{text FinFun_Syntax} to reactivate it again\<close>
   1.363  
   1.364  no_type_notation
   1.365    finfun ("(_ =>f /_)" [22, 21] 21)