replaced program_defs_ref by proper context data (via attribute "program");
authorwenzelm
Sun Jul 29 14:30:07 2007 +0200 (2007-07-29)
changeset 24051896fb015079c
parent 24050 248da5f0e735
child 24052 90dd4df2c7c3
replaced program_defs_ref by proper context data (via attribute "program");
src/ZF/UNITY/AllocImpl.thy
src/ZF/UNITY/ClientImpl.thy
src/ZF/UNITY/Constrains.thy
src/ZF/UNITY/Mutex.thy
src/ZF/UNITY/SubstAx.thy
     1.1 --- a/src/ZF/UNITY/AllocImpl.thy	Sun Jul 29 14:30:06 2007 +0200
     1.2 +++ b/src/ZF/UNITY/AllocImpl.thy	Sun Jul 29 14:30:07 2007 +0200
     1.3 @@ -69,10 +69,7 @@
     1.4  
     1.5  declare alloc_prog_def [THEN def_prg_Init, simp]
     1.6  declare alloc_prog_def [THEN def_prg_AllowedActs, simp]
     1.7 -ML
     1.8 -{*
     1.9 -program_defs_ref := [thm"alloc_prog_def"]
    1.10 -*}
    1.11 +declare alloc_prog_def [program]
    1.12  
    1.13  declare  alloc_giv_act_def [THEN def_act_simp, simp]
    1.14  declare  alloc_rel_act_def [THEN def_act_simp, simp]
     2.1 --- a/src/ZF/UNITY/ClientImpl.thy	Sun Jul 29 14:30:06 2007 +0200
     2.2 +++ b/src/ZF/UNITY/ClientImpl.thy	Sun Jul 29 14:30:07 2007 +0200
     2.3 @@ -96,10 +96,7 @@
     2.4  
     2.5  declare client_prog_def [THEN def_prg_Init, simp]
     2.6  declare client_prog_def [THEN def_prg_AllowedActs, simp]
     2.7 -ML
     2.8 -{*
     2.9 -program_defs_ref := [thm"client_prog_def"]
    2.10 -*}
    2.11 +declare client_prog_def [program]
    2.12  
    2.13  declare  client_rel_act_def [THEN def_act_simp, simp]
    2.14  declare  client_tok_act_def [THEN def_act_simp, simp]
     3.1 --- a/src/ZF/UNITY/Constrains.thy	Sun Jul 29 14:30:06 2007 +0200
     3.2 +++ b/src/ZF/UNITY/Constrains.thy	Sun Jul 29 14:30:07 2007 +0200
     3.3 @@ -533,7 +533,7 @@
     3.4  val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I);
     3.5  
     3.6  (*To allow expansion of the program's definition when appropriate*)
     3.7 -val program_defs_ref = ref ([]: thm list);
     3.8 +structure ProgramDefs = NamedThmsFun(val name = "program" val description = "program definitions");
     3.9  
    3.10  (*proves "co" properties when the program is specified*)
    3.11  
    3.12 @@ -549,7 +549,7 @@
    3.13                (* Three subgoals *)
    3.14                rewrite_goal_tac [st_set_def] 3,
    3.15                REPEAT (force_tac css 2),
    3.16 -              full_simp_tac (ss addsimps !program_defs_ref) 1,
    3.17 +              full_simp_tac (ss addsimps (ProgramDefs.get ctxt)) 1,
    3.18                ALLGOALS (clarify_tac cs),
    3.19                REPEAT (FIRSTGOAL (etac disjE)),
    3.20                ALLGOALS (clarify_tac cs),
    3.21 @@ -564,6 +564,8 @@
    3.22      rtac AlwaysI i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i;
    3.23  *}
    3.24  
    3.25 +setup ProgramDefs.setup
    3.26 +
    3.27  method_setup safety = {*
    3.28    Method.ctxt_args (fn ctxt =>
    3.29      Method.SIMPLE_METHOD' (constrains_tac ctxt)) *}
     4.1 --- a/src/ZF/UNITY/Mutex.thy	Sun Jul 29 14:30:06 2007 +0200
     4.2 +++ b/src/ZF/UNITY/Mutex.thy	Sun Jul 29 14:30:07 2007 +0200
     4.3 @@ -149,10 +149,7 @@
     4.4  
     4.5  
     4.6  declare Mutex_def [THEN def_prg_Init, simp]
     4.7 -ML
     4.8 -{*
     4.9 -program_defs_ref := [thm"Mutex_def"]
    4.10 -*}
    4.11 +declare Mutex_def [program]
    4.12  
    4.13  declare  U0_def [THEN def_act_simp, simp]
    4.14  declare  U1_def [THEN def_act_simp, simp]
     5.1 --- a/src/ZF/UNITY/SubstAx.thy	Sun Jul 29 14:30:06 2007 +0200
     5.2 +++ b/src/ZF/UNITY/SubstAx.thy	Sun Jul 29 14:30:07 2007 +0200
     5.3 @@ -412,7 +412,7 @@
     5.4                    REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
     5.5                                      EnsuresI, ensuresI] 1),
     5.6                (*now there are two subgoals: co & transient*)
     5.7 -              simp_tac (ss addsimps !program_defs_ref) 2,
     5.8 +              simp_tac (ss addsimps (ProgramDefs.get ctxt)) 2,
     5.9                res_inst_tac [("act", sact)] transientI 2,
    5.10                   (*simplify the command's domain*)
    5.11                simp_tac (ss addsimps [domain_def]) 3,