--- 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
-----------------------------
--- 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.
--- 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: "\<forall>L. L \<in> valid A n B \<longrightarrow> Suc i < len L
\<longrightarrow> ins (L,Suc i,M) \<notin> 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 \<in> p1; B \<notin> bad; A \<notin> bad |] ==>
pro B ofr A r I (cons M L) J C \<in> set evs \<longrightarrow> Guard ofr {priK A} (spies evs)"
+supply [[simproc del: defined_all]]
apply (erule p1.induct) (* +3 subgoals *)
(* Nil *)
apply simp
--- 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: "\<forall>L. L \<in> valid A n B \<longrightarrow> Suc i < len L
\<longrightarrow> ins (L,Suc i,M) \<notin> 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 \<in> p2; B \<notin> bad; A \<notin> bad |] ==>
pro B ofr A r I (cons M L) J C \<in> set evs \<longrightarrow> Guard ofr {priK A} (spies evs)"
+supply [[simproc del: defined_all]]
apply (erule p2.induct) (* +3 subgoals *)
(* Nil *)
apply simp
--- 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'"
--- 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' \<and> 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 \<Longrightarrow>
--- 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 ("\<forall>x. P x") = \<open>K Quantifier1.rearrange_All\<close>
simproc_setup defined_all("\<And>x. PROP P x") = \<open>K Quantifier1.rearrange_all\<close>
-declare [[simproc del: defined_all]]
-
text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>
simproc_setup neq ("x = y") = \<open>fn _ =>
--- 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 \<open>cons case\<close>
apply (pair aa)
- apply auto
done
(* important property of ex2seq: can be shiftet, as defined "pointwise" *)
--- 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)
--- 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>\<open>apply clarsimp\<close>
\<^cancel>\<open>apply(rename_tac ps')\<close>
\<^cancel>\<open>apply(fastforce intro:notin_List_update[THEN iffD2])\<close>
- apply fastforce
done
text\<open>And now with ghost variables \<^term>\<open>ps\<close> and \<^term>\<open>qs\<close>. 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 \<and> 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
--- 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
--- 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>\<open>apply simp\<close>
\<^cancel>\<open>apply(rule_tac x = "p#qs" in exI)\<close>
\<^cancel>\<open>apply simp\<close>
- apply fastforce
done
@@ -254,7 +253,6 @@
apply vcg_simp
apply clarsimp
apply clarsimp
-apply clarsimp
done
@@ -427,7 +425,6 @@
{islist next p \<and> 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
--- 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 @@
"\<forall>m i. x\<in>cptn \<longrightarrow> m \<le> length x
\<longrightarrow> (\<forall>i. Suc i < m \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i) \<longrightarrow> Suc i < m
\<longrightarrow> x!i -e\<rightarrow> 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 "(\<forall>i. Suc i < nata \<longrightarrow> (((P, t) # xs) ! i, xs ! i) \<notin> 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="\<lambda>j. H j \<longrightarrow> (J j) \<notin> ctran" for H J in allE,simp)
done
@@ -232,6 +233,7 @@
(\<forall>i. (Suc i)<length x \<longrightarrow>
(x!i -e\<rightarrow> x!(Suc i)) \<longrightarrow> (snd(x!i), snd(x!(Suc i))) \<in> rely) \<longrightarrow>
(\<forall>i. j\<le>i \<and> i<k \<longrightarrow> x!i -e\<rightarrow> x!Suc i) \<longrightarrow> snd(x!k)\<in>p \<and> 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 @@
" \<lbrakk>pre \<subseteq> {s. f s \<in> post}; {(s, t). s \<in> pre \<and> t = f s} \<subseteq> guar;
stable pre rely; stable post rely\<rbrakk>
\<Longrightarrow> \<Turnstile> 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\<in> cptn_mod \<Longrightarrow> \<forall>s P. x !0=(Some (Seq P Q), s) \<longrightarrow>
(\<forall>i<length x. fst(x!i)\<noteq>Some Q) \<longrightarrow>
(\<exists>xs\<in> 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 @@
(\<forall>j<i. fst(x!j)\<noteq>(Some Q)) \<longrightarrow>
(\<exists>xs ys. xs \<in> cp (Some P) s \<and> length xs=Suc i
\<and> ys \<in> cp (Some Q) (snd(xs !i)) \<and> 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 @@
"\<lbrakk> pre \<inter> - b \<subseteq> post; \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s, s) \<in> guar;
stable pre rely; stable post rely; x \<in> cptn_mod \<rbrakk>
\<Longrightarrow> \<forall>s xs. x=(Some(While b P),s)#xs \<longrightarrow> x\<in>assum(pre, rely) \<longrightarrow> x \<in> comm (guar, post)"
+ supply [[simproc del: defined_all]]
apply(erule cptn_mod.induct)
apply safe
apply (simp_all del:last.simps)
--- 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]:
"\<forall>s Q t xs.((Some a, s), Q, t) \<in> ctran \<longrightarrow> (Q, t) # xs \<in> cptn_mod
\<longrightarrow> (Some a, s) # (Q, t) # xs \<in> cptn_mod"
+ supply [[simproc del: defined_all]]
apply(induct a)
apply simp_all
\<comment> \<open>basic\<close>
@@ -718,6 +719,7 @@
(\<exists>clist. (length clist = length xs) \<and>
(xs, s)#ys \<propto> map (\<lambda>i. (fst i,s)#(snd i)) (zip xs clist) \<and>
(\<forall>i<length xs. (xs!i,s)#(clist!i) \<in> cptn))"
+ supply [[simproc del: defined_all]]
apply(induct ys)
apply(clarify)
apply(rule_tac x="map (\<lambda>i. []) [0..<length xs]" in exI)
--- a/src/HOL/Library/Quantified_Premise_Simproc.thy Thu Jul 02 08:49:04 2020 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-(* Author: Florian Haftmann, TU München *)
-
-theory Quantified_Premise_Simproc
- imports Main
-begin
-
-declare [[simproc add: defined_all]]
-
-end
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Jul 02 12:10:58 2020 +0000
@@ -410,6 +410,7 @@
\<longrightarrow>
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
--- 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+)
--- 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\<sharp>[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 <a>.M (x).N) y \<Longrightarrow> False"
@@ -2958,7 +2960,7 @@
lemma not_fin_subst1:
assumes a: "\<not>(fin M x)"
shows "\<not>(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: "\<not>(fin M x)"
shows "\<not>(fin (M{y:=<c>.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\<noteq>y" "x\<sharp>P"
shows "M[x\<turnstile>n>y]{y:=<c>.P} = Cut <c>.P (x).(M{y:=<c>.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 <a>.M x \<longrightarrow>\<^sub>a R"
shows "\<exists>M'. R = NotL <a>.M' x \<and> M\<longrightarrow>\<^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 \<longrightarrow>\<^sub>a R"
shows "\<exists>M'. R = NotR (x).M' a \<and> M\<longrightarrow>\<^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 <a>.M <b>.N c\<longrightarrow>\<^sub>a R"
shows "(\<exists>M'. R = AndR <a>.M' <b>.N c \<and> M\<longrightarrow>\<^sub>aM') \<or> (\<exists>N'. R = AndR <a>.M <b>.N' c \<and> N\<longrightarrow>\<^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 \<longrightarrow>\<^sub>a R"
shows "\<exists>M'. R = AndL1 (x).M' y \<and> M\<longrightarrow>\<^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 \<longrightarrow>\<^sub>a R"
shows "\<exists>M'. R = AndL2 (x).M' y \<and> M\<longrightarrow>\<^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\<longrightarrow>\<^sub>a R"
shows "(\<exists>M'. R = OrL (x).M' (y).N z \<and> M\<longrightarrow>\<^sub>aM') \<or> (\<exists>N'. R = OrL (x).M (y).N' z \<and> N\<longrightarrow>\<^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 <a>.M b \<longrightarrow>\<^sub>a R"
shows "\<exists>M'. R = OrR1 <a>.M' b \<and> M\<longrightarrow>\<^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 <a>.M b \<longrightarrow>\<^sub>a R"
shows "\<exists>M'. R = OrR2 <a>.M' b \<and> M\<longrightarrow>\<^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 <a>.M (y).N z\<longrightarrow>\<^sub>a R"
shows "(\<exists>M'. R = ImpL <a>.M' (y).N z \<and> M\<longrightarrow>\<^sub>aM') \<or> (\<exists>N'. R = ImpL <a>.M (y).N' z \<and> N\<longrightarrow>\<^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).<a>.M b \<longrightarrow>\<^sub>a R"
shows "\<exists>M'. R = ImpR (x).<a>.M' b \<and> M\<longrightarrow>\<^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 "\<exists>c'::coname. c'\<sharp>(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 "\<exists>x'::name. x'\<sharp>(trm{x:=<b>.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)
--- 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\<turnstile>c>b] = AndR <c>.M <d>.N e" "c\<sharp>(a,b,d,e,N,R)" "d\<sharp>(a,b,c,e,M,R)" "e\<sharp>a"
shows "(\<exists>M' N'. R = AndR <c>.M' <d>.N' e \<and> M'[a\<turnstile>c>b] = M \<and> N'[a\<turnstile>c>b] = N \<and> c\<sharp>N' \<and> d\<sharp>M') \<or>
(\<exists>M' N'. R = AndR <c>.M' <d>.N' a \<and> b=e \<and> M'[a\<turnstile>c>b] = M \<and> N'[a\<turnstile>c>b] = N \<and> c\<sharp>N' \<and> d\<sharp>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\<turnstile>n>y] = OrL (v).M (w).N u" "v\<sharp>(R,N,u,x,y)" "w\<sharp>(R,M,u,x,y)" "x\<noteq>y"
shows "(\<exists>M' N'. (R = OrL (v).M' (w).N' u) \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N) \<or>
(\<exists>M' N'. (R = OrL (v).M' (w).N' x) \<and> y=u \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>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)]\<bullet>trm1" in exI)
@@ -1550,7 +1550,7 @@
assumes a: "R[x\<turnstile>n>y] = ImpL <c>.M (w).N u" "c\<sharp>(R,N)" "w\<sharp>(R,M,u,x,y)" "x\<noteq>y"
shows "(\<exists>M' N'. (R = ImpL <c>.M' (w).N' u) \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N) \<or>
(\<exists>M' N'. (R = ImpL <c>.M' (w).N' x) \<and> y=u \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>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)]\<bullet>trm1" in exI)
@@ -2367,7 +2367,7 @@
and a3: "(x):N \<in> (\<parallel>(B)\<parallel>)"
and a4: "SNa N"
shows "SNa (Cut <a>.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)
--- 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 @@
"(\<exists>r'. r \<rightarrow>\<^sub>\<beta> r' \<and> s = r' \<degree>\<degree> rs) \<or>
(\<exists>rs'. rs [\<rightarrow>\<^sub>\<beta>]\<^sub>1 rs' \<and> s = r \<degree>\<degree> rs') \<or>
(\<exists>t u us. x \<sharp> r \<longrightarrow> r = (Lam [x].t) \<and> rs = u # us \<and> s = t[x::=u] \<degree>\<degree> us)"
+ supply [[simproc del: defined_all]]
apply (nominal_induct u \<equiv> "r \<degree>\<degree> rs" s avoiding: x r rs rule: beta.strong_induct)
apply (simp add: App_eq_foldl_conv)
apply (split if_split_asm)
--- 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 \<Longrightarrow> A \<noteq> {} \<Longrightarrow>
fold_random_permutation f x A =
pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}))"
-by (force, simp_all)
+ by simp_all fastforce
termination proof (relation "Wellfounded.measure (\<lambda>(_,_,A). card A)")
fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b and y :: 'a
assume A: "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)"
@@ -126,7 +126,7 @@
| "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow>
fold_bind_random_permutation f g x A =
pmf_of_set A \<bind> (\<lambda>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 (\<lambda>(_,_,_,A). card A)")
fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b
and y :: 'a and g :: "'b \<Rightarrow> 'c pmf"
--- 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 \<Longrightarrow> L as vs \<Longrightarrow> 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 \<Longrightarrow> good vs \<Longrightarrow> 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 \<Longrightarrow> L as vs \<Longrightarrow> 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 \<Longrightarrow> good ws \<Longrightarrow> 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 \<Longrightarrow> ws \<noteq> [] \<Longrightarrow> T a ws zs"
+ supply [[simproc del: defined_all]]
apply (induct set: R)
apply iprover
apply (case_tac vs)
--- 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: "\<And>p. is_path r p 0 j k \<Longrightarrow> 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 \<Longrightarrow> is_path' r i ys k \<Longrightarrow>
--- 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 \<tturnstile> ts @ [t] : Ts \<Longrightarrow>
- (\<And>Us U. Ts = Us @ [U] \<Longrightarrow> e \<tturnstile> ts : Us \<Longrightarrow> e \<turnstile> t : U \<Longrightarrow> P) \<Longrightarrow> 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 \<open>e \<tturnstile> ts @ [t] : Ts\<close>
+ obtains Us and U where \<open>Ts = Us @ [U]\<close> \<open>e \<tturnstile> ts : Us\<close> \<open>e \<turnstile> t : U\<close>
+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 \<tturnstile> ts @ [t] : Us @ [U]" by simp
+ then have "e \<tturnstile> ts : Us" "e \<turnstile> t : U" by (simp_all add: types_snoc_eq)
+ with snoc show ?thesis by (rule that)
+qed
subsection \<open>n-ary function types\<close>
--- 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
--- 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
--- 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