src/HOL/TLA/TLA.ML

 bind_thm("dup_dmdD", (temp_unlift DmdDmd) RS iffD1);
 
 
 (* ------------------------ STL4 ------------------------------------------- *)
 qed_goal "STL4" TLA.thy "(F .-> G)  ==> ([]F .-> []G)"
-   (fn [prem] => [Auto_tac(),
+   (fn [prem] => [Auto_tac,
 		  rtac ((temp_mp normalT) RS mp) 1,
 		  REPEAT (ares_tac [prem, necT RS tempD] 1)
 		 ]);
 
 (* A more practical variant as an (unlifted) elimination rule *)

    (fn prems => [ REPEAT (resolve_tac (prems @ [temp_mp DmdImpl]) 1) ]);
 
 
 (* ------------------------ STL5 ------------------------------------------- *)
 qed_goal "STL5" TLA.thy "([]F .& []G) .= ([](F .& G))"
-   (fn _ => [Auto_tac(),
+   (fn _ => [Auto_tac,
 	     subgoal_tac "sigma |= [](G .-> (F .& G))" 1,
 	     etac ((temp_mp normalT) RS mp) 1, atac 1,
 	     ALLGOALS (fast_tac (temp_cs addSEs [STL4E]))
 	    ]);
 (* rewrite rule to split conjunctions under boxes *)

 	     atac 1
 	    ]);
 
 qed_goalw "DmdImpl2" TLA.thy [dmd_def]
    "!!sigma. [| (sigma |= <>F); (sigma |= [](F .-> G)) |] ==> (sigma |= <>G)"
-   (fn _ => [Auto_tac(),
+   (fn _ => [Auto_tac,
 	     etac notE 1,
 	     merge_box_tac 1,
 	     fast_tac (temp_cs addSEs [STL4E]) 1
 	    ]);
 

 	  ]);
 
 (* ------------------------ STL6 ------------------------------------------- *)
 (* Used in the proof of STL6, but useful in itself. *)
 qed_goalw "BoxDmdT" TLA.thy [dmd_def] "[]F .& <>G .-> <>([]F .& G)"
-  (fn _ => [ Auto_tac(),
+  (fn _ => [ Auto_tac,
              etac dup_boxE 1,
 	     merge_box_tac 1,
              etac swap 1,
              fast_tac (temp_cs addSEs [STL4E]) 1 ]);
 bind_thm("BoxDmd", temp_conjmp BoxDmdT);
 
 (* weaker than BoxDmd, but more polymorphic (and often just right) *)
 qed_goalw "BoxDmdT2" TLA.thy [dmd_def] "<>F .& []G .-> <>(F .& G)"
-  (fn _ => [ Auto_tac(),
+  (fn _ => [ Auto_tac,
 	     merge_box_tac 1,
              fast_tac (temp_cs addSEs [notE,STL4E]) 1
 	   ]);
 
 qed_goal "STL6" TLA.thy "<>[]F .& <>[]G .-> <>[](F .& G)"

 	    rtac ((temp_unlift DmdDmd) RS iffD1) 1,
 	    etac disjE 1,
 	    etac DmdImplE 1, rtac BoxDmdT 1,
 	    (* the second subgoal needs commutativity of .&, which complicates the proof *)
 	    etac DmdImplE 1,
-	    Auto_tac(),
+	    Auto_tac,
 	    etac (temp_conjimpE BoxDmdT) 1, atac 1, etac thin_rl 1,
 	    fast_tac (temp_cs addSEs [DmdImplE]) 1
 	   ]);
 
 

 
 (* ------------------------ Further rewrites ----------------------------------------- *)
 section "Further rewrites";
 
 qed_goalw "NotBox" TLA.thy [dmd_def] "(.~[]F) .= (<>.~F)"
-   (fn _ => [ Auto_tac() ]);
+   (fn _ => [ Auto_tac ]);
 
 qed_goalw "NotDmd" TLA.thy [dmd_def] "(.~<>F) .= ([].~F)"
-   (fn _ => [ Auto_tac () ]);
+   (fn _ => [ Auto_tac ]);
 
 (* These are not by default included in temp_css, because they could be harmful,
    e.g. []F .& .~[]F becomes []F .& <>.~F !! *)
 val more_temp_simps =  (map temp_rewrite [STL3, DmdDmd, NotBox, NotDmd])
                        @ (map (fn th => (temp_unlift th) RS eq_reflection)

 qed_goal "BoxDmdBox" TLA.thy "([]<>[]F) .= (<>[]F)"
    (fn _ => [ auto_tac (temp_css addSDs2 [STL2D]),
               rtac ccontr 1,
               subgoal_tac "sigma |= <>[][]F .& <>[].~[]F" 1,
               etac thin_rl 1,
-              Auto_tac(),
+              Auto_tac,
 	      etac (temp_conjimpE STL6) 1, atac 1,
 	      Asm_full_simp_tac 1,
 	      ALLGOALS (asm_full_simp_tac (simpset() addsimps more_temp_simps))
 	    ]);
 

 qed_goal "BoxOr" TLA.thy 
    "!!sigma. [| (sigma |= []F .| []G) |] ==> (sigma |= [](F .| G))"
    (fn _ => [ fast_tac (temp_cs addSEs [STL4E]) 1 ]);
 
 qed_goal "DBImplBD" TLA.thy "<>[](F::temporal) .-> []<>F"
-  (fn _ => [Auto_tac(),
+  (fn _ => [Auto_tac,
 	    rtac ccontr 1,
-	    auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6])
+	    old_auto_tac (temp_css addsimps2 more_temp_simps 
+			           addEs2 [temp_conjimpE STL6])
 	   ]);
 
 (* Although the script is the same, the derivation isn't polymorphic and doesn't
    work for other types of formulas (uses STL2).
 *)
 qed_goal "DBImplBDAct" TLA.thy "<>[](A::action) .-> []<>A"
-  (fn _ => [Auto_tac(),
+  (fn _ => [Auto_tac,
 	    rtac ccontr 1,
-	    auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6])
+	    old_auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6])
 	   ]);
 
 qed_goal "BoxDmdDmdBox" TLA.thy
    "!!sigma. [| (sigma |= []<>F); (sigma |= <>[]G) |] ==> (sigma |= []<>(F .& G))"
    (fn _ => [rtac ccontr 1,

   (fn _ => [rewrite_goals_tac Init_simps,
 	    fast_tac (temp_cs addSIs [temp_mp primeI, STL2bD]) 1]);
 
 (* Auxiliary lemma allows priming of boxed actions *)
 qed_goal "BoxPrime" TLA.thy "[]P .-> [](P .& P`)"
-  (fn _ => [Auto_tac(),
+  (fn _ => [Auto_tac,
 	    etac dup_boxE 1,
 	    auto_tac (temp_css addsimps2 [boxact_def]
 		               addSIs2 [STL2bD_pr] addSEs2 [STL4E])
 	   ]);
 

 	     fast_tac (temp_cs addSEs [TLA2E]) 1,
 	     auto_tac (temp_css addsimps2 [stable_def] addSEs2 [INV1I,STL4E])
 	    ]);
 
 qed_goalw "DmdRec" TLA.thy [dmd_def] "(<>$P) .= (Init($P) .| (<>P$))"
-   (fn _ => [Auto_tac(),
+   (fn _ => [Auto_tac,
 	     etac notE 1,
 	     SELECT_GOAL (auto_tac (temp_css addsimps2 (stable_def::Init_simps)
 				             addIs2 [INV1I] addEs2 [STL4E])) 1,
 	     SELECT_GOAL (auto_tac (temp_css addsimps2 Init_simps addSDs2 [STL2bD])) 1,
 	     fast_tac (temp_cs addSEs [notE,TLA2E]) 1

 	     SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1
 	    ]);
 
 (* The "=>" part of the following is a little intricate. *)
 qed_goal "InfinitePrime" TLA.thy "([]<>$P) .= ([]<>P$)"
-   (fn _ => [Auto_tac(),
+   (fn _ => [Auto_tac,
 	     rtac classical 1,
 	     rtac (temp_mp DBImplBDAct) 1,
 	     subgoal_tac "sigma |= <>[]$P" 1,
 	     fast_tac (temp_cs addSEs [DmdImplE,TLA2E]) 1,
 	     subgoal_tac "sigma |= <>[](<>$P .& [].~P$)" 1,

    "!!sigma. [| (sigma |= Init P); (sigma |= P ~> Q) |] ==> (sigma |= <>Q)"
    (fn _ => [ fast_tac (temp_cs addSDs [temp_mp STL2]) 1 ]);
 
 qed_goalw "streett_leadsto" TLA.thy [leadsto]
    "([]<>P .-> []<>Q) .= (<>(P ~> Q))"
-   (fn _ => [Auto_tac(),
+   (fn _ => [Auto_tac,
              asm_full_simp_tac (simpset() addsimps boxact_def::more_temp_simps) 1,
              SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImplE,STL4E] 
                                              addsimps2 Init_simps)) 1,
              SELECT_GOAL (auto_tac (temp_css addSIs2 [ImplDmdD] addSEs2 [STL4E])) 1,
              subgoal_tac "sigma |= []<><>Q" 1,

    "[| P .& N  .-> P` .| Q`;   \
 \      P .& N .& <A>_v .-> Q`;   \
 \      P .& N .-> $(Enabled(<A>_v)) |]   \
 \  ==> []N .& WF(A)_v .-> (P ~> Q)"
    (fn [prem1,prem2,prem3]
-             => [auto_tac (temp_css addSDs2 [BoxWFI]),
-		 etac STL4Edup 1, atac 1,
-		 Auto_tac(),
-		 subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
-		 auto_tac (temp_css addSDs2 [unless]),
-		 etac (temp_conjimpE INV1) 1, atac 1,
-		 merge_box_tac 1,
-		 rtac STL2D 1,
-		 rtac EnsuresInfinite 1, atac 2,
-		 SELECT_GOAL (auto_tac (temp_css addsimps2 [WF_alt])) 1,
-		 atac 2,
-		 subgoal_tac "sigmaa |= [][]$(Enabled(<A>_v))" 1,
-		 merge_box_tac 1,
-		 SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
-		 SELECT_GOAL ((rewtac (temp_rewrite STL3)) THEN
-			      (auto_tac (temp_css addSEs2 [STL4E] addSIs2 [action_mp prem3]))) 1,
-		 fast_tac (action_cs addSIs [action_mp prem2]) 1,
-		 fast_tac (temp_cs addIs [temp_mp DmdPrime]) 1,
-		 fast_tac (temp_cs addSEs [STL4E] addSIs [action_mp prem1]) 1
-		]);
+	 => [auto_tac (temp_css addSDs2 [BoxWFI]),
+	     etac STL4Edup 1, atac 1,
+	     Auto_tac,
+	     subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
+	     auto_tac (temp_css addSDs2 [unless]),
+	     etac (temp_conjimpE INV1) 1, atac 1,
+	     merge_box_tac 1,
+	     rtac STL2D 1,
+	     rtac EnsuresInfinite 1, atac 2,
+	     SELECT_GOAL (old_auto_tac (temp_css addsimps2 [WF_alt])) 1,
+	     atac 2,
+	     subgoal_tac "sigmaa |= [][]$(Enabled(<A>_v))" 1,
+	     merge_box_tac 1,
+	     SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
+	     SELECT_GOAL ((rewtac (temp_rewrite STL3)) THEN
+			  (auto_tac (temp_css addSEs2 [STL4E] addSIs2 [action_mp prem3]))) 1,
+	     fast_tac (action_cs addSIs [action_mp prem2]) 1,
+	     fast_tac (temp_cs addIs [temp_mp DmdPrime]) 1,
+	     fast_tac (temp_cs addSEs [STL4E] addSIs [action_mp prem1]) 1
+	    ]);
 
 (* Sometimes easier to use; designed for action B rather than state predicate Q *)
 qed_goalw "WF_leadsto" TLA.thy [leadsto]
    "[| N .& P .-> $Enabled (<A>_v);            \
 \      N .& <A>_v .-> B;                  \ 
 \      [](N .& [.~A]_v) .-> stable P  |]  \
 \   ==> []N .& WF(A)_v .-> (P ~> B)"
    (fn [prem1,prem2,prem3]
        => [auto_tac (temp_css addSDs2 [BoxWFI]),
            etac STL4Edup 1, atac 1,
-           Auto_tac(),
+           Auto_tac,
            subgoal_tac "sigmaa |= <><A>_v" 1,
            SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImpl2,STL4E] addSIs2 [action_mp prem2])) 1,
            rtac classical 1,
            rtac STL2D 1,
            auto_tac (temp_css addsimps2 WF_def::more_temp_simps addSEs2 [mp]),

    (fn [prem1,prem2,prem3] =>
                 [auto_tac (temp_css addSDs2 [BoxSFI]),
 		 eres_inst_tac [("F","F")] dup_boxE 1,
 		 merge_temp_box_tac 1,
 		 etac STL4Edup 1, atac 1,
-		 Auto_tac(),
+		 Auto_tac,
 		 subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
 		 auto_tac (temp_css addSDs2 [unless]),
 		 etac (temp_conjimpE INV1) 1, atac 1,
 		 merge_act_box_tac 1,
 		 rtac STL2D 1,
 		 rtac EnsuresInfinite 1, atac 2,
-		 SELECT_GOAL (auto_tac (temp_css addsimps2 [SF_alt])) 1,
+		 SELECT_GOAL (old_auto_tac (temp_css addsimps2 [SF_alt])) 1,
 		 atac 2,
 		 subgoal_tac "sigmaa |= []<>$(Enabled(<A>_v))" 1,
 		 SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
 		 eres_inst_tac [("F","F")] dup_boxE 1,
 		 etac STL4Edup 1, atac 1,

 \      P .& P` .& <N .& A>_f .-> B;   \
 \      P .& $(Enabled(<M>_g)) .-> $(Enabled(<A>_f));   \
 \      [](N .& [.~B]_f) .& WF(A)_f .& []F .& <>[]($(Enabled(<M>_g))) .-> <>[]P |]   \
 \  ==> []N .& WF(A)_f .& []F .-> WF(M)_g"
    (fn [prem1,prem2,prem3,prem4]
-       => [Auto_tac(),
+       => [Auto_tac,
 	   case_tac "sigma |= <>[]$Enabled(<M>_g)" 1,
 	   SELECT_GOAL (auto_tac (temp_css addsimps2 [WF_def,dmd_def])) 2,
 	   case_tac "sigma |= <>[][.~B]_f" 1,
 	   subgoal_tac "sigma |= <>[]P" 1,
 	   asm_full_simp_tac (simpset() addsimps [WF_def]) 1,

 	   subgoal_tac "sigma |= <>[]$Enabled(<A>_f)" 1,
 	   dtac mp 1, atac 1,
 	   subgoal_tac "sigma |= <>([]N .& []P .& []<><A>_f)" 1,
 	   rtac ((temp_unlift DmdBoxDmd) RS iffD1) 1,
 	   eres_inst_tac [("F","[]N .& []P .& []<><A>_f")] DmdImplE 1,
-	   SELECT_GOAL (Auto_tac()) 1,
+	   SELECT_GOAL Auto_tac 1,
 	   dres_inst_tac [("P","P")] (temp_mp BoxPrime) 1,
 	   merge_act_box_tac 1,
 	   etac InfImpl 1, atac 1,
 	   SELECT_GOAL (auto_tac (temp_css addsimps2 [angle_def] addSIs2 [action_mp prem2])) 1,
 	   etac BoxDmd 1,
 	   dres_inst_tac [("F","<><A>_f"),("G","[]P")] BoxDmd 1, atac 1,
 	   eres_inst_tac [("F","[]<><A>_f .& []P")] DmdImplE 1,
-	   SELECT_GOAL (Auto_tac ()) 1,
+	   SELECT_GOAL Auto_tac 1,
 	   rtac (temp_mp (prem3 RS STL4 RS DmdImpl)) 1,
 	   fast_tac (temp_cs addIs [STL4E,DmdImplE]) 1,
 	   etac (temp_conjimpE STL6) 1, atac 1,
 	   eres_inst_tac [("V","sigma |= <>[][.~ B]_f")] thin_rl 1,
 	   dtac BoxWFI 1,

 \      P .& P` .& <N .& A>_f .-> B;   \
 \      P .& $(Enabled(<M>_g)) .-> $(Enabled(<A>_f));   \
 \      [](N .& [.~B]_f) .& SF(A)_f .& []F .& []<>($(Enabled(<M>_g))) .-> <>[]P |]   \
 \  ==> []N .& SF(A)_f .& []F .-> SF(M)_g"
    (fn [prem1,prem2,prem3,prem4]
-       => [Auto_tac(),
+       => [Auto_tac,
 	   case_tac "sigma |= []<>$Enabled(<M>_g)" 1,
 	   SELECT_GOAL (auto_tac (temp_css addsimps2 [SF_def,dmd_def])) 2,
 	   case_tac "sigma |= <>[][.~B]_f" 1,
 	   subgoal_tac "sigma |= <>[]P" 1,
 	   asm_full_simp_tac (simpset() addsimps [SF_def]) 1,

 	   subgoal_tac "sigma |= []<>$Enabled(<A>_f)" 1,
 	   dtac mp 1, atac 1,
 	   subgoal_tac "sigma |= <>([]N .& []P .& []<><A>_f)" 1,
 	   rtac ((temp_unlift DmdBoxDmd) RS iffD1) 1,
 	   eres_inst_tac [("F","[]N .& []P .& []<><A>_f")] DmdImplE 1,
-	   SELECT_GOAL (Auto_tac()) 1,
+	   SELECT_GOAL Auto_tac 1,
 	   dres_inst_tac [("P","P")] (temp_mp BoxPrime) 1,
 	   merge_act_box_tac 1,
 	   etac InfImpl 1, atac 1,
 	   SELECT_GOAL (auto_tac (temp_css addsimps2 [angle_def] addSIs2 [action_mp prem2])) 1,
 	   etac BoxDmd 1,
 	   dres_inst_tac [("F","<><A>_f"),("G","[]P")] BoxDmd 1, atac 1,
 	   eres_inst_tac [("F","[]<><A>_f .& []P")] DmdImplE 1,
-	   SELECT_GOAL (Auto_tac ()) 1,
+	   SELECT_GOAL Auto_tac 1,
 	   rtac (temp_mp (prem3 RS DmdImpl RS STL4)) 1,
 	   fast_tac (temp_cs addEs [STL4E,DmdImplE]) 1,
 	   dtac BoxSFI 1,
 	   eres_inst_tac [("F","N")] dup_boxE 1,
 	   eres_inst_tac [("F","F")] dup_boxE 1,

          [cut_facts_tac [prem1] 1,
           etac wf_induct 1,
           subgoal_tac "sigma |= []((REX y. #((y,x):r) .& F y) .-> <>G)" 1,
 	  cut_facts_tac prems 1,
 	  etac STL4Edup 1, atac 1,
-	  Auto_tac(), etac swap 1, atac 1,
+	  Auto_tac, etac swap 1, atac 1,
 	  rtac dup_dmdD 1,
 	  etac DmdImpl2 1, atac 1,
 	  subgoal_tac "sigma |= [](RALL y. #((y,x):r) .& F y .-> <>G)" 1,
 	  fast_tac (temp_cs addSEs [STL4E]) 1,
 	  auto_tac (temp_css addsimps2 [all_box]),

 	       ]);
 
 (* If r is well-founded, state function v cannot decrease forever *)
 qed_goal "wf_not_box_decrease" TLA.thy
   "!!r. wf r ==> [][ {[v$, $v]} .: #r ]_v .-> <>[][#False]_v"
-  (fn _ => [Auto_tac(),
+  (fn _ => [Auto_tac,
             subgoal_tac "ALL x. (sigma |= [](Init($v .= #x) .-> <>[][#False]_v))" 1,
             etac allE 1,
             dtac STL2D 1,
             auto_tac (temp_css addsimps2 [Init_def]),
             etac wf_dmd 1,

             etac swap 1,
             subgoal_tac "sigma |= []($v .= #xa)" 1,
             dres_inst_tac [("P", "$v .= #xa")] (temp_mp BoxPrime) 1,
             SELECT_GOAL (auto_tac (temp_css addEs2 [STL4E] addsimps2 [square_def])) 1,
             SELECT_GOAL (auto_tac (temp_css addSIs2 [INV1I] addsimps2 [Init_def])) 1,
-            auto_tac (temp_css addsimps2 [square_def] addSIs2 [unless] addSEs2 [STL4E])
+            old_auto_tac (temp_css addsimps2 [square_def] addSIs2 [unless] addSEs2 [STL4E])
            ]);
 
 (* "wf ?r  ==>  <>[][{[?v$, $?v]} .: #?r]_?v .-> <>[][#False]_?v" *)
 bind_thm("wf_not_dmd_box_decrease",
          standard(rewrite_rule more_temp_simps (wf_not_box_decrease RS DmdImpl)));

 (* If there are infinitely many steps where v decreases w.r.t. r, then there
    have to be infinitely many non-stuttering steps where v doesn't decrease.
 *)
 qed_goal "wf_box_dmd_decrease" TLA.thy
   "wf r ==> []<>({[v$, $v]} .: #r) .-> []<><.~({[v$, $v]} .: #r)>_v"
-  (fn [prem] => [Auto_tac(),
+  (fn [prem] => [Auto_tac,
                  rtac ccontr 1,
                  asm_full_simp_tac 
                    (simpset() addsimps ([action_rewrite not_angle] @ more_temp_simps)) 1,
                  dtac (prem RS (temp_mp wf_not_dmd_box_decrease)) 1,
                  dtac BoxDmdDmdBox 1, atac 1,
                  subgoal_tac "sigma |= []<>((#False)::action)" 1,
-                 SELECT_GOAL (Auto_tac()) 1,
+                 SELECT_GOAL Auto_tac 1,
                  etac STL4E 1,
                  rtac DmdImpl 1,
                  auto_tac (action_css addsimps2 [square_def] addSEs2 [prem RS wf_irrefl])
                 ]);
 
 (* In particular, for natural numbers, if n decreases infinitely often
    then it has to increase infinitely often.
 *)
 qed_goal "nat_box_dmd_decrease" TLA.thy
   "!!n::nat stfun. []<>(n$ .< $n) .-> []<>($n .< n$)"
-  (fn _ => [Auto_tac(),
+  (fn _ => [Auto_tac,
             subgoal_tac "sigma |= []<><.~( {[n$,$n]} .: #less_than)>_n" 1,
             etac thin_rl 1, etac STL4E 1, rtac DmdImpl 1,
             SELECT_GOAL (auto_tac (claset(), simpset() addsimps [angle_def])) 1,
             rtac nat_less_cases 1,
-            Auto_tac(),
+            Auto_tac,
             rtac (temp_mp wf_box_dmd_decrease) 1,
             auto_tac (claset() addSEs [STL4E] addSIs [DmdImpl], simpset())
            ]);
 
 (* ------------------------------------------------------------------------- *)