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