src/HOL/Library/FinFun.thy
author Andreas Lochbihler
Tue May 29 15:31:58 2012 +0200 (2012-05-29)
changeset 48028 a5377f6d9f14
child 48029 9d9c9069abbc
permissions -rw-r--r--
move FinFuns from AFP to repository
Andreas@48028
     1
(* Author: Andreas Lochbihler, Uni Karlsruhe *)
Andreas@48028
     2
Andreas@48028
     3
header {* Almost everywhere constant functions *}
Andreas@48028
     4
Andreas@48028
     5
theory FinFun
Andreas@48028
     6
imports Card_Univ
Andreas@48028
     7
begin
Andreas@48028
     8
Andreas@48028
     9
text {*
Andreas@48028
    10
  This theory defines functions which are constant except for finitely
Andreas@48028
    11
  many points (FinFun) and introduces a type finfin along with a
Andreas@48028
    12
  number of operators for them. The code generator is set up such that
Andreas@48028
    13
  such functions can be represented as data in the generated code and
Andreas@48028
    14
  all operators are executable.
Andreas@48028
    15
Andreas@48028
    16
  For details, see Formalising FinFuns - Generating Code for Functions as Data by A. Lochbihler in TPHOLs 2009.
Andreas@48028
    17
*}
Andreas@48028
    18
Andreas@48028
    19
Andreas@48028
    20
definition "code_abort" :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a"
Andreas@48028
    21
where [simp, code del]: "code_abort f = f ()"
Andreas@48028
    22
Andreas@48028
    23
code_abort "code_abort"
Andreas@48028
    24
Andreas@48028
    25
hide_const (open) "code_abort"
Andreas@48028
    26
Andreas@48028
    27
subsection {* The @{text "map_default"} operation *}
Andreas@48028
    28
Andreas@48028
    29
definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
Andreas@48028
    30
where "map_default b f a \<equiv> case f a of None \<Rightarrow> b | Some b' \<Rightarrow> b'"
Andreas@48028
    31
Andreas@48028
    32
lemma map_default_delete [simp]:
Andreas@48028
    33
  "map_default b (f(a := None)) = (map_default b f)(a := b)"
Andreas@48028
    34
by(simp add: map_default_def fun_eq_iff)
Andreas@48028
    35
Andreas@48028
    36
lemma map_default_insert:
Andreas@48028
    37
  "map_default b (f(a \<mapsto> b')) = (map_default b f)(a := b')"
Andreas@48028
    38
by(simp add: map_default_def fun_eq_iff)
Andreas@48028
    39
Andreas@48028
    40
lemma map_default_empty [simp]: "map_default b empty = (\<lambda>a. b)"
Andreas@48028
    41
by(simp add: fun_eq_iff map_default_def)
Andreas@48028
    42
Andreas@48028
    43
lemma map_default_inject:
Andreas@48028
    44
  fixes g g' :: "'a \<rightharpoonup> 'b"
Andreas@48028
    45
  assumes infin_eq: "\<not> finite (UNIV :: 'a set) \<or> b = b'"
Andreas@48028
    46
  and fin: "finite (dom g)" and b: "b \<notin> ran g"
Andreas@48028
    47
  and fin': "finite (dom g')" and b': "b' \<notin> ran g'"
Andreas@48028
    48
  and eq': "map_default b g = map_default b' g'"
Andreas@48028
    49
  shows "b = b'" "g = g'"
Andreas@48028
    50
proof -
Andreas@48028
    51
  from infin_eq show bb': "b = b'"
Andreas@48028
    52
  proof
Andreas@48028
    53
    assume infin: "\<not> finite (UNIV :: 'a set)"
Andreas@48028
    54
    from fin fin' have "finite (dom g \<union> dom g')" by auto
Andreas@48028
    55
    with infin have "UNIV - (dom g \<union> dom g') \<noteq> {}" by(auto dest: finite_subset)
Andreas@48028
    56
    then obtain a where a: "a \<notin> dom g \<union> dom g'" by auto
Andreas@48028
    57
    hence "map_default b g a = b" "map_default b' g' a = b'" by(auto simp add: map_default_def)
Andreas@48028
    58
    with eq' show "b = b'" by simp
Andreas@48028
    59
  qed
Andreas@48028
    60
Andreas@48028
    61
  show "g = g'"
Andreas@48028
    62
  proof
Andreas@48028
    63
    fix x
Andreas@48028
    64
    show "g x = g' x"
Andreas@48028
    65
    proof(cases "g x")
Andreas@48028
    66
      case None
Andreas@48028
    67
      hence "map_default b g x = b" by(simp add: map_default_def)
Andreas@48028
    68
      with bb' eq' have "map_default b' g' x = b'" by simp
Andreas@48028
    69
      with b' have "g' x = None" by(simp add: map_default_def ran_def split: option.split_asm)
Andreas@48028
    70
      with None show ?thesis by simp
Andreas@48028
    71
    next
Andreas@48028
    72
      case (Some c)
Andreas@48028
    73
      with b have cb: "c \<noteq> b" by(auto simp add: ran_def)
Andreas@48028
    74
      moreover from Some have "map_default b g x = c" by(simp add: map_default_def)
Andreas@48028
    75
      with eq' have "map_default b' g' x = c" by simp
Andreas@48028
    76
      ultimately have "g' x = Some c" using b' bb' by(auto simp add: map_default_def split: option.splits)
Andreas@48028
    77
      with Some show ?thesis by simp
Andreas@48028
    78
    qed
Andreas@48028
    79
  qed
Andreas@48028
    80
qed
Andreas@48028
    81
Andreas@48028
    82
subsection {* The finfun type *}
Andreas@48028
    83
Andreas@48028
    84
definition "finfun = {f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
Andreas@48028
    85
Andreas@48028
    86
typedef (open) ('a,'b) finfun  ("(_ \<Rightarrow>\<^isub>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
Andreas@48028
    87
proof -
Andreas@48028
    88
  have "\<exists>f. finite {x. f x \<noteq> undefined}"
Andreas@48028
    89
  proof
Andreas@48028
    90
    show "finite {x. (\<lambda>y. undefined) x \<noteq> undefined}" by auto
Andreas@48028
    91
  qed
Andreas@48028
    92
  then show ?thesis unfolding finfun_def by auto
Andreas@48028
    93
qed
Andreas@48028
    94
Andreas@48028
    95
setup_lifting type_definition_finfun
Andreas@48028
    96
Andreas@48028
    97
lemma fun_upd_finfun: "y(a := b) \<in> finfun \<longleftrightarrow> y \<in> finfun"
Andreas@48028
    98
proof -
Andreas@48028
    99
  { fix b'
Andreas@48028
   100
    have "finite {a'. (y(a := b)) a' \<noteq> b'} = finite {a'. y a' \<noteq> b'}"
Andreas@48028
   101
    proof(cases "b = b'")
Andreas@48028
   102
      case True
Andreas@48028
   103
      hence "{a'. (y(a := b)) a' \<noteq> b'} = {a'. y a' \<noteq> b'} - {a}" by auto
Andreas@48028
   104
      thus ?thesis by simp
Andreas@48028
   105
    next
Andreas@48028
   106
      case False
Andreas@48028
   107
      hence "{a'. (y(a := b)) a' \<noteq> b'} = insert a {a'. y a' \<noteq> b'}" by auto
Andreas@48028
   108
      thus ?thesis by simp
Andreas@48028
   109
    qed }
Andreas@48028
   110
  thus ?thesis unfolding finfun_def by blast
Andreas@48028
   111
qed
Andreas@48028
   112
Andreas@48028
   113
lemma const_finfun: "(\<lambda>x. a) \<in> finfun"
Andreas@48028
   114
by(auto simp add: finfun_def)
Andreas@48028
   115
Andreas@48028
   116
lemma finfun_left_compose:
Andreas@48028
   117
  assumes "y \<in> finfun"
Andreas@48028
   118
  shows "g \<circ> y \<in> finfun"
Andreas@48028
   119
proof -
Andreas@48028
   120
  from assms obtain b where "finite {a. y a \<noteq> b}"
Andreas@48028
   121
    unfolding finfun_def by blast
Andreas@48028
   122
  hence "finite {c. g (y c) \<noteq> g b}"
Andreas@48028
   123
  proof(induct "{a. y a \<noteq> b}" arbitrary: y)
Andreas@48028
   124
    case empty
Andreas@48028
   125
    hence "y = (\<lambda>a. b)" by(auto intro: ext)
Andreas@48028
   126
    thus ?case by(simp)
Andreas@48028
   127
  next
Andreas@48028
   128
    case (insert x F)
Andreas@48028
   129
    note IH = `\<And>y. F = {a. y a \<noteq> b} \<Longrightarrow> finite {c. g (y c) \<noteq> g b}`
Andreas@48028
   130
    from `insert x F = {a. y a \<noteq> b}` `x \<notin> F`
Andreas@48028
   131
    have F: "F = {a. (y(x := b)) a \<noteq> b}" by(auto)
Andreas@48028
   132
    show ?case
Andreas@48028
   133
    proof(cases "g (y x) = g b")
Andreas@48028
   134
      case True
Andreas@48028
   135
      hence "{c. g ((y(x := b)) c) \<noteq> g b} = {c. g (y c) \<noteq> g b}" by auto
Andreas@48028
   136
      with IH[OF F] show ?thesis by simp
Andreas@48028
   137
    next
Andreas@48028
   138
      case False
Andreas@48028
   139
      hence "{c. g (y c) \<noteq> g b} = insert x {c. g ((y(x := b)) c) \<noteq> g b}" by auto
Andreas@48028
   140
      with IH[OF F] show ?thesis by(simp)
Andreas@48028
   141
    qed
Andreas@48028
   142
  qed
Andreas@48028
   143
  thus ?thesis unfolding finfun_def by auto
Andreas@48028
   144
qed
Andreas@48028
   145
Andreas@48028
   146
lemma assumes "y \<in> finfun"
Andreas@48028
   147
  shows fst_finfun: "fst \<circ> y \<in> finfun"
Andreas@48028
   148
  and snd_finfun: "snd \<circ> y \<in> finfun"
Andreas@48028
   149
proof -
Andreas@48028
   150
  from assms obtain b c where bc: "finite {a. y a \<noteq> (b, c)}"
Andreas@48028
   151
    unfolding finfun_def by auto
Andreas@48028
   152
  have "{a. fst (y a) \<noteq> b} \<subseteq> {a. y a \<noteq> (b, c)}"
Andreas@48028
   153
    and "{a. snd (y a) \<noteq> c} \<subseteq> {a. y a \<noteq> (b, c)}" by auto
Andreas@48028
   154
  hence "finite {a. fst (y a) \<noteq> b}" 
Andreas@48028
   155
    and "finite {a. snd (y a) \<noteq> c}" using bc by(auto intro: finite_subset)
Andreas@48028
   156
  thus "fst \<circ> y \<in> finfun" "snd \<circ> y \<in> finfun"
Andreas@48028
   157
    unfolding finfun_def by auto
Andreas@48028
   158
qed
Andreas@48028
   159
Andreas@48028
   160
lemma map_of_finfun: "map_of xs \<in> finfun"
Andreas@48028
   161
unfolding finfun_def
Andreas@48028
   162
by(induct xs)(auto simp add: Collect_neg_eq Collect_conj_eq Collect_imp_eq intro: finite_subset)
Andreas@48028
   163
Andreas@48028
   164
lemma Diag_finfun: "(\<lambda>x. (f x, g x)) \<in> finfun \<longleftrightarrow> f \<in> finfun \<and> g \<in> finfun"
Andreas@48028
   165
by(auto intro: finite_subset simp add: Collect_neg_eq Collect_imp_eq Collect_conj_eq finfun_def)
Andreas@48028
   166
Andreas@48028
   167
lemma finfun_right_compose:
Andreas@48028
   168
  assumes g: "g \<in> finfun" and inj: "inj f"
Andreas@48028
   169
  shows "g o f \<in> finfun"
Andreas@48028
   170
proof -
Andreas@48028
   171
  from g obtain b where b: "finite {a. g a \<noteq> b}" unfolding finfun_def by blast
Andreas@48028
   172
  moreover have "f ` {a. g (f a) \<noteq> b} \<subseteq> {a. g a \<noteq> b}" by auto
Andreas@48028
   173
  moreover from inj have "inj_on f {a.  g (f a) \<noteq> b}" by(rule subset_inj_on) blast
Andreas@48028
   174
  ultimately have "finite {a. g (f a) \<noteq> b}"
Andreas@48028
   175
    by(blast intro: finite_imageD[where f=f] finite_subset)
Andreas@48028
   176
  thus ?thesis unfolding finfun_def by auto
Andreas@48028
   177
qed
Andreas@48028
   178
Andreas@48028
   179
lemma finfun_curry:
Andreas@48028
   180
  assumes fin: "f \<in> finfun"
Andreas@48028
   181
  shows "curry f \<in> finfun" "curry f a \<in> finfun"
Andreas@48028
   182
proof -
Andreas@48028
   183
  from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
Andreas@48028
   184
  moreover have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
Andreas@48028
   185
  hence "{a. curry f a \<noteq> (\<lambda>b. c)} = fst ` {ab. f ab \<noteq> c}"
Andreas@48028
   186
    by(auto simp add: curry_def fun_eq_iff)
Andreas@48028
   187
  ultimately have "finite {a. curry f a \<noteq> (\<lambda>b. c)}" by simp
Andreas@48028
   188
  thus "curry f \<in> finfun" unfolding finfun_def by blast
Andreas@48028
   189
  
Andreas@48028
   190
  have "snd ` {ab. f ab \<noteq> c} = {b. \<exists>a. f (a, b) \<noteq> c}" by(force)
Andreas@48028
   191
  hence "{b. f (a, b) \<noteq> c} \<subseteq> snd ` {ab. f ab \<noteq> c}" by auto
Andreas@48028
   192
  hence "finite {b. f (a, b) \<noteq> c}" by(rule finite_subset)(rule finite_imageI[OF c])
Andreas@48028
   193
  thus "curry f a \<in> finfun" unfolding finfun_def by auto
Andreas@48028
   194
qed
Andreas@48028
   195
Andreas@48028
   196
lemmas finfun_simp = 
Andreas@48028
   197
  fst_finfun snd_finfun Abs_finfun_inverse Rep_finfun_inverse Abs_finfun_inject Rep_finfun_inject Diag_finfun finfun_curry
Andreas@48028
   198
lemmas finfun_iff = const_finfun fun_upd_finfun Rep_finfun map_of_finfun
Andreas@48028
   199
lemmas finfun_intro = finfun_left_compose fst_finfun snd_finfun
Andreas@48028
   200
Andreas@48028
   201
lemma Abs_finfun_inject_finite:
Andreas@48028
   202
  fixes x y :: "'a \<Rightarrow> 'b"
Andreas@48028
   203
  assumes fin: "finite (UNIV :: 'a set)"
Andreas@48028
   204
  shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
Andreas@48028
   205
proof
Andreas@48028
   206
  assume "Abs_finfun x = Abs_finfun y"
Andreas@48028
   207
  moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
Andreas@48028
   208
    by(auto intro: finite_subset[OF _ fin])
Andreas@48028
   209
  ultimately show "x = y" by(simp add: Abs_finfun_inject)
Andreas@48028
   210
qed simp
Andreas@48028
   211
Andreas@48028
   212
lemma Abs_finfun_inject_finite_class:
Andreas@48028
   213
  fixes x y :: "('a :: finite) \<Rightarrow> 'b"
Andreas@48028
   214
  shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
Andreas@48028
   215
using finite_UNIV
Andreas@48028
   216
by(simp add: Abs_finfun_inject_finite)
Andreas@48028
   217
Andreas@48028
   218
lemma Abs_finfun_inj_finite:
Andreas@48028
   219
  assumes fin: "finite (UNIV :: 'a set)"
Andreas@48028
   220
  shows "inj (Abs_finfun :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b)"
Andreas@48028
   221
proof(rule inj_onI)
Andreas@48028
   222
  fix x y :: "'a \<Rightarrow> 'b"
Andreas@48028
   223
  assume "Abs_finfun x = Abs_finfun y"
Andreas@48028
   224
  moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
Andreas@48028
   225
    by(auto intro: finite_subset[OF _ fin])
Andreas@48028
   226
  ultimately show "x = y" by(simp add: Abs_finfun_inject)
Andreas@48028
   227
qed
Andreas@48028
   228
Andreas@48028
   229
declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
Andreas@48028
   230
Andreas@48028
   231
lemma Abs_finfun_inverse_finite:
Andreas@48028
   232
  fixes x :: "'a \<Rightarrow> 'b"
Andreas@48028
   233
  assumes fin: "finite (UNIV :: 'a set)"
Andreas@48028
   234
  shows "Rep_finfun (Abs_finfun x) = x"
Andreas@48028
   235
proof -
Andreas@48028
   236
  from fin have "x \<in> finfun"
Andreas@48028
   237
    by(auto simp add: finfun_def intro: finite_subset)
Andreas@48028
   238
  thus ?thesis by simp
Andreas@48028
   239
qed
Andreas@48028
   240
Andreas@48028
   241
declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
Andreas@48028
   242
Andreas@48028
   243
lemma Abs_finfun_inverse_finite_class:
Andreas@48028
   244
  fixes x :: "('a :: finite) \<Rightarrow> 'b"
Andreas@48028
   245
  shows "Rep_finfun (Abs_finfun x) = x"
Andreas@48028
   246
using finite_UNIV by(simp add: Abs_finfun_inverse_finite)
Andreas@48028
   247
Andreas@48028
   248
lemma finfun_eq_finite_UNIV: "finite (UNIV :: 'a set) \<Longrightarrow> (finfun :: ('a \<Rightarrow> 'b) set) = UNIV"
Andreas@48028
   249
unfolding finfun_def by(auto intro: finite_subset)
Andreas@48028
   250
Andreas@48028
   251
lemma finfun_finite_UNIV_class: "finfun = (UNIV :: ('a :: finite \<Rightarrow> 'b) set)"
Andreas@48028
   252
by(simp add: finfun_eq_finite_UNIV)
Andreas@48028
   253
Andreas@48028
   254
lemma map_default_in_finfun:
Andreas@48028
   255
  assumes fin: "finite (dom f)"
Andreas@48028
   256
  shows "map_default b f \<in> finfun"
Andreas@48028
   257
unfolding finfun_def
Andreas@48028
   258
proof(intro CollectI exI)
Andreas@48028
   259
  from fin show "finite {a. map_default b f a \<noteq> b}"
Andreas@48028
   260
    by(auto simp add: map_default_def dom_def Collect_conj_eq split: option.splits)
Andreas@48028
   261
qed
Andreas@48028
   262
Andreas@48028
   263
lemma finfun_cases_map_default:
Andreas@48028
   264
  obtains b g where "f = Abs_finfun (map_default b g)" "finite (dom g)" "b \<notin> ran g"
Andreas@48028
   265
proof -
Andreas@48028
   266
  obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by(cases f)
Andreas@48028
   267
  from y obtain b where b: "finite {a. y a \<noteq> b}" unfolding finfun_def by auto
Andreas@48028
   268
  let ?g = "(\<lambda>a. if y a = b then None else Some (y a))"
Andreas@48028
   269
  have "map_default b ?g = y" by(simp add: fun_eq_iff map_default_def)
Andreas@48028
   270
  with f have "f = Abs_finfun (map_default b ?g)" by simp
Andreas@48028
   271
  moreover from b have "finite (dom ?g)" by(auto simp add: dom_def)
Andreas@48028
   272
  moreover have "b \<notin> ran ?g" by(auto simp add: ran_def)
Andreas@48028
   273
  ultimately show ?thesis by(rule that)
Andreas@48028
   274
qed
Andreas@48028
   275
Andreas@48028
   276
Andreas@48028
   277
subsection {* Kernel functions for type @{typ "'a \<Rightarrow>\<^isub>f 'b"} *}
Andreas@48028
   278
Andreas@48028
   279
lift_definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("\<lambda>\<^isup>f/ _" [0] 1)
Andreas@48028
   280
is "\<lambda> b x. b" by (rule const_finfun)
Andreas@48028
   281
Andreas@48028
   282
lift_definition finfun_update :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>f/ _ := _')" [1000,0,0] 1000) is "fun_upd" by (simp add: fun_upd_finfun)
Andreas@48028
   283
Andreas@48028
   284
declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
Andreas@48028
   285
Andreas@48028
   286
lemma finfun_update_twist: "a \<noteq> a' \<Longrightarrow> f(\<^sup>f a := b)(\<^sup>f a' := b') = f(\<^sup>f a' := b')(\<^sup>f a := b)"
Andreas@48028
   287
by transfer (simp add: fun_upd_twist)
Andreas@48028
   288
Andreas@48028
   289
lemma finfun_update_twice [simp]:
Andreas@48028
   290
  "finfun_update (finfun_update f a b) a b' = finfun_update f a b'"
Andreas@48028
   291
by transfer simp
Andreas@48028
   292
Andreas@48028
   293
lemma finfun_update_const_same: "(\<lambda>\<^isup>f b)(\<^sup>f a := b) = (\<lambda>\<^isup>f b)"
Andreas@48028
   294
by transfer (simp add: fun_eq_iff)
Andreas@48028
   295
Andreas@48028
   296
declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
Andreas@48028
   297
Andreas@48028
   298
subsection {* Code generator setup *}
Andreas@48028
   299
Andreas@48028
   300
definition finfun_update_code :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>fc/ _ := _')" [1000,0,0] 1000)
Andreas@48028
   301
where [simp, code del]: "finfun_update_code = finfun_update"
Andreas@48028
   302
Andreas@48028
   303
code_datatype finfun_const finfun_update_code
Andreas@48028
   304
Andreas@48028
   305
lemma finfun_update_const_code [code]:
Andreas@48028
   306
  "(\<lambda>\<^isup>f b)(\<^sup>f a := b') = (if b = b' then (\<lambda>\<^isup>f b) else finfun_update_code (\<lambda>\<^isup>f b) a b')"
Andreas@48028
   307
by(simp add: finfun_update_const_same)
Andreas@48028
   308
Andreas@48028
   309
lemma finfun_update_update_code [code]:
Andreas@48028
   310
  "(finfun_update_code f a b)(\<^sup>f a' := b') = (if a = a' then f(\<^sup>f a := b') else finfun_update_code (f(\<^sup>f a' := b')) a b)"
Andreas@48028
   311
by(simp add: finfun_update_twist)
Andreas@48028
   312
Andreas@48028
   313
Andreas@48028
   314
subsection {* Setup for quickcheck *}
Andreas@48028
   315
Andreas@48028
   316
quickcheck_generator finfun constructors: finfun_update_code, "finfun_const :: 'b => 'a \<Rightarrow>\<^isub>f 'b"
Andreas@48028
   317
Andreas@48028
   318
subsection {* @{text "finfun_update"} as instance of @{text "comp_fun_commute"} *}
Andreas@48028
   319
Andreas@48028
   320
declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
Andreas@48028
   321
Andreas@48028
   322
interpretation finfun_update: comp_fun_commute "\<lambda>a f. f(\<^sup>f a :: 'a := b')"
Andreas@48028
   323
proof
Andreas@48028
   324
  fix a a' :: 'a
Andreas@48028
   325
  show "(\<lambda>f. f(\<^sup>f a := b')) \<circ> (\<lambda>f. f(\<^sup>f a' := b')) = (\<lambda>f. f(\<^sup>f a' := b')) \<circ> (\<lambda>f. f(\<^sup>f a := b'))"
Andreas@48028
   326
  proof
Andreas@48028
   327
    fix b
Andreas@48028
   328
    have "(Rep_finfun b)(a := b', a' := b') = (Rep_finfun b)(a' := b', a := b')"
Andreas@48028
   329
      by(cases "a = a'")(auto simp add: fun_upd_twist)
Andreas@48028
   330
    then have "b(\<^sup>f a := b')(\<^sup>f a' := b') = b(\<^sup>f a' := b')(\<^sup>f a := b')"
Andreas@48028
   331
      by(auto simp add: finfun_update_def fun_upd_twist)
Andreas@48028
   332
    then show "((\<lambda>f. f(\<^sup>f a := b')) \<circ> (\<lambda>f. f(\<^sup>f a' := b'))) b = ((\<lambda>f. f(\<^sup>f a' := b')) \<circ> (\<lambda>f. f(\<^sup>f a := b'))) b"
Andreas@48028
   333
      by (simp add: fun_eq_iff)
Andreas@48028
   334
  qed
Andreas@48028
   335
qed
Andreas@48028
   336
Andreas@48028
   337
lemma fold_finfun_update_finite_univ:
Andreas@48028
   338
  assumes fin: "finite (UNIV :: 'a set)"
Andreas@48028
   339
  shows "Finite_Set.fold (\<lambda>a f. f(\<^sup>f a := b')) (\<lambda>\<^isup>f b) (UNIV :: 'a set) = (\<lambda>\<^isup>f b')"
Andreas@48028
   340
proof -
Andreas@48028
   341
  { fix A :: "'a set"
Andreas@48028
   342
    from fin have "finite A" by(auto intro: finite_subset)
Andreas@48028
   343
    hence "Finite_Set.fold (\<lambda>a f. f(\<^sup>f a := b')) (\<lambda>\<^isup>f b) A = Abs_finfun (\<lambda>a. if a \<in> A then b' else b)"
Andreas@48028
   344
    proof(induct)
Andreas@48028
   345
      case (insert x F)
Andreas@48028
   346
      have "(\<lambda>a. if a = x then b' else (if a \<in> F then b' else b)) = (\<lambda>a. if a = x \<or> a \<in> F then b' else b)"
Andreas@48028
   347
        by(auto intro: ext)
Andreas@48028
   348
      with insert show ?case
Andreas@48028
   349
        by(simp add: finfun_const_def fun_upd_def)(simp add: finfun_update_def Abs_finfun_inverse_finite[OF fin] fun_upd_def)
Andreas@48028
   350
    qed(simp add: finfun_const_def) }
Andreas@48028
   351
  thus ?thesis by(simp add: finfun_const_def)
Andreas@48028
   352
qed
Andreas@48028
   353
Andreas@48028
   354
Andreas@48028
   355
subsection {* Default value for FinFuns *}
Andreas@48028
   356
Andreas@48028
   357
definition finfun_default_aux :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"
Andreas@48028
   358
where [code del]: "finfun_default_aux f = (if finite (UNIV :: 'a set) then undefined else THE b. finite {a. f a \<noteq> b})"
Andreas@48028
   359
Andreas@48028
   360
lemma finfun_default_aux_infinite:
Andreas@48028
   361
  fixes f :: "'a \<Rightarrow> 'b"
Andreas@48028
   362
  assumes infin: "\<not> finite (UNIV :: 'a set)"
Andreas@48028
   363
  and fin: "finite {a. f a \<noteq> b}"
Andreas@48028
   364
  shows "finfun_default_aux f = b"
Andreas@48028
   365
proof -
Andreas@48028
   366
  let ?B = "{a. f a \<noteq> b}"
Andreas@48028
   367
  from fin have "(THE b. finite {a. f a \<noteq> b}) = b"
Andreas@48028
   368
  proof(rule the_equality)
Andreas@48028
   369
    fix b'
Andreas@48028
   370
    assume "finite {a. f a \<noteq> b'}" (is "finite ?B'")
Andreas@48028
   371
    with infin fin have "UNIV - (?B' \<union> ?B) \<noteq> {}" by(auto dest: finite_subset)
Andreas@48028
   372
    then obtain a where a: "a \<notin> ?B' \<union> ?B" by auto
Andreas@48028
   373
    thus "b' = b" by auto
Andreas@48028
   374
  qed
Andreas@48028
   375
  thus ?thesis using infin by(simp add: finfun_default_aux_def)
Andreas@48028
   376
qed
Andreas@48028
   377
Andreas@48028
   378
Andreas@48028
   379
lemma finite_finfun_default_aux:
Andreas@48028
   380
  fixes f :: "'a \<Rightarrow> 'b"
Andreas@48028
   381
  assumes fin: "f \<in> finfun"
Andreas@48028
   382
  shows "finite {a. f a \<noteq> finfun_default_aux f}"
Andreas@48028
   383
proof(cases "finite (UNIV :: 'a set)")
Andreas@48028
   384
  case True thus ?thesis using fin
Andreas@48028
   385
    by(auto simp add: finfun_def finfun_default_aux_def intro: finite_subset)
Andreas@48028
   386
next
Andreas@48028
   387
  case False
Andreas@48028
   388
  from fin obtain b where b: "finite {a. f a \<noteq> b}" (is "finite ?B")
Andreas@48028
   389
    unfolding finfun_def by blast
Andreas@48028
   390
  with False show ?thesis by(simp add: finfun_default_aux_infinite)
Andreas@48028
   391
qed
Andreas@48028
   392
Andreas@48028
   393
lemma finfun_default_aux_update_const:
Andreas@48028
   394
  fixes f :: "'a \<Rightarrow> 'b"
Andreas@48028
   395
  assumes fin: "f \<in> finfun"
Andreas@48028
   396
  shows "finfun_default_aux (f(a := b)) = finfun_default_aux f"
Andreas@48028
   397
proof(cases "finite (UNIV :: 'a set)")
Andreas@48028
   398
  case False
Andreas@48028
   399
  from fin obtain b' where b': "finite {a. f a \<noteq> b'}" unfolding finfun_def by blast
Andreas@48028
   400
  hence "finite {a'. (f(a := b)) a' \<noteq> b'}"
Andreas@48028
   401
  proof(cases "b = b' \<and> f a \<noteq> b'") 
Andreas@48028
   402
    case True
Andreas@48028
   403
    hence "{a. f a \<noteq> b'} = insert a {a'. (f(a := b)) a' \<noteq> b'}" by auto
Andreas@48028
   404
    thus ?thesis using b' by simp
Andreas@48028
   405
  next
Andreas@48028
   406
    case False
Andreas@48028
   407
    moreover
Andreas@48028
   408
    { assume "b \<noteq> b'"
Andreas@48028
   409
      hence "{a'. (f(a := b)) a' \<noteq> b'} = insert a {a. f a \<noteq> b'}" by auto
Andreas@48028
   410
      hence ?thesis using b' by simp }
Andreas@48028
   411
    moreover
Andreas@48028
   412
    { assume "b = b'" "f a = b'"
Andreas@48028
   413
      hence "{a'. (f(a := b)) a' \<noteq> b'} = {a. f a \<noteq> b'}" by auto
Andreas@48028
   414
      hence ?thesis using b' by simp }
Andreas@48028
   415
    ultimately show ?thesis by blast
Andreas@48028
   416
  qed
Andreas@48028
   417
  with False b' show ?thesis by(auto simp del: fun_upd_apply simp add: finfun_default_aux_infinite)
Andreas@48028
   418
next
Andreas@48028
   419
  case True thus ?thesis by(simp add: finfun_default_aux_def)
Andreas@48028
   420
qed
Andreas@48028
   421
Andreas@48028
   422
lift_definition finfun_default :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'b"
Andreas@48028
   423
is "finfun_default_aux" ..
Andreas@48028
   424
Andreas@48028
   425
lemma finite_finfun_default: "finite {a. Rep_finfun f a \<noteq> finfun_default f}"
Andreas@48028
   426
apply transfer apply (erule finite_finfun_default_aux)
Andreas@48028
   427
unfolding Rel_def fun_rel_def cr_finfun_def by simp
Andreas@48028
   428
Andreas@48028
   429
lemma finfun_default_const: "finfun_default ((\<lambda>\<^isup>f b) :: 'a \<Rightarrow>\<^isub>f 'b) = (if finite (UNIV :: 'a set) then undefined else b)"
Andreas@48028
   430
apply(transfer)
Andreas@48028
   431
apply(auto simp add: finfun_default_aux_infinite)
Andreas@48028
   432
apply(simp add: finfun_default_aux_def)
Andreas@48028
   433
done
Andreas@48028
   434
Andreas@48028
   435
lemma finfun_default_update_const:
Andreas@48028
   436
  "finfun_default (f(\<^sup>f a := b)) = finfun_default f"
Andreas@48028
   437
by transfer (simp add: finfun_default_aux_update_const)
Andreas@48028
   438
Andreas@48028
   439
lemma finfun_default_const_code [code]:
Andreas@48028
   440
  "finfun_default ((\<lambda>\<^isup>f c) :: ('a :: card_UNIV) \<Rightarrow>\<^isub>f 'b) = (if card_UNIV (TYPE('a)) = 0 then c else undefined)"
Andreas@48028
   441
by(simp add: finfun_default_const card_UNIV_eq_0_infinite_UNIV)
Andreas@48028
   442
Andreas@48028
   443
lemma finfun_default_update_code [code]:
Andreas@48028
   444
  "finfun_default (finfun_update_code f a b) = finfun_default f"
Andreas@48028
   445
by(simp add: finfun_default_update_const)
Andreas@48028
   446
Andreas@48028
   447
subsection {* Recursion combinator and well-formedness conditions *}
Andreas@48028
   448
Andreas@48028
   449
definition finfun_rec :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<Rightarrow> 'c"
Andreas@48028
   450
where [code del]:
Andreas@48028
   451
  "finfun_rec cnst upd f \<equiv>
Andreas@48028
   452
   let b = finfun_default f;
Andreas@48028
   453
       g = THE g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g
Andreas@48028
   454
   in Finite_Set.fold (\<lambda>a. upd a (map_default b g a)) (cnst b) (dom g)"
Andreas@48028
   455
Andreas@48028
   456
locale finfun_rec_wf_aux =
Andreas@48028
   457
  fixes cnst :: "'b \<Rightarrow> 'c"
Andreas@48028
   458
  and upd :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c"
Andreas@48028
   459
  assumes upd_const_same: "upd a b (cnst b) = cnst b"
Andreas@48028
   460
  and upd_commute: "a \<noteq> a' \<Longrightarrow> upd a b (upd a' b' c) = upd a' b' (upd a b c)"
Andreas@48028
   461
  and upd_idemp: "b \<noteq> b' \<Longrightarrow> upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
Andreas@48028
   462
begin
Andreas@48028
   463
Andreas@48028
   464
Andreas@48028
   465
lemma upd_left_comm: "comp_fun_commute (\<lambda>a. upd a (f a))"
Andreas@48028
   466
by(unfold_locales)(auto intro: upd_commute simp add: fun_eq_iff)
Andreas@48028
   467
Andreas@48028
   468
lemma upd_upd_twice: "upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
Andreas@48028
   469
by(cases "b \<noteq> b'")(auto simp add: fun_upd_def upd_const_same upd_idemp)
Andreas@48028
   470
Andreas@48028
   471
declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
Andreas@48028
   472
Andreas@48028
   473
lemma map_default_update_const:
Andreas@48028
   474
  assumes fin: "finite (dom f)"
Andreas@48028
   475
  and anf: "a \<notin> dom f"
Andreas@48028
   476
  and fg: "f \<subseteq>\<^sub>m g"
Andreas@48028
   477
  shows "upd a d  (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)) =
Andreas@48028
   478
         Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)"
Andreas@48028
   479
proof -
Andreas@48028
   480
  let ?upd = "\<lambda>a. upd a (map_default d g a)"
Andreas@48028
   481
  let ?fr = "\<lambda>A. Finite_Set.fold ?upd (cnst d) A"
Andreas@48028
   482
  interpret gwf: comp_fun_commute "?upd" by(rule upd_left_comm)
Andreas@48028
   483
  
Andreas@48028
   484
  from fin anf fg show ?thesis
Andreas@48028
   485
  proof(induct "dom f" arbitrary: f)
Andreas@48028
   486
    case empty
Andreas@48028
   487
    from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
Andreas@48028
   488
    thus ?case by(simp add: finfun_const_def upd_const_same)
Andreas@48028
   489
  next
Andreas@48028
   490
    case (insert a' A)
Andreas@48028
   491
    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)`
Andreas@48028
   492
    note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
Andreas@48028
   493
    note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
Andreas@48028
   494
    
Andreas@48028
   495
    from domf obtain b where b: "f a' = Some b" by auto
Andreas@48028
   496
    let ?f' = "f(a' := None)"
Andreas@48028
   497
    have "upd a d (?fr (insert a' A)) = upd a d (upd a' (map_default d g a') (?fr A))"
Andreas@48028
   498
      by(subst gwf.fold_insert[OF fin a'nA]) rule
Andreas@48028
   499
    also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
Andreas@48028
   500
    hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
Andreas@48028
   501
    also from anf domf have "a \<noteq> a'" by auto note upd_commute[OF this]
Andreas@48028
   502
    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)
Andreas@48028
   503
    note A also note IH[OF A `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g`]
Andreas@48028
   504
    also have "upd a' (map_default d f a') (?fr (dom (f(a' := None)))) = ?fr (dom f)"
Andreas@48028
   505
      unfolding domf[symmetric] gwf.fold_insert[OF fin a'nA] ga' unfolding A ..
Andreas@48028
   506
    also have "insert a' (dom ?f') = dom f" using domf by auto
Andreas@48028
   507
    finally show ?case .
Andreas@48028
   508
  qed
Andreas@48028
   509
qed
Andreas@48028
   510
Andreas@48028
   511
lemma map_default_update_twice:
Andreas@48028
   512
  assumes fin: "finite (dom f)"
Andreas@48028
   513
  and anf: "a \<notin> dom f"
Andreas@48028
   514
  and fg: "f \<subseteq>\<^sub>m g"
Andreas@48028
   515
  shows "upd a d'' (upd a d' (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))) =
Andreas@48028
   516
         upd a d'' (Finite_Set.fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))"
Andreas@48028
   517
proof -
Andreas@48028
   518
  let ?upd = "\<lambda>a. upd a (map_default d g a)"
Andreas@48028
   519
  let ?fr = "\<lambda>A. Finite_Set.fold ?upd (cnst d) A"
Andreas@48028
   520
  interpret gwf: comp_fun_commute "?upd" by(rule upd_left_comm)
Andreas@48028
   521
  
Andreas@48028
   522
  from fin anf fg show ?thesis
Andreas@48028
   523
  proof(induct "dom f" arbitrary: f)
Andreas@48028
   524
    case empty
Andreas@48028
   525
    from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
Andreas@48028
   526
    thus ?case by(auto simp add: finfun_const_def finfun_update_def upd_upd_twice)
Andreas@48028
   527
  next
Andreas@48028
   528
    case (insert a' A)
Andreas@48028
   529
    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))`
Andreas@48028
   530
    note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
Andreas@48028
   531
    note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
Andreas@48028
   532
    
Andreas@48028
   533
    from domf obtain b where b: "f a' = Some b" by auto
Andreas@48028
   534
    let ?f' = "f(a' := None)"
Andreas@48028
   535
    let ?b' = "case f a' of None \<Rightarrow> d | Some b \<Rightarrow> b"
Andreas@48028
   536
    from domf have "upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (upd a d' (?fr (insert a' A)))" by simp
Andreas@48028
   537
    also note gwf.fold_insert[OF fin a'nA]
Andreas@48028
   538
    also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
Andreas@48028
   539
    hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
Andreas@48028
   540
    also from anf domf have ana': "a \<noteq> a'" by auto note upd_commute[OF this]
Andreas@48028
   541
    also note upd_commute[OF ana']
Andreas@48028
   542
    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)
Andreas@48028
   543
    note A also note IH[OF A `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g`]
Andreas@48028
   544
    also note upd_commute[OF ana'[symmetric]] also note ga'[symmetric] also note A[symmetric]
Andreas@48028
   545
    also note gwf.fold_insert[symmetric, OF fin a'nA] also note domf
Andreas@48028
   546
    finally show ?case .
Andreas@48028
   547
  qed
Andreas@48028
   548
qed
Andreas@48028
   549
Andreas@48028
   550
declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
Andreas@48028
   551
Andreas@48028
   552
lemma map_default_eq_id [simp]: "map_default d ((\<lambda>a. Some (f a)) |` {a. f a \<noteq> d}) = f"
Andreas@48028
   553
by(auto simp add: map_default_def restrict_map_def intro: ext)
Andreas@48028
   554
Andreas@48028
   555
lemma finite_rec_cong1:
Andreas@48028
   556
  assumes f: "comp_fun_commute f" and g: "comp_fun_commute g"
Andreas@48028
   557
  and fin: "finite A"
Andreas@48028
   558
  and eq: "\<And>a. a \<in> A \<Longrightarrow> f a = g a"
Andreas@48028
   559
  shows "Finite_Set.fold f z A = Finite_Set.fold g z A"
Andreas@48028
   560
proof -
Andreas@48028
   561
  interpret f: comp_fun_commute f by(rule f)
Andreas@48028
   562
  interpret g: comp_fun_commute g by(rule g)
Andreas@48028
   563
  { fix B
Andreas@48028
   564
    assume BsubA: "B \<subseteq> A"
Andreas@48028
   565
    with fin have "finite B" by(blast intro: finite_subset)
Andreas@48028
   566
    hence "B \<subseteq> A \<Longrightarrow> Finite_Set.fold f z B = Finite_Set.fold g z B"
Andreas@48028
   567
    proof(induct)
Andreas@48028
   568
      case empty thus ?case by simp
Andreas@48028
   569
    next
Andreas@48028
   570
      case (insert a B)
Andreas@48028
   571
      note finB = `finite B` note anB = `a \<notin> B` note sub = `insert a B \<subseteq> A`
Andreas@48028
   572
      note IH = `B \<subseteq> A \<Longrightarrow> Finite_Set.fold f z B = Finite_Set.fold g z B`
Andreas@48028
   573
      from sub anB have BpsubA: "B \<subset> A" and BsubA: "B \<subseteq> A" and aA: "a \<in> A" by auto
Andreas@48028
   574
      from IH[OF BsubA] eq[OF aA] finB anB
Andreas@48028
   575
      show ?case by(auto)
Andreas@48028
   576
    qed
Andreas@48028
   577
    with BsubA have "Finite_Set.fold f z B = Finite_Set.fold g z B" by blast }
Andreas@48028
   578
  thus ?thesis by blast
Andreas@48028
   579
qed
Andreas@48028
   580
Andreas@48028
   581
declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
Andreas@48028
   582
Andreas@48028
   583
lemma finfun_rec_upd [simp]:
Andreas@48028
   584
  "finfun_rec cnst upd (f(\<^sup>f a' := b')) = upd a' b' (finfun_rec cnst upd f)"
Andreas@48028
   585
proof -
Andreas@48028
   586
  obtain b where b: "b = finfun_default f" by auto
Andreas@48028
   587
  let ?the = "\<lambda>f g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g"
Andreas@48028
   588
  obtain g where g: "g = The (?the f)" by blast
Andreas@48028
   589
  obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by (cases f)
Andreas@48028
   590
  from f y b have bfin: "finite {a. y a \<noteq> b}" by(simp add: finfun_default_def finite_finfun_default_aux)
Andreas@48028
   591
Andreas@48028
   592
  let ?g = "(\<lambda>a. Some (y a)) |` {a. y a \<noteq> b}"
Andreas@48028
   593
  from bfin have fing: "finite (dom ?g)" by auto
Andreas@48028
   594
  have bran: "b \<notin> ran ?g" by(auto simp add: ran_def restrict_map_def)
Andreas@48028
   595
  have yg: "y = map_default b ?g" by simp
Andreas@48028
   596
  have gg: "g = ?g" unfolding g
Andreas@48028
   597
  proof(rule the_equality)
Andreas@48028
   598
    from f y bfin show "?the f ?g"
Andreas@48028
   599
      by(auto)(simp add: restrict_map_def ran_def split: split_if_asm)
Andreas@48028
   600
  next
Andreas@48028
   601
    fix g'
Andreas@48028
   602
    assume "?the f g'"
Andreas@48028
   603
    hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
Andreas@48028
   604
      and eq: "Abs_finfun (map_default b ?g) = Abs_finfun (map_default b g')" using f yg by auto
Andreas@48028
   605
    from fin' fing have "map_default b ?g \<in> finfun" "map_default b g' \<in> finfun" by(blast intro: map_default_in_finfun)+
Andreas@48028
   606
    with eq have "map_default b ?g = map_default b g'" by simp
Andreas@48028
   607
    with fing bran fin' ran' show "g' = ?g" by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
Andreas@48028
   608
  qed
Andreas@48028
   609
Andreas@48028
   610
  show ?thesis
Andreas@48028
   611
  proof(cases "b' = b")
Andreas@48028
   612
    case True
Andreas@48028
   613
    note b'b = True
Andreas@48028
   614
Andreas@48028
   615
    let ?g' = "(\<lambda>a. Some ((y(a' := b)) a)) |` {a. (y(a' := b)) a \<noteq> b}"
Andreas@48028
   616
    from bfin b'b have fing': "finite (dom ?g')"
Andreas@48028
   617
      by(auto simp add: Collect_conj_eq Collect_imp_eq intro: finite_subset)
Andreas@48028
   618
    have brang': "b \<notin> ran ?g'" by(auto simp add: ran_def restrict_map_def)
Andreas@48028
   619
Andreas@48028
   620
    let ?b' = "\<lambda>a. case ?g' a of None \<Rightarrow> b | Some b \<Rightarrow> b"
Andreas@48028
   621
    let ?b = "map_default b ?g"
Andreas@48028
   622
    from upd_left_comm upd_left_comm fing'
Andreas@48028
   623
    have "Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g') = Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')"
Andreas@48028
   624
      by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b b map_default_def)
Andreas@48028
   625
    also interpret gwf: comp_fun_commute "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
Andreas@48028
   626
    have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g') = upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))"
Andreas@48028
   627
    proof(cases "y a' = b")
Andreas@48028
   628
      case True
Andreas@48028
   629
      with b'b have g': "?g' = ?g" by(auto simp add: restrict_map_def intro: ext)
Andreas@48028
   630
      from True have a'ndomg: "a' \<notin> dom ?g" by auto
Andreas@48028
   631
      from f b'b b show ?thesis unfolding g'
Andreas@48028
   632
        by(subst map_default_update_const[OF fing a'ndomg map_le_refl, symmetric]) simp
Andreas@48028
   633
    next
Andreas@48028
   634
      case False
Andreas@48028
   635
      hence domg: "dom ?g = insert a' (dom ?g')" by auto
Andreas@48028
   636
      from False b'b have a'ndomg': "a' \<notin> dom ?g'" by auto
Andreas@48028
   637
      have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g')) = 
Andreas@48028
   638
            upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'))"
Andreas@48028
   639
        using fing' a'ndomg' unfolding b'b by(rule gwf.fold_insert)
Andreas@48028
   640
      hence "upd a' b (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g'))) =
Andreas@48028
   641
             upd a' b (upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')))" by simp
Andreas@48028
   642
      also from b'b have g'leg: "?g' \<subseteq>\<^sub>m ?g" by(auto simp add: restrict_map_def map_le_def)
Andreas@48028
   643
      note map_default_update_twice[OF fing' a'ndomg' this, of b "?b a'" b]
Andreas@48028
   644
      also note map_default_update_const[OF fing' a'ndomg' g'leg, of b]
Andreas@48028
   645
      finally show ?thesis unfolding b'b domg[unfolded b'b] by(rule sym)
Andreas@48028
   646
    qed
Andreas@48028
   647
    also have "The (?the (f(\<^sup>f a' := b'))) = ?g'"
Andreas@48028
   648
    proof(rule the_equality)
Andreas@48028
   649
      from f y b b'b brang' fing' show "?the (f(\<^sup>f a' := b')) ?g'"
Andreas@48028
   650
        by(auto simp del: fun_upd_apply simp add: finfun_update_def)
Andreas@48028
   651
    next
Andreas@48028
   652
      fix g'
Andreas@48028
   653
      assume "?the (f(\<^sup>f a' := b')) g'"
Andreas@48028
   654
      hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
Andreas@48028
   655
        and eq: "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')" 
Andreas@48028
   656
        by(auto simp del: fun_upd_apply)
Andreas@48028
   657
      from fin' fing' have "map_default b g' \<in> finfun" "map_default b ?g' \<in> finfun"
Andreas@48028
   658
        by(blast intro: map_default_in_finfun)+
Andreas@48028
   659
      with eq f b'b b have "map_default b ?g' = map_default b g'"
Andreas@48028
   660
        by(simp del: fun_upd_apply add: finfun_update_def)
Andreas@48028
   661
      with fing' brang' fin' ran' show "g' = ?g'"
Andreas@48028
   662
        by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
Andreas@48028
   663
    qed
Andreas@48028
   664
    ultimately show ?thesis unfolding finfun_rec_def Let_def b gg[unfolded g b] using bfin b'b b
Andreas@48028
   665
      by(simp only: finfun_default_update_const map_default_def)
Andreas@48028
   666
  next
Andreas@48028
   667
    case False
Andreas@48028
   668
    note b'b = this
Andreas@48028
   669
    let ?g' = "?g(a' \<mapsto> b')"
Andreas@48028
   670
    let ?b' = "map_default b ?g'"
Andreas@48028
   671
    let ?b = "map_default b ?g"
Andreas@48028
   672
    from fing have fing': "finite (dom ?g')" by auto
Andreas@48028
   673
    from bran b'b have bnrang': "b \<notin> ran ?g'" by(auto simp add: ran_def)
Andreas@48028
   674
    have ffmg': "map_default b ?g' = y(a' := b')" by(auto intro: ext simp add: map_default_def restrict_map_def)
Andreas@48028
   675
    with f y have f_Abs: "f(\<^sup>f a' := b') = Abs_finfun (map_default b ?g')" by(auto simp add: finfun_update_def)
Andreas@48028
   676
    have g': "The (?the (f(\<^sup>f a' := b'))) = ?g'"
Andreas@48028
   677
    proof (rule the_equality)
Andreas@48028
   678
      from fing' bnrang' f_Abs show "?the (f(\<^sup>f a' := b')) ?g'" by(auto simp add: finfun_update_def restrict_map_def)
Andreas@48028
   679
    next
Andreas@48028
   680
      fix g' assume "?the (f(\<^sup>f a' := b')) g'"
Andreas@48028
   681
      hence f': "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')"
Andreas@48028
   682
        and fin': "finite (dom g')" and brang': "b \<notin> ran g'" by auto
Andreas@48028
   683
      from fing' fin' have "map_default b ?g' \<in> finfun" "map_default b g' \<in> finfun"
Andreas@48028
   684
        by(auto intro: map_default_in_finfun)
Andreas@48028
   685
      with f' f_Abs have "map_default b g' = map_default b ?g'" by simp
Andreas@48028
   686
      with fin' brang' fing' bnrang' show "g' = ?g'"
Andreas@48028
   687
        by(rule map_default_inject[OF disjI2[OF refl]])
Andreas@48028
   688
    qed
Andreas@48028
   689
    have dom: "dom (((\<lambda>a. Some (y a)) |` {a. y a \<noteq> b})(a' \<mapsto> b')) = insert a' (dom ((\<lambda>a. Some (y a)) |` {a. y a \<noteq> b}))"
Andreas@48028
   690
      by auto
Andreas@48028
   691
    show ?thesis
Andreas@48028
   692
    proof(cases "y a' = b")
Andreas@48028
   693
      case True
Andreas@48028
   694
      hence a'ndomg: "a' \<notin> dom ?g" by auto
Andreas@48028
   695
      from f y b'b True have yff: "y = map_default b (?g' |` dom ?g)"
Andreas@48028
   696
        by(auto simp add: restrict_map_def map_default_def intro!: ext)
Andreas@48028
   697
      hence f': "f = Abs_finfun (map_default b (?g' |` dom ?g))" using f by simp
Andreas@48028
   698
      interpret g'wf: comp_fun_commute "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
Andreas@48028
   699
      from upd_left_comm upd_left_comm fing
Andreas@48028
   700
      have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g) = Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)"
Andreas@48028
   701
        by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b True map_default_def)
Andreas@48028
   702
      thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric]
Andreas@48028
   703
        unfolding g' g[symmetric] gg g'wf.fold_insert[OF fing a'ndomg, of "cnst b", folded dom]
Andreas@48028
   704
        by -(rule arg_cong2[where f="upd a'"], simp_all add: map_default_def)
Andreas@48028
   705
    next
Andreas@48028
   706
      case False
Andreas@48028
   707
      hence "insert a' (dom ?g) = dom ?g" by auto
Andreas@48028
   708
      moreover {
Andreas@48028
   709
        let ?g'' = "?g(a' := None)"
Andreas@48028
   710
        let ?b'' = "map_default b ?g''"
Andreas@48028
   711
        from False have domg: "dom ?g = insert a' (dom ?g'')" by auto
Andreas@48028
   712
        from False have a'ndomg'': "a' \<notin> dom ?g''" by auto
Andreas@48028
   713
        have fing'': "finite (dom ?g'')" by(rule finite_subset[OF _ fing]) auto
Andreas@48028
   714
        have bnrang'': "b \<notin> ran ?g''" by(auto simp add: ran_def restrict_map_def)
Andreas@48028
   715
        interpret gwf: comp_fun_commute "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
Andreas@48028
   716
        interpret g'wf: comp_fun_commute "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
Andreas@48028
   717
        have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g''))) =
Andreas@48028
   718
              upd a' b' (upd a' (?b a') (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')))"
Andreas@48028
   719
          unfolding gwf.fold_insert[OF fing'' a'ndomg''] f ..
Andreas@48028
   720
        also have g''leg: "?g |` dom ?g'' \<subseteq>\<^sub>m ?g" by(auto simp add: map_le_def)
Andreas@48028
   721
        have "dom (?g |` dom ?g'') = dom ?g''" by auto
Andreas@48028
   722
        note map_default_update_twice[where d=b and f = "?g |` dom ?g''" and a=a' and d'="?b a'" and d''=b' and g="?g",
Andreas@48028
   723
                                     unfolded this, OF fing'' a'ndomg'' g''leg]
Andreas@48028
   724
        also have b': "b' = ?b' a'" by(auto simp add: map_default_def)
Andreas@48028
   725
        from upd_left_comm upd_left_comm fing''
Andreas@48028
   726
        have "Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'') = Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g'')"
Andreas@48028
   727
          by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b map_default_def)
Andreas@48028
   728
        with b' have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')) =
Andreas@48028
   729
                     upd a' (?b' a') (Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g''))" by simp
Andreas@48028
   730
        also note g'wf.fold_insert[OF fing'' a'ndomg'', symmetric]
Andreas@48028
   731
        finally have "upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g)) =
Andreas@48028
   732
                   Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)"
Andreas@48028
   733
          unfolding domg . }
Andreas@48028
   734
      ultimately have "Finite_Set.fold (\<lambda>a. upd a (?b' a)) (cnst b) (insert a' (dom ?g)) =
Andreas@48028
   735
                    upd a' b' (Finite_Set.fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))" by simp
Andreas@48028
   736
      thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric] g[symmetric] g' dom[symmetric]
Andreas@48028
   737
        using b'b gg by(simp add: map_default_insert)
Andreas@48028
   738
    qed
Andreas@48028
   739
  qed
Andreas@48028
   740
qed
Andreas@48028
   741
Andreas@48028
   742
declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
Andreas@48028
   743
Andreas@48028
   744
end
Andreas@48028
   745
Andreas@48028
   746
locale finfun_rec_wf = finfun_rec_wf_aux + 
Andreas@48028
   747
  assumes const_update_all:
Andreas@48028
   748
  "finite (UNIV :: 'a set) \<Longrightarrow> Finite_Set.fold (\<lambda>a. upd a b') (cnst b) (UNIV :: 'a set) = cnst b'"
Andreas@48028
   749
begin
Andreas@48028
   750
Andreas@48028
   751
declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
Andreas@48028
   752
Andreas@48028
   753
lemma finfun_rec_const [simp]:
Andreas@48028
   754
  "finfun_rec cnst upd (\<lambda>\<^isup>f c) = cnst c"
Andreas@48028
   755
proof(cases "finite (UNIV :: 'a set)")
Andreas@48028
   756
  case False
Andreas@48028
   757
  hence "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = c" by(simp add: finfun_default_const)
Andreas@48028
   758
  moreover have "(THE g :: 'a \<rightharpoonup> 'b. (\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g) = empty"
Andreas@48028
   759
  proof (rule the_equality)
Andreas@48028
   760
    show "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c empty) \<and> finite (dom empty) \<and> c \<notin> ran empty"
Andreas@48028
   761
      by(auto simp add: finfun_const_def)
Andreas@48028
   762
  next
Andreas@48028
   763
    fix g :: "'a \<rightharpoonup> 'b"
Andreas@48028
   764
    assume "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g"
Andreas@48028
   765
    hence g: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c g)" and fin: "finite (dom g)" and ran: "c \<notin> ran g" by blast+
Andreas@48028
   766
    from g map_default_in_finfun[OF fin, of c] have "map_default c g = (\<lambda>a. c)"
Andreas@48028
   767
      by(simp add: finfun_const_def)
Andreas@48028
   768
    moreover have "map_default c empty = (\<lambda>a. c)" by simp
Andreas@48028
   769
    ultimately show "g = empty" by-(rule map_default_inject[OF disjI2[OF refl] fin ran], auto)
Andreas@48028
   770
  qed
Andreas@48028
   771
  ultimately show ?thesis by(simp add: finfun_rec_def)
Andreas@48028
   772
next
Andreas@48028
   773
  case True
Andreas@48028
   774
  hence default: "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = undefined" by(simp add: finfun_default_const)
Andreas@48028
   775
  let ?the = "\<lambda>g :: 'a \<rightharpoonup> 'b. (\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g) \<and> finite (dom g) \<and> undefined \<notin> ran g"
Andreas@48028
   776
  show ?thesis
Andreas@48028
   777
  proof(cases "c = undefined")
Andreas@48028
   778
    case True
Andreas@48028
   779
    have the: "The ?the = empty"
Andreas@48028
   780
    proof (rule the_equality)
Andreas@48028
   781
      from True show "?the empty" by(auto simp add: finfun_const_def)
Andreas@48028
   782
    next
Andreas@48028
   783
      fix g'
Andreas@48028
   784
      assume "?the g'"
Andreas@48028
   785
      hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g')"
Andreas@48028
   786
        and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
Andreas@48028
   787
      from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
Andreas@48028
   788
      with fg have "map_default undefined g' = (\<lambda>a. c)"
Andreas@48028
   789
        by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
Andreas@48028
   790
      with True show "g' = empty"
Andreas@48028
   791
        by -(rule map_default_inject(2)[OF _ fin g], auto)
Andreas@48028
   792
    qed
Andreas@48028
   793
    show ?thesis unfolding finfun_rec_def using `finite UNIV` True
Andreas@48028
   794
      unfolding Let_def the default by(simp)
Andreas@48028
   795
  next
Andreas@48028
   796
    case False
Andreas@48028
   797
    have the: "The ?the = (\<lambda>a :: 'a. Some c)"
Andreas@48028
   798
    proof (rule the_equality)
Andreas@48028
   799
      from False True show "?the (\<lambda>a :: 'a. Some c)"
Andreas@48028
   800
        by(auto simp add: map_default_def [abs_def] finfun_const_def dom_def ran_def)
Andreas@48028
   801
    next
Andreas@48028
   802
      fix g' :: "'a \<rightharpoonup> 'b"
Andreas@48028
   803
      assume "?the g'"
Andreas@48028
   804
      hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default undefined g')"
Andreas@48028
   805
        and fin: "finite (dom g')" and g: "undefined \<notin> ran g'" by simp_all
Andreas@48028
   806
      from fin have "map_default undefined g' \<in> finfun" by(rule map_default_in_finfun)
Andreas@48028
   807
      with fg have "map_default undefined g' = (\<lambda>a. c)"
Andreas@48028
   808
        by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
Andreas@48028
   809
      with True False show "g' = (\<lambda>a::'a. Some c)"
Andreas@48028
   810
        by - (rule map_default_inject(2)[OF _ fin g],
Andreas@48028
   811
          auto simp add: dom_def ran_def map_default_def [abs_def])
Andreas@48028
   812
    qed
Andreas@48028
   813
    show ?thesis unfolding finfun_rec_def using True False
Andreas@48028
   814
      unfolding Let_def the default by(simp add: dom_def map_default_def const_update_all)
Andreas@48028
   815
  qed
Andreas@48028
   816
qed
Andreas@48028
   817
Andreas@48028
   818
declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
Andreas@48028
   819
Andreas@48028
   820
end
Andreas@48028
   821
Andreas@48028
   822
subsection {* Weak induction rule and case analysis for FinFuns *}
Andreas@48028
   823
Andreas@48028
   824
declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
Andreas@48028
   825
Andreas@48028
   826
lemma finfun_weak_induct [consumes 0, case_names const update]:
Andreas@48028
   827
  assumes const: "\<And>b. P (\<lambda>\<^isup>f b)"
Andreas@48028
   828
  and update: "\<And>f a b. P f \<Longrightarrow> P (f(\<^sup>f a := b))"
Andreas@48028
   829
  shows "P x"
Andreas@48028
   830
proof(induct x rule: Abs_finfun_induct)
Andreas@48028
   831
  case (Abs_finfun y)
Andreas@48028
   832
  then obtain b where "finite {a. y a \<noteq> b}" unfolding finfun_def by blast
Andreas@48028
   833
  thus ?case using `y \<in> finfun`
Andreas@48028
   834
  proof(induct "{a. y a \<noteq> b}" arbitrary: y rule: finite_induct)
Andreas@48028
   835
    case empty
Andreas@48028
   836
    hence "\<And>a. y a = b" by blast
Andreas@48028
   837
    hence "y = (\<lambda>a. b)" by(auto intro: ext)
Andreas@48028
   838
    hence "Abs_finfun y = finfun_const b" unfolding finfun_const_def by simp
Andreas@48028
   839
    thus ?case by(simp add: const)
Andreas@48028
   840
  next
Andreas@48028
   841
    case (insert a A)
Andreas@48028
   842
    note IH = `\<And>y. \<lbrakk> A = {a. y a \<noteq> b}; y \<in> finfun  \<rbrakk> \<Longrightarrow> P (Abs_finfun y)`
Andreas@48028
   843
    note y = `y \<in> finfun`
Andreas@48028
   844
    with `insert a A = {a. y a \<noteq> b}` `a \<notin> A`
Andreas@48028
   845
    have "A = {a'. (y(a := b)) a' \<noteq> b}" "y(a := b) \<in> finfun" by auto
Andreas@48028
   846
    from IH[OF this] have "P (finfun_update (Abs_finfun (y(a := b))) a (y a))" by(rule update)
Andreas@48028
   847
    thus ?case using y unfolding finfun_update_def by simp
Andreas@48028
   848
  qed
Andreas@48028
   849
qed
Andreas@48028
   850
Andreas@48028
   851
declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
Andreas@48028
   852
Andreas@48028
   853
lemma finfun_exhaust_disj: "(\<exists>b. x = finfun_const b) \<or> (\<exists>f a b. x = finfun_update f a b)"
Andreas@48028
   854
by(induct x rule: finfun_weak_induct) blast+
Andreas@48028
   855
Andreas@48028
   856
lemma finfun_exhaust:
Andreas@48028
   857
  obtains b where "x = (\<lambda>\<^isup>f b)"
Andreas@48028
   858
        | f a b where "x = f(\<^sup>f a := b)"
Andreas@48028
   859
by(atomize_elim)(rule finfun_exhaust_disj)
Andreas@48028
   860
Andreas@48028
   861
lemma finfun_rec_unique:
Andreas@48028
   862
  fixes f :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'c"
Andreas@48028
   863
  assumes c: "\<And>c. f (\<lambda>\<^isup>f c) = cnst c"
Andreas@48028
   864
  and u: "\<And>g a b. f (g(\<^sup>f a := b)) = upd g a b (f g)"
Andreas@48028
   865
  and c': "\<And>c. f' (\<lambda>\<^isup>f c) = cnst c"
Andreas@48028
   866
  and u': "\<And>g a b. f' (g(\<^sup>f a := b)) = upd g a b (f' g)"
Andreas@48028
   867
  shows "f = f'"
Andreas@48028
   868
proof
Andreas@48028
   869
  fix g :: "'a \<Rightarrow>\<^isub>f 'b"
Andreas@48028
   870
  show "f g = f' g"
Andreas@48028
   871
    by(induct g rule: finfun_weak_induct)(auto simp add: c u c' u')
Andreas@48028
   872
qed
Andreas@48028
   873
Andreas@48028
   874
Andreas@48028
   875
subsection {* Function application *}
Andreas@48028
   876
Andreas@48028
   877
definition finfun_apply :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b" ("_\<^sub>f" [1000] 1000)
Andreas@48028
   878
where [code del]: "finfun_apply = (\<lambda>f a. finfun_rec (\<lambda>b. b) (\<lambda>a' b c. if (a = a') then b else c) f)"
Andreas@48028
   879
Andreas@48028
   880
interpretation finfun_apply_aux: finfun_rec_wf_aux "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
Andreas@48028
   881
by(unfold_locales) auto
Andreas@48028
   882
Andreas@48028
   883
interpretation finfun_apply: finfun_rec_wf "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
Andreas@48028
   884
proof(unfold_locales)
Andreas@48028
   885
  fix b' b :: 'a
Andreas@48028
   886
  assume fin: "finite (UNIV :: 'b set)"
Andreas@48028
   887
  { fix A :: "'b set"
Andreas@48028
   888
    interpret comp_fun_commute "\<lambda>a'. If (a = a') b'" by(rule finfun_apply_aux.upd_left_comm)
Andreas@48028
   889
    from fin have "finite A" by(auto intro: finite_subset)
Andreas@48028
   890
    hence "Finite_Set.fold (\<lambda>a'. If (a = a') b') b A = (if a \<in> A then b' else b)"
Andreas@48028
   891
      by induct auto }
Andreas@48028
   892
  from this[of UNIV] show "Finite_Set.fold (\<lambda>a'. If (a = a') b') b UNIV = b'" by simp
Andreas@48028
   893
qed
Andreas@48028
   894
Andreas@48028
   895
lemma finfun_const_apply [simp, code]: "(\<lambda>\<^isup>f b)\<^sub>f a = b"
Andreas@48028
   896
by(simp add: finfun_apply_def)
Andreas@48028
   897
Andreas@48028
   898
lemma finfun_upd_apply: "f(\<^sup>fa := b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')"
Andreas@48028
   899
  and finfun_upd_apply_code [code]: "(finfun_update_code f a b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')"
Andreas@48028
   900
by(simp_all add: finfun_apply_def)
Andreas@48028
   901
Andreas@48028
   902
lemma finfun_upd_apply_same [simp]:
Andreas@48028
   903
  "f(\<^sup>fa := b)\<^sub>f a = b"
Andreas@48028
   904
by(simp add: finfun_upd_apply)
Andreas@48028
   905
Andreas@48028
   906
lemma finfun_upd_apply_other [simp]:
Andreas@48028
   907
  "a \<noteq> a' \<Longrightarrow> f(\<^sup>fa := b)\<^sub>f a' = f\<^sub>f a'"
Andreas@48028
   908
by(simp add: finfun_upd_apply)
Andreas@48028
   909
Andreas@48028
   910
declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
Andreas@48028
   911
Andreas@48028
   912
lemma finfun_apply_Rep_finfun:
Andreas@48028
   913
  "finfun_apply = Rep_finfun"
Andreas@48028
   914
proof(rule finfun_rec_unique)
Andreas@48028
   915
  fix c show "Rep_finfun (\<lambda>\<^isup>f c) = (\<lambda>a. c)" by(auto simp add: finfun_const_def)
Andreas@48028
   916
next
Andreas@48028
   917
  fix g a b show "Rep_finfun g(\<^sup>f a := b) = (\<lambda>c. if c = a then b else Rep_finfun g c)"
Andreas@48028
   918
    by(auto simp add: finfun_update_def fun_upd_finfun Abs_finfun_inverse Rep_finfun intro: ext)
Andreas@48028
   919
qed(auto intro: ext)
Andreas@48028
   920
Andreas@48028
   921
lemma finfun_ext: "(\<And>a. f\<^sub>f a = g\<^sub>f a) \<Longrightarrow> f = g"
Andreas@48028
   922
by(auto simp add: finfun_apply_Rep_finfun Rep_finfun_inject[symmetric] simp del: Rep_finfun_inject intro: ext)
Andreas@48028
   923
Andreas@48028
   924
declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
Andreas@48028
   925
Andreas@48028
   926
lemma expand_finfun_eq: "(f = g) = (f\<^sub>f = g\<^sub>f)"
Andreas@48028
   927
by(auto intro: finfun_ext)
Andreas@48028
   928
Andreas@48028
   929
lemma finfun_const_inject [simp]: "(\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b') \<equiv> b = b'"
Andreas@48028
   930
by(simp add: expand_finfun_eq fun_eq_iff)
Andreas@48028
   931
Andreas@48028
   932
lemma finfun_const_eq_update:
Andreas@48028
   933
  "((\<lambda>\<^isup>f b) = f(\<^sup>f a := b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f\<^sub>f a' = b))"
Andreas@48028
   934
by(auto simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
Andreas@48028
   935
Andreas@48028
   936
subsection {* Function composition *}
Andreas@48028
   937
Andreas@48028
   938
definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'a \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'b" (infixr "\<circ>\<^isub>f" 55)
Andreas@48028
   939
where [code del]: "g \<circ>\<^isub>f f  = finfun_rec (\<lambda>b. (\<lambda>\<^isup>f g b)) (\<lambda>a b c. c(\<^sup>f a := g b)) f"
Andreas@48028
   940
Andreas@48028
   941
interpretation finfun_comp_aux: finfun_rec_wf_aux "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))"
Andreas@48028
   942
by(unfold_locales)(auto simp add: finfun_upd_apply intro: finfun_ext)
Andreas@48028
   943
Andreas@48028
   944
interpretation finfun_comp: finfun_rec_wf "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))"
Andreas@48028
   945
proof
Andreas@48028
   946
  fix b' b :: 'a
Andreas@48028
   947
  assume fin: "finite (UNIV :: 'c set)"
Andreas@48028
   948
  { fix A :: "'c set"
Andreas@48028
   949
    from fin have "finite A" by(auto intro: finite_subset)
Andreas@48028
   950
    hence "Finite_Set.fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) A =
Andreas@48028
   951
      Abs_finfun (\<lambda>a. if a \<in> A then g b' else g b)"
Andreas@48028
   952
      by induct (simp_all add: finfun_const_def, auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite fun_eq_iff fin) }
Andreas@48028
   953
  from this[of UNIV] show "Finite_Set.fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) UNIV = (\<lambda>\<^isup>f g b')"
Andreas@48028
   954
    by(simp add: finfun_const_def)
Andreas@48028
   955
qed
Andreas@48028
   956
Andreas@48028
   957
lemma finfun_comp_const [simp, code]:
Andreas@48028
   958
  "g \<circ>\<^isub>f (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f g c)"
Andreas@48028
   959
by(simp add: finfun_comp_def)
Andreas@48028
   960
Andreas@48028
   961
lemma finfun_comp_update [simp]: "g \<circ>\<^isub>f (f(\<^sup>f a := b)) = (g \<circ>\<^isub>f f)(\<^sup>f a := g b)"
Andreas@48028
   962
  and finfun_comp_update_code [code]: "g \<circ>\<^isub>f (finfun_update_code f a b) = finfun_update_code (g \<circ>\<^isub>f f) a (g b)"
Andreas@48028
   963
by(simp_all add: finfun_comp_def)
Andreas@48028
   964
Andreas@48028
   965
lemma finfun_comp_apply [simp]:
Andreas@48028
   966
  "(g \<circ>\<^isub>f f)\<^sub>f = g \<circ> f\<^sub>f"
Andreas@48028
   967
by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply intro: ext)
Andreas@48028
   968
Andreas@48028
   969
lemma finfun_comp_comp_collapse [simp]: "f \<circ>\<^isub>f g \<circ>\<^isub>f h = (f o g) \<circ>\<^isub>f h"
Andreas@48028
   970
by(induct h rule: finfun_weak_induct) simp_all
Andreas@48028
   971
Andreas@48028
   972
lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>\<^isub>f f = (\<lambda>\<^isup>f c)"
Andreas@48028
   973
by(induct f rule: finfun_weak_induct)(auto intro: finfun_ext simp add: finfun_upd_apply)
Andreas@48028
   974
Andreas@48028
   975
lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>\<^isub>f f = f" "id \<circ>\<^isub>f f = f"
Andreas@48028
   976
by(induct f rule: finfun_weak_induct) auto
Andreas@48028
   977
Andreas@48028
   978
declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
Andreas@48028
   979
Andreas@48028
   980
lemma finfun_comp_conv_comp: "g \<circ>\<^isub>f f = Abs_finfun (g \<circ> finfun_apply f)"
Andreas@48028
   981
proof -
Andreas@48028
   982
  have "(\<lambda>f. g \<circ>\<^isub>f f) = (\<lambda>f. Abs_finfun (g \<circ> finfun_apply f))"
Andreas@48028
   983
  proof(rule finfun_rec_unique)
Andreas@48028
   984
    { fix c show "Abs_finfun (g \<circ> (\<lambda>\<^isup>f c)\<^sub>f) = (\<lambda>\<^isup>f g c)"
Andreas@48028
   985
        by(simp add: finfun_comp_def o_def)(simp add: finfun_const_def) }
Andreas@48028
   986
    { fix g' a b show "Abs_finfun (g \<circ> g'(\<^sup>f a := b)\<^sub>f) = (Abs_finfun (g \<circ> g'\<^sub>f))(\<^sup>f a := g b)"
Andreas@48028
   987
      proof -
Andreas@48028
   988
        obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
Andreas@48028
   989
        moreover hence "(g \<circ> g'\<^sub>f) \<in> finfun" by(simp add: finfun_apply_Rep_finfun finfun_left_compose)
Andreas@48028
   990
        moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto intro: ext)
Andreas@48028
   991
        ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def finfun_apply_Rep_finfun)
Andreas@48028
   992
      qed }
Andreas@48028
   993
  qed auto
Andreas@48028
   994
  thus ?thesis by(auto simp add: fun_eq_iff)
Andreas@48028
   995
qed
Andreas@48028
   996
Andreas@48028
   997
declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
Andreas@48028
   998
Andreas@48028
   999
definition finfun_comp2 :: "'b \<Rightarrow>\<^isub>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c" (infixr "\<^sub>f\<circ>" 55)
Andreas@48028
  1000
where [code del]: "finfun_comp2 g f = Abs_finfun (Rep_finfun g \<circ> f)"
Andreas@48028
  1001
Andreas@48028
  1002
declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
Andreas@48028
  1003
Andreas@48028
  1004
lemma finfun_comp2_const [code, simp]: "finfun_comp2 (\<lambda>\<^isup>f c) f = (\<lambda>\<^isup>f c)"
Andreas@48028
  1005
by(simp add: finfun_comp2_def finfun_const_def comp_def)
Andreas@48028
  1006
Andreas@48028
  1007
lemma finfun_comp2_update:
Andreas@48028
  1008
  assumes inj: "inj f"
Andreas@48028
  1009
  shows "finfun_comp2 (g(\<^sup>f b := c)) f = (if b \<in> range f then (finfun_comp2 g f)(\<^sup>f inv f b := c) else finfun_comp2 g f)"
Andreas@48028
  1010
proof(cases "b \<in> range f")
Andreas@48028
  1011
  case True
Andreas@48028
  1012
  from inj have "\<And>x. (Rep_finfun g)(f x := c) \<circ> f = (Rep_finfun g \<circ> f)(x := c)" by(auto intro!: ext dest: injD)
Andreas@48028
  1013
  with inj True show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def finfun_right_compose)
Andreas@48028
  1014
next
Andreas@48028
  1015
  case False
Andreas@48028
  1016
  hence "(Rep_finfun g)(b := c) \<circ> f = Rep_finfun g \<circ> f" by(auto simp add: fun_eq_iff)
Andreas@48028
  1017
  with False show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def)
Andreas@48028
  1018
qed
Andreas@48028
  1019
Andreas@48028
  1020
declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
Andreas@48028
  1021
Andreas@48028
  1022
Andreas@48028
  1023
Andreas@48028
  1024
subsection {* Universal quantification *}
Andreas@48028
  1025
Andreas@48028
  1026
definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
Andreas@48028
  1027
where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P\<^sub>f a"
Andreas@48028
  1028
Andreas@48028
  1029
lemma finfun_All_except_const: "finfun_All_except A (\<lambda>\<^isup>f b) \<longleftrightarrow> b \<or> set A = UNIV"
Andreas@48028
  1030
by(auto simp add: finfun_All_except_def)
Andreas@48028
  1031
Andreas@48028
  1032
lemma finfun_All_except_const_finfun_UNIV_code [code]:
Andreas@48028
  1033
  "finfun_All_except A (\<lambda>\<^isup>f b) = (b \<or> is_list_UNIV A)"
Andreas@48028
  1034
by(simp add: finfun_All_except_const is_list_UNIV_iff)
Andreas@48028
  1035
Andreas@48028
  1036
lemma finfun_All_except_update: 
Andreas@48028
  1037
  "finfun_All_except A f(\<^sup>f a := b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
Andreas@48028
  1038
by(fastforce simp add: finfun_All_except_def finfun_upd_apply)
Andreas@48028
  1039
Andreas@48028
  1040
lemma finfun_All_except_update_code [code]:
Andreas@48028
  1041
  fixes a :: "'a :: card_UNIV"
Andreas@48028
  1042
  shows "finfun_All_except A (finfun_update_code f a b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
Andreas@48028
  1043
by(simp add: finfun_All_except_update)
Andreas@48028
  1044
Andreas@48028
  1045
definition finfun_All :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
Andreas@48028
  1046
where "finfun_All = finfun_All_except []"
Andreas@48028
  1047
Andreas@48028
  1048
lemma finfun_All_const [simp]: "finfun_All (\<lambda>\<^isup>f b) = b"
Andreas@48028
  1049
by(simp add: finfun_All_def finfun_All_except_def)
Andreas@48028
  1050
Andreas@48028
  1051
lemma finfun_All_update: "finfun_All f(\<^sup>f a := b) = (b \<and> finfun_All_except [a] f)"
Andreas@48028
  1052
by(simp add: finfun_All_def finfun_All_except_update)
Andreas@48028
  1053
Andreas@48028
  1054
lemma finfun_All_All: "finfun_All P = All P\<^sub>f"
Andreas@48028
  1055
by(simp add: finfun_All_def finfun_All_except_def)
Andreas@48028
  1056
Andreas@48028
  1057
Andreas@48028
  1058
definition finfun_Ex :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
Andreas@48028
  1059
where "finfun_Ex P = Not (finfun_All (Not \<circ>\<^isub>f P))"
Andreas@48028
  1060
Andreas@48028
  1061
lemma finfun_Ex_Ex: "finfun_Ex P = Ex P\<^sub>f"
Andreas@48028
  1062
unfolding finfun_Ex_def finfun_All_All by simp
Andreas@48028
  1063
Andreas@48028
  1064
lemma finfun_Ex_const [simp]: "finfun_Ex (\<lambda>\<^isup>f b) = b"
Andreas@48028
  1065
by(simp add: finfun_Ex_def)
Andreas@48028
  1066
Andreas@48028
  1067
Andreas@48028
  1068
subsection {* A diagonal operator for FinFuns *}
Andreas@48028
  1069
Andreas@48028
  1070
definition finfun_Diag :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c \<Rightarrow> 'a \<Rightarrow>\<^isub>f ('b \<times> 'c)" ("(1'(_,/ _')\<^sup>f)" [0, 0] 1000)
Andreas@48028
  1071
where [code del]: "finfun_Diag f g = finfun_rec (\<lambda>b. Pair b \<circ>\<^isub>f g) (\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))) f"
Andreas@48028
  1072
Andreas@48028
  1073
interpretation finfun_Diag_aux: finfun_rec_wf_aux "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))"
Andreas@48028
  1074
by(unfold_locales)(simp_all add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
Andreas@48028
  1075
Andreas@48028
  1076
interpretation finfun_Diag: finfun_rec_wf "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))"
Andreas@48028
  1077
proof
Andreas@48028
  1078
  fix b' b :: 'a
Andreas@48028
  1079
  assume fin: "finite (UNIV :: 'c set)"
Andreas@48028
  1080
  { fix A :: "'c set"
Andreas@48028
  1081
    interpret comp_fun_commute "\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))" by(rule finfun_Diag_aux.upd_left_comm)
Andreas@48028
  1082
    from fin have "finite A" by(auto intro: finite_subset)
Andreas@48028
  1083
    hence "Finite_Set.fold (\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))) (Pair b \<circ>\<^isub>f g) A =
Andreas@48028
  1084
      Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g\<^sub>f a))"
Andreas@48028
  1085
      by(induct)(simp_all add: finfun_const_def finfun_comp_conv_comp o_def,
Andreas@48028
  1086
                 auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite fun_eq_iff fin) }
Andreas@48028
  1087
  from this[of UNIV] show "Finite_Set.fold (\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))) (Pair b \<circ>\<^isub>f g) UNIV = Pair b' \<circ>\<^isub>f g"
Andreas@48028
  1088
    by(simp add: finfun_const_def finfun_comp_conv_comp o_def)
Andreas@48028
  1089
qed
Andreas@48028
  1090
Andreas@48028
  1091
lemma finfun_Diag_const1: "(\<lambda>\<^isup>f b, g)\<^sup>f = Pair b \<circ>\<^isub>f g"
Andreas@48028
  1092
by(simp add: finfun_Diag_def)
Andreas@48028
  1093
Andreas@48028
  1094
text {*
Andreas@48028
  1095
  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 @{text "\<circ>\<^isub>f"}.
Andreas@48028
  1096
*}
Andreas@48028
  1097
Andreas@48028
  1098
lemma finfun_Diag_const_code [code]:
Andreas@48028
  1099
  "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
Andreas@48028
  1100
  "(\<lambda>\<^isup>f b, g(\<^sup>fc a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>fc a := (b, c))"
Andreas@48028
  1101
by(simp_all add: finfun_Diag_const1)
Andreas@48028
  1102
Andreas@48028
  1103
lemma finfun_Diag_update1: "(f(\<^sup>f a := b), g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))"
Andreas@48028
  1104
  and finfun_Diag_update1_code [code]: "(finfun_update_code f a b, g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))"
Andreas@48028
  1105
by(simp_all add: finfun_Diag_def)
Andreas@48028
  1106
Andreas@48028
  1107
lemma finfun_Diag_const2: "(f, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>\<^isub>f f"
Andreas@48028
  1108
by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
Andreas@48028
  1109
Andreas@48028
  1110
lemma finfun_Diag_update2: "(f, g(\<^sup>f a := c))\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (f\<^sub>f a, c))"
Andreas@48028
  1111
by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
Andreas@48028
  1112
Andreas@48028
  1113
lemma finfun_Diag_const_const [simp]: "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
Andreas@48028
  1114
by(simp add: finfun_Diag_const1)
Andreas@48028
  1115
Andreas@48028
  1116
lemma finfun_Diag_const_update:
Andreas@48028
  1117
  "(\<lambda>\<^isup>f b, g(\<^sup>f a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>f a := (b, c))"
Andreas@48028
  1118
by(simp add: finfun_Diag_const1)
Andreas@48028
  1119
Andreas@48028
  1120
lemma finfun_Diag_update_const:
Andreas@48028
  1121
  "(f(\<^sup>f a := b), \<lambda>\<^isup>f c)\<^sup>f = (f, \<lambda>\<^isup>f c)\<^sup>f(\<^sup>f a := (b, c))"
Andreas@48028
  1122
by(simp add: finfun_Diag_def)
Andreas@48028
  1123
Andreas@48028
  1124
lemma finfun_Diag_update_update:
Andreas@48028
  1125
  "(f(\<^sup>f a := b), g(\<^sup>f a' := c))\<^sup>f = (if a = a' then (f, g)\<^sup>f(\<^sup>f a := (b, c)) else (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))(\<^sup>f a' := (f\<^sub>f a', c)))"
Andreas@48028
  1126
by(auto simp add: finfun_Diag_update1 finfun_Diag_update2)
Andreas@48028
  1127
Andreas@48028
  1128
lemma finfun_Diag_apply [simp]: "(f, g)\<^sup>f\<^sub>f = (\<lambda>x. (f\<^sub>f x, g\<^sub>f x))"
Andreas@48028
  1129
by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply intro: ext)
Andreas@48028
  1130
Andreas@48028
  1131
declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
Andreas@48028
  1132
Andreas@48028
  1133
lemma finfun_Diag_conv_Abs_finfun:
Andreas@48028
  1134
  "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (Rep_finfun f x, Rep_finfun g x)))"
Andreas@48028
  1135
proof -
Andreas@48028
  1136
  have "(\<lambda>f :: 'a \<Rightarrow>\<^isub>f 'b. (f, g)\<^sup>f) = (\<lambda>f. Abs_finfun ((\<lambda>x. (Rep_finfun f x, Rep_finfun g x))))"
Andreas@48028
  1137
  proof(rule finfun_rec_unique)
Andreas@48028
  1138
    { fix c show "Abs_finfun (\<lambda>x. (Rep_finfun (\<lambda>\<^isup>f c) x, Rep_finfun g x)) = Pair c \<circ>\<^isub>f g"
Andreas@48028
  1139
        by(simp add: finfun_comp_conv_comp finfun_apply_Rep_finfun o_def finfun_const_def) }
Andreas@48028
  1140
    { fix g' a b
Andreas@48028
  1141
      show "Abs_finfun (\<lambda>x. (Rep_finfun g'(\<^sup>f a := b) x, Rep_finfun g x)) =
Andreas@48028
  1142
            (Abs_finfun (\<lambda>x. (Rep_finfun g' x, Rep_finfun g x)))(\<^sup>f a := (b, g\<^sub>f a))"
Andreas@48028
  1143
        by(auto simp add: finfun_update_def fun_eq_iff finfun_apply_Rep_finfun simp del: fun_upd_apply) simp }
Andreas@48028
  1144
  qed(simp_all add: finfun_Diag_const1 finfun_Diag_update1)
Andreas@48028
  1145
  thus ?thesis by(auto simp add: fun_eq_iff)
Andreas@48028
  1146
qed
Andreas@48028
  1147
Andreas@48028
  1148
declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
Andreas@48028
  1149
Andreas@48028
  1150
lemma finfun_Diag_eq: "(f, g)\<^sup>f = (f', g')\<^sup>f \<longleftrightarrow> f = f' \<and> g = g'"
Andreas@48028
  1151
by(auto simp add: expand_finfun_eq fun_eq_iff)
Andreas@48028
  1152
Andreas@48028
  1153
definition finfun_fst :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
Andreas@48028
  1154
where [code]: "finfun_fst f = fst \<circ>\<^isub>f f"
Andreas@48028
  1155
Andreas@48028
  1156
lemma finfun_fst_const: "finfun_fst (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f fst bc)"
Andreas@48028
  1157
by(simp add: finfun_fst_def)
Andreas@48028
  1158
Andreas@48028
  1159
lemma finfun_fst_update: "finfun_fst (f(\<^sup>f a := bc)) = (finfun_fst f)(\<^sup>f a := fst bc)"
Andreas@48028
  1160
  and finfun_fst_update_code: "finfun_fst (finfun_update_code f a bc) = (finfun_fst f)(\<^sup>f a := fst bc)"
Andreas@48028
  1161
by(simp_all add: finfun_fst_def)
Andreas@48028
  1162
Andreas@48028
  1163
lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>\<^isub>f g) = (fst \<circ> f) \<circ>\<^isub>f g"
Andreas@48028
  1164
by(simp add: finfun_fst_def)
Andreas@48028
  1165
Andreas@48028
  1166
lemma finfun_fst_conv [simp]: "finfun_fst (f, g)\<^sup>f = f"
Andreas@48028
  1167
by(induct f rule: finfun_weak_induct)(simp_all add: finfun_Diag_const1 finfun_fst_comp_conv o_def finfun_Diag_update1 finfun_fst_update)
Andreas@48028
  1168
Andreas@48028
  1169
lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst o Rep_finfun f))"
Andreas@48028
  1170
by(simp add: finfun_fst_def [abs_def] finfun_comp_conv_comp finfun_apply_Rep_finfun)
Andreas@48028
  1171
Andreas@48028
  1172
Andreas@48028
  1173
definition finfun_snd :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c"
Andreas@48028
  1174
where [code]: "finfun_snd f = snd \<circ>\<^isub>f f"
Andreas@48028
  1175
Andreas@48028
  1176
lemma finfun_snd_const: "finfun_snd (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f snd bc)"
Andreas@48028
  1177
by(simp add: finfun_snd_def)
Andreas@48028
  1178
Andreas@48028
  1179
lemma finfun_snd_update: "finfun_snd (f(\<^sup>f a := bc)) = (finfun_snd f)(\<^sup>f a := snd bc)"
Andreas@48028
  1180
  and finfun_snd_update_code [code]: "finfun_snd (finfun_update_code f a bc) = (finfun_snd f)(\<^sup>f a := snd bc)"
Andreas@48028
  1181
by(simp_all add: finfun_snd_def)
Andreas@48028
  1182
Andreas@48028
  1183
lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>\<^isub>f g) = (snd \<circ> f) \<circ>\<^isub>f g"
Andreas@48028
  1184
by(simp add: finfun_snd_def)
Andreas@48028
  1185
Andreas@48028
  1186
lemma finfun_snd_conv [simp]: "finfun_snd (f, g)\<^sup>f = g"
Andreas@48028
  1187
apply(induct f rule: finfun_weak_induct)
Andreas@48028
  1188
apply(auto simp add: finfun_Diag_const1 finfun_snd_comp_conv o_def finfun_Diag_update1 finfun_snd_update finfun_upd_apply intro: finfun_ext)
Andreas@48028
  1189
done
Andreas@48028
  1190
Andreas@48028
  1191
lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd o Rep_finfun f))"
Andreas@48028
  1192
by(simp add: finfun_snd_def [abs_def] finfun_comp_conv_comp finfun_apply_Rep_finfun)
Andreas@48028
  1193
Andreas@48028
  1194
lemma finfun_Diag_collapse [simp]: "(finfun_fst f, finfun_snd f)\<^sup>f = f"
Andreas@48028
  1195
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)
Andreas@48028
  1196
Andreas@48028
  1197
subsection {* Currying for FinFuns *}
Andreas@48028
  1198
Andreas@48028
  1199
definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b \<Rightarrow>\<^isub>f 'c"
Andreas@48028
  1200
where [code del]: "finfun_curry = finfun_rec (finfun_const \<circ> finfun_const) (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c)))"
Andreas@48028
  1201
Andreas@48028
  1202
interpretation finfun_curry_aux: finfun_rec_wf_aux "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))"
Andreas@48028
  1203
apply(unfold_locales)
Andreas@48028
  1204
apply(auto simp add: split_def finfun_update_twist finfun_upd_apply split_paired_all finfun_update_const_same)
Andreas@48028
  1205
done
Andreas@48028
  1206
Andreas@48028
  1207
declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
Andreas@48028
  1208
Andreas@48028
  1209
interpretation finfun_curry: finfun_rec_wf "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))"
Andreas@48028
  1210
proof(unfold_locales)
Andreas@48028
  1211
  fix b' b :: 'b
Andreas@48028
  1212
  assume fin: "finite (UNIV :: ('c \<times> 'a) set)"
Andreas@48028
  1213
  hence fin1: "finite (UNIV :: 'c set)" and fin2: "finite (UNIV :: 'a set)"
Andreas@48028
  1214
    unfolding UNIV_Times_UNIV[symmetric]
Andreas@48028
  1215
    by(fastforce dest: finite_cartesian_productD1 finite_cartesian_productD2)+
Andreas@48028
  1216
  note [simp] = Abs_finfun_inverse_finite[OF fin] Abs_finfun_inverse_finite[OF fin1] Abs_finfun_inverse_finite[OF fin2]
Andreas@48028
  1217
  { fix A :: "('c \<times> 'a) set"
Andreas@48028
  1218
    interpret comp_fun_commute "\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b'"
Andreas@48028
  1219
      by(rule finfun_curry_aux.upd_left_comm)
Andreas@48028
  1220
    from fin have "finite A" by(auto intro: finite_subset)
Andreas@48028
  1221
    hence "Finite_Set.fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b') ((finfun_const \<circ> finfun_const) b) A = Abs_finfun (\<lambda>a. Abs_finfun (\<lambda>b''. if (a, b'') \<in> A then b' else b))"
Andreas@48028
  1222
      by induct (simp_all, auto simp add: finfun_update_def finfun_const_def split_def finfun_apply_Rep_finfun intro!: arg_cong[where f="Abs_finfun"] ext) }
Andreas@48028
  1223
  from this[of UNIV]
Andreas@48028
  1224
  show "Finite_Set.fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b') ((finfun_const \<circ> finfun_const) b) UNIV = (finfun_const \<circ> finfun_const) b'"
Andreas@48028
  1225
    by(simp add: finfun_const_def)
Andreas@48028
  1226
qed
Andreas@48028
  1227
Andreas@48028
  1228
declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
Andreas@48028
  1229
Andreas@48028
  1230
lemma finfun_curry_const [simp, code]: "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
Andreas@48028
  1231
by(simp add: finfun_curry_def)
Andreas@48028
  1232
Andreas@48028
  1233
lemma finfun_curry_update [simp]:
Andreas@48028
  1234
  "finfun_curry (f(\<^sup>f (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
Andreas@48028
  1235
  and finfun_curry_update_code [code]:
Andreas@48028
  1236
  "finfun_curry (f(\<^sup>fc (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
Andreas@48028
  1237
by(simp_all add: finfun_curry_def)
Andreas@48028
  1238
Andreas@48028
  1239
declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
Andreas@48028
  1240
Andreas@48028
  1241
lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun"
Andreas@48028
  1242
  shows "(\<lambda>a. Abs_finfun (curry f a)) \<in> finfun"
Andreas@48028
  1243
proof -
Andreas@48028
  1244
  from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
Andreas@48028
  1245
  have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
Andreas@48028
  1246
  hence "{a. curry f a \<noteq> (\<lambda>x. c)} = fst ` {ab. f ab \<noteq> c}"
Andreas@48028
  1247
    by(auto simp add: curry_def fun_eq_iff)
Andreas@48028
  1248
  with fin c have "finite {a.  Abs_finfun (curry f a) \<noteq> (\<lambda>\<^isup>f c)}"
Andreas@48028
  1249
    by(simp add: finfun_const_def finfun_curry)
Andreas@48028
  1250
  thus ?thesis unfolding finfun_def by auto
Andreas@48028
  1251
qed
Andreas@48028
  1252
Andreas@48028
  1253
lemma finfun_curry_conv_curry:
Andreas@48028
  1254
  fixes f :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c"
Andreas@48028
  1255
  shows "finfun_curry f = Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a))"
Andreas@48028
  1256
proof -
Andreas@48028
  1257
  have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>\<^isub>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a)))"
Andreas@48028
  1258
  proof(rule finfun_rec_unique)
Andreas@48028
  1259
    { fix c show "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" by simp }
Andreas@48028
  1260
    { fix f a c show "finfun_curry (f(\<^sup>f a := c)) = (finfun_curry f)(\<^sup>f fst a := ((finfun_curry f)\<^sub>f (fst a))(\<^sup>f snd a := c))"
Andreas@48028
  1261
        by(cases a) simp }
Andreas@48028
  1262
    { fix c show "Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun (\<lambda>\<^isup>f c)) a)) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
Andreas@48028
  1263
        by(simp add: finfun_curry_def finfun_const_def curry_def) }
Andreas@48028
  1264
    { fix g a b
Andreas@48028
  1265
      show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (Rep_finfun g(\<^sup>f a := b)) aa)) =
Andreas@48028
  1266
       (Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))(\<^sup>f
Andreas@48028
  1267
       fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))\<^sub>f (fst a))(\<^sup>f snd a := b))"
Andreas@48028
  1268
        by(cases a)(auto intro!: ext arg_cong[where f=Abs_finfun] simp add: finfun_curry_def finfun_update_def finfun_apply_Rep_finfun finfun_curry finfun_Abs_finfun_curry) }
Andreas@48028
  1269
  qed
Andreas@48028
  1270
  thus ?thesis by(auto simp add: fun_eq_iff)
Andreas@48028
  1271
qed
Andreas@48028
  1272
Andreas@48028
  1273
subsection {* Executable equality for FinFuns *}
Andreas@48028
  1274
Andreas@48028
  1275
lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
Andreas@48028
  1276
by(simp add: expand_finfun_eq fun_eq_iff finfun_All_All o_def)
Andreas@48028
  1277
Andreas@48028
  1278
instantiation finfun :: ("{card_UNIV,equal}",equal) equal begin
Andreas@48028
  1279
definition eq_finfun_def [code]: "HOL.equal f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
Andreas@48028
  1280
instance by(intro_classes)(simp add: eq_finfun_All_ext eq_finfun_def)
Andreas@48028
  1281
end
Andreas@48028
  1282
Andreas@48028
  1283
lemma [code nbe]:
Andreas@48028
  1284
  "HOL.equal (f :: _ \<Rightarrow>\<^isub>f _) f \<longleftrightarrow> True"
Andreas@48028
  1285
  by (fact equal_refl)
Andreas@48028
  1286
Andreas@48028
  1287
subsection {* An operator that explicitly removes all redundant updates in the generated representations *}
Andreas@48028
  1288
Andreas@48028
  1289
definition finfun_clearjunk :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
Andreas@48028
  1290
where [simp, code del]: "finfun_clearjunk = id"
Andreas@48028
  1291
Andreas@48028
  1292
lemma finfun_clearjunk_const [code]: "finfun_clearjunk (\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b)"
Andreas@48028
  1293
by simp
Andreas@48028
  1294
Andreas@48028
  1295
lemma finfun_clearjunk_update [code]: "finfun_clearjunk (finfun_update_code f a b) = f(\<^sup>f a := b)"
Andreas@48028
  1296
by simp
Andreas@48028
  1297
Andreas@48028
  1298
subsection {* The domain of a FinFun as a FinFun *}
Andreas@48028
  1299
Andreas@48028
  1300
definition finfun_dom :: "('a \<Rightarrow>\<^isub>f 'b) \<Rightarrow> ('a \<Rightarrow>\<^isub>f bool)"
Andreas@48028
  1301
where [code del]: "finfun_dom f = Abs_finfun (\<lambda>a. f\<^sub>f a \<noteq> finfun_default f)"
Andreas@48028
  1302
Andreas@48028
  1303
lemma finfun_dom_const:
Andreas@48028
  1304
  "finfun_dom ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = (\<lambda>\<^isup>f finite (UNIV :: 'a set) \<and> c \<noteq> undefined)"
Andreas@48028
  1305
unfolding finfun_dom_def finfun_default_const
Andreas@48028
  1306
by(auto)(simp_all add: finfun_const_def)
Andreas@48028
  1307
Andreas@48028
  1308
text {*
Andreas@48028
  1309
  @{term "finfun_dom" } raises an exception when called on a FinFun whose domain is a finite type. 
Andreas@48028
  1310
  For such FinFuns, the default value (and as such the domain) is undefined.
Andreas@48028
  1311
*}
Andreas@48028
  1312
Andreas@48028
  1313
lemma finfun_dom_const_code [code]:
Andreas@48028
  1314
  "finfun_dom ((\<lambda>\<^isup>f c) :: ('a :: card_UNIV) \<Rightarrow>\<^isub>f 'b) = 
Andreas@48028
  1315
   (if card_UNIV (TYPE('a)) = 0 then (\<lambda>\<^isup>f False) else FinFun.code_abort (\<lambda>_. finfun_dom (\<lambda>\<^isup>f c)))"
Andreas@48028
  1316
unfolding card_UNIV_eq_0_infinite_UNIV
Andreas@48028
  1317
by(simp add: finfun_dom_const)
Andreas@48028
  1318
Andreas@48028
  1319
lemma finfun_dom_finfunI: "(\<lambda>a. f\<^sub>f a \<noteq> finfun_default f) \<in> finfun"
Andreas@48028
  1320
using finite_finfun_default[of f]
Andreas@48028
  1321
by(simp add: finfun_def finfun_apply_Rep_finfun exI[where x=False])
Andreas@48028
  1322
Andreas@48028
  1323
lemma finfun_dom_update [simp]:
Andreas@48028
  1324
  "finfun_dom (f(\<^sup>f a := b)) = (finfun_dom f)(\<^sup>f a := (b \<noteq> finfun_default f))"
Andreas@48028
  1325
unfolding finfun_dom_def finfun_update_def
Andreas@48028
  1326
apply(simp add: finfun_default_update_const finfun_upd_apply finfun_dom_finfunI)
Andreas@48028
  1327
apply(fold finfun_update.rep_eq)
Andreas@48028
  1328
apply(simp add: finfun_upd_apply fun_eq_iff finfun_default_update_const)
Andreas@48028
  1329
done
Andreas@48028
  1330
Andreas@48028
  1331
lemma finfun_dom_update_code [code]:
Andreas@48028
  1332
  "finfun_dom (finfun_update_code f a b) = finfun_update_code (finfun_dom f) a (b \<noteq> finfun_default f)"
Andreas@48028
  1333
by(simp)
Andreas@48028
  1334
Andreas@48028
  1335
lemma finite_finfun_dom: "finite {x. (finfun_dom f)\<^sub>f x}"
Andreas@48028
  1336
proof(induct f rule: finfun_weak_induct)
Andreas@48028
  1337
  case (const b)
Andreas@48028
  1338
  thus ?case
Andreas@48028
  1339
    by (cases "finite (UNIV :: 'a set) \<and> b \<noteq> undefined")
Andreas@48028
  1340
      (auto simp add: finfun_dom_const UNIV_def [symmetric] Set.empty_def [symmetric])
Andreas@48028
  1341
next
Andreas@48028
  1342
  case (update f a b)
Andreas@48028
  1343
  have "{x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} =
Andreas@48028
  1344
    (if b = finfun_default f then {x. (finfun_dom f)\<^sub>f x} - {a} else insert a {x. (finfun_dom f)\<^sub>f x})"
Andreas@48028
  1345
    by (auto simp add: finfun_upd_apply split: split_if_asm)
Andreas@48028
  1346
  thus ?case using update by simp
Andreas@48028
  1347
qed
Andreas@48028
  1348
Andreas@48028
  1349
Andreas@48028
  1350
subsection {* The domain of a FinFun as a sorted list *}
Andreas@48028
  1351
Andreas@48028
  1352
definition finfun_to_list :: "('a :: linorder) \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a list"
Andreas@48028
  1353
where
Andreas@48028
  1354
  "finfun_to_list f = (THE xs. set xs = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs \<and> distinct xs)"
Andreas@48028
  1355
Andreas@48028
  1356
lemma set_finfun_to_list [simp]: "set (finfun_to_list f) = {x. (finfun_dom f)\<^sub>f x}" (is ?thesis1)
Andreas@48028
  1357
  and sorted_finfun_to_list: "sorted (finfun_to_list f)" (is ?thesis2)
Andreas@48028
  1358
  and distinct_finfun_to_list: "distinct (finfun_to_list f)" (is ?thesis3)
Andreas@48028
  1359
proof -
Andreas@48028
  1360
  have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
Andreas@48028
  1361
    unfolding finfun_to_list_def
Andreas@48028
  1362
    by(rule theI')(rule finite_sorted_distinct_unique finite_finfun_dom)+
Andreas@48028
  1363
  thus ?thesis1 ?thesis2 ?thesis3 by simp_all
Andreas@48028
  1364
qed
Andreas@48028
  1365
Andreas@48028
  1366
lemma finfun_const_False_conv_bot: "(\<lambda>\<^isup>f False)\<^sub>f = bot"
Andreas@48028
  1367
by auto
Andreas@48028
  1368
Andreas@48028
  1369
lemma finfun_const_True_conv_top: "(\<lambda>\<^isup>f True)\<^sub>f = top"
Andreas@48028
  1370
by auto
Andreas@48028
  1371
Andreas@48028
  1372
lemma finfun_to_list_const:
Andreas@48028
  1373
  "finfun_to_list ((\<lambda>\<^isup>f c) :: ('a :: {linorder} \<Rightarrow>\<^isub>f 'b)) = 
Andreas@48028
  1374
  (if \<not> finite (UNIV :: 'a set) \<or> c = undefined then [] else THE xs. set xs = UNIV \<and> sorted xs \<and> distinct xs)"
Andreas@48028
  1375
by(auto simp add: finfun_to_list_def finfun_const_False_conv_bot finfun_const_True_conv_top finfun_dom_const)
Andreas@48028
  1376
Andreas@48028
  1377
lemma finfun_to_list_const_code [code]:
Andreas@48028
  1378
  "finfun_to_list ((\<lambda>\<^isup>f c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>\<^isub>f 'b)) =
Andreas@48028
  1379
   (if card_UNIV (TYPE('a)) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((\<lambda>\<^isup>f c) :: ('a \<Rightarrow>\<^isub>f 'b))))"
Andreas@48028
  1380
unfolding card_UNIV_eq_0_infinite_UNIV
Andreas@48028
  1381
by(auto simp add: finfun_to_list_const)
Andreas@48028
  1382
Andreas@48028
  1383
lemma remove1_insort_insert_same:
Andreas@48028
  1384
  "x \<notin> set xs \<Longrightarrow> remove1 x (insort_insert x xs) = xs"
Andreas@48028
  1385
by (metis insort_insert_insort remove1_insort)
Andreas@48028
  1386
Andreas@48028
  1387
lemma finfun_dom_conv:
Andreas@48028
  1388
  "(finfun_dom f)\<^sub>f x \<longleftrightarrow> f\<^sub>f x \<noteq> finfun_default f"
Andreas@48028
  1389
by(induct f rule: finfun_weak_induct)(auto simp add: finfun_dom_const finfun_default_const finfun_default_update_const finfun_upd_apply)
Andreas@48028
  1390
Andreas@48028
  1391
lemma finfun_to_list_update:
Andreas@48028
  1392
  "finfun_to_list (f(\<^sup>f a := b)) = 
Andreas@48028
  1393
  (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
Andreas@48028
  1394
proof(subst finfun_to_list_def, rule the_equality)
Andreas@48028
  1395
  fix xs
Andreas@48028
  1396
  assume "set xs = {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} \<and> sorted xs \<and> distinct xs"
Andreas@48028
  1397
  hence eq: "set xs = {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x}"
Andreas@48028
  1398
    and [simp]: "sorted xs" "distinct xs" by simp_all
Andreas@48028
  1399
  show "xs = (if b = finfun_default f then remove1 a (finfun_to_list f) else insort_insert a (finfun_to_list f))"
Andreas@48028
  1400
  proof(cases "b = finfun_default f")
Andreas@48028
  1401
    case True [simp]
Andreas@48028
  1402
    show ?thesis
Andreas@48028
  1403
    proof(cases "(finfun_dom f)\<^sub>f a")
Andreas@48028
  1404
      case True
Andreas@48028
  1405
      have "finfun_to_list f = insort_insert a xs"
Andreas@48028
  1406
        unfolding finfun_to_list_def
Andreas@48028
  1407
      proof(rule the_equality)
Andreas@48028
  1408
        have "set (insort_insert a xs) = insert a (set xs)" by(simp add: set_insort_insert)
Andreas@48028
  1409
        also note eq also
Andreas@48028
  1410
        have "insert a {x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} = {x. (finfun_dom f)\<^sub>f x}" using True
Andreas@48028
  1411
          by(auto simp add: finfun_upd_apply split: split_if_asm)
Andreas@48028
  1412
        finally show 1: "set (insort_insert a xs) = {x. (finfun_dom f)\<^sub>f x} \<and> sorted (insort_insert a xs) \<and> distinct (insort_insert a xs)"
Andreas@48028
  1413
          by(simp add: sorted_insort_insert distinct_insort_insert)
Andreas@48028
  1414
Andreas@48028
  1415
        fix xs'
Andreas@48028
  1416
        assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
Andreas@48028
  1417
        thus "xs' = insort_insert a xs" using 1 by(auto dest: sorted_distinct_set_unique)
Andreas@48028
  1418
      qed
Andreas@48028
  1419
      with eq True show ?thesis by(simp add: remove1_insort_insert_same)
Andreas@48028
  1420
    next
Andreas@48028
  1421
      case False
Andreas@48028
  1422
      hence "f\<^sub>f a = b" by(auto simp add: finfun_dom_conv)
Andreas@48028
  1423
      hence f: "f(\<^sup>f a := b) = f" by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
Andreas@48028
  1424
      from eq have "finfun_to_list f = xs" unfolding f finfun_to_list_def
Andreas@48028
  1425
        by(auto elim: sorted_distinct_set_unique intro!: the_equality)
Andreas@48028
  1426
      with eq False show ?thesis unfolding f by(simp add: remove1_idem)
Andreas@48028
  1427
    qed
Andreas@48028
  1428
  next
Andreas@48028
  1429
    case False
Andreas@48028
  1430
    show ?thesis
Andreas@48028
  1431
    proof(cases "(finfun_dom f)\<^sub>f a")
Andreas@48028
  1432
      case True
Andreas@48028
  1433
      have "finfun_to_list f = xs"
Andreas@48028
  1434
        unfolding finfun_to_list_def
Andreas@48028
  1435
      proof(rule the_equality)
Andreas@48028
  1436
        have "finfun_dom f = finfun_dom f(\<^sup>f a := b)" using False True
Andreas@48028
  1437
          by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
Andreas@48028
  1438
        with eq show 1: "set xs = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs \<and> distinct xs"
Andreas@48028
  1439
          by(simp del: finfun_dom_update)
Andreas@48028
  1440
        
Andreas@48028
  1441
        fix xs'
Andreas@48028
  1442
        assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
Andreas@48028
  1443
        thus "xs' = xs" using 1 by(auto elim: sorted_distinct_set_unique)
Andreas@48028
  1444
      qed
Andreas@48028
  1445
      thus ?thesis using False True eq by(simp add: insort_insert_triv)
Andreas@48028
  1446
    next
Andreas@48028
  1447
      case False
Andreas@48028
  1448
      have "finfun_to_list f = remove1 a xs"
Andreas@48028
  1449
        unfolding finfun_to_list_def
Andreas@48028
  1450
      proof(rule the_equality)
Andreas@48028
  1451
        have "set (remove1 a xs) = set xs - {a}" by simp
Andreas@48028
  1452
        also note eq also
Andreas@48028
  1453
        have "{x. (finfun_dom f(\<^sup>f a := b))\<^sub>f x} - {a} = {x. (finfun_dom f)\<^sub>f x}" using False
Andreas@48028
  1454
          by(auto simp add: finfun_upd_apply split: split_if_asm)
Andreas@48028
  1455
        finally show 1: "set (remove1 a xs) = {x. (finfun_dom f)\<^sub>f x} \<and> sorted (remove1 a xs) \<and> distinct (remove1 a xs)"
Andreas@48028
  1456
          by(simp add: sorted_remove1)
Andreas@48028
  1457
        
Andreas@48028
  1458
        fix xs'
Andreas@48028
  1459
        assume "set xs' = {x. (finfun_dom f)\<^sub>f x} \<and> sorted xs' \<and> distinct xs'"
Andreas@48028
  1460
        thus "xs' = remove1 a xs" using 1 by(blast intro: sorted_distinct_set_unique)
Andreas@48028
  1461
      qed
Andreas@48028
  1462
      thus ?thesis using False eq `b \<noteq> finfun_default f` 
Andreas@48028
  1463
        by (simp add: insort_insert_insort insort_remove1)
Andreas@48028
  1464
    qed
Andreas@48028
  1465
  qed
Andreas@48028
  1466
qed (auto simp add: distinct_finfun_to_list sorted_finfun_to_list sorted_remove1 set_insort_insert sorted_insort_insert distinct_insort_insert finfun_upd_apply split: split_if_asm)
Andreas@48028
  1467
Andreas@48028
  1468
lemma finfun_to_list_update_code [code]:
Andreas@48028
  1469
  "finfun_to_list (finfun_update_code f a b) = 
Andreas@48028
  1470
  (if b = finfun_default f then List.remove1 a (finfun_to_list f) else List.insort_insert a (finfun_to_list f))"
Andreas@48028
  1471
by(simp add: finfun_to_list_update)
Andreas@48028
  1472
Andreas@48028
  1473
end