src/HOL/Boogie/Tools/boogie_split.ML
changeset 33662 7be6ee4ee67f
parent 33522 737589bb9bb8
child 33710 ffc5176a9105
     1.1 --- a/src/HOL/Boogie/Tools/boogie_split.ML	Fri Nov 13 15:06:19 2009 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_split.ML	Fri Nov 13 15:10:28 2009 +0100
     1.3 @@ -114,12 +114,15 @@
     1.4  local
     1.5    val split_rules = [@{thm impI}, @{thm conjI}, @{thm TrueI}]
     1.6  
     1.7 -  fun prep_tac ctxt args facts =
     1.8 +  fun ALL_GOALS false tac = ALLGOALS tac
     1.9 +    | ALL_GOALS true tac = PARALLEL_GOALS (HEADGOAL tac)
    1.10 +
    1.11 +  fun prep_tac ctxt ((parallel, verbose), subs) facts =
    1.12      HEADGOAL (Method.insert_tac facts)
    1.13      THEN HEADGOAL (REPEAT_ALL_NEW (Tactic.resolve_tac split_rules))
    1.14      THEN unique_case_names (ProofContext.theory_of ctxt)
    1.15 -    THEN ALLGOALS (SUBGOAL (fn (t, i) =>
    1.16 -      TRY (sub_tactics_tac ctxt args (case_name_of t) i)))
    1.17 +    THEN ALL_GOALS parallel (SUBGOAL (fn (t, i) =>
    1.18 +      TRY (sub_tactics_tac ctxt (verbose, subs) (case_name_of t) i)))
    1.19  
    1.20    val drop_assert_at = Conv.concl_conv ~1 (Conv.try_conv (Conv.arg_conv
    1.21      (Conv.rewr_conv (as_meta_eq @{thm assert_at_def}))))
    1.22 @@ -136,12 +139,14 @@
    1.23            (ProofContext.theory_of ctxt, Thm.prop_of st) names)
    1.24          Tactical.all_tac st))
    1.25  
    1.26 -  val verbose_opt = Args.parens (Args.$$$ "verbose") >> K true
    1.27 +  val options =
    1.28 +    Args.parens (Args.$$$ "verbose") >> K (false, true) ||
    1.29 +    Args.parens (Args.$$$ "fast_verbose") >> K (true, true)
    1.30    val sub_tactics = Args.$$$ "try" -- Args.colon |-- Scan.repeat1 Args.name
    1.31  in
    1.32  val setup_split_vc = Method.setup @{binding split_vc}
    1.33 -  (Scan.lift (Scan.optional verbose_opt false -- Scan.optional sub_tactics [])
    1.34 -    >> split_vc)
    1.35 +  (Scan.lift (Scan.optional options (true, false) --
    1.36 +    Scan.optional sub_tactics []) >> split_vc)
    1.37    ("Splits a Boogie-generated verification conditions into smaller problems" ^
    1.38     " and tries to solve the splinters with the supplied sub-tactics.")
    1.39  end