# HG changeset patch # User haftmann # Date 1593691858 0 # Node ID bad75618fb8277c6073e641b11ec53ded49343df # Parent ace45a11a45ed97dfb656340e0488d3fc006cd2e extraction of equations x = t from premises beneath meta-all diff -r ace45a11a45e -r bad75618fb82 CONTRIBUTORS --- a/CONTRIBUTORS Thu Jul 02 08:49:04 2020 +0000 +++ b/CONTRIBUTORS Thu Jul 02 12:10:58 2020 +0000 @@ -20,6 +20,10 @@ * May 2020: Florian Haftmann Generic algebraically founded bit operations NOT, AND, OR, XOR. +* June 2020: Florian Haftmann + Simproc defined_all for more aggressive substitution with variables + from assumptions. + Contributions to Isabelle2020 ----------------------------- diff -r ace45a11a45e -r bad75618fb82 NEWS --- a/NEWS Thu Jul 02 08:49:04 2020 +0000 +++ b/NEWS Thu Jul 02 12:10:58 2020 +0000 @@ -77,10 +77,10 @@ * Session HOL-Word: Theory Z2 is not used any longer. Minor INCOMPATIBILITY. -* Rewrite rule subst_all performs +* Simproc defined_all and rewrite rule subst_all perform more aggressive substitution with variables from assumptions. INCOMPATIBILITY, use something like -"supply subst_all [simp del]" +"supply subst_all [simp del] [[simproc del: defined_all]]" to leave fragile proofs unaffected. diff -r ace45a11a45e -r bad75618fb82 src/HOL/Auth/Guard/P1.thy --- a/src/HOL/Auth/Guard/P1.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/Auth/Guard/P1.thy Thu Jul 02 12:10:58 2020 +0000 @@ -282,6 +282,7 @@ lemma insertion_resilience: "\L. L \ valid A n B \ Suc i < len L \ ins (L,Suc i,M) \ valid A n B" +supply [[simproc del: defined_all]] apply (induct i) (* i = 0 *) apply clarify @@ -481,6 +482,7 @@ lemma pro_imp_Guard [rule_format]: "[| evs \ p1; B \ bad; A \ bad |] ==> pro B ofr A r I (cons M L) J C \ set evs \ Guard ofr {priK A} (spies evs)" +supply [[simproc del: defined_all]] apply (erule p1.induct) (* +3 subgoals *) (* Nil *) apply simp diff -r ace45a11a45e -r bad75618fb82 src/HOL/Auth/Guard/P2.thy --- a/src/HOL/Auth/Guard/P2.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/Auth/Guard/P2.thy Thu Jul 02 12:10:58 2020 +0000 @@ -193,6 +193,7 @@ lemma insertion_resilience: "\L. L \ valid A n B \ Suc i < len L \ ins (L,Suc i,M) \ valid A n B" +supply [[simproc del: defined_all]] apply (induct i) (* i = 0 *) apply clarify @@ -393,6 +394,7 @@ lemma pro_imp_Guard [rule_format]: "[| evs \ p2; B \ bad; A \ bad |] ==> pro B ofr A r I (cons M L) J C \ set evs \ Guard ofr {priK A} (spies evs)" +supply [[simproc del: defined_all]] apply (erule p2.induct) (* +3 subgoals *) (* Nil *) apply simp diff -r ace45a11a45e -r bad75618fb82 src/HOL/Bali/DefiniteAssignmentCorrect.thy --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Thu Jul 02 12:10:58 2020 +0000 @@ -981,7 +981,8 @@ from fvar obtain upd w where upd: "upd = snd (fst (fvar statDeclC stat fn a s2))" and v: "v=(w,upd)" - by (cases "fvar statDeclC stat fn a s2") simp + by (cases "fvar statDeclC stat fn a s2") + (simp, use surjective_pairing in blast) { fix j val fix s::state assume "normal s3" @@ -1025,7 +1026,8 @@ from avar obtain upd w where upd: "upd = snd (fst (avar G i a s2))" and v: "v=(w,upd)" - by (cases "avar G i a s2") simp + by (cases "avar G i a s2") + (simp, use surjective_pairing in blast) { fix j val fix s::state assume "normal s2'" diff -r ace45a11a45e -r bad75618fb82 src/HOL/Data_Structures/AVL_Bal_Set.thy --- a/src/HOL/Data_Structures/AVL_Bal_Set.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/Data_Structures/AVL_Bal_Set.thy Thu Jul 02 12:10:58 2020 +0000 @@ -139,7 +139,6 @@ avl t' \ height t = height t' + (if decr t t' then 1 else 0)" apply(induction t arbitrary: t' a rule: split_max_induct) apply(auto simp: max_absorb1 max_absorb2 height_1_iff split!: splits prod.splits) -apply(fastforce)+ done lemma avl_delete: "avl t \ diff -r ace45a11a45e -r bad75618fb82 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/HOL.thy Thu Jul 02 12:10:58 2020 +0000 @@ -1234,8 +1234,6 @@ simproc_setup defined_All ("\x. P x") = \K Quantifier1.rearrange_All\ simproc_setup defined_all("\x. PROP P x") = \K Quantifier1.rearrange_all\ -declare [[simproc del: defined_all]] - text \Simproc for proving \(y = x) \ False\ from premise \\ (x = y)\:\ simproc_setup neq ("x = y") = \fn _ => diff -r ace45a11a45e -r bad75618fb82 src/HOL/HOLCF/IOA/Abstraction.thy --- a/src/HOL/HOLCF/IOA/Abstraction.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/HOLCF/IOA/Abstraction.thy Thu Jul 02 12:10:58 2020 +0000 @@ -296,7 +296,6 @@ apply (simp add: nil_is_Conc) text \cons case\ apply (pair aa) - apply auto done (* important property of ex2seq: can be shiftet, as defined "pointwise" *) diff -r ace45a11a45e -r bad75618fb82 src/HOL/HOLCF/IOA/TLS.thy --- a/src/HOL/HOLCF/IOA/TLS.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/HOLCF/IOA/TLS.thy Thu Jul 02 12:10:58 2020 +0000 @@ -153,9 +153,7 @@ apply (pair ex) apply (Seq_case x2) apply (simp add: unlift_def) - apply fast apply (simp add: unlift_def) - apply fast apply (simp add: unlift_def) apply (pair a) apply (Seq_case_simp s) diff -r ace45a11a45e -r bad75618fb82 src/HOL/Hoare/Pointer_Examples.thy --- a/src/HOL/Hoare/Pointer_Examples.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/Hoare/Pointer_Examples.thy Thu Jul 02 12:10:58 2020 +0000 @@ -31,7 +31,6 @@ \<^cancel>\apply clarsimp\ \<^cancel>\apply(rename_tac ps')\ \<^cancel>\apply(fastforce intro:notin_List_update[THEN iffD2])\ - apply fastforce done text\And now with ghost variables \<^term>\ps\ and \<^term>\qs\. Even @@ -48,7 +47,6 @@ {List next q (rev Ps @ Qs)}" apply vcg_simp apply fastforce -apply fastforce done text "A longer readable version:" @@ -104,7 +102,6 @@ apply vcg_simp apply clarsimp apply clarsimp -apply clarsimp done @@ -461,7 +458,6 @@ apply (simp only:distPath_def) apply vcg_simp apply clarsimp - apply clarsimp apply (case_tac "(q = Null)") apply (fastforce intro: Path_is_List) apply clarsimp @@ -499,7 +495,6 @@ {islist next p \ map elem (rev(list next p)) = Xs}" apply vcg_simp apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin) -apply fastforce done diff -r ace45a11a45e -r bad75618fb82 src/HOL/Hoare/Pointer_ExamplesAbort.thy --- a/src/HOL/Hoare/Pointer_ExamplesAbort.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/Hoare/Pointer_ExamplesAbort.thy Thu Jul 02 12:10:58 2020 +0000 @@ -23,7 +23,6 @@ apply vcg_simp apply fastforce apply(fastforce intro:notin_List_update[THEN iffD2]) -apply fastforce done end diff -r ace45a11a45e -r bad75618fb82 src/HOL/Hoare/Pointers0.thy --- a/src/HOL/Hoare/Pointers0.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/Hoare/Pointers0.thy Thu Jul 02 12:10:58 2020 +0000 @@ -198,7 +198,6 @@ \<^cancel>\apply simp\ \<^cancel>\apply(rule_tac x = "p#qs" in exI)\ \<^cancel>\apply simp\ - apply fastforce done @@ -254,7 +253,6 @@ apply vcg_simp apply clarsimp apply clarsimp -apply clarsimp done @@ -427,7 +425,6 @@ {islist next p \ map elem (rev(list next p)) = Xs}" apply vcg_simp apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin) -apply fastforce done diff -r ace45a11a45e -r bad75618fb82 src/HOL/Hoare_Parallel/RG_Hoare.thy --- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Thu Jul 02 12:10:58 2020 +0000 @@ -174,6 +174,7 @@ "\m i. x\cptn \ m \ length x \ (\i. Suc i < m \ \ x!i -c\ x!Suc i) \ Suc i < m \ x!i -e\ x!Suc i" + supply [[simproc del: defined_all]] apply(induct x,simp) apply clarify apply(erule cptn.cases,simp) @@ -185,7 +186,7 @@ apply(subgoal_tac "(\i. Suc i < nata \ (((P, t) # xs) ! i, xs ! i) \ ctran)") apply force apply clarify - apply(erule_tac x="Suc ia" in allE,simp) + apply(erule_tac x="Suc ia" in allE,simp) apply(erule_tac x="0" and P="\j. H j \ (J j) \ ctran" for H J in allE,simp) done @@ -232,6 +233,7 @@ (\i. (Suc i) (x!i -e\ x!(Suc i)) \ (snd(x!i), snd(x!(Suc i))) \ rely) \ (\i. j\i \ i x!i -e\ x!Suc i) \ snd(x!k)\p \ fst(x!j)=fst(x!k)" + supply [[simproc del: defined_all]] apply(induct x) apply clarify apply(force elim:cptn.cases) @@ -326,6 +328,7 @@ " \pre \ {s. f s \ post}; {(s, t). s \ pre \ t = f s} \ guar; stable pre rely; stable post rely\ \ \ Basic f sat [pre, rely, guar, post]" + supply [[simproc del: defined_all]] apply(unfold com_validity_def) apply clarify apply(simp add:comm_def) @@ -595,6 +598,7 @@ "x\ cptn_mod \ \s P. x !0=(Some (Seq P Q), s) \ (\iSome Q) \ (\xs\ cp (Some P) s. x=map (lift Q) xs)" + supply [[simproc del: defined_all]] apply(erule cptn_mod.induct) apply(unfold cp_def) apply safe @@ -625,6 +629,7 @@ (\j(Some Q)) \ (\xs ys. xs \ cp (Some P) s \ length xs=Suc i \ ys \ cp (Some Q) (snd(xs !i)) \ x=(map (lift Q) xs)@tl ys)" + supply [[simproc del: defined_all]] apply(erule cptn.induct) apply(unfold cp_def) apply safe @@ -879,6 +884,7 @@ "\ pre \ - b \ post; \ P sat [pre \ b, rely, guar, pre]; \s. (s, s) \ guar; stable pre rely; stable post rely; x \ cptn_mod \ \ \s xs. x=(Some(While b P),s)#xs \ x\assum(pre, rely) \ x \ comm (guar, post)" + supply [[simproc del: defined_all]] apply(erule cptn_mod.induct) apply safe apply (simp_all del:last.simps) diff -r ace45a11a45e -r bad75618fb82 src/HOL/Hoare_Parallel/RG_Tran.thy --- a/src/HOL/Hoare_Parallel/RG_Tran.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/Hoare_Parallel/RG_Tran.thy Thu Jul 02 12:10:58 2020 +0000 @@ -176,6 +176,7 @@ lemma cptn_onlyif_cptn_mod_aux [rule_format]: "\s Q t xs.((Some a, s), Q, t) \ ctran \ (Q, t) # xs \ cptn_mod \ (Some a, s) # (Q, t) # xs \ cptn_mod" + supply [[simproc del: defined_all]] apply(induct a) apply simp_all \ \basic\ @@ -718,6 +719,7 @@ (\clist. (length clist = length xs) \ (xs, s)#ys \ map (\i. (fst i,s)#(snd i)) (zip xs clist) \ (\i cptn))" + supply [[simproc del: defined_all]] apply(induct ys) apply(clarify) apply(rule_tac x="map (\i. []) [0.. sttp_of (compTpInitLvars jmb lvars (ST, pre @ replicate (length lvars) Err)) = (ST, pre @ map (Fun.comp OK snd) lvars)" + supply [[simproc del: defined_all]] apply (induct lvars) apply simp diff -r ace45a11a45e -r bad75618fb82 src/HOL/MicroJava/J/WellForm.thy --- a/src/HOL/MicroJava/J/WellForm.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/MicroJava/J/WellForm.thy Thu Jul 02 12:10:58 2020 +0000 @@ -532,7 +532,6 @@ apply (erule_tac x = "Da" in allE) apply (clarsimp) apply (simp add: map_of_map) - apply (clarify) apply (subst method_rec, assumption+) apply (simp add: map_add_def map_of_map split: option.split) done @@ -552,7 +551,6 @@ apply (erule_tac x = "Da" in allE) apply (clarsimp) apply (simp add: map_of_map) - apply (clarify) apply (subst method_rec, assumption+) apply (simp add: map_add_def map_of_map split: option.split) done @@ -599,7 +597,6 @@ apply (simp (no_asm_use) only: map_add_Some_iff) apply (erule disjE) apply (simp (no_asm_use) add: map_of_map) apply blast -apply blast apply (rule trans [symmetric], rule sym, assumption) apply (rule_tac x=vn in fun_cong) apply (rule trans, rule field_rec, assumption+) diff -r ace45a11a45e -r bad75618fb82 src/HOL/Nominal/Examples/Class1.thy --- a/src/HOL/Nominal/Examples/Class1.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/Nominal/Examples/Class1.thy Thu Jul 02 12:10:58 2020 +0000 @@ -2936,7 +2936,9 @@ apply(subgoal_tac "y\[aa].Ma") apply(drule sym) apply(simp_all add: abs_fresh) -done +apply (metis abs_fresh(5)) +done + lemma fin_rest_elims: shows "fin (Cut .M (x).N) y \ False" @@ -2958,7 +2960,7 @@ lemma not_fin_subst1: assumes a: "\(fin M x)" shows "\(fin (M{c:=(y).P}) x)" -using a +using a [[simproc del: defined_all]] apply(nominal_induct M avoiding: x c y P rule: trm.strong_induct) apply(auto) apply(drule fin_elims, simp) @@ -3043,7 +3045,7 @@ lemma not_fin_subst2: assumes a: "\(fin M x)" shows "\(fin (M{y:=.P}) x)" -using a +using a [[simproc del: defined_all]] apply(nominal_induct M avoiding: x c y P rule: trm.strong_induct) apply(auto) apply(erule fin.cases, simp_all add: trm.inject) @@ -3157,7 +3159,6 @@ apply(drule fin_elims, simp) apply(drule fin_elims, simp) apply(rule fin.intros) -apply(auto)[1] apply(rule subst_fresh) apply(simp) apply(drule fin_elims, simp) @@ -3195,7 +3196,7 @@ lemma fin_substn_nrename: assumes a: "fin M x" "x\y" "x\P" shows "M[x\n>y]{y:=.P} = Cut .P (x).(M{y:=.P})" -using a +using a [[simproc del: defined_all]] apply(nominal_induct M avoiding: x y c P rule: trm.strong_induct) apply(drule fin_Ax_elim) apply(simp) @@ -3440,7 +3441,6 @@ apply(rule exists_fresh'(1)[OF fs_name1]) apply(drule fic_elims, simp) apply(drule fic_elims, simp) -apply(auto)[1] apply(simp add: abs_fresh fresh_atm) apply(drule freshc_after_substn) apply(simp add: fic.intros abs_fresh) @@ -3471,7 +3471,6 @@ apply(drule fic_elims, simp) apply(rule exists_fresh'(2)[OF fs_coname1]) apply(drule fic_elims, simp) -apply(erule conjE)+ apply(drule freshc_after_substc) apply(simp) apply(simp add: fic.intros abs_fresh) @@ -3501,7 +3500,6 @@ apply(drule fic_elims, simp) apply(rule exists_fresh'(2)[OF fs_coname1]) apply(drule fic_elims, simp) -apply(auto)[1] apply(simp add: abs_fresh fresh_atm) apply(drule freshc_after_substc) apply(simp) @@ -3514,7 +3512,6 @@ apply(drule fic_elims, simp) apply(rule exists_fresh'(2)[OF fs_coname1]) apply(drule fic_elims, simp) -apply(auto)[1] apply(simp add: abs_fresh fresh_atm) apply(drule freshc_after_substc) apply(simp) @@ -3528,7 +3525,6 @@ apply(drule fic_elims, simp) apply(rule exists_fresh'(2)[OF fs_coname1]) apply(drule fic_elims, simp) -apply(auto)[1] apply(simp add: abs_fresh fresh_atm) apply(drule freshc_after_substc) apply(simp) @@ -3546,7 +3542,6 @@ apply(drule fic_elims, simp) apply(drule fic_elims, simp) apply(rule fic.intros) -apply(auto)[1] apply(rule subst_fresh) apply(simp) apply(drule fic_elims, simp) @@ -3590,7 +3585,6 @@ apply(drule fic_elims, simp) apply(drule fic_elims, simp) apply(rule fic.intros) -apply(auto)[1] apply(rule subst_fresh) apply(simp) apply(drule fic_elims, simp) @@ -3683,7 +3677,6 @@ apply(simp) apply(drule fic_ImpR_elim) apply(simp add: abs_fresh fresh_atm) -apply(auto)[1] apply(generate_fresh "coname") apply(fresh_fun_simp) apply(simp add: trm.inject alpha fresh_atm calc_atm abs_fresh fresh_prod) @@ -4715,7 +4708,7 @@ lemma a_redu_NotL_elim: assumes a: "NotL .M x \\<^sub>a R" shows "\M'. R = NotL .M' x \ M\\<^sub>aM'" -using a +using a [[simproc del: defined_all]] apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) @@ -4736,7 +4729,7 @@ lemma a_redu_NotR_elim: assumes a: "NotR (x).M a \\<^sub>a R" shows "\M'. R = NotR (x).M' a \ M\\<^sub>aM'" -using a +using a [[simproc del: defined_all]] apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) @@ -4757,7 +4750,7 @@ lemma a_redu_AndR_elim: assumes a: "AndR .M .N c\\<^sub>a R" shows "(\M'. R = AndR .M' .N c \ M\\<^sub>aM') \ (\N'. R = AndR .M .N' c \ N\\<^sub>aN')" -using a +using a [[simproc del: defined_all]] apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) @@ -4846,7 +4839,7 @@ lemma a_redu_AndL1_elim: assumes a: "AndL1 (x).M y \\<^sub>a R" shows "\M'. R = AndL1 (x).M' y \ M\\<^sub>aM'" -using a +using a [[simproc del: defined_all]] apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) @@ -4867,7 +4860,7 @@ lemma a_redu_AndL2_elim: assumes a: "AndL2 (x).M y \\<^sub>a R" shows "\M'. R = AndL2 (x).M' y \ M\\<^sub>aM'" -using a +using a [[simproc del: defined_all]] apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) @@ -4888,7 +4881,7 @@ lemma a_redu_OrL_elim: assumes a: "OrL (x).M (y).N z\\<^sub>a R" shows "(\M'. R = OrL (x).M' (y).N z \ M\\<^sub>aM') \ (\N'. R = OrL (x).M (y).N' z \ N\\<^sub>aN')" -using a +using a [[simproc del: defined_all]] apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) @@ -4977,7 +4970,7 @@ lemma a_redu_OrR1_elim: assumes a: "OrR1 .M b \\<^sub>a R" shows "\M'. R = OrR1 .M' b \ M\\<^sub>aM'" -using a +using a [[simproc del: defined_all]] apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) @@ -4998,7 +4991,7 @@ lemma a_redu_OrR2_elim: assumes a: "OrR2 .M b \\<^sub>a R" shows "\M'. R = OrR2 .M' b \ M\\<^sub>aM'" -using a +using a [[simproc del: defined_all]] apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) @@ -5019,7 +5012,7 @@ lemma a_redu_ImpL_elim: assumes a: "ImpL .M (y).N z\\<^sub>a R" shows "(\M'. R = ImpL .M' (y).N z \ M\\<^sub>aM') \ (\N'. R = ImpL .M (y).N' z \ N\\<^sub>aN')" -using a +using a [[simproc del: defined_all]] apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) @@ -5108,7 +5101,7 @@ lemma a_redu_ImpR_elim: assumes a: "ImpR (x)..M b \\<^sub>a R" shows "\M'. R = ImpR (x)..M' b \ M\\<^sub>aM'" -using a +using a [[simproc del: defined_all]] apply(erule_tac a_redu.cases, simp_all add: trm.inject) apply(erule_tac l_redu.cases, simp_all add: trm.inject) apply(erule_tac c_redu.cases, simp_all add: trm.inject) @@ -5454,7 +5447,6 @@ apply(rule exists_fresh'(2)[OF fs_coname1]) apply(drule fin_elims, simp) apply(drule fin_elims, simp) -apply(auto)[1] apply(drule freshn_after_substc) apply(simp add: fin.intros) apply(subgoal_tac "\c'::coname. c'\(trm1{coname3:=(x).P},P,coname1,trm2{coname3:=(x).P},coname2)") @@ -5466,12 +5458,10 @@ apply(rule exists_fresh'(2)[OF fs_coname1]) apply(drule fin_elims, simp) apply(drule fin_elims, simp) -apply(auto)[1] apply(simp add: abs_fresh fresh_atm) apply(drule freshn_after_substc) apply(simp add: fin.intros abs_fresh) apply(drule fin_elims, simp) -apply(auto)[1] apply(simp add: abs_fresh fresh_atm) apply(drule freshn_after_substc) apply(simp add: fin.intros abs_fresh) @@ -5578,7 +5568,6 @@ apply(drule fic_elims, simp) apply(drule fic_elims, simp) apply(drule fic_elims, simp) -apply(auto)[1] apply(drule freshc_after_substn) apply(simp add: fic.intros) apply(subgoal_tac "\x'::name. x'\(trm{x:=.P},P)") @@ -5612,12 +5601,10 @@ apply(rule exists_fresh'(1)[OF fs_name1]) apply(drule fic_elims, simp) apply(drule fic_elims, simp) -apply(auto)[1] apply(simp add: abs_fresh fresh_atm) apply(drule freshc_after_substn) apply(simp add: fic.intros abs_fresh) apply(drule fic_elims, simp) -apply(auto)[1] apply(simp add: abs_fresh fresh_atm) apply(drule freshc_after_substn) apply(simp add: fic.intros abs_fresh) @@ -5630,7 +5617,6 @@ apply(rule exists_fresh'(1)[OF fs_name1]) apply(drule fic_elims, simp) apply(drule fic_elims, simp) -apply(auto)[1] apply(simp add: abs_fresh fresh_atm) apply(drule freshc_after_substn) apply(simp add: fic.intros abs_fresh) diff -r ace45a11a45e -r bad75618fb82 src/HOL/Nominal/Examples/Class3.thy --- a/src/HOL/Nominal/Examples/Class3.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/Nominal/Examples/Class3.thy Thu Jul 02 12:10:58 2020 +0000 @@ -297,7 +297,7 @@ assumes a: "R[a\c>b] = AndR .M .N e" "c\(a,b,d,e,N,R)" "d\(a,b,c,e,M,R)" "e\a" shows "(\M' N'. R = AndR .M' .N' e \ M'[a\c>b] = M \ N'[a\c>b] = N \ c\N' \ d\M') \ (\M' N'. R = AndR .M' .N' a \ b=e \ M'[a\c>b] = M \ N'[a\c>b] = N \ c\N' \ d\M')" -using a +using a [[simproc del: defined_all]] apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct) apply(auto split: if_splits simp add: trm.inject alpha)[1] apply(auto split: if_splits simp add: trm.inject alpha)[1] @@ -1487,7 +1487,7 @@ assumes a: "R[x\n>y] = OrL (v).M (w).N u" "v\(R,N,u,x,y)" "w\(R,M,u,x,y)" "x\y" shows "(\M' N'. (R = OrL (v).M' (w).N' u) \ M'[x\n>y] = M \ N'[x\n>y] = N) \ (\M' N'. (R = OrL (v).M' (w).N' x) \ y=u \ M'[x\n>y] = M \ N'[x\n>y] = N)" -using a +using a [[simproc del: defined_all]] apply(nominal_induct R avoiding: y x u v w M N rule: trm.strong_induct) apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject) apply(rule_tac x="[(name1,v)]\trm1" in exI) @@ -1550,7 +1550,7 @@ assumes a: "R[x\n>y] = ImpL .M (w).N u" "c\(R,N)" "w\(R,M,u,x,y)" "x\y" shows "(\M' N'. (R = ImpL .M' (w).N' u) \ M'[x\n>y] = M \ N'[x\n>y] = N) \ (\M' N'. (R = ImpL .M' (w).N' x) \ y=u \ M'[x\n>y] = M \ N'[x\n>y] = N)" -using a +using a [[simproc del: defined_all]] apply(nominal_induct R avoiding: y x u c w M N rule: trm.strong_induct) apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject) apply(rule_tac x="[(coname,c)]\trm1" in exI) @@ -2367,7 +2367,7 @@ and a3: "(x):N \ (\(B)\)" and a4: "SNa N" shows "SNa (Cut .M (x).N)" -using a1 a2 a3 a4 +using a1 a2 a3 a4 [[simproc del: defined_all]] apply(induct B M N arbitrary: a x rule: my_wf_induct_triple''[OF wf_measure_triple]) apply(rule SNaI) apply(drule Cut_a_redu_elim) diff -r ace45a11a45e -r bad75618fb82 src/HOL/Nominal/Examples/Standardization.thy --- a/src/HOL/Nominal/Examples/Standardization.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/Nominal/Examples/Standardization.thy Thu Jul 02 12:10:58 2020 +0000 @@ -368,6 +368,7 @@ "(\r'. r \\<^sub>\ r' \ s = r' \\ rs) \ (\rs'. rs [\\<^sub>\]\<^sub>1 rs' \ s = r \\ rs') \ (\t u us. x \ r \ r = (Lam [x].t) \ rs = u # us \ s = t[x::=u] \\ us)" + supply [[simproc del: defined_all]] apply (nominal_induct u \ "r \\ rs" s avoiding: x r rs rule: beta.strong_induct) apply (simp add: App_eq_foldl_conv) apply (split if_split_asm) diff -r ace45a11a45e -r bad75618fb82 src/HOL/Probability/Random_Permutations.thy --- a/src/HOL/Probability/Random_Permutations.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/Probability/Random_Permutations.thy Thu Jul 02 12:10:58 2020 +0000 @@ -51,7 +51,7 @@ | "finite A \ A \ {} \ fold_random_permutation f x A = pmf_of_set A \ (\a. fold_random_permutation f (f a x) (A - {a}))" -by (force, simp_all) + by simp_all fastforce termination proof (relation "Wellfounded.measure (\(_,_,A). card A)") fix A :: "'a set" and f :: "'a \ 'b \ 'b" and x :: 'b and y :: 'a assume A: "finite A" "A \ {}" "y \ set_pmf (pmf_of_set A)" @@ -126,7 +126,7 @@ | "finite A \ A \ {} \ fold_bind_random_permutation f g x A = pmf_of_set A \ (\a. fold_bind_random_permutation f g (f a x) (A - {a}))" -by (force, simp_all) + by simp_all fastforce termination proof (relation "Wellfounded.measure (\(_,_,_,A). card A)") fix A :: "'a set" and f :: "'a \ 'b \ 'b" and x :: 'b and y :: 'a and g :: "'b \ 'c pmf" diff -r ace45a11a45e -r bad75618fb82 src/HOL/Proofs/Extraction/Higman.thy --- a/src/HOL/Proofs/Extraction/Higman.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/Proofs/Extraction/Higman.thy Thu Jul 02 12:10:58 2020 +0000 @@ -58,6 +58,7 @@ by (erule L.induct) iprover+ lemma lemma2': "R a vs ws \ L as vs \ L (a # as) ws" + supply [[simproc del: defined_all]] apply (induct set: R) apply (erule L.cases) apply simp+ @@ -69,17 +70,19 @@ done lemma lemma2: "R a vs ws \ good vs \ good ws" + supply [[simproc del: defined_all]] apply (induct set: R) apply iprover apply (erule good.cases) apply simp_all apply (rule good0) apply (erule lemma2') - apply assumption + apply assumption apply (erule good1) done lemma lemma3': "T a vs ws \ L as vs \ L (a # as) ws" + supply [[simproc del: defined_all]] apply (induct set: T) apply (erule L.cases) apply simp_all @@ -93,6 +96,7 @@ done lemma lemma3: "T a ws zs \ good ws \ good zs" + supply [[simproc del: defined_all]] apply (induct set: T) apply (erule good.cases) apply simp_all @@ -107,6 +111,7 @@ done lemma lemma4: "R a ws zs \ ws \ [] \ T a ws zs" + supply [[simproc del: defined_all]] apply (induct set: R) apply iprover apply (case_tac vs) diff -r ace45a11a45e -r bad75618fb82 src/HOL/Proofs/Extraction/Warshall.thy --- a/src/HOL/Proofs/Extraction/Warshall.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/Proofs/Extraction/Warshall.thy Thu Jul 02 12:10:58 2020 +0000 @@ -62,8 +62,8 @@ theorem lemma2: "\p. is_path r p 0 j k \ r j k = T" unfolding is_path_def apply (simp cong add: conj_cong add: split_paired_all) - apply (case_tac "aa") - apply simp+ + apply (case_tac a) + apply simp_all done theorem is_path'_conc: "is_path' r j xs i \ is_path' r i ys k \ diff -r ace45a11a45e -r bad75618fb82 src/HOL/Proofs/Lambda/LambdaType.thy --- a/src/HOL/Proofs/Lambda/LambdaType.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/Proofs/Lambda/LambdaType.thy Thu Jul 02 12:10:58 2020 +0000 @@ -120,13 +120,19 @@ apply simp done -lemma types_snocE: "e \ ts @ [t] : Ts \ - (\Us U. Ts = Us @ [U] \ e \ ts : Us \ e \ t : U \ P) \ P" - apply (cases Ts rule: rev_exhaust2) - apply simp - apply (case_tac "ts @ [t]") - apply (simp add: types_snoc_eq)+ - done +lemma types_snocE: + assumes \e \ ts @ [t] : Ts\ + obtains Us and U where \Ts = Us @ [U]\ \e \ ts : Us\ \e \ t : U\ +proof (cases Ts rule: rev_exhaust2) + case Nil + with assms show ?thesis + by (cases "ts @ [t]") simp_all +next + case (snoc Us U) + with assms have "e \ ts @ [t] : Us @ [U]" by simp + then have "e \ ts : Us" "e \ t : U" by (simp_all add: types_snoc_eq) + with snoc show ?thesis by (rule that) +qed subsection \n-ary function types\ diff -r ace45a11a45e -r bad75618fb82 src/HOL/Proofs/Lambda/WeakNorm.thy --- a/src/HOL/Proofs/Lambda/WeakNorm.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Thu Jul 02 12:10:58 2020 +0000 @@ -261,7 +261,7 @@ declare NF.induct [ind_realizer] declare rtranclp.induct [ind_realizer irrelevant] declare rtyping.induct [ind_realizer] -lemmas [extraction_expand] = conj_assoc listall_cons_eq +lemmas [extraction_expand] = conj_assoc listall_cons_eq subst_all equal_allI extract type_NF diff -r ace45a11a45e -r bad75618fb82 src/HOL/ROOT --- a/src/HOL/ROOT Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/ROOT Thu Jul 02 12:10:58 2020 +0000 @@ -73,7 +73,6 @@ OptionalSugar (*prototypic tools*) Predicate_Compile_Quickcheck - Quantified_Premise_Simproc (*legacy tools*) Old_Datatype Old_Recdef diff -r ace45a11a45e -r bad75618fb82 src/HOL/Word/Bits_Int.thy --- a/src/HOL/Word/Bits_Int.thy Thu Jul 02 08:49:04 2020 +0000 +++ b/src/HOL/Word/Bits_Int.thy Thu Jul 02 12:10:58 2020 +0000 @@ -823,7 +823,6 @@ apply clarsimp apply (drule bthrs) apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm) - apply clarify apply (erule allE, erule impE, erule exI) apply (case_tac k) apply clarsimp