--- a/src/HOL/Fun.thy Sun Mar 29 22:30:26 2020 +0200
+++ b/src/HOL/Fun.thy Sun Mar 29 22:30:43 2020 +0200
@@ -738,7 +738,7 @@
by (simp add: fun_eq_iff)
lemma fun_upd_twist: "a \<noteq> c \<Longrightarrow> (m(a := b))(c := d) = (m(c := d))(a := b)"
- by (rule ext) auto
+ by auto
lemma inj_on_fun_updI: "inj_on f A \<Longrightarrow> y \<notin> f ` A \<Longrightarrow> inj_on (f(x := y)) A"
by (auto simp: inj_on_def)
--- a/src/HOL/Int.thy Sun Mar 29 22:30:26 2020 +0200
+++ b/src/HOL/Int.thy Sun Mar 29 22:30:43 2020 +0200
@@ -136,21 +136,23 @@
by (cases "k = 0") (simp_all add: distrib_right add_strict_mono)
qed
-lemma zero_le_imp_eq_int: "0 \<le> k \<Longrightarrow> \<exists>n. k = int n"
- for k :: int
- apply transfer
- apply clarsimp
- apply (rule_tac x="a - b" in exI)
- apply simp
- done
+lemma zero_le_imp_eq_int:
+ assumes "k \<ge> (0::int)" shows "\<exists>n. k = int n"
+proof -
+ have "b \<le> a \<Longrightarrow> \<exists>n::nat. a = n + b" for a b
+ by (rule_tac x="a - b" in exI) simp
+ with assms show ?thesis
+ by transfer auto
+qed
-lemma zero_less_imp_eq_int: "0 < k \<Longrightarrow> \<exists>n>0. k = int n"
- for k :: int
- apply transfer
- apply clarsimp
- apply (rule_tac x="a - b" in exI)
- apply simp
- done
+lemma zero_less_imp_eq_int:
+ assumes "k > (0::int)" shows "\<exists>n>0. k = int n"
+proof -
+ have "b < a \<Longrightarrow> \<exists>n::nat. n>0 \<and> a = n + b" for a b
+ by (rule_tac x="a - b" in exI) simp
+ with assms show ?thesis
+ by transfer auto
+qed
lemma zmult_zless_mono2: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
for i j k :: int
@@ -185,12 +187,12 @@
lemma zless_iff_Suc_zadd: "w < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))"
for w z :: int
- apply transfer
- apply auto
- apply (rename_tac a b c d)
- apply (rule_tac x="c+b - Suc(a+d)" in exI)
- apply arith
- done
+proof -
+ have "\<And>a b c d. a + d < c + b \<Longrightarrow> \<exists>n. c + b = Suc (a + n + d)"
+ by (rule_tac x="c+b - Suc(a+d)" in exI) arith
+ then show ?thesis
+ by transfer auto
+qed
lemma zabs_less_one_iff [simp]: "\<bar>z\<bar> < 1 \<longleftrightarrow> z = 0" (is "?lhs \<longleftrightarrow> ?rhs")
for z :: int
@@ -471,16 +473,16 @@
qed
instance int :: no_top
- apply standard
- apply (rule_tac x="x + 1" in exI)
- apply simp
- done
+proof
+ show "\<And>x::int. \<exists>y. x < y"
+ by (rule_tac x="x + 1" in exI) simp
+qed
instance int :: no_bot
- apply standard
- apply (rule_tac x="x - 1" in exI)
- apply simp
- done
+proof
+ show "\<And>x::int. \<exists>y. y < x"
+ by (rule_tac x="x - 1" in exI) simp
+qed
subsection \<open>Magnitude of an Integer, as a Natural Number: \<open>nat\<close>\<close>
@@ -732,12 +734,14 @@
for a :: "'a::linordered_idom"
by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
-lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
- apply transfer
- apply clarsimp
- apply (rule_tac x="b - Suc a" in exI)
- apply arith
- done
+lemma negD:
+ assumes "x < 0" shows "\<exists>n. x = - (int (Suc n))"
+proof -
+ have "\<And>a b. a < b \<Longrightarrow> \<exists>n. Suc (a + n) = b"
+ by (rule_tac x="b - Suc a" in exI) arith
+ with assms show ?thesis
+ by transfer auto
+qed
subsection \<open>Cases and induction\<close>
@@ -754,13 +758,17 @@
text \<open>This is the default, with a negative case.\<close>
lemma int_cases [case_names nonneg neg, cases type: int]:
- "(\<And>n. z = int n \<Longrightarrow> P) \<Longrightarrow> (\<And>n. z = - (int (Suc n)) \<Longrightarrow> P) \<Longrightarrow> P"
- apply (cases "z < 0")
- apply (blast dest!: negD)
- apply (simp add: linorder_not_less del: of_nat_Suc)
- apply auto
- apply (blast dest: nat_0_le [THEN sym])
- done
+ assumes pos: "\<And>n. z = int n \<Longrightarrow> P" and neg: "\<And>n. z = - (int (Suc n)) \<Longrightarrow> P"
+ shows P
+proof (cases "z < 0")
+ case True
+ with neg show ?thesis
+ by (blast dest!: negD)
+next
+ case False
+ with pos show ?thesis
+ by (force simp add: linorder_not_less dest: nat_0_le [THEN sym])
+qed
lemma int_cases3 [case_names zero pos neg]:
fixes k :: int
@@ -891,31 +899,19 @@
by (subst of_nat_numeral [symmetric], rule Ints_of_nat)
lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
- apply (auto simp add: Ints_def)
- apply (rule range_eqI)
- apply (rule of_int_add [symmetric])
- done
+ by (force simp add: Ints_def simp flip: of_int_add intro: range_eqI)
lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
- apply (auto simp add: Ints_def)
- apply (rule range_eqI)
- apply (rule of_int_minus [symmetric])
- done
+ by (force simp add: Ints_def simp flip: of_int_minus intro: range_eqI)
lemma minus_in_Ints_iff: "-x \<in> \<int> \<longleftrightarrow> x \<in> \<int>"
using Ints_minus[of x] Ints_minus[of "-x"] by auto
lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
- apply (auto simp add: Ints_def)
- apply (rule range_eqI)
- apply (rule of_int_diff [symmetric])
- done
+ by (force simp add: Ints_def simp flip: of_int_diff intro: range_eqI)
lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
- apply (auto simp add: Ints_def)
- apply (rule range_eqI)
- apply (rule of_int_mult [symmetric])
- done
+ by (force simp add: Ints_def simp flip: of_int_mult intro: range_eqI)
lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
by (induct n) simp_all
@@ -1234,12 +1230,15 @@
of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
qed
-lemma nat_mult_distrib_neg: "z \<le> 0 \<Longrightarrow> nat (z * z') = nat (- z) * nat (- z')"
- for z z' :: int
- apply (rule trans)
- apply (rule_tac [2] nat_mult_distrib)
- apply auto
- done
+lemma nat_mult_distrib_neg:
+ assumes "z \<le> (0::int)" shows "nat (z * z') = nat (- z) * nat (- z')" (is "?L = ?R")
+proof -
+ have "?L = nat (- z * - z')"
+ using assms by auto
+ also have "... = ?R"
+ by (rule nat_mult_distrib) (use assms in auto)
+ finally show ?thesis .
+qed
lemma nat_abs_mult_distrib: "nat \<bar>w * z\<bar> = nat \<bar>w\<bar> * nat \<bar>z\<bar>"
by (cases "z = 0 \<or> w = 0")
@@ -1332,16 +1331,14 @@
(* `set:int': dummy construction *)
theorem int_gr_induct [case_names base step, induct set: int]:
fixes i k :: int
- assumes gr: "k < i"
- and base: "P (k + 1)"
- and step: "\<And>i. k < i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
+ assumes "k < i" "P (k + 1)" "\<And>i. k < i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
shows "P i"
- apply (rule int_ge_induct[of "k + 1"])
- using gr apply arith
- apply (rule base)
- apply (rule step)
- apply simp_all
- done
+proof -
+ have "k+1 \<le> i"
+ using assms by auto
+ then show ?thesis
+ by (induction i rule: int_ge_induct) (auto simp: assms)
+qed
theorem int_le_induct [consumes 1, case_names base step]:
fixes i k :: int
@@ -1367,16 +1364,14 @@
theorem int_less_induct [consumes 1, case_names base step]:
fixes i k :: int
- assumes less: "i < k"
- and base: "P (k - 1)"
- and step: "\<And>i. i < k \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
+ assumes "i < k" "P (k - 1)" "\<And>i. i < k \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
shows "P i"
- apply (rule int_le_induct[of _ "k - 1"])
- using less apply arith
- apply (rule base)
- apply (rule step)
- apply simp_all
- done
+proof -
+ have "i \<le> k-1"
+ using assms by auto
+ then show ?thesis
+ by (induction i rule: int_le_induct) (auto simp: assms)
+qed
theorem int_induct [case_names base step1 step2]:
fixes k :: int
@@ -1401,26 +1396,30 @@
subsection \<open>Intermediate value theorems\<close>
+lemma nat_ivt_aux:
+ "\<lbrakk>\<forall>i<n. \<bar>f (Suc i) - f i\<bar> \<le> 1; f 0 \<le> k; k \<le> f n\<rbrakk> \<Longrightarrow> \<exists>i \<le> n. f i = k"
+ for m n :: nat and k :: int
+proof (induct n)
+ case (Suc n)
+ show ?case
+ proof (cases "k = f (Suc n)")
+ case False
+ with Suc have "k \<le> f n"
+ by auto
+ with Suc show ?thesis
+ by (auto simp add: abs_if split: if_split_asm intro: le_SucI)
+ qed (use Suc in auto)
+qed auto
+
lemma nat_intermed_int_val:
- "\<exists>i. m \<le> i \<and> i \<le> n \<and> f i = k"
- if "\<forall>i. m \<le> i \<and> i < n \<longrightarrow> \<bar>f (Suc i) - f i\<bar> \<le> 1"
- "m \<le> n" "f m \<le> k" "k \<le> f n"
- for m n :: nat and k :: int
+ fixes m n :: nat and k :: int
+ assumes "\<forall>i. m \<le> i \<and> i < n \<longrightarrow> \<bar>f (Suc i) - f i\<bar> \<le> 1" "m \<le> n" "f m \<le> k" "k \<le> f n"
+ shows "\<exists>i. m \<le> i \<and> i \<le> n \<and> f i = k"
proof -
- have "(\<forall>i<n. \<bar>f (Suc i) - f i\<bar> \<le> 1) \<Longrightarrow> f 0 \<le> k \<Longrightarrow> k \<le> f n
- \<Longrightarrow> (\<exists>i \<le> n. f i = k)"
- for n :: nat and f
- apply (induct n)
- apply auto
- apply (erule_tac x = n in allE)
- apply (case_tac "k = f (Suc n)")
- apply (auto simp add: abs_if split: if_split_asm intro: le_SucI)
- done
- from this [of "n - m" "f \<circ> plus m"] that show ?thesis
- apply auto
- apply (rule_tac x = "m + i" in exI)
- apply auto
- done
+ obtain i where "i \<le> n - m" "k = f (m + i)"
+ using nat_ivt_aux [of "n - m" "f \<circ> plus m" k] assms by auto
+ with assms show ?thesis
+ by (rule_tac x = "m + i" in exI) auto
qed
lemma nat0_intermed_int_val:
@@ -1465,14 +1464,12 @@
by (auto dest: pos_zmult_eq_1_iff_lemma)
qed
-lemma zmult_eq_1_iff: "m * n = 1 \<longleftrightarrow> (m = 1 \<and> n = 1) \<or> (m = - 1 \<and> n = - 1)"
+lemma zmult_eq_1_iff: "m * n = 1 \<longleftrightarrow> (m = 1 \<and> n = 1) \<or> (m = - 1 \<and> n = - 1)" (is "?L = ?R")
for m n :: int
- apply (rule iffI)
- apply (frule pos_zmult_eq_1_iff_lemma)
- apply (simp add: mult.commute [of m])
- apply (frule pos_zmult_eq_1_iff_lemma)
- apply auto
- done
+proof
+ assume L: ?L show ?R
+ using pos_zmult_eq_1_iff_lemma [OF L] L by force
+qed auto
lemma infinite_UNIV_int [simp]: "\<not> finite (UNIV::int set)"
proof
@@ -1677,13 +1674,12 @@
using nat_less_eq_zless[of a "numeral x ^ n"]
by (cases "a < 0") (auto simp: nat_power_eq less_le_trans[where y=0])
-lemma zdvd_imp_le: "z dvd n \<Longrightarrow> 0 < n \<Longrightarrow> z \<le> n"
- for n z :: int
- apply (cases n)
- apply auto
- apply (cases z)
- apply (auto simp add: dvd_imp_le)
- done
+lemma zdvd_imp_le: "z \<le> n" if "z dvd n" "0 < n" for n z :: int
+proof (cases n)
+ case (nonneg n)
+ show ?thesis
+ by (cases z) (use nonneg dvd_imp_le that in auto)
+qed (use that in auto)
lemma zdvd_period:
fixes a d :: int
--- a/src/HOL/Map.thy Sun Mar 29 22:30:26 2020 +0200
+++ b/src/HOL/Map.thy Sun Mar 29 22:30:43 2020 +0200
@@ -110,18 +110,19 @@
lemma map_upd_Some_unfold:
"((m(a\<mapsto>b)) x = Some y) = (x = a \<and> b = y \<or> x \<noteq> a \<and> m x = Some y)"
-by auto
+ by auto
lemma image_map_upd [simp]: "x \<notin> A \<Longrightarrow> m(x \<mapsto> y) ` A = m ` A"
-by auto
+ by auto
-lemma finite_range_updI: "finite (range f) \<Longrightarrow> finite (range (f(a\<mapsto>b)))"
-unfolding image_def
-apply (simp (no_asm_use) add:full_SetCompr_eq)
-apply (rule finite_subset)
- prefer 2 apply assumption
-apply (auto)
-done
+lemma finite_range_updI:
+ assumes "finite (range f)" shows "finite (range (f(a\<mapsto>b)))"
+proof -
+ have "range (f(a\<mapsto>b)) \<subseteq> insert (Some b) (range f)"
+ by auto
+ then show ?thesis
+ by (rule finite_subset) (use assms in auto)
+qed
subsection \<open>@{term [source] map_of}\<close>
@@ -143,21 +144,19 @@
lemma map_of_eq_Some_iff [simp]:
"distinct(map fst xys) \<Longrightarrow> (map_of xys x = Some y) = ((x,y) \<in> set xys)"
-apply (induct xys)
- apply simp
-apply (auto simp: map_of_eq_None_iff [symmetric])
-done
+proof (induct xys)
+ case (Cons xy xys)
+ then show ?case
+ by (cases xy) (auto simp flip: map_of_eq_None_iff)
+qed auto
lemma Some_eq_map_of_iff [simp]:
"distinct(map fst xys) \<Longrightarrow> (Some y = map_of xys x) = ((x,y) \<in> set xys)"
by (auto simp del: map_of_eq_Some_iff simp: map_of_eq_Some_iff [symmetric])
-lemma map_of_is_SomeI [simp]: "\<lbrakk> distinct(map fst xys); (x,y) \<in> set xys \<rbrakk>
- \<Longrightarrow> map_of xys x = Some y"
-apply (induct xys)
- apply simp
-apply force
-done
+lemma map_of_is_SomeI [simp]:
+ "\<lbrakk>distinct(map fst xys); (x,y) \<in> set xys\<rbrakk> \<Longrightarrow> map_of xys x = Some y"
+ by simp
lemma map_of_zip_is_None [simp]:
"length xs = length ys \<Longrightarrow> (map_of (zip xs ys) x = None) = (x \<notin> set xs)"
@@ -233,12 +232,11 @@
by (induct xs) (simp_all add: fun_eq_iff)
lemma finite_range_map_of: "finite (range (map_of xys))"
-apply (induct xys)
- apply (simp_all add: image_constant)
-apply (rule finite_subset)
- prefer 2 apply assumption
-apply auto
-done
+proof (induct xys)
+ case (Cons a xys)
+ then show ?case
+ using finite_range_updI by fastforce
+qed auto
lemma map_of_SomeD: "map_of xs k = Some y \<Longrightarrow> (k, y) \<in> set xs"
by (induct xs) (auto split: if_splits)
@@ -334,23 +332,24 @@
by (rule ext) (auto simp: map_add_def dom_def split: option.split)
lemma map_of_append[simp]: "map_of (xs @ ys) = map_of ys ++ map_of xs"
-unfolding map_add_def
-apply (induct xs)
- apply simp
-apply (rule ext)
-apply (simp split: option.split)
-done
+ unfolding map_add_def
+proof (induct xs)
+ case (Cons a xs)
+ then show ?case
+ by (force split: option.split)
+qed auto
lemma finite_range_map_of_map_add:
"finite (range f) \<Longrightarrow> finite (range (f ++ map_of l))"
-apply (induct l)
- apply (auto simp del: fun_upd_apply)
-apply (erule finite_range_updI)
-done
+proof (induct l)
+case (Cons a l)
+ then show ?case
+ by (metis finite_range_updI map_add_upd map_of.simps(2))
+qed auto
lemma inj_on_map_add_dom [iff]:
"inj_on (m ++ m') (dom m') = inj_on m' (dom m')"
-by (fastforce simp: map_add_def dom_def inj_on_def split: option.splits)
+ by (fastforce simp: map_add_def dom_def inj_on_def split: option.splits)
lemma map_upds_fold_map_upd:
"m(ks[\<mapsto>]vs) = foldl (\<lambda>m (k, v). m(k \<mapsto> v)) m (zip ks vs)"
@@ -369,46 +368,46 @@
subsection \<open>@{term [source] restrict_map}\<close>
lemma restrict_map_to_empty [simp]: "m|`{} = empty"
-by (simp add: restrict_map_def)
+ by (simp add: restrict_map_def)
lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
-by (auto simp: restrict_map_def)
+ by (auto simp: restrict_map_def)
lemma restrict_map_empty [simp]: "empty|`D = empty"
-by (simp add: restrict_map_def)
+ by (simp add: restrict_map_def)
lemma restrict_in [simp]: "x \<in> A \<Longrightarrow> (m|`A) x = m x"
-by (simp add: restrict_map_def)
+ by (simp add: restrict_map_def)
lemma restrict_out [simp]: "x \<notin> A \<Longrightarrow> (m|`A) x = None"
-by (simp add: restrict_map_def)
+ by (simp add: restrict_map_def)
lemma ran_restrictD: "y \<in> ran (m|`A) \<Longrightarrow> \<exists>x\<in>A. m x = Some y"
-by (auto simp: restrict_map_def ran_def split: if_split_asm)
+ by (auto simp: restrict_map_def ran_def split: if_split_asm)
lemma dom_restrict [simp]: "dom (m|`A) = dom m \<inter> A"
-by (auto simp: restrict_map_def dom_def split: if_split_asm)
+ by (auto simp: restrict_map_def dom_def split: if_split_asm)
lemma restrict_upd_same [simp]: "m(x\<mapsto>y)|`(-{x}) = m|`(-{x})"
-by (rule ext) (auto simp: restrict_map_def)
+ by (rule ext) (auto simp: restrict_map_def)
lemma restrict_restrict [simp]: "m|`A|`B = m|`(A\<inter>B)"
-by (rule ext) (auto simp: restrict_map_def)
+ by (rule ext) (auto simp: restrict_map_def)
lemma restrict_fun_upd [simp]:
"m(x := y)|`D = (if x \<in> D then (m|`(D-{x}))(x := y) else m|`D)"
-by (simp add: restrict_map_def fun_eq_iff)
+ by (simp add: restrict_map_def fun_eq_iff)
lemma fun_upd_None_restrict [simp]:
"(m|`D)(x := None) = (if x \<in> D then m|`(D - {x}) else m|`D)"
-by (simp add: restrict_map_def fun_eq_iff)
+ by (simp add: restrict_map_def fun_eq_iff)
lemma fun_upd_restrict: "(m|`D)(x := y) = (m|`(D-{x}))(x := y)"
-by (simp add: restrict_map_def fun_eq_iff)
+ by (simp add: restrict_map_def fun_eq_iff)
lemma fun_upd_restrict_conv [simp]:
"x \<in> D \<Longrightarrow> (m|`D)(x := y) = (m|`(D-{x}))(x := y)"
-by (simp add: restrict_map_def fun_eq_iff)
+ by (rule fun_upd_restrict)
lemma map_of_map_restrict:
"map_of (map (\<lambda>k. (k, f k)) ks) = (Some \<circ> f) |` set ks"
@@ -416,47 +415,62 @@
lemma restrict_complement_singleton_eq:
"f |` (- {x}) = f(x := None)"
- by (simp add: restrict_map_def fun_eq_iff)
+ by auto
subsection \<open>@{term [source] map_upds}\<close>
lemma map_upds_Nil1 [simp]: "m([] [\<mapsto>] bs) = m"
-by (simp add: map_upds_def)
+ by (simp add: map_upds_def)
lemma map_upds_Nil2 [simp]: "m(as [\<mapsto>] []) = m"
-by (simp add:map_upds_def)
+ by (simp add:map_upds_def)
lemma map_upds_Cons [simp]: "m(a#as [\<mapsto>] b#bs) = (m(a\<mapsto>b))(as[\<mapsto>]bs)"
-by (simp add:map_upds_def)
+ by (simp add:map_upds_def)
-lemma map_upds_append1 [simp]: "size xs < size ys \<Longrightarrow>
- m(xs@[x] [\<mapsto>] ys) = m(xs [\<mapsto>] ys)(x \<mapsto> ys!size xs)"
-apply(induct xs arbitrary: ys m)
- apply (clarsimp simp add: neq_Nil_conv)
-apply (case_tac ys)
- apply simp
-apply simp
-done
+lemma map_upds_append1 [simp]:
+ "size xs < size ys \<Longrightarrow> m(xs@[x] [\<mapsto>] ys) = m(xs [\<mapsto>] ys)(x \<mapsto> ys!size xs)"
+proof (induct xs arbitrary: ys m)
+ case Nil
+ then show ?case
+ by (auto simp: neq_Nil_conv)
+next
+ case (Cons a xs)
+ then show ?case
+ by (cases ys) auto
+qed
lemma map_upds_list_update2_drop [simp]:
"size xs \<le> i \<Longrightarrow> m(xs[\<mapsto>]ys[i:=y]) = m(xs[\<mapsto>]ys)"
-apply (induct xs arbitrary: m ys i)
- apply simp
-apply (case_tac ys)
- apply simp
-apply (simp split: nat.split)
-done
+proof (induct xs arbitrary: m ys i)
+ case Nil
+ then show ?case
+ by auto
+next
+ case (Cons a xs)
+ then show ?case
+ by (cases ys) (use Cons in \<open>auto split: nat.split\<close>)
+qed
+text \<open>Something weirdly sensitive about this proof, which needs only four lines in apply style\<close>
lemma map_upd_upds_conv_if:
"(f(x\<mapsto>y))(xs [\<mapsto>] ys) =
(if x \<in> set(take (length ys) xs) then f(xs [\<mapsto>] ys)
else (f(xs [\<mapsto>] ys))(x\<mapsto>y))"
-apply (induct xs arbitrary: x y ys f)
- apply simp
-apply (case_tac ys)
- apply (auto split: if_split simp: fun_upd_twist)
-done
+proof (induct xs arbitrary: x y ys f)
+ case (Cons a xs)
+ show ?case
+ proof (cases ys)
+ case (Cons z zs)
+ then show ?thesis
+ using Cons.hyps
+ apply (auto split: if_split simp: fun_upd_twist)
+ using Cons.hyps apply fastforce+
+ done
+ qed auto
+qed auto
+
lemma map_upds_twist [simp]:
"a \<notin> set as \<Longrightarrow> m(a\<mapsto>b)(as[\<mapsto>]bs) = m(as[\<mapsto>]bs)(a\<mapsto>b)"
@@ -464,39 +478,42 @@
lemma map_upds_apply_nontin [simp]:
"x \<notin> set xs \<Longrightarrow> (f(xs[\<mapsto>]ys)) x = f x"
-apply (induct xs arbitrary: ys)
- apply simp
-apply (case_tac ys)
- apply (auto simp: map_upd_upds_conv_if)
-done
+proof (induct xs arbitrary: ys)
+ case (Cons a xs)
+ then show ?case
+ by (cases ys) (auto simp: map_upd_upds_conv_if)
+qed auto
lemma fun_upds_append_drop [simp]:
"size xs = size ys \<Longrightarrow> m(xs@zs[\<mapsto>]ys) = m(xs[\<mapsto>]ys)"
-apply (induct xs arbitrary: m ys)
- apply simp
-apply (case_tac ys)
- apply simp_all
-done
+proof (induct xs arbitrary: ys)
+ case (Cons a xs)
+ then show ?case
+ by (cases ys) (auto simp: map_upd_upds_conv_if)
+qed auto
lemma fun_upds_append2_drop [simp]:
"size xs = size ys \<Longrightarrow> m(xs[\<mapsto>]ys@zs) = m(xs[\<mapsto>]ys)"
-apply (induct xs arbitrary: m ys)
- apply simp
-apply (case_tac ys)
- apply simp_all
-done
-
+proof (induct xs arbitrary: ys)
+ case (Cons a xs)
+ then show ?case
+ by (cases ys) (auto simp: map_upd_upds_conv_if)
+qed auto
lemma restrict_map_upds[simp]:
"\<lbrakk> length xs = length ys; set xs \<subseteq> D \<rbrakk>
\<Longrightarrow> m(xs [\<mapsto>] ys)|`D = (m|`(D - set xs))(xs [\<mapsto>] ys)"
-apply (induct xs arbitrary: m ys)
- apply simp
-apply (case_tac ys)
- apply simp
-apply (simp add: Diff_insert [symmetric] insert_absorb)
-apply (simp add: map_upd_upds_conv_if)
-done
+proof (induct xs arbitrary: m ys)
+ case (Cons a xs)
+ then show ?case
+ proof (cases ys)
+ case (Cons z zs)
+ with Cons.hyps Cons.prems show ?thesis
+ apply (simp add: insert_absorb flip: Diff_insert)
+ apply (auto simp add: map_upd_upds_conv_if)
+ done
+ qed auto
+qed auto
subsection \<open>@{term [source] dom}\<close>
@@ -537,11 +554,12 @@
lemma dom_map_upds [simp]:
"dom(m(xs[\<mapsto>]ys)) = set(take (length ys) xs) \<union> dom m"
-apply (induct xs arbitrary: m ys)
- apply simp
-apply (case_tac ys)
- apply auto
-done
+proof (induct xs arbitrary: ys)
+ case (Cons a xs)
+ then show ?case
+ by (cases ys) (auto simp: map_upd_upds_conv_if)
+qed auto
+
lemma dom_map_add [simp]: "dom (m ++ n) = dom n \<union> dom m"
by (auto simp: dom_def)
@@ -638,12 +656,9 @@
lemma ran_empty [simp]: "ran empty = {}"
by (auto simp: ran_def)
-lemma ran_map_upd [simp]: "m a = None \<Longrightarrow> ran(m(a\<mapsto>b)) = insert b (ran m)"
+lemma ran_map_upd [simp]: "m a = None \<Longrightarrow> ran(m(a\<mapsto>b)) = insert b (ran m)"
unfolding ran_def
-apply auto
-apply (subgoal_tac "aa \<noteq> a")
- apply auto
-done
+ by force
lemma ran_map_add:
assumes "dom m1 \<inter> dom m2 = {}"
@@ -712,11 +727,11 @@
lemma map_le_upds [simp]:
"f \<subseteq>\<^sub>m g \<Longrightarrow> f(as [\<mapsto>] bs) \<subseteq>\<^sub>m g(as [\<mapsto>] bs)"
-apply (induct as arbitrary: f g bs)
- apply simp
-apply (case_tac bs)
- apply auto
-done
+proof (induct as arbitrary: f g bs)
+ case (Cons a as)
+ then show ?case
+ by (cases bs) (use Cons in auto)
+qed auto
lemma map_le_implies_dom_le: "(f \<subseteq>\<^sub>m g) \<Longrightarrow> (dom f \<subseteq> dom g)"
by (fastforce simp add: map_le_def dom_def)
@@ -728,11 +743,8 @@
by (auto simp add: map_le_def dom_def)
lemma map_le_antisym: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m f \<rbrakk> \<Longrightarrow> f = g"
-unfolding map_le_def
-apply (rule ext)
-apply (case_tac "x \<in> dom f", simp)
-apply (case_tac "x \<in> dom g", simp, fastforce)
-done
+ unfolding map_le_def
+ by (metis ext domIff)
lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m g ++ f"
by (fastforce simp: map_le_def)