--- a/Admin/isatest/isatest-makedist Tue Jun 02 23:49:46 2009 -0700
+++ b/Admin/isatest/isatest-makedist Tue Jun 02 23:56:12 2009 -0700
@@ -105,7 +105,7 @@
#sleep 15
$SSH macbroy22 "$MAKEALL $HOME/settings/at64-poly-5.1-para"
sleep 15
-$SSH macbroy23 "$MAKEALL -l HOL $HOME/settings/at-sml-dev-e"
+$SSH macbroy23 "$MAKEALL $HOME/settings/at-sml-dev-e"
sleep 15
$SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly"
sleep 15
--- a/src/HOL/Code_Numeral.thy Tue Jun 02 23:49:46 2009 -0700
+++ b/src/HOL/Code_Numeral.thy Tue Jun 02 23:56:12 2009 -0700
@@ -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 23:49:46 2009 -0700
+++ b/src/HOL/Finite_Set.thy Tue Jun 02 23:56:12 2009 -0700
@@ -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 23:49:46 2009 -0700
+++ b/src/HOL/Hilbert_Choice.thy Tue Jun 02 23:56:12 2009 -0700
@@ -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/Integration.thy Tue Jun 02 23:49:46 2009 -0700
+++ b/src/HOL/Integration.thy Tue Jun 02 23:56:12 2009 -0700
@@ -108,6 +108,86 @@
with `a \<le> b` show ?thesis by auto
qed
+lemma fine_covers_all:
+ assumes "fine \<delta> (a, c) D" and "a < x" and "x \<le> c"
+ shows "\<exists> N < length D. \<forall> d t e. D ! N = (d,t,e) \<longrightarrow> d < x \<and> x \<le> e"
+ using assms
+proof (induct set: fine)
+ case (2 b c D a t)
+ thus ?case
+ proof (cases "b < x")
+ case True
+ with 2 obtain N where *: "N < length D"
+ and **: "\<And> d t e. D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" by auto
+ hence "Suc N < length ((a,t,b)#D) \<and>
+ (\<forall> d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
+ thus ?thesis by auto
+ next
+ case False with 2
+ have "0 < length ((a,t,b)#D) \<and>
+ (\<forall> d t' e. ((a,t,b)#D) ! 0 = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
+ thus ?thesis by auto
+ qed
+qed auto
+
+lemma fine_append_split:
+ assumes "fine \<delta> (a,b) D" and "D2 \<noteq> []" and "D = D1 @ D2"
+ shows "fine \<delta> (a,fst (hd D2)) D1" (is "?fine1")
+ and "fine \<delta> (fst (hd D2), b) D2" (is "?fine2")
+proof -
+ from assms
+ have "?fine1 \<and> ?fine2"
+ proof (induct arbitrary: D1 D2)
+ case (2 b c D a' x D1 D2)
+ note induct = this
+
+ thus ?case
+ proof (cases D1)
+ case Nil
+ hence "fst (hd D2) = a'" using 2 by auto
+ with fine_Cons[OF `fine \<delta> (b,c) D` induct(3,4,5)] Nil induct
+ show ?thesis by (auto intro: fine_Nil)
+ next
+ case (Cons d1 D1')
+ with induct(2)[OF `D2 \<noteq> []`, of D1'] induct(8)
+ have "fine \<delta> (b, fst (hd D2)) D1'" and "fine \<delta> (fst (hd D2), c) D2" and
+ "d1 = (a', x, b)" by auto
+ with fine_Cons[OF this(1) induct(3,4,5), OF induct(6)] Cons
+ show ?thesis by auto
+ qed
+ qed auto
+ thus ?fine1 and ?fine2 by auto
+qed
+
+lemma fine_\<delta>_expand:
+ assumes "fine \<delta> (a,b) D"
+ and "\<And> x. \<lbrakk> a \<le> x ; x \<le> b \<rbrakk> \<Longrightarrow> \<delta> x \<le> \<delta>' x"
+ shows "fine \<delta>' (a,b) D"
+using assms proof induct
+ case 1 show ?case by (rule fine_Nil)
+next
+ case (2 b c D a x)
+ show ?case
+ proof (rule fine_Cons)
+ show "fine \<delta>' (b,c) D" using 2 by auto
+ from fine_imp_le[OF 2(1)] 2(6) `x \<le> b`
+ show "b - a < \<delta>' x"
+ using 2(7)[OF `a \<le> x`] by auto
+ qed (auto simp add: 2)
+qed
+
+lemma fine_single_boundaries:
+ assumes "fine \<delta> (a,b) D" and "D = [(d, t, e)]"
+ shows "a = d \<and> b = e"
+using assms proof induct
+ case (2 b c D a x)
+ hence "D = []" and "a = d" and "b = e" by auto
+ moreover
+ from `fine \<delta> (b,c) D` `D = []` have "b = c"
+ by (rule empty_fine_imp_eq)
+ ultimately show ?case by simp
+qed auto
+
subsection {* Riemann sum *}
@@ -133,6 +213,9 @@
lemma rsum_add: "rsum D (\<lambda>x. f x + g x) = rsum D f + rsum D g"
by (induct D, auto simp add: algebra_simps)
+lemma rsum_append: "rsum (D1 @ D2) f = rsum D1 f + rsum D2 f"
+unfolding rsum_def map_append listsum_append ..
+
subsection {* Gauge integrability (definite) *}
@@ -232,6 +315,144 @@
algebra_simps rsum_right_distrib)
done
+lemma Integral_add:
+ assumes "Integral (a, b) f x1"
+ assumes "Integral (b, c) f x2"
+ assumes "a \<le> b" and "b \<le> c"
+ shows "Integral (a, c) f (x1 + x2)"
+proof (cases "a < b \<and> b < c", simp only: Integral_def split_conv, rule allI, rule impI)
+ fix \<epsilon> :: real assume "0 < \<epsilon>"
+ hence "0 < \<epsilon> / 2" by auto
+
+ assume "a < b \<and> b < c"
+ hence "a < b" and "b < c" by auto
+
+ from `Integral (a, b) f x1`[simplified Integral_def split_conv,
+ rule_format, OF `0 < \<epsilon>/2`]
+ obtain \<delta>1 where \<delta>1_gauge: "gauge {a..b} \<delta>1"
+ and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)" by auto
+
+ from `Integral (b, c) f x2`[simplified Integral_def split_conv,
+ rule_format, OF `0 < \<epsilon>/2`]
+ obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2"
+ and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)" by auto
+
+ def \<delta> \<equiv> "\<lambda> x. if x < b then min (\<delta>1 x) (b - x)
+ else if x = b then min (\<delta>1 b) (\<delta>2 b)
+ else min (\<delta>2 x) (x - b)"
+
+ have "gauge {a..c} \<delta>"
+ using \<delta>1_gauge \<delta>2_gauge unfolding \<delta>_def gauge_def by auto
+ moreover {
+ fix D :: "(real \<times> real \<times> real) list"
+ assume fine: "fine \<delta> (a,c) D"
+ from fine_covers_all[OF this `a < b` `b \<le> c`]
+ obtain N where "N < length D"
+ and *: "\<forall> d t e. D ! N = (d, t, e) \<longrightarrow> d < b \<and> b \<le> e"
+ by auto
+ obtain d t e where D_eq: "D ! N = (d, t, e)" by (cases "D!N", auto)
+ with * have "d < b" and "b \<le> e" by auto
+ have in_D: "(d, t, e) \<in> set D"
+ using D_eq[symmetric] using `N < length D` by auto
+
+ from mem_fine[OF fine in_D]
+ have "d < e" and "d \<le> t" and "t \<le> e" by auto
+
+ have "t = b"
+ proof (rule ccontr)
+ assume "t \<noteq> b"
+ with mem_fine3[OF fine in_D] `b \<le> e` `d \<le> t` `t \<le> e` `d < b` \<delta>_def
+ show False by (cases "t < b") auto
+ qed
+
+ let ?D1 = "take N D"
+ let ?D2 = "drop N D"
+ def D1 \<equiv> "take N D @ [(d, t, b)]"
+ def D2 \<equiv> "(if b = e then [] else [(b, t, e)]) @ drop (Suc N) D"
+
+ have "D \<noteq> []" using `N < length D` by auto
+ from hd_drop_conv_nth[OF this `N < length D`]
+ have "fst (hd ?D2) = d" using `D ! N = (d, t, e)` by auto
+ with fine_append_split[OF _ _ append_take_drop_id[symmetric]]
+ have fine1: "fine \<delta> (a,d) ?D1" and fine2: "fine \<delta> (d,c) ?D2"
+ using `N < length D` fine by auto
+
+ have "fine \<delta>1 (a,b) D1" unfolding D1_def
+ proof (rule fine_append)
+ show "fine \<delta>1 (a, d) ?D1"
+ proof (rule fine1[THEN fine_\<delta>_expand])
+ fix x assume "a \<le> x" "x \<le> d"
+ hence "x \<le> b" using `d < b` `x \<le> d` by auto
+ thus "\<delta> x \<le> \<delta>1 x" unfolding \<delta>_def by auto
+ qed
+
+ have "b - d < \<delta>1 t"
+ using mem_fine3[OF fine in_D] \<delta>_def `b \<le> e` `t = b` by auto
+ from `d < b` `d \<le> t` `t = b` this
+ show "fine \<delta>1 (d, b) [(d, t, b)]" using fine_single by auto
+ qed
+ note rsum1 = I1[OF this]
+
+ have drop_split: "drop N D = [D ! N] @ drop (Suc N) D"
+ using nth_drop'[OF `N < length D`] by simp
+
+ have fine2: "fine \<delta>2 (e,c) (drop (Suc N) D)"
+ proof (cases "drop (Suc N) D = []")
+ case True
+ note * = fine2[simplified drop_split True D_eq append_Nil2]
+ have "e = c" using fine_single_boundaries[OF * refl] by auto
+ thus ?thesis unfolding True using fine_Nil by auto
+ next
+ case False
+ note * = fine_append_split[OF fine2 False drop_split]
+ from fine_single_boundaries[OF *(1)]
+ have "fst (hd (drop (Suc N) D)) = e" using D_eq by auto
+ with *(2) have "fine \<delta> (e,c) (drop (Suc N) D)" by auto
+ thus ?thesis
+ proof (rule fine_\<delta>_expand)
+ fix x assume "e \<le> x" and "x \<le> c"
+ thus "\<delta> x \<le> \<delta>2 x" using `b \<le> e` unfolding \<delta>_def by auto
+ qed
+ qed
+
+ have "fine \<delta>2 (b, c) D2"
+ proof (cases "e = b")
+ case True thus ?thesis using fine2 by (simp add: D1_def D2_def)
+ next
+ case False
+ have "e - b < \<delta>2 b"
+ using mem_fine3[OF fine in_D] \<delta>_def `d < b` `t = b` by auto
+ with False `t = b` `b \<le> e`
+ show ?thesis using D2_def
+ by (auto intro!: fine_append[OF _ fine2] fine_single
+ simp del: append_Cons)
+ qed
+ note rsum2 = I2[OF this]
+
+ have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f"
+ using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto
+ also have "\<dots> = rsum D1 f + rsum D2 f"
+ by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append algebra_simps)
+ finally have "\<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>"
+ using add_strict_mono[OF rsum1 rsum2] by simp
+ }
+ ultimately show "\<exists> \<delta>. gauge {a .. c} \<delta> \<and>
+ (\<forall>D. fine \<delta> (a,c) D \<longrightarrow> \<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>)"
+ by blast
+next
+ case False
+ hence "a = b \<or> b = c" using `a \<le> b` and `b \<le> c` by auto
+ thus ?thesis
+ proof (rule disjE)
+ assume "a = b" hence "x1 = 0"
+ using `Integral (a, b) f x1` Integral_zero Integral_unique[of a b] by auto
+ thus ?thesis using `a = b` `Integral (b, c) f x2` by auto
+ next
+ assume "b = c" hence "x2 = 0"
+ using `Integral (b, c) f x2` Integral_zero Integral_unique[of b c] by auto
+ thus ?thesis using `b = c` `Integral (a, b) f x1` by auto
+ qed
+qed
text{*Fundamental theorem of calculus (Part I)*}
@@ -339,18 +560,6 @@
lemma Integral_subst: "[| Integral(a,b) f k1; k2=k1 |] ==> Integral(a,b) f k2"
by simp
-lemma Integral_add:
- "[| a \<le> b; b \<le> c; Integral(a,b) f' k1; Integral(b,c) f' k2;
- \<forall>x. a \<le> x & x \<le> c --> DERIV f x :> f' x |]
- ==> Integral(a,c) f' (k1 + k2)"
-apply (rule FTC1 [THEN Integral_subst], auto)
-apply (frule FTC1, auto)
-apply (frule_tac a = b in FTC1, auto)
-apply (drule_tac x = x in spec, auto)
-apply (drule_tac ?k2.0 = "f b - f a" in Integral_unique)
-apply (drule_tac [3] ?k2.0 = "f c - f b" in Integral_unique, auto)
-done
-
subsection {* Additivity Theorem of Gauge Integral *}
text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *}
--- a/src/HOL/IsaMakefile Tue Jun 02 23:49:46 2009 -0700
+++ b/src/HOL/IsaMakefile Tue Jun 02 23:56:12 2009 -0700
@@ -316,6 +316,7 @@
Library/Abstract_Rat.thy \
Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy \
Library/Euclidean_Space.thy Library/Sum_Of_Squares.thy Library/positivstellensatz.ML \
+ Library/Convex_Euclidean_Space.thy \
Library/sum_of_squares.ML Library/Glbs.thy Library/normarith.ML \
Library/Executable_Set.thy Library/Infinite_Set.thy \
Library/FuncSet.thy Library/Permutations.thy Library/Determinants.thy\
@@ -837,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 23:49:46 2009 -0700
+++ b/src/HOL/Library/Code_Integer.thy Tue Jun 02 23:56:12 2009 -0700
@@ -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/Convex_Euclidean_Space.thy Tue Jun 02 23:49:46 2009 -0700
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy Tue Jun 02 23:56:12 2009 -0700
@@ -1,6 +1,6 @@
-(* Title: Convex
- ID: $Id:
- Author: Robert Himmelmann, TU Muenchen*)
+(* Title: HOL/Library/Convex_Euclidean_Space.thy
+ Author: Robert Himmelmann, TU Muenchen
+*)
header {* Convex sets, functions and related things. *}
@@ -2196,7 +2196,7 @@
lemma convex_interval: "convex {a .. b}" "convex {a<..<b::real^'n::finite}"
apply(rule_tac[!] is_interval_convex) using is_interval_interval by auto
-subsection {* On real^1, is_interval, convex and connected are all equivalent. *}
+subsection {* On @{text "real^1"}, @{text "is_interval"}, @{text "convex"} and @{text "connected"} are all equivalent. *}
lemma is_interval_1:
"is_interval s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b \<longrightarrow> x \<in> s)"
--- a/src/HOL/Library/Efficient_Nat.thy Tue Jun 02 23:49:46 2009 -0700
+++ b/src/HOL/Library/Efficient_Nat.thy Tue Jun 02 23:56:12 2009 -0700
@@ -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 23:56:12 2009 -0700
@@ -0,0 +1,1601 @@
+
+(* 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.
+*}
+
+
+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/Formal_Power_Series.thy Tue Jun 02 23:49:46 2009 -0700
+++ b/src/HOL/Library/Formal_Power_Series.thy Tue Jun 02 23:56:12 2009 -0700
@@ -329,7 +329,8 @@
lemma fps_const_add [simp]: "fps_const (c::'a\<Colon>monoid_add) + fps_const d = fps_const (c + d)"
by (simp add: fps_ext)
-
+lemma fps_const_sub [simp]: "fps_const (c::'a\<Colon>group_add) - fps_const d = fps_const (c - d)"
+ by (simp add: fps_ext)
lemma fps_const_mult[simp]: "fps_const (c::'a\<Colon>ring) * fps_const d = fps_const (c * d)"
by (simp add: fps_eq_iff fps_mult_nth setsum_0')
@@ -396,6 +397,18 @@
qed (rule number_of_fps_def)
end
+lemma number_of_fps_const: "(number_of k::('a::comm_ring_1) fps) = fps_const (of_int k)"
+
+proof(induct k rule: int_induct[where k=0])
+ case base thus ?case unfolding number_of_fps_def of_int_0 by simp
+next
+ case (step1 i) thus ?case unfolding number_of_fps_def
+ by (simp add: fps_const_add[symmetric] del: fps_const_add)
+next
+ case (step2 i) thus ?case unfolding number_of_fps_def
+ by (simp add: fps_const_sub[symmetric] del: fps_const_sub)
+qed
+
subsection{* Inverses of formal power series *}
declare setsum_cong[fundef_cong]
@@ -956,6 +969,9 @@
"fps_const (a::'a::{comm_ring_1}) oo b = fps_const (a)"
by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta)
+lemma number_of_compose[simp]: "(number_of k::('a::{comm_ring_1}) fps) oo b = number_of k"
+ unfolding number_of_fps_const by simp
+
lemma X_fps_compose_startby0[simp]: "a$0 = 0 \<Longrightarrow> X oo a = (a :: ('a :: comm_ring_1) fps)"
by (simp add: fps_eq_iff fps_compose_def mult_delta_left setsum_delta
power_Suc not_le)
@@ -2262,6 +2278,45 @@
show "?dia = inverse ?d" by simp
qed
+lemma fps_inv_idempotent:
+ assumes a0: "a$0 = 0" and a1: "a$1 \<noteq> 0"
+ shows "fps_inv (fps_inv a) = a"
+proof-
+ let ?r = "fps_inv"
+ have ra0: "?r a $ 0 = 0" by (simp add: fps_inv_def)
+ from a1 have ra1: "?r a $ 1 \<noteq> 0" by (simp add: fps_inv_def field_simps)
+ have X0: "X$0 = 0" by simp
+ from fps_inv[OF ra0 ra1] have "?r (?r a) oo ?r a = X" .
+ then have "?r (?r a) oo ?r a oo a = X oo a" by simp
+ then have "?r (?r a) oo (?r a oo a) = a"
+ unfolding X_fps_compose_startby0[OF a0]
+ unfolding fps_compose_assoc[OF a0 ra0, symmetric] .
+ then show ?thesis unfolding fps_inv[OF a0 a1] by simp
+qed
+
+lemma fps_ginv_ginv:
+ assumes a0: "a$0 = 0" and a1: "a$1 \<noteq> 0"
+ and c0: "c$0 = 0" and c1: "c$1 \<noteq> 0"
+ shows "fps_ginv b (fps_ginv c a) = b oo a oo fps_inv c"
+proof-
+ let ?r = "fps_ginv"
+ from c0 have rca0: "?r c a $0 = 0" by (simp add: fps_ginv_def)
+ from a1 c1 have rca1: "?r c a $ 1 \<noteq> 0" by (simp add: fps_ginv_def field_simps)
+ from fps_ginv[OF rca0 rca1]
+ have "?r b (?r c a) oo ?r c a = b" .
+ then have "?r b (?r c a) oo ?r c a oo a = b oo a" by simp
+ then have "?r b (?r c a) oo (?r c a oo a) = b oo a"
+ apply (subst fps_compose_assoc)
+ using a0 c0 by (auto simp add: fps_ginv_def)
+ then have "?r b (?r c a) oo c = b oo a"
+ unfolding fps_ginv[OF a0 a1] .
+ then have "?r b (?r c a) oo c oo fps_inv c= b oo a oo fps_inv c" by simp
+ then have "?r b (?r c a) oo (c oo fps_inv c) = b oo a oo fps_inv c"
+ apply (subst fps_compose_assoc)
+ using a0 c0 by (auto simp add: fps_inv_def)
+ then show ?thesis unfolding fps_inv_right[OF c0 c1] by simp
+qed
+
subsection{* Elementary series *}
subsubsection{* Exponential series *}
@@ -2330,7 +2385,6 @@
lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::field_char_0)) = (fps_const a)^n * (E a)"
by (induct n, auto simp add: power_Suc)
-
lemma X_compose_E[simp]: "X oo E (a::'a::{field}) = E a - 1"
by (simp add: fps_eq_iff X_fps_compose)
@@ -2348,10 +2402,9 @@
lemma fps_const_inverse:
- "inverse (fps_const (a::'a::{field, division_by_zero})) = fps_const (inverse a)"
+ "a \<noteq> 0 \<Longrightarrow> inverse (fps_const (a::'a::field)) = fps_const (inverse a)"
apply (auto simp add: fps_eq_iff fps_inverse_def) by (case_tac "n", auto)
-
lemma inverse_one_plus_X:
"inverse (1 + X) = Abs_fps (\<lambda>n. (- 1 ::'a::{field})^n)"
(is "inverse ?l = ?r")
@@ -2365,21 +2418,45 @@
lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)"
by (induct n, auto simp add: ring_simps E_add_mult power_Suc)
-subsubsection{* Logarithmic series *}
-definition "(L::'a::field_char_0 fps)
- = Abs_fps (\<lambda>n. (- 1) ^ Suc n / of_nat n)"
+lemma assumes r: "r (Suc k) 1 = 1"
+ shows "fps_radical r (Suc k) (E (c::'a::{field_char_0})) = E (c / of_nat (Suc k))"
+proof-
+ let ?ck = "(c / of_nat (Suc k))"
+ let ?r = "fps_radical r (Suc k)"
+ have eq0[simp]: "?ck * of_nat (Suc k) = c" "of_nat (Suc k) * ?ck = c"
+ by (simp_all del: of_nat_Suc)
+ have th0: "E ?ck ^ (Suc k) = E c" unfolding E_power_mult eq0 ..
+ have th: "r (Suc k) (E c $0) ^ Suc k = E c $ 0"
+ "r (Suc k) (E c $ 0) = E ?ck $ 0" "E c $ 0 \<noteq> 0" using r by simp_all
+ from th0 radical_unique[where r=r and k=k, OF th]
+ show ?thesis by auto
+qed
-lemma fps_deriv_L: "fps_deriv L = inverse (1 + X)"
- unfolding inverse_one_plus_X
- by (simp add: L_def fps_eq_iff power_Suc del: of_nat_Suc)
+lemma Ec_E1_eq:
+ "E (1::'a::{field_char_0}) oo (fps_const c * X) = E c"
+ apply (auto simp add: fps_eq_iff E_def fps_compose_def power_mult_distrib)
+ by (simp add: cond_value_iff cond_application_beta setsum_delta' cong del: if_weak_cong)
+subsubsection{* Logarithmic series *}
-lemma L_nth: "L $ n = (- 1) ^ Suc n / of_nat n"
- by (simp add: L_def)
+lemma Abs_fps_if_0:
+ "Abs_fps(%n. if n=0 then (v::'a::ring_1) else f n) = fps_const v + X * Abs_fps (%n. f (Suc n))"
+ by (auto simp add: fps_eq_iff)
+
+definition L:: "'a::{field_char_0} \<Rightarrow> 'a fps" where
+ "L c \<equiv> fps_const (1/c) * Abs_fps (\<lambda>n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n)"
+lemma fps_deriv_L: "fps_deriv (L c) = fps_const (1/c) * inverse (1 + X)"
+ unfolding inverse_one_plus_X
+ by (simp add: L_def fps_eq_iff del: of_nat_Suc)
+
+lemma L_nth: "L c $ n = (if n=0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))"
+ by (simp add: L_def field_simps)
+
+lemma L_0[simp]: "L c $ 0 = 0" by (simp add: L_def)
lemma L_E_inv:
- assumes a: "a \<noteq> (0::'a::{field_char_0,division_by_zero})"
- shows "L = fps_const a * fps_inv (E a - 1)" (is "?l = ?r")
+ assumes a: "a\<noteq> (0::'a::{field_char_0})"
+ shows "L a = fps_inv (E a - 1)" (is "?l = ?r")
proof-
let ?b = "E a - 1"
have b0: "?b $ 0 = 0" by simp
@@ -2391,15 +2468,29 @@
finally have eq: "fps_deriv (E a - 1) oo fps_inv (E a - 1) = fps_const a * (X + 1)" .
from fps_inv_deriv[OF b0 b1, unfolded eq]
have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (X + 1)"
+ using a
by (simp add: fps_const_inverse eq fps_divide_def fps_inverse_mult)
- hence "fps_deriv (fps_const a * fps_inv ?b) = inverse (X + 1)"
- using a by (simp add: fps_divide_def field_simps)
hence "fps_deriv ?l = fps_deriv ?r"
- by (simp add: fps_deriv_L add_commute)
+ by (simp add: fps_deriv_L add_commute fps_divide_def divide_inverse)
then show ?thesis unfolding fps_deriv_eq_iff
by (simp add: L_nth fps_inv_def)
qed
+lemma L_mult_add:
+ assumes c0: "c\<noteq>0" and d0: "d\<noteq>0"
+ shows "L c + L d = fps_const (c+d) * L (c*d)"
+ (is "?r = ?l")
+proof-
+ from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_simps)
+ have "fps_deriv ?r = fps_const (1/c + 1/d) * inverse (1 + X)"
+ by (simp add: fps_deriv_L fps_const_add[symmetric] algebra_simps del: fps_const_add)
+ also have "\<dots> = fps_deriv ?l"
+ apply (simp add: fps_deriv_L)
+ by (simp add: fps_eq_iff eq)
+ finally show ?thesis
+ unfolding fps_deriv_eq_iff by simp
+qed
+
subsubsection{* Formal trigonometric functions *}
definition "fps_sin (c::'a::field_char_0) =
--- a/src/HOL/Library/Library.thy Tue Jun 02 23:49:46 2009 -0700
+++ b/src/HOL/Library/Library.thy Tue Jun 02 23:56:12 2009 -0700
@@ -14,6 +14,7 @@
Commutative_Ring
Continuity
ContNotDenum
+ Convex_Euclidean_Space
Countable
Determinants
Diagonalize
@@ -21,6 +22,7 @@
Enum
Eval_Witness
Executable_Set
+ Fin_Fun
Float
Formal_Power_Series
FrechetDeriv
--- a/src/HOL/List.thy Tue Jun 02 23:49:46 2009 -0700
+++ b/src/HOL/List.thy Tue Jun 02 23:56:12 2009 -0700
@@ -2464,6 +2464,12 @@
case False with d show ?thesis by auto
qed
+lemma distinct_concat:
+ assumes "distinct xs"
+ and "\<And> ys. ys \<in> set xs \<Longrightarrow> distinct ys"
+ and "\<And> ys zs. \<lbrakk> ys \<in> set xs ; zs \<in> set xs ; ys \<noteq> zs \<rbrakk> \<Longrightarrow> set ys \<inter> set zs = {}"
+ shows "distinct (concat xs)"
+ using assms by (induct xs) auto
text {* It is best to avoid this indexed version of distinct, but
sometimes it is useful. *}
@@ -2617,6 +2623,10 @@
lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"
by (induct n) auto
+lemma map_replicate_const:
+ "map (\<lambda> x. k) lst = replicate (length lst) k"
+ by (induct lst) auto
+
lemma replicate_app_Cons_same:
"(replicate n x) @ (x # xs) = x # replicate n x @ xs"
by (induct n) auto
@@ -2696,6 +2706,9 @@
"map (\<lambda>i. x) [0..<i] = replicate i x"
by (induct i) (simp_all add: replicate_append_same)
+lemma concat_replicate_trivial[simp]:
+ "concat (replicate i []) = []"
+ by (induct i) (auto simp add: map_replicate_const)
lemma replicate_empty[simp]: "(replicate n x = []) \<longleftrightarrow> n=0"
by (induct n) auto
--- a/src/HOL/Map.thy Tue Jun 02 23:49:46 2009 -0700
+++ b/src/HOL/Map.thy Tue Jun 02 23:56:12 2009 -0700
@@ -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/atp_manager.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/HOL/Tools/atp_manager.ML Tue Jun 02 23:56:12 2009 -0700
@@ -81,9 +81,9 @@
fun ord ((a, _), (b, _)) = Time.compare (a, b);
);
-val lookup_thread = AList.lookup Thread.equal;
-val delete_thread = AList.delete Thread.equal;
-val update_thread = AList.update Thread.equal;
+fun lookup_thread xs = AList.lookup Thread.equal xs;
+fun delete_thread xs = AList.delete Thread.equal xs;
+fun update_thread xs = AList.update Thread.equal xs;
(* state of thread manager *)
@@ -104,6 +104,7 @@
val state = Synchronized.var "atp_manager"
(make_state NONE ThreadHeap.empty ThreadHeap.empty [] [] [] []);
+
(* unregister thread *)
fun unregister (success, message) thread = Synchronized.change state
--- a/src/HOL/Tools/atp_wrapper.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/HOL/Tools/atp_wrapper.ML Tue Jun 02 23:56:12 2009 -0700
@@ -113,13 +113,13 @@
fun tptp_prover_opts max_new theory_const =
tptp_prover_opts_full max_new theory_const false;
-val tptp_prover = tptp_prover_opts 60 true;
+fun tptp_prover x = tptp_prover_opts 60 true x;
(*for structured proofs: prover must support TSTP*)
fun full_prover_opts max_new theory_const =
tptp_prover_opts_full max_new theory_const true;
-val full_prover = full_prover_opts 60 true;
+fun full_prover x = full_prover_opts 60 true x;
(* Vampire *)
--- a/src/HOL/Tools/datatype_package.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/HOL/Tools/datatype_package.ML Tue Jun 02 23:56:12 2009 -0700
@@ -386,7 +386,8 @@
val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
descr sorts thy9;
- val dt_infos = map (make_dt_info NONE (flat descr) sorts induct reccomb_names rec_thms)
+ val dt_infos = map
+ (make_dt_info (SOME new_type_names) (flat descr) sorts induct reccomb_names rec_thms)
((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
@@ -586,7 +587,7 @@
val _ = (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
[] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
- fun prep_dt_spec (tvs, tname, mx, constrs) (dts', constr_syntax, sorts, i) =
+ fun prep_dt_spec ((tvs, tname, mx, constrs), tname') (dts', constr_syntax, sorts, i) =
let
fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
let
@@ -595,7 +596,7 @@
[] => ()
| vs => error ("Extra type variables on rhs: " ^ commas vs))
in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
- Sign.full_name_path tmp_thy (Binding.name_of tname))
+ Sign.full_name_path tmp_thy tname')
(Binding.map_name (Syntax.const_name mx') cname),
map (dtyp_of_typ new_dts) cargs')],
constr_syntax' @ [(cname, mx')], sorts'')
@@ -616,7 +617,8 @@
" in datatype " ^ quote (Binding.str_of tname))
end;
- val (dts', constr_syntax, sorts', i) = fold prep_dt_spec dts ([], [], [], 0);
+ val (dts', constr_syntax, sorts', i) =
+ fold prep_dt_spec (dts ~~ new_type_names) ([], [], [], 0);
val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (tyvars \\ map fst sorts'));
val dt_info = get_datatypes thy;
val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
--- a/src/HOL/Tools/nat_numeral_simprocs.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Tue Jun 02 23:56:12 2009 -0700
@@ -149,7 +149,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first_coeff = find_first_coeff []
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
[@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
@@ -238,7 +238,7 @@
val dest_coeff = dest_coeff
val left_distrib = @{thm left_add_mult_distrib} RS trans
val prove_conv = Arith_Data.prove_conv_nohyps
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
@@ -263,7 +263,7 @@
struct
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1 = Numeral_Simprocs.num_ss addsimps
numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
@@ -369,7 +369,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first = find_first_t []
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
val simplify_meta_eq = cancel_simplify_meta_eq
@@ -380,7 +380,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_eq_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj}
);
structure LessCancelFactor = ExtractCommonTermFun
@@ -388,7 +388,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_less_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj}
);
structure LeCancelFactor = ExtractCommonTermFun
@@ -396,7 +396,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq}
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_le_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj}
);
structure DivideCancelFactor = ExtractCommonTermFun
@@ -404,7 +404,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_div_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_div_cancel_disj}
);
structure DvdCancelFactor = ExtractCommonTermFun
@@ -412,7 +412,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
- val simp_conv = K(K (SOME @{thm nat_mult_dvd_cancel_disj}))
+ fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj}
);
val cancel_factor =
--- a/src/HOL/Tools/numeral.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/HOL/Tools/numeral.ML Tue Jun 02 23:56:12 2009 -0700
@@ -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/Tools/numeral_simprocs.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/HOL/Tools/numeral_simprocs.ML Tue Jun 02 23:56:12 2009 -0700
@@ -232,7 +232,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
val find_first_coeff = find_first_coeff []
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
@@ -310,7 +310,7 @@
val dest_coeff = dest_coeff 1
val left_distrib = @{thm combine_common_factor} RS trans
val prove_conv = Arith_Data.prove_conv_nohyps
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
@@ -336,7 +336,7 @@
val dest_coeff = dest_fcoeff 1
val left_distrib = @{thm combine_common_factor} RS trans
val prove_conv = Arith_Data.prove_conv_nohyps
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps
fun norm_tac ss =
@@ -387,7 +387,7 @@
struct
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
@@ -533,7 +533,7 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first = find_first_t []
- val trans_tac = K Arith_Data.trans_tac
+ fun trans_tac _ = Arith_Data.trans_tac
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
val simplify_meta_eq = cancel_simplify_meta_eq
@@ -545,7 +545,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
- val simp_conv = K (K (SOME @{thm mult_cancel_left}))
+ fun simp_conv _ _ = SOME @{thm mult_cancel_left}
);
(*for ordered rings*)
@@ -574,7 +574,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.div}
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
- val simp_conv = K (K (SOME @{thm div_mult_mult1_if}))
+ fun simp_conv _ _ = SOME @{thm div_mult_mult1_if}
);
structure ModCancelFactor = ExtractCommonTermFun
@@ -582,7 +582,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.mod}
val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT
- val simp_conv = K (K (SOME @{thm mod_mult_mult1}))
+ fun simp_conv _ _ = SOME @{thm mod_mult_mult1}
);
(*for idoms*)
@@ -591,7 +591,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
- val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left}))
+ fun simp_conv _ _ = SOME @{thm dvd_mult_cancel_left}
);
(*Version for all fields, including unordered ones (type complex).*)
@@ -600,7 +600,7 @@
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name HOL.divide}
val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
- val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if}))
+ fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
);
val cancel_factors =
--- a/src/HOL/ex/Codegenerator.thy Tue Jun 02 23:49:46 2009 -0700
+++ /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 23:56:12 2009 -0700
@@ -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 23:49:46 2009 -0700
+++ b/src/HOL/ex/Codegenerator_Pretty.thy Tue Jun 02 23:56:12 2009 -0700
@@ -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 23:56:12 2009 -0700
@@ -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 23:56:12 2009 -0700
@@ -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 23:49:46 2009 -0700
+++ /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 23:56:12 2009 -0700
@@ -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 23:49:46 2009 -0700
+++ b/src/HOL/ex/ROOT.ML Tue Jun 02 23:56:12 2009 -0700
@@ -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/Pure/General/markup.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/Pure/General/markup.ML Tue Jun 02 23:56:12 2009 -0700
@@ -108,6 +108,7 @@
val pidN: string
val sessionN: string
val promptN: string val prompt: T
+ val readyN: string val ready: T
val no_output: output * output
val default_output: T -> output * output
val add_mode: string -> (T -> output * output) -> unit
@@ -307,6 +308,7 @@
val sessionN = "session";
val (promptN, prompt) = markup_elem "prompt";
+val (readyN, ready) = markup_elem "ready";
--- a/src/Pure/General/markup.scala Tue Jun 02 23:49:46 2009 -0700
+++ b/src/Pure/General/markup.scala Tue Jun 02 23:56:12 2009 -0700
@@ -163,6 +163,8 @@
val SIGNAL = "signal"
val EXIT = "exit"
+ val READY = "ready"
+
/* content */
--- a/src/Pure/General/secure.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/Pure/General/secure.ML Tue Jun 02 23:56:12 2009 -0700
@@ -9,6 +9,7 @@
val set_secure: unit -> unit
val is_secure: unit -> bool
val deny_secure: string -> unit
+ val secure_mltext: unit -> unit
val use_text: use_context -> int * string -> bool -> string -> unit
val use_file: use_context -> bool -> string -> unit
val toplevel_pp: string list -> string -> unit
--- a/src/Pure/IsaMakefile Tue Jun 02 23:49:46 2009 -0700
+++ b/src/Pure/IsaMakefile Tue Jun 02 23:56:12 2009 -0700
@@ -55,19 +55,20 @@
General/table.ML General/url.ML General/xml.ML General/yxml.ML \
Isar/ROOT.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \
Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \
- Isar/constdefs.ML Isar/context_rules.ML \
- Isar/element.ML Isar/expression.ML Isar/isar_cmd.ML \
- Isar/isar_document.ML Isar/isar_syn.ML Isar/local_defs.ML \
- Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \
- Isar/method.ML Isar/object_logic.ML Isar/obtain.ML \
- Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \
- Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \
- Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \
- Isar/rule_cases.ML Isar/rule_insts.ML Isar/skip_proof.ML \
- Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML \
- Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML \
- ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \
- ML/ml_test.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
+ Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \
+ Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML \
+ Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \
+ Isar/local_theory.ML Isar/locale.ML Isar/method.ML \
+ Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \
+ Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \
+ Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \
+ Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \
+ Isar/rule_insts.ML Isar/skip_proof.ML Isar/spec_parse.ML \
+ Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML \
+ Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_compiler.ML \
+ ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML \
+ ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML \
+ ML-Systems/install_pp_polyml.ML \
ML-Systems/install_pp_polyml-experimental.ML \
ML-Systems/use_context.ML Proof/extraction.ML \
Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
--- a/src/Pure/Isar/ROOT.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/Pure/Isar/ROOT.ML Tue Jun 02 23:56:12 2009 -0700
@@ -24,6 +24,13 @@
use "outer_parse.ML";
use "value_parse.ML";
use "args.ML";
+
+(*ML support*)
+use "../ML/ml_syntax.ML";
+use "../ML/ml_env.ML";
+if ml_system = "polyml-experimental"
+then use "../ML/ml_compiler_polyml-5.3.ML"
+else use "../ML/ml_compiler.ML";
use "../ML/ml_context.ML";
(*theory sources*)
--- a/src/Pure/Isar/attrib.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/Pure/Isar/attrib.ML Tue Jun 02 23:56:12 2009 -0700
@@ -240,7 +240,7 @@
(* rename_abs *)
-val rename_abs = Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars');
+fun rename_abs x = (Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars')) x;
(* unfold / fold definitions *)
--- a/src/Pure/Isar/isar_syn.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/Pure/Isar/isar_syn.ML Tue Jun 02 23:56:12 2009 -0700
@@ -296,11 +296,11 @@
(* use ML text *)
fun propagate_env (context as Context.Proof lthy) =
- Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
+ Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
| propagate_env context = context;
fun propagate_env_prf prf = Proof.map_contexts
- (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf;
+ (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf;
val _ =
OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl)
--- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML Tue Jun 02 23:56:12 2009 -0700
@@ -1,6 +1,6 @@
(* Title: Pure/ML-Systems/compiler_polyml-5.0.ML
-Runtime compilation -- for PolyML.compilerEx in version 5.0 and 5.1.
+Runtime compilation for Poly/ML 5.0 and 5.1.
*)
fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
--- a/src/Pure/ML-Systems/polyml_common.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/Pure/ML-Systems/polyml_common.ML Tue Jun 02 23:56:12 2009 -0700
@@ -17,6 +17,8 @@
val forget_structure = PolyML.Compiler.forgetStructure;
+val _ = PolyML.Compiler.forgetValue "print";
+
(* Compiler options *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_compiler.ML Tue Jun 02 23:56:12 2009 -0700
@@ -0,0 +1,23 @@
+(* Title: Pure/ML/ml_compiler.ML
+ Author: Makarius
+
+Runtime compilation -- generic version.
+*)
+
+signature ML_COMPILER =
+sig
+ val eval: bool -> Position.T -> ML_Lex.token list -> unit
+end
+
+structure ML_Compiler: ML_COMPILER =
+struct
+
+fun eval verbose pos toks =
+ let
+ val line = the_default 1 (Position.line_of pos);
+ val file = the_default "ML" (Position.file_of pos);
+ val text = ML_Lex.flatten toks;
+ in Secure.use_text ML_Env.local_context (line, file) verbose text end;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Tue Jun 02 23:56:12 2009 -0700
@@ -0,0 +1,144 @@
+(* Title: Pure/ML/ml_compiler_polyml-5.3.ML
+ Author: Makarius
+
+Advanced runtime compilation for Poly/ML 5.3 (SVN 762).
+*)
+
+signature ML_COMPILER =
+sig
+ val eval: bool -> Position.T -> ML_Lex.token list -> unit
+end
+
+structure ML_Compiler: ML_COMPILER =
+struct
+
+(* original source positions *)
+
+fun position_of (SOME context) (loc: PolyML.location) =
+ (case pairself (ML_Env.token_position context) (#startPosition loc, #endPosition loc) of
+ (SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2)
+ | (SOME pos, NONE) => pos
+ | _ => Position.line_file (#startLine loc) (#file loc))
+ | position_of NONE (loc: PolyML.location) = Position.line_file (#startLine loc) (#file loc);
+
+
+(* parse trees *)
+
+fun report_parse_tree context depth space =
+ let
+ val pos_of = position_of context;
+ fun report loc (PolyML.PTtype types) =
+ PolyML.NameSpace.displayTypeExpression (types, depth, space)
+ |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
+ |> Position.report_text Markup.ML_typing (pos_of loc)
+ | report loc (PolyML.PTdeclaredAt decl) =
+ Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) ""
+ |> Position.report_text Markup.ML_ref (pos_of loc)
+ | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
+ | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
+ | report _ _ = ()
+ and report_tree (loc, props) = List.app (report loc) props;
+ in report_tree end;
+
+
+(* eval ML source tokens *)
+
+fun eval verbose pos toks =
+ let
+ val _ = Secure.secure_mltext ();
+ val {name_space = space, print, error = err, ...} = ML_Env.local_context;
+
+
+ (* input *)
+
+ val input =
+ if is_none (Context.thread_data ()) then map (pair 0) toks
+ else Context.>>> (ML_Env.register_tokens toks);
+ val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input);
+
+ val current_line = ref (the_default 1 (Position.line_of pos));
+
+ fun get_index () =
+ the_default 0 (get_first (fn (_, []) => NONE | (i, _) => SOME i) (! input_buffer));
+
+ fun get () =
+ (case ! input_buffer of
+ [] => NONE
+ | (_, []) :: rest => (input_buffer := rest; get ())
+ | (i, c :: cs) :: rest =>
+ (input_buffer := (i, cs) :: rest;
+ if c = #"\n" then current_line := ! current_line + 1 else ();
+ SOME c));
+
+
+ (* output *)
+
+ val output_buffer = ref Buffer.empty;
+ fun output () = Buffer.content (! output_buffer);
+ fun put s = change output_buffer (Buffer.add s);
+
+ fun put_message {message, hard, location, context = _} =
+ (put (if hard then "Error: " else "Warning: ");
+ put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
+ put (Position.str_of (position_of (Context.thread_data ()) location) ^ "\n"));
+
+
+ (* results *)
+
+ val depth = get_print_depth ();
+
+ fun apply_result {fixes, types, signatures, structures, functors, values} =
+ let
+ fun display disp x =
+ if depth > 0 then
+ (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n")
+ else ();
+
+ fun apply_fix (a, b) =
+ (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b));
+ fun apply_type (a, b) =
+ (display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b));
+ fun apply_sig (a, b) =
+ (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b));
+ fun apply_struct (a, b) =
+ (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b));
+ fun apply_funct (a, b) =
+ (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b));
+ fun apply_val (a, b) =
+ (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b));
+ in
+ List.app apply_fix fixes;
+ List.app apply_type types;
+ List.app apply_sig signatures;
+ List.app apply_struct structures;
+ List.app apply_funct functors;
+ List.app apply_val values
+ end;
+
+ fun result_fun (phase1, phase2) () =
+ (case phase1 of NONE => ()
+ | SOME parse_tree => report_parse_tree (Context.thread_data ()) depth space parse_tree;
+ case phase2 of NONE => err "Static Errors"
+ | SOME code => apply_result (code ())); (* FIXME Toplevel.program *)
+
+
+ (* compiler invocation *)
+
+ val parameters =
+ [PolyML.Compiler.CPOutStream put,
+ PolyML.Compiler.CPNameSpace space,
+ PolyML.Compiler.CPErrorMessageProc put_message,
+ PolyML.Compiler.CPLineNo (fn () => ! current_line),
+ PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
+ PolyML.Compiler.CPLineOffset get_index,
+ PolyML.Compiler.CPCompilerResultFun result_fun];
+ val _ =
+ (while not (List.null (! input_buffer)) do
+ PolyML.compiler (get, parameters) ())
+ handle exn =>
+ (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+ err (output ()); raise exn);
+ in if verbose then print (output ()) else () end;
+
+end;
+
--- a/src/Pure/ML/ml_context.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/Pure/ML/ml_context.ML Tue Jun 02 23:56:12 2009 -0700
@@ -19,9 +19,6 @@
val the_global_context: unit -> theory
val the_local_context: unit -> Proof.context
val exec: (unit -> unit) -> Context.generic -> Context.generic
- val inherit_env: Context.generic -> Context.generic -> Context.generic
- val name_space: ML_Name_Space.T
- val local_context: use_context
val stored_thms: thm list ref
val ml_store_thm: string * thm -> unit
val ml_store_thms: string * thm list -> unit
@@ -54,78 +51,6 @@
| NONE => error "Missing context after execution");
-(* ML name space *)
-
-structure ML_Env = GenericDataFun
-(
- type T =
- ML_Name_Space.valueVal Symtab.table *
- ML_Name_Space.typeVal Symtab.table *
- ML_Name_Space.fixityVal Symtab.table *
- ML_Name_Space.structureVal Symtab.table *
- ML_Name_Space.signatureVal Symtab.table *
- ML_Name_Space.functorVal Symtab.table;
- val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
- val extend = I;
- fun merge _
- ((val1, type1, fixity1, structure1, signature1, functor1),
- (val2, type2, fixity2, structure2, signature2, functor2)) : T =
- (Symtab.merge (K true) (val1, val2),
- Symtab.merge (K true) (type1, type2),
- Symtab.merge (K true) (fixity1, fixity2),
- Symtab.merge (K true) (structure1, structure2),
- Symtab.merge (K true) (signature1, signature2),
- Symtab.merge (K true) (functor1, functor2));
-);
-
-val inherit_env = ML_Env.put o ML_Env.get;
-
-val name_space: ML_Name_Space.T =
- let
- fun lookup sel1 sel2 name =
- Context.thread_data ()
- |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (ML_Env.get context)) name)
- |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
-
- fun all sel1 sel2 () =
- Context.thread_data ()
- |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (ML_Env.get context)))
- |> append (sel2 ML_Name_Space.global ())
- |> sort_distinct (string_ord o pairself #1);
-
- fun enter ap1 sel2 entry =
- if is_some (Context.thread_data ()) then
- Context.>> (ML_Env.map (ap1 (Symtab.update entry)))
- else sel2 ML_Name_Space.global entry;
- in
- {lookupVal = lookup #1 #lookupVal,
- lookupType = lookup #2 #lookupType,
- lookupFix = lookup #3 #lookupFix,
- lookupStruct = lookup #4 #lookupStruct,
- lookupSig = lookup #5 #lookupSig,
- lookupFunct = lookup #6 #lookupFunct,
- enterVal = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal,
- enterType = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType,
- enterFix = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix,
- enterStruct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct,
- enterSig = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig,
- enterFunct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct,
- allVal = all #1 #allVal,
- allType = all #2 #allType,
- allFix = all #3 #allFix,
- allStruct = all #4 #allStruct,
- allSig = all #5 #allSig,
- allFunct = all #6 #allFunct}
- end;
-
-val local_context: use_context =
- {tune_source = ML_Parse.fix_ints,
- name_space = name_space,
- str_of_pos = Position.str_of oo Position.line_file,
- print = writeln,
- error = error};
-
-
(* theorem bindings *)
val stored_thms: thm list ref = ref [];
@@ -139,8 +64,8 @@
else if not (ML_Syntax.is_identifier name) then
error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
else setmp stored_thms ths' (fn () =>
- use_text local_context (0, "") true
- ("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);")) ();
+ ML_Compiler.eval true Position.none
+ (ML_Lex.tokenize ("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);"))) ();
in () end;
val ml_store_thms = ml_store "";
@@ -199,6 +124,7 @@
val struct_name = "Isabelle";
val begin_env = ML_Lex.tokenize ("structure " ^ struct_name ^ " =\nstruct\n");
val end_env = ML_Lex.tokenize "end;";
+val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";
in
@@ -240,26 +166,21 @@
fun eval verbose pos txt =
let
- fun eval_raw p = use_text local_context
- (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p));
-
(*prepare source text*)
val _ = Position.report Markup.ML_source pos;
val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
- val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ())
- |>> pairself (implode o map ML_Lex.text_of);
- val _ = if ! trace then tracing (cat_lines [env, body]) else ();
+ val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
+ val _ =
+ if ! trace then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
+ else ();
(*prepare static ML environment*)
val _ = Context.setmp_thread_data env_ctxt
- (fn () => (eval_raw Position.none false env; Context.thread_data ())) ()
- |> (fn NONE => () | SOME context' => Context.>> (inherit_env context'));
+ (fn () => (ML_Compiler.eval false Position.none env; Context.thread_data ())) ()
+ |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
- (*eval ML*)
- val _ = eval_raw pos verbose body;
-
- (*reset static ML environment*)
- val _ = eval_raw Position.none false "structure Isabelle = struct end";
+ val _ = ML_Compiler.eval verbose pos body;
+ val _ = ML_Compiler.eval false Position.none reset_env;
in () end;
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_env.ML Tue Jun 02 23:56:12 2009 -0700
@@ -0,0 +1,111 @@
+(* Title: Pure/ML/ml_env.ML
+ Author: Makarius
+
+Local environment of ML sources and results.
+*)
+
+signature ML_ENV =
+sig
+ val inherit: Context.generic -> Context.generic -> Context.generic
+ val register_tokens: ML_Lex.token list -> Context.generic ->
+ (serial * ML_Lex.token) list * Context.generic
+ val token_position: Context.generic -> serial -> Position.T option
+ val name_space: ML_Name_Space.T
+ val local_context: use_context
+end
+
+structure ML_Env: ML_ENV =
+struct
+
+(* context data *)
+
+structure Env = GenericDataFun
+(
+ type T =
+ Position.T Inttab.table *
+ (ML_Name_Space.valueVal Symtab.table *
+ ML_Name_Space.typeVal Symtab.table *
+ ML_Name_Space.fixityVal Symtab.table *
+ ML_Name_Space.structureVal Symtab.table *
+ ML_Name_Space.signatureVal Symtab.table *
+ ML_Name_Space.functorVal Symtab.table);
+ val empty =
+ (Inttab.empty,
+ (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
+ val extend = I;
+ fun merge _
+ ((toks1, (val1, type1, fixity1, structure1, signature1, functor1)),
+ (toks2, (val2, type2, fixity2, structure2, signature2, functor2))) : T =
+ (Inttab.merge (K true) (toks1, toks2),
+ (Symtab.merge (K true) (val1, val2),
+ Symtab.merge (K true) (type1, type2),
+ Symtab.merge (K true) (fixity1, fixity2),
+ Symtab.merge (K true) (structure1, structure2),
+ Symtab.merge (K true) (signature1, signature2),
+ Symtab.merge (K true) (functor1, functor2)));
+);
+
+val inherit = Env.put o Env.get;
+
+
+(* source tokens *)
+
+fun register_tokens toks context =
+ let
+ val regs = map (fn tok => (serial (), tok)) toks;
+ val context' = context
+ |> Env.map (apfst (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs));
+ in (regs, context') end;
+
+val token_position = Inttab.lookup o #1 o Env.get;
+
+
+(* results *)
+
+val name_space: ML_Name_Space.T =
+ let
+ fun lookup sel1 sel2 name =
+ Context.thread_data ()
+ |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#2 (Env.get context))) name)
+ |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
+
+ fun all sel1 sel2 () =
+ Context.thread_data ()
+ |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#2 (Env.get context))))
+ |> append (sel2 ML_Name_Space.global ())
+ |> sort_distinct (string_ord o pairself #1);
+
+ fun enter ap1 sel2 entry =
+ if is_some (Context.thread_data ()) then
+ Context.>> (Env.map (apsnd (ap1 (Symtab.update entry))))
+ else sel2 ML_Name_Space.global entry;
+ in
+ {lookupVal = lookup #1 #lookupVal,
+ lookupType = lookup #2 #lookupType,
+ lookupFix = lookup #3 #lookupFix,
+ lookupStruct = lookup #4 #lookupStruct,
+ lookupSig = lookup #5 #lookupSig,
+ lookupFunct = lookup #6 #lookupFunct,
+ enterVal = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal,
+ enterType = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType,
+ enterFix = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix,
+ enterStruct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct,
+ enterSig = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig,
+ enterFunct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct,
+ allVal = all #1 #allVal,
+ allType = all #2 #allType,
+ allFix = all #3 #allFix,
+ allStruct = all #4 #allStruct,
+ allSig = all #5 #allSig,
+ allFunct = all #6 #allFunct}
+ end;
+
+val local_context: use_context =
+ {tune_source = ML_Parse.fix_ints,
+ name_space = name_space,
+ str_of_pos = Position.str_of oo Position.line_file,
+ print = writeln,
+ error = error};
+
+end;
+
--- a/src/Pure/ML/ml_lex.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/Pure/ML/ml_lex.ML Tue Jun 02 23:56:12 2009 -0700
@@ -18,6 +18,7 @@
val kind_of: token -> token_kind
val content_of: token -> string
val text_of: token -> string
+ val flatten: token list -> string
val report_token: token -> unit
val keywords: string list
val source: (Symbol.symbol, 'a) Source.source ->
@@ -73,6 +74,8 @@
Error msg => error msg
| _ => Symbol.escape (content_of tok));
+val flatten = implode o map text_of;
+
fun is_regular (Token (_, (Error _, _))) = false
| is_regular (Token (_, (EOF, _))) = false
| is_regular _ = true;
--- a/src/Pure/ML/ml_test.ML Tue Jun 02 23:49:46 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,191 +0,0 @@
-(* Title: Pure/ML/ml_test.ML
- Author: Makarius
-
-Test of advanced ML compiler invocation in Poly/ML 5.3 (SVN 744).
-*)
-
-signature ML_TEST =
-sig
- val position_of: Proof.context -> PolyML.location -> Position.T
- val eval: bool -> Position.T -> ML_Lex.token list -> unit
-end
-
-structure ML_Test: ML_TEST =
-struct
-
-(* extra ML environment *)
-
-structure Extra_Env = GenericDataFun
-(
- type T = Position.T Inttab.table; (*position of registered tokens*)
- val empty = Inttab.empty;
- val extend = I;
- fun merge _ = Inttab.merge (K true);
-);
-
-fun inherit_env context =
- ML_Context.inherit_env context #>
- Extra_Env.put (Extra_Env.get context);
-
-fun register_tokens toks context =
- let
- val regs = map (fn tok => (serial (), tok)) toks;
- val context' = context
- |> Extra_Env.map (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs);
- in (regs, context') end;
-
-fun position_of ctxt
- ({file, startLine = line, startPosition = i, endPosition = j, ...}: PolyML.location) =
- (case pairself (Inttab.lookup (Extra_Env.get (Context.Proof ctxt))) (i, j) of
- (SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2)
- | (SOME pos, NONE) => pos
- | _ => Position.line_file line file);
-
-
-(* parse trees *)
-
-fun report_parse_tree context depth space =
- let
- val pos_of = position_of (Context.proof_of context);
- fun report loc (PolyML.PTtype types) =
- PolyML.NameSpace.displayTypeExpression (types, depth, space)
- |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
- |> Position.report_text Markup.ML_typing (pos_of loc)
- | report loc (PolyML.PTdeclaredAt decl) =
- Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) ""
- |> Position.report_text Markup.ML_ref (pos_of loc)
- | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
- | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
- | report _ _ = ()
- and report_tree (loc, props) = List.app (report loc) props;
- in report_tree end;
-
-
-(* eval ML source tokens *)
-
-fun use_text ({name_space = space, print, error, ...}: use_context) verbose pos toks =
- let
- (* input *)
-
- val input = Context.>>> (register_tokens toks);
- val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input);
-
- val current_line = ref (the_default 1 (Position.line_of pos));
-
- fun get_index () =
- the_default 0 (get_first (fn (_, []) => NONE | (i, _) => SOME i) (! input_buffer));
-
- fun get () =
- (case ! input_buffer of
- [] => NONE
- | (_, []) :: rest => (input_buffer := rest; get ())
- | (i, c :: cs) :: rest =>
- (input_buffer := (i, cs) :: rest;
- if c = #"\n" then current_line := ! current_line + 1 else ();
- SOME c));
-
-
- (* output *)
-
- val output_buffer = ref Buffer.empty;
- fun output () = Buffer.content (! output_buffer);
- fun put s = change output_buffer (Buffer.add s);
-
- fun put_message {message, hard, location, context = _} =
- (put (if hard then "Error: " else "Warning: ");
- put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
- put (Position.str_of
- (position_of (Context.proof_of (the (Context.thread_data ()))) location) ^ "\n"));
-
-
- (* results *)
-
- val depth = get_print_depth ();
-
- fun apply_result {fixes, types, signatures, structures, functors, values} =
- let
- fun display disp x =
- if depth > 0 then
- (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n")
- else ();
-
- fun apply_fix (a, b) =
- (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b));
- fun apply_type (a, b) =
- (display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b));
- fun apply_sig (a, b) =
- (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b));
- fun apply_struct (a, b) =
- (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b));
- fun apply_funct (a, b) =
- (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b));
- fun apply_val (a, b) =
- (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b));
- in
- List.app apply_fix fixes;
- List.app apply_type types;
- List.app apply_sig signatures;
- List.app apply_struct structures;
- List.app apply_funct functors;
- List.app apply_val values
- end;
-
- fun result_fun (phase1, phase2) () =
- (case phase1 of NONE => ()
- | SOME parse_tree => report_parse_tree (the (Context.thread_data ())) depth space parse_tree;
- case phase2 of NONE => error "Static Errors"
- | SOME code => apply_result (Toplevel.program code));
-
-
- (* compiler invocation *)
-
- val parameters =
- [PolyML.Compiler.CPOutStream put,
- PolyML.Compiler.CPNameSpace space,
- PolyML.Compiler.CPErrorMessageProc put_message,
- PolyML.Compiler.CPLineNo (fn () => ! current_line),
- PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
- PolyML.Compiler.CPLineOffset get_index,
- PolyML.Compiler.CPCompilerResultFun result_fun];
- val _ =
- (while not (List.null (! input_buffer)) do
- PolyML.compiler (get, parameters) ())
- handle exn =>
- (put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); raise exn);
- in if verbose then print (output ()) else () end;
-
-val eval = use_text ML_Context.local_context;
-
-
-(* ML test command *)
-
-fun ML_test (txt, pos) =
- let
- val _ = Position.report Markup.ML_source pos;
- val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
- val ((env, body), env_ctxt) = ML_Context.eval_antiquotes (ants, pos) (Context.thread_data ());
-
- val _ = Context.setmp_thread_data env_ctxt
- (fn () => (eval false Position.none env; Context.thread_data ())) ()
- |> (fn NONE => () | SOME context' => Context.>> (inherit_env context'));
- val _ = eval true pos body;
- val _ = eval false Position.none (ML_Lex.tokenize "structure Isabelle = struct end");
- in () end;
-
-
-local structure P = OuterParse and K = OuterKeyword in
-
-fun propagate_env (context as Context.Proof lthy) =
- Context.Proof (LocalTheory.map_contexts (inherit_env context) lthy)
- | propagate_env context = context;
-
-val _ =
- OuterSyntax.command "ML_test" "advanced ML compiler test" (K.tag_ml K.thy_decl)
- (P.ML_source >> (fn src =>
- Toplevel.generic_theory (ML_Context.exec (fn () => ML_test src) #> propagate_env)));
-
-end;
-
-end;
-
--- a/src/Pure/ROOT.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/Pure/ROOT.ML Tue Jun 02 23:56:12 2009 -0700
@@ -46,7 +46,6 @@
use "Syntax/syntax.ML";
use "type_infer.ML";
-use "ML/ml_syntax.ML";
(*core of tactical proof system*)
use "net.ML";
@@ -98,6 +97,5 @@
(*configuration for Proof General*)
cd "ProofGeneral"; use "ROOT.ML"; cd "..";
-if ml_system = "polyml-experimental" then use "ML/ml_test.ML" else ();
use "pure_setup.ML";
--- a/src/Pure/System/isabelle_process.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/Pure/System/isabelle_process.ML Tue Jun 02 23:56:12 2009 -0700
@@ -133,6 +133,7 @@
(change print_mode (update (op =) isabelle_processN);
setup_channels out |> init_message;
OuterKeyword.report ();
+ Output.status (Markup.markup Markup.ready "");
Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
end;
--- a/src/Tools/Compute_Oracle/am_compiler.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/Tools/Compute_Oracle/am_compiler.ML Tue Jun 02 23:56:12 2009 -0700
@@ -185,7 +185,7 @@
in
compiled_rewriter := NONE;
- use_text ML_Context.local_context (1, "") false (!buffer);
+ use_text ML_Env.local_context (1, "") false (!buffer);
case !compiled_rewriter of
NONE => raise (Compile "cannot communicate with compiled function")
| SOME r => (compiled_rewriter := NONE; r)
--- a/src/Tools/Compute_Oracle/am_sml.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/Tools/Compute_Oracle/am_sml.ML Tue Jun 02 23:56:12 2009 -0700
@@ -492,7 +492,7 @@
fun writeTextFile name s = File.write (Path.explode name) s
-fun use_source src = use_text ML_Context.local_context (1, "") false src
+fun use_source src = use_text ML_Env.local_context (1, "") false src
fun compile cache_patterns const_arity eqs =
let
--- a/src/Tools/code/code_haskell.ML Tue Jun 02 23:49:46 2009 -0700
+++ b/src/Tools/code/code_haskell.ML Tue Jun 02 23:56:12 2009 -0700
@@ -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 23:49:46 2009 -0700
+++ b/src/Tools/code/code_ml.ML Tue Jun 02 23:56:12 2009 -0700
@@ -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, "::")
@@ -1081,7 +1082,7 @@
fun isar_seri_sml module_name =
Code_Target.parse_args (Scan.succeed ())
#> (fn () => serialize_ml target_SML
- (SOME (use_text ML_Context.local_context (1, "generated code") false))
+ (SOME (use_text ML_Env.local_context (1, "generated code") false))
pr_sml_module pr_sml_stmt module_name);
fun isar_seri_ocaml module_name =