# HG changeset patch
# User wenzelm
# Date 1373547418 -7200
# Node ID a8a81453833d453ef5a8adfbe4de007d58025203
# Parent  40298d3834639eaca7cfaa6dd97539e6b5ff42b2
more precise fact declarations -- fewer warnings;

diff -r 40298d383463 -r a8a81453833d src/HOL/Hoare_Parallel/Gar_Coll.thy
--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy	Thu Jul 11 14:42:11 2013 +0200
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy	Thu Jul 11 14:56:58 2013 +0200
@@ -75,7 +75,7 @@
 apply(unfold Mutator_def)
 apply annhoare
 apply(simp_all add:Redirect_Edge Color_Target)
-apply(simp add:mutator_defs Redirect_Edge_def)
+apply(simp add:mutator_defs)
 done
 
 subsection {* The Collector *}
@@ -768,7 +768,7 @@
 apply(unfold Collector_def Mutator_def)
 apply interfree_aux
 apply(simp_all add:collector_mutator_interfree)
-apply(unfold modules collector_defs mutator_defs)
+apply(unfold modules collector_defs Mut_init_def)
 apply(tactic  {* TRYALL (interfree_aux_tac @{context}) *})
 --{* 32 subgoals left *}
 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
@@ -789,7 +789,7 @@
 apply(unfold Collector_def Mutator_def)
 apply interfree_aux
 apply(simp_all add:collector_mutator_interfree)
-apply(unfold modules collector_defs mutator_defs)
+apply(unfold modules collector_defs Mut_init_def)
 apply(tactic  {* TRYALL (interfree_aux_tac @{context}) *})
 --{* 64 subgoals left *}
 apply(simp_all add:nth_list_update Invariants Append_to_free0)+
diff -r 40298d383463 -r a8a81453833d src/HOL/Hoare_Parallel/OG_Tactics.thy
--- a/src/HOL/Hoare_Parallel/OG_Tactics.thy	Thu Jul 11 14:42:11 2013 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Tactics.thy	Thu Jul 11 14:56:58 2013 +0200
@@ -258,19 +258,20 @@
 transformation. *}
 
 lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
-by fast
-lemma list_length: "length []=0 \<and> length (x#xs) = Suc(length xs)"
-by simp
-lemma list_lemmas: "length []=0 \<and> length (x#xs) = Suc(length xs) 
-\<and> (x#xs) ! 0=x \<and> (x#xs) ! Suc n = xs ! n"
-by simp
+  by fast
+
+lemma list_length: "length []=0" "length (x#xs) = Suc(length xs)"
+  by simp_all
+lemma list_lemmas: "length []=0" "length (x#xs) = Suc(length xs)"
+    "(x#xs) ! 0 = x" "(x#xs) ! Suc n = xs ! n"
+  by simp_all
 lemma le_Suc_eq_insert: "{i. i <Suc n} = insert n {i. i< n}"
-by auto
+  by auto
 lemmas primrecdef_list = "pre.simps" "assertions.simps" "atomics.simps" "atom_com.simps"
 lemmas my_simp_list = list_lemmas fst_conv snd_conv
 not_less0 refl le_Suc_eq_insert Suc_not_Zero Zero_not_Suc nat.inject
 Collect_mem_eq ball_simps option.simps primrecdef_list
-lemmas ParallelConseq_list = INTER_eq Collect_conj_eq length_map length_upt length_append list_length
+lemmas ParallelConseq_list = INTER_eq Collect_conj_eq length_map length_upt length_append
 
 ML {*
 fun before_interfree_simp_tac ctxt =
diff -r 40298d383463 -r a8a81453833d src/HOL/Hoare_Parallel/RG_Hoare.thy
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Thu Jul 11 14:42:11 2013 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Thu Jul 11 14:56:58 2013 +0200
@@ -5,7 +5,6 @@
 subsection {* Proof System for Component Programs *}
 
 declare Un_subset_iff [simp del] le_sup_iff [simp del]
-declare Cons_eq_map_conv [iff]
 
 definition stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where  
   "stable \<equiv> \<lambda>f g. (\<forall>x y. x \<in> f \<longrightarrow> (x, y) \<in> g \<longrightarrow> y \<in> f)" 
@@ -478,7 +477,7 @@
 apply(frule_tac i="length x - 1" in exists_ctran_Await_None,force)
   apply (case_tac x,simp+)
  apply(rule last_fst_esp,simp add:last_length)
- apply(case_tac x, (simp add:cptn_not_empty)+)
+ apply(case_tac x, simp+)
 apply clarify
 apply(simp add:assum_def)
 apply clarify
@@ -592,7 +591,6 @@
 apply simp
 done
 
-declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del]
 lemma Seq_sound1 [rule_format]: 
   "x\<in> cptn_mod \<Longrightarrow> \<forall>s P. x !0=(Some (Seq P Q), s) \<longrightarrow> 
   (\<forall>i<length x. fst(x!i)\<noteq>Some Q) \<longrightarrow> 
@@ -620,7 +618,6 @@
  apply(simp add:lift_def)
 apply simp
 done
-declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del]
 
 lemma Seq_sound2 [rule_format]: 
   "x \<in> cptn \<Longrightarrow> \<forall>s P i. x!0=(Some (Seq P Q), s) \<longrightarrow> i<length x 
@@ -842,7 +839,7 @@
 apply(induct ys)
  apply simp
 apply clarify
-apply (simp add:nth_append length_append)
+apply (simp add:nth_append)
 done
 
 lemma assum_after_body: 
@@ -1108,7 +1105,7 @@
 apply(unfold par_cp_def)
 apply (rule ccontr) 
 --{* By contradiction: *}
-apply (simp del: Un_subset_iff)
+apply simp
 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)
@@ -1128,7 +1125,7 @@
  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 del: Un_subset_iff)
+apply(simp add:assum_def)
 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)
@@ -1136,7 +1133,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 del: Un_subset_iff)
+apply simp
 apply(erule subsetD)
 apply simp
 apply(simp add:conjoin_def compat_label_def)
@@ -1206,14 +1203,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 del: Un_subset_iff)
+apply(simp add: ParallelCom_def)
 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 del: Un_subset_iff)
+apply simp
 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+)
@@ -1256,14 +1253,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 del: Un_subset_iff)
+apply(simp add: ParallelCom_def)
 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 del: Un_subset_iff)
+apply simp
 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)