--- 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)+
--- 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 =
--- 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)