--- a/NEWS Thu Apr 09 20:42:32 2015 +0200
+++ b/NEWS Thu Apr 09 20:42:38 2015 +0200
@@ -339,6 +339,10 @@
\<subset># ~> #\<subset>#
\<subseteq># ~> #\<subseteq>#
INCOMPATIBILITY.
+ - Introduced abbreviations for ill-named multiset operations:
+ <#, \<subset># abbreviate < (strict subset)
+ <=#, \<le>#, \<subseteq># abbreviate <= (subset or equal)
+ INCOMPATIBILITY.
- Renamed
in_multiset_of ~> in_multiset_in_set
INCOMPATIBILITY.
--- 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 \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
+ "A <# B \<equiv> A < B"
+abbreviation (xsymbols) subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50) where
+ "A \<subset># B \<equiv> A < B"
+
+abbreviation less_eq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
+ "A <=# B \<equiv> A \<le> B"
+abbreviation (xsymbols) leq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<le>#" 50) where
+ "A \<le># B \<equiv> A \<le> B"
+abbreviation (xsymbols) subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subseteq>#" 50) where
+ "A \<subseteq># B \<equiv> A \<le> B"
+
lemma mset_less_eqI:
"(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<le> B"
by (simp add: mset_le_def)
--- 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)
--- 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;
--- 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 "(\<forall>x y. (P x y | R x y) \<longrightarrow> T x y) \<longrightarrow> trans T \<longrightarrow> (\<forall>Q. (\<forall>x y. (P x y | R x y) \<longrightarrow> Q x y) \<longrightarrow> trans Q \<longrightarrow> subset T Q)
- \<longrightarrow> trans_closure TP P
- \<longrightarrow> trans_closure TR R
- \<longrightarrow> (T x y = (TP x y | TR x y))"
-refute [expect = genuine]
-oops
-
text {* "Every surjective function is invertible." *}
lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"