# HG changeset patch # User haftmann # Date 1591284622 0 # Node ID 4e0a58818edc72b7cb6444e182d8ba31ca1b0329 # Parent 4c5778d8a53df6e81dfe4198c0aba4101072c904 more simp rules diff -r 4c5778d8a53d -r 4e0a58818edc src/HOL/Data_Structures/Sorting.thy --- a/src/HOL/Data_Structures/Sorting.thy Wed Jun 03 11:44:21 2020 +0200 +++ b/src/HOL/Data_Structures/Sorting.thy Thu Jun 04 15:30:22 2020 +0000 @@ -205,7 +205,8 @@ lemma length_msort: "length(msort xs) = length xs" proof (induction xs rule: msort.induct) case (1 xs) - thus ?case by (auto simp: msort.simps[of xs] length_merge) + show ?case + by (auto simp: msort.simps [of xs] 1 length_merge) qed text \Why structured proof? To have the name "xs" to specialize msort.simps with xs diff -r 4c5778d8a53d -r 4e0a58818edc src/HOL/Data_Structures/Trie_Fun.thy --- a/src/HOL/Data_Structures/Trie_Fun.thy Wed Jun 03 11:44:21 2020 +0200 +++ b/src/HOL/Data_Structures/Trie_Fun.thy Thu Jun 04 15:30:22 2020 +0000 @@ -67,12 +67,11 @@ case 1 thus ?case by (force split: option.splits) next case 2 - thus ?case - apply (auto simp add: image_iff split!: if_splits option.splits) - apply blast - apply (metis insertE insertI2 insert_Diff_single option.inject) - apply blast - by (metis insertE insertI2 insert_Diff_single option.inject) + show ?case + apply (auto simp add: image_iff 2 split!: if_splits option.splits) + apply (metis DiffI empty_iff insert_iff option.inject) + apply (metis DiffI empty_iff insert_iff option.inject) + done qed interpretation S: Set diff -r 4c5778d8a53d -r 4e0a58818edc src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Jun 03 11:44:21 2020 +0200 +++ b/src/HOL/HOL.thy Thu Jun 04 15:30:22 2020 +0000 @@ -941,6 +941,36 @@ lemma eta_contract_eq: "(\s. f s) = f" .. +lemma subst_all: + \(\x. x = a \ PROP P x) \ PROP P a\ +proof (rule equal_intr_rule) + assume *: \\x. x = a \ PROP P x\ + show \PROP P a\ + by (rule *) (rule refl) +next + fix x + assume \PROP P a\ and \x = a\ + from \x = a\ have \x \ a\ + by (rule eq_reflection) + with \PROP P a\ show \PROP P x\ + by simp +qed + +lemma subst_all': + \(\x. a = x \ PROP P x) \ PROP P a\ +proof (rule equal_intr_rule) + assume *: \\x. a = x \ PROP P x\ + show \PROP P a\ + by (rule *) (rule refl) +next + fix x + assume \PROP P a\ and \a = x\ + from \a = x\ have \a \ x\ + by (rule eq_reflection) + with \PROP P a\ show \PROP P x\ + by simp +qed + lemma simp_thms: shows not_not: "(\ \ P) = P" and Not_eq_iff: "((\ P) = (\ Q)) = (P = Q)" @@ -1372,6 +1402,8 @@ ex_simps all_simps simp_thms + subst_all + subst_all' lemmas [cong] = imp_cong simp_implies_cong lemmas [split] = if_split diff -r 4c5778d8a53d -r 4e0a58818edc src/HOL/Proofs/Lambda/NormalForm.thy --- a/src/HOL/Proofs/Lambda/NormalForm.thy Wed Jun 03 11:44:21 2020 +0200 +++ b/src/HOL/Proofs/Lambda/NormalForm.thy Thu Jun 04 15:30:22 2020 +0000 @@ -91,8 +91,8 @@ lemma nat_le_dec: "\n::nat. m < n \ \ (m < n)" apply (induct m) apply (case_tac n) - apply (case_tac [3] n) - apply (simp del: simp_thms, iprover?)+ + apply (case_tac [3] n) + apply (simp del: simp_thms subst_all subst_all', iprover?)+ done lemma App_NF_D: assumes NF: "NF (Var n \\ ts)" diff -r 4c5778d8a53d -r 4e0a58818edc src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Wed Jun 03 11:44:21 2020 +0200 +++ b/src/HOL/Transcendental.thy Thu Jun 04 15:30:22 2020 +0000 @@ -688,7 +688,7 @@ qed then have "\p q. \p < n; q < n - Suc 0\ \ norm ((z + h) ^ q * z ^ (n - 2 - q)) \ K ^ (n - 2)" - by simp + by (simp del: subst_all') then show "norm (\pq of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))"