# HG changeset patch # User wenzelm # Date 1428604958 -7200 # Node ID 09be0495dcc2015aea497ca978d59bbd1e672822 # Parent 7b80ddb65e3e18b3992404c704369d1ced98e97e# Parent a81dc82ecba3f7dc1abb30a40aa20bdf1f8d6c70 merged diff -r a81dc82ecba3 -r 09be0495dcc2 NEWS --- a/NEWS Thu Apr 09 20:42:32 2015 +0200 +++ b/NEWS Thu Apr 09 20:42:38 2015 +0200 @@ -339,6 +339,10 @@ \# ~> #\# \# ~> #\# INCOMPATIBILITY. + - Introduced abbreviations for ill-named multiset operations: + <#, \# abbreviate < (strict subset) + <=#, \#, \# abbreviate <= (subset or equal) + INCOMPATIBILITY. - Renamed in_multiset_of ~> in_multiset_in_set INCOMPATIBILITY. diff -r a81dc82ecba3 -r 09be0495dcc2 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Thu Apr 09 20:42:32 2015 +0200 +++ b/src/HOL/Library/Multiset.thy Thu Apr 09 20:42:38 2015 +0200 @@ -295,6 +295,18 @@ end +abbreviation less_mset :: "'a multiset \ 'a multiset \ bool" (infix "<#" 50) where + "A <# B \ A < B" +abbreviation (xsymbols) subset_mset :: "'a multiset \ 'a multiset \ bool" (infix "\#" 50) where + "A \# B \ A < B" + +abbreviation less_eq_mset :: "'a multiset \ 'a multiset \ bool" (infix "<=#" 50) where + "A <=# B \ A \ B" +abbreviation (xsymbols) leq_mset :: "'a multiset \ 'a multiset \ bool" (infix "\#" 50) where + "A \# B \ A \ B" +abbreviation (xsymbols) subseteq_mset :: "'a multiset \ 'a multiset \ bool" (infix "\#" 50) where + "A \# B \ A \ B" + lemma mset_less_eqI: "(\x. count A x \ count B x) \ A \ B" by (simp add: mset_le_def) diff -r a81dc82ecba3 -r 09be0495dcc2 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Apr 09 20:42:32 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Apr 09 20:42:38 2015 +0200 @@ -51,8 +51,8 @@ val massage_let_if_case: Proof.context -> (term -> bool) -> (typ list -> term -> term) -> typ list -> term -> term val massage_nested_corec_call: Proof.context -> (term -> bool) -> - (typ list -> typ -> typ -> term -> term) -> (typ -> typ -> term -> term) -> typ list -> typ -> - term -> term + (typ list -> typ -> typ -> term -> term) -> (typ list -> typ -> typ -> term -> term) -> + typ list -> typ -> typ -> term -> term val expand_to_ctr_term: Proof.context -> string -> typ list -> term -> term val massage_corec_code_rhs: Proof.context -> (typ list -> term -> term list -> term) -> typ list -> term -> term @@ -306,7 +306,7 @@ fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) = Ts ---> T; -fun massage_nested_corec_call ctxt has_call massage_call wrap_noncall bound_Ts U t0 = +fun massage_nested_corec_call ctxt has_call massage_call massage_noncall bound_Ts U T t0 = let fun check_no_call t = if has_call t then unexpected_corec_call ctxt [t0] t else (); @@ -314,7 +314,7 @@ (Type (@{type_name fun}, [T1, T2])) t = Abs (Name.uu, T1, massage_mutual_call bound_Ts U2 T2 (incr_boundvars 1 t $ Bound 0)) | massage_mutual_call bound_Ts U T t = - if has_call t then massage_call bound_Ts T U t else wrap_noncall T U t; + (if has_call t then massage_call else massage_noncall) bound_Ts U T t; fun massage_map bound_Ts (Type (_, Us)) (Type (s, Ts)) t = (case try (dest_map ctxt s) t of @@ -374,20 +374,20 @@ end | t1 $ t2 => (if has_call t2 then - massage_mutual_call bound_Ts U T t - else - massage_map bound_Ts U T t1 $ t2 - handle NO_MAP _ => massage_mutual_call bound_Ts U T t) + massage_mutual_call bound_Ts U T t + else + massage_map bound_Ts U T t1 $ t2 + handle NO_MAP _ => massage_mutual_call bound_Ts U T t) | Abs (s, T', t') => Abs (s, T', massage_any_call (T' :: bound_Ts) (range_type U) (range_type T) t') | _ => massage_mutual_call bound_Ts U T t)) | _ => ill_formed_corec_call ctxt t) else - wrap_noncall T U t) bound_Ts; + massage_noncall bound_Ts U T t) bound_Ts; val T = fastype_of1 (bound_Ts, t0); in - if has_call t0 then massage_any_call bound_Ts U T t0 else wrap_noncall T U t0 + (if has_call t0 then massage_any_call else massage_noncall) bound_Ts U T t0 end; fun expand_to_ctr_term ctxt s Ts t = @@ -894,7 +894,7 @@ NONE => I | SOME {fun_args, rhs_term, ...} => let - fun massage_call bound_Ts T U t0 = + fun massage_call bound_Ts U T t0 = let val U2 = (case try dest_sumT U of @@ -919,17 +919,16 @@ rewrite bound_Ts t0 end; - fun wrap_noncall T U t = build_map ctxt [] (uncurry Inl_const o dest_sumT o snd) (T, U) $ t; + fun massage_noncall bound_Ts U T t = + build_map ctxt [] (uncurry Inl_const o dest_sumT o snd) (T, U) $ t; val bound_Ts = List.rev (map fastype_of fun_args); - - fun build t = - rhs_term - |> massage_nested_corec_call ctxt has_call massage_call wrap_noncall bound_Ts - (range_type (fastype_of t)) - |> abs_tuple_balanced fun_args; in - build + fn t => + rhs_term + |> massage_nested_corec_call ctxt has_call massage_call massage_noncall bound_Ts + (range_type (fastype_of t)) (fastype_of1 (bound_Ts, rhs_term)) + |> abs_tuple_balanced fun_args end); fun build_corec_args_sel ctxt has_call (all_sel_eqns : coeqn_data_sel list) diff -r a81dc82ecba3 -r 09be0495dcc2 src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Apr 09 20:42:32 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Apr 09 20:42:38 2015 +0200 @@ -54,7 +54,7 @@ fun mk_abs_zero_nat T = Term.absdummy T HOLogic.zero; -fun mk_pointfull ctxt th = unfold_thms ctxt [o_apply] (th RS fun_cong); +fun mk_pointful ctxt thm = unfold_thms ctxt [o_apply] (thm RS fun_cong); fun mk_unabs_def_unused_0 n = funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong); @@ -235,7 +235,7 @@ (Spec_Rules.retrieve lthy0 @{const size ('a)} |> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm))); - val nested_size_maps = map (mk_pointfull lthy2) nested_size_gen_o_maps @ nested_size_gen_o_maps; + val nested_size_maps = map (mk_pointful lthy2) nested_size_gen_o_maps @ nested_size_gen_o_maps; val all_inj_maps = @{thm prod.inj_map} :: map inj_map_of_bnf (fp_bnfs @ fp_nesting_bnfs @ live_nesting_bnfs) |> distinct Thm.eq_thm_prop; diff -r a81dc82ecba3 -r 09be0495dcc2 src/HOL/ex/Refute_Examples.thy --- a/src/HOL/ex/Refute_Examples.thy Thu Apr 09 20:42:32 2015 +0200 +++ b/src/HOL/ex/Refute_Examples.thy Thu Apr 09 20:42:38 2015 +0200 @@ -259,15 +259,6 @@ refute [expect = genuine] oops -text {* "The union of transitive closures is equal to the transitive closure of unions." *} - -lemma "(\x y. (P x y | R x y) \ T x y) \ trans T \ (\Q. (\x y. (P x y | R x y) \ Q x y) \ trans Q \ subset T Q) - \ trans_closure TP P - \ trans_closure TR R - \ (T x y = (TP x y | TR x y))" -refute [expect = genuine] -oops - text {* "Every surjective function is invertible." *} lemma "(\y. \x. y = f x) \ (\g. \x. g (f x) = x)"