# HG changeset patch # User wenzelm # Date 1407868959 -7200 # Node ID a2a7c1de4752775fd5b6fa62b47d8281973bdd11 # Parent f7f75b33d6c859bc5d0823e9226bb25c414f6592# Parent f5d73caba4e53e95542cb5ab256a78b354de9555 merged diff -r f5d73caba4e5 -r a2a7c1de4752 src/Doc/Datatypes/Datatypes.thy --- 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]} diff -r f5d73caba4e5 -r a2a7c1de4752 src/HOL/BNF_GFP.thy --- 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: "\\x. s = x \ P\ \ P" -by simp + by simp lemma obj_sumE: "\\x. s = Inl x \ P; \x. s = Inr x \ P\ \ P" -by (cases s) auto + by (cases s) auto lemma not_TrueE: "\ True \ P" -by (erule notE, rule TrueI) + by (erule notE, rule TrueI) lemma neq_eq_eq_contradict: "\t \ u; s = t; s = u\ \ P" -by fast + by fast lemma case_sum_expand_Inr: "f o Inl = g \ 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 \ h = f o Inr \ 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 \ B) ^-1 = B \ A" -by fast + by fast lemma equiv_proj: - assumes e: "equiv A R" and "z \ R" + assumes e: "equiv A R" and m: "z \ R" shows "(proj R o fst) z = (proj R o snd) z" proof - - from assms(2) have z: "(fst z, snd z) \ R" by auto + from m have z: "(fst z, snd z) \ R" by auto with e have "\x. (fst z, x) \ R \ (snd z, x) \ R" "\x. (snd z, x) \ R \ (fst z, x) \ 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 \ 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: "\b = f x; c = g x; x \ A\ \ (b, c) \ image2 A f g" -unfolding image2_def by auto + unfolding image2_def by auto lemma IdD: "(a, b) \ Id \ 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) \ Gr A f \ x \ A" -unfolding Gr_def by simp + unfolding Gr_def by simp lemma GrD2: "(x, fx) \ Gr A f \ f x = fx" -unfolding Gr_def by simp + unfolding Gr_def by simp lemma Gr_incl: "Gr A f \ A <*> B \ f ` A \ B" -unfolding Gr_def by auto + unfolding Gr_def by auto lemma subset_Collect_iff: "B \ A \ (B \ {x \ A. P x}) = (\x \ B. P x)" -by blast + by blast lemma subset_CollectI: "B \ A \ (\x. x \ B \ Q x \ P x) \ ({x \ B. Q x} \ {x \ 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 \ Y \ X \ Collect (split (in_rel Y))" -by auto + by auto lemma Collect_split_in_rel_leE: "X \ Collect (split (in_rel Y)) \ (X \ Y \ R) \ R" -by force + by force lemma conversep_in_rel: "(in_rel R)\\ = in_rel (R\)" -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 \ {(f a1, f a2) | a1 a2. (a1,a2) \ R}" + "relImage R f \ {(f a1, f a2) | a1 a2. (a1,a2) \ R}" definition relInvImage where -"relInvImage A R f \ {(a1, a2) | a1 a2. a1 \ A \ a2 \ A \ (f a1, f a2) \ R}" + "relInvImage A R f \ {(a1, a2) | a1 a2. a1 \ A \ a2 \ A \ (f a1, f a2) \ R}" lemma relImage_Gr: -"\R \ A \ A\ \ relImage R f = (Gr A f)^-1 O R O Gr A f" -unfolding relImage_def Gr_def relcomp_def by auto + "\R \ A \ A\ \ 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: "\R \ B \ B\ \ 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 \ R2 \ relImage R1 f \ relImage R2 f" -unfolding relImage_def by auto + "R1 \ R2 \ relImage R1 f \ relImage R2 f" + unfolding relImage_def by auto lemma relInvImage_mono: -"R1 \ R2 \ relInvImage A R1 f \ relInvImage A R2 f" -unfolding relInvImage_def by auto + "R1 \ R2 \ relInvImage A R1 f \ relInvImage A R2 f" + unfolding relInvImage_def by auto lemma relInvImage_Id_on: -"(\a1 a2. f a1 = f a2 \ a1 = a2) \ relInvImage A (Id_on B) f \ Id" -unfolding relInvImage_def Id_on_def by auto + "(\a1 a2. f a1 = f a2 \ a1 = a2) \ relInvImage A (Id_on B) f \ Id" + unfolding relInvImage_def Id_on_def by auto lemma relInvImage_UNIV_relImage: -"R \ relInvImage UNIV (relImage R f) f" -unfolding relInvImage_def relImage_def by auto + "R \ 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) \ 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) \ 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 \ f ` A <*> f ` A" -shows "relImage (relInvImage A R f) f = R" -using assms unfolding relImage_def relInvImage_def by fast + assumes "R \ 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 \ a = (x, y) \ P (fst a) (snd a)" -by simp + by simp lemma fst_diag_id: "(fst \ (%x. (x, x))) z = id z" by simp lemma snd_diag_id: "(snd \ (%x. (x, x))) z = id z" by simp @@ -159,76 +159,75 @@ definition shift where "shift lab k = (\kl. lab (k # kl))" lemma empty_Shift: "\[] \ Kl; k \ Succ Kl []\ \ [] \ Shift Kl k" -unfolding Shift_def Succ_def by simp + unfolding Shift_def Succ_def by simp lemma SuccD: "k \ Succ Kl kl \ kl @ [k] \ Kl" -unfolding Succ_def by simp + unfolding Succ_def by simp lemmas SuccE = SuccD[elim_format] lemma SuccI: "kl @ [k] \ Kl \ k \ Succ Kl kl" -unfolding Succ_def by simp + unfolding Succ_def by simp lemma ShiftD: "kl \ Shift Kl k \ k # kl \ 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 \ inj_on f A \ f ` A \ Field r \ Card_order r" definition "toCard A r \ SOME f. toCard_pred A r f" lemma ex_toCard_pred: -"\|A| \o r; Card_order r\ \ \ 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 + "\|A| \o r; Card_order r\ \ \ 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: "\|A| \o r; Card_order r\ \ 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: "\|A| \o r; Card_order r; x \ A; y \ A\ \ - toCard A r x = toCard A r y \ x = y" -using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast +lemma toCard_inj: "\|A| \o r; Card_order r; x \ A; y \ A\ \ toCard A r x = toCard A r y \ x = y" + using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast definition "fromCard A r k \ SOME b. b \ A \ toCard A r b = k" lemma fromCard_toCard: -"\|A| \o r; Card_order r; b \ A\ \ fromCard A r (toCard A r b) = b" -unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj) + "\|A| \o r; Card_order r; b \ A\ \ 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 \ Field r \ Inl a \ 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 \ Field s \ Inr a \ 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) \ f 0 = f1" -by auto + by auto lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) \ 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) \ f [] = f1" -by auto + by auto lemma rec_list_Cons_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \ f (x # xs) = f2 x xs (f xs)" -by auto + by auto lemma not_arg_cong_Inr: "x \ y \ Inr x \ Inr y" -by simp + by simp lemma Collect_splitD: "x \ Collect (split A) \ A (fst x) (snd x)" -by auto + by auto definition image2p where "image2p f g R = (\x y. \x' y'. R x' y' \ f x' = x \ g y' = y)" @@ -250,20 +249,21 @@ lemma equiv_Eps_in: "\equiv A r; X \ A//r\ \ Eps (%x. x \ X) \ 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 \ A//r" -shows "Eps (%x. x \ X) \ 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 \ A//r" + shows "Eps (%x. x \ X) \ 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 \ A//r" -shows "proj r (Eps (%x. x \ X)) = X" -unfolding proj_def proof auto + assumes "equiv A r" and "X \ A//r" + shows "proj r (Eps (%x. x \ X)) = X" +unfolding proj_def +proof auto fix x assume x: "x \ X" thus "(Eps (%x. x \ X), x) \ 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 \ A" shows "(univ f) (proj r x) = f x" -unfolding univ_def proof - +proof (unfold univ_def) have prj: "proj r x \ A//r" using x proj_preserves by fast hence "Eps (%y. y \ proj r x) \ A" using ECH equiv_Eps_preserves by fast moreover have "proj r (Eps (%y. y \ 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: "\ x \ A. f x \ B" -shows "\X \ A//r. univ f X \ B" + assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\ x \ A. f x \ B" + shows "\X \ A//r. univ f X \ B" proof fix X assume "X \ A//r" then obtain x where x: "x \ A" and X: "X = proj r x" using ECH proj_image[of r A] by blast diff -r f5d73caba4e5 -r a2a7c1de4752 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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') = diff -r f5d73caba4e5 -r a2a7c1de4752 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- 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 diff -r f5d73caba4e5 -r a2a7c1de4752 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- 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 diff -r f5d73caba4e5 -r a2a7c1de4752 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- 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 \ " ^ - (is_some eqn_data_disc_opt ? K (Syntax.string_of_term @{context} disc_concl ^ "\n \ ")) "" ^ - space_implode "\n \ " (map (Syntax.string_of_term @{context}) sel_concls) ^ - "\nfor premise(s)\n \ " ^ - space_implode "\n \ " (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 \ " ^ - space_implode "\n \ " (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 \ " ^ - space_implode "\n \ " (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))))