--- 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
--- 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
--- 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#} \<longleftrightarrow> M = {#} \<and> x = y"
+ by auto
+
subsubsection \<open>Pointwise ordering induced by count\<close>
@@ -659,6 +663,15 @@
lemma Diff_eq_empty_iff_mset: "A - B = {#} \<longleftrightarrow> A \<subseteq># B"
by (auto simp: multiset_eq_iff subseteq_mset_def)
+lemma add_mset_subseteq_single_iff[iff]: "add_mset a M \<subseteq># {#b#} \<longleftrightarrow> M = {#} \<and> a = b"
+proof
+ assume A: "add_mset a M \<subseteq># {#b#}"
+ then have \<open>a = b\<close>
+ by (auto dest: mset_subset_eq_insertD)
+ then show "M={#} \<and> a=b"
+ using A by (simp add: mset_subset_eq_add_mset_cancel)
+qed simp
+
subsubsection \<open>Intersection and bounded union\<close>
@@ -1317,6 +1330,11 @@
lemma filter_filter_mset: "filter_mset P (filter_mset Q M) = {#x \<in># M. Q x \<and> P x#}"
by (auto simp: multiset_eq_iff)
+lemma
+ filter_mset_True[simp]: "{#y \<in># M. True#} = M" and
+ filter_mset_False[simp]: "{#y \<in># M. False#} = {#}"
+ by (auto simp: multiset_eq_iff)
+
subsubsection \<open>Size\<close>
@@ -2173,7 +2191,7 @@
lemma sum_mset_0_iff [simp]:
"sum_mset M = (0::'a::canonically_ordered_monoid_add)
\<longleftrightarrow> (\<forall>x \<in> 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 \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> '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 \<open>Alternative representations\<close>
--- 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#} \<longleftrightarrow> x < y"
+ unfolding less_multiset\<^sub>H\<^sub>O by simp
+
+lemma mset_le_single_iff[iff]: "{#x#} \<le> {#y#} \<longleftrightarrow> x \<le> 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)
--- 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 \<le> size (t::'a tree)"
+by (induction t) auto
+
lemma size1_height: "size t + 1 \<le> 2 ^ height (t::'a tree)"
proof(induction t)
case (Node l a r)
--- 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
--- 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]);