--- a/src/HOL/Algebra/Divisibility.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Mon Sep 12 07:55:43 2011 +0200
@@ -650,7 +650,7 @@
finally have linv: "\<one> = c \<otimes> b" .
from ccarr linv[symmetric] rinv[symmetric]
- have "b \<in> Units G" unfolding Units_def by fastsimp
+ have "b \<in> Units G" unfolding Units_def by fastforce
with nunit
show "False" ..
qed
@@ -710,8 +710,8 @@
fixes G (structure)
shows "properfactor G = lless (division_rel G)"
apply (rule ext) apply (rule ext) apply rule
- apply (fastsimp elim: properfactorE2 intro: weak_llessI)
-apply (fastsimp elim: weak_llessE intro: properfactorI2)
+ apply (fastforce elim: properfactorE2 intro: weak_llessI)
+apply (fastforce elim: weak_llessE intro: properfactorI2)
done
lemma (in monoid) properfactor_cong_l [trans]:
@@ -751,26 +751,26 @@
and carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G"
shows "properfactor G (c \<otimes> a) (c \<otimes> b)"
using ab carr
-by (fastsimp elim: properfactorE intro: properfactorI)
+by (fastforce elim: properfactorE intro: properfactorI)
lemma (in monoid_cancel) properfactor_mult_l [simp]:
assumes carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G"
shows "properfactor G (c \<otimes> a) (c \<otimes> b) = properfactor G a b"
using carr
-by (fastsimp elim: properfactorE intro: properfactorI)
+by (fastforce elim: properfactorE intro: properfactorI)
lemma (in comm_monoid_cancel) properfactor_mult_rI [intro]:
assumes ab: "properfactor G a b"
and carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G"
shows "properfactor G (a \<otimes> c) (b \<otimes> c)"
using ab carr
-by (fastsimp elim: properfactorE intro: properfactorI)
+by (fastforce elim: properfactorE intro: properfactorI)
lemma (in comm_monoid_cancel) properfactor_mult_r [simp]:
assumes carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G"
shows "properfactor G (a \<otimes> c) (b \<otimes> c) = properfactor G a b"
using carr
-by (fastsimp elim: properfactorE intro: properfactorI)
+by (fastforce elim: properfactorE intro: properfactorI)
lemma (in monoid) properfactor_prod_r:
assumes ab: "properfactor G a b"
@@ -1811,7 +1811,7 @@
assumes "x \<in> carrier G"
shows "x \<in> assocs G x"
using assms
-by (fastsimp intro: closure_ofI2)
+by (fastforce intro: closure_ofI2)
lemma (in monoid) assocs_repr_independenceD:
assumes repr: "assocs G x = assocs G y"
@@ -2007,7 +2007,7 @@
from tm as'carr[THEN subsetD] bscarr[THEN subsetD]
have "as' [\<sim>] bs"
- by (induct as' arbitrary: bs) (simp, fastsimp dest: assocs_eqD[THEN associated_sym])
+ by (induct as' arbitrary: bs) (simp, fastforce dest: assocs_eqD[THEN associated_sym])
from tp and this
show "essentially_equal G as bs" by (fast intro: essentially_equalI)
@@ -3451,7 +3451,7 @@
by (intro ih[of a']) simp
hence ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
- apply (elim essentially_equalE) apply (fastsimp intro: essentially_equalI)
+ apply (elim essentially_equalE) apply (fastforce intro: essentially_equalI)
done
from carr
--- a/src/HOL/Algebra/FiniteProduct.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy Mon Sep 12 07:55:43 2011 +0200
@@ -171,7 +171,7 @@
(EX y. (A, y) \<in> foldSetD D f e & v = f x y)"
apply auto
apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE])
- apply (fastsimp dest: foldSetD_imp_finite)
+ apply (fastforce dest: foldSetD_imp_finite)
apply assumption
apply assumption
apply (blast intro: foldSetD_determ)
@@ -328,7 +328,7 @@
apply fast
apply fast
apply assumption
- apply (fastsimp intro: m_closed)
+ apply (fastforce intro: m_closed)
apply simp+
apply fast
apply (auto simp add: finprod_def)
@@ -431,13 +431,13 @@
next
assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
"g \<in> insert x B \<rightarrow> carrier G"
- thus "f \<in> B -> carrier G" by fastsimp
+ thus "f \<in> B -> carrier G" by fastforce
next
assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
"g \<in> insert x B \<rightarrow> carrier G"
- thus "f x \<in> carrier G" by fastsimp
+ thus "f x \<in> carrier G" by fastforce
qed
- also from insert have "... = g x \<otimes> finprod G g B" by fastsimp
+ also from insert have "... = g x \<otimes> finprod G g B" by fastforce
also from insert have "... = finprod G g (insert x B)"
by (intro finprod_insert [THEN sym]) auto
finally show ?case .
--- a/src/HOL/Algebra/Group.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Algebra/Group.thy Mon Sep 12 07:55:43 2011 +0200
@@ -549,7 +549,7 @@
lemma (in group) hom_compose:
"[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
-by (fastsimp simp add: hom_def compose_def)
+by (fastforce simp add: hom_def compose_def)
definition
iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60)
@@ -781,7 +781,7 @@
fix A
assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
then have Int_subgroup: "subgroup (\<Inter>A) G"
- by (fastsimp intro: subgroups_Inter)
+ by (fastforce intro: subgroups_Inter)
show "\<exists>I. greatest ?L I (Lower ?L A)"
proof
show "greatest ?L (\<Inter>A) (Lower ?L A)"
@@ -794,13 +794,13 @@
by (rule subgroup_imp_group)
from groupH have monoidH: "monoid ?H"
by (rule group.is_monoid)
- from H have Int_subset: "?Int \<subseteq> H" by fastsimp
+ from H have Int_subset: "?Int \<subseteq> H" by fastforce
then show "le ?L ?Int H" by simp
next
fix H
assume H: "H \<in> Lower ?L A"
with L Int_subgroup show "le ?L H ?Int"
- by (fastsimp simp: Lower_def intro: Inter_greatest)
+ by (fastforce simp: Lower_def intro: Inter_greatest)
next
show "A \<subseteq> carrier ?L" by (rule L)
next
--- a/src/HOL/Algebra/Lattice.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Algebra/Lattice.thy Mon Sep 12 07:55:43 2011 +0200
@@ -644,7 +644,7 @@
show "x \<squnion> (y \<squnion> z) .= s"
proof (rule weak_le_antisym)
from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
- by (fastsimp intro!: join_le elim: least_Upper_above)
+ by (fastforce intro!: join_le elim: least_Upper_above)
next
from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
by (erule_tac least_le)
@@ -885,7 +885,7 @@
show "x \<sqinter> (y \<sqinter> z) .= i"
proof (rule weak_le_antisym)
from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
- by (fastsimp intro!: meet_le elim: greatest_Lower_below)
+ by (fastforce intro!: meet_le elim: greatest_Lower_below)
next
from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
by (erule_tac greatest_le)
@@ -1289,7 +1289,7 @@
show "EX s. least ?L s (Upper ?L B)"
proof
from B show "least ?L (\<Union> B) (Upper ?L B)"
- by (fastsimp intro!: least_UpperI simp: Upper_def)
+ by (fastforce intro!: least_UpperI simp: Upper_def)
qed
next
fix B
@@ -1299,7 +1299,7 @@
from B show "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
@{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
- by (fastsimp intro!: greatest_LowerI simp: Lower_def)
+ by (fastforce intro!: greatest_LowerI simp: Lower_def)
qed
qed
--- a/src/HOL/Algebra/UnivPoly.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Mon Sep 12 07:55:43 2011 +0200
@@ -105,7 +105,7 @@
proof
fix i
assume "max n m < i"
- with boundn and boundm and UP show "p i \<oplus> q i = \<zero>" by fastsimp
+ with boundn and boundm and UP show "p i \<oplus> q i = \<zero>" by fastforce
qed
then show ?thesis ..
qed
@@ -780,7 +780,7 @@
then have "EX m. deg R p <= m & coeff P p m ~= \<zero>" by (simp add: deg minus)
then show ?thesis by (auto intro: that)
qed
- with deg_belowI R have "deg R p = m" by fastsimp
+ with deg_belowI R have "deg R p = m" by fastforce
with m_coeff show ?thesis by simp
qed
@@ -827,7 +827,7 @@
lemma deg_monom [simp]:
"[| a ~= \<zero>; a \<in> carrier R |] ==> deg R (monom P a n) = n"
- by (fastsimp intro: le_antisym deg_aboveI deg_belowI)
+ by (fastforce intro: le_antisym deg_aboveI deg_belowI)
lemma deg_const [simp]:
assumes R: "a \<in> carrier R" shows "deg R (monom P a 0) = 0"
@@ -1061,7 +1061,7 @@
finally have "coeff P p 0 \<otimes> coeff P q 0 = \<zero>" .
with R have "coeff P p 0 = \<zero> | coeff P q 0 = \<zero>"
by (simp add: R.integral_iff)
- with p q show "p = \<zero>\<^bsub>P\<^esub> | q = \<zero>\<^bsub>P\<^esub>" by fastsimp
+ with p q show "p = \<zero>\<^bsub>P\<^esub> | q = \<zero>\<^bsub>P\<^esub>" by fastforce
qed
qed
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Mon Sep 12 07:55:43 2011 +0200
@@ -209,7 +209,7 @@
fix i
assume "max n m < i"
with boundn and boundm show "f i + g i = 0"
- by (fastsimp simp add: algebra_simps)
+ by (fastforce simp add: algebra_simps)
qed
then show "(%i. (f i + g i)) : UP"
by (unfold UP_def) fast
@@ -516,7 +516,7 @@
then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus)
then show ?thesis by (auto intro: that)
qed
- with deg_belowI have "deg p = m" by fastsimp
+ with deg_belowI have "deg p = m" by fastforce
with m_coeff show ?thesis by simp
qed
@@ -564,7 +564,7 @@
lemma deg_monom [simp]:
"a ~= 0 ==> deg (monom a n::'a::ring up) = n"
-by (fastsimp intro: le_antisym deg_aboveI deg_belowI)
+by (fastforce intro: le_antisym deg_aboveI deg_belowI)
lemma deg_const [simp]:
"deg (monom (a::'a::ring) 0) = 0"
@@ -769,7 +769,7 @@
also from pq have "... = 0" by simp
finally have "coeff p 0 * coeff q 0 = 0" .
then have "coeff p 0 = 0 | coeff q 0 = 0" by (simp only: integral_iff)
- with p q show "p = 0 | q = 0" by fastsimp
+ with p q show "p = 0 | q = 0" by fastforce
qed
qed
--- a/src/HOL/Auth/Guard/Extensions.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Auth/Guard/Extensions.thy Mon Sep 12 07:55:43 2011 +0200
@@ -198,7 +198,7 @@
lemma parts_invKey [rule_format,dest]:"X:parts {Y} ==>
X:analz (insert (Crypt K Y) H) --> X ~:analz H --> Key (invKey K):analz H"
-by (erule parts.induct, (fastsimp dest: parts.Fst parts.Snd parts.Body)+)
+by (erule parts.induct, (fastforce dest: parts.Fst parts.Snd parts.Body)+)
lemma in_analz: "Y:analz H ==> EX X. X:H & Y:parts {X}"
by (erule analz.induct, auto intro: parts.Fst parts.Snd parts.Body)
--- a/src/HOL/Auth/Kerberos_BAN_Gets.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy Mon Sep 12 07:55:43 2011 +0200
@@ -288,7 +288,7 @@
apply (blast dest: used_evs_rev [THEN equalityD2, THEN contra_subsetD]
used_takeWhile_used)
txt{*subcase: CT before*}
-apply (fastsimp dest!: set_evs_rev [THEN equalityD2, THEN contra_subsetD, THEN takeWhile_void])
+apply (fastforce dest!: set_evs_rev [THEN equalityD2, THEN contra_subsetD, THEN takeWhile_void])
done
--- a/src/HOL/Auth/OtwayReesBella.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Auth/OtwayReesBella.thy Mon Sep 12 07:55:43 2011 +0200
@@ -277,7 +277,7 @@
apply disentangle
apply (drule_tac [5] Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN analz.Snd])
prefer 8 apply clarify
-apply (analz_freshCryptK, spy_analz, fastsimp)
+apply (analz_freshCryptK, spy_analz, fastforce)
done
@@ -365,7 +365,7 @@
apply (drule Gets_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd], assumption)
apply (drule analz_hard, assumption, assumption, assumption, assumption)
apply (drule OR4_imp_Gets, assumption, assumption)
-apply (fastsimp dest!: Gets_imp_knows [THEN analz.Inj] analz.Decrypt)
+apply (fastforce dest!: Gets_imp_knows [THEN analz.Inj] analz.Decrypt)
done
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Mon Sep 12 07:55:43 2011 +0200
@@ -605,7 +605,7 @@
\<in> set evs;
evs \<in> sr \<rbrakk> \<Longrightarrow> A=A'"
apply (erule rev_mp, erule rev_mp, erule sr.induct, simp_all)
-apply (fastsimp dest: Outpts_parts_used)
+apply (fastforce dest: Outpts_parts_used)
apply blast
done
@@ -615,7 +615,7 @@
Outpts (Card B') B' \<lbrace>Nonce Nb, Key SK', Cert1', Cert2'\<rbrace> \<in> set evs;
evs \<in> sr \<rbrakk> \<Longrightarrow> B=B' \<and> SK=SK' \<and> Cert1=Cert1' \<and> Cert2=Cert2'"
apply (erule rev_mp, erule rev_mp, erule sr.induct, simp_all)
-apply (fastsimp dest: Outpts_parts_used)
+apply (fastforce dest: Outpts_parts_used)
apply blast
done
@@ -626,7 +626,7 @@
Outpts (Card B') B' \<lbrace>Nonce Nb', Key SK, Cert1', Cert2'\<rbrace> \<in> set evs;
evs \<in> sr \<rbrakk> \<Longrightarrow> B=B' \<and> Nb=Nb' \<and> Cert1=Cert1' \<and> Cert2=Cert2'"
apply (erule rev_mp, erule rev_mp, erule sr.induct, simp_all)
-apply (fastsimp dest: Outpts_parts_used)
+apply (fastforce dest: Outpts_parts_used)
apply blast
done
@@ -644,9 +644,9 @@
"\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, rest\<rbrace> \<in> set evs; evs \<in> sr \<rbrakk>
\<Longrightarrow> Unique (Outpts (Card A) A \<lbrace>Nonce Na, rest\<rbrace>) on evs"
apply (erule rev_mp, erule sr.induct, simp_all add: Unique_def)
-apply (fastsimp dest: Outpts_parts_used)
+apply (fastforce dest: Outpts_parts_used)
apply blast
-apply (fastsimp dest: Outpts_parts_used)
+apply (fastforce dest: Outpts_parts_used)
apply blast
done
@@ -699,7 +699,7 @@
evs \<in> sr \<rbrakk>
\<Longrightarrow> Nonce (Pairkey(A,B)) \<in> analz (knows Spy evs)"
apply (case_tac "A = Spy")
-apply (fastsimp dest!: Inputs_imp_knows_Spy_secureM [THEN analz.Inj])
+apply (fastforce dest!: Inputs_imp_knows_Spy_secureM [THEN analz.Inj])
apply (blast dest!: Pairkey_Inputs_imp_Gets [THEN Pairkey_Gets_analz_knows_Spy])
done
@@ -977,7 +977,7 @@
(*fake*)
apply spy_analz
(*forge*)
-apply (fastsimp dest: analz.Inj)
+apply (fastforce dest: analz.Inj)
(*SR7: used B\<noteq>Spy*)
(*SR7F*)
apply clarify
@@ -1028,7 +1028,7 @@
(*Forge*)
apply (rotate_tac 7)
apply (drule parts.Inj)
-apply (fastsimp dest: Outpts_B_Card_form_7)
+apply (fastforce dest: Outpts_B_Card_form_7)
(*SR7*)
apply (blast dest!: Outpts_B_Card_form_7)
(*SR7F*)
@@ -1036,10 +1036,10 @@
apply (drule Outpts_parts_used)
apply simp
(*faster than
- apply (fastsimp dest: Outpts_parts_used)
+ apply (fastforce dest: Outpts_parts_used)
*)
(*SR10*)
-apply (fastsimp dest: Outpts_B_Card_form_7)
+apply (fastforce dest: Outpts_B_Card_form_7)
(*SR10F - uses assumption Card A not cloned*)
apply clarify
apply (drule Outpts_B_Card_form_7, assumption)
@@ -1346,7 +1346,7 @@
Outpts (Card B) B \<lbrace>Nonce Nb, Key K, Certificate, Cert2\<rbrace> \<in> set evs"
apply (erule rev_mp)
apply (erule sr.induct)
-prefer 18 apply (fastsimp dest: Outpts_A_Card_form_10)
+prefer 18 apply (fastforce dest: Outpts_A_Card_form_10)
apply auto
done
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Mon Sep 12 07:55:43 2011 +0200
@@ -614,7 +614,7 @@
\<in> set evs;
evs \<in> srb \<rbrakk> \<Longrightarrow> A=A'"
apply (erule rev_mp, erule rev_mp, erule srb.induct, simp_all)
-apply (fastsimp dest: Outpts_parts_used)
+apply (fastforce dest: Outpts_parts_used)
apply blast
done
@@ -624,7 +624,7 @@
Outpts (Card B') B' \<lbrace>Nonce Nb, Agent A', Key SK', Cert1', Cert2'\<rbrace> \<in> set evs;
evs \<in> srb \<rbrakk> \<Longrightarrow> B=B' \<and> A=A' \<and> SK=SK' \<and> Cert1=Cert1' \<and> Cert2=Cert2'"
apply (erule rev_mp, erule rev_mp, erule srb.induct, simp_all)
-apply (fastsimp dest: Outpts_parts_used)
+apply (fastforce dest: Outpts_parts_used)
apply blast
done
@@ -635,7 +635,7 @@
Outpts (Card B') B' \<lbrace>Nonce Nb', Agent A', Key SK, Cert1', Cert2'\<rbrace> \<in> set evs;
evs \<in> srb \<rbrakk> \<Longrightarrow> B=B' \<and> A=A' \<and> Nb=Nb' \<and> Cert1=Cert1' \<and> Cert2=Cert2'"
apply (erule rev_mp, erule rev_mp, erule srb.induct, simp_all)
-apply (fastsimp dest: Outpts_parts_used)
+apply (fastforce dest: Outpts_parts_used)
apply blast
done
@@ -654,9 +654,9 @@
"\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, rest\<rbrace> \<in> set evs; evs \<in> srb \<rbrakk>
\<Longrightarrow> Unique (Outpts (Card A) A \<lbrace>Nonce Na, rest\<rbrace>) on evs"
apply (erule rev_mp, erule srb.induct, simp_all add: Unique_def)
-apply (fastsimp dest: Outpts_parts_used)
+apply (fastforce dest: Outpts_parts_used)
apply blast
-apply (fastsimp dest: Outpts_parts_used)
+apply (fastforce dest: Outpts_parts_used)
apply blast
done
@@ -709,7 +709,7 @@
evs \<in> srb \<rbrakk>
\<Longrightarrow> Nonce (Pairkey(A,B)) \<in> analz (knows Spy evs)"
apply (case_tac "A = Spy")
-apply (fastsimp dest!: Inputs_imp_knows_Spy_secureM [THEN analz.Inj])
+apply (fastforce dest!: Inputs_imp_knows_Spy_secureM [THEN analz.Inj])
apply (blast dest!: Pairkey_Inputs_imp_Gets [THEN Pairkey_Gets_analz_knows_Spy])
done
@@ -978,7 +978,7 @@
(*fake*)
apply spy_analz
(*forge*)
-apply (fastsimp dest: analz.Inj)
+apply (fastforce dest: analz.Inj)
(*SR_U7: used B\<noteq>Spy*)
(*SR_U7F*)
apply clarify
@@ -1018,7 +1018,7 @@
(*Forge*)
apply (rotate_tac 7)
apply (drule parts.Inj)
-apply (fastsimp dest: Outpts_B_Card_form_7)
+apply (fastforce dest: Outpts_B_Card_form_7)
(*SR_U7*)
apply (blast dest!: Outpts_B_Card_form_7)
(*SR_U7F*)
@@ -1026,10 +1026,10 @@
apply (drule Outpts_parts_used)
apply simp
(*faster than
- apply (fastsimp dest: Outpts_parts_used)
+ apply (fastforce dest: Outpts_parts_used)
*)
(*SR_U10*)
-apply (fastsimp dest: Outpts_B_Card_form_7)
+apply (fastforce dest: Outpts_B_Card_form_7)
(*SR_U10F - uses assumption Card A not cloned*)
apply clarify
apply (drule Outpts_B_Card_form_7, assumption)
@@ -1345,7 +1345,7 @@
Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Certificate, Cert2\<rbrace> \<in> set evs"
apply (erule rev_mp)
apply (erule srb.induct)
-prefer 18 apply (fastsimp dest: Outpts_A_Card_form_10)
+prefer 18 apply (fastforce dest: Outpts_A_Card_form_10)
apply auto
done
--- a/src/HOL/Bali/AxCompl.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Bali/AxCompl.thy Mon Sep 12 07:55:43 2011 +0200
@@ -303,14 +303,14 @@
(is "G,A\<turnstile>{Normal ?P} .Init C. {?R}")
proof (rule ax_cases [where ?C="initd C"])
show "G,A\<turnstile>{Normal ?P \<and>. initd C} .Init C. {?R}"
- by (rule ax_derivs.Done [THEN conseq1]) (fastsimp intro: init_done)
+ by (rule ax_derivs.Done [THEN conseq1]) (fastforce intro: init_done)
next
have "G,A\<turnstile>{Normal (?P \<and>. Not \<circ> initd C)} .Init C. {?R}"
proof (cases n)
case 0
with is_cls
show ?thesis
- by - (rule ax_impossible [THEN conseq1],fastsimp dest: nyinitcls_emptyD)
+ by - (rule ax_impossible [THEN conseq1],fastforce dest: nyinitcls_emptyD)
next
case (Suc m)
with mgf_hyp have mgf_hyp': "\<And> t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>}"
@@ -342,7 +342,7 @@
case False
from mgf_hyp'
have "G,A\<turnstile>{?P'} .Init (super c). {?Q}"
- by (rule MGFnD' [THEN conseq12]) (fastsimp simp add: False c)
+ by (rule MGFnD' [THEN conseq12]) (fastforce simp add: False c)
with False show ?thesis
by simp
qed
@@ -350,7 +350,7 @@
from Suc is_cls
show "Normal (?P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C))
\<Rightarrow> ?P'"
- by (fastsimp elim: nyinitcls_le_SucD)
+ by (fastforce elim: nyinitcls_le_SucD)
qed
next
from mgf_hyp'
@@ -390,7 +390,7 @@
mode: "mode = invmode statM e" and
T: "T =Inl (resTy statM)" and
eq_accC_accC': "accC=accC'"
- by cases fastsimp+
+ by cases fastforce+
let ?Q="(\<lambda>Y s1 (x,s) . x = None \<and>
(\<exists>a. G\<turnstile>Norm s \<midarrow>e-\<succ>a\<rightarrow> s1 \<and>
(normal s1 \<longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT)
@@ -1072,7 +1072,7 @@
apply (rule MGFnD [OF mgf_e1, THEN ax_NormalD])
apply (rule allI)
apply (rule MGFnD' [OF mgf_e2, THEN conseq12])
- apply (fastsimp intro: eval.AVar)
+ apply (fastforce intro: eval.AVar)
done
next
case (InsInitV c v)
@@ -1084,7 +1084,7 @@
apply (rule MGFn_NormalI)
apply (rule ax_derivs.NewC)
apply (rule MGFn_InitD [OF hyp, THEN conseq2])
- apply (fastsimp intro: eval.NewC)
+ apply (fastforce intro: eval.NewC)
done
next
case (NewA T e)
@@ -1102,7 +1102,7 @@
apply (rule ax_derivs.Skip [THEN conseq1])
apply (clarsimp intro: eval.Skip)
apply (erule MGFnD' [THEN conseq12])
- apply (fastsimp intro: eval.NewA)
+ apply (fastforce intro: eval.NewA)
done
next
case (Cast C e)
@@ -1110,7 +1110,7 @@
apply -
apply (rule MGFn_NormalI)
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Cast])
- apply (fastsimp intro: eval.Cast)
+ apply (fastforce intro: eval.Cast)
done
next
case (Inst e C)
@@ -1118,7 +1118,7 @@
apply -
apply (rule MGFn_NormalI)
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Inst])
- apply (fastsimp intro: eval.Inst)
+ apply (fastforce intro: eval.Inst)
done
next
case (Lit v)
@@ -1126,7 +1126,7 @@
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.Lit [THEN conseq1])
- apply (fastsimp intro: eval.Lit)
+ apply (fastforce intro: eval.Lit)
done
next
case (UnOp unop e)
@@ -1135,7 +1135,7 @@
apply (rule MGFn_NormalI)
apply (rule ax_derivs.UnOp)
apply (erule MGFnD' [THEN conseq12])
- apply (fastsimp intro: eval.UnOp)
+ apply (fastforce intro: eval.UnOp)
done
next
case (BinOp binop e1 e2)
@@ -1148,7 +1148,7 @@
apply (case_tac "need_second_arg binop v1")
apply simp
apply (erule MGFnD' [THEN conseq12])
- apply (fastsimp intro: eval.BinOp)
+ apply (fastforce intro: eval.BinOp)
apply simp
apply (rule ax_Normal_cases)
apply (rule ax_derivs.Skip [THEN conseq1])
@@ -1157,7 +1157,7 @@
apply simp
apply simp
apply (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
- apply (fastsimp intro: eval.BinOp)
+ apply (fastforce intro: eval.BinOp)
done
next
case Super
@@ -1165,7 +1165,7 @@
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.Super [THEN conseq1])
- apply (fastsimp intro: eval.Super)
+ apply (fastforce intro: eval.Super)
done
next
case (Acc v)
@@ -1173,7 +1173,7 @@
apply -
apply (rule MGFn_NormalI)
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Acc])
- apply (fastsimp intro: eval.Acc simp add: split_paired_all)
+ apply (fastforce intro: eval.Acc simp add: split_paired_all)
done
next
case (Ass v e)
@@ -1184,7 +1184,7 @@
apply (erule MGFnD [THEN ax_NormalD])
apply (rule allI)
apply (erule MGFnD'[THEN conseq12])
- apply (fastsimp intro: eval.Ass simp add: split_paired_all)
+ apply (fastforce intro: eval.Ass simp add: split_paired_all)
done
next
case (Cond e1 e2 e3)
@@ -1197,14 +1197,14 @@
apply (rule ax_Normal_cases)
prefer 2
apply (rule ax_derivs.Abrupt [THEN conseq1],clarsimp simp add: Let_def)
- apply (fastsimp intro: eval.Cond)
+ apply (fastforce intro: eval.Cond)
apply (case_tac "b")
apply simp
apply (erule MGFnD'[THEN conseq12])
- apply (fastsimp intro: eval.Cond)
+ apply (fastforce intro: eval.Cond)
apply simp
apply (erule MGFnD'[THEN conseq12])
- apply (fastsimp intro: eval.Cond)
+ apply (fastforce intro: eval.Cond)
done
next
case (Call accC statT mode e mn pTs' ps)
@@ -1238,7 +1238,7 @@
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.Skip [THEN conseq1])
- apply (fastsimp intro: eval.Skip)
+ apply (fastforce intro: eval.Skip)
done
next
case (Expr e)
@@ -1246,7 +1246,7 @@
apply -
apply (rule MGFn_NormalI)
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Expr])
- apply (fastsimp intro: eval.Expr)
+ apply (fastforce intro: eval.Expr)
done
next
case (Lab l c)
@@ -1254,7 +1254,7 @@
apply -
apply (rule MGFn_NormalI)
apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Lab])
- apply (fastsimp intro: eval.Lab)
+ apply (fastforce intro: eval.Lab)
done
next
case (Comp c1 c2)
@@ -1264,7 +1264,7 @@
apply (rule ax_derivs.Comp)
apply (erule MGFnD [THEN ax_NormalD])
apply (erule MGFnD' [THEN conseq12])
- apply (fastsimp intro: eval.Comp)
+ apply (fastforce intro: eval.Comp)
done
next
case (If' e c1 c2)
@@ -1277,14 +1277,14 @@
apply (rule ax_Normal_cases)
prefer 2
apply (rule ax_derivs.Abrupt [THEN conseq1],clarsimp simp add: Let_def)
- apply (fastsimp intro: eval.If)
+ apply (fastforce intro: eval.If)
apply (case_tac "b")
apply simp
apply (erule MGFnD' [THEN conseq12])
- apply (fastsimp intro: eval.If)
+ apply (fastforce intro: eval.If)
apply simp
apply (erule MGFnD' [THEN conseq12])
- apply (fastsimp intro: eval.If)
+ apply (fastforce intro: eval.If)
done
next
case (Loop l e c)
@@ -1307,7 +1307,7 @@
apply -
apply (rule MGFn_NormalI)
apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Throw])
- apply (fastsimp intro: eval.Throw)
+ apply (fastforce intro: eval.Throw)
done
next
case (TryC c1 C vn c2)
@@ -1318,10 +1318,10 @@
?Q = " (\<lambda>Y' s' s. normal s \<and> (\<exists>s''. G\<turnstile>s \<midarrow>\<langle>c1\<rangle>\<^sub>s\<succ>\<rightarrow> (Y',s'') \<and>
G\<turnstile>s'' \<midarrow>sxalloc\<rightarrow> s')) \<and>. G\<turnstile>init\<le>n"])
apply (erule MGFnD [THEN ax_NormalD, THEN conseq2])
- apply (fastsimp elim: sxalloc_gext [THEN card_nyinitcls_gext])
+ apply (fastforce elim: sxalloc_gext [THEN card_nyinitcls_gext])
apply (erule MGFnD'[THEN conseq12])
- apply (fastsimp intro: eval.Try)
- apply (fastsimp intro: eval.Try)
+ apply (fastforce intro: eval.Try)
+ apply (fastforce intro: eval.Try)
done
next
case (Fin c1 c2)
@@ -1345,7 +1345,7 @@
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.Nil [THEN conseq1])
- apply (fastsimp intro: eval.Nil)
+ apply (fastforce intro: eval.Nil)
done
next
case (Cons_expr e es)
@@ -1356,7 +1356,7 @@
apply (erule MGFnD [THEN ax_NormalD])
apply (rule allI)
apply (erule MGFnD'[THEN conseq12])
- apply (fastsimp intro: eval.Cons)
+ apply (fastforce intro: eval.Cons)
done
qed
}
--- a/src/HOL/Bali/AxExample.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Bali/AxExample.thy Mon Sep 12 07:55:43 2011 +0200
@@ -133,7 +133,7 @@
apply (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")
apply (tactic "ax_tac 1")
apply (tactic {* inst1_tac @{context} "R" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> vs = [Null]) \<and>. heap_free two)" *})
-apply fastsimp
+apply fastforce
prefer 4
apply (rule ax_derivs.Done [THEN conseq1],force)
apply (rule ax_subst_Val_allI)
--- a/src/HOL/Bali/AxSound.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Bali/AxSound.thy Mon Sep 12 07:55:43 2011 +0200
@@ -459,7 +459,7 @@
show "P (In2 vf) s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
proof
from eval normal_s0 obtain "s1=s0" "vf=lvar vn (store s0)"
- by (fastsimp elim: evaln_elim_cases)
+ by (fastforce elim: evaln_elim_cases)
with P show "P (In2 vf) s1 Z"
by simp
next
@@ -500,7 +500,7 @@
eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s2" and
fvar: "(vf,s2')=fvar statDeclC stat fn a s2" and
s3: "s3 = check_field_access G accC statDeclC fn stat a s2'"
- using normal_s0 by (fastsimp elim: evaln_elim_cases)
+ using normal_s0 by (fastforce elim: evaln_elim_cases)
have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
proof -
from wf wt_e
@@ -593,7 +593,7 @@
eval_e1: "G\<turnstile>s0 \<midarrow>e1-\<succ>a\<midarrow>n\<rightarrow> s1" and
eval_e2: "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n\<rightarrow> s2" and
avar: "avar G i a s2 =(vf, s2')"
- using normal_s0 by (fastsimp elim: evaln_elim_cases)
+ using normal_s0 by (fastforce elim: evaln_elim_cases)
from valid_e1 P valid_A conf_s0 eval_e1 wt_e1 da_e1
obtain Q: "Q \<lfloor>a\<rfloor>\<^sub>e s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G, L)"
by (rule validE)
@@ -654,7 +654,7 @@
eval_init: "G\<turnstile>s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1" and
alloc: "G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2" and
v: "v=Addr a"
- using normal_s0 by (fastsimp elim: evaln_elim_cases)
+ using normal_s0 by (fastforce elim: evaln_elim_cases)
from valid_init P valid_A conf_s0 eval_init wt_init da_init
obtain "(Alloc G (CInst C) Q) \<diamondsuit> s1 Z"
by (rule validE)
@@ -696,7 +696,7 @@
eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n\<rightarrow> s2" and
alloc: "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" and
v: "v=Addr a"
- using normal_s0 by (fastsimp elim: evaln_elim_cases)
+ using normal_s0 by (fastforce elim: evaln_elim_cases)
obtain I where
da_init:
"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>init_comp_ty T\<rangle>\<^sub>s\<guillemotright> I"
@@ -766,7 +766,7 @@
from eval obtain s1 where
eval_e: "G\<turnstile>s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1" and
s2: "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits T) ClassCast) s1"
- using normal_s0 by (fastsimp elim: evaln_elim_cases)
+ using normal_s0 by (fastforce elim: evaln_elim_cases)
from valid_e P valid_A conf_s0 eval_e wt_e da_e
have "(\<lambda>Val:v:. \<lambda>s.. abupd (raise_if (\<not> G,s\<turnstile>v fits T) ClassCast) .;
Q\<leftarrow>In1 v) \<lfloor>v\<rfloor>\<^sub>e s1 Z"
@@ -805,7 +805,7 @@
from eval obtain a where
eval_e: "G\<turnstile>s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1" and
v: "v = Bool (a \<noteq> Null \<and> G,store s1\<turnstile>a fits RefT T)"
- using normal_s0 by (fastsimp elim: evaln_elim_cases)
+ using normal_s0 by (fastforce elim: evaln_elim_cases)
from valid_e P valid_A conf_s0 eval_e wt_e da_e
have "(\<lambda>Val:v:. \<lambda>s.. Q\<leftarrow>In1 (Bool (v \<noteq> Null \<and> G,s\<turnstile>v fits RefT T)))
\<lfloor>a\<rfloor>\<^sub>e s1 Z"
@@ -859,7 +859,7 @@
from eval obtain ve where
eval_e: "G\<turnstile>s0 \<midarrow>e-\<succ>ve\<midarrow>n\<rightarrow> s1" and
v: "v = eval_unop unop ve"
- using normal_s0 by (fastsimp elim: evaln_elim_cases)
+ using normal_s0 by (fastforce elim: evaln_elim_cases)
from valid_e P valid_A conf_s0 eval_e wt_e da_e
have "(\<lambda>Val:v:. Q\<leftarrow>In1 (eval_unop unop v)) \<lfloor>ve\<rfloor>\<^sub>e s1 Z"
by (rule validE)
@@ -912,7 +912,7 @@
eval_e2: "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)
\<succ>\<midarrow>n\<rightarrow> (\<lfloor>v2\<rfloor>\<^sub>e, s2)" and
v: "v=eval_binop binop v1 v2"
- using normal_s0 by (fastsimp elim: evaln_elim_cases)
+ using normal_s0 by (fastforce elim: evaln_elim_cases)
from valid_e1 P valid_A conf_s0 eval_e1 wt_e1 da_e1
obtain Q: "Q \<lfloor>v1\<rfloor>\<^sub>e s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"
by (rule validE)
@@ -994,7 +994,7 @@
by (cases "\<exists> n. var=LVar n") (insert da.LVar,auto elim!: da_elim_cases)
from eval obtain w upd where
eval_var: "G\<turnstile>s0 \<midarrow>var=\<succ>(v, upd)\<midarrow>n\<rightarrow> s1"
- using normal_s0 by (fastsimp elim: evaln_elim_cases)
+ using normal_s0 by (fastforce elim: evaln_elim_cases)
from valid_var P valid_A conf_s0 eval_var wt_var da_var
have "(\<lambda>Var:(v, f):. Q\<leftarrow>In1 v) \<lfloor>(v, upd)\<rfloor>\<^sub>v s1 Z"
by (rule validE)
@@ -1151,7 +1151,7 @@
from eval obtain b s1 where
eval_e0: "G\<turnstile>s0 \<midarrow>e0-\<succ>b\<midarrow>n\<rightarrow> s1" and
eval_then_else: "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2"
- using normal_s0 by (fastsimp elim: evaln_elim_cases)
+ using normal_s0 by (fastforce elim: evaln_elim_cases)
from valid_e0 P valid_A conf_s0 eval_e0 wt_e0 da_e0
obtain "P' \<lfloor>b\<rfloor>\<^sub>e s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"
by (rule validE)
@@ -1246,7 +1246,7 @@
mode: "mode = invmode statM e" and
T: "T =(resTy statM)" and
eq_accC_accC': "accC=accC'"
- by cases fastsimp+
+ by cases fastforce+
from da obtain C where
da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s0)))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> C" and
da_args: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm C \<guillemotright>\<langle>args\<rangle>\<^sub>l\<guillemotright> E"
@@ -1635,7 +1635,7 @@
abrupt s2 = Some (Jump (Cont l))
then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)"and
s4: "s4 = abupd (absorb Ret) s3"
- using normal_s0 by (fastsimp elim: evaln_elim_cases)
+ using normal_s0 by (fastforce elim: evaln_elim_cases)
obtain C' where
da_c': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright> C'"
proof -
@@ -1720,7 +1720,7 @@
eval_e: "G\<turnstile>s0 \<midarrow>e-\<succ>ve\<midarrow>n\<rightarrow> s1" and
eval_es: "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2" and
v: "v=ve#vs"
- using normal_s0 by (fastsimp elim: evaln_elim_cases)
+ using normal_s0 by (fastforce elim: evaln_elim_cases)
from valid_e P valid_A conf_s0 eval_e wt_e da_e
obtain Q: "Q \<lfloor>ve\<rfloor>\<^sub>e s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"
by (rule validE)
@@ -1768,7 +1768,7 @@
show "P \<diamondsuit> s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
proof -
from eval obtain "s1=s0"
- using normal_s0 by (fastsimp elim: evaln_elim_cases)
+ using normal_s0 by (fastforce elim: evaln_elim_cases)
with P conf_s0 show ?thesis
by simp
qed
@@ -1796,7 +1796,7 @@
by cases simp
from eval obtain v where
eval_e: "G\<turnstile>s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
- using normal_s0 by (fastsimp elim: evaln_elim_cases)
+ using normal_s0 by (fastforce elim: evaln_elim_cases)
from valid_e P valid_A conf_s0 eval_e wt_e da_e
obtain Q: "(Q\<leftarrow>\<diamondsuit>) \<lfloor>v\<rfloor>\<^sub>e s1 Z" and "s1\<Colon>\<preceq>(G,L)"
by (rule validE)
@@ -1827,7 +1827,7 @@
from eval obtain s1 where
eval_c: "G\<turnstile>s0 \<midarrow>c\<midarrow>n\<rightarrow> s1" and
s2: "s2 = abupd (absorb l) s1"
- using normal_s0 by (fastsimp elim: evaln_elim_cases)
+ using normal_s0 by (fastforce elim: evaln_elim_cases)
from valid_c P valid_A conf_s0 eval_c wt_c da_c
obtain Q: "(abupd (absorb l) .; Q) \<diamondsuit> s1 Z"
by (rule validE)
@@ -1859,7 +1859,7 @@
from eval obtain s1 where
eval_c1: "G\<turnstile>s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1" and
eval_c2: "G\<turnstile>s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2"
- using normal_s0 by (fastsimp elim: evaln_elim_cases)
+ using normal_s0 by (fastforce elim: evaln_elim_cases)
from wt obtain
wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
@@ -2297,7 +2297,7 @@
s3: "if G,s2\<turnstile>catch C
then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n\<rightarrow> s3
else s3 = s2"
- using normal_s0 by (fastsimp elim: evaln_elim_cases)
+ using normal_s0 by (fastforce elim: evaln_elim_cases)
from wt obtain
wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
wt_c2: "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
@@ -2429,7 +2429,7 @@
s3: "s3 = (if \<exists>err. abr1 = Some (Error err)
then (abr1, s1)
else abupd (abrupt_if (abr1 \<noteq> None) abr1) s2)"
- using normal_s0 by (fastsimp elim: evaln_elim_cases)
+ using normal_s0 by (fastforce elim: evaln_elim_cases)
from wt obtain
wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"
--- a/src/HOL/Bali/DefiniteAssignment.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy Mon Sep 12 07:55:43 2011 +0200
@@ -972,7 +972,7 @@
case (UnOp unop e)
thus ?case
by - (erule wt_elim_cases,cases unop,
- (fastsimp simp add: assignsE_const_simp)+)
+ (fastforce simp add: assignsE_const_simp)+)
next
case (BinOp binop e1 e2)
from BinOp.prems obtain e1T e2T
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Mon Sep 12 07:55:43 2011 +0200
@@ -65,7 +65,7 @@
case False
with eval obtain s0' abr where "G\<turnstile>(Some abr,s0') \<midarrow>Body D c-\<succ>v\<rightarrow>s1"
"s0 = (Some abr, s0')"
- by (cases s0) fastsimp
+ by (cases s0) fastforce
with this jump
show ?thesis
by (cases) (simp)
@@ -89,7 +89,7 @@
case False
with eval obtain s0' abr where "G\<turnstile>(Some abr,s0') \<midarrow>Methd D sig-\<succ>v\<rightarrow>s1"
"s0 = (Some abr, s0')"
- by (cases s0) fastsimp
+ by (cases s0) fastforce
with this jump
show ?thesis
by (cases) (simp)
@@ -1102,7 +1102,7 @@
apply (rule jumpNestingOk_evalE)
apply assumption
apply simp
- apply fastsimp
+ apply fastforce
done
qed
@@ -2789,7 +2789,7 @@
by blast
moreover from brk_c2' brk_c2 A
have "?BreakAssigned s1 s2 A"
- by fastsimp
+ by fastforce
with True
have "?BreakAssigned (Norm s0) s2 A" by simp
moreover from res_c2 True
@@ -2874,7 +2874,7 @@
by blast
moreover from brk_c1' brk_c1 A
have "?BreakAssigned s1 s2 A"
- by fastsimp
+ by fastforce
with normal_s1
have "?BreakAssigned (Norm s0) s2 A" by simp
moreover from res_c1 normal_s1 have "?ResAssigned (Norm s0) s2"
@@ -2904,7 +2904,7 @@
by blast
moreover from brk_c2' brk_c2 A
have "?BreakAssigned s1 s2 A"
- by fastsimp
+ by fastforce
with normal_s1
have "?BreakAssigned (Norm s0) s2 A" by simp
moreover from res_c2 normal_s1 have "?ResAssigned (Norm s0) s2"
@@ -3025,7 +3025,7 @@
proof -
from brk_A_A' brk_A'
have "?BreakAssigned (abupd (absorb (Cont l)) s2) s3 A"
- by fastsimp
+ by fastforce
moreover
from True have "normal (abupd (absorb (Cont l)) s2)"
by (cases s2) auto
@@ -3046,11 +3046,11 @@
by auto
with nrm_C_C' nrm_C' A
have "?NormalAssigned s3 A"
- by fastsimp
+ by fastforce
moreover
from eq_s3_s2 brk_C_C' brk_C' normal_s1 A
have "?BreakAssigned (Norm s0) s3 A"
- by fastsimp
+ by fastforce
moreover
from eq_s3_s2 res_s2 normal_s1 have "?ResAssigned (Norm s0) s3"
by simp
@@ -3275,7 +3275,7 @@
from brkAss_C2 have "?BreakAssigned (Norm s0) s3 C2'"
by (cases s2) (auto simp add: new_xcpt_var_def)
with brk_C2' A show ?thesis
- by fastsimp
+ by fastforce
qed
moreover
from resAss_s3 have "?ResAssigned (Norm s0) s3"
@@ -3353,7 +3353,7 @@
by blast
moreover
from brkAss_C2' brk_C2' have "?BreakAssigned (Norm s1) s2 C2"
- by fastsimp
+ by fastforce
ultimately
show ?thesis
using that resAss_s2' by simp
@@ -3379,7 +3379,7 @@
by (cases s2) (simp add: abrupt_if_def)
with normal_s3 nrmAss_C1 s3 s1_s2
show ?thesis
- by fastsimp
+ by fastforce
qed
moreover
have "nrm C2 \<subseteq> dom (locals (snd s3))"
@@ -3389,7 +3389,7 @@
by (cases s2) (simp add: abrupt_if_def)
with normal_s3 nrmAss_C2 s3 s1_s2
show ?thesis
- by fastsimp
+ by fastforce
qed
ultimately have "nrm C1 \<union> nrm C2 \<subseteq> \<dots>"
by (rule Un_least)
--- a/src/HOL/Bali/Eval.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Bali/Eval.thy Mon Sep 12 07:55:43 2011 +0200
@@ -901,7 +901,7 @@
then have "False" by induct auto
}
then show ?thesis
- by (cases s') fastsimp
+ by (cases s') fastforce
qed
@@ -914,7 +914,7 @@
then have "False" by induct auto
}
then show ?thesis
- by (cases s') fastsimp
+ by (cases s') fastforce
qed
lemma eval_InsInitV: "G\<turnstile>Norm s\<midarrow>InsInitV c w=\<succ>v\<rightarrow> s' = False"
@@ -926,7 +926,7 @@
then have "False" by induct auto
}
then show ?thesis
- by (cases s') fastsimp
+ by (cases s') fastforce
qed
lemma eval_FinA: "G\<turnstile>Norm s\<midarrow>FinA a c\<rightarrow> s' = False"
@@ -938,7 +938,7 @@
then have "False" by induct auto
}
then show ?thesis
- by (cases s') fastsimp
+ by (cases s') fastforce
qed
lemma eval_no_abrupt_lemma:
--- a/src/HOL/Bali/Evaln.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Bali/Evaln.thy Mon Sep 12 07:55:43 2011 +0200
@@ -305,7 +305,7 @@
then have "False" by induct auto
}
then show ?thesis
- by (cases s') fastsimp
+ by (cases s') fastforce
qed
lemma evaln_InsInitE: "G\<turnstile>Norm s\<midarrow>In1l (InsInitE c e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
@@ -317,7 +317,7 @@
then have "False" by induct auto
}
then show ?thesis
- by (cases s') fastsimp
+ by (cases s') fastforce
qed
lemma evaln_InsInitV: "G\<turnstile>Norm s\<midarrow>In2 (InsInitV c w)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
@@ -329,7 +329,7 @@
then have "False" by induct auto
}
then show ?thesis
- by (cases s') fastsimp
+ by (cases s') fastforce
qed
lemma evaln_FinA: "G\<turnstile>Norm s\<midarrow>In1r (FinA a c)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
@@ -341,7 +341,7 @@
then have "False" by induct auto
}
then show ?thesis
- by (cases s') fastsimp
+ by (cases s') fastforce
qed
lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow>
@@ -602,7 +602,7 @@
moreover
from Try.hyps obtain n2 where
"if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
- by fastsimp
+ by fastforce
ultimately
have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
by (auto intro!: evaln.Try le_maxI1 le_maxI2)
--- a/src/HOL/Bali/TypeSafe.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Mon Sep 12 07:55:43 2011 +0200
@@ -1335,7 +1335,7 @@
proof (cases "(tab(x\<mapsto>y)) vn \<noteq> Some z")
case True
with some ys have "(tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = Some z"
- by (fastsimp intro: Cons.hyps)
+ by (fastforce intro: Cons.hyps)
with ys show ?thesis
by simp
next
@@ -3012,7 +3012,7 @@
mode: "mode = invmode statM e" and
T: "T =Inl (resTy statM)" and
eq_accC_accC': "accC=accC'"
- by (rule wt_elim_cases) fastsimp+
+ by (rule wt_elim_cases) fastforce+
from Call.prems obtain E where
da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1l e\<guillemotright> E" and
--- a/src/HOL/Bali/WellForm.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Bali/WellForm.thy Mon Sep 12 07:55:43 2011 +0200
@@ -2788,7 +2788,7 @@
proof -
from im statM statT isT_statT wf not_Private_statM
have "is_static im = is_static statM"
- by (fastsimp dest: wf_imethds_hiding_objmethdsD)
+ by (fastforce dest: wf_imethds_hiding_objmethdsD)
with wf isT_statT statT im
have "\<not> is_static statM"
by (auto dest: wf_prog_idecl imethds_wf_mhead)
--- a/src/HOL/Big_Operators.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Big_Operators.thy Mon Sep 12 07:55:43 2011 +0200
@@ -503,7 +503,7 @@
thus ?case by simp
next
case insert
- thus ?case using add_mono by fastsimp
+ thus ?case using add_mono by fastforce
qed
next
case False
@@ -893,11 +893,11 @@
lemma setprod_cong:
"A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
-by(fastsimp simp: setprod_def intro: fold_image_cong)
+by(fastforce simp: setprod_def intro: fold_image_cong)
lemma strong_setprod_cong[cong]:
"A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
-by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong)
+by(fastforce simp: simp_implies_def setprod_def intro: fold_image_cong)
lemma setprod_reindex_cong: "inj_on f A ==>
B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
@@ -1590,7 +1590,7 @@
proof -
interpret ab_semigroup_idem_mult min
by (rule ab_semigroup_idem_mult_min)
- from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
+ from assms fold1_in show ?thesis by (fastforce simp: Min_def min_def)
qed
lemma Max_in [simp]:
@@ -1599,7 +1599,7 @@
proof -
interpret ab_semigroup_idem_mult max
by (rule ab_semigroup_idem_mult_max)
- from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
+ from assms fold1_in [of A] show ?thesis by (fastforce simp: Max_def max_def)
qed
lemma Min_le [simp]:
@@ -1739,8 +1739,8 @@
then have A: "?A = A" using insert_Diff_single insert_absorb by auto
then have "P ?B" using `P {}` step IH[of ?B] by blast
moreover
- have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastsimp
- ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastsimp
+ have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce
+ ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastforce
qed
qed
--- a/src/HOL/Decision_Procs/Cooper.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Mon Sep 12 07:55:43 2011 +0200
@@ -1657,7 +1657,7 @@
prefer 2
apply(drule minusinfinity)
apply assumption+
-apply(fastsimp)
+apply(fastforce)
apply clarsimp
apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
apply(frule_tac x = x and z=z in decr_lemma)
@@ -1665,7 +1665,7 @@
prefer 2
apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
prefer 2 apply arith
- apply fastsimp
+ apply fastforce
apply(drule (1) periodic_finite_ex)
apply blast
apply(blast dest:decr_mult_lemma)
--- a/src/HOL/Decision_Procs/MIR.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Mon Sep 12 07:55:43 2011 +0200
@@ -2733,7 +2733,7 @@
prefer 2
apply(drule minusinfinity)
apply assumption+
-apply(fastsimp)
+apply(fastforce)
apply clarsimp
apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
apply(frule_tac x = x and z=z in decr_lemma)
@@ -2741,7 +2741,7 @@
prefer 2
apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
prefer 2 apply arith
- apply fastsimp
+ apply fastforce
apply(drule (1) periodic_finite_ex)
apply blast
apply(blast dest:decr_mult_lemma)
--- a/src/HOL/Deriv.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Deriv.thy Mon Sep 12 07:55:43 2011 +0200
@@ -745,7 +745,7 @@
proof (rule ccontr)
assume "\<not> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
with M1 have M3: "\<forall>x. a \<le> x & x \<le> b --> f x < M"
- by (fastsimp simp add: linorder_not_le [symmetric])
+ by (fastforce simp add: linorder_not_le [symmetric])
hence "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. inverse (M - f x)) x"
by (auto simp add: con)
from isCont_bounded [OF le this]
--- a/src/HOL/Divides.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Divides.thy Mon Sep 12 07:55:43 2011 +0200
@@ -194,7 +194,7 @@
apply (unfold dvd_def)
apply auto
apply(blast intro:mult_assoc[symmetric])
-apply(fastsimp simp add: mult_assoc)
+apply(fastforce simp add: mult_assoc)
done
lemma dvd_mod_imp_dvd: "[| k dvd m mod n; k dvd n |] ==> k dvd m"
@@ -2232,7 +2232,7 @@
lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"
apply (rule split_zmod[THEN iffD2])
-apply(fastsimp dest: q_pos_lemma intro: split_mult_pos_le)
+apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
done
--- a/src/HOL/Equiv_Relations.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Equiv_Relations.thy Mon Sep 12 07:55:43 2011 +0200
@@ -349,7 +349,7 @@
apply(subst card_UN_disjoint)
apply assumption
apply simp
- apply(fastsimp simp add:inj_on_def)
+ apply(fastforce simp add:inj_on_def)
apply simp
done
--- a/src/HOL/Finite_Set.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Finite_Set.thy Mon Sep 12 07:55:43 2011 +0200
@@ -124,7 +124,7 @@
lemma finite_Collect_less_nat [iff]:
"finite {n::nat. n < k}"
- by (fastsimp simp: finite_conv_nat_seg_image)
+ by (fastforce simp: finite_conv_nat_seg_image)
lemma finite_Collect_le_nat [iff]:
"finite {n::nat. n \<le> k}"
@@ -2040,7 +2040,7 @@
show "A = insert b (A-{b})" using b by blast
show "b \<notin> A - {b}" by blast
show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
- using assms b fin by(fastsimp dest:mk_disjoint_insert)+
+ using assms b fin by(fastforce dest:mk_disjoint_insert)+
qed
qed
@@ -2056,7 +2056,7 @@
lemma card_le_Suc_iff: "finite A \<Longrightarrow>
Suc n \<le> card A = (\<exists>a B. A = insert a B \<and> a \<notin> B \<and> n \<le> card B \<and> finite B)"
-by (fastsimp simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
+by (fastforce simp: card_Suc_eq less_eq_nat.simps(2) insert_eq_iff
dest: subset_singletonD split: nat.splits if_splits)
lemma finite_fun_UNIVD2:
@@ -2242,7 +2242,7 @@
lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
-by(fastsimp simp:surj_def dest!: endo_inj_surj)
+by(fastforce simp:surj_def dest!: endo_inj_surj)
corollary infinite_UNIV_nat[iff]: "~finite(UNIV::nat set)"
proof
--- a/src/HOL/Fun.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Fun.thy Mon Sep 12 07:55:43 2011 +0200
@@ -461,7 +461,7 @@
lemma surj_vimage_empty:
assumes "surj f" shows "f -` A = {} \<longleftrightarrow> A = {}"
using surj_image_vimage_eq[OF `surj f`, of A]
- by (intro iffI) fastsimp+
+ by (intro iffI) fastforce+
lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
by (simp add: inj_on_def, blast)
@@ -603,7 +603,7 @@
by (rule ext, auto)
lemma inj_on_fun_updI: "\<lbrakk> inj_on f A; y \<notin> f`A \<rbrakk> \<Longrightarrow> inj_on (f(x:=y)) A"
-by (fastsimp simp:inj_on_def image_def)
+by (fastforce simp:inj_on_def image_def)
lemma fun_upd_image:
"f(x:=y) ` A = (if x \<in> A then insert y (f ` (A-{x})) else f ` A)"
--- a/src/HOL/GCD.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/GCD.thy Mon Sep 12 07:55:43 2011 +0200
@@ -525,7 +525,7 @@
lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
apply(rule antisym)
- apply (fastsimp intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
+ apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
apply simp
done
@@ -1604,7 +1604,7 @@
apply simp
apply (rule Max_le_iff[THEN iffD2])
apply (metis all_not_in_conv finite_divisors_nat finite_INT)
- apply fastsimp
+ apply fastforce
apply clarsimp
apply (metis Gcd_dvd_nat Max_in dvd_0_left dvd_Gcd_nat dvd_imp_le linorder_antisym_conv3 not_less0)
done
@@ -1670,9 +1670,9 @@
apply(rule Lcm_eq_Max_nat)
apply simp
apply blast
- apply fastsimp
+ apply fastforce
apply clarsimp
- apply(fastsimp intro: finite_divisors_nat intro!: finite_INT)
+ apply(fastforce intro: finite_divisors_nat intro!: finite_INT)
done
qed
qed
--- a/src/HOL/HOLCF/IMP/Denotational.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/HOLCF/IMP/Denotational.thy Mon Sep 12 07:55:43 2011 +0200
@@ -48,8 +48,8 @@
lemma D_implies_eval: "!s t. D c\<cdot>(Discr s) = (Def t) --> (c,s) \<Rightarrow> t"
apply (induct c)
- apply fastsimp
- apply fastsimp
+ apply fastforce
+ apply fastforce
apply force
apply (simp (no_asm))
apply force
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Mon Sep 12 07:55:43 2011 +0200
@@ -299,7 +299,7 @@
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
(* a~: act B; a~: act A *)
-apply (fastsimp intro!: ext_is_act simp: externals_of_par)
+apply (fastforce intro!: ext_is_act simp: externals_of_par)
done
declare FiniteConc [simp]
@@ -452,7 +452,7 @@
apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
(* Case a~:A, a~:B *)
-apply (fastsimp intro!: ext_is_act simp: externals_of_par)
+apply (fastforce intro!: ext_is_act simp: externals_of_par)
done
--- a/src/HOL/HOLCF/IOA/meta_theory/Seq.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Seq.thy Mon Sep 12 07:55:43 2011 +0200
@@ -275,7 +275,7 @@
lemma Finite_cons_a: "Finite x --> a~=UU --> x=a##xs --> Finite xs"
apply (intro strip)
apply (erule Finite.cases)
-apply fastsimp
+apply fastforce
apply simp
done
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Mon Sep 12 07:55:43 2011 +0200
@@ -836,7 +836,7 @@
==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)"
apply (drule divide_Seq2)
(*Auto_tac no longer proves it*)
-apply fastsimp
+apply fastforce
done
lemmas [simp] = FilterPQ FilterConc Conc_cong
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Mon Sep 12 07:55:43 2011 +0200
@@ -197,9 +197,9 @@
apply (tactic {* pair_tac @{context} "a" 1 *})
apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
apply blast
-apply fastsimp
+apply fastforce
apply (tactic {* pair_tac @{context} "a" 1 *})
- apply fastsimp
+ apply fastforce
done
end
--- a/src/HOL/HOLCF/Library/Stream.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/HOLCF/Library/Stream.thy Mon Sep 12 07:55:43 2011 +0200
@@ -865,7 +865,7 @@
apply (drule ex_sconc,auto)
apply (erule contrapos_pp)
apply (insert stream_finite_i_rt)
- apply (fastsimp simp add: slen_infinite,auto)
+ apply (fastforce simp add: slen_infinite,auto)
by (simp add: sconc_def)
lemma sconc_finite: "(#x~=\<infinity> & #y~=\<infinity>) = (#(x ooo y)~=\<infinity>)"
--- a/src/HOL/Hilbert_Choice.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Hilbert_Choice.thy Mon Sep 12 07:55:43 2011 +0200
@@ -148,7 +148,7 @@
lemma inv_into_image_cancel[simp]:
"inj_on f A ==> S <= A ==> inv_into A f ` f ` S = S"
-by(fastsimp simp: image_def)
+by(fastforce simp: image_def)
lemma inj_imp_surj_inv: "inj f ==> surj (inv f)"
by (blast intro!: surjI inv_into_f_f)
--- a/src/HOL/Hoare/Arith2.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Hoare/Arith2.thy Mon Sep 12 07:55:43 2011 +0200
@@ -39,12 +39,12 @@
lemma cd_diff_l: "n<=m ==> cd x m n = cd x (m-n) n"
apply (unfold cd_def)
- apply (fastsimp dest: dvd_diffD)
+ apply (fastforce dest: dvd_diffD)
done
lemma cd_diff_r: "m<=n ==> cd x m n = cd x m (n-m)"
apply (unfold cd_def)
- apply (fastsimp dest: dvd_diffD)
+ apply (fastforce dest: dvd_diffD)
done
--- a/src/HOL/Hoare/Heap.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Hoare/Heap.thy Mon Sep 12 07:55:43 2011 +0200
@@ -32,15 +32,15 @@
lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)"
apply(case_tac xs)
-apply fastsimp
-apply fastsimp
+apply fastforce
+apply fastforce
done
lemma [simp]: "Path h (Ref a) as z =
(as = [] \<and> z = Ref a \<or> (\<exists>bs. as = a#bs \<and> Path h (h a) bs z))"
apply(case_tac as)
-apply fastsimp
-apply fastsimp
+apply fastforce
+apply fastforce
done
lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
@@ -116,12 +116,12 @@
lemma List_hd_not_in_tl[simp]: "List h (h a) as \<Longrightarrow> a \<notin> set as"
apply (clarsimp simp add:in_set_conv_decomp)
apply(frule List_app[THEN iffD1])
-apply(fastsimp dest: List_unique)
+apply(fastforce dest: List_unique)
done
lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
apply(induct as, simp)
-apply(fastsimp dest:List_hd_not_in_tl)
+apply(fastforce dest:List_hd_not_in_tl)
done
lemma Path_is_List:
@@ -165,7 +165,7 @@
lemma list_Ref_conv[simp]:
"islist h (h a) \<Longrightarrow> list h (Ref a) = a # list h (h a)"
apply(insert List_Ref[of h])
-apply(fastsimp simp:List_conv_islist_list)
+apply(fastforce simp:List_conv_islist_list)
done
lemma [simp]: "islist h (h a) \<Longrightarrow> a \<notin> set(list h (h a))"
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Mon Sep 12 07:55:43 2011 +0200
@@ -76,7 +76,7 @@
lemma CondRule:
"p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
\<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
-by (fastsimp simp:Valid_def image_def)
+by (fastforce simp:Valid_def image_def)
lemma While_aux:
assumes "Sem (WHILE b INV {i} DO c OD) s s'"
--- a/src/HOL/Hoare/Pointer_Examples.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Hoare/Pointer_Examples.thy Mon Sep 12 07:55:43 2011 +0200
@@ -23,20 +23,20 @@
DO r := p; p := p^.tl; r^.tl := q; q := r OD
{List tl q (rev Ps @ Qs)}"
apply vcg_simp
- apply fastsimp
- apply(fastsimp intro:notin_List_update[THEN iffD2])
+ apply fastforce
+ apply(fastforce intro:notin_List_update[THEN iffD2])
(* explicit:
apply clarify
apply(rename_tac ps b qs)
apply clarsimp
apply(rename_tac ps')
- apply(fastsimp intro:notin_List_update[THEN iffD2])
+ apply(fastforce intro:notin_List_update[THEN iffD2])
apply(rule_tac x = ps' in exI)
apply simp
apply(rule_tac x = "b#qs" in exI)
apply simp
*)
-apply fastsimp
+apply fastforce
done
text{* And now with ghost variables @{term ps} and @{term qs}. Even
@@ -52,8 +52,8 @@
qs := (hd ps) # qs; ps := tl ps OD
{List next q (rev Ps @ Qs)}"
apply vcg_simp
- apply fastsimp
-apply fastsimp
+ apply fastforce
+apply fastforce
done
text "A longer readable version:"
@@ -69,7 +69,7 @@
fix tl p q r
assume "List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}"
thus "\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
- rev ps @ qs = rev Ps @ Qs" by fastsimp
+ rev ps @ qs = rev Ps @ Qs" by fastforce
next
fix tl p q r
assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
@@ -77,12 +77,12 @@
(is "(\<exists>ps qs. ?I ps qs) \<and> _")
then obtain ps qs a where I: "?I ps qs \<and> p = Ref a"
by fast
- then obtain ps' where "ps = a # ps'" by fastsimp
+ then obtain ps' where "ps = a # ps'" by fastforce
hence "List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
List (tl(p \<rightarrow> q)) p (a#qs) \<and>
set ps' \<inter> set (a#qs) = {} \<and>
rev ps' @ (a#qs) = rev Ps @ Qs"
- using I by fastsimp
+ using I by fastforce
thus "\<exists>ps' qs'. List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and>
List (tl(p \<rightarrow> q)) p qs' \<and>
set ps' \<inter> set qs' = {} \<and>
@@ -91,7 +91,7 @@
fix tl p q r
assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> Null"
- thus "List tl q (rev Ps @ Qs)" by fastsimp
+ thus "List tl q (rev Ps @ Qs)" by fastforce
qed
@@ -144,7 +144,7 @@
{p = X}"
apply vcg_simp
apply blast
- apply fastsimp
+ apply fastforce
apply clarsimp
done
@@ -196,7 +196,7 @@
{List tl p (splice Ps Qs)}"
apply vcg_simp
apply(rule_tac x = "[]" in exI)
- apply fastsimp
+ apply fastforce
apply clarsimp
apply(rename_tac y bs qqs)
apply(case_tac bs) apply simp
@@ -208,7 +208,7 @@
apply simp
apply(rule_tac x = "qqs" in exI)
apply simp
-apply (fastsimp simp:List_app)
+apply (fastforce simp:List_app)
done
@@ -259,13 +259,13 @@
apply vcg_simp
apply (simp_all add: cand_def cor_def)
-apply (fastsimp)
+apply (fastforce)
apply clarsimp
apply(rule conjI)
apply clarsimp
apply(rule conjI)
-apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
+apply (fastforce intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
apply clarsimp
apply(rule conjI)
apply (clarsimp)
@@ -282,7 +282,7 @@
apply(clarsimp simp:eq_sym_conv)
apply(rule_tac x = "bsa" in exI)
apply(simp)
-apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
+apply (fastforce intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv)
apply(clarsimp simp add:List_app)
done
@@ -311,7 +311,7 @@
apply vcg_simp
apply (simp_all add: cand_def cor_def)
-apply (fastsimp)
+apply (fastforce)
apply clarsimp
apply(rule conjI)
@@ -393,8 +393,8 @@
apply vcg_simp
apply (simp_all add: cand_def cor_def)
- apply (fastsimp)
- apply (fastsimp simp: eq_sym_conv)
+ apply (fastforce)
+ apply (fastforce simp: eq_sym_conv)
apply(clarsimp)
done
@@ -470,7 +470,7 @@
apply clarsimp
apply clarsimp
apply (case_tac "(q = Null)")
- apply (fastsimp intro: Path_is_List)
+ apply (fastforce intro: Path_is_List)
apply clarsimp
apply (rule_tac x= "bs" in exI)
apply (rule_tac x= "y # qs" in exI)
@@ -506,7 +506,7 @@
{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 fastsimp
+apply fastforce
done
--- a/src/HOL/Hoare/Pointer_ExamplesAbort.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Hoare/Pointer_ExamplesAbort.thy Mon Sep 12 07:55:43 2011 +0200
@@ -21,9 +21,9 @@
DO r := p; (p \<noteq> Null \<rightarrow> p := p^.tl); r^.tl := q; q := r OD
{List tl q (rev Ps @ Qs)}"
apply vcg_simp
- apply fastsimp
- apply(fastsimp intro:notin_List_update[THEN iffD2])
-apply fastsimp
+ apply fastforce
+ apply(fastforce intro:notin_List_update[THEN iffD2])
+apply fastforce
done
end
--- a/src/HOL/Hoare/Pointers0.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Hoare/Pointers0.thy Mon Sep 12 07:55:43 2011 +0200
@@ -51,15 +51,15 @@
lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)"
apply(case_tac xs)
-apply fastsimp
-apply fastsimp
+apply fastforce
+apply fastforce
done
lemma [simp]: "a \<noteq> Null \<Longrightarrow> Path h a as z =
(as = [] \<and> z = a \<or> (\<exists>bs. as = a#bs \<and> Path h (h a) bs z))"
apply(case_tac as)
-apply fastsimp
-apply fastsimp
+apply fastforce
+apply fastforce
done
lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
@@ -110,12 +110,12 @@
lemma List_hd_not_in_tl[simp]: "List h (h a) as \<Longrightarrow> a \<notin> set as"
apply (clarsimp simp add:in_set_conv_decomp)
apply(frule List_app[THEN iffD1])
-apply(fastsimp dest: List_unique)
+apply(fastforce dest: List_unique)
done
lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
apply(induct as, simp)
-apply(fastsimp dest:List_hd_not_in_tl)
+apply(fastforce dest:List_hd_not_in_tl)
done
subsection "Functional abstraction"
@@ -152,7 +152,7 @@
lemma list_Ref_conv[simp]:
"\<lbrakk> a \<noteq> Null; islist h (h a) \<rbrakk> \<Longrightarrow> list h a = a # list h (h a)"
apply(insert List_Ref[of _ h])
-apply(fastsimp simp:List_conv_islist_list)
+apply(fastforce simp:List_conv_islist_list)
done
lemma [simp]: "islist h (h a) \<Longrightarrow> a \<notin> set(list h (h a))"
@@ -187,8 +187,8 @@
DO r := p; p := p^.tl; r^.tl := q; q := r OD
{List tl q (rev Ps @ Qs)}"
apply vcg_simp
- apply fastsimp
- apply(fastsimp intro:notin_List_update[THEN iffD2])
+ apply fastforce
+ apply(fastforce intro:notin_List_update[THEN iffD2])
(* explicily:
apply clarify
apply(rename_tac ps qs)
@@ -199,7 +199,7 @@
apply(rule_tac x = "p#qs" in exI)
apply simp
*)
-apply fastsimp
+apply fastforce
done
@@ -216,19 +216,19 @@
fix tl p q r
assume "List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}"
thus "\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
- rev ps @ qs = rev Ps @ Qs" by fastsimp
+ rev ps @ qs = rev Ps @ Qs" by fastforce
next
fix tl p q r
assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
rev ps @ qs = rev Ps @ Qs) \<and> p \<noteq> Null"
(is "(\<exists>ps qs. ?I ps qs) \<and> _")
then obtain ps qs where I: "?I ps qs \<and> p \<noteq> Null" by fast
- then obtain ps' where "ps = p # ps'" by fastsimp
+ then obtain ps' where "ps = p # ps'" by fastforce
hence "List (tl(p := q)) (p^.tl) ps' \<and>
List (tl(p := q)) p (p#qs) \<and>
set ps' \<inter> set (p#qs) = {} \<and>
rev ps' @ (p#qs) = rev Ps @ Qs"
- using I by fastsimp
+ using I by fastforce
thus "\<exists>ps' qs'. List (tl(p := q)) (p^.tl) ps' \<and>
List (tl(p := q)) p qs' \<and>
set ps' \<inter> set qs' = {} \<and>
@@ -237,7 +237,7 @@
fix tl p q r
assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> Null"
- thus "List tl q (rev Ps @ Qs)" by fastsimp
+ thus "List tl q (rev Ps @ Qs)" by fastforce
qed
@@ -276,9 +276,9 @@
apply vcg_simp
apply(case_tac "p = Null")
apply clarsimp
- apply fastsimp
+ apply fastforce
apply clarsimp
- apply fastsimp
+ apply fastforce
apply clarsimp
done
@@ -293,7 +293,7 @@
{p = X}"
apply vcg_simp
apply blast
- apply fastsimp
+ apply fastforce
apply clarsimp
done
@@ -311,7 +311,7 @@
apply(erule converse_rtranclE)
apply simp
apply(simp)
-apply(fastsimp elim:converse_rtranclE)
+apply(fastforce elim:converse_rtranclE)
done
@@ -350,7 +350,7 @@
{List tl r (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}"
apply vcg_simp
-apply (fastsimp)
+apply (fastforce)
apply clarsimp
apply(rule conjI)
@@ -359,7 +359,7 @@
apply(rule_tac x = "rs @ [s]" in exI)
apply simp
apply(rule_tac x = "bs" in exI)
-apply (fastsimp simp:eq_sym_conv)
+apply (fastforce simp:eq_sym_conv)
apply clarsimp
apply(rule conjI)
@@ -428,7 +428,7 @@
{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 fastsimp
+apply fastforce
done
--- a/src/HOL/Hoare/SchorrWaite.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Hoare/SchorrWaite.thy Mon Sep 12 07:55:43 2011 +0200
@@ -295,20 +295,20 @@
proof
show "?L \<subseteq> ?R"
proof (rule still_reachable)
- show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B" by(fastsimp simp:addrs_def relS_def rel_def addr_p_eq
+ show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B" by(fastforce simp:addrs_def relS_def rel_def addr_p_eq
intro:oneStep_reachable Image_iff[THEN iffD2])
show "\<forall>(x,y) \<in> ?Ra-?Rb. y \<in> (?Rb\<^sup>* `` addrs ?B)" by (clarsimp simp:relS_def)
- (fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd1)
+ (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
qed
show "?R \<subseteq> ?L"
proof (rule still_reachable)
show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
- by(fastsimp simp:addrs_def rel_defs addr_p_eq
+ by(fastforce simp:addrs_def rel_defs addr_p_eq
intro:oneStep_reachable Image_iff[THEN iffD2])
next
show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
by (clarsimp simp:relS_def)
- (fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd2)
+ (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd2)
qed
qed
with i3 have poI3: "R = reachable ?Rb ?B" by (simp add:reachable_def)
@@ -326,10 +326,10 @@
have rewrite: "\<forall>s\<in>set stack_tl. (r(p \<rightarrow> t)) s = r s"
by (auto simp add:p_notin_stack_tl intro:fun_upd_other)
show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
- by (fastsimp cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
+ by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
by (clarsimp simp:restr_def relS_def)
- (fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd1)
+ (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
qed
-- "We now bring a term from the right to the left of the subset relation."
hence subset: "?Ra\<^sup>* `` addrs ?A - ?Rb\<^sup>* `` addrs ?T \<subseteq> ?Rb\<^sup>* `` addrs ?B"
@@ -404,16 +404,16 @@
have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B"
proof (rule still_reachable_eq)
show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B"
- by(fastsimp simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
+ by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
next
show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
- by(fastsimp simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
+ by(fastforce simp:addrs_def rel_defs addr_p_eq intro:oneStep_reachable Image_iff[THEN iffD2])
next
show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)"
- by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
+ by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
next
show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
- by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
+ by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
qed
with i3
have swI3: "?swI3" by (simp add:reachable_def)
@@ -428,10 +428,10 @@
have rewrite: "(\<forall>s\<in>set stack_tl. (r(addr p := l(addr p))) s = r s)"
by (auto simp add:p_notin_stack_tl intro:fun_upd_other)
show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
- by (fastsimp cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
+ by (fastforce cong:map_cong simp:stack_eq addrs_def rewrite intro:self_reachable)
next
show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
- by (clarsimp simp:relS_def restr_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
+ by (clarsimp simp:relS_def restr_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd1)
qed
then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B"
by blast
@@ -501,16 +501,16 @@
have "?Ra\<^sup>* `` addrs ?A = ?Rb\<^sup>* `` addrs ?B"
proof (rule still_reachable_eq)
show "addrs ?A \<subseteq> ?Rb\<^sup>* `` addrs ?B"
- by(fastsimp simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
+ by(fastforce simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
next
show "addrs ?B \<subseteq> ?Ra\<^sup>* `` addrs ?A"
- by(fastsimp simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
+ by(fastforce simp:addrs_def rel_defs addr_t_eq intro:oneStep_reachable Image_iff[THEN iffD2])
next
show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``addrs ?B)"
- by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def dest:rel_upd1)
+ by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def dest:rel_upd1)
next
show "\<forall>(x, y)\<in>?Rb-?Ra. y\<in>(?Ra\<^sup>*``addrs ?A)"
- by (clarsimp simp:relS_def) (fastsimp simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
+ by (clarsimp simp:relS_def) (fastforce simp add:rel_def Image_iff addrs_def fun_upd_apply dest:rel_upd2)
qed
with i3
have puI3: "?puI3" by (simp add:reachable_def)
@@ -523,11 +523,11 @@
have "?Ra\<^sup>*``addrs ?A \<subseteq> ?Rb\<^sup>*``(addrs ?B \<union> addrs ?T)"
proof (rule still_reachable)
show "addrs ?A \<subseteq> ?Rb\<^sup>* `` (addrs ?B \<union> addrs ?T)"
- by (fastsimp simp:new_stack_eq addrs_def intro:self_reachable)
+ by (fastforce simp:new_stack_eq addrs_def intro:self_reachable)
next
show "\<forall>(x, y)\<in>?Ra-?Rb. y\<in>(?Rb\<^sup>*``(addrs ?B \<union> addrs ?T))"
by (clarsimp simp:relS_def new_stack_eq restr_un restr_upd)
- (fastsimp simp add:rel_def Image_iff restr_def addrs_def fun_upd_apply addr_t_eq dest:rel_upd3)
+ (fastforce simp add:rel_def Image_iff restr_def addrs_def fun_upd_apply addr_t_eq dest:rel_upd3)
qed
then have subset: "?Ra\<^sup>*``addrs ?A - ?Rb\<^sup>*``addrs ?T \<subseteq> ?Rb\<^sup>*``addrs ?B"
by blast
@@ -537,7 +537,7 @@
assume a: "x \<in> R \<and> \<not> ?new_m x"
have xDisj: "x=(addr t) \<or> x\<noteq>(addr t)" by simp
with i4 a have inc: "x \<in> ?Ra\<^sup>*``addrs ?A"
- by (fastsimp simp:addr_t_eq addrs_def reachable_def intro:self_reachable)
+ by (fastforce simp:addr_t_eq addrs_def reachable_def intro:self_reachable)
have exc: "x \<notin> ?Rb\<^sup>*`` addrs ?T"
using xDisj a n_m_addr_t
by (clarsimp simp add:addrs_def addr_t_eq)
--- a/src/HOL/Hoare/SepLogHeap.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Hoare/SepLogHeap.thy Mon Sep 12 07:55:43 2011 +0200
@@ -72,7 +72,7 @@
lemma List_hd_not_in_tl[simp]: "List h b as \<Longrightarrow> h a = Some b \<Longrightarrow> a \<notin> set as"
apply (clarsimp simp add:in_set_conv_decomp)
apply(frule List_app[THEN iffD1])
-apply(fastsimp dest: List_unique)
+apply(fastforce dest: List_unique)
done
lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
--- a/src/HOL/Hoare/Separation.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Hoare/Separation.thy Mon Sep 12 07:55:43 2011 +0200
@@ -191,7 +191,7 @@
apply vcg
apply(simp_all add: star_def ortho_def singl_def)
-apply fastsimp
+apply fastforce
apply (clarsimp simp add:List_non_null)
apply(rename_tac ps')
@@ -214,7 +214,7 @@
apply(simp)
apply fast
-apply(fastsimp)
+apply(fastforce)
done
end
--- a/src/HOL/Hoare_Parallel/OG_Examples.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Mon Sep 12 07:55:43 2011 +0200
@@ -192,7 +192,7 @@
--{* 6 subgoals left *}
prefer 6
apply(erule_tac x=i in allE)
-apply fastsimp
+apply fastforce
--{* 5 subgoals left *}
prefer 5
apply(case_tac [!] "j=k")
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy Mon Sep 12 07:55:43 2011 +0200
@@ -286,7 +286,7 @@
apply force
apply(rule Basic)
apply force
- apply fastsimp
+ apply fastforce
apply force
apply force
apply(rule Basic)
--- a/src/HOL/IMP/AbsInt0.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/IMP/AbsInt0.thy Mon Sep 12 07:55:43 2011 +0200
@@ -36,7 +36,7 @@
lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
proof(induct c arbitrary: s t S0)
- case SKIP thus ?case by fastsimp
+ case SKIP thus ?case by fastforce
next
case Assign thus ?case
by (auto simp: lookup_update aval'_sound)
--- a/src/HOL/IMP/AbsInt0_fun.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/IMP/AbsInt0_fun.thy Mon Sep 12 07:55:43 2011 +0200
@@ -71,7 +71,7 @@
let ?F = "lift f x0"
obtain k where "pfp_above f x0 = (?F^^k) x0"
using pfp_funpow `pfp_above f x0 \<noteq> Top`
- by(fastsimp simp add: pfp_above_def)
+ by(fastforce simp add: pfp_above_def)
moreover
{ fix n have "(?F^^n) x0 \<sqsubseteq> p"
proof(induct n)
@@ -97,7 +97,7 @@
let ?p = "pfp_above f x0"
obtain k where 1: "?p = ((f\<up>x0)^^k) x0"
using pfp_funpow `?p \<noteq> Top`
- by(fastsimp simp add: pfp_above_def)
+ by(fastforce simp add: pfp_above_def)
thus ?thesis using chain mono by simp
qed
@@ -174,7 +174,7 @@
lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
proof(induct c arbitrary: s t S0)
- case SKIP thus ?case by fastsimp
+ case SKIP thus ?case by fastforce
next
case Assign thus ?case by (auto simp: aval'_sound)
next
--- a/src/HOL/IMP/AbsInt1.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/IMP/AbsInt1.thy Mon Sep 12 07:55:43 2011 +0200
@@ -171,12 +171,12 @@
lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> t <:: AI c S"
proof(induct c arbitrary: s t S)
- case SKIP thus ?case by fastsimp
+ case SKIP thus ?case by fastforce
next
case Assign thus ?case
by (auto simp: lookup_update aval'_sound)
next
- case Semi thus ?case by fastsimp
+ case Semi thus ?case by fastforce
next
case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound)
next
--- a/src/HOL/IMP/Comp_Rev.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/IMP/Comp_Rev.thy Mon Sep 12 07:55:43 2011 +0200
@@ -41,7 +41,7 @@
lemma exec_Suc [trans]:
"\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^(Suc n) c''"
- by (fastsimp simp del: split_paired_Ex)
+ by (fastforce simp del: split_paired_Ex)
lemma exec_exec_n:
"P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> \<exists>n. P \<turnstile> c \<rightarrow>^n c'"
@@ -118,7 +118,7 @@
{ fix p assume "p \<in> ?x \<or> p \<in> ?xs"
hence "p \<in> succs (x#xs) n"
proof
- assume "p \<in> ?x" thus ?thesis by (fastsimp simp: succs_def)
+ assume "p \<in> ?x" thus ?thesis by (fastforce simp: succs_def)
next
assume "p \<in> ?xs"
then obtain i where "?isuccs p xs (1+n) i"
@@ -138,7 +138,7 @@
lemma succs_shift:
"(p - n \<in> succs P 0) = (p \<in> succs P n)"
- by (fastsimp simp: succs_def isuccs_def split: instr.split)
+ by (fastforce simp: succs_def isuccs_def split: instr.split)
lemma inj_op_plus [simp]:
"inj (op + (i::int))"
@@ -227,7 +227,7 @@
case (Semi c1 c2)
from Semi.prems
show ?case
- by (fastsimp dest: Semi.hyps [THEN subsetD])
+ by (fastforce dest: Semi.hyps [THEN subsetD])
next
case (If b c1 c2)
from If.prems
@@ -289,7 +289,7 @@
{ assume "j0 \<in> {0 ..< isize c}"
with j0 j rest c
have ?case
- by (fastsimp dest!: Suc.hyps intro!: exec_Suc)
+ by (fastforce dest!: Suc.hyps intro!: exec_Suc)
} moreover {
assume "j0 \<notin> {0 ..< isize c}"
moreover
@@ -298,7 +298,7 @@
ultimately
have "j0 \<in> exits c" by (simp add: exits_def)
with c j0 rest
- have ?case by fastsimp
+ have ?case by fastforce
}
ultimately
show ?case by cases
@@ -352,7 +352,7 @@
by (rule exec1_drop_left)
also
then have "i' - isize P \<in> succs P' 0"
- by (fastsimp dest!: succs_iexec1)
+ by (fastforce dest!: succs_iexec1)
with `exits P' \<subseteq> {0..}`
have "isize P \<le> i'" by (auto simp: exits_def)
from rest this `exits P' \<subseteq> {0..}`
@@ -383,7 +383,7 @@
P' \<turnstile> (0,s'',stk'') \<rightarrow>^k2 (j - isize P, s', stk')"
proof (cases "P")
case Nil with exec
- show ?thesis by fastsimp
+ show ?thesis by fastforce
next
case Cons
hence "0 < isize P" by simp
@@ -398,7 +398,7 @@
then obtain j0 where "j = isize P + j0" ..
ultimately
show ?thesis using exits
- by (fastsimp dest: exec_n_drop_left)
+ by (fastforce dest: exec_n_drop_left)
qed
@@ -424,7 +424,7 @@
"[ADD] \<turnstile> (0,s2,stk2) \<rightarrow>^n3 (1, s', stk')"
by (auto dest!: exec_n_split_full)
- thus ?case by (fastsimp dest: Plus.hyps simp: exec_n_simps)
+ thus ?case by (fastforce dest: Plus.hyps simp: exec_n_simps)
qed (auto simp: exec_n_simps)
lemma bcomp_split:
@@ -435,7 +435,7 @@
(i' = isize (bcomp b c i) \<or> i' = i + isize (bcomp b c i)) \<and>
bcomp b c i @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^m (j, s', stk') \<and>
n = k + m"
- using assms by (cases "bcomp b c i = []") (fastsimp dest!: exec_n_drop_right)+
+ using assms by (cases "bcomp b c i = []") (fastforce dest!: exec_n_drop_right)+
lemma bcomp_exec_n [dest]:
assumes "bcomp b c j \<turnstile> (0, s, stk) \<rightarrow>^n (i, s', stk')"
@@ -448,7 +448,7 @@
next
case (Not b)
from Not.prems show ?case
- by (fastsimp dest!: Not.hyps)
+ by (fastforce dest!: Not.hyps)
next
case (And b1 b2)
@@ -469,7 +469,7 @@
by (auto dest!: And.hyps)
with b2 j
show ?case
- by (fastsimp dest!: And.hyps simp: exec_n_end split: split_if_asm)
+ by (fastforce dest!: And.hyps simp: exec_n_end split: split_if_asm)
next
case Less
thus ?case by (auto dest!: exec_n_split_full simp: exec_n_simps) (* takes time *)
@@ -490,10 +490,10 @@
next
case (Assign x a)
thus ?case
- by simp (fastsimp dest!: exec_n_split_full simp: exec_n_simps)
+ by simp (fastforce dest!: exec_n_split_full simp: exec_n_simps)
next
case (Semi c1 c2)
- thus ?case by (fastsimp dest!: exec_n_split_full)
+ thus ?case by (fastforce dest!: exec_n_split_full)
next
case (If b c1 c2)
note If.hyps [dest!]
@@ -518,14 +518,14 @@
"ccomp c1@JMP (isize (ccomp c2))#ccomp c2 \<turnstile>
(if bval b s then 0 else isize (ccomp c1)+1, s, stk) \<rightarrow>^m
(1 + isize (ccomp c1) + isize (ccomp c2), t, stk')"
- by (fastsimp dest: exec_n_drop_left simp: exits_Cons isuccs_def algebra_simps)
+ by (fastforce dest: exec_n_drop_left simp: exits_Cons isuccs_def algebra_simps)
show ?case
proof (cases "bval b s")
case True with cs'
show ?thesis
by simp
- (fastsimp dest: exec_n_drop_right
+ (fastforce dest: exec_n_drop_right
split: split_if_asm simp: exec_n_simps)
next
case False with cs'
@@ -545,7 +545,7 @@
with "1.prems"
have ?case
by simp
- (fastsimp dest!: bcomp_exec_n bcomp_split
+ (fastforce dest!: bcomp_exec_n bcomp_split
simp: exec_n_simps)
} moreover {
assume b: "bval b s"
@@ -558,7 +558,7 @@
obtain k where
cs: "?cs \<turnstile> (isize ?bs, s, stk) \<rightarrow>^k (isize ?cs, t, stk')" and
k: "k \<le> n"
- by (fastsimp dest!: bcomp_split)
+ by (fastforce dest!: bcomp_split)
have ?case
proof cases
--- a/src/HOL/IMP/Compiler.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/IMP/Compiler.thy Mon Sep 12 07:55:43 2011 +0200
@@ -94,7 +94,7 @@
subsection{* Verification infrastructure *}
lemma exec_trans: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''"
- by (induct rule: exec.induct) fastsimp+
+ by (induct rule: exec.induct) fastforce+
inductive_cases iexec1_cases [elim!]:
"LOADI n \<turnstile>i c \<rightarrow> c'"
@@ -131,7 +131,7 @@
by auto
lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
- by (induct rule: exec.induct) (fastsimp intro: exec1_appendR)+
+ by (induct rule: exec.induct) (fastforce intro: exec1_appendR)+
lemma iexec1_shiftI:
assumes "X \<turnstile>i (i,s,stk) \<rightarrow> (i',s',stk')"
@@ -201,7 +201,7 @@
lemma acomp_correct[intro]:
"acomp a \<turnstile> (0,s,stk) \<rightarrow>* (isize(acomp a),s,aval a s#stk)"
- by (induct a arbitrary: stk) fastsimp+
+ by (induct a arbitrary: stk) fastforce+
fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where
"bcomp (B bv) c n = (if bv=c then [JMP n] else [])" |
@@ -224,14 +224,14 @@
(0,s,stk) \<rightarrow>* (isize(bcomp b c n) + (if c = bval b s then n else 0),s,stk)"
proof(induct b arbitrary: c n m)
case Not
- from Not(1)[where c="~c"] Not(2) show ?case by fastsimp
+ from Not(1)[where c="~c"] Not(2) show ?case by fastforce
next
case (And b1 b2)
from And(1)[of "if c then isize (bcomp b2 c n) else isize (bcomp b2 c n) + n"
"False"]
And(2)[of n "c"] And(3)
- show ?case by fastsimp
-qed fastsimp+
+ show ?case by fastforce
+qed fastforce+
fun ccomp :: "com \<Rightarrow> instr list" where
"ccomp SKIP = []" |
@@ -258,15 +258,15 @@
"(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (isize(ccomp c),t,stk)"
proof(induct arbitrary: stk rule: big_step_induct)
case (Assign x a s)
- show ?case by (fastsimp simp:fun_upd_def cong: if_cong)
+ show ?case by (fastforce simp:fun_upd_def cong: if_cong)
next
case (Semi c1 s1 s2 c2 s3)
let ?cc1 = "ccomp c1" let ?cc2 = "ccomp c2"
have "?cc1 @ ?cc2 \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cc1,s2,stk)"
- using Semi.hyps(2) by fastsimp
+ using Semi.hyps(2) by fastforce
moreover
have "?cc1 @ ?cc2 \<turnstile> (isize ?cc1,s2,stk) \<rightarrow>* (isize(?cc1 @ ?cc2),s3,stk)"
- using Semi.hyps(4) by fastsimp
+ using Semi.hyps(4) by fastforce
ultimately show ?case by simp (blast intro: exec_trans)
next
case (WhileTrue b s1 c s2 s3)
@@ -274,13 +274,13 @@
let ?cb = "bcomp b False (isize ?cc + 1)"
let ?cw = "ccomp(WHILE b DO c)"
have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)"
- using WhileTrue(1,3) by fastsimp
+ using WhileTrue(1,3) by fastforce
moreover
have "?cw \<turnstile> (isize ?cb + isize ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
- by fastsimp
+ by fastforce
moreover
have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue(5))
ultimately show ?case by(blast intro: exec_trans)
-qed fastsimp+
+qed fastforce+
end
--- a/src/HOL/IMP/Def_Ass_Sound_Small.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/IMP/Def_Ass_Sound_Small.thy Mon Sep 12 07:55:43 2011 +0200
@@ -14,7 +14,7 @@
then obtain bv where "bval b s = Some bv" by (auto dest!:bval_Some)
then show ?case
by(cases bv)(auto intro: small_step.IfTrue small_step.IfFalse)
-qed (fastsimp intro: small_step.intros)+
+qed (fastforce intro: small_step.intros)+
lemma D_mono: "D A c M \<Longrightarrow> A \<subseteq> A' \<Longrightarrow> EX M'. D A' c M' & M <= M'"
proof (induct c arbitrary: A A' M)
@@ -26,7 +26,7 @@
with If.hyps `A \<subseteq> A'` obtain M1' M2'
where "D A' c1 M1'" "D A' c2 M2'" and "M1 \<subseteq> M1'" "M2 \<subseteq> M2'" by metis
hence "D A' (IF b THEN c1 ELSE c2) (M1' \<inter> M2')" and "M \<subseteq> M1' \<inter> M2'"
- using `vars b \<subseteq> A` `A \<subseteq> A'` `M = M1 \<inter> M2` by(fastsimp intro: D.intros)+
+ using `vars b \<subseteq> A` `A \<subseteq> A'` `M = M1 \<inter> M2` by(fastforce intro: D.intros)+
thus ?case by metis
next
case While thus ?case by auto (metis D.intros(5) subset_trans)
--- a/src/HOL/IMP/Fold.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/IMP/Fold.thy Mon Sep 12 07:55:43 2011 +0200
@@ -56,7 +56,7 @@
lemma approx_merge:
"approx t1 s \<or> approx t2 s \<Longrightarrow> approx (merge t1 t2) s"
- by (fastsimp simp: merge_def approx_def)
+ by (fastforce simp: merge_def approx_def)
lemma approx_map_le:
"approx t2 s \<Longrightarrow> t1 \<subseteq>\<^sub>m t2 \<Longrightarrow> approx t1 s"
@@ -385,7 +385,7 @@
IF Fold.bsimp_const b t THEN bfold c1 t ELSE bfold c2 t"
by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def)
thus ?case using If
- by (fastsimp simp: bvalsimp_const_B split: bexp.splits bool.splits
+ by (fastforce simp: bvalsimp_const_B split: bexp.splits bool.splits
intro: equiv_up_to_trans)
next
case (While b c)
--- a/src/HOL/IMP/HoareT.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/IMP/HoareT.thy Mon Sep 12 07:55:43 2011 +0200
@@ -70,7 +70,7 @@
apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps)
apply clarsimp
apply arith
-apply fastsimp
+apply fastforce
apply(rule Semi)
prefer 2
apply(rule Assign)
@@ -95,7 +95,7 @@
qed
next
case If thus ?case by auto blast
-qed fastsimp+
+qed fastforce+
text{*
--- a/src/HOL/IMP/Hoare_Examples.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/IMP/Hoare_Examples.thy Mon Sep 12 07:55:43 2011 +0200
@@ -59,8 +59,8 @@
prefer 2
apply(rule Assign)
apply(rule Assign')
-apply(fastsimp simp: atLeastAtMostPlus1_int_conv algebra_simps)
-apply(fastsimp)
+apply(fastforce simp: atLeastAtMostPlus1_int_conv algebra_simps)
+apply(fastforce)
apply(rule Semi)
prefer 2
apply(rule Assign)
--- a/src/HOL/IMP/Sem_Equiv.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/IMP/Sem_Equiv.thy Mon Sep 12 07:55:43 2011 +0200
@@ -107,7 +107,7 @@
next
case WhileFalse
thus ?case by (auto simp: bequiv_up_to_def)
-qed (fastsimp simp: equiv_up_to_def bequiv_up_to_def hoare_valid_def)+
+qed (fastforce simp: equiv_up_to_def bequiv_up_to_def hoare_valid_def)+
lemma bequiv_context_subst:
"P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (P s \<and> bval b s) = (P s \<and> bval b' s)"
@@ -128,7 +128,7 @@
lemma equiv_up_to_while_weak:
"P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> \<Turnstile> {P} c {P} \<Longrightarrow>
P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
- by (fastsimp elim!: equiv_up_to_while equiv_up_to_weaken
+ by (fastforce elim!: equiv_up_to_while equiv_up_to_weaken
simp: hoare_valid_def)
lemma equiv_up_to_if:
@@ -139,7 +139,7 @@
lemma equiv_up_to_if_weak:
"P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> d \<sim> d' \<Longrightarrow>
P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
- by (fastsimp elim!: equiv_up_to_if equiv_up_to_weaken)
+ by (fastforce elim!: equiv_up_to_if equiv_up_to_weaken)
lemma equiv_up_to_if_True [intro!]:
"(\<And>s. P s \<Longrightarrow> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c1"
--- a/src/HOL/IMP/Types.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/IMP/Types.thy Mon Sep 12 07:55:43 2011 +0200
@@ -120,7 +120,7 @@
lemma apreservation:
"\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> taval a s v \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> type v = \<tau>"
apply(induct arbitrary: v rule: atyping.induct)
-apply (fastsimp simp: styping_def)+
+apply (fastforce simp: styping_def)+
done
lemma aprogress: "\<Gamma> \<turnstile> a : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s \<Longrightarrow> \<exists>v. taval a s v"
@@ -131,11 +131,11 @@
proof (cases v1)
case Iv
with Plus_ty(1,3,5) v show ?thesis
- by(fastsimp intro: taval.intros(4) dest!: apreservation)
+ by(fastforce intro: taval.intros(4) dest!: apreservation)
next
case Rv
with Plus_ty(1,3,5) v show ?thesis
- by(fastsimp intro: taval.intros(5) dest!: apreservation)
+ by(fastforce intro: taval.intros(5) dest!: apreservation)
qed
qed (auto intro: taval.intros)
@@ -148,11 +148,11 @@
proof (cases v1)
case Iv
with Less_ty v show ?thesis
- by (fastsimp intro!: tbval.intros(4) dest!:apreservation)
+ by (fastforce intro!: tbval.intros(4) dest!:apreservation)
next
case Rv
with Less_ty v show ?thesis
- by (fastsimp intro!: tbval.intros(5) dest!:apreservation)
+ by (fastforce intro!: tbval.intros(5) dest!:apreservation)
qed
qed (auto intro: tbval.intros)
--- a/src/HOL/IMP/VC.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/IMP/VC.thy Mon Sep 12 07:55:43 2011 +0200
@@ -100,7 +100,7 @@
show ?case (is "\<exists>ac. ?C ac")
proof
show "?C(Asemi ac1 ac2)"
- using ih1 ih2 by (fastsimp elim!: pre_mono vc_mono)
+ using ih1 ih2 by (fastforce elim!: pre_mono vc_mono)
qed
next
case (If P b c1 Q c2)
--- a/src/HOL/Imperative_HOL/Mrec.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Imperative_HOL/Mrec.thy Mon Sep 12 07:55:43 2011 +0200
@@ -95,11 +95,11 @@
from mrec have "P x h (snd (the (mrec x h))) (fst (the (mrec x h)))"
proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom])
case (1 x h)
- obtain rr h' where "the (mrec x h) = (rr, h')" by fastsimp
+ obtain rr h' where "the (mrec x h) = (rr, h')" by fastforce
show ?case
proof (cases "execute (f x) h")
case (Some result)
- then obtain a h1 where exec_f: "execute (f x) h = Some (a, h1)" by fastsimp
+ then obtain a h1 where exec_f: "execute (f x) h = Some (a, h1)" by fastforce
note Inl' = this
show ?thesis
proof (cases a)
@@ -112,7 +112,7 @@
show ?thesis
proof (cases "mrec b h1")
case (Some result)
- then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastsimp
+ then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastforce
moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))"
apply (intro 1(2))
apply (auto simp add: Inr Inl')
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Mon Sep 12 07:55:43 2011 +0200
@@ -105,7 +105,7 @@
unfolding part1.simps[of a l r p]
by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
from rec_condition have "l \<le> r - 1" by arith
- from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
+ from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastforce
qed
qed
qed
@@ -128,7 +128,7 @@
case False (* recursive case *)
with cr 1 show ?thesis
unfolding part1.simps [of a l r p] swap_def
- by (auto elim!: effect_bindE effect_ifE effect_nthE effect_returnE effect_updE) fastsimp
+ by (auto elim!: effect_bindE effect_ifE effect_nthE effect_returnE effect_updE) fastforce
qed
qed
@@ -158,7 +158,7 @@
unfolding part1.simps[of a l r p]
by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
from 1(1)[OF rec_condition True rec1]
- show ?thesis by fastsimp
+ show ?thesis by fastforce
next
case False
with rec_condition cr
@@ -170,7 +170,7 @@
"\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h a ! i = Array.get h1 a ! i"
unfolding swap_def
by (elim effect_bindE effect_nthE effect_updE effect_returnE) auto
- with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
+ with 1(2) [OF rec_condition False rec2] show ?thesis by fastforce
qed
qed
qed
@@ -205,7 +205,7 @@
unfolding part1.simps[of a l r p]
by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
from True part_outer_remains[OF rec1] have a_l: "Array.get h' a ! l \<le> p"
- by fastsimp
+ by fastforce
have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
with 1(1)[OF False True rec1] a_l show ?thesis
by auto
@@ -220,7 +220,7 @@
unfolding swap_def
by (auto simp add: Array.length_def elim!: effect_bindE effect_nthE effect_updE effect_returnE)
with part_outer_remains [OF rec2] lr have a_r: "Array.get h' a ! r \<ge> p"
- by fastsimp
+ by fastforce
have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
with 1(2)[OF lr False rec2] a_r show ?thesis
by auto
@@ -268,7 +268,7 @@
proof -
from assms part_outer_remains part_returns_index_in_bounds show ?thesis
unfolding partition.simps swap_def
- by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) fastsimp
+ by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) fastforce
qed
lemma partition_returns_index_in_bounds:
@@ -311,7 +311,7 @@
note middle_in_bounds = part_returns_index_in_bounds[OF part this]
from part_outer_remains[OF part] `l < r`
have "Array.get h a ! r = Array.get h1 a ! r"
- by fastsimp
+ by fastforce
with swap
have right_remains: "Array.get h a ! r = Array.get h' a ! rs"
unfolding swap_def
@@ -328,7 +328,7 @@
have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
with part_partitions[OF part] right_remains True
- have "Array.get h1 a ! i \<le> Array.get h' a ! rs" by fastsimp
+ have "Array.get h1 a ! i \<le> Array.get h' a ! rs" by fastforce
with i_props h'_def in_bounds have "Array.get h' a ! i \<le> Array.get h' a ! rs"
unfolding Array.update_def Array.length_def by simp
}
@@ -345,15 +345,15 @@
have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
from part_partitions[OF part] rs_equals right_remains i_is
have "Array.get h' a ! rs \<le> Array.get h1 a ! i"
- by fastsimp
- with i_props h'_def show ?thesis by fastsimp
+ by fastforce
+ with i_props h'_def show ?thesis by fastforce
next
assume i_is: "rs < i \<and> i = r"
with rs_equals have "Suc middle \<noteq> r" by arith
with middle_in_bounds `l < r` have "Suc middle \<le> r - 1" by arith
with part_partitions[OF part] right_remains
have "Array.get h' a ! rs \<le> Array.get h1 a ! (Suc middle)"
- by fastsimp
+ by fastforce
with i_is True rs_equals right_remains h'_def
show ?thesis using in_bounds
unfolding Array.update_def Array.length_def
@@ -370,7 +370,7 @@
with swap_length_remains in_bounds middle_in_bounds rs_equals
have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
from part_partitions[OF part] rs_equals right_remains i_is_left
- have "Array.get h1 a ! i \<le> Array.get h' a ! rs" by fastsimp
+ have "Array.get h1 a ! i \<le> Array.get h' a ! rs" by fastforce
with i_props h'_def have "Array.get h' a ! i \<le> Array.get h' a ! rs"
unfolding Array.update_def by simp
}
@@ -386,8 +386,8 @@
have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
from part_partitions[OF part] rs_equals right_remains i_is
have "Array.get h' a ! rs \<le> Array.get h1 a ! i"
- by fastsimp
- with i_props h'_def show ?thesis by fastsimp
+ by fastforce
+ with i_props h'_def show ?thesis by fastforce
next
assume i_is: "i = r"
from i_is False rs_equals right_remains h'_def
@@ -469,7 +469,7 @@
assume pivot: "l \<le> p \<and> p \<le> r"
assume i_outer: "i < l \<or> r < i"
from partition_outer_remains [OF part True] i_outer
- have "Array.get h a !i = Array.get h1 a ! i" by fastsimp
+ have "Array.get h a !i = Array.get h1 a ! i" by fastforce
moreover
with 1(1) [OF True pivot qs1] pivot i_outer
have "Array.get h1 a ! i = Array.get h2 a ! i" by auto
@@ -579,7 +579,7 @@
unfolding Array.length_def subarray_def by auto
with length_remains[OF effect] have "sorted (Array.get h' a)"
unfolding Array.length_def by simp
- with quicksort_permutes [OF effect] properties_for_sort show ?thesis by fastsimp
+ with quicksort_permutes [OF effect] properties_for_sort show ?thesis by fastforce
qed
subsection {* No Errors in quicksort *}
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Mon Sep 12 07:55:43 2011 +0200
@@ -78,7 +78,7 @@
by (auto elim: effect_elims)
from swp rev 1 True show ?thesis
unfolding swap.simps
- by (elim effect_elims) fastsimp
+ by (elim effect_elims) fastforce
next
case False
with 1[unfolded rev.simps[of a i j]]
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Sep 12 07:55:43 2011 +0200
@@ -238,7 +238,7 @@
shows "p \<notin> set rs"
proof (rule ccontr)
assume a: "\<not> (p \<notin> set rs)"
- from this obtain as bs where split:"rs = as @ p # bs" by (fastsimp dest: split_list)
+ from this obtain as bs where split:"rs = as @ p # bs" by (fastforce dest: split_list)
with assms obtain q where "refs_of h q (p # bs)" by (fast dest: refs_of_append)
with assms split show "False"
by (cases q,auto dest: refs_of_is_fun)
@@ -255,7 +255,7 @@
lemma refs_of'_distinct: "refs_of' h p rs \<Longrightarrow> distinct rs"
unfolding refs_of'_def'
- by (fastsimp simp add: refs_of_distinct refs_of_next)
+ by (fastforce simp add: refs_of_distinct refs_of_next)
subsection {* Interaction of these predicates with our heap transitions *}
@@ -272,7 +272,7 @@
next
case (Node a ref)
from Cons(2) Node obtain rs' where 1: "refs_of h (Ref.get h ref) rs'" and rs_rs': "rs = ref # rs'" by auto
- from Cons(3) rs_rs' have "ref \<noteq> p" by fastsimp
+ from Cons(3) rs_rs' have "ref \<noteq> p" by fastforce
hence ref_eq: "Ref.get (Ref.set p v h) ref = (Ref.get h ref)" by (auto simp add: Ref.get_set_neq)
from rs_rs' Cons(3) have 2: "p \<notin> set rs'" by simp
from Cons.hyps[OF 1 2] Node ref_eq show ?thesis by simp
@@ -290,7 +290,7 @@
next
case (Node a ref)
from Cons(2) Node obtain rs' where 1: "refs_of h (Ref.get h ref) rs'" and rs_rs': "rs = ref # rs'" by auto
- from Cons(3) rs_rs' have "ref \<noteq> p" by fastsimp
+ from Cons(3) rs_rs' have "ref \<noteq> p" by fastforce
hence ref_eq: "Ref.get (Ref.set p v h) ref = (Ref.get h ref)" by (auto simp add: Ref.get_set_neq)
from rs_rs' Cons(3) have 2: "p \<notin> set rs'" by simp
from Cons.hyps[OF 1 2] Node ref_eq show ?thesis by auto
@@ -308,7 +308,7 @@
next
case (Node a ref)
from Cons(2) Node have 1:"refs_of (Ref.set p v h) (Ref.get (Ref.set p v h) ref) xs" and x_ref: "x = ref" by auto
- from Cons(3) this have "ref \<noteq> p" by fastsimp
+ from Cons(3) this have "ref \<noteq> p" by fastforce
hence ref_eq: "Ref.get (Ref.set p v h) ref = (Ref.get h ref)" by (auto simp add: Ref.get_set_neq)
from Cons(3) have 2: "p \<notin> set xs" by simp
with Cons.hyps 1 2 Node ref_eq show ?thesis
@@ -395,9 +395,9 @@
from Cons(2-3) Node have ref_eq: "Ref.get h x = Ref.get h' x" by auto
from ref_eq refs_of_next have 1: "refs_of h (Ref.get h' x) xs'" by simp
from Cons(2) Cons(3) have "\<forall>ref \<in> set xs'. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref"
- by fastsimp
+ by fastforce
with Cons(3) 1 have 2: "\<forall>refs. refs_of h (Ref.get h' x) refs \<longrightarrow> (\<forall>ref \<in> set refs. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref)"
- by (fastsimp dest: refs_of_is_fun)
+ by (fastforce dest: refs_of_is_fun)
from Cons.hyps[OF 1 2] have "refs_of h' (Ref.get h' x) xs'" .
with Node show ?case by simp
qed
@@ -410,10 +410,10 @@
proof -
from assms obtain prs where refs:"refs_of h (Ref.get h r) prs" and xs_def: "xs = r # prs"
unfolding refs_of'_def' by auto
- from xs_def assms have x_eq: "Ref.get h r = Ref.get h' r" by fastsimp
+ from xs_def assms have x_eq: "Ref.get h r = Ref.get h' r" by fastforce
from refs assms xs_def have 2: "\<forall>refs. refs_of h (Ref.get h r) refs \<longrightarrow>
(\<forall>ref\<in>set refs. Ref.present h ref \<and> Ref.present h' ref \<and> Ref.get h ref = Ref.get h' ref)"
- by (fastsimp dest: refs_of_is_fun)
+ by (fastforce dest: refs_of_is_fun)
from refs_of_invariant [OF refs 2] xs_def x_eq show ?thesis
unfolding refs_of'_def' by auto
qed
@@ -490,7 +490,7 @@
from refs_unchanged rs'_def have refs_still_present: "\<forall>ref\<in>set rs'. Ref.present h' ref" by auto
from refs_of_invariant[OF rs'_def refs_unchanged] refs_unchanged Node effect_refnew refs_still_present
have sndgoal: "\<forall>rs. refs_of h' r rs \<longrightarrow> (\<forall>ref\<in>set rs. Ref.present h' ref)"
- by (fastsimp elim!: effect_refE dest: refs_of_is_fun)
+ by (fastforce elim!: effect_refE dest: refs_of_is_fun)
from fstgoal sndgoal show ?case ..
qed
@@ -516,7 +516,7 @@
by (auto elim!: effect_bindE)
from make_llist[OF makell] have "list_of h1 r1 xs" ..
from traverse [OF this] trav show ?thesis
- using effect_deterministic by fastsimp
+ using effect_deterministic by fastforce
qed
section {* Proving correctness of in-place reversal *}
@@ -568,8 +568,8 @@
by (auto simp add: rev'.simps [of q p] elim!: effect_bindE effect_lookupE effect_updateE)
from Cons(3) obtain qrs where qrs_def: "refs_of' h q qrs" by (elim list_of'_refs_of')
from Cons(4) obtain prs where prs_def: "refs_of' h p prs" by (elim list_of'_refs_of')
- from qrs_def prs_def Cons(5) have distinct_pointers: "set qrs \<inter> set prs = {}" by fastsimp
- from qrs_def prs_def distinct_pointers refs_of'E have p_notin_qrs: "p \<notin> set qrs" by fastsimp
+ from qrs_def prs_def Cons(5) have distinct_pointers: "set qrs \<inter> set prs = {}" by fastforce
+ from qrs_def prs_def distinct_pointers refs_of'E have p_notin_qrs: "p \<notin> set qrs" by fastforce
from Cons(3) qrs_def this have 1: "list_of' (Ref.set p (Node x q) h) p (x#qs)"
unfolding list_of'_def
apply (simp)
@@ -578,7 +578,7 @@
from list_of'_refs_of'2[OF Cons(4)] p_is_Node prs_def obtain refs where refs_def: "refs_of' h ref refs" and prs_refs: "prs = p # refs"
unfolding refs_of'_def' by auto
from prs_refs prs_def have p_not_in_refs: "p \<notin> set refs"
- by (fastsimp dest!: refs_of'_distinct)
+ by (fastforce dest!: refs_of'_distinct)
with refs_def p_is_Node list_of'_ref have 2: "list_of' (Ref.set p (Node x q) h) ref xs"
by (auto simp add: list_of'_set_ref)
from p_notin_qrs qrs_def have refs_of1: "refs_of' (Ref.set p (Node x q) h) p (p#qrs)"
@@ -621,7 +621,7 @@
by (auto elim!: effect_ref)
from list_of_h obtain refs where refs_def: "refs_of h r refs" by (rule list_of_refs_of)
from validHeap init refs_def have heap_eq: "\<forall>refs. refs_of h r refs \<longrightarrow> (\<forall>ref\<in>set refs. Ref.present h ref \<and> Ref.present h2 ref \<and> Ref.get h ref = Ref.get h2 ref)"
- by (fastsimp elim!: effect_ref dest: refs_of_is_fun)
+ by (fastforce elim!: effect_ref dest: refs_of_is_fun)
from list_of_invariant[OF list_of_h heap_eq] have "list_of h2 r xs" .
from init this Node have a2: "list_of' h2 p xs"
apply -
@@ -642,7 +642,7 @@
with init all_ref_present have q_is_new: "q \<notin> set (p#refs)"
by (auto elim!: effect_refE intro!: Ref.noteq_I)
from refs_of_p refs_of_q q_is_new have a3: "\<forall>qrs prs. refs_of' h2 q qrs \<and> refs_of' h2 p prs \<longrightarrow> set prs \<inter> set qrs = {}"
- by (fastsimp simp only: set.simps dest: refs_of'_is_fun)
+ by (fastforce simp only: set.simps dest: refs_of'_is_fun)
from rev'_invariant [OF effect_rev' a1 a2 a3] have "list_of h3 (Ref.get h3 v) (List.rev xs)"
unfolding list_of'_def by auto
with lookup show ?thesis
@@ -891,7 +891,7 @@
show ?thesis using assms(1) assms(2) assms(4) assms(5)
proof (induct arbitrary: xs ys rs rule: merge_induct3[OF ps_def qs_def assms(3)])
case 1
- from 1(5) 1(7) have "rs = ys" by (fastsimp simp add: refs_of'_is_fun)
+ from 1(5) 1(7) have "rs = ys" by (fastforce simp add: refs_of'_is_fun)
thus ?case by auto
next
case 2
@@ -947,10 +947,10 @@
where pnrs_def: "prs = p#pnrs"
and refs_of'_pn: "refs_of' h pn pnrs"
by (rule refs_of'_Node)
- from prs_def qrs_def 3(9) pnrs_def refs_of'_distinct[OF prs_def] have p_in: "p \<notin> set pnrs \<union> set qrs" by fastsimp
- from prs_def qrs_def 3(9) pnrs_def have no_inter: "set pnrs \<inter> set qrs = {}" by fastsimp
+ from prs_def qrs_def 3(9) pnrs_def refs_of'_distinct[OF prs_def] have p_in: "p \<notin> set pnrs \<union> set qrs" by fastforce
+ from prs_def qrs_def 3(9) pnrs_def have no_inter: "set pnrs \<inter> set qrs = {}" by fastforce
from no_inter refs_of'_pn qrs_def have no_inter2: "\<forall>qrs prs. refs_of' h q qrs \<and> refs_of' h pn prs \<longrightarrow> set prs \<inter> set qrs = {}"
- by (fastsimp dest: refs_of'_is_fun)
+ by (fastforce dest: refs_of'_is_fun)
from merge_unchanged[OF refs_of'_pn qrs_def 3(6) no_inter p_in] have p_stays: "Ref.get h1 p = Ref.get h p" ..
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
@@ -964,10 +964,10 @@
where qnrs_def: "qrs = q#qnrs"
and refs_of'_qn: "refs_of' h qn qnrs"
by (rule refs_of'_Node)
- from prs_def qrs_def 4(9) qnrs_def refs_of'_distinct[OF qrs_def] have q_in: "q \<notin> set prs \<union> set qnrs" by fastsimp
- from prs_def qrs_def 4(9) qnrs_def have no_inter: "set prs \<inter> set qnrs = {}" by fastsimp
+ from prs_def qrs_def 4(9) qnrs_def refs_of'_distinct[OF qrs_def] have q_in: "q \<notin> set prs \<union> set qnrs" by fastforce
+ from prs_def qrs_def 4(9) qnrs_def have no_inter: "set prs \<inter> set qnrs = {}" by fastforce
from no_inter refs_of'_qn prs_def have no_inter2: "\<forall>qrs prs. refs_of' h qn qrs \<and> refs_of' h p prs \<longrightarrow> set prs \<inter> set qrs = {}"
- by (fastsimp dest: refs_of'_is_fun)
+ by (fastforce dest: refs_of'_is_fun)
from merge_unchanged[OF prs_def refs_of'_qn 4(6) no_inter q_in] have q_stays: "Ref.get h1 q = Ref.get h q" ..
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
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Mon Sep 12 07:55:43 2011 +0200
@@ -83,7 +83,7 @@
proof -
from resolv_clauses interp have "(\<exists>l \<in> cli - {lit}. interpLit a l) \<or> interpLit a lit"
"(\<exists>l \<in> clj - {compl lit}. interpLit a l) \<or> interpLit a (compl lit)" by auto
- with lit_not_zero show ?thesis by (fastsimp simp add: bex_Un)
+ with lit_not_zero show ?thesis by (fastforce simp add: bex_Un)
qed
lemma interpClause_resolvants:
@@ -132,7 +132,7 @@
proof -
have "set (Array.get h a[i := Some b]) \<subseteq> insert (Some b) (set (Array.get h a))" by (rule set_update_subset_insert)
with assms show ?thesis
- unfolding array_ran_def Array.update_def by fastsimp
+ unfolding array_ran_def Array.update_def by fastforce
qed
lemma array_ran_upd_array_None:
@@ -243,7 +243,7 @@
case (3 l v va r)
thus ?case
unfolding resolve1.simps
- by (fastsimp dest!: res_mem)
+ by (fastforce dest!: res_mem)
qed
lemma resolve2_Inv:
@@ -264,7 +264,7 @@
case (3 l v va r)
thus ?case
unfolding resolve2.simps
- by (fastsimp dest!: res_mem simp add: merge_Nil)
+ by (fastforce dest!: res_mem simp add: merge_Nil)
qed
lemma res_thm'_Inv:
@@ -279,14 +279,14 @@
assume resolve2: "effect (resolve2 (compl x) xs (y # ys)) h h' r"
from resolve2_Inv [OF resolve2] cond have ?case
apply -
- by (rule exI[of _ "x"]) fastsimp
+ by (rule exI[of _ "x"]) fastforce
} moreover
{
assume cond: "\<not> (x = l \<or> x = compl l)" "y = l \<or> y = compl l"
assume resolve1: "effect (resolve1 (compl y) (x # xs) ys) h h' r"
from resolve1_Inv [OF resolve1] cond have ?case
apply -
- by (rule exI[of _ "compl y"]) fastsimp
+ by (rule exI[of _ "compl y"]) fastforce
} moreover
{
fix r'
@@ -317,7 +317,7 @@
apply simp
apply simp
apply simp
- apply fastsimp
+ apply fastforce
done
next
case (2 l ys r)
@@ -517,7 +517,7 @@
case (Cons x xs)
{
fix h1 ret
- obtain l j where x_is: "x = (l, j)" by fastsimp
+ obtain l j where x_is: "x = (l, j)" by fastforce
assume res_thm2: "effect (res_thm2 a x cli) h h1 ret"
with x_is have res_thm2': "effect (res_thm2 a (l, j) cli) h h1 ret" by simp
note step = res_thm2_Inv [OF res_thm2' Cons.prems(2) Cons.prems(3)]
@@ -616,7 +616,7 @@
have "set (xs[i := Some b]) \<subseteq> insert (Some b) (set xs)"
by (simp only: set_update_subset_insert)
with assms have "Some cl \<in> insert (Some b) (set xs)"
- unfolding list_ran_def by fastsimp
+ unfolding list_ran_def by fastforce
thus ?thesis
unfolding list_ran_def by auto
qed
--- a/src/HOL/Imperative_HOL/ex/Sorted_List.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Imperative_HOL/ex/Sorted_List.thy Mon Sep 12 07:55:43 2011 +0200
@@ -77,7 +77,7 @@
apply (auto simp add: sorted_Cons)
apply (subgoal_tac "x \<notin> set xs")
apply (simp add: notinset_remove)
-apply fastsimp
+apply fastforce
done
lemma sorted_remove1:
--- a/src/HOL/Imperative_HOL/ex/Subarray.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Imperative_HOL/ex/Subarray.thy Mon Sep 12 07:55:43 2011 +0200
@@ -19,7 +19,7 @@
lemma subarray_upd2: " i < n \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
apply (simp add: subarray_def Array.update_def)
apply (subst sublist'_update2)
-apply fastsimp
+apply fastforce
apply simp
done
--- a/src/HOL/Imperative_HOL/ex/Sublist.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Imperative_HOL/ex/Sublist.thy Mon Sep 12 07:55:43 2011 +0200
@@ -24,10 +24,10 @@
apply (subgoal_tac "{ja. j \<le> Suc ja \<and> Suc ja < k} = {j - Suc 0..<k - Suc 0}")
apply (subgoal_tac "{j. Suc j < k} = {0..<k - Suc 0}")
apply simp
-apply fastsimp
-apply fastsimp
-apply fastsimp
-apply fastsimp
+apply fastforce
+apply fastforce
+apply fastforce
+apply fastforce
apply (erule_tac x="i - 1" in meta_allE)
apply (erule_tac x="j - 1" in meta_allE)
apply (erule_tac x="k - 1" in meta_allE)
@@ -36,10 +36,10 @@
apply (subgoal_tac "{j. i \<le> Suc j \<and> Suc j < k} = {i - 1..<k - 1}")
apply (subgoal_tac " i - 1 \<le> j - 1 \<and> j - 1 \<le> k - 1")
apply simp
-apply fastsimp
-apply fastsimp
-apply fastsimp
-apply fastsimp
+apply fastforce
+apply fastforce
+apply fastforce
+apply fastforce
done
lemma sublist_update1: "i \<notin> inds \<Longrightarrow> sublist (xs[i := v]) inds = sublist xs inds"
@@ -143,18 +143,18 @@
apply (induct xs arbitrary: ys inds inds')
apply simp
apply (drule sym, rule sym)
-apply (simp add: sublist_Nil, fastsimp)
+apply (simp add: sublist_Nil, fastforce)
apply (case_tac ys)
-apply (simp add: sublist_Nil, fastsimp)
+apply (simp add: sublist_Nil, fastforce)
apply (auto simp add: sublist_Cons)
apply (erule_tac x="list" in meta_allE)
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
-apply fastsimp
+apply fastforce
apply (erule_tac x="list" in meta_allE)
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
-apply fastsimp
+apply fastforce
done
lemma sublist_eq: "\<lbrakk> \<forall>i \<in> inds. ((i < length xs) \<and> (i < length ys)) \<or> ((i \<ge> length xs ) \<and> (i \<ge> length ys)); \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
@@ -166,10 +166,10 @@
apply (auto simp add: sublist_Cons)
apply (erule_tac x="list" in meta_allE)
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
-apply fastsimp
+apply fastforce
apply (erule_tac x="list" in meta_allE)
apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
-apply fastsimp
+apply fastforce
done
lemma sublist_eq_samelength: "\<lbrakk> length xs = length ys; \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
--- a/src/HOL/Library/Convex.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Library/Convex.thy Mon Sep 12 07:55:43 2011 +0200
@@ -112,7 +112,7 @@
hence "(\<Sum> j \<in> s. a j) = 0"
using asms by auto
hence "\<And> j. j \<in> s \<Longrightarrow> a j = 0"
- using setsum_nonneg_0[where 'b=real] asms by fastsimp
+ using setsum_nonneg_0[where 'b=real] asms by fastforce
hence ?case using asms by auto }
moreover
{ assume asm: "a i \<noteq> 1"
@@ -125,13 +125,13 @@
{ fix j assume "j \<in> s"
hence "?a j \<ge> 0"
using i0 asms divide_nonneg_pos
- by fastsimp } note a_nonneg = this
+ by fastforce } note a_nonneg = this
have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
- hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
+ hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastforce
hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
from this asms
- have "(\<Sum>j\<in>s. ?a j *\<^sub>R y j) \<in> C" using a_nonneg by fastsimp
+ have "(\<Sum>j\<in>s. ?a j *\<^sub>R y j) \<in> C" using a_nonneg by fastforce
hence "a i *\<^sub>R y i + (1 - a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) \<in> C"
using asms[unfolded convex_def, rule_format] yai ai1 by auto
hence "a i *\<^sub>R y i + (\<Sum> j \<in> s. (1 - a i) *\<^sub>R (?a j *\<^sub>R y j)) \<in> C"
@@ -256,7 +256,7 @@
using assms(4,5) by (auto simp add: mult_left_mono add_mono)
also have "\<dots> = max (f x) (f y)" using assms(6) unfolding distrib[THEN sym] by auto
finally show ?thesis
- using assms unfolding convex_on_def by fastsimp
+ using assms unfolding convex_on_def by fastforce
qed
lemma convex_distance[intro]:
@@ -363,7 +363,7 @@
hence "\<mu> > 0" "(1 - \<mu>) > 0" using asms by auto
hence "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms
by (auto simp add: add_pos_pos mult_pos_pos) }
- ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0" using assms by fastsimp
+ ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0" using assms by fastforce
qed
lemma convex_on_setsum:
@@ -393,7 +393,7 @@
hence "(\<Sum> j \<in> s. a j) = 0"
using asms by auto
hence "\<And> j. j \<in> s \<Longrightarrow> a j = 0"
- using setsum_nonneg_0[where 'b=real] asms by fastsimp
+ using setsum_nonneg_0[where 'b=real] asms by fastforce
hence ?case using asms by auto }
moreover
{ assume asm: "a i \<noteq> 1"
@@ -406,9 +406,9 @@
{ fix j assume "j \<in> s"
hence "?a j \<ge> 0"
using i0 asms divide_nonneg_pos
- by fastsimp } note a_nonneg = this
+ by fastforce } note a_nonneg = this
have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
- hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastsimp
+ hence "(\<Sum> j \<in> s. a j) = 1 - a i" using setsum.insert asms by fastforce
hence "(\<Sum> j \<in> s. a j) / (1 - a i) = 1" using i0 by auto
hence a1: "(\<Sum> j \<in> s. ?a j) = 1" unfolding setsum_divide_distrib by simp
have "convex C" using asms by auto
@@ -497,7 +497,7 @@
let ?x = "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y"
assume asm: "convex C" "x \<in> C" "y \<in> C" "\<mu> \<ge> 0" "\<mu> \<le> 1"
hence "1 - \<mu> \<ge> 0" by auto
- hence xpos: "?x \<in> C" using asm unfolding convex_alt by fastsimp
+ hence xpos: "?x \<in> C" using asm unfolding convex_alt by fastforce
have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x)
\<ge> \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
using add_mono[OF mult_left_mono[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
@@ -550,7 +550,7 @@
THEN f', THEN MVT2[OF `x < y`, rule_format, unfolded atLeastAtMost_iff[symmetric]]]
by auto
hence "z1 \<in> C" using atMostAtLeast_subset_convex
- `convex C` `x \<in> C` `y \<in> C` `x < y` by fastsimp
+ `convex C` `x \<in> C` `y \<in> C` `x < y` by fastforce
from z1 have z1': "f x - f y = (x - y) * f' z1"
by (simp add:field_simps)
obtain z2 where z2: "z2 > x" "z2 < z1" "f' z1 - f' x = (z1 - x) * f'' z2"
@@ -567,7 +567,7 @@
finally have cool': "f' y - (f x - f y) / (x - y) = (y - z1) * f'' z3" by simp
have A': "y - z1 \<ge> 0" using z1 by auto
have "z3 \<in> C" using z3 asm atMostAtLeast_subset_convex
- `convex C` `x \<in> C` `z1 \<in> C` `x < z1` by fastsimp
+ `convex C` `x \<in> C` `z1 \<in> C` `x < z1` by fastforce
hence B': "f'' z3 \<ge> 0" using assms by auto
from A' B' have "(y - z1) * f'' z3 \<ge> 0" using mult_nonneg_nonneg by auto
from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0" by auto
@@ -582,7 +582,7 @@
finally have cool: "(f y - f x) / (y - x) - f' x = (z1 - x) * f'' z2" by simp
have A: "z1 - x \<ge> 0" using z1 by auto
have "z2 \<in> C" using z2 z1 asm atMostAtLeast_subset_convex
- `convex C` `z1 \<in> C` `y \<in> C` `z1 < y` by fastsimp
+ `convex C` `z1 \<in> C` `y \<in> C` `z1 < y` by fastforce
hence B: "f'' z2 \<ge> 0" using assms by auto
from A B have "(z1 - x) * f'' z2 \<ge> 0" using mult_nonneg_nonneg by auto
from cool this have "(f y - f x) / (y - x) - f' x \<ge> 0" by auto
@@ -608,7 +608,7 @@
assumes f'': "\<And> x. x \<in> C \<Longrightarrow> DERIV f' x :> (f'' x)"
assumes pos: "\<And> x. x \<in> C \<Longrightarrow> f'' x \<ge> 0"
shows "convex_on C f"
-using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastsimp
+using f''_imp_f'[OF conv f' f'' pos] assms pos_convex_function by fastforce
lemma minus_log_convex:
fixes b :: real
--- a/src/HOL/Library/Extended_Nat.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Library/Extended_Nat.thy Mon Sep 12 07:55:43 2011 +0200
@@ -487,7 +487,7 @@
proof (rule finite_subset)
show "finite (enat ` {..n})" by blast
- have "A \<subseteq> {..enat n}" using le_fin by fastsimp
+ have "A \<subseteq> {..enat n}" using le_fin by fastforce
also have "\<dots> \<subseteq> enat ` {..n}"
by (rule subsetI) (case_tac x, auto)
finally show "A \<subseteq> enat ` {..n}" .
--- a/src/HOL/Library/Extended_Real.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy Mon Sep 12 07:55:43 2011 +0200
@@ -1887,7 +1887,7 @@
proof safe case goal1
have "ereal B < ereal (B + 1)" by auto
also have "... <= f n" using goal1 N by auto
- finally show ?case using B by fastsimp
+ finally show ?case using B by fastforce
qed
qed
next
@@ -1916,7 +1916,7 @@
proof safe case goal1
have "ereal (B - 1) >= f n" using goal1 N by auto
also have "... < ereal B" by auto
- finally show ?case using B by fastsimp
+ finally show ?case using B by fastforce
qed
qed
next assume ?l show ?r
--- a/src/HOL/Library/Infinite_Set.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Library/Infinite_Set.thy Mon Sep 12 07:55:43 2011 +0200
@@ -544,7 +544,7 @@
lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
apply (induct n arbitrary: S)
- apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
+ apply (fastforce intro: LeastI dest!: infinite_imp_nonempty)
apply simp
apply (metis DiffE infinite_remove)
done
--- a/src/HOL/Library/Multiset.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Sep 12 07:55:43 2011 +0200
@@ -218,7 +218,7 @@
lemma add_eq_conv_diff:
"M + {#a#} = N + {#b#} \<longleftrightarrow> M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#}" (is "?lhs = ?rhs")
-(* shorter: by (simp add: multiset_eq_iff) fastsimp *)
+(* shorter: by (simp add: multiset_eq_iff) fastforce *)
proof
assume ?rhs then show ?lhs
by (auto simp add: add_assoc add_commute [of "{#b#}"])
--- a/src/HOL/Library/Permutation.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Library/Permutation.thy Mon Sep 12 07:55:43 2011 +0200
@@ -153,7 +153,7 @@
lemma perm_distinct_iff: "xs <~~> ys ==> distinct xs = distinct ys"
apply (induct pred: perm)
apply simp_all
- apply fastsimp
+ apply fastforce
apply (metis perm_set_eq)
done
@@ -171,7 +171,7 @@
apply (metis Cons Cons_eq_appendI distinct.simps(2)
distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
- apply (fastsimp simp add: insert_ident)
+ apply (fastforce simp add: insert_ident)
apply (metis distinct_remdups set_remdups)
apply (subgoal_tac "length (remdups xs) < Suc (length xs)")
apply simp
--- a/src/HOL/Library/Polynomial.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Library/Polynomial.thy Mon Sep 12 07:55:43 2011 +0200
@@ -1134,7 +1134,7 @@
and poly_gcd_dvd2 [iff]: "poly_gcd x y dvd y"
apply (induct x y rule: poly_gcd.induct)
apply (simp_all add: poly_gcd.simps)
- apply (fastsimp simp add: smult_dvd_iff dest: inverse_zero_imp_zero)
+ apply (fastforce simp add: smult_dvd_iff dest: inverse_zero_imp_zero)
apply (blast dest: dvd_mod_imp_dvd)
done
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Sep 12 07:55:43 2011 +0200
@@ -49,11 +49,11 @@
lemma subset_eq[code_pred_inline]:
"(P :: 'a => bool) < (Q :: 'a => bool) == ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall> x. P x --> Q x))"
-by (rule eq_reflection) (fastsimp simp add: mem_def)
+by (rule eq_reflection) (fastforce simp add: mem_def)
lemma set_equality[code_pred_inline]:
"(A = B) = ((\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x))"
-by (fastsimp simp add: mem_def)
+by (fastforce simp add: mem_def)
section {* Setup for Numerals *}
@@ -218,7 +218,7 @@
unfolding mem_def[symmetric, of _ xc]
apply auto
unfolding mem_def
- apply fastsimp
+ apply fastforce
done
qed
@@ -240,7 +240,7 @@
apply auto
apply (case_tac xc)
apply auto
- apply fastsimp
+ apply fastforce
done
qed
--- a/src/HOL/Library/Quickcheck_Types.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Library/Quickcheck_Types.thy Mon Sep 12 07:55:43 2011 +0200
@@ -353,7 +353,7 @@
}
from `x : A` this show "Inf A <= x"
unfolding Inf_flat_complete_lattice_def
- by fastsimp
+ by fastforce
next
fix z A
assume z: "\<And>x. x : A ==> z <= (x :: 'a flat_complete_lattice)"
@@ -412,7 +412,7 @@
}
from `x : A` this show "x <= Sup A"
unfolding Sup_flat_complete_lattice_def
- by fastsimp
+ by fastforce
next
fix z A
assume z: "\<And>x. x : A ==> x <= (z :: 'a flat_complete_lattice)"
--- a/src/HOL/Library/Ramsey.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Library/Ramsey.thy Mon Sep 12 07:55:43 2011 +0200
@@ -64,7 +64,7 @@
have "V = insert v (?M \<union> ?N)" using `v : V` by auto
hence "card V = card(insert v (?M \<union> ?N))" by metis
also have "\<dots> = card ?M + card ?N + 1" using `finite V`
- by(fastsimp intro: card_Un_disjoint)
+ by(fastforce intro: card_Un_disjoint)
finally have "card V = card ?M + card ?N + 1" .
hence "r1+r2 \<le> card ?M + card ?N + 1" using `r1+r2 \<le> card V` by simp
hence "r1 \<le> card ?M \<or> r2 \<le> card ?N" by arith
@@ -325,7 +325,7 @@
"\<exists>Y t. Y \<subseteq> Z & infinite Y & t < s & (\<forall>x\<in>Y. \<forall>y\<in>Y. x\<noteq>y --> f{x,y} = t)"
proof -
have part2: "\<forall>X. X \<subseteq> Z & finite X & card X = 2 --> f X < s"
- using part by (fastsimp simp add: eval_nat_numeral card_Suc_eq)
+ using part by (fastforce simp add: eval_nat_numeral card_Suc_eq)
obtain Y t
where "Y \<subseteq> Z" "infinite Y" "t < s"
"(\<forall>X. X \<subseteq> Y & finite X & card X = 2 --> f X = t)"
--- a/src/HOL/Library/Set_Algebras.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Library/Set_Algebras.thy Mon Sep 12 07:55:43 2011 +0200
@@ -356,7 +356,7 @@
lemma set_plus_image:
fixes S T :: "'n::semigroup_add set" shows "S \<oplus> T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
- unfolding set_plus_def by (fastsimp simp: image_iff)
+ unfolding set_plus_def by (fastforce simp: image_iff)
lemma set_setsum_alt:
assumes fin: "finite I"
--- a/src/HOL/Library/Transitive_Closure_Table.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Mon Sep 12 07:55:43 2011 +0200
@@ -189,7 +189,7 @@
declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
-code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastsimp
+code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
subsection {* A simple example *}
--- a/src/HOL/Library/Zorn.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Library/Zorn.thy Mon Sep 12 07:55:43 2011 +0200
@@ -480,12 +480,12 @@
by(auto simp add:wf_eq_minimal Field_def Domain_def Range_def) metis
thus ?thesis using `wf(m-Id)` `x \<notin> Field m`
wf_subset[OF `wf ?s` Diff_subset]
- by (fastsimp intro!: wf_Un simp add: Un_Diff Field_def)
+ by (fastforce intro!: wf_Un simp add: Un_Diff Field_def)
qed
ultimately have "Well_order ?m" by(simp add:order_on_defs)
--{*We show that the extension is above m*}
moreover hence "(m,?m) : I" using `Well_order m` `x \<notin> Field m`
- by(fastsimp simp:I_def init_seg_of_def Field_def Domain_def Range_def)
+ by(fastforce simp:I_def init_seg_of_def Field_def Domain_def Range_def)
ultimately
--{*This contradicts maximality of m:*}
have False using max `x \<notin> Field m` unfolding Field_def by blast
@@ -501,7 +501,7 @@
using well_ordering[where 'a = "'a"] by blast
let ?r = "{(x,y). x:A & y:A & (x,y):r}"
have 1: "Field ?r = A" using wo univ
- by(fastsimp simp: Field_def Domain_def Range_def order_on_defs refl_on_def)
+ by(fastforce simp: Field_def Domain_def Range_def order_on_defs refl_on_def)
have "Refl r" "trans r" "antisym r" "Total r" "wf(r-Id)"
using `Well_order r` by(simp_all add:order_on_defs)
have "Refl ?r" using `Refl r` by(auto simp:refl_on_def 1 univ)
--- a/src/HOL/List.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/List.thy Mon Sep 12 07:55:43 2011 +0200
@@ -659,10 +659,10 @@
lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) =
(EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)"
apply (induct xs arbitrary: ys zs ts)
- apply fastsimp
+ apply fastforce
apply(case_tac zs)
apply simp
-apply fastsimp
+apply fastforce
done
lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)"
@@ -997,9 +997,9 @@
case (Cons a xs)
show ?case
proof cases
- assume "x = a" thus ?case using Cons by fastsimp
+ assume "x = a" thus ?case using Cons by fastforce
next
- assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI)
+ assume "x \<noteq> a" thus ?case using Cons by(fastforce intro!: Cons_eq_appendI)
qed
qed
@@ -1016,7 +1016,7 @@
proof cases
assume "x = a" thus ?case using snoc by (metis List.set.simps(1) emptyE)
next
- assume "x \<noteq> a" thus ?case using snoc by fastsimp
+ assume "x \<noteq> a" thus ?case using snoc by fastforce
qed
qed
@@ -1078,7 +1078,7 @@
next
assume "\<not> P x"
hence "\<exists>x\<in>set xs. P x" using snoc(2) by simp
- thus ?thesis using `\<not> P x` snoc(1) by fastsimp
+ thus ?thesis using `\<not> P x` snoc(1) by fastforce
qed
qed
@@ -1216,7 +1216,7 @@
qed
next
assume "\<not> P y"
- with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastsimp
+ with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastforce
then have "?Q (y#us)" by simp
then show ?thesis ..
qed
@@ -2986,7 +2986,7 @@
"k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)"
apply(induct ns arbitrary: k)
apply simp
-apply(fastsimp simp add:nth_Cons split: nat.split)
+apply(fastforce simp add:nth_Cons split: nat.split)
done
lemma listsum_update_nat:
@@ -4671,7 +4671,7 @@
\<longleftrightarrow> (xs, ys) \<in> listrel1 r \<and> x = y \<or> xs = ys \<and> (x,y) \<in> r" (is "?L \<longleftrightarrow> ?R")
proof
assume ?L thus ?R
- by (fastsimp simp: listrel1_def snoc_eq_iff_butlast butlast_append)
+ by (fastforce simp: listrel1_def snoc_eq_iff_butlast butlast_append)
next
assume ?R then show ?L unfolding listrel1_def by force
qed
@@ -4734,7 +4734,7 @@
apply (induct set: acc)
apply clarify
apply (rule accI)
-apply (fastsimp dest!: in_set_conv_decomp[THEN iffD1] simp: listrel1_def)
+apply (fastforce dest!: in_set_conv_decomp[THEN iffD1] simp: listrel1_def)
done
lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r"
--- a/src/HOL/MacLaurin.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/MacLaurin.thy Mon Sep 12 07:55:43 2011 +0200
@@ -190,7 +190,7 @@
(\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
diff n t / real (fact n) * h ^ n"
proof (cases "n")
- case 0 with INIT1 INIT2 show ?thesis by fastsimp
+ case 0 with INIT1 INIT2 show ?thesis by fastforce
next
case Suc
hence "n > 0" by simp
@@ -198,7 +198,7 @@
f h =
(\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (fact n) * h ^ n"
by (rule Maclaurin)
- thus ?thesis by fastsimp
+ thus ?thesis by fastforce
qed
lemma Maclaurin2_objl:
--- a/src/HOL/Map.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Map.thy Mon Sep 12 07:55:43 2011 +0200
@@ -332,7 +332,7 @@
lemma inj_on_map_add_dom [iff]:
"inj_on (m ++ m') (dom m') = inj_on m' (dom m')"
-by (fastsimp 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)"
@@ -443,7 +443,7 @@
lemma map_upds_twist [simp]:
"a ~: set as ==> m(a|->b)(as[|->]bs) = m(as[|->]bs)(a|->b)"
-using set_take_subset by (fastsimp simp add: map_upd_upds_conv_if)
+using set_take_subset by (fastforce simp add: map_upd_upds_conv_if)
lemma map_upds_apply_nontin [simp]:
"x ~: set xs ==> (f(xs[|->]ys)) x = f x"
@@ -631,7 +631,7 @@
by (force simp add: map_le_def)
lemma map_le_upd[simp]: "f \<subseteq>\<^sub>m g ==> f(a := b) \<subseteq>\<^sub>m g(a := b)"
-by (fastsimp simp add: map_le_def)
+by (fastforce simp add: map_le_def)
lemma map_le_imp_upd_le [simp]: "m1 \<subseteq>\<^sub>m m2 \<Longrightarrow> m1(x := None) \<subseteq>\<^sub>m m2(x \<mapsto> y)"
by (force simp add: map_le_def)
@@ -645,7 +645,7 @@
done
lemma map_le_implies_dom_le: "(f \<subseteq>\<^sub>m g) \<Longrightarrow> (dom f \<subseteq> dom g)"
-by (fastsimp simp add: map_le_def dom_def)
+by (fastforce simp add: map_le_def dom_def)
lemma map_le_refl [simp]: "f \<subseteq>\<^sub>m f"
by (simp add: map_le_def)
@@ -657,17 +657,17 @@
unfolding map_le_def
apply (rule ext)
apply (case_tac "x \<in> dom f", simp)
-apply (case_tac "x \<in> dom g", simp, fastsimp)
+apply (case_tac "x \<in> dom g", simp, fastforce)
done
lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
-by (fastsimp simp add: map_le_def)
+by (fastforce simp add: map_le_def)
lemma map_le_iff_map_add_commute: "(f \<subseteq>\<^sub>m f ++ g) = (f++g = g++f)"
-by(fastsimp simp: map_add_def map_le_def fun_eq_iff split: option.splits)
+by(fastforce simp: map_add_def map_le_def fun_eq_iff split: option.splits)
lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
-by (fastsimp simp add: map_le_def map_add_def dom_def)
+by (fastforce simp add: map_le_def map_add_def dom_def)
lemma map_add_le_mapI: "\<lbrakk> f \<subseteq>\<^sub>m h; g \<subseteq>\<^sub>m h; f \<subseteq>\<^sub>m f++g \<rbrakk> \<Longrightarrow> f++g \<subseteq>\<^sub>m h"
by (clarsimp simp add: map_le_def map_add_def dom_def split: option.splits)
--- a/src/HOL/MicroJava/BV/BVExample.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Mon Sep 12 07:55:43 2011 +0200
@@ -275,10 +275,10 @@
apply clarify
apply (elim pc_end pc_next pc_0)
apply simp
- apply (fastsimp simp add: match_exception_entry_def sup_state_conv subcls1)
+ apply (fastforce simp add: match_exception_entry_def sup_state_conv subcls1)
apply simp
apply simp
- apply (fastsimp simp add: sup_state_conv subcls1)
+ apply (fastforce simp add: sup_state_conv subcls1)
apply simp
apply (simp add: app_def xcpt_app_def)
apply simp
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Mon Sep 12 07:55:43 2011 +0200
@@ -294,7 +294,7 @@
}
ultimately show ?thesis using Getfield field "class" stk hconf wf
apply clarsimp
- apply (fastsimp intro: wf_prog_ws_prog
+ apply (fastforce intro: wf_prog_ws_prog
dest!: hconfD widen_cfs_fields oconf_objD)
done
next
--- a/src/HOL/MicroJava/BV/Correct.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy Mon Sep 12 07:55:43 2011 +0200
@@ -241,7 +241,7 @@
"\<lbrakk> hp a = Some obj'; obj_ty obj' = obj_ty obj''; G,hp\<turnstile>obj\<surd> \<rbrakk>
\<Longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
apply (unfold oconf_def lconf_def)
- apply (fastsimp intro: approx_val_heap_update)
+ apply (fastforce intro: approx_val_heap_update)
done
section {* hconf *}
@@ -257,7 +257,7 @@
G,hp\<turnstile>v::\<preceq>T; G\<turnstile>h hp\<surd> \<rbrakk>
\<Longrightarrow> G\<turnstile>h hp(a \<mapsto> (oT, fs(X\<mapsto>v)))\<surd>"
apply (simp add: hconf_def)
- apply (fastsimp intro: oconf_heap_update oconf_field_update
+ apply (fastforce intro: oconf_heap_update oconf_field_update
simp add: obj_ty_def)
done
--- a/src/HOL/MicroJava/BV/JType.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/MicroJava/BV/JType.thy Mon Sep 12 07:55:43 2011 +0200
@@ -114,7 +114,7 @@
apply (case_tac "EX C. Class C : M")
prefer 2
apply (case_tac T)
- apply (fastsimp simp add: PrimT_PrimT2)
+ apply (fastforce simp add: PrimT_PrimT2)
apply simp
apply (subgoal_tac "ref_ty = NullT")
apply simp
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Mon Sep 12 07:55:43 2011 +0200
@@ -73,44 +73,44 @@
apply (clarsimp simp add: not_Err_eq)
apply (drule listE_nth_in, assumption)
- apply fastsimp
+ apply fastforce
- apply (fastsimp simp add: not_None_eq)
+ apply (fastforce simp add: not_None_eq)
- apply (fastsimp simp add: not_None_eq typeof_empty_is_type)
+ apply (fastforce simp add: not_None_eq typeof_empty_is_type)
apply clarsimp
apply (erule disjE)
- apply fastsimp
+ apply fastforce
apply clarsimp
apply (rule_tac x="1" in exI)
- apply fastsimp
+ apply fastforce
apply clarsimp
apply (erule disjE)
- apply (fastsimp dest: field_fields fields_is_type)
+ apply (fastforce dest: field_fields fields_is_type)
apply (simp add: match_some_entry image_iff)
apply (rule_tac x=1 in exI)
- apply fastsimp
+ apply fastforce
apply clarsimp
apply (erule disjE)
- apply fastsimp
+ apply fastforce
apply (simp add: match_some_entry image_iff)
apply (rule_tac x=1 in exI)
- apply fastsimp
+ apply fastforce
apply clarsimp
apply (erule disjE)
- apply fastsimp
+ apply fastforce
apply clarsimp
apply (rule_tac x=1 in exI)
- apply fastsimp
+ apply fastforce
defer
- apply fastsimp
- apply fastsimp
+ apply fastforce
+ apply fastforce
apply clarsimp
apply (rule_tac x="n'+2" in exI)
@@ -124,26 +124,26 @@
apply (rule_tac x="Suc (Suc (Suc (Suc (length ST))))" in exI)
apply simp
- apply fastsimp
- apply fastsimp
- apply fastsimp
- apply fastsimp
+ apply fastforce
+ apply fastforce
+ apply fastforce
+ apply fastforce
apply clarsimp
apply (erule disjE)
- apply fastsimp
+ apply fastforce
apply clarsimp
apply (rule_tac x=1 in exI)
- apply fastsimp
+ apply fastforce
apply (erule disjE)
apply clarsimp
apply (drule method_wf_mdecl, assumption+)
apply (clarsimp simp add: wf_mdecl_def wf_mhead_def)
- apply fastsimp
+ apply fastforce
apply clarsimp
apply (rule_tac x=1 in exI)
- apply fastsimp
+ apply fastforce
done
lemmas [iff] = not_None_eq
--- a/src/HOL/MicroJava/Comp/AuxLemmas.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy Mon Sep 12 07:55:43 2011 +0200
@@ -81,7 +81,7 @@
"(\<forall>y\<in>set ys. y \<notin> set xs) \<Longrightarrow> map (the \<circ> f(ys[\<mapsto>]vs)) xs = map (the \<circ> f) xs"
apply (induct xs arbitrary: f vs)
apply simp
-apply fastsimp
+apply fastforce
done
lemma map_upds_distinct [simp]:
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy Mon Sep 12 07:55:43 2011 +0200
@@ -102,7 +102,7 @@
by clarify (rule pp_ub1)
with sum have "\<forall>x \<in> set (?map ss1). x <=_r ?s1" by simp
with less have "\<forall>x \<in> set (?map ss2). x <=_r ?s1"
- by (fastsimp dest!: mapD lesub_step_typeD intro: trans_r)
+ by (fastforce dest!: mapD lesub_step_typeD intro: trans_r)
moreover
from map1 x have "x <=_r (?sum ss1)" by (rule pp_ub2)
with sum have "x <=_r ?s1" by simp
--- a/src/HOL/MicroJava/DFA/Listn.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/MicroJava/DFA/Listn.thy Mon Sep 12 07:55:43 2011 +0200
@@ -230,12 +230,12 @@
next
fix n l ls
assume "?list (l#ls) n"
- then obtain n' where n: "n = Suc n'" "l \<in> A" and list_n': "ls@b \<in> list n' A" by fastsimp
+ then obtain n' where n: "n = Suc n'" "l \<in> A" and list_n': "ls@b \<in> list n' A" by fastforce
assume "\<And>n. ls @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A"
hence "\<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A" by this (rule list_n')
then obtain n1 n2 where "n' = n1 + n2" "ls \<in> list n1 A" "b \<in> list n2 A" by fast
with n have "?P (l#ls) n (n1+1) n2" by simp
- thus "\<exists>n1 n2. ?P (l#ls) n n1 n2" by fastsimp
+ thus "\<exists>n1 n2. ?P (l#ls) n n1 n2" by fastforce
qed
moreover
assume "a@b \<in> list n A" "\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P"
@@ -504,7 +504,7 @@
lemma closed_lift2_sup:
"closed (err A) (lift2 f) \<Longrightarrow>
closed (err (list n A)) (lift2 (sup f))"
- by (fastsimp simp add: closed_def plussub_def sup_def lift2_def
+ by (fastforce simp add: closed_def plussub_def sup_def lift2_def
coalesce_in_err_list closed_map2_list
split: err.split)
@@ -528,7 +528,7 @@
apply (unfold Listn.upto_esl_def)
apply (simp (no_asm_simp) only: split_tupled_all)
apply simp
-apply (fastsimp intro!: err_semilat_UnionI err_semilat_sup
+apply (fastforce intro!: err_semilat_UnionI err_semilat_sup
dest: lesub_list_impl_same_size
simp add: plussub_def Listn.sup_def)
done
--- a/src/HOL/MicroJava/DFA/Semilat.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/MicroJava/DFA/Semilat.thy Mon Sep 12 07:55:43 2011 +0200
@@ -300,7 +300,7 @@
lemma is_lub_some_lub:
"\<lbrakk> single_valued r; acyclic r; (x,u)\<in>r^*; (y,u)\<in>r^* \<rbrakk>
\<Longrightarrow> is_lub (r^* ) x y (some_lub (r^* ) x y)";
- (*<*) by (fastsimp dest: single_valued_has_lubs simp add: some_lub_conv) (*>*)
+ (*<*) by (fastforce dest: single_valued_has_lubs simp add: some_lub_conv) (*>*)
subsection{*An executable lub-finder*}
@@ -369,6 +369,6 @@
lemma is_lub_exec_lub:
"\<lbrakk> single_valued r; acyclic r; (x,u):r^*; (y,u):r^*; \<forall>x y. (x,y) \<in> r \<longrightarrow> f x = y \<rbrakk>
\<Longrightarrow> is_lub (r^* ) x y (exec_lub r f x y)"
- (*<*) by (fastsimp dest: single_valued_has_lubs simp add: exec_lub_conv) (*>*)
+ (*<*) by (fastforce dest: single_valued_has_lubs simp add: exec_lub_conv) (*>*)
end
--- a/src/HOL/MicroJava/J/WellForm.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy Mon Sep 12 07:55:43 2011 +0200
@@ -314,7 +314,7 @@
apply( frule class_Object)
apply( clarify)
apply( frule fields_rec, assumption)
-apply( fastsimp)
+apply( fastforce)
apply( tactic "safe_tac (put_claset HOL_cs @{context})")
apply( subst fields_rec)
apply( assumption)
@@ -410,8 +410,8 @@
apply( simp add: wf_cdecl_def)
apply( drule map_of_SomeD)
apply( subgoal_tac "md = Object")
-apply( fastsimp)
-apply( fastsimp)
+apply( fastforce)
+apply( fastforce)
apply( clarify)
apply( frule_tac C = C in method_rec)
apply( assumption)
@@ -445,8 +445,8 @@
apply( simp add: ws_cdecl_def)
apply( drule map_of_SomeD)
apply( subgoal_tac "md = Object")
-apply( fastsimp)
-apply( fastsimp)
+apply( fastforce)
+apply( fastforce)
apply( clarify)
apply( frule_tac C = C in method_rec)
apply( assumption)
@@ -648,7 +648,7 @@
apply( frule fields_rec, assumption)
apply( drule class_wf_struct, assumption)
apply( simp add: ws_cdecl_def wf_fdecl_def)
-apply( fastsimp)
+apply( fastforce)
apply( subst fields_rec)
apply( fast)
apply( assumption)
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Sep 12 07:55:43 2011 +0200
@@ -1014,7 +1014,7 @@
using reduced_labelling[of label n x] using assms by auto
lemma reduced_labelling_0: assumes "j\<in>{1..n}" "label x j = 0" shows "reduced label n x \<noteq> j - 1"
- using reduced_labelling[of label n x] using assms by fastsimp
+ using reduced_labelling[of label n x] using assms by fastforce
lemma reduced_labelling_1: assumes "j\<in>{1..n}" "label x j \<noteq> 0" shows "reduced label n x < j"
using assms and reduced_labelling[of label n x] apply(erule_tac x=j in allE) by auto
@@ -1077,8 +1077,8 @@
case True then guess j .. hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab (n + 1) x \<noteq> j - 1" apply-apply(rule reduced_labelling_0) apply assumption
apply(rule assms(2)[rule_format]) using sa(1)[unfolded ksimplex_def] unfolding sa by auto moreover
have "j - 1 \<in> {0..n}" using `j\<in>{1..n+1}` by auto
- ultimately have False unfolding sa(4)[THEN sym] unfolding image_iff by fastsimp thus ?thesis by auto next
- case False hence "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p" using sa(5) by fastsimp then guess j .. note j=this
+ ultimately have False unfolding sa(4)[THEN sym] unfolding image_iff by fastforce thus ?thesis by auto next
+ case False hence "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p" using sa(5) by fastforce then guess j .. note j=this
thus ?thesis proof(cases "j = n+1")
case False hence *:"j\<in>{1..n}" using j by auto
hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab n x < j" apply(rule reduced_labelling_1) proof- fix x assume "x\<in>f"
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Sep 12 07:55:43 2011 +0200
@@ -115,7 +115,7 @@
shows "setsum (%i. f i *\<^sub>R basis i) d = (x::'a::euclidean_space)
<-> (!i<DIM('a). (i:d --> f i = x$$i) & (i ~: d --> x $$ i = 0))"
proof- have *:"\<And>x a b P. x * (if P then a else b) = (if P then x*a else x*b)" by auto
- have **:"finite d" apply(rule finite_subset[OF assms]) by fastsimp
+ have **:"finite d" apply(rule finite_subset[OF assms]) by fastforce
have ***:"\<And>i. (setsum (%i. f i *\<^sub>R ((basis i)::'a)) d) $$ i = (\<Sum>x\<in>d. if x = i then f x else 0)"
unfolding euclidean_component_setsum euclidean_component_scaleR basis_component *
apply(rule setsum_cong2) using assms by auto
@@ -1319,7 +1319,7 @@
using setsum_cong2 [of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x))" u] unfolding obt(4,5) by auto
ultimately have "\<exists>k u x. (\<forall>i\<in>{1..k}. 0 \<le> u i \<and> x i \<in> p) \<and> setsum u {1..k} = 1 \<and> (\<Sum>i::nat = 1..k. u i *\<^sub>R x i) = y"
- apply(rule_tac x="card s" in exI) apply(rule_tac x="u \<circ> f" in exI) apply(rule_tac x=f in exI) by fastsimp
+ apply(rule_tac x="card s" in exI) apply(rule_tac x="u \<circ> f" in exI) apply(rule_tac x=f in exI) by fastforce
hence "y \<in> ?lhs" unfolding convex_hull_indexed by auto }
ultimately show ?thesis unfolding set_eq_iff by blast
qed
@@ -2884,7 +2884,7 @@
shows "dist a (closest_point s a) < dist a x"
apply(rule ccontr) apply(rule_tac notE[OF assms(4)])
apply(rule closest_point_unique[OF assms(1-3), of a])
- using closest_point_le[OF assms(2), of _ a] by fastsimp
+ using closest_point_le[OF assms(2), of _ a] by fastforce
lemma closest_point_lipschitz:
assumes "convex s" "closed s" "s \<noteq> {}"
@@ -4229,7 +4229,7 @@
ultimately
have "!i. ( (ALL i:d. 0 < x$$i) & (ALL i. i ~: d --> x$$i = 0) ) --> 0 <= x$$i" by metis
hence h2: "x : convex hull (insert 0 ?p)" using as assms
- unfolding substd_simplex[OF assms] by fastsimp
+ unfolding substd_simplex[OF assms] by fastforce
obtain a where a:"a:d" using `d ~= {}` by auto
let ?d = "(1 - setsum (op $$ x) d) / real (card d)"
have "0 < card d" using `d ~={}` `finite d` by (simp add: card_gt_0_iff)
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Sep 12 07:55:43 2011 +0200
@@ -700,7 +700,7 @@
have "\<bar>(f (x + c *\<^sub>R basis j) - f x - ?v) $$ k\<bar> \<le>
norm (f (x + c *\<^sub>R basis j) - f x - ?v)" by (rule component_le_norm)
also have "\<dots> \<le> \<bar>?D k $$ j\<bar> / 2 * \<bar>c\<bar>"
- using e'[THEN conjunct2, rule_format, OF *] and norm_basis[of j] by fastsimp
+ using e'[THEN conjunct2, rule_format, OF *] and norm_basis[of j] by fastforce
finally have "\<bar>(f (x + c *\<^sub>R basis j) - f x - ?v) $$ k\<bar> \<le> \<bar>?D k $$ j\<bar> / 2 * \<bar>c\<bar>" by simp
hence "\<bar>f (x + c *\<^sub>R basis j) $$ k - f x $$ k - c * ?D k $$ j\<bar> \<le> \<bar>?D k $$ j\<bar> / 2 * \<bar>c\<bar>"
unfolding euclidean_simps euclidean_lambda_beta using j k
@@ -1285,7 +1285,7 @@
have "g' (f' a (\<chi>\<chi> i.1)) = (\<chi>\<chi> i.1)" "(\<chi>\<chi> i.1) \<noteq> (0::'n)" defer
apply(subst euclidean_eq) using f'g' by auto
hence *:"0 < onorm g'"
- unfolding onorm_pos_lt[OF assms(3)[unfolded linear_linear]] by fastsimp
+ unfolding onorm_pos_lt[OF assms(3)[unfolded linear_linear]] by fastforce
def k \<equiv> "1 / onorm g' / 2" have *:"k>0" unfolding k_def using * by auto
guess d1 using assms(6)[rule_format,OF *] .. note d1=this
from `open s` obtain d2 where "d2>0" "ball a d2 \<subseteq> s" using `a\<in>s` ..
--- a/src/HOL/Multivariate_Analysis/Integration.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Sep 12 07:55:43 2011 +0200
@@ -133,7 +133,7 @@
case True show ?thesis proof(cases "x\<in>{a<..<b}")
case True then guess d unfolding open_contains_ball_eq[OF open_interval,rule_format] ..
thus ?thesis apply(rule_tac x=i in bexI,rule_tac x=x in exI,rule_tac x="min d e" in exI)
- unfolding ab using interval_open_subset_closed[of a b] and e by fastsimp+ next
+ unfolding ab using interval_open_subset_closed[of a b] and e by fastforce+ next
case False then obtain k where "x$$k \<le> a$$k \<or> x$$k \<ge> b$$k" and k:"k<DIM('a)" unfolding mem_interval by(auto simp add:not_less)
hence "x$$k = a$$k \<or> x$$k = b$$k" using True unfolding ab and mem_interval apply(erule_tac x=k in allE) by auto
hence "\<exists>x. ball x (e/2) \<subseteq> s \<inter> (\<Union>f)" proof(erule_tac disjE)
@@ -232,7 +232,7 @@
case True thus ?thesis unfolding content_def if_P[OF True] unfolding interval_eq_empty apply-
apply(rule,erule exE) apply(rule_tac x=i in exI) by auto next
case False note this[unfolded interval_eq_empty not_ex not_less]
- hence as:"\<forall>i<DIM('a). b $$ i \<ge> a $$ i" by fastsimp
+ hence as:"\<forall>i<DIM('a). b $$ i \<ge> a $$ i" by fastforce
show ?thesis unfolding content_def if_not_P[OF False] setprod_zero_iff[OF finite_lessThan]
apply(rule) apply(erule_tac[!] exE bexE) unfolding interval_bounds[OF as] apply(rule_tac x=x in exI) defer
apply(rule_tac x=i in bexI) using as apply(erule_tac x=i in allE) by auto qed
@@ -251,7 +251,7 @@
lemma content_pos_lt_eq: "0 < content {a..b::'a::ordered_euclidean_space} \<longleftrightarrow> (\<forall>i<DIM('a). a$$i < b$$i)"
apply(rule) defer apply(rule content_pos_lt,assumption) proof- assume "0 < content {a..b}"
- hence "content {a..b} \<noteq> 0" by auto thus "\<forall>i<DIM('a). a$$i < b$$i" unfolding content_eq_0 not_ex not_le by fastsimp qed
+ hence "content {a..b} \<noteq> 0" by auto thus "\<forall>i<DIM('a). a$$i < b$$i" unfolding content_eq_0 not_ex not_le by fastforce qed
lemma content_empty[simp]: "content {} = 0" unfolding content_def by auto
@@ -270,7 +270,7 @@
using assms[unfolded subset_eq mem_interval,rule_format,OF ab_ab(1),of i] using i by auto qed qed
lemma content_lt_nz: "0 < content {a..b} \<longleftrightarrow> content {a..b} \<noteq> 0"
- unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastsimp
+ unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce
subsection {* The notion of a gauge --- simply an open set containing the point. *}
@@ -343,7 +343,7 @@
lemma forall_in_division:
"d division_of i \<Longrightarrow> ((\<forall>x\<in>d. P x) \<longleftrightarrow> (\<forall>a b. {a..b} \<in> d \<longrightarrow> P {a..b}))"
- unfolding division_of_def by fastsimp
+ unfolding division_of_def by fastforce
lemma division_of_subset: assumes "p division_of (\<Union>p)" "q \<subseteq> p" shows "q division_of (\<Union>q)"
apply(rule division_ofI) proof- note as=division_ofD[OF assms(1)]
@@ -621,7 +621,7 @@
next assume as:"interior {a..b} = {}" "{a..b} \<noteq> {}"
show thesis apply(rule that[of "insert {a..b} p"],rule division_ofI)
unfolding finite_insert apply(rule assm(1)) unfolding Union_insert
- using assm(2-4) as apply- by(fastsimp dest: assm(5))+
+ using assm(2-4) as apply- by(fastforce dest: assm(5))+
next assume as:"p \<noteq> {}" "interior {a..b} \<noteq> {}" "{a..b}\<noteq>{}"
have "\<forall>k\<in>p. \<exists>q. (insert {a..b} q) division_of ({a..b} \<union> k)" proof case goal1
from assm(4)[OF this] guess c .. then guess d ..
@@ -763,7 +763,7 @@
proof(rule division_ofI) note assm=tagged_division_ofD[OF assms]
show "\<Union>snd ` s = i" "finite (snd ` s)" using assm by auto
fix k assume k:"k \<in> snd ` s" then obtain xk where xk:"(xk, k) \<in> s" by auto
- thus "k \<subseteq> i" "k \<noteq> {}" "\<exists>a b. k = {a..b}" using assm apply- by fastsimp+
+ thus "k \<subseteq> i" "k \<noteq> {}" "\<exists>a b. k = {a..b}" using assm apply- by fastforce+
fix k' assume k':"k' \<in> snd ` s" "k \<noteq> k'" from this(1) obtain xk' where xk':"(xk', k') \<in> s" by auto
thus "interior k \<inter> interior k' = {}" apply-apply(rule assm(5)) apply(rule xk xk')+ using k' by auto
qed
@@ -967,7 +967,7 @@
subsection {* The set we're concerned with must be closed. *}
lemma division_of_closed: "s division_of i \<Longrightarrow> closed (i::('n::ordered_euclidean_space) set)"
- unfolding division_of_def by fastsimp
+ unfolding division_of_def by fastforce
subsection {* General bisection principle for intervals; might be useful elsewhere. *}
@@ -1015,8 +1015,8 @@
assume "s \<noteq> t" hence "\<not> (c = e \<and> d = f)" unfolding c_d e_f by auto
then obtain i where "c$$i \<noteq> e$$i \<or> d$$i \<noteq> f$$i" and i':"i<DIM('a)" unfolding de_Morgan_conj euclidean_eq[where 'a='a] by auto
hence i:"c$$i \<noteq> e$$i" "d$$i \<noteq> f$$i" apply- apply(erule_tac[!] disjE)
- proof- assume "c$$i \<noteq> e$$i" thus "d$$i \<noteq> f$$i" using c_d(2)[of i] e_f(2)[of i] by fastsimp
- next assume "d$$i \<noteq> f$$i" thus "c$$i \<noteq> e$$i" using c_d(2)[of i] e_f(2)[of i] by fastsimp
+ proof- assume "c$$i \<noteq> e$$i" thus "d$$i \<noteq> f$$i" using c_d(2)[of i] e_f(2)[of i] by fastforce
+ next assume "d$$i \<noteq> f$$i" thus "c$$i \<noteq> e$$i" using c_d(2)[of i] e_f(2)[of i] by fastforce
qed have *:"\<And>s t. (\<And>a. a\<in>s \<Longrightarrow> a\<in>t \<Longrightarrow> False) \<Longrightarrow> s \<inter> t = {}" by auto
show "interior s \<inter> interior t = {}" unfolding e_f c_d interior_closed_interval proof(rule *)
fix x assume "x\<in>{c<..<d}" "x\<in>{e<..<f}"
@@ -1024,9 +1024,9 @@
apply-apply(erule_tac[!] x=i in allE)+ by auto
show False using c_d(2)[OF i'] apply- apply(erule_tac disjE)
proof(erule_tac[!] conjE) assume as:"c $$ i = a $$ i" "d $$ i = (a $$ i + b $$ i) / 2"
- show False using e_f(2)[of i] and i x unfolding as by(fastsimp simp add:field_simps)
+ show False using e_f(2)[of i] and i x unfolding as by(fastforce simp add:field_simps)
next assume as:"c $$ i = (a $$ i + b $$ i) / 2" "d $$ i = b $$ i"
- show False using e_f(2)[of i] and i x unfolding as by(fastsimp simp add:field_simps)
+ show False using e_f(2)[of i] and i x unfolding as by(fastforce simp add:field_simps)
qed qed qed
also have "\<Union> ?A = {a..b}" proof(rule set_eqI,rule)
fix x assume "x\<in>\<Union>?A" then guess Y unfolding Union_iff ..
@@ -1606,7 +1606,7 @@
thus "l \<subseteq> d1 x" unfolding xl' by auto
show "x\<in>l" "l \<subseteq> {a..b} \<inter> {x. x $$ k \<le> c}" unfolding xl' using p(4-6)[OF xl'(3)] using xl'(4)
using lem0(1)[OF xl'(3-4)] by auto
- show "\<exists>a b. l = {a..b}" unfolding xl' using p(6)[OF xl'(3)] by(fastsimp simp add: interval_split[OF k,where c=c])
+ show "\<exists>a b. l = {a..b}" unfolding xl' using p(6)[OF xl'(3)] by(fastforce simp add: interval_split[OF k,where c=c])
fix y r let ?goal = "interior l \<inter> interior r = {}" assume yr:"(y,r)\<in>?M1"
then guess y' r' unfolding mem_Collect_eq apply- unfolding Pair_eq apply((erule exE)+,(erule conjE)+) . note yr'=this
assume as:"(x,l) \<noteq> (y,r)" show "interior l \<inter> interior r = {}"
@@ -1626,7 +1626,7 @@
thus "l \<subseteq> d2 x" unfolding xl' by auto
show "x\<in>l" "l \<subseteq> {a..b} \<inter> {x. x $$ k \<ge> c}" unfolding xl' using p(4-6)[OF xl'(3)] using xl'(4)
using lem0(2)[OF xl'(3-4)] by auto
- show "\<exists>a b. l = {a..b}" unfolding xl' using p(6)[OF xl'(3)] by(fastsimp simp add: interval_split[OF k, where c=c])
+ show "\<exists>a b. l = {a..b}" unfolding xl' using p(6)[OF xl'(3)] by(fastforce simp add: interval_split[OF k, where c=c])
fix y r let ?goal = "interior l \<inter> interior r = {}" assume yr:"(y,r)\<in>?M2"
then guess y' r' unfolding mem_Collect_eq apply- unfolding Pair_eq apply((erule exE)+,(erule conjE)+) . note yr'=this
assume as:"(x,l) \<noteq> (y,r)" show "interior l \<inter> interior r = {}"
@@ -1689,11 +1689,11 @@
apply(subst setsum_Un_zero) apply(rule p1 p2)+ apply(rule) unfolding split_paired_all split_conv
proof- fix a b assume ab:"(a,b) \<in> p1 \<inter> p2"
have "(a,b) \<in> p1" using ab by auto from p1(4)[OF this] guess u v apply-by(erule exE)+ note uv =this
- have "b \<subseteq> {x. x$$k = c}" using ab p1(3)[of a b] p2(3)[of a b] by fastsimp
+ have "b \<subseteq> {x. x$$k = c}" using ab p1(3)[of a b] p2(3)[of a b] by fastforce
moreover have "interior {x::'a. x $$ k = c} = {}"
proof(rule ccontr) case goal1 then obtain x where x:"x\<in>interior {x::'a. x$$k = c}" by auto
then guess e unfolding mem_interior .. note e=this
- have x:"x$$k = c" using x interior_subset by fastsimp
+ have x:"x$$k = c" using x interior_subset by fastforce
have *:"\<And>i. i<DIM('a) \<Longrightarrow> \<bar>(x - (x + (\<chi>\<chi> i. if i = k then e / 2 else 0))) $$ i\<bar>
= (if i = k then e/2 else 0)" using e by auto
have "(\<Sum>i<DIM('a). \<bar>(x - (x + (\<chi>\<chi> i. if i = k then e / 2 else 0))) $$ i\<bar>) =
@@ -1790,7 +1790,7 @@
lemma monoidalI: assumes "\<And>x y. opp x y = opp y x"
"\<And>x y z. opp x (opp y z) = opp (opp x y) z"
"\<And>x. opp (neutral opp) x = x" shows "monoidal opp"
- unfolding monoidal_def using assms by fastsimp
+ unfolding monoidal_def using assms by fastforce
lemma monoidal_ac: assumes "monoidal opp"
shows "opp (neutral opp) a = a" "opp a (neutral opp) = a" "opp a b = opp b a"
@@ -2721,7 +2721,7 @@
lemma integrable_spike: assumes "negligible s" "\<forall>x\<in>(t - s). g x = f x" "f integrable_on t"
shows "g integrable_on t"
using assms unfolding integrable_on_def apply-apply(erule exE)
- apply(rule,rule has_integral_spike) by fastsimp+
+ apply(rule,rule has_integral_spike) by fastforce+
lemma integral_spike: assumes "negligible s" "\<forall>x\<in>(t - s). g x = f x"
shows "integral t f = integral t g"
@@ -2860,7 +2860,7 @@
proof safe show "(\<lambda>y. f x) integrable_on l" unfolding integrable_on_def l by(rule,rule has_integral_const)
fix y assume y:"y\<in>l" note fineD[OF p(2) as,unfolded subset_eq,rule_format,OF this]
note d(2)[OF _ _ this[unfolded mem_ball]]
- thus "norm (f y - f x) \<le> e" using y p'(2-3)[OF as] unfolding dist_norm l norm_minus_commute by fastsimp qed qed
+ thus "norm (f y - f x) \<le> e" using y p'(2-3)[OF as] unfolding dist_norm l norm_minus_commute by fastforce qed qed
from e have "0 \<le> e" by auto from approximable_on_division[OF this division_of_tagged_division[OF p(1)] *] guess g .
thus "\<exists>g. (\<forall>x\<in>{a..b}. norm (f x - g x) \<le> e) \<and> g integrable_on {a..b}" by auto qed
@@ -3034,7 +3034,7 @@
def y \<equiv> "(\<chi>\<chi> j. if j = i then if c$$i \<le> (a$$i + b$$i) / 2 then c$$i +
min e (b$$i - c$$i) / 2 else c$$i - min e (c$$i - a$$i) / 2 else x$$j)::'a"
show "\<exists>x'\<in>\<Union>(s - {k}). x' \<noteq> x \<and> dist x' x < e" apply(rule_tac x=y in bexI)
- proof have "d \<in> {c..d}" using s(3)[OF k(1)] unfolding k interval_eq_empty mem_interval by(fastsimp simp add: not_less)
+ proof have "d \<in> {c..d}" using s(3)[OF k(1)] unfolding k interval_eq_empty mem_interval by(fastforce simp add: not_less)
hence "d \<in> {a..b}" using s(2)[OF k(1)] unfolding k by auto note di = this[unfolded mem_interval,THEN spec[where x=i]]
hence xyi:"y$$i \<noteq> x$$i" unfolding y_def unfolding i xi euclidean_lambda_beta'[OF i(2)] if_P[OF refl]
apply(cases) apply(subst if_P,assumption) unfolding if_not_P not_le using as(2)
@@ -3099,7 +3099,7 @@
lemma integrable_combine: fixes f::"real \<Rightarrow> 'a::banach"
assumes "a \<le> c" "c \<le> b" "f integrable_on {a..c}" "f integrable_on {c..b}"
- shows "f integrable_on {a..b}" using assms unfolding integrable_on_def by(fastsimp intro!:has_integral_combine)
+ shows "f integrable_on {a..b}" using assms unfolding integrable_on_def by(fastforce intro!:has_integral_combine)
subsection {* Reduce integrability to "local" integrability. *}
@@ -3219,7 +3219,7 @@
thus "x \<in> \<Union>{k. \<exists>x. (x, k) \<in> (\<lambda>(x, k). (g x, g ` k)) ` p}" apply-
apply(rule_tac X="g ` X" in UnionI) defer apply(rule_tac x="h x" in image_eqI)
using X(2) assms(3)[rule_format,of x] by auto
- qed note ** = d(2)[OF this] have *:"inj_on (\<lambda>(x, k). (g x, g ` k)) p" using inj(1) unfolding inj_on_def by fastsimp
+ qed note ** = d(2)[OF this] have *:"inj_on (\<lambda>(x, k). (g x, g ` k)) p" using inj(1) unfolding inj_on_def by fastforce
have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _") unfolding algebra_simps add_left_cancel
unfolding setsum_reindex[OF *] apply(subst scaleR_right.setsum) defer apply(rule setsum_cong2) unfolding o_def split_paired_all split_conv
apply(drule p(4)) apply safe unfolding assms(7)[rule_format] using p by auto
@@ -4347,7 +4347,7 @@
shows "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x - integral k f) p) \<le> e" (is "?x \<le> e")
proof- { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" thus ?thesis by (blast intro: field_le_epsilon) }
fix k::real assume k:"k>0" note p' = tagged_partial_division_ofD[OF p(1)]
- have "\<Union>snd ` p \<subseteq> {a..b}" using p'(3) by fastsimp
+ have "\<Union>snd ` p \<subseteq> {a..b}" using p'(3) by fastforce
note partial_division_of_tagged_division[OF p(1)] this
from partial_division_extend_interval[OF this] guess q . note q=this and q' = division_ofD[OF this(2)]
def r \<equiv> "q - snd ` p" have "snd ` p \<inter> r = {}" unfolding r_def by auto
@@ -4380,7 +4380,7 @@
apply(rule,rule q') using q(1) p' unfolding r_def by auto qed
moreover have "\<Union>snd ` p \<union> \<Union>r = {a..b}" "{qq i |i. i \<in> r} = qq ` r"
unfolding Union_Un_distrib[THEN sym] r_def using q by auto
- ultimately show "?p tagged_division_of {a..b}" by fastsimp qed
+ ultimately show "?p tagged_division_of {a..b}" by fastforce qed
hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>\<Union>qq ` r. content k *\<^sub>R f x) -
integral {a..b} f) < e" apply(subst setsum_Un_zero[THEN sym]) apply(rule p') prefer 3
@@ -5448,7 +5448,7 @@
have "\<exists>y\<in>?S. \<not> y \<ge> i + e"
proof(rule ccontr) case goal1 hence "i \<ge> i + e" apply-
- apply(rule isGlb_le_isLb[OF i]) apply(rule isLbI) unfolding setge_def by fastsimp+
+ apply(rule isGlb_le_isLb[OF i]) apply(rule isLbI) unfolding setge_def by fastforce+
thus False using e by auto
qed then guess y .. note y=this[unfolded not_le]
from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
@@ -5492,7 +5492,7 @@
have "\<exists>y\<in>?S. \<not> y \<le> i - e"
proof(rule ccontr) case goal1 hence "i \<le> i - e" apply-
- apply(rule isLub_le_isUb[OF i]) apply(rule isUbI) unfolding setle_def by fastsimp+
+ apply(rule isLub_le_isUb[OF i]) apply(rule isUbI) unfolding setle_def by fastforce+
thus False using e by auto
qed then guess y .. note y=this[unfolded not_le]
from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Sep 12 07:55:43 2011 +0200
@@ -1256,7 +1256,7 @@
have "x\<in>UNIV" by auto from this[unfolded span_basis[THEN sym]]
have "\<exists>u. (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R v) = x"
unfolding range_basis span_insert_0 apply(subst (asm) span_finite) by auto
- thus ?thesis by fastsimp
+ thus ?thesis by fastforce
qed
lemma span_basis'[simp]:"span ((basis::nat=>'a) ` {..<DIM('a::euclidean_space)}) = UNIV"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Sep 12 07:55:43 2011 +0200
@@ -4224,8 +4224,8 @@
unfolding compact_eq_bounded_closed
using bounded_Int and closed_Int and assms(1) by auto
ultimately obtain x where "x\<in>cball a (dist b a) \<inter> s" "\<forall>y\<in>cball a (dist b a) \<inter> s. dist a x \<le> dist a y"
- using continuous_attains_inf[of ?B "dist a"] by fastsimp
- thus ?thesis by fastsimp
+ using continuous_attains_inf[of ?B "dist a"] by fastforce
+ thus ?thesis by fastforce
qed
@@ -4603,7 +4603,7 @@
lemma interval_ne_empty: fixes a :: "'a::ordered_euclidean_space" shows
"{a .. b} \<noteq> {} \<longleftrightarrow> (\<forall>i<DIM('a). a$$i \<le> b$$i)" and
"{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i<DIM('a). a$$i < b$$i)"
- unfolding interval_eq_empty[of a b] by fastsimp+
+ unfolding interval_eq_empty[of a b] by fastforce+
lemma interval_sing:
fixes a :: "'a::ordered_euclidean_space"
@@ -4672,7 +4672,7 @@
} note part1 = this
show ?th3 unfolding subset_eq and Ball_def and mem_interval
apply(rule,rule,rule,rule) apply(rule part1) unfolding subset_eq and Ball_def and mem_interval
- prefer 4 apply auto by(erule_tac x=i in allE,erule_tac x=i in allE,fastsimp)+
+ prefer 4 apply auto by(erule_tac x=i in allE,erule_tac x=i in allE,fastforce)+
{ assume as:"{c<..<d} \<subseteq> {a<..<b}" "\<forall>i<DIM('a). c$$i < d$$i"
fix i assume i:"i<DIM('a)"
from as(1) have "{c<..<d} \<subseteq> {a..b}" using interval_open_subset_closed[of a b] by auto
@@ -5834,7 +5834,7 @@
{ assume as:"dist a b > dist (f n x) (f n y)"
then obtain Na Nb where "\<forall>m\<ge>Na. dist (f (r m) x) a < (dist a b - dist (f n x) (f n y)) / 2"
and "\<forall>m\<ge>Nb. dist (f (r m) y) b < (dist a b - dist (f n x) (f n y)) / 2"
- using lima limb unfolding h_def Lim_sequentially by (fastsimp simp del: less_divide_eq_number_of1)
+ using lima limb unfolding h_def Lim_sequentially by (fastforce simp del: less_divide_eq_number_of1)
hence "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) < dist a b - dist (f n x) (f n y)"
apply(erule_tac x="Na+Nb+n" in allE)
apply(erule_tac x="Na+Nb+n" in allE) apply simp
@@ -5853,10 +5853,10 @@
have [simp]:"a = b" proof(rule ccontr)
def e \<equiv> "dist a b - dist (g a) (g b)"
- assume "a\<noteq>b" hence "e > 0" unfolding e_def using dist by fastsimp
+ assume "a\<noteq>b" hence "e > 0" unfolding e_def using dist by fastforce
hence "\<exists>n. dist (f n x) a < e/2 \<and> dist (f n y) b < e/2"
using lima limb unfolding Lim_sequentially
- apply (auto elim!: allE[where x="e/2"]) apply(rule_tac x="r (max N Na)" in exI) unfolding h_def by fastsimp
+ apply (auto elim!: allE[where x="e/2"]) apply(rule_tac x="r (max N Na)" in exI) unfolding h_def by fastforce
then obtain n where n:"dist (f n x) a < e/2 \<and> dist (f n y) b < e/2" by auto
have "dist (f (Suc n) x) (g a) \<le> dist (f n x) a"
using dist[THEN bspec[where x="f n x"], THEN bspec[where x="a"]] and fs by auto
@@ -5869,7 +5869,7 @@
have [simp]:"\<And>n. f (Suc n) x = f n y" unfolding f_def y_def by(induct_tac n)auto
{ fix x y assume "x\<in>s" "y\<in>s" moreover
fix e::real assume "e>0" ultimately
- have "dist y x < e \<longrightarrow> dist (g y) (g x) < e" using dist by fastsimp }
+ have "dist y x < e \<longrightarrow> dist (g y) (g x) < e" using dist by fastforce }
hence "continuous_on s g" unfolding continuous_on_iff by auto
hence "((snd \<circ> h \<circ> r) ---> g a) sequentially" unfolding continuous_on_sequentially
--- a/src/HOL/Nat.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Nat.thy Mon Sep 12 07:55:43 2011 +0200
@@ -320,7 +320,7 @@
lemma one_eq_mult_iff [simp,no_atp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
apply (rule trans)
- apply (rule_tac [2] mult_eq_1_iff, fastsimp)
+ apply (rule_tac [2] mult_eq_1_iff, fastforce)
done
lemma nat_mult_eq_1_iff [simp]: "m * n = (1::nat) \<longleftrightarrow> m = 1 \<and> n = 1"
--- a/src/HOL/Nominal/Examples/Fsub.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy Mon Sep 12 07:55:43 2011 +0200
@@ -665,7 +665,7 @@
nominal_inductive subtype_of
apply (simp_all add: abs_fresh)
- apply (fastsimp simp add: valid_ty_dom_fresh dest: subtype_implies_ok)
+ apply (fastforce simp add: valid_ty_dom_fresh dest: subtype_implies_ok)
apply (force simp add: closed_in_fresh dest: subtype_implies_closed subtype_implies_ok)+
done
@@ -1030,7 +1030,7 @@
case (SA_all T\<^isub>1 S\<^isub>1 Y S\<^isub>2 T\<^isub>2 \<Gamma> X \<Delta>)
have IH_inner\<^isub>1: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> T\<^isub>1 <: S\<^isub>1"
and IH_inner\<^isub>2: "(((TVarB Y T\<^isub>1)#\<Delta>)@[(TVarB X P)]@\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2"
- by (fastsimp intro: SA_all)+
+ by (fastforce intro: SA_all)+
then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> (\<forall>Y<:S\<^isub>1. S\<^isub>2) <: (\<forall>Y<:T\<^isub>1. T\<^isub>2)" by auto
qed
}
@@ -1401,7 +1401,7 @@
show ?case using h1 h2 by auto
next
case (SA_all T1 S1 X S2 T2)
- have h1:"((TVarB X T1 # \<Gamma>) @ \<Delta>)\<turnstile>S2<:T2" by (fastsimp intro: SA_all)
+ have h1:"((TVarB X T1 # \<Gamma>) @ \<Delta>)\<turnstile>S2<:T2" by (fastforce intro: SA_all)
have h2:"(\<Gamma> @ \<Delta>)\<turnstile>T1<:S1" using SA_all by auto
then show ?case using h1 h2 by auto
qed (auto)
@@ -1421,16 +1421,16 @@
then show ?case by force
next
case (T_Abs x T1 t2 T2 P D)
- then show ?case by (fastsimp dest: typing_ok)
+ then show ?case by (fastforce dest: typing_ok)
next
case (T_Sub t S T P D)
- then show ?case using subtype_narrow by fastsimp
+ then show ?case using subtype_narrow by fastforce
next
case (T_TAbs X' T1 t2 T2 P D)
- then show ?case by (fastsimp dest: typing_ok)
+ then show ?case by (fastforce dest: typing_ok)
next
case (T_TApp X' t1 T2 T11 T12 P D)
- then have "D @ TVarB X P # \<Gamma> \<turnstile> t1 : Forall X' T12 T11" by fastsimp
+ then have "D @ TVarB X P # \<Gamma> \<turnstile> t1 : Forall X' T12 T11" by fastforce
moreover have "(D @ [TVarB X Q] @ \<Gamma>) \<turnstile> T2<:T11" using T_TApp by auto
then have "(D @ [TVarB X P] @ \<Gamma>) \<turnstile> T2<:T11" using `\<Gamma>\<turnstile>P<:Q`
by (rule subtype_narrow)
@@ -1474,7 +1474,7 @@
case (T_TAbs X T1 t2 T2 x u D)
from `TVarB X T1 # D @ VarB x U # \<Gamma> \<turnstile> t2 : T2` have "X \<sharp> T1"
by (auto simp add: valid_ty_dom_fresh dest: typing_ok intro!: closed_in_fresh)
- with `X \<sharp> u` and T_TAbs show ?case by fastsimp
+ with `X \<sharp> u` and T_TAbs show ?case by fastforce
next
case (T_TApp X t1 T2 T11 T12 x u D)
then have "(D@\<Gamma>) \<turnstile>T2<:T11" using T_TApp by (auto dest: strengthening)
--- a/src/HOL/Nominal/Examples/Standardization.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Nominal/Examples/Standardization.thy Mon Sep 12 07:55:43 2011 +0200
@@ -296,7 +296,7 @@
apply (erule exE)
apply (rename_tac ts)
apply (case_tac ts)
- apply fastsimp
+ apply fastforce
apply force
apply (erule disjE)
apply blast
--- a/src/HOL/Number_Theory/MiscAlgebra.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy Mon Sep 12 07:55:43 2011 +0200
@@ -259,7 +259,7 @@
apply blast
apply (erule finite_UN_I)
apply blast
- apply (fastsimp)
+ apply (fastforce)
apply (auto intro!: funcsetI finprod_closed)
done
--- a/src/HOL/Old_Number_Theory/Factorization.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Old_Number_Theory/Factorization.thy Mon Sep 12 07:55:43 2011 +0200
@@ -128,7 +128,7 @@
"primel xs \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> Suc 0 < prod xs"
apply (induct xs)
apply simp
- apply (fastsimp simp: primel_def prime_def elim: one_less_mult)
+ apply (fastforce simp: primel_def prime_def elim: one_less_mult)
done
lemma primel_prod_gz: "primel xs ==> 0 < prod xs"
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Mon Sep 12 07:55:43 2011 +0200
@@ -527,7 +527,7 @@
ultimately have "int(card (S1)) = setsum (%j. int(card (f1 j))) P_set"
by auto
also have "... = setsum (%j. q * j div p) P_set"
- using aux3a by(fastsimp intro: setsum_cong)
+ using aux3a by(fastforce intro: setsum_cong)
finally show ?thesis .
qed
@@ -551,7 +551,7 @@
ultimately have "int(card (S2)) = setsum (%j. int(card (f2 j))) Q_set"
by auto
also have "... = setsum (%j. p * j div q) Q_set"
- using aux3b by(fastsimp intro: setsum_cong)
+ using aux3b by(fastforce intro: setsum_cong)
finally show ?thesis .
qed
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Mon Sep 12 07:55:43 2011 +0200
@@ -283,8 +283,8 @@
code_pred [random_dseq inductify] matrix
apply (cases x)
- unfolding matrix_def apply fastsimp
- apply fastsimp done
+ unfolding matrix_def apply fastforce
+ apply fastforce done
values [random_dseq 2, 2, 15] 6 "{(M::int list list, n, m). matrix M n m}"
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Mon Sep 12 07:55:43 2011 +0200
@@ -244,7 +244,7 @@
from alt_nil nil show thesis by auto
next
case cons
- from alt_cons cons show thesis by fastsimp
+ from alt_cons cons show thesis by fastforce
qed
qed
@@ -469,7 +469,7 @@
next
fix xs ys zs x
assume "xa = x # xs" "xb = ys" "xc = x # zs" "append2 xs ys zs"
- from this append2(2) show thesis by fastsimp
+ from this append2(2) show thesis by fastforce
qed
qed
@@ -913,7 +913,7 @@
assume "has_length xs i" "has_length ys i" "r (x, y)"
from this has_length show "lexn r (Suc i) (x # xs, y # ys)"
unfolding lexn_conv Collect_def mem_def
- by fastsimp
+ by fastforce
next
assume "lexn r i (xs, ys)"
thm lexn_conv
@@ -935,8 +935,8 @@
apply (auto simp add: has_length)
apply (case_tac xys)
apply auto
- apply fastsimp
- apply fastsimp done
+ apply fastforce
+ apply fastforce done
qed
values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
--- a/src/HOL/Presburger.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Presburger.thy Mon Sep 12 07:55:43 2011 +0200
@@ -28,7 +28,7 @@
"\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})<z. (d dvd x + s) = (d dvd x + s)"
"\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
"\<exists>z.\<forall>x<z. F = F"
- by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastsimp)+) simp_all
+ by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastforce)+) simp_all
lemma pinf:
"\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x>z. P x = P' x; \<exists>z.\<forall>x>z. Q x = Q' x\<rbrakk>
@@ -44,7 +44,7 @@
"\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})>z. (d dvd x + s) = (d dvd x + s)"
"\<exists>z.\<forall>(x::'a::{linorder,plus,Rings.dvd})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
"\<exists>z.\<forall>x>z. F = F"
- by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastsimp)+) simp_all
+ by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastforce)+) simp_all
lemma inf_period:
"\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk>
@@ -342,7 +342,7 @@
lemma simp_from_to: "{i..j::int} = (if j < i then {} else insert i {i+1..j})"
apply(simp add:atLeastAtMost_def atLeast_def atMost_def)
-apply(fastsimp)
+apply(fastforce)
done
theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Rings.dvd}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
--- a/src/HOL/Probability/Binary_Product_Measure.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Mon Sep 12 07:55:43 2011 +0200
@@ -106,7 +106,7 @@
apply - apply (rule bexI[of _ "space M1"]) apply (rule bexI[of _ X])
using M2.sets_into_space by force+ }
ultimately have "?fst \<and> ?snd"
- by (fastsimp simp: measurable_def sets_sigma space_pair_measure
+ by (fastforce simp: measurable_def sets_sigma space_pair_measure
intro!: sigma_sets.Basic)
then show ?fst ?snd by auto
qed
@@ -437,7 +437,7 @@
show ?thesis unfolding space_pair_measure
proof (intro exI[of _ ?F] conjI allI)
show "range ?F \<subseteq> sets E" using F1 F2
- by (fastsimp intro!: pair_measure_generatorI)
+ by (fastforce intro!: pair_measure_generatorI)
next
have "space M1 \<times> space M2 \<subseteq> (\<Union>i. ?F i)"
proof (intro subsetI)
--- a/src/HOL/Probability/Borel_Space.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Mon Sep 12 07:55:43 2011 +0200
@@ -127,7 +127,7 @@
"\<forall>S\<in>sets borel. ?f -` S \<inter> A \<in> op \<inter> A ` sets M"
then have "?f -` S \<inter> A \<in> op \<inter> A ` sets M" by auto
then have f: "?f -` S \<inter> A \<in> sets M"
- using `A \<in> sets M` sets_into_space by fastsimp
+ using `A \<in> sets M` sets_into_space by fastforce
show "?f -` S \<inter> space M \<in> sets M"
proof cases
assume "0 \<in> S"
--- a/src/HOL/Probability/Finite_Product_Measure.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Mon Sep 12 07:55:43 2011 +0200
@@ -477,7 +477,7 @@
proof (unfold measurable_def, intro CollectI conjI ballI)
fix A assume "A \<in> sets (M i)"
then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) = (\<Pi>\<^isub>E j\<in>I. if i = j then A else space (M j))"
- using M.sets_into_space `i \<in> I` by (fastsimp dest: Pi_mem split: split_if_asm)
+ using M.sets_into_space `i \<in> I` by (fastforce dest: Pi_mem split: split_if_asm)
then show "(\<lambda>x. x i) -` A \<inter> space (Pi\<^isub>M I M) \<in> sets (Pi\<^isub>M I M)"
using `A \<in> sets (M i)` by (auto intro!: product_algebraI)
qed (insert `i \<in> I`, auto)
@@ -641,8 +641,8 @@
show "?m (Pi\<^isub>E (insert i I) A) = (\<Prod>i\<in>insert i I. M.\<mu> i (A i))"
unfolding * using A
apply (subst P.pair_measure_times)
- using A apply fastsimp
- using A apply fastsimp
+ using A apply fastforce
+ using A apply fastforce
using `i \<notin> I` `finite I` prod[of A] A by (auto simp: ac_simps) }
note product = this
have *: "sigma I'.G\<lparr> measure := ?\<nu> \<rparr> = I'.P\<lparr> measure := ?\<nu> \<rparr>"
--- a/src/HOL/Probability/Information.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Probability/Information.thy Mon Sep 12 07:55:43 2011 +0200
@@ -35,7 +35,7 @@
have "convex_on {0 <..} (\<lambda> x. - log b x)"
by (rule minus_log_convex[OF `b > 1`])
hence "- log b (\<Sum> i \<in> s. a i * y i) \<le> (\<Sum> i \<in> s. a i * - log b (y i))"
- using convex_on_setsum[of _ _ "\<lambda> x. - log b x"] assms pos_is_convex by fastsimp
+ using convex_on_setsum[of _ _ "\<lambda> x. - log b x"] assms pos_is_convex by fastforce
thus ?thesis by (auto simp add:setsum_negf le_imp_neg_le)
qed
@@ -1327,7 +1327,7 @@
shows "finite (g`A)"
proof -
from subvimage_translator_image[OF svi]
- obtain h where "g`A = h`f`A" by fastsimp
+ obtain h where "g`A = h`f`A" by fastforce
with fin show "finite (g`A)" by simp
qed
--- a/src/HOL/Probability/Lebesgue_Integration.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Mon Sep 12 07:55:43 2011 +0200
@@ -216,7 +216,7 @@
shows "simple_function M f \<longleftrightarrow> finite (f`space M) \<and> f \<in> borel_measurable M"
using simple_function_borel_measurable[of f]
borel_measurable_simple_function[of f]
- by (fastsimp simp: simple_function_def)
+ by (fastforce simp: simple_function_def)
lemma (in sigma_algebra) simple_function_const[intro, simp]:
"simple_function M (\<lambda>x. c)"
@@ -462,7 +462,7 @@
have f: "finite (f`A) \<longleftrightarrow> finite (?f`space M)"
proof cases
assume "A = space M"
- then have "f`A = ?f`space M" by (fastsimp simp: image_iff)
+ then have "f`A = ?f`space M" by (fastforce simp: image_iff)
then show ?thesis by simp
next
assume "A \<noteq> space M"
--- a/src/HOL/Probability/Lebesgue_Measure.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Mon Sep 12 07:55:43 2011 +0200
@@ -18,7 +18,7 @@
unfolding cube_def by auto
lemma cube_subset[intro]: "n \<le> N \<Longrightarrow> cube n \<subseteq> cube N"
- by (fastsimp simp: eucl_le[where 'a='a] cube_def)
+ by (fastforce simp: eucl_le[where 'a='a] cube_def)
lemma cube_subset_iff:
"cube n \<subseteq> cube N \<longleftrightarrow> n \<le> N"
@@ -26,9 +26,9 @@
assume subset: "cube n \<subseteq> (cube N::'a set)"
then have "((\<chi>\<chi> i. real n)::'a) \<in> cube N"
using DIM_positive[where 'a='a]
- by (fastsimp simp: cube_def eucl_le[where 'a='a])
+ by (fastforce simp: cube_def eucl_le[where 'a='a])
then show "n \<le> N"
- by (fastsimp simp: cube_def eucl_le[where 'a='a])
+ by (fastforce simp: cube_def eucl_le[where 'a='a])
next
assume "n \<le> N" then show "cube n \<subseteq> (cube N::'a set)" by (rule cube_subset)
qed
@@ -873,7 +873,7 @@
show "Int_stable ?E" using Int_stable_cuboids .
show "range cube \<subseteq> sets ?E" unfolding cube_def_raw by auto
show "incseq cube" using cube_subset_Suc by (auto intro!: incseq_SucI)
- { fix x have "\<exists>n. x \<in> cube n" using mem_big_cube[of x] by fastsimp }
+ { fix x have "\<exists>n. x \<in> cube n" using mem_big_cube[of x] by fastforce }
then show "(\<Union>i. cube i) = space ?E" by auto
{ fix i show "lborel.\<mu> (cube i) \<noteq> \<infinity>" unfolding cube_def by auto }
show "A \<in> sets (sigma ?E)" "sets (sigma ?E) = sets lborel" "space ?E = space lborel"
@@ -997,7 +997,7 @@
proof (rule measure_unique_Int_stable[where X=X, OF Int_stable_atLeastAtMost], unfold * **)
show "X \<in> sets (sigma ?E)"
unfolding borel_eq_atLeastAtMost[symmetric] by fact
- have "\<And>x. \<exists>xa. x \<in> cube xa" apply(rule_tac x=x in mem_big_cube) by fastsimp
+ have "\<And>x. \<exists>xa. x \<in> cube xa" apply(rule_tac x=x in mem_big_cube) by fastforce
then show "(\<Union>i. cube i) = space ?E" by auto
show "incseq cube" by (intro incseq_SucI cube_subset_Suc)
show "range cube \<subseteq> sets ?E"
--- a/src/HOL/Probability/Measure.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Probability/Measure.thy Mon Sep 12 07:55:43 2011 +0200
@@ -940,7 +940,7 @@
proof (intro exI[of _ "\<lambda>n. \<Union>i\<le>n. F i"] conjI allI)
from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto
then show "(\<Union>n. \<Union> i\<le>n. F i) = space M"
- using F by fastsimp
+ using F by fastforce
next
fix n
have "\<mu> (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. \<mu> (F i))" using F
--- a/src/HOL/Probability/Probability_Measure.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy Mon Sep 12 07:55:43 2011 +0200
@@ -989,8 +989,8 @@
also have "\<dots> = real_of_nat (card (space M)) * prob {x}" by simp
finally have one: "1 = real (card (space M)) * prob {x}"
using real_eq_of_nat by auto
- hence two: "real (card (space M)) \<noteq> 0" by fastsimp
- from one have three: "prob {x} \<noteq> 0" by fastsimp
+ hence two: "real (card (space M)) \<noteq> 0" by fastforce
+ from one have three: "prob {x} \<noteq> 0" by fastforce
thus ?thesis using one two three divide_cancel_right
by (auto simp:field_simps)
qed
--- a/src/HOL/Probability/Radon_Nikodym.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy Mon Sep 12 07:55:43 2011 +0200
@@ -32,7 +32,7 @@
show ?thesis
proof (safe intro!: bexI[of _ ?h] del: notI)
have "\<And>i. A i \<in> sets M"
- using range by fastsimp+
+ using range by fastforce+
then have "integral\<^isup>P M ?h = (\<Sum>i. n i * \<mu> (A i))" using pos
by (simp add: positive_integral_suminf positive_integral_cmult_indicator)
also have "\<dots> \<le> (\<Sum>i. (1 / 2)^Suc i)"
@@ -640,7 +640,7 @@
have Union: "(SUP i. \<mu> (?O i)) = \<mu> (\<Union>i. ?O i)"
proof (rule continuity_from_below[of ?O])
show "range ?O \<subseteq> sets M" using Q' by (auto intro!: finite_UN)
- show "incseq ?O" by (fastsimp intro!: incseq_SucI)
+ show "incseq ?O" by (fastforce intro!: incseq_SucI)
qed
have Q'_sets: "\<And>i. Q' i \<in> sets M" using Q' by auto
have O_sets: "\<And>i. ?O i \<in> sets M"
@@ -654,7 +654,7 @@
also have "\<dots> < \<infinity>" using Q' by (simp add: setsum_Pinfty)
finally show "\<nu> (?O i) \<noteq> \<infinity>" by simp
qed auto
- have O_mono: "\<And>n. ?O n \<subseteq> ?O (Suc n)" by fastsimp
+ have O_mono: "\<And>n. ?O n \<subseteq> ?O (Suc n)" by fastforce
have a_eq: "?a = \<mu> (\<Union>i. ?O i)" unfolding Union[symmetric]
proof (rule antisym)
show "?a \<le> (SUP i. \<mu> (?O i))" unfolding a_Lim
@@ -676,7 +676,7 @@
show ?thesis
proof (intro bexI exI conjI ballI impI allI)
show "disjoint_family Q"
- by (fastsimp simp: disjoint_family_on_def Q_def
+ by (fastforce simp: disjoint_family_on_def Q_def
split: nat.split_asm)
show "range Q \<subseteq> sets M"
using Q_sets by auto
@@ -697,7 +697,7 @@
proof (rule continuity_from_below[of "\<lambda>i. ?O i \<union> A", symmetric, simplified])
show "range (\<lambda>i. ?O i \<union> A) \<subseteq> sets M"
using `\<nu> A \<noteq> \<infinity>` O_sets A by auto
- qed (fastsimp intro!: incseq_SucI)
+ qed (fastforce intro!: incseq_SucI)
also have "\<dots> \<le> ?a"
proof (safe intro!: SUP_leI)
fix i have "?O i \<union> A \<in> ?Q"
@@ -734,14 +734,14 @@
case 0 then show ?case by (simp add: Q_def)
next
case (Suc j)
- have eq: "\<And>j. (\<Union>i\<le>j. ?O i) = (\<Union>i\<le>j. Q' i)" by fastsimp
+ have eq: "\<And>j. (\<Union>i\<le>j. ?O i) = (\<Union>i\<le>j. Q' i)" by fastforce
have "{..j} \<union> {..Suc j} = {..Suc j}" by auto
then have "(\<Union>i\<le>Suc j. Q' i) = (\<Union>i\<le>j. Q' i) \<union> Q (Suc j)"
by (simp add: UN_Un[symmetric] Q_def del: UN_Un)
then show ?case using Suc by (auto simp add: eq atMost_Suc)
qed }
then have "(\<Union>j. (\<Union>i\<le>j. ?O i)) = (\<Union>j. (\<Union>i\<le>j. Q i))" by simp
- then show "space M - ?O_0 = space M - (\<Union>i. Q i)" by fastsimp
+ then show "space M - ?O_0 = space M - (\<Union>i. Q i)" by fastforce
qed
qed
--- a/src/HOL/Probability/Sigma_Algebra.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Mon Sep 12 07:55:43 2011 +0200
@@ -810,7 +810,7 @@
assumes "sets E \<subseteq> Pow (space E)" and "f \<in> space M \<rightarrow> space E"
shows "f \<in> measurable M (sigma E) \<longleftrightarrow> (\<forall>A\<in>sets E. f -` A \<inter> space M \<in> sets M)"
using measurable_sigma[OF assms]
- by (fastsimp simp: measurable_def sets_sigma intro: sigma_sets.intros)
+ by (fastforce simp: measurable_def sets_sigma intro: sigma_sets.intros)
section "Disjoint families"
@@ -1426,7 +1426,7 @@
assumes "sigma_algebra M" shows "dynkin_system M"
proof -
interpret sigma_algebra M by fact
- show ?thesis using sets_into_space by (fastsimp intro!: dynkin_systemI)
+ show ?thesis using sets_into_space by (fastforce intro!: dynkin_systemI)
qed
subsection "Intersection stable algebras"
@@ -1481,13 +1481,13 @@
{ fix D assume "A \<in> D" and d: "dynkin_system \<lparr> space = space M, sets = D \<rparr>"
then have "A \<subseteq> space M" by (auto simp: dynkin_system_def subset_class_def) }
moreover have "{D. dynkin_system \<lparr> space = space M, sets = D\<rparr> \<and> sets M \<subseteq> D} \<noteq> {}"
- using assms dynkin_system_trivial by fastsimp
+ using assms dynkin_system_trivial by fastforce
ultimately show "A \<subseteq> space (dynkin M)"
unfolding dynkin_def using assms
by simp (metis dynkin_system_def subset_class_def in_mono)
next
show "space (dynkin M) \<in> sets (dynkin M)"
- unfolding dynkin_def using dynkin_system.space by fastsimp
+ unfolding dynkin_def using dynkin_system.space by fastforce
next
fix A assume "A \<in> sets (dynkin M)"
then show "space (dynkin M) - A \<in> sets (dynkin M)"
@@ -1532,7 +1532,7 @@
assume "disjoint_family A" "range A \<subseteq> {Q. Q \<subseteq> space M \<and> Q \<inter> D \<in> sets M}"
then have "\<And>i. A i \<subseteq> space M" "disjoint_family (\<lambda>i. A i \<inter> D)"
"range (\<lambda>i. A i \<inter> D) \<subseteq> sets M" "(\<Union>x. A x) \<inter> D = (\<Union>x. A x \<inter> D)"
- by ((fastsimp simp: disjoint_family_on_def)+)
+ by ((fastforce simp: disjoint_family_on_def)+)
then show "(\<Union>x. A x) \<subseteq> space M \<and> (\<Union>x. A x) \<inter> D \<in> sets M"
by (auto simp del: UN_simps)
qed
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Mon Sep 12 07:55:43 2011 +0200
@@ -201,7 +201,7 @@
have *: "\<And>j. j < n \<Longrightarrow>
(x ! j = x ! (Suc j mod n)) = (y ! j = y ! (Suc j mod n))"
using inv unfolding inversion_def map_eq_conv payer_def coin_def
- by fastsimp
+ by fastforce
show "x = y"
proof (rule nth_equalityI, simp, rule allI, rule impI)
fix j assume "j < length x" hence "j < n" using `length xs = n` by simp
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Mon Sep 12 07:55:43 2011 +0200
@@ -476,11 +476,11 @@
also have "\<dots> = -(\<Sum>obs\<in>t`OB`msgs. \<P>(t\<circ>OB) {obs} * ?Ht obs)"
apply (subst SIGMA_image_vimage[symmetric, of "OB`msgs" t])
apply (subst setsum_reindex)
- apply (fastsimp intro!: inj_onI)
+ apply (fastforce intro!: inj_onI)
apply simp
apply (subst setsum_Sigma[symmetric, unfolded split_def])
- using finite_space apply fastsimp
- using finite_space apply fastsimp
+ using finite_space apply fastforce
+ using finite_space apply fastforce
apply (safe intro!: setsum_cong)
using P_t_sum_P_O
by (simp add: setsum_divide_distrib[symmetric] field_simps **
--- a/src/HOL/Proofs/Lambda/Commutation.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Proofs/Lambda/Commutation.thy Mon Sep 12 07:55:43 2011 +0200
@@ -68,7 +68,7 @@
lemma square_rtrancl_reflcl_commute:
"square R S (S^**) (R^==) ==> commute (R^**) (S^**)"
apply (unfold commute_def)
- apply (fastsimp dest: square_reflcl square_sym [THEN square_rtrancl])
+ apply (fastforce dest: square_reflcl square_sym [THEN square_rtrancl])
done
--- a/src/HOL/Proofs/Lambda/ListOrder.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Proofs/Lambda/ListOrder.thy Mon Sep 12 07:55:43 2011 +0200
@@ -49,7 +49,7 @@
apply (erule exE)
apply (rename_tac ts)
apply (case_tac ts)
- apply fastsimp
+ apply fastforce
apply force
apply (erule disjE)
apply blast
--- a/src/HOL/Proofs/Lambda/ParRed.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Proofs/Lambda/ParRed.thy Mon Sep 12 07:55:43 2011 +0200
@@ -58,7 +58,7 @@
lemma par_beta_lift [simp]:
"t => t' \<Longrightarrow> lift t n => lift t' n"
- by (induct t arbitrary: t' n) fastsimp+
+ by (induct t arbitrary: t' n) fastforce+
lemma par_beta_subst:
"s => s' \<Longrightarrow> t => t' \<Longrightarrow> t[s/n] => t'[s'/n]"
@@ -67,8 +67,8 @@
apply (erule par_beta_cases)
apply simp
apply (simp add: subst_subst [symmetric])
- apply (fastsimp intro!: par_beta_lift)
- apply fastsimp
+ apply (fastforce intro!: par_beta_lift)
+ apply fastforce
done
--- a/src/HOL/Proofs/Lambda/StrongNorm.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Proofs/Lambda/StrongNorm.thy Mon Sep 12 07:55:43 2011 +0200
@@ -158,7 +158,7 @@
(is "listsp IT (?ls as)")
proof induct
case Nil
- show ?case by fastsimp
+ show ?case by fastforce
next
case (Cons b bs)
hence I: "?R b" by simp
@@ -197,7 +197,7 @@
hence "listsp IT (map (\<lambda>x. x[u/i]) rs)"
proof induct
case Nil
- show ?case by fastsimp
+ show ?case by fastforce
next
case (Cons a as)
hence I: "?R a" by simp
@@ -214,7 +214,7 @@
assume "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
and "\<And>e T' u i. PROP ?Q r e T' u i T"
with uIT uT show "IT (Abs r[u/i])"
- by fastsimp
+ by fastforce
next
case (Beta r a as e_ T'_ u_ i_)
assume T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a \<degree>\<degree> as : T'"
--- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Mon Sep 12 07:55:43 2011 +0200
@@ -110,7 +110,7 @@
js \<noteq> {} \<Longrightarrow> (\<And>js'. js' \<in> iseq xs (Suc i) \<Longrightarrow> Max js' = i \<Longrightarrow> finite js' \<Longrightarrow>
js' \<noteq> {} \<Longrightarrow> card js' \<le> card js) \<Longrightarrow>
j = liseq' xs i"
- by (fastsimp simp add: liseq'_def iseq_finite
+ by (fastforce simp add: liseq'_def iseq_finite
intro: Max_eqI [symmetric])
lemma liseq_ge:
@@ -122,7 +122,7 @@
(\<And>js'. js' \<in> iseq xs i \<Longrightarrow> finite js' \<Longrightarrow>
js' \<noteq> {} \<Longrightarrow> card js' \<le> card js) \<Longrightarrow>
j = liseq xs i"
- by (fastsimp simp add: liseq_def iseq_finite
+ by (fastforce simp add: liseq_def iseq_finite
intro: Max_eqI [symmetric])
lemma max_notin: "finite xs \<Longrightarrow> Max xs < x \<Longrightarrow> x \<notin> xs"
--- a/src/HOL/SetInterval.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/SetInterval.thy Mon Sep 12 07:55:43 2011 +0200
@@ -657,7 +657,7 @@
case (insert b A)
moreover hence "b ~: A" by auto
moreover have "A <= {k..<k+card A}" and "b = k+card A"
- using `b ~: A` insert by fastsimp+
+ using `b ~: A` insert by fastforce+
ultimately show ?case by auto
qed
next
@@ -688,7 +688,7 @@
lemma UN_le_add_shift:
"(\<Union>i\<le>n::nat. M(i+k)) = (\<Union>i\<in>{k..n+k}. M i)" (is "?A = ?B")
proof
- show "?A <= ?B" by fastsimp
+ show "?A <= ?B" by fastforce
next
show "?B <= ?A"
proof
@@ -899,7 +899,7 @@
lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}"
apply (rule card_bij_eq [of Suc _ _ "\<lambda>x. x - Suc 0"])
apply simp
-apply fastsimp
+apply fastforce
apply auto
apply (rule inj_on_diff_nat)
apply auto
@@ -1020,7 +1020,7 @@
apply(rule ccontr)
apply(insert linorder_le_less_linear[of i n])
apply(clarsimp simp:linorder_not_le)
-apply(fastsimp)
+apply(fastforce)
done
--- a/src/HOL/Statespace/DistinctTreeProver.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Mon Sep 12 07:55:43 2011 +0200
@@ -141,7 +141,7 @@
case None
with l'_l Some x_l_Some del
show ?thesis
- by (fastsimp split: split_if_asm)
+ by (fastforce split: split_if_asm)
qed
next
case None
@@ -154,12 +154,12 @@
by simp
with Some x_l_None del
show ?thesis
- by (fastsimp split: split_if_asm)
+ by (fastforce split: split_if_asm)
next
case None
with x_l_None del
show ?thesis
- by (fastsimp split: split_if_asm)
+ by (fastforce split: split_if_asm)
qed
qed
qed
@@ -198,12 +198,12 @@
with dist_l' dist_r' l'_l Some x_l_Some del d dist_l_r
show ?thesis
- by fastsimp
+ by fastforce
next
case None
with l'_l dist_l' x_l_Some del d dist_l_r dist_r
show ?thesis
- by fastsimp
+ by fastforce
qed
next
case None
@@ -218,12 +218,12 @@
have "set_of r' \<subseteq> set_of r".
with Some dist_r' x_l_None del dist_l d dist_l_r
show ?thesis
- by fastsimp
+ by fastforce
next
case None
with x_l_None del dist_l dist_r d dist_l_r
show ?thesis
- by (fastsimp split: split_if_asm)
+ by (fastforce split: split_if_asm)
qed
qed
qed
--- a/src/HOL/TLA/TLA.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/TLA/TLA.thy Mon Sep 12 07:55:43 2011 +0200
@@ -251,7 +251,7 @@
assumes prem: "|- F --> G"
shows "|- <>F --> <>G"
apply (unfold dmd_def)
- apply (fastsimp intro!: prem [temp_use] elim!: STL4E [temp_use])
+ apply (fastforce intro!: prem [temp_use] elim!: STL4E [temp_use])
done
lemma DmdImplE: "[| sigma |= <>F; |- F --> G |] ==> sigma |= <>G"
@@ -262,7 +262,7 @@
apply auto
apply (subgoal_tac "sigma |= [] (G --> (F & G))")
apply (erule normalT [temp_use])
- apply (fastsimp elim!: STL4E [temp_use])+
+ apply (fastforce elim!: STL4E [temp_use])+
done
(* rewrite rule to split conjunctions under boxes *)
@@ -322,7 +322,7 @@
lemma DmdOr: "|- (<>(F | G)) = (<>F | <>G)"
apply (auto simp add: dmd_def split_box_conj [try_rewrite])
- apply (erule contrapos_np, merge_box, fastsimp elim!: STL4E [temp_use])+
+ apply (erule contrapos_np, merge_box, fastforce elim!: STL4E [temp_use])+
done
lemma exT: "|- (EX x. <>(F x)) = (<>(EX x. F x))"
@@ -343,7 +343,7 @@
apply auto
apply (erule notE)
apply merge_box
- apply (fastsimp elim!: STL4E [temp_use])
+ apply (fastforce elim!: STL4E [temp_use])
done
lemma InfImpl:
@@ -354,7 +354,7 @@
apply (insert 1 2)
apply (erule_tac F = G in dup_boxE)
apply merge_box
- apply (fastsimp elim!: STL4E [temp_use] DmdImpl2 [temp_use] intro!: 3 [temp_use])
+ apply (fastforce elim!: STL4E [temp_use] DmdImpl2 [temp_use] intro!: 3 [temp_use])
done
(* ------------------------ STL6 ------------------------------------------- *)
@@ -365,7 +365,7 @@
apply (erule dup_boxE)
apply merge_box
apply (erule contrapos_np)
- apply (fastsimp elim!: STL4E [temp_use])
+ apply (fastforce elim!: STL4E [temp_use])
done
(* weaker than BoxDmd, but more polymorphic (and often just right) *)
@@ -373,14 +373,14 @@
apply (unfold dmd_def)
apply clarsimp
apply merge_box
- apply (fastsimp elim!: notE STL4E [temp_use])
+ apply (fastforce elim!: notE STL4E [temp_use])
done
lemma BoxDmd2_simple: "|- []F & <>G --> <>(G & F)"
apply (unfold dmd_def)
apply clarsimp
apply merge_box
- apply (fastsimp elim!: notE STL4E [temp_use])
+ apply (fastforce elim!: notE STL4E [temp_use])
done
lemma DmdImpldup:
@@ -406,7 +406,7 @@
apply (drule BoxDmd [temp_use])
apply assumption
apply (erule thin_rl)
- apply (fastsimp elim!: DmdImplE [temp_use])
+ apply (fastforce elim!: DmdImplE [temp_use])
done
@@ -467,7 +467,7 @@
(* ------------------------ Miscellaneous ----------------------------------- *)
lemma BoxOr: "!!sigma. [| sigma |= []F | []G |] ==> sigma |= [](F | G)"
- by (fastsimp elim!: STL4E [temp_use])
+ by (fastforce elim!: STL4E [temp_use])
(* "persistently implies infinitely often" *)
lemma DBImplBD: "|- <>[]F --> []<>F"
@@ -487,7 +487,7 @@
apply assumption
apply (subgoal_tac "sigma |= <>[]~F")
apply (force simp: dmd_def)
- apply (fastsimp elim: DmdImplE [temp_use] STL4E [temp_use])
+ apply (fastforce elim: DmdImplE [temp_use] STL4E [temp_use])
done
@@ -498,7 +498,7 @@
(* ------------------------ TLA2 ------------------------------------------- *)
lemma STL2_pr: "|- []P --> Init P & Init P`"
- by (fastsimp intro!: STL2_gen [temp_use] primeI [temp_use])
+ by (fastforce intro!: STL2_gen [temp_use] primeI [temp_use])
(* Auxiliary lemma allows priming of boxed actions *)
lemma BoxPrime: "|- []P --> []($P & P$)"
@@ -523,7 +523,7 @@
lemma DmdPrime: "|- (<>P`) --> (<>P)"
apply (unfold dmd_def)
- apply (fastsimp elim!: TLA2E [temp_use])
+ apply (fastforce elim!: TLA2E [temp_use])
done
lemmas PrimeDmd = InitDmd_gen [temp_use, THEN DmdPrime [temp_use], standard]
@@ -557,7 +557,7 @@
lemma StableT:
"!!P. |- $P & A --> P` ==> |- []A --> stable P"
apply (unfold stable_def)
- apply (fastsimp elim!: STL4E [temp_use])
+ apply (fastforce elim!: STL4E [temp_use])
done
lemma Stable: "[| sigma |= []A; |- $P & A --> P` |] ==> sigma |= stable P"
@@ -617,7 +617,7 @@
apply (clarsimp dest!: BoxPrime [temp_use])
apply merge_box
apply (erule contrapos_np)
- apply (fastsimp elim!: Stable [temp_use])
+ apply (fastforce elim!: Stable [temp_use])
done
@@ -627,7 +627,7 @@
(* Recursive expansions of [] and <> for state predicates *)
lemma BoxRec: "|- ([]P) = (Init P & []P`)"
apply (auto intro!: STL2_gen [temp_use])
- apply (fastsimp elim!: TLA2E [temp_use])
+ apply (fastforce elim!: TLA2E [temp_use])
apply (auto simp: stable_def elim!: INV1 [temp_use] STL4E [temp_use])
done
@@ -645,12 +645,12 @@
apply (rule classical)
apply (rule DBImplBD [temp_use])
apply (subgoal_tac "sigma |= <>[]P")
- apply (fastsimp elim!: DmdImplE [temp_use] TLA2E [temp_use])
+ apply (fastforce elim!: DmdImplE [temp_use] TLA2E [temp_use])
apply (subgoal_tac "sigma |= <>[] (<>P & []~P`)")
apply (force simp: boxInit_stp [temp_use]
elim!: DmdImplE [temp_use] STL4E [temp_use] DmdRec2 [temp_use])
apply (force intro!: STL6 [temp_use] simp: more_temp_simps3)
- apply (fastsimp intro: DmdPrime [temp_use] elim!: STL4E [temp_use])
+ apply (fastforce intro: DmdPrime [temp_use] elim!: STL4E [temp_use])
done
lemma InfiniteEnsures:
@@ -666,12 +666,12 @@
(* alternative definitions of fairness *)
lemma WF_alt: "|- WF(A)_v = ([]<>~Enabled(<A>_v) | []<><A>_v)"
apply (unfold WF_def dmd_def)
- apply fastsimp
+ apply fastforce
done
lemma SF_alt: "|- SF(A)_v = (<>[]~Enabled(<A>_v) | []<><A>_v)"
apply (unfold SF_def dmd_def)
- apply fastsimp
+ apply fastforce
done
(* theorems to "box" fairness conditions *)
@@ -679,19 +679,19 @@
by (auto simp: WF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use])
lemma WF_Box: "|- ([]WF(A)_v) = WF(A)_v"
- by (fastsimp intro!: BoxWFI [temp_use] dest!: STL2 [temp_use])
+ by (fastforce intro!: BoxWFI [temp_use] dest!: STL2 [temp_use])
lemma BoxSFI: "|- SF(A)_v --> []SF(A)_v"
by (auto simp: SF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use])
lemma SF_Box: "|- ([]SF(A)_v) = SF(A)_v"
- by (fastsimp intro!: BoxSFI [temp_use] dest!: STL2 [temp_use])
+ by (fastforce intro!: BoxSFI [temp_use] dest!: STL2 [temp_use])
lemmas more_temp_simps = more_temp_simps3 WF_Box [temp_rewrite] SF_Box [temp_rewrite]
lemma SFImplWF: "|- SF(A)_v --> WF(A)_v"
apply (unfold SF_def WF_def)
- apply (fastsimp dest!: DBImplBD [temp_use])
+ apply (fastforce dest!: DBImplBD [temp_use])
done
(* A tactic that "boxes" all fairness conditions. Apply more_temp_simps to "unbox". *)
@@ -716,13 +716,13 @@
apply (unfold leadsto_def)
apply auto
apply (simp add: more_temp_simps)
- apply (fastsimp elim!: DmdImplE [temp_use] STL4E [temp_use])
- apply (fastsimp intro!: InitDmd [temp_use] elim!: STL4E [temp_use])
+ apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use])
+ apply (fastforce intro!: InitDmd [temp_use] elim!: STL4E [temp_use])
apply (subgoal_tac "sigma |= []<><>G")
apply (simp add: more_temp_simps)
apply (drule BoxDmdDmdBox [temp_use])
apply assumption
- apply (fastsimp elim!: DmdImplE [temp_use] STL4E [temp_use])
+ apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use])
done
lemma leadsto_infinite: "|- []<>F & (F ~> G) --> []<>G"
@@ -880,7 +880,7 @@
apply clarsimp
apply (subgoal_tac "sigma |= (B | C) ~> D")
apply (erule_tac G = "LIFT (B | C)" in LatticeTransitivity [temp_use])
- apply (fastsimp intro!: LatticeDisjunctionIntro [temp_use])+
+ apply (fastforce intro!: LatticeDisjunctionIntro [temp_use])+
done
lemma LatticeTriangle: "|- (A ~> D | B) & (B ~> D) --> (A ~> D)"
--- a/src/HOL/TPTP/CASC_Setup.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/TPTP/CASC_Setup.thy Mon Sep 12 07:55:43 2011 +0200
@@ -141,7 +141,7 @@
ORELSE
SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac ctxt))
ORELSE
- SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac ctxt))
+ SOLVE_TIMEOUT max_secs "fastforce" (ALLGOALS (fast_force_tac ctxt))
*}
method_setup isabellep = {*
--- a/src/HOL/Taylor.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Taylor.thy Mon Sep 12 07:55:43 2011 +0200
@@ -50,8 +50,8 @@
let ?H = "x + c"
from X have "c<?H & ?H<b \<and> f b = (\<Sum>m = 0..<n. diff m c / real (fact m) * (b - c) ^ m) +
diff n ?H / real (fact n) * (b - c) ^ n"
- by fastsimp
- thus ?thesis by fastsimp
+ by fastforce
+ thus ?thesis by fastforce
qed
qed
@@ -90,8 +90,8 @@
let ?H = "x + c"
from X have "a<?H & ?H<c \<and> f a = (\<Sum>m = 0..<n. diff m c / real (fact m) * (a - c) ^ m) +
diff n ?H / real (fact n) * (a - c) ^ n"
- by fastsimp
- thus ?thesis by fastsimp
+ by fastforce
+ thus ?thesis by fastforce
qed
qed
@@ -107,7 +107,7 @@
note INIT
moreover from DERIV and INTERV
have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
- by fastsimp
+ by fastforce
moreover note True
moreover from INTERV have "c \<le> b" by simp
ultimately have EX: "\<exists>t>x. t < c \<and> f x =
@@ -120,7 +120,7 @@
note INIT
moreover from DERIV and INTERV
have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
- by fastsimp
+ by fastforce
moreover from INTERV have "a \<le> c" by arith
moreover from False and INTERV have "c < x" by arith
ultimately have EX: "\<exists>t>c. t < x \<and> f x =
--- a/src/HOL/Tools/SMT/smt_normalize.ML Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Mon Sep 12 07:55:43 2011 +0200
@@ -475,7 +475,7 @@
"op * = (%a b. nat (int a * int b))"
"op div = (%a b. nat (int a div int b))"
"op mod = (%a b. nat (int a mod int b))"
- by (fastsimp simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+}
+ by (fastforce simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+}
val ints = map mk_meta_eq @{lemma
"int 0 = 0"
--- a/src/HOL/Tools/SMT/z3_proof_literals.ML Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_literals.ML Mon Sep 12 07:55:43 2011 +0200
@@ -276,7 +276,7 @@
local
val cp1 = @{lemma "(~P) = (~Q) ==> P = Q" by simp}
- val cp2 = @{lemma "(~P) = Q ==> P = (~Q)" by fastsimp}
+ val cp2 = @{lemma "(~P) = Q ==> P = (~Q)" by fastforce}
val cp3 = @{lemma "P = (~Q) ==> (~P) = Q" by simp}
in
fun contrapos1 prove (ct, cu) = prove (negate ct, negate cu) COMP cp1
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Sep 12 07:55:43 2011 +0200
@@ -385,7 +385,7 @@
val apply_rules = [
@{lemma "(~n | P) & (n | ~P) ==> P == n" by (atomize(full)) fast},
@{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n"
- by (atomize(full)) fastsimp} ]
+ by (atomize(full)) fastforce} ]
val inst_rule = Z3_Proof_Tools.match_instantiate Thm.dest_arg
--- a/src/HOL/Tools/TFL/post.ML Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Tools/TFL/post.ML Mon Sep 12 07:55:43 2011 +0200
@@ -40,7 +40,7 @@
terminator =
asm_simp_tac (simpset_of ctxt) 1
THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE
- fast_simp_tac (ctxt addSDs [@{thm not0_implies_Suc}]) 1),
+ fast_force_tac (ctxt addSDs [@{thm not0_implies_Suc}]) 1),
simplifier = Rules.simpl_conv (simpset_of ctxt) []};
--- a/src/HOL/Tools/try_methods.ML Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Tools/try_methods.ML Mon Sep 12 07:55:43 2011 +0200
@@ -101,7 +101,7 @@
[("simp", ((false, true), simp_attrs)),
("auto", ((true, true), full_attrs)),
("fast", ((false, false), clas_attrs)),
- ("fastsimp", ((false, false), full_attrs)),
+ ("fastforce", ((false, false), full_attrs)),
("force", ((false, false), full_attrs)),
("blast", ((false, true), clas_attrs)),
("metis", ((false, true), metis_attrs)),
--- a/src/HOL/Transitive_Closure.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Transitive_Closure.thy Mon Sep 12 07:55:43 2011 +0200
@@ -487,7 +487,7 @@
lemmas trancl_converseD = tranclp_converseD [to_set]
lemma tranclp_converse: "(r^--1)^++ = (r^++)^--1"
- by (fastsimp simp add: fun_eq_iff
+ by (fastforce simp add: fun_eq_iff
intro!: tranclp_converseI dest!: tranclp_converseD)
lemmas trancl_converse = tranclp_converse [to_set]
@@ -730,7 +730,7 @@
lemma rel_pow_Suc_I2:
"(x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> (x, z) \<in> R ^^ Suc n"
- by (induct n arbitrary: z) (simp, fastsimp)
+ by (induct n arbitrary: z) (simp, fastforce)
lemma rel_pow_0_E:
"(x, y) \<in> R ^^ 0 \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P"
@@ -821,7 +821,7 @@
apply (clarsimp simp: rtrancl_is_UN_rel_pow)
apply (rule_tac x="Suc n" in exI)
apply (clarsimp simp: rel_comp_def)
- apply fastsimp
+ apply fastforce
apply clarsimp
apply (case_tac n, simp)
apply clarsimp
@@ -942,7 +942,7 @@
lemma rtrancl_finite_eq_rel_pow:
"finite R \<Longrightarrow> R^* = (UN n : {n. n <= card R}. R^^n)"
-by(fastsimp simp: rtrancl_power dest: rel_pow_finite_bounded)
+by(fastforce simp: rtrancl_power dest: rel_pow_finite_bounded)
lemma trancl_finite_eq_rel_pow:
"finite R \<Longrightarrow> R^+ = (UN n : {n. 0 < n & n <= card R}. R^^n)"
--- a/src/HOL/UNITY/Transformers.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/UNITY/Transformers.thy Mon Sep 12 07:55:43 2011 +0200
@@ -440,7 +440,7 @@
apply (rule subsetI)
apply (erule wens_set.induct)
txt{*Basis*}
- apply (fastsimp simp add: wens_single_finite_def)
+ apply (fastforce simp add: wens_single_finite_def)
txt{*Wens inductive step*}
apply (case_tac "acta = Id", simp)
apply (simp add: wens_single_eq)
--- a/src/HOL/Unix/Unix.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Unix/Unix.thy Mon Sep 12 07:55:43 2011 +0200
@@ -450,7 +450,7 @@
with root' show ?thesis by cases auto
next
case readdir
- with root' show ?thesis by cases fastsimp+
+ with root' show ?thesis by cases fastforce+
qed
text {*
@@ -1028,7 +1028,7 @@
also have "\<dots> \<noteq> None"
proof -
from ys obtain us u where rev_ys: "ys = us @ [u]"
- by (cases ys rule: rev_cases) fastsimp+
+ by (cases ys rule: rev_cases) fastforce+
with tr path
have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or>
lookup root ((path @ [y]) @ us) \<noteq> None"
--- a/src/HOL/Word/Bit_Representation.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Word/Bit_Representation.thy Mon Sep 12 07:55:43 2011 +0200
@@ -856,7 +856,7 @@
shows "0 < length y \<Longrightarrow> P"
apply (cases y, simp)
apply (rule y)
- apply fastsimp
+ apply fastforce
done
lemma list_exhaust_size_eq0:
--- a/src/HOL/Word/Word.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Word/Word.thy Mon Sep 12 07:55:43 2011 +0200
@@ -655,7 +655,7 @@
lemma to_bl_use_of_bl:
"(to_bl w = bl) = (w = of_bl bl \<and> length bl = length (to_bl w))"
- by (fastsimp elim!: word_bl.Abs_inverse [simplified])
+ by (fastforce elim!: word_bl.Abs_inverse [simplified])
lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)"
unfolding word_reverse_def by (simp add: word_bl.Abs_inverse)
@@ -3702,7 +3702,7 @@
apply (case_tac "word_split c")
apply (frule test_bit_split)
apply (erule trans)
- apply (fastsimp intro ! : word_eqI simp add : word_size)
+ apply (fastforce intro ! : word_eqI simp add : word_size)
done
-- {* this odd result is analogous to @{text "ucast_id"},
--- a/src/HOL/ex/Set_Algebras.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/ex/Set_Algebras.thy Mon Sep 12 07:55:43 2011 +0200
@@ -321,7 +321,7 @@
lemma set_plus_image:
fixes S T :: "'n::semigroup_add set" shows "S \<oplus> T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
- unfolding set_plus_def by (fastsimp simp: image_iff)
+ unfolding set_plus_def by (fastforce simp: image_iff)
lemma set_setsum_alt:
assumes fin: "finite I"
--- a/src/HOL/ex/While_Combinator_Example.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/ex/While_Combinator_Example.thy Mon Sep 12 07:55:43 2011 +0200
@@ -25,7 +25,7 @@
apply assumption
apply clarsimp
apply (blast dest: monoD)
- apply (fastsimp intro!: lfp_lowerbound)
+ apply (fastforce intro!: lfp_lowerbound)
apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
apply (clarsimp simp add: finite_psubset_def order_less_le)
apply (blast dest: monoD)
--- a/src/Provers/clasimp.ML Sun Sep 11 22:56:05 2011 +0200
+++ b/src/Provers/clasimp.ML Mon Sep 12 07:55:43 2011 +0200
@@ -23,7 +23,7 @@
val mk_auto_tac: Proof.context -> int -> int -> tactic
val auto_tac: Proof.context -> tactic
val force_tac: Proof.context -> int -> tactic
- val fast_simp_tac: Proof.context -> int -> tactic
+ val fast_force_tac: Proof.context -> int -> tactic
val slow_simp_tac: Proof.context -> int -> tactic
val best_simp_tac: Proof.context -> int -> tactic
val iff_add: attribute
@@ -169,12 +169,14 @@
(* basic combinations *)
-val fast_simp_tac = Classical.fast_tac o addss;
+fun fast_simp_tac ctxt i =
+ let val _ = legacy_feature "Old name 'fastsimp' - use 'fastforce' instead"
+ in Classical.fast_tac (addss ctxt) i end;
+
+val fast_force_tac = Classical.fast_tac o addss;
val slow_simp_tac = Classical.slow_tac o addss;
val best_simp_tac = Classical.best_tac o addss;
-
-
(** concrete syntax **)
(* attributes *)
@@ -215,7 +217,8 @@
val clasimp_setup =
Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
- Method.setup @{binding fastsimp} (clasimp_method' fast_simp_tac) "combined fast and simp" #>
+ Method.setup @{binding fastsimp} (clasimp_method' fast_simp_tac) "combined fast and simp (legacy name)" #>
+ Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #>
Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>
Method.setup @{binding force} (clasimp_method' force_tac) "force" #>