--- a/src/HOL/Combinatorics/Permutations.thy Sun Aug 25 21:27:25 2024 +0100
+++ b/src/HOL/Combinatorics/Permutations.thy Mon Aug 26 21:59:35 2024 +0100
@@ -377,13 +377,10 @@
lemma permutes_insert_lemma:
assumes "p permutes (insert a S)"
shows "transpose a (p a) \<circ> p permutes S"
- apply (rule permutes_superset[where S = "insert a S"])
- apply (rule permutes_compose[OF assms])
- apply (rule permutes_swap_id, simp)
- using permutes_in_image[OF assms, of a]
- apply simp
- apply (auto simp add: Ball_def)
- done
+proof (rule permutes_superset[where S = "insert a S"])
+ show "Transposition.transpose a (p a) \<circ> p permutes insert a S"
+ by (meson assms insertI1 permutes_compose permutes_in_image permutes_swap_id)
+qed auto
lemma permutes_insert: "{p. p permutes (insert a S)} =
(\<lambda>(b, p). transpose a b \<circ> p) ` {(b, p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}"
@@ -444,11 +441,7 @@
then have "finite ?pF"
by (auto intro: card_ge_0_finite)
with \<open>finite F\<close> card.insert_remove have pF'f: "finite ?pF'"
- apply (simp only: Collect_case_prod Collect_mem_eq)
- apply (rule finite_cartesian_product)
- apply simp_all
- done
-
+ by simp
have ginj: "inj_on ?g ?pF'"
proof -
{
@@ -593,21 +586,10 @@
declare permutation_id[unfolded id_def, simp]
lemma swapidseq_swap: "swapidseq (if a = b then 0 else 1) (transpose a b)"
- apply clarsimp
- using comp_Suc[of 0 id a b]
- apply simp
- done
+ using swapidseq.simps by fastforce
lemma permutation_swap_id: "permutation (transpose a b)"
-proof (cases "a = b")
- case True
- then show ?thesis by simp
-next
- case False
- then show ?thesis
- unfolding permutation_def
- using swapidseq_swap[of a b] by blast
-qed
+ by (meson permutation_def swapidseq_swap)
lemma swapidseq_comp_add: "swapidseq n p \<Longrightarrow> swapidseq m q \<Longrightarrow> swapidseq (n + m) (p \<circ> q)"
@@ -616,14 +598,8 @@
then show ?case by simp
next
case (comp_Suc n p a b m q)
- have eq: "Suc n + m = Suc (n + m)"
- by arith
- show ?case
- apply (simp only: eq comp_assoc)
- apply (rule swapidseq.comp_Suc)
- using comp_Suc.hyps(2)[OF comp_Suc.prems] comp_Suc.hyps(3)
- apply blast+
- done
+ then show ?case
+ by (metis add_Suc comp_assoc swapidseq.comp_Suc)
qed
lemma permutation_compose: "permutation p \<Longrightarrow> permutation q \<Longrightarrow> permutation (p \<circ> q)"
@@ -696,40 +672,19 @@
shows "\<And>a b c d. a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow> P a b c d"
using assms by metis
-lemma swap_general: "a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow>
- transpose a b \<circ> transpose c d = id \<or>
+lemma swap_general:
+ assumes "a \<noteq> b" "c \<noteq> d"
+ shows "transpose a b \<circ> transpose c d = id \<or>
(\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and>
transpose a b \<circ> transpose c d = transpose x y \<circ> transpose a z)"
-proof -
- assume neq: "a \<noteq> b" "c \<noteq> d"
- have "a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow>
- (transpose a b \<circ> transpose c d = id \<or>
- (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and>
- transpose a b \<circ> transpose c d = transpose x y \<circ> transpose a z))"
- apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d])
- apply (simp_all only: ac_simps)
- apply (metis id_comp swap_id_common swap_id_common' swap_id_independent transpose_comp_involutory)
- done
- with neq show ?thesis by metis
-qed
+ by (metis assms swap_id_common' swap_id_independent transpose_commute transpose_comp_involutory)
lemma swapidseq_id_iff[simp]: "swapidseq 0 p \<longleftrightarrow> p = id"
using swapidseq.cases[of 0 p "p = id"] by auto
lemma swapidseq_cases: "swapidseq n p \<longleftrightarrow>
n = 0 \<and> p = id \<or> (\<exists>a b q m. n = Suc m \<and> p = transpose a b \<circ> q \<and> swapidseq m q \<and> a \<noteq> b)"
- apply (rule iffI)
- apply (erule swapidseq.cases[of n p])
- apply simp
- apply (rule disjI2)
- apply (rule_tac x= "a" in exI)
- apply (rule_tac x= "b" in exI)
- apply (rule_tac x= "pa" in exI)
- apply (rule_tac x= "na" in exI)
- apply simp
- apply auto
- apply (rule comp_Suc, simp_all)
- done
+ by (meson comp_Suc id swapidseq.cases)
lemma fixing_swapidseq_decrease:
assumes "swapidseq n p"
@@ -757,33 +712,21 @@
then show ?thesis
by (simp only: cdqm o_assoc) (simp add: cdqm)
next
- case prems: 2
+ case 2
then have az: "a \<noteq> z"
by simp
- from prems have *: "(transpose x y \<circ> h) a = a \<longleftrightarrow> h a = a" for h
+ from 2 have *: "(transpose x y \<circ> h) a = a \<longleftrightarrow> h a = a" for h
by (simp add: transpose_def)
from cdqm(2) have "transpose a b \<circ> p = transpose a b \<circ> (transpose c d \<circ> q)"
by simp
- then have "transpose a b \<circ> p = transpose x y \<circ> (transpose a z \<circ> q)"
- by (simp add: o_assoc prems)
- then have "(transpose a b \<circ> p) a = (transpose x y \<circ> (transpose a z \<circ> q)) a"
- by simp
- then have "(transpose x y \<circ> (transpose a z \<circ> q)) a = a"
- unfolding Suc by metis
- then have "(transpose a z \<circ> q) a = a"
- by (simp only: *)
- from Suc.hyps[OF cdqm(3)[ unfolded cdqm(5)[symmetric]] az this]
- have **: "swapidseq (n - 1) (transpose a z \<circ> q)" "n \<noteq> 0"
- by blast+
- from \<open>n \<noteq> 0\<close> have ***: "Suc n - 1 = Suc (n - 1)"
+ then have \<section>: "transpose a b \<circ> p = transpose x y \<circ> (transpose a z \<circ> q)"
+ by (simp add: o_assoc 2)
+ obtain **: "swapidseq (n - 1) (transpose a z \<circ> q)" and "n\<noteq>0"
+ by (metis "*" "\<section>" Suc.hyps Suc.prems(3) az cdqm(3,5))
+ then have "Suc n - 1 = Suc (n - 1)"
by auto
- show ?thesis
- apply (simp only: cdqm(2) prems o_assoc ***)
- apply (simp only: Suc_not_Zero simp_thms comp_assoc)
- apply (rule comp_Suc)
- using ** prems
- apply blast+
- done
+ with 2 show ?thesis
+ using "**" \<section> swapidseq.simps by blast
qed
qed
@@ -829,15 +772,9 @@
qed
lemma evenperm_unique:
- assumes p: "swapidseq n p"
- and n:"even n = b"
+ assumes "swapidseq n p" and"even n = b"
shows "evenperm p = b"
- unfolding n[symmetric] evenperm_def
- apply (rule swapidseq_even_even[where p = p])
- apply (rule someI[where x = n])
- using p
- apply blast+
- done
+ by (metis evenperm_def assms someI swapidseq_even_even)
subsection \<open>And it has the expected composition properties\<close>
@@ -881,17 +818,7 @@
lemma permutation_bijective:
assumes "permutation p"
shows "bij p"
-proof -
- from assms obtain n where n: "swapidseq n p"
- unfolding permutation_def by blast
- from swapidseq_inverse_exists[OF n] obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id"
- by blast
- then show ?thesis
- unfolding bij_iff
- apply (auto simp add: fun_eq_iff)
- apply metis
- done
-qed
+ by (meson assms o_bij permutation_def swapidseq_inverse_exists)
lemma permutation_finite_support:
assumes "permutation p"
@@ -944,17 +871,7 @@
qed
lemma permutation: "permutation p \<longleftrightarrow> bij p \<and> finite {x. p x \<noteq> x}"
- (is "?lhs \<longleftrightarrow> ?b \<and> ?f")
-proof
- assume ?lhs
- with permutation_bijective permutation_finite_support show "?b \<and> ?f"
- by auto
-next
- assume "?b \<and> ?f"
- then have "?f" "?b" by blast+
- from permutation_lemma[OF this] show ?lhs
- by blast
-qed
+ using permutation_bijective permutation_finite_support permutation_lemma by auto
lemma permutation_inverse_works:
assumes "permutation p"
@@ -966,22 +883,7 @@
assumes p: "permutation p"
and q: "permutation q"
shows "inv (p \<circ> q) = inv q \<circ> inv p"
-proof -
- note ps = permutation_inverse_works[OF p]
- note qs = permutation_inverse_works[OF q]
- have "p \<circ> q \<circ> (inv q \<circ> inv p) = p \<circ> (q \<circ> inv q) \<circ> inv p"
- by (simp add: o_assoc)
- also have "\<dots> = id"
- by (simp add: ps qs)
- finally have *: "p \<circ> q \<circ> (inv q \<circ> inv p) = id" .
- have "inv q \<circ> inv p \<circ> (p \<circ> q) = inv q \<circ> (inv p \<circ> p) \<circ> q"
- by (simp add: o_assoc)
- also have "\<dots> = id"
- by (simp add: ps qs)
- finally have **: "inv q \<circ> inv p \<circ> (p \<circ> q) = id" .
- show ?thesis
- by (rule inv_unique_comp[OF * **])
-qed
+ by (simp add: o_inv_distrib p permutation_bijective q)
subsection \<open>Relation to \<open>permutes\<close>\<close>
@@ -1365,44 +1267,28 @@
from permutes_natset_le[OF permutes_inv[OF p] this] have "inv p = inv id"
by simp
then show ?thesis
- apply (subst permutes_inv_inv[OF p, symmetric])
- apply (rule inv_unique_comp)
- apply simp_all
- done
+ using p permutes_inv_inv by fastforce
qed
lemma image_inverse_permutations: "{inv p |p. p permutes S} = {p. p permutes S}"
- apply (rule set_eqI)
- apply auto
- using permutes_inv_inv permutes_inv
- apply auto
- apply (rule_tac x="inv x" in exI)
- apply auto
- done
+ using permutes_inv permutes_inv_inv by force
lemma image_compose_permutations_left:
assumes "q permutes S"
shows "{q \<circ> p |p. p permutes S} = {p. p permutes S}"
- apply (rule set_eqI)
- apply auto
- apply (rule permutes_compose)
- using assms
- apply auto
- apply (rule_tac x = "inv q \<circ> x" in exI)
- apply (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o)
- done
+proof -
+ have "\<And>p. p permutes S \<Longrightarrow> q \<circ> p permutes S"
+ by (simp add: assms permutes_compose)
+ moreover have "\<And>x. x permutes S \<Longrightarrow> \<exists>p. x = q \<circ> p \<and> p permutes S"
+ by (metis assms id_comp o_assoc permutes_compose permutes_inv permutes_inv_o(1))
+ ultimately show ?thesis
+ by auto
+qed
lemma image_compose_permutations_right:
assumes "q permutes S"
shows "{p \<circ> q | p. p permutes S} = {p . p permutes S}"
- apply (rule set_eqI)
- apply auto
- apply (rule permutes_compose)
- using assms
- apply auto
- apply (rule_tac x = "x \<circ> inv q" in exI)
- apply (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o comp_assoc)
- done
+ by (metis (no_types, opaque_lifting) assms comp_id fun.map_comp permutes_compose permutes_inv permutes_inv_o(2))
lemma permutes_in_seg: "p permutes {1 ..n} \<Longrightarrow> i \<in> {1..n} \<Longrightarrow> 1 \<le> p i \<and> p i \<le> n"
by (simp add: permutes_def) metis
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Sun Aug 25 21:27:25 2024 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Mon Aug 26 21:59:35 2024 +0100
@@ -326,13 +326,13 @@
lemma rel_fun_liminf[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal liminf liminf"
proof -
- have "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal (\<lambda>x. sup 0 (liminf x)) liminf"
+ have "\<forall>x y. rel_fun (=) pcr_ennreal x y \<longrightarrow> pcr_ennreal (sup 0 (liminf x)) (liminf y) \<Longrightarrow>
+ \<forall>x y. rel_fun (=) pcr_ennreal x y \<longrightarrow> pcr_ennreal (liminf x) (liminf y)"
+ by (auto simp: comp_def Liminf_bounded rel_fun_eq_pcr_ennreal)
+ moreover have "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal (\<lambda>x. sup 0 (liminf x)) liminf"
unfolding liminf_SUP_INF[abs_def] by (transfer_prover_start, transfer_step+; simp)
- then show ?thesis
- apply (subst (asm) (2) rel_fun_def)
- apply (subst (2) rel_fun_def)
- apply (auto simp: comp_def max.absorb2 Liminf_bounded rel_fun_eq_pcr_ennreal)
- done
+ ultimately show ?thesis
+ by (simp add: rel_fun_def)
qed
lemma rel_fun_limsup[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal limsup limsup"
@@ -633,9 +633,7 @@
unfolding divide_ennreal_def infinity_ennreal_def
apply transfer
subgoal for a b c
- apply (cases a b c rule: ereal3_cases)
- apply (auto simp: top_ereal_def)
- done
+ by (cases a b c rule: ereal3_cases) (auto simp: top_ereal_def)
done
lemma ennreal_mult_divide_eq:
@@ -798,7 +796,7 @@
obtains (real) r :: real where "0 \<le> r" "x = ennreal r" | (top) "x = top"
apply transfer
subgoal for x thesis
- by (cases x) (auto simp: max.absorb2 top_ereal_def)
+ by (cases x) (auto simp: top_ereal_def)
done
lemmas ennreal2_cases = ennreal_cases[case_product ennreal_cases]
@@ -1152,10 +1150,11 @@
(* Contributed by Dominique Unruh *)
lemma ennreal_of_enat_plus[simp]: \<open>ennreal_of_enat (a+b) = ennreal_of_enat a + ennreal_of_enat b\<close>
- apply (induct a)
- apply (metis enat.exhaust ennreal_add_eq_top ennreal_of_enat_enat ennreal_of_enat_infty infinity_ennreal_def of_nat_add plus_enat_simps(1) plus_eq_infty_iff_enat)
- apply simp
- done
+proof (induct a)
+ case (enat nat)
+ with enat.simps show ?case
+ by (smt (verit, del_insts) add.commute add_top_left_ennreal enat.exhaust enat_defs(4) ennreal_of_enat_def of_nat_add)
+qed auto
(* Contributed by Dominique Unruh *)
lemma sum_ennreal_of_enat[simp]: "(\<Sum>i\<in>I. ennreal_of_enat (f i)) = ennreal_of_enat (sum f I)"
@@ -1553,7 +1552,7 @@
have *: "e2ennreal (max x 0) = e2ennreal x" for x
by (simp add: e2ennreal_def max.commute)
have "((\<lambda>i. max (f i) 0) \<longlongrightarrow> max l 0) F"
- apply (intro tendsto_intros) using assms by auto
+ using assms by (intro tendsto_intros) auto
then have "((\<lambda>i. enn2ereal(e2ennreal (max (f i) 0))) \<longlongrightarrow> enn2ereal (e2ennreal (max l 0))) F"
by (subst enn2ereal_e2ennreal, auto)+
then have "((\<lambda>i. e2ennreal (max (f i) 0)) \<longlongrightarrow> e2ennreal (max l 0)) F"
@@ -1574,7 +1573,7 @@
apply transfer
subgoal for A
using Sup_countable_SUP[of A]
- by (force simp add: incseq_def[symmetric] SUP_upper2 max.absorb2 image_subset_iff Sup_upper2 cong: conj_cong)
+ by (force simp add: incseq_def[symmetric] SUP_upper2 image_subset_iff Sup_upper2 cong: conj_cong)
done
lemma ennreal_Inf_countable_INF:
@@ -1582,11 +1581,7 @@
unfolding decseq_def
apply transfer
subgoal for A
- using Inf_countable_INF[of A]
- apply (clarsimp simp flip: decseq_def)
- subgoal for f
- by (intro exI[of _ f]) auto
- done
+ using Inf_countable_INF[of A] by (simp flip: decseq_def) blast
done
lemma ennreal_SUP_countable_SUP:
@@ -1617,10 +1612,7 @@
lemma ennreal_suminf_SUP_eq:
fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ennreal"
shows "(\<And>i. incseq (\<lambda>n. f n i)) \<Longrightarrow> (\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
- apply (rule ennreal_suminf_SUP_eq_directed)
- subgoal for N n j
- by (auto simp: incseq_def intro!:exI[of _ "max n j"])
- done
+ by (metis ennreal_suminf_SUP_eq_directed incseqD nat_le_linear)
lemma ennreal_SUP_add_left:
fixes c :: ennreal
@@ -1792,6 +1784,7 @@
lemma ennreal_tendsto_top_eq_at_top:
"((\<lambda>z. ennreal (f z)) \<longlongrightarrow> top) F \<longleftrightarrow> (LIM z F. f z :> at_top)"
unfolding filterlim_at_top_dense tendsto_top_iff_ennreal
+ using ennreal_less_iff eventually_mono
apply (auto simp: ennreal_less_iff)
subgoal for y
by (auto elim!: eventually_mono allE[of _ "max 0 y"])
--- a/src/HOL/Library/Finite_Map.thy Sun Aug 25 21:27:25 2024 +0100
+++ b/src/HOL/Library/Finite_Map.thy Mon Aug 26 21:59:35 2024 +0100
@@ -500,7 +500,7 @@
lift_definition fmadd :: "('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap" (infixl "++\<^sub>f" 100)
is map_add
parametric map_add_transfer
-by simp
+ by simp
lemma fmlookup_add[simp]:
"fmlookup (m ++\<^sub>f n) x = (if x |\<in>| fmdom n then fmlookup n x else fmlookup m x)"
@@ -510,67 +510,63 @@
lemma fmdom'_add[simp]: "fmdom' (m ++\<^sub>f n) = fmdom' m \<union> fmdom' n" by transfer' auto
lemma fmadd_drop_left_dom: "fmdrop_fset (fmdom n) m ++\<^sub>f n = m ++\<^sub>f n"
-by (rule fmap_ext) auto
+ by (rule fmap_ext) auto
lemma fmadd_restrict_right_dom: "fmrestrict_fset (fmdom n) (m ++\<^sub>f n) = n"
-by (rule fmap_ext) auto
+ by (rule fmap_ext) auto
lemma fmfilter_add_distrib[simp]: "fmfilter P (m ++\<^sub>f n) = fmfilter P m ++\<^sub>f fmfilter P n"
-by transfer' (auto simp: map_filter_def map_add_def)
+ by transfer' (auto simp: map_filter_def map_add_def)
lemma fmdrop_add_distrib[simp]: "fmdrop a (m ++\<^sub>f n) = fmdrop a m ++\<^sub>f fmdrop a n"
-unfolding fmfilter_alt_defs by simp
+ unfolding fmfilter_alt_defs by simp
lemma fmdrop_set_add_distrib[simp]: "fmdrop_set A (m ++\<^sub>f n) = fmdrop_set A m ++\<^sub>f fmdrop_set A n"
-unfolding fmfilter_alt_defs by simp
+ unfolding fmfilter_alt_defs by simp
lemma fmdrop_fset_add_distrib[simp]: "fmdrop_fset A (m ++\<^sub>f n) = fmdrop_fset A m ++\<^sub>f fmdrop_fset A n"
-unfolding fmfilter_alt_defs by simp
+ unfolding fmfilter_alt_defs by simp
lemma fmrestrict_set_add_distrib[simp]:
"fmrestrict_set A (m ++\<^sub>f n) = fmrestrict_set A m ++\<^sub>f fmrestrict_set A n"
-unfolding fmfilter_alt_defs by simp
+ unfolding fmfilter_alt_defs by simp
lemma fmrestrict_fset_add_distrib[simp]:
"fmrestrict_fset A (m ++\<^sub>f n) = fmrestrict_fset A m ++\<^sub>f fmrestrict_fset A n"
-unfolding fmfilter_alt_defs by simp
+ unfolding fmfilter_alt_defs by simp
lemma fmadd_empty[simp]: "fmempty ++\<^sub>f m = m" "m ++\<^sub>f fmempty = m"
-by (transfer'; auto)+
+ by (transfer'; auto)+
lemma fmadd_idempotent[simp]: "m ++\<^sub>f m = m"
-by transfer' (auto simp: map_add_def split: option.splits)
+ by transfer' (auto simp: map_add_def split: option.splits)
lemma fmadd_assoc[simp]: "m ++\<^sub>f (n ++\<^sub>f p) = m ++\<^sub>f n ++\<^sub>f p"
-by transfer' simp
+ by transfer' simp
lemma fmadd_fmupd[simp]: "m ++\<^sub>f fmupd a b n = fmupd a b (m ++\<^sub>f n)"
-by (rule fmap_ext) simp
+ by (rule fmap_ext) simp
lift_definition fmpred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> bool"
is map_pred
parametric map_pred_transfer
-.
+ .
lemma fmpredI[intro]:
assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x y"
shows "fmpred P m"
-using assms
-by transfer' (auto simp: map_pred_def split: option.splits)
+ using assms
+ by transfer' (auto simp: map_pred_def split: option.splits)
lemma fmpredD[dest]: "fmpred P m \<Longrightarrow> fmlookup m x = Some y \<Longrightarrow> P x y"
-by transfer' (auto simp: map_pred_def split: option.split_asm)
+ by transfer' (auto simp: map_pred_def split: option.split_asm)
lemma fmpred_iff: "fmpred P m \<longleftrightarrow> (\<forall>x y. fmlookup m x = Some y \<longrightarrow> P x y)"
-by auto
+ by auto
lemma fmpred_alt_def: "fmpred P m \<longleftrightarrow> fBall (fmdom m) (\<lambda>x. P x (the (fmlookup m x)))"
-unfolding fmpred_iff
-apply auto
-apply (rename_tac x y)
-apply (erule_tac x = x in fBallE)
-apply simp
-by (simp add: fmlookup_dom_iff)
+ unfolding fmpred_iff
+ using fmdomI by fastforce
lemma fmpred_mono_strong:
assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x y \<Longrightarrow> Q x y"
@@ -578,40 +574,37 @@
using assms unfolding fmpred_iff by auto
lemma fmpred_mono[mono]: "P \<le> Q \<Longrightarrow> fmpred P \<le> fmpred Q"
-apply rule
-apply (rule fmpred_mono_strong[where P = P and Q = Q])
-apply auto
-done
+ by auto
lemma fmpred_empty[intro!, simp]: "fmpred P fmempty"
-by auto
+ by auto
lemma fmpred_upd[intro]: "fmpred P m \<Longrightarrow> P x y \<Longrightarrow> fmpred P (fmupd x y m)"
-by transfer' (auto simp: map_pred_def map_upd_def)
+ by transfer' (auto simp: map_pred_def map_upd_def)
lemma fmpred_updD[dest]: "fmpred P (fmupd x y m) \<Longrightarrow> P x y"
-by auto
+ by auto
lemma fmpred_add[intro]: "fmpred P m \<Longrightarrow> fmpred P n \<Longrightarrow> fmpred P (m ++\<^sub>f n)"
-by transfer' (auto simp: map_pred_def map_add_def split: option.splits)
+ by transfer' (auto simp: map_pred_def map_add_def split: option.splits)
lemma fmpred_filter[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmfilter Q m)"
-by transfer' (auto simp: map_pred_def map_filter_def)
+ by transfer' (auto simp: map_pred_def map_filter_def)
lemma fmpred_drop[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop a m)"
-by (auto simp: fmfilter_alt_defs)
+ by (auto simp: fmfilter_alt_defs)
lemma fmpred_drop_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_set A m)"
-by (auto simp: fmfilter_alt_defs)
+ by (auto simp: fmfilter_alt_defs)
lemma fmpred_drop_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_fset A m)"
-by (auto simp: fmfilter_alt_defs)
+ by (auto simp: fmfilter_alt_defs)
lemma fmpred_restrict_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_set A m)"
-by (auto simp: fmfilter_alt_defs)
+ by (auto simp: fmfilter_alt_defs)
lemma fmpred_restrict_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_fset A m)"
-by (auto simp: fmfilter_alt_defs)
+ by (auto simp: fmfilter_alt_defs)
lemma fmpred_cases[consumes 1]:
assumes "fmpred P m"
@@ -667,18 +660,18 @@
unfolding fmfilter_alt_defs by (rule fmfilter_subset)
lift_definition fset_of_fmap :: "('a, 'b) fmap \<Rightarrow> ('a \<times> 'b) fset" is set_of_map
-by (rule set_of_map_finite)
+ by (rule set_of_map_finite)
lemma fset_of_fmap_inj[intro, simp]: "inj fset_of_fmap"
-apply rule
-apply transfer'
-using set_of_map_inj unfolding inj_def by auto
+ apply rule
+ apply transfer'
+ using set_of_map_inj unfolding inj_def by auto
lemma fset_of_fmap_iff[simp]: "(a, b) |\<in>| fset_of_fmap m \<longleftrightarrow> fmlookup m a = Some b"
by transfer' (auto simp: set_of_map_def)
-lemma fset_of_fmap_iff'[simp]: "(a, b) \<in> fset (fset_of_fmap m) \<longleftrightarrow> fmlookup m a = Some b"
-by transfer' (auto simp: set_of_map_def)
+lemma fset_of_fmap_iff': "(a, b) \<in> fset (fset_of_fmap m) \<longleftrightarrow> fmlookup m a = Some b"
+ by simp
lift_definition fmap_of_list :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) fmap"
is map_of
@@ -688,28 +681,25 @@
lemma fmap_of_list_simps[simp]:
"fmap_of_list [] = fmempty"
"fmap_of_list ((k, v) # kvs) = fmupd k v (fmap_of_list kvs)"
-by (transfer, simp add: map_upd_def)+
+ by (transfer, simp add: map_upd_def)+
lemma fmap_of_list_app[simp]: "fmap_of_list (xs @ ys) = fmap_of_list ys ++\<^sub>f fmap_of_list xs"
-by transfer' simp
+ by transfer' simp
lemma fmupd_alt_def: "fmupd k v m = m ++\<^sub>f fmap_of_list [(k, v)]"
-by transfer' (auto simp: map_upd_def)
+ by simp
lemma fmpred_of_list[intro]:
assumes "\<And>k v. (k, v) \<in> set xs \<Longrightarrow> P k v"
shows "fmpred P (fmap_of_list xs)"
-using assms
-by (induction xs) (transfer'; auto simp: map_pred_def)+
+ using assms
+ by (induction xs) (transfer'; auto simp: map_pred_def)+
lemma fmap_of_list_SomeD: "fmlookup (fmap_of_list xs) k = Some v \<Longrightarrow> (k, v) \<in> set xs"
-by transfer' (auto dest: map_of_SomeD)
+ by transfer' (auto dest: map_of_SomeD)
lemma fmdom_fmap_of_list[simp]: "fmdom (fmap_of_list xs) = fset_of_list (map fst xs)"
-apply transfer'
-apply (subst dom_map_of_conv_image_fst)
-apply auto
-done
+ by transfer' (simp add: dom_map_of_conv_image_fst)
lift_definition fmrel_on_fset :: "'a fset \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap \<Rightarrow> bool"
is rel_map_on_set
@@ -721,109 +711,103 @@
lemma fmrel_on_fsetI[intro]:
assumes "\<And>x. x |\<in>| S \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
shows "fmrel_on_fset S P m n"
-using assms
-unfolding fmrel_on_fset_alt_def by auto
+ by (simp add: assms fmrel_on_fset_alt_def)
lemma fmrel_on_fset_mono[mono]: "R \<le> Q \<Longrightarrow> fmrel_on_fset S R \<le> fmrel_on_fset S Q"
-unfolding fmrel_on_fset_alt_def[abs_def]
-apply (intro le_funI fBall_mono)
-using option.rel_mono by auto
+ unfolding fmrel_on_fset_alt_def[abs_def]
+ using option.rel_mono by blast
lemma fmrel_on_fsetD: "x |\<in>| S \<Longrightarrow> fmrel_on_fset S P m n \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
-unfolding fmrel_on_fset_alt_def
-by auto
+ unfolding fmrel_on_fset_alt_def
+ by auto
lemma fmrel_on_fsubset: "fmrel_on_fset S R m n \<Longrightarrow> T |\<subseteq>| S \<Longrightarrow> fmrel_on_fset T R m n"
-unfolding fmrel_on_fset_alt_def
-by auto
+ unfolding fmrel_on_fset_alt_def
+ by auto
lemma fmrel_on_fset_unionI:
"fmrel_on_fset A R m n \<Longrightarrow> fmrel_on_fset B R m n \<Longrightarrow> fmrel_on_fset (A |\<union>| B) R m n"
-unfolding fmrel_on_fset_alt_def
-by auto
+ unfolding fmrel_on_fset_alt_def
+ by auto
lemma fmrel_on_fset_updateI:
assumes "fmrel_on_fset S P m n" "P v\<^sub>1 v\<^sub>2"
shows "fmrel_on_fset (finsert k S) P (fmupd k v\<^sub>1 m) (fmupd k v\<^sub>2 n)"
-using assms
-unfolding fmrel_on_fset_alt_def
-by auto
+ using assms
+ unfolding fmrel_on_fset_alt_def
+ by auto
lift_definition fmimage :: "('a, 'b) fmap \<Rightarrow> 'a fset \<Rightarrow> 'b fset" is "\<lambda>m S. {b|a b. m a = Some b \<and> a \<in> S}"
-subgoal for m S
- apply (rule finite_subset[where B = "ran m"])
- apply (auto simp: ran_def)[]
- by (rule finite_ran)
-done
+ by (smt (verit, del_insts) Collect_mono_iff finite_surj ran_alt_def ran_def)
lemma fmimage_alt_def: "fmimage m S = fmran (fmrestrict_fset S m)"
-by transfer' (auto simp: ran_def map_restrict_set_def map_filter_def)
+ by transfer' (auto simp: ran_def map_restrict_set_def map_filter_def)
lemma fmimage_empty[simp]: "fmimage m fempty = fempty"
-by transfer' auto
+ by transfer' auto
lemma fmimage_subset_ran[simp]: "fmimage m S |\<subseteq>| fmran m"
-by transfer' (auto simp: ran_def)
+ by transfer' (auto simp: ran_def)
lemma fmimage_dom[simp]: "fmimage m (fmdom m) = fmran m"
-by transfer' (auto simp: ran_def)
+ by transfer' (auto simp: ran_def)
lemma fmimage_inter: "fmimage m (A |\<inter>| B) |\<subseteq>| fmimage m A |\<inter>| fmimage m B"
-by transfer' auto
+ by transfer' auto
lemma fimage_inter_dom[simp]:
"fmimage m (fmdom m |\<inter>| A) = fmimage m A"
"fmimage m (A |\<inter>| fmdom m) = fmimage m A"
-by (transfer'; auto)+
+ by (transfer'; auto)+
lemma fmimage_union[simp]: "fmimage m (A |\<union>| B) = fmimage m A |\<union>| fmimage m B"
-by transfer' auto
+ by transfer' auto
lemma fmimage_Union[simp]: "fmimage m (ffUnion A) = ffUnion (fmimage m |`| A)"
-by transfer' auto
+ by transfer' auto
lemma fmimage_filter[simp]: "fmimage (fmfilter P m) A = fmimage m (ffilter P A)"
-by transfer' (auto simp: map_filter_def)
+ by transfer' (auto simp: map_filter_def)
lemma fmimage_drop[simp]: "fmimage (fmdrop a m) A = fmimage m (A - {|a|})"
-by transfer' (auto simp: map_filter_def map_drop_def)
+ by (simp add: fmimage_alt_def)
lemma fmimage_drop_fset[simp]: "fmimage (fmdrop_fset B m) A = fmimage m (A - B)"
-by transfer' (auto simp: map_filter_def map_drop_set_def)
+ by transfer' (auto simp: map_filter_def map_drop_set_def)
lemma fmimage_restrict_fset[simp]: "fmimage (fmrestrict_fset B m) A = fmimage m (A |\<inter>| B)"
-by transfer' (auto simp: map_filter_def map_restrict_set_def)
+ by transfer' (auto simp: map_filter_def map_restrict_set_def)
lemma fmfilter_ran[simp]: "fmran (fmfilter P m) = fmimage m (ffilter P (fmdom m))"
-by transfer' (auto simp: ran_def map_filter_def)
+ by transfer' (auto simp: ran_def map_filter_def)
lemma fmran_drop[simp]: "fmran (fmdrop a m) = fmimage m (fmdom m - {|a|})"
-by transfer' (auto simp: ran_def map_drop_def map_filter_def)
+ by transfer' (auto simp: ran_def map_drop_def map_filter_def)
lemma fmran_drop_fset[simp]: "fmran (fmdrop_fset A m) = fmimage m (fmdom m - A)"
-by transfer' (auto simp: ran_def map_drop_set_def map_filter_def)
+ by transfer' (auto simp: ran_def map_drop_set_def map_filter_def)
lemma fmran_restrict_fset: "fmran (fmrestrict_fset A m) = fmimage m (fmdom m |\<inter>| A)"
-by transfer' (auto simp: ran_def map_restrict_set_def map_filter_def)
+ by transfer' (auto simp: ran_def map_restrict_set_def map_filter_def)
lemma fmlookup_image_iff: "y |\<in>| fmimage m A \<longleftrightarrow> (\<exists>x. fmlookup m x = Some y \<and> x |\<in>| A)"
-by transfer' (auto simp: ran_def)
+ by transfer' (auto simp: ran_def)
lemma fmimageI: "fmlookup m x = Some y \<Longrightarrow> x |\<in>| A \<Longrightarrow> y |\<in>| fmimage m A"
-by (auto simp: fmlookup_image_iff)
+ by (auto simp: fmlookup_image_iff)
lemma fmimageE[elim]:
assumes "y |\<in>| fmimage m A"
obtains x where "fmlookup m x = Some y" "x |\<in>| A"
-using assms by (auto simp: fmlookup_image_iff)
+ using assms by (auto simp: fmlookup_image_iff)
lift_definition fmcomp :: "('b, 'c) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap" (infixl "\<circ>\<^sub>f" 55)
is map_comp
parametric map_comp_transfer
-by (rule dom_comp_finite)
+ by (rule dom_comp_finite)
lemma fmlookup_comp[simp]: "fmlookup (m \<circ>\<^sub>f n) x = Option.bind (fmlookup n x) (fmlookup m)"
-by transfer' (auto simp: map_comp_def split: option.splits)
+ by transfer' (auto simp: map_comp_def split: option.splits)
end
@@ -839,13 +823,14 @@
lemma fmran'_alt_def: "fmran' m = fset (fmran m)"
-including fset.lifting
-by transfer' (auto simp: ran_def fun_eq_iff)
+ including fset.lifting
+ by transfer' (auto simp: ran_def fun_eq_iff)
lemma fmlookup_ran'_iff: "y \<in> fmran' m \<longleftrightarrow> (\<exists>x. fmlookup m x = Some y)"
-by transfer' (auto simp: ran_def)
+ by transfer' (auto simp: ran_def)
-lemma fmran'I: "fmlookup m x = Some y \<Longrightarrow> y \<in> fmran' m" by (auto simp: fmlookup_ran'_iff)
+lemma fmran'I: "fmlookup m x = Some y \<Longrightarrow> y \<in> fmran' m"
+ by (auto simp: fmlookup_ran'_iff)
lemma fmran'E[elim]:
assumes "y \<in> fmran' m"
@@ -858,22 +843,19 @@
lemma fmrelI[intro]:
assumes "\<And>x. rel_option R (fmlookup m x) (fmlookup n x)"
shows "fmrel R m n"
-using assms
-by transfer' auto
+ using assms
+ by transfer' auto
lemma fmrel_upd[intro]: "fmrel P m n \<Longrightarrow> P x y \<Longrightarrow> fmrel P (fmupd k x m) (fmupd k y n)"
-by transfer' (auto simp: map_upd_def rel_fun_def)
+ by transfer' (auto simp: map_upd_def rel_fun_def)
lemma fmrelD[dest]: "fmrel P m n \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
-by transfer' (auto simp: rel_fun_def)
+ by transfer' (auto simp: rel_fun_def)
lemma fmrel_addI[intro]:
assumes "fmrel P m n" "fmrel P a b"
shows "fmrel P (m ++\<^sub>f a) (n ++\<^sub>f b)"
-using assms
-apply transfer'
-apply (auto simp: rel_fun_def map_add_def)
-by (metis option.case_eq_if option.collapse option.rel_sel)
+ by (smt (verit, del_insts) assms domIff fmdom.rep_eq fmlookup_add fmrel_iff option.rel_sel)
lemma fmrel_cases[consumes 1]:
assumes "fmrel P m n"
@@ -974,72 +956,77 @@
qed
lemma fmrel_rel_fmran': "fmrel P x y \<Longrightarrow> rel_set P (fmran' x) (fmran' y)"
-unfolding fmran'_alt_def
-by (metis fmrel_rel_fmran rel_fset_fset)
+ unfolding fmran'_alt_def
+ by (metis fmrel_rel_fmran rel_fset_fset)
lemma pred_fmap_fmpred[simp]: "pred_fmap P = fmpred (\<lambda>_. P)"
-unfolding fmap.pred_set fmran'_alt_def
-including fset.lifting
-apply transfer'
-apply (rule ext)
-apply (auto simp: map_pred_def ran_def split: option.splits dest: )
-done
+ unfolding fmap.pred_set fmran'_alt_def
+ using fmranI by fastforce
lemma pred_fmap_id[simp]: "pred_fmap id (fmmap f m) \<longleftrightarrow> pred_fmap f m"
-unfolding fmap.pred_set fmap.set_map
-by simp
+ unfolding fmap.pred_set fmap.set_map
+ by simp
lemma pred_fmapD: "pred_fmap P m \<Longrightarrow> x |\<in>| fmran m \<Longrightarrow> P x"
-by auto
+ by auto
lemma fmlookup_map[simp]: "fmlookup (fmmap f m) x = map_option f (fmlookup m x)"
-by transfer' auto
+ by transfer' auto
lemma fmpred_map[simp]: "fmpred P (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>k v. P k (f v)) m"
-unfolding fmpred_iff pred_fmap_def fmap.set_map
-by auto
+ unfolding fmpred_iff pred_fmap_def fmap.set_map
+ by auto
lemma fmpred_id[simp]: "fmpred (\<lambda>_. id) (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>_. f) m"
-by simp
+ by simp
lemma fmmap_add[simp]: "fmmap f (m ++\<^sub>f n) = fmmap f m ++\<^sub>f fmmap f n"
-by transfer' (auto simp: map_add_def fun_eq_iff split: option.splits)
+ by transfer' (auto simp: map_add_def fun_eq_iff split: option.splits)
lemma fmmap_empty[simp]: "fmmap f fmempty = fmempty"
-by transfer auto
+ by transfer auto
lemma fmdom_map[simp]: "fmdom (fmmap f m) = fmdom m"
-including fset.lifting
-by transfer' simp
+ including fset.lifting
+ by transfer' simp
lemma fmdom'_map[simp]: "fmdom' (fmmap f m) = fmdom' m"
-by transfer' simp
+ by transfer' simp
lemma fmran_fmmap[simp]: "fmran (fmmap f m) = f |`| fmran m"
-including fset.lifting
-by transfer' (auto simp: ran_def)
+ including fset.lifting
+ by transfer' (auto simp: ran_def)
lemma fmran'_fmmap[simp]: "fmran' (fmmap f m) = f ` fmran' m"
-by transfer' (auto simp: ran_def)
+ by transfer' (auto simp: ran_def)
lemma fmfilter_fmmap[simp]: "fmfilter P (fmmap f m) = fmmap f (fmfilter P m)"
-by transfer' (auto simp: map_filter_def)
+ by transfer' (auto simp: map_filter_def)
+
+lemma fmdrop_fmmap[simp]: "fmdrop a (fmmap f m) = fmmap f (fmdrop a m)"
+ unfolding fmfilter_alt_defs by simp
+
+lemma fmdrop_set_fmmap[simp]: "fmdrop_set A (fmmap f m) = fmmap f (fmdrop_set A m)"
+ unfolding fmfilter_alt_defs by simp
-lemma fmdrop_fmmap[simp]: "fmdrop a (fmmap f m) = fmmap f (fmdrop a m)" unfolding fmfilter_alt_defs by simp
-lemma fmdrop_set_fmmap[simp]: "fmdrop_set A (fmmap f m) = fmmap f (fmdrop_set A m)" unfolding fmfilter_alt_defs by simp
-lemma fmdrop_fset_fmmap[simp]: "fmdrop_fset A (fmmap f m) = fmmap f (fmdrop_fset A m)" unfolding fmfilter_alt_defs by simp
-lemma fmrestrict_set_fmmap[simp]: "fmrestrict_set A (fmmap f m) = fmmap f (fmrestrict_set A m)" unfolding fmfilter_alt_defs by simp
-lemma fmrestrict_fset_fmmap[simp]: "fmrestrict_fset A (fmmap f m) = fmmap f (fmrestrict_fset A m)" unfolding fmfilter_alt_defs by simp
+lemma fmdrop_fset_fmmap[simp]: "fmdrop_fset A (fmmap f m) = fmmap f (fmdrop_fset A m)"
+ unfolding fmfilter_alt_defs by simp
+
+lemma fmrestrict_set_fmmap[simp]: "fmrestrict_set A (fmmap f m) = fmmap f (fmrestrict_set A m)"
+ unfolding fmfilter_alt_defs by simp
+
+lemma fmrestrict_fset_fmmap[simp]: "fmrestrict_fset A (fmmap f m) = fmmap f (fmrestrict_fset A m)"
+ unfolding fmfilter_alt_defs by simp
lemma fmmap_subset[intro]: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmmap f m \<subseteq>\<^sub>f fmmap f n"
-by transfer' (auto simp: map_le_def)
+ by transfer' (auto simp: map_le_def)
lemma fmmap_fset_of_fmap: "fset_of_fmap (fmmap f m) = (\<lambda>(k, v). (k, f v)) |`| fset_of_fmap m"
-including fset.lifting
-by transfer' (auto simp: set_of_map_def)
+ including fset.lifting
+ by transfer' (auto simp: set_of_map_def)
lemma fmmap_fmupd: "fmmap f (fmupd x y m) = fmupd x (f y) (fmmap f m)"
-by transfer' (auto simp: fun_eq_iff map_upd_def)
+ by transfer' (auto simp: fun_eq_iff map_upd_def)
subsection \<open>\<^const>\<open>size\<close> setup\<close>
@@ -1056,20 +1043,18 @@
end
lemma size_fmap_overloaded_simps[simp]: "size x = size (fset_of_fmap x)"
-unfolding size_fmap_overloaded_def
-by simp
+ unfolding size_fmap_overloaded_def
+ by simp
-lemma fmap_size_o_map: "inj h \<Longrightarrow> size_fmap f g \<circ> fmmap h = size_fmap f (g \<circ> h)"
+lemma fmap_size_o_map: "size_fmap f g \<circ> fmmap h = size_fmap f (g \<circ> h)"
+proof -
+ have inj: "inj_on (\<lambda>(k, v). (k, h v)) (fset (fset_of_fmap m))" for m
+ using inj_on_def by force
+ show ?thesis
unfolding size_fmap_def
- apply (auto simp: fun_eq_iff fmmap_fset_of_fmap)
- apply (subst sum.reindex)
- subgoal for m
- using prod.inj_map[unfolded map_prod_def, of "\<lambda>x. x" h]
- unfolding inj_on_def
- by auto
- subgoal
- by (rule sum.cong) (auto split: prod.splits)
- done
+ apply (clarsimp simp: fun_eq_iff fmmap_fset_of_fmap sum.reindex [OF inj])
+ by (rule sum.cong) (auto split: prod.splits)
+qed
setup \<open>
BNF_LFP_Size.register_size_global \<^type_name>\<open>fmap\<close> \<^const_name>\<open>size_fmap\<close>
@@ -1082,53 +1067,51 @@
lift_definition fmmap_keys :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap" is
"\<lambda>f m a. map_option (f a) (m a)"
-unfolding dom_def
-by simp
+ unfolding dom_def
+ by simp
lemma fmpred_fmmap_keys[simp]: "fmpred P (fmmap_keys f m) = fmpred (\<lambda>a b. P a (f a b)) m"
-by transfer' (auto simp: map_pred_def split: option.splits)
+ by transfer' (auto simp: map_pred_def split: option.splits)
lemma fmdom_fmmap_keys[simp]: "fmdom (fmmap_keys f m) = fmdom m"
-including fset.lifting
-by transfer' auto
+ including fset.lifting
+ by transfer' auto
lemma fmlookup_fmmap_keys[simp]: "fmlookup (fmmap_keys f m) x = map_option (f x) (fmlookup m x)"
-by transfer' simp
+ by transfer' simp
lemma fmfilter_fmmap_keys[simp]: "fmfilter P (fmmap_keys f m) = fmmap_keys f (fmfilter P m)"
-by transfer' (auto simp: map_filter_def)
+ by transfer' (auto simp: map_filter_def)
lemma fmdrop_fmmap_keys[simp]: "fmdrop a (fmmap_keys f m) = fmmap_keys f (fmdrop a m)"
-unfolding fmfilter_alt_defs by simp
+ unfolding fmfilter_alt_defs by simp
lemma fmdrop_set_fmmap_keys[simp]: "fmdrop_set A (fmmap_keys f m) = fmmap_keys f (fmdrop_set A m)"
-unfolding fmfilter_alt_defs by simp
+ unfolding fmfilter_alt_defs by simp
lemma fmdrop_fset_fmmap_keys[simp]: "fmdrop_fset A (fmmap_keys f m) = fmmap_keys f (fmdrop_fset A m)"
-unfolding fmfilter_alt_defs by simp
+ unfolding fmfilter_alt_defs by simp
lemma fmrestrict_set_fmmap_keys[simp]: "fmrestrict_set A (fmmap_keys f m) = fmmap_keys f (fmrestrict_set A m)"
-unfolding fmfilter_alt_defs by simp
+ unfolding fmfilter_alt_defs by simp
lemma fmrestrict_fset_fmmap_keys[simp]: "fmrestrict_fset A (fmmap_keys f m) = fmmap_keys f (fmrestrict_fset A m)"
-unfolding fmfilter_alt_defs by simp
+ unfolding fmfilter_alt_defs by simp
lemma fmmap_keys_subset[intro]: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmmap_keys f m \<subseteq>\<^sub>f fmmap_keys f n"
-by transfer' (auto simp: map_le_def dom_def)
+ by transfer' (auto simp: map_le_def dom_def)
definition sorted_list_of_fmap :: "('a::linorder, 'b) fmap \<Rightarrow> ('a \<times> 'b) list" where
-"sorted_list_of_fmap m = map (\<lambda>k. (k, the (fmlookup m k))) (sorted_list_of_fset (fmdom m))"
+ "sorted_list_of_fmap m = map (\<lambda>k. (k, the (fmlookup m k))) (sorted_list_of_fset (fmdom m))"
lemma list_all_sorted_list[simp]: "list_all P (sorted_list_of_fmap m) = fmpred (curry P) m"
unfolding sorted_list_of_fmap_def curry_def list.pred_map
-apply (auto simp: list_all_iff)
-including fset.lifting
-by (transfer; auto simp: dom_def map_pred_def split: option.splits)+
+ by (smt (verit, best) Ball_set comp_def fmpred_alt_def sorted_list_of_fset_simps(1))
lemma map_of_sorted_list[simp]: "map_of (sorted_list_of_fmap m) = fmlookup m"
-unfolding sorted_list_of_fmap_def
-including fset.lifting
-by transfer (simp add: map_of_map_keys)
+ unfolding sorted_list_of_fmap_def
+ including fset.lifting
+ by transfer (simp add: map_of_map_keys)
subsection \<open>Additional properties\<close>
@@ -1138,7 +1121,7 @@
shows "\<exists>m. fmdom' m = S \<and> fmpred Q m"
proof -
obtain f where f: "Q x (f x)" if "x \<in> S" for x
- using assms by (metis bchoice)
+ using assms by metis
define f' where "f' x = (if x \<in> S then Some (f x) else None)" for x
have "eq_onp (\<lambda>m. finite (dom m)) f' f'"
@@ -1157,15 +1140,15 @@
context includes lifting_syntax begin
lemma fmempty_transfer[simp, intro, transfer_rule]: "fmrel P fmempty fmempty"
-by transfer auto
+ by transfer auto
lemma fmadd_transfer[transfer_rule]:
"(fmrel P ===> fmrel P ===> fmrel P) fmadd fmadd"
-by (intro fmrel_addI rel_funI)
+ by (intro fmrel_addI rel_funI)
lemma fmupd_transfer[transfer_rule]:
"((=) ===> P ===> fmrel P ===> fmrel P) fmupd fmupd"
-by auto
+ by auto
end
@@ -1176,21 +1159,18 @@
fix m n
assume "fmrel T m n"
then have "fmlookup (fmmap Abs m) x = fmlookup n x" for x
- apply (cases rule: fmrel_cases[where x = x])
- using assms unfolding Quotient_alt_def by auto
+ using assms unfolding Quotient_alt_def
+ by (cases rule: fmrel_cases[where x = x]) auto
then show "fmmap Abs m = n"
by (rule fmap_ext)
next
fix m
show "fmrel T (fmmap Rep m) m"
unfolding fmap.rel_map
- apply (rule fmap.rel_refl)
- using assms unfolding Quotient_alt_def
- by auto
+ by (metis (mono_tags) Quotient_alt_def assms fmap.rel_refl)
next
from assms have "R = T OO T\<inverse>\<inverse>"
unfolding Quotient_alt_def4 by simp
-
then show "fmrel R = fmrel T OO (fmrel T)\<inverse>\<inverse>"
by (simp add: fmap.rel_compp fmap.rel_conversep)
qed
@@ -1201,7 +1181,7 @@
lemma fmap_distinct[simp]:
"fmempty \<noteq> fmupd k v m"
"fmupd k v m \<noteq> fmempty"
-by (transfer'; auto simp: map_upd_def fun_eq_iff)+
+ by (transfer'; auto simp: map_upd_def fun_eq_iff)+
lifting_update fmap.lifting
@@ -1259,20 +1239,13 @@
by auto
with insert have "P (fmdrop x m)"
by auto
-
- have "x |\<in>| fmdom m"
- using insert by auto
- then obtain y where "fmlookup m x = Some y"
- by auto
+ moreover
+ obtain y where "fmlookup m x = Some y"
+ using insert.hyps by force
hence "m = fmupd x y (fmdrop x m)"
by (auto intro: fmap_ext)
-
- show ?case
- apply (subst \<open>m = _\<close>)
- apply (rule assms)
- apply fact
- apply simp
- done
+ ultimately show ?case
+ by (metis assms(2) fmdrop_lookup)
qed
@@ -1339,32 +1312,27 @@
by transfer (simp add: merge_conv')
lemma fmmap_of_list[code]: "fmmap f (fmap_of_list m) = fmap_of_list (map (apsnd f) m)"
-apply transfer
-apply (subst map_of_map[symmetric])
-apply (auto simp: apsnd_def map_prod_def)
-done
+ apply transfer
+ by (metis (no_types, lifting) apsnd_conv map_eq_conv map_of_map old.prod.case old.prod.exhaust)
lemma fmmap_keys_of_list[code]:
"fmmap_keys f (fmap_of_list m) = fmap_of_list (map (\<lambda>(a, b). (a, f a b)) m)"
-apply transfer
-subgoal for f m by (induction m) (auto simp: apsnd_def map_prod_def fun_eq_iff)
-done
+ apply transfer
+ subgoal for f m by (induction m) (auto simp: apsnd_def map_prod_def fun_eq_iff)
+ done
lemma fmimage_of_list[code]:
"fmimage (fmap_of_list m) A = fset_of_list (map snd (filter (\<lambda>(k, _). k |\<in>| A) (AList.clearjunk m)))"
-apply (subst fmimage_alt_def)
-apply (subst fmfilter_alt_defs)
-apply (subst fmfilter_of_list)
-apply (subst fmran_of_list)
-apply transfer'
-apply (subst AList.restrict_eq[symmetric])
-apply (subst clearjunk_restrict)
-apply (subst AList.restrict_eq)
-by auto
+ apply (subst fmimage_alt_def)
+ apply (subst fmfilter_alt_defs)
+ apply (subst fmfilter_of_list)
+ apply (subst fmran_of_list)
+ apply transfer'
+ by (metis AList.restrict_eq clearjunk_restrict list.set_map)
lemma fmcomp_list[code]:
"fmap_of_list m \<circ>\<^sub>f fmap_of_list n = fmap_of_list (AList.compose n m)"
-by (rule fmap_ext) (simp add: fmlookup_of_list compose_conv map_comp_def split: option.splits)
+ by (rule fmap_ext) (simp add: fmlookup_of_list compose_conv map_comp_def split: option.splits)
end
--- a/src/HOL/Library/Lattice_Algebras.thy Sun Aug 25 21:27:25 2024 +0100
+++ b/src/HOL/Library/Lattice_Algebras.thy Mon Aug 26 21:59:35 2024 +0100
@@ -9,34 +9,25 @@
class semilattice_inf_ab_group_add = ordered_ab_group_add + semilattice_inf
begin
-lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + c)"
- apply (rule order.antisym)
- apply (simp_all add: le_infI)
- apply (rule add_le_imp_le_left [of "uminus a"])
- apply (simp only: add.assoc [symmetric], simp add: diff_le_eq add.commute)
- done
+lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + c)" (is "?L=?R")
+proof (intro order.antisym)
+ show "?R \<le> ?L"
+ by (metis add_commute diff_le_eq inf_greatest inf_le1 inf_le2)
+qed simp
lemma add_inf_distrib_right: "inf a b + c = inf (a + c) (b + c)"
-proof -
- have "c + inf a b = inf (c + a) (c + b)"
- by (simp add: add_inf_distrib_left)
- then show ?thesis
- by (simp add: add.commute)
-qed
+ using add_commute add_inf_distrib_left by presburger
end
class semilattice_sup_ab_group_add = ordered_ab_group_add + semilattice_sup
begin
-lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a + c)"
- apply (rule order.antisym)
- apply (rule add_le_imp_le_left [of "uminus a"])
- apply (simp only: add.assoc [symmetric], simp)
- apply (simp add: le_diff_eq add.commute)
- apply (rule le_supI)
- apply (rule add_le_imp_le_left [of "a"], simp only: add.assoc[symmetric], simp)+
- done
+lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a + c)" (is "?L = ?R")
+proof (rule order.antisym)
+ show "?L \<le> ?R"
+ by (metis add_commute le_diff_eq sup.bounded_iff sup_ge1 sup_ge2)
+qed simp
lemma add_sup_distrib_right: "sup a b + c = sup (a + c) (b + c)"
proof -
@@ -193,22 +184,13 @@
qed
lemma inf_0_imp_0: "inf a (- a) = 0 \<Longrightarrow> a = 0"
- apply (simp add: inf_eq_neg_sup)
- apply (simp add: sup_commute)
- apply (erule sup_0_imp_0)
- done
+ by (metis local.neg_0_equal_iff_equal neg_inf_eq_sup sup_0_imp_0)
-lemma inf_0_eq_0 [simp, no_atp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
- apply (rule iffI)
- apply (erule inf_0_imp_0)
- apply simp
- done
+lemma inf_0_eq_0 [simp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
+ by (metis inf_0_imp_0 inf.idem minus_zero)
-lemma sup_0_eq_0 [simp, no_atp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
- apply (rule iffI)
- apply (erule sup_0_imp_0)
- apply simp
- done
+lemma sup_0_eq_0 [simp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
+ by (metis minus_zero sup.idem sup_0_imp_0)
lemma zero_le_double_add_iff_zero_le_single_add [simp]: "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
(is "?lhs \<longleftrightarrow> ?rhs")
@@ -361,11 +343,7 @@
have e: "- a - b = - (a + b)"
by simp
from a d e have "\<bar>a + b\<bar> \<le> sup ?m ?n"
- apply -
- apply (drule abs_leI)
- apply (simp_all only: algebra_simps minus_add)
- apply (metis add_uminus_conv_diff d sup_commute uminus_add_conv_diff)
- done
+ by (metis abs_leI)
with g[symmetric] show ?thesis by simp
qed
qed
@@ -418,31 +396,21 @@
have bh: "u = a \<Longrightarrow> v = b \<Longrightarrow>
u * v = pprt a * pprt b + pprt a * nprt b +
nprt a * pprt b + nprt a * nprt b" for u v :: 'a
- apply (subst prts[of u], subst prts[of v])
- apply (simp add: algebra_simps)
- done
+ by (metis add.commute combine_common_factor distrib_left prts)
note b = this[OF refl[of a] refl[of b]]
have xy: "- ?x \<le> ?y"
apply simp
- apply (metis (full_types) add_increasing add_uminus_conv_diff
- lattice_ab_group_add_class.minus_le_self_iff minus_add_distrib mult_nonneg_nonneg
- mult_nonpos_nonpos nprt_le_zero zero_le_pprt)
- done
+ by (meson add_increasing2 diff_le_eq neg_le_0_iff_le nprt_le_zero order.trans split_mult_pos_le zero_le_pprt)
have yx: "?y \<le> ?x"
apply simp
- apply (metis (full_types) add_nonpos_nonpos add_uminus_conv_diff
- lattice_ab_group_add_class.le_minus_self_iff minus_add_distrib mult_nonneg_nonpos
- mult_nonpos_nonneg nprt_le_zero zero_le_pprt)
- done
- have i1: "a * b \<le> \<bar>a\<bar> * \<bar>b\<bar>"
- by (simp only: a b yx)
- have i2: "- (\<bar>a\<bar> * \<bar>b\<bar>) \<le> a * b"
- by (simp only: a b xy)
+ by (metis add_decreasing2 diff_0 diff_mono diff_zero mult_nonpos_nonneg mult_right_mono_neg mult_zero_left nprt_le_zero zero_le_pprt)
show ?thesis
- apply (rule abs_leI)
- apply (simp add: i1)
- apply (simp add: i2[simplified minus_le_iff])
- done
+ proof (rule abs_leI)
+ show "a * b \<le> \<bar>a\<bar> * \<bar>b\<bar>"
+ by (simp only: a b yx)
+ show "- (a * b) \<le> \<bar>a\<bar> * \<bar>b\<bar>"
+ by (metis a bh minus_le_iff xy)
+ qed
qed
instance lattice_ring \<subseteq> ordered_ring_abs
@@ -452,40 +420,20 @@
show "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
proof -
have s: "(0 \<le> a * b) \<or> (a * b \<le> 0)"
- apply auto
- apply (rule_tac split_mult_pos_le)
- apply (rule_tac contrapos_np[of "a * b \<le> 0"])
- apply simp
- apply (rule_tac split_mult_neg_le)
- using a
- apply blast
- done
+ by (metis a split_mult_neg_le split_mult_pos_le)
have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
by (simp flip: prts)
show ?thesis
proof (cases "0 \<le> a * b")
case True
then show ?thesis
- apply (simp_all add: mulprts abs_prts)
- using a
- apply (auto simp add:
- algebra_simps
- iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
- iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
- apply(drule (1) mult_nonneg_nonpos[of a b], simp)
- apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
- done
+ using a split_mult_neg_le by fastforce
next
case False
with s have "a * b \<le> 0"
by simp
then show ?thesis
- apply (simp_all add: mulprts abs_prts)
- apply (insert a)
- apply (auto simp add: algebra_simps)
- apply(drule (1) mult_nonneg_nonneg[of a b],simp)
- apply(drule (1) mult_nonpos_nonpos[of a b],simp)
- done
+ using a split_mult_pos_le by fastforce
qed
qed
qed
--- a/src/HOL/Library/Word.thy Sun Aug 25 21:27:25 2024 +0100
+++ b/src/HOL/Library/Word.thy Mon Aug 26 21:59:35 2024 +0100
@@ -14,8 +14,7 @@
lemma signed_take_bit_decr_length_iff:
\<open>signed_take_bit (LENGTH('a::len) - Suc 0) k = signed_take_bit (LENGTH('a) - Suc 0) l
\<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
- by (cases \<open>LENGTH('a)\<close>)
- (simp_all add: signed_take_bit_eq_iff_take_bit_eq)
+ by (simp add: signed_take_bit_eq_iff_take_bit_eq)
subsection \<open>Fundamentals\<close>
@@ -42,19 +41,19 @@
lift_definition plus_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
is \<open>(+)\<close>
- by (auto simp add: take_bit_eq_mod intro: mod_add_cong)
+ by (auto simp: take_bit_eq_mod intro: mod_add_cong)
lift_definition minus_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
is \<open>(-)\<close>
- by (auto simp add: take_bit_eq_mod intro: mod_diff_cong)
+ by (auto simp: take_bit_eq_mod intro: mod_diff_cong)
lift_definition uminus_word :: \<open>'a word \<Rightarrow> 'a word\<close>
is uminus
- by (auto simp add: take_bit_eq_mod intro: mod_minus_cong)
+ by (auto simp: take_bit_eq_mod intro: mod_minus_cong)
lift_definition times_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
is \<open>(*)\<close>
- by (auto simp add: take_bit_eq_mod intro: mod_mult_cong)
+ by (auto simp: take_bit_eq_mod intro: mod_mult_cong)
instance
by (standard; transfer) (simp_all add: algebra_simps)
@@ -187,7 +186,7 @@
lemma [code]:
\<open>Word.the_int (- w) = (let k = Word.the_int w in if w = 0 then 0 else 2 ^ LENGTH('a) - k)\<close>
for w :: \<open>'a::len word\<close>
- by transfer (auto simp add: take_bit_eq_mod zmod_zminus1_eq_if)
+ by transfer (auto simp: take_bit_eq_mod zmod_zminus1_eq_if)
lemma [code]:
\<open>Word.the_int (v - w) = take_bit LENGTH('a) (Word.the_int v - Word.the_int w)\<close>
@@ -650,10 +649,10 @@
have "k mod r = ((k mod r) div (l mod r) * (l mod r)
+ (k mod r) mod (l mod r)) mod r"
by (simp add: div_mult_mod_eq)
- also have "... = (((k mod r) div (l mod r) * (l mod r)) mod r
+ also have "\<dots> = (((k mod r) div (l mod r) * (l mod r)) mod r
+ (k mod r) mod (l mod r)) mod r"
by (simp add: mod_add_left_eq)
- also have "... = (((k mod r) div (l mod r) * l) mod r
+ also have "\<dots> = (((k mod r) div (l mod r) * l) mod r
+ (k mod r) mod (l mod r)) mod r"
by (simp add: mod_mult_right_eq)
finally have "k mod r = ((k mod r) div (l mod r) * l
@@ -695,7 +694,7 @@
instance word :: (len) semiring_parity
by (standard; transfer)
- (auto simp add: mod_2_eq_odd take_bit_Suc elim: evenE dest: le_Suc_ex)
+ (auto simp: mod_2_eq_odd take_bit_Suc elim: evenE dest: le_Suc_ex)
lemma word_bit_induct [case_names zero even odd]:
\<open>P a\<close> if word_zero: \<open>P 0\<close>
@@ -723,7 +722,7 @@
with even.IH have \<open>P (of_nat n)\<close>
by simp
moreover from \<open>n < 2 ^ m\<close> even.hyps have \<open>0 < (of_nat n :: 'a word)\<close>
- by (auto simp add: word_greater_zero_iff l word_of_nat_eq_0_iff)
+ by (auto simp: word_greater_zero_iff l word_of_nat_eq_0_iff)
moreover from \<open>n < 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - Suc 0)\<close>
using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>]
by (simp add: l take_bit_eq_mod)
@@ -774,7 +773,7 @@
by simp
moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\<close>
with \<open>LENGTH('a) = Suc n\<close> have \<open>take_bit LENGTH('a) k = take_bit n k\<close>
- by (auto simp add: take_bit_Suc_from_most)
+ by (auto simp: take_bit_Suc_from_most)
ultimately have \<open>take_bit LENGTH('a) (k * 2) = take_bit LENGTH('a) k * 2\<close>
by (simp add: take_bit_eq_mod)
with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (k * 2) div take_bit LENGTH('a) 2)
@@ -792,12 +791,12 @@
using pos_zmod_mult_2 [of \<open>2 ^ n\<close> k] by (simp add: ac_simps)
moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\<close>
with \<open>LENGTH('a) = Suc n\<close> have \<open>take_bit LENGTH('a) k = take_bit n k\<close>
- by (auto simp add: take_bit_Suc_from_most)
+ by (auto simp: take_bit_Suc_from_most)
ultimately have \<open>take_bit LENGTH('a) (1 + k * 2) = 1 + take_bit LENGTH('a) k * 2\<close>
by (simp add: take_bit_eq_mod)
with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (1 + k * 2) div take_bit LENGTH('a) 2)
= take_bit LENGTH('a) k\<close>
- by (auto simp add: take_bit_Suc)
+ by (auto simp: take_bit_Suc)
qed
ultimately show ?thesis
by simp
@@ -871,7 +870,7 @@
for a :: \<open>'a word\<close> and m n :: nat
apply transfer
using drop_bit_eq_div [symmetric, where ?'a = int,of _ 1]
- apply (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: drop_bit_eq_div simp del: power.simps)
+ apply (auto simp: not_less take_bit_drop_bit ac_simps simp flip: drop_bit_eq_div simp del: power.simps)
apply (simp add: drop_bit_take_bit)
done
show \<open>even (2 * a div 2 ^ Suc n) \<longleftrightarrow> even (a div 2 ^ n)\<close> if \<open>2 ^ Suc n \<noteq> (0::'a word)\<close>
@@ -885,7 +884,7 @@
lemma bit_word_eqI:
\<open>a = b\<close> if \<open>\<And>n. n < LENGTH('a) \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close>
for a b :: \<open>'a::len word\<close>
- using that by transfer (auto simp add: nat_less_le bit_eq_iff bit_take_bit_iff)
+ using that by transfer (auto simp: nat_less_le bit_eq_iff bit_take_bit_iff)
lemma bit_imp_le_length:
\<open>n < LENGTH('a)\<close> if \<open>bit w n\<close>
@@ -988,20 +987,16 @@
by transfer (simp add: not_eq_complement)
show \<open>v AND w = of_bool (odd v \<and> odd w) + 2 * (v div 2 AND w div 2)\<close>
apply transfer
- apply (rule bit_eqI)
- apply (auto simp add: even_bit_succ_iff bit_simps bit_0 simp flip: bit_Suc)
- done
+ by (rule bit_eqI) (auto simp: even_bit_succ_iff bit_simps bit_0 simp flip: bit_Suc)
show \<open>v OR w = of_bool (odd v \<or> odd w) + 2 * (v div 2 OR w div 2)\<close>
apply transfer
- apply (rule bit_eqI)
- apply (auto simp add: even_bit_succ_iff bit_simps bit_0 simp flip: bit_Suc)
- done
+ by (rule bit_eqI) (auto simp: even_bit_succ_iff bit_simps bit_0 simp flip: bit_Suc)
show \<open>v XOR w = of_bool (odd v \<noteq> odd w) + 2 * (v div 2 XOR w div 2)\<close>
apply transfer
apply (rule bit_eqI)
subgoal for k l n
apply (cases n)
- apply (auto simp add: even_bit_succ_iff bit_simps bit_0 even_xor_iff simp flip: bit_Suc)
+ apply (auto simp: even_bit_succ_iff bit_simps bit_0 even_xor_iff simp flip: bit_Suc)
done
done
show \<open>mask n = 2 ^ n - (1 :: 'a word)\<close>
@@ -1173,14 +1168,14 @@
lemma unsigned_drop_bit_eq:
\<open>unsigned (drop_bit n w) = drop_bit n (take_bit LENGTH('b) (unsigned w))\<close>
for w :: \<open>'b::len word\<close>
- by (rule bit_eqI) (auto simp add: bit_unsigned_iff bit_take_bit_iff bit_drop_bit_eq Bit_Operations.bit_drop_bit_eq possible_bit_def dest: bit_imp_le_length)
+ by (rule bit_eqI) (auto simp: bit_unsigned_iff bit_take_bit_iff bit_drop_bit_eq Bit_Operations.bit_drop_bit_eq possible_bit_def dest: bit_imp_le_length)
end
lemma ucast_drop_bit_eq:
\<open>ucast (drop_bit n w) = drop_bit n (ucast w :: 'b::len word)\<close>
if \<open>LENGTH('a) \<le> LENGTH('b)\<close> for w :: \<open>'a::len word\<close>
- by (rule bit_word_eqI) (use that in \<open>auto simp add: bit_unsigned_iff bit_drop_bit_eq dest: bit_imp_le_length\<close>)
+ by (rule bit_word_eqI) (use that in \<open>auto simp: bit_unsigned_iff bit_drop_bit_eq dest: bit_imp_le_length\<close>)
context semiring_bit_operations
begin
@@ -1260,7 +1255,7 @@
\<open>bit (signed w) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> bit w (min (LENGTH('b) - Suc 0) n)\<close>
for w :: \<open>'b::len word\<close>
by (transfer fixing: bit)
- (auto simp add: bit_of_int_iff Bit_Operations.bit_signed_take_bit_iff min_def)
+ (auto simp: bit_of_int_iff Bit_Operations.bit_signed_take_bit_iff min_def)
lemma signed_push_bit_eq:
\<open>signed (push_bit n w) = signed_take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w :: 'a))\<close>
@@ -1273,7 +1268,7 @@
\<open>signed (take_bit n w) = (if n < LENGTH('b) then take_bit n (signed w) else signed w)\<close>
for w :: \<open>'b::len word\<close>
by (transfer fixing: take_bit; cases \<open>LENGTH('b)\<close>)
- (auto simp add: Bit_Operations.signed_take_bit_take_bit Bit_Operations.take_bit_signed_take_bit take_bit_of_int min_def less_Suc_eq)
+ (auto simp: Bit_Operations.signed_take_bit_take_bit Bit_Operations.take_bit_signed_take_bit take_bit_of_int min_def less_Suc_eq)
context
includes bit_operations_syntax
@@ -1318,7 +1313,7 @@
by simp
case False
then show ?thesis
- by transfer (auto simp add: signed_take_bit_eq intro: order_trans *)
+ by transfer (auto simp: signed_take_bit_eq intro: order_trans *)
qed
lemma sint_less:
@@ -1446,10 +1441,10 @@
by simp
lemma uint_0_iff: "uint x = 0 \<longleftrightarrow> x = 0"
- by (auto simp add: unsigned_word_eqI)
+ by (auto simp: unsigned_word_eqI)
lemma unat_0_iff: "unat x = 0 \<longleftrightarrow> x = 0"
- by (auto simp add: unsigned_word_eqI)
+ by (auto simp: unsigned_word_eqI)
lemma unat_0: "unat 0 = 0"
by (fact unsigned_0)
@@ -1547,9 +1542,7 @@
lemma mod_word_self [simp]:
\<open>w mod w = 0\<close> for w :: \<open>'a::len word\<close>
- apply (cases \<open>w = 0\<close>)
- apply auto
- using div_mult_mod_eq [of w w] by (simp add: div_word_self)
+ by (simp add: word_mod_def)
lemma div_word_less:
\<open>w div v = 0\<close> if \<open>w < v\<close> for w v :: \<open>'a::len word\<close>
@@ -1628,10 +1621,10 @@
by transfer simp
lift_definition word_succ :: "'a::len word \<Rightarrow> 'a word" is "\<lambda>x. x + 1"
- by (auto simp add: take_bit_eq_mod intro: mod_add_cong)
+ by (auto simp: take_bit_eq_mod intro: mod_add_cong)
lift_definition word_pred :: "'a::len word \<Rightarrow> 'a word" is "\<lambda>x. x - 1"
- by (auto simp add: take_bit_eq_mod intro: mod_diff_cong)
+ by (auto simp: take_bit_eq_mod intro: mod_diff_cong)
lemma word_succ_alt [code]:
"word_succ a = word_of_int (uint a + 1)"
@@ -1670,7 +1663,7 @@
by simp
have \<open>a = 0\<close> if \<open>2 * a = 0\<close> and \<open>a \<noteq> 2 ^ (LENGTH('a) - Suc 0)\<close>
using that by transfer
- (auto simp add: take_bit_eq_0_iff take_bit_eq_mod *)
+ (auto simp: take_bit_eq_0_iff take_bit_eq_mod *)
moreover have \<open>2 ^ LENGTH('a) = (0 :: 'a word)\<close>
by transfer simp
then have \<open>2 * 2 ^ (LENGTH('a) - Suc 0) = (0 :: 'a word)\<close>
@@ -1712,7 +1705,7 @@
using signed_take_bit_decr_length_iff by force+
lemma signed_linorder: \<open>class.linorder word_sle word_sless\<close>
- by (standard; transfer) (auto simp add: signed_take_bit_decr_length_iff)
+ by (standard; transfer) (auto simp: signed_take_bit_decr_length_iff)
interpretation signed: linorder word_sle word_sless
by (fact signed_linorder)
@@ -1751,7 +1744,7 @@
by transfer (simp add: nat_le_eq_zle)
lemma word_less_nat_alt: "a < b \<longleftrightarrow> unat a < unat b"
- by transfer (auto simp add: less_le [of 0])
+ by transfer (auto simp: less_le [of 0])
lemmas unat_mono = word_less_nat_alt [THEN iffD1]
@@ -1761,7 +1754,7 @@
assume *: "(\<And>b. (\<And>a. a < b \<Longrightarrow> P a) \<Longrightarrow> P b)"
have "wf (measure unat)" ..
moreover have "{(a, b :: ('a::len) word). a < b} \<subseteq> measure unat"
- by (auto simp add: word_less_nat_alt)
+ by (auto simp: word_less_nat_alt)
ultimately have "wf {(a, b :: ('a::len) word). a < b}"
by (rule wf_subset)
then show "P a" using *
@@ -1809,7 +1802,7 @@
lemma bit_sint_iff:
\<open>bit (sint w) n \<longleftrightarrow> n \<ge> LENGTH('a) \<and> bit w (LENGTH('a) - 1) \<or> bit w n\<close>
for w :: \<open>'a::len word\<close>
- by transfer (auto simp add: bit_signed_take_bit_iff min_def le_less not_less)
+ by transfer (auto simp: bit_signed_take_bit_iff min_def le_less not_less)
lemma bit_word_ucast_iff:
\<open>bit (ucast w :: 'b::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> n < LENGTH('b) \<and> bit w n\<close>
@@ -1820,7 +1813,7 @@
\<open>bit (scast w :: 'b::len word) n \<longleftrightarrow>
n < LENGTH('b) \<and> (bit w n \<or> LENGTH('a) \<le> n \<and> bit w (LENGTH('a) - Suc 0))\<close>
for w :: \<open>'a::len word\<close>
- by transfer (auto simp add: bit_signed_take_bit_iff le_less min_def)
+ by transfer (auto simp: bit_signed_take_bit_iff le_less min_def)
lemma bit_word_iff_drop_bit_and [code]:
\<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close> for a :: \<open>'a::len word\<close>
@@ -1856,7 +1849,7 @@
moreover have \<open>bit (r div 2) = bit r \<circ> Suc\<close> for r :: int
by (simp add: fun_eq_iff bit_Suc)
moreover from Suc.prems have \<open>even k \<longleftrightarrow> even l\<close>
- by (auto simp add: take_bit_Suc elim!: evenE oddE) arith+
+ by (auto simp: take_bit_Suc elim!: evenE oddE) arith+
ultimately show ?case
by (simp only: map_Suc_upt upt_conv_Cons flip: list.map_comp) (simp add: bit_0)
qed
@@ -1886,10 +1879,10 @@
numeral_inc numeral_eq_Suc flip: mult_2)
have even: \<open>take_bit (Suc q) (2 * w) = 2 * take_bit q w\<close> for w :: \<open>'a::len word\<close>
by (rule bit_word_eqI)
- (auto simp add: bit_take_bit_iff bit_double_iff)
+ (auto simp: bit_take_bit_iff bit_double_iff)
have odd: \<open>take_bit (Suc q) (1 + 2 * w) = 1 + 2 * take_bit q w\<close> for w :: \<open>'a::len word\<close>
by (rule bit_eqI)
- (auto simp add: bit_take_bit_iff bit_double_iff even_bit_succ_iff)
+ (auto simp: bit_take_bit_iff bit_double_iff even_bit_succ_iff)
show ?P
using even [of w] by (simp add: num)
show ?Q
@@ -1912,8 +1905,8 @@
\<open>bit (signed_drop_bit m w) n \<longleftrightarrow> bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n)\<close>
for w :: \<open>'a::len word\<close>
apply transfer
- apply (auto simp add: bit_drop_bit_eq bit_signed_take_bit_iff not_le min_def)
- apply (metis add.commute le_antisym less_diff_conv less_eq_decr_length_iff)
+ apply (auto simp: bit_drop_bit_eq bit_signed_take_bit_iff not_le min_def)
+ apply (metis Suc_pred add.commute le_less_Suc_eq len_gt_0 less_diff_conv)
apply (metis le_antisym less_eq_decr_length_iff)
done
@@ -1940,7 +1933,7 @@
next
case (Suc n)
then show ?thesis
- by (force simp add: bit_signed_drop_bit_iff not_le less_diff_conv ac_simps intro!: bit_word_eqI)
+ by (force simp: bit_signed_drop_bit_iff not_le less_diff_conv ac_simps intro!: bit_word_eqI)
qed
lemma signed_drop_bit_0 [simp]:
@@ -1954,7 +1947,7 @@
then show ?thesis
apply simp
apply (rule bit_eqI)
- by (auto simp add: bit_sint_iff bit_drop_bit_eq bit_signed_drop_bit_iff dest: bit_imp_le_length)
+ by (auto simp: bit_sint_iff bit_drop_bit_eq bit_signed_drop_bit_iff dest: bit_imp_le_length)
qed auto
@@ -1963,18 +1956,18 @@
lemma set_bit_eq_idem_iff:
\<open>Bit_Operations.set_bit n w = w \<longleftrightarrow> bit w n \<or> n \<ge> LENGTH('a)\<close>
for w :: \<open>'a::len word\<close>
- by (simp add: bit_eq_iff) (auto simp add: bit_simps not_le)
+ by (simp add: bit_eq_iff) (auto simp: bit_simps not_le)
lemma unset_bit_eq_idem_iff:
\<open>unset_bit n w = w \<longleftrightarrow> bit w n \<longrightarrow> n \<ge> LENGTH('a)\<close>
for w :: \<open>'a::len word\<close>
- by (simp add: bit_eq_iff) (auto simp add: bit_simps dest: bit_imp_le_length)
+ by (simp add: bit_eq_iff) (auto simp: bit_simps dest: bit_imp_le_length)
lemma flip_bit_eq_idem_iff:
\<open>flip_bit n w = w \<longleftrightarrow> n \<ge> LENGTH('a)\<close>
for w :: \<open>'a::len word\<close>
using linorder_le_less_linear
- by (simp add: bit_eq_iff) (auto simp add: bit_simps)
+ by (simp add: bit_eq_iff) (auto simp: bit_simps)
subsection \<open>Rotation\<close>
@@ -2054,7 +2047,7 @@
n < LENGTH('a) \<and> bit k ((n + q) mod LENGTH('a))\<close>
using \<open>q < LENGTH('a)\<close>
by (cases \<open>q + n \<ge> LENGTH('a)\<close>)
- (auto simp add: bit_concat_bit_iff bit_drop_bit_eq
+ (auto simp: bit_concat_bit_iff bit_drop_bit_eq
bit_take_bit_iff le_mod_geq ac_simps)
ultimately show \<open>n < LENGTH('a) \<and>
bit (concat_bit (LENGTH('a) - m mod LENGTH('a))
@@ -2092,7 +2085,7 @@
n < LENGTH('a) \<and> bit l ((n + m) mod LENGTH('a))\<close>
using \<open>m < LENGTH('a)\<close>
by (cases \<open>m + n \<ge> LENGTH('a)\<close>)
- (auto simp add: bit_concat_bit_iff bit_drop_bit_eq
+ (auto simp: bit_concat_bit_iff bit_drop_bit_eq
bit_take_bit_iff nat_less_iff not_le not_less ac_simps
le_diff_conv le_mod_geq)
ultimately show \<open>n < LENGTH('a)
@@ -2280,12 +2273,12 @@
lemma word_int_split:
"P (word_int_case f x) =
(\<forall>i. x = (word_of_int i :: 'b::len word) \<and> 0 \<le> i \<and> i < 2 ^ LENGTH('b) \<longrightarrow> P (f i))"
- by transfer (auto simp add: take_bit_eq_mod)
+ by transfer (auto simp: take_bit_eq_mod)
lemma word_int_split_asm:
"P (word_int_case f x) =
(\<nexists>n. x = (word_of_int n :: 'b::len word) \<and> 0 \<le> n \<and> n < 2 ^ LENGTH('b::len) \<and> \<not> P (f n))"
- by transfer (auto simp add: take_bit_eq_mod)
+ by transfer (auto simp: take_bit_eq_mod)
lemma uint_range_size: "0 \<le> uint w \<and> uint w < 2 ^ size w"
by transfer simp
@@ -2368,7 +2361,7 @@
lemma ucast_mask_eq:
\<open>ucast (mask n :: 'b word) = mask (min LENGTH('b::len) n)\<close>
- by (simp add: bit_eq_iff) (auto simp add: bit_mask_iff bit_ucast_iff)
+ by (simp add: bit_eq_iff) (auto simp: bit_mask_iff bit_ucast_iff)
\<comment> \<open>literal u(s)cast\<close>
lemma ucast_bintr [simp]:
@@ -2613,8 +2606,8 @@
\<open>signed_drop_bit n (1 :: 'a::len word) = of_bool (LENGTH('a) = 1 \<or> n = 0)\<close>
apply (transfer fixing: n)
apply (cases \<open>LENGTH('a)\<close>)
- apply (auto simp add: take_bit_signed_take_bit)
- apply (auto simp add: take_bit_drop_bit gr0_conv_Suc simp flip: take_bit_eq_self_iff_drop_bit_eq_0)
+ apply (auto simp: take_bit_signed_take_bit)
+ apply (auto simp: take_bit_drop_bit gr0_conv_Suc simp flip: take_bit_eq_self_iff_drop_bit_eq_0)
done
lemma take_bit_word_beyond_length_eq:
@@ -2816,7 +2809,7 @@
by linarith
qed
ultimately have \<open>unat w = unat v * unat (word_of_nat n :: 'a word)\<close>
- by (auto simp add: take_bit_nat_eq_self_iff unsigned_of_nat intro: sym)
+ by (auto simp: take_bit_nat_eq_self_iff unsigned_of_nat intro: sym)
with that show thesis .
qed
@@ -2863,7 +2856,7 @@
lemma udvd_nat_alt:
\<open>a udvd b \<longleftrightarrow> (\<exists>n. unat b = n * unat a)\<close>
- by (auto simp add: udvd_iff_dvd)
+ by (auto simp: udvd_iff_dvd)
lemma udvd_unfold_int:
\<open>a udvd b \<longleftrightarrow> (\<exists>n\<ge>0. uint b = n * uint a)\<close>
@@ -2921,8 +2914,7 @@
unfolding uint_word_ariths by (simp add: zmod_le_nonneg_dividend)
lemma uint_sub_ge: "uint (x - y) \<ge> uint x - uint y"
- unfolding uint_word_ariths
- by (simp flip: take_bit_eq_mod add: take_bit_int_greater_eq_self_iff)
+ by (smt (verit, ccfv_SIG) uint_nonnegative uint_sub_lem)
lemma int_mod_ge: \<open>a \<le> a mod n\<close> if \<open>a < n\<close> \<open>0 < n\<close>
for a n :: int
@@ -2932,8 +2924,7 @@
"\<lbrakk>x < z; y < z; 0 \<le> y; 0 \<le> x; 0 \<le> z\<rbrakk> \<Longrightarrow>
(x + y) mod z = (if x + y < z then x + y else x + y - z)"
for x y z :: int
- apply (simp add: not_less)
- by (metis (no_types) add_strict_mono diff_ge_0_iff_ge diff_less_eq minus_mod_self2 mod_pos_pos_trivial)
+ by (smt (verit, best) minus_mod_self2 mod_pos_pos_trivial)
lemma uint_plus_if':
"uint (a + b) =
@@ -2946,7 +2937,7 @@
"\<lbrakk>x < z; y < z; 0 \<le> y; 0 \<le> x; 0 \<le> z\<rbrakk> \<Longrightarrow>
(x - y) mod z = (if y \<le> x then x - y else x - y + z)"
for x y z :: int
- using mod_pos_pos_trivial [of "x - y + z" z] by (auto simp add: not_le)
+ using mod_pos_pos_trivial [of "x - y + z" z] by (auto simp: not_le)
lemma uint_sub_if':
"uint (a - b) =
@@ -2962,11 +2953,11 @@
lemma unat_split: "P (unat x) \<longleftrightarrow> (\<forall>n. of_nat n = x \<and> n < 2^LENGTH('a) \<longrightarrow> P n)"
for x :: "'a::len word"
- by (auto simp add: unsigned_of_nat take_bit_nat_eq_self)
+ by (auto simp: unsigned_of_nat take_bit_nat_eq_self)
lemma unat_split_asm: "P (unat x) \<longleftrightarrow> (\<nexists>n. of_nat n = x \<and> n < 2^LENGTH('a) \<and> \<not> P n)"
for x :: "'a::len word"
- by (auto simp add: unsigned_of_nat take_bit_nat_eq_self)
+ using unat_split by auto
lemma un_ui_le:
\<open>unat a \<le> unat b \<longleftrightarrow> uint a \<le> uint b\<close>
@@ -2977,10 +2968,9 @@
(if unat a + unat b < 2 ^ LENGTH('a)
then unat a + unat b
else unat a + unat b - 2 ^ LENGTH('a))\<close> for a b :: \<open>'a::len word\<close>
- apply (auto simp add: not_less le_iff_add)
+ apply (auto simp: not_less le_iff_add)
apply (metis (mono_tags, lifting) of_nat_add of_nat_unat take_bit_nat_eq_self_iff unsigned_less unsigned_of_nat unsigned_word_eqI)
- apply (smt (verit, ccfv_SIG) dbl_simps(3) dbl_simps(5) numerals(1) of_nat_0_le_iff of_nat_add of_nat_eq_iff of_nat_numeral of_nat_power of_nat_unat uint_plus_if' unsigned_1)
- done
+ by (smt (verit, ccfv_SIG) numeral_Bit0 numerals(1) of_nat_0_le_iff of_nat_1 of_nat_add of_nat_eq_iff of_nat_power of_nat_unat uint_plus_if')
lemma unat_sub_if_size:
"unat (x - y) =
@@ -2991,9 +2981,9 @@
{ assume xy: "\<not> uint y \<le> uint x"
have "nat (uint x - uint y + 2 ^ LENGTH('a)) = nat (uint x + 2 ^ LENGTH('a) - uint y)"
by simp
- also have "... = nat (uint x + 2 ^ LENGTH('a)) - nat (uint y)"
+ also have "\<dots> = nat (uint x + 2 ^ LENGTH('a)) - nat (uint y)"
by (simp add: nat_diff_distrib')
- also have "... = nat (uint x) + 2 ^ LENGTH('a) - nat (uint y)"
+ also have "\<dots> = nat (uint x) + 2 ^ LENGTH('a) - nat (uint y)"
by (metis nat_add_distrib nat_eq_numeral_power_cancel_iff order_less_imp_le unsigned_0 unsigned_greater_eq unsigned_less)
finally have "nat (uint x - uint y + 2 ^ LENGTH('a)) = nat (uint x) + 2 ^ LENGTH('a) - nat (uint y)" .
}
@@ -3006,12 +2996,12 @@
lemma uint_split:
"P (uint x) = (\<forall>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^LENGTH('a) \<longrightarrow> P i)"
for x :: "'a::len word"
- by transfer (auto simp add: take_bit_eq_mod)
+ by transfer (auto simp: take_bit_eq_mod)
lemma uint_split_asm:
"P (uint x) = (\<nexists>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^LENGTH('a) \<and> \<not> P i)"
for x :: "'a::len word"
- by (auto simp add: unsigned_of_int take_bit_int_eq_self)
+ by (auto simp: unsigned_of_int take_bit_int_eq_self)
subsection \<open>Some proof tool support\<close>
@@ -3111,13 +3101,13 @@
lemma no_plus_overflow_uint_size: "x \<le> x + y \<longleftrightarrow> uint x + uint y < 2 ^ size x"
for x y :: "'a::len word"
- by (auto simp add: word_size word_le_def uint_add_lem uint_sub_lem)
+ by (auto simp: word_size word_le_def uint_add_lem uint_sub_lem)
lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size]
lemma no_ulen_sub: "x \<ge> x - y \<longleftrightarrow> uint y \<le> uint x"
for x y :: "'a::len word"
- by (auto simp add: word_size word_le_def uint_add_lem uint_sub_lem)
+ by (auto simp: word_size word_le_def uint_add_lem uint_sub_lem)
lemma no_olen_add': "x \<le> y + x \<longleftrightarrow> uint y + uint x < 2 ^ LENGTH('a)"
for x y :: "'a::len word"
@@ -3328,7 +3318,7 @@
by (cases k) auto
lemma of_nat_neq_0: "0 < k \<Longrightarrow> k < 2 ^ LENGTH('a::len) \<Longrightarrow> of_nat k \<noteq> (0 :: 'a word)"
- by (auto simp add : of_nat_0)
+ by (auto simp : of_nat_0)
lemma Abs_fnat_hom_add: "of_nat a + of_nat b = of_nat (a + b)"
by simp
@@ -3496,12 +3486,12 @@
lemma range_uint: \<open>range (uint :: 'a word \<Rightarrow> int) = {0..<2 ^ LENGTH('a::len)}\<close>
apply transfer
- apply (auto simp add: image_iff)
+ apply (auto simp: image_iff)
apply (metis take_bit_int_eq_self_iff)
done
lemma UNIV_eq: \<open>(UNIV :: 'a word set) = word_of_int ` {0..<2 ^ LENGTH('a::len)}\<close>
- by (auto simp add: image_iff) (metis atLeastLessThan_iff linorder_not_le uint_split)
+ by (auto simp: image_iff) (metis atLeastLessThan_iff linorder_not_le uint_split)
lemma card_word: "CARD('a word) = 2 ^ LENGTH('a::len)"
by (simp add: UNIV_eq card_image inj_on_word_of_int)
@@ -3720,7 +3710,7 @@
lemma word_rev_rev [simp] : "word_reverse (word_reverse w) = w"
by (rule bit_word_eqI)
- (auto simp add: bit_word_reverse_iff bit_imp_le_length Suc_diff_Suc)
+ (auto simp: bit_word_reverse_iff bit_imp_le_length Suc_diff_Suc)
lemma word_rev_gal: "word_reverse w = u \<Longrightarrow> word_reverse u = w"
by (metis word_rev_rev)
@@ -3889,7 +3879,7 @@
lemma and_mask_wi':
"word_of_int i AND mask n = (word_of_int (take_bit (min LENGTH('a) n) i) :: 'a::len word)"
- by (auto simp add: and_mask_wi min_def wi_bintr)
+ by (auto simp: and_mask_wi min_def wi_bintr)
lemma and_mask_no: "numeral i AND mask n = word_of_int (take_bit n (numeral i))"
unfolding word_numeral_alt by (rule and_mask_wi)
@@ -3975,7 +3965,7 @@
\<open>bit (slice1 m w :: 'b::len word) n \<longleftrightarrow> m - LENGTH('a) \<le> n \<and> n < min LENGTH('b) m
\<and> bit w (n + (LENGTH('a) - m) - (m - LENGTH('a)))\<close>
for w :: \<open>'a::len word\<close>
- by (auto simp add: slice1_def bit_ucast_iff bit_drop_bit_eq bit_push_bit_iff not_less not_le ac_simps
+ by (auto simp: slice1_def bit_ucast_iff bit_drop_bit_eq bit_push_bit_iff not_less not_le ac_simps
dest: bit_imp_le_length)
definition slice :: \<open>nat \<Rightarrow> 'a::len word \<Rightarrow> 'b::len word\<close>
@@ -4072,7 +4062,7 @@
lemma word_cat_split_alt: "\<lbrakk>size w \<le> size u + size v; word_split w = (u,v)\<rbrakk> \<Longrightarrow> word_cat u v = w"
unfolding word_split_def
- by (rule bit_word_eqI) (auto simp add: bit_word_cat_iff not_less word_size bit_ucast_iff bit_drop_bit_eq)
+ by (rule bit_word_eqI) (auto simp: bit_word_cat_iff not_less word_size bit_ucast_iff bit_drop_bit_eq)
lemmas word_cat_split_size = sym [THEN [2] word_cat_split_alt [symmetric]]
@@ -4091,7 +4081,7 @@
show "bit u n = bit ((slice LENGTH('b) w)::'a word) n" if "n < LENGTH('a)" for n
using assms bit_imp_le_length
unfolding word_split_def bit_slice_iff
- by (fastforce simp add: \<section> ac_simps word_size bit_ucast_iff bit_drop_bit_eq)
+ by (fastforce simp: \<section> ac_simps word_size bit_ucast_iff bit_drop_bit_eq)
qed
show "v = slice 0 w"
by (metis Pair_inject assms ucast_slice word_split_bin')
@@ -4100,13 +4090,13 @@
lemma slice_cat1 [OF refl]:
"\<lbrakk>wc = word_cat a b; size a + size b \<le> size wc\<rbrakk> \<Longrightarrow> slice (size b) wc = a"
- by (rule bit_word_eqI) (auto simp add: bit_slice_iff bit_word_cat_iff word_size)
+ by (rule bit_word_eqI) (auto simp: bit_slice_iff bit_word_cat_iff word_size)
lemmas slice_cat2 = trans [OF slice_id word_cat_id]
lemma cat_slices:
"\<lbrakk>a = slice n c; b = slice 0 c; n = size b; size c \<le> size a + size b\<rbrakk> \<Longrightarrow> word_cat a b = c"
- by (rule bit_word_eqI) (auto simp add: bit_slice_iff bit_word_cat_iff word_size)
+ by (rule bit_word_eqI) (auto simp: bit_slice_iff bit_word_cat_iff word_size)
lemma word_split_cat_alt:
assumes "w = word_cat u v" and size: "size u + size v \<le> size w"
@@ -4114,7 +4104,7 @@
proof -
have "ucast ((drop_bit LENGTH('c) (word_cat u v))::'a word) = u" "ucast ((word_cat u v)::'a word) = v"
using assms
- by (auto simp add: word_size bit_ucast_iff bit_drop_bit_eq bit_word_cat_iff intro: bit_eqI)
+ by (auto simp: word_size bit_ucast_iff bit_drop_bit_eq bit_word_cat_iff intro: bit_eqI)
then show ?thesis
by (simp add: assms(1) word_split_bin')
qed
@@ -4160,7 +4150,7 @@
proof (rule bit_word_eqI)
show "bit (word_rotr k (word_rotl k v)) n = bit v n" if "n < LENGTH('a)" for n
using that
- by (auto simp add: word_rot_lem word_rotl_eq_word_rotr word_rotr_word_rotr_eq bit_word_rotr_iff algebra_simps split: nat_diff_split)
+ by (auto simp: word_rot_lem word_rotl_eq_word_rotr word_rotr_word_rotr_eq bit_word_rotr_iff algebra_simps split: nat_diff_split)
qed
lemma word_rot_gal:
@@ -4184,8 +4174,7 @@
apply (simp add: mod_simps)
done
then have \<open>LENGTH('a) - Suc ((m + n) mod LENGTH('a)) =
- (LENGTH('a) + LENGTH('a) - Suc (m + n mod LENGTH('a))) mod
- LENGTH('a)\<close>
+ (LENGTH('a) + LENGTH('a) - Suc (m + n mod LENGTH('a))) mod LENGTH('a)\<close>
by simp
with \<open>m < LENGTH('a)\<close> show \<open>bit ?lhs m \<longleftrightarrow> bit ?rhs m\<close>
by (simp add: bit_simps)
@@ -4238,7 +4227,7 @@
"word_rotr n (x OR y) = word_rotr n x OR word_rotr n y"
"word_rotl n (x XOR y) = word_rotl n x XOR word_rotl n y"
"word_rotr n (x XOR y) = word_rotr n x XOR word_rotr n y"
- by (rule bit_word_eqI, auto simp add: bit_word_rotl_iff bit_word_rotr_iff bit_and_iff bit_or_iff bit_xor_iff bit_not_iff algebra_simps not_le)+
+ by (rule bit_word_eqI, auto simp: bit_word_rotl_iff bit_word_rotr_iff bit_and_iff bit_or_iff bit_xor_iff bit_not_iff algebra_simps not_le)+
end
@@ -4368,7 +4357,7 @@
lemma word_le_less_eq: "x \<le> y \<longleftrightarrow> x = y \<or> x < y"
for x y :: "'z::len word"
- by (auto simp add: order_class.le_less)
+ by (auto simp: order_class.le_less)
lemma mod_plus_cong:
fixes b b' :: int
@@ -4491,7 +4480,7 @@
by (induct n) auto
lemma word_rec_id_eq: "(\<And>m. m < n \<Longrightarrow> f m = id) \<Longrightarrow> word_rec z f n = z"
- by (induction n) (auto simp add: unatSuc unat_arith_simps(2))
+ by (induction n) (auto simp: unatSuc unat_arith_simps(2))
lemma word_rec_max:
assumes "\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id"
@@ -4502,7 +4491,7 @@
by (metis (mono_tags, lifting) add.commute add_diff_cancel_left' comp_apply less_le olen_add_eqv plus_minus_no_overflow word_n1_ge)
have "word_rec z f (- 1) = word_rec (word_rec z f (- 1 - (- 1 - n))) (f \<circ> (+) (- 1 - (- 1 - n))) (- 1 - n)"
by (meson word_n1_ge word_rec_twice)
- also have "... = word_rec z f n"
+ also have "\<dots> = word_rec z f n"
by (metis (no_types, lifting) \<section> diff_add_cancel minus_diff_eq uminus_add_conv_diff word_rec_id_eq)
finally show ?thesis .
qed
--- a/src/HOL/ex/LocaleTest2.thy Sun Aug 25 21:27:25 2024 +0100
+++ b/src/HOL/ex/LocaleTest2.thy Mon Aug 26 21:59:35 2024 +0100
@@ -11,7 +11,7 @@
section \<open>Test of Locale Interpretation\<close>
theory LocaleTest2
-imports Main
+imports Main
begin
section \<open>Interpretation of Defined Concepts\<close>
@@ -482,33 +482,31 @@
thm int.circular
lemma "\<lbrakk> (x::int) \<le> y; y \<le> z; z \<le> x\<rbrakk> \<Longrightarrow> x = y \<and> y = z"
- apply (rule int.circular) apply assumption apply assumption apply assumption done
+ by simp
+
thm int.abs_test
lemma "((<) :: [int, int] => bool) = (<)"
- apply (rule int.abs_test) done
+ by (rule int.abs_test)
interpretation int: dlat "(<=) :: [int, int] => bool"
rewrites meet_eq: "dlat.meet (<=) (x::int) y = min x y"
and join_eq: "dlat.join (<=) (x::int) y = max x y"
proof -
show "dlat ((<=) :: [int, int] => bool)"
- apply unfold_locales
- apply (unfold int.is_inf_def int.is_sup_def)
- apply arith+
- done
+ proof unfold_locales
+ fix x y :: int
+ show "\<exists>inf. int.is_inf x y inf"
+ using int.is_inf_def by fastforce
+ show "\<exists>sup. int.is_sup x y sup"
+ using int.is_sup_def by fastforce
+ qed
then interpret int: dlat "(<=) :: [int, int] => bool" .
txt \<open>Interpretation to ease use of definitions, which are
conditional in general but unconditional after interpretation.\<close>
show "dlat.meet (<=) (x::int) y = min x y"
- apply (unfold int.meet_def)
- apply (rule the_equality)
- apply (unfold int.is_inf_def)
- by auto
+ by (smt (verit, best) int.meet_related int.meet_related2)
show "dlat.join (<=) (x::int) y = max x y"
- apply (unfold int.join_def)
- apply (rule the_equality)
- apply (unfold int.is_sup_def)
- by auto
+ by (smt (verit, best) int.join_related int.join_related2)
qed
interpretation int: dlo "(<=) :: [int, int] => bool"
@@ -533,9 +531,7 @@
then interpret nat: dpo "(<=) :: [nat, nat] => bool" .
txt \<open>Gives interpreted version of \<open>less_def\<close> (without condition).\<close>
show "dpo.less (<=) (x::nat) y = (x < y)"
- apply (unfold nat.less_def)
- apply auto
- done
+ by (simp add: nat.less_def nat_less_le)
qed
interpretation nat: dlat "(<=) :: [nat, nat] => bool"
@@ -543,23 +539,20 @@
and "dlat.join (<=) (x::nat) y = max x y"
proof -
show "dlat ((<=) :: [nat, nat] => bool)"
- apply unfold_locales
- apply (unfold nat.is_inf_def nat.is_sup_def)
- apply arith+
- done
+ proof
+ fix x y :: nat
+ show "\<exists>inf. nat.is_inf x y inf"
+ by (metis nat.is_inf_def nle_le)
+ show "\<exists>sup. nat.is_sup x y sup"
+ by (metis nat.is_sup_def nle_le)
+ qed
then interpret nat: dlat "(<=) :: [nat, nat] => bool" .
txt \<open>Interpretation to ease use of definitions, which are
conditional in general but unconditional after interpretation.\<close>
show "dlat.meet (<=) (x::nat) y = min x y"
- apply (unfold nat.meet_def)
- apply (rule the_equality)
- apply (unfold nat.is_inf_def)
- by auto
+ by (metis min_def nat.meet_connection nat.meet_connection2 nle_le)
show "dlat.join (<=) (x::nat) y = max x y"
- apply (unfold nat.join_def)
- apply (rule the_equality)
- apply (unfold nat.is_sup_def)
- by auto
+ by (metis max_def nat.join_connection2 nat.join_related2 nle_le)
qed
interpretation nat: dlo "(<=) :: [nat, nat] => bool"
@@ -584,9 +577,8 @@
then interpret nat_dvd: dpo "(dvd) :: [nat, nat] => bool" .
txt \<open>Gives interpreted version of \<open>less_def\<close> (without condition).\<close>
show "dpo.less (dvd) (x::nat) y = (x dvd y & x ~= y)"
- apply (unfold nat_dvd.less_def)
- apply auto
- done
+ unfolding nat_dvd.less_def
+ by auto
qed
interpretation nat_dvd: dlat "(dvd) :: [nat, nat] => bool"
@@ -594,36 +586,33 @@
and "dlat.join (dvd) (x::nat) y = lcm x y"
proof -
show "dlat ((dvd) :: [nat, nat] => bool)"
- apply unfold_locales
- apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def)
- apply (rule_tac x = "gcd x y" in exI)
- apply auto [1]
- apply (rule_tac x = "lcm x y" in exI)
- apply (auto intro: dvd_lcm1 dvd_lcm2 lcm_least)
- done
+ proof
+ fix x y :: nat
+ show "\<exists>inf. nat_dvd.is_inf x y inf"
+ unfolding nat_dvd.is_inf_def
+ by (force simp: intro: exI [where x = "gcd x y"])
+ show "\<exists>sup. nat_dvd.is_sup x y sup"
+ unfolding nat_dvd.is_sup_def
+ by (force simp: intro: exI [where x = "lcm x y"])
+ qed
then interpret nat_dvd: dlat "(dvd) :: [nat, nat] => bool" .
txt \<open>Interpretation to ease use of definitions, which are
conditional in general but unconditional after interpretation.\<close>
show "dlat.meet (dvd) (x::nat) y = gcd x y"
- apply (unfold nat_dvd.meet_def)
- apply (rule the_equality)
- apply (unfold nat_dvd.is_inf_def)
- by auto
+ by (meson gcd_unique_nat nat_dvd.meetI)
show "dlat.join (dvd) (x::nat) y = lcm x y"
- apply (unfold nat_dvd.join_def)
- apply (rule the_equality)
- apply (unfold nat_dvd.is_sup_def)
- by (auto intro: dvd_lcm1 dvd_lcm2 lcm_least)
+ by (simp add: nat_dvd.joinI)
qed
text \<open>Interpreted theorems from the locales, involving defined terms.\<close>
thm nat_dvd.less_def text \<open>from dpo\<close>
-lemma "((x::nat) dvd y & x ~= y) = (x dvd y & x ~= y)"
- apply (rule nat_dvd.less_def) done
+lemma "((x::nat) dvd y \<and> x \<noteq> y) = (x dvd y \<and> x \<noteq> y)"
+ by simp
+
thm nat_dvd.meet_left text \<open>from dlat\<close>
lemma "gcd x y dvd (x::nat)"
- apply (rule nat_dvd.meet_left) done
+ by blast
subsection \<open>Group example with defined operations \<open>inv\<close> and \<open>unit\<close>\<close>
@@ -670,19 +659,11 @@
lemma unit_l_inv:
"unit x ==> inv x ** x = one"
- apply (simp add: unit_def inv_def) apply (erule exE)
- apply (rule theI2, fast)
- apply (rule inv_unique)
- apply fast+
- done
+ by (smt (verit, ccfv_threshold) inv_unique local.inv_def theI' unit_def)
lemma unit_r_inv:
"unit x ==> x ** inv x = one"
- apply (simp add: unit_def inv_def) apply (erule exE)
- apply (rule theI2, fast)
- apply (rule inv_unique)
- apply fast+
- done
+ by (metis inv_unique unit_l_inv unit_r_inv_ex)
lemma unit_inv_unit [intro, simp]:
"unit x ==> unit (inv x)"
@@ -801,15 +782,10 @@
lemma inv_comm:
"x ** y = one ==> y ** x = one"
- by (rule unit_inv_comm) auto
+ using unit unit_inv_comm by blast
-lemma inv_equality:
- "y ** x = one ==> inv x = y"
- apply (simp add: inv_def)
- apply (rule the_equality)
- apply (simp add: inv_comm [of y x])
- apply (rule r_cancel [THEN iffD1], auto)
- done
+lemma inv_equality: "y ** x = one \<Longrightarrow> inv x = y"
+ by (metis assoc r_inv r_one)
end
@@ -843,45 +819,20 @@
(*
from this interpret Dmonoid "(o)" "id :: 'a => 'a" .
*)
+ have "\<And>y. \<lbrakk>f \<circ> y = id; y \<circ> f = id\<rbrakk> \<Longrightarrow> bij f"
+ using o_bij by auto
+ moreover have "bij f \<Longrightarrow> \<exists>y. f \<circ> y = id \<and> y \<circ> f = id"
+ by (meson bij_betw_def inv_o_cancel surj_iff)
+ ultimately
show "Dmonoid.unit (o) (id :: 'a => 'a) f = bij f"
- apply (unfold Dmonoid.unit_def [OF Dmonoid])
- apply rule apply clarify
- proof -
- fix f g
- assume id1: "f o g = id" and id2: "g o f = id"
- show "bij f"
- proof (rule bijI)
- show "inj f"
- proof (rule inj_onI)
- fix x y
- assume "f x = f y"
- then have "(g o f) x = (g o f) y" by simp
- with id2 show "x = y" by simp
- qed
- next
- show "surj f"
- proof (rule surjI)
- fix x
- from id1 have "(f o g) x = x" by simp
- then show "f (g x) = x" by simp
- qed
- qed
- next
- fix f
- assume bij: "bij f"
- then
- have inv: "f o Hilbert_Choice.inv f = id & Hilbert_Choice.inv f o f = id"
- by (simp add: bij_def surj_iff inj_iff)
- show "\<exists>g. f \<circ> g = id \<and> g \<circ> f = id" by rule (rule inv)
- qed
+ by (metis Dmonoid Dmonoid.unit_def)
qed
thm Dmonoid.unit_def Dfun.unit_def
thm Dmonoid.inv_inj_on_unit Dfun.inv_inj_on_unit
-lemma unit_id:
- "(f :: unit => unit) = id"
+lemma unit_id: "(f :: unit => unit) = id"
by rule simp
interpretation Dfun: Dgrp "(o)" "id :: unit => unit"
@@ -891,20 +842,14 @@
note Dmonoid = this
show "Dgrp (o) (id :: unit => unit)"
-apply unfold_locales
-apply (unfold Dmonoid.unit_def [OF Dmonoid])
-apply (insert unit_id)
-apply simp
-done
+ proof
+ fix x :: "unit \<Rightarrow> unit"
+ show "Dmonoid.unit (\<circ>) id x"
+ by (simp add: Dmonoid Dmonoid.unit_def unit_id)
+ qed
show "Dmonoid.inv (o) id f = inv (f :: unit \<Rightarrow> unit)"
-apply (unfold Dmonoid.inv_def [OF Dmonoid])
-apply (insert unit_id)
-apply simp
-apply (rule the_equality)
-apply rule
-apply rule
-apply simp
-done
+ unfolding Dmonoid.inv_def [OF Dmonoid]
+ by force
qed
thm Dfun.unit_l_inv Dfun.l_inv
--- a/src/ZF/ex/misc.thy Sun Aug 25 21:27:25 2024 +0100
+++ b/src/ZF/ex/misc.thy Mon Aug 26 21:59:35 2024 +0100
@@ -9,7 +9,6 @@
theory misc imports ZF begin
-
subsection\<open>Various Small Problems\<close>
text\<open>The singleton problems are much harder in HOL.\<close>