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