--- a/doc-src/TutorialI/CTL/CTL.thy Mon Aug 02 16:06:13 2004 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy Tue Aug 03 13:48:00 2004 +0200
@@ -117,34 +117,19 @@
@{thm lfp_lowerbound[of _ "S",no_vars]} \hfill (@{thm[source]lfp_lowerbound})
\end{center}
The instance of the premise @{prop"f S \<subseteq> S"} is proved pointwise,
-a decision that clarification takes for us:
+a decision that \isa{auto} takes for us:
*};
apply(rule lfp_lowerbound);
-apply(clarsimp simp add: af_def Paths_def);
+apply(auto simp add: af_def Paths_def);
txt{*
@{subgoals[display,indent=0,margin=70,goals_limit=1]}
-Now we eliminate the disjunction. The case @{prop"p(0::nat) \<in> A"} is trivial:
-*};
-
-apply(erule disjE);
- apply(blast);
-
-txt{*\noindent
-In the other case we set @{term t} to @{term"p(1::nat)"} and simplify matters:
+In this remaining case, we set @{term t} to @{term"p(1::nat)"}.
+The rest is automatic.
*};
apply(erule_tac x = "p 1" in allE);
-apply(clarsimp);
-
-txt{*
-@{subgoals[display,indent=0,margin=70,goals_limit=1]}
-It merely remains to set @{term pa} to @{term"\<lambda>i. p(i+1::nat)"}, that is,
-@{term p} without its first element. The rest is automatic:
-*};
-
-apply(erule_tac x = "\<lambda>i. p(i+1)" in allE);
-apply force;
+apply(auto);
done;
@@ -389,11 +374,9 @@
lemma "lfp(eufix A B) \<subseteq> eusem A B"
apply(rule lfp_lowerbound)
-apply(clarsimp simp add: eusem_def eufix_def);
-apply(erule disjE);
+apply(auto simp add: eusem_def eufix_def);
apply(rule_tac x = "[]" in exI);
apply simp
-apply(clarsimp);
apply(rule_tac x = "y#xc" in exI);
apply simp;
done
--- a/doc-src/TutorialI/CTL/document/CTL.tex Mon Aug 02 16:06:13 2004 +0200
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Tue Aug 03 13:48:00 2004 +0200
@@ -110,52 +110,28 @@
\isa{f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound})
\end{center}
The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise,
-a decision that clarification takes for us:%
+a decision that \isa{auto} takes for us:%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}{\isacharparenleft}rule\ lfp{\isacharunderscore}lowerbound{\isacharparenright}\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptxt}%
\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ {\isadigit{0}}\ {\isasymin}\ A\ {\isasymor}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}}{\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}{\isasymforall}t{\isachardot}\ }{\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}{\isasymforall}p{\isachardot}\ }{\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}t{\isachardot}\ }{\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}t{\isachardot}\ {\isacharparenleft}{\isasymforall}p{\isachardot}\ }{\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ }{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
\end{isabelle}
-Now we eliminate the disjunction. The case \isa{p\ {\isadigit{0}}\ {\isasymin}\ A} is trivial:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}erule\ disjE{\isacharparenright}\isanewline
-\ \isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isamarkupfalse%
-%
-\begin{isamarkuptxt}%
-\noindent
-In the other case we set \isa{t} to \isa{p\ {\isadigit{1}}} and simplify matters:%
+In this remaining case, we set \isa{t} to \isa{p\ {\isadigit{1}}}.
+The rest is automatic.%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ {\isadigit{1}}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isamarkupfalse%
-%
-\begin{isamarkuptxt}%
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ }{\isasymforall}pa{\isachardot}\ p\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ pa\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ {\isasymforall}pa{\isachardot}\ }{\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
-\end{isabelle}
-It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}}, that is,
-\isa{p} without its first element. The rest is automatic:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
-\isamarkupfalse%
-\isacommand{apply}\ force\isanewline
+\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
\isamarkupfalse%
\isacommand{done}\isamarkupfalse%
%
@@ -463,8 +439,6 @@
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
-\isamarkupfalse%
-\isamarkupfalse%
%
\begin{isamarkuptext}%
Let us close this section with a few words about the executability of
--- a/src/HOL/Bali/TypeSafe.thy Mon Aug 02 16:06:13 2004 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Tue Aug 03 13:48:00 2004 +0200
@@ -1477,7 +1477,7 @@
qed
next
show "?Hd x y \<union> ?Tl xs ys \<subseteq> ?List x xs y ys"
- proof
+ proof (rule subsetI)
fix el
assume el_in_hd_tl: "el \<in> ?Hd x y \<union> ?Tl xs ys"
show "el \<in> ?List x xs y ys"
@@ -2978,7 +2978,7 @@
by simp
from da_e1 s0_s1 True obtain E1' where
"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'"
- by - (rule da_weakenE,auto)
+ by - (rule da_weakenE, auto iff del: Un_subset_iff)
with conf_s1 wt_e1
obtain
"s2\<Colon>\<preceq>(G, L)"
@@ -2997,7 +2997,7 @@
by simp
from da_e2 s0_s1 False obtain E2' where
"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'"
- by - (rule da_weakenE,auto)
+ by - (rule da_weakenE, auto iff del: Un_subset_iff)
with conf_s1 wt_e2
obtain
"s2\<Colon>\<preceq>(G, L)"
--- a/src/HOL/HoareParallel/OG_Hoare.thy Mon Aug 02 16:06:13 2004 +0200
+++ b/src/HOL/HoareParallel/OG_Hoare.thy Tue Aug 03 13:48:00 2004 +0200
@@ -117,19 +117,13 @@
apply (induct "k")
apply(simp (no_asm) add: L3_5v_lemma3)
apply(simp (no_asm) add: L3_5iv L3_5ii Parallel_empty)
-apply(rule Un_least)
- apply(rule subset_trans)
- prefer 2 apply simp
- apply(erule L3_5i)
+apply(rule conjI)
+ apply (blast dest: L3_5i)
apply(simp add: SEM_def sem_def id_def)
-apply clarify
-apply(drule rtrancl_imp_UN_rel_pow)
-apply clarify
-apply(drule Basic_ntran)
- apply fast+
+apply (blast dest: Basic_ntran rtrancl_imp_UN_rel_pow)
done
-lemma atom_hoare_sound [rule_format (no_asm)]:
+lemma atom_hoare_sound [rule_format]:
" \<parallel>- p c q \<longrightarrow> atom_com(c) \<longrightarrow> \<parallel>= p c q"
apply (unfold com_validity_def)
apply(rule oghoare_induct)
@@ -143,19 +137,11 @@
prefer 2 apply simp
apply(simp add: L3_5ii L3_5i)
--{* Cond *}
- apply(rule impI)
apply(simp add: L3_5iv)
- apply(erule Un_least)
- apply assumption
--{* While *}
- apply(rule impI)
- apply(simp add: L3_5v)
- apply(rule UN_least)
- apply(drule SEM_fwhile)
- apply assumption
+ apply (force simp add: L3_5v dest: SEM_fwhile)
--{* Conseq *}
-apply(simp add: SEM_def sem_def)
-apply force
+apply(force simp add: SEM_def sem_def)
done
subsection {* Soundness of the System for Component Programs *}
@@ -450,7 +436,7 @@
apply simp+
done
-lemma oghoare_sound [rule_format (no_asm)]: "\<parallel>- p c q \<longrightarrow> \<parallel>= p c q"
+lemma oghoare_sound [rule_format]: "\<parallel>- p c q \<longrightarrow> \<parallel>= p c q"
apply (unfold com_validity_def)
apply(rule oghoare_induct)
apply(rule TrueI)+
@@ -477,16 +463,11 @@
apply(simp add: L3_5ii L3_5i)
--{* Cond *}
apply(simp add: L3_5iv)
- apply(erule Un_least)
- apply assumption
--{* While *}
apply(simp add: L3_5v)
- apply(rule UN_least)
- apply(drule SEM_fwhile)
- apply assumption
+ apply (blast dest: SEM_fwhile)
--{* Conseq *}
-apply(simp add: SEM_def sem_def)
-apply auto
+apply(auto simp add: SEM_def sem_def)
done
end
\ No newline at end of file
--- a/src/HOL/HoareParallel/RG_Examples.thy Mon Aug 02 16:06:13 2004 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy Tue Aug 03 13:48:00 2004 +0200
@@ -26,16 +26,7 @@
COEND
SAT [\<lbrace> n < length \<acute>A \<rbrace>, \<lbrace> \<ordmasculine>A = \<ordfeminine>A \<rbrace>, \<lbrace> True \<rbrace>, \<lbrace> \<forall>i < n. \<acute>A ! i = 0 \<rbrace>]"
apply(rule Parallel)
- apply simp
- apply clarify
- apply simp
- apply(erule disjE)
- apply simp
- apply clarify
- apply simp
- apply auto
-apply(rule Basic)
-apply auto
+apply (auto intro!: Basic)
done
lemma Example1_parameterized:
@@ -53,33 +44,14 @@
(\<forall>i<length \<ordmasculine>A . (i<k*n \<longrightarrow> \<ordmasculine>A!i = \<ordfeminine>A!i) \<and> ((Suc k)*n \<le> i\<longrightarrow> \<ordmasculine>A!i = \<ordfeminine>A!i))\<rbrace>,
\<lbrace>\<forall>i<n. \<acute>A!(k*n+i) = 0\<rbrace>]"
apply(rule Parallel)
- apply simp
- apply clarify
- apply simp
- apply(erule disjE)
- apply clarify
- apply simp
- apply clarify
- apply simp
- apply clarify
- apply simp
- apply(erule_tac x="k*n +i" in allE)
- apply(subgoal_tac "k*n+i <length (A b)")
- apply force
- apply(erule le_less_trans2)
- apply(case_tac t,simp+)
- apply (simp add:add_commute)
- apply(rule add_le_mono)
- apply simp
- apply simp
- apply simp
- apply clarify
- apply(rotate_tac -1)
+ apply auto
+ apply(erule_tac x="k*n +i" in allE)
+ apply(subgoal_tac "k*n+i <length (A b)")
apply force
- apply force
- apply force
-apply simp
-apply clarify
+ apply(erule le_less_trans2)
+ apply(case_tac t,simp+)
+ apply (simp add:add_commute)
+ apply(simp add: add_le_mono)
apply(rule Basic)
apply simp
apply clarify
@@ -88,12 +60,10 @@
apply(erule le_less_trans2)
apply(case_tac t,simp+)
apply (simp add:add_commute)
- apply(rule add_le_mono)
- apply simp
- apply simp
- apply force+
+ apply(rule add_le_mono, auto)
done
+
subsection {* Increment a Variable in Parallel *}
subsubsection {* Two components *}
@@ -134,7 +104,7 @@
apply clarify
apply(case_tac i)
apply simp
- apply(erule disjE)
+ apply(rule conjI)
apply clarify
apply simp
apply clarify
@@ -142,7 +112,7 @@
apply(case_tac j,simp)
apply simp
apply simp
- apply(erule disjE)
+ apply(rule conjI)
apply clarify
apply simp
apply clarify
@@ -179,10 +149,7 @@
apply(rule Basic)
apply simp_all
apply(rule subset_refl)
-apply(rule Basic)
-apply simp_all
-apply clarify
-apply simp
+apply(auto intro!: Basic)
done
subsubsection {* Parameterized *}
--- a/src/HOL/HoareParallel/RG_Hoare.thy Mon Aug 02 16:06:13 2004 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy Tue Aug 03 13:48:00 2004 +0200
@@ -4,6 +4,8 @@
subsection {* Proof System for Component Programs *}
+declare Un_subset_iff [iff del]
+
constdefs
stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"
"stable \<equiv> \<lambda>f g. (\<forall>x y. x \<in> f \<longrightarrow> (x, y) \<in> g \<longrightarrow> y \<in> f)"
@@ -1179,12 +1181,9 @@
\<Longrightarrow> \<forall>j i. i<length clist \<and> Suc j<length x \<longrightarrow> (clist!i!j) -c\<rightarrow> (clist!i!Suc j)
\<longrightarrow> (snd(clist!i!j), snd(clist!i!Suc j)) \<in> Guar(xs!i)"
apply(unfold par_cp_def)
+apply (rule ccontr)
--{* By contradiction: *}
-apply(subgoal_tac "True")
- prefer 2
- apply simp
-apply(erule_tac Q="True" in contrapos_pp)
-apply simp
+apply (simp del: Un_subset_iff)
apply(erule exE)
--{* the first c-tran that does not satisfy the guarantee-condition is from @{text "\<sigma>_i"} at step @{text "m"}. *}
apply(drule_tac n=j and P="\<lambda>j. \<exists>i. ?H i j" in Ex_first_occurrence)
@@ -1199,13 +1198,12 @@
apply(simp add:cp_def comm_def)
apply(drule_tac c="take (Suc (Suc m)) (clist ! i)" in subsetD)
apply simp
- apply(erule_tac x=i in allE, erule impE, assumption,erule conjE)
- apply(erule takecptn_is_cptn)
+ apply (blast intro: takecptn_is_cptn)
apply simp
apply clarify
apply(erule_tac x=m and P="\<lambda>j. ?I j \<and> ?J j \<longrightarrow> ?H j" in allE)
apply (simp add:conjoin_def same_length_def)
-apply(simp add:assum_def)
+apply(simp add:assum_def del: Un_subset_iff)
apply(rule conjI)
apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<in>cp (?K j) (?J j)" in allE)
apply(simp add:cp_def par_assum_def)
@@ -1213,7 +1211,7 @@
apply simp
apply clarify
apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> ?M \<union> UNION (?S j) (?T j) \<subseteq> (?L j)" in allE)
-apply simp
+apply(simp del: Un_subset_iff)
apply(erule subsetD)
apply simp
apply(simp add:conjoin_def compat_label_def)
@@ -1242,6 +1240,7 @@
apply (force simp add:par_assum_def same_state_def)
done
+
lemma three [rule_format]:
"\<lbrakk> xs\<noteq>[]; \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j))
\<subseteq> Rely (xs ! i);
@@ -1282,14 +1281,14 @@
x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely); Suc i < length x;
x ! i -pc\<rightarrow> x ! Suc i\<rbrakk>
\<Longrightarrow> (snd (x ! i), snd (x ! Suc i)) \<in> guar"
-apply(simp add: ParallelCom_def)
+apply(simp add: ParallelCom_def del: Un_subset_iff)
apply(subgoal_tac "(map (Some \<circ> fst) xs)\<noteq>[]")
prefer 2
apply simp
apply(frule rev_subsetD)
apply(erule one [THEN equalityD1])
apply(erule subsetD)
-apply simp
+apply (simp del: Un_subset_iff)
apply clarify
apply(drule_tac pre=pre and rely=rely and x=x and s=s and xs=xs and clist=clist in two)
apply(assumption+)
@@ -1332,14 +1331,14 @@
\<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely);
All_None (fst (last x)) \<rbrakk> \<Longrightarrow> snd (last x) \<in> post"
-apply(simp add: ParallelCom_def)
+apply(simp add: ParallelCom_def del: Un_subset_iff)
apply(subgoal_tac "(map (Some \<circ> fst) xs)\<noteq>[]")
prefer 2
apply simp
apply(frule rev_subsetD)
apply(erule one [THEN equalityD1])
apply(erule subsetD)
-apply simp
+apply(simp del: Un_subset_iff)
apply clarify
apply(subgoal_tac "\<forall>i<length clist. clist!i\<in>assum(Pre(xs!i), Rely(xs!i))")
apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> \<Turnstile> (?J i) sat [?I i,?K i,?M i,?N i]" in allE,erule impE,assumption)
--- a/src/HOL/Hyperreal/SEQ.thy Mon Aug 02 16:06:13 2004 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Tue Aug 03 13:48:00 2004 +0200
@@ -1048,7 +1048,7 @@
apply (simp add: inverse_eq_divide pos_divide_less_eq)
done
-subsubsection{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
+text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) ----> 0"
by (blast intro!: LIMSEQ_realpow_zero abs_ge_zero)
--- a/src/HOL/Set.thy Mon Aug 02 16:06:13 2004 +0200
+++ b/src/HOL/Set.thy Tue Aug 03 13:48:00 2004 +0200
@@ -1275,7 +1275,7 @@
lemma Int_UNIV [simp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
by blast
-lemma Int_subset_iff: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
+lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
by blast
lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
@@ -1352,7 +1352,8 @@
lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
by blast
-lemma Un_subset_iff: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
+
+lemma Un_subset_iff [simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
by blast
lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
@@ -1473,7 +1474,7 @@
by blast
lemma UN_absorb: "k \<in> I ==> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
- by blast
+ by auto
lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
by blast
--- a/src/HOL/UNITY/Follows.thy Mon Aug 02 16:06:13 2004 +0200
+++ b/src/HOL/UNITY/Follows.thy Tue Aug 03 13:48:00 2004 +0200
@@ -36,14 +36,12 @@
done
lemma Follows_constant [iff]: "F \<in> (%s. c) Fols (%s. c)"
-by (unfold Follows_def, auto)
+by (simp add: Follows_def)
lemma mono_Follows_o: "mono h ==> f Fols g \<subseteq> (h o f) Fols (h o g)"
-apply (unfold Follows_def, clarify)
-apply (simp add: mono_Increasing_o [THEN [2] rev_subsetD]
- mono_Always_o [THEN [2] rev_subsetD]
- mono_LeadsTo_o [THEN [2] rev_subsetD, THEN INT_D])
-done
+by (auto simp add: Follows_def mono_Increasing_o [THEN [2] rev_subsetD]
+ mono_Always_o [THEN [2] rev_subsetD]
+ mono_LeadsTo_o [THEN [2] rev_subsetD, THEN INT_D])
lemma mono_Follows_apply:
"mono h ==> f Fols g \<subseteq> (%x. h (f x)) Fols (%x. h (g x))"
@@ -53,7 +51,7 @@
lemma Follows_trans:
"[| F \<in> f Fols g; F \<in> g Fols h |] ==> F \<in> f Fols h"
-apply (unfold Follows_def)
+apply (simp add: Follows_def)
apply (simp add: Always_eq_includes_reachable)
apply (blast intro: order_trans LeadsTo_Trans)
done
@@ -62,17 +60,17 @@
subsection{*Destruction rules*}
lemma Follows_Increasing1: "F \<in> f Fols g ==> F \<in> Increasing f"
-by (unfold Follows_def, blast)
+by (simp add: Follows_def)
lemma Follows_Increasing2: "F \<in> f Fols g ==> F \<in> Increasing g"
-by (unfold Follows_def, blast)
+by (simp add: Follows_def)
lemma Follows_Bounded: "F \<in> f Fols g ==> F \<in> Always {s. f s \<subseteq> g s}"
-by (unfold Follows_def, blast)
+by (simp add: Follows_def)
lemma Follows_LeadsTo:
"F \<in> f Fols g ==> F \<in> {s. k \<le> g s} LeadsTo {s. k \<le> f s}"
-by (unfold Follows_def, blast)
+by (simp add: Follows_def)
lemma Follows_LeadsTo_pfixLe:
"F \<in> f Fols g ==> F \<in> {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}"
@@ -96,7 +94,7 @@
lemma Always_Follows1:
"[| F \<in> Always {s. f s = f' s}; F \<in> f Fols g |] ==> F \<in> f' Fols g"
-apply (unfold Follows_def Increasing_def Stable_def, auto)
+apply (simp add: Follows_def Increasing_def Stable_def, auto)
apply (erule_tac [3] Always_LeadsTo_weaken)
apply (erule_tac A = "{s. z \<le> f s}" and A' = "{s. z \<le> f s}"
in Always_Constrains_weaken, auto)
@@ -106,7 +104,7 @@
lemma Always_Follows2:
"[| F \<in> Always {s. g s = g' s}; F \<in> f Fols g |] ==> F \<in> f Fols g'"
-apply (unfold Follows_def Increasing_def Stable_def, auto)
+apply (simp add: Follows_def Increasing_def Stable_def, auto)
apply (erule_tac [3] Always_LeadsTo_weaken)
apply (erule_tac A = "{s. z \<le> g s}" and A' = "{s. z \<le> g s}"
in Always_Constrains_weaken, auto)
@@ -121,7 +119,7 @@
lemma increasing_Un:
"[| F \<in> increasing f; F \<in> increasing g |]
==> F \<in> increasing (%s. (f s) \<union> (g s))"
-apply (unfold increasing_def stable_def constrains_def, auto)
+apply (simp add: increasing_def stable_def constrains_def, auto)
apply (drule_tac x = "f xa" in spec)
apply (drule_tac x = "g xa" in spec)
apply (blast dest!: bspec)
@@ -162,8 +160,7 @@
lemma Follows_Un:
"[| F \<in> f' Fols f; F \<in> g' Fols g |]
==> F \<in> (%s. (f' s) \<union> (g' s)) Fols (%s. (f s) \<union> (g s))"
-apply (unfold Follows_def)
-apply (simp add: Increasing_Un Always_Un, auto)
+apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff, auto)
apply (rule LeadsTo_Trans)
apply (blast intro: Follows_Un_lemma)
(*Weakening is used to exchange Un's arguments*)
@@ -176,7 +173,7 @@
lemma increasing_union:
"[| F \<in> increasing f; F \<in> increasing g |]
==> F \<in> increasing (%s. (f s) + (g s :: ('a::order) multiset))"
-apply (unfold increasing_def stable_def constrains_def, auto)
+apply (simp add: increasing_def stable_def constrains_def, auto)
apply (drule_tac x = "f xa" in spec)
apply (drule_tac x = "g xa" in spec)
apply (drule bspec, assumption)
@@ -223,7 +220,7 @@
"!!g g' ::'b => ('a::order) multiset.
[| F \<in> f' Fols f; F \<in> g' Fols g |]
==> F \<in> (%s. (f' s) + (g' s)) Fols (%s. (f s) + (g s))"
-apply (unfold Follows_def)
+apply (simp add: Follows_def)
apply (simp add: Increasing_union Always_union, auto)
apply (rule LeadsTo_Trans)
apply (blast intro: Follows_union_lemma)
--- a/src/HOL/UNITY/ProgressSets.thy Mon Aug 02 16:06:13 2004 +0200
+++ b/src/HOL/UNITY/ProgressSets.thy Tue Aug 03 13:48:00 2004 +0200
@@ -486,11 +486,11 @@
shows "closed F T B L"
apply (simp add: closed_def, clarify)
apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice])
-apply (simp add: Int_Un_distrib cl_Un [OF lattice] Un_subset_iff
+apply (simp add: Int_Un_distrib cl_Un [OF lattice] Un_subset_iff
cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1)
apply (subgoal_tac "cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))")
prefer 2
- apply (simp add: commutes [unfolded commutes_def])
+ apply (cut_tac commutes, simp add: commutes_def)
apply (erule subset_trans)
apply (simp add: cl_ident)
apply (blast intro: rev_subsetD [OF _ wp_mono])
@@ -548,7 +548,7 @@
and TL: "T \<in> L"
and Fstable: "F \<in> stable T"
shows "commutes F T B L"
-apply (simp add: commutes_def, clarify)
+apply (simp add: commutes_def del: Int_subset_iff, clarify)
apply (rename_tac t)
apply (subgoal_tac "\<exists>s. (s,t) \<in> relcl L & s \<in> T \<inter> wp act M")
prefer 2
--- a/src/HOL/UNITY/Transformers.thy Mon Aug 02 16:06:13 2004 +0200
+++ b/src/HOL/UNITY/Transformers.thy Tue Aug 03 13:48:00 2004 +0200
@@ -121,6 +121,10 @@
text{*Assertion 4.17 in the thesis*}
lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
+ --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
+ is declared as an iff-rule, then it's almost impossible to prove.
+ One proof is via @{text meson} after expanding all definitions, but it's
+ slow!*}
text{*Assertion (7): 4.18 in the thesis. NOTE that many of these results
hold for an arbitrary action. We often do not require @{term "act \<in> Acts F"}*}