new simprules Int_subset_iff and Un_subset_iff
authorpaulson
Tue Aug 03 13:48:00 2004 +0200 (2004-08-03)
changeset 1510204b0e943fcc9
parent 15101 d027515e2aa6
child 15103 79846e8792eb
new simprules Int_subset_iff and Un_subset_iff
doc-src/TutorialI/CTL/CTL.thy
doc-src/TutorialI/CTL/document/CTL.tex
src/HOL/Bali/TypeSafe.thy
src/HOL/HoareParallel/OG_Hoare.thy
src/HOL/HoareParallel/RG_Examples.thy
src/HOL/HoareParallel/RG_Hoare.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Set.thy
src/HOL/UNITY/Follows.thy
src/HOL/UNITY/ProgressSets.thy
src/HOL/UNITY/Transformers.thy
     1.1 --- a/doc-src/TutorialI/CTL/CTL.thy	Mon Aug 02 16:06:13 2004 +0200
     1.2 +++ b/doc-src/TutorialI/CTL/CTL.thy	Tue Aug 03 13:48:00 2004 +0200
     1.3 @@ -117,34 +117,19 @@
     1.4  @{thm lfp_lowerbound[of _ "S",no_vars]} \hfill (@{thm[source]lfp_lowerbound})
     1.5  \end{center}
     1.6  The instance of the premise @{prop"f S \<subseteq> S"} is proved pointwise,
     1.7 -a decision that clarification takes for us:
     1.8 +a decision that \isa{auto} takes for us:
     1.9  *};
    1.10  apply(rule lfp_lowerbound);
    1.11 -apply(clarsimp simp add: af_def Paths_def);
    1.12 +apply(auto simp add: af_def Paths_def);
    1.13  
    1.14  txt{*
    1.15  @{subgoals[display,indent=0,margin=70,goals_limit=1]}
    1.16 -Now we eliminate the disjunction. The case @{prop"p(0::nat) \<in> A"} is trivial:
    1.17 -*};
    1.18 -
    1.19 -apply(erule disjE);
    1.20 - apply(blast);
    1.21 -
    1.22 -txt{*\noindent
    1.23 -In the other case we set @{term t} to @{term"p(1::nat)"} and simplify matters:
    1.24 +In this remaining case, we set @{term t} to @{term"p(1::nat)"}.
    1.25 +The rest is automatic.
    1.26  *};
    1.27  
    1.28  apply(erule_tac x = "p 1" in allE);
    1.29 -apply(clarsimp);
    1.30 -
    1.31 -txt{*
    1.32 -@{subgoals[display,indent=0,margin=70,goals_limit=1]}
    1.33 -It merely remains to set @{term pa} to @{term"\<lambda>i. p(i+1::nat)"}, that is, 
    1.34 -@{term p} without its first element.  The rest is automatic:
    1.35 -*};
    1.36 -
    1.37 -apply(erule_tac x = "\<lambda>i. p(i+1)" in allE);
    1.38 -apply force;
    1.39 +apply(auto);
    1.40  done;
    1.41  
    1.42  
    1.43 @@ -389,11 +374,9 @@
    1.44  
    1.45  lemma "lfp(eufix A B) \<subseteq> eusem A B"
    1.46  apply(rule lfp_lowerbound)
    1.47 -apply(clarsimp simp add: eusem_def eufix_def);
    1.48 -apply(erule disjE);
    1.49 +apply(auto simp add: eusem_def eufix_def);
    1.50   apply(rule_tac x = "[]" in exI);
    1.51   apply simp
    1.52 -apply(clarsimp);
    1.53  apply(rule_tac x = "y#xc" in exI);
    1.54  apply simp;
    1.55  done
     2.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex	Mon Aug 02 16:06:13 2004 +0200
     2.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex	Tue Aug 03 13:48:00 2004 +0200
     2.3 @@ -110,52 +110,28 @@
     2.4  \isa{f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound})
     2.5  \end{center}
     2.6  The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise,
     2.7 -a decision that clarification takes for us:%
     2.8 +a decision that \isa{auto} takes for us:%
     2.9  \end{isamarkuptxt}%
    2.10  \isamarkuptrue%
    2.11  \isacommand{apply}{\isacharparenleft}rule\ lfp{\isacharunderscore}lowerbound{\isacharparenright}\isanewline
    2.12  \isamarkupfalse%
    2.13 -\isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
    2.14 +\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
    2.15  %
    2.16  \begin{isamarkuptxt}%
    2.17  \begin{isabelle}%
    2.18 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ {\isadigit{0}}\ {\isasymin}\ A\ {\isasymor}\isanewline
    2.19 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}}{\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
    2.20 -\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
    2.21 -\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
    2.22 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
    2.23 +\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
    2.24 +\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
    2.25  \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ }{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
    2.26  \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
    2.27  \end{isabelle}
    2.28 -Now we eliminate the disjunction. The case \isa{p\ {\isadigit{0}}\ {\isasymin}\ A} is trivial:%
    2.29 -\end{isamarkuptxt}%
    2.30 -\isamarkuptrue%
    2.31 -\isacommand{apply}{\isacharparenleft}erule\ disjE{\isacharparenright}\isanewline
    2.32 -\ \isamarkupfalse%
    2.33 -\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isamarkupfalse%
    2.34 -%
    2.35 -\begin{isamarkuptxt}%
    2.36 -\noindent
    2.37 -In the other case we set \isa{t} to \isa{p\ {\isadigit{1}}} and simplify matters:%
    2.38 +In this remaining case, we set \isa{t} to \isa{p\ {\isadigit{1}}}.
    2.39 +The rest is automatic.%
    2.40  \end{isamarkuptxt}%
    2.41  \isamarkuptrue%
    2.42  \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ {\isadigit{1}}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
    2.43  \isamarkupfalse%
    2.44 -\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isamarkupfalse%
    2.45 -%
    2.46 -\begin{isamarkuptxt}%
    2.47 -\begin{isabelle}%
    2.48 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\isanewline
    2.49 -\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
    2.50 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ {\isasymforall}pa{\isachardot}\ }{\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
    2.51 -\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
    2.52 -\end{isabelle}
    2.53 -It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}}, that is, 
    2.54 -\isa{p} without its first element.  The rest is automatic:%
    2.55 -\end{isamarkuptxt}%
    2.56 -\isamarkuptrue%
    2.57 -\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
    2.58 -\isamarkupfalse%
    2.59 -\isacommand{apply}\ force\isanewline
    2.60 +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
    2.61  \isamarkupfalse%
    2.62  \isacommand{done}\isamarkupfalse%
    2.63  %
    2.64 @@ -463,8 +439,6 @@
    2.65  \isamarkupfalse%
    2.66  \isamarkupfalse%
    2.67  \isamarkupfalse%
    2.68 -\isamarkupfalse%
    2.69 -\isamarkupfalse%
    2.70  %
    2.71  \begin{isamarkuptext}%
    2.72  Let us close this section with a few words about the executability of
     3.1 --- a/src/HOL/Bali/TypeSafe.thy	Mon Aug 02 16:06:13 2004 +0200
     3.2 +++ b/src/HOL/Bali/TypeSafe.thy	Tue Aug 03 13:48:00 2004 +0200
     3.3 @@ -1477,7 +1477,7 @@
     3.4    qed
     3.5  next
     3.6    show "?Hd x y \<union> ?Tl xs ys  \<subseteq> ?List x xs y ys" 
     3.7 -  proof 
     3.8 +  proof (rule subsetI)
     3.9      fix el 
    3.10      assume  el_in_hd_tl: "el \<in>  ?Hd x y \<union> ?Tl xs ys"
    3.11      show "el \<in> ?List x xs y ys"
    3.12 @@ -2978,7 +2978,7 @@
    3.13  	  by simp
    3.14  	from da_e1 s0_s1 True obtain E1' where
    3.15  	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'"
    3.16 -	  by - (rule da_weakenE,auto)
    3.17 +	  by - (rule da_weakenE, auto iff del: Un_subset_iff)
    3.18  	with conf_s1 wt_e1
    3.19  	obtain 
    3.20  	  "s2\<Colon>\<preceq>(G, L)"
    3.21 @@ -2997,7 +2997,7 @@
    3.22  	  by simp
    3.23  	from da_e2 s0_s1 False obtain E2' where
    3.24  	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'"
    3.25 -	  by - (rule da_weakenE,auto)
    3.26 +	  by - (rule da_weakenE, auto iff del: Un_subset_iff)
    3.27  	with conf_s1 wt_e2
    3.28  	obtain 
    3.29  	  "s2\<Colon>\<preceq>(G, L)"
     4.1 --- a/src/HOL/HoareParallel/OG_Hoare.thy	Mon Aug 02 16:06:13 2004 +0200
     4.2 +++ b/src/HOL/HoareParallel/OG_Hoare.thy	Tue Aug 03 13:48:00 2004 +0200
     4.3 @@ -117,19 +117,13 @@
     4.4  apply (induct "k")
     4.5   apply(simp (no_asm) add: L3_5v_lemma3)
     4.6  apply(simp (no_asm) add: L3_5iv L3_5ii Parallel_empty)
     4.7 -apply(rule Un_least)
     4.8 - apply(rule subset_trans)
     4.9 -  prefer 2 apply simp
    4.10 - apply(erule L3_5i)
    4.11 +apply(rule conjI)
    4.12 + apply (blast dest: L3_5i) 
    4.13  apply(simp add: SEM_def sem_def id_def)
    4.14 -apply clarify
    4.15 -apply(drule rtrancl_imp_UN_rel_pow)
    4.16 -apply clarify
    4.17 -apply(drule Basic_ntran)
    4.18 - apply fast+
    4.19 +apply (blast dest: Basic_ntran rtrancl_imp_UN_rel_pow) 
    4.20  done
    4.21  
    4.22 -lemma atom_hoare_sound [rule_format (no_asm)]: 
    4.23 +lemma atom_hoare_sound [rule_format]: 
    4.24   " \<parallel>- p c q \<longrightarrow> atom_com(c) \<longrightarrow> \<parallel>= p c q"
    4.25  apply (unfold com_validity_def)
    4.26  apply(rule oghoare_induct)
    4.27 @@ -143,19 +137,11 @@
    4.28      prefer 2 apply simp
    4.29     apply(simp add: L3_5ii L3_5i)
    4.30  --{* Cond *}
    4.31 -  apply(rule impI)
    4.32    apply(simp add: L3_5iv)
    4.33 -  apply(erule Un_least)
    4.34 -  apply assumption
    4.35  --{* While *}
    4.36 - apply(rule impI)
    4.37 - apply(simp add: L3_5v)
    4.38 - apply(rule UN_least)
    4.39 - apply(drule SEM_fwhile)
    4.40 - apply assumption
    4.41 + apply (force simp add: L3_5v dest: SEM_fwhile) 
    4.42  --{* Conseq *}
    4.43 -apply(simp add: SEM_def sem_def)
    4.44 -apply force
    4.45 +apply(force simp add: SEM_def sem_def)
    4.46  done
    4.47      
    4.48  subsection {* Soundness of the System for Component Programs *}
    4.49 @@ -450,7 +436,7 @@
    4.50  apply simp+
    4.51  done
    4.52  
    4.53 -lemma oghoare_sound [rule_format (no_asm)]: "\<parallel>- p c q \<longrightarrow> \<parallel>= p c q"
    4.54 +lemma oghoare_sound [rule_format]: "\<parallel>- p c q \<longrightarrow> \<parallel>= p c q"
    4.55  apply (unfold com_validity_def)
    4.56  apply(rule oghoare_induct)
    4.57  apply(rule TrueI)+
    4.58 @@ -477,16 +463,11 @@
    4.59     apply(simp add: L3_5ii L3_5i)
    4.60  --{* Cond *}
    4.61    apply(simp add: L3_5iv)
    4.62 -  apply(erule Un_least)
    4.63 -  apply assumption
    4.64  --{* While *}
    4.65   apply(simp add: L3_5v)
    4.66 - apply(rule UN_least)
    4.67 - apply(drule SEM_fwhile)
    4.68 - apply assumption
    4.69 + apply (blast dest: SEM_fwhile) 
    4.70  --{* Conseq *}
    4.71 -apply(simp add: SEM_def sem_def)
    4.72 -apply auto
    4.73 +apply(auto simp add: SEM_def sem_def)
    4.74  done
    4.75  
    4.76  end
    4.77 \ No newline at end of file
     5.1 --- a/src/HOL/HoareParallel/RG_Examples.thy	Mon Aug 02 16:06:13 2004 +0200
     5.2 +++ b/src/HOL/HoareParallel/RG_Examples.thy	Tue Aug 03 13:48:00 2004 +0200
     5.3 @@ -26,16 +26,7 @@
     5.4      COEND
     5.5   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>]"
     5.6  apply(rule Parallel)
     5.7 -    apply simp
     5.8 -    apply clarify
     5.9 -    apply simp
    5.10 -    apply(erule disjE)
    5.11 -     apply simp
    5.12 -    apply clarify
    5.13 -    apply simp
    5.14 -   apply auto
    5.15 -apply(rule Basic)
    5.16 -apply auto
    5.17 +apply (auto intro!: Basic) 
    5.18  done
    5.19  
    5.20  lemma Example1_parameterized: 
    5.21 @@ -53,33 +44,14 @@
    5.22        (\<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>, 
    5.23        \<lbrace>\<forall>i<n. \<acute>A!(k*n+i) = 0\<rbrace>]"
    5.24  apply(rule Parallel)
    5.25 -    apply simp
    5.26 -    apply clarify
    5.27 -    apply simp
    5.28 -    apply(erule disjE)
    5.29 -     apply clarify
    5.30 -     apply simp
    5.31 -    apply clarify
    5.32 -    apply simp
    5.33 -    apply clarify
    5.34 -    apply simp
    5.35 -    apply(erule_tac x="k*n +i" in allE)
    5.36 -    apply(subgoal_tac "k*n+i <length (A b)")
    5.37 -     apply force
    5.38 -    apply(erule le_less_trans2) 
    5.39 -    apply(case_tac t,simp+)
    5.40 -    apply (simp add:add_commute)
    5.41 -    apply(rule add_le_mono)
    5.42 -     apply simp
    5.43 -    apply simp
    5.44 -   apply simp
    5.45 -   apply clarify
    5.46 -   apply(rotate_tac -1)
    5.47 +    apply auto
    5.48 +  apply(erule_tac x="k*n +i" in allE)
    5.49 +  apply(subgoal_tac "k*n+i <length (A b)")
    5.50     apply force
    5.51 -  apply force
    5.52 - apply force
    5.53 -apply simp
    5.54 -apply clarify
    5.55 +  apply(erule le_less_trans2) 
    5.56 +  apply(case_tac t,simp+)
    5.57 +  apply (simp add:add_commute)
    5.58 +  apply(simp add: add_le_mono)
    5.59  apply(rule Basic)
    5.60     apply simp
    5.61     apply clarify
    5.62 @@ -88,12 +60,10 @@
    5.63     apply(erule le_less_trans2)
    5.64     apply(case_tac t,simp+)
    5.65     apply (simp add:add_commute)
    5.66 -   apply(rule add_le_mono)
    5.67 -    apply simp
    5.68 -   apply simp
    5.69 -  apply force+
    5.70 +   apply(rule add_le_mono, auto)
    5.71  done
    5.72  
    5.73 +
    5.74  subsection {* Increment a Variable in Parallel *}
    5.75  
    5.76  subsubsection {* Two components *}
    5.77 @@ -134,7 +104,7 @@
    5.78     apply clarify
    5.79     apply(case_tac i)
    5.80      apply simp
    5.81 -    apply(erule disjE)
    5.82 +    apply(rule conjI)
    5.83       apply clarify
    5.84       apply simp
    5.85      apply clarify
    5.86 @@ -142,7 +112,7 @@
    5.87      apply(case_tac j,simp)
    5.88      apply simp
    5.89     apply simp
    5.90 -   apply(erule disjE)
    5.91 +   apply(rule conjI)
    5.92      apply clarify
    5.93      apply simp
    5.94     apply clarify
    5.95 @@ -179,10 +149,7 @@
    5.96   apply(rule Basic)
    5.97    apply simp_all
    5.98   apply(rule subset_refl)
    5.99 -apply(rule Basic)
   5.100 -apply simp_all
   5.101 -apply clarify
   5.102 -apply simp
   5.103 +apply(auto intro!: Basic)
   5.104  done
   5.105  
   5.106  subsubsection {* Parameterized *}
     6.1 --- a/src/HOL/HoareParallel/RG_Hoare.thy	Mon Aug 02 16:06:13 2004 +0200
     6.2 +++ b/src/HOL/HoareParallel/RG_Hoare.thy	Tue Aug 03 13:48:00 2004 +0200
     6.3 @@ -4,6 +4,8 @@
     6.4  
     6.5  subsection {* Proof System for Component Programs *}
     6.6  
     6.7 +declare Un_subset_iff [iff del]
     6.8 +
     6.9  constdefs
    6.10    stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"  
    6.11    "stable \<equiv> \<lambda>f g. (\<forall>x y. x \<in> f \<longrightarrow> (x, y) \<in> g \<longrightarrow> y \<in> f)" 
    6.12 @@ -1179,12 +1181,9 @@
    6.13    \<Longrightarrow> \<forall>j i. i<length clist \<and> Suc j<length x \<longrightarrow> (clist!i!j) -c\<rightarrow> (clist!i!Suc j) 
    6.14    \<longrightarrow> (snd(clist!i!j), snd(clist!i!Suc j)) \<in> Guar(xs!i)"
    6.15  apply(unfold par_cp_def)
    6.16 +apply (rule ccontr) 
    6.17  --{* By contradiction: *}
    6.18 -apply(subgoal_tac "True")
    6.19 - prefer 2
    6.20 - apply simp 
    6.21 -apply(erule_tac Q="True" in contrapos_pp)
    6.22 -apply simp
    6.23 +apply (simp del: Un_subset_iff)
    6.24  apply(erule exE)
    6.25  --{* the first c-tran that does not satisfy the guarantee-condition is from @{text "\<sigma>_i"} at step @{text "m"}. *}
    6.26  apply(drule_tac n=j and P="\<lambda>j. \<exists>i. ?H i j" in Ex_first_occurrence)
    6.27 @@ -1199,13 +1198,12 @@
    6.28   apply(simp add:cp_def comm_def)
    6.29   apply(drule_tac c="take (Suc (Suc m)) (clist ! i)" in subsetD)
    6.30    apply simp
    6.31 -  apply(erule_tac x=i in allE, erule impE, assumption,erule conjE)
    6.32 -  apply(erule takecptn_is_cptn)
    6.33 +  apply (blast intro: takecptn_is_cptn) 
    6.34   apply simp
    6.35   apply clarify
    6.36   apply(erule_tac x=m and P="\<lambda>j. ?I j \<and> ?J j \<longrightarrow> ?H j" in allE)
    6.37   apply (simp add:conjoin_def same_length_def)
    6.38 -apply(simp add:assum_def)
    6.39 +apply(simp add:assum_def del: Un_subset_iff)
    6.40  apply(rule conjI)
    6.41   apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow>  ?I j \<in>cp (?K j) (?J j)" in allE)
    6.42   apply(simp add:cp_def par_assum_def)
    6.43 @@ -1213,7 +1211,7 @@
    6.44   apply simp
    6.45  apply clarify
    6.46  apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> ?M \<union> UNION (?S j) (?T j) \<subseteq>  (?L j)" in allE)
    6.47 -apply simp
    6.48 +apply(simp del: Un_subset_iff)
    6.49  apply(erule subsetD)
    6.50  apply simp
    6.51  apply(simp add:conjoin_def compat_label_def)
    6.52 @@ -1242,6 +1240,7 @@
    6.53  apply (force simp add:par_assum_def same_state_def)
    6.54  done
    6.55  
    6.56 +
    6.57  lemma three [rule_format]: 
    6.58    "\<lbrakk> xs\<noteq>[]; \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j)) 
    6.59     \<subseteq> Rely (xs ! i);
    6.60 @@ -1282,14 +1281,14 @@
    6.61     x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely); Suc i < length x; 
    6.62     x ! i -pc\<rightarrow> x ! Suc i\<rbrakk>
    6.63    \<Longrightarrow> (snd (x ! i), snd (x ! Suc i)) \<in> guar"
    6.64 -apply(simp add: ParallelCom_def)
    6.65 +apply(simp add: ParallelCom_def del: Un_subset_iff)
    6.66  apply(subgoal_tac "(map (Some \<circ> fst) xs)\<noteq>[]")
    6.67   prefer 2
    6.68   apply simp
    6.69  apply(frule rev_subsetD)
    6.70   apply(erule one [THEN equalityD1])
    6.71  apply(erule subsetD)
    6.72 -apply simp
    6.73 +apply (simp del: Un_subset_iff)
    6.74  apply clarify
    6.75  apply(drule_tac pre=pre and rely=rely and  x=x and s=s and xs=xs and clist=clist in two)
    6.76  apply(assumption+)
    6.77 @@ -1332,14 +1331,14 @@
    6.78      \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)];
    6.79      x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely); 
    6.80     All_None (fst (last x)) \<rbrakk> \<Longrightarrow> snd (last x) \<in> post"
    6.81 -apply(simp add: ParallelCom_def)
    6.82 +apply(simp add: ParallelCom_def del: Un_subset_iff)
    6.83  apply(subgoal_tac "(map (Some \<circ> fst) xs)\<noteq>[]")
    6.84   prefer 2
    6.85   apply simp
    6.86  apply(frule rev_subsetD)
    6.87   apply(erule one [THEN equalityD1])
    6.88  apply(erule subsetD)
    6.89 -apply simp
    6.90 +apply(simp del: Un_subset_iff)
    6.91  apply clarify
    6.92  apply(subgoal_tac "\<forall>i<length clist. clist!i\<in>assum(Pre(xs!i), Rely(xs!i))")
    6.93   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)
     7.1 --- a/src/HOL/Hyperreal/SEQ.thy	Mon Aug 02 16:06:13 2004 +0200
     7.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Tue Aug 03 13:48:00 2004 +0200
     7.3 @@ -1048,7 +1048,7 @@
     7.4  apply (simp add: inverse_eq_divide pos_divide_less_eq)
     7.5  done
     7.6  
     7.7 -subsubsection{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
     7.8 +text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
     7.9  
    7.10  lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) ----> 0"
    7.11  by (blast intro!: LIMSEQ_realpow_zero abs_ge_zero)
     8.1 --- a/src/HOL/Set.thy	Mon Aug 02 16:06:13 2004 +0200
     8.2 +++ b/src/HOL/Set.thy	Tue Aug 03 13:48:00 2004 +0200
     8.3 @@ -1275,7 +1275,7 @@
     8.4  lemma Int_UNIV [simp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
     8.5    by blast
     8.6  
     8.7 -lemma Int_subset_iff: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
     8.8 +lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
     8.9    by blast
    8.10  
    8.11  lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
    8.12 @@ -1352,7 +1352,8 @@
    8.13  
    8.14  lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
    8.15    by blast
    8.16 -lemma Un_subset_iff: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
    8.17 +
    8.18 +lemma Un_subset_iff [simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
    8.19    by blast
    8.20  
    8.21  lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
    8.22 @@ -1473,7 +1474,7 @@
    8.23    by blast
    8.24  
    8.25  lemma UN_absorb: "k \<in> I ==> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
    8.26 -  by blast
    8.27 +  by auto
    8.28  
    8.29  lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
    8.30    by blast
     9.1 --- a/src/HOL/UNITY/Follows.thy	Mon Aug 02 16:06:13 2004 +0200
     9.2 +++ b/src/HOL/UNITY/Follows.thy	Tue Aug 03 13:48:00 2004 +0200
     9.3 @@ -36,14 +36,12 @@
     9.4  done
     9.5  
     9.6  lemma Follows_constant [iff]: "F \<in> (%s. c) Fols (%s. c)"
     9.7 -by (unfold Follows_def, auto)
     9.8 +by (simp add: Follows_def)
     9.9  
    9.10  lemma mono_Follows_o: "mono h ==> f Fols g \<subseteq> (h o f) Fols (h o g)"
    9.11 -apply (unfold Follows_def, clarify)
    9.12 -apply (simp add: mono_Increasing_o [THEN [2] rev_subsetD]
    9.13 -                 mono_Always_o [THEN [2] rev_subsetD]
    9.14 -                 mono_LeadsTo_o [THEN [2] rev_subsetD, THEN INT_D])
    9.15 -done
    9.16 +by (auto simp add: Follows_def mono_Increasing_o [THEN [2] rev_subsetD]
    9.17 +		   mono_Always_o [THEN [2] rev_subsetD]
    9.18 +		   mono_LeadsTo_o [THEN [2] rev_subsetD, THEN INT_D])
    9.19  
    9.20  lemma mono_Follows_apply:
    9.21       "mono h ==> f Fols g \<subseteq> (%x. h (f x)) Fols (%x. h (g x))"
    9.22 @@ -53,7 +51,7 @@
    9.23  
    9.24  lemma Follows_trans: 
    9.25       "[| F \<in> f Fols g;  F \<in> g Fols h |] ==> F \<in> f Fols h"
    9.26 -apply (unfold Follows_def)
    9.27 +apply (simp add: Follows_def)
    9.28  apply (simp add: Always_eq_includes_reachable)
    9.29  apply (blast intro: order_trans LeadsTo_Trans)
    9.30  done
    9.31 @@ -62,17 +60,17 @@
    9.32  subsection{*Destruction rules*}
    9.33  
    9.34  lemma Follows_Increasing1: "F \<in> f Fols g ==> F \<in> Increasing f"
    9.35 -by (unfold Follows_def, blast)
    9.36 +by (simp add: Follows_def)
    9.37  
    9.38  lemma Follows_Increasing2: "F \<in> f Fols g ==> F \<in> Increasing g"
    9.39 -by (unfold Follows_def, blast)
    9.40 +by (simp add: Follows_def)
    9.41  
    9.42  lemma Follows_Bounded: "F \<in> f Fols g ==> F \<in> Always {s. f s \<subseteq> g s}"
    9.43 -by (unfold Follows_def, blast)
    9.44 +by (simp add: Follows_def)
    9.45  
    9.46  lemma Follows_LeadsTo: 
    9.47       "F \<in> f Fols g ==> F \<in> {s. k \<le> g s} LeadsTo {s. k \<le> f s}"
    9.48 -by (unfold Follows_def, blast)
    9.49 +by (simp add: Follows_def)
    9.50  
    9.51  lemma Follows_LeadsTo_pfixLe:
    9.52       "F \<in> f Fols g ==> F \<in> {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}"
    9.53 @@ -96,7 +94,7 @@
    9.54  lemma Always_Follows1: 
    9.55       "[| F \<in> Always {s. f s = f' s}; F \<in> f Fols g |] ==> F \<in> f' Fols g"
    9.56  
    9.57 -apply (unfold Follows_def Increasing_def Stable_def, auto)
    9.58 +apply (simp add: Follows_def Increasing_def Stable_def, auto)
    9.59  apply (erule_tac [3] Always_LeadsTo_weaken)
    9.60  apply (erule_tac A = "{s. z \<le> f s}" and A' = "{s. z \<le> f s}" 
    9.61         in Always_Constrains_weaken, auto)
    9.62 @@ -106,7 +104,7 @@
    9.63  
    9.64  lemma Always_Follows2: 
    9.65       "[| F \<in> Always {s. g s = g' s}; F \<in> f Fols g |] ==> F \<in> f Fols g'"
    9.66 -apply (unfold Follows_def Increasing_def Stable_def, auto)
    9.67 +apply (simp add: Follows_def Increasing_def Stable_def, auto)
    9.68  apply (erule_tac [3] Always_LeadsTo_weaken)
    9.69  apply (erule_tac A = "{s. z \<le> g s}" and A' = "{s. z \<le> g s}"
    9.70         in Always_Constrains_weaken, auto)
    9.71 @@ -121,7 +119,7 @@
    9.72  lemma increasing_Un: 
    9.73      "[| F \<in> increasing f;  F \<in> increasing g |]  
    9.74       ==> F \<in> increasing (%s. (f s) \<union> (g s))"
    9.75 -apply (unfold increasing_def stable_def constrains_def, auto)
    9.76 +apply (simp add: increasing_def stable_def constrains_def, auto)
    9.77  apply (drule_tac x = "f xa" in spec)
    9.78  apply (drule_tac x = "g xa" in spec)
    9.79  apply (blast dest!: bspec)
    9.80 @@ -162,8 +160,7 @@
    9.81  lemma Follows_Un: 
    9.82      "[| F \<in> f' Fols f;  F \<in> g' Fols g |]  
    9.83       ==> F \<in> (%s. (f' s) \<union> (g' s)) Fols (%s. (f s) \<union> (g s))"
    9.84 -apply (unfold Follows_def)
    9.85 -apply (simp add: Increasing_Un Always_Un, auto)
    9.86 +apply (simp add: Follows_def Increasing_Un Always_Un del: Un_subset_iff, auto)
    9.87  apply (rule LeadsTo_Trans)
    9.88  apply (blast intro: Follows_Un_lemma)
    9.89  (*Weakening is used to exchange Un's arguments*)
    9.90 @@ -176,7 +173,7 @@
    9.91  lemma increasing_union: 
    9.92      "[| F \<in> increasing f;  F \<in> increasing g |]  
    9.93       ==> F \<in> increasing (%s. (f s) + (g s :: ('a::order) multiset))"
    9.94 -apply (unfold increasing_def stable_def constrains_def, auto)
    9.95 +apply (simp add: increasing_def stable_def constrains_def, auto)
    9.96  apply (drule_tac x = "f xa" in spec)
    9.97  apply (drule_tac x = "g xa" in spec)
    9.98  apply (drule bspec, assumption) 
    9.99 @@ -223,7 +220,7 @@
   9.100       "!!g g' ::'b => ('a::order) multiset.  
   9.101          [| F \<in> f' Fols f;  F \<in> g' Fols g |]  
   9.102          ==> F \<in> (%s. (f' s) + (g' s)) Fols (%s. (f s) + (g s))"
   9.103 -apply (unfold Follows_def)
   9.104 +apply (simp add: Follows_def)
   9.105  apply (simp add: Increasing_union Always_union, auto)
   9.106  apply (rule LeadsTo_Trans)
   9.107  apply (blast intro: Follows_union_lemma)
    10.1 --- a/src/HOL/UNITY/ProgressSets.thy	Mon Aug 02 16:06:13 2004 +0200
    10.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Tue Aug 03 13:48:00 2004 +0200
    10.3 @@ -486,11 +486,11 @@
    10.4    shows "closed F T B L"
    10.5  apply (simp add: closed_def, clarify)
    10.6  apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice])  
    10.7 -apply (simp add: Int_Un_distrib cl_Un [OF lattice] Un_subset_iff
    10.8 +apply (simp add: Int_Un_distrib cl_Un [OF lattice] Un_subset_iff 
    10.9                   cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1)
   10.10  apply (subgoal_tac "cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))") 
   10.11   prefer 2 
   10.12 - apply (simp add: commutes [unfolded commutes_def]) 
   10.13 + apply (cut_tac commutes, simp add: commutes_def) 
   10.14  apply (erule subset_trans) 
   10.15  apply (simp add: cl_ident)
   10.16  apply (blast intro: rev_subsetD [OF _ wp_mono]) 
   10.17 @@ -548,7 +548,7 @@
   10.18        and TL: "T \<in> L"
   10.19        and Fstable: "F \<in> stable T"
   10.20    shows  "commutes F T B L"
   10.21 -apply (simp add: commutes_def, clarify)  
   10.22 +apply (simp add: commutes_def del: Int_subset_iff, clarify)  
   10.23  apply (rename_tac t)
   10.24  apply (subgoal_tac "\<exists>s. (s,t) \<in> relcl L & s \<in> T \<inter> wp act M") 
   10.25   prefer 2 
    11.1 --- a/src/HOL/UNITY/Transformers.thy	Mon Aug 02 16:06:13 2004 +0200
    11.2 +++ b/src/HOL/UNITY/Transformers.thy	Tue Aug 03 13:48:00 2004 +0200
    11.3 @@ -121,6 +121,10 @@
    11.4  text{*Assertion 4.17 in the thesis*}
    11.5  lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A" 
    11.6  by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
    11.7 +  --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
    11.8 +      is declared as an iff-rule, then it's almost impossible to prove. 
    11.9 +      One proof is via @{text meson} after expanding all definitions, but it's
   11.10 +      slow!*}
   11.11  
   11.12  text{*Assertion (7): 4.18 in the thesis.  NOTE that many of these results
   11.13  hold for an arbitrary action.  We often do not require @{term "act \<in> Acts F"}*}