remove old uses of 'simp_tac HOLCF_ss'
authorhuffman
Sat Oct 16 17:09:57 2010 -0700 (2010-10-16)
changeset 400289ee4e0ab2964
parent 40027 98f2d8280eb4
child 40029 57e7f651fc70
remove old uses of 'simp_tac HOLCF_ss'
src/HOLCF/ex/Focus_ex.thy
src/HOLCF/ex/Hoare.thy
src/HOLCF/ex/Loop.thy
     1.1 --- a/src/HOLCF/ex/Focus_ex.thy	Sat Oct 16 16:39:06 2010 -0700
     1.2 +++ b/src/HOLCF/ex/Focus_ex.thy	Sat Oct 16 17:09:57 2010 -0700
     1.3 @@ -160,9 +160,9 @@
     1.4  apply (rule_tac [2] conjI)
     1.5  prefer 3 apply (assumption)
     1.6  apply (drule sym)
     1.7 -apply (tactic "asm_simp_tac HOLCF_ss 1")
     1.8 +apply (simp)
     1.9  apply (drule sym)
    1.10 -apply (tactic "asm_simp_tac HOLCF_ss 1")
    1.11 +apply (simp)
    1.12  apply (erule exE)
    1.13  apply (rule_tac x = "f" in exI)
    1.14  apply (erule conjE)+
    1.15 @@ -189,7 +189,7 @@
    1.16  apply (intro strip)
    1.17  apply (rule_tac x = "fix$ (LAM k. snd (f$(x,k)))" in exI)
    1.18  apply (rule conjI)
    1.19 - apply (tactic "asm_simp_tac HOLCF_ss 1")
    1.20 + apply (simp)
    1.21   apply (rule prod_eqI, simp, simp)
    1.22   apply (rule trans)
    1.23    apply (rule fix_eq)
    1.24 @@ -220,9 +220,6 @@
    1.25  apply (subgoal_tac "! w y. f$(x, w) = (y, w) --> z << w")
    1.26  apply (rule fix_eqI)
    1.27  apply simp
    1.28 -(*apply (rule allI)*)
    1.29 -(*apply (tactic "simp_tac HOLCF_ss 1")*)
    1.30 -(*apply (intro strip)*)
    1.31  apply (subgoal_tac "f$(x, za) = (fst (f$(x,za)) ,za)")
    1.32  apply fast
    1.33  apply (rule prod_eqI, simp, simp)
     2.1 --- a/src/HOLCF/ex/Hoare.thy	Sat Oct 16 16:39:06 2010 -0700
     2.2 +++ b/src/HOLCF/ex/Hoare.thy	Sat Oct 16 17:09:57 2010 -0700
     2.3 @@ -188,7 +188,7 @@
     2.4  apply assumption
     2.5  apply assumption
     2.6  apply (simp (no_asm))
     2.7 -apply (tactic "simp_tac HOLCF_ss 1")
     2.8 +apply (simp (no_asm))
     2.9  apply (rule trans)
    2.10  apply (rule p_def3)
    2.11  apply (simp (no_asm) del: iterate_Suc add: iterate_Suc [symmetric])
    2.12 @@ -222,7 +222,7 @@
    2.13  apply assumption
    2.14  apply assumption
    2.15  apply (simp (no_asm))
    2.16 -apply (tactic "asm_simp_tac HOLCF_ss 1")
    2.17 +apply (simp)
    2.18  apply (rule trans)
    2.19  apply (rule p_def3)
    2.20  apply simp
    2.21 @@ -238,7 +238,7 @@
    2.22  apply (rule allI)
    2.23  apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
    2.24  apply (erule spec)
    2.25 -apply (tactic "asm_simp_tac HOLCF_ss 1")
    2.26 +apply (simp)
    2.27  apply (rule iterate_Suc [THEN subst])
    2.28  apply (erule spec)
    2.29  done
    2.30 @@ -258,7 +258,7 @@
    2.31  apply (simp (no_asm))
    2.32  apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
    2.33  apply (erule spec)
    2.34 -apply (tactic "asm_simp_tac HOLCF_ss 1")
    2.35 +apply (simp)
    2.36  apply (rule iterate_Suc [THEN subst])
    2.37  apply (erule spec)
    2.38  done
    2.39 @@ -283,7 +283,7 @@
    2.40  apply (simp (no_asm))
    2.41  apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$ (x::'a))" in ssubst)
    2.42  apply (erule spec)
    2.43 -apply (tactic "asm_simp_tac HOLCF_ss 1")
    2.44 +apply (simp)
    2.45  apply (rule iterate_Suc [THEN subst])
    2.46  apply (erule spec)
    2.47  done
    2.48 @@ -338,7 +338,7 @@
    2.49  apply (intro strip)
    2.50  apply (erule conjE)
    2.51  apply (subst q_def3)
    2.52 -apply (tactic "asm_simp_tac HOLCF_ss 1")
    2.53 +apply (simp)
    2.54  apply hypsubst
    2.55  apply (simp (no_asm))
    2.56  apply (intro strip)
    2.57 @@ -354,10 +354,10 @@
    2.58  apply assumption
    2.59  apply assumption
    2.60  apply (simp (no_asm))
    2.61 -apply (tactic "asm_simp_tac HOLCF_ss 1")
    2.62 +apply (simp)
    2.63  apply (rule trans)
    2.64  apply (rule q_def3)
    2.65 -apply (tactic "asm_simp_tac HOLCF_ss 1")
    2.66 +apply (simp)
    2.67  done
    2.68  
    2.69  (* ------- (ALL k. b1$(iterate k$g$x)=TT) ==> q o p = q   ----- *)
     3.1 --- a/src/HOLCF/ex/Loop.thy	Sat Oct 16 16:39:06 2010 -0700
     3.2 +++ b/src/HOLCF/ex/Loop.thy	Sat Oct 16 17:09:57 2010 -0700
     3.3 @@ -104,12 +104,11 @@
     3.4  apply (simp (no_asm) add: step_def2)
     3.5  apply (rule_tac p = "b$ (iterate n$ (step$b$g) $x) " in trE)
     3.6  apply (erule notE)
     3.7 -apply (tactic {* asm_simp_tac (HOLCF_ss addsimps [@{thm step_def2}]) 1 *})
     3.8 -apply (tactic "asm_simp_tac HOLCF_ss 1")
     3.9 +apply (simp add: step_def2)
    3.10 +apply (simp (no_asm_simp))
    3.11  apply (rule mp)
    3.12  apply (erule spec)
    3.13 -apply (tactic {* asm_simp_tac (HOLCF_ss delsimps [@{thm iterate_Suc}]
    3.14 -  addsimps [@{thm loop_lemma2}]) 1 *})
    3.15 +apply (simp (no_asm_simp) del: iterate_Suc add: loop_lemma2)
    3.16  apply (rule_tac s = "iterate (Suc n) $ (step$b$g) $x"
    3.17    and t = "g$ (iterate n$ (step$b$g) $x) " in ssubst)
    3.18  prefer 2 apply (assumption)