--- a/Admin/isatest/isatest-statistics Fri Oct 19 15:12:52 2012 +0200
+++ b/Admin/isatest/isatest-statistics Sun Oct 21 17:04:13 2012 +0200
@@ -75,7 +75,7 @@
mkdir -p "$DIR" || fail "Bad directory: $DIR"
$ZGREP "^Finished .*elapsed" \
- $(find "$LOG_DIR" -name "$LOG_NAME" -ctime "-${TIMESPAN}") | \
+ $(find "$LOG_DIR" -name "$LOG_NAME" -mtime "-${TIMESPAN}") | \
perl -e '
while (<>) {
if (m/(\d\d\d\d)-(\d\d)-(\d\d).*:Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time/) {
--- a/Admin/isatest/isatest-stats Fri Oct 19 15:12:52 2012 +0200
+++ b/Admin/isatest/isatest-stats Sun Oct 21 17:04:13 2012 +0200
@@ -6,7 +6,7 @@
THIS="$(cd "$(dirname "$0")"; pwd)"
-PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly-e mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at64-poly-5.1-para at-mac-poly-5.1-para at-sml-dev"
+PLATFORMS="at-poly at-poly-test afp at64-poly mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-sml-dev"
ISABELLE_SESSIONS="
HOL
--- a/NEWS Fri Oct 19 15:12:52 2012 +0200
+++ b/NEWS Sun Oct 21 17:04:13 2012 +0200
@@ -70,6 +70,9 @@
*** HOL ***
+* Moved operation product, sublists and n_lists from Enum.thy
+to List.thy. INCOMPATIBILITY.
+
* Simplified 'typedef' specifications: historical options for implicit
set definition and alternative name have been discontinued. The
former behavior of "typedef (open) t = A" is now the default, but
--- a/src/HOL/Codegenerator_Test/RBT_Set_Test.thy Fri Oct 19 15:12:52 2012 +0200
+++ b/src/HOL/Codegenerator_Test/RBT_Set_Test.thy Sun Oct 21 17:04:13 2012 +0200
@@ -5,7 +5,7 @@
header {* Test of the code generator using an implementation of sets by RBT trees *}
theory RBT_Set_Test
-imports Library "~~/src/HOL/Library/RBT_Set"
+imports "~~/src/HOL/Library/Library" "~~/src/HOL/Library/RBT_Set"
begin
(*
--- a/src/HOL/Enum.thy Fri Oct 19 15:12:52 2012 +0200
+++ b/src/HOL/Enum.thy Sun Oct 21 17:04:13 2012 +0200
@@ -11,20 +11,23 @@
class enum =
fixes enum :: "'a list"
fixes enum_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
- fixes enum_ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
+ fixes enum_ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
assumes UNIV_enum: "UNIV = set enum"
and enum_distinct: "distinct enum"
- assumes enum_all : "enum_all P = (\<forall> x. P x)"
- assumes enum_ex : "enum_ex P = (\<exists> x. P x)"
+ assumes enum_all_UNIV: "enum_all P \<longleftrightarrow> Ball UNIV P"
+ assumes enum_ex_UNIV: "enum_ex P \<longleftrightarrow> Bex UNIV P"
+ -- {* tailored towards simple instantiation *}
begin
subclass finite proof
qed (simp add: UNIV_enum)
-lemma enum_UNIV: "set enum = UNIV" unfolding UNIV_enum ..
+lemma enum_UNIV:
+ "set enum = UNIV"
+ by (simp only: UNIV_enum)
lemma in_enum: "x \<in> set enum"
- unfolding enum_UNIV by auto
+ by (simp add: enum_UNIV)
lemma enum_eq_I:
assumes "\<And>x. x \<in> set xs"
@@ -34,10 +37,82 @@
with enum_UNIV show ?thesis by simp
qed
+lemma enum_all [simp]:
+ "enum_all = HOL.All"
+ by (simp add: fun_eq_iff enum_all_UNIV)
+
+lemma enum_ex [simp]:
+ "enum_ex = HOL.Ex"
+ by (simp add: fun_eq_iff enum_ex_UNIV)
+
end
-subsection {* Equality and order on functions *}
+subsection {* Implementations using @{class enum} *}
+
+subsubsection {* Unbounded operations and quantifiers *}
+
+lemma Collect_code [code]:
+ "Collect P = set (filter P enum)"
+ by (simp add: enum_UNIV)
+
+definition card_UNIV :: "'a itself \<Rightarrow> nat"
+where
+ [code del]: "card_UNIV TYPE('a) = card (UNIV :: 'a set)"
+
+lemma [code]:
+ "card_UNIV TYPE('a :: enum) = card (set (Enum.enum :: 'a list))"
+ by (simp only: card_UNIV_def enum_UNIV)
+
+lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> enum_all P"
+ by simp
+
+lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> enum_ex P"
+ by simp
+
+lemma exists1_code [code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum"
+ by (auto simp add: list_ex1_iff enum_UNIV)
+
+
+subsubsection {* An executable choice operator *}
+
+definition
+ [code del]: "enum_the = The"
+
+lemma [code]:
+ "The P = (case filter P enum of [x] => x | _ => enum_the P)"
+proof -
+ {
+ fix a
+ assume filter_enum: "filter P enum = [a]"
+ have "The P = a"
+ proof (rule the_equality)
+ fix x
+ assume "P x"
+ show "x = a"
+ proof (rule ccontr)
+ assume "x \<noteq> a"
+ from filter_enum obtain us vs
+ where enum_eq: "enum = us @ [a] @ vs"
+ and "\<forall> x \<in> set us. \<not> P x"
+ and "\<forall> x \<in> set vs. \<not> P x"
+ and "P a"
+ by (auto simp add: filter_eq_Cons_iff) (simp only: filter_empty_conv[symmetric])
+ with `P x` in_enum[of x, unfolded enum_eq] `x \<noteq> a` show "False" by auto
+ qed
+ next
+ from filter_enum show "P a" by (auto simp add: filter_eq_Cons_iff)
+ qed
+ }
+ from this show ?thesis
+ unfolding enum_the_def by (auto split: list.split)
+qed
+
+code_abort enum_the
+code_const enum_the (Eval "(fn p => raise Match)")
+
+
+subsubsection {* Equality and order on functions *}
instantiation "fun" :: (enum, equal) equal
begin
@@ -46,13 +121,13 @@
"HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
instance proof
-qed (simp_all add: equal_fun_def enum_UNIV fun_eq_iff)
+qed (simp_all add: equal_fun_def fun_eq_iff enum_UNIV)
end
lemma [code]:
"HOL.equal f g \<longleftrightarrow> enum_all (%x. f x = g x)"
-by (auto simp add: equal enum_all fun_eq_iff)
+ by (auto simp add: equal fun_eq_iff)
lemma [code nbe]:
"HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
@@ -62,72 +137,46 @@
fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
shows "f \<le> g \<longleftrightarrow> enum_all (\<lambda>x. f x \<le> g x)"
and "f < g \<longleftrightarrow> f \<le> g \<and> enum_ex (\<lambda>x. f x \<noteq> g x)"
- by (simp_all add: enum_all enum_ex fun_eq_iff le_fun_def order_less_le)
-
-
-subsection {* Quantifiers *}
-
-lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> enum_all P"
- by (simp add: enum_all)
-
-lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> enum_ex P"
- by (simp add: enum_ex)
-
-lemma exists1_code[code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum"
-unfolding list_ex1_iff enum_UNIV by auto
+ by (simp_all add: fun_eq_iff le_fun_def order_less_le)
-subsection {* Default instances *}
+subsubsection {* Operations on relations *}
-primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
- "n_lists 0 xs = [[]]"
- | "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
+lemma [code]:
+ "Id = image (\<lambda>x. (x, x)) (set Enum.enum)"
+ by (auto intro: imageI in_enum)
-lemma n_lists_Nil [simp]: "n_lists n [] = (if n = 0 then [[]] else [])"
- by (induct n) simp_all
+lemma tranclp_unfold [code, no_atp]:
+ "tranclp r a b \<longleftrightarrow> (a, b) \<in> trancl {(x, y). r x y}"
+ by (simp add: trancl_def)
-lemma length_n_lists: "length (n_lists n xs) = length xs ^ n"
- by (induct n) (auto simp add: length_concat o_def listsum_triv)
+lemma rtranclp_rtrancl_eq [code, no_atp]:
+ "rtranclp r x y \<longleftrightarrow> (x, y) \<in> rtrancl {(x, y). r x y}"
+ by (simp add: rtrancl_def)
-lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
- by (induct n arbitrary: ys) auto
+lemma max_ext_eq [code]:
+ "max_ext R = {(X, Y). finite X \<and> finite Y \<and> Y \<noteq> {} \<and> (\<forall>x. x \<in> X \<longrightarrow> (\<exists>xa \<in> Y. (x, xa) \<in> R))}"
+ by (auto simp add: max_ext.simps)
-lemma set_n_lists: "set (n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}"
-proof (rule set_eqI)
- fix ys :: "'a list"
- show "ys \<in> set (n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
- proof -
- have "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
- by (induct n arbitrary: ys) auto
- moreover have "\<And>x. ys \<in> set (n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs"
- by (induct n arbitrary: ys) auto
- moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (n_lists (length ys) xs)"
- by (induct ys) auto
- ultimately show ?thesis by auto
- qed
-qed
+lemma max_extp_eq [code]:
+ "max_extp r x y \<longleftrightarrow> (x, y) \<in> max_ext {(x, y). r x y}"
+ by (simp add: max_ext_def)
+
+lemma mlex_eq [code]:
+ "f <*mlex*> R = {(x, y). f x < f y \<or> (f x \<le> f y \<and> (x, y) \<in> R)}"
+ by (auto simp add: mlex_prod_def)
-lemma distinct_n_lists:
- assumes "distinct xs"
- shows "distinct (n_lists n xs)"
-proof (rule card_distinct)
- from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
- have "card (set (n_lists n xs)) = card (set xs) ^ n"
- proof (induct n)
- case 0 then show ?case by simp
- next
- case (Suc n)
- moreover have "card (\<Union>ys\<in>set (n_lists n xs). (\<lambda>y. y # ys) ` set xs)
- = (\<Sum>ys\<in>set (n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
- by (rule card_UN_disjoint) auto
- moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
- by (rule card_image) (simp add: inj_on_def)
- ultimately show ?case by auto
- qed
- also have "\<dots> = length xs ^ n" by (simp add: card_length)
- finally show "card (set (n_lists n xs)) = length (n_lists n xs)"
- by (simp add: length_n_lists)
-qed
+lemma [code]:
+ fixes xs :: "('a::finite \<times> 'a) list"
+ shows "acc (set xs) = bacc (set xs) (card_UNIV TYPE('a))"
+ by (simp add: card_UNIV_def acc_bacc_eq)
+
+lemma [code]:
+ "accp r = (\<lambda>x. x \<in> acc {(x, y). r x y})"
+ by (simp add: acc_def)
+
+
+subsection {* Default instances for @{class enum} *}
lemma map_of_zip_enum_is_Some:
assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
@@ -161,32 +210,29 @@
with length enum_distinct show "xs = ys" by (rule map_of_zip_inject)
qed
-definition
- all_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
+definition all_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
where
- "all_n_lists P n = (\<forall>xs \<in> set (n_lists n enum). P xs)"
+ "all_n_lists P n \<longleftrightarrow> (\<forall>xs \<in> set (List.n_lists n enum). P xs)"
lemma [code]:
- "all_n_lists P n = (if n = 0 then P [] else enum_all (%x. all_n_lists (%xs. P (x # xs)) (n - 1)))"
-unfolding all_n_lists_def enum_all
-by (cases n) (auto simp add: enum_UNIV)
+ "all_n_lists P n \<longleftrightarrow> (if n = 0 then P [] else enum_all (%x. all_n_lists (%xs. P (x # xs)) (n - 1)))"
+ unfolding all_n_lists_def enum_all
+ by (cases n) (auto simp add: enum_UNIV)
-definition
- ex_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
+definition ex_n_lists :: "(('a :: enum) list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"
where
- "ex_n_lists P n = (\<exists>xs \<in> set (n_lists n enum). P xs)"
+ "ex_n_lists P n \<longleftrightarrow> (\<exists>xs \<in> set (List.n_lists n enum). P xs)"
lemma [code]:
- "ex_n_lists P n = (if n = 0 then P [] else enum_ex (%x. ex_n_lists (%xs. P (x # xs)) (n - 1)))"
-unfolding ex_n_lists_def enum_ex
-by (cases n) (auto simp add: enum_UNIV)
-
+ "ex_n_lists P n \<longleftrightarrow> (if n = 0 then P [] else enum_ex (%x. ex_n_lists (%xs. P (x # xs)) (n - 1)))"
+ unfolding ex_n_lists_def enum_ex
+ by (cases n) (auto simp add: enum_UNIV)
instantiation "fun" :: (enum, enum) enum
begin
definition
- "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
+ "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (List.n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
definition
"enum_all P = all_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))"
@@ -194,7 +240,6 @@
definition
"enum_ex P = ex_n_lists (\<lambda>bs. P (the o map_of (zip enum bs))) (length (enum :: 'a list))"
-
instance proof
show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
proof (rule UNIV_eq_I)
@@ -208,13 +253,13 @@
from map_of_zip_enum_inject
show "distinct (enum \<Colon> ('a \<Rightarrow> 'b) list)"
by (auto intro!: inj_onI simp add: enum_fun_def
- distinct_map distinct_n_lists enum_distinct set_n_lists enum_all)
+ distinct_map distinct_n_lists enum_distinct set_n_lists)
next
fix P
- show "enum_all (P :: ('a \<Rightarrow> 'b) \<Rightarrow> bool) = (\<forall>x. P x)"
+ show "enum_all (P :: ('a \<Rightarrow> 'b) \<Rightarrow> bool) = Ball UNIV P"
proof
assume "enum_all P"
- show "\<forall>x. P x"
+ show "Ball UNIV P"
proof
fix f :: "'a \<Rightarrow> 'b"
have f: "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
@@ -228,19 +273,19 @@
from this f show "P f" by auto
qed
next
- assume "\<forall>x. P x"
+ assume "Ball UNIV P"
from this show "enum_all P"
unfolding enum_all_fun_def all_n_lists_def by auto
qed
next
fix P
- show "enum_ex (P :: ('a \<Rightarrow> 'b) \<Rightarrow> bool) = (\<exists>x. P x)"
+ show "enum_ex (P :: ('a \<Rightarrow> 'b) \<Rightarrow> bool) = Bex UNIV P"
proof
assume "enum_ex P"
- from this show "\<exists>x. P x"
+ from this show "Bex UNIV P"
unfolding enum_ex_fun_def ex_n_lists_def by auto
next
- assume "\<exists>x. P x"
+ assume "Bex UNIV P"
from this obtain f where "P f" ..
have f: "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
by (auto simp add: map_of_zip_map fun_eq_iff intro: in_enum)
@@ -258,239 +303,18 @@
end
lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list)
- in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
+ in map (\<lambda>ys. the o map_of (zip enum_a ys)) (List.n_lists (length enum_a) enum))"
by (simp add: enum_fun_def Let_def)
lemma enum_all_fun_code [code]:
"enum_all P = (let enum_a = (enum :: 'a::{enum, equal} list)
in all_n_lists (\<lambda>bs. P (the o map_of (zip enum_a bs))) (length enum_a))"
- by (simp add: enum_all_fun_def Let_def)
+ by (simp only: enum_all_fun_def Let_def)
lemma enum_ex_fun_code [code]:
"enum_ex P = (let enum_a = (enum :: 'a::{enum, equal} list)
in ex_n_lists (\<lambda>bs. P (the o map_of (zip enum_a bs))) (length enum_a))"
- by (simp add: enum_ex_fun_def Let_def)
-
-instantiation unit :: enum
-begin
-
-definition
- "enum = [()]"
-
-definition
- "enum_all P = P ()"
-
-definition
- "enum_ex P = P ()"
-
-instance proof
-qed (auto simp add: enum_unit_def UNIV_unit enum_all_unit_def enum_ex_unit_def intro: unit.exhaust)
-
-end
-
-instantiation bool :: enum
-begin
-
-definition
- "enum = [False, True]"
-
-definition
- "enum_all P = (P False \<and> P True)"
-
-definition
- "enum_ex P = (P False \<or> P True)"
-
-instance proof
- fix P
- show "enum_all (P :: bool \<Rightarrow> bool) = (\<forall>x. P x)"
- unfolding enum_all_bool_def by (auto, case_tac x) auto
-next
- fix P
- show "enum_ex (P :: bool \<Rightarrow> bool) = (\<exists>x. P x)"
- unfolding enum_ex_bool_def by (auto, case_tac x) auto
-qed (auto simp add: enum_bool_def UNIV_bool)
-
-end
-
-primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
- "product [] _ = []"
- | "product (x#xs) ys = map (Pair x) ys @ product xs ys"
-
-lemma product_list_set:
- "set (product xs ys) = set xs \<times> set ys"
- by (induct xs) auto
-
-lemma distinct_product:
- assumes "distinct xs" and "distinct ys"
- shows "distinct (product xs ys)"
- using assms by (induct xs)
- (auto intro: inj_onI simp add: product_list_set distinct_map)
-
-instantiation prod :: (enum, enum) enum
-begin
-
-definition
- "enum = product enum enum"
-
-definition
- "enum_all P = enum_all (%x. enum_all (%y. P (x, y)))"
-
-definition
- "enum_ex P = enum_ex (%x. enum_ex (%y. P (x, y)))"
-
-
-instance by default
- (simp_all add: enum_prod_def product_list_set distinct_product
- enum_UNIV enum_distinct enum_all_prod_def enum_all enum_ex_prod_def enum_ex)
-
-end
-
-instantiation sum :: (enum, enum) enum
-begin
-
-definition
- "enum = map Inl enum @ map Inr enum"
-
-definition
- "enum_all P = (enum_all (%x. P (Inl x)) \<and> enum_all (%x. P (Inr x)))"
-
-definition
- "enum_ex P = (enum_ex (%x. P (Inl x)) \<or> enum_ex (%x. P (Inr x)))"
-
-instance proof
- fix P
- show "enum_all (P :: ('a + 'b) \<Rightarrow> bool) = (\<forall>x. P x)"
- unfolding enum_all_sum_def enum_all
- by (auto, case_tac x) auto
-next
- fix P
- show "enum_ex (P :: ('a + 'b) \<Rightarrow> bool) = (\<exists>x. P x)"
- unfolding enum_ex_sum_def enum_ex
- by (auto, case_tac x) auto
-qed (auto simp add: enum_UNIV enum_sum_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct)
-
-end
-
-instantiation nibble :: enum
-begin
-
-definition
- "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
- Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
-
-definition
- "enum_all P = (P Nibble0 \<and> P Nibble1 \<and> P Nibble2 \<and> P Nibble3 \<and> P Nibble4 \<and> P Nibble5 \<and> P Nibble6 \<and> P Nibble7
- \<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF)"
-
-definition
- "enum_ex P = (P Nibble0 \<or> P Nibble1 \<or> P Nibble2 \<or> P Nibble3 \<or> P Nibble4 \<or> P Nibble5 \<or> P Nibble6 \<or> P Nibble7
- \<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF)"
-
-instance proof
- fix P
- show "enum_all (P :: nibble \<Rightarrow> bool) = (\<forall>x. P x)"
- unfolding enum_all_nibble_def
- by (auto, case_tac x) auto
-next
- fix P
- show "enum_ex (P :: nibble \<Rightarrow> bool) = (\<exists>x. P x)"
- unfolding enum_ex_nibble_def
- by (auto, case_tac x) auto
-qed (simp_all add: enum_nibble_def UNIV_nibble)
-
-end
-
-instantiation char :: enum
-begin
-
-definition
- "enum = map (split Char) (product enum enum)"
-
-lemma enum_chars [code]:
- "enum = chars"
- unfolding enum_char_def chars_def enum_nibble_def by simp
-
-definition
- "enum_all P = list_all P chars"
-
-definition
- "enum_ex P = list_ex P chars"
-
-lemma set_enum_char: "set (enum :: char list) = UNIV"
- by (auto intro: char.exhaust simp add: enum_char_def product_list_set enum_UNIV full_SetCompr_eq [symmetric])
-
-instance proof
- fix P
- show "enum_all (P :: char \<Rightarrow> bool) = (\<forall>x. P x)"
- unfolding enum_all_char_def enum_chars[symmetric]
- by (auto simp add: list_all_iff set_enum_char)
-next
- fix P
- show "enum_ex (P :: char \<Rightarrow> bool) = (\<exists>x. P x)"
- unfolding enum_ex_char_def enum_chars[symmetric]
- by (auto simp add: list_ex_iff set_enum_char)
-next
- show "distinct (enum :: char list)"
- by (auto intro: inj_onI simp add: enum_char_def product_list_set distinct_map distinct_product enum_distinct)
-qed (auto simp add: set_enum_char)
-
-end
-
-instantiation option :: (enum) enum
-begin
-
-definition
- "enum = None # map Some enum"
-
-definition
- "enum_all P = (P None \<and> enum_all (%x. P (Some x)))"
-
-definition
- "enum_ex P = (P None \<or> enum_ex (%x. P (Some x)))"
-
-instance proof
- fix P
- show "enum_all (P :: 'a option \<Rightarrow> bool) = (\<forall>x. P x)"
- unfolding enum_all_option_def enum_all
- by (auto, case_tac x) auto
-next
- fix P
- show "enum_ex (P :: 'a option \<Rightarrow> bool) = (\<exists>x. P x)"
- unfolding enum_ex_option_def enum_ex
- by (auto, case_tac x) auto
-qed (auto simp add: enum_UNIV enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct)
-end
-
-primrec sublists :: "'a list \<Rightarrow> 'a list list" where
- "sublists [] = [[]]"
- | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
-
-lemma length_sublists:
- "length (sublists xs) = 2 ^ length xs"
- by (induct xs) (simp_all add: Let_def)
-
-lemma sublists_powset:
- "set ` set (sublists xs) = Pow (set xs)"
-proof -
- have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
- by (auto simp add: image_def)
- have "set (map set (sublists xs)) = Pow (set xs)"
- by (induct xs)
- (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
- then show ?thesis by simp
-qed
-
-lemma distinct_set_sublists:
- assumes "distinct xs"
- shows "distinct (map set (sublists xs))"
-proof (rule card_distinct)
- have "finite (set xs)" by rule
- then have "card (Pow (set xs)) = 2 ^ card (set xs)" by (rule card_Pow)
- with assms distinct_card [of xs]
- have "card (Pow (set xs)) = 2 ^ length xs" by simp
- then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
- by (simp add: sublists_powset length_sublists)
-qed
+ by (simp only: enum_ex_fun_def Let_def)
instantiation set :: (enum) enum
begin
@@ -510,6 +334,133 @@
end
+instantiation unit :: enum
+begin
+
+definition
+ "enum = [()]"
+
+definition
+ "enum_all P = P ()"
+
+definition
+ "enum_ex P = P ()"
+
+instance proof
+qed (auto simp add: enum_unit_def enum_all_unit_def enum_ex_unit_def)
+
+end
+
+instantiation bool :: enum
+begin
+
+definition
+ "enum = [False, True]"
+
+definition
+ "enum_all P \<longleftrightarrow> P False \<and> P True"
+
+definition
+ "enum_ex P \<longleftrightarrow> P False \<or> P True"
+
+instance proof
+qed (simp_all only: enum_bool_def enum_all_bool_def enum_ex_bool_def UNIV_bool, simp_all)
+
+end
+
+instantiation prod :: (enum, enum) enum
+begin
+
+definition
+ "enum = List.product enum enum"
+
+definition
+ "enum_all P = enum_all (%x. enum_all (%y. P (x, y)))"
+
+definition
+ "enum_ex P = enum_ex (%x. enum_ex (%y. P (x, y)))"
+
+
+instance by default
+ (simp_all add: enum_prod_def product_list_set distinct_product
+ enum_UNIV enum_distinct enum_all_prod_def enum_ex_prod_def)
+
+end
+
+instantiation sum :: (enum, enum) enum
+begin
+
+definition
+ "enum = map Inl enum @ map Inr enum"
+
+definition
+ "enum_all P \<longleftrightarrow> enum_all (\<lambda>x. P (Inl x)) \<and> enum_all (\<lambda>x. P (Inr x))"
+
+definition
+ "enum_ex P \<longleftrightarrow> enum_ex (\<lambda>x. P (Inl x)) \<or> enum_ex (\<lambda>x. P (Inr x))"
+
+instance proof
+qed (simp_all only: enum_sum_def enum_all_sum_def enum_ex_sum_def UNIV_sum,
+ auto simp add: enum_UNIV distinct_map enum_distinct)
+
+end
+
+instantiation nibble :: enum
+begin
+
+definition
+ "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
+ Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
+
+definition
+ "enum_all P \<longleftrightarrow> P Nibble0 \<and> P Nibble1 \<and> P Nibble2 \<and> P Nibble3 \<and> P Nibble4 \<and> P Nibble5 \<and> P Nibble6 \<and> P Nibble7
+ \<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF"
+
+definition
+ "enum_ex P \<longleftrightarrow> P Nibble0 \<or> P Nibble1 \<or> P Nibble2 \<or> P Nibble3 \<or> P Nibble4 \<or> P Nibble5 \<or> P Nibble6 \<or> P Nibble7
+ \<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF"
+
+instance proof
+qed (simp_all only: enum_nibble_def enum_all_nibble_def enum_ex_nibble_def UNIV_nibble, simp_all)
+
+end
+
+instantiation char :: enum
+begin
+
+definition
+ "enum = chars"
+
+definition
+ "enum_all P \<longleftrightarrow> list_all P chars"
+
+definition
+ "enum_ex P \<longleftrightarrow> list_ex P chars"
+
+instance proof
+qed (simp_all only: enum_char_def enum_all_char_def enum_ex_char_def UNIV_set_chars distinct_chars,
+ simp_all add: list_all_iff list_ex_iff)
+
+end
+
+instantiation option :: (enum) enum
+begin
+
+definition
+ "enum = None # map Some enum"
+
+definition
+ "enum_all P \<longleftrightarrow> P None \<and> enum_all (\<lambda>x. P (Some x))"
+
+definition
+ "enum_ex P \<longleftrightarrow> P None \<or> enum_ex (\<lambda>x. P (Some x))"
+
+instance proof
+qed (simp_all only: enum_option_def enum_all_option_def enum_ex_option_def UNIV_option_conv,
+ auto simp add: distinct_map enum_UNIV enum_distinct)
+
+end
+
subsection {* Small finite types *}
@@ -519,6 +470,10 @@
notation (output) a\<^isub>1 ("a\<^isub>1")
+lemma UNIV_finite_1:
+ "UNIV = {a\<^isub>1}"
+ by (auto intro: finite_1.exhaust)
+
instantiation finite_1 :: enum
begin
@@ -532,29 +487,20 @@
"enum_ex P = P a\<^isub>1"
instance proof
- fix P
- show "enum_all (P :: finite_1 \<Rightarrow> bool) = (\<forall>x. P x)"
- unfolding enum_all_finite_1_def
- by (auto, case_tac x) auto
-next
- fix P
- show "enum_ex (P :: finite_1 \<Rightarrow> bool) = (\<exists>x. P x)"
- unfolding enum_ex_finite_1_def
- by (auto, case_tac x) auto
-qed (auto simp add: enum_finite_1_def intro: finite_1.exhaust)
+qed (simp_all only: enum_finite_1_def enum_all_finite_1_def enum_ex_finite_1_def UNIV_finite_1, simp_all)
end
instantiation finite_1 :: linorder
begin
+definition less_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
+where
+ "x < (y :: finite_1) \<longleftrightarrow> False"
+
definition less_eq_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
where
- "less_eq_finite_1 x y = True"
-
-definition less_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
-where
- "less_finite_1 x y = False"
+ "x \<le> (y :: finite_1) \<longleftrightarrow> True"
instance
apply (intro_classes)
@@ -571,6 +517,10 @@
notation (output) a\<^isub>1 ("a\<^isub>1")
notation (output) a\<^isub>2 ("a\<^isub>2")
+lemma UNIV_finite_2:
+ "UNIV = {a\<^isub>1, a\<^isub>2}"
+ by (auto intro: finite_2.exhaust)
+
instantiation finite_2 :: enum
begin
@@ -578,22 +528,13 @@
"enum = [a\<^isub>1, a\<^isub>2]"
definition
- "enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2)"
+ "enum_all P \<longleftrightarrow> P a\<^isub>1 \<and> P a\<^isub>2"
definition
- "enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2)"
+ "enum_ex P \<longleftrightarrow> P a\<^isub>1 \<or> P a\<^isub>2"
instance proof
- fix P
- show "enum_all (P :: finite_2 \<Rightarrow> bool) = (\<forall>x. P x)"
- unfolding enum_all_finite_2_def
- by (auto, case_tac x) auto
-next
- fix P
- show "enum_ex (P :: finite_2 \<Rightarrow> bool) = (\<exists>x. P x)"
- unfolding enum_ex_finite_2_def
- by (auto, case_tac x) auto
-qed (auto simp add: enum_finite_2_def intro: finite_2.exhaust)
+qed (simp_all only: enum_finite_2_def enum_all_finite_2_def enum_ex_finite_2_def UNIV_finite_2, simp_all)
end
@@ -602,30 +543,32 @@
definition less_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
where
- "less_finite_2 x y = ((x = a\<^isub>1) & (y = a\<^isub>2))"
+ "x < y \<longleftrightarrow> x = a\<^isub>1 \<and> y = a\<^isub>2"
definition less_eq_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
where
- "less_eq_finite_2 x y = ((x = y) \<or> (x < y))"
-
+ "x \<le> y \<longleftrightarrow> x = y \<or> x < (y :: finite_2)"
instance
apply (intro_classes)
apply (auto simp add: less_finite_2_def less_eq_finite_2_def)
-apply (metis finite_2.distinct finite_2.nchotomy)+
+apply (metis finite_2.nchotomy)+
done
end
hide_const (open) a\<^isub>1 a\<^isub>2
-
datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
notation (output) a\<^isub>1 ("a\<^isub>1")
notation (output) a\<^isub>2 ("a\<^isub>2")
notation (output) a\<^isub>3 ("a\<^isub>3")
+lemma UNIV_finite_3:
+ "UNIV = {a\<^isub>1, a\<^isub>2, a\<^isub>3}"
+ by (auto intro: finite_3.exhaust)
+
instantiation finite_3 :: enum
begin
@@ -633,22 +576,13 @@
"enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3]"
definition
- "enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3)"
+ "enum_all P \<longleftrightarrow> P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3"
definition
- "enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3)"
+ "enum_ex P \<longleftrightarrow> P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3"
instance proof
- fix P
- show "enum_all (P :: finite_3 \<Rightarrow> bool) = (\<forall>x. P x)"
- unfolding enum_all_finite_3_def
- by (auto, case_tac x) auto
-next
- fix P
- show "enum_ex (P :: finite_3 \<Rightarrow> bool) = (\<exists>x. P x)"
- unfolding enum_ex_finite_3_def
- by (auto, case_tac x) auto
-qed (auto simp add: enum_finite_3_def intro: finite_3.exhaust)
+qed (simp_all only: enum_finite_3_def enum_all_finite_3_def enum_ex_finite_3_def UNIV_finite_3, simp_all)
end
@@ -657,13 +591,11 @@
definition less_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
where
- "less_finite_3 x y = (case x of a\<^isub>1 => (y \<noteq> a\<^isub>1)
- | a\<^isub>2 => (y = a\<^isub>3)| a\<^isub>3 => False)"
+ "x < y = (case x of a\<^isub>1 \<Rightarrow> y \<noteq> a\<^isub>1 | a\<^isub>2 \<Rightarrow> y = a\<^isub>3 | a\<^isub>3 \<Rightarrow> False)"
definition less_eq_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
where
- "less_eq_finite_3 x y = ((x = y) \<or> (x < y))"
-
+ "x \<le> y \<longleftrightarrow> x = y \<or> x < (y :: finite_3)"
instance proof (intro_classes)
qed (auto simp add: less_finite_3_def less_eq_finite_3_def split: finite_3.split_asm)
@@ -672,7 +604,6 @@
hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3
-
datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
notation (output) a\<^isub>1 ("a\<^isub>1")
@@ -680,6 +611,10 @@
notation (output) a\<^isub>3 ("a\<^isub>3")
notation (output) a\<^isub>4 ("a\<^isub>4")
+lemma UNIV_finite_4:
+ "UNIV = {a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4}"
+ by (auto intro: finite_4.exhaust)
+
instantiation finite_4 :: enum
begin
@@ -687,22 +622,13 @@
"enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4]"
definition
- "enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3 \<and> P a\<^isub>4)"
+ "enum_all P \<longleftrightarrow> P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3 \<and> P a\<^isub>4"
definition
- "enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3 \<or> P a\<^isub>4)"
+ "enum_ex P \<longleftrightarrow> P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3 \<or> P a\<^isub>4"
instance proof
- fix P
- show "enum_all (P :: finite_4 \<Rightarrow> bool) = (\<forall>x. P x)"
- unfolding enum_all_finite_4_def
- by (auto, case_tac x) auto
-next
- fix P
- show "enum_ex (P :: finite_4 \<Rightarrow> bool) = (\<exists>x. P x)"
- unfolding enum_ex_finite_4_def
- by (auto, case_tac x) auto
-qed (auto simp add: enum_finite_4_def intro: finite_4.exhaust)
+qed (simp_all only: enum_finite_4_def enum_all_finite_4_def enum_ex_finite_4_def UNIV_finite_4, simp_all)
end
@@ -717,6 +643,10 @@
notation (output) a\<^isub>4 ("a\<^isub>4")
notation (output) a\<^isub>5 ("a\<^isub>5")
+lemma UNIV_finite_5:
+ "UNIV = {a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4, a\<^isub>5}"
+ by (auto intro: finite_5.exhaust)
+
instantiation finite_5 :: enum
begin
@@ -724,246 +654,23 @@
"enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4, a\<^isub>5]"
definition
- "enum_all P = (P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3 \<and> P a\<^isub>4 \<and> P a\<^isub>5)"
+ "enum_all P \<longleftrightarrow> P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3 \<and> P a\<^isub>4 \<and> P a\<^isub>5"
definition
- "enum_ex P = (P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3 \<or> P a\<^isub>4 \<or> P a\<^isub>5)"
+ "enum_ex P \<longleftrightarrow> P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3 \<or> P a\<^isub>4 \<or> P a\<^isub>5"
instance proof
- fix P
- show "enum_all (P :: finite_5 \<Rightarrow> bool) = (\<forall>x. P x)"
- unfolding enum_all_finite_5_def
- by (auto, case_tac x) auto
-next
- fix P
- show "enum_ex (P :: finite_5 \<Rightarrow> bool) = (\<exists>x. P x)"
- unfolding enum_ex_finite_5_def
- by (auto, case_tac x) auto
-qed (auto simp add: enum_finite_5_def intro: finite_5.exhaust)
+qed (simp_all only: enum_finite_5_def enum_all_finite_5_def enum_ex_finite_5_def UNIV_finite_5, simp_all)
end
hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
-subsection {* An executable THE operator on finite types *}
-
-definition
- [code del]: "enum_the P = The P"
-
-lemma [code]:
- "The P = (case filter P enum of [x] => x | _ => enum_the P)"
-proof -
- {
- fix a
- assume filter_enum: "filter P enum = [a]"
- have "The P = a"
- proof (rule the_equality)
- fix x
- assume "P x"
- show "x = a"
- proof (rule ccontr)
- assume "x \<noteq> a"
- from filter_enum obtain us vs
- where enum_eq: "enum = us @ [a] @ vs"
- and "\<forall> x \<in> set us. \<not> P x"
- and "\<forall> x \<in> set vs. \<not> P x"
- and "P a"
- by (auto simp add: filter_eq_Cons_iff) (simp only: filter_empty_conv[symmetric])
- with `P x` in_enum[of x, unfolded enum_eq] `x \<noteq> a` show "False" by auto
- qed
- next
- from filter_enum show "P a" by (auto simp add: filter_eq_Cons_iff)
- qed
- }
- from this show ?thesis
- unfolding enum_the_def by (auto split: list.split)
-qed
-
-code_abort enum_the
-code_const enum_the (Eval "(fn p => raise Match)")
-
-subsection {* Further operations on finite types *}
-
-lemma Collect_code[code]:
- "Collect P = set (filter P enum)"
-by (auto simp add: enum_UNIV)
-
-lemma [code]:
- "Id = image (%x. (x, x)) (set Enum.enum)"
-by (auto intro: imageI in_enum)
-
-lemma tranclp_unfold [code, no_atp]:
- "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
-by (simp add: trancl_def)
-
-lemma rtranclp_rtrancl_eq[code, no_atp]:
- "rtranclp r x y = ((x, y) : rtrancl {(x, y). r x y})"
-unfolding rtrancl_def by auto
-
-lemma max_ext_eq[code]:
- "max_ext R = {(X, Y). finite X & finite Y & Y ~={} & (ALL x. x : X --> (EX xa : Y. (x, xa) : R))}"
-by (auto simp add: max_ext.simps)
-
-lemma max_extp_eq[code]:
- "max_extp r x y = ((x, y) : max_ext {(x, y). r x y})"
-unfolding max_ext_def by auto
-
-lemma mlex_eq[code]:
- "f <*mlex*> R = {(x, y). f x < f y \<or> (f x <= f y \<and> (x, y) : R)}"
-unfolding mlex_prod_def by auto
-
-subsection {* Executable accessible part *}
-(* FIXME: should be moved somewhere else !? *)
-
-subsubsection {* Finite monotone eventually stable sequences *}
-
-lemma finite_mono_remains_stable_implies_strict_prefix:
- fixes f :: "nat \<Rightarrow> 'a::order"
- assumes S: "finite (range f)" "mono f" and eq: "\<forall>n. f n = f (Suc n) \<longrightarrow> f (Suc n) = f (Suc (Suc n))"
- shows "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m < f n) \<and> (\<forall>n\<ge>N. f N = f n)"
- using assms
-proof -
- have "\<exists>n. f n = f (Suc n)"
- proof (rule ccontr)
- assume "\<not> ?thesis"
- then have "\<And>n. f n \<noteq> f (Suc n)" by auto
- then have "\<And>n. f n < f (Suc n)"
- using `mono f` by (auto simp: le_less mono_iff_le_Suc)
- with lift_Suc_mono_less_iff[of f]
- have "\<And>n m. n < m \<Longrightarrow> f n < f m" by auto
- then have "inj f"
- by (auto simp: inj_on_def) (metis linorder_less_linear order_less_imp_not_eq)
- with `finite (range f)` have "finite (UNIV::nat set)"
- by (rule finite_imageD)
- then show False by simp
- qed
- then obtain n where n: "f n = f (Suc n)" ..
- def N \<equiv> "LEAST n. f n = f (Suc n)"
- have N: "f N = f (Suc N)"
- unfolding N_def using n by (rule LeastI)
- show ?thesis
- proof (intro exI[of _ N] conjI allI impI)
- fix n assume "N \<le> n"
- then have "\<And>m. N \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m = f N"
- proof (induct rule: dec_induct)
- case (step n) then show ?case
- using eq[rule_format, of "n - 1"] N
- by (cases n) (auto simp add: le_Suc_eq)
- qed simp
- from this[of n] `N \<le> n` show "f N = f n" by auto
- next
- fix n m :: nat assume "m < n" "n \<le> N"
- then show "f m < f n"
- proof (induct rule: less_Suc_induct[consumes 1])
- case (1 i)
- then have "i < N" by simp
- then have "f i \<noteq> f (Suc i)"
- unfolding N_def by (rule not_less_Least)
- with `mono f` show ?case by (simp add: mono_iff_le_Suc less_le)
- qed auto
- qed
-qed
-
-lemma finite_mono_strict_prefix_implies_finite_fixpoint:
- fixes f :: "nat \<Rightarrow> 'a set"
- assumes S: "\<And>i. f i \<subseteq> S" "finite S"
- and inj: "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n) \<and> (\<forall>n\<ge>N. f N = f n)"
- shows "f (card S) = (\<Union>n. f n)"
-proof -
- from inj obtain N where inj: "(\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n)" and eq: "(\<forall>n\<ge>N. f N = f n)" by auto
-
- { fix i have "i \<le> N \<Longrightarrow> i \<le> card (f i)"
- proof (induct i)
- case 0 then show ?case by simp
- next
- case (Suc i)
- with inj[rule_format, of "Suc i" i]
- have "(f i) \<subset> (f (Suc i))" by auto
- moreover have "finite (f (Suc i))" using S by (rule finite_subset)
- ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono)
- with Suc show ?case using inj by auto
- qed
- }
- then have "N \<le> card (f N)" by simp
- also have "\<dots> \<le> card S" using S by (intro card_mono)
- finally have "f (card S) = f N" using eq by auto
- then show ?thesis using eq inj[rule_format, of N]
- apply auto
- apply (case_tac "n < N")
- apply (auto simp: not_less)
- done
-qed
-
-subsubsection {* Bounded accessible part *}
-
-fun bacc :: "('a * 'a) set => nat => 'a set"
-where
- "bacc r 0 = {x. \<forall> y. (y, x) \<notin> r}"
-| "bacc r (Suc n) = (bacc r n Un {x. \<forall> y. (y, x) : r --> y : bacc r n})"
-
-lemma bacc_subseteq_acc:
- "bacc r n \<subseteq> acc r"
-by (induct n) (auto intro: acc.intros)
-
-lemma bacc_mono:
- "n <= m ==> bacc r n \<subseteq> bacc r m"
-by (induct rule: dec_induct) auto
-
-lemma bacc_upper_bound:
- "bacc (r :: ('a * 'a) set) (card (UNIV :: ('a :: enum) set)) = (UN n. bacc r n)"
-proof -
- have "mono (bacc r)" unfolding mono_def by (simp add: bacc_mono)
- moreover have "\<forall>n. bacc r n = bacc r (Suc n) \<longrightarrow> bacc r (Suc n) = bacc r (Suc (Suc n))" by auto
- moreover have "finite (range (bacc r))" by auto
- ultimately show ?thesis
- by (intro finite_mono_strict_prefix_implies_finite_fixpoint)
- (auto intro: finite_mono_remains_stable_implies_strict_prefix simp add: enum_UNIV)
-qed
-
-lemma acc_subseteq_bacc:
- assumes "finite r"
- shows "acc r \<subseteq> (UN n. bacc r n)"
-proof
- fix x
- assume "x : acc r"
- then have "\<exists> n. x : bacc r n"
- proof (induct x arbitrary: rule: acc.induct)
- case (accI x)
- then have "\<forall>y. \<exists> n. (y, x) \<in> r --> y : bacc r n" by simp
- from choice[OF this] obtain n where n: "\<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r (n y)" ..
- obtain n where "\<And>y. (y, x) : r \<Longrightarrow> y : bacc r n"
- proof
- fix y assume y: "(y, x) : r"
- with n have "y : bacc r (n y)" by auto
- moreover have "n y <= Max ((%(y, x). n y) ` r)"
- using y `finite r` by (auto intro!: Max_ge)
- note bacc_mono[OF this, of r]
- ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto
- qed
- then show ?case
- by (auto simp add: Let_def intro!: exI[of _ "Suc n"])
- qed
- then show "x : (UN n. bacc r n)" by auto
-qed
-
-lemma acc_bacc_eq: "acc ((set xs) :: (('a :: enum) * 'a) set) = bacc (set xs) (card (UNIV :: 'a set))"
-by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound finite_set order_eq_iff)
-
-definition
- [code del]: "card_UNIV = card UNIV"
-
-lemma [code]:
- "card_UNIV TYPE('a :: enum) = card (set (Enum.enum :: 'a list))"
-unfolding card_UNIV_def enum_UNIV ..
-
-declare acc_bacc_eq[folded card_UNIV_def, code]
-
-lemma [code_unfold]: "accp r = (%x. x : acc {(x, y). r x y})"
-unfolding acc_def by simp
subsection {* Closing up *}
hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5
-hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product ntrancl
+hide_const (open) enum enum_all enum_ex all_n_lists ex_n_lists ntrancl
end
+
--- a/src/HOL/Hilbert_Choice.thy Fri Oct 19 15:12:52 2012 +0200
+++ b/src/HOL/Hilbert_Choice.thy Sun Oct 21 17:04:13 2012 +0200
@@ -6,7 +6,7 @@
header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
theory Hilbert_Choice
-imports Nat Wellfounded Plain
+imports Nat Wellfounded Big_Operators
keywords "specification" "ax_specification" :: thy_goal
begin
@@ -643,6 +643,144 @@
done
+subsection {* An aside: bounded accessible part *}
+
+text {* Finite monotone eventually stable sequences *}
+
+lemma finite_mono_remains_stable_implies_strict_prefix:
+ fixes f :: "nat \<Rightarrow> 'a::order"
+ assumes S: "finite (range f)" "mono f" and eq: "\<forall>n. f n = f (Suc n) \<longrightarrow> f (Suc n) = f (Suc (Suc n))"
+ shows "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m < f n) \<and> (\<forall>n\<ge>N. f N = f n)"
+ using assms
+proof -
+ have "\<exists>n. f n = f (Suc n)"
+ proof (rule ccontr)
+ assume "\<not> ?thesis"
+ then have "\<And>n. f n \<noteq> f (Suc n)" by auto
+ then have "\<And>n. f n < f (Suc n)"
+ using `mono f` by (auto simp: le_less mono_iff_le_Suc)
+ with lift_Suc_mono_less_iff[of f]
+ have "\<And>n m. n < m \<Longrightarrow> f n < f m" by auto
+ then have "inj f"
+ by (auto simp: inj_on_def) (metis linorder_less_linear order_less_imp_not_eq)
+ with `finite (range f)` have "finite (UNIV::nat set)"
+ by (rule finite_imageD)
+ then show False by simp
+ qed
+ then obtain n where n: "f n = f (Suc n)" ..
+ def N \<equiv> "LEAST n. f n = f (Suc n)"
+ have N: "f N = f (Suc N)"
+ unfolding N_def using n by (rule LeastI)
+ show ?thesis
+ proof (intro exI[of _ N] conjI allI impI)
+ fix n assume "N \<le> n"
+ then have "\<And>m. N \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m = f N"
+ proof (induct rule: dec_induct)
+ case (step n) then show ?case
+ using eq[rule_format, of "n - 1"] N
+ by (cases n) (auto simp add: le_Suc_eq)
+ qed simp
+ from this[of n] `N \<le> n` show "f N = f n" by auto
+ next
+ fix n m :: nat assume "m < n" "n \<le> N"
+ then show "f m < f n"
+ proof (induct rule: less_Suc_induct[consumes 1])
+ case (1 i)
+ then have "i < N" by simp
+ then have "f i \<noteq> f (Suc i)"
+ unfolding N_def by (rule not_less_Least)
+ with `mono f` show ?case by (simp add: mono_iff_le_Suc less_le)
+ qed auto
+ qed
+qed
+
+lemma finite_mono_strict_prefix_implies_finite_fixpoint:
+ fixes f :: "nat \<Rightarrow> 'a set"
+ assumes S: "\<And>i. f i \<subseteq> S" "finite S"
+ and inj: "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n) \<and> (\<forall>n\<ge>N. f N = f n)"
+ shows "f (card S) = (\<Union>n. f n)"
+proof -
+ from inj obtain N where inj: "(\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n)" and eq: "(\<forall>n\<ge>N. f N = f n)" by auto
+
+ { fix i have "i \<le> N \<Longrightarrow> i \<le> card (f i)"
+ proof (induct i)
+ case 0 then show ?case by simp
+ next
+ case (Suc i)
+ with inj[rule_format, of "Suc i" i]
+ have "(f i) \<subset> (f (Suc i))" by auto
+ moreover have "finite (f (Suc i))" using S by (rule finite_subset)
+ ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono)
+ with Suc show ?case using inj by auto
+ qed
+ }
+ then have "N \<le> card (f N)" by simp
+ also have "\<dots> \<le> card S" using S by (intro card_mono)
+ finally have "f (card S) = f N" using eq by auto
+ then show ?thesis using eq inj[rule_format, of N]
+ apply auto
+ apply (case_tac "n < N")
+ apply (auto simp: not_less)
+ done
+qed
+
+primrec bacc :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> 'a set"
+where
+ "bacc r 0 = {x. \<forall> y. (y, x) \<notin> r}"
+| "bacc r (Suc n) = (bacc r n \<union> {x. \<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r n})"
+
+lemma bacc_subseteq_acc:
+ "bacc r n \<subseteq> acc r"
+ by (induct n) (auto intro: acc.intros)
+
+lemma bacc_mono:
+ "n \<le> m \<Longrightarrow> bacc r n \<subseteq> bacc r m"
+ by (induct rule: dec_induct) auto
+
+lemma bacc_upper_bound:
+ "bacc (r :: ('a \<times> 'a) set) (card (UNIV :: 'a::finite set)) = (\<Union>n. bacc r n)"
+proof -
+ have "mono (bacc r)" unfolding mono_def by (simp add: bacc_mono)
+ moreover have "\<forall>n. bacc r n = bacc r (Suc n) \<longrightarrow> bacc r (Suc n) = bacc r (Suc (Suc n))" by auto
+ moreover have "finite (range (bacc r))" by auto
+ ultimately show ?thesis
+ by (intro finite_mono_strict_prefix_implies_finite_fixpoint)
+ (auto intro: finite_mono_remains_stable_implies_strict_prefix)
+qed
+
+lemma acc_subseteq_bacc:
+ assumes "finite r"
+ shows "acc r \<subseteq> (\<Union>n. bacc r n)"
+proof
+ fix x
+ assume "x : acc r"
+ then have "\<exists> n. x : bacc r n"
+ proof (induct x arbitrary: rule: acc.induct)
+ case (accI x)
+ then have "\<forall>y. \<exists> n. (y, x) \<in> r --> y : bacc r n" by simp
+ from choice[OF this] obtain n where n: "\<forall>y. (y, x) \<in> r \<longrightarrow> y \<in> bacc r (n y)" ..
+ obtain n where "\<And>y. (y, x) : r \<Longrightarrow> y : bacc r n"
+ proof
+ fix y assume y: "(y, x) : r"
+ with n have "y : bacc r (n y)" by auto
+ moreover have "n y <= Max ((%(y, x). n y) ` r)"
+ using y `finite r` by (auto intro!: Max_ge)
+ note bacc_mono[OF this, of r]
+ ultimately show "y : bacc r (Max ((%(y, x). n y) ` r))" by auto
+ qed
+ then show ?case
+ by (auto simp add: Let_def intro!: exI[of _ "Suc n"])
+ qed
+ then show "x : (UN n. bacc r n)" by auto
+qed
+
+lemma acc_bacc_eq:
+ fixes A :: "('a :: finite \<times> 'a) set"
+ assumes "finite A"
+ shows "acc A = bacc A (card (UNIV :: 'a set))"
+ using assms by (metis acc_subseteq_bacc bacc_subseteq_acc bacc_upper_bound order_eq_iff)
+
+
subsection {* Specification package -- Hilbertized version *}
lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c"
@@ -651,3 +789,4 @@
ML_file "Tools/choice_specification.ML"
end
+
--- a/src/HOL/Library/Cardinality.thy Fri Oct 19 15:12:52 2012 +0200
+++ b/src/HOL/Library/Cardinality.thy Sun Oct 21 17:04:13 2012 +0200
@@ -92,7 +92,7 @@
unfolding bs[symmetric] distinct_card[OF distb] ..
have ca: "CARD('a) = length as"
unfolding as[symmetric] distinct_card[OF dista] ..
- let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (Enum.n_lists (length as) bs)"
+ let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (List.n_lists (length as) bs)"
have "UNIV = set ?xs"
proof(rule UNIV_eq_I)
fix f :: "'a \<Rightarrow> 'b"
@@ -103,8 +103,8 @@
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 (Enum.n_lists (length as) bs)"
- and ys: "ys \<in> set (Enum.n_lists (length as) bs)"
+ assume xs: "xs \<in> set (List.n_lists (length as) bs)"
+ and ys: "ys \<in> set (List.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)
@@ -472,3 +472,4 @@
hide_const (open) card' finite' subset' eq_set
end
+
--- a/src/HOL/Library/Mapping.thy Fri Oct 19 15:12:52 2012 +0200
+++ b/src/HOL/Library/Mapping.thy Sun Oct 21 17:04:13 2012 +0200
@@ -5,7 +5,7 @@
header {* An abstract view on maps for code generation. *}
theory Mapping
-imports Main "~~/src/HOL/Library/Quotient_Option"
+imports Main
begin
subsection {* Type definition and primitive operations *}
@@ -61,7 +61,10 @@
| Some v \<Rightarrow> m (k \<mapsto> (f v)))" .
lemma map_entry_code [code]: "map_entry k f m = (case lookup m k of None \<Rightarrow> m
- | Some v \<Rightarrow> update k (f v) m)" by transfer rule
+ | Some v \<Rightarrow> update k (f v) m)"
+ apply (cases "lookup m k")
+ apply simp_all
+ by (transfer, simp)+
definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
"map_default k v f m = map_entry k f (default k v m)"
--- a/src/HOL/Library/RBT.thy Fri Oct 19 15:12:52 2012 +0200
+++ b/src/HOL/Library/RBT.thy Sun Oct 21 17:04:13 2012 +0200
@@ -97,9 +97,6 @@
"RBT_Impl.keys (impl_of t) = keys t"
by transfer (rule refl)
-(* FIXME *)
-lemma [transfer_rule]: "(fun_rel (fun_rel op = op =) op =) dom dom" unfolding fun_rel_def by auto
-
lemma lookup_keys:
"dom (lookup t) = set (keys t)"
by transfer (simp add: rbt_lookup_keys)
--- a/src/HOL/Library/RBT_Set.thy Fri Oct 19 15:12:52 2012 +0200
+++ b/src/HOL/Library/RBT_Set.thy Sun Oct 21 17:04:13 2012 +0200
@@ -63,6 +63,11 @@
lemma [code, code del]:
"Bex = Bex" ..
+term can_select
+
+lemma [code, code del]:
+ "can_select = can_select" ..
+
lemma [code, code del]:
"Set.union = Set.union" ..
--- a/src/HOL/List.thy Fri Oct 19 15:12:52 2012 +0200
+++ b/src/HOL/List.thy Sun Oct 21 17:04:13 2012 +0200
@@ -160,6 +160,13 @@
-- {*Warning: simpset does not contain this definition, but separate
theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
+primrec
+ product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
+ "product [] _ = []"
+ | "product (x#xs) ys = map (Pair x) ys @ product xs ys"
+
+hide_const (open) product
+
primrec
upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
upt_0: "[i..<0] = []"
@@ -228,6 +235,18 @@
sublist :: "'a list => nat set => 'a list" where
"sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
+primrec
+ sublists :: "'a list \<Rightarrow> 'a list list" where
+ "sublists [] = [[]]"
+| "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
+
+primrec
+ n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
+ "n_lists 0 xs = [[]]"
+| "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
+
+hide_const (open) n_lists
+
fun splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"splice [] ys = ys" |
"splice xs [] = xs" |
@@ -253,6 +272,7 @@
@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
@{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
@{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
+@{lemma "List.product [a,b] [c,d] = [(a, c), (a, d), (b, c), (b, d)]" by simp}\\
@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
@{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\
@{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\
@@ -272,6 +292,8 @@
@{lemma "nth [a,b,c,d] 2 = c" by simp}\\
@{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
@{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
+@{lemma "sublists [a,b] = [[a, b], [a], [b], []]" by simp}\\
+@{lemma "List.n_lists 2 [a,b,c] = [[a, a], [b, a], [c, a], [a, b], [b, b], [c, b], [a, c], [b, c], [c, c]]" by (simp add: eval_nat_numeral)}\\
@{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by simp}\\
@{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\
@{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
@@ -490,6 +512,7 @@
hide_const (open) coset
+
subsubsection {* @{const Nil} and @{const Cons} *}
lemma not_Cons_self [simp]:
@@ -527,6 +550,7 @@
lemma inj_split_Cons: "inj_on (\<lambda>(xs, n). n#xs) X"
by (auto intro!: inj_onI)
+
subsubsection {* @{const length} *}
text {*
@@ -788,7 +812,7 @@
*}
-subsubsection {* @{text map} *}
+subsubsection {* @{const map} *}
lemma hd_map:
"xs \<noteq> [] \<Longrightarrow> hd (map f xs) = f (hd xs)"
@@ -917,9 +941,10 @@
enriched_type map: map
by (simp_all add: id_def)
-declare map.id[simp]
-
-subsubsection {* @{text rev} *}
+declare map.id [simp]
+
+
+subsubsection {* @{const rev} *}
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"
by (induct xs) auto
@@ -966,7 +991,7 @@
by(rule rev_cases[of xs]) auto
-subsubsection {* @{text set} *}
+subsubsection {* @{const set} *}
declare set.simps [code_post] --"pretty output"
@@ -1128,7 +1153,7 @@
by (induct xs) auto
-subsubsection {* @{text filter} *}
+subsubsection {* @{const filter} *}
lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
by (induct xs) auto
@@ -1310,7 +1335,7 @@
declare partition.simps[simp del]
-subsubsection {* @{text concat} *}
+subsubsection {* @{const concat} *}
lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
by (induct xs) auto
@@ -1346,7 +1371,7 @@
by (simp add: concat_eq_concat_iff)
-subsubsection {* @{text nth} *}
+subsubsection {* @{const nth} *}
lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"
by auto
@@ -1458,7 +1483,7 @@
qed
-subsubsection {* @{text list_update} *}
+subsubsection {* @{const list_update} *}
lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"
by (induct xs arbitrary: i) (auto split: nat.split)
@@ -1548,7 +1573,7 @@
by simp_all
-subsubsection {* @{text last} and @{text butlast} *}
+subsubsection {* @{const last} and @{const butlast} *}
lemma last_snoc [simp]: "last (xs @ [x]) = x"
by (induct xs) auto
@@ -1650,7 +1675,7 @@
by (metis append_butlast_last_id append_is_Nil_conv butlast_snoc last_snoc not_Cons_self)
-subsubsection {* @{text take} and @{text drop} *}
+subsubsection {* @{const take} and @{const drop} *}
lemma take_0 [simp]: "take 0 xs = []"
by (induct xs) auto
@@ -1904,7 +1929,7 @@
done
-subsubsection {* @{text takeWhile} and @{text dropWhile} *}
+subsubsection {* @{const takeWhile} and @{const dropWhile} *}
lemma length_takeWhile_le: "length (takeWhile P xs) \<le> length xs"
by (induct xs) auto
@@ -2068,7 +2093,7 @@
by (induct k arbitrary: l, simp_all)
-subsubsection {* @{text zip} *}
+subsubsection {* @{const zip} *}
lemma zip_Nil [simp]: "zip [] ys = []"
by (induct ys) auto
@@ -2230,7 +2255,7 @@
by (auto simp add: zip_map_fst_snd)
-subsubsection {* @{text list_all2} *}
+subsubsection {* @{const list_all2} *}
lemma list_all2_lengthD [intro?]:
"list_all2 P xs ys ==> length xs = length ys"
@@ -2387,6 +2412,13 @@
by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
+subsubsection {* @{const List.product} *}
+
+lemma product_list_set:
+ "set (List.product xs ys) = set xs \<times> set ys"
+ by (induct xs) auto
+
+
subsubsection {* @{const fold} with natural argument order *}
lemma fold_simps [code]: -- {* eta-expanded variant for generated code -- enables tail-recursion optimisation in Scala *}
@@ -2613,6 +2645,7 @@
declare SUP_set_fold [code]
+
subsubsection {* Fold variants: @{const foldr} and @{const foldl} *}
text {* Correspondence *}
@@ -2667,7 +2700,7 @@
by (simp add: fold_append_concat_rev foldr_conv_fold)
-subsubsection {* @{text upt} *}
+subsubsection {* @{const upt} *}
lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
-- {* simp does not terminate! *}
@@ -2830,7 +2863,7 @@
qed
-subsubsection {* @{text "distinct"} and @{text remdups} *}
+subsubsection {* @{const distinct} and @{const remdups} *}
lemma distinct_tl:
"distinct xs \<Longrightarrow> distinct (tl xs)"
@@ -2885,7 +2918,6 @@
"distinct(map f xs) = (distinct xs & inj_on f (set xs))"
by (induct xs) auto
-
lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
by (induct xs) auto
@@ -3020,6 +3052,12 @@
qed
qed (auto simp: dec_def)
+lemma distinct_product:
+ assumes "distinct xs" and "distinct ys"
+ shows "distinct (List.product xs ys)"
+ using assms by (induct xs)
+ (auto intro: inj_onI simp add: product_list_set distinct_map)
+
lemma length_remdups_concat:
"length (remdups (concat xss)) = card (\<Union>xs\<in>set xss. set xs)"
by (simp add: distinct_card [symmetric])
@@ -3083,6 +3121,7 @@
"distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))"
by (metis distinct.simps(2) hd.simps hd_in_set list.simps(2) set_ConsD set_rev_mp set_subset_Cons)
+
subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
lemma (in monoid_add) listsum_simps [simp]:
@@ -3342,7 +3381,7 @@
using assms by (induct xs) simp_all
-subsubsection {* @{text removeAll} *}
+subsubsection {* @{const removeAll} *}
lemma removeAll_filter_not_eq:
"removeAll x = filter (\<lambda>y. x \<noteq> y)"
@@ -3388,7 +3427,7 @@
by(metis map_removeAll_inj_on subset_inj_on subset_UNIV)
-subsubsection {* @{text replicate} *}
+subsubsection {* @{const replicate} *}
lemma length_replicate [simp]: "length (replicate n x) = n"
by (induct n) auto
@@ -3578,7 +3617,7 @@
qed
-subsubsection{*@{text rotate1} and @{text rotate}*}
+subsubsection {* @{const rotate1} and @{const rotate} *}
lemma rotate0[simp]: "rotate 0 = id"
by(simp add:rotate_def)
@@ -3672,7 +3711,7 @@
using mod_less_divisor[of "length xs" n] by arith
-subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
+subsubsection {* @{const sublist} --- a generalization of @{const nth} to sets *}
lemma sublist_empty [simp]: "sublist xs {} = []"
by (auto simp add: sublist_def)
@@ -3755,6 +3794,82 @@
qed
+subsubsection {* @{const sublists} and @{const List.n_lists} *}
+
+lemma length_sublists:
+ "length (sublists xs) = 2 ^ length xs"
+ by (induct xs) (simp_all add: Let_def)
+
+lemma sublists_powset:
+ "set ` set (sublists xs) = Pow (set xs)"
+proof -
+ have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
+ by (auto simp add: image_def)
+ have "set (map set (sublists xs)) = Pow (set xs)"
+ by (induct xs)
+ (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
+ then show ?thesis by simp
+qed
+
+lemma distinct_set_sublists:
+ assumes "distinct xs"
+ shows "distinct (map set (sublists xs))"
+proof (rule card_distinct)
+ have "finite (set xs)" by rule
+ then have "card (Pow (set xs)) = 2 ^ card (set xs)" by (rule card_Pow)
+ with assms distinct_card [of xs]
+ have "card (Pow (set xs)) = 2 ^ length xs" by simp
+ then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
+ by (simp add: sublists_powset length_sublists)
+qed
+
+lemma n_lists_Nil [simp]: "List.n_lists n [] = (if n = 0 then [[]] else [])"
+ by (induct n) simp_all
+
+lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n"
+ by (induct n) (auto simp add: length_concat o_def listsum_triv)
+
+lemma length_n_lists_elem: "ys \<in> set (List.n_lists n xs) \<Longrightarrow> length ys = n"
+ by (induct n arbitrary: ys) auto
+
+lemma set_n_lists: "set (List.n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}"
+proof (rule set_eqI)
+ fix ys :: "'a list"
+ show "ys \<in> set (List.n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
+ proof -
+ have "ys \<in> set (List.n_lists n xs) \<Longrightarrow> length ys = n"
+ by (induct n arbitrary: ys) auto
+ moreover have "\<And>x. ys \<in> set (List.n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs"
+ by (induct n arbitrary: ys) auto
+ moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (List.n_lists (length ys) xs)"
+ by (induct ys) auto
+ ultimately show ?thesis by auto
+ qed
+qed
+
+lemma distinct_n_lists:
+ assumes "distinct xs"
+ shows "distinct (List.n_lists n xs)"
+proof (rule card_distinct)
+ from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
+ have "card (set (List.n_lists n xs)) = card (set xs) ^ n"
+ proof (induct n)
+ case 0 then show ?case by simp
+ next
+ case (Suc n)
+ moreover have "card (\<Union>ys\<in>set (List.n_lists n xs). (\<lambda>y. y # ys) ` set xs)
+ = (\<Sum>ys\<in>set (List.n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
+ by (rule card_UN_disjoint) auto
+ moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
+ by (rule card_image) (simp add: inj_on_def)
+ ultimately show ?case by auto
+ qed
+ also have "\<dots> = length xs ^ n" by (simp add: card_length)
+ finally show "card (set (List.n_lists n xs)) = length (List.n_lists n xs)"
+ by (simp add: length_n_lists)
+qed
+
+
subsubsection {* @{const splice} *}
lemma splice_Nil2 [simp, code]: "splice xs [] = xs"
@@ -5319,6 +5434,15 @@
"xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
by (simp add: list_ex_iff)
+definition can_select :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
+where
+ [code_abbrev]: "can_select P A = (\<exists>!x\<in>A. P x)"
+
+lemma can_select_set_list_ex1 [code]:
+ "can_select P (set A) = list_ex1 P A"
+ by (simp add: list_ex1_iff can_select_def)
+
+
text {* Executable checks for relations on sets *}
definition listrel1p :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
@@ -5531,6 +5655,7 @@
hide_const (open) member null maps map_filter all_interval_nat all_interval_int gen_length
+
subsubsection {* Pretty lists *}
ML_file "Tools/list_code.ML"
@@ -5698,6 +5823,7 @@
hide_const (open) map_project
+
text {* Operations on relations *}
lemma product_code [code]:
--- a/src/HOL/Quickcheck_Exhaustive.thy Fri Oct 19 15:12:52 2012 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy Sun Oct 21 17:04:13 2012 +0200
@@ -234,7 +234,7 @@
"enum_term_of_fun = (%_ _. let
enum_term_of_a = enum_term_of (TYPE('a));
mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a
- in map (%ys. mk_term (%_. ys) ()) (Enum.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
+ in map (%ys. mk_term (%_. ys) ()) (List.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
instance ..
@@ -308,7 +308,7 @@
definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
where
"enum_term_of_prod = (%_ _. map (%(x, y). termify_pair TYPE('a) TYPE('b) x y)
- (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
+ (List.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
instance ..
--- a/src/HOL/String.thy Fri Oct 19 15:12:52 2012 +0200
+++ b/src/HOL/String.thy Sun Oct 21 17:04:13 2012 +0200
@@ -149,6 +149,14 @@
Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
+lemma UNIV_set_chars:
+ "UNIV = set chars"
+ by (simp only: UNIV_char UNIV_nibble) code_simp
+
+lemma distinct_chars:
+ "distinct chars"
+ by code_simp
+
subsection {* Strings as dedicated type *}
@@ -213,3 +221,4 @@
hide_type (open) literal
end
+
--- a/src/HOL/Sum_Type.thy Fri Oct 19 15:12:52 2012 +0200
+++ b/src/HOL/Sum_Type.thy Sun Oct 21 17:04:13 2012 +0200
@@ -209,8 +209,19 @@
show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto
qed
+lemma UNIV_sum:
+ "UNIV = Inl ` UNIV \<union> Inr ` UNIV"
+proof -
+ { fix x :: "'a + 'b"
+ assume "x \<notin> range Inr"
+ then have "x \<in> range Inl"
+ by (cases x) simp_all
+ } then show ?thesis by auto
+qed
+
hide_const (open) Suml Sumr Projl Projr
hide_const (open) sum
end
+
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Oct 19 15:12:52 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Oct 21 17:04:13 2012 +0200
@@ -819,7 +819,7 @@
val t1 = try_metis s1 s0 ()
val t2 = try_metis s2 (SOME s1) ()
val timeout =
- t1 + t2 |> Time.toReal |> curry Real.* merge_timeout_slack
+ Time.+ (t1, t2) |> Time.toReal |> curry Real.* merge_timeout_slack
|> Time.fromReal
in
(TimeLimit.timeLimit timeout (try_metis s12 s0) ();
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Fri Oct 19 15:12:52 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Sun Oct 21 17:04:13 2012 +0200
@@ -95,8 +95,8 @@
fun strip [] qs vs t = (t, rev vs, qs)
| strip (p :: ps) qs vs (Const ("Product_Type.prod.prod_case", _) $ t) =
strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) vs t
- | strip (p :: ps) qs vs (Abs (s, T, t)) = strip ps qs ((s, T) :: vs) t
- | strip (p :: ps) qs vs t = strip ps qs
+ | strip (_ :: ps) qs vs (Abs (s, T, t)) = strip ps qs ((s, T) :: vs) t
+ | strip (_ :: ps) qs vs t = strip ps qs
((Name.uu_, hd (binder_types (fastype_of1 (map snd vs, t)))) :: vs)
(incr_boundvars 1 t $ Bound 0)
in strip [[]] [] [] end;
@@ -206,7 +206,7 @@
val unused_bounds = subtract (op =) (distinct (op =) (maps loose_bnos conjs'))
(0 upto (length vs - 1))
val (pats, fm) =
- mk_formula vs (foldr1 HOLogic.mk_conj (conjs' @ map mk_mem_UNIV unused_bounds))
+ mk_formula ((x, T) :: vs) (foldr1 HOLogic.mk_conj (conjs' @ map mk_mem_UNIV unused_bounds))
fun mk_set (Atom pt) = (case map (lookup pt) pats of [t'] => t' | ts => foldr1 mk_sigma ts)
| mk_set (Un (f1, f2)) = mk_sup (mk_set f1, mk_set f2)
| mk_set (Int (f1, f2)) = mk_inf (mk_set f1, mk_set f2)
@@ -235,9 +235,13 @@
Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
| _ => raise CTERM ("eq_conv", [ct]))
+val vimageI2' = @{lemma "f a \<notin> A ==> a \<notin> f -` A" by simp}
+val vimageE' =
+ @{lemma "a \<notin> f -` B ==> (\<And> x. f a = x ==> x \<notin> B ==> P) ==> P" by simp}
+
val elim_Collect_tac = dtac @{thm iffD1[OF mem_Collect_eq]}
THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE}))
- THEN' TRY o etac @{thm conjE}
+ THEN' REPEAT_DETERM o etac @{thm conjE}
THEN' TRY o hyp_subst_tac;
fun intro_image_tac ctxt = rtac @{thm image_eqI}
@@ -264,7 +268,7 @@
THEN' tac1_of_formula fm2
| tac1_of_formula (Atom _) =
REPEAT_DETERM1 o (rtac @{thm SigmaI}
- ORELSE' (rtac @{thm vimageI2} THEN'
+ ORELSE' ((rtac @{thm vimageI2} ORELSE' rtac vimageI2') THEN'
TRY o Simplifier.simp_tac (HOL_basic_ss addsimps [@{thm prod.cases}]))
ORELSE' rtac @{thm UNIV_I}
ORELSE' rtac @{thm iffD2[OF Compl_iff]}
@@ -284,10 +288,10 @@
TRY o REPEAT_DETERM1 o
(dtac @{thm iffD1[OF mem_Sigma_iff]}
ORELSE' etac @{thm conjE}
- ORELSE' (etac @{thm vimageE}
+ ORELSE' etac @{thm ComplE}
+ ORELSE' ((etac @{thm vimageE} ORELSE' etac vimageE')
THEN' TRY o Simplifier.full_simp_tac (HOL_basic_ss addsimps [@{thm prod.cases}])
THEN' TRY o hyp_subst_tac)
- ORELSE' etac @{thm ComplE}
ORELSE' atac)
fun tac ctxt fm =
@@ -312,8 +316,9 @@
(* preprocessing conversion:
rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} *)
-fun comprehension_conv ctxt ct =
+fun comprehension_conv ss ct =
let
+ val ctxt = Simplifier.the_context ss
fun dest_Collect (Const (@{const_name Collect}, T) $ t) = (HOLogic.dest_setT (body_type T), t)
| dest_Collect t = raise TERM ("dest_Collect", [t])
fun list_ex vs t = fold_rev (fn (x, T) => fn t => HOLogic.exists_const T $ Abs (x, T, t)) vs t
@@ -329,56 +334,64 @@
in
HOLogic.Collect_const T $ absdummy T (list_ex vs (HOLogic.mk_conj (eq, t'')))
end;
- val tac =
+ val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.cases}
+ fun is_eq th = is_some (try (HOLogic.dest_eq o HOLogic.dest_Trueprop) (prop_of th))
+ fun tac ctxt =
rtac @{thm set_eqI}
THEN' Simplifier.simp_tac
- (HOL_basic_ss addsimps [@{thm split_paired_all}, @{thm mem_Collect_eq}, @{thm prod.cases}])
+ (Simplifier.inherit_context ss (HOL_basic_ss addsimps unfold_thms))
THEN' rtac @{thm iffI}
THEN' REPEAT_DETERM o rtac @{thm exI}
THEN' rtac @{thm conjI} THEN' rtac @{thm refl} THEN' atac
THEN' REPEAT_DETERM o etac @{thm exE}
THEN' etac @{thm conjE}
THEN' REPEAT_DETERM o etac @{thm Pair_inject}
- THEN' hyp_subst_tac
- THEN' (atac ORELSE' rtac @{thm refl})
+ THEN' Subgoal.FOCUS (fn {prems, ...} =>
+ Simplifier.simp_tac
+ (Simplifier.inherit_context ss (HOL_basic_ss addsimps (filter is_eq prems))) 1) ctxt
+ THEN' TRY o atac
in
case try mk_term (term_of ct) of
NONE => Thm.reflexive ct
| SOME t' =>
- Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (term_of ct, t'))) (K (tac 1))
- RS @{thm eq_reflection}
+ Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (term_of ct, t')))
+ (fn {context, ...} => tac context 1)
+ RS @{thm eq_reflection}
end
(* main simprocs *)
-val prep_thms = map mk_meta_eq [@{thm Bex_def}, @{thm Pow_iff[symmetric]}]
+val prep_thms =
+ map mk_meta_eq ([@{thm Bex_def}, @{thm Pow_iff[symmetric]}] @ @{thms ex_simps[symmetric]})
val post_thms =
map mk_meta_eq [@{thm Times_Un_distrib1[symmetric]},
@{lemma "A \<times> B \<union> A \<times> C = A \<times> (B \<union> C)" by auto},
@{lemma "(A \<times> B \<inter> C \<times> D) = (A \<inter> C) \<times> (B \<inter> D)" by auto}]
-fun conv ctxt t =
+fun conv ss t =
let
+ val ctxt = Simplifier.the_context ss
val ct = cterm_of (Proof_Context.theory_of ctxt) t
- val prep_eq = (comprehension_conv ctxt then_conv Raw_Simplifier.rewrite true prep_thms) ct
+ fun unfold_conv thms =
+ Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
+ (Raw_Simplifier.inherit_context ss empty_ss addsimps thms)
+ val prep_eq = (comprehension_conv ss then_conv unfold_conv prep_thms) ct
val t' = term_of (Thm.rhs_of prep_eq)
fun mk_thm (fm, t'') = Goal.prove ctxt [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq (t', t''))) (fn {context, ...} => tac context fm 1)
fun unfold th = th RS ((prep_eq RS meta_eq_to_obj_eq) RS @{thm trans})
- fun post th = Conv.fconv_rule (Trueprop_conv (eq_conv Conv.all_conv
- (Raw_Simplifier.rewrite true post_thms))) th
+ val post = Conv.fconv_rule (Trueprop_conv (eq_conv Conv.all_conv (unfold_conv post_thms)))
in
Option.map (post o unfold o mk_thm) (rewrite_term t')
end;
fun base_simproc ss redex =
let
- val ctxt = Simplifier.the_context ss
val set_compr = term_of redex
in
- conv ctxt set_compr
+ conv ss set_compr
|> Option.map (fn thm => thm RS @{thm eq_reflection})
end;
@@ -397,7 +410,7 @@
val pred $ set_compr = term_of redex
val arg_cong' = instantiate_arg_cong ctxt pred
in
- conv ctxt set_compr
+ conv ss set_compr
|> Option.map (fn thm => thm RS arg_cong' RS @{thm eq_reflection})
end;
--- a/src/HOL/Wellfounded.thy Fri Oct 19 15:12:52 2012 +0200
+++ b/src/HOL/Wellfounded.thy Sun Oct 21 17:04:13 2012 +0200
@@ -764,9 +764,9 @@
with Mw show "?N2 \<in> ?W" by (simp only:)
next
assume "M \<noteq> {}"
- have N2: "(?N2, M) \<in> max_ext r"
- by (rule max_extI[OF _ _ `M \<noteq> {}`]) (insert asm1, auto intro: finites)
-
+ from asm1 finites have N2: "(?N2, M) \<in> max_ext r"
+ by (rule_tac max_extI[OF _ _ `M \<noteq> {}`]) auto
+
with `M \<in> ?W` show "?N2 \<in> ?W" by (rule acc_downward)
qed
with finites have "?N1 \<union> ?N2 \<in> ?W"
--- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Fri Oct 19 15:12:52 2012 +0200
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Sun Oct 21 17:04:13 2012 +0200
@@ -125,6 +125,12 @@
where
"common_subsets S1 S2 = {S. S \<subseteq> S1 \<and> S \<subseteq> S2}"
-export_code union common_subsets in Haskell file -
+definition products :: "nat set => nat set => nat set"
+where
+ "products A B = {c. EX a b. a : A & b : B & c = a * b}"
+
+export_code products in Haskell file -
+
+export_code union common_subsets products in Haskell file -
end
--- a/src/Pure/Concurrent/future.ML Fri Oct 19 15:12:52 2012 +0200
+++ b/src/Pure/Concurrent/future.ML Sun Oct 21 17:04:13 2012 +0200
@@ -497,8 +497,6 @@
(* join *)
-local
-
fun get_result x =
(case peek x of
NONE => Exn.Exn (Fail "Unfinished future")
@@ -509,6 +507,8 @@
| SOME exn => Exn.Exn exn)
else res);
+local
+
fun join_next deps = (*requires SYNCHRONIZED*)
if null deps then NONE
else
@@ -561,23 +561,25 @@
else map (fn e => value_result (Exn.interruptible_capture e ())) es;
fun map_future f x =
- let
- val task = task_of x;
- val group = Task_Queue.group_of_task task;
- val (result, job) = future_job group true (fn () => f (join x));
+ if is_finished x then value (f (join x))
+ else
+ let
+ val task = task_of x;
+ val group = Task_Queue.group_of_task task;
+ val (result, job) = future_job group true (fn () => f (join x));
- val extended = SYNCHRONIZED "extend" (fn () =>
- (case Task_Queue.extend task job (! queue) of
- SOME queue' => (queue := queue'; true)
- | NONE => false));
- in
- if extended then Future {promised = false, task = task, result = result}
- else
- (singleton o cond_forks)
- {name = "map_future", group = SOME group, deps = [task],
- pri = Task_Queue.pri_of_task task, interrupts = true}
- (fn () => f (join x))
- end;
+ val extended = SYNCHRONIZED "extend" (fn () =>
+ (case Task_Queue.extend task job (! queue) of
+ SOME queue' => (queue := queue'; true)
+ | NONE => false));
+ in
+ if extended then Future {promised = false, task = task, result = result}
+ else
+ (singleton o cond_forks)
+ {name = "map_future", group = SOME group, deps = [task],
+ pri = Task_Queue.pri_of_task task, interrupts = true}
+ (fn () => f (join x))
+ end;
(* promised futures -- fulfilled by external means *)
--- a/src/Pure/Proof/extraction.ML Fri Oct 19 15:12:52 2012 +0200
+++ b/src/Pure/Proof/extraction.ML Sun Oct 21 17:04:13 2012 +0200
@@ -60,7 +60,7 @@
| _ => nullT))
| typeof_proc _ _ _ = NONE;
-fun rlz_proc (Const ("realizes", Type (_, [Type ("Null", []), _])) $ r $ t) = SOME t
+fun rlz_proc (Const ("realizes", Type (_, [Type ("Null", []), _])) $ _ $ t) = SOME t
| rlz_proc (Const ("realizes", Type (_, [T, _])) $ r $ t) =
(case strip_comb t of
(Var (ixn, U), ts) => SOME (list_comb (Var (ixn, T --> U), r :: ts))
@@ -370,7 +370,6 @@
(rev (Term.add_vars prop' []));
val cs = maps (fn T => map (pair T) S) Ts;
val constraints' = map Logic.mk_of_class cs;
- val cs' = rev (cs @ map (Logic.dest_of_class o snd) constraints);
fun typ_map T = Type.strip_sorts
(map_atyps (fn U => if member (op =) atyps U then atyp_map U else U) T);
fun mk_hyp (T, c) = Hyp (Logic.mk_of_class (typ_map T, c));
@@ -524,40 +523,41 @@
fun realizes_null vs prop = app_rlz_rews [] vs
(Const ("realizes", nullT --> propT --> propT) $ nullt $ prop);
- fun corr d defs vs ts Ts hs cs (PBound i) _ _ = (defs, PBound i)
+ fun corr d vs ts Ts hs cs _ (PBound i) _ defs = (PBound i, defs)
- | corr d defs vs ts Ts hs cs (Abst (s, SOME T, prf)) (Abst (_, _, prf')) t =
- let val (defs', corr_prf) = corr d defs vs [] (T :: Ts)
- (dummyt :: hs) cs prf (Proofterm.incr_pboundvars 1 0 prf')
- (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE)
- in (defs', Abst (s, SOME T, corr_prf)) end
+ | corr d vs ts Ts hs cs t (Abst (s, SOME T, prf)) (Abst (_, _, prf')) defs =
+ let val (corr_prf, defs') = corr d vs [] (T :: Ts)
+ (dummyt :: hs) cs (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE)
+ prf (Proofterm.incr_pboundvars 1 0 prf') defs
+ in (Abst (s, SOME T, corr_prf), defs') end
- | corr d defs vs ts Ts hs cs (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) t =
+ | corr d vs ts Ts hs cs t (AbsP (s, SOME prop, prf)) (AbsP (_, _, prf')) defs =
let
val T = etype_of thy' vs Ts prop;
val u = if T = nullT then
(case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE)
else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE);
- val (defs', corr_prf) =
- corr d defs vs [] (T :: Ts) (prop :: hs)
- (prop :: cs) (Proofterm.incr_pboundvars 0 1 prf)
- (Proofterm.incr_pboundvars 0 1 prf') u;
+ val (corr_prf, defs') =
+ corr d vs [] (T :: Ts) (prop :: hs)
+ (prop :: cs) u (Proofterm.incr_pboundvars 0 1 prf)
+ (Proofterm.incr_pboundvars 0 1 prf') defs;
val rlz = Const ("realizes", T --> propT --> propT)
- in (defs',
+ in (
if T = nullT then AbsP ("R",
SOME (app_rlz_rews Ts vs (rlz $ nullt $ prop)),
Proofterm.prf_subst_bounds [nullt] corr_prf)
else Abst (s, SOME T, AbsP ("R",
SOME (app_rlz_rews (T :: Ts) vs
- (rlz $ Bound 0 $ incr_boundvars 1 prop)), corr_prf)))
+ (rlz $ Bound 0 $ incr_boundvars 1 prop)), corr_prf)), defs')
end
- | corr d defs vs ts Ts hs cs (prf % SOME t) (prf' % _) t' =
+ | corr d vs ts Ts hs cs t' (prf % SOME t) (prf' % _) defs =
let
val (Us, T) = strip_type (fastype_of1 (Ts, t));
- val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs cs prf prf'
+ val (corr_prf, defs') = corr d vs (t :: ts) Ts hs cs
(if member (op =) rtypes (tname_of T) then t'
- else (case t' of SOME (u $ _) => SOME u | _ => NONE));
+ else (case t' of SOME (u $ _) => SOME u | _ => NONE))
+ prf prf' defs;
val u = if not (member (op =) rtypes (tname_of T)) then t else
let
val eT = etype_of thy' vs Ts t;
@@ -569,26 +569,28 @@
SOME ((_, SOME f)) => f r eT u T
| _ => Const ("realizes", eT --> T --> T) $ r $ u)
in app_rlz_rews Ts vs (fold_rev (Term.abs o pair "x") Us' u') end
- in (defs', corr_prf % SOME u) end
+ in (corr_prf % SOME u, defs') end
- | corr d defs vs ts Ts hs cs (prf1 %% prf2) (prf1' %% prf2') t =
+ | corr d vs ts Ts hs cs t (prf1 %% prf2) (prf1' %% prf2') defs =
let
val prop = Reconstruct.prop_of' hs prf2';
val T = etype_of thy' vs Ts prop;
- val (defs1, f, u) = if T = nullT then (defs, t, NONE) else
+ val (f, u, defs1) = if T = nullT then (t, NONE, defs) else
(case t of
- SOME (f $ u) => (defs, SOME f, SOME u)
+ SOME (f $ u) => (SOME f, SOME u, defs)
| _ =>
- let val (defs1, u) = extr d defs vs [] Ts hs prf2'
- in (defs1, NONE, SOME u) end)
- val (defs2, corr_prf1) = corr d defs1 vs [] Ts hs cs prf1 prf1' f;
- val (defs3, corr_prf2) = corr d defs2 vs [] Ts hs cs prf2 prf2' u;
+ let val (u, defs1) = extr d vs [] Ts hs prf2' defs
+ in (NONE, SOME u, defs1) end)
+ val ((corr_prf1, corr_prf2), defs2) =
+ defs1
+ |> corr d vs [] Ts hs cs f prf1 prf1'
+ ||>> corr d vs [] Ts hs cs u prf2 prf2';
in
- if T = nullT then (defs3, corr_prf1 %% corr_prf2) else
- (defs3, corr_prf1 % u %% corr_prf2)
+ if T = nullT then (corr_prf1 %% corr_prf2, defs2) else
+ (corr_prf1 % u %% corr_prf2, defs2)
end
- | corr d defs vs ts Ts hs cs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
+ | corr d vs ts Ts hs cs _ (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ defs =
let
val prf = Proofterm.join_proof body;
val (vs', tye) = find_inst prop Ts ts vs;
@@ -597,10 +599,10 @@
val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye;
val T = etype_of thy' vs' [] prop;
val defs' = if T = nullT then defs
- else fst (extr d defs vs ts Ts hs prf0)
+ else snd (extr d vs ts Ts hs prf0 defs)
in
- if T = nullT andalso realizes_null vs' prop aconv prop then (defs, prf0)
- else case Symtab.lookup realizers name of
+ if T = nullT andalso realizes_null vs' prop aconv prop then (prf0, defs)
+ else (case Symtab.lookup realizers name of
NONE => (case find vs' (find' name defs') of
NONE =>
let
@@ -609,8 +611,8 @@
(if null vs' then ""
else " (relevant variables: " ^ commas_quote vs' ^ ")"));
val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
- val (defs'', corr_prf0) = corr (d + 1) defs' vs' [] [] []
- (rev shyps) prf' prf' NONE;
+ val (corr_prf0, defs'') = corr (d + 1) vs' [] [] []
+ (rev shyps) NONE prf' prf' defs';
val corr_prf = mkabsp shyps corr_prf0;
val corr_prop = Reconstruct.prop_of corr_prf;
val corr_prf' =
@@ -624,70 +626,69 @@
(map (get_var_type corr_prop) (vfs_of prop)) |>
mkabsp shyps
in
- ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
- Proofterm.proof_combP (prf_subst_TVars tye' corr_prf', sprfs))
+ (Proofterm.proof_combP (prf_subst_TVars tye' corr_prf', sprfs),
+ (name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'')
end
| SOME (_, (_, prf')) =>
- (defs', Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs)))
+ (Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs'))
| SOME rs => (case find vs' rs of
- SOME (_, prf') => (defs', Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs))
+ SOME (_, prf') => (Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs')
| NONE => error ("corr: no realizer for instance of theorem " ^
quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
- (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))))
+ (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))))
end
- | corr d defs vs ts Ts hs cs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
+ | corr d vs ts Ts hs cs _ (prf0 as PAxm (s, prop, SOME Ts')) _ defs =
let
val (vs', tye) = find_inst prop Ts ts vs;
val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
in
if etype_of thy' vs' [] prop = nullT andalso
- realizes_null vs' prop aconv prop then (defs, prf0)
+ realizes_null vs' prop aconv prop then (prf0, defs)
else case find vs' (Symtab.lookup_list realizers s) of
- SOME (_, prf) => (defs,
- Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye))
+ SOME (_, prf) => (Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye),
+ defs)
| NONE => error ("corr: no realizer for instance of axiom " ^
quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
(Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))
end
- | corr d defs vs ts Ts hs _ _ _ _ = error "corr: bad proof"
+ | corr d vs ts Ts hs _ _ _ _ defs = error "corr: bad proof"
- and extr d defs vs ts Ts hs (PBound i) = (defs, Bound i)
+ and extr d vs ts Ts hs (PBound i) defs = (Bound i, defs)
- | extr d defs vs ts Ts hs (Abst (s, SOME T, prf)) =
- let val (defs', t) = extr d defs vs []
- (T :: Ts) (dummyt :: hs) (Proofterm.incr_pboundvars 1 0 prf)
- in (defs', Abs (s, T, t)) end
+ | extr d vs ts Ts hs (Abst (s, SOME T, prf)) defs =
+ let val (t, defs') = extr d vs []
+ (T :: Ts) (dummyt :: hs) (Proofterm.incr_pboundvars 1 0 prf) defs
+ in (Abs (s, T, t), defs') end
- | extr d defs vs ts Ts hs (AbsP (s, SOME t, prf)) =
+ | extr d vs ts Ts hs (AbsP (s, SOME t, prf)) defs =
let
val T = etype_of thy' vs Ts t;
- val (defs', t) =
- extr d defs vs [] (T :: Ts) (t :: hs) (Proofterm.incr_pboundvars 0 1 prf)
- in (defs',
- if T = nullT then subst_bound (nullt, t) else Abs (s, T, t))
+ val (t, defs') =
+ extr d vs [] (T :: Ts) (t :: hs) (Proofterm.incr_pboundvars 0 1 prf) defs
+ in
+ (if T = nullT then subst_bound (nullt, t) else Abs (s, T, t), defs')
end
- | extr d defs vs ts Ts hs (prf % SOME t) =
- let val (defs', u) = extr d defs vs (t :: ts) Ts hs prf
- in (defs',
- if member (op =) rtypes (tname_of (body_type (fastype_of1 (Ts, t)))) then u
- else u $ t)
+ | extr d vs ts Ts hs (prf % SOME t) defs =
+ let val (u, defs') = extr d vs (t :: ts) Ts hs prf defs
+ in (if member (op =) rtypes (tname_of (body_type (fastype_of1 (Ts, t)))) then u
+ else u $ t, defs')
end
- | extr d defs vs ts Ts hs (prf1 %% prf2) =
+ | extr d vs ts Ts hs (prf1 %% prf2) defs =
let
- val (defs', f) = extr d defs vs [] Ts hs prf1;
+ val (f, defs') = extr d vs [] Ts hs prf1 defs;
val prop = Reconstruct.prop_of' hs prf2;
val T = etype_of thy' vs Ts prop
in
- if T = nullT then (defs', f) else
- let val (defs'', t) = extr d defs' vs [] Ts hs prf2
- in (defs'', f $ t) end
+ if T = nullT then (f, defs') else
+ let val (t, defs'') = extr d vs [] Ts hs prf2 defs'
+ in (f $ t, defs'') end
end
- | extr d defs vs ts Ts hs (prf0 as PThm (_, ((s, prop, SOME Ts'), body))) =
+ | extr d vs ts Ts hs (prf0 as PThm (_, ((s, prop, SOME Ts'), body))) defs =
let
val prf = Proofterm.join_proof body;
val (vs', tye) = find_inst prop Ts ts vs;
@@ -702,9 +703,9 @@
(if null vs' then ""
else " (relevant variables: " ^ commas_quote vs' ^ ")"));
val prf' = prep (Reconstruct.reconstruct_proof thy' prop prf);
- val (defs', t) = extr (d + 1) defs vs' [] [] [] prf';
- val (defs'', corr_prf) = corr (d + 1) defs' vs' [] [] []
- (rev shyps) prf' prf' (SOME t);
+ val (t, defs') = extr (d + 1) vs' [] [] [] prf' defs;
+ val (corr_prf, defs'') = corr (d + 1) vs' [] [] []
+ (rev shyps) (SOME t) prf' prf' defs';
val nt = Envir.beta_norm t;
val args = filter_out (fn v => member (op =) rtypes
@@ -742,30 +743,30 @@
(map (get_var_type corr_prop) (vfs_of prop)) |>
mkabsp shyps
in
- ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
- subst_TVars tye' u)
+ (subst_TVars tye' u,
+ (s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'')
end
- | SOME ((_, u), _) => (defs, subst_TVars tye' u))
+ | SOME ((_, u), _) => (subst_TVars tye' u, defs))
| SOME rs => (case find vs' rs of
- SOME (t, _) => (defs, subst_TVars tye' t)
+ SOME (t, _) => (subst_TVars tye' t, defs)
| NONE => error ("extr: no realizer for instance of theorem " ^
quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
(Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))))
end
- | extr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) =
+ | extr d vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) defs =
let
val (vs', tye) = find_inst prop Ts ts vs;
val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
in
case find vs' (Symtab.lookup_list realizers s) of
- SOME (t, _) => (defs, subst_TVars tye' t)
+ SOME (t, _) => (subst_TVars tye' t, defs)
| NONE => error ("extr: no realizer for instance of axiom " ^
quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
(Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))
end
- | extr d defs vs ts Ts hs _ = error "extr: bad proof";
+ | extr d vs ts Ts hs _ defs = error "extr: bad proof";
fun prep_thm (thm, vs) =
let
@@ -779,7 +780,7 @@
in (Reconstruct.reconstruct_proof thy prop prf, vs) end;
val defs =
- fold (fn (prf, vs) => fn defs => fst (extr 0 defs vs [] [] [] prf))
+ fold (fn (prf, vs) => snd o extr 0 vs [] [] [] prf)
(map prep_thm thms) [];
fun add_def (s, (vs, ((t, u), (prf, _)))) thy =
--- a/src/Pure/System/build.scala Fri Oct 19 15:12:52 2012 +0200
+++ b/src/Pure/System/build.scala Sun Oct 21 17:04:13 2012 +0200
@@ -690,7 +690,8 @@
val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
if (rc != 0 && (verbose || !no_build)) {
val unfinished =
- (for ((name, res) <- results.iterator if res.rc != 0) yield name).toList.sorted
+ (for ((name, res) <- results.iterator if res.rc != 0) yield name).toList
+ .sorted(scala.math.Ordering.String) // FIXME scala-2.10.0-RC1
echo("Unfinished session(s): " + commas(unfinished))
}
rc
--- a/src/Pure/System/options.scala Fri Oct 19 15:12:52 2012 +0200
+++ b/src/Pure/System/options.scala Sun Oct 21 17:04:13 2012 +0200
@@ -198,32 +198,36 @@
/* internal lookup and update */
- val bool = new Object
+ class Bool_Access
{
def apply(name: String): Boolean = get(name, Options.Bool, Properties.Value.Boolean.unapply)
def update(name: String, x: Boolean): Options =
put(name, Options.Bool, Properties.Value.Boolean(x))
}
+ val bool = new Bool_Access
- val int = new Object
+ class Int_Access
{
def apply(name: String): Int = get(name, Options.Int, Properties.Value.Int.unapply)
def update(name: String, x: Int): Options =
put(name, Options.Int, Properties.Value.Int(x))
}
+ val int = new Int_Access
- val real = new Object
+ class Real_Access
{
def apply(name: String): Double = get(name, Options.Real, Properties.Value.Double.unapply)
def update(name: String, x: Double): Options =
put(name, Options.Real, Properties.Value.Double(x))
}
+ val real = new Real_Access
- val string = new Object
+ class String_Access
{
def apply(name: String): String = get(name, Options.String, s => Some(s))
def update(name: String, x: String): Options = put(name, Options.String, x)
}
+ val string = new String_Access
/* external updates */
@@ -363,7 +367,7 @@
options = options + (name, x)
}
- val bool = new Object
+ class Bool_Access
{
def apply(name: String): Boolean = options.bool(name)
def update(name: String, x: Boolean)
@@ -372,8 +376,9 @@
options = options.bool.update(name, x)
}
}
+ val bool = new Bool_Access
- val int = new Object
+ class Int_Access
{
def apply(name: String): Int = options.int(name)
def update(name: String, x: Int)
@@ -382,8 +387,9 @@
options = options.int.update(name, x)
}
}
+ val int = new Int_Access
- val real = new Object
+ class Real_Access
{
def apply(name: String): Double = options.real(name)
def update(name: String, x: Double)
@@ -392,8 +398,9 @@
options = options.real.update(name, x)
}
}
+ val real = new Real_Access
- val string = new Object
+ class String_Access
{
def apply(name: String): String = options.string(name)
def update(name: String, x: String)
@@ -402,5 +409,6 @@
options = options.string.update(name, x)
}
}
+ val string = new String_Access
}
--- a/src/Pure/build-jars Fri Oct 19 15:12:52 2012 +0200
+++ b/src/Pure/build-jars Sun Oct 21 17:04:13 2012 +0200
@@ -211,6 +211,9 @@
[ -e "$SCALA_HOME/lib/scala-actors.jar" ] && \
cp "$SCALA_HOME/lib/scala-actors.jar" "$TARGET_DIR/ext"
+ [ -e "$SCALA_HOME/lib/scala-reflect.jar" ] && \
+ cp "$SCALA_HOME/lib/scala-reflect.jar" "$TARGET_DIR/ext"
+
popd >/dev/null
rm -rf classes
--- a/src/Tools/Graphview/src/graph_panel.scala Fri Oct 19 15:12:52 2012 +0200
+++ b/src/Tools/Graphview/src/graph_panel.scala Sun Oct 21 17:04:13 2012 +0200
@@ -67,7 +67,7 @@
def apply_layout() = visualizer.Coordinates.layout()
- private val paint_panel = new Panel {
+ private class Paint_Panel extends Panel {
def set_preferred_size() {
val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds()
val s = Transform.scale
@@ -86,6 +86,7 @@
visualizer.Drawer.paint_all_visible(g, true)
}
}
+ private val paint_panel = new Paint_Panel
contents = paint_panel
listenTo(keys)
--- a/src/Tools/jEdit/README.html Fri Oct 19 15:12:52 2012 +0200
+++ b/src/Tools/jEdit/README.html Sun Oct 21 17:04:13 2012 +0200
@@ -5,7 +5,7 @@
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<style type="text/css" media="screen">
-body { font-family: STIXGeneral, IsabelleText; font-size: 14pt; }
+body { font-family: IsabelleText; font-size: 14pt; }
</style>
<title>Welcome to the Isabelle/jEdit Prover IDE</title>
</head>
--- a/src/Tools/jEdit/README_BUILD Fri Oct 19 15:12:52 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-Requirements for instantaneous build from repository
-====================================================
-
-* Java JDK 1.7 from Oracle
- http://www.oracle.com/technetwork/java/javase/downloads/index.html
-
- (experimental support for JDK/OpenJDK 1.7)
-
-* Scala 2.9.2
- http://www.scala-lang.org
-
- (experimental support for Scala 2.10.x milestones)
-
- Note that the official directory layout of JDK and Scala is required!
-
-* Auxiliary jedit_build component according to Admin/components/main
-
-
-Build and run
-=============
-
-isabelle jedit -l HOL Test.thy
-
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Oct 19 15:12:52 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Sun Oct 21 17:04:13 2012 +0200
@@ -92,7 +92,6 @@
BUILD_ONLY=false
BUILD_JARS="jars"
-FRESH_OPTION=""
JEDIT_SESSION_DIRS=""
JEDIT_LOGIC="$ISABELLE_LOGIC"
JEDIT_PRINT_MODE=""
@@ -117,7 +116,6 @@
fi
;;
f)
- FRESH_OPTION="-f"
BUILD_JARS="jars_fresh"
;;
j)
@@ -166,11 +164,14 @@
## dependencies
-[ -e "$ISABELLE_HOME/Admin/build" ] && \
- {
+if [ -e "$ISABELLE_HOME/Admin/build" ]; then
+ if [ "$BUILD_JARS" = jars_fresh ]; then
+ "$ISABELLE_TOOL" graphview -b -f || exit $?
+ else
"$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?
- "$ISABELLE_TOOL" graphview -b $FRESH_OPTION || exit $?
- }
+ "$ISABELLE_TOOL" graphview -b || exit $?
+ fi
+fi
PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar"
GRAPHVIEW_JAR="$ISABELLE_HOME/lib/classes/ext/Graphview.jar"
--- a/src/Tools/jEdit/src/jedit_lib.scala Fri Oct 19 15:12:52 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala Sun Oct 21 17:04:13 2012 +0200
@@ -168,5 +168,17 @@
Some(new Gfx_Range(p.x, p.y, q.x + r - p.x))
else None
}
+
+
+ /* pixel range */
+
+ def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
+ {
+ val range = point_range(text_area.getBuffer, text_area.xyToOffset(x, y))
+ gfx_range(text_area, range) match {
+ case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
+ case _ => None
+ }
+ }
}
--- a/src/Tools/jEdit/src/rich_text_area.scala Fri Oct 19 15:12:52 2012 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Sun Oct 21 17:04:13 2012 +0200
@@ -173,14 +173,16 @@
if ((control || hovering) && !buffer.isLoading) {
JEdit_Lib.buffer_lock(buffer) {
- val rendering = get_rendering()
- val mouse_offset = text_area.xyToOffset(e.getX(), e.getY())
- val mouse_range = JEdit_Lib.point_range(buffer, mouse_offset)
- for ((area, require_control) <- active_areas)
- {
- if (control == require_control)
- area.update_rendering(rendering, mouse_range)
- else area.reset
+ JEdit_Lib.pixel_range(text_area, e.getX(), e.getY()) match {
+ case None =>
+ case Some(range) =>
+ val rendering = get_rendering()
+ for ((area, require_control) <- active_areas)
+ {
+ if (control == require_control)
+ area.update_rendering(rendering, range)
+ else area.reset
+ }
}
}
}
@@ -200,15 +202,17 @@
val rendering = get_rendering()
val snapshot = rendering.snapshot
if (!snapshot.is_outdated) {
- val offset = text_area.xyToOffset(x, y)
- val range = Text.Range(offset, offset + 1)
- val tip =
- if (control) rendering.tooltip(range)
- else rendering.tooltip_message(range)
- if (!tip.isEmpty) {
- val painter = text_area.getPainter
- val y1 = y + painter.getFontMetrics.getHeight / 2
- new Pretty_Tooltip(view, painter, rendering, x, y1, tip)
+ JEdit_Lib.pixel_range(text_area, x, y) match {
+ case None =>
+ case Some(range) =>
+ val tip =
+ if (control) rendering.tooltip(range)
+ else rendering.tooltip_message(range)
+ if (!tip.isEmpty) {
+ val painter = text_area.getPainter
+ val y1 = y + painter.getFontMetrics.getHeight / 2
+ new Pretty_Tooltip(view, painter, rendering, x, y1, tip)
+ }
}
}
null