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.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.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.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.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.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.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)
```