merged

--- a/src/HOL/Code_Numeral.thy	Tue Jun 02 16:56:55 2009 +0200
+++ b/src/HOL/Code_Numeral.thy	Tue Jun 02 18:26:12 2009 +0200
@@ -279,7 +279,7 @@
 
 code_type code_numeral
   (SML "int")
-  (OCaml "int")
+  (OCaml "Big'_int.big'_int")
   (Haskell "Int")
 
 code_instance code_numeral :: eq
@@ -287,45 +287,46 @@
 
 setup {*
   fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false false) ["SML", "OCaml", "Haskell"]
+    false false) ["SML", "Haskell"]
+  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} false true "OCaml"
 *}
 
 code_reserved SML Int int
-code_reserved OCaml Pervasives int
+code_reserved OCaml Big_int
 
 code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   (SML "Int.+/ ((_),/ (_))")
-  (OCaml "Pervasives.( + )")
+  (OCaml "Big'_int.add'_big'_int")
   (Haskell infixl 6 "+")
 
 code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   (SML "Int.max/ (_/ -/ _,/ 0 : int)")
-  (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
+  (OCaml "Big'_int.max'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)/ Big'_int.zero'_big'_int")
   (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
 
 code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   (SML "Int.*/ ((_),/ (_))")
-  (OCaml "Pervasives.( * )")
+  (OCaml "Big'_int.mult'_big'_int")
   (Haskell infixl 7 "*")
 
 code_const div_mod_code_numeral
   (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
-  (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
+  (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))")
   (Haskell "divMod")
 
 code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "!((_ : Int.int) = _)")
-  (OCaml "!((_ : int) = _)")
+  (OCaml "Big'_int.eq'_big'_int")
   (Haskell infixl 4 "==")
 
 code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "Int.<=/ ((_),/ (_))")
-  (OCaml "!((_ : int) <= _)")
+  (OCaml "Big'_int.le'_big'_int")
   (Haskell infix 4 "<=")
 
 code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "Int.</ ((_),/ (_))")
-  (OCaml "!((_ : int) < _)")
+  (OCaml "Big'_int.lt'_big'_int")
   (Haskell infix 4 "<")
 
 end

--- a/src/HOL/Finite_Set.thy	Tue Jun 02 16:56:55 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Jun 02 18:26:12 2009 +0200
@@ -1926,34 +1926,40 @@
 But now that we have @{text setsum} things are easy:
 *}
 
-definition card :: "'a set \<Rightarrow> nat"
-where "card A = setsum (\<lambda>x. 1) A"
+definition card :: "'a set \<Rightarrow> nat" where
+  "card A = setsum (\<lambda>x. 1) A"
+
+lemmas card_eq_setsum = card_def
 
 lemma card_empty [simp]: "card {} = 0"
-by (simp add: card_def)
-
-lemma card_infinite [simp]: "~ finite A ==> card A = 0"
-by (simp add: card_def)
-
-lemma card_eq_setsum: "card A = setsum (%x. 1) A"
-by (simp add: card_def)
+  by (simp add: card_def)
 
 lemma card_insert_disjoint [simp]:
   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
-by(simp add: card_def)
+  by (simp add: card_def)
 
 lemma card_insert_if:
   "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
-by (simp add: insert_absorb)
+  by (simp add: insert_absorb)
+
+lemma card_infinite [simp]: "~ finite A ==> card A = 0"
+  by (simp add: card_def)
+
+lemma card_ge_0_finite:
+  "card A > 0 \<Longrightarrow> finite A"
+  by (rule ccontr) simp
 
 lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})"
-apply auto
-apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
-done
+  apply auto
+  apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
+  done
+
+lemma finite_UNIV_card_ge_0:
+  "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0"
+  by (rule ccontr) simp
 
 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
-by auto
-
+  by auto
 
 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
@@ -2049,6 +2055,24 @@
        finite_subset [of _ "\<Union> (insert x F)"])
 done
 
+lemma card_eq_UNIV_imp_eq_UNIV:
+  assumes fin: "finite (UNIV :: 'a set)"
+  and card: "card A = card (UNIV :: 'a set)"
+  shows "A = (UNIV :: 'a set)"
+proof
+  show "A \<subseteq> UNIV" by simp
+  show "UNIV \<subseteq> A"
+  proof
+    fix x
+    show "x \<in> A"
+    proof (rule ccontr)
+      assume "x \<notin> A"
+      then have "A \<subset> UNIV" by auto
+      with fin have "card A < card (UNIV :: 'a set)" by (fact psubset_card_mono)
+      with card show False by simp
+    qed
+  qed
+qed
 
 text{*The form of a finite set of given cardinality*}
 
@@ -2078,6 +2102,17 @@
  apply(auto intro:ccontr)
 done
 
+lemma finite_fun_UNIVD2:
+  assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
+  shows "finite (UNIV :: 'b set)"
+proof -
+  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))"
+    by(rule finite_imageI)
+  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)"
+    by(rule UNIV_eq_I) auto
+  ultimately show "finite (UNIV :: 'b set)" by simp
+qed
+
 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
 apply (cases "finite A")
 apply (erule finite_induct)

--- a/src/HOL/Hilbert_Choice.thy	Tue Jun 02 16:56:55 2009 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Tue Jun 02 18:26:12 2009 +0200
@@ -219,6 +219,25 @@
 apply (blast intro: bij_is_inj [THEN inv_f_f, symmetric])
 done
 
+lemma finite_fun_UNIVD1:
+  assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
+  and card: "card (UNIV :: 'b set) \<noteq> Suc 0"
+  shows "finite (UNIV :: 'a set)"
+proof -
+  from fin have finb: "finite (UNIV :: 'b set)" by (rule finite_fun_UNIVD2)
+  with card have "card (UNIV :: 'b set) \<ge> Suc (Suc 0)"
+    by (cases "card (UNIV :: 'b set)") (auto simp add: card_eq_0_iff)
+  then obtain n where "card (UNIV :: 'b set) = Suc (Suc n)" "n = card (UNIV :: 'b set) - Suc (Suc 0)" by auto
+  then obtain b1 b2 where b1b2: "(b1 :: 'b) \<noteq> (b2 :: 'b)" by (auto simp add: card_Suc_eq)
+  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))" by (rule finite_imageI)
+  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
+  proof (rule UNIV_eq_I)
+    fix x :: 'a
+    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_def)
+    thus "x \<in> range (\<lambda>f\<Colon>'a \<Rightarrow> 'b. inv f b1)" by blast
+  qed
+  ultimately show "finite (UNIV :: 'a set)" by simp
+qed
 
 subsection {*Inverse of a PI-function (restricted domain)*}
 

--- a/src/HOL/IsaMakefile	Tue Jun 02 16:56:55 2009 +0200
+++ b/src/HOL/IsaMakefile	Tue Jun 02 18:26:12 2009 +0200
@@ -838,11 +838,12 @@
   ex/Arith_Examples.thy				\
   ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy		\
   ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy		\
-  ex/CodegenSML_Test.thy ex/Codegenerator.thy				\
-  ex/Codegenerator_Pretty.thy ex/Coherent.thy				\
+  ex/CodegenSML_Test.thy ex/Codegenerator_Candidates.thy				\
+  ex/Codegenerator_Pretty.thy ex/Codegenerator_Test.thy \
+  ex/Codegenerator_Pretty_Test.thy ex/Coherent.thy				\
   ex/Commutative_RingEx.thy ex/Commutative_Ring_Complete.thy		\
   ex/Efficient_Nat_examples.thy		\
-  ex/Eval_Examples.thy ex/ExecutableContent.thy				\
+  ex/Eval_Examples.thy				\
   ex/Formal_Power_Series_Examples.thy ex/Fundefs.thy			\
   ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy		\
   ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy	\

--- a/src/HOL/Library/Code_Integer.thy	Tue Jun 02 16:56:55 2009 +0200
+++ b/src/HOL/Library/Code_Integer.thy	Tue Jun 02 18:26:12 2009 +0200
@@ -93,11 +93,10 @@
 
 code_const Code_Numeral.int_of
   (SML "IntInf.fromInt")
-  (OCaml "Big'_int.big'_int'_of'_int")
+  (OCaml "_")
   (Haskell "toEnum")
 
 code_reserved SML IntInf
-code_reserved OCaml Big_int
 
 text {* Evaluation *}
 

--- a/src/HOL/Library/Efficient_Nat.thy	Tue Jun 02 16:56:55 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jun 02 18:26:12 2009 +0200
@@ -371,12 +371,12 @@
 
 code_const Code_Numeral.of_nat
   (SML "IntInf.toInt")
-  (OCaml "Big'_int.int'_of'_big'_int")
+  (OCaml "_")
   (Haskell "fromEnum")
 
 code_const Code_Numeral.nat_of
   (SML "IntInf.fromInt")
-  (OCaml "Big'_int.big'_int'_of'_int")
+  (OCaml "_")
   (Haskell "toEnum")
 
 text {* Using target language arithmetic operations whenever appropriate *}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Fin_Fun.thy	Tue Jun 02 18:26:12 2009 +0200
@@ -0,0 +1,1605 @@
+
+(* Author: Andreas Lochbihler, Uni Karlsruhe *)
+
+header {* Almost everywhere constant functions *}
+
+theory Fin_Fun
+imports Main Infinite_Set Enum
+begin
+
+text {*
+  This theory defines functions which are constant except for finitely
+  many points (FinFun) and introduces a type finfin along with a
+  number of operators for them. The code generator is set up such that
+  such functions can be represented as data in the generated code and
+  all operators are executable.
+
+  For details, see Formalising FinFuns - Generating Code for Functions as Data by A. Lochbihler in TPHOLs 2009.
+*}
+
+(*FIXME move to Map.thy*)
+lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
+  by (auto simp add: restrict_map_def intro: ext)
+
+
+subsection {* The @{text "map_default"} operation *}
+
+definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+where "map_default b f a \<equiv> case f a of None \<Rightarrow> b | Some b' \<Rightarrow> b'"
+
+lemma map_default_delete [simp]:
+  "map_default b (f(a := None)) = (map_default b f)(a := b)"
+by(simp add: map_default_def expand_fun_eq)
+
+lemma map_default_insert:
+  "map_default b (f(a \<mapsto> b')) = (map_default b f)(a := b')"
+by(simp add: map_default_def expand_fun_eq)
+
+lemma map_default_empty [simp]: "map_default b empty = (\<lambda>a. b)"
+by(simp add: expand_fun_eq map_default_def)
+
+lemma map_default_inject:
+  fixes g g' :: "'a \<rightharpoonup> 'b"
+  assumes infin_eq: "\<not> finite (UNIV :: 'a set) \<or> b = b'"
+  and fin: "finite (dom g)" and b: "b \<notin> ran g"
+  and fin': "finite (dom g')" and b': "b' \<notin> ran g'"
+  and eq': "map_default b g = map_default b' g'"
+  shows "b = b'" "g = g'"
+proof -
+  from infin_eq show bb': "b = b'"
+  proof
+    assume infin: "\<not> finite (UNIV :: 'a set)"
+    from fin fin' have "finite (dom g \<union> dom g')" by auto
+    with infin have "UNIV - (dom g \<union> dom g') \<noteq> {}" by(auto dest: finite_subset)
+    then obtain a where a: "a \<notin> dom g \<union> dom g'" by auto
+    hence "map_default b g a = b" "map_default b' g' a = b'" by(auto simp add: map_default_def)
+    with eq' show "b = b'" by simp
+  qed
+
+  show "g = g'"
+  proof
+    fix x
+    show "g x = g' x"
+    proof(cases "g x")
+      case None
+      hence "map_default b g x = b" by(simp add: map_default_def)
+      with bb' eq' have "map_default b' g' x = b'" by simp
+      with b' have "g' x = None" by(simp add: map_default_def ran_def split: option.split_asm)
+      with None show ?thesis by simp
+    next
+      case (Some c)
+      with b have cb: "c \<noteq> b" by(auto simp add: ran_def)
+      moreover from Some have "map_default b g x = c" by(simp add: map_default_def)
+      with eq' have "map_default b' g' x = c" by simp
+      ultimately have "g' x = Some c" using b' bb' by(auto simp add: map_default_def split: option.splits)
+      with Some show ?thesis by simp
+    qed
+  qed
+qed
+
+subsection {* The finfun type *}
+
+typedef ('a,'b) finfun = "{f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
+apply(auto)
+apply(rule_tac x="\<lambda>x. arbitrary" in exI)
+apply(auto)
+done
+
+syntax
+  "finfun"      :: "type \<Rightarrow> type \<Rightarrow> type"         ("(_ \<Rightarrow>\<^isub>f /_)" [22, 21] 21)
+
+lemma fun_upd_finfun: "y(a := b) \<in> finfun \<longleftrightarrow> y \<in> finfun"
+proof -
+  { fix b'
+    have "finite {a'. (y(a := b)) a' \<noteq> b'} = finite {a'. y a' \<noteq> b'}"
+    proof(cases "b = b'")
+      case True
+      hence "{a'. (y(a := b)) a' \<noteq> b'} = {a'. y a' \<noteq> b'} - {a}" by auto
+      thus ?thesis by simp
+    next
+      case False
+      hence "{a'. (y(a := b)) a' \<noteq> b'} = insert a {a'. y a' \<noteq> b'}" by auto
+      thus ?thesis by simp
+    qed }
+  thus ?thesis unfolding finfun_def by blast
+qed
+
+lemma const_finfun: "(\<lambda>x. a) \<in> finfun"
+by(auto simp add: finfun_def)
+
+lemma finfun_left_compose:
+  assumes "y \<in> finfun"
+  shows "g \<circ> y \<in> finfun"
+proof -
+  from assms obtain b where "finite {a. y a \<noteq> b}"
+    unfolding finfun_def by blast
+  hence "finite {c. g (y c) \<noteq> g b}"
+  proof(induct x\<equiv>"{a. y a \<noteq> b}" arbitrary: y)
+    case empty
+    hence "y = (\<lambda>a. b)" by(auto intro: ext)
+    thus ?case by(simp)
+  next
+    case (insert x F)
+    note IH = `\<And>y. F = {a. y a \<noteq> b} \<Longrightarrow> finite {c. g (y c) \<noteq> g b}`
+    from `insert x F = {a. y a \<noteq> b}` `x \<notin> F`
+    have F: "F = {a. (y(x := b)) a \<noteq> b}" by(auto)
+    show ?case
+    proof(cases "g (y x) = g b")
+      case True
+      hence "{c. g ((y(x := b)) c) \<noteq> g b} = {c. g (y c) \<noteq> g b}" by auto
+      with IH[OF F] show ?thesis by simp
+    next
+      case False
+      hence "{c. g (y c) \<noteq> g b} = insert x {c. g ((y(x := b)) c) \<noteq> g b}" by auto
+      with IH[OF F] show ?thesis by(simp)
+    qed
+  qed
+  thus ?thesis unfolding finfun_def by auto
+qed
+
+lemma assumes "y \<in> finfun"
+  shows fst_finfun: "fst \<circ> y \<in> finfun"
+  and snd_finfun: "snd \<circ> y \<in> finfun"
+proof -
+  from assms obtain b c where bc: "finite {a. y a \<noteq> (b, c)}"
+    unfolding finfun_def by auto
+  have "{a. fst (y a) \<noteq> b} \<subseteq> {a. y a \<noteq> (b, c)}"
+    and "{a. snd (y a) \<noteq> c} \<subseteq> {a. y a \<noteq> (b, c)}" by auto
+  hence "finite {a. fst (y a) \<noteq> b}" 
+    and "finite {a. snd (y a) \<noteq> c}" using bc by(auto intro: finite_subset)
+  thus "fst \<circ> y \<in> finfun" "snd \<circ> y \<in> finfun"
+    unfolding finfun_def by auto
+qed
+
+lemma map_of_finfun: "map_of xs \<in> finfun"
+unfolding finfun_def
+by(induct xs)(auto simp add: Collect_neg_eq Collect_conj_eq Collect_imp_eq intro: finite_subset)
+
+lemma Diag_finfun: "(\<lambda>x. (f x, g x)) \<in> finfun \<longleftrightarrow> f \<in> finfun \<and> g \<in> finfun"
+by(auto intro: finite_subset simp add: Collect_neg_eq Collect_imp_eq Collect_conj_eq finfun_def)
+
+lemma finfun_right_compose:
+  assumes g: "g \<in> finfun" and inj: "inj f"
+  shows "g o f \<in> finfun"
+proof -
+  from g obtain b where b: "finite {a. g a \<noteq> b}" unfolding finfun_def by blast
+  moreover have "f ` {a. g (f a) \<noteq> b} \<subseteq> {a. g a \<noteq> b}" by auto
+  moreover from inj have "inj_on f {a.  g (f a) \<noteq> b}" by(rule subset_inj_on) blast
+  ultimately have "finite {a. g (f a) \<noteq> b}"
+    by(blast intro: finite_imageD[where f=f] finite_subset)
+  thus ?thesis unfolding finfun_def by auto
+qed
+
+lemma finfun_curry:
+  assumes fin: "f \<in> finfun"
+  shows "curry f \<in> finfun" "curry f a \<in> finfun"
+proof -
+  from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
+  moreover have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
+  hence "{a. curry f a \<noteq> (\<lambda>b. c)} = fst ` {ab. f ab \<noteq> c}"
+    by(auto simp add: curry_def expand_fun_eq)
+  ultimately have "finite {a. curry f a \<noteq> (\<lambda>b. c)}" by simp
+  thus "curry f \<in> finfun" unfolding finfun_def by blast
+  
+  have "snd ` {ab. f ab \<noteq> c} = {b. \<exists>a. f (a, b) \<noteq> c}" by(force)
+  hence "{b. f (a, b) \<noteq> c} \<subseteq> snd ` {ab. f ab \<noteq> c}" by auto
+  hence "finite {b. f (a, b) \<noteq> c}" by(rule finite_subset)(rule finite_imageI[OF c])
+  thus "curry f a \<in> finfun" unfolding finfun_def by auto
+qed
+
+lemmas finfun_simp = 
+  fst_finfun snd_finfun Abs_finfun_inverse Rep_finfun_inverse Abs_finfun_inject Rep_finfun_inject Diag_finfun finfun_curry
+lemmas finfun_iff = const_finfun fun_upd_finfun Rep_finfun map_of_finfun
+lemmas finfun_intro = finfun_left_compose fst_finfun snd_finfun
+
+lemma Abs_finfun_inject_finite:
+  fixes x y :: "'a \<Rightarrow> 'b"
+  assumes fin: "finite (UNIV :: 'a set)"
+  shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
+proof
+  assume "Abs_finfun x = Abs_finfun y"
+  moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
+    by(auto intro: finite_subset[OF _ fin])
+  ultimately show "x = y" by(simp add: Abs_finfun_inject)
+qed simp
+
+lemma Abs_finfun_inject_finite_class:
+  fixes x y :: "('a :: finite) \<Rightarrow> 'b"
+  shows "Abs_finfun x = Abs_finfun y \<longleftrightarrow> x = y"
+using finite_UNIV
+by(simp add: Abs_finfun_inject_finite)
+
+lemma Abs_finfun_inj_finite:
+  assumes fin: "finite (UNIV :: 'a set)"
+  shows "inj (Abs_finfun :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b)"
+proof(rule inj_onI)
+  fix x y :: "'a \<Rightarrow> 'b"
+  assume "Abs_finfun x = Abs_finfun y"
+  moreover have "x \<in> finfun" "y \<in> finfun" unfolding finfun_def
+    by(auto intro: finite_subset[OF _ fin])
+  ultimately show "x = y" by(simp add: Abs_finfun_inject)
+qed
+
+declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
+
+lemma Abs_finfun_inverse_finite:
+  fixes x :: "'a \<Rightarrow> 'b"
+  assumes fin: "finite (UNIV :: 'a set)"
+  shows "Rep_finfun (Abs_finfun x) = x"
+proof -
+  from fin have "x \<in> finfun"
+    by(auto simp add: finfun_def intro: finite_subset)
+  thus ?thesis by simp
+qed
+
+declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
+
+lemma Abs_finfun_inverse_finite_class:
+  fixes x :: "('a :: finite) \<Rightarrow> 'b"
+  shows "Rep_finfun (Abs_finfun x) = x"
+using finite_UNIV by(simp add: Abs_finfun_inverse_finite)
+
+lemma finfun_eq_finite_UNIV: "finite (UNIV :: 'a set) \<Longrightarrow> (finfun :: ('a \<Rightarrow> 'b) set) = UNIV"
+unfolding finfun_def by(auto intro: finite_subset)
+
+lemma finfun_finite_UNIV_class: "finfun = (UNIV :: ('a :: finite \<Rightarrow> 'b) set)"
+by(simp add: finfun_eq_finite_UNIV)
+
+lemma map_default_in_finfun:
+  assumes fin: "finite (dom f)"
+  shows "map_default b f \<in> finfun"
+unfolding finfun_def
+proof(intro CollectI exI)
+  from fin show "finite {a. map_default b f a \<noteq> b}"
+    by(auto simp add: map_default_def dom_def Collect_conj_eq split: option.splits)
+qed
+
+lemma finfun_cases_map_default:
+  obtains b g where "f = Abs_finfun (map_default b g)" "finite (dom g)" "b \<notin> ran g"
+proof -
+  obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by(cases f)
+  from y obtain b where b: "finite {a. y a \<noteq> b}" unfolding finfun_def by auto
+  let ?g = "(\<lambda>a. if y a = b then None else Some (y a))"
+  have "map_default b ?g = y" by(simp add: expand_fun_eq map_default_def)
+  with f have "f = Abs_finfun (map_default b ?g)" by simp
+  moreover from b have "finite (dom ?g)" by(auto simp add: dom_def)
+  moreover have "b \<notin> ran ?g" by(auto simp add: ran_def)
+  ultimately show ?thesis by(rule that)
+qed
+
+
+subsection {* Kernel functions for type @{typ "'a \<Rightarrow>\<^isub>f 'b"} *}
+
+definition finfun_const :: "'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("\<lambda>\<^isup>f/ _" [0] 1)
+where [code del]: "(\<lambda>\<^isup>f b) = Abs_finfun (\<lambda>x. b)"
+
+definition finfun_update :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>f/ _ := _')" [1000,0,0] 1000)
+where [code del]: "f(\<^sup>fa := b) = Abs_finfun ((Rep_finfun f)(a := b))"
+
+declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
+
+lemma finfun_update_twist: "a \<noteq> a' \<Longrightarrow> f(\<^sup>f a := b)(\<^sup>f a' := b') = f(\<^sup>f a' := b')(\<^sup>f a := b)"
+by(simp add: finfun_update_def fun_upd_twist)
+
+lemma finfun_update_twice [simp]:
+  "finfun_update (finfun_update f a b) a b' = finfun_update f a b'"
+by(simp add: finfun_update_def)
+
+lemma finfun_update_const_same: "(\<lambda>\<^isup>f b)(\<^sup>f a := b) = (\<lambda>\<^isup>f b)"
+by(simp add: finfun_update_def finfun_const_def expand_fun_eq)
+
+declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
+
+subsection {* Code generator setup *}
+
+definition finfun_update_code :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b" ("_'(\<^sup>f\<^sup>c/ _ := _')" [1000,0,0] 1000)
+where [simp, code del]: "finfun_update_code = finfun_update"
+
+code_datatype finfun_const finfun_update_code
+
+lemma finfun_update_const_code [code]:
+  "(\<lambda>\<^isup>f b)(\<^sup>f a := b') = (if b = b' then (\<lambda>\<^isup>f b) else finfun_update_code (\<lambda>\<^isup>f b) a b')"
+by(simp add: finfun_update_const_same)
+
+lemma finfun_update_update_code [code]:
+  "(finfun_update_code f a b)(\<^sup>f a' := b') = (if a = a' then f(\<^sup>f a := b') else finfun_update_code (f(\<^sup>f a' := b')) a b)"
+by(simp add: finfun_update_twist)
+
+
+subsection {* Setup for quickcheck *}
+
+notation fcomp (infixl "o>" 60)
+notation scomp (infixl "o\<rightarrow>" 60)
+
+definition (in term_syntax) valtermify_finfun_const ::
+  "'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a\<Colon>typerep \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term)" where
+  "valtermify_finfun_const y = Code_Eval.valtermify finfun_const {\<cdot>} y"
+
+definition (in term_syntax) valtermify_finfun_update_code ::
+  "'a\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> 'b\<Colon>typerep \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<times> (unit \<Rightarrow> Code_Eval.term)" where
+  "valtermify_finfun_update_code x y f = Code_Eval.valtermify finfun_update_code {\<cdot>} f {\<cdot>} x {\<cdot>} y"
+
+instantiation finfun :: (random, random) random
+begin
+
+primrec random_finfun' :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b \<times> (unit \<Rightarrow> Code_Eval.term)) \<times> Random.seed" where
+    "random_finfun' 0 j = Quickcheck.collapse (Random.select_default 0
+       (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y)))
+       (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
+  | "random_finfun' (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_default i
+       (random j o\<rightarrow> (\<lambda>x. random j o\<rightarrow> (\<lambda>y. random_finfun' i j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f)))))
+       (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
+                         
+definition 
+  "random i = random_finfun' i i"
+
+instance ..
+
+end
+
+lemma select_default_zero:
+  "Random.select_default 0 y y = Random.select_default 0 x y"
+  by (simp add: select_default_def)
+
+lemma random_finfun'_code [code]:
+  "random_finfun' i j = Quickcheck.collapse (Random.select_default (i - 1)
+    (random j o\<rightarrow> (\<lambda>x. random j o\<rightarrow> (\<lambda>y. random_finfun' (i - 1) j o\<rightarrow> (\<lambda>f. Pair (valtermify_finfun_update_code x y f)))))
+    (random j o\<rightarrow> (\<lambda>y. Pair (valtermify_finfun_const y))))"
+  apply (cases i rule: code_numeral.exhaust)
+  apply (simp_all only: random_finfun'.simps code_numeral_zero_minus_one Suc_code_numeral_minus_one)
+  apply (subst select_default_zero) apply (simp only:)
+  done
+
+no_notation fcomp (infixl "o>" 60)
+no_notation scomp (infixl "o\<rightarrow>" 60)
+
+
+subsection {* @{text "finfun_update"} as instance of @{text "fun_left_comm"} *}
+
+declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
+
+interpretation finfun_update: fun_left_comm "\<lambda>a f. f(\<^sup>f a :: 'a := b')"
+proof
+  fix a' a :: 'a
+  fix b
+  have "(Rep_finfun b)(a := b', a' := b') = (Rep_finfun b)(a' := b', a := b')"
+    by(cases "a = a'")(auto simp add: fun_upd_twist)
+  thus "b(\<^sup>f a := b')(\<^sup>f a' := b') = b(\<^sup>f a' := b')(\<^sup>f a := b')"
+    by(auto simp add: finfun_update_def fun_upd_twist)
+qed
+
+lemma fold_finfun_update_finite_univ:
+  assumes fin: "finite (UNIV :: 'a set)"
+  shows "fold (\<lambda>a f. f(\<^sup>f a := b')) (\<lambda>\<^isup>f b) (UNIV :: 'a set) = (\<lambda>\<^isup>f b')"
+proof -
+  { fix A :: "'a set"
+    from fin have "finite A" by(auto intro: finite_subset)
+    hence "fold (\<lambda>a f. f(\<^sup>f a := b')) (\<lambda>\<^isup>f b) A = Abs_finfun (\<lambda>a. if a \<in> A then b' else b)"
+    proof(induct)
+      case (insert x F)
+      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)"
+        by(auto intro: ext)
+      with insert show ?case
+        by(simp add: finfun_const_def fun_upd_def)(simp add: finfun_update_def Abs_finfun_inverse_finite[OF fin] fun_upd_def)
+    qed(simp add: finfun_const_def) }
+  thus ?thesis by(simp add: finfun_const_def)
+qed
+
+
+subsection {* Default value for FinFuns *}
+
+definition finfun_default_aux :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"
+where [code del]: "finfun_default_aux f = (if finite (UNIV :: 'a set) then arbitrary else THE b. finite {a. f a \<noteq> b})"
+
+lemma finfun_default_aux_infinite:
+  fixes f :: "'a \<Rightarrow> 'b"
+  assumes infin: "infinite (UNIV :: 'a set)"
+  and fin: "finite {a. f a \<noteq> b}"
+  shows "finfun_default_aux f = b"
+proof -
+  let ?B = "{a. f a \<noteq> b}"
+  from fin have "(THE b. finite {a. f a \<noteq> b}) = b"
+  proof(rule the_equality)
+    fix b'
+    assume "finite {a. f a \<noteq> b'}" (is "finite ?B'")
+    with infin fin have "UNIV - (?B' \<union> ?B) \<noteq> {}" by(auto dest: finite_subset)
+    then obtain a where a: "a \<notin> ?B' \<union> ?B" by auto
+    thus "b' = b" by auto
+  qed
+  thus ?thesis using infin by(simp add: finfun_default_aux_def)
+qed
+
+
+lemma finite_finfun_default_aux:
+  fixes f :: "'a \<Rightarrow> 'b"
+  assumes fin: "f \<in> finfun"
+  shows "finite {a. f a \<noteq> finfun_default_aux f}"
+proof(cases "finite (UNIV :: 'a set)")
+  case True thus ?thesis using fin
+    by(auto simp add: finfun_def finfun_default_aux_def intro: finite_subset)
+next
+  case False
+  from fin obtain b where b: "finite {a. f a \<noteq> b}" (is "finite ?B")
+    unfolding finfun_def by blast
+  with False show ?thesis by(simp add: finfun_default_aux_infinite)
+qed
+
+lemma finfun_default_aux_update_const:
+  fixes f :: "'a \<Rightarrow> 'b"
+  assumes fin: "f \<in> finfun"
+  shows "finfun_default_aux (f(a := b)) = finfun_default_aux f"
+proof(cases "finite (UNIV :: 'a set)")
+  case False
+  from fin obtain b' where b': "finite {a. f a \<noteq> b'}" unfolding finfun_def by blast
+  hence "finite {a'. (f(a := b)) a' \<noteq> b'}"
+  proof(cases "b = b' \<and> f a \<noteq> b'") 
+    case True
+    hence "{a. f a \<noteq> b'} = insert a {a'. (f(a := b)) a' \<noteq> b'}" by auto
+    thus ?thesis using b' by simp
+  next
+    case False
+    moreover
+    { assume "b \<noteq> b'"
+      hence "{a'. (f(a := b)) a' \<noteq> b'} = insert a {a. f a \<noteq> b'}" by auto
+      hence ?thesis using b' by simp }
+    moreover
+    { assume "b = b'" "f a = b'"
+      hence "{a'. (f(a := b)) a' \<noteq> b'} = {a. f a \<noteq> b'}" by auto
+      hence ?thesis using b' by simp }
+    ultimately show ?thesis by blast
+  qed
+  with False b' show ?thesis by(auto simp del: fun_upd_apply simp add: finfun_default_aux_infinite)
+next
+  case True thus ?thesis by(simp add: finfun_default_aux_def)
+qed
+
+definition finfun_default :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'b"
+  where [code del]: "finfun_default f = finfun_default_aux (Rep_finfun f)"
+
+lemma finite_finfun_default: "finite {a. Rep_finfun f a \<noteq> finfun_default f}"
+unfolding finfun_default_def by(simp add: finite_finfun_default_aux)
+
+lemma finfun_default_const: "finfun_default ((\<lambda>\<^isup>f b) :: 'a \<Rightarrow>\<^isub>f 'b) = (if finite (UNIV :: 'a set) then arbitrary else b)"
+apply(auto simp add: finfun_default_def finfun_const_def finfun_default_aux_infinite)
+apply(simp add: finfun_default_aux_def)
+done
+
+lemma finfun_default_update_const:
+  "finfun_default (f(\<^sup>f a := b)) = finfun_default f"
+unfolding finfun_default_def finfun_update_def
+by(simp add: finfun_default_aux_update_const)
+
+subsection {* Recursion combinator and well-formedness conditions *}
+
+definition finfun_rec :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow>\<^isub>f 'b) \<Rightarrow> 'c"
+where [code del]:
+  "finfun_rec cnst upd f \<equiv>
+   let b = finfun_default f;
+       g = THE g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g
+   in fold (\<lambda>a. upd a (map_default b g a)) (cnst b) (dom g)"
+
+locale finfun_rec_wf_aux =
+  fixes cnst :: "'b \<Rightarrow> 'c"
+  and upd :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c"
+  assumes upd_const_same: "upd a b (cnst b) = cnst b"
+  and upd_commute: "a \<noteq> a' \<Longrightarrow> upd a b (upd a' b' c) = upd a' b' (upd a b c)"
+  and upd_idemp: "b \<noteq> b' \<Longrightarrow> upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
+begin
+
+
+lemma upd_left_comm: "fun_left_comm (\<lambda>a. upd a (f a))"
+by(unfold_locales)(auto intro: upd_commute)
+
+lemma upd_upd_twice: "upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)"
+by(cases "b \<noteq> b'")(auto simp add: fun_upd_def upd_const_same upd_idemp)
+
+declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
+
+lemma map_default_update_const:
+  assumes fin: "finite (dom f)"
+  and anf: "a \<notin> dom f"
+  and fg: "f \<subseteq>\<^sub>m g"
+  shows "upd a d  (fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)) =
+         fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f)"
+proof -
+  let ?upd = "\<lambda>a. upd a (map_default d g a)"
+  let ?fr = "\<lambda>A. fold ?upd (cnst d) A"
+  interpret gwf: fun_left_comm "?upd" by(rule upd_left_comm)
+  
+  from fin anf fg show ?thesis
+  proof(induct A\<equiv>"dom f" arbitrary: f)
+    case empty
+    from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
+    thus ?case by(simp add: finfun_const_def upd_const_same)
+  next
+    case (insert a' A)
+    note IH = `\<And>f.  \<lbrakk> a \<notin> dom f; f \<subseteq>\<^sub>m g; A = dom f\<rbrakk> \<Longrightarrow> upd a d (?fr (dom f)) = ?fr (dom f)`
+    note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
+    note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
+    
+    from domf obtain b where b: "f a' = Some b" by auto
+    let ?f' = "f(a' := None)"
+    have "upd a d (?fr (insert a' A)) = upd a d (upd a' (map_default d g a') (?fr A))"
+      by(subst gwf.fold_insert[OF fin a'nA]) rule
+    also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
+    hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
+    also from anf domf have "a \<noteq> a'" by auto note upd_commute[OF this]
+    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)
+    note A also note IH[OF `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g` A]
+    also have "upd a' (map_default d f a') (?fr (dom (f(a' := None)))) = ?fr (dom f)"
+      unfolding domf[symmetric] gwf.fold_insert[OF fin a'nA] ga' unfolding A ..
+    also have "insert a' (dom ?f') = dom f" using domf by auto
+    finally show ?case .
+  qed
+qed
+
+lemma map_default_update_twice:
+  assumes fin: "finite (dom f)"
+  and anf: "a \<notin> dom f"
+  and fg: "f \<subseteq>\<^sub>m g"
+  shows "upd a d'' (upd a d' (fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))) =
+         upd a d'' (fold (\<lambda>a. upd a (map_default d g a)) (cnst d) (dom f))"
+proof -
+  let ?upd = "\<lambda>a. upd a (map_default d g a)"
+  let ?fr = "\<lambda>A. fold ?upd (cnst d) A"
+  interpret gwf: fun_left_comm "?upd" by(rule upd_left_comm)
+  
+  from fin anf fg show ?thesis
+  proof(induct A\<equiv>"dom f" arbitrary: f)
+    case empty
+    from `{} = dom f` have "f = empty" by(auto simp add: dom_def intro: ext)
+    thus ?case by(auto simp add: finfun_const_def finfun_update_def upd_upd_twice)
+  next
+    case (insert a' A)
+    note IH = `\<And>f. \<lbrakk>a \<notin> dom f; f \<subseteq>\<^sub>m g; A = dom f\<rbrakk> \<Longrightarrow> upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (?fr (dom f))`
+    note fin = `finite A` note anf = `a \<notin> dom f` note a'nA = `a' \<notin> A`
+    note domf = `insert a' A = dom f` note fg = `f \<subseteq>\<^sub>m g`
+    
+    from domf obtain b where b: "f a' = Some b" by auto
+    let ?f' = "f(a' := None)"
+    let ?b' = "case f a' of None \<Rightarrow> d | Some b \<Rightarrow> b"
+    from domf have "upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (upd a d' (?fr (insert a' A)))" by simp
+    also note gwf.fold_insert[OF fin a'nA]
+    also from b fg have "g a' = f a'" by(auto simp add: map_le_def intro: domI dest: bspec)
+    hence ga': "map_default d g a' = map_default d f a'" by(simp add: map_default_def)
+    also from anf domf have ana': "a \<noteq> a'" by auto note upd_commute[OF this]
+    also note upd_commute[OF ana']
+    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)
+    note A also note IH[OF `a \<notin> dom ?f'` `?f' \<subseteq>\<^sub>m g` A]
+    also note upd_commute[OF ana'[symmetric]] also note ga'[symmetric] also note A[symmetric]
+    also note gwf.fold_insert[symmetric, OF fin a'nA] also note domf
+    finally show ?case .
+  qed
+qed
+
+declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
+
+lemma map_default_eq_id [simp]: "map_default d ((\<lambda>a. Some (f a)) |` {a. f a \<noteq> d}) = f"
+by(auto simp add: map_default_def restrict_map_def intro: ext)
+
+lemma finite_rec_cong1:
+  assumes f: "fun_left_comm f" and g: "fun_left_comm g"
+  and fin: "finite A"
+  and eq: "\<And>a. a \<in> A \<Longrightarrow> f a = g a"
+  shows "fold f z A = fold g z A"
+proof -
+  interpret f: fun_left_comm f by(rule f)
+  interpret g: fun_left_comm g by(rule g)
+  { fix B
+    assume BsubA: "B \<subseteq> A"
+    with fin have "finite B" by(blast intro: finite_subset)
+    hence "B \<subseteq> A \<Longrightarrow> fold f z B = fold g z B"
+    proof(induct)
+      case empty thus ?case by simp
+    next
+      case (insert a B)
+      note finB = `finite B` note anB = `a \<notin> B` note sub = `insert a B \<subseteq> A`
+      note IH = `B \<subseteq> A \<Longrightarrow> fold f z B = fold g z B`
+      from sub anB have BpsubA: "B \<subset> A" and BsubA: "B \<subseteq> A" and aA: "a \<in> A" by auto
+      from IH[OF BsubA] eq[OF aA] finB anB
+      show ?case by(auto)
+    qed
+    with BsubA have "fold f z B = fold g z B" by blast }
+  thus ?thesis by blast
+qed
+
+declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
+
+lemma finfun_rec_upd [simp]:
+  "finfun_rec cnst upd (f(\<^sup>f a' := b')) = upd a' b' (finfun_rec cnst upd f)"
+proof -
+  obtain b where b: "b = finfun_default f" by auto
+  let ?the = "\<lambda>f g. f = Abs_finfun (map_default b g) \<and> finite (dom g) \<and> b \<notin> ran g"
+  obtain g where g: "g = The (?the f)" by blast
+  obtain y where f: "f = Abs_finfun y" and y: "y \<in> finfun" by (cases f)
+  from f y b have bfin: "finite {a. y a \<noteq> b}" by(simp add: finfun_default_def finite_finfun_default_aux)
+
+  let ?g = "(\<lambda>a. Some (y a)) |` {a. y a \<noteq> b}"
+  from bfin have fing: "finite (dom ?g)" by auto
+  have bran: "b \<notin> ran ?g" by(auto simp add: ran_def restrict_map_def)
+  have yg: "y = map_default b ?g" by simp
+  have gg: "g = ?g" unfolding g
+  proof(rule the_equality)
+    from f y bfin show "?the f ?g"
+      by(auto)(simp add: restrict_map_def ran_def split: split_if_asm)
+  next
+    fix g'
+    assume "?the f g'"
+    hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
+      and eq: "Abs_finfun (map_default b ?g) = Abs_finfun (map_default b g')" using f yg by auto
+    from fin' fing have "map_default b ?g \<in> finfun" "map_default b g' \<in> finfun" by(blast intro: map_default_in_finfun)+
+    with eq have "map_default b ?g = map_default b g'" by simp
+    with fing bran fin' ran' show "g' = ?g" by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
+  qed
+
+  show ?thesis
+  proof(cases "b' = b")
+    case True
+    note b'b = True
+
+    let ?g' = "(\<lambda>a. Some ((y(a' := b)) a)) |` {a. (y(a' := b)) a \<noteq> b}"
+    from bfin b'b have fing': "finite (dom ?g')"
+      by(auto simp add: Collect_conj_eq Collect_imp_eq intro: finite_subset)
+    have brang': "b \<notin> ran ?g'" by(auto simp add: ran_def restrict_map_def)
+
+    let ?b' = "\<lambda>a. case ?g' a of None \<Rightarrow> b | Some b \<Rightarrow> b"
+    let ?b = "map_default b ?g"
+    from upd_left_comm upd_left_comm fing'
+    have "fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g') = fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')"
+      by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b b map_default_def)
+    also interpret gwf: fun_left_comm "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
+    have "fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g') = upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))"
+    proof(cases "y a' = b")
+      case True
+      with b'b have g': "?g' = ?g" by(auto simp add: restrict_map_def intro: ext)
+      from True have a'ndomg: "a' \<notin> dom ?g" by auto
+      from f b'b b show ?thesis unfolding g'
+        by(subst map_default_update_const[OF fing a'ndomg map_le_refl, symmetric]) simp
+    next
+      case False
+      hence domg: "dom ?g = insert a' (dom ?g')" by auto
+      from False b'b have a'ndomg': "a' \<notin> dom ?g'" by auto
+      have "fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g')) = 
+            upd a' (?b a') (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'))"
+        using fing' a'ndomg' unfolding b'b by(rule gwf.fold_insert)
+      hence "upd a' b (fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g'))) =
+             upd a' b (upd a' (?b a') (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g')))" by simp
+      also from b'b have g'leg: "?g' \<subseteq>\<^sub>m ?g" by(auto simp add: restrict_map_def map_le_def)
+      note map_default_update_twice[OF fing' a'ndomg' this, of b "?b a'" b]
+      also note map_default_update_const[OF fing' a'ndomg' g'leg, of b]
+      finally show ?thesis unfolding b'b domg[unfolded b'b] by(rule sym)
+    qed
+    also have "The (?the (f(\<^sup>f a' := b'))) = ?g'"
+    proof(rule the_equality)
+      from f y b b'b brang' fing' show "?the (f(\<^sup>f a' := b')) ?g'"
+        by(auto simp del: fun_upd_apply simp add: finfun_update_def)
+    next
+      fix g'
+      assume "?the (f(\<^sup>f a' := b')) g'"
+      hence fin': "finite (dom g')" and ran': "b \<notin> ran g'"
+        and eq: "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')" 
+        by(auto simp del: fun_upd_apply)
+      from fin' fing' have "map_default b g' \<in> finfun" "map_default b ?g' \<in> finfun"
+        by(blast intro: map_default_in_finfun)+
+      with eq f b'b b have "map_default b ?g' = map_default b g'"
+        by(simp del: fun_upd_apply add: finfun_update_def)
+      with fing' brang' fin' ran' show "g' = ?g'"
+        by(rule map_default_inject[OF disjI2[OF refl], THEN sym])
+    qed
+    ultimately show ?thesis unfolding finfun_rec_def Let_def b gg[unfolded g b] using bfin b'b b
+      by(simp only: finfun_default_update_const map_default_def)
+  next
+    case False
+    note b'b = this
+    let ?g' = "?g(a' \<mapsto> b')"
+    let ?b' = "map_default b ?g'"
+    let ?b = "map_default b ?g"
+    from fing have fing': "finite (dom ?g')" by auto
+    from bran b'b have bnrang': "b \<notin> ran ?g'" by(auto simp add: ran_def)
+    have ffmg': "map_default b ?g' = y(a' := b')" by(auto intro: ext simp add: map_default_def restrict_map_def)
+    with f y have f_Abs: "f(\<^sup>f a' := b') = Abs_finfun (map_default b ?g')" by(auto simp add: finfun_update_def)
+    have g': "The (?the (f(\<^sup>f a' := b'))) = ?g'"
+    proof
+      from fing' bnrang' f_Abs show "?the (f(\<^sup>f a' := b')) ?g'" by(auto simp add: finfun_update_def restrict_map_def)
+    next
+      fix g' assume "?the (f(\<^sup>f a' := b')) g'"
+      hence f': "f(\<^sup>f a' := b') = Abs_finfun (map_default b g')"
+        and fin': "finite (dom g')" and brang': "b \<notin> ran g'" by auto
+      from fing' fin' have "map_default b ?g' \<in> finfun" "map_default b g' \<in> finfun"
+        by(auto intro: map_default_in_finfun)
+      with f' f_Abs have "map_default b g' = map_default b ?g'" by simp
+      with fin' brang' fing' bnrang' show "g' = ?g'"
+        by(rule map_default_inject[OF disjI2[OF refl]])
+    qed
+    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}))"
+      by auto
+    show ?thesis
+    proof(cases "y a' = b")
+      case True
+      hence a'ndomg: "a' \<notin> dom ?g" by auto
+      from f y b'b True have yff: "y = map_default b (?g' |` dom ?g)"
+        by(auto simp add: restrict_map_def map_default_def intro!: ext)
+      hence f': "f = Abs_finfun (map_default b (?g' |` dom ?g))" using f by simp
+      interpret g'wf: fun_left_comm "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
+      from upd_left_comm upd_left_comm fing
+      have "fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g) = fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)"
+        by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b True map_default_def)
+      thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric]
+        unfolding g' g[symmetric] gg g'wf.fold_insert[OF fing a'ndomg, of "cnst b", folded dom]
+        by -(rule arg_cong2[where f="upd a'"], simp_all add: map_default_def)
+    next
+      case False
+      hence "insert a' (dom ?g) = dom ?g" by auto
+      moreover {
+        let ?g'' = "?g(a' := None)"
+        let ?b'' = "map_default b ?g''"
+        from False have domg: "dom ?g = insert a' (dom ?g'')" by auto
+        from False have a'ndomg'': "a' \<notin> dom ?g''" by auto
+        have fing'': "finite (dom ?g'')" by(rule finite_subset[OF _ fing]) auto
+        have bnrang'': "b \<notin> ran ?g''" by(auto simp add: ran_def restrict_map_def)
+        interpret gwf: fun_left_comm "\<lambda>a. upd a (?b a)" by(rule upd_left_comm)
+        interpret g'wf: fun_left_comm "\<lambda>a. upd a (?b' a)" by(rule upd_left_comm)
+        have "upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (insert a' (dom ?g''))) =
+              upd a' b' (upd a' (?b a') (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')))"
+          unfolding gwf.fold_insert[OF fing'' a'ndomg''] f ..
+        also have g''leg: "?g |` dom ?g'' \<subseteq>\<^sub>m ?g" by(auto simp add: map_le_def)
+        have "dom (?g |` dom ?g'') = dom ?g''" by auto
+        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",
+                                     unfolded this, OF fing'' a'ndomg'' g''leg]
+        also have b': "b' = ?b' a'" by(auto simp add: map_default_def)
+        from upd_left_comm upd_left_comm fing''
+        have "fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'') = fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g'')"
+          by(rule finite_rec_cong1)(auto simp add: restrict_map_def b'b map_default_def)
+        with b' have "upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g'')) =
+                     upd a' (?b' a') (fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g''))" by simp
+        also note g'wf.fold_insert[OF fing'' a'ndomg'', symmetric]
+        finally have "upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g)) =
+                   fold (\<lambda>a. upd a (?b' a)) (cnst b) (dom ?g)"
+          unfolding domg . }
+      ultimately have "fold (\<lambda>a. upd a (?b' a)) (cnst b) (insert a' (dom ?g)) =
+                    upd a' b' (fold (\<lambda>a. upd a (?b a)) (cnst b) (dom ?g))" by simp
+      thus ?thesis unfolding finfun_rec_def Let_def finfun_default_update_const b[symmetric] g[symmetric] g' dom[symmetric]
+        using b'b gg by(simp add: map_default_insert)
+    qed
+  qed
+qed
+
+declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
+
+end
+
+locale finfun_rec_wf = finfun_rec_wf_aux + 
+  assumes const_update_all:
+  "finite (UNIV :: 'a set) \<Longrightarrow> fold (\<lambda>a. upd a b') (cnst b) (UNIV :: 'a set) = cnst b'"
+begin
+
+declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
+
+lemma finfun_rec_const [simp]:
+  "finfun_rec cnst upd (\<lambda>\<^isup>f c) = cnst c"
+proof(cases "finite (UNIV :: 'a set)")
+  case False
+  hence "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = c" by(simp add: finfun_default_const)
+  moreover have "(THE g :: 'a \<rightharpoonup> 'b. (\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g) = empty"
+  proof
+    show "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c empty) \<and> finite (dom empty) \<and> c \<notin> ran empty"
+      by(auto simp add: finfun_const_def)
+  next
+    fix g :: "'a \<rightharpoonup> 'b"
+    assume "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c g) \<and> finite (dom g) \<and> c \<notin> ran g"
+    hence g: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default c g)" and fin: "finite (dom g)" and ran: "c \<notin> ran g" by blast+
+    from g map_default_in_finfun[OF fin, of c] have "map_default c g = (\<lambda>a. c)"
+      by(simp add: finfun_const_def)
+    moreover have "map_default c empty = (\<lambda>a. c)" by simp
+    ultimately show "g = empty" by-(rule map_default_inject[OF disjI2[OF refl] fin ran], auto)
+  qed
+  ultimately show ?thesis by(simp add: finfun_rec_def)
+next
+  case True
+  hence default: "finfun_default ((\<lambda>\<^isup>f c) :: 'a \<Rightarrow>\<^isub>f 'b) = arbitrary" by(simp add: finfun_default_const)
+  let ?the = "\<lambda>g :: 'a \<rightharpoonup> 'b. (\<lambda>\<^isup>f c) = Abs_finfun (map_default arbitrary g) \<and> finite (dom g) \<and> arbitrary \<notin> ran g"
+  show ?thesis
+  proof(cases "c = arbitrary")
+    case True
+    have the: "The ?the = empty"
+    proof
+      from True show "?the empty" by(auto simp add: finfun_const_def)
+    next
+      fix g'
+      assume "?the g'"
+      hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default arbitrary g')"
+        and fin: "finite (dom g')" and g: "arbitrary \<notin> ran g'" by simp_all
+      from fin have "map_default arbitrary g' \<in> finfun" by(rule map_default_in_finfun)
+      with fg have "map_default arbitrary g' = (\<lambda>a. c)"
+        by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
+      with True show "g' = empty"
+        by -(rule map_default_inject(2)[OF _ fin g], auto)
+    qed
+    show ?thesis unfolding finfun_rec_def using `finite UNIV` True
+      unfolding Let_def the default by(simp)
+  next
+    case False
+    have the: "The ?the = (\<lambda>a :: 'a. Some c)"
+    proof
+      from False True show "?the (\<lambda>a :: 'a. Some c)"
+        by(auto simp add: map_default_def_raw finfun_const_def dom_def ran_def)
+    next
+      fix g' :: "'a \<rightharpoonup> 'b"
+      assume "?the g'"
+      hence fg: "(\<lambda>\<^isup>f c) = Abs_finfun (map_default arbitrary g')"
+        and fin: "finite (dom g')" and g: "arbitrary \<notin> ran g'" by simp_all
+      from fin have "map_default arbitrary g' \<in> finfun" by(rule map_default_in_finfun)
+      with fg have "map_default arbitrary g' = (\<lambda>a. c)"
+        by(auto simp add: finfun_const_def intro: Abs_finfun_inject[THEN iffD1])
+      with True False show "g' = (\<lambda>a::'a. Some c)"
+        by -(rule map_default_inject(2)[OF _ fin g], auto simp add: dom_def ran_def map_default_def_raw)
+    qed
+    show ?thesis unfolding finfun_rec_def using True False
+      unfolding Let_def the default by(simp add: dom_def map_default_def const_update_all)
+  qed
+qed
+
+declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
+
+end
+
+subsection {* Weak induction rule and case analysis for FinFuns *}
+
+declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
+
+lemma finfun_weak_induct [consumes 0, case_names const update]:
+  assumes const: "\<And>b. P (\<lambda>\<^isup>f b)"
+  and update: "\<And>f a b. P f \<Longrightarrow> P (f(\<^sup>f a := b))"
+  shows "P x"
+proof(induct x rule: Abs_finfun_induct)
+  case (Abs_finfun y)
+  then obtain b where "finite {a. y a \<noteq> b}" unfolding finfun_def by blast
+  thus ?case using `y \<in> finfun`
+  proof(induct x\<equiv>"{a. y a \<noteq> b}" arbitrary: y rule: finite_induct)
+    case empty
+    hence "\<And>a. y a = b" by blast
+    hence "y = (\<lambda>a. b)" by(auto intro: ext)
+    hence "Abs_finfun y = finfun_const b" unfolding finfun_const_def by simp
+    thus ?case by(simp add: const)
+  next
+    case (insert a A)
+    note IH = `\<And>y. \<lbrakk> y \<in> finfun; A = {a. y a \<noteq> b} \<rbrakk> \<Longrightarrow> P (Abs_finfun y)`
+    note y = `y \<in> finfun`
+    with `insert a A = {a. y a \<noteq> b}` `a \<notin> A`
+    have "y(a := b) \<in> finfun" "A = {a'. (y(a := b)) a' \<noteq> b}" by auto
+    from IH[OF this] have "P (finfun_update (Abs_finfun (y(a := b))) a (y a))" by(rule update)
+    thus ?case using y unfolding finfun_update_def by simp
+  qed
+qed
+
+declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
+
+lemma finfun_exhaust_disj: "(\<exists>b. x = finfun_const b) \<or> (\<exists>f a b. x = finfun_update f a b)"
+by(induct x rule: finfun_weak_induct) blast+
+
+lemma finfun_exhaust:
+  obtains b where "x = (\<lambda>\<^isup>f b)"
+        | f a b where "x = f(\<^sup>f a := b)"
+by(atomize_elim)(rule finfun_exhaust_disj)
+
+lemma finfun_rec_unique:
+  fixes f :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'c"
+  assumes c: "\<And>c. f (\<lambda>\<^isup>f c) = cnst c"
+  and u: "\<And>g a b. f (g(\<^sup>f a := b)) = upd g a b (f g)"
+  and c': "\<And>c. f' (\<lambda>\<^isup>f c) = cnst c"
+  and u': "\<And>g a b. f' (g(\<^sup>f a := b)) = upd g a b (f' g)"
+  shows "f = f'"
+proof
+  fix g :: "'a \<Rightarrow>\<^isub>f 'b"
+  show "f g = f' g"
+    by(induct g rule: finfun_weak_induct)(auto simp add: c u c' u')
+qed
+
+
+subsection {* Function application *}
+
+definition finfun_apply :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow> 'b" ("_\<^sub>f" [1000] 1000)
+where [code del]: "finfun_apply = (\<lambda>f a. finfun_rec (\<lambda>b. b) (\<lambda>a' b c. if (a = a') then b else c) f)"
+
+interpretation finfun_apply_aux: finfun_rec_wf_aux "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
+by(unfold_locales) auto
+
+interpretation finfun_apply: finfun_rec_wf "\<lambda>b. b" "\<lambda>a' b c. if (a = a') then b else c"
+proof(unfold_locales)
+  fix b' b :: 'a
+  assume fin: "finite (UNIV :: 'b set)"
+  { fix A :: "'b set"
+    interpret fun_left_comm "\<lambda>a'. If (a = a') b'" by(rule finfun_apply_aux.upd_left_comm)
+    from fin have "finite A" by(auto intro: finite_subset)
+    hence "fold (\<lambda>a'. If (a = a') b') b A = (if a \<in> A then b' else b)"
+      by induct auto }
+  from this[of UNIV] show "fold (\<lambda>a'. If (a = a') b') b UNIV = b'" by simp
+qed
+
+lemma finfun_const_apply [simp, code]: "(\<lambda>\<^isup>f b)\<^sub>f a = b"
+by(simp add: finfun_apply_def)
+
+lemma finfun_upd_apply: "f(\<^sup>fa := b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')"
+  and finfun_upd_apply_code [code]: "(finfun_update_code f a b)\<^sub>f a' = (if a = a' then b else f\<^sub>f a')"
+by(simp_all add: finfun_apply_def)
+
+lemma finfun_upd_apply_same [simp]:
+  "f(\<^sup>fa := b)\<^sub>f a = b"
+by(simp add: finfun_upd_apply)
+
+lemma finfun_upd_apply_other [simp]:
+  "a \<noteq> a' \<Longrightarrow> f(\<^sup>fa := b)\<^sub>f a' = f\<^sub>f a'"
+by(simp add: finfun_upd_apply)
+
+declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
+
+lemma finfun_apply_Rep_finfun:
+  "finfun_apply = Rep_finfun"
+proof(rule finfun_rec_unique)
+  fix c show "Rep_finfun (\<lambda>\<^isup>f c) = (\<lambda>a. c)" by(auto simp add: finfun_const_def)
+next
+  fix g a b show "Rep_finfun g(\<^sup>f a := b) = (\<lambda>c. if c = a then b else Rep_finfun g c)"
+    by(auto simp add: finfun_update_def fun_upd_finfun Abs_finfun_inverse Rep_finfun intro: ext)
+qed(auto intro: ext)
+
+lemma finfun_ext: "(\<And>a. f\<^sub>f a = g\<^sub>f a) \<Longrightarrow> f = g"
+by(auto simp add: finfun_apply_Rep_finfun Rep_finfun_inject[symmetric] simp del: Rep_finfun_inject intro: ext)
+
+declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
+
+lemma expand_finfun_eq: "(f = g) = (f\<^sub>f = g\<^sub>f)"
+by(auto intro: finfun_ext)
+
+lemma finfun_const_inject [simp]: "(\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b') \<equiv> b = b'"
+by(simp add: expand_finfun_eq expand_fun_eq)
+
+lemma finfun_const_eq_update:
+  "((\<lambda>\<^isup>f b) = f(\<^sup>f a := b')) = (b = b' \<and> (\<forall>a'. a \<noteq> a' \<longrightarrow> f\<^sub>f a' = b))"
+by(auto simp add: expand_finfun_eq expand_fun_eq finfun_upd_apply)
+
+subsection {* Function composition *}
+
+definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'a \<Rightarrow> 'c \<Rightarrow>\<^isub>f 'b" (infixr "\<circ>\<^isub>f" 55)
+where [code del]: "g \<circ>\<^isub>f f  = finfun_rec (\<lambda>b. (\<lambda>\<^isup>f g b)) (\<lambda>a b c. c(\<^sup>f a := g b)) f"
+
+interpretation finfun_comp_aux: finfun_rec_wf_aux "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))"
+by(unfold_locales)(auto simp add: finfun_upd_apply intro: finfun_ext)
+
+interpretation finfun_comp: finfun_rec_wf "(\<lambda>b. (\<lambda>\<^isup>f g b))" "(\<lambda>a b c. c(\<^sup>f a := g b))"
+proof
+  fix b' b :: 'a
+  assume fin: "finite (UNIV :: 'c set)"
+  { fix A :: "'c set"
+    from fin have "finite A" by(auto intro: finite_subset)
+    hence "fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) A =
+      Abs_finfun (\<lambda>a. if a \<in> A then g b' else g b)"
+      by induct (simp_all add: finfun_const_def, auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite expand_fun_eq fin) }
+  from this[of UNIV] show "fold (\<lambda>(a :: 'c) c. c(\<^sup>f a := g b')) (\<lambda>\<^isup>f g b) UNIV = (\<lambda>\<^isup>f g b')"
+    by(simp add: finfun_const_def)
+qed
+
+lemma finfun_comp_const [simp, code]:
+  "g \<circ>\<^isub>f (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f g c)"
+by(simp add: finfun_comp_def)
+
+lemma finfun_comp_update [simp]: "g \<circ>\<^isub>f (f(\<^sup>f a := b)) = (g \<circ>\<^isub>f f)(\<^sup>f a := g b)"
+  and finfun_comp_update_code [code]: "g \<circ>\<^isub>f (finfun_update_code f a b) = finfun_update_code (g \<circ>\<^isub>f f) a (g b)"
+by(simp_all add: finfun_comp_def)
+
+lemma finfun_comp_apply [simp]:
+  "(g \<circ>\<^isub>f f)\<^sub>f = g \<circ> f\<^sub>f"
+by(induct f rule: finfun_weak_induct)(auto simp add: finfun_upd_apply intro: ext)
+
+lemma finfun_comp_comp_collapse [simp]: "f \<circ>\<^isub>f g \<circ>\<^isub>f h = (f o g) \<circ>\<^isub>f h"
+by(induct h rule: finfun_weak_induct) simp_all
+
+lemma finfun_comp_const1 [simp]: "(\<lambda>x. c) \<circ>\<^isub>f f = (\<lambda>\<^isup>f c)"
+by(induct f rule: finfun_weak_induct)(auto intro: finfun_ext simp add: finfun_upd_apply)
+
+lemma finfun_comp_id1 [simp]: "(\<lambda>x. x) \<circ>\<^isub>f f = f" "id \<circ>\<^isub>f f = f"
+by(induct f rule: finfun_weak_induct) auto
+
+declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
+
+lemma finfun_comp_conv_comp: "g \<circ>\<^isub>f f = Abs_finfun (g \<circ> finfun_apply f)"
+proof -
+  have "(\<lambda>f. g \<circ>\<^isub>f f) = (\<lambda>f. Abs_finfun (g \<circ> finfun_apply f))"
+  proof(rule finfun_rec_unique)
+    { fix c show "Abs_finfun (g \<circ> (\<lambda>\<^isup>f c)\<^sub>f) = (\<lambda>\<^isup>f g c)"
+        by(simp add: finfun_comp_def o_def)(simp add: finfun_const_def) }
+    { fix g' a b show "Abs_finfun (g \<circ> g'(\<^sup>f a := b)\<^sub>f) = (Abs_finfun (g \<circ> g'\<^sub>f))(\<^sup>f a := g b)"
+      proof -
+        obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
+        moreover hence "(g \<circ> g'\<^sub>f) \<in> finfun" by(simp add: finfun_apply_Rep_finfun finfun_left_compose)
+        moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto intro: ext)
+        ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def finfun_apply_Rep_finfun)
+      qed }
+  qed auto
+  thus ?thesis by(auto simp add: expand_fun_eq)
+qed
+
+declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
+
+
+
+definition finfun_comp2 :: "'b \<Rightarrow>\<^isub>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c" (infixr "\<^sub>f\<circ>" 55)
+where [code del]: "finfun_comp2 g f = Abs_finfun (Rep_finfun g \<circ> f)"
+
+declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
+
+lemma finfun_comp2_const [code, simp]: "finfun_comp2 (\<lambda>\<^isup>f c) f = (\<lambda>\<^isup>f c)"
+by(simp add: finfun_comp2_def finfun_const_def comp_def)
+
+lemma finfun_comp2_update:
+  assumes inj: "inj f"
+  shows "finfun_comp2 (g(\<^sup>f b := c)) f = (if b \<in> range f then (finfun_comp2 g f)(\<^sup>f inv f b := c) else finfun_comp2 g f)"
+proof(cases "b \<in> range f")
+  case True
+  from inj have "\<And>x. (Rep_finfun g)(f x := c) \<circ> f = (Rep_finfun g \<circ> f)(x := c)" by(auto intro!: ext dest: injD)
+  with inj True show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def finfun_right_compose)
+next
+  case False
+  hence "(Rep_finfun g)(b := c) \<circ> f = Rep_finfun g \<circ> f" by(auto simp add: expand_fun_eq)
+  with False show ?thesis by(auto simp add: finfun_comp2_def finfun_update_def)
+qed
+
+declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
+
+subsection {* A type class for computing the cardinality of a type's universe *}
+
+class card_UNIV = 
+  fixes card_UNIV :: "'a itself \<Rightarrow> nat"
+  assumes card_UNIV: "card_UNIV x = card (UNIV :: 'a set)"
+begin
+
+lemma card_UNIV_neq_0_finite_UNIV:
+  "card_UNIV x \<noteq> 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
+by(simp add: card_UNIV card_eq_0_iff)
+
+lemma card_UNIV_ge_0_finite_UNIV:
+  "card_UNIV x > 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
+by(auto simp add: card_UNIV intro: card_ge_0_finite finite_UNIV_card_ge_0)
+
+lemma card_UNIV_eq_0_infinite_UNIV:
+  "card_UNIV x = 0 \<longleftrightarrow> infinite (UNIV :: 'a set)"
+by(simp add: card_UNIV card_eq_0_iff)
+
+definition is_list_UNIV :: "'a list \<Rightarrow> bool"
+where "is_list_UNIV xs = (let c = card_UNIV (TYPE('a)) in if c = 0 then False else size (remdups xs) = c)"
+
+lemma is_list_UNIV_iff:
+  fixes xs :: "'a list"
+  shows "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
+proof
+  assume "is_list_UNIV xs"
+  hence c: "card_UNIV (TYPE('a)) > 0" and xs: "size (remdups xs) = card_UNIV (TYPE('a))"
+    unfolding is_list_UNIV_def by(simp_all add: Let_def split: split_if_asm)
+  from c have fin: "finite (UNIV :: 'a set)" by(auto simp add: card_UNIV_ge_0_finite_UNIV)
+  have "card (set (remdups xs)) = size (remdups xs)" by(subst distinct_card) auto
+  also note set_remdups
+  finally show "set xs = UNIV" using fin unfolding xs card_UNIV by-(rule card_eq_UNIV_imp_eq_UNIV)
+next
+  assume xs: "set xs = UNIV"
+  from finite_set[of xs] have fin: "finite (UNIV :: 'a set)" unfolding xs .
+  hence "card_UNIV (TYPE ('a)) \<noteq> 0" unfolding card_UNIV_neq_0_finite_UNIV .
+  moreover have "size (remdups xs) = card (set (remdups xs))"
+    by(subst distinct_card) auto
+  ultimately show "is_list_UNIV xs" using xs by(simp add: is_list_UNIV_def Let_def card_UNIV)
+qed
+
+lemma card_UNIV_eq_0_is_list_UNIV_False:
+  assumes cU0: "card_UNIV x = 0"
+  shows "is_list_UNIV = (\<lambda>xs. False)"
+proof(rule ext)
+  fix xs :: "'a list"
+  from cU0 have "infinite (UNIV :: 'a set)"
+    by(auto simp only: card_UNIV_eq_0_infinite_UNIV)
+  moreover have "finite (set xs)" by(rule finite_set)
+  ultimately have "(UNIV :: 'a set) \<noteq> set xs" by(auto simp del: finite_set)
+  thus "is_list_UNIV xs = False" unfolding is_list_UNIV_iff by simp
+qed
+
+end
+
+subsection {* Instantiations for @{text "card_UNIV"} *}
+
+subsubsection {* @{typ "nat"} *}
+
+instantiation nat :: card_UNIV begin
+
+definition card_UNIV_nat_def:
+  "card_UNIV_class.card_UNIV = (\<lambda>a :: nat itself. 0)"
+
+instance proof
+  fix x :: "nat itself"
+  show "card_UNIV x = card (UNIV :: nat set)"
+    unfolding card_UNIV_nat_def by simp
+qed
+
+end
+
+subsubsection {* @{typ "int"} *}
+
+instantiation int :: card_UNIV begin
+
+definition card_UNIV_int_def:
+  "card_UNIV_class.card_UNIV = (\<lambda>a :: int itself. 0)"
+
+instance proof
+  fix x :: "int itself"
+  show "card_UNIV x = card (UNIV :: int set)"
+    unfolding card_UNIV_int_def by simp
+qed
+
+end
+
+subsubsection {* @{typ "'a list"} *}
+
+instantiation list :: (type) card_UNIV begin
+
+definition card_UNIV_list_def:
+  "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a list itself. 0)"
+
+instance proof
+  fix x :: "'a list itself"
+  show "card_UNIV x = card (UNIV :: 'a list set)"
+    unfolding card_UNIV_list_def by(simp add: infinite_UNIV_listI)
+qed
+
+end
+
+subsubsection {* @{typ "unit"} *}
+
+lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
+  unfolding UNIV_unit by simp
+
+instantiation unit :: card_UNIV begin
+
+definition card_UNIV_unit_def: 
+  "card_UNIV_class.card_UNIV = (\<lambda>a :: unit itself. 1)"
+
+instance proof
+  fix x :: "unit itself"
+  show "card_UNIV x = card (UNIV :: unit set)"
+    by(simp add: card_UNIV_unit_def card_UNIV_unit)
+qed
+
+end
+
+subsubsection {* @{typ "bool"} *}
+
+lemma card_UNIV_bool: "card (UNIV :: bool set) = 2"
+  unfolding UNIV_bool by simp
+
+instantiation bool :: card_UNIV begin
+
+definition card_UNIV_bool_def: 
+  "card_UNIV_class.card_UNIV = (\<lambda>a :: bool itself. 2)"
+
+instance proof
+  fix x :: "bool itself"
+  show "card_UNIV x = card (UNIV :: bool set)"
+    by(simp add: card_UNIV_bool_def card_UNIV_bool)
+qed
+
+end
+
+subsubsection {* @{typ "char"} *}
+
+lemma card_UNIV_char: "card (UNIV :: char set) = 256"
+proof -
+  from enum_distinct
+  have "card (set (enum :: char list)) = length (enum :: char list)"
+    by -(rule distinct_card)
+  also have "set enum = (UNIV :: char set)" by auto
+  also note enum_char
+  finally show ?thesis by simp
+qed
+
+instantiation char :: card_UNIV begin
+
+definition card_UNIV_char_def: 
+  "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
+
+instance proof
+  fix x :: "char itself"
+  show "card_UNIV x = card (UNIV :: char set)"
+    by(simp add: card_UNIV_char_def card_UNIV_char)
+qed
+
+end
+
+subsubsection {* @{typ "'a \<times> 'b"} *}
+
+instantiation * :: (card_UNIV, card_UNIV) card_UNIV begin
+
+definition card_UNIV_product_def: 
+  "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
+
+instance proof
+  fix x :: "('a \<times> 'b) itself"
+  show "card_UNIV x = card (UNIV :: ('a \<times> 'b) set)"
+    by(simp add: card_UNIV_product_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
+qed
+
+end
+
+subsubsection {* @{typ "'a + 'b"} *}
+
+instantiation "+" :: (card_UNIV, card_UNIV) card_UNIV begin
+
+definition card_UNIV_sum_def: 
+  "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
+                           in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
+
+instance proof
+  fix x :: "('a + 'b) itself"
+  show "card_UNIV x = card (UNIV :: ('a + 'b) set)"
+    by (auto simp add: card_UNIV_sum_def card_UNIV card_eq_0_iff UNIV_Plus_UNIV[symmetric] finite_Plus_iff Let_def card_Plus simp del: UNIV_Plus_UNIV dest!: card_ge_0_finite)
+qed
+
+end
+
+subsubsection {* @{typ "'a \<Rightarrow> 'b"} *}
+
+instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
+
+definition card_UNIV_fun_def: 
+  "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
+                           in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
+
+instance proof
+  fix x :: "('a \<Rightarrow> 'b) itself"
+
+  { assume "0 < card (UNIV :: 'a set)"
+    and "0 < card (UNIV :: 'b set)"
+    hence fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)"
+      by(simp_all only: card_ge_0_finite)
+    from finite_distinct_list[OF finb] obtain bs 
+      where bs: "set bs = (UNIV :: 'b set)" and distb: "distinct bs" by blast
+    from finite_distinct_list[OF fina] obtain as
+      where as: "set as = (UNIV :: 'a set)" and dista: "distinct as" by blast
+    have cb: "card (UNIV :: 'b set) = length bs"
+      unfolding bs[symmetric] distinct_card[OF distb] ..
+    have ca: "card (UNIV :: 'a set) = length as"
+      unfolding as[symmetric] distinct_card[OF dista] ..
+    let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (n_lists (length as) bs)"
+    have "UNIV = set ?xs"
+    proof(rule UNIV_eq_I)
+      fix f :: "'a \<Rightarrow> 'b"
+      from as have "f = the \<circ> map_of (zip as (map f as))"
+        by(auto simp add: map_of_zip_map intro: ext)
+      thus "f \<in> set ?xs" using bs by(auto simp add: set_n_lists)
+    qed
+    moreover have "distinct ?xs" unfolding distinct_map
+    proof(intro conjI distinct_n_lists distb inj_onI)
+      fix xs ys :: "'b list"
+      assume xs: "xs \<in> set (n_lists (length as) bs)"
+        and ys: "ys \<in> set (n_lists (length as) bs)"
+        and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)"
+      from xs ys have [simp]: "length xs = length as" "length ys = length as"
+        by(simp_all add: length_n_lists_elem)
+      have "map_of (zip as xs) = map_of (zip as ys)"
+      proof
+        fix x
+        from as bs have "\<exists>y. map_of (zip as xs) x = Some y" "\<exists>y. map_of (zip as ys) x = Some y"
+          by(simp_all add: map_of_zip_is_Some[symmetric])
+        with eq show "map_of (zip as xs) x = map_of (zip as ys) x"
+          by(auto dest: fun_cong[where x=x])
+      qed
+      with dista show "xs = ys" by(simp add: map_of_zip_inject)
+    qed
+    hence "card (set ?xs) = length ?xs" by(simp only: distinct_card)
+    moreover have "length ?xs = length bs ^ length as" by(simp add: length_n_lists)
+    ultimately have "card (UNIV :: ('a \<Rightarrow> 'b) set) = card (UNIV :: 'b set) ^ card (UNIV :: 'a set)"
+      using cb ca by simp }
+  moreover {
+    assume cb: "card (UNIV :: 'b set) = Suc 0"
+    then obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq)
+    have eq: "UNIV = {\<lambda>x :: 'a. b ::'b}"
+    proof(rule UNIV_eq_I)
+      fix x :: "'a \<Rightarrow> 'b"
+      { fix y
+        have "x y \<in> UNIV" ..
+        hence "x y = b" unfolding b by simp }
+      thus "x \<in> {\<lambda>x. b}" by(auto intro: ext)
+    qed
+    have "card (UNIV :: ('a \<Rightarrow> 'b) set) = Suc 0" unfolding eq by simp }
+  ultimately show "card_UNIV x = card (UNIV :: ('a \<Rightarrow> 'b) set)"
+    unfolding card_UNIV_fun_def card_UNIV Let_def
+    by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1)
+qed
+
+end
+
+subsubsection {* @{typ "'a option"} *}
+
+instantiation option :: (card_UNIV) card_UNIV
+begin
+
+definition card_UNIV_option_def: 
+  "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a option itself. let c = card_UNIV (TYPE('a))
+                           in if c \<noteq> 0 then Suc c else 0)"
+
+instance proof
+  fix x :: "'a option itself"
+  show "card_UNIV x = card (UNIV :: 'a option set)"
+    unfolding UNIV_option_conv
+    by(auto simp add: card_UNIV_option_def card_UNIV card_eq_0_iff Let_def intro: inj_Some dest: finite_imageD)
+      (subst card_insert_disjoint, auto simp add: card_eq_0_iff card_image inj_Some intro: finite_imageI card_ge_0_finite)
+qed
+
+end
+
+
+subsection {* Universal quantification *}
+
+definition finfun_All_except :: "'a list \<Rightarrow> 'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
+where [code del]: "finfun_All_except A P \<equiv> \<forall>a. a \<in> set A \<or> P\<^sub>f a"
+
+lemma finfun_All_except_const: "finfun_All_except A (\<lambda>\<^isup>f b) \<longleftrightarrow> b \<or> set A = UNIV"
+by(auto simp add: finfun_All_except_def)
+
+lemma finfun_All_except_const_finfun_UNIV_code [code]:
+  "finfun_All_except A (\<lambda>\<^isup>f b) = (b \<or> is_list_UNIV A)"
+by(simp add: finfun_All_except_const is_list_UNIV_iff)
+
+lemma finfun_All_except_update: 
+  "finfun_All_except A f(\<^sup>f a := b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
+by(fastsimp simp add: finfun_All_except_def finfun_upd_apply)
+
+lemma finfun_All_except_update_code [code]:
+  fixes a :: "'a :: card_UNIV"
+  shows "finfun_All_except A (finfun_update_code f a b) = ((a \<in> set A \<or> b) \<and> finfun_All_except (a # A) f)"
+by(simp add: finfun_All_except_update)
+
+definition finfun_All :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
+where "finfun_All = finfun_All_except []"
+
+lemma finfun_All_const [simp]: "finfun_All (\<lambda>\<^isup>f b) = b"
+by(simp add: finfun_All_def finfun_All_except_def)
+
+lemma finfun_All_update: "finfun_All f(\<^sup>f a := b) = (b \<and> finfun_All_except [a] f)"
+by(simp add: finfun_All_def finfun_All_except_update)
+
+lemma finfun_All_All: "finfun_All P = All P\<^sub>f"
+by(simp add: finfun_All_def finfun_All_except_def)
+
+
+definition finfun_Ex :: "'a \<Rightarrow>\<^isub>f bool \<Rightarrow> bool"
+where "finfun_Ex P = Not (finfun_All (Not \<circ>\<^isub>f P))"
+
+lemma finfun_Ex_Ex: "finfun_Ex P = Ex P\<^sub>f"
+unfolding finfun_Ex_def finfun_All_All by simp
+
+lemma finfun_Ex_const [simp]: "finfun_Ex (\<lambda>\<^isup>f b) = b"
+by(simp add: finfun_Ex_def)
+
+
+subsection {* A diagonal operator for FinFuns *}
+
+definition finfun_Diag :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c \<Rightarrow> 'a \<Rightarrow>\<^isub>f ('b \<times> 'c)" ("(1'(_,/ _')\<^sup>f)" [0, 0] 1000)
+where [code del]: "finfun_Diag f g = finfun_rec (\<lambda>b. Pair b \<circ>\<^isub>f g) (\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))) f"
+
+interpretation finfun_Diag_aux: finfun_rec_wf_aux "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))"
+by(unfold_locales)(simp_all add: expand_finfun_eq expand_fun_eq finfun_upd_apply)
+
+interpretation finfun_Diag: finfun_rec_wf "\<lambda>b. Pair b \<circ>\<^isub>f g" "\<lambda>a b c. c(\<^sup>f a := (b, g\<^sub>f a))"
+proof
+  fix b' b :: 'a
+  assume fin: "finite (UNIV :: 'c set)"
+  { fix A :: "'c set"
+    interpret fun_left_comm "\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))" by(rule finfun_Diag_aux.upd_left_comm)
+    from fin have "finite A" by(auto intro: finite_subset)
+    hence "fold (\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))) (Pair b \<circ>\<^isub>f g) A =
+      Abs_finfun (\<lambda>a. (if a \<in> A then b' else b, g\<^sub>f a))"
+      by(induct)(simp_all add: finfun_const_def finfun_comp_conv_comp o_def,
+                 auto simp add: finfun_update_def Abs_finfun_inverse_finite fun_upd_def Abs_finfun_inject_finite expand_fun_eq fin) }
+  from this[of UNIV] show "fold (\<lambda>a c. c(\<^sup>f a := (b', g\<^sub>f a))) (Pair b \<circ>\<^isub>f g) UNIV = Pair b' \<circ>\<^isub>f g"
+    by(simp add: finfun_const_def finfun_comp_conv_comp o_def)
+qed
+
+lemma finfun_Diag_const1: "(\<lambda>\<^isup>f b, g)\<^sup>f = Pair b \<circ>\<^isub>f g"
+by(simp add: finfun_Diag_def)
+
+text {*
+  Do not use @{thm finfun_Diag_const1} for the code generator because @{term "Pair b"} is injective, i.e. if @{term g} is free of redundant updates, there is no need to check for redundant updates as is done for @{text "\<circ>\<^isub>f"}.
+*}
+
+lemma finfun_Diag_const_code [code]:
+  "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
+  "(\<lambda>\<^isup>f b, g(\<^sup>f\<^sup>c a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>f\<^sup>c a := (b, c))"
+by(simp_all add: finfun_Diag_const1)
+
+lemma finfun_Diag_update1: "(f(\<^sup>f a := b), g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))"
+  and finfun_Diag_update1_code [code]: "(finfun_update_code f a b, g)\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))"
+by(simp_all add: finfun_Diag_def)
+
+lemma finfun_Diag_const2: "(f, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>b. (b, c)) \<circ>\<^isub>f f"
+by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
+
+lemma finfun_Diag_update2: "(f, g(\<^sup>f a := c))\<^sup>f = (f, g)\<^sup>f(\<^sup>f a := (f\<^sub>f a, c))"
+by(induct f rule: finfun_weak_induct)(auto intro!: finfun_ext simp add: finfun_upd_apply finfun_Diag_const1 finfun_Diag_update1)
+
+lemma finfun_Diag_const_const [simp]: "(\<lambda>\<^isup>f b, \<lambda>\<^isup>f c)\<^sup>f = (\<lambda>\<^isup>f (b, c))"
+by(simp add: finfun_Diag_const1)
+
+lemma finfun_Diag_const_update:
+  "(\<lambda>\<^isup>f b, g(\<^sup>f a := c))\<^sup>f = (\<lambda>\<^isup>f b, g)\<^sup>f(\<^sup>f a := (b, c))"
+by(simp add: finfun_Diag_const1)
+
+lemma finfun_Diag_update_const:
+  "(f(\<^sup>f a := b), \<lambda>\<^isup>f c)\<^sup>f = (f, \<lambda>\<^isup>f c)\<^sup>f(\<^sup>f a := (b, c))"
+by(simp add: finfun_Diag_def)
+
+lemma finfun_Diag_update_update:
+  "(f(\<^sup>f a := b), g(\<^sup>f a' := c))\<^sup>f = (if a = a' then (f, g)\<^sup>f(\<^sup>f a := (b, c)) else (f, g)\<^sup>f(\<^sup>f a := (b, g\<^sub>f a))(\<^sup>f a' := (f\<^sub>f a', c)))"
+by(auto simp add: finfun_Diag_update1 finfun_Diag_update2)
+
+lemma finfun_Diag_apply [simp]: "(f, g)\<^sup>f\<^sub>f = (\<lambda>x. (f\<^sub>f x, g\<^sub>f x))"
+by(induct f rule: finfun_weak_induct)(auto simp add: finfun_Diag_const1 finfun_Diag_update1 finfun_upd_apply intro: ext)
+
+declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
+
+lemma finfun_Diag_conv_Abs_finfun:
+  "(f, g)\<^sup>f = Abs_finfun ((\<lambda>x. (Rep_finfun f x, Rep_finfun g x)))"
+proof -
+  have "(\<lambda>f :: 'a \<Rightarrow>\<^isub>f 'b. (f, g)\<^sup>f) = (\<lambda>f. Abs_finfun ((\<lambda>x. (Rep_finfun f x, Rep_finfun g x))))"
+  proof(rule finfun_rec_unique)
+    { fix c show "Abs_finfun (\<lambda>x. (Rep_finfun (\<lambda>\<^isup>f c) x, Rep_finfun g x)) = Pair c \<circ>\<^isub>f g"
+        by(simp add: finfun_comp_conv_comp finfun_apply_Rep_finfun o_def finfun_const_def) }
+    { fix g' a b
+      show "Abs_finfun (\<lambda>x. (Rep_finfun g'(\<^sup>f a := b) x, Rep_finfun g x)) =
+            (Abs_finfun (\<lambda>x. (Rep_finfun g' x, Rep_finfun g x)))(\<^sup>f a := (b, g\<^sub>f a))"
+        by(auto simp add: finfun_update_def expand_fun_eq finfun_apply_Rep_finfun simp del: fun_upd_apply) simp }
+  qed(simp_all add: finfun_Diag_const1 finfun_Diag_update1)
+  thus ?thesis by(auto simp add: expand_fun_eq)
+qed
+
+declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
+
+lemma finfun_Diag_eq: "(f, g)\<^sup>f = (f', g')\<^sup>f \<longleftrightarrow> f = f' \<and> g = g'"
+by(auto simp add: expand_finfun_eq expand_fun_eq)
+
+definition finfun_fst :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
+where [code]: "finfun_fst f = fst \<circ>\<^isub>f f"
+
+lemma finfun_fst_const: "finfun_fst (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f fst bc)"
+by(simp add: finfun_fst_def)
+
+lemma finfun_fst_update: "finfun_fst (f(\<^sup>f a := bc)) = (finfun_fst f)(\<^sup>f a := fst bc)"
+  and finfun_fst_update_code: "finfun_fst (finfun_update_code f a bc) = (finfun_fst f)(\<^sup>f a := fst bc)"
+by(simp_all add: finfun_fst_def)
+
+lemma finfun_fst_comp_conv: "finfun_fst (f \<circ>\<^isub>f g) = (fst \<circ> f) \<circ>\<^isub>f g"
+by(simp add: finfun_fst_def)
+
+lemma finfun_fst_conv [simp]: "finfun_fst (f, g)\<^sup>f = f"
+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)
+
+lemma finfun_fst_conv_Abs_finfun: "finfun_fst = (\<lambda>f. Abs_finfun (fst o Rep_finfun f))"
+by(simp add: finfun_fst_def_raw finfun_comp_conv_comp finfun_apply_Rep_finfun)
+
+
+definition finfun_snd :: "'a \<Rightarrow>\<^isub>f ('b \<times> 'c) \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'c"
+where [code]: "finfun_snd f = snd \<circ>\<^isub>f f"
+
+lemma finfun_snd_const: "finfun_snd (\<lambda>\<^isup>f bc) = (\<lambda>\<^isup>f snd bc)"
+by(simp add: finfun_snd_def)
+
+lemma finfun_snd_update: "finfun_snd (f(\<^sup>f a := bc)) = (finfun_snd f)(\<^sup>f a := snd bc)"
+  and finfun_snd_update_code [code]: "finfun_snd (finfun_update_code f a bc) = (finfun_snd f)(\<^sup>f a := snd bc)"
+by(simp_all add: finfun_snd_def)
+
+lemma finfun_snd_comp_conv: "finfun_snd (f \<circ>\<^isub>f g) = (snd \<circ> f) \<circ>\<^isub>f g"
+by(simp add: finfun_snd_def)
+
+lemma finfun_snd_conv [simp]: "finfun_snd (f, g)\<^sup>f = g"
+apply(induct f rule: finfun_weak_induct)
+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)
+done
+
+lemma finfun_snd_conv_Abs_finfun: "finfun_snd = (\<lambda>f. Abs_finfun (snd o Rep_finfun f))"
+by(simp add: finfun_snd_def_raw finfun_comp_conv_comp finfun_apply_Rep_finfun)
+
+lemma finfun_Diag_collapse [simp]: "(finfun_fst f, finfun_snd f)\<^sup>f = f"
+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)
+
+subsection {* Currying for FinFuns *}
+
+definition finfun_curry :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b \<Rightarrow>\<^isub>f 'c"
+where [code del]: "finfun_curry = finfun_rec (finfun_const \<circ> finfun_const) (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c)))"
+
+interpretation finfun_curry_aux: finfun_rec_wf_aux "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))"
+apply(unfold_locales)
+apply(auto simp add: split_def finfun_update_twist finfun_upd_apply split_paired_all finfun_update_const_same)
+done
+
+declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
+
+interpretation finfun_curry: finfun_rec_wf "finfun_const \<circ> finfun_const" "\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))"
+proof(unfold_locales)
+  fix b' b :: 'b
+  assume fin: "finite (UNIV :: ('c \<times> 'a) set)"
+  hence fin1: "finite (UNIV :: 'c set)" and fin2: "finite (UNIV :: 'a set)"
+    unfolding UNIV_Times_UNIV[symmetric]
+    by(fastsimp dest: finite_cartesian_productD1 finite_cartesian_productD2)+
+  note [simp] = Abs_finfun_inverse_finite[OF fin] Abs_finfun_inverse_finite[OF fin1] Abs_finfun_inverse_finite[OF fin2]
+  { fix A :: "('c \<times> 'a) set"
+    interpret fun_left_comm "\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b'"
+      by(rule finfun_curry_aux.upd_left_comm)
+    from fin have "finite A" by(auto intro: finite_subset)
+    hence "fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b') ((finfun_const \<circ> finfun_const) b) A = Abs_finfun (\<lambda>a. Abs_finfun (\<lambda>b''. if (a, b'') \<in> A then b' else b))"
+      by induct (simp_all, auto simp add: finfun_update_def finfun_const_def split_def finfun_apply_Rep_finfun intro!: arg_cong[where f="Abs_finfun"] ext) }
+  from this[of UNIV]
+  show "fold (\<lambda>a :: 'c \<times> 'a. (\<lambda>(a, b) c f. f(\<^sup>f a := (f\<^sub>f a)(\<^sup>f b := c))) a b') ((finfun_const \<circ> finfun_const) b) UNIV = (finfun_const \<circ> finfun_const) b'"
+    by(simp add: finfun_const_def)
+qed
+
+declare finfun_simp [simp del] finfun_iff [iff del] finfun_intro [rule del]
+
+lemma finfun_curry_const [simp, code]: "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
+by(simp add: finfun_curry_def)
+
+lemma finfun_curry_update [simp]:
+  "finfun_curry (f(\<^sup>f (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
+  and finfun_curry_update_code [code]:
+  "finfun_curry (f(\<^sup>f\<^sup>c (a, b) := c)) = (finfun_curry f)(\<^sup>f a := ((finfun_curry f)\<^sub>f a)(\<^sup>f b := c))"
+by(simp_all add: finfun_curry_def)
+
+declare finfun_simp [simp] finfun_iff [iff] finfun_intro [intro]
+
+lemma finfun_Abs_finfun_curry: assumes fin: "f \<in> finfun"
+  shows "(\<lambda>a. Abs_finfun (curry f a)) \<in> finfun"
+proof -
+  from fin obtain c where c: "finite {ab. f ab \<noteq> c}" unfolding finfun_def by blast
+  have "{a. \<exists>b. f (a, b) \<noteq> c} = fst ` {ab. f ab \<noteq> c}" by(force)
+  hence "{a. curry f a \<noteq> (\<lambda>x. c)} = fst ` {ab. f ab \<noteq> c}"
+    by(auto simp add: curry_def expand_fun_eq)
+  with fin c have "finite {a.  Abs_finfun (curry f a) \<noteq> (\<lambda>\<^isup>f c)}"
+    by(simp add: finfun_const_def finfun_curry)
+  thus ?thesis unfolding finfun_def by auto
+qed
+
+lemma finfun_curry_conv_curry:
+  fixes f :: "('a \<times> 'b) \<Rightarrow>\<^isub>f 'c"
+  shows "finfun_curry f = Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a))"
+proof -
+  have "finfun_curry = (\<lambda>f :: ('a \<times> 'b) \<Rightarrow>\<^isub>f 'c. Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun f) a)))"
+  proof(rule finfun_rec_unique)
+    { fix c show "finfun_curry (\<lambda>\<^isup>f c) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)" by simp }
+    { fix f a c show "finfun_curry (f(\<^sup>f a := c)) = (finfun_curry f)(\<^sup>f fst a := ((finfun_curry f)\<^sub>f (fst a))(\<^sup>f snd a := c))"
+        by(cases a) simp }
+    { fix c show "Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun (\<lambda>\<^isup>f c)) a)) = (\<lambda>\<^isup>f \<lambda>\<^isup>f c)"
+        by(simp add: finfun_curry_def finfun_const_def curry_def) }
+    { fix g a b
+      show "Abs_finfun (\<lambda>aa. Abs_finfun (curry (Rep_finfun g(\<^sup>f a := b)) aa)) =
+       (Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))(\<^sup>f
+       fst a := ((Abs_finfun (\<lambda>a. Abs_finfun (curry (Rep_finfun g) a)))\<^sub>f (fst a))(\<^sup>f snd a := b))"
+        by(cases a)(auto intro!: ext arg_cong[where f=Abs_finfun] simp add: finfun_curry_def finfun_update_def finfun_apply_Rep_finfun finfun_curry finfun_Abs_finfun_curry) }
+  qed
+  thus ?thesis by(auto simp add: expand_fun_eq)
+qed
+
+subsection {* Executable equality for FinFuns *}
+
+lemma eq_finfun_All_ext: "(f = g) \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
+by(simp add: expand_finfun_eq expand_fun_eq finfun_All_All o_def)
+
+instantiation finfun :: ("{card_UNIV,eq}",eq) eq begin
+definition eq_finfun_def: "eq_class.eq f g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x = y) \<circ>\<^isub>f (f, g)\<^sup>f)"
+instance by(intro_classes)(simp add: eq_finfun_All_ext eq_finfun_def)
+end
+
+subsection {* Operator that explicitly removes all redundant updates in the generated representations *}
+
+definition finfun_clearjunk :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'a \<Rightarrow>\<^isub>f 'b"
+where [simp, code del]: "finfun_clearjunk = id"
+
+lemma finfun_clearjunk_const [code]: "finfun_clearjunk (\<lambda>\<^isup>f b) = (\<lambda>\<^isup>f b)"
+by simp
+
+lemma finfun_clearjunk_update [code]: "finfun_clearjunk (finfun_update_code f a b) = f(\<^sup>f a := b)"
+by simp
+
+end
\ No newline at end of file

--- a/src/HOL/Library/Library.thy	Tue Jun 02 16:56:55 2009 +0200
+++ b/src/HOL/Library/Library.thy	Tue Jun 02 18:26:12 2009 +0200
@@ -22,6 +22,7 @@
   Enum
   Eval_Witness
   Executable_Set
+  Fin_Fun
   Float
   Formal_Power_Series
   FrechetDeriv

--- a/src/HOL/Map.thy	Tue Jun 02 16:56:55 2009 +0200
+++ b/src/HOL/Map.thy	Tue Jun 02 18:26:12 2009 +0200
@@ -332,6 +332,9 @@
 lemma restrict_map_to_empty [simp]: "m|`{} = empty"
 by (simp add: restrict_map_def)
 
+lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
+by (auto simp add: restrict_map_def intro: ext)
+
 lemma restrict_map_empty [simp]: "empty|`D = empty"
 by (simp add: restrict_map_def)
 

--- a/src/HOL/Tools/numeral.ML	Tue Jun 02 16:56:55 2009 +0200
+++ b/src/HOL/Tools/numeral.ML	Tue Jun 02 18:26:12 2009 +0200
@@ -77,7 +77,7 @@
       (Code_Printer.str o Code_Printer.literal_numeral literals unbounded
         o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
   in
-    thy |>  Code_Target.add_syntax_const target number_of
+    thy |> Code_Target.add_syntax_const target number_of
       (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min}, @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
   end;
 

--- a/src/HOL/ex/Codegenerator.thy	Tue Jun 02 16:56:55 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(*  ID:         $Id$
-    Author:     Florian Haftmann, TU Muenchen
-*)
-
-header {* Tests and examples for code generator *}
-
-theory Codegenerator
-imports ExecutableContent
-begin
-
-ML {* (*FIXME get rid of this*)
-nonfix union;
-nonfix inter;
-nonfix upto;
-*}
-
-export_code * in SML module_name CodegenTest
-  in OCaml module_name CodegenTest file -
-  in Haskell file -
-
-ML {*
-infix union;
-infix inter;
-infix 4 upto;
-*}
-
-end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Codegenerator_Candidates.thy	Tue Jun 02 18:26:12 2009 +0200
@@ -0,0 +1,44 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* A huge collection of equations to generate code from *}
+
+theory Codegenerator_Candidates
+imports
+  Complex_Main
+  AssocList
+  Binomial
+  Commutative_Ring
+  Enum
+  List_Prefix
+  Nat_Infinity
+  Nested_Environment
+  Option_ord
+  Permutation
+  Primes
+  Product_ord
+  SetsAndFunctions
+  While_Combinator
+  Word
+  "~~/src/HOL/ex/Commutative_Ring_Complete"
+  "~~/src/HOL/ex/Records"
+begin
+
+(*temporary Haskell workaround*)
+declare typerep_fun_def [code inline]
+declare typerep_prod_def [code inline]
+declare typerep_sum_def [code inline]
+declare typerep_cpoint_ext_type_def [code inline]
+declare typerep_itself_def [code inline]
+declare typerep_list_def [code inline]
+declare typerep_option_def [code inline]
+declare typerep_point_ext_type_def [code inline]
+declare typerep_point'_ext_type_def [code inline]
+declare typerep_point''_ext_type_def [code inline]
+declare typerep_pol_def [code inline]
+declare typerep_polex_def [code inline]
+
+(*avoid popular infixes*)
+code_reserved SML union inter upto
+
+end

--- a/src/HOL/ex/Codegenerator_Pretty.thy	Tue Jun 02 16:56:55 2009 +0200
+++ b/src/HOL/ex/Codegenerator_Pretty.thy	Tue Jun 02 18:26:12 2009 +0200
@@ -1,29 +1,12 @@
-(*  Title:      HOL/ex/Codegenerator_Pretty.thy
-    Author:     Florian Haftmann, TU Muenchen
-*)
 
-header {* Simple examples for pretty numerals and such *}
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Generating code using pretty literals and natural number literals  *}
 
 theory Codegenerator_Pretty
-imports ExecutableContent Code_Char Efficient_Nat
+imports "~~/src/HOL/ex/Codegenerator_Candidates" Code_Char Efficient_Nat
 begin
 
 declare isnorm.simps [code del]
 
-ML {* (*FIXME get rid of this*)
-nonfix union;
-nonfix inter;
-nonfix upto;
-*}
-
-export_code * in SML module_name CodegenTest
-  in OCaml module_name CodegenTest file -
-  in Haskell file -
-
-ML {*
-infix union;
-infix inter;
-infix 4 upto;
-*}
-
 end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Codegenerator_Pretty_Test.thy	Tue Jun 02 18:26:12 2009 +0200
@@ -0,0 +1,14 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Pervasive test of code generator using pretty literals *}
+
+theory Codegenerator_Pretty_Test
+imports Codegenerator_Pretty
+begin
+
+export_code * in SML module_name CodegenTest
+  in OCaml module_name CodegenTest file -
+  in Haskell file -
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Codegenerator_Test.thy	Tue Jun 02 18:26:12 2009 +0200
@@ -0,0 +1,14 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Pervasive test of code generator *}
+
+theory Codegenerator_Test
+imports Codegenerator_Candidates
+begin
+
+export_code * in SML module_name CodegenTest
+  in OCaml module_name CodegenTest file -
+  in Haskell file -
+
+end

--- a/src/HOL/ex/ExecutableContent.thy	Tue Jun 02 16:56:55 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(*  Author:     Florian Haftmann, TU Muenchen
-*)
-
-header {* A huge set of executable constants *}
-
-theory ExecutableContent
-imports
-  Complex_Main
-  AssocList
-  Binomial
-  Commutative_Ring
-  Enum
-  List_Prefix
-  Nat_Infinity
-  Nested_Environment
-  Option_ord
-  Permutation
-  Primes
-  Product_ord
-  SetsAndFunctions
-  While_Combinator
-  Word
-  "~~/src/HOL/ex/Commutative_Ring_Complete"
-  "~~/src/HOL/ex/Records"
-begin
-
-end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Landau.thy	Tue Jun 02 18:26:12 2009 +0200
@@ -0,0 +1,226 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Comparing growth of functions on natural numbers by a preorder relation *}
+
+theory Landau
+imports Main Preorder
+begin
+
+text {*
+  We establish a preorder releation @{text "\<lesssim>"} on functions
+  from @{text "\<nat>"} to @{text "\<nat>"} such that @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.
+*}
+
+subsection {* Auxiliary *}
+
+lemma Ex_All_bounded:
+  fixes n :: nat
+  assumes "\<exists>n. \<forall>m\<ge>n. P m"
+  obtains m where "m \<ge> n" and "P m"
+proof -
+  from assms obtain q where m_q: "\<forall>m\<ge>q. P m" ..
+  let ?m = "max q n"
+  have "?m \<ge> n" by auto
+  moreover from m_q have "P ?m" by auto
+  ultimately show thesis ..
+qed
+    
+
+subsection {* The @{text "\<lesssim>"} relation *}
+
+definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50) where
+  "f \<lesssim> g \<longleftrightarrow> (\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * g m)"
+
+lemma less_eq_fun_intro:
+  assumes "\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * g m"
+  shows "f \<lesssim> g"
+  unfolding less_eq_fun_def by (rule assms)
+
+lemma less_eq_fun_not_intro:
+  assumes "\<And>c n. \<exists>m\<ge>n. Suc c * g m < f m"
+  shows "\<not> f \<lesssim> g"
+  using assms unfolding less_eq_fun_def linorder_not_le [symmetric]
+  by blast
+
+lemma less_eq_fun_elim:
+  assumes "f \<lesssim> g"
+  obtains n c where "\<And>m. m \<ge> n \<Longrightarrow> f m \<le> Suc c * g m"
+  using assms unfolding less_eq_fun_def by blast
+
+lemma less_eq_fun_not_elim:
+  assumes "\<not> f \<lesssim> g"
+  obtains m where "m \<ge> n" and "Suc c * g m < f m"
+  using assms unfolding less_eq_fun_def linorder_not_le [symmetric]
+  by blast
+
+lemma less_eq_fun_refl:
+  "f \<lesssim> f"
+proof (rule less_eq_fun_intro)
+  have "\<exists>n. \<forall>m\<ge>n. f m \<le> Suc 0 * f m" by auto
+  then show "\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * f m" by blast
+qed
+
+lemma less_eq_fun_trans:
+  assumes f_g: "f \<lesssim> g" and g_h: "g \<lesssim> h"
+  shows f_h: "f \<lesssim> h"
+proof -
+  from f_g obtain n\<^isub>1 c\<^isub>1
+    where P1: "\<And>m. m \<ge> n\<^isub>1 \<Longrightarrow> f m \<le> Suc c\<^isub>1 * g m"
+  by (erule less_eq_fun_elim)
+  moreover from g_h obtain n\<^isub>2 c\<^isub>2
+    where P2: "\<And>m. m \<ge> n\<^isub>2 \<Longrightarrow> g m \<le> Suc c\<^isub>2 * h m"
+  by (erule less_eq_fun_elim)
+  ultimately have "\<And>m. m \<ge> max n\<^isub>1 n\<^isub>2 \<Longrightarrow> f m \<le> Suc c\<^isub>1 * g m \<and> g m \<le> Suc c\<^isub>2 * h m"
+  by auto
+  moreover {
+    fix k l r :: nat
+    assume k_l: "k \<le> Suc c\<^isub>1 * l" and l_r: "l \<le> Suc c\<^isub>2 * r"
+    from l_r have "Suc c\<^isub>1 * l \<le> (Suc c\<^isub>1 * Suc c\<^isub>2) * r"
+    by (auto simp add: mult_le_cancel_left mult_assoc simp del: times_nat.simps mult_Suc_right)
+    with k_l have "k \<le> (Suc c\<^isub>1 * Suc c\<^isub>2) * r" by (rule preorder_class.order_trans)
+  }
+  ultimately have "\<And>m. m \<ge> max n\<^isub>1 n\<^isub>2 \<Longrightarrow> f m \<le> (Suc c\<^isub>1 * Suc c\<^isub>2) * h m" by auto
+  then have "\<And>m. m \<ge> max n\<^isub>1 n\<^isub>2 \<Longrightarrow> f m \<le> Suc ((Suc c\<^isub>1 * Suc c\<^isub>2) - 1) * h m" by auto
+  then show ?thesis unfolding less_eq_fun_def by blast
+qed
+
+
+subsection {* The @{text "\<approx>"} relation, the equivalence relation induced by @{text "\<lesssim>"} *}
+
+definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50) where
+  "f \<cong> g \<longleftrightarrow> (\<exists>d c n. \<forall>m\<ge>n. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m)"
+
+lemma equiv_fun_intro:
+  assumes "\<exists>d c n. \<forall>m\<ge>n. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
+  shows "f \<cong> g"
+  unfolding equiv_fun_def by (rule assms)
+
+lemma equiv_fun_not_intro:
+  assumes "\<And>d c n. \<exists>m\<ge>n. Suc d * f m < g m \<or> Suc c * g m < f m"
+  shows "\<not> f \<cong> g"
+  unfolding equiv_fun_def
+  by (auto simp add: assms linorder_not_le
+    simp del: times_nat.simps mult_Suc_right)
+
+lemma equiv_fun_elim:
+  assumes "f \<cong> g"
+  obtains n d c
+    where "\<And>m. m \<ge> n \<Longrightarrow> g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
+  using assms unfolding equiv_fun_def by blast
+
+lemma equiv_fun_not_elim:
+  fixes n d c
+  assumes "\<not> f \<cong> g"
+  obtains m where "m \<ge> n"
+    and "Suc d * f m < g m \<or> Suc c * g m < f m"
+  using assms unfolding equiv_fun_def
+  by (auto simp add: linorder_not_le, blast)
+
+lemma equiv_fun_less_eq_fun:
+  "f \<cong> g \<longleftrightarrow> f \<lesssim> g \<and> g \<lesssim> f"
+proof
+  assume x_y: "f \<cong> g"
+  then obtain n d c
+    where interv: "\<And>m. m \<ge> n \<Longrightarrow> g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
+  by (erule equiv_fun_elim)
+  from interv have "\<exists>c n. \<forall>m \<ge> n. f m \<le> Suc c * g m" by auto
+  then have f_g: "f \<lesssim> g" by (rule less_eq_fun_intro)
+  from interv have "\<exists>d n. \<forall>m \<ge> n. g m \<le> Suc d * f m" by auto
+  then have g_f: "g \<lesssim> f" by (rule less_eq_fun_intro)
+  from f_g g_f show "f \<lesssim> g \<and> g \<lesssim> f" by auto
+next
+  assume assm: "f \<lesssim> g \<and> g \<lesssim> f"
+  from assm less_eq_fun_elim obtain c n\<^isub>1 where
+    bound1: "\<And>m. m \<ge> n\<^isub>1 \<Longrightarrow> f m \<le> Suc c * g m" 
+    by blast
+  from assm less_eq_fun_elim obtain d n\<^isub>2 where
+    bound2: "\<And>m. m \<ge> n\<^isub>2 \<Longrightarrow> g m \<le> Suc d * f m"
+    by blast
+  from bound2 have "\<And>m. m \<ge> max n\<^isub>1 n\<^isub>2 \<Longrightarrow> g m \<le> Suc d * f m"
+  by auto
+  with bound1
+    have "\<forall>m \<ge> max n\<^isub>1 n\<^isub>2. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
+    by auto
+  then
+    have "\<exists>d c n. \<forall>m\<ge>n. g m \<le> Suc d * f m \<and> f m \<le> Suc c * g m"
+    by blast
+  then show "f \<cong> g" by (rule equiv_fun_intro)
+qed
+
+subsection {* The @{text "\<prec>"} relation, the strict part of @{text "\<lesssim>"} *}
+
+definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50) where
+  "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f"
+
+lemma less_fun_intro:
+  assumes "\<And>c. \<exists>n. \<forall>m\<ge>n. Suc c * f m < g m"
+  shows "f \<prec> g"
+proof (unfold less_fun_def, rule conjI)
+  from assms obtain n
+    where "\<forall>m\<ge>n. Suc 0 * f m < g m" ..
+  then have "\<forall>m\<ge>n. f m \<le> Suc 0 * g m" by auto
+  then have "\<exists>c n. \<forall>m\<ge>n. f m \<le> Suc c * g m" by blast
+  then show "f \<lesssim> g" by (rule less_eq_fun_intro)
+next
+  show "\<not> g \<lesssim> f"
+  proof (rule less_eq_fun_not_intro)
+    fix c n :: nat
+    from assms have "\<exists>n. \<forall>m\<ge>n. Suc c * f m < g m" by blast
+    then obtain m where "m \<ge> n" and "Suc c * f m < g m"
+      by (rule Ex_All_bounded)
+    then show "\<exists>m\<ge>n. Suc c * f m < g m" by blast
+  qed
+qed
+
+text {*
+  We would like to show (or refute) that @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"},
+  i.e.~@{prop "f \<prec> g \<longleftrightarrow> (\<forall>c. \<exists>n. \<forall>m>n. f m < Suc c * g m)"} but did not manage to
+  do so.
+*}
+
+
+subsection {* Assert that @{text "\<lesssim>"} is ineed a preorder *}
+
+interpretation fun_order: preorder_equiv less_eq_fun less_fun
+  where "preorder_equiv.equiv less_eq_fun = equiv_fun"
+proof -
+  interpret preorder_equiv less_eq_fun less_fun proof
+  qed (simp_all add: less_fun_def less_eq_fun_refl, auto intro: less_eq_fun_trans)
+  show "preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
+  show "preorder_equiv.equiv less_eq_fun = equiv_fun"
+    by (simp add: expand_fun_eq equiv_def equiv_fun_less_eq_fun)
+qed
+
+
+subsection {* Simple examples *}
+
+lemma "(\<lambda>_. n) \<lesssim> (\<lambda>n. n)"
+proof (rule less_eq_fun_intro)
+  show "\<exists>c q. \<forall>m\<ge>q. n \<le> Suc c * m"
+  proof -
+    have "\<forall>m\<ge>n. n \<le> Suc 0 * m" by simp
+    then show ?thesis by blast
+  qed
+qed
+
+lemma "(\<lambda>n. n) \<cong> (\<lambda>n. Suc k * n)"
+proof (rule equiv_fun_intro)
+  show "\<exists>d c n. \<forall>m\<ge>n. Suc k * m \<le> Suc d * m \<and> m \<le> Suc c * (Suc k * m)"
+  proof -
+    have "\<forall>m\<ge>n. Suc k * m \<le> Suc k * m \<and> m \<le> Suc c * (Suc k * m)" by simp
+    then show ?thesis by blast
+  qed
+qed  
+
+lemma "(\<lambda>_. n) \<prec> (\<lambda>n. n)"
+proof (rule less_fun_intro)
+  fix c
+  show "\<exists>q. \<forall>m\<ge>q. Suc c * n < m"
+  proof -
+    have "\<forall>m\<ge>Suc c * n + 1. Suc c * n < m" by simp
+    then show ?thesis by blast
+  qed
+qed
+
+end

--- a/src/HOL/ex/ROOT.ML	Tue Jun 02 16:56:55 2009 +0200
+++ b/src/HOL/ex/ROOT.ML	Tue Jun 02 18:26:12 2009 +0200
@@ -6,13 +6,12 @@
 no_document use_thys [
   "State_Monad",
   "Efficient_Nat_examples",
-  "ExecutableContent",
   "FuncSet",
   "Word",
   "Eval_Examples",
   "Quickcheck_Generators",
-  "Codegenerator",
-  "Codegenerator_Pretty",
+  "Codegenerator_Test",
+  "Codegenerator_Pretty_Test",
   "NormalForm",
   "../NumberTheory/Factorization",
   "Predicate_Compile",
@@ -67,7 +66,8 @@
   "HarmonicSeries",
   "Refute_Examples",
   "Quickcheck_Examples",
-  "Formal_Power_Series_Examples"
+  "Formal_Power_Series_Examples",
+  "Landau"
 ];
 
 setmp Proofterm.proofs 2 use_thy "Hilbert_Classical";

--- a/src/Tools/code/code_haskell.ML	Tue Jun 02 16:56:55 2009 +0200
+++ b/src/Tools/code/code_haskell.ML	Tue Jun 02 18:26:12 2009 +0200
@@ -106,10 +106,10 @@
               |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
               |>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t])
             val (ps, vars') = fold_map pr binds vars;
-          in
+          in 
             Pretty.block_enclose (
-              str "let {",
-              concat [str "}", str "in", pr_term tyvars thm vars' NOBR body]
+              str "(let {",
+              concat [str "}", str "in", pr_term tyvars thm vars' NOBR body, str ")"]
             ) ps
           end
       | pr_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) =
@@ -124,7 +124,8 @@
               str "})"
             ) (map pr clauses)
           end
-      | pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
+      | pr_case tyvars thm vars fxy ((_, []), _) =
+          (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
     fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) =
           let
             val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;

--- a/src/Tools/code/code_ml.ML	Tue Jun 02 16:56:55 2009 +0200
+++ b/src/Tools/code/code_ml.ML	Tue Jun 02 18:26:12 2009 +0200
@@ -444,7 +444,8 @@
               |>> (fn p => concat
                   [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
             val (ps, vars') = fold_map pr binds vars;
-          in Pretty.chunks (ps @| pr_term is_closure thm vars' NOBR body) end
+            fun mk_brack (p :: ps) = Pretty.block [str "(", p] :: ps;
+          in Pretty.chunks (mk_brack ps @| Pretty.block [pr_term is_closure thm vars' NOBR body, str ")"]) end
       | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) =
           let
             fun pr delim (pat, body) =
@@ -649,7 +650,7 @@
               str ("type '" ^ v),
               (str o deresolve) class,
               str "=",
-              enum_default "();;" ";" "{" "};;" (
+              enum_default "unit;;" ";" "{" "};;" (
                 map pr_superclass_field superclasses
                 @ map pr_classparam_field classparams
               )
@@ -708,17 +709,17 @@
       val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
         then chr i else c
     in s end;
+  fun bignum_ocaml k = if k <= 1073741823
+    then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
+    else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
 in Literals {
   literal_char = enclose "'" "'" o char_ocaml,
   literal_string = quote o translate_string char_ocaml,
   literal_numeral = fn unbounded => fn k => if k >= 0 then
-      if unbounded then
-        "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
+      if unbounded then bignum_ocaml k
       else string_of_int k
     else
-      if unbounded then
-        "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
-          o string_of_int o op ~) k ^ ")"
+      if unbounded then "(Big_int.minus_big_int " ^ bignum_ocaml (~ k) ^ ")"
       else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
   literal_list = Pretty.enum ";" "[" "]",
   infix_cons = (6, "::")