src/HOL/TLA/TLA.ML
changeset 4089 96fba19bcbe2
parent 3807 82a99b090d9d
child 4423 a129b817b58a
     1.1 --- a/src/HOL/TLA/TLA.ML	Mon Nov 03 12:12:10 1997 +0100
     1.2 +++ b/src/HOL/TLA/TLA.ML	Mon Nov 03 12:13:18 1997 +0100
     1.3 @@ -47,7 +47,7 @@
     1.4  AddDs [tempD];
     1.5  
     1.6  val temp_cs = action_cs addSIs [tempI] addDs [tempD];
     1.7 -val temp_css = (temp_cs,!simpset);
     1.8 +val temp_css = (temp_cs,simpset());
     1.9  
    1.10  (* ========================================================================= *)
    1.11  section "Init";
    1.12 @@ -366,7 +366,7 @@
    1.13                Auto_tac(),
    1.14  	      etac (temp_conjimpE STL6) 1, atac 1,
    1.15  	      Asm_full_simp_tac 1,
    1.16 -	      ALLGOALS (asm_full_simp_tac (!simpset addsimps more_temp_simps))
    1.17 +	      ALLGOALS (asm_full_simp_tac (simpset() addsimps more_temp_simps))
    1.18  	    ]);
    1.19  
    1.20  qed_goalw "DmdBoxDmd" TLA.thy [dmd_def] "(<>[]<>F) .= ([]<>F)"
    1.21 @@ -494,13 +494,13 @@
    1.22  
    1.23  fun auto_inv_tac ss =
    1.24    SELECT_GOAL
    1.25 -    ((inv_tac (!claset,ss) 1) THEN
    1.26 +    ((inv_tac (claset(),ss) 1) THEN
    1.27       (TRYALL (action_simp_tac (ss addsimps [Init_def,square_def]) [] [])));
    1.28  
    1.29  
    1.30  qed_goalw "unless" TLA.thy [dmd_def]
    1.31     "!!sigma. (sigma |= [](P .-> P` .| Q`)) ==> (sigma |= stable P .| <>Q`)"
    1.32 -   (fn _ => [action_simp_tac (!simpset) [disjCI] [] 1,
    1.33 +   (fn _ => [action_simp_tac (simpset()) [disjCI] [] 1,
    1.34  	     merge_box_tac 1,
    1.35  	     fast_tac (temp_cs addSEs [Stable]) 1
    1.36  	    ]);
    1.37 @@ -593,12 +593,12 @@
    1.38  qed_goalw "streett_leadsto" TLA.thy [leadsto]
    1.39     "([]<>P .-> []<>Q) .= (<>(P ~> Q))"
    1.40     (fn _ => [Auto_tac(),
    1.41 -             asm_full_simp_tac (!simpset addsimps boxact_def::more_temp_simps) 1,
    1.42 +             asm_full_simp_tac (simpset() addsimps boxact_def::more_temp_simps) 1,
    1.43               SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImplE,STL4E] 
    1.44                                               addsimps2 Init_simps)) 1,
    1.45               SELECT_GOAL (auto_tac (temp_css addSIs2 [ImplDmdD] addSEs2 [STL4E])) 1,
    1.46               subgoal_tac "sigma |= []<><>Q" 1,
    1.47 -             asm_full_simp_tac (!simpset addsimps more_temp_simps) 1,
    1.48 +             asm_full_simp_tac (simpset() addsimps more_temp_simps) 1,
    1.49               rewtac (temp_rewrite DmdAct),
    1.50               dtac BoxDmdDmdBox 1, atac 1,
    1.51               auto_tac (temp_css addSEs2 [DmdImplE,STL4E])
    1.52 @@ -683,7 +683,7 @@
    1.53  	     auto_tac (temp_css addSEs2 [STL4E]),
    1.54  	     rewtac (temp_rewrite DmdAct),
    1.55  	     subgoal_tac "sigmaa |= <><> Init H" 1,
    1.56 -	     asm_full_simp_tac (!simpset addsimps more_temp_simps) 1,
    1.57 +	     asm_full_simp_tac (simpset() addsimps more_temp_simps) 1,
    1.58  	     fast_tac (temp_cs addSEs [DmdImpl2]) 1
    1.59  	    ]);
    1.60  
    1.61 @@ -810,7 +810,7 @@
    1.62  	   SELECT_GOAL (auto_tac (temp_css addsimps2 [WF_def,dmd_def])) 2,
    1.63  	   case_tac "sigma |= <>[][.~B]_f" 1,
    1.64  	   subgoal_tac "sigma |= <>[]P" 1,
    1.65 -	   asm_full_simp_tac (!simpset addsimps [WF_def]) 1,
    1.66 +	   asm_full_simp_tac (simpset() addsimps [WF_def]) 1,
    1.67  	   rtac (temp_mp (prem1 RS DmdImpl RS STL4)) 1,
    1.68  	   eres_inst_tac [("V","sigma |= <>[][.~B]_f")] thin_rl 1,
    1.69  	   etac (temp_conjimpE STL6) 1, atac 1,
    1.70 @@ -844,10 +844,10 @@
    1.71  	   SELECT_GOAL
    1.72  	     (auto_tac (temp_css addsimps2 [symmetric(temp_rewrite STL5), temp_rewrite STL3]
    1.73  		                 addIs2 [(temp_unlift WF_Box) RS iffD1, temp_mp ImplDmd])) 1,
    1.74 -	   asm_full_simp_tac (!simpset addsimps (WF_def::more_temp_simps)) 1,
    1.75 +	   asm_full_simp_tac (simpset() addsimps (WF_def::more_temp_simps)) 1,
    1.76  	   etac InfImpl 1, atac 1,
    1.77  	   SELECT_GOAL (auto_tac (temp_css addSIs2 [action_mp prem1])) 1,
    1.78 -	   ALLGOALS (asm_full_simp_tac (!simpset addsimps [square_def,angle_def]))
    1.79 +	   ALLGOALS (asm_full_simp_tac (simpset() addsimps [square_def,angle_def]))
    1.80  	  ]);
    1.81  
    1.82  qed_goal "SF2" TLA.thy
    1.83 @@ -862,7 +862,7 @@
    1.84  	   SELECT_GOAL (auto_tac (temp_css addsimps2 [SF_def,dmd_def])) 2,
    1.85  	   case_tac "sigma |= <>[][.~B]_f" 1,
    1.86  	   subgoal_tac "sigma |= <>[]P" 1,
    1.87 -	   asm_full_simp_tac (!simpset addsimps [SF_def]) 1,
    1.88 +	   asm_full_simp_tac (simpset() addsimps [SF_def]) 1,
    1.89  	   rtac (temp_mp (prem1 RS DmdImpl RS STL4)) 1,
    1.90  	   eres_inst_tac [("V","sigma |= <>[][.~B]_f")] thin_rl 1,
    1.91  	   dtac BoxDmdDmdBox 1, atac 1,
    1.92 @@ -894,10 +894,10 @@
    1.93  	     (auto_tac (temp_css addsimps2 [symmetric(temp_rewrite STL5), temp_rewrite STL3]
    1.94  		                 addIs2 [(temp_unlift WF_Box) RS iffD1, temp_mp ImplDmd]
    1.95  			         addSEs2 [DmdImplE])) 1,
    1.96 -	   asm_full_simp_tac (!simpset addsimps (SF_def::more_temp_simps)) 1,
    1.97 +	   asm_full_simp_tac (simpset() addsimps (SF_def::more_temp_simps)) 1,
    1.98  	   eres_inst_tac [("F",".~ [.~ B]_f")] InfImpl 1, atac 1,
    1.99  	   SELECT_GOAL (auto_tac (temp_css addSIs2 [action_mp prem1])) 1,
   1.100 -	   ALLGOALS (asm_full_simp_tac (!simpset addsimps [square_def,angle_def]))
   1.101 +	   ALLGOALS (asm_full_simp_tac (simpset() addsimps [square_def,angle_def]))
   1.102  	  ]);
   1.103  
   1.104  (* ------------------------------------------------------------------------- *)
   1.105 @@ -951,7 +951,7 @@
   1.106              etac wf_dmd 1,
   1.107              etac dup_boxE 1,
   1.108              etac STL4E 1,
   1.109 -            action_simp_tac (!simpset addsimps [con_abs]) [tempI] [] 1,
   1.110 +            action_simp_tac (simpset() addsimps [con_abs]) [tempI] [] 1,
   1.111              case_tac "sigma |= <>[][#False]_v" 1,
   1.112              ALLGOALS Asm_full_simp_tac,
   1.113              rewrite_goals_tac more_temp_simps,
   1.114 @@ -983,7 +983,7 @@
   1.115    (fn [prem] => [Auto_tac(),
   1.116                   rtac ccontr 1,
   1.117                   asm_full_simp_tac 
   1.118 -                   (!simpset addsimps ([action_rewrite not_angle] @ more_temp_simps)) 1,
   1.119 +                   (simpset() addsimps ([action_rewrite not_angle] @ more_temp_simps)) 1,
   1.120                   dtac (prem RS (temp_mp wf_not_dmd_box_decrease)) 1,
   1.121                   dtac BoxDmdDmdBox 1, atac 1,
   1.122                   subgoal_tac "sigma |= []<>((#False)::action)" 1,
   1.123 @@ -1001,11 +1001,11 @@
   1.124    (fn _ => [Auto_tac(),
   1.125              subgoal_tac "sigma |= []<><.~( {[n$,$n]} .: #less_than)>_n" 1,
   1.126              etac thin_rl 1, etac STL4E 1, rtac DmdImpl 1,
   1.127 -            SELECT_GOAL (auto_tac (!claset, !simpset addsimps [angle_def])) 1,
   1.128 +            SELECT_GOAL (auto_tac (claset(), simpset() addsimps [angle_def])) 1,
   1.129              rtac nat_less_cases 1,
   1.130              Auto_tac(),
   1.131              rtac (temp_mp wf_box_dmd_decrease) 1,
   1.132 -            auto_tac (!claset addSEs [STL4E] addSIs [DmdImpl], !simpset)
   1.133 +            auto_tac (claset() addSEs [STL4E] addSIs [DmdImpl], simpset())
   1.134             ]);
   1.135  
   1.136  (* ------------------------------------------------------------------------- *)