# HG changeset patch # User wenzelm # Date 1477597964 -7200 # Node ID efdd4c5daf7d66d05e98520c09b1aeaf7ebdd7fa # Parent 91eae3a1be515d0524f36711c8ccca4509018577# Parent 681fae6b00b5e118388ae4dc995a93401ece0190 merged diff -r 681fae6b00b5 -r efdd4c5daf7d Admin/components/components.sha1 --- a/Admin/components/components.sha1 Thu Oct 27 21:52:12 2016 +0200 +++ b/Admin/components/components.sha1 Thu Oct 27 21:52:44 2016 +0200 @@ -8,6 +8,7 @@ a5e02b5e990da4275dc5d4480c3b72fc73160c28 cvc4-1.5pre-1.tar.gz 4d9658fd2688ae8ac78da8fdfcbf85960f871b71 cvc4-1.5pre-2.tar.gz b01fdb93f2dc2b8bcfd41c6091d91b37d6e240f9 cvc4-1.5pre-3.tar.gz +76ff6103b8560f0e2778bbfbdb05f5fa18f850b7 cvc4-1.5pre-4.tar.gz 03aec2ec5757301c9df149f115d1f4f1d2cafd9e cvc4-1.5pre.tar.gz 842d9526f37b928cf9e22f141884365129990d63 cygwin-20130110.tar.gz cb3b0706d208f104b800267697204f6d82f7b48a cygwin-20130114.tar.gz diff -r 681fae6b00b5 -r efdd4c5daf7d Admin/components/main --- a/Admin/components/main Thu Oct 27 21:52:12 2016 +0200 +++ b/Admin/components/main Thu Oct 27 21:52:44 2016 +0200 @@ -1,7 +1,7 @@ #main components for everyday use, without big impact on overall build time bash_process-1.2.1 csdp-6.x -cvc4-1.5pre-3 +cvc4-1.5pre-4 e-1.8 Haskabelle-2015 isabelle_fonts-20160830 diff -r 681fae6b00b5 -r efdd4c5daf7d src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Thu Oct 27 21:52:12 2016 +0200 +++ b/src/HOL/Library/Multiset.thy Thu Oct 27 21:52:44 2016 +0200 @@ -495,6 +495,10 @@ then show ?thesis using B by simp qed +lemma add_mset_eq_singleton_iff[iff]: + "add_mset x M = {#y#} \ M = {#} \ x = y" + by auto + subsubsection \Pointwise ordering induced by count\ @@ -659,6 +663,15 @@ lemma Diff_eq_empty_iff_mset: "A - B = {#} \ A \# B" by (auto simp: multiset_eq_iff subseteq_mset_def) +lemma add_mset_subseteq_single_iff[iff]: "add_mset a M \# {#b#} \ M = {#} \ a = b" +proof + assume A: "add_mset a M \# {#b#}" + then have \a = b\ + by (auto dest: mset_subset_eq_insertD) + then show "M={#} \ a=b" + using A by (simp add: mset_subset_eq_add_mset_cancel) +qed simp + subsubsection \Intersection and bounded union\ @@ -1317,6 +1330,11 @@ lemma filter_filter_mset: "filter_mset P (filter_mset Q M) = {#x \# M. Q x \ P x#}" by (auto simp: multiset_eq_iff) +lemma + filter_mset_True[simp]: "{#y \# M. True#} = M" and + filter_mset_False[simp]: "{#y \# M. False#} = {#}" + by (auto simp: multiset_eq_iff) + subsubsection \Size\ @@ -2173,7 +2191,7 @@ lemma sum_mset_0_iff [simp]: "sum_mset M = (0::'a::canonically_ordered_monoid_add) \ (\x \ set_mset M. x = 0)" -by(induction M) (auto simp: add_eq_0_iff_both_eq_0) +by(induction M) auto lemma sum_mset_diff: fixes M N :: "('a :: ordered_cancel_comm_monoid_diff) multiset" @@ -2193,6 +2211,9 @@ lemma size_mset_set [simp]: "size (mset_set A) = card A" by (simp only: size_eq_sum_mset card_eq_sum sum_unfold_sum_mset) +lemma sum_mset_sum_list: "sum_mset (mset xs) = sum_list xs" + by (induction xs) auto + syntax (ASCII) "_sum_mset_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_add" ("(3SUM _:#_. _)" [0, 51, 10] 10) syntax @@ -2342,6 +2363,9 @@ then show ?thesis by (simp add: normalize_prod_mset) qed +lemma prod_mset_prod_list: "prod_mset (mset xs) = prod_list xs" + by (induct xs) auto + subsection \Alternative representations\ diff -r 681fae6b00b5 -r efdd4c5daf7d src/HOL/Library/Multiset_Order.thy --- a/src/HOL/Library/Multiset_Order.thy Thu Oct 27 21:52:12 2016 +0200 +++ b/src/HOL/Library/Multiset_Order.thy Thu Oct 27 21:52:44 2016 +0200 @@ -280,6 +280,12 @@ unfolding less_multiset\<^sub>H\<^sub>O by (metis count_greater_zero_iff le_imp_less_or_eq less_imp_not_less not_gr_zero union_iff) +lemma mset_lt_single_iff[iff]: "{#x#} < {#y#} \ x < y" + unfolding less_multiset\<^sub>H\<^sub>O by simp + +lemma mset_le_single_iff[iff]: "{#x#} \ {#y#} \ x \ y" for x y :: "'a::order" + unfolding less_eq_multiset\<^sub>H\<^sub>O by force + instance multiset :: (linorder) linordered_cancel_ab_semigroup_add by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq) diff -r 681fae6b00b5 -r efdd4c5daf7d src/HOL/Library/Tree.thy --- a/src/HOL/Library/Tree.thy Thu Oct 27 21:52:12 2016 +0200 +++ b/src/HOL/Library/Tree.thy Thu Oct 27 21:52:44 2016 +0200 @@ -141,6 +141,9 @@ lemma height_map_tree[simp]: "height (map_tree f t) = height t" by (induction t) auto +lemma height_le_size_tree: "height t \ size (t::'a tree)" +by (induction t) auto + lemma size1_height: "size t + 1 \ 2 ^ height (t::'a tree)" proof(induction t) case (Node l a r) diff -r 681fae6b00b5 -r efdd4c5daf7d src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Oct 27 21:52:12 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Oct 27 21:52:44 2016 +0200 @@ -117,10 +117,9 @@ local_theory -> Ctr_Sugar.ctr_sugar * local_theory val derive_map_set_rel_pred_thms: (string -> bool) -> BNF_Util.fp_kind -> int -> typ list -> typ list -> typ -> typ -> thm list -> thm list -> thm list -> thm list -> thm list -> - thm list -> thm list -> thm list -> thm list -> thm list -> string -> BNF_Def.bnf -> - BNF_Def.bnf list -> typ -> term -> thm -> thm -> thm -> thm list -> thm -> thm -> thm list -> - thm -> thm list -> thm list -> thm list -> typ list list -> Ctr_Sugar.ctr_sugar -> - local_theory -> + thm list -> thm list -> thm list -> thm list -> string -> BNF_Def.bnf -> BNF_Def.bnf list -> + typ -> term -> thm -> thm -> thm -> thm list -> thm -> thm -> thm list -> thm -> thm list -> + thm list -> thm list -> typ list list -> Ctr_Sugar.ctr_sugar -> local_theory -> (thm list * thm list * thm list list * thm list * thm list * thm list * thm list * thm list * thm list * thm list * thm list list list list * thm list list list list * thm list * thm list * thm list * thm list * thm list) * local_theory @@ -698,9 +697,9 @@ end; fun derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs fp_nesting_set_maps - fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_map_ident0s live_nesting_set_maps - live_nesting_rel_eqs live_nesting_rel_eq_onps fp_nested_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT - ctor ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm + fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs + live_nesting_rel_eq_onps fp_nested_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor + dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm extra_unfolds_map extra_unfolds_set extra_unfolds_rel ctr_Tss ({casex, case_thms, discs, selss, sel_defs, ctrs, exhaust, exhaust_discs, disc_thmss, sel_thmss, injects, distincts, distinct_discsss, ...} : ctr_sugar) @@ -742,7 +741,7 @@ let val argA_Ts = binder_types (fastype_of ctrA); val argB_Ts = binder_types (fastype_of ctrB); - val ((argAs, argBs), names_ctxt) = ctxt + val ((argAs, argBs), names_ctxt) = ctxt |> mk_Frees "x" argA_Ts ||>> mk_Frees "y" argB_Ts; val ctrA_args = list_comb (ctrA, argAs); @@ -810,6 +809,30 @@ val selAss = map (map (mk_disc_or_sel As)) selss; val selBss = map (map (mk_disc_or_sel Bs)) selss; + val map_ctor_thm = + if fp = Least_FP then + fp_map_thm + else + let + val ctorA = mk_ctor As ctor; + val ctorB = mk_ctor Bs ctor; + + val y_T = domain_type (fastype_of ctorA); + val (y as Free (y_s, _), _) = lthy + |> yield_singleton (mk_Frees "y") y_T; + + val ctor_cong = + infer_instantiate' lthy [NONE, NONE, SOME (Thm.cterm_of lthy ctorB)] arg_cong; + val fp_map_thm' = fp_map_thm + |> infer_instantiate' lthy (replicate live NONE @ + [SOME (Thm.cterm_of lthy (ctorA $ y))]) + |> unfold_thms lthy [dtor_ctor]; + + val map_ctor_thm0 = fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans); + in + Thm.generalize ([], [y_s]) (Thm.maxidx_of map_ctor_thm0 + 1) map_ctor_thm0 + end; + val map_thms = let fun mk_goal ctrA ctrB xs ys = @@ -828,22 +851,10 @@ val goals = @{map 4} mk_goal ctrAs ctrBs xss yss; val goal = Logic.mk_conjunction_balanced goals; val vars = Variable.add_free_names lthy goal []; - - val fp_map_thm' = - if fp = Least_FP then - fp_map_thm - else - let - val ctor' = mk_ctor Bs ctor; - val ctor_cong = - infer_instantiate' lthy [NONE, NONE, SOME (Thm.cterm_of lthy ctor')] arg_cong; - in - fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans) - end; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => - mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map_thm' - live_nesting_map_id0s ctr_defs' extra_unfolds_map) + mk_map_tac ctxt abs_inverses pre_map_def map_ctor_thm live_nesting_map_id0s ctr_defs' + extra_unfolds_map) |> Thm.close_derivation |> Conjunction.elim_balanced (length goals) end; @@ -880,6 +891,28 @@ val set_thms = set0_thms |> map (unfold_thms lthy @{thms insert_is_Un[THEN sym] Un_empty_left Un_insert_left}); + val rel_ctor_thm = + if fp = Least_FP then + fp_rel_thm + else + let + val ctorA = mk_ctor As ctor; + val ctorB = mk_ctor Bs ctor; + + val y_T = domain_type (fastype_of ctorA); + val z_T = domain_type (fastype_of ctorB); + val ((y as Free (y_s, _), z as Free (z_s, _)), _) = lthy + |> yield_singleton (mk_Frees "y") y_T + ||>> yield_singleton (mk_Frees "z") z_T; + + val rel_ctor_thm0 = fp_rel_thm + |> infer_instantiate' lthy (replicate live NONE @ + [SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))]) + |> unfold_thms lthy [dtor_ctor]; + in + Thm.generalize ([], [y_s, z_s]) (Thm.maxidx_of rel_ctor_thm0 + 1) rel_ctor_thm0 + end; + val rel_inject_thms = let fun mk_goal ctrA ctrB xs ys = @@ -897,8 +930,8 @@ val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => - mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel_thm live_nesting_rel_eqs - ctr_defs' extra_unfolds_rel) + mk_rel_tac ctxt abs_inverses pre_rel_def rel_ctor_thm live_nesting_rel_eqs ctr_defs' + extra_unfolds_rel) |> Thm.close_derivation |> Conjunction.elim_balanced (length goals) end; @@ -923,8 +956,8 @@ val vars = Variable.add_free_names lthy goal []; in Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} => - mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel_thm - live_nesting_rel_eqs ctr_defs' extra_unfolds_rel) + mk_rel_tac ctxt abs_inverses pre_rel_def rel_ctor_thm live_nesting_rel_eqs + ctr_defs' extra_unfolds_rel) |> Thm.close_derivation |> Conjunction.elim_balanced (length goals) end) @@ -2469,11 +2502,10 @@ disc_bindings sel_bindingss sel_default_eqs ctrs0 ctor_iff_dtor_thm ctr_defs #> (fn (ctr_sugar, lthy) => derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs - fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s - live_nesting_map_ident0s live_nesting_set_maps live_nesting_rel_eqs - live_nesting_rel_eq_onps [] fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor dtor_ctor - pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm [] [] [] ctr_Tss - ctr_sugar lthy + fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps + live_nesting_rel_eqs live_nesting_rel_eq_onps [] fp_b_name fp_bnf fp_bnfs fpT ctor + ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms + fp_rel_thm [] [] [] ctr_Tss ctr_sugar lthy |>> pair ctr_sugar) ##>> (if fp = Least_FP then define_rec (the recs_args_types) mk_binding fpTs Cs reps diff -r 681fae6b00b5 -r efdd4c5daf7d src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Oct 27 21:52:12 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Oct 27 21:52:44 2016 +0200 @@ -30,8 +30,8 @@ val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list -> thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic - val mk_map_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> thm list -> - thm list -> tactic + val mk_map_tac: Proof.context -> thm list -> thm -> thm -> thm list -> thm list -> thm list -> + tactic val mk_map_disc_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> thm list -> tactic @@ -39,8 +39,8 @@ tactic val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list -> term list list list list -> thm list -> thm list -> thm list -> thm list -> tactic - val mk_rel_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> thm list -> - thm list -> tactic + val mk_rel_tac: Proof.context -> thm list -> thm -> thm -> thm list -> thm list -> thm list -> + tactic val mk_rel_case_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list -> thm list -> thm list -> tactic val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list -> @@ -392,11 +392,11 @@ (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss selsss)); -fun mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map' live_nesting_map_id0s ctr_defs' +fun mk_map_tac ctxt abs_inverses pre_map_def map_ctor live_nesting_map_id0s ctr_defs' extra_unfolds = TRYALL Goal.conjunction_tac THEN - unfold_thms_tac ctxt (pre_map_def :: dtor_ctor :: fp_map' :: abs_inverses @ - live_nesting_map_id0s @ ctr_defs' @ extra_unfolds @ sumprod_thms_map @ + unfold_thms_tac ctxt (pre_map_def :: map_ctor :: abs_inverses @ live_nesting_map_id0s @ + ctr_defs' @ extra_unfolds @ sumprod_thms_map @ @{thms o_apply id_apply id_o o_id}) THEN ALLGOALS (rtac ctxt refl); @@ -419,11 +419,10 @@ unfold_thms_tac ctxt (@{thm id_apply} :: maps @ sels @ map_id0s) THEN ALLGOALS (rtac ctxt refl); -fun mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel live_nesting_rel_eqs ctr_defs' - extra_unfolds = +fun mk_rel_tac ctxt abs_inverses pre_rel_def rel_ctor live_nesting_rel_eqs ctr_defs' extra_unfolds = TRYALL Goal.conjunction_tac THEN - unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: fp_rel :: abs_inverses @ live_nesting_rel_eqs @ - ctr_defs' @ extra_unfolds @ sumprod_thms_rel @ @{thms vimage2p_def o_apply sum.inject + unfold_thms_tac ctxt (pre_rel_def :: rel_ctor :: abs_inverses @ live_nesting_rel_eqs @ ctr_defs' @ + extra_unfolds @ sumprod_thms_rel @ @{thms vimage2p_def o_apply sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]] not_False_eq_True}) THEN ALLGOALS (resolve_tac ctxt [TrueI, refl]);