--- a/src/HOL/Finite_Set.thy Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Finite_Set.thy Fri Jun 05 13:35:33 2009 +0200
@@ -3266,4 +3266,109 @@
end
+
+subsection {* Expressing set operations via @{const fold} *}
+
+lemma (in fun_left_comm) fun_left_comm_apply:
+ "fun_left_comm (\<lambda>x. f (g x))"
+proof
+qed (simp_all add: fun_left_comm)
+
+lemma (in fun_left_comm_idem) fun_left_comm_idem_apply:
+ "fun_left_comm_idem (\<lambda>x. f (g x))"
+ by (rule fun_left_comm_idem.intro, rule fun_left_comm_apply, unfold_locales)
+ (simp_all add: fun_left_idem)
+
+lemma fun_left_comm_idem_insert:
+ "fun_left_comm_idem insert"
+proof
+qed auto
+
+lemma fun_left_comm_idem_remove:
+ "fun_left_comm_idem (\<lambda>x A. A - {x})"
+proof
+qed auto
+
+lemma fun_left_comm_idem_inter:
+ "fun_left_comm_idem op \<inter>"
+proof
+qed auto
+
+lemma fun_left_comm_idem_union:
+ "fun_left_comm_idem op \<union>"
+proof
+qed auto
+
+lemma union_fold_insert:
+ assumes "finite A"
+ shows "A \<union> B = fold insert B A"
+proof -
+ interpret fun_left_comm_idem insert by (fact fun_left_comm_idem_insert)
+ from `finite A` show ?thesis by (induct A arbitrary: B) simp_all
+qed
+
+lemma minus_fold_remove:
+ assumes "finite A"
+ shows "B - A = fold (\<lambda>x A. A - {x}) B A"
+proof -
+ interpret fun_left_comm_idem "\<lambda>x A. A - {x}" by (fact fun_left_comm_idem_remove)
+ from `finite A` show ?thesis by (induct A arbitrary: B) auto
+qed
+
+lemma inter_Inter_fold_inter:
+ assumes "finite A"
+ shows "B \<inter> Inter A = fold (op \<inter>) B A"
+proof -
+ interpret fun_left_comm_idem "op \<inter>" by (fact fun_left_comm_idem_inter)
+ from `finite A` show ?thesis by (induct A arbitrary: B)
+ (simp_all add: fold_fun_comm Int_commute)
+qed
+
+lemma union_Union_fold_union:
+ assumes "finite A"
+ shows "B \<union> Union A = fold (op \<union>) B A"
+proof -
+ interpret fun_left_comm_idem "op \<union>" by (fact fun_left_comm_idem_union)
+ from `finite A` show ?thesis by (induct A arbitrary: B)
+ (simp_all add: fold_fun_comm Un_commute)
+qed
+
+lemma Inter_fold_inter:
+ assumes "finite A"
+ shows "Inter A = fold (op \<inter>) UNIV A"
+ using assms inter_Inter_fold_inter [of A UNIV] by simp
+
+lemma Union_fold_union:
+ assumes "finite A"
+ shows "Union A = fold (op \<union>) {} A"
+ using assms union_Union_fold_union [of A "{}"] by simp
+
+lemma inter_INTER_fold_inter:
+ assumes "finite A"
+ shows "B \<inter> INTER A f = fold (\<lambda>A. op \<inter> (f A)) B A" (is "?inter = ?fold")
+proof (rule sym)
+ interpret fun_left_comm_idem "op \<inter>" by (fact fun_left_comm_idem_inter)
+ interpret fun_left_comm_idem "\<lambda>A. op \<inter> (f A)" by (fact fun_left_comm_idem_apply)
+ from `finite A` show "?fold = ?inter" by (induct A arbitrary: B) auto
+qed
+
+lemma union_UNION_fold_union:
+ assumes "finite A"
+ shows "B \<union> UNION A f = fold (\<lambda>A. op \<union> (f A)) B A" (is "?union = ?fold")
+proof (rule sym)
+ interpret fun_left_comm_idem "op \<union>" by (fact fun_left_comm_idem_union)
+ interpret fun_left_comm_idem "\<lambda>A. op \<union> (f A)" by (fact fun_left_comm_idem_apply)
+ from `finite A` show "?fold = ?union" by (induct A arbitrary: B) auto
+qed
+
+lemma INTER_fold_inter:
+ assumes "finite A"
+ shows "INTER A f = fold (\<lambda>A. op \<inter> (f A)) UNIV A"
+ using assms inter_INTER_fold_inter [of A UNIV] by simp
+
+lemma UNION_fold_union:
+ assumes "finite A"
+ shows "UNION A f = fold (\<lambda>A. op \<union> (f A)) {} A"
+ using assms union_UNION_fold_union [of A "{}"] by simp
+
end
--- a/src/HOL/Hilbert_Choice.thy Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Hilbert_Choice.thy Fri Jun 05 13:35:33 2009 +0200
@@ -12,9 +12,7 @@
subsection {* Hilbert's epsilon *}
-axiomatization
- Eps :: "('a => bool) => 'a"
-where
+axiomatization Eps :: "('a => bool) => 'a" where
someI: "P x ==> P (Eps P)"
syntax (epsilon)
@@ -586,74 +584,6 @@
by blast
-text{*Many of these bindings are used by the ATP linkup, and not just by
-legacy proof scripts.*}
-ML
-{*
-val inv_def = thm "inv_def";
-val Inv_def = thm "Inv_def";
-
-val someI = thm "someI";
-val someI_ex = thm "someI_ex";
-val someI2 = thm "someI2";
-val someI2_ex = thm "someI2_ex";
-val some_equality = thm "some_equality";
-val some1_equality = thm "some1_equality";
-val some_eq_ex = thm "some_eq_ex";
-val some_eq_trivial = thm "some_eq_trivial";
-val some_sym_eq_trivial = thm "some_sym_eq_trivial";
-val choice = thm "choice";
-val bchoice = thm "bchoice";
-val inv_id = thm "inv_id";
-val inv_f_f = thm "inv_f_f";
-val inv_f_eq = thm "inv_f_eq";
-val inj_imp_inv_eq = thm "inj_imp_inv_eq";
-val inj_transfer = thm "inj_transfer";
-val inj_iff = thm "inj_iff";
-val inj_imp_surj_inv = thm "inj_imp_surj_inv";
-val f_inv_f = thm "f_inv_f";
-val surj_f_inv_f = thm "surj_f_inv_f";
-val inv_injective = thm "inv_injective";
-val inj_on_inv = thm "inj_on_inv";
-val surj_imp_inj_inv = thm "surj_imp_inj_inv";
-val surj_iff = thm "surj_iff";
-val surj_imp_inv_eq = thm "surj_imp_inv_eq";
-val bij_imp_bij_inv = thm "bij_imp_bij_inv";
-val inv_equality = thm "inv_equality";
-val inv_inv_eq = thm "inv_inv_eq";
-val o_inv_distrib = thm "o_inv_distrib";
-val image_surj_f_inv_f = thm "image_surj_f_inv_f";
-val image_inv_f_f = thm "image_inv_f_f";
-val inv_image_comp = thm "inv_image_comp";
-val bij_image_Collect_eq = thm "bij_image_Collect_eq";
-val bij_vimage_eq_inv_image = thm "bij_vimage_eq_inv_image";
-val Inv_f_f = thm "Inv_f_f";
-val f_Inv_f = thm "f_Inv_f";
-val Inv_injective = thm "Inv_injective";
-val inj_on_Inv = thm "inj_on_Inv";
-val split_paired_Eps = thm "split_paired_Eps";
-val Eps_split = thm "Eps_split";
-val Eps_split_eq = thm "Eps_split_eq";
-val wf_iff_no_infinite_down_chain = thm "wf_iff_no_infinite_down_chain";
-val Inv_mem = thm "Inv_mem";
-val Inv_f_eq = thm "Inv_f_eq";
-val Inv_comp = thm "Inv_comp";
-val tfl_some = thm "tfl_some";
-val make_neg_rule = thm "make_neg_rule";
-val make_refined_neg_rule = thm "make_refined_neg_rule";
-val make_pos_rule = thm "make_pos_rule";
-val make_neg_rule' = thm "make_neg_rule'";
-val make_pos_rule' = thm "make_pos_rule'";
-val make_neg_goal = thm "make_neg_goal";
-val make_pos_goal = thm "make_pos_goal";
-val conj_forward = thm "conj_forward";
-val disj_forward = thm "disj_forward";
-val disj_forward2 = thm "disj_forward2";
-val all_forward = thm "all_forward";
-val ex_forward = thm "ex_forward";
-*}
-
-
subsection {* Meson package *}
use "Tools/meson.ML"
@@ -668,4 +598,5 @@
use "Tools/specification_package.ML"
+
end
--- a/src/HOL/IsaMakefile Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/IsaMakefile Fri Jun 05 13:35:33 2009 +0200
@@ -349,6 +349,7 @@
Library/Preorder.thy \
Library/Product_plus.thy \
Library/Product_Vector.thy \
+ Library/Tree.thy \
Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
Library/reify_data.ML Library/reflection.ML \
Library/LaTeXsugar.thy Library/OptionalSugar.thy
--- a/src/HOL/Library/Enum.thy Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Library/Enum.thy Fri Jun 05 13:35:33 2009 +0200
@@ -43,8 +43,8 @@
definition
"eq_class.eq f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
-instance by default
- (simp_all add: eq_fun_def enum_all expand_fun_eq)
+instance proof
+qed (simp_all add: eq_fun_def enum_all expand_fun_eq)
end
@@ -185,8 +185,8 @@
definition
"enum = [()]"
-instance by default
- (simp_all add: enum_unit_def UNIV_unit)
+instance proof
+qed (simp_all add: enum_unit_def UNIV_unit)
end
@@ -196,8 +196,8 @@
definition
"enum = [False, True]"
-instance by default
- (simp_all add: enum_bool_def UNIV_bool)
+instance proof
+qed (simp_all add: enum_bool_def UNIV_bool)
end
@@ -275,8 +275,8 @@
"enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
-instance by default
- (simp_all add: enum_nibble_def UNIV_nibble)
+instance proof
+qed (simp_all add: enum_nibble_def UNIV_nibble)
end
@@ -357,9 +357,9 @@
Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
unfolding enum_char_def enum_nibble_def by simp
-instance by default
- (auto intro: char.exhaust injI simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric]
- distinct_map distinct_product enum_distinct)
+instance proof
+qed (auto intro: char.exhaust injI simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric]
+ distinct_map distinct_product enum_distinct)
end
@@ -369,8 +369,8 @@
definition
"enum = None # map Some enum"
-instance by default
- (auto simp add: enum_all enum_option_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct)
+instance proof
+qed (auto simp add: enum_all enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct)
end
--- a/src/HOL/Library/LaTeXsugar.thy Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy Fri Jun 05 13:35:33 2009 +0200
@@ -34,7 +34,7 @@
(* insert *)
translations
- "{x} \<union> A" <= "insert x A"
+ "{x} \<union> A" <= "CONST insert x A"
"{x,y}" <= "{x} \<union> {y}"
"{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
"{x}" <= "{x} \<union> \<emptyset>"
--- a/src/HOL/Library/Mapping.thy Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Library/Mapping.thy Fri Jun 05 13:35:33 2009 +0200
@@ -1,6 +1,4 @@
-(* Title: HOL/Library/Mapping.thy
- Author: Florian Haftmann, TU Muenchen
-*)
+(* Author: Florian Haftmann, TU Muenchen *)
header {* An abstract view on maps for code generation. *}
@@ -132,4 +130,23 @@
by (rule sym)
(auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff map_compose [symmetric] comp_def)
+
+subsection {* Some technical code lemmas *}
+
+lemma [code]:
+ "map_case f m = f (Mapping.lookup m)"
+ by (cases m) simp
+
+lemma [code]:
+ "map_rec f m = f (Mapping.lookup m)"
+ by (cases m) simp
+
+lemma [code]:
+ "Nat.size (m :: (_, _) map) = 0"
+ by (cases m) simp
+
+lemma [code]:
+ "map_size f g m = 0"
+ by (cases m) simp
+
end
\ No newline at end of file
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Fri Jun 05 13:35:33 2009 +0200
@@ -484,25 +484,30 @@
subsection{* Hausdorff and other separation properties *}
-axclass t0_space \<subseteq> topological_space
- t0_space:
- "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)"
-
-axclass t1_space \<subseteq> topological_space
- t1_space:
- "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<notin> U \<and> x \<notin> V \<and> y \<in> V"
-
-instance t1_space \<subseteq> t0_space
-by default (fast dest: t1_space)
+class t0_space =
+ assumes t0_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)"
+
+class t1_space =
+ assumes t1_space: "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<notin> U \<and> x \<notin> V \<and> y \<in> V"
+begin
+
+subclass t0_space
+proof
+qed (fast dest: t1_space)
+
+end
text {* T2 spaces are also known as Hausdorff spaces. *}
-axclass t2_space \<subseteq> topological_space
- hausdorff:
- "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
-
-instance t2_space \<subseteq> t1_space
-by default (fast dest: hausdorff)
+class t2_space =
+ assumes hausdorff: "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
+begin
+
+subclass t1_space
+proof
+qed (fast dest: hausdorff)
+
+end
instance metric_space \<subseteq> t2_space
proof
@@ -568,9 +573,9 @@
using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"]
by metis (* FIXME: VERY slow! *)
-axclass perfect_space \<subseteq> metric_space
+class perfect_space =
(* FIXME: perfect_space should inherit from topological_space *)
- islimpt_UNIV [simp, intro]: "x islimpt UNIV"
+ assumes islimpt_UNIV [simp, intro]: "(x::'a::metric_space) islimpt UNIV"
lemma perfect_choose_dist:
fixes x :: "'a::perfect_space"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Tree.thy Fri Jun 05 13:35:33 2009 +0200
@@ -0,0 +1,142 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Trees implementing mappings. *}
+
+theory Tree
+imports Mapping
+begin
+
+subsection {* Type definition and operations *}
+
+datatype ('a, 'b) tree = Empty
+ | Branch 'b 'a "('a, 'b) tree" "('a, 'b) tree"
+
+primrec lookup :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> 'a \<rightharpoonup> 'b" where
+ "lookup Empty = (\<lambda>_. None)"
+ | "lookup (Branch v k l r) = (\<lambda>k'. if k' = k then Some v
+ else if k' \<le> k then lookup l k' else lookup r k')"
+
+primrec update :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) tree \<Rightarrow> ('a, 'b) tree" where
+ "update k v Empty = Branch v k Empty Empty"
+ | "update k' v' (Branch v k l r) = (if k' = k then
+ Branch v' k l r else if k' \<le> k
+ then Branch v k (update k' v' l) r
+ else Branch v k l (update k' v' r))"
+
+primrec keys :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> 'a list" where
+ "keys Empty = []"
+ | "keys (Branch _ k l r) = k # keys l @ keys r"
+
+definition size :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> nat" where
+ "size t = length (filter (\<lambda>x. x \<noteq> None) (map (lookup t) (remdups (keys t))))"
+
+fun bulkload :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) tree" where
+ [simp del]: "bulkload ks f = (case ks of [] \<Rightarrow> Empty | _ \<Rightarrow> let
+ mid = length ks div 2;
+ ys = take mid ks;
+ x = ks ! mid;
+ zs = drop (Suc mid) ks
+ in Branch (f x) x (bulkload ys f) (bulkload zs f))"
+
+
+subsection {* Properties *}
+
+lemma dom_lookup:
+ "dom (Tree.lookup t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))"
+proof -
+ have "dom (Tree.lookup t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (keys t))"
+ by (induct t) (auto simp add: dom_if)
+ also have "\<dots> = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))"
+ by simp
+ finally show ?thesis .
+qed
+
+lemma lookup_finite:
+ "finite (dom (lookup t))"
+ unfolding dom_lookup by simp
+
+lemma lookup_update:
+ "lookup (update k v t) = (lookup t)(k \<mapsto> v)"
+ by (induct t) (simp_all add: expand_fun_eq)
+
+lemma lookup_bulkload:
+ "sorted ks \<Longrightarrow> lookup (bulkload ks f) = (Some o f) |` set ks"
+proof (induct ks f rule: bulkload.induct)
+ case (1 ks f) show ?case proof (cases ks)
+ case Nil then show ?thesis by (simp add: bulkload.simps)
+ next
+ case (Cons w ws)
+ then have case_simp: "\<And>w v::('a, 'b) tree. (case ks of [] \<Rightarrow> v | _ \<Rightarrow> w) = w"
+ by (cases ks) auto
+ from Cons have "ks \<noteq> []" by simp
+ then have "0 < length ks" by simp
+ let ?mid = "length ks div 2"
+ let ?ys = "take ?mid ks"
+ let ?x = "ks ! ?mid"
+ let ?zs = "drop (Suc ?mid) ks"
+ from `ks \<noteq> []` have ks_split: "ks = ?ys @ [?x] @ ?zs"
+ by (simp add: id_take_nth_drop)
+ then have in_ks: "\<And>x. x \<in> set ks \<longleftrightarrow> x \<in> set (?ys @ [?x] @ ?zs)"
+ by simp
+ with ks_split have ys_x: "\<And>y. y \<in> set ?ys \<Longrightarrow> y \<le> ?x"
+ and x_zs: "\<And>z. z \<in> set ?zs \<Longrightarrow> ?x \<le> z"
+ using `sorted ks` sorted_append [of "?ys" "[?x] @ ?zs"] sorted_append [of "[?x]" "?zs"]
+ by simp_all
+ have ys: "lookup (bulkload ?ys f) = (Some o f) |` set ?ys"
+ by (rule "1.hyps"(1)) (auto intro: Cons sorted_take `sorted ks`)
+ have zs: "lookup (bulkload ?zs f) = (Some o f) |` set ?zs"
+ by (rule "1.hyps"(2)) (auto intro: Cons sorted_drop `sorted ks`)
+ show ?thesis using `0 < length ks`
+ by (simp add: bulkload.simps)
+ (auto simp add: restrict_map_def in_ks case_simp Let_def ys zs expand_fun_eq
+ dest: in_set_takeD in_set_dropD ys_x x_zs)
+ qed
+qed
+
+
+subsection {* Trees as mappings *}
+
+definition Tree :: "('a\<Colon>linorder, 'b) tree \<Rightarrow> ('a, 'b) map" where
+ "Tree t = Map (Tree.lookup t)"
+
+lemma [code, code del]:
+ "(eq_class.eq :: (_, _) map \<Rightarrow> _) = eq_class.eq" ..
+
+lemma [code, code del]:
+ "Mapping.delete k m = Mapping.delete k m" ..
+
+code_datatype Tree
+
+lemma empty_Tree [code]:
+ "Mapping.empty = Tree Empty"
+ by (simp add: Tree_def Mapping.empty_def)
+
+lemma lookup_Tree [code]:
+ "Mapping.lookup (Tree t) = lookup t"
+ by (simp add: Tree_def)
+
+lemma update_Tree [code]:
+ "Mapping.update k v (Tree t) = Tree (update k v t)"
+ by (simp add: Tree_def lookup_update)
+
+lemma keys_Tree [code]:
+ "Mapping.keys (Tree t) = set (filter (\<lambda>k. lookup t k \<noteq> None) (remdups (keys t)))"
+ by (simp add: Tree_def dom_lookup)
+
+lemma size_Tree [code]:
+ "Mapping.size (Tree t) = size t"
+proof -
+ have "card (dom (Tree.lookup t)) = length (filter (\<lambda>x. x \<noteq> None) (map (lookup t) (remdups (keys t))))"
+ unfolding dom_lookup by (subst distinct_card) (auto simp add: comp_def)
+ then show ?thesis by (auto simp add: Tree_def Mapping.size_def size_def)
+qed
+
+lemma tabulate_Tree [code]:
+ "Mapping.tabulate ks f = Tree (bulkload (sort ks) f)"
+proof -
+ have "Mapping.lookup (Mapping.tabulate ks f) = Mapping.lookup (Tree (bulkload (sort ks) f))"
+ by (simp add: lookup_Tree lookup_bulkload lookup_tabulate)
+ then show ?thesis by (simp add: lookup_inject)
+qed
+
+end
--- a/src/HOL/List.thy Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/List.thy Fri Jun 05 13:35:33 2009 +0200
@@ -2144,7 +2144,7 @@
"\<lbrakk>Q x ; \<forall> x\<in> set xs. P x; \<forall> x y. P x \<and> Q y \<longrightarrow> Q (f y x) \<rbrakk> \<Longrightarrow> Q (foldl f x xs)"
by (induct xs arbitrary: x, simp_all)
-text{* @{const foldl} and @{text concat} *}
+text {* @{const foldl} and @{const concat} *}
lemma foldl_conv_concat:
"foldl (op @) xs xss = xs @ concat xss"
@@ -2158,6 +2158,13 @@
lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"
by (simp add: foldl_conv_concat)
+text {* @{const Finite_Set.fold} and @{const foldl} *}
+
+lemma (in fun_left_comm_idem) fold_set:
+ "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
+ by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
+
+
subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
--- a/src/HOL/Nominal/nominal_package.ML Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Fri Jun 05 13:35:33 2009 +0200
@@ -732,17 +732,18 @@
let val xs = Long_Name.explode s;
in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
- val (descr'', ndescr) = ListPair.unzip (List.mapPartial
+ val (descr'', ndescr) = ListPair.unzip (map_filter
(fn (i, ("Nominal.noption", _, _)) => NONE
| (i, (s, dts, constrs)) =>
let
val SOME index = AList.lookup op = ty_idxs i;
- val (constrs1, constrs2) = ListPair.unzip
- (map (fn (cname, cargs) => apfst (pair (strip_nth_name 2 (strip_nth_name 1 cname)))
- (Library.foldl_map (fn (dts, dt) =>
+ val (constrs2, constrs1) =
+ map_split (fn (cname, cargs) =>
+ apsnd (pair (strip_nth_name 2 (strip_nth_name 1 cname)))
+ (fold_map (fn dt => fn dts =>
let val (dts', dt') = strip_option dt
- in (dts @ dts' @ [reindex dt'], (length dts, length dts')) end)
- ([], cargs))) constrs)
+ in ((length dts, length dts'), dts @ dts' @ [reindex dt']) end)
+ cargs [])) constrs
in SOME ((index, (strip_nth_name 1 s, map reindex dts, constrs1)),
(index, constrs2))
end) descr);
--- a/src/HOL/Set.thy Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Set.thy Fri Jun 05 13:35:33 2009 +0200
@@ -20,7 +20,6 @@
consts
Collect :: "('a => bool) => 'a set" -- "comprehension"
"op :" :: "'a => 'a set => bool" -- "membership"
- insert :: "'a => 'a set => 'a set"
Ball :: "'a set => ('a => bool) => bool" -- "bounded universal quantifiers"
Bex :: "'a set => ('a => bool) => bool" -- "bounded existential quantifiers"
Bex1 :: "'a set => ('a => bool) => bool" -- "bounded unique existential quantifiers"
@@ -58,19 +57,6 @@
translations
"{x. P}" == "Collect (%x. P)"
-definition empty :: "'a set" ("{}") where
- "empty \<equiv> {x. False}"
-
-definition UNIV :: "'a set" where
- "UNIV \<equiv> {x. True}"
-
-syntax
- "@Finset" :: "args => 'a set" ("{(_)}")
-
-translations
- "{x, xs}" == "insert x {xs}"
- "{x}" == "insert x {}"
-
definition Int :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
"A Int B \<equiv> {x. x \<in> A \<and> x \<in> B}"
@@ -85,6 +71,22 @@
"Int" (infixl "\<inter>" 70) and
"Un" (infixl "\<union>" 65)
+definition empty :: "'a set" ("{}") where
+ "empty \<equiv> {x. False}"
+
+definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+ "insert a B \<equiv> {x. x = a} \<union> B"
+
+definition UNIV :: "'a set" where
+ "UNIV \<equiv> {x. True}"
+
+syntax
+ "@Finset" :: "args => 'a set" ("{(_)}")
+
+translations
+ "{x, xs}" == "CONST insert x {xs}"
+ "{x}" == "CONST insert x {}"
+
syntax
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10)
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3EX _:_./ _)" [0, 0, 10] 10)
@@ -408,7 +410,6 @@
defs
Pow_def: "Pow A == {B. B <= A}"
- insert_def: "insert a B == {x. x=a} Un B"
image_def: "f`A == {y. EX x:A. y = f(x)}"
@@ -811,7 +812,7 @@
by blast
-subsubsection {* Augmenting a set -- insert *}
+subsubsection {* Augmenting a set -- @{const insert} *}
lemma insert_iff [simp]: "(a : insert b A) = (a = b | a:A)"
by (unfold insert_def) blast
--- a/src/HOL/TLA/Intensional.thy Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/TLA/Intensional.thy Fri Jun 05 13:35:33 2009 +0200
@@ -126,8 +126,8 @@
"_liftLeq" == "_lift2 (op <=)"
"_liftMem" == "_lift2 (op :)"
"_liftNotMem x xs" == "_liftNot (_liftMem x xs)"
- "_liftFinset (_liftargs x xs)" == "_lift2 insert x (_liftFinset xs)"
- "_liftFinset x" == "_lift2 insert x (_const {})"
+ "_liftFinset (_liftargs x xs)" == "_lift2 CONST insert x (_liftFinset xs)"
+ "_liftFinset x" == "_lift2 CONST insert x (_const {})"
"_liftPair x (_liftargs y z)" == "_liftPair x (_liftPair y z)"
"_liftPair" == "_lift2 Pair"
"_liftCons" == "lift2 Cons"
--- a/src/HOL/Tools/datatype_codegen.ML Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Fri Jun 05 13:35:33 2009 +0200
@@ -89,10 +89,10 @@
val dts' = map (DatatypeAux.typ_of_dtyp descr sorts) dts;
val T = Type (tname, dts');
val rest = mk_term_of_def gr "and " xs;
- val (_, eqs) = Library.foldl_map (fn (prfx, (cname, Ts)) =>
+ val (eqs, _) = fold_map (fn (cname, Ts) => fn prfx =>
let val args = map (fn i =>
str ("x" ^ string_of_int i)) (1 upto length Ts)
- in (" | ", Pretty.blk (4,
+ in (Pretty.blk (4,
[str prfx, mk_term_of gr module' false T, Pretty.brk 1,
if null Ts then str (snd (get_const_id gr cname))
else parens (Pretty.block
@@ -100,9 +100,9 @@
Pretty.brk 1, mk_tuple args]),
str " =", Pretty.brk 1] @
mk_constr_term cname Ts T
- (map (fn (x, U) => [Pretty.block [mk_term_of gr module' false U,
- Pretty.brk 1, x]]) (args ~~ Ts))))
- end) (prfx, cs')
+ (map2 (fn x => fn U => [Pretty.block [mk_term_of gr module' false U,
+ Pretty.brk 1, x]]) args Ts)), " | ")
+ end) cs' prfx
in eqs @ rest end;
fun mk_gen_of_def gr prfx [] = []
--- a/src/HOL/Tools/datatype_realizer.ML Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Fri Jun 05 13:35:33 2009 +0200
@@ -56,17 +56,17 @@
fun mk_all i s T t =
if i mem is then list_all_free ([(s, T)], t) else t;
- val (prems, rec_fns) = split_list (List.concat (snd (Library.foldl_map
- (fn (j, ((i, (_, _, constrs)), T)) => Library.foldl_map (fn (j, (cname, cargs)) =>
+ val (prems, rec_fns) = split_list (flat (fst (fold_map
+ (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
let
val Ts = map (typ_of_dtyp descr sorts) cargs;
val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
- val recs = List.filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
+ val recs = filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
val frees = tnames ~~ Ts;
fun mk_prems vs [] =
let
- val rT = List.nth (rec_result_Ts, i);
+ val rT = nth (rec_result_Ts) i;
val vs' = filter_out is_unit vs;
val f = mk_Free "f" (map fastype_of vs' ---> rT) j;
val f' = Envir.eta_contract (list_abs_free
@@ -80,7 +80,7 @@
val k = body_index dt;
val (Us, U) = strip_type T;
val i = length Us;
- val rT = List.nth (rec_result_Ts, k);
+ val rT = nth (rec_result_Ts) k;
val r = Free ("r" ^ s, Us ---> rT);
val (p, f) = mk_prems (vs @ [r]) ds
in (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
@@ -89,9 +89,8 @@
(app_bnds (Free (s, T)) i))), p)), f)
end
- in (j + 1,
- apfst (curry list_all_free frees) (mk_prems (map Free frees) recs))
- end) (j, constrs)) (1, descr ~~ recTs))));
+ in (apfst (curry list_all_free frees) (mk_prems (map Free frees) recs), j + 1) end)
+ constrs) (descr ~~ recTs) 1)));
fun mk_proj j [] t = t
| mk_proj j (i :: is) t = if null is then t else
--- a/src/HOL/Tools/hologic.ML Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Tools/hologic.ML Fri Jun 05 13:35:33 2009 +0200
@@ -122,8 +122,10 @@
val mk_typerep: typ -> term
val mk_term_of: typ -> term -> term
val reflect_term: term -> term
+ val mk_valtermify_app: string -> (string * typ) list -> typ -> term
val mk_return: typ -> typ -> term -> term
val mk_ST: ((term * typ) * (string * typ) option) list -> term -> typ -> typ option * typ -> term
+ val mk_random: typ -> term -> term
end;
structure HOLogic: HOLOGIC =
@@ -152,13 +154,13 @@
let
val sT = mk_setT T;
val empty = Const ("Set.empty", sT);
- fun insert t u = Const ("insert", T --> sT --> sT) $ t $ u;
+ fun insert t u = Const ("Set.insert", T --> sT --> sT) $ t $ u;
in fold_rev insert ts empty end;
fun mk_UNIV T = Const ("Set.UNIV", mk_setT T);
-fun dest_set (Const ("Orderings.bot", _)) = []
- | dest_set (Const ("insert", _) $ t $ u) = t :: dest_set u
+fun dest_set (Const ("Set.empty", _)) = []
+ | dest_set (Const ("Set.insert", _) $ t $ u) = t :: dest_set u
| dest_set t = raise TERM ("dest_set", [t]);
fun Collect_const T = Const ("Collect", (T --> boolT) --> mk_setT T);
@@ -617,6 +619,19 @@
| reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t)
| reflect_term t = t;
+fun mk_valtermify_app c vs T =
+ let
+ fun termifyT T = mk_prodT (T, unitT --> termT);
+ fun valapp T T' = Const ("Code_Eval.valapp",
+ termifyT (T --> T') --> termifyT T --> termifyT T');
+ fun mk_fTs [] _ = []
+ | mk_fTs (_ :: Ts) T = (Ts ---> T) :: mk_fTs Ts T;
+ val Ts = map snd vs;
+ val t = Const (c, Ts ---> T);
+ val tt = mk_prod (t, Abs ("u", unitT, reflect_term t));
+ fun app (t, (fT, (v, T))) = valapp T fT $ t $ Free (v, termifyT T);
+ in Library.foldl app (tt, mk_fTs Ts T ~~ vs) end;
+
(* open state monads *)
@@ -633,4 +648,10 @@
$ t $ t', U)
in fold_rev mk_clause clauses (t, U) |> fst end;
+val code_numeralT = Type ("Code_Numeral.code_numeral", []);
+val random_seedT = mk_prodT (code_numeralT, code_numeralT);
+
+fun mk_random T t = Const ("Quickcheck.random_class.random", code_numeralT
+ --> random_seedT --> mk_prodT (mk_prodT (T, unitT --> termT), random_seedT)) $ t;
+
end;
--- a/src/HOL/Tools/inductive_realizer.ML Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Jun 05 13:35:33 2009 +0200
@@ -315,16 +315,16 @@
fun get f = (these oo Option.map) f;
val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
- val (_, constrss) = Library.foldl_map (fn ((recs, dummies), (s, rs)) =>
- if s mem rsets then
+ val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>
+ if member (op =) rsets s then
let
val (d :: dummies') = dummies;
val (recs1, recs2) = chop (length rs) (if d then tl recs else recs)
- in ((recs2, dummies'), map (head_of o hd o rev o snd o strip_comb o
- fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1)
+ in (map (head_of o hd o rev o snd o strip_comb o fst o
+ HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1, (recs2, dummies'))
end
- else ((recs, dummies), replicate (length rs) Extraction.nullt))
- ((get #rec_thms dt_info, dummies), rss);
+ else (replicate (length rs) Extraction.nullt, (recs, dummies)))
+ rss (get #rec_thms dt_info, dummies);
val rintrs = map (fn (intr, c) => Envir.eta_contract
(Extraction.realizes_of thy2 vs
(if c = Extraction.nullt then c else list_comb (c, map Var (rev
@@ -360,7 +360,7 @@
(** realizer for induction rule **)
- val Ps = List.mapPartial (fn _ $ M $ P => if pred_of M mem rsets then
+ val Ps = map_filter (fn _ $ M $ P => if pred_of M mem rsets then
SOME (fst (fst (dest_Var (head_of P)))) else NONE)
(HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
--- a/src/HOL/Tools/meson.ML Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Tools/meson.ML Fri Jun 05 13:35:33 2009 +0200
@@ -46,6 +46,19 @@
val max_clauses_default = 60;
val (max_clauses, setup) = Attrib.config_int "max_clauses" max_clauses_default;
+val disj_forward = @{thm disj_forward};
+val disj_forward2 = @{thm disj_forward2};
+val make_pos_rule = @{thm make_pos_rule};
+val make_pos_rule' = @{thm make_pos_rule'};
+val make_pos_goal = @{thm make_pos_goal};
+val make_neg_rule = @{thm make_neg_rule};
+val make_neg_rule' = @{thm make_neg_rule'};
+val make_neg_goal = @{thm make_neg_goal};
+val conj_forward = @{thm conj_forward};
+val all_forward = @{thm all_forward};
+val ex_forward = @{thm ex_forward};
+val choice = @{thm choice};
+
val not_conjD = thm "meson_not_conjD";
val not_disjD = thm "meson_not_disjD";
val not_notD = thm "meson_not_notD";
--- a/src/HOL/Tools/res_axioms.ML Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML Fri Jun 05 13:35:33 2009 +0200
@@ -258,7 +258,7 @@
val cex = Thm.cterm_of thy (HOLogic.exists_const T)
val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
- fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1
+ fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS @{thm someI_ex}) 1
in Goal.prove_internal [ex_tm] conc tacf
|> forall_intr_list frees
|> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
--- a/src/HOL/ex/Codegenerator_Candidates.thy Fri Jun 05 09:54:47 2009 +0200
+++ b/src/HOL/ex/Codegenerator_Candidates.thy Fri Jun 05 13:35:33 2009 +0200
@@ -18,6 +18,7 @@
Primes
Product_ord
SetsAndFunctions
+ Tree
While_Combinator
Word
"~~/src/HOL/ex/Commutative_Ring_Complete"