--- a/src/HOL/Boogie/Tools/boogie_split.ML Fri Dec 11 15:06:12 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,174 +0,0 @@
-(* Title: HOL/Boogie/Tools/boogie_split.ML
- Author: Sascha Boehme, TU Muenchen
-
-Method to split Boogie-generate verification conditions and pass the splinters
-to user-supplied automated sub-tactics.
-*)
-
-signature BOOGIE_SPLIT =
-sig
- val add_sub_tactic: string * (Proof.context -> int -> tactic) -> theory ->
- theory
- val sub_tactic_names: theory -> string list
- val setup: theory -> theory
-end
-
-structure Boogie_Split: BOOGIE_SPLIT =
-struct
-
-(* sub-tactics store *)
-
-structure Sub_Tactics = Theory_Data
-(
- type T = (Proof.context -> int -> tactic) Symtab.table
- val empty = Symtab.empty
- val extend = I
- fun merge data = Symtab.merge (K true) data
-)
-
-fun add_sub_tactic tac = Sub_Tactics.map (Symtab.update_new tac)
-
-val sub_tactic_names = Symtab.keys o Sub_Tactics.get
-
-fun lookup_sub_tactic ctxt name =
- (case Symtab.lookup (Sub_Tactics.get (ProofContext.theory_of ctxt)) name of
- SOME tac => SOME (name, tac)
- | NONE => (warning ("Unknown sub-tactic: " ^ quote name); NONE))
-
-fun as_meta_eq eq = eq RS @{thm eq_reflection}
-
-fun full_implies_conv cv ct =
- (case try Thm.dest_implies ct of
- NONE => cv ct
- | SOME (cp, cc) => Drule.imp_cong_rule (cv cp) (full_implies_conv cv cc))
-
-fun sub_tactics_tac ctxt (verbose, sub_tac_names) case_name =
- let
- fun trace msg = if verbose then tracing msg else ()
- fun trying name = trace ("Trying tactic " ^ quote name ^ " on case " ^
- quote case_name ^ " ...")
- fun solved () = trace ("Case solved: " ^ quote case_name)
- fun failed () = trace ("Case remains unsolved: " ^ quote case_name)
-
- infix IF_UNSOLVED
- fun (tac1 IF_UNSOLVED tac2) i st = st |> (tac1 i THEN (fn st' =>
- let val j = i + Thm.nprems_of st' - Thm.nprems_of st
- in
- if i > j then (solved (); Tactical.all_tac st')
- else Seq.INTERVAL tac2 i j st'
- end))
-
- fun TRY_ALL [] _ st = (failed (); Tactical.no_tac st)
- | TRY_ALL ((name, tac) :: tacs) i st = (trying name;
- (TRY o tac ctxt IF_UNSOLVED TRY_ALL tacs) i st)
-
- val unfold_labels = Conv.try_conv (Conv.arg_conv
- (More_Conv.rewrs_conv (map as_meta_eq @{thms labels})))
- in
- CONVERSION (full_implies_conv unfold_labels)
- THEN' TRY_ALL (map_filter (lookup_sub_tactic ctxt) sub_tac_names)
- end
-
-
-(* case names *)
-
-fun case_name_of t =
- (case HOLogic.dest_Trueprop (Logic.strip_imp_concl t) of
- @{term assert_at} $ Free (n, _) $ _ => n
- | _ => raise TERM ("case_name_of", [t]))
-
-local
- fun make_case_name (i, t) =
- the_default ("B_" ^ string_of_int (i + 1)) (try case_name_of t)
-
- val assert_intro = Thm.symmetric (as_meta_eq @{thm assert_at_def})
- val l = Thm.dest_arg1 (Thm.rhs_of assert_intro)
- fun intro new =
- Conv.rewr_conv (Thm.instantiate ([], [(l, new)]) assert_intro)
-
- val assert_eq = @{lemma "assert_at x t == assert_at y t"
- by (simp add: assert_at_def)}
- val (x, y) = pairself Thm.dest_arg1 (Thm.dest_binop (Thm.cprop_of assert_eq))
- fun rename old new =
- Conv.rewr_conv (Thm.instantiate ([], [(x, old), (y, new)]) assert_eq)
-
- fun at_concl cv = Conv.concl_conv ~1 (Conv.arg_conv cv)
- fun make_label thy name = Thm.cterm_of thy (Free (name, @{typ bool}))
-
- fun rename_case thy new ct =
- (case try case_name_of (Thm.term_of ct) of
- NONE => at_concl (intro (make_label thy new))
- | SOME old => if new = old then Conv.all_conv
- else at_concl (rename (make_label thy old) (make_label thy new))) ct
-in
-fun unique_case_names thy st =
- let
- val names = map_index make_case_name (Thm.prems_of st)
- |> ` (duplicates (op =)) |-> Name.variant_list
- in ALLGOALS (fn i => CONVERSION (rename_case thy (nth names (i-1))) i) st end
-end
-
-
-(* splitting method *)
-
-local
- val intro_rules = [@{thm impI}, @{thm conjI}, @{thm TrueI}]
- val elim_rules = [@{thm conjE}, @{thm TrueE}]
- val split_tac = REPEAT_ALL_NEW
- (Tactic.resolve_tac intro_rules ORELSE' Tactic.eresolve_tac elim_rules)
-
- fun ALL_GOALS false tac = ALLGOALS tac
- | ALL_GOALS true tac = PARALLEL_GOALS (HEADGOAL tac)
-
- fun prep_tac ctxt ((parallel, verbose), subs) facts =
- HEADGOAL (Method.insert_tac facts)
- THEN HEADGOAL split_tac
- THEN unique_case_names (ProofContext.theory_of ctxt)
- THEN ALL_GOALS parallel (SUBGOAL (fn (t, i) =>
- TRY (sub_tactics_tac ctxt (verbose, subs) (case_name_of t) i)))
-
- val drop_assert_at = Conv.concl_conv ~1 (Conv.try_conv (Conv.arg_conv
- (Conv.rewr_conv (as_meta_eq @{thm assert_at_def}))))
-
- fun split_vc args ctxt = METHOD_CASES (fn facts =>
- prep_tac ctxt args facts #>
- Seq.maps (fn st =>
- st
- |> ALLGOALS (CONVERSION drop_assert_at)
- |> Seq.map (pair (map (rpair [] o case_name_of) (Thm.prems_of st)))) #>
- Seq.maps (fn (names, st) =>
- CASES
- (Rule_Cases.make_common false
- (ProofContext.theory_of ctxt, Thm.prop_of st) names)
- Tactical.all_tac st))
-
- val options =
- Args.parens (Args.$$$ "verbose") >> K (false, true) ||
- Args.parens (Args.$$$ "fast_verbose") >> K (true, true)
- val sub_tactics = Args.$$$ "try" -- Args.colon |-- Scan.repeat1 Args.name
-in
-val setup_split_vc = Method.setup @{binding split_vc}
- (Scan.lift (Scan.optional options (true, false) --
- Scan.optional sub_tactics []) >> split_vc)
- ("Splits a Boogie-generated verification conditions into smaller problems" ^
- " and tries to solve the splinters with the supplied sub-tactics.")
-end
-
-
-(* predefined sub-tactics *)
-
-fun fast_sub_tac ctxt = Classical.fast_tac (Classical.claset_of ctxt)
-fun simp_sub_tac ctxt =
- Simplifier.asm_full_simp_tac (Simplifier.simpset_of ctxt)
-fun smt_sub_tac ctxt = SMT_Solver.smt_tac ctxt (Split_VC_SMT_Rules.get ctxt)
-
-
-(* setup *)
-
-val setup =
- setup_split_vc #>
- add_sub_tactic ("fast", fast_sub_tac) #>
- add_sub_tactic ("simp", simp_sub_tac) #>
- add_sub_tactic ("smt", smt_sub_tac)
-
-end