src/HOL/TLA/TLA.ML
changeset 4477 b3e5857d8d99
parent 4423 a129b817b58a
child 4651 70dd492a1698
     1.1 --- a/src/HOL/TLA/TLA.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOL/TLA/TLA.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -135,7 +135,7 @@
     1.4  
     1.5  (* ------------------------ STL4 ------------------------------------------- *)
     1.6  qed_goal "STL4" TLA.thy "(F .-> G)  ==> ([]F .-> []G)"
     1.7 -   (fn [prem] => [Auto_tac(),
     1.8 +   (fn [prem] => [Auto_tac,
     1.9  		  rtac ((temp_mp normalT) RS mp) 1,
    1.10  		  REPEAT (ares_tac [prem, necT RS tempD] 1)
    1.11  		 ]);
    1.12 @@ -163,7 +163,7 @@
    1.13  
    1.14  (* ------------------------ STL5 ------------------------------------------- *)
    1.15  qed_goal "STL5" TLA.thy "([]F .& []G) .= ([](F .& G))"
    1.16 -   (fn _ => [Auto_tac(),
    1.17 +   (fn _ => [Auto_tac,
    1.18  	     subgoal_tac "sigma |= [](G .-> (F .& G))" 1,
    1.19  	     etac ((temp_mp normalT) RS mp) 1, atac 1,
    1.20  	     ALLGOALS (fast_tac (temp_cs addSEs [STL4E]))
    1.21 @@ -238,7 +238,7 @@
    1.22  
    1.23  qed_goalw "DmdImpl2" TLA.thy [dmd_def]
    1.24     "!!sigma. [| (sigma |= <>F); (sigma |= [](F .-> G)) |] ==> (sigma |= <>G)"
    1.25 -   (fn _ => [Auto_tac(),
    1.26 +   (fn _ => [Auto_tac,
    1.27  	     etac notE 1,
    1.28  	     merge_box_tac 1,
    1.29  	     fast_tac (temp_cs addSEs [STL4E]) 1
    1.30 @@ -256,7 +256,7 @@
    1.31  (* ------------------------ STL6 ------------------------------------------- *)
    1.32  (* Used in the proof of STL6, but useful in itself. *)
    1.33  qed_goalw "BoxDmdT" TLA.thy [dmd_def] "[]F .& <>G .-> <>([]F .& G)"
    1.34 -  (fn _ => [ Auto_tac(),
    1.35 +  (fn _ => [ Auto_tac,
    1.36               etac dup_boxE 1,
    1.37  	     merge_box_tac 1,
    1.38               etac swap 1,
    1.39 @@ -265,7 +265,7 @@
    1.40  
    1.41  (* weaker than BoxDmd, but more polymorphic (and often just right) *)
    1.42  qed_goalw "BoxDmdT2" TLA.thy [dmd_def] "<>F .& []G .-> <>(F .& G)"
    1.43 -  (fn _ => [ Auto_tac(),
    1.44 +  (fn _ => [ Auto_tac,
    1.45  	     merge_box_tac 1,
    1.46               fast_tac (temp_cs addSEs [notE,STL4E]) 1
    1.47  	   ]);
    1.48 @@ -278,7 +278,7 @@
    1.49  	    etac DmdImplE 1, rtac BoxDmdT 1,
    1.50  	    (* the second subgoal needs commutativity of .&, which complicates the proof *)
    1.51  	    etac DmdImplE 1,
    1.52 -	    Auto_tac(),
    1.53 +	    Auto_tac,
    1.54  	    etac (temp_conjimpE BoxDmdT) 1, atac 1, etac thin_rl 1,
    1.55  	    fast_tac (temp_cs addSEs [DmdImplE]) 1
    1.56  	   ]);
    1.57 @@ -347,10 +347,10 @@
    1.58  section "Further rewrites";
    1.59  
    1.60  qed_goalw "NotBox" TLA.thy [dmd_def] "(.~[]F) .= (<>.~F)"
    1.61 -   (fn _ => [ Auto_tac() ]);
    1.62 +   (fn _ => [ Auto_tac ]);
    1.63  
    1.64  qed_goalw "NotDmd" TLA.thy [dmd_def] "(.~<>F) .= ([].~F)"
    1.65 -   (fn _ => [ Auto_tac () ]);
    1.66 +   (fn _ => [ Auto_tac ]);
    1.67  
    1.68  (* These are not by default included in temp_css, because they could be harmful,
    1.69     e.g. []F .& .~[]F becomes []F .& <>.~F !! *)
    1.70 @@ -363,7 +363,7 @@
    1.71                rtac ccontr 1,
    1.72                subgoal_tac "sigma |= <>[][]F .& <>[].~[]F" 1,
    1.73                etac thin_rl 1,
    1.74 -              Auto_tac(),
    1.75 +              Auto_tac,
    1.76  	      etac (temp_conjimpE STL6) 1, atac 1,
    1.77  	      Asm_full_simp_tac 1,
    1.78  	      ALLGOALS (asm_full_simp_tac (simpset() addsimps more_temp_simps))
    1.79 @@ -382,18 +382,19 @@
    1.80     (fn _ => [ fast_tac (temp_cs addSEs [STL4E]) 1 ]);
    1.81  
    1.82  qed_goal "DBImplBD" TLA.thy "<>[](F::temporal) .-> []<>F"
    1.83 -  (fn _ => [Auto_tac(),
    1.84 +  (fn _ => [Auto_tac,
    1.85  	    rtac ccontr 1,
    1.86 -	    auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6])
    1.87 +	    old_auto_tac (temp_css addsimps2 more_temp_simps 
    1.88 +			           addEs2 [temp_conjimpE STL6])
    1.89  	   ]);
    1.90  
    1.91  (* Although the script is the same, the derivation isn't polymorphic and doesn't
    1.92     work for other types of formulas (uses STL2).
    1.93  *)
    1.94  qed_goal "DBImplBDAct" TLA.thy "<>[](A::action) .-> []<>A"
    1.95 -  (fn _ => [Auto_tac(),
    1.96 +  (fn _ => [Auto_tac,
    1.97  	    rtac ccontr 1,
    1.98 -	    auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6])
    1.99 +	    old_auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6])
   1.100  	   ]);
   1.101  
   1.102  qed_goal "BoxDmdDmdBox" TLA.thy
   1.103 @@ -420,7 +421,7 @@
   1.104  
   1.105  (* Auxiliary lemma allows priming of boxed actions *)
   1.106  qed_goal "BoxPrime" TLA.thy "[]P .-> [](P .& P`)"
   1.107 -  (fn _ => [Auto_tac(),
   1.108 +  (fn _ => [Auto_tac,
   1.109  	    etac dup_boxE 1,
   1.110  	    auto_tac (temp_css addsimps2 [boxact_def]
   1.111  		               addSIs2 [STL2bD_pr] addSEs2 [STL4E])
   1.112 @@ -517,7 +518,7 @@
   1.113  	    ]);
   1.114  
   1.115  qed_goalw "DmdRec" TLA.thy [dmd_def] "(<>$P) .= (Init($P) .| (<>P$))"
   1.116 -   (fn _ => [Auto_tac(),
   1.117 +   (fn _ => [Auto_tac,
   1.118  	     etac notE 1,
   1.119  	     SELECT_GOAL (auto_tac (temp_css addsimps2 (stable_def::Init_simps)
   1.120  				             addIs2 [INV1I] addEs2 [STL4E])) 1,
   1.121 @@ -533,7 +534,7 @@
   1.122  
   1.123  (* The "=>" part of the following is a little intricate. *)
   1.124  qed_goal "InfinitePrime" TLA.thy "([]<>$P) .= ([]<>P$)"
   1.125 -   (fn _ => [Auto_tac(),
   1.126 +   (fn _ => [Auto_tac,
   1.127  	     rtac classical 1,
   1.128  	     rtac (temp_mp DBImplBDAct) 1,
   1.129  	     subgoal_tac "sigma |= <>[]$P" 1,
   1.130 @@ -592,7 +593,7 @@
   1.131  
   1.132  qed_goalw "streett_leadsto" TLA.thy [leadsto]
   1.133     "([]<>P .-> []<>Q) .= (<>(P ~> Q))"
   1.134 -   (fn _ => [Auto_tac(),
   1.135 +   (fn _ => [Auto_tac,
   1.136               asm_full_simp_tac (simpset() addsimps boxact_def::more_temp_simps) 1,
   1.137               SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImplE,STL4E] 
   1.138                                               addsimps2 Init_simps)) 1,
   1.139 @@ -725,26 +726,26 @@
   1.140  \      P .& N .-> $(Enabled(<A>_v)) |]   \
   1.141  \  ==> []N .& WF(A)_v .-> (P ~> Q)"
   1.142     (fn [prem1,prem2,prem3]
   1.143 -             => [auto_tac (temp_css addSDs2 [BoxWFI]),
   1.144 -		 etac STL4Edup 1, atac 1,
   1.145 -		 Auto_tac(),
   1.146 -		 subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
   1.147 -		 auto_tac (temp_css addSDs2 [unless]),
   1.148 -		 etac (temp_conjimpE INV1) 1, atac 1,
   1.149 -		 merge_box_tac 1,
   1.150 -		 rtac STL2D 1,
   1.151 -		 rtac EnsuresInfinite 1, atac 2,
   1.152 -		 SELECT_GOAL (auto_tac (temp_css addsimps2 [WF_alt])) 1,
   1.153 -		 atac 2,
   1.154 -		 subgoal_tac "sigmaa |= [][]$(Enabled(<A>_v))" 1,
   1.155 -		 merge_box_tac 1,
   1.156 -		 SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
   1.157 -		 SELECT_GOAL ((rewtac (temp_rewrite STL3)) THEN
   1.158 -			      (auto_tac (temp_css addSEs2 [STL4E] addSIs2 [action_mp prem3]))) 1,
   1.159 -		 fast_tac (action_cs addSIs [action_mp prem2]) 1,
   1.160 -		 fast_tac (temp_cs addIs [temp_mp DmdPrime]) 1,
   1.161 -		 fast_tac (temp_cs addSEs [STL4E] addSIs [action_mp prem1]) 1
   1.162 -		]);
   1.163 +	 => [auto_tac (temp_css addSDs2 [BoxWFI]),
   1.164 +	     etac STL4Edup 1, atac 1,
   1.165 +	     Auto_tac,
   1.166 +	     subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
   1.167 +	     auto_tac (temp_css addSDs2 [unless]),
   1.168 +	     etac (temp_conjimpE INV1) 1, atac 1,
   1.169 +	     merge_box_tac 1,
   1.170 +	     rtac STL2D 1,
   1.171 +	     rtac EnsuresInfinite 1, atac 2,
   1.172 +	     SELECT_GOAL (old_auto_tac (temp_css addsimps2 [WF_alt])) 1,
   1.173 +	     atac 2,
   1.174 +	     subgoal_tac "sigmaa |= [][]$(Enabled(<A>_v))" 1,
   1.175 +	     merge_box_tac 1,
   1.176 +	     SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
   1.177 +	     SELECT_GOAL ((rewtac (temp_rewrite STL3)) THEN
   1.178 +			  (auto_tac (temp_css addSEs2 [STL4E] addSIs2 [action_mp prem3]))) 1,
   1.179 +	     fast_tac (action_cs addSIs [action_mp prem2]) 1,
   1.180 +	     fast_tac (temp_cs addIs [temp_mp DmdPrime]) 1,
   1.181 +	     fast_tac (temp_cs addSEs [STL4E] addSIs [action_mp prem1]) 1
   1.182 +	    ]);
   1.183  
   1.184  (* Sometimes easier to use; designed for action B rather than state predicate Q *)
   1.185  qed_goalw "WF_leadsto" TLA.thy [leadsto]
   1.186 @@ -755,7 +756,7 @@
   1.187     (fn [prem1,prem2,prem3]
   1.188         => [auto_tac (temp_css addSDs2 [BoxWFI]),
   1.189             etac STL4Edup 1, atac 1,
   1.190 -           Auto_tac(),
   1.191 +           Auto_tac,
   1.192             subgoal_tac "sigmaa |= <><A>_v" 1,
   1.193             SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImpl2,STL4E] addSIs2 [action_mp prem2])) 1,
   1.194             rtac classical 1,
   1.195 @@ -779,14 +780,14 @@
   1.196  		 eres_inst_tac [("F","F")] dup_boxE 1,
   1.197  		 merge_temp_box_tac 1,
   1.198  		 etac STL4Edup 1, atac 1,
   1.199 -		 Auto_tac(),
   1.200 +		 Auto_tac,
   1.201  		 subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
   1.202  		 auto_tac (temp_css addSDs2 [unless]),
   1.203  		 etac (temp_conjimpE INV1) 1, atac 1,
   1.204  		 merge_act_box_tac 1,
   1.205  		 rtac STL2D 1,
   1.206  		 rtac EnsuresInfinite 1, atac 2,
   1.207 -		 SELECT_GOAL (auto_tac (temp_css addsimps2 [SF_alt])) 1,
   1.208 +		 SELECT_GOAL (old_auto_tac (temp_css addsimps2 [SF_alt])) 1,
   1.209  		 atac 2,
   1.210  		 subgoal_tac "sigmaa |= []<>$(Enabled(<A>_v))" 1,
   1.211  		 SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
   1.212 @@ -805,7 +806,7 @@
   1.213  \      [](N .& [.~B]_f) .& WF(A)_f .& []F .& <>[]($(Enabled(<M>_g))) .-> <>[]P |]   \
   1.214  \  ==> []N .& WF(A)_f .& []F .-> WF(M)_g"
   1.215     (fn [prem1,prem2,prem3,prem4]
   1.216 -       => [Auto_tac(),
   1.217 +       => [Auto_tac,
   1.218  	   case_tac "sigma |= <>[]$Enabled(<M>_g)" 1,
   1.219  	   SELECT_GOAL (auto_tac (temp_css addsimps2 [WF_def,dmd_def])) 2,
   1.220  	   case_tac "sigma |= <>[][.~B]_f" 1,
   1.221 @@ -819,7 +820,7 @@
   1.222  	   subgoal_tac "sigma |= <>([]N .& []P .& []<><A>_f)" 1,
   1.223  	   rtac ((temp_unlift DmdBoxDmd) RS iffD1) 1,
   1.224  	   eres_inst_tac [("F","[]N .& []P .& []<><A>_f")] DmdImplE 1,
   1.225 -	   SELECT_GOAL (Auto_tac()) 1,
   1.226 +	   SELECT_GOAL Auto_tac 1,
   1.227  	   dres_inst_tac [("P","P")] (temp_mp BoxPrime) 1,
   1.228  	   merge_act_box_tac 1,
   1.229  	   etac InfImpl 1, atac 1,
   1.230 @@ -827,7 +828,7 @@
   1.231  	   etac BoxDmd 1,
   1.232  	   dres_inst_tac [("F","<><A>_f"),("G","[]P")] BoxDmd 1, atac 1,
   1.233  	   eres_inst_tac [("F","[]<><A>_f .& []P")] DmdImplE 1,
   1.234 -	   SELECT_GOAL (Auto_tac ()) 1,
   1.235 +	   SELECT_GOAL Auto_tac 1,
   1.236  	   rtac (temp_mp (prem3 RS STL4 RS DmdImpl)) 1,
   1.237  	   fast_tac (temp_cs addIs [STL4E,DmdImplE]) 1,
   1.238  	   etac (temp_conjimpE STL6) 1, atac 1,
   1.239 @@ -857,7 +858,7 @@
   1.240  \      [](N .& [.~B]_f) .& SF(A)_f .& []F .& []<>($(Enabled(<M>_g))) .-> <>[]P |]   \
   1.241  \  ==> []N .& SF(A)_f .& []F .-> SF(M)_g"
   1.242     (fn [prem1,prem2,prem3,prem4]
   1.243 -       => [Auto_tac(),
   1.244 +       => [Auto_tac,
   1.245  	   case_tac "sigma |= []<>$Enabled(<M>_g)" 1,
   1.246  	   SELECT_GOAL (auto_tac (temp_css addsimps2 [SF_def,dmd_def])) 2,
   1.247  	   case_tac "sigma |= <>[][.~B]_f" 1,
   1.248 @@ -871,7 +872,7 @@
   1.249  	   subgoal_tac "sigma |= <>([]N .& []P .& []<><A>_f)" 1,
   1.250  	   rtac ((temp_unlift DmdBoxDmd) RS iffD1) 1,
   1.251  	   eres_inst_tac [("F","[]N .& []P .& []<><A>_f")] DmdImplE 1,
   1.252 -	   SELECT_GOAL (Auto_tac()) 1,
   1.253 +	   SELECT_GOAL Auto_tac 1,
   1.254  	   dres_inst_tac [("P","P")] (temp_mp BoxPrime) 1,
   1.255  	   merge_act_box_tac 1,
   1.256  	   etac InfImpl 1, atac 1,
   1.257 @@ -879,7 +880,7 @@
   1.258  	   etac BoxDmd 1,
   1.259  	   dres_inst_tac [("F","<><A>_f"),("G","[]P")] BoxDmd 1, atac 1,
   1.260  	   eres_inst_tac [("F","[]<><A>_f .& []P")] DmdImplE 1,
   1.261 -	   SELECT_GOAL (Auto_tac ()) 1,
   1.262 +	   SELECT_GOAL Auto_tac 1,
   1.263  	   rtac (temp_mp (prem3 RS DmdImpl RS STL4)) 1,
   1.264  	   fast_tac (temp_cs addEs [STL4E,DmdImplE]) 1,
   1.265  	   dtac BoxSFI 1,
   1.266 @@ -915,7 +916,7 @@
   1.267            subgoal_tac "sigma |= []((REX y. #((y,x):r) .& F y) .-> <>G)" 1,
   1.268  	  cut_facts_tac prems 1,
   1.269  	  etac STL4Edup 1, atac 1,
   1.270 -	  Auto_tac(), etac swap 1, atac 1,
   1.271 +	  Auto_tac, etac swap 1, atac 1,
   1.272  	  rtac dup_dmdD 1,
   1.273  	  etac DmdImpl2 1, atac 1,
   1.274  	  subgoal_tac "sigma |= [](RALL y. #((y,x):r) .& F y .-> <>G)" 1,
   1.275 @@ -943,7 +944,7 @@
   1.276  (* If r is well-founded, state function v cannot decrease forever *)
   1.277  qed_goal "wf_not_box_decrease" TLA.thy
   1.278    "!!r. wf r ==> [][ {[v$, $v]} .: #r ]_v .-> <>[][#False]_v"
   1.279 -  (fn _ => [Auto_tac(),
   1.280 +  (fn _ => [Auto_tac,
   1.281              subgoal_tac "ALL x. (sigma |= [](Init($v .= #x) .-> <>[][#False]_v))" 1,
   1.282              etac allE 1,
   1.283              dtac STL2D 1,
   1.284 @@ -968,7 +969,7 @@
   1.285              dres_inst_tac [("P", "$v .= #xa")] (temp_mp BoxPrime) 1,
   1.286              SELECT_GOAL (auto_tac (temp_css addEs2 [STL4E] addsimps2 [square_def])) 1,
   1.287              SELECT_GOAL (auto_tac (temp_css addSIs2 [INV1I] addsimps2 [Init_def])) 1,
   1.288 -            auto_tac (temp_css addsimps2 [square_def] addSIs2 [unless] addSEs2 [STL4E])
   1.289 +            old_auto_tac (temp_css addsimps2 [square_def] addSIs2 [unless] addSEs2 [STL4E])
   1.290             ]);
   1.291  
   1.292  (* "wf ?r  ==>  <>[][{[?v$, $?v]} .: #?r]_?v .-> <>[][#False]_?v" *)
   1.293 @@ -980,14 +981,14 @@
   1.294  *)
   1.295  qed_goal "wf_box_dmd_decrease" TLA.thy
   1.296    "wf r ==> []<>({[v$, $v]} .: #r) .-> []<><.~({[v$, $v]} .: #r)>_v"
   1.297 -  (fn [prem] => [Auto_tac(),
   1.298 +  (fn [prem] => [Auto_tac,
   1.299                   rtac ccontr 1,
   1.300                   asm_full_simp_tac 
   1.301                     (simpset() addsimps ([action_rewrite not_angle] @ more_temp_simps)) 1,
   1.302                   dtac (prem RS (temp_mp wf_not_dmd_box_decrease)) 1,
   1.303                   dtac BoxDmdDmdBox 1, atac 1,
   1.304                   subgoal_tac "sigma |= []<>((#False)::action)" 1,
   1.305 -                 SELECT_GOAL (Auto_tac()) 1,
   1.306 +                 SELECT_GOAL Auto_tac 1,
   1.307                   etac STL4E 1,
   1.308                   rtac DmdImpl 1,
   1.309                   auto_tac (action_css addsimps2 [square_def] addSEs2 [prem RS wf_irrefl])
   1.310 @@ -998,12 +999,12 @@
   1.311  *)
   1.312  qed_goal "nat_box_dmd_decrease" TLA.thy
   1.313    "!!n::nat stfun. []<>(n$ .< $n) .-> []<>($n .< n$)"
   1.314 -  (fn _ => [Auto_tac(),
   1.315 +  (fn _ => [Auto_tac,
   1.316              subgoal_tac "sigma |= []<><.~( {[n$,$n]} .: #less_than)>_n" 1,
   1.317              etac thin_rl 1, etac STL4E 1, rtac DmdImpl 1,
   1.318              SELECT_GOAL (auto_tac (claset(), simpset() addsimps [angle_def])) 1,
   1.319              rtac nat_less_cases 1,
   1.320 -            Auto_tac(),
   1.321 +            Auto_tac,
   1.322              rtac (temp_mp wf_box_dmd_decrease) 1,
   1.323              auto_tac (claset() addSEs [STL4E] addSIs [DmdImpl], simpset())
   1.324             ]);