--- a/src/Doc/Datatypes/Datatypes.thy Tue Aug 12 20:18:27 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Aug 12 20:42:39 2014 +0200
@@ -858,9 +858,16 @@
@{thm list.set(1)[no_vars]} \\
@{thm list.set(2)[no_vars]}
+\item[@{text "t."}\hthm{set_cases}\rm:] ~ \\
+@{thm list.set_cases[no_vars]}
+
\item[@{text "t."}\hthm{set_empty}\rm:] ~ \\
@{thm list.set_empty[no_vars]}
+\item[@{text "t."}\hthm{set_intros}\rm:] ~ \\
+@{thm list.set_intros(1)[no_vars]} \\
+@{thm list.set_intros(2)[no_vars]}
+
\item[@{text "t."}\hthm{sel_set}\rm:] ~ \\
@{thm list.sel_set[no_vars]}
--- a/src/HOL/BNF_GFP.thy Tue Aug 12 20:18:27 2014 +0200
+++ b/src/HOL/BNF_GFP.thy Tue Aug 12 20:42:39 2014 +0200
@@ -22,33 +22,33 @@
*}
lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by simp
+ by simp
lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by (cases s) auto
+ by (cases s) auto
lemma not_TrueE: "\<not> True \<Longrightarrow> P"
-by (erule notE, rule TrueI)
+ by (erule notE, rule TrueI)
lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
-by fast
+ by fast
lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
-by (auto split: sum.splits)
+ by (auto split: sum.splits)
lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
-apply rule
- apply (rule ext, force split: sum.split)
-by (rule ext, metis case_sum_o_inj(2))
+ apply rule
+ apply (rule ext, force split: sum.split)
+ by (rule ext, metis case_sum_o_inj(2))
lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
-by fast
+ by fast
lemma equiv_proj:
- assumes e: "equiv A R" and "z \<in> R"
+ assumes e: "equiv A R" and m: "z \<in> R"
shows "(proj R o fst) z = (proj R o snd) z"
proof -
- from assms(2) have z: "(fst z, snd z) \<in> R" by auto
+ from m have z: "(fst z, snd z) \<in> R" by auto
with e have "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R"
unfolding equiv_def sym_def trans_def by blast+
then show ?thesis unfolding proj_def[abs_def] by auto
@@ -58,93 +58,93 @@
definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
lemma Id_on_Gr: "Id_on A = Gr A id"
-unfolding Id_on_def Gr_def by auto
+ unfolding Id_on_def Gr_def by auto
lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
-unfolding image2_def by auto
+ unfolding image2_def by auto
lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
-by auto
+ by auto
lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
-unfolding image2_def Gr_def by auto
+ unfolding image2_def Gr_def by auto
lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
-unfolding Gr_def by simp
+ unfolding Gr_def by simp
lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
-unfolding Gr_def by simp
+ unfolding Gr_def by simp
lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
-unfolding Gr_def by auto
+ unfolding Gr_def by auto
lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
-by blast
+ by blast
lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})"
-by blast
+ by blast
lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
-unfolding fun_eq_iff by auto
+ unfolding fun_eq_iff by auto
lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))"
-by auto
+ by auto
lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
-by force
+ by force
lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
-unfolding fun_eq_iff by auto
+ unfolding fun_eq_iff by auto
lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
-unfolding fun_eq_iff by auto
+ unfolding fun_eq_iff by auto
lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
-unfolding Gr_def Grp_def fun_eq_iff by auto
+ unfolding Gr_def Grp_def fun_eq_iff by auto
definition relImage where
-"relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
+ "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
definition relInvImage where
-"relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
+ "relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
lemma relImage_Gr:
-"\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
-unfolding relImage_def Gr_def relcomp_def by auto
+ "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
+ unfolding relImage_def Gr_def relcomp_def by auto
lemma relInvImage_Gr: "\<lbrakk>R \<subseteq> B \<times> B\<rbrakk> \<Longrightarrow> relInvImage A R f = Gr A f O R O (Gr A f)^-1"
-unfolding Gr_def relcomp_def image_def relInvImage_def by auto
+ unfolding Gr_def relcomp_def image_def relInvImage_def by auto
lemma relImage_mono:
-"R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
-unfolding relImage_def by auto
+ "R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
+ unfolding relImage_def by auto
lemma relInvImage_mono:
-"R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
-unfolding relInvImage_def by auto
+ "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
+ unfolding relInvImage_def by auto
lemma relInvImage_Id_on:
-"(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
-unfolding relInvImage_def Id_on_def by auto
+ "(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
+ unfolding relInvImage_def Id_on_def by auto
lemma relInvImage_UNIV_relImage:
-"R \<subseteq> relInvImage UNIV (relImage R f) f"
-unfolding relInvImage_def relImage_def by auto
+ "R \<subseteq> relInvImage UNIV (relImage R f) f"
+ unfolding relInvImage_def relImage_def by auto
lemma relImage_proj:
-assumes "equiv A R"
-shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
-unfolding relImage_def Id_on_def
-using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
-by (auto simp: proj_preserves)
+ assumes "equiv A R"
+ shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
+ unfolding relImage_def Id_on_def
+ using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
+ by (auto simp: proj_preserves)
lemma relImage_relInvImage:
-assumes "R \<subseteq> f ` A <*> f ` A"
-shows "relImage (relInvImage A R f) f = R"
-using assms unfolding relImage_def relInvImage_def by fast
+ assumes "R \<subseteq> f ` A <*> f ` A"
+ shows "relImage (relInvImage A R f) f = R"
+ using assms unfolding relImage_def relInvImage_def by fast
lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
-by simp
+ by simp
lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z" by simp
lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z" by simp
@@ -159,76 +159,75 @@
definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
-unfolding Shift_def Succ_def by simp
+ unfolding Shift_def Succ_def by simp
lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
-unfolding Succ_def by simp
+ unfolding Succ_def by simp
lemmas SuccE = SuccD[elim_format]
lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
-unfolding Succ_def by simp
+ unfolding Succ_def by simp
lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
-unfolding Shift_def by simp
+ unfolding Shift_def by simp
lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
-unfolding Succ_def Shift_def by auto
+ unfolding Succ_def Shift_def by auto
lemma length_Cons: "length (x # xs) = Suc (length xs)"
-by simp
+ by simp
lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
-by simp
+ by simp
(*injection into the field of a cardinal*)
definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
lemma ex_toCard_pred:
-"\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
-unfolding toCard_pred_def
-using card_of_ordLeq[of A "Field r"]
- ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
-by blast
+ "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
+ unfolding toCard_pred_def
+ using card_of_ordLeq[of A "Field r"]
+ ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
+ by blast
lemma toCard_pred_toCard:
"\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
-unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
+ unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
-lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow>
- toCard A r x = toCard A r y \<longleftrightarrow> x = y"
-using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
+lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> toCard A r x = toCard A r y \<longleftrightarrow> x = y"
+ using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
lemma fromCard_toCard:
-"\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
-unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
+ "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
+ unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
-unfolding Field_card_of csum_def by auto
+ unfolding Field_card_of csum_def by auto
lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
-unfolding Field_card_of csum_def by auto
+ unfolding Field_card_of csum_def by auto
lemma rec_nat_0_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
-by auto
+ by auto
lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
-by auto
+ by auto
lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
-by auto
+ by auto
lemma rec_list_Cons_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
-by auto
+ by auto
lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
-by simp
+ by simp
lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
-by auto
+ by auto
definition image2p where
"image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)"
@@ -250,20 +249,21 @@
lemma equiv_Eps_in:
"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
-apply (rule someI2_ex)
-using in_quotient_imp_non_empty by blast
+ apply (rule someI2_ex)
+ using in_quotient_imp_non_empty by blast
lemma equiv_Eps_preserves:
-assumes ECH: "equiv A r" and X: "X \<in> A//r"
-shows "Eps (%x. x \<in> X) \<in> A"
-apply (rule in_mono[rule_format])
- using assms apply (rule in_quotient_imp_subset)
-by (rule equiv_Eps_in) (rule assms)+
+ assumes ECH: "equiv A r" and X: "X \<in> A//r"
+ shows "Eps (%x. x \<in> X) \<in> A"
+ apply (rule in_mono[rule_format])
+ using assms apply (rule in_quotient_imp_subset)
+ by (rule equiv_Eps_in) (rule assms)+
lemma proj_Eps:
-assumes "equiv A r" and "X \<in> A//r"
-shows "proj r (Eps (%x. x \<in> X)) = X"
-unfolding proj_def proof auto
+ assumes "equiv A r" and "X \<in> A//r"
+ shows "proj r (Eps (%x. x \<in> X)) = X"
+unfolding proj_def
+proof auto
fix x assume x: "x \<in> X"
thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
next
@@ -276,7 +276,7 @@
lemma univ_commute:
assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
shows "(univ f) (proj r x) = f x"
-unfolding univ_def proof -
+proof (unfold univ_def)
have prj: "proj r x \<in> A//r" using x proj_preserves by fast
hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
@@ -285,9 +285,8 @@
qed
lemma univ_preserves:
-assumes ECH: "equiv A r" and RES: "f respects r" and
- PRES: "\<forall> x \<in> A. f x \<in> B"
-shows "\<forall>X \<in> A//r. univ f X \<in> B"
+ assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall> x \<in> A. f x \<in> B"
+ shows "\<forall>X \<in> A//r. univ f X \<in> B"
proof
fix X assume "X \<in> A//r"
then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Aug 12 20:18:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Aug 12 20:42:39 2014 +0200
@@ -102,7 +102,9 @@
val disc_map_iffN = "disc_map_iff";
val sel_mapN = "sel_map";
val sel_setN = "sel_set";
+val set_casesN = "set_cases";
val set_emptyN = "set_empty";
+val set_introsN = "set_intros";
val set_inductN = "set_induct";
structure Data = Generic_Data
@@ -113,6 +115,12 @@
fun merge data : T = Symtab.merge (K true) data;
);
+fun zipping_map f =
+ let
+ fun zmap _ [] = []
+ | zmap xs (y :: ys) = f (xs, y, ys) :: zmap (xs @ [y]) ys
+ in zmap [] end;
+
fun choose_binary_fun fs AB =
find_first (fastype_of #> binder_types #> (fn [A, B] => AB = (A, B))) fs;
fun build_binary_fun_app fs a b =
@@ -501,10 +509,10 @@
val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq
(map2 (build_the_rel lthy (Rs @ IRs) []) fpA_Ts fpB_Ts) IRs));
- val rel_induct0_thm = Goal.prove_sorry lthy [] premises goal
- (fn {context = ctxt, prems = prems} =>
- mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (certify ctxt) IRs) exhausts ctor_defss
- ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs)
+ val rel_induct0_thm =
+ Goal.prove_sorry lthy [] premises goal (fn {context = ctxt, prems} =>
+ mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (certify ctxt) IRs) exhausts ctor_defss
+ ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
in
@@ -752,12 +760,12 @@
val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq
IRs (map2 (build_the_rel lthy (Rs @ IRs) []) fpA_Ts fpB_Ts)));
- val rel_coinduct0_thm = Goal.prove_sorry lthy [] premises goal
- (fn {context = ctxt, prems = prems} =>
- mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (certify ctxt) IRs) prems
- (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars)
- (map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects
- rel_pre_defs abs_inverses live_nesting_rel_eqs)
+ val rel_coinduct0_thm =
+ Goal.prove_sorry lthy [] premises goal (fn {context = ctxt, prems} =>
+ mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (certify ctxt) IRs) prems
+ (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars)
+ (map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects
+ rel_pre_defs abs_inverses live_nesting_rel_eqs)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
in
@@ -771,7 +779,7 @@
let
fun mk_prems A Ps ctr_args t ctxt =
(case fastype_of t of
- Type (type_name, xs) =>
+ Type (type_name, innerTs) =>
(case bnf_of ctxt type_name of
NONE => ([], ctxt)
| SOME bnf =>
@@ -794,7 +802,7 @@
ctxt'))
end;
in
- fold_map (seq_assm t o mk_set xs) (sets_of_bnf bnf) ctxt
+ fold_map (seq_assm t o mk_set innerTs) (sets_of_bnf bnf) ctxt
|>> flat
end)
| T =>
@@ -803,7 +811,7 @@
fun mk_prems_for_ctr A Ps ctr ctxt =
let
- val (args, ctxt') = mk_Frees "arg" (binder_types (fastype_of ctr)) ctxt;
+ val (args, ctxt') = mk_Frees "z" (binder_types (fastype_of ctr)) ctxt;
in
fold_map (mk_prems A Ps (list_comb (ctr, args))) args ctxt'
|>> map (fold_rev Logic.all args) o flat
@@ -835,10 +843,11 @@
|>> apfst (apsnd (Library.foldr1 HOLogic.mk_conj))
|>> apsnd flat;
- val thm = Goal.prove_sorry lthy [] premises (HOLogic.mk_Trueprop conclusion)
- (fn {context = ctxt, prems = prems} =>
- mk_set_induct0_tac ctxt (map (certify ctxt'') Ps) prems dtor_set_inducts exhausts
- set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses)
+ val thm =
+ Goal.prove_sorry lthy [] premises (HOLogic.mk_Trueprop conclusion)
+ (fn {context = ctxt, prems} =>
+ mk_set_induct0_tac ctxt (map (certify ctxt'') Ps) prems dtor_set_inducts exhausts
+ set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses)
|> singleton (Proof_Context.export ctxt'' ctxt)
|> Thm.close_derivation;
@@ -1267,6 +1276,7 @@
disc_bindings), sel_bindingss), raw_sel_default_eqs) no_defs_lthy =
let
val fp_b_name = Binding.name_of fp_b;
+ val fpBT = B_ify fpT;
val ctr_absT = domain_type (fastype_of ctor);
@@ -1389,11 +1399,10 @@
else fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans))))
|> singleton (Proof_Context.export names_lthy no_defs_lthy);
-
fun mk_set0_thm fp_set_thm ctr_def' cxIn =
fold_thms lthy [ctr_def']
(unfold_thms lthy (pre_set_defs @ fp_nesting_set_maps @ live_nesting_set_maps @
- (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_set @
+ (if fp = Least_FP then [] else [dtor_ctor]) @ basic_sumprod_thms_set @
@{thms UN_Un sup_assoc[THEN sym]} @ abs_inverses)
(cterm_instantiate_pos [SOME cxIn] fp_set_thm))
|> singleton (Proof_Context.export names_lthy no_defs_lthy);
@@ -1438,9 +1447,9 @@
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
mk_set_empty_tac ctxt (certify ctxt u) exhaust set0_thms (flat disc_thmss))
- |> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy
- |> map Thm.close_derivation
+ |> Conjunction.elim_balanced (length goals)
+ |> Proof_Context.export names_lthy lthy
+ |> map Thm.close_derivation
end;
val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
@@ -1489,31 +1498,136 @@
map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th)
rel_inject_thms ms;
- val (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms,
- (rel_cases_thm, rel_cases_attrs)) =
+ val (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms, set_intros_thms,
+ (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs)) =
let
- val (((Ds, As), Bs), names_lthy) = lthy
- |> mk_TFrees (dead_of_bnf fp_bnf)
- ||>> mk_TFrees (live_of_bnf fp_bnf)
- ||>> mk_TFrees (live_of_bnf fp_bnf);
- val TA as Type (_, ADs) = mk_T_of_bnf Ds As fp_bnf;
- val TB as Type (_, BDs) = mk_T_of_bnf Ds Bs fp_bnf;
- val fTs = map2 (curry op -->) As Bs;
- val rel = mk_rel_of_bnf Ds As Bs fp_bnf;
- val ((((fs, Rs), ta), tb), names_lthy) = names_lthy
+ val live_AsBs = filter (op <>) (As ~~ Bs);
+ val fTs = map (op -->) live_AsBs;
+ val rel = mk_rel live As Bs (rel_of_bnf fp_bnf);
+ val (((((fs, Rs), ta), tb), thesis), names_lthy) = names_lthy
|> mk_Frees "f" fTs
- ||>> mk_Frees "R" (map2 mk_pred2T As Bs)
- ||>> yield_singleton (mk_Frees "a") TA
- ||>> yield_singleton (mk_Frees "b") TB;
- val map_term = mk_map_of_bnf Ds As Bs fp_bnf;
- val discAs = map (mk_disc_or_sel ADs) discs;
- val selAss = map (map (mk_disc_or_sel ADs)) selss;
+ ||>> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs)
+ ||>> yield_singleton (mk_Frees "a") fpT
+ ||>> yield_singleton (mk_Frees "b") fpBT
+ ||>> apfst HOLogic.mk_Trueprop o
+ yield_singleton (mk_Frees "thesis") HOLogic.boolT;
+ val map_term = mk_map live As Bs (map_of_bnf fp_bnf);
+ val ctrAs = map (mk_ctr As) ctrs;
+ val setAs = map (mk_set As) (sets_of_bnf fp_bnf);
+ val discAs = map (mk_disc_or_sel As) discs;
+ val selAss = map (map (mk_disc_or_sel As)) selss;
val discAs_selAss = flat (map2 (map o pair) discAs selAss);
+ val (set_cases_thms, set_cases_attrss) =
+ let
+ fun mk_prems assms elem t ctxt =
+ (case fastype_of t of
+ Type (type_name, xs) =>
+ (case bnf_of ctxt type_name of
+ NONE => ([], ctxt)
+ | SOME bnf =>
+ apfst flat (fold_map (fn set => fn ctxt =>
+ let
+ val X = HOLogic.dest_setT (range_type (fastype_of set));
+ val new_var = not (X = fastype_of elem);
+ val (x, ctxt') =
+ if new_var then yield_singleton (mk_Frees "x") X ctxt
+ else (elem, ctxt);
+ in
+ mk_prems (mk_Trueprop_mem (x, set $ t) :: assms) elem x ctxt'
+ |>> map (if new_var then Logic.all x else I)
+ end) (map (mk_set xs) (sets_of_bnf bnf)) ctxt))
+ | T => rpair ctxt
+ (if T = fastype_of elem then [fold (curry Logic.mk_implies) assms thesis]
+ else []));
+ in
+ split_list (map (fn set =>
+ let
+ val A = HOLogic.dest_setT (range_type (fastype_of set));
+ val (elem, names_lthy) = yield_singleton (mk_Frees "e") A names_lthy;
+ val premss =
+ map (fn ctr =>
+ let
+ val (args, names_lthy) =
+ mk_Frees "z" (binder_types (fastype_of ctr)) names_lthy;
+ in
+ flat (zipping_map (fn (prev_args, arg, next_args) =>
+ let
+ val (args_with_elem, args_without_elem) =
+ if fastype_of arg = A then
+ (prev_args @ [elem] @ next_args, prev_args @ next_args)
+ else
+ `I (prev_args @ [arg] @ next_args);
+ in
+ mk_prems
+ [mk_Trueprop_eq (ta, Term.list_comb (ctr, args_with_elem))]
+ elem arg names_lthy
+ |> fst
+ |> map (fold_rev Logic.all args_without_elem)
+ end) args)
+ end) ctrAs;
+ val goal = Logic.mk_implies (mk_Trueprop_mem (elem, set $ ta), thesis);
+ val thm =
+ Goal.prove_sorry lthy [] (flat premss) goal
+ (fn {context = ctxt, prems} =>
+ mk_set_cases_tac ctxt (certify ctxt ta) prems exhaust set_thms)
+ |> singleton (Proof_Context.export names_lthy lthy)
+ |> Thm.close_derivation
+ |> rotate_prems ~1;
+ in
+ (thm, [](* TODO: [@{attributes [elim?]},
+ Attrib.internal (K (Induct.cases_pred (name_of_set set)))] *))
+ end) setAs)
+ end;
+
+ val set_intros_thms =
+ let
+ fun mk_goals A setA ctr_args t ctxt =
+ (case fastype_of t of
+ Type (type_name, innerTs) =>
+ (case bnf_of ctxt type_name of
+ NONE => ([], ctxt)
+ | SOME bnf =>
+ apfst flat (fold_map (fn set => fn ctxt =>
+ let
+ val X = HOLogic.dest_setT (range_type (fastype_of set));
+ val (x, ctxt') = yield_singleton (mk_Frees "x") X ctxt;
+ val assm = mk_Trueprop_mem (x, set $ t);
+ in
+ apfst (map (Logic.mk_implies o pair assm))
+ (mk_goals A setA ctr_args x ctxt')
+ end) (map (mk_set innerTs) (sets_of_bnf bnf)) ctxt))
+ | T =>
+ (if T = A then [mk_Trueprop_mem (t, setA $ ctr_args)] else [], ctxt));
+
+ val (goals, names_lthy) =
+ apfst flat (fold_map (fn set => fn ctxt =>
+ let
+ val A = HOLogic.dest_setT (range_type (fastype_of set));
+ in
+ apfst flat (fold_map (fn ctr => fn ctxt =>
+ let
+ val (args, ctxt') =
+ mk_Frees "arg" (binder_types (fastype_of ctr)) ctxt;
+ val ctr_args = Term.list_comb (ctr, args);
+ in
+ apfst flat (fold_map (mk_goals A set ctr_args) args ctxt')
+ end) ctrAs ctxt)
+ end) setAs lthy);
+ in
+ if null goals then []
+ else
+ Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+ (fn {context = ctxt, prems = _} => mk_set_intros_tac ctxt set0_thms)
+ |> Conjunction.elim_balanced (length goals)
+ |> Proof_Context.export names_lthy lthy
+ |> map Thm.close_derivation
+ end;
+
val rel_sel_thms =
let
- val discBs = map (mk_disc_or_sel BDs) discs;
- val selBss = map (map (mk_disc_or_sel BDs)) selss;
+ val discBs = map (mk_disc_or_sel Bs) discs;
+ val selBss = map (map (mk_disc_or_sel Bs)) selss;
val n = length discAs;
fun mk_rhs n k discA selAs discB selBs =
@@ -1539,18 +1653,15 @@
mk_rel_sel_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
(flat disc_thmss) (flat sel_thmss) rel_inject_thms distincts
rel_distinct_thms)
- |> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy
+ |> Conjunction.elim_balanced (length goals)
+ |> Proof_Context.export names_lthy lthy
+ |> map Thm.close_derivation
end;
val (rel_cases_thm, rel_cases_attrs) =
let
- val (thesis, names_lthy) = apfst HOLogic.mk_Trueprop
- (yield_singleton (mk_Frees "thesis") HOLogic.boolT names_lthy);
-
val rel_Rs_a_b = list_comb (rel, Rs) $ ta $ tb;
- val ctrAs = map (mk_ctr ADs) ctrs;
- val ctrBs = map (mk_ctr BDs) ctrs;
+ val ctrBs = map (mk_ctr Bs) ctrs;
fun mk_assms ctrA ctrB ctxt =
let
@@ -1572,9 +1683,10 @@
end;
val (assms, names_lthy) = fold_map2 mk_assms ctrAs ctrBs names_lthy;
- val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms,
- thesis);
- val thm = Goal.prove_sorry lthy [] [] goal
+ val goal =
+ Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, thesis);
+ val thm =
+ Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} =>
mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
injects rel_inject_thms distincts rel_distinct_thms
@@ -1592,7 +1704,7 @@
val disc_map_iff_thms =
let
- val discsB = map (mk_disc_or_sel BDs) discs;
+ val discsB = map (mk_disc_or_sel Bs) discs;
val discsA_t = map (fn disc1 => Term.betapply (disc1, ta)) discAs;
fun mk_goal (discA_t, discB) =
@@ -1611,8 +1723,9 @@
(fn {context = ctxt, prems = _} =>
mk_disc_map_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
map_thms)
- |> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy
+ |> Conjunction.elim_balanced (length goals)
+ |> Proof_Context.export names_lthy lthy
+ |> map Thm.close_derivation
end;
val sel_map_thms =
@@ -1620,14 +1733,15 @@
fun mk_goal (discA, selA) =
let
val prem = Term.betapply (discA, ta);
- val selB = mk_disc_or_sel BDs selA;
+ val selB = mk_disc_or_sel Bs selA;
val lhs = selB $ (Term.list_comb (map_term, fs) $ ta);
val lhsT = fastype_of lhs;
- val map_rhsT = map_atyps (perhaps (AList.lookup (op =) (Bs ~~ As))) lhsT;
+ val map_rhsT =
+ map_atyps (perhaps (AList.lookup (op =) (map swap live_AsBs))) lhsT;
val map_rhs = build_map lthy []
- (the o (AList.lookup (op =) ((As ~~ Bs) ~~ fs))) (map_rhsT, lhsT);
+ (the o (AList.lookup (op =) (live_AsBs ~~ fs))) (map_rhsT, lhsT);
val rhs = (case map_rhs of
- Const (@{const_name id}, _) => selA $ ta
+ Const (@{const_name id}, _) => selA $ ta
| _ => map_rhs $ (selA $ ta));
val concl = mk_Trueprop_eq (lhs, rhs);
in
@@ -1643,14 +1757,13 @@
(fn {context = ctxt, prems = _} =>
mk_sel_map_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
map_thms (flat sel_thmss))
- |> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy
+ |> Conjunction.elim_balanced (length goals)
+ |> Proof_Context.export names_lthy lthy
+ |> map Thm.close_derivation
end;
val sel_set_thms =
let
- val setsA = map (mk_set ADs) (sets_of_bnf fp_bnf);
-
fun mk_goal discA selA setA ctxt =
let
val prem = Term.betapply (discA, ta);
@@ -1659,7 +1772,7 @@
fun travese_nested_types t ctxt =
(case fastype_of t of
- Type (type_name, xs) =>
+ Type (type_name, innerTs) =>
(case bnf_of ctxt type_name of
NONE => ([], ctxt)
| SOME bnf =>
@@ -1674,7 +1787,7 @@
|>> map (Logic.mk_implies o pair assm)
end;
in
- fold_map (seq_assm t o mk_set xs) (sets_of_bnf bnf) ctxt
+ fold_map (seq_assm t o mk_set innerTs) (sets_of_bnf bnf) ctxt
|>> flat
end)
| T =>
@@ -1699,21 +1812,22 @@
([], ctxt)
end;
val (goals, names_lthy) = apfst (flat o flat) (fold_map (fn (disc, sel) =>
- fold_map (mk_goal disc sel) setsA) discAs_selAss names_lthy);
+ fold_map (mk_goal disc sel) setAs) discAs_selAss names_lthy);
in
if null goals then
[]
else
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
- mk_sel_set_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
- (flat sel_thmss) set0_thms)
- |> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy
+ mk_sel_set_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
+ (flat sel_thmss) set0_thms)
+ |> Conjunction.elim_balanced (length goals)
+ |> Proof_Context.export names_lthy lthy
+ |> map Thm.close_derivation
end;
in
- (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms,
- (rel_cases_thm, rel_cases_attrs))
+ (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms, set_intros_thms,
+ (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs))
end;
val anonymous_notes =
@@ -1732,7 +1846,9 @@
(setN, set_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
(sel_mapN, sel_map_thms, K []),
(sel_setN, sel_set_thms, K []),
- (set_emptyN, set_empty_thms, K [])]
+ (set_casesN, set_cases_thms, nth set_cases_attrss),
+ (set_emptyN, set_empty_thms, K []),
+ (set_introsN, set_intros_thms, K [])]
|> massage_simple_notes fp_b_name;
val (noted, lthy') =
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Aug 12 20:18:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Aug 12 20:42:39 2014 +0200
@@ -10,6 +10,7 @@
sig
val sumprod_thms_map: thm list
val sumprod_thms_set: thm list
+ val basic_sumprod_thms_set: thm list
val sumprod_thms_rel: thm list
val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list ->
@@ -38,9 +39,11 @@
thm list -> thm list -> tactic
val mk_sel_map_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
val mk_sel_set_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
+ val mk_set_cases_tac: Proof.context -> cterm -> thm list -> thm -> thm list -> tactic
val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
val mk_set_induct0_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list ->
thm list -> thm list -> thm list -> thm list -> tactic
+ val mk_set_intros_tac: Proof.context -> thm list -> tactic
end;
structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS =
@@ -56,9 +59,10 @@
val simp_thms' = @{thms simp_thms(6,7,8,11,12,15,16,22,24)};
val sumprod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps};
-val sumprod_thms_set =
- @{thms UN_empty UN_insert UN_simps(10) UN_iff Un_empty_left Un_empty_right Un_iff Union_Un_distrib
- image_iff o_apply map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps};
+val basic_sumprod_thms_set =
+ @{thms UN_empty UN_insert UN_iff Un_empty_left Un_empty_right Un_iff Union_Un_distrib
+ o_apply map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps};
+val sumprod_thms_set = @{thms UN_simps(10) image_iff} @ basic_sumprod_thms_set;
val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_apply prod.inject id_apply conj_assoc};
fun hhf_concl_conv cv ctxt ct =
@@ -299,6 +303,14 @@
hyp_subst_tac ctxt) THEN'
(rtac @{thm singletonI} ORELSE' atac));
+fun mk_set_cases_tac ctxt ct assms exhaust sets =
+ HEADGOAL (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW hyp_subst_tac ctxt) THEN
+ unfold_thms_tac ctxt sets THEN
+ REPEAT_DETERM (HEADGOAL
+ (eresolve_tac @{thms FalseE emptyE singletonE UnE UN_E insertE} ORELSE'
+ hyp_subst_tac ctxt ORELSE'
+ SELECT_GOAL (SOLVE (HEADGOAL (eresolve_tac assms THEN' REPEAT_DETERM o atac)))));
+
fun mk_set_empty_tac ctxt ct exhaust sets discs =
TRYALL Goal.conjunction_tac THEN
ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
@@ -307,6 +319,13 @@
SOME (thm RS eqFalseI) handle THM _ => NONE) discs) THEN
ALLGOALS (rtac refl ORELSE' etac FalseE);
+fun mk_set_intros_tac ctxt sets =
+ TRYALL Goal.conjunction_tac THEN
+ unfold_thms_tac ctxt sets THEN
+ TRYALL (REPEAT o
+ (resolve_tac @{thms UnI1 UnI2} ORELSE'
+ eresolve_tac @{thms UN_I UN_I[rotated]}) THEN' (rtac @{thm singletonI} ORELSE' atac));
+
fun mk_set_induct0_tac ctxt cts assms dtor_set_inducts exhausts set_pre_defs ctor_defs dtor_ctors
Abs_pre_inverses =
let
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Aug 12 20:18:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Aug 12 20:42:39 2014 +0200
@@ -8,6 +8,7 @@
signature BNF_FP_N2M_SUGAR =
sig
val unfold_lets_splits: term -> term
+ val unfold_splits_lets: term -> term
val dest_map: Proof.context -> string -> term -> term * term list
val mutualize_fp_sugars: BNF_Util.fp_kind -> int list -> binding list -> typ list -> term list ->
@@ -60,18 +61,22 @@
Local_Theory.declaration {syntax = false, pervasive = false}
(fn phi => Data.map (Typtab.update (key, morph_n2m_sugar phi n2m_sugar)));
-fun unfold_lets_splits (Const (@{const_name Let}, _) $ arg1 $ arg2) =
- unfold_lets_splits (betapply (arg2, arg1))
- | unfold_lets_splits (t as Const (@{const_name case_prod}, _) $ u) =
- (case unfold_lets_splits u of
+fun unfold_lets_splits (Const (@{const_name Let}, _) $ t $ u) =
+ unfold_lets_splits (betapply (unfold_splits_lets u, t))
+ | unfold_lets_splits (t $ u) = betapply (unfold_lets_splits t, unfold_lets_splits u)
+ | unfold_lets_splits (Abs (s, T, t)) = Abs (s, T, unfold_lets_splits t)
+ | unfold_lets_splits t = t
+and unfold_splits_lets ((t as Const (@{const_name case_prod}, _)) $ u) =
+ (case unfold_splits_lets u of
u' as Abs (s1, T1, Abs (s2, T2, _)) =>
let val v = Var ((s1 ^ s2, Term.maxidx_of_term u' + 1), HOLogic.mk_prodT (T1, T2)) in
lambda v (incr_boundvars 1 (betapplys (u', [HOLogic.mk_fst v, HOLogic.mk_snd v])))
end
- | _ => t)
- | unfold_lets_splits (t $ u) = betapply (pairself unfold_lets_splits (t, u))
- | unfold_lets_splits (Abs (s, T, t)) = Abs (s, T, unfold_lets_splits t)
- | unfold_lets_splits t = t;
+ | _ => t $ unfold_lets_splits u)
+ | unfold_splits_lets (t as Const (@{const_name Let}, _) $ _ $ _) = unfold_lets_splits t
+ | unfold_splits_lets (t $ u) = betapply (unfold_splits_lets t, unfold_lets_splits u)
+ | unfold_splits_lets (Abs (s, T, t)) = Abs (s, T, unfold_splits_lets t)
+ | unfold_splits_lets t = unfold_lets_splits t;
fun mk_map_pattern ctxt s =
let
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Aug 12 20:18:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Aug 12 20:42:39 2014 +0200
@@ -198,7 +198,7 @@
end
| (c as Const (@{const_name case_prod}, _), arg :: args) =>
massage_rec bound_Ts
- (unfold_lets_splits (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
+ (unfold_splits_lets (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
| (Const (c, _), args as _ :: _ :: _) =>
(case try strip_fun_type (Sign.the_const_type thy c) of
SOME (gen_branch_Ts, gen_body_fun_T) =>
@@ -694,14 +694,6 @@
handle ListPair.UnequalLengths =>
primcorec_error_eqn "partially applied constructor in right-hand side" rhs;
-(*
-val _ = tracing ("reduced\n " ^ Syntax.string_of_term @{context} concl ^ "\nto\n \<cdot> " ^
- (is_some eqn_data_disc_opt ? K (Syntax.string_of_term @{context} disc_concl ^ "\n \<cdot> ")) "" ^
- space_implode "\n \<cdot> " (map (Syntax.string_of_term @{context}) sel_concls) ^
- "\nfor premise(s)\n \<cdot> " ^
- space_implode "\n \<cdot> " (map (Syntax.string_of_term @{context}) prems));
-*)
-
val eqns_data_sel =
map (dissect_coeqn_sel lthy fun_names basic_ctr_specss eqn_pos
(SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt eqn0 (SOME ctr)) sel_concls;
@@ -890,11 +882,6 @@
| currys Ts t = t $ mk_tuple1_balanced (List.rev Ts) (map Bound (length Ts - 1 downto 0))
|> fold_rev (Term.abs o pair Name.uu) Ts;
-(*
-val _ = tracing ("corecursor arguments:\n \<cdot> " ^
- space_implode "\n \<cdot> " (map (Syntax.string_of_term lthy) corec_args));
-*)
-
val excludess' =
disc_eqnss
|> map (map (fn x => (#fun_args x, #ctr_no x, #prems x, #auto_gen x))
@@ -1006,10 +993,6 @@
|> map2 (curry (op |>)) (map (map (fn {ctr, sels, ...} =>
(ctr, map (K []) sels))) basic_ctr_specss);
-(*
-val _ = tracing ("callssss = " ^ @{make_string} callssss);
-*)
-
val ((n2m, corec_specs', _, coinduct_thm, strong_coinduct_thm, coinduct_thms,
strong_coinduct_thms), lthy') =
corec_specs_of bs arg_Ts res_Ts frees callssss lthy;
@@ -1051,11 +1034,6 @@
else
tac_opt;
-(*
-val _ = tracing ("exclusiveness properties:\n \<cdot> " ^
- space_implode "\n \<cdot> " (maps (map (Syntax.string_of_term lthy o snd)) excludess'));
-*)
-
val excludess'' = map3 (fn tac_opt => fn sequential => map (fn (j, goal) =>
(j, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation)
(exclude_tac tac_opt sequential j), goal))))