--- a/src/HOL/BNF_Examples/Misc_Primcorec.thy Thu Feb 27 21:31:58 2014 +0100
+++ b/src/HOL/BNF_Examples/Misc_Primcorec.thy Thu Feb 27 21:36:40 2014 +0100
@@ -97,6 +97,19 @@
| MyCons t ts => MyCons (id_tree t) (id_trees2 ts))"
primcorec
+ trunc_tree :: "'a bin_rose_tree \<Rightarrow> 'a bin_rose_tree" and
+ trunc_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and
+ trunc_trees2 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist"
+where
+ "trunc_tree t = (case t of BRTree a ts ts' => BRTree a (trunc_trees1 ts) (trunc_trees2 ts'))" |
+ "trunc_trees1 ts = (case ts of
+ MyNil => MyNil
+ | MyCons t _ => MyCons (trunc_tree t) MyNil)" |
+ "trunc_trees2 ts = (case ts of
+ MyNil => MyNil
+ | MyCons t ts => MyCons (trunc_tree t) MyNil)"
+
+primcorec
freeze_exp :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) exp \<Rightarrow> ('a, 'b) exp" and
freeze_trm :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) trm \<Rightarrow> ('a, 'b) trm" and
freeze_factor :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) factor \<Rightarrow> ('a, 'b) factor"
--- a/src/HOL/BNF_Examples/Misc_Primrec.thy Thu Feb 27 21:31:58 2014 +0100
+++ b/src/HOL/BNF_Examples/Misc_Primrec.thy Thu Feb 27 21:36:40 2014 +0100
@@ -102,6 +102,17 @@
"id_trees2 (MyCons t ts) = MyCons (id_tree t) (id_trees2 ts)"
primrec
+ trunc_tree :: "'a bin_rose_tree \<Rightarrow> 'a bin_rose_tree" and
+ trunc_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and
+ trunc_trees2 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist"
+where
+ "trunc_tree (BRTree a ts ts') = BRTree a (trunc_trees1 ts) (trunc_trees2 ts')" |
+ "trunc_trees1 MyNil = MyNil" |
+ "trunc_trees1 (MyCons t ts) = MyCons (id_tree t) MyNil" |
+ "trunc_trees2 MyNil = MyNil" |
+ "trunc_trees2 (MyCons t ts) = MyCons (id_tree t) MyNil"
+
+primrec
is_ground_exp :: "('a, 'b) exp \<Rightarrow> bool" and
is_ground_trm :: "('a, 'b) trm \<Rightarrow> bool" and
is_ground_factor :: "('a, 'b) factor \<Rightarrow> bool"
--- a/src/HOL/BNF_LFP.thy Thu Feb 27 21:31:58 2014 +0100
+++ b/src/HOL/BNF_LFP.thy Thu Feb 27 21:36:40 2014 +0100
@@ -236,6 +236,9 @@
lemma id_transfer: "fun_rel A A id id"
unfolding fun_rel_def by simp
+lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
+ by simp
+
ML_file "Tools/BNF/bnf_lfp_util.ML"
ML_file "Tools/BNF/bnf_lfp_tactics.ML"
ML_file "Tools/BNF/bnf_lfp.ML"
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Feb 27 21:31:58 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Feb 27 21:36:40 2014 +0100
@@ -925,17 +925,10 @@
by (rule subspace_setsum, rule subspace_span)
lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
- apply (auto simp only: span_add span_sub)
- apply (subgoal_tac "(x + y) - x \<in> span S")
- apply simp
- apply (simp only: span_add span_sub)
- done
+ by (metis add_minus_cancel scaleR_minus1_left subspace_def subspace_span)
text {* Mapping under linear image. *}
-lemma image_subset_iff_subset_vimage: "f ` A \<subseteq> B \<longleftrightarrow> A \<subseteq> f -` B"
- by auto (* TODO: move *)
-
lemma span_linear_image:
assumes lf: "linear f"
shows "span (f ` S) = f ` (span S)"
@@ -1271,29 +1264,13 @@
assume i: ?rhs
show ?lhs
using i False
- apply simp
apply (auto simp add: dependent_def)
- apply (case_tac "aa = a")
- apply auto
- apply (subgoal_tac "insert a S - {aa} = insert a (S - {aa})")
- apply simp
- apply (subgoal_tac "a \<in> span (insert aa (S - {aa}))")
- apply (subgoal_tac "insert aa (S - {aa}) = S")
- apply simp
- apply blast
- apply (rule in_span_insert)
- apply assumption
- apply blast
- apply blast
- done
+ by (metis in_span_insert insert_Diff insert_Diff_if insert_iff)
qed
qed
text {* The degenerate case of the Exchange Lemma. *}
-lemma mem_delete: "x \<in> (A - {a}) \<longleftrightarrow> x \<noteq> a \<and> x \<in> A"
- by blast
-
lemma spanning_subset_independent:
assumes BA: "B \<subseteq> A"
and iA: "independent A"
@@ -1345,23 +1322,16 @@
let ?P = "\<lambda>t'. card t' = card t \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
let ?ths = "\<exists>t'. ?P t'"
{
- assume st: "s \<subseteq> t"
- from st ft span_mono[OF st]
- have ?ths
- apply -
- apply (rule exI[where x=t])
- apply (auto intro: span_superset)
- done
+ assume "s \<subseteq> t"
+ then have ?ths
+ by (metis ft Un_commute sp sup_ge1)
}
moreover
{
assume st: "t \<subseteq> s"
from spanning_subset_independent[OF st s sp] st ft span_mono[OF st]
have ?ths
- apply -
- apply (rule exI[where x=t])
- apply (auto intro: span_superset)
- done
+ by (metis Un_absorb sp)
}
moreover
{
@@ -3099,12 +3069,7 @@
unfolding scaleR_scaleR
unfolding norm_scaleR
apply (subgoal_tac "norm x * c = \<bar>c\<bar> * norm x \<or> norm x * c = - \<bar>c\<bar> * norm x")
- apply (case_tac "c \<le> 0", simp add: field_simps)
- apply (simp add: field_simps)
- apply (case_tac "c \<le> 0", simp add: field_simps)
- apply (simp add: field_simps)
- apply simp
- apply simp
+ apply (auto simp add: field_simps)
done
end
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Feb 27 21:31:58 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Feb 27 21:36:40 2014 +0100
@@ -569,10 +569,7 @@
fix K
assume K: "K \<subseteq> Collect ?L"
have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)"
- apply (rule set_eqI)
- apply (simp add: Ball_def image_iff)
- apply metis
- done
+ by blast
from K[unfolded th0 subset_image_iff]
obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk"
by blast
@@ -595,21 +592,11 @@
lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)"
unfolding closedin_def topspace_subtopology
- apply (simp add: openin_subtopology)
- apply (rule iffI)
- apply clarify
- apply (rule_tac x="topspace U - T" in exI)
- apply auto
- done
+ by (auto simp add: openin_subtopology)
lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U"
unfolding openin_subtopology
- apply (rule iffI, clarify)
- apply (frule openin_subset[of U])
- apply blast
- apply (rule exI[where x="topspace U"])
- apply auto
- done
+ by auto (metis IntD1 in_mono openin_subset)
lemma subtopology_superset:
assumes UV: "topspace U \<subseteq> V"
@@ -695,11 +682,7 @@
lemma closed_closedin_trans:
"closed S \<Longrightarrow> closed T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> closedin (subtopology euclidean S) T"
- apply (subgoal_tac "S \<inter> T = T" )
- apply auto
- apply (frule closedin_closed_Int[of T S])
- apply simp
- done
+ by (metis closedin_closed inf.absorb2)
lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
by (auto simp add: closedin_closed)
@@ -720,16 +703,10 @@
apply clarsimp
apply (rule_tac x="d - dist x a" in exI)
apply (clarsimp simp add: less_diff_eq)
- apply (erule rev_bexI)
- apply (rule_tac x=d in exI, clarify)
- apply (erule le_less_trans [OF dist_triangle])
- done
+ by (metis dist_commute dist_triangle_lt)
assume ?rhs then have 2: "S = U \<inter> T"
- unfolding T_def
- apply auto
- apply (drule (1) bspec, erule rev_bexI)
- apply auto
- done
+ unfolding T_def
+ by auto (metis dist_self)
from 1 2 show ?lhs
unfolding openin_open open_dist by fast
qed
@@ -811,12 +788,6 @@
"a - b \<ge> c \<longleftrightarrow> a \<ge> c + b"
by arith+
-lemma open_vimage: (* TODO: move to Topological_Spaces.thy *)
- assumes "open s" and "continuous_on UNIV f"
- shows "open (vimage f s)"
- using assms unfolding continuous_on_open_vimage [OF open_UNIV]
- by simp
-
lemma open_ball [intro, simp]: "open (ball x e)"
proof -
have "open (dist x -` {..<e})"
@@ -955,9 +926,7 @@
e1 \<noteq> {} \<and>
e2 \<noteq> {})"
unfolding connected_def openin_open
- apply safe
- apply blast+
- done
+ by blast
lemma exists_diff:
fixes P :: "'a set \<Rightarrow> bool"
@@ -984,9 +953,7 @@
have "\<not> connected S \<longleftrightarrow>
(\<exists>e1 e2. open e1 \<and> open (- e2) \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
unfolding connected_def openin_open closedin_closed
- apply (subst exists_diff)
- apply blast
- done
+ by (metis double_complement)
then have th0: "connected S \<longleftrightarrow>
\<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
(is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)")
@@ -1430,13 +1397,8 @@
next
assume "\<not> a islimpt S"
then show "trivial_limit (at a within S)"
- unfolding trivial_limit_def
- unfolding eventually_at_topological
- unfolding islimpt_def
- apply clarsimp
- apply (rule_tac x=T in exI)
- apply auto
- done
+ unfolding trivial_limit_def eventually_at_topological islimpt_def
+ by metis
qed
lemma trivial_limit_at_iff: "trivial_limit (at a) \<longleftrightarrow> \<not> a islimpt UNIV"
@@ -1926,9 +1888,7 @@
lemma closed_sequential_limits:
fixes S :: "'a::first_countable_topology set"
shows "closed S \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially \<longrightarrow> l \<in> S)"
- using closure_sequential [where 'a='a] closure_closed [where 'a='a]
- closed_limpt [where 'a='a] islimpt_sequential [where 'a='a] mem_delete [where 'a='a]
- by metis
+by (metis closure_sequential closure_subset_eq subset_iff)
lemma closure_approachable:
fixes S :: "'a::metric_space set"
@@ -2483,13 +2443,7 @@
lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
unfolding bounded_def
- apply safe
- apply (rule_tac x="dist a x + e" in exI)
- apply clarify
- apply (drule (1) bspec)
- apply (erule order_trans [OF dist_triangle add_left_mono])
- apply auto
- done
+ by auto (metis add_commute add_le_cancel_right dist_commute dist_triangle_le)
lemma bounded_iff: "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. norm x \<le> a)"
unfolding bounded_any_center [where a=0]
@@ -2499,10 +2453,7 @@
assumes "\<forall>x\<in>s. abs (x::real) \<le> B"
shows "bounded s"
unfolding bounded_def dist_real_def
- apply (rule_tac x=0 in exI)
- using assms
- apply auto
- done
+ by (metis abs_minus_commute assms diff_0_right)
lemma bounded_empty [simp]: "bounded {}"
by (simp add: bounded_def)
@@ -2550,17 +2501,7 @@
lemma bounded_Un[simp]: "bounded (S \<union> T) \<longleftrightarrow> bounded S \<and> bounded T"
apply (auto simp add: bounded_def)
- apply (rename_tac x y r s)
- apply (rule_tac x=x in exI)
- apply (rule_tac x="max r (dist x y + s)" in exI)
- apply (rule ballI)
- apply safe
- apply (drule (1) bspec)
- apply simp
- apply (drule (1) bspec)
- apply (rule max.coboundedI2)
- apply (erule order_trans [OF dist_triangle add_left_mono])
- done
+ by (metis Un_iff add_le_cancel_left dist_triangle le_max_iff_disj max.order_iff)
lemma bounded_Union[intro]: "finite F \<Longrightarrow> \<forall>S\<in>F. bounded S \<Longrightarrow> bounded (\<Union>F)"
by (induct rule: finite_induct[of F]) auto
@@ -3847,25 +3788,11 @@
lemma bounded_fst: "bounded s \<Longrightarrow> bounded (fst ` s)"
unfolding bounded_def
- apply clarify
- apply (rule_tac x="a" in exI)
- apply (rule_tac x="e" in exI)
- apply clarsimp
- apply (drule (1) bspec)
- apply (simp add: dist_Pair_Pair)
- apply (erule order_trans [OF real_sqrt_sum_squares_ge1])
- done
+ by (metis (erased, hide_lams) dist_fst_le image_iff order_trans)
lemma bounded_snd: "bounded s \<Longrightarrow> bounded (snd ` s)"
unfolding bounded_def
- apply clarify
- apply (rule_tac x="b" in exI)
- apply (rule_tac x="e" in exI)
- apply clarsimp
- apply (drule (1) bspec)
- apply (simp add: dist_Pair_Pair)
- apply (erule order_trans [OF real_sqrt_sum_squares_ge2])
- done
+ by (metis (no_types, hide_lams) dist_snd_le image_iff order.trans)
instance prod :: (heine_borel, heine_borel) heine_borel
proof
@@ -3916,7 +3843,6 @@
using assms unfolding compact_def by blast
note lr' = seq_suble [OF lr(2)]
-
{
fix e :: real
assume "e > 0"
@@ -4434,10 +4360,8 @@
"continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s. dist x' x < d --> dist (f x') (f x) < e)"
unfolding continuous_within and Lim_within
apply auto
- unfolding dist_nz[symmetric]
- apply (auto del: allE elim!:allE)
- apply(rule_tac x=d in exI)
- apply auto
+ apply (metis dist_nz dist_self)
+ apply blast
done
lemma continuous_at_eps_delta:
@@ -4521,11 +4445,7 @@
"continuous_on s f \<longleftrightarrow>
(\<forall>x\<in>s. \<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
unfolding continuous_on_def Lim_within
- apply (intro ball_cong [OF refl] all_cong ex_cong)
- apply (rename_tac y, case_tac "y = x")
- apply simp
- apply (simp add: dist_nz)
- done
+ by (metis dist_pos_lt dist_self)
definition uniformly_continuous_on :: "'a set \<Rightarrow> ('a::metric_space \<Rightarrow> 'b::metric_space) \<Rightarrow> bool"
where "uniformly_continuous_on s f \<longleftrightarrow>
@@ -4552,10 +4472,7 @@
lemma continuous_on_interior:
"continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
- apply (erule interiorE)
- apply (drule (1) continuous_on_subset)
- apply (simp add: continuous_on_eq_continuous_at)
- done
+ by (metis continuous_on_eq_continuous_at continuous_on_subset interiorE)
lemma continuous_on_eq:
"(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
--- a/src/HOL/Set.thy Thu Feb 27 21:31:58 2014 +0100
+++ b/src/HOL/Set.thy Thu Feb 27 21:36:40 2014 +0100
@@ -1763,6 +1763,9 @@
lemma image_vimage_eq [simp]: "f ` (f -` A) = A Int range f"
by blast
+lemma image_subset_iff_subset_vimage: "f ` A \<subseteq> B \<longleftrightarrow> A \<subseteq> f -` B"
+ by blast
+
lemma vimage_const [simp]: "((\<lambda>x. c) -` A) = (if c \<in> A then UNIV else {})"
by auto
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Feb 27 21:31:58 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Feb 27 21:36:40 2014 +0100
@@ -9,12 +9,14 @@
sig
type fp_sugar =
{T: typ,
+ X: typ,
fp: BNF_Util.fp_kind,
fp_res_index: int,
fp_res: BNF_FP_Util.fp_result,
pre_bnf: BNF_Def.bnf,
nested_bnfs: BNF_Def.bnf list,
nesting_bnfs: BNF_Def.bnf list,
+ ctrXs_Tss: typ list list,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
co_iters: term list,
@@ -61,9 +63,8 @@
* (string * term list * term list list
* ((term list list * term list list list) * typ list) list) option)
* Proof.context
- val mk_coiter_fun_arg_types: typ list list list -> typ list -> int list -> term ->
- typ list list
- * (typ list list list list * typ list list list * typ list list list list * typ list)
+ val repair_nullary_single_ctr: typ list list -> typ list list
+ val mk_coiter_p_pred_types: typ list -> int list -> typ list list
val define_iters: string list ->
(typ list list * typ list list list list * term list list * term list list list list) list ->
(string -> binding) -> typ list -> typ list -> term list -> Proof.context ->
@@ -115,12 +116,14 @@
type fp_sugar =
{T: typ,
+ X: typ,
fp: fp_kind,
fp_res_index: int,
fp_res: fp_result,
pre_bnf: bnf,
nested_bnfs: bnf list,
nesting_bnfs: bnf list,
+ ctrXs_Tss: typ list list,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
co_iters: term list,
@@ -131,16 +134,18 @@
disc_co_iterss: thm list list,
sel_co_itersss: thm list list list};
-fun morph_fp_sugar phi ({T, fp, fp_res, fp_res_index, pre_bnf, nested_bnfs, nesting_bnfs, ctr_defs,
- ctr_sugar, co_iters, maps, common_co_inducts, co_inducts, co_iter_thmss, disc_co_iterss,
- sel_co_itersss} : fp_sugar) =
+fun morph_fp_sugar phi ({T, X, fp, fp_res, fp_res_index, pre_bnf, nested_bnfs, nesting_bnfs,
+ ctrXs_Tss, ctr_defs, ctr_sugar, co_iters, maps, common_co_inducts, co_inducts, co_iter_thmss,
+ disc_co_iterss, sel_co_itersss} : fp_sugar) =
{T = Morphism.typ phi T,
+ X = Morphism.typ phi X,
fp = fp,
fp_res = morph_fp_result phi fp_res,
fp_res_index = fp_res_index,
pre_bnf = morph_bnf phi pre_bnf,
nested_bnfs = map (morph_bnf phi) nested_bnfs,
nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
+ ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
ctr_defs = map (Morphism.thm phi) ctr_defs,
ctr_sugar = morph_ctr_sugar phi ctr_sugar,
co_iters = map (Morphism.term phi) co_iters,
@@ -178,17 +183,17 @@
Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Data.map (Symtab.update (key, morph_fp_sugar phi fp_sugar)));
-fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss
- ctr_sugars co_iterss mapss common_co_inducts co_inductss co_iter_thmsss disc_co_itersss
- sel_co_iterssss lthy =
+fun register_fp_sugars Xs fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctrXs_Tsss
+ ctr_defss ctr_sugars co_iterss mapss common_co_inducts co_inductss co_iter_thmsss
+ disc_co_itersss sel_co_iterssss lthy =
(0, lthy)
|> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
- register_fp_sugar s {T = T, fp = fp, fp_res = fp_res, fp_res_index = kk,
+ register_fp_sugar s {T = T, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk,
pre_bnf = nth pre_bnfs kk, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs,
- ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk, co_iters = nth co_iterss kk,
- maps = nth mapss kk, common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk,
- co_iter_thmss = nth co_iter_thmsss kk, disc_co_iterss = nth disc_co_itersss kk,
- sel_co_itersss = nth sel_co_iterssss kk}
+ ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk,
+ co_iters = nth co_iterss kk, maps = nth mapss kk, common_co_inducts = common_co_inducts,
+ co_inducts = nth co_inductss kk, co_iter_thmss = nth co_iter_thmsss kk,
+ disc_co_iterss = nth disc_co_itersss kk, sel_co_itersss = nth sel_co_iterssss kk}
lthy)) Ts
|> snd;
@@ -381,13 +386,13 @@
([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy)
end;
+(*avoid "'a itself" arguments in coiterators*)
+fun repair_nullary_single_ctr [[]] = [[@{typ unit}]]
+ | repair_nullary_single_ctr Tss = Tss;
+
fun mk_coiter_fun_arg_types0 ctr_Tsss Cs ns fun_Ts =
let
- (*avoid "'a itself" arguments in coiterators*)
- fun repair_arity [[]] = [[@{typ unit}]]
- | repair_arity Tss = Tss;
-
- val ctr_Tsss' = map repair_arity ctr_Tsss;
+ val ctr_Tsss' = map repair_nullary_single_ctr ctr_Tsss;
val f_sum_prod_Ts = map range_type fun_Ts;
val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts;
val f_Tsss = map2 (map2 (dest_tupleT o length)) ctr_Tsss' f_prod_Tss;
@@ -400,10 +405,6 @@
fun mk_coiter_p_pred_types Cs ns = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
-fun mk_coiter_fun_arg_types ctr_Tsss Cs ns dtor_coiter =
- (mk_coiter_p_pred_types Cs ns,
- mk_coiter_fun_arg_types0 ctr_Tsss Cs ns (binder_fun_types (fastype_of dtor_coiter)));
-
fun mk_coiters_args_types ctr_Tsss Cs ns dtor_coiter_fun_Tss lthy =
let
val p_Tss = mk_coiter_p_pred_types Cs ns;
@@ -1385,9 +1386,9 @@
|> Spec_Rules.add Spec_Rules.Equational (map un_fold_of iterss, flat fold_thmss)
|> Spec_Rules.add Spec_Rules.Equational (map co_rec_of iterss, flat rec_thmss)
|> Local_Theory.notes (common_notes @ notes) |> snd
- |> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars
- iterss mapss [induct_thm] (map single induct_thms) (transpose [fold_thmss, rec_thmss])
- (replicate nn []) (replicate nn [])
+ |> register_fp_sugars Xs Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctrXs_Tsss
+ ctr_defss ctr_sugars iterss mapss [induct_thm] (map single induct_thms)
+ (transpose [fold_thmss, rec_thmss]) (replicate nn []) (replicate nn [])
end;
fun derive_note_coinduct_coiters_thms_for_types
@@ -1450,8 +1451,8 @@
|> add_spec_rules un_fold_of sel_unfold_thmss unfold_thmss
|> add_spec_rules co_rec_of sel_corec_thmss corec_thmss
|> Local_Theory.notes (common_notes @ notes) |> snd
- |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss
- ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]
+ |> register_fp_sugars Xs Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctrXs_Tsss
+ ctr_defss ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]
(transpose [coinduct_thms, strong_coinduct_thms])
(transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss])
(transpose [sel_unfold_thmsss, sel_corec_thmsss])
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Feb 27 21:31:58 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Feb 27 21:36:40 2014 +0100
@@ -10,12 +10,12 @@
val unfold_lets_splits: term -> term
val dest_map: Proof.context -> string -> term -> term * term list
- val mutualize_fp_sugars: BNF_Util.fp_kind -> binding list -> typ list -> (term -> int list) ->
+ val mutualize_fp_sugars: BNF_Util.fp_kind -> binding list -> typ list -> term list ->
term list list list list -> BNF_FP_Def_Sugar.fp_sugar list -> local_theory ->
(BNF_FP_Def_Sugar.fp_sugar list
* (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
* local_theory
- val nested_to_mutual_fps: BNF_Util.fp_kind -> binding list -> typ list -> (term -> int list) ->
+ val nested_to_mutual_fps: BNF_Util.fp_kind -> binding list -> typ list -> term list ->
(term * term list list) list list -> local_theory ->
(typ list * int list * BNF_FP_Def_Sugar.fp_sugar list
* (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
@@ -103,8 +103,13 @@
fun key_of_fp_eqs fp fpTs fp_eqs =
Type (fp_case fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs);
+fun get_indices callers t =
+ callers
+ |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
+ |> map_filter I;
+
(* TODO: test with sort constraints on As *)
-fun mutualize_fp_sugars fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 =
+fun mutualize_fp_sugars fp bs fpTs callers callssss fp_sugars0 no_defs_lthy0 =
let
val thy = Proof_Context.theory_of no_defs_lthy0;
@@ -112,6 +117,8 @@
fun incompatible_calls ts =
error ("Incompatible " ^ co_prefix fp ^ "recursive calls: " ^ commas (map qsotm ts));
+ fun mutual_self_call caller t =
+ error ("Unsupported mutual self-call " ^ qsotm t ^ " from " ^ qsotm caller);
fun nested_self_call t =
error ("Unsupported nested self-call " ^ qsotm t);
@@ -146,7 +153,7 @@
||>> variant_tfrees fp_b_names;
fun check_call_dead live_call call =
- if null (get_indices call) then () else incompatible_calls [live_call, call];
+ if null (get_indices callers call) then () else incompatible_calls [live_call, call];
fun freeze_fpTs_type_based_default (T as Type (s, Ts)) =
(case filter (curry (op =) T o snd) (map_index I fpTs) of
@@ -154,31 +161,36 @@
| _ => Type (s, map freeze_fpTs_type_based_default Ts))
| freeze_fpTs_type_based_default T = T;
- fun freeze_fpTs_mutual_call calls T =
- (case fold (union (op =)) (map get_indices calls) [] of
- [] => freeze_fpTs_type_based_default T
- | [kk] => nth Xs kk
+ fun freeze_fpTs_mutual_call kk fpT calls T =
+ (case fold (union (op =)) (map (get_indices callers) calls) [] of
+ [] => if T = fpT then nth Xs kk else freeze_fpTs_type_based_default T
+ | [kk'] =>
+ if T = fpT andalso kk' <> kk then
+ mutual_self_call (nth callers kk)
+ (the (find_first (not o null o get_indices callers) calls))
+ else
+ nth Xs kk'
| _ => incompatible_calls calls);
- fun freeze_fpTs_map (fpT as Type (_, Ts')) (callss, (live_call :: _, dead_calls))
+ fun freeze_fpTs_map kk (fpT as Type (_, Ts')) (callss, (live_call :: _, dead_calls))
(Type (s, Ts)) =
if Ts' = Ts then
nested_self_call live_call
else
(List.app (check_call_dead live_call) dead_calls;
- Type (s, map2 (freeze_fpTs_call fpT)
+ Type (s, map2 (freeze_fpTs_call kk fpT)
(flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) [] (transpose callss)) Ts))
- and freeze_fpTs_call fpT calls (T as Type (s, _)) =
+ and freeze_fpTs_call kk fpT calls (T as Type (s, _)) =
(case map_partition (try (snd o dest_map no_defs_lthy s)) calls of
([], _) =>
(case map_partition (try (snd o dest_abs_or_applied_map no_defs_lthy s)) calls of
- ([], _) => freeze_fpTs_mutual_call calls T
- | callsp => freeze_fpTs_map fpT callsp T)
- | callsp => freeze_fpTs_map fpT callsp T)
- | freeze_fpTs_call _ _ T = T;
+ ([], _) => freeze_fpTs_mutual_call kk fpT calls T
+ | callsp => freeze_fpTs_map kk fpT callsp T)
+ | callsp => freeze_fpTs_map kk fpT callsp T)
+ | freeze_fpTs_call _ _ _ T = T;
val ctr_Tsss = map (map binder_types) ctr_Tss;
- val ctrXs_Tsss = map3 (map2 o map2 o freeze_fpTs_call) fpTs callssss ctr_Tsss;
+ val ctrXs_Tsss = map4 (map2 o map2 oo freeze_fpTs_call) kks fpTs callssss ctr_Tsss;
val ctrXs_sum_prod_Ts = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctrXs_Tsss;
val ns = map length ctr_Tsss;
@@ -254,11 +266,12 @@
val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
- fun mk_target_fp_sugar T kk pre_bnf ctr_defs ctr_sugar co_iters maps co_inducts un_fold_thms
- co_rec_thms disc_unfold_thms disc_corec_thms sel_unfold_thmss sel_corec_thmss =
- {T = T, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf,
- nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, ctr_defs = ctr_defs,
- ctr_sugar = ctr_sugar, co_iters = co_iters, maps = maps,
+ fun mk_target_fp_sugar T X kk pre_bnf ctrXs_Tss ctr_defs ctr_sugar co_iters maps co_inducts
+ un_fold_thms co_rec_thms disc_unfold_thms disc_corec_thms sel_unfold_thmss
+ sel_corec_thmss =
+ {T = T, X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf,
+ nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, ctrXs_Tss = ctrXs_Tss,
+ ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_iters = co_iters, maps = maps,
common_co_inducts = common_co_inducts, co_inducts = co_inducts,
co_iter_thmss = [un_fold_thms, co_rec_thms],
disc_co_iterss = [disc_unfold_thms, disc_corec_thms],
@@ -266,9 +279,9 @@
|> morph_fp_sugar phi;
val target_fp_sugars =
- map14 mk_target_fp_sugar fpTs kks pre_bnfs ctr_defss ctr_sugars co_iterss mapss
- (transpose co_inductss) un_fold_thmss co_rec_thmss disc_unfold_thmss disc_corec_thmss
- sel_unfold_thmsss sel_corec_thmsss;
+ map16 mk_target_fp_sugar fpTs Xs kks pre_bnfs ctrXs_Tsss ctr_defss ctr_sugars co_iterss
+ mapss (transpose co_inductss) un_fold_thmss co_rec_thmss disc_unfold_thmss
+ disc_corec_thmss sel_unfold_thmsss sel_corec_thmsss;
val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
in
@@ -292,7 +305,9 @@
f (T, U) #> (if s = s' then fold (fold_subtype_pairs f) (Ts ~~ Us) else I)
| fold_subtype_pairs f TU = f TU;
-fun nested_to_mutual_fps fp actual_bs actual_Ts get_indices actual_callssss0 lthy =
+val impossible_caller = Bound ~1;
+
+fun nested_to_mutual_fps fp actual_bs actual_Ts actual_callers actual_callssss0 lthy =
let
val qsoty = quote o Syntax.string_of_typ lthy;
val qsotys = space_implode " or " o map qsoty;
@@ -391,23 +406,23 @@
val common_name = mk_common_name (map Binding.name_of actual_bs);
val bs = pad_list (Binding.name common_name) nn actual_bs;
+ val callers = pad_list impossible_caller nn actual_callers;
fun permute xs = permute_like (op =) Ts perm_Ts xs;
fun unpermute perm_xs = permute_like (op =) perm_Ts Ts perm_xs;
val perm_bs = permute bs;
+ val perm_callers = permute callers;
val perm_kks = permute kks;
val perm_callssss0 = permute callssss0;
val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts;
val perm_callssss = map2 (indexify_callsss o #ctrs o #ctr_sugar) perm_fp_sugars0 perm_callssss0;
- val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
-
val ((perm_fp_sugars, fp_sugar_thms), lthy) =
if num_groups > 1 then
- mutualize_fp_sugars fp perm_bs perm_frozen_gen_Ts get_perm_indices perm_callssss
- perm_fp_sugars0 lthy
+ mutualize_fp_sugars fp perm_bs perm_frozen_gen_Ts perm_callers perm_callssss perm_fp_sugars0
+ lthy
else
((perm_fp_sugars0, (NONE, NONE)), lthy);
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Thu Feb 27 21:31:58 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Thu Feb 27 21:36:40 2014 +0100
@@ -38,7 +38,6 @@
val mk_compN: int -> typ list -> term * term -> term
val mk_comp: typ list -> term * term -> term
- val get_free_indices: ((binding * typ) * 'a) list -> term -> int list
val mk_co_iter: theory -> fp_kind -> typ -> typ list -> term -> term
val mk_conjunctN: int -> int -> thm
@@ -109,10 +108,6 @@
val mk_comp = mk_compN 1;
-fun get_free_indices fixes t = map (fst #>> Binding.name_of #> Free) fixes
- |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE)
- |> map_filter I;
-
fun mk_co_iter thy fp fpT Cs t =
let
val ((f_Cs, prebody), body) = strip_type (fastype_of t) |>> split_last;
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Feb 27 21:31:58 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Feb 27 21:36:40 2014 +0100
@@ -966,10 +966,10 @@
val sum_card_order = mk_sum_card_order bd_card_orders;
- val sbd_ordIso = fold_thms lthy [sbd_def]
- (@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order]);
- val sbd_card_order = fold_thms lthy [sbd_def]
- (@{thm card_order_dir_image} OF [Abs_sbdT_bij, sum_card_order]);
+ val sbd_ordIso = @{thm ssubst_Pair_rhs} OF
+ [@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order], sbd_def];
+ val sbd_card_order = @{thm iffD2[OF arg_cong[of _ _ card_order]]} OF
+ [sbd_def, @{thm card_order_dir_image} OF [Abs_sbdT_bij, sum_card_order]];
val sbd_Cinfinite = @{thm Cinfinite_cong} OF [sbd_ordIso, sum_Cinfinite];
val sbd_Card_order = sbd_Cinfinite RS conjunct2;
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Feb 27 21:31:58 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Feb 27 21:36:40 2014 +0100
@@ -370,33 +370,44 @@
(case fp_sugar_of ctxt s of SOME {maps, ...} => maps | NONE => [])
| map_thms_of_typ _ _ = [];
-fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 =
+fun corec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 =
let
val thy = Proof_Context.theory_of lthy0;
- val ((missing_res_Ts, perm0_kks,
- fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
- common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
- nested_to_mutual_fps Greatest_FP bs res_Ts get_indices callssss0 lthy0;
+ val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs, co_iters = coiter1 :: _,
+ common_co_inducts = common_coinduct_thms, ...} :: _,
+ (_, gfp_sugar_thms)), lthy) =
+ nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0;
val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars;
val indices = map #fp_res_index fp_sugars;
val perm_indices = map #fp_res_index perm_fp_sugars;
- val perm_ctrss = map (#ctrs o #ctr_sugar) perm_fp_sugars;
- val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
- val perm_gfpTs = map (body_type o fastype_of o hd) perm_ctrss;
+ val perm_gfpTs = map #T perm_fp_sugars;
+ val perm_ctrXs_Tsss' = map (repair_nullary_single_ctr o #ctrXs_Tss) perm_fp_sugars;
val nn0 = length res_Ts;
val nn = length perm_gfpTs;
val kks = 0 upto nn - 1;
- val perm_ns = map length perm_ctr_Tsss;
+ val perm_ns' = map length perm_ctrXs_Tsss';
+
+ val perm_Ts = map #T perm_fp_sugars;
+ val perm_Xs = map #X perm_fp_sugars;
+ val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o #co_iters) perm_fp_sugars;
+ val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs);
- val perm_Cs = map (fn {fp_res, fp_res_index, ...} => domain_type (body_fun_type (fastype_of
- (co_rec_of (nth (#xtor_co_iterss fp_res) fp_res_index))))) perm_fp_sugars;
- val (perm_p_Tss, (perm_q_Tssss, _, perm_f_Tssss, _)) =
- mk_coiter_fun_arg_types perm_ctr_Tsss perm_Cs perm_ns (co_rec_of dtor_coiters1);
+ fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)]
+ | zip_corecT U =
+ (case AList.lookup (op =) Xs_TCs U of
+ SOME (T, C) => [T, C]
+ | NONE => [U]);
+
+ val perm_p_Tss = mk_coiter_p_pred_types perm_Cs perm_ns';
+ val perm_f_Tssss =
+ map2 (fn C => map (map (map (curry (op -->) C) o zip_corecT))) perm_Cs perm_ctrXs_Tsss';
+ val perm_q_Tssss =
+ map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) perm_f_Tssss;
val (perm_p_hss, h) = indexedd perm_p_Tss 0;
val (perm_q_hssss, h') = indexedddd perm_q_Tssss h;
@@ -915,7 +926,8 @@
val fun_names = map Binding.name_of bs;
val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts;
- val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =));
+ val frees = map (fst #>> Binding.name_of #> Free) fixes;
+ val has_call = exists_subterm (member (op =) frees);
val eqns_data =
fold_map2 (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss) (tag_list 0 (map snd specs))
of_specs_opt []
@@ -936,7 +948,7 @@
val ((n2m, corec_specs', _, coinduct_thm, strong_coinduct_thm, coinduct_thms,
strong_coinduct_thms), lthy') =
- corec_specs_of bs arg_Ts res_Ts (get_free_indices fixes) callssss lthy;
+ corec_specs_of bs arg_Ts res_Ts frees callssss lthy;
val corec_specs = take actual_nn corec_specs';
val ctr_specss = map #ctr_specs corec_specs;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Feb 27 21:31:58 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Feb 27 21:36:40 2014 +0100
@@ -82,6 +82,7 @@
fun mk_FTs Ts = map2 (fn Ds => mk_T_of_bnf Ds Ts) Dss bnfs;
val (params, params') = `(map Term.dest_TFree) (mk_params passiveAs);
+ val (dead_params, dead_params') = `(map Term.dest_TFree) (subtract (op =) passiveAs params');
val FTsAs = mk_FTs allAs;
val FTsBs = mk_FTs allBs;
val FTsCs = mk_FTs allCs;
@@ -159,7 +160,6 @@
val bd_Cinfinites = map (fn thm => thm RS @{thm Cinfinite_csum1}) bd0_Cinfinites;
val bd_Cnotzeros = map (fn thm => thm RS @{thm Cinfinite_Cnotzero}) bd_Cinfinites;
val bd_Cinfinite = hd bd_Cinfinites;
- val bd_Cnotzero = hd bd_Cnotzeros;
val set_bdss =
map2 (fn set_bd0s => fn bd0_Card_order =>
map (fn thm => ctrans OF [thm, bd0_Card_order RS @{thm ordLeq_csum1}]) set_bd0s)
@@ -552,32 +552,87 @@
(* bounds *)
- val sum_Card_order = if n = 1 then bd_Card_order else @{thm Card_order_csum};
- val sum_Cnotzero = if n = 1 then bd_Cnotzero else bd_Cnotzero RS @{thm csum_Cnotzero1};
- val sum_Cinfinite = if n = 1 then bd_Cinfinite else bd_Cinfinite RS @{thm Cinfinite_csum1};
- fun mk_set_bd_sums i bd_Card_order bds =
- if n = 1 then bds
- else map (fn thm => bd_Card_order RS mk_ordLeq_csum n i thm) bds;
- val set_bd_sumss = map3 mk_set_bd_sums ks bd_Card_orders set_bdss;
+ val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
+ val sum_bdT = fst (dest_relT (fastype_of sum_bd));
+
+ val (lthy, sbd, sbd_card_order, sbd_Cinfinite, sbd_Card_order, set_sbdss, in_sbds) =
+ if n = 1
+ then (lthy, sum_bd, hd bd_card_orders, bd_Cinfinite, bd_Card_order, set_bdss, in_bds)
+ else
+ let
+ val sbdT_bind = mk_internal_b sum_bdTN;
+
+ val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
+ typedef (sbdT_bind, dead_params, NoSyn)
+ (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
+
+ val sbdT = Type (sbdT_name, dead_params');
+ val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);
+
+ val sbd_bind = mk_internal_b sum_bdN;
+ val sbd_def_bind = (Thm.def_binding sbd_bind, []);
+
+ val sbd_spec = mk_dir_image sum_bd Abs_sbdT;
+
+ val ((sbd_free, (_, sbd_def_free)), (lthy, lthy_old)) =
+ lthy
+ |> Local_Theory.define ((sbd_bind, NoSyn), (sbd_def_bind, sbd_spec))
+ ||> `Local_Theory.restore;
+
+ val phi = Proof_Context.export_morphism lthy_old lthy;
+
+ val sbd_def = Morphism.thm phi sbd_def_free RS meta_eq_to_obj_eq;
+ val sbd = Const (fst (Term.dest_Const (Morphism.term phi sbd_free)), mk_relT (`I sbdT));
+
+ val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
+ val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info);
- fun mk_in_bd_sum i Co Cnz bd =
- if n = 1 then bd
- else Cnz RS ((Co RS mk_ordLeq_csum n i (Co RS @{thm ordLeq_refl})) RS
- (bd RS @{thm ordLeq_transitive[OF _ cexp_mono2_Cnotzero[OF _ Card_order_csum]]}));
- val in_bd_sums = map4 mk_in_bd_sum ks bd_Card_orders bd_Cnotzeros in_bds;
+ fun mk_sum_Cinfinite [thm] = thm
+ | mk_sum_Cinfinite (thm :: thms) =
+ @{thm Cinfinite_csum_strong} OF [thm, mk_sum_Cinfinite thms];
+
+ val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites;
+ val sum_Card_order = sum_Cinfinite RS conjunct2;
+
+ fun mk_sum_card_order [thm] = thm
+ | mk_sum_card_order (thm :: thms) =
+ @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
+
+ val sum_card_order = mk_sum_card_order bd_card_orders;
+
+ val sbd_ordIso = @{thm ssubst_Pair_rhs} OF
+ [@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order], sbd_def];
+ val sbd_Cinfinite = @{thm Cinfinite_cong} OF [sbd_ordIso, sum_Cinfinite];
+ val sbd_Card_order = sbd_Cinfinite RS conjunct2;
- val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
- val suc_bd = mk_cardSuc sum_bd;
+ val sbd_card_order = @{thm iffD2[OF arg_cong[of _ _ card_order]]} OF
+ [sbd_def, @{thm card_order_dir_image} OF [Abs_sbdT_bij, sum_card_order]];
+
+ fun mk_set_sbd i bd_Card_order bds =
+ map (fn thm => @{thm ordLeq_ordIso_trans} OF
+ [bd_Card_order RS mk_ordLeq_csum n i thm, sbd_ordIso]) bds;
+ val set_sbdss = map3 mk_set_sbd ks bd_Card_orders set_bdss;
+
+ fun mk_in_bd_sum i Co Cnz bd =
+ Cnz RS ((@{thm ordLeq_ordIso_trans} OF
+ [Co RS mk_ordLeq_csum n i (Co RS @{thm ordLeq_refl}), sbd_ordIso]) RS
+ (bd RS @{thm ordLeq_transitive[OF _ cexp_mono2_Cnotzero[OF _ Card_order_csum]]}));
+ val in_sbds = map4 mk_in_bd_sum ks bd_Card_orders bd_Cnotzeros in_bds;
+ in
+ (lthy, sbd, sbd_card_order, sbd_Cinfinite, sbd_Card_order, set_sbdss, in_sbds)
+ end;
+
+ val sbd_Cnotzero = sbd_Cinfinite RS @{thm Cinfinite_Cnotzero};
+ val suc_bd = mk_cardSuc sbd;
+
val field_suc_bd = mk_Field suc_bd;
val suc_bdT = fst (dest_relT (fastype_of suc_bd));
fun mk_Asuc_bd [] = mk_cexp ctwo suc_bd
| mk_Asuc_bd As =
mk_cexp (mk_csum (Library.foldr1 (uncurry mk_csum) (map mk_card_of As)) ctwo) suc_bd;
- val suc_bd_Card_order = if n = 1 then bd_Card_order RS @{thm cardSuc_Card_order}
- else @{thm cardSuc_Card_order[OF Card_order_csum]};
- val suc_bd_Cinfinite = if n = 1 then bd_Cinfinite RS @{thm Cinfinite_cardSuc}
- else bd_Cinfinite RS @{thm Cinfinite_cardSuc[OF Cinfinite_csum1]};
+ val suc_bd_Card_order = sbd_Card_order RS @{thm cardSuc_Card_order};
+ val suc_bd_Cinfinite = sbd_Cinfinite RS @{thm Cinfinite_cardSuc};
val suc_bd_Cnotzero = suc_bd_Cinfinite RS @{thm Cinfinite_Cnotzero};
val suc_bd_worel = suc_bd_Card_order RS @{thm Card_order_wo_rel}
val basis_Asuc = if m = 0 then @{thm ordLeq_refl[OF Card_order_ctwo]}
@@ -679,8 +734,8 @@
(Goal.prove_sorry lthy [] []
(HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, card_conjunction)))
(K (mk_min_algs_card_of_tac card_cT card_ct
- m suc_bd_worel min_algs_thms in_bd_sums
- sum_Card_order sum_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero
+ m suc_bd_worel min_algs_thms in_sbds
+ sbd_Card_order sbd_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero
suc_bd_Asuc_bd Asuc_bd_Cinfinite)))
|> Thm.close_derivation;
@@ -741,8 +796,8 @@
val goal = fold_rev Logic.all ss (HOLogic.mk_Trueprop (mk_alg min_algs ss));
val alg_min_alg = Goal.prove_sorry lthy [] [] goal
- (K (mk_alg_min_alg_tac m alg_def min_alg_defs suc_bd_limit_thm sum_Cinfinite
- set_bd_sumss min_algs_thms min_algs_mono_thms))
+ (K (mk_alg_min_alg_tac m alg_def min_alg_defs suc_bd_limit_thm sbd_Cinfinite
+ set_sbdss min_algs_thms min_algs_mono_thms))
|> Thm.close_derivation;
fun mk_card_of_thm min_alg def = Goal.prove_sorry lthy [] []
@@ -1438,7 +1493,7 @@
fn T => fn lthy =>
define_bnf_consts Dont_Inline (user_policy Note_Some lthy) (SOME deads)
map_b rel_b set_bs
- ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sum_bd), wits), NONE) lthy)
+ ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy)
bs map_bs rel_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy;
val (_, Iconsts, Iconst_defs, mk_Iconsts) = split_list4 Ibnf_consts;
@@ -1586,7 +1641,7 @@
let
fun mk_set_bd z bd set = mk_ordLeq (mk_card_of (set $ z)) bd;
- fun mk_cphi z set = certify lthy (Term.absfree (dest_Free z) (mk_set_bd z sum_bd set));
+ fun mk_cphi z set = certify lthy (Term.absfree (dest_Free z) (mk_set_bd z sbd set));
val cphiss = map (map2 mk_cphi Izs) Isetss_by_range;
@@ -1598,7 +1653,7 @@
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map3 mk_set_bd Izs Ibds sets))) Isetss_by_range;
- fun mk_tac ctxt induct = mk_set_bd_tac ctxt m (rtac induct) sum_Cinfinite set_bd_sumss;
+ fun mk_tac ctxt induct = mk_set_bd_tac ctxt m (rtac induct) sbd_Cinfinite set_sbdss;
val thms =
map4 (fn goal => fn ctor_sets => fn induct => fn i =>
singleton (Proof_Context.export names_lthy lthy)
@@ -1705,9 +1760,9 @@
val map_cong0_tacs = map (fn thm => fn ctxt => mk_map_cong0_tac ctxt m thm) Imap_cong0_thms;
val set_map0_tacss = map (map (K o mk_set_map0_tac)) (transpose Iset_Imap0_thmss);
val bd_co_tacs = replicate n (fn ctxt =>
- unfold_thms_tac ctxt Ibd_defs THEN mk_bd_card_order_tac bd_card_orders);
+ unfold_thms_tac ctxt Ibd_defs THEN rtac sbd_card_order 1);
val bd_cinf_tacs = replicate n (fn ctxt =>
- unfold_thms_tac ctxt Ibd_defs THEN rtac (sum_Cinfinite RS conjunct1) 1);
+ unfold_thms_tac ctxt Ibd_defs THEN rtac (sbd_Cinfinite RS conjunct1) 1);
val set_bd_tacss = map (map (fn thm => K (rtac thm 1))) (transpose Iset_bd_thmss);
val le_rel_OO_tacs = map (fn i =>
K ((rtac @{thm predicate2I} THEN' etac (le_Irel_OO_thm RS mk_conjunctN n i RS mp)) 1)) ks;
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Feb 27 21:31:58 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Feb 27 21:36:40 2014 +0100
@@ -99,8 +99,6 @@
| NONE => error ("Unsupported recursion via type constructor " ^ quote s ^
" not corresponding to new-style datatype (cf. \"datatype_new\")"));
- fun get_var_indices (Var ((_, kk), _)) = [kk];
-
val (Tparentss_kkssss, _) = nested_Tparentss_indicessss_of [] fpT1 0;
val Tparentss = map fst Tparentss_kkssss;
val Ts = map (fst o hd) Tparentss;
@@ -110,14 +108,6 @@
val ctrss0 = map (#ctrs o #ctr_sugar) fp_sugars0;
val ctr_Tsss0 = map (map (binder_types o fastype_of)) ctrss0;
- fun apply_comps n kk =
- mk_partial_compN n (replicate n @{typ unit} ---> @{typ unit})
- (Var ((Name.uu, kk), @{typ "unit => unit"}));
-
- val callssss =
- map2 (map2 (map2 (fn kks => fn ctr_T => map (apply_comps (num_binder_types ctr_T)) kks)))
- kkssss ctr_Tsss0;
-
val b_names = Name.variant_list [] (map base_name_of_typ Ts);
val compat_b_names = map (prefix compatN) b_names;
val compat_bs = map Binding.name compat_b_names;
@@ -126,9 +116,18 @@
val nn_fp = length fpTs;
val nn = length Ts;
+ val callers = map (fn kk => Var ((Name.uu, kk), @{typ "unit => unit"})) (0 upto nn - 1);
+
+ fun apply_comps n kk =
+ mk_partial_compN n (replicate n @{typ unit} ---> @{typ unit}) (nth callers kk);
+
+ val callssss =
+ map2 (map2 (map2 (fn kks => fn ctr_T => map (apply_comps (num_binder_types ctr_T)) kks)))
+ kkssss ctr_Tsss0;
+
val ((fp_sugars, (lfp_sugar_thms, _)), lthy) =
if nn > nn_fp then
- mutualize_fp_sugars Least_FP compat_bs Ts get_var_indices callssss fp_sugars0 lthy
+ mutualize_fp_sugars Least_FP compat_bs Ts callers callssss fp_sugars0 lthy
else
((fp_sugars0, (NONE, NONE)), lthy);
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Feb 27 21:31:58 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Feb 27 21:36:40 2014 +0100
@@ -21,9 +21,9 @@
type lfp_rec_extension =
{nested_simps: thm list,
is_new_datatype: Proof.context -> string -> bool,
- get_basic_lfp_sugars: binding list -> typ list -> (term -> int list) ->
- (term * term list list) list list -> local_theory ->
- typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory,
+ get_basic_lfp_sugars: binding list -> typ list -> term list ->
+ (term * term list list) list list -> local_theory ->
+ typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory,
rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
term -> term -> term -> term};
@@ -92,9 +92,9 @@
type lfp_rec_extension =
{nested_simps: thm list,
is_new_datatype: Proof.context -> string -> bool,
- get_basic_lfp_sugars: binding list -> typ list -> (term -> int list) ->
- (term * term list list) list list -> local_theory ->
- typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory,
+ get_basic_lfp_sugars: binding list -> typ list -> term list ->
+ (term * term list list) list list -> local_theory ->
+ typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory,
rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
term -> term -> term -> term};
@@ -118,22 +118,22 @@
SOME {is_new_datatype, ...} => is_new_datatype ctxt
| NONE => K false);
-fun get_basic_lfp_sugars bs arg_Ts get_indices callssss lthy =
+fun get_basic_lfp_sugars bs arg_Ts callers callssss lthy =
(case Data.get (Proof_Context.theory_of lthy) of
- SOME {get_basic_lfp_sugars, ...} => get_basic_lfp_sugars bs arg_Ts get_indices callssss lthy
- | NONE => error "Not implemented yet");
+ SOME {get_basic_lfp_sugars, ...} => get_basic_lfp_sugars bs arg_Ts callers callssss lthy
+ | NONE => error "Functionality not loaded yet");
fun rewrite_nested_rec_call ctxt =
(case Data.get (Proof_Context.theory_of ctxt) of
SOME {rewrite_nested_rec_call, ...} => rewrite_nested_rec_call ctxt);
-fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 =
+fun rec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 =
let
val thy = Proof_Context.theory_of lthy0;
val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, nested_map_idents, nested_map_comps,
induct_thm, n2m, lthy) =
- get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0;
+ get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0;
val perm_basic_lfp_sugars = sort (int_ord o pairself #fp_res_index) basic_lfp_sugars;
@@ -427,7 +427,8 @@
|> map (fn (x, y) => the_single y
handle List.Empty => raise PRIMREC ("missing equations for function " ^ quote x, []));
- val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =));
+ val frees = map (fst #>> Binding.name_of #> Free) fixes;
+ val has_call = exists_subterm (member (op =) frees);
val arg_Ts = map (#rec_type o hd) funs_data;
val res_Ts = map (#res_type o hd) funs_data;
val callssss = funs_data
@@ -444,7 +445,7 @@
| (b, _) :: _ => raise PRIMREC ("type of " ^ Binding.print b ^ " contains top sort", []));
val ((n2m, rec_specs, _, induct_thm, induct_thms), lthy) =
- rec_specs_of bs arg_Ts res_Ts (get_free_indices fixes) callssss lthy0;
+ rec_specs_of bs arg_Ts res_Ts frees callssss lthy0;
val actual_nn = length funs_data;
@@ -469,7 +470,8 @@
|> map_filter (try (fn (x, [y]) =>
(#fun_name x, #user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
|> map2 (fn j => fn (fun_name, user_eqn, num_extra_args, rec_thm) =>
- mk_primrec_tac lthy' num_extra_args nested_map_idents nested_map_comps def_thms rec_thm
+ mk_primrec_tac lthy' num_extra_args nested_map_idents nested_map_comps def_thms
+ rec_thm
|> K |> Goal.prove_sorry lthy' [] [] user_eqn
(* for code extraction from proof terms: *)
|> singleton (Proof_Context.export lthy' lthy)
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Thu Feb 27 21:31:58 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Thu Feb 27 21:36:40 2014 +0100
@@ -26,26 +26,26 @@
{T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_defs = ctr_defs,
ctr_sugar = ctr_sugar, recx = co_rec_of iters, rec_thms = co_rec_of iter_thmss};
-fun get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0 =
+fun get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0 =
let
val ((missing_arg_Ts, perm0_kks,
fp_sugars as {nested_bnfs, co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)),
lthy) =
- nested_to_mutual_fps Least_FP bs arg_Ts get_indices callssss0 lthy0;
+ nested_to_mutual_fps Least_FP bs arg_Ts callers callssss0 lthy0;
val Ts = map #T fp_sugars;
+ val Xs = map #X fp_sugars;
val Cs = map (body_type o fastype_of o co_rec_of o #co_iters) fp_sugars;
- val Ts_Cs = Ts ~~ Cs;
+ val Xs_TCs = Xs ~~ (Ts ~~ Cs);
- fun zip_recT (T as Type (s, Ts)) =
- (case AList.lookup (op =) Ts_Cs T of
- SOME C => [T, C]
- | NONE => [Type (s, map (HOLogic.mk_tupleT o zip_recT) Ts)])
- | zip_recT T = [T];
+ fun zip_recT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_recT) Us)]
+ | zip_recT U =
+ (case AList.lookup (op =) Xs_TCs U of
+ SOME (T, C) => [T, C]
+ | NONE => [U]);
- val ctrss = map (#ctrs o #ctr_sugar) fp_sugars;
- val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss;
- val fun_arg_Tssss = map (map (map zip_recT)) ctr_Tsss;
+ val ctrXs_Tsss = map #ctrXs_Tss fp_sugars;
+ val fun_arg_Tssss = map (map (map zip_recT)) ctrXs_Tsss;
val nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs;
val nested_map_comps = map map_comp_of_bnf nested_bnfs;
--- a/src/HOL/Tools/BNF/bnf_util.ML Thu Feb 27 21:31:58 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML Thu Feb 27 21:36:40 2014 +0100
@@ -31,10 +31,18 @@
val map13: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list
- val map14:
- ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n -> 'o) ->
+ val map14: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
+ 'o) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list
+ val map15: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
+ 'o -> 'p) ->
+ 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
+ 'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list
+ val map16: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
+ 'o -> 'p -> 'q) ->
+ 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
+ 'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list -> 'q list
val fold_map4: ('a -> 'b -> 'c -> 'd -> 'e -> 'f * 'e) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e -> 'f list * 'e
val fold_map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g * 'f) ->
@@ -202,6 +210,21 @@
map14 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s
| map14 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+fun map15 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
+ | map15 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
+ (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s) =
+ f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ::
+ map15 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s
+ | map15 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+
+fun map16 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
+ | map16 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
+ (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s)
+ (x16::x16s) =
+ f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 ::
+ map16 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s x16s
+ | map16 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+
fun fold_map4 _ [] [] [] [] acc = ([], acc)
| fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc =
let
--- a/src/HOL/Tools/Lifting/lifting_def.ML Thu Feb 27 21:31:58 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Thu Feb 27 21:36:40 2014 +0100
@@ -530,12 +530,16 @@
val unfold_ret_val_invs = Conv.bottom_conv
(K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy
val cr_to_pcr_conv = Raw_Simplifier.rewrite lthy false (get_cr_pcr_eqs lthy)
- val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv (cr_to_pcr_conv then_conv simp_arrows_conv))
+ val unfold_inv_conv =
+ Conv.top_sweep_conv (K (Conv.rewr_conv @{thm invariant_def[THEN eq_reflection]})) lthy
+ val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv
+ (cr_to_pcr_conv then_conv simp_arrows_conv))
val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
val beta_conv = Thm.beta_conversion true
val eq_thm =
- (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
+ (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs
+ then_conv unfold_inv_conv) ctm
in
Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
end
--- a/src/HOL/Topological_Spaces.thy Thu Feb 27 21:31:58 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy Thu Feb 27 21:36:40 2014 +0100
@@ -1711,6 +1711,12 @@
shows "open (f -` B)"
by (metis assms continuous_on_open_vimage le_iff_inf)
+corollary open_vimage:
+ assumes "open s" and "continuous_on UNIV f"
+ shows "open (f -` s)"
+ using assms unfolding continuous_on_open_vimage [OF open_UNIV]
+ by simp
+
lemma continuous_on_closed_invariant:
"continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> (\<exists>A. closed A \<and> A \<inter> s = f -` B \<inter> s))"
proof -
--- a/src/Pure/Tools/simplifier_trace.scala Thu Feb 27 21:31:58 2014 +0100
+++ b/src/Pure/Tools/simplifier_trace.scala Thu Feb 27 21:36:40 2014 +0100
@@ -263,7 +263,6 @@
case Some((id, _)) =>
do_cancel(serial, id)
case None =>
- System.err.println("handle_cancel: unknown serial " + serial)
}
case Clear_Memory =>
--- a/src/Tools/Code/code_ml.ML Thu Feb 27 21:31:58 2014 +0100
+++ b/src/Tools/Code/code_ml.ML Thu Feb 27 21:36:40 2014 +0100
@@ -805,7 +805,7 @@
Code_Namespace.hierarchical_program ctxt {
module_name = module_name, reserved = reserved, identifiers = identifiers,
empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
- cyclic_modules = false, class_transitive = false,
+ cyclic_modules = false, class_transitive = true,
class_relation_public = true, empty_data = (),
memorize_data = K I, modify_stmts = modify_stmts }
end;
--- a/src/Tools/Code/code_namespace.ML Thu Feb 27 21:31:58 2014 +0100
+++ b/src/Tools/Code/code_namespace.ML Thu Feb 27 21:36:40 2014 +0100
@@ -95,9 +95,7 @@
let
val succs = Code_Symbol.Graph.Keys.dest o Code_Symbol.Graph.imm_succs gr;
val deps1 = succs sym;
- val deps2 = if class_transitive
- then []
- else [] |> fold (union (op =)) (map succs deps1) |> subtract (op =) deps1
+ val deps2 = [] |> fold (union (op =)) (map succs deps1) |> subtract (op =) deps1
in (deps1, deps2) end;
in
{ is_datatype_or_class = is_datatype_or_class,
@@ -115,6 +113,7 @@
| Code_Thingol.Classinst _ => (SOME Opaque, NONE)
| Code_Thingol.Datatypecons _ => (SOME Public, SOME Opaque)
| Code_Thingol.Classparam _ => (SOME Public, SOME Opaque)
+ | Code_Thingol.Class _ => (SOME Opaque, NONE)
| Code_Thingol.Classrel _ =>
(if class_relation_public
then (SOME Public, SOME Opaque)
--- a/src/Tools/Code/code_scala.ML Thu Feb 27 21:31:58 2014 +0100
+++ b/src/Tools/Code/code_scala.ML Thu Feb 27 21:36:40 2014 +0100
@@ -145,17 +145,12 @@
|> single
|> enclose "(" ")"
end;
- fun privatize Code_Namespace.Public = concat
- | privatize _ = concat o cons (str "private");
- fun privatize' Code_Namespace.Public = concat
- | privatize' Code_Namespace.Opaque = concat
- | privatize' _ = concat o cons (str "private");
fun print_context tyvars vs sym = applify "[" "]"
(fn (v, sort) => (Pretty.block o map str)
(lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort))
NOBR ((str o deresolve) sym) vs;
fun print_defhead export tyvars vars const vs params tys ty =
- privatize export [str "def", constraint (applify "(" ")" (fn (param, ty) =>
+ concat [str "def", constraint (applify "(" ")" (fn (param, ty) =>
constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
NOBR (print_context tyvars vs (Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
str "="];
@@ -218,7 +213,7 @@
val tyvars = intro_tyvars (map (rpair []) vs) reserved;
fun print_co ((co, vs_args), tys) =
concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR
- ((privatize export o map str) ["final", "case", "class", deresolve_const co]) vs_args)
+ ((concat o map str) ["final", "case", "class", deresolve_const co]) vs_args)
@@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg))
(Name.invent_names (snd reserved) "a" tys))),
str "extends",
@@ -227,7 +222,7 @@
];
in
Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars)
- NOBR ((privatize' export o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
+ NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
:: map print_co cos)
end
| print_stmt (Type_Class class, (export, Code_Thingol.Class (v, (classrels, classparams)))) =
@@ -249,7 +244,7 @@
val auxs = Name.invent (snd proto_vars) "a" (length tys);
val vars = intro_vars auxs proto_vars;
in
- privatize' export [str "def", constraint (Pretty.block [applify "(" ")"
+ concat [str "def", constraint (Pretty.block [applify "(" ")"
(fn (aux, ty) => constraint ((str o lookup_var vars) aux)
(print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_const classparam))
(auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
@@ -260,7 +255,7 @@
in
Pretty.chunks (
(Pretty.block_enclose
- (privatize' export ([str "trait", (add_typarg o deresolve_class) class]
+ (concat ([str "trait", (add_typarg o deresolve_class) class]
@ the_list (print_super_classes classrels) @ [str "{"]), str "}")
(map print_classparam_val classparams))
:: map print_classparam_def classparams
@@ -289,7 +284,7 @@
(const, map (IVar o SOME) auxs))
end;
in
- Pretty.block_enclose (privatize export [str "implicit def",
+ Pretty.block_enclose (concat [str "implicit def",
constraint (print_context tyvars vs sym) (print_dicttyp tyvars classtyp),
str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
(map print_classparam_instance (inst_params @ superinst_params))
--- a/src/Tools/Code/code_target.ML Thu Feb 27 21:31:58 2014 +0100
+++ b/src/Tools/Code/code_target.ML Thu Feb 27 21:36:40 2014 +0100
@@ -353,7 +353,7 @@
const_syntax = Code_Symbol.lookup_constant_data printings,
tyco_syntax = Code_Symbol.lookup_type_constructor_data printings,
class_syntax = Code_Symbol.lookup_type_class_data printings },
- (syms_all, program))
+ (subtract (op =) syms_hidden syms, program))
end;
fun mount_serializer ctxt target some_width module_name args program syms =
@@ -374,7 +374,7 @@
else (check_name true raw_module_name; raw_module_name)
val (mounted_serializer, (prepared_syms, prepared_program)) =
mount_serializer ctxt target some_width module_name args program syms;
- in mounted_serializer prepared_program (if all_public then prepared_syms else []) end;
+ in mounted_serializer prepared_program (if all_public then [] else prepared_syms) end;
fun assert_module_name "" = error "Empty module name not allowed here"
| assert_module_name module_name = module_name;