# HG changeset patch
# User paulson
# Date 1091533680 -7200
# Node ID 04b0e943fcc96b5ef871330bc4b5d984577bcd32
# Parent  d027515e2aa61b4767afe4993df703142bcb4101
new simprules Int_subset_iff and Un_subset_iff

diff -r d027515e2aa6 -r 04b0e943fcc9 doc-src/TutorialI/CTL/CTL.thy
--- 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
diff -r d027515e2aa6 -r 04b0e943fcc9 doc-src/TutorialI/CTL/document/CTL.tex
--- 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
diff -r d027515e2aa6 -r 04b0e943fcc9 src/HOL/Bali/TypeSafe.thy
--- 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)"
diff -r d027515e2aa6 -r 04b0e943fcc9 src/HOL/HoareParallel/OG_Hoare.thy
--- 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
diff -r d027515e2aa6 -r 04b0e943fcc9 src/HOL/HoareParallel/RG_Examples.thy
--- 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 *}
diff -r d027515e2aa6 -r 04b0e943fcc9 src/HOL/HoareParallel/RG_Hoare.thy
--- 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)
diff -r d027515e2aa6 -r 04b0e943fcc9 src/HOL/Hyperreal/SEQ.thy
--- 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)
diff -r d027515e2aa6 -r 04b0e943fcc9 src/HOL/Set.thy
--- 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
diff -r d027515e2aa6 -r 04b0e943fcc9 src/HOL/UNITY/Follows.thy
--- 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)
diff -r d027515e2aa6 -r 04b0e943fcc9 src/HOL/UNITY/ProgressSets.thy
--- 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 
diff -r d027515e2aa6 -r 04b0e943fcc9 src/HOL/UNITY/Transformers.thy
--- 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"}*}