src/HOL/SMT_Examples/boogie.ML
changeset 54447 019394de2b41
parent 52734 077149654ab4
child 55788 67699e08e969
     1.1 --- a/src/HOL/SMT_Examples/boogie.ML	Sat Nov 16 13:12:02 2013 +0100
     1.2 +++ b/src/HOL/SMT_Examples/boogie.ML	Sat Nov 16 16:57:09 2013 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature BOOGIE =
     1.6  sig
     1.7 -  val boogie_prove: string -> theory -> theory
     1.8 +  val boogie_prove: theory -> string -> unit
     1.9  end
    1.10  
    1.11  structure Boogie: BOOGIE =
    1.12 @@ -299,21 +299,33 @@
    1.13    ALLGOALS (SMT_Solver.smt_tac ctxt (boogie_rules @ axioms))
    1.14  
    1.15  
    1.16 -fun boogie_prove file_name thy =
    1.17 +fun boogie_prove thy text =
    1.18    let
    1.19 -    val (text, thy') = Thy_Load.use_file (Path.explode file_name) thy
    1.20      val lines = explode_lines text
    1.21  
    1.22      val ((axioms, vc), ctxt) =
    1.23        empty_context
    1.24        |> parse_lines lines
    1.25        |> add_unique_axioms
    1.26 -      |> build_proof_context thy'
    1.27 +      |> build_proof_context thy
    1.28  
    1.29      val _ = Goal.prove ctxt [] axioms vc (fn {prems, context} =>
    1.30        boogie_tac context prems)
    1.31      val _ = writeln "Verification condition proved successfully"
    1.32  
    1.33 -  in thy' end
    1.34 +  in () end
    1.35 +
    1.36 +
    1.37 +(* Isar command *)
    1.38 +
    1.39 +val _ =
    1.40 +  Outer_Syntax.command @{command_spec "boogie_file"}
    1.41 +    "prove verification condition from .b2i file"
    1.42 +    (Thy_Load.provide_parse_files "boogie_file" >> (fn files =>
    1.43 +      Toplevel.theory (fn thy =>
    1.44 +        let
    1.45 +          val ([{text, ...}], thy') = files thy;
    1.46 +          val _ = boogie_prove thy' text;
    1.47 +        in thy' end)))
    1.48  
    1.49  end