--- a/src/Doc/System/Sessions.thy Thu Apr 06 10:21:45 2017 +0200
+++ b/src/Doc/System/Sessions.thy Thu Apr 06 10:22:03 2017 +0200
@@ -70,7 +70,9 @@
;
value: @{syntax name} | @{syntax real}
;
- theories: @'theories' opts? ( @{syntax name} * )
+ theory_entry: @{syntax name} ('(' @'global' ')')?
+ ;
+ theories: @'theories' opts? (theory_entry*)
;
files: @'files' (@{syntax name}+)
;
@@ -116,6 +118,11 @@
of \isakeyword{theories} may be given. Options are only active for each
\isakeyword{theories} block separately.
+ A theory name that is followed by \<open>(\<close>\isakeyword{global}\<open>)\<close> is treated
+ literally in other session specifications or theory imports. In contrast,
+ the default is to qualify theory names by the session name, in order to
+ ensure globally unique names in big session trees.
+
\<^descr> \isakeyword{files}~\<open>files\<close> lists additional source files that are involved
in the processing of this session. This should cover anything outside the
formal content of the theory sources. In contrast, files that are loaded
--- a/src/FOL/ROOT Thu Apr 06 10:21:45 2017 +0200
+++ b/src/FOL/ROOT Thu Apr 06 10:22:03 2017 +0200
@@ -15,9 +15,9 @@
Michael Dummett, Elements of Intuitionism (Oxford, 1977)
*}
- global_theories
- IFOL
- FOL
+ theories
+ IFOL (global)
+ FOL (global)
document_files "root.tex"
session "FOL-ex" in ex = FOL +
--- a/src/HOL/HOLCF/Bifinite.thy Thu Apr 06 10:21:45 2017 +0200
+++ b/src/HOL/HOLCF/Bifinite.thy Thu Apr 06 10:22:03 2017 +0200
@@ -5,7 +5,7 @@
section \<open>Profinite and bifinite cpos\<close>
theory Bifinite
-imports Map_Functions "~~/src/HOL/Library/Countable"
+imports Map_Functions Cprod Sprod Sfun Up "~~/src/HOL/Library/Countable"
begin
default_sort cpo
--- a/src/HOL/HOLCF/Completion.thy Thu Apr 06 10:21:45 2017 +0200
+++ b/src/HOL/HOLCF/Completion.thy Thu Apr 06 10:22:03 2017 +0200
@@ -5,7 +5,7 @@
section \<open>Defining algebraic domains by ideal completion\<close>
theory Completion
-imports Plain_HOLCF
+imports Cfun
begin
subsection \<open>Ideals over a preorder\<close>
@@ -137,8 +137,11 @@
lemma is_lub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> x"
by (erule exE, drule is_lub_lub, erule is_lubD2)
+
subsection \<open>Locale for ideal completion\<close>
+hide_const (open) Filter.principal
+
locale ideal_completion = preorder +
fixes principal :: "'a::type \<Rightarrow> 'b::cpo"
fixes rep :: "'b::cpo \<Rightarrow> 'a::type set"
--- a/src/HOL/HOLCF/Deflation.thy Thu Apr 06 10:21:45 2017 +0200
+++ b/src/HOL/HOLCF/Deflation.thy Thu Apr 06 10:22:03 2017 +0200
@@ -5,7 +5,7 @@
section \<open>Continuous deflations and ep-pairs\<close>
theory Deflation
-imports Plain_HOLCF
+imports Cfun
begin
default_sort cpo
--- a/src/HOL/HOLCF/Fixrec.thy Thu Apr 06 10:21:45 2017 +0200
+++ b/src/HOL/HOLCF/Fixrec.thy Thu Apr 06 10:22:03 2017 +0200
@@ -5,7 +5,7 @@
section "Package for defining recursive functions in HOLCF"
theory Fixrec
-imports Plain_HOLCF
+imports Cprod Sprod Ssum Up One Tr Fix
keywords "fixrec" :: thy_decl
begin
@@ -139,7 +139,7 @@
match_TT :: "tr \<rightarrow> 'c match \<rightarrow> 'c match"
where
"match_TT = (\<Lambda> x k. If x then k else fail)"
-
+
definition
match_FF :: "tr \<rightarrow> 'c match \<rightarrow> 'c match"
where
--- a/src/HOL/HOLCF/HOLCF.thy Thu Apr 06 10:21:45 2017 +0200
+++ b/src/HOL/HOLCF/HOLCF.thy Thu Apr 06 10:22:03 2017 +0200
@@ -1,5 +1,6 @@
(* Title: HOL/HOLCF/HOLCF.thy
Author: Franz Regensburger
+ Author: Brian Huffman
HOLCF -- a semantic extension of HOL by the LCF logic.
*)
--- a/src/HOL/HOLCF/Map_Functions.thy Thu Apr 06 10:21:45 2017 +0200
+++ b/src/HOL/HOLCF/Map_Functions.thy Thu Apr 06 10:22:03 2017 +0200
@@ -5,7 +5,7 @@
section \<open>Map functions for various types\<close>
theory Map_Functions
-imports Deflation
+imports Deflation Sprod Ssum Sfun Up
begin
subsection \<open>Map operator for continuous function space\<close>
--- a/src/HOL/HOLCF/Plain_HOLCF.thy Thu Apr 06 10:21:45 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(* Title: HOL/HOLCF/Plain_HOLCF.thy
- Author: Brian Huffman
-*)
-
-section \<open>Plain HOLCF\<close>
-
-theory Plain_HOLCF
-imports Cfun Sfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix
-begin
-
-text \<open>
- Basic HOLCF concepts and types; does not include definition packages.
-\<close>
-
-hide_const (open) Filter.principal
-
-end
--- a/src/HOL/Library/More_List.thy Thu Apr 06 10:21:45 2017 +0200
+++ b/src/HOL/Library/More_List.thy Thu Apr 06 10:22:03 2017 +0200
@@ -39,10 +39,6 @@
"strip_while P (x # xs) = x # strip_while P xs \<longleftrightarrow> \<not> (P x \<and> (\<forall>x\<in>set xs. P x))"
by (induct xs rule: rev_induct) (simp_all add: strip_while_def)
-lemma strip_while_not_last [simp]:
- "\<not> P (last xs) \<Longrightarrow> strip_while P xs = xs"
- by (cases xs rule: rev_cases) simp_all
-
lemma split_strip_while_append:
fixes xs :: "'a list"
obtains ys zs :: "'a list"
@@ -64,6 +60,32 @@
"strip_while P (map f xs) = map f (strip_while (P \<circ> f) xs)"
by (simp add: strip_while_def rev_map dropWhile_map)
+lemma strip_while_dropWhile_commute:
+ "strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)"
+proof (induct xs)
+ case Nil
+ then show ?case
+ by simp
+next
+ case (Cons x xs)
+ show ?case
+ proof (cases "\<forall>y\<in>set xs. P y")
+ case True
+ with dropWhile_append2 [of "rev xs"] show ?thesis
+ by (auto simp add: strip_while_def dest: set_dropWhileD)
+ next
+ case False
+ then obtain y where "y \<in> set xs" and "\<not> P y"
+ by blast
+ with Cons dropWhile_append3 [of P y "rev xs"] show ?thesis
+ by (simp add: strip_while_def)
+ qed
+qed
+
+lemma dropWhile_strip_while_commute:
+ "dropWhile P (strip_while Q xs) = strip_while Q (dropWhile P xs)"
+ by (simp add: strip_while_dropWhile_commute)
+
definition no_leading :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
where
@@ -134,6 +156,10 @@
"no_trailing P (x # xs) \<longleftrightarrow> no_trailing P xs \<and> (xs = [] \<longrightarrow> \<not> P x)"
by simp
+lemma no_trailing_append:
+ "no_trailing P (xs @ ys) \<longleftrightarrow> no_trailing P ys \<and> (ys = [] \<longrightarrow> no_trailing P xs)"
+ by (induct xs) simp_all
+
lemma no_trailing_append_Cons [simp]:
"no_trailing P (xs @ y # ys) \<longleftrightarrow> no_trailing P (y # ys)"
by simp
@@ -142,6 +168,10 @@
"no_trailing P (strip_while P xs)"
by (induct xs rule: rev_induct) simp_all
+lemma strip_while_idem [simp]:
+ "no_trailing P xs \<Longrightarrow> strip_while P xs = xs"
+ by (cases xs rule: rev_cases) simp_all
+
lemma strip_while_eq_obtain_trailing:
assumes "strip_while P xs = ys"
obtains zs where "xs = ys @ zs" and "\<And>z. z \<in> set zs \<Longrightarrow> P z" and "no_trailing P ys"
@@ -172,9 +202,18 @@
qed
lemma no_trailing_map:
- "no_trailing P (map f xs) = no_trailing (P \<circ> f) xs"
+ "no_trailing P (map f xs) \<longleftrightarrow> no_trailing (P \<circ> f) xs"
by (simp add: last_map no_trailing_unfold)
+lemma no_trailing_drop [simp]:
+ "no_trailing P (drop n xs)" if "no_trailing P xs"
+proof -
+ from that have "no_trailing P (take n xs @ drop n xs)"
+ by simp
+ then show ?thesis
+ by (simp only: no_trailing_append)
+qed
+
lemma no_trailing_upt [simp]:
"no_trailing P [n..<m] \<longleftrightarrow> (n < m \<longrightarrow> \<not> P (m - 1))"
by (auto simp add: no_trailing_unfold)
--- a/src/HOL/Library/Polynomial.thy Thu Apr 06 10:21:45 2017 +0200
+++ b/src/HOL/Library/Polynomial.thy Thu Apr 06 10:22:03 2017 +0200
@@ -103,7 +103,8 @@
begin
lift_definition zero_poly :: "'a poly"
- is "\<lambda>_. 0" by (rule MOST_I) simp
+ is "\<lambda>_. 0"
+ by (rule MOST_I) simp
instance ..
@@ -377,11 +378,13 @@
with Cons show ?case by auto
qed
-lemma last_coeffs_not_0: "p \<noteq> 0 \<Longrightarrow> last (coeffs p) \<noteq> 0"
- by (induct p) (auto simp add: cCons_def)
-
-lemma strip_while_coeffs [simp]: "strip_while (HOL.eq 0) (coeffs p) = coeffs p"
- by (cases "p = 0") (auto dest: last_coeffs_not_0 intro: strip_while_not_last)
+lemma no_trailing_coeffs [simp]:
+ "no_trailing (HOL.eq 0) (coeffs p)"
+ by (induct p) auto
+
+lemma strip_while_coeffs [simp]:
+ "strip_while (HOL.eq 0) (coeffs p) = coeffs p"
+ by simp
lemma coeffs_eq_iff: "p = q \<longleftrightarrow> coeffs p = coeffs q"
(is "?P \<longleftrightarrow> ?Q")
@@ -402,11 +405,12 @@
lemma coeffs_eqI:
assumes coeff: "\<And>n. coeff p n = nth_default 0 xs n"
- assumes zero: "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0"
+ assumes zero: "no_trailing (HOL.eq 0) xs"
shows "coeffs p = xs"
proof -
- from coeff have "p = Poly xs" by (simp add: poly_eq_iff)
- with zero show ?thesis by simp (cases xs; simp)
+ from coeff have "p = Poly xs"
+ by (simp add: poly_eq_iff)
+ with zero show ?thesis by simp
qed
lemma degree_eq_length_coeffs [code]: "degree p = length (coeffs p) - 1"
@@ -737,28 +741,26 @@
have *: "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n"
for xs ys :: "'a list" and n
proof (induct xs ys arbitrary: n rule: plus_coeffs.induct)
- case 3
- then show ?case by (cases n) (auto simp: cCons_def)
- qed simp_all
- have **: "last (plus_coeffs xs ys) \<noteq> 0"
- if "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0" and "ys \<noteq> [] \<Longrightarrow> last ys \<noteq> 0" and "plus_coeffs xs ys \<noteq> []"
- for xs ys :: "'a list"
- using that
- proof (induct xs ys rule: plus_coeffs.induct)
- case 3
- then show ?case by (auto simp add: cCons_def) metis
+ case (3 x xs y ys n)
+ then show ?case
+ by (cases n) (auto simp add: cCons_def)
qed simp_all
+ have **: "no_trailing (HOL.eq 0) (plus_coeffs xs ys)"
+ if "no_trailing (HOL.eq 0) xs" and "no_trailing (HOL.eq 0) ys"
+ for xs ys :: "'a list"
+ using that by (induct xs ys rule: plus_coeffs.induct) (simp_all add: cCons_def)
show ?thesis
- apply (rule coeffs_eqI)
- apply (simp add: * nth_default_coeffs_eq)
- apply (rule **)
- apply (auto dest: last_coeffs_not_0)
- done
+ by (rule coeffs_eqI) (auto simp add: * nth_default_coeffs_eq intro: **)
qed
-lemma coeffs_uminus [code abstract]: "coeffs (- p) = map (\<lambda>a. - a) (coeffs p)"
- by (rule coeffs_eqI)
- (simp_all add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq)
+lemma coeffs_uminus [code abstract]:
+ "coeffs (- p) = map uminus (coeffs p)"
+proof -
+ have eq_0: "HOL.eq 0 \<circ> uminus = HOL.eq (0::'a)"
+ by (simp add: fun_eq_iff)
+ show ?thesis
+ by (rule coeffs_eqI) (simp_all add: nth_default_map_eq nth_default_coeffs_eq no_trailing_map eq_0)
+qed
lemma [code]: "p - q = p + - q"
for p q :: "'a::ab_group_add poly"
@@ -885,9 +887,12 @@
lemma coeffs_smult [code abstract]:
"coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))"
for p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
- by (rule coeffs_eqI)
- (auto simp add: not_0_coeffs_not_Nil last_map last_coeffs_not_0
- nth_default_map_eq nth_default_coeffs_eq)
+proof -
+ have eq_0: "HOL.eq 0 \<circ> times a = HOL.eq (0::'a)" if "a \<noteq> 0"
+ using that by (simp add: fun_eq_iff)
+ show ?thesis
+ by (rule coeffs_eqI) (auto simp add: no_trailing_map nth_default_map_eq nth_default_coeffs_eq eq_0)
+qed
lemma smult_eq_iff:
fixes b :: "'a :: field"
@@ -1120,16 +1125,15 @@
"coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))"
by (simp add: map_poly_def)
-lemma set_coeffs_map_poly:
- "(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)"
- by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0)
-
lemma coeffs_map_poly':
assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
shows "coeffs (map_poly f p) = map f (coeffs p)"
- by (cases "p = 0")
- (auto simp: assms coeffs_map_poly last_map last_coeffs_not_0
- intro!: strip_while_not_last split: if_splits)
+ using assms by (simp add: coeffs_map_poly no_trailing_map strip_while_idem_iff)
+ (metis comp_def no_leading_def no_trailing_coeffs)
+
+lemma set_coeffs_map_poly:
+ "(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)"
+ by (simp add: coeffs_map_poly')
lemma degree_map_poly:
assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
@@ -2146,7 +2150,8 @@
lemma poly_shift_monom: "poly_shift n (monom c m) = (if m \<ge> n then monom c (m - n) else 0)"
by (auto simp add: poly_eq_iff coeff_poly_shift)
-lemma coeffs_shift_poly [code abstract]: "coeffs (poly_shift n p) = drop n (coeffs p)"
+lemma coeffs_shift_poly [code abstract]:
+ "coeffs (poly_shift n p) = drop n (coeffs p)"
proof (cases "p = 0")
case True
then show ?thesis by simp
@@ -2154,7 +2159,7 @@
case False
then show ?thesis
by (intro coeffs_eqI)
- (simp_all add: coeff_poly_shift nth_default_drop last_coeffs_not_0 nth_default_coeffs_eq)
+ (simp_all add: coeff_poly_shift nth_default_drop nth_default_coeffs_eq)
qed
@@ -2192,7 +2197,7 @@
unfolding no_trailing_unfold by auto
then show ?thesis
by (intro coeffs_eqI)
- (simp_all add: coeff_poly_cutoff last_coeffs_not_0 nth_default_take nth_default_coeffs_eq)
+ (simp_all add: coeff_poly_cutoff nth_default_take nth_default_coeffs_eq)
qed
@@ -2308,7 +2313,8 @@
for xs :: "_::{comm_semiring_0,semiring_no_zero_divisors} poly list"
by (induct xs) (simp_all add: reflect_poly_mult)
-lemma reflect_poly_Poly_nz: "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0 \<Longrightarrow> reflect_poly (Poly xs) = Poly (rev xs)"
+lemma reflect_poly_Poly_nz:
+ "no_trailing (HOL.eq 0) xs \<Longrightarrow> reflect_poly (Poly xs) = Poly (rev xs)"
by (simp add: reflect_poly_def)
lemmas reflect_poly_simps =
@@ -4137,39 +4143,36 @@
qed simp
qed simp
-lemma pseudo_divmod_impl[code]: "pseudo_divmod (f::'a::comm_ring_1 poly) g =
- map_prod poly_of_list poly_of_list (pseudo_divmod_list (coeffs f) (coeffs g))"
+lemma pseudo_divmod_impl [code]:
+ "pseudo_divmod f g = map_prod poly_of_list poly_of_list (pseudo_divmod_list (coeffs f) (coeffs g))"
+ for f g :: "'a::comm_ring_1 poly"
proof (cases "g = 0")
case False
- then have coeffs_g_nonempty:"(coeffs g) \<noteq> []"
- by simp
- then have lastcoeffs: "last (coeffs g) = coeff g (degree g)"
- by (simp add: hd_rev last_coeffs_eq_coeff_degree not_0_coeffs_not_Nil)
- obtain q r where qr:
- "pseudo_divmod_main_list
- (last (coeffs g)) (rev [])
- (rev (coeffs f)) (rev (coeffs g))
- (1 + length (coeffs f) - length (coeffs g)) = (q, rev (rev r))"
+ then have "last (coeffs g) \<noteq> 0"
+ and "last (coeffs g) = lead_coeff g"
+ and "coeffs g \<noteq> []"
+ by (simp_all add: last_coeffs_eq_coeff_degree)
+ moreover obtain q r where qr: "pseudo_divmod_main_list
+ (last (coeffs g)) (rev [])
+ (rev (coeffs f)) (rev (coeffs g))
+ (1 + length (coeffs f) -
+ length (coeffs g)) = (q, rev (rev r))"
by force
- then have qr':
- "pseudo_divmod_main_list
- (hd (rev (coeffs g))) []
- (rev (coeffs f)) (rev (coeffs g))
- (1 + length (coeffs f) - length (coeffs g)) = (q, r)"
- using hd_rev[OF coeffs_g_nonempty] by auto
- from False have cg: "coeffs g = [] \<longleftrightarrow> False"
- by auto
- from False have last_non0: "last (coeffs g) \<noteq> 0"
- by (simp add: last_coeffs_not_0)
- from False show ?thesis
- unfolding pseudo_divmod_def pseudo_divmod_list_def Let_def qr' map_prod_def split cg if_False
- pseudo_divmod_main_list_invar[OF last_non0 _ _ qr,unfolded lastcoeffs,simplified,symmetric,OF False]
- poly_of_list_def
- by (auto simp: degree_eq_length_coeffs)
+ ultimately have "(Poly q, Poly (rev r)) = pseudo_divmod_main (lead_coeff g) 0 f g
+ (length (coeffs f) - Suc 0) (Suc (length (coeffs f)) - length (coeffs g))"
+ by (subst pseudo_divmod_main_list_invar [symmetric]) auto
+ moreover have "pseudo_divmod_main_list
+ (hd (rev (coeffs g))) []
+ (rev (coeffs f)) (rev (coeffs g))
+ (1 + length (coeffs f) -
+ length (coeffs g)) = (q, r)"
+ using qr hd_rev [OF \<open>coeffs g \<noteq> []\<close>] by simp
+ ultimately show ?thesis
+ by (auto simp: degree_eq_length_coeffs pseudo_divmod_def pseudo_divmod_list_def Let_def)
next
case True
then show ?thesis
- by (auto simp: pseudo_divmod_def pseudo_divmod_list_def)
+ by (auto simp add: pseudo_divmod_def pseudo_divmod_list_def)
qed
lemma pseudo_mod_main_list:
--- a/src/HOL/Library/Polynomial_Factorial.thy Thu Apr 06 10:21:45 2017 +0200
+++ b/src/HOL/Library/Polynomial_Factorial.thy Thu Apr 06 10:22:03 2017 +0200
@@ -16,8 +16,8 @@
subsection \<open>Various facts about polynomials\<close>
-lemma prod_mset_const_poly: "prod_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (image_mset f A):]"
- by (induction A) (simp_all add: one_poly_def mult_ac)
+lemma prod_mset_const_poly: " (\<Prod>x\<in>#A. [:f x:]) = [:prod_mset (image_mset f A):]"
+ by (induct A) (simp_all add: one_poly_def ac_simps)
lemma irreducible_const_poly_iff:
fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
@@ -168,14 +168,15 @@
by (auto elim!: dvdE)
lemma prod_mset_fract_poly:
- "prod_mset (image_mset (\<lambda>x. fract_poly (f x)) A) = fract_poly (prod_mset (image_mset f A))"
- by (induction A) (simp_all add: mult_ac)
+ "(\<Prod>x\<in>#A. map_poly to_fract (f x)) = fract_poly (prod_mset (image_mset f A))"
+ by (induct A) (simp_all add: ac_simps)
lemma is_unit_fract_poly_iff:
"p dvd 1 \<longleftrightarrow> fract_poly p dvd 1 \<and> content p = 1"
proof safe
assume A: "p dvd 1"
- with fract_poly_dvd[of p 1] show "is_unit (fract_poly p)" by simp
+ with fract_poly_dvd [of p 1] show "is_unit (fract_poly p)"
+ by simp
from A show "content p = 1"
by (auto simp: is_unit_poly_iff normalize_1_iff)
next
--- a/src/HOL/Number_Theory/Fib.thy Thu Apr 06 10:21:45 2017 +0200
+++ b/src/HOL/Number_Theory/Fib.thy Thu Apr 06 10:22:03 2017 +0200
@@ -14,29 +14,28 @@
subsection \<open>Fibonacci numbers\<close>
fun fib :: "nat \<Rightarrow> nat"
-where
- fib0: "fib 0 = 0"
-| fib1: "fib (Suc 0) = 1"
-| fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
+ where
+ fib0: "fib 0 = 0"
+ | fib1: "fib (Suc 0) = 1"
+ | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
subsection \<open>Basic Properties\<close>
-lemma fib_1 [simp]: "fib (1::nat) = 1"
+lemma fib_1 [simp]: "fib 1 = 1"
by (metis One_nat_def fib1)
-lemma fib_2 [simp]: "fib (2::nat) = 1"
- using fib.simps(3) [of 0]
- by (simp add: numeral_2_eq_2)
+lemma fib_2 [simp]: "fib 2 = 1"
+ using fib.simps(3) [of 0] by (simp add: numeral_2_eq_2)
lemma fib_plus_2: "fib (n + 2) = fib (n + 1) + fib n"
by (metis Suc_eq_plus1 add_2_eq_Suc' fib.simps(3))
-lemma fib_add: "fib (Suc (n+k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
+lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
by (induct n rule: fib.induct) (auto simp add: field_simps)
lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
- by (induct n rule: fib.induct) (auto simp add: )
+ by (induct n rule: fib.induct) auto
subsection \<open>More efficient code\<close>
@@ -45,21 +44,22 @@
The naive approach is very inefficient since the branching recursion leads to many
values of @{term fib} being computed multiple times. We can avoid this by ``remembering''
the last two values in the sequence, yielding a tail-recursive version.
- This is far from optimal (it takes roughly $O(n\cdot M(n))$ time where $M(n)$ is the
+ This is far from optimal (it takes roughly $O(n\cdot M(n))$ time where $M(n)$ is the
time required to multiply two $n$-bit integers), but much better than the naive version,
which is exponential.
\<close>
-fun gen_fib :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
- "gen_fib a b 0 = a"
-| "gen_fib a b (Suc 0) = b"
-| "gen_fib a b (Suc (Suc n)) = gen_fib b (a + b) (Suc n)"
+fun gen_fib :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+ where
+ "gen_fib a b 0 = a"
+ | "gen_fib a b (Suc 0) = b"
+ | "gen_fib a b (Suc (Suc n)) = gen_fib b (a + b) (Suc n)"
lemma gen_fib_recurrence: "gen_fib a b (Suc (Suc n)) = gen_fib a b n + gen_fib a b (Suc n)"
- by (induction a b n rule: gen_fib.induct) simp_all
-
+ by (induct a b n rule: gen_fib.induct) simp_all
+
lemma gen_fib_fib: "gen_fib (fib n) (fib (Suc n)) m = fib (n + m)"
- by (induction m rule: fib.induct) (simp_all del: gen_fib.simps(3) add: gen_fib_recurrence)
+ by (induct m rule: fib.induct) (simp_all del: gen_fib.simps(3) add: gen_fib_recurrence)
lemma fib_conv_gen_fib: "fib n = gen_fib 0 1 n"
using gen_fib_fib[of 0 n] by simp
@@ -70,22 +70,22 @@
subsection \<open>A Few Elementary Results\<close>
text \<open>
- \medskip Concrete Mathematics, page 278: Cassini's identity. The proof is
+ \<^medskip> Concrete Mathematics, page 278: Cassini's identity. The proof is
much easier using integers, not natural numbers!
\<close>
lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"
- by (induct n rule: fib.induct) (auto simp add: field_simps power2_eq_square power_add)
+ by (induct n rule: fib.induct) (auto simp add: field_simps power2_eq_square power_add)
lemma fib_Cassini_nat:
"fib (Suc (Suc n)) * fib n =
(if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
- using fib_Cassini_int [of n] by (auto simp del: of_nat_mult of_nat_power)
+ using fib_Cassini_int [of n] by (auto simp del: of_nat_mult of_nat_power)
subsection \<open>Law 6.111 of Concrete Mathematics\<close>
-lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
+lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
apply (induct n rule: fib.induct)
apply auto
apply (metis gcd_add1 add.commute)
@@ -109,12 +109,12 @@
proof (cases "m < n")
case True
then have "m \<le> n" by auto
- with \<open>0 < m\<close> have pos_n: "0 < n" by auto
- with \<open>0 < m\<close> \<open>m < n\<close> have diff: "n - m < n" by auto
+ with \<open>0 < m\<close> have "0 < n" by auto
+ with \<open>0 < m\<close> \<open>m < n\<close> have *: "n - m < n" by auto
have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
- by (simp add: mod_if [of n]) (insert \<open>m < n\<close>, auto)
+ by (simp add: mod_if [of n]) (use \<open>m < n\<close> in auto)
also have "\<dots> = gcd (fib m) (fib (n - m))"
- by (simp add: less.hyps diff \<open>0 < m\<close>)
+ by (simp add: less.hyps * \<open>0 < m\<close>)
also have "\<dots> = gcd (fib m) (fib n)"
by (simp add: gcd_fib_diff \<open>m \<le> n\<close>)
finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
@@ -125,8 +125,7 @@
qed
qed
-lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
- \<comment> \<open>Law 6.111\<close>
+lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" \<comment> \<open>Law 6.111\<close>
by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd.commute gcd_fib_mod)
theorem fib_mult_eq_sum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
@@ -136,49 +135,55 @@
subsection \<open>Closed form\<close>
lemma fib_closed_form:
- defines "\<phi> \<equiv> (1 + sqrt 5) / (2::real)" and "\<psi> \<equiv> (1 - sqrt 5) / (2::real)"
- shows "of_nat (fib n) = (\<phi> ^ n - \<psi> ^ n) / sqrt 5"
-proof (induction n rule: fib.induct)
+ fixes \<phi> \<psi> :: real
+ defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
+ and "\<psi> \<equiv> (1 - sqrt 5) / 2"
+ shows "of_nat (fib n) = (\<phi> ^ n - \<psi> ^ n) / sqrt 5"
+proof (induct n rule: fib.induct)
fix n :: nat
assume IH1: "of_nat (fib n) = (\<phi> ^ n - \<psi> ^ n) / sqrt 5"
assume IH2: "of_nat (fib (Suc n)) = (\<phi> ^ Suc n - \<psi> ^ Suc n) / sqrt 5"
have "of_nat (fib (Suc (Suc n))) = of_nat (fib (Suc n)) + of_nat (fib n)" by simp
- also have "... = (\<phi>^n*(\<phi> + 1) - \<psi>^n*(\<psi> + 1)) / sqrt 5"
+ also have "\<dots> = (\<phi>^n * (\<phi> + 1) - \<psi>^n * (\<psi> + 1)) / sqrt 5"
by (simp add: IH1 IH2 field_simps)
also have "\<phi> + 1 = \<phi>\<^sup>2" by (simp add: \<phi>_def field_simps power2_eq_square)
also have "\<psi> + 1 = \<psi>\<^sup>2" by (simp add: \<psi>_def field_simps power2_eq_square)
- also have "\<phi>^n * \<phi>\<^sup>2 - \<psi>^n * \<psi>\<^sup>2 = \<phi> ^ Suc (Suc n) - \<psi> ^ Suc (Suc n)"
+ also have "\<phi>^n * \<phi>\<^sup>2 - \<psi>^n * \<psi>\<^sup>2 = \<phi> ^ Suc (Suc n) - \<psi> ^ Suc (Suc n)"
by (simp add: power2_eq_square)
finally show "of_nat (fib (Suc (Suc n))) = (\<phi> ^ Suc (Suc n) - \<psi> ^ Suc (Suc n)) / sqrt 5" .
qed (simp_all add: \<phi>_def \<psi>_def field_simps)
lemma fib_closed_form':
- defines "\<phi> \<equiv> (1 + sqrt 5) / (2 :: real)" and "\<psi> \<equiv> (1 - sqrt 5) / (2 :: real)"
+ fixes \<phi> \<psi> :: real
+ defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
+ and "\<psi> \<equiv> (1 - sqrt 5) / 2"
assumes "n > 0"
- shows "fib n = round (\<phi> ^ n / sqrt 5)"
+ shows "fib n = round (\<phi> ^ n / sqrt 5)"
proof (rule sym, rule round_unique')
have "\<bar>\<phi> ^ n / sqrt 5 - of_int (int (fib n))\<bar> = \<bar>\<psi>\<bar> ^ n / sqrt 5"
by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] field_simps power_abs)
also {
from assms have "\<bar>\<psi>\<bar>^n \<le> \<bar>\<psi>\<bar>^1"
by (intro power_decreasing) (simp_all add: algebra_simps real_le_lsqrt)
- also have "... < sqrt 5 / 2" by (simp add: \<psi>_def field_simps)
+ also have "\<dots> < sqrt 5 / 2" by (simp add: \<psi>_def field_simps)
finally have "\<bar>\<psi>\<bar>^n / sqrt 5 < 1/2" by (simp add: field_simps)
}
finally show "\<bar>\<phi> ^ n / sqrt 5 - of_int (int (fib n))\<bar> < 1/2" .
qed
lemma fib_asymptotics:
- defines "\<phi> \<equiv> (1 + sqrt 5) / (2 :: real)"
- shows "(\<lambda>n. real (fib n) / (\<phi> ^ n / sqrt 5)) \<longlonglongrightarrow> 1"
+ fixes \<phi> :: real
+ defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
+ shows "(\<lambda>n. real (fib n) / (\<phi> ^ n / sqrt 5)) \<longlonglongrightarrow> 1"
proof -
- define \<psi> where "\<psi> \<equiv> (1 - sqrt 5) / (2 :: real)"
+ define \<psi> :: real where "\<psi> \<equiv> (1 - sqrt 5) / 2"
have "\<phi> > 1" by (simp add: \<phi>_def)
- hence A: "\<phi> \<noteq> 0" by auto
+ then have *: "\<phi> \<noteq> 0" by auto
have "(\<lambda>n. (\<psi> / \<phi>) ^ n) \<longlonglongrightarrow> 0"
by (rule LIMSEQ_power_zero) (simp_all add: \<phi>_def \<psi>_def field_simps add_pos_pos)
- hence "(\<lambda>n. 1 - (\<psi> / \<phi>) ^ n) \<longlonglongrightarrow> 1 - 0" by (intro tendsto_diff tendsto_const)
- with A show ?thesis
+ then have "(\<lambda>n. 1 - (\<psi> / \<phi>) ^ n) \<longlonglongrightarrow> 1 - 0"
+ by (intro tendsto_diff tendsto_const)
+ with * show ?thesis
by (simp add: divide_simps fib_closed_form [folded \<phi>_def \<psi>_def])
qed
@@ -186,58 +191,72 @@
subsection \<open>Divide-and-Conquer recurrence\<close>
text \<open>
- The following divide-and-conquer recurrence allows for a more efficient computation
- of Fibonacci numbers; however, it requires memoisation of values to be reasonably
+ The following divide-and-conquer recurrence allows for a more efficient computation
+ of Fibonacci numbers; however, it requires memoisation of values to be reasonably
efficient, cutting the number of values to be computed to logarithmically many instead of
- linearly many. The vast majority of the computation time is then actually spent on the
+ linearly many. The vast majority of the computation time is then actually spent on the
multiplication, since the output number is exponential in the input number.
\<close>
lemma fib_rec_odd:
- defines "\<phi> \<equiv> (1 + sqrt 5) / (2 :: real)" and "\<psi> \<equiv> (1 - sqrt 5) / (2 :: real)"
- shows "fib (Suc (2*n)) = fib n^2 + fib (Suc n)^2"
+ fixes \<phi> \<psi> :: real
+ defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
+ and "\<psi> \<equiv> (1 - sqrt 5) / 2"
+ shows "fib (Suc (2 * n)) = fib n^2 + fib (Suc n)^2"
proof -
have "of_nat (fib n^2 + fib (Suc n)^2) = ((\<phi> ^ n - \<psi> ^ n)\<^sup>2 + (\<phi> * \<phi> ^ n - \<psi> * \<psi> ^ n)\<^sup>2)/5"
by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] field_simps power2_eq_square)
- also have "(\<phi> ^ n - \<psi> ^ n)\<^sup>2 + (\<phi> * \<phi> ^ n - \<psi> * \<psi> ^ n)\<^sup>2 =
- \<phi>^(2*n) + \<psi>^(2*n) - 2*(\<phi>*\<psi>)^n + \<phi>^(2*n+2) + \<psi>^(2*n+2) - 2*(\<phi>*\<psi>)^(n+1)" (is "_ = ?A")
- by (simp add: power2_eq_square algebra_simps power_mult power_mult_distrib)
- also have "\<phi> * \<psi> = -1" by (simp add: \<phi>_def \<psi>_def field_simps)
- hence "?A = \<phi>^(2*n+1) * (\<phi> + inverse \<phi>) + \<psi>^(2*n+1) * (\<psi> + inverse \<psi>)"
+ also
+ let ?A = "\<phi>^(2 * n) + \<psi>^(2 * n) - 2*(\<phi> * \<psi>)^n + \<phi>^(2 * n + 2) + \<psi>^(2 * n + 2) - 2*(\<phi> * \<psi>)^(n + 1)"
+ have "(\<phi> ^ n - \<psi> ^ n)\<^sup>2 + (\<phi> * \<phi> ^ n - \<psi> * \<psi> ^ n)\<^sup>2 = ?A"
+ by (simp add: power2_eq_square algebra_simps power_mult power_mult_distrib)
+ also have "\<phi> * \<psi> = -1"
+ by (simp add: \<phi>_def \<psi>_def field_simps)
+ then have "?A = \<phi>^(2 * n + 1) * (\<phi> + inverse \<phi>) + \<psi>^(2 * n + 1) * (\<psi> + inverse \<psi>)"
by (auto simp: field_simps power2_eq_square)
- also have "1 + sqrt 5 > 0" by (auto intro: add_pos_pos)
- hence "\<phi> + inverse \<phi> = sqrt 5" by (simp add: \<phi>_def field_simps)
- also have "\<psi> + inverse \<psi> = -sqrt 5" by (simp add: \<psi>_def field_simps)
- also have "(\<phi> ^ (2*n+1) * sqrt 5 + \<psi> ^ (2*n+1)* - sqrt 5) / 5 =
- (\<phi> ^ (2*n+1) - \<psi> ^ (2*n+1)) * (sqrt 5 / 5)" by (simp add: field_simps)
- also have "sqrt 5 / 5 = inverse (sqrt 5)" by (simp add: field_simps)
- also have "(\<phi> ^ (2*n+1) - \<psi> ^ (2*n+1)) * ... = of_nat (fib (Suc (2*n)))"
+ also have "1 + sqrt 5 > 0"
+ by (auto intro: add_pos_pos)
+ then have "\<phi> + inverse \<phi> = sqrt 5"
+ by (simp add: \<phi>_def field_simps)
+ also have "\<psi> + inverse \<psi> = -sqrt 5"
+ by (simp add: \<psi>_def field_simps)
+ also have "(\<phi> ^ (2 * n + 1) * sqrt 5 + \<psi> ^ (2 * n + 1) * - sqrt 5) / 5 =
+ (\<phi> ^ (2 * n + 1) - \<psi> ^ (2 * n + 1)) * (sqrt 5 / 5)"
+ by (simp add: field_simps)
+ also have "sqrt 5 / 5 = inverse (sqrt 5)"
+ by (simp add: field_simps)
+ also have "(\<phi> ^ (2 * n + 1) - \<psi> ^ (2 * n + 1)) * \<dots> = of_nat (fib (Suc (2 * n)))"
by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] divide_inverse)
- finally show ?thesis by (simp only: of_nat_eq_iff)
+ finally show ?thesis
+ by (simp only: of_nat_eq_iff)
qed
-lemma fib_rec_even: "fib (2*n) = (fib (n - 1) + fib (n + 1)) * fib n"
-proof (induction n)
+lemma fib_rec_even: "fib (2 * n) = (fib (n - 1) + fib (n + 1)) * fib n"
+proof (induct n)
+ case 0
+ then show ?case by simp
+next
case (Suc n)
let ?rfib = "\<lambda>x. real (fib x)"
- have "2 * (Suc n) = Suc (Suc (2*n))" by simp
- also have "real (fib ...) = ?rfib n^2 + ?rfib (Suc n)^2 + (?rfib (n - 1) + ?rfib (n + 1)) * ?rfib n"
+ have "2 * (Suc n) = Suc (Suc (2 * n))" by simp
+ also have "real (fib \<dots>) = ?rfib n^2 + ?rfib (Suc n)^2 + (?rfib (n - 1) + ?rfib (n + 1)) * ?rfib n"
by (simp add: fib_rec_odd Suc)
also have "(?rfib (n - 1) + ?rfib (n + 1)) * ?rfib n = (2 * ?rfib (n + 1) - ?rfib n) * ?rfib n"
by (cases n) simp_all
- also have "?rfib n^2 + ?rfib (Suc n)^2 + ... = (?rfib (Suc n) + 2 * ?rfib n) * ?rfib (Suc n)"
+ also have "?rfib n^2 + ?rfib (Suc n)^2 + \<dots> = (?rfib (Suc n) + 2 * ?rfib n) * ?rfib (Suc n)"
by (simp add: algebra_simps power2_eq_square)
- also have "... = real ((fib (Suc n - 1) + fib (Suc n + 1)) * fib (Suc n))" by simp
+ also have "\<dots> = real ((fib (Suc n - 1) + fib (Suc n + 1)) * fib (Suc n))" by simp
finally show ?case by (simp only: of_nat_eq_iff)
-qed simp
+qed
-lemma fib_rec_even': "fib (2*n) = (2*fib (n - 1) + fib n) * fib n"
+lemma fib_rec_even': "fib (2 * n) = (2 * fib (n - 1) + fib n) * fib n"
by (subst fib_rec_even, cases n) simp_all
lemma fib_rec:
- "fib n = (if n = 0 then 0 else if n = 1 then 1 else
- if even n then let n' = n div 2; fn = fib n' in (2 * fib (n' - 1) + fn) * fn
- else let n' = n div 2 in fib n' ^ 2 + fib (Suc n') ^ 2)"
+ "fib n =
+ (if n = 0 then 0 else if n = 1 then 1
+ else if even n then let n' = n div 2; fn = fib n' in (2 * fib (n' - 1) + fn) * fn
+ else let n' = n div 2 in fib n' ^ 2 + fib (Suc n') ^ 2)"
by (auto elim: evenE oddE simp: fib_rec_odd fib_rec_even' Let_def)
@@ -247,7 +266,8 @@
by (induct n) auto
lemma sum_choose_drop_zero:
- "(\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k) choose (k - 1)) = (\<Sum>j = 0..n. (n-j) choose j)"
+ "(\<Sum>k = 0..Suc n. if k = 0 then 0 else (Suc n - k) choose (k - 1)) =
+ (\<Sum>j = 0..n. (n-j) choose j)"
by (rule trans [OF sum.cong sum_drop_zero]) auto
lemma ne_diagonal_fib: "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
@@ -260,17 +280,16 @@
next
case (3 n)
have "(\<Sum>k = 0..Suc n. Suc (Suc n) - k choose k) =
- (\<Sum>k = 0..Suc n. (Suc n - k choose k) + (if k=0 then 0 else (Suc n - k choose (k - 1))))"
+ (\<Sum>k = 0..Suc n. (Suc n - k choose k) + (if k = 0 then 0 else (Suc n - k choose (k - 1))))"
by (rule sum.cong) (simp_all add: choose_reduce_nat)
- also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
- (\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))"
+ also have "\<dots> =
+ (\<Sum>k = 0..Suc n. Suc n - k choose k) +
+ (\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))"
by (simp add: sum.distrib)
- also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
- (\<Sum>j = 0..n. n - j choose j)"
+ also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) + (\<Sum>j = 0..n. n - j choose j)"
by (metis sum_choose_drop_zero)
finally show ?case using 3
by simp
qed
end
-
--- a/src/HOL/ROOT Thu Apr 06 10:21:45 2017 +0200
+++ b/src/HOL/ROOT Thu Apr 06 10:22:03 2017 +0200
@@ -4,9 +4,9 @@
description {*
Classical Higher-order Logic.
*}
- global_theories
- Main
- Complex_Main
+ theories
+ Main (global)
+ Complex_Main (global)
files
"Tools/Quickcheck/Narrowing_Engine.hs"
"Tools/Quickcheck/PNF_Narrowing_Engine.hs"
@@ -60,6 +60,17 @@
Refute
document_files "root.bib" "root.tex"
+session "HOL-Analysis" (main timing) in Analysis = HOL +
+ theories
+ Analysis (global)
+ document_files
+ "root.tex"
+
+session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" +
+ theories
+ Approximations
+ Circle_Area
+
session "HOL-Hahn_Banach" in Hahn_Banach = HOL +
description {*
Author: Gertrud Bauer, TU Munich
@@ -205,11 +216,7 @@
"~~/src/HOL/Algebra/Ring"
"~~/src/HOL/Algebra/FiniteProduct"
theories
- Pocklington
- Gauss
Number_Theory
- Euclidean_Algorithm
- Factorial_Ring
document_files
"root.tex"
@@ -709,18 +716,7 @@
theories
ATP_Problem_Import
-session "HOL-Analysis" (main timing) in Analysis = HOL +
- theories
- Analysis
- document_files
- "root.tex"
-
-session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" +
- theories
- Approximations
- Circle_Area
-
-session "HOL-Probability" (timing) in "Probability" = "HOL-Analysis" +
+session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
theories [document = false]
"~~/src/HOL/Library/Countable"
"~~/src/HOL/Library/Permutation"
@@ -728,7 +724,7 @@
"~~/src/HOL/Library/Diagonal_Subsequence"
"~~/src/HOL/Library/Finite_Map"
theories
- Probability
+ Probability (global)
document_files "root.tex"
session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
@@ -824,7 +820,8 @@
"Tests/Type_Class"
session "HOL-Word" (main timing) in Word = HOL +
- theories Word
+ theories
+ Word (global)
document_files "root.bib" "root.tex"
session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
@@ -872,7 +869,8 @@
session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +
options [document = false]
- theories SPARK
+ theories
+ SPARK (global)
session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
options [document = false, spark_prv = false]
@@ -1039,9 +1037,7 @@
"~~/src/HOL/Library/Nat_Bijection"
"~~/src/HOL/Library/Countable"
theories
- Plain_HOLCF
- Fixrec
- HOLCF
+ HOLCF (global)
document_files "root.tex"
session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
--- a/src/HOL/Tools/Function/function.ML Thu Apr 06 10:21:45 2017 +0200
+++ b/src/HOL/Tools/Function/function.ML Thu Apr 06 10:22:03 2017 +0200
@@ -120,7 +120,7 @@
val info =
{ add_simps=addsmps, fnames=fnames, case_names=cnames, psimps=psimps',
- pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
+ pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', totality=NONE,
fs=fs, R=R, dom=dom, defname=defname, is_partial=true, cases=flat cases',
pelims=pelims',elims=NONE}
@@ -202,7 +202,8 @@
|-> (fn ((simps,(_,inducts)), elims) => fn lthy =>
let val info' = { is_partial=false, defname=defname, fnames=fnames, add_simps=add_simps,
case_names=case_names, fs=fs, R=R, dom=dom, psimps=psimps, pinducts=pinducts,
- simps=SOME simps, inducts=SOME inducts, termination=termination, cases=cases, pelims=pelims, elims=SOME elims}
+ simps=SOME simps, inducts=SOME inducts, termination=termination, totality=SOME totality,
+ cases=cases, pelims=pelims, elims=SOME elims}
in
(info',
lthy
--- a/src/HOL/Tools/Function/function_common.ML Thu Apr 06 10:21:45 2017 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Thu Apr 06 10:22:03 2017 +0200
@@ -22,6 +22,7 @@
simps : thm list option,
inducts : thm list option,
termination : thm,
+ totality : thm option,
cases : thm list,
pelims: thm list list,
elims: thm list list option}
@@ -46,6 +47,7 @@
simps : thm list option,
inducts : thm list option,
termination : thm,
+ totality : thm option,
cases : thm list,
pelims : thm list list,
elims : thm list list option}
@@ -291,7 +293,7 @@
domintros : thm list option}
fun transform_function_data phi ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
- simps, inducts, termination, defname, is_partial, cases, pelims, elims} : info) =
+ simps, inducts, termination, totality, defname, is_partial, cases, pelims, elims} : info) =
let
val term = Morphism.term phi
val thm = Morphism.thm phi
@@ -301,7 +303,8 @@
fs = map term fs, R = term R, dom = term dom, psimps = fact psimps,
pinducts = fact pinducts, simps = Option.map fact simps,
inducts = Option.map fact inducts, termination = thm termination,
- defname = Morphism.binding phi defname, is_partial=is_partial, cases = fact cases,
+ totality = Option.map thm totality, defname = Morphism.binding phi defname,
+ is_partial = is_partial, cases = fact cases,
elims = Option.map (map fact) elims, pelims = map fact pelims }
end
--- a/src/Pure/GUI/gui.scala Thu Apr 06 10:21:45 2017 +0200
+++ b/src/Pure/GUI/gui.scala Thu Apr 06 10:22:03 2017 +0200
@@ -93,12 +93,13 @@
}
private def simple_dialog(kind: Int, default_title: String,
- parent: Component, title: String, message: Seq[Any])
+ parent: Component, title: String, message: Iterable[Any])
{
GUI_Thread.now {
- val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
- JOptionPane.showMessageDialog(parent,
- java_message.toArray.asInstanceOf[Array[AnyRef]],
+ val java_message =
+ message.iterator.map({ case x: scala.swing.Component => x.peer case x => x }).
+ toArray.asInstanceOf[Array[AnyRef]]
+ JOptionPane.showMessageDialog(parent, java_message,
if (title == null) default_title else title, kind)
}
}
--- a/src/Pure/General/linear_set.scala Thu Apr 06 10:21:45 2017 +0200
+++ b/src/Pure/General/linear_set.scala Thu Apr 06 10:22:03 2017 +0200
@@ -78,7 +78,7 @@
}
}
- def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] = // FIXME reverse fold
+ def append_after(hook: Option[A], elems: Traversable[A]): Linear_Set[A] = // FIXME reverse fold
((hook, this) /: elems) {
case ((last, set), elem) => (Some(elem), set.insert_after(last, elem))
}._2
--- a/src/Pure/Isar/keyword.scala Thu Apr 06 10:21:45 2017 +0200
+++ b/src/Pure/Isar/keyword.scala Thu Apr 06 10:22:03 2017 +0200
@@ -93,11 +93,19 @@
/** keyword tables **/
- type Spec = ((String, List[String]), List[String])
+ object Spec
+ {
+ val none: Spec = Spec("")
+ }
+ sealed case class Spec(kind: String, exts: List[String] = Nil, tags: List[String] = Nil)
+ {
+ def is_none: Boolean = kind == ""
- val no_spec: Spec = (("", Nil), Nil)
- val before_command_spec: Spec = ((BEFORE_COMMAND, Nil), Nil)
- val quasi_command_spec: Spec = ((QUASI_COMMAND, Nil), Nil)
+ override def toString: String =
+ kind +
+ (if (exts.isEmpty) "" else " (" + commas_quote(exts) + ")") +
+ (if (tags.isEmpty) "" else tags.map(quote).mkString(" % ", " % ", ""))
+ }
object Keywords
{
@@ -165,9 +173,13 @@
def add_keywords(header: Thy_Header.Keywords): Keywords =
(this /: header) {
- case (keywords, (name, ((kind, exts), _))) =>
- if (kind == "") keywords + Symbol.decode(name) + Symbol.encode(name)
- else keywords + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts)
+ case (keywords, (name, spec)) =>
+ if (spec.is_none)
+ keywords + Symbol.decode(name) + Symbol.encode(name)
+ else
+ keywords +
+ (Symbol.decode(name), spec.kind, spec.exts) +
+ (Symbol.encode(name), spec.kind, spec.exts)
}
--- a/src/Pure/Isar/outer_syntax.scala Thu Apr 06 10:21:45 2017 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Thu Apr 06 10:22:03 2017 +0200
@@ -57,9 +57,9 @@
/* keywords */
- def + (name: String, kind: String = "", tags: List[String] = Nil): Outer_Syntax =
+ def + (name: String, kind: String = "", exts: List[String] = Nil): Outer_Syntax =
{
- val keywords1 = keywords + (name, kind, tags)
+ val keywords1 = keywords + (name, kind, exts)
val completion1 =
completion.add_keyword(name).
add_abbrevs(
@@ -71,8 +71,10 @@
def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
(this /: keywords) {
- case (syntax, (name, ((kind, tags), _))) =>
- syntax + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
+ case (syntax, (name, spec)) =>
+ syntax +
+ (Symbol.decode(name), spec.kind, spec.exts) +
+ (Symbol.encode(name), spec.kind, spec.exts)
}
--- a/src/Pure/PIDE/protocol.scala Thu Apr 06 10:21:45 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala Thu Apr 06 10:22:03 2017 +0200
@@ -361,10 +361,12 @@
val master_dir = File.standard_url(name.master_dir)
val theory = Long_Name.base_name(name.theory)
val imports = header.imports.map({ case (a, _) => a.node })
+ val keywords =
+ header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) })
(Nil,
pair(string, pair(string, pair(list(string), pair(list(pair(string,
pair(pair(string, list(string)), list(string)))), list(string)))))(
- (master_dir, (theory, (imports, (header.keywords, header.errors)))))) },
+ (master_dir, (theory, (imports, (keywords, header.errors)))))) },
{ case Document.Node.Perspective(a, b, c) =>
(bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
list(pair(id, pair(string, list(string))))(c.dest)) }))
--- a/src/Pure/PIDE/resources.scala Thu Apr 06 10:21:45 2017 +0200
+++ b/src/Pure/PIDE/resources.scala Thu Apr 06 10:22:03 2017 +0200
@@ -67,35 +67,27 @@
}
else Nil
- def init_name(global: Boolean, raw_path: Path): Document.Node.Name =
+ def import_name(dir: String, s: String): Document.Node.Name =
{
- val path = raw_path.expand
- val node = path.implode
- val qualifier = if (global) "" else session_name
- val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse(""))
- val master_dir = if (theory == "") "" else path.dir.implode
- Document.Node.Name(node, master_dir, theory)
- }
-
- def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
- {
- val theory = Thy_Header.base_name(s)
- val is_qualified = Thy_Header.is_base_name(s) && Long_Name.is_qualified(s)
+ val thy = Thy_Header.base_name(s)
+ val is_global = session_base.global_theories.contains(thy)
+ val is_qualified = Long_Name.is_qualified(thy)
val known_theory =
- session_base.known_theories.get(theory) orElse
- (if (is_qualified) session_base.known_theories.get(Long_Name.base_name(theory))
- else session_base.known_theories.get(Long_Name.qualify(session_name, theory)))
+ session_base.known_theories.get(thy) orElse
+ (if (is_global) None
+ else if (is_qualified) session_base.known_theories.get(Long_Name.base_name(thy))
+ else session_base.known_theories.get(Long_Name.qualify(session_name, thy)))
known_theory match {
case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
case Some(name) => name
- case None if is_qualified => Document.Node.Name.theory(theory)
case None =>
val path = Path.explode(s)
- val node = append(master.master_dir, thy_path(path))
- val master_dir = append(master.master_dir, path.dir)
- Document.Node.Name(node, master_dir, Long_Name.qualify(session_name, theory))
+ val node = append(dir, thy_path(path))
+ val master_dir = append(dir, path.dir)
+ val theory = if (is_global || is_qualified) thy else Long_Name.qualify(session_name, thy)
+ Document.Node.Name(node, master_dir, theory)
}
}
@@ -123,7 +115,7 @@
Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
val imports =
- header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) })
+ header.imports.map({ case (s, pos) => (import_name(node_name.master_dir, s), pos) })
Document.Node.Header(imports, header.keywords, header.abbrevs)
}
catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
@@ -140,9 +132,11 @@
def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
if (Thy_Header.is_ml_root(name.theory))
- Some(Document.Node.Header(List((import_name(name, Thy_Header.ML_BOOTSTRAP), Position.none))))
+ Some(Document.Node.Header(
+ List((import_name(name.master_dir, Thy_Header.ML_BOOTSTRAP), Position.none))))
else if (Thy_Header.is_bootstrap(name.theory))
- Some(Document.Node.Header(List((import_name(name, Thy_Header.PURE), Position.none))))
+ Some(Document.Node.Header(
+ List((import_name(name.master_dir, Thy_Header.PURE), Position.none))))
else None
--- a/src/Pure/PIDE/text.scala Thu Apr 06 10:21:45 2017 +0200
+++ b/src/Pure/PIDE/text.scala Thu Apr 06 10:22:03 2017 +0200
@@ -82,7 +82,7 @@
def full: Perspective = Perspective(List(Range.full))
- def apply(ranges: Seq[Range]): Perspective =
+ def apply(ranges: List[Range]): Perspective =
{
val result = new mutable.ListBuffer[Range]
var last: Option[Range] = None
--- a/src/Pure/ROOT Thu Apr 06 10:21:45 2017 +0200
+++ b/src/Pure/ROOT Thu Apr 06 10:22:03 2017 +0200
@@ -5,7 +5,6 @@
The Pure logical framework
*}
options [threads = 1]
- global_theories
- Pure
theories
+ Pure (global)
ML_Bootstrap
--- a/src/Pure/Thy/present.scala Thu Apr 06 10:21:45 2017 +0200
+++ b/src/Pure/Thy/present.scala Thu Apr 06 10:22:03 2017 +0200
@@ -18,19 +18,19 @@
def session_graph(
parent_session: String,
- parent_loaded: String => Boolean,
+ parent_base: Sessions.Base,
deps: List[Thy_Info.Dep]): Graph_Display.Graph =
{
val parent_session_node =
Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
def node(name: Document.Node.Name): Graph_Display.Node =
- if (parent_loaded(name.theory)) parent_session_node
- else Graph_Display.Node(name.theory, "theory." + name.theory)
+ if (parent_base.loaded_theory(name)) parent_session_node
+ else Graph_Display.Node(Long_Name.base_name(name.theory), "theory." + name.theory)
(Graph_Display.empty_graph /: deps) {
case (g, dep) =>
- if (parent_loaded(dep.name.theory)) g
+ if (parent_base.loaded_theory(dep.name)) g
else {
val a = node(dep.name)
val bs = dep.header.imports.map({ case (name, _) => node(name) })
--- a/src/Pure/Thy/sessions.scala Thu Apr 06 10:21:45 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Thu Apr 06 10:22:03 2017 +0200
@@ -30,6 +30,7 @@
}
sealed case class Base(
+ global_theories: Set[String] = Set.empty,
loaded_theories: Set[String] = Set.empty,
known_theories: Map[String, Document.Node.Name] = Map.empty,
keywords: Thy_Header.Keywords = Nil,
@@ -54,7 +55,9 @@
verbose: Boolean = false,
list_files: Boolean = false,
check_keywords: Set[String] = Set.empty,
+ global_theories: Set[String] = Set.empty,
tree: Tree): Deps =
+ {
Deps((Map.empty[String, Base] /: tree.topological_order)(
{ case (deps, (name, info)) =>
if (progress.stopped) throw Exn.Interrupt()
@@ -77,10 +80,8 @@
val thy_deps =
{
val root_theories =
- info.theories.flatMap({
- case (global, _, thys) =>
- thys.map(thy =>
- (resources.init_name(global, info.dir + resources.thy_path(thy)), info.pos))
+ info.theories.flatMap({ case (_, thys) =>
+ thys.map(thy => (resources.import_name(info.dir.implode, thy), info.pos))
})
val thy_deps = resources.thy_info.dependencies(root_theories)
@@ -132,14 +133,16 @@
if (check_keywords.nonEmpty)
Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
- val sources = all_files.map(p => (p, SHA1.digest(p.file)))
+ val base =
+ Base(global_theories = global_theories,
+ loaded_theories = loaded_theories,
+ known_theories = known_theories,
+ keywords = keywords,
+ syntax = syntax,
+ sources = all_files.map(p => (p, SHA1.digest(p.file))),
+ session_graph =
+ Present.session_graph(info.parent getOrElse "", parent_base, thy_deps.deps))
- val session_graph =
- Present.session_graph(info.parent getOrElse "",
- parent_base.loaded_theories, thy_deps.deps)
-
- val base =
- Base(loaded_theories, known_theories, keywords, syntax, sources, session_graph)
deps + (name -> base)
}
catch {
@@ -148,11 +151,14 @@
quote(name) + Position.here(info.pos))
}
}))
+ }
def session_base(options: Options, session: String, dirs: List[Path] = Nil): Base =
{
- val (_, tree) = load(options, dirs = dirs).selection(sessions = List(session))
- dependencies(tree = tree)(session)
+ val full_tree = load(options, dirs = dirs)
+ val (_, tree) = full_tree.selection(sessions = List(session))
+
+ dependencies(global_theories = full_tree.global_theories, tree = tree)(session)
}
@@ -167,7 +173,8 @@
parent: Option[String],
description: String,
options: Options,
- theories: List[(Boolean, Options, List[Path])],
+ theories: List[(Options, List[String])],
+ global_theories: List[String],
files: List[Path],
document_files: List[(Path, Path)],
meta_digest: SHA1.Digest)
@@ -177,7 +184,7 @@
object Tree
{
- def apply(infos: Seq[(String, Info)]): Tree =
+ def apply(infos: Traversable[(String, Info)]): Tree =
{
val graph1 =
(Graph.string[Info] /: infos) {
@@ -207,6 +214,7 @@
}
}
}
+
new Tree(graph2)
}
}
@@ -217,6 +225,12 @@
def apply(name: String): Info = graph.get_node(name)
def isDefinedAt(name: String): Boolean = graph.defined(name)
+ def global_theories: Set[String] =
+ (for {
+ (_, (info, _)) <- graph.iterator
+ name <- info.global_theories.iterator }
+ yield name).toSet
+
def selection(
requirements: Boolean = false,
all_sessions: Boolean = false,
@@ -281,18 +295,17 @@
private val IN = "in"
private val DESCRIPTION = "description"
private val OPTIONS = "options"
- private val GLOBAL_THEORIES = "global_theories"
private val THEORIES = "theories"
+ private val GLOBAL = "global"
private val FILES = "files"
private val DOCUMENT_FILES = "document_files"
lazy val root_syntax =
- Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" + IN +
+ Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" + GLOBAL + IN +
(CHAPTER, Keyword.THY_DECL) +
(SESSION, Keyword.THY_DECL) +
(DESCRIPTION, Keyword.QUASI_COMMAND) +
(OPTIONS, Keyword.QUASI_COMMAND) +
- (GLOBAL_THEORIES, Keyword.QUASI_COMMAND) +
(THEORIES, Keyword.QUASI_COMMAND) +
(FILES, Keyword.QUASI_COMMAND) +
(DOCUMENT_FILES, Keyword.QUASI_COMMAND)
@@ -309,7 +322,7 @@
parent: Option[String],
description: String,
options: List[Options.Spec],
- theories: List[(Boolean, List[Options.Spec], List[String])],
+ theories: List[(List[Options.Spec], List[(String, Boolean)])],
files: List[String],
document_files: List[(String, String)]) extends Entry
@@ -329,10 +342,16 @@
{ case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
+ val global =
+ ($$$("(") ~! $$$(GLOBAL) ~ $$$(")")) ^^ { case _ => true } | success(false)
+
+ val theory_entry =
+ theory_name ~ global ^^ { case x ~ y => (x, y) }
+
val theories =
- ($$$(GLOBAL_THEORIES) | $$$(THEORIES)) ~!
- ((options | success(Nil)) ~ rep(theory_name)) ^^
- { case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
+ $$$(THEORIES) ~!
+ ((options | success(Nil)) ~ rep(theory_entry)) ^^
+ { case _ ~ (x ~ y) => (x, y) }
val document_files =
$$$(DOCUMENT_FILES) ~!
@@ -369,8 +388,17 @@
val session_options = options ++ entry.options
val theories =
- entry.theories.map({ case (global, opts, thys) =>
- (global, session_options ++ opts, thys.map(Path.explode(_))) })
+ entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) })
+
+ val global_theories =
+ for { (_, thys) <- entry.theories; (thy, global) <- thys if global }
+ yield {
+ val thy_name = Path.explode(thy).expand.base.implode
+ if (Long_Name.is_qualified(thy_name))
+ error("Bad qualified name for global theory " + quote(thy_name))
+ else thy_name
+ }
+
val files = entry.files.map(Path.explode(_))
val document_files =
entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
@@ -381,8 +409,8 @@
val info =
Info(entry_chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
- entry.parent, entry.description, session_options, theories, files,
- document_files, meta_digest)
+ entry.parent, entry.description, session_options, theories, global_theories,
+ files, document_files, meta_digest)
(name, info)
}
--- a/src/Pure/Thy/thy_header.scala Thu Apr 06 10:21:45 2017 +0200
+++ b/src/Pure/Thy/thy_header.scala Thu Apr 06 10:22:03 2017 +0200
@@ -39,28 +39,28 @@
val bootstrap_header: Keywords =
List(
- ("%", Keyword.no_spec),
- ("(", Keyword.no_spec),
- (")", Keyword.no_spec),
- (",", Keyword.no_spec),
- ("::", Keyword.no_spec),
- ("=", Keyword.no_spec),
- (AND, Keyword.no_spec),
- (BEGIN, Keyword.quasi_command_spec),
- (IMPORTS, Keyword.quasi_command_spec),
- (KEYWORDS, Keyword.quasi_command_spec),
- (ABBREVS, Keyword.quasi_command_spec),
- (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
- (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
- (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
- (SUBSUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
- (PARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
- (SUBPARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
- (TEXT, (((Keyword.DOCUMENT_BODY, Nil), Nil))),
- (TXT, (((Keyword.DOCUMENT_BODY, Nil), Nil))),
- (TEXT_RAW, (((Keyword.DOCUMENT_RAW, Nil), Nil))),
- (THEORY, ((Keyword.THY_BEGIN, Nil), List("theory"))),
- ("ML", ((Keyword.THY_DECL, Nil), List("ML"))))
+ ("%", Keyword.Spec.none),
+ ("(", Keyword.Spec.none),
+ (")", Keyword.Spec.none),
+ (",", Keyword.Spec.none),
+ ("::", Keyword.Spec.none),
+ ("=", Keyword.Spec.none),
+ (AND, Keyword.Spec.none),
+ (BEGIN, Keyword.Spec(Keyword.QUASI_COMMAND)),
+ (IMPORTS, Keyword.Spec(Keyword.QUASI_COMMAND)),
+ (KEYWORDS, Keyword.Spec(Keyword.QUASI_COMMAND)),
+ (ABBREVS, Keyword.Spec(Keyword.QUASI_COMMAND)),
+ (CHAPTER, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
+ (SECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
+ (SUBSECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
+ (SUBSUBSECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
+ (PARAGRAPH, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
+ (SUBPARAGRAPH, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
+ (TEXT, Keyword.Spec(Keyword.DOCUMENT_BODY)),
+ (TXT, Keyword.Spec(Keyword.DOCUMENT_BODY)),
+ (TEXT_RAW, Keyword.Spec(Keyword.DOCUMENT_RAW)),
+ (THEORY, Keyword.Spec(Keyword.THY_BEGIN, tags = List("theory"))),
+ ("ML", Keyword.Spec(Keyword.THY_DECL, tags = List("ML"))))
private val bootstrap_keywords =
Keyword.Keywords.empty.add_keywords(bootstrap_header)
@@ -80,9 +80,6 @@
private val Base_Name = new Regex(""".*?([^/\\:]+)""")
private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
- def is_base_name(s: String): Boolean =
- s != "" && !s.exists("/\\:".contains(_))
-
def base_name(s: String): String =
s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
@@ -114,12 +111,12 @@
val keyword_spec =
atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
- { case x ~ y ~ z => ((x, y), z) }
+ { case x ~ y ~ z => Keyword.Spec(x, y, z) }
val keyword_decl =
rep1(string) ~
opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
- { case xs ~ y => xs.map((_, y.getOrElse(Keyword.no_spec))) }
+ { case xs ~ y => xs.map((_, y.getOrElse(Keyword.Spec.none))) }
val keyword_decls =
keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
@@ -192,7 +189,8 @@
val f = Symbol.decode _
Thy_Header((f(name._1), name._2),
imports.map({ case (a, b) => (f(a), b) }),
- keywords.map({ case (a, ((b, c), d)) => (f(a), ((f(b), c.map(f)), d.map(f))) }),
+ keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
+ (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
abbrevs.map({ case (a, b) => (f(a), f(b)) }))
}
}
--- a/src/Pure/Tools/build.scala Thu Apr 06 10:21:45 2017 +0200
+++ b/src/Pure/Tools/build.scala Thu Apr 06 10:22:03 2017 +0200
@@ -200,16 +200,15 @@
val args_yxml =
YXML.string_of_body(
{
- val theories = info.theories.map(x => (x._2, x._3))
import XML.Encode._
pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
pair(string, pair(string, pair(string, pair(Path.encode,
- list(pair(Options.encode, list(Path.encode))))))))))))))(
+ list(pair(Options.encode, list(string))))))))))))))(
(Symbol.codes, (command_timings, (do_output, (verbose,
(store.browser_info, (info.document_files, (File.standard_path(graph_file),
(parent, (info.chapter, (name, (Path.current,
- theories))))))))))))
+ info.theories))))))))))))
})
val env =
@@ -396,7 +395,9 @@
val full_tree = Sessions.load(build_options, dirs, select_dirs)
val (selected, selected_tree) = selection(full_tree)
val deps =
- Sessions.dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
+ Sessions.dependencies(
+ progress, true, verbose, list_files, check_keywords,
+ full_tree.global_theories, selected_tree)
def sources_stamp(name: String): List[String] =
(selected_tree(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
--- a/src/ZF/ZF.thy Thu Apr 06 10:21:45 2017 +0200
+++ b/src/ZF/ZF.thy Thu Apr 06 10:22:03 2017 +0200
@@ -217,7 +217,7 @@
definition relation :: "i \<Rightarrow> o" \<comment> \<open>recognizes sets of pairs\<close>
where "relation(r) == \<forall>z\<in>r. \<exists>x y. z = \<langle>x,y\<rangle>"
-definition function :: "i \<Rightarrow> o" \<comment> \<open>recognizes functions; can have non-pairs\<close>
+definition "function" :: "i \<Rightarrow> o" \<comment> \<open>recognizes functions; can have non-pairs\<close>
where "function(r) == \<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> (\<forall>y'. \<langle>x,y'\<rangle> \<in> r \<longrightarrow> y = y')"
definition Image :: "[i, i] \<Rightarrow> i" (infixl "``" 90) \<comment> \<open>image\<close>