--- 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"
--- 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)
--- 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)
--- 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)
--- 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]
--- 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]
--- 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"
--- 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"
--- 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)
--- 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)"
--- 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
--- 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"
--- 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") *}
--- 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)