# HG changeset patch
# User huffman
# Date 1266528599 28800
# Node ID a03462cbf86f25c2278e784a3dc0890a9eb3651f
# Parent  67689d276c70a375215430b9174e3be6fbe6153f
get rid of warnings about duplicate simp rules in all HOLCF theories

diff -r 67689d276c70 -r a03462cbf86f src/HOLCF/FOCUS/Fstream.thy
--- a/src/HOLCF/FOCUS/Fstream.thy	Thu Feb 18 12:36:09 2010 -0800
+++ b/src/HOLCF/FOCUS/Fstream.thy	Thu Feb 18 13:29:59 2010 -0800
@@ -207,7 +207,7 @@
 lemma fsfilter_fscons:
         "A(C)x~> xs = (if x:A then x~> (A(C)xs) else A(C)xs)"
 apply (unfold fsfilter_def)
-apply (simp add: fscons_def2 sfilter_scons If_and_if)
+apply (simp add: fscons_def2 If_and_if)
 done
 
 lemma fsfilter_emptys: "{}(C)x = UU"
diff -r 67689d276c70 -r a03462cbf86f src/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOLCF/FOCUS/Fstreams.thy	Thu Feb 18 12:36:09 2010 -0800
+++ b/src/HOLCF/FOCUS/Fstreams.thy	Thu Feb 18 13:29:59 2010 -0800
@@ -208,9 +208,6 @@
 by (simp add: fsmap_def fsingleton_def2 flift2_def)
 
 
-declare range_composition[simp del]
-
-
 lemma fstreams_chain_lemma[rule_format]:
   "ALL s x y. stream_take n$(s::'a fstream) << x & x << y & y << s & x ~= y --> stream_take (Suc n)$s << y"
 apply (induct_tac n, auto)
@@ -225,7 +222,7 @@
 apply (drule stream_prefix, auto)
 apply (case_tac "y=UU",auto)
 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
-apply (auto simp add: stream.inverts)
+apply auto
 apply (simp add: flat_less_iff)
 apply (erule_tac x="tt" in allE)
 apply (erule_tac x="yb" in allE, auto)
diff -r 67689d276c70 -r a03462cbf86f src/HOLCF/IOA/ABP/Correctness.thy
--- a/src/HOLCF/IOA/ABP/Correctness.thy	Thu Feb 18 12:36:09 2010 -0800
+++ b/src/HOLCF/IOA/ABP/Correctness.thy	Thu Feb 18 13:29:59 2010 -0800
@@ -57,10 +57,12 @@
   and impl_asigs = sender_asig_def receiver_asig_def
 
 declare let_weak_cong [cong]
-declare Let_def [simp] ioa_triple_proj [simp] starts_of_par [simp]
+declare ioa_triple_proj [simp] starts_of_par [simp]
 
 lemmas env_ioas = env_ioa_def env_asig_def env_trans_def
-lemmas hom_ioas [simp] = env_ioas impl_ioas impl_trans impl_asigs asig_projections set_lemmas
+lemmas hom_ioas =
+  env_ioas [simp] impl_ioas [simp] impl_trans [simp] impl_asigs [simp]
+  asig_projections set_lemmas
 
 
 subsection {* lemmas about reduce *}
@@ -96,7 +98,7 @@
 apply (induct_tac "l")
 apply (simp (no_asm))
 apply (case_tac "list=[]")
- apply (simp add: reverse.simps)
+ apply simp
  apply (rule impI)
 apply (simp (no_asm))
 apply (cut_tac l = "list" in cons_not_nil)
diff -r 67689d276c70 -r a03462cbf86f src/HOLCF/IOA/NTP/Correctness.thy
--- a/src/HOLCF/IOA/NTP/Correctness.thy	Thu Feb 18 12:36:09 2010 -0800
+++ b/src/HOLCF/IOA/NTP/Correctness.thy	Thu Feb 18 13:29:59 2010 -0800
@@ -50,7 +50,7 @@
   apply (simp (no_asm) add: impl_ioas)
   apply (simp (no_asm) add: impl_asigs)
   apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections)
-  apply (simp (no_asm) add: "transitions" unfold_renaming)
+  apply (simp (no_asm) add: "transitions"(1) unfold_renaming)
   txt {* 1 *}
   apply (simp (no_asm) add: impl_ioas)
   apply (simp (no_asm) add: impl_asigs)
diff -r 67689d276c70 -r a03462cbf86f src/HOLCF/IOA/NTP/Impl.thy
--- a/src/HOLCF/IOA/NTP/Impl.thy	Thu Feb 18 12:36:09 2010 -0800
+++ b/src/HOLCF/IOA/NTP/Impl.thy	Thu Feb 18 13:29:59 2010 -0800
@@ -61,7 +61,7 @@
 
 subsection {* Invariants *}
 
-declare Let_def [simp] le_SucI [simp]
+declare le_SucI [simp]
 
 lemmas impl_ioas =
   impl_def sender_ioa_def receiver_ioa_def srch_ioa_thm [THEN eq_reflection]
diff -r 67689d276c70 -r a03462cbf86f src/HOLCF/IOA/Storage/Correctness.thy
--- a/src/HOLCF/IOA/Storage/Correctness.thy	Thu Feb 18 12:36:09 2010 -0800
+++ b/src/HOLCF/IOA/Storage/Correctness.thy	Thu Feb 18 13:29:59 2010 -0800
@@ -18,7 +18,6 @@
                         in
                         (! l:used. l < k) & b=c}"
 
-declare split_paired_All [simp]
 declare split_paired_Ex [simp del]
 
 
diff -r 67689d276c70 -r a03462cbf86f src/HOLCF/IOA/meta_theory/CompoExecs.thy
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Thu Feb 18 12:36:09 2010 -0800
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Thu Feb 18 13:29:59 2010 -0800
@@ -62,7 +62,7 @@
         asig_comp sigA sigB))"
 
 
-lemmas [simp del] = ex_simps all_simps split_paired_All
+lemmas [simp del] = split_paired_All
 
 
 section "recursive equations of operators"
diff -r 67689d276c70 -r a03462cbf86f src/HOLCF/IOA/meta_theory/CompoScheds.thy
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Thu Feb 18 12:36:09 2010 -0800
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Thu Feb 18 13:29:59 2010 -0800
@@ -64,9 +64,6 @@
         asig_comp sigA sigB))"
 
 
-declare surjective_pairing [symmetric, simp]
-
-
 subsection "mkex rewrite rules"
 
 
diff -r 67689d276c70 -r a03462cbf86f src/HOLCF/IOA/meta_theory/CompoTraces.thy
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Feb 18 12:36:09 2010 -0800
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Feb 18 13:29:59 2010 -0800
@@ -207,18 +207,18 @@
 (* a:A, a:B *)
 apply simp
 apply (rule Forall_Conc_impl [THEN mp])
-apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
+apply (simp add: intA_is_not_actB int_is_act)
 apply (rule Forall_Conc_impl [THEN mp])
-apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
+apply (simp add: intA_is_not_actB int_is_act)
 (* a:A,a~:B *)
 apply simp
 apply (rule Forall_Conc_impl [THEN mp])
-apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
+apply (simp add: intA_is_not_actB int_is_act)
 apply (case_tac "a:act B")
 (* a~:A, a:B *)
 apply simp
 apply (rule Forall_Conc_impl [THEN mp])
-apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
+apply (simp add: intA_is_not_actB int_is_act)
 (* a~:A,a~:B *)
 apply auto
 done
@@ -230,7 +230,7 @@
   [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
 apply auto
 apply (rule Forall_Conc_impl [THEN mp])
-apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
+apply (simp add: intA_is_not_actB int_is_act)
 done
 
 lemma ForallAnBmksch [rule_format (no_asm)]: "!!A B. compatible A B ==>  
@@ -240,7 +240,7 @@
   [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
 apply auto
 apply (rule Forall_Conc_impl [THEN mp])
-apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act)
+apply (simp add: intA_is_not_actB int_is_act)
 done
 
 (* safe-tac makes too many case distinctions with this lemma in the next proof *)
@@ -345,14 +345,12 @@
 apply (rule_tac x = "Takewhile (%a. a:int B) $y @@ a>>y1" in exI)
 apply (rule_tac x = "y2" in exI)
 (* elminate all obligations up to two depending on Conc_assoc *)
-apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act int_is_not_ext FilterConc)
+apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc)
 apply (simp (no_asm) add: Conc_assoc FilterConc)
 done
 
 lemmas reduceA_mksch = conjI [THEN [6] conjI [THEN [5] reduceA_mksch1]]
 
-declare FilterConc [simp del]
-
 lemma reduceB_mksch1 [rule_format]:
 " [| Finite a_s; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>   
  ! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) a_s & 
@@ -393,7 +391,7 @@
 apply (rule_tac x = "Takewhile (%a. a:int A) $x @@ a>>x1" in exI)
 apply (rule_tac x = "x2" in exI)
 (* elminate all obligations up to two depending on Conc_assoc *)
-apply (simp add: ForallPTakewhileQ intA_is_not_actB int_is_act int_is_not_ext FilterConc)
+apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc)
 apply (simp (no_asm) add: Conc_assoc FilterConc)
 done
 
@@ -573,7 +571,7 @@
 apply (rule take_reduction)
 
 (* f A (tw iA) = tw ~eA *)
-apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)
+apply (simp add: int_is_act not_ext_is_int_or_not_act)
 apply (rule refl)
 apply (simp add: int_is_act not_ext_is_int_or_not_act)
 apply (rotate_tac -11)
@@ -582,7 +580,7 @@
 
 (* assumption Forall tr *)
 (* assumption schB *)
-apply (simp add: Forall_Conc ext_and_act)
+apply (simp add: ext_and_act)
 (* assumption schA *)
 apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
 apply assumption
@@ -595,7 +593,7 @@
 (* assumption Forall schA *)
 apply (drule_tac s = "schA" and P = "Forall (%x. x:act A) " in subst)
 apply assumption
-apply (simp add: ForallPTakewhileQ int_is_act)
+apply (simp add: int_is_act)
 
 (* case x:actions(asig_of A) & x: actions(asig_of B) *)
 
@@ -623,7 +621,7 @@
 apply assumption
 
 (* f A (tw iA) = tw ~eA *)
-apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)
+apply (simp add: int_is_act not_ext_is_int_or_not_act)
 
 (* rewrite assumption forall and schB *)
 apply (rotate_tac 13)
@@ -792,7 +790,7 @@
 apply (rule take_reduction)
 
 (* f B (tw iB) = tw ~eB *)
-apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)
+apply (simp add: int_is_act not_ext_is_int_or_not_act)
 apply (rule refl)
 apply (simp add: int_is_act not_ext_is_int_or_not_act)
 apply (rotate_tac -11)
@@ -800,7 +798,7 @@
 (* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
 
 (* assumption schA *)
-apply (simp add: Forall_Conc ext_and_act)
+apply (simp add: ext_and_act)
 (* assumption schB *)
 apply (drule_tac x = "schB" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
 apply assumption
@@ -813,7 +811,7 @@
 (* assumption Forall schB *)
 apply (drule_tac s = "schB" and P = "Forall (%x. x:act B) " in subst)
 apply assumption
-apply (simp add: ForallPTakewhileQ int_is_act)
+apply (simp add: int_is_act)
 
 (* case x:actions(asig_of A) & x: actions(asig_of B) *)
 
@@ -840,7 +838,7 @@
 apply assumption
 
 (* f B (tw iB) = tw ~eB *)
-apply (simp add: FilterPTakewhileQid int_is_act not_ext_is_int_or_not_act)
+apply (simp add: int_is_act not_ext_is_int_or_not_act)
 
 (* rewrite assumption forall and schB *)
 apply (rotate_tac 13)
diff -r 67689d276c70 -r a03462cbf86f src/HOLCF/IOA/meta_theory/LiveIOA.thy
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Thu Feb 18 12:36:09 2010 -0800
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Thu Feb 18 13:29:59 2010 -0800
@@ -43,8 +43,6 @@
                                            ((corresp_ex (fst AM) f exec) |== (snd AM))))"
 
 
-declare split_paired_Ex [simp del]
-
 lemma live_implements_trans:
 "!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |]
       ==> live_implements (A,LA) (C,LC)"
diff -r 67689d276c70 -r a03462cbf86f src/HOLCF/IOA/meta_theory/RefCorrectness.thy
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Thu Feb 18 12:36:09 2010 -0800
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Thu Feb 18 13:29:59 2010 -0800
@@ -165,7 +165,7 @@
 (* --------------------------------------------------- *)
 
 lemma mk_traceConc: "mk_trace C$(ex1 @@ ex2)= (mk_trace C$ex1) @@ (mk_trace C$ex2)"
-apply (simp add: mk_trace_def filter_act_def FilterConc MapConc)
+apply (simp add: mk_trace_def filter_act_def MapConc)
 done
 
 
diff -r 67689d276c70 -r a03462cbf86f src/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Thu Feb 18 12:36:09 2010 -0800
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Thu Feb 18 13:29:59 2010 -0800
@@ -110,7 +110,6 @@
 
 
 declare Finite.intros [simp]
-declare seq.rews [simp]
 
 
 subsection {* recursive equations of operators *}
@@ -361,7 +360,7 @@
 
 lemma scons_inject_eq:
  "[|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)"
-by (simp add: seq.injects)
+by simp
 
 lemma nil_less_is_nil: "nil<<x ==> nil=x"
 apply (rule_tac x="x" in seq.casedist)
@@ -447,7 +446,7 @@
 apply (intro strip)
 apply (erule Finite.cases)
 apply fastsimp
-apply (simp add: seq.injects)
+apply simp
 done
 
 lemma Finite_cons: "a~=UU ==>(Finite (a##x)) = (Finite x)"
@@ -461,7 +460,7 @@
 apply (induct arbitrary: y set: Finite)
 apply (rule_tac x=y in seq.casedist, simp, simp, simp)
 apply (rule_tac x=y in seq.casedist, simp, simp)
-apply (simp add: seq.inverts)
+apply simp
 done
 
 lemma adm_Finite [simp]: "adm Finite"
diff -r 67689d276c70 -r a03462cbf86f src/HOLCF/IOA/meta_theory/TLS.thy
--- a/src/HOLCF/IOA/meta_theory/TLS.thy	Thu Feb 18 12:36:09 2010 -0800
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Thu Feb 18 13:29:59 2010 -0800
@@ -87,7 +87,6 @@
 
 
 lemmas [simp del] = ex_simps all_simps split_paired_Ex
-declare Let_def [simp]
 
 declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
 
diff -r 67689d276c70 -r a03462cbf86f src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Thu Feb 18 12:36:09 2010 -0800
+++ b/src/HOLCF/ex/Stream.thy	Thu Feb 18 13:29:59 2010 -0800
@@ -358,8 +358,7 @@
 by (drule stream_finite_lemma1,auto)
 
 lemma slen_less_1_eq: "(#x < Fin (Suc 0)) = (x = \<bottom>)"
-by (rule stream.casedist [of x], auto simp del: iSuc_Fin
-    simp add: Fin_0 iSuc_Fin[THEN sym] i0_iless_iSuc iSuc_mono)
+by (rule stream.casedist [of x], auto simp add: Fin_0 iSuc_Fin[THEN sym])
 
 lemma slen_empty_eq: "(#x = 0) = (x = \<bottom>)"
 by (rule stream.casedist [of x], auto)