src/HOL/IMPP/Hoare.thy
changeset 30607 c3d1590debd8
parent 27364 a8672b0e2b15
child 35431 8758fe1fc9f8
     1.1 --- a/src/HOL/IMPP/Hoare.thy	Fri Mar 20 11:26:59 2009 +0100
     1.2 +++ b/src/HOL/IMPP/Hoare.thy	Fri Mar 20 15:24:18 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/IMPP/Hoare.thy
     1.5 -    ID:         $Id$
     1.6      Author:     David von Oheimb
     1.7      Copyright   1999 TUM
     1.8  *)
     1.9 @@ -219,7 +218,7 @@
    1.10  apply           (rule hoare_derivs.conseq, intro strip, tactic "smp_tac 2 1", clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI)
    1.11  prefer 7
    1.12  apply          (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast)
    1.13 -apply         (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) (thms "hoare_derivs.intros")) THEN_ALL_NEW CLASET' fast_tac) *})
    1.14 +apply         (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) (thms "hoare_derivs.intros")) THEN_ALL_NEW (fast_tac @{claset})) *})
    1.15  done
    1.16  
    1.17  lemma weak_Body: "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}"
    1.18 @@ -291,7 +290,7 @@
    1.19     simp_tac @{simpset}, clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
    1.20  apply       (simp_all (no_asm_use) add: triple_valid_def2)
    1.21  apply       (intro strip, tactic "smp_tac 2 1", blast) (* conseq *)
    1.22 -apply      (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *}) (* Skip, Ass, Local *)
    1.23 +apply      (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *}) (* Skip, Ass, Local *)
    1.24  prefer 3 apply   (force) (* Call *)
    1.25  apply  (erule_tac [2] evaln_elim_cases) (* If *)
    1.26  apply   blast+
    1.27 @@ -336,17 +335,17 @@
    1.28  lemma MGF_lemma1 [rule_format (no_asm)]: "state_not_singleton ==>  
    1.29    !pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}"
    1.30  apply (induct_tac c)
    1.31 -apply        (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *})
    1.32 +apply        (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
    1.33  prefer 7 apply        (fast intro: domI)
    1.34  apply (erule_tac [6] MGT_alternD)
    1.35  apply       (unfold MGT_def)
    1.36  apply       (drule_tac [7] bspec, erule_tac [7] domI)
    1.37 -apply       (rule_tac [7] escape, tactic {* CLASIMPSET' clarsimp_tac 7 *},
    1.38 +apply       (rule_tac [7] escape, tactic {* clarsimp_tac @{clasimpset} 7 *},
    1.39    rule_tac [7] P1 = "%Z' s. s= (setlocs Z newlocs) [Loc Arg ::= fun Z]" in hoare_derivs.Call [THEN conseq1], erule_tac [7] conseq12)
    1.40  apply        (erule_tac [!] thin_rl)
    1.41  apply (rule hoare_derivs.Skip [THEN conseq2])
    1.42  apply (rule_tac [2] hoare_derivs.Ass [THEN conseq1])
    1.43 -apply        (rule_tac [3] escape, tactic {* CLASIMPSET' clarsimp_tac 3 *},
    1.44 +apply        (rule_tac [3] escape, tactic {* clarsimp_tac @{clasimpset} 3 *},
    1.45    rule_tac [3] P1 = "%Z' s. s= (Z[Loc loc::=fun Z])" in hoare_derivs.Local [THEN conseq1],
    1.46    erule_tac [3] conseq12)
    1.47  apply         (erule_tac [5] hoare_derivs.Comp, erule_tac [5] conseq12)
    1.48 @@ -365,7 +364,7 @@
    1.49    shows "finite U ==> uG = mgt_call`U ==>  
    1.50    !G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})"
    1.51  apply (induct_tac n)
    1.52 -apply  (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *})
    1.53 +apply  (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
    1.54  apply  (subgoal_tac "G = mgt_call ` U")
    1.55  prefer 2
    1.56  apply   (simp add: card_seteq finite_imageI)