# HG changeset patch # User haftmann # Date 1243959972 -7200 # Node ID 5c563b9688327a423010f4fd23270a6966752dca # Parent 8c8d615f04aef84018548ebd0f138272a5f4e46e# Parent b3a785a69538e5ff9637d319d93f03ea2f6523ac merged diff -r 8c8d615f04ae -r 5c563b968832 src/HOL/Code_Numeral.thy --- 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 + \ code_numeral \ code_numeral \ code_numeral" (SML "Int.+/ ((_),/ (_))") - (OCaml "Pervasives.( + )") + (OCaml "Big'_int.add'_big'_int") (Haskell infixl 6 "+") code_const "subtract_code_numeral \ code_numeral \ code_numeral \ 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 * \ code_numeral \ code_numeral \ 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 \ code_numeral \ code_numeral \ bool" (SML "!((_ : Int.int) = _)") - (OCaml "!((_ : int) = _)") + (OCaml "Big'_int.eq'_big'_int") (Haskell infixl 4 "==") code_const "op \ \ code_numeral \ code_numeral \ bool" (SML "Int.<=/ ((_),/ (_))") - (OCaml "!((_ : int) <= _)") + (OCaml "Big'_int.le'_big'_int") (Haskell infix 4 "<=") code_const "op < \ code_numeral \ code_numeral \ bool" (SML "Int. nat" -where "card A = setsum (\x. 1) A" +definition card :: "'a set \ nat" where + "card A = setsum (\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 \ 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 \ 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) \ 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 _ "\ (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 \ UNIV" by simp + show "UNIV \ A" + proof + fix x + show "x \ A" + proof (rule ccontr) + assume "x \ A" + then have "A \ 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 \ 'b) set)" + shows "finite (UNIV :: 'b set)" +proof - + from fin have "finite (range (\f :: 'a \ 'b. f arbitrary))" + by(rule finite_imageI) + moreover have "UNIV = range (\f :: 'a \ 'b. f arbitrary)" + by(rule UNIV_eq_I) auto + ultimately show "finite (UNIV :: 'b set)" by simp +qed + lemma setsum_constant [simp]: "(\x \ A. y) = of_nat(card A) * y" apply (cases "finite A") apply (erule finite_induct) diff -r 8c8d615f04ae -r 5c563b968832 src/HOL/Hilbert_Choice.thy --- 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 \ 'b) set)" + and card: "card (UNIV :: 'b set) \ 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) \ 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) \ (b2 :: 'b)" by (auto simp add: card_Suc_eq) + from fin have "finite (range (\f :: 'a \ 'b. inv f b1))" by (rule finite_imageI) + moreover have "UNIV = range (\f :: 'a \ 'b. inv f b1)" + proof (rule UNIV_eq_I) + fix x :: 'a + from b1b2 have "x = inv (\y. if y = x then b1 else b2) b1" by (simp add: inv_def) + thus "x \ range (\f\'a \ 'b. inv f b1)" by blast + qed + ultimately show "finite (UNIV :: 'a set)" by simp +qed subsection {*Inverse of a PI-function (restricted domain)*} diff -r 8c8d615f04ae -r 5c563b968832 src/HOL/IsaMakefile --- 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 \ diff -r 8c8d615f04ae -r 5c563b968832 src/HOL/Library/Code_Integer.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 *} diff -r 8c8d615f04ae -r 5c563b968832 src/HOL/Library/Efficient_Nat.thy --- 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 *} diff -r 8c8d615f04ae -r 5c563b968832 src/HOL/Library/Fin_Fun.thy --- /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 \ ('a \ 'b) \ 'a \ 'b" +where "map_default b f a \ case f a of None \ b | Some b' \ 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 \ 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 = (\a. b)" +by(simp add: expand_fun_eq map_default_def) + +lemma map_default_inject: + fixes g g' :: "'a \ 'b" + assumes infin_eq: "\ finite (UNIV :: 'a set) \ b = b'" + and fin: "finite (dom g)" and b: "b \ ran g" + and fin': "finite (dom g')" and b': "b' \ 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: "\ finite (UNIV :: 'a set)" + from fin fin' have "finite (dom g \ dom g')" by auto + with infin have "UNIV - (dom g \ dom g') \ {}" by(auto dest: finite_subset) + then obtain a where a: "a \ dom g \ 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 \ 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\'b. \b. finite {a. f a \ b}}" +apply(auto) +apply(rule_tac x="\x. arbitrary" in exI) +apply(auto) +done + +syntax + "finfun" :: "type \ type \ type" ("(_ \\<^isub>f /_)" [22, 21] 21) + +lemma fun_upd_finfun: "y(a := b) \ finfun \ y \ finfun" +proof - + { fix b' + have "finite {a'. (y(a := b)) a' \ b'} = finite {a'. y a' \ b'}" + proof(cases "b = b'") + case True + hence "{a'. (y(a := b)) a' \ b'} = {a'. y a' \ b'} - {a}" by auto + thus ?thesis by simp + next + case False + hence "{a'. (y(a := b)) a' \ b'} = insert a {a'. y a' \ b'}" by auto + thus ?thesis by simp + qed } + thus ?thesis unfolding finfun_def by blast +qed + +lemma const_finfun: "(\x. a) \ finfun" +by(auto simp add: finfun_def) + +lemma finfun_left_compose: + assumes "y \ finfun" + shows "g \ y \ finfun" +proof - + from assms obtain b where "finite {a. y a \ b}" + unfolding finfun_def by blast + hence "finite {c. g (y c) \ g b}" + proof(induct x\"{a. y a \ b}" arbitrary: y) + case empty + hence "y = (\a. b)" by(auto intro: ext) + thus ?case by(simp) + next + case (insert x F) + note IH = `\y. F = {a. y a \ b} \ finite {c. g (y c) \ g b}` + from `insert x F = {a. y a \ b}` `x \ F` + have F: "F = {a. (y(x := b)) a \ b}" by(auto) + show ?case + proof(cases "g (y x) = g b") + case True + hence "{c. g ((y(x := b)) c) \ g b} = {c. g (y c) \ g b}" by auto + with IH[OF F] show ?thesis by simp + next + case False + hence "{c. g (y c) \ g b} = insert x {c. g ((y(x := b)) c) \ 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 \ finfun" + shows fst_finfun: "fst \ y \ finfun" + and snd_finfun: "snd \ y \ finfun" +proof - + from assms obtain b c where bc: "finite {a. y a \ (b, c)}" + unfolding finfun_def by auto + have "{a. fst (y a) \ b} \ {a. y a \ (b, c)}" + and "{a. snd (y a) \ c} \ {a. y a \ (b, c)}" by auto + hence "finite {a. fst (y a) \ b}" + and "finite {a. snd (y a) \ c}" using bc by(auto intro: finite_subset) + thus "fst \ y \ finfun" "snd \ y \ finfun" + unfolding finfun_def by auto +qed + +lemma map_of_finfun: "map_of xs \ 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: "(\x. (f x, g x)) \ finfun \ f \ finfun \ g \ 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 \ finfun" and inj: "inj f" + shows "g o f \ finfun" +proof - + from g obtain b where b: "finite {a. g a \ b}" unfolding finfun_def by blast + moreover have "f ` {a. g (f a) \ b} \ {a. g a \ b}" by auto + moreover from inj have "inj_on f {a. g (f a) \ b}" by(rule subset_inj_on) blast + ultimately have "finite {a. g (f a) \ 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 \ finfun" + shows "curry f \ finfun" "curry f a \ finfun" +proof - + from fin obtain c where c: "finite {ab. f ab \ c}" unfolding finfun_def by blast + moreover have "{a. \b. f (a, b) \ c} = fst ` {ab. f ab \ c}" by(force) + hence "{a. curry f a \ (\b. c)} = fst ` {ab. f ab \ c}" + by(auto simp add: curry_def expand_fun_eq) + ultimately have "finite {a. curry f a \ (\b. c)}" by simp + thus "curry f \ finfun" unfolding finfun_def by blast + + have "snd ` {ab. f ab \ c} = {b. \a. f (a, b) \ c}" by(force) + hence "{b. f (a, b) \ c} \ snd ` {ab. f ab \ c}" by auto + hence "finite {b. f (a, b) \ c}" by(rule finite_subset)(rule finite_imageI[OF c]) + thus "curry f a \ 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 \ 'b" + assumes fin: "finite (UNIV :: 'a set)" + shows "Abs_finfun x = Abs_finfun y \ x = y" +proof + assume "Abs_finfun x = Abs_finfun y" + moreover have "x \ finfun" "y \ 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) \ 'b" + shows "Abs_finfun x = Abs_finfun y \ 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 \ 'b) \ 'a \\<^isub>f 'b)" +proof(rule inj_onI) + fix x y :: "'a \ 'b" + assume "Abs_finfun x = Abs_finfun y" + moreover have "x \ finfun" "y \ 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 \ 'b" + assumes fin: "finite (UNIV :: 'a set)" + shows "Rep_finfun (Abs_finfun x) = x" +proof - + from fin have "x \ 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) \ '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) \ (finfun :: ('a \ 'b) set) = UNIV" +unfolding finfun_def by(auto intro: finite_subset) + +lemma finfun_finite_UNIV_class: "finfun = (UNIV :: ('a :: finite \ 'b) set)" +by(simp add: finfun_eq_finite_UNIV) + +lemma map_default_in_finfun: + assumes fin: "finite (dom f)" + shows "map_default b f \ finfun" +unfolding finfun_def +proof(intro CollectI exI) + from fin show "finite {a. map_default b f a \ 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 \ ran g" +proof - + obtain y where f: "f = Abs_finfun y" and y: "y \ finfun" by(cases f) + from y obtain b where b: "finite {a. y a \ b}" unfolding finfun_def by auto + let ?g = "(\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 \ ran ?g" by(auto simp add: ran_def) + ultimately show ?thesis by(rule that) +qed + + +subsection {* Kernel functions for type @{typ "'a \\<^isub>f 'b"} *} + +definition finfun_const :: "'b \ 'a \\<^isub>f 'b" ("\\<^isup>f/ _" [0] 1) +where [code del]: "(\\<^isup>f b) = Abs_finfun (\x. b)" + +definition finfun_update :: "'a \\<^isub>f 'b \ 'a \ 'b \ 'a \\<^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 \ a' \ 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: "(\\<^isup>f b)(\<^sup>f a := b) = (\\<^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 \\<^isub>f 'b \ 'a \ 'b \ 'a \\<^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]: + "(\\<^isup>f b)(\<^sup>f a := b') = (if b = b' then (\\<^isup>f b) else finfun_update_code (\\<^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\" 60) + +definition (in term_syntax) valtermify_finfun_const :: + "'b\typerep \ (unit \ Code_Eval.term) \ ('a\typerep \\<^isub>f 'b) \ (unit \ Code_Eval.term)" where + "valtermify_finfun_const y = Code_Eval.valtermify finfun_const {\} y" + +definition (in term_syntax) valtermify_finfun_update_code :: + "'a\typerep \ (unit \ Code_Eval.term) \ 'b\typerep \ (unit \ Code_Eval.term) \ ('a \\<^isub>f 'b) \ (unit \ Code_Eval.term) \ ('a \\<^isub>f 'b) \ (unit \ Code_Eval.term)" where + "valtermify_finfun_update_code x y f = Code_Eval.valtermify finfun_update_code {\} f {\} x {\} y" + +instantiation finfun :: (random, random) random +begin + +primrec random_finfun' :: "code_numeral \ code_numeral \ Random.seed \ ('a \\<^isub>f 'b \ (unit \ Code_Eval.term)) \ Random.seed" where + "random_finfun' 0 j = Quickcheck.collapse (Random.select_default 0 + (random j o\ (\y. Pair (valtermify_finfun_const y))) + (random j o\ (\y. Pair (valtermify_finfun_const y))))" + | "random_finfun' (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_default i + (random j o\ (\x. random j o\ (\y. random_finfun' i j o\ (\f. Pair (valtermify_finfun_update_code x y f))))) + (random j o\ (\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\ (\x. random j o\ (\y. random_finfun' (i - 1) j o\ (\f. Pair (valtermify_finfun_update_code x y f))))) + (random j o\ (\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\" 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 "\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 (\a f. f(\<^sup>f a := b')) (\\<^isup>f b) (UNIV :: 'a set) = (\\<^isup>f b')" +proof - + { fix A :: "'a set" + from fin have "finite A" by(auto intro: finite_subset) + hence "fold (\a f. f(\<^sup>f a := b')) (\\<^isup>f b) A = Abs_finfun (\a. if a \ A then b' else b)" + proof(induct) + case (insert x F) + have "(\a. if a = x then b' else (if a \ F then b' else b)) = (\a. if a = x \ a \ 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 \ 'b) \ 'b" +where [code del]: "finfun_default_aux f = (if finite (UNIV :: 'a set) then arbitrary else THE b. finite {a. f a \ b})" + +lemma finfun_default_aux_infinite: + fixes f :: "'a \ 'b" + assumes infin: "infinite (UNIV :: 'a set)" + and fin: "finite {a. f a \ b}" + shows "finfun_default_aux f = b" +proof - + let ?B = "{a. f a \ b}" + from fin have "(THE b. finite {a. f a \ b}) = b" + proof(rule the_equality) + fix b' + assume "finite {a. f a \ b'}" (is "finite ?B'") + with infin fin have "UNIV - (?B' \ ?B) \ {}" by(auto dest: finite_subset) + then obtain a where a: "a \ ?B' \ ?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 \ 'b" + assumes fin: "f \ finfun" + shows "finite {a. f a \ 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 \ 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 \ 'b" + assumes fin: "f \ 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 \ b'}" unfolding finfun_def by blast + hence "finite {a'. (f(a := b)) a' \ b'}" + proof(cases "b = b' \ f a \ b'") + case True + hence "{a. f a \ b'} = insert a {a'. (f(a := b)) a' \ b'}" by auto + thus ?thesis using b' by simp + next + case False + moreover + { assume "b \ b'" + hence "{a'. (f(a := b)) a' \ b'} = insert a {a. f a \ b'}" by auto + hence ?thesis using b' by simp } + moreover + { assume "b = b'" "f a = b'" + hence "{a'. (f(a := b)) a' \ b'} = {a. f a \ 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 \\<^isub>f 'b \ 'b" + where [code del]: "finfun_default f = finfun_default_aux (Rep_finfun f)" + +lemma finite_finfun_default: "finite {a. Rep_finfun f a \ finfun_default f}" +unfolding finfun_default_def by(simp add: finite_finfun_default_aux) + +lemma finfun_default_const: "finfun_default ((\\<^isup>f b) :: 'a \\<^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 \ 'c) \ ('a \ 'b \ 'c \ 'c) \ ('a \\<^isub>f 'b) \ 'c" +where [code del]: + "finfun_rec cnst upd f \ + let b = finfun_default f; + g = THE g. f = Abs_finfun (map_default b g) \ finite (dom g) \ b \ ran g + in fold (\a. upd a (map_default b g a)) (cnst b) (dom g)" + +locale finfun_rec_wf_aux = + fixes cnst :: "'b \ 'c" + and upd :: "'a \ 'b \ 'c \ 'c" + assumes upd_const_same: "upd a b (cnst b) = cnst b" + and upd_commute: "a \ a' \ upd a b (upd a' b' c) = upd a' b' (upd a b c)" + and upd_idemp: "b \ b' \ upd a b'' (upd a b' (cnst b)) = upd a b'' (cnst b)" +begin + + +lemma upd_left_comm: "fun_left_comm (\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 \ 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 \ dom f" + and fg: "f \\<^sub>m g" + shows "upd a d (fold (\a. upd a (map_default d g a)) (cnst d) (dom f)) = + fold (\a. upd a (map_default d g a)) (cnst d) (dom f)" +proof - + let ?upd = "\a. upd a (map_default d g a)" + let ?fr = "\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\"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 = `\f. \ a \ dom f; f \\<^sub>m g; A = dom f\ \ upd a d (?fr (dom f)) = ?fr (dom f)` + note fin = `finite A` note anf = `a \ dom f` note a'nA = `a' \ A` + note domf = `insert a' A = dom f` note fg = `f \\<^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 \ a'" by auto note upd_commute[OF this] + also from domf a'nA anf fg have "a \ dom ?f'" "?f' \\<^sub>m g" and A: "A = dom ?f'" by(auto simp add: ran_def map_le_def) + note A also note IH[OF `a \ dom ?f'` `?f' \\<^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 \ dom f" + and fg: "f \\<^sub>m g" + shows "upd a d'' (upd a d' (fold (\a. upd a (map_default d g a)) (cnst d) (dom f))) = + upd a d'' (fold (\a. upd a (map_default d g a)) (cnst d) (dom f))" +proof - + let ?upd = "\a. upd a (map_default d g a)" + let ?fr = "\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\"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 = `\f. \a \ dom f; f \\<^sub>m g; A = dom f\ \ upd a d'' (upd a d' (?fr (dom f))) = upd a d'' (?fr (dom f))` + note fin = `finite A` note anf = `a \ dom f` note a'nA = `a' \ A` + note domf = `insert a' A = dom f` note fg = `f \\<^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 \ d | Some b \ 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 \ a'" by auto note upd_commute[OF this] + also note upd_commute[OF ana'] + also from domf a'nA anf fg have "a \ dom ?f'" "?f' \\<^sub>m g" and A: "A = dom ?f'" by(auto simp add: ran_def map_le_def) + note A also note IH[OF `a \ dom ?f'` `?f' \\<^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 ((\a. Some (f a)) |` {a. f a \ 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: "\a. a \ A \ 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 \ A" + with fin have "finite B" by(blast intro: finite_subset) + hence "B \ A \ 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 \ B` note sub = `insert a B \ A` + note IH = `B \ A \ fold f z B = fold g z B` + from sub anB have BpsubA: "B \ A" and BsubA: "B \ A" and aA: "a \ 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 = "\f g. f = Abs_finfun (map_default b g) \ finite (dom g) \ b \ ran g" + obtain g where g: "g = The (?the f)" by blast + obtain y where f: "f = Abs_finfun y" and y: "y \