enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
--- a/NEWS Wed Mar 12 22:57:50 2014 +0100
+++ b/NEWS Thu Mar 13 07:07:07 2014 +0100
@@ -98,6 +98,12 @@
*** HOL ***
+* Simplifier: Enhanced solver of preconditions of rewrite rules
+ can now deal with conjunctions.
+ For help with converting proofs, the old behaviour of the simplifier
+ can be restored like this: declare/using [[simp_legacy_precond]]
+ This configuration option will disappear again in the future.
+
* HOL-Word:
* Abandoned fact collection "word_arith_alts", which is a
duplicate of "word_arith_wis".
--- a/src/HOL/Auth/Guard/Guard_Yahalom.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy Thu Mar 13 07:07:07 2014 +0100
@@ -218,12 +218,12 @@
apply (rule Guard_extand, simp, blast)
apply (case_tac "NAa=NB", clarify)
apply (frule Says_imp_spies)
-apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
+apply (frule in_Guard_kparts_Crypt, simp+)
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
apply (drule ya2'_imp_ya1'_parts, simp, blast, blast)
apply (case_tac "NBa=NB", clarify)
apply (frule Says_imp_spies)
-apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
+apply (frule in_Guard_kparts_Crypt, simp+)
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
apply (drule NB_is_uniq_in_ya2', simp+, blast, simp+)
apply (simp add: No_Nonce, blast)
@@ -239,7 +239,7 @@
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Aa in ya3_shrK, simp)
apply (frule ya3'_imp_ya2', simp+, blast, clarify)
apply (frule_tac A=B' in Says_imp_spies)
-apply (rotate_tac -1, frule in_Guard_kparts_Crypt, simp+, blast, simp+)
+apply (rotate_tac -1, frule in_Guard_kparts_Crypt, simp+)
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
apply (drule NB_is_uniq_in_ya2', simp+, blast, clarify)
apply (drule ya3'_imp_ya3, simp+)
--- a/src/HOL/Auth/Public.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Auth/Public.thy Thu Mar 13 07:07:07 2014 +0100
@@ -414,7 +414,7 @@
(*Tactic for possibility theorems*)
fun possibility_tac ctxt =
REPEAT (*omit used_Says so that Nonces start from different traces!*)
- (ALLGOALS (simp_tac (ctxt delsimps [@{thm used_Says}]))
+ (ALLGOALS (simp_tac (ctxt setSolver safe_solver delsimps [@{thm used_Says}]))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac [refl, conjI, @{thm Nonce_supply}]))
--- a/src/HOL/Auth/ZhouGollmann.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Auth/ZhouGollmann.thy Thu Mar 13 07:07:07 2014 +0100
@@ -101,7 +101,7 @@
THEN zg.ZG2, THEN zg.Reception [of _ B A],
THEN zg.ZG3, THEN zg.Reception [of _ A TTP],
THEN zg.ZG4])
-apply (possibility, auto)
+apply (basic_possibility, auto)
done
subsection {*Basic Lemmas*}
--- a/src/HOL/Bali/Example.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Bali/Example.thy Thu Mar 13 07:07:07 2014 +0100
@@ -1280,8 +1280,6 @@
apply (rule conjI)
apply (rule eval_Is (* Init Object *))
apply (simp)
-apply (rule conjI, rule HOL.refl)+
-apply (rule HOL.refl)
apply (simp)
apply (rule conjI, rule_tac [2] HOL.refl)
apply (rule eval_Is (* Expr *))
--- a/src/HOL/Bali/Trans.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Bali/Trans.thy Thu Mar 13 07:07:07 2014 +0100
@@ -23,12 +23,7 @@
| (FVar) accC statDeclC stat a fn where "v={accC,statDeclC,stat}(Lit a)..fn"
| (AVar) a i where "v=(Lit a).[Lit i]"
using ground LVar FVar AVar
- apply (cases v)
- apply (simp add: groundVar_def)
- apply (simp add: groundVar_def,blast)
- apply (simp add: groundVar_def,blast)
- apply (simp add: groundVar_def)
- done
+ by (cases v) (auto simp add: groundVar_def)
definition
groundExprs :: "expr list \<Rightarrow> bool"
--- a/src/HOL/Decision_Procs/Approximation.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Mar 13 07:07:07 2014 +0100
@@ -2613,7 +2613,7 @@
and inequality: "u \<le> lx \<and> ux \<le> l'"
by (cases "approx prec x vs", auto,
cases "approx prec a vs", auto,
- cases "approx prec b vs", auto, blast)
+ cases "approx prec b vs", auto)
from inequality approx[OF AtLeastAtMost.prems(2) l_eq] approx[OF AtLeastAtMost.prems(2) u_eq] approx[OF AtLeastAtMost.prems(2) x_eq]
show ?case by auto
qed
@@ -2902,7 +2902,7 @@
(Mult (Inverse (Num (Float (int k) 0)))
(Mult (Add (Var (Suc (Suc 0))) (Minus (Num c)))
(Var (Suc 0))))) [Some (l1, u1), Some (l2, u2), vs!x]"
- by (auto elim!: lift_bin) blast
+ by (auto elim!: lift_bin)
from bnd_c `x < length xs`
have bnd: "bounded_by (xs[x:=c]) (vs[x:= Some (c,c)])"
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Mar 13 07:07:07 2014 +0100
@@ -473,7 +473,6 @@
then have ?case using 4
apply (cases "p +\<^sub>p p' = 0\<^sub>p")
apply (auto simp add: Let_def)
- apply blast
done
}
ultimately have ?case by blast
--- a/src/HOL/HOLCF/IOA/meta_theory/Seq.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Seq.thy Thu Mar 13 07:07:07 2014 +0100
@@ -5,7 +5,7 @@
header {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *}
theory Seq
-imports HOLCF
+imports "../../HOLCF"
begin
default_sort pcpo
--- a/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy Thu Mar 13 07:07:07 2014 +0100
@@ -99,7 +99,6 @@
apply (erule conjE)
apply (simp add: Let_def)
apply (rule_tac x = "ex" in someI)
-apply (erule conjE)
apply assumption
done
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Thu Mar 13 07:07:07 2014 +0100
@@ -196,10 +196,7 @@
apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
apply (tactic {* pair_tac @{context} "a" 1 *})
apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
-apply blast
-apply fastforce
apply (tactic {* pair_tac @{context} "a" 1 *})
- apply fastforce
done
end
--- a/src/HOL/HOLCF/Universal.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/HOLCF/Universal.thy Thu Mar 13 07:07:07 2014 +0100
@@ -111,12 +111,11 @@
"ubasis_until P 0 = 0"
| "finite S \<Longrightarrow> ubasis_until P (node i a S) =
(if P (node i a S) then node i a S else ubasis_until P a)"
- apply clarify
- apply (rule_tac x=b in node_cases)
- apply simp
+ apply clarify
+ apply (rule_tac x=b in node_cases)
apply simp
- apply fast
apply simp
+ apply fast
apply simp
apply simp
done
--- a/src/HOL/Hoare_Parallel/RG_Tran.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Tran.thy Thu Mar 13 07:07:07 2014 +0100
@@ -196,7 +196,6 @@
apply(erule_tac x="Some P2" in allE)
apply(erule allE,erule impE, assumption)
apply(drule div_seq,simp)
-apply force
apply clarify
apply(erule disjE)
apply clarify
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Mar 13 07:07:07 2014 +0100
@@ -918,7 +918,7 @@
from 3(7)[OF no_inter2] obtain rs where rs_def: "refs_of' h1 r1 rs" by (rule list_of'_refs_of')
from refs_of'_merge[OF refs_of'_pn qrs_def 3(6) no_inter this] p_in have p_rs: "p \<notin> set rs" by auto
with 3(7)[OF no_inter2] 3(1-5) 3(8) p_rs rs_def p_stays
- show ?case by auto
+ show ?case by (auto simp: list_of'_set_ref)
next
case (4 x xs' y ys' p q pn qn h1 r1 h')
from 4(1) obtain prs where prs_def: "refs_of' h p prs" by (rule list_of'_refs_of')
@@ -935,7 +935,7 @@
from 4(7)[OF no_inter2] obtain rs where rs_def: "refs_of' h1 r1 rs" by (rule list_of'_refs_of')
from refs_of'_merge[OF prs_def refs_of'_qn 4(6) no_inter this] q_in have q_rs: "q \<notin> set rs" by auto
with 4(7)[OF no_inter2] 4(1-5) 4(8) q_rs rs_def q_stays
- show ?case by auto
+ show ?case by (auto simp: list_of'_set_ref)
qed
section {* Code generation *}
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Thu Mar 13 07:07:07 2014 +0100
@@ -59,7 +59,7 @@
by hoare
lemma "\<turnstile> \<lbrace>True\<rbrace> \<acute>M := a; \<acute>N := b \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>"
- by hoare simp
+ by hoare
lemma
"\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Thu Mar 13 07:07:07 2014 +0100
@@ -204,7 +204,6 @@
apply auto
apply (case_tac xc)
apply auto
- apply fastforce
done
qed
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Thu Mar 13 07:07:07 2014 +0100
@@ -236,7 +236,7 @@
then obtain stk loc C sig pc frs' where
xcp [simp]: "xcp = None" and
frs [simp]: "frs = (stk,loc,C,sig,pc)#frs'"
- by (clarsimp simp add: neq_Nil_conv) fast
+ by (clarsimp simp add: neq_Nil_conv)
from conforms obtain ST LT rT maxs maxl ins et where
hconf: "G \<turnstile>h hp \<surd>" and
@@ -245,7 +245,7 @@
phi: "Phi C sig ! pc = Some (ST,LT)" and
frame: "correct_frame G hp (ST,LT) maxl ins (stk,loc,C,sig,pc)" and
frames: "correct_frames G hp Phi rT sig frs'"
- by (auto simp add: correct_state_def) (rule that)
+ by (auto simp add: correct_state_def)
from frame obtain
stk: "approx_stk G hp stk ST" and
@@ -354,7 +354,7 @@
obtain D fs where
hp: "hp (the_Addr x) = Some (D,fs)" and
D: "G \<turnstile> D \<preceq>C C"
- by - (drule non_npD, assumption, clarsimp, blast)
+ by - (drule non_npD, assumption, clarsimp)
hence "hp (the_Addr x) \<noteq> None" (is ?P1) by simp
moreover
from wf mth hp D
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Thu Mar 13 07:07:07 2014 +0100
@@ -889,7 +889,7 @@
loc: "hp ref = Some obj" and
obj_ty: "obj_ty obj = Class D" and
D: "G \<turnstile> Class D \<preceq> X"
- by (auto simp add: conf_def) blast
+ by (auto simp add: conf_def)
with X_Ref obtain X' where X': "X = Class X'"
by (blast dest: widen_Class)
@@ -1052,7 +1052,7 @@
meth'': "method (G, D) sig = Some (D'', rT'', body)" and
ST0': "ST' = rev apTs @ Class D # ST0'" and
len': "length apTs = length pt"
- by clarsimp blast
+ by clarsimp
from f frame'
obtain
@@ -1074,7 +1074,7 @@
methD': "method (G, D') sig = Some (mD, rT0, body')" and
lessD': "G \<turnstile> X \<preceq> Class D'" and
suc_pc': "Suc pc' < length ins'"
- by (clarsimp simp add: wt_instr_def eff_def norm_eff_def) blast
+ by (clarsimp simp add: wt_instr_def eff_def norm_eff_def)
from len len' ST0 ST0'
have "X = Class D" by simp
--- a/src/HOL/MicroJava/BV/EffectMono.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/BV/EffectMono.thy Thu Mar 13 07:07:07 2014 +0100
@@ -161,7 +161,7 @@
where s2: "s2 = (vT' # oT' # ST', LT')" and
oT': "G\<turnstile> oT' \<preceq> oT" and
vT': "G\<turnstile> vT' \<preceq> vT"
- by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp, rule that)
+ by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp)
moreover
from vT' vT
have "G \<turnstile> vT' \<preceq> b" by (rule widen_trans)
--- a/src/HOL/MicroJava/BV/JVMType.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy Thu Mar 13 07:07:07 2014 +0100
@@ -258,7 +258,7 @@
assume l: "length (l#ls) = length b"
then obtain b' bs where b: "b = b'#bs"
- by (cases b) (simp, simp add: neq_Nil_conv, rule that)
+ by (cases b) (simp, simp add: neq_Nil_conv)
with f
have "\<forall>n. n < length ls \<longrightarrow> (G \<turnstile> (ls!n) <=o (bs!n))"
--- a/src/HOL/MicroJava/Comp/CorrComp.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy Thu Mar 13 07:07:07 2014 +0100
@@ -523,7 +523,6 @@
apply (rule_tac ?instrs0.0 = "[load_default_val b]" in progression_transitive, simp)
apply (rule progression_one_step)
apply (simp (no_asm_simp) add: load_default_val_def)
-apply (rule conjI, simp)+ apply (rule HOL.refl)
apply (rule progression_one_step)
apply (simp (no_asm_simp))
@@ -816,7 +815,7 @@
apply (rule_tac ?instrs0.0 = "[Dup]" in progression_transitive, simp)
apply (rule progression_one_step)
apply (simp add: gh_def)
-apply (rule conjI, simp)+ apply simp
+apply simp
apply (rule progression_one_step)
apply (simp add: gh_def)
(* the following falls out of the general scheme *)
@@ -865,8 +864,6 @@
(* Dup_x1 *)
apply (rule progression_one_step)
apply (simp add: gh_def)
- apply (rule conjI, simp)+ apply simp
-
(* Putfield \<longrightarrow> still looks nasty*)
apply (rule progression_one_step)
@@ -948,7 +945,6 @@
apply simp
apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
apply (rule progression_one_step, simp)
-apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
apply fast
@@ -958,18 +954,17 @@
apply simp
apply (rule_tac ?instrs0.0 = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c1)))]" in progression_transitive, simp)
apply (rule progression_one_step) apply simp
-apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
apply (rule_tac ?instrs0.0 = "(compStmt (gmb G CL S) c1)" in progression_transitive, simp)
apply fast
apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
-apply (simp, rule conjI, (rule HOL.refl)+)
+apply (simp)
apply simp apply (rule conjI, simp) apply (simp add: nat_add_distrib)
apply (rule progression_refl)
(* case b= False *)
apply simp
apply (rule_tac ?instrs1.0 = "compStmt (gmb G CL S) c2" in jump_fwd_progression)
-apply (simp, rule conjI, (rule HOL.refl)+)
+apply (simp)
apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
apply fast
@@ -992,12 +987,11 @@
apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
apply (rule progression_one_step)
apply simp
- apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
apply fast
apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
-apply (simp, rule conjI, rule HOL.refl, rule HOL.refl)
+apply (simp)
apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
apply (rule progression_refl)
@@ -1022,12 +1016,10 @@
apply simp
apply (rule jump_bwd_progression)
apply simp
-apply (rule conjI, (rule HOL.refl)+)
apply (rule_tac ?instrs0.0 = "[LitPush (Bool False)]" in progression_transitive, simp (no_asm_simp))
apply (rule progression_one_step)
apply simp
- apply (rule conjI, simp)+ apply simp
apply (rule_tac ?instrs0.0 = "compExpr (gmb G CL S) e" in progression_transitive, rule HOL.refl)
apply fast
@@ -1038,7 +1030,6 @@
apply (rule_tac ?instrs0.0 = "[Ifcmpeq (2 + int (length (compStmt (gmb G CL S) c)))]" in progression_transitive, simp)
apply (rule progression_one_step) apply simp
-apply (rule conjI, rule HOL.refl)+ apply (rule HOL.refl)
apply fast
(* case b= False \<longrightarrow> contradiction*)
@@ -1126,7 +1117,6 @@
apply (simp (no_asm_use) only: exec_instr.simps)
apply (erule thin_rl, erule thin_rl, erule thin_rl)
apply (simp add: compMethod_def raise_system_xcpt_def)
-apply (rule conjI, simp)+ apply (rule HOL.refl)
(* get instructions of invoked method *)
apply (simp (no_asm_simp) add: gis_def gmb_def compMethod_def)
@@ -1177,7 +1167,6 @@
apply (frule non_npD) apply assumption
apply (erule exE)+ apply simp
apply (rule conf_obj_AddrI) apply simp
-apply (rule conjI, (rule HOL.refl)+)
apply (rule widen_Class_Class [THEN iffD1], rule widen.refl)
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Mar 13 07:07:07 2014 +0100
@@ -1268,7 +1268,6 @@
apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
apply (rule exI)+
apply (simp add: wf_prog_ws_prog [THEN comp_method])
- apply auto
done
@@ -2517,16 +2516,13 @@
(start_ST, start_LT C pTs (length lvars))))
= (start_ST, inited_LT C pTs lvars)")
prefer 2 apply (rule compTpInitLvars_LT_ST) apply (rule HOL.refl) apply assumption
-apply (simp only:)
apply (subgoal_tac "(snd (compTpStmt (pns, lvars, blk, res) G blk
(start_ST, inited_LT C pTs lvars)))
= (start_ST, inited_LT C pTs lvars)")
prefer 2 apply (erule conjE)+
apply (rule compTpStmt_LT_ST) apply (rule HOL.refl) apply assumption+
apply (simp only:)+ apply (simp (no_asm_simp) add: is_inited_LT_def)
-apply (simp only:)
-apply (rule compTpExpr_LT_ST) apply (rule HOL.refl) apply assumption+
- apply (simp only:)+ apply (simp (no_asm_simp) add: is_inited_LT_def)
+ apply (simp (no_asm_simp) add: is_inited_LT_def)
(* Return *)
--- a/src/HOL/MicroJava/J/Eval.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy Thu Mar 13 07:07:07 2014 +0100
@@ -226,7 +226,7 @@
next
case (Call a b c d e f g h i j k l m n o p q r s t u v s4)
with Call_code show ?thesis
- by(cases "s4")(simp, (erule meta_allE meta_impE|rule conjI refl| assumption)+)
+ by(cases "s4") auto
qed(erule (3) that[OF refl]|assumption)+
next
case evals
--- a/src/HOL/MicroJava/J/WellForm.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy Thu Mar 13 07:07:07 2014 +0100
@@ -565,7 +565,7 @@
apply clarify
apply (frule wf_prog_ws_prog)
apply (frule fields_Object, assumption+)
-apply (simp only: is_class_Object) apply simp
+apply (simp only: is_class_Object)
apply clarify
apply (frule fields_rec)
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Mar 13 07:07:07 2014 +0100
@@ -2958,10 +2958,10 @@
fix f
assume *: "Ball f open" "s \<union> t \<subseteq> \<Union>f"
from * `compact s` obtain s' where "s' \<subseteq> f \<and> finite s' \<and> s \<subseteq> \<Union>s'"
- unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis
+ unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f])
moreover
from * `compact t` obtain t' where "t' \<subseteq> f \<and> finite t' \<and> t \<subseteq> \<Union>t'"
- unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis
+ unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f])
ultimately show "\<exists>f'\<subseteq>f. finite f' \<and> s \<union> t \<subseteq> \<Union>f'"
by (auto intro!: exI[of _ "s' \<union> t'"])
qed
--- a/src/HOL/Nominal/Examples/Class1.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Nominal/Examples/Class1.thy Thu Mar 13 07:07:07 2014 +0100
@@ -1702,32 +1702,13 @@
next
case (NotR y M d)
then show ?case
- apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
- apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{d:=(x).N},([(c,d)]\<bullet>M){c:=(x).N})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_NotR)
- apply(simp add: trm.inject alpha)
- apply(rule exists_fresh'(2)[OF fs_coname1])
- done
+ by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
next
case (AndR c1 M c2 M' c3)
then show ?case
- apply(simp)
- apply(auto)
- apply(simp add: fresh_prod calc_atm fresh_atm abs_fresh)
- apply(simp add: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
- apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{c3:=(x).N},
- M'{c3:=(x).N},c1,c2,c3,([(c,c3)]\<bullet>M){c:=(x).N},([(c,c3)]\<bullet>M'){c:=(x).N})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_AndR)
- apply (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh subst_fresh)
- apply(rule exists_fresh'(2)[OF fs_coname1])
- apply(simp add: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
- apply(simp add: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
- apply(auto simp add: trm.inject alpha)
- done
+ apply(auto simp add: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
+ apply (metis (erased, hide_lams))
+ by metis
next
case AndL1
then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
@@ -1737,25 +1718,11 @@
next
case (OrR1 d M e)
then show ?case
- apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
- apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{e:=(x).N},([(c,e)]\<bullet>M){c:=(x).N},d,e)")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_OrR1)
- apply(simp add: trm.inject alpha)
- apply(rule exists_fresh'(2)[OF fs_coname1])
- done
+ by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
next
case (OrR2 d M e)
then show ?case
- apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
- apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{e:=(x).N},([(c,e)]\<bullet>M){c:=(x).N},d,e)")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_OrR2)
- apply(simp add: trm.inject alpha)
- apply(rule exists_fresh'(2)[OF fs_coname1])
- done
+ by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
next
case (OrL x1 M x2 M' x3)
then show ?case
@@ -1764,24 +1731,16 @@
case ImpL
then show ?case
by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+ metis
next
case (ImpR y d M e)
then show ?case
- apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
- apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{e:=(x).N},([(c,e)]\<bullet>M){c:=(x).N},d,e)")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_ImpR)
- apply(simp add: trm.inject alpha)
- apply(rule exists_fresh'(2)[OF fs_coname1])
- done
+ by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
next
case (Cut d M y M')
then show ?case
- apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
- apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
- apply(simp add: calc_atm)
- done
+ by(simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+ (metis crename.simps(1) crename_id crename_rename)
qed
lemma substc_rename2:
@@ -1885,14 +1844,7 @@
next
case (NotL d M z)
then show ?case
- apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
- apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(N,M{x:=<a>.N},([(y,x)]\<bullet>M){y:=<a>.N})")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_NotL)
- apply(simp add: trm.inject alpha)
- apply(rule exists_fresh'(1)[OF fs_name1])
- done
+ by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
next
case (AndR c1 M c2 M' c3)
then show ?case
@@ -1906,37 +1858,16 @@
next
case (AndL1 u M v)
then show ?case
- apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
- apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(N,M{x:=<a>.N},([(y,x)]\<bullet>M){y:=<a>.N},u,v)")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_AndL1)
- apply(simp add: trm.inject alpha)
- apply(rule exists_fresh'(1)[OF fs_name1])
- done
+ by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
next
case (AndL2 u M v)
then show ?case
- apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
- apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(N,M{x:=<a>.N},([(y,x)]\<bullet>M){y:=<a>.N},u,v)")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_AndL2)
- apply(simp add: trm.inject alpha)
- apply(rule exists_fresh'(1)[OF fs_name1])
- done
+ by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
next
case (OrL x1 M x2 M' x3)
then show ?case
- apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
- apply(subgoal_tac
- "\<exists>a'::name. a'\<sharp>(N,M{x:=<a>.N},M'{x:=<a>.N},([(y,x)]\<bullet>M){y:=<a>.N},([(y,x)]\<bullet>M'){y:=<a>.N},x1,x2)")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_OrL)
- apply(simp add: trm.inject alpha)
- apply(rule exists_fresh'(1)[OF fs_name1])
- done
+ by(simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+ (metis (poly_guards_query))
next
case ImpR
then show ?case
@@ -1944,21 +1875,15 @@
next
case (ImpL d M v M' u)
then show ?case
- apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
- apply(subgoal_tac
- "\<exists>a'::name. a'\<sharp>(N,M{u:=<a>.N},M'{u:=<a>.N},([(y,u)]\<bullet>M){y:=<a>.N},([(y,u)]\<bullet>M'){y:=<a>.N},d,v)")
- apply(erule exE, simp add: fresh_prod)
- apply(erule conjE)+
- apply(simp add: fresh_fun_simp_ImpL)
- apply(simp add: trm.inject alpha)
- apply(rule exists_fresh'(1)[OF fs_name1])
- done
+ by(simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+ (metis (poly_guards_query))
next
case (Cut d M y M')
then show ?case
apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm)
+ apply metis
done
qed
--- a/src/HOL/Nominal/Examples/Class2.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Nominal/Examples/Class2.thy Thu Mar 13 07:07:07 2014 +0100
@@ -2869,15 +2869,9 @@
apply(rotate_tac 10)
apply(drule_tac x="a" in meta_spec)
apply(auto simp add: ty.inject)
-apply(blast)
-apply(blast)
-apply(blast)
apply(rotate_tac 10)
apply(drule_tac x="a" in meta_spec)
apply(auto simp add: ty.inject)
-apply(blast)
-apply(blast)
-apply(blast)
done
termination
--- a/src/HOL/Old_Number_Theory/Pocklington.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy Thu Mar 13 07:07:07 2014 +0100
@@ -615,7 +615,7 @@
from x(3)[rule_format, of z] z(2,3) have "z=x"
unfolding modeq_def mod_less[OF y(2)] by simp}
with xm x(1,2) have "\<exists>!x. x \<in> ?S \<and> (?h \<circ> op * a) x = y"
- unfolding modeq_def mod_less[OF y(2)] by auto }
+ unfolding modeq_def mod_less[OF y(2)] by safe auto }
thus "\<forall>y\<in>{m. coprime m n \<and> m < n}.
\<exists>!x. x \<in> {m. coprime m n \<and> m < n} \<and> ((\<lambda>m. m mod n) \<circ> op * a) x = y" by blast
next
--- a/src/HOL/Proofs/Lambda/LambdaType.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Proofs/Lambda/LambdaType.thy Thu Mar 13 07:07:07 2014 +0100
@@ -130,10 +130,6 @@
apply (case_tac ys)
apply simp
apply simp
- apply atomize
- apply (erule allE)+
- apply (erule mp, rule conjI)
- apply (rule refl)+
done
lemma types_snocE: "e \<tturnstile> ts @ [t] : Ts \<Longrightarrow>
@@ -142,7 +138,6 @@
apply simp
apply (case_tac "ts @ [t]")
apply (simp add: types_snoc_eq)+
- apply iprover
done
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Thu Mar 13 07:07:07 2014 +0100
@@ -93,7 +93,7 @@
next
case (Cons a as)
with argsT obtain T'' Ts where Us: "Us = T'' # Ts"
- by (cases Us) (rule FalseE, simp+, erule that)
+ by (cases Us) (rule FalseE, simp)
from varT and Us have varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
by simp
from varT eq have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'" by cases auto
--- a/src/HOL/Quotient.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Quotient.thy Thu Mar 13 07:07:07 2014 +0100
@@ -487,15 +487,7 @@
lemma bex1_bexeq_reg:
shows "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
- apply (simp add: Ex1_def Bex1_rel_def in_respects)
- apply clarify
- apply auto
- apply (rule bexI)
- apply assumption
- apply (simp add: in_respects)
- apply (simp add: in_respects)
- apply auto
- done
+ by (auto simp add: Ex1_def Bex1_rel_def Bex_def Ball_def in_respects)
lemma bex1_bexeq_reg_eqv:
assumes a: "equivp R"
--- a/src/HOL/Tools/simpdata.ML Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Tools/simpdata.ML Thu Mar 13 07:07:07 2014 +0100
@@ -109,10 +109,21 @@
fun mksimps pairs (_: Proof.context) =
map_filter (try mk_eq) o mk_atomize pairs o gen_all;
+val simp_legacy_precond =
+ Attrib.setup_config_bool @{binding "simp_legacy_precond"} (K false)
+
fun unsafe_solver_tac ctxt =
- (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
- FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt),
- atac, etac @{thm FalseE}];
+ let
+ val intros =
+ if Config.get ctxt simp_legacy_precond then [] else [@{thm conjI}]
+ val sol_thms =
+ reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt;
+ fun sol_tac i =
+ FIRST [resolve_tac sol_thms i, atac i , etac @{thm FalseE} i] ORELSE
+ (match_tac intros THEN_ALL_NEW sol_tac) i
+ in
+ (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' sol_tac
+ end;
val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
--- a/src/HOL/Word/Bool_List_Representation.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy Thu Mar 13 07:07:07 2014 +0100
@@ -941,7 +941,6 @@
apply (subst bin_rsplit_aux.simps)
apply (subst bin_rsplit_aux.simps)
apply (clarsimp split: prod.split)
- apply auto
done
lemma bin_rsplitl_aux_append:
@@ -950,7 +949,6 @@
apply (subst bin_rsplitl_aux.simps)
apply (subst bin_rsplitl_aux.simps)
apply (clarsimp split: prod.split)
- apply auto
done
lemmas rsplit_aux_apps [where bs = "[]"] =
--- a/src/HOL/ZF/HOLZF.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/ZF/HOLZF.thy Thu Mar 13 07:07:07 2014 +0100
@@ -261,7 +261,7 @@
apply (frule Elem_Elem_PFun[where p=y], simp)
apply (subgoal_tac "isFun F")
apply (simp add: isFun_def isOpair_def)
- apply (auto simp add: Fst Snd, blast)
+ apply (auto simp add: Fst Snd)
apply (auto simp add: PFun_def Sep)
done