equal
deleted
inserted
replaced
43 Scan.optional Attrib.thms [] >> (fn thms => fn ctxt => METHOD (fn facts => |
43 Scan.optional Attrib.thms [] >> (fn thms => fn ctxt => METHOD (fn facts => |
44 let val tac = if all then boogie_all_tac else HEADGOAL oo boogie_tac |
44 let val tac = if all then boogie_all_tac else HEADGOAL oo boogie_tac |
45 in tac ctxt (thms @ facts) end)) |
45 in tac ctxt (thms @ facts) end)) |
46 |
46 |
47 val setup_boogie = Method.setup @{binding boogie} (boogie_method false) |
47 val setup_boogie = Method.setup @{binding boogie} (boogie_method false) |
48 ("Applies an SMT solver to the current goal " ^ |
48 "apply an SMT solver to the current goal \ |
49 "using the current set of Boogie background axioms") |
49 \using the current set of Boogie background axioms" |
50 |
50 |
51 val setup_boogie_all = Method.setup @{binding boogie_all} (boogie_method true) |
51 val setup_boogie_all = Method.setup @{binding boogie_all} (boogie_method true) |
52 ("Applies an SMT solver to all goals " ^ |
52 "apply an SMT solver to all goals \ |
53 "using the current set of Boogie background axioms") |
53 \using the current set of Boogie background axioms" |
54 |
54 |
55 |
55 |
56 local |
56 local |
57 fun explode_conj (@{term HOL.conj} $ t $ u) = explode_conj t @ explode_conj u |
57 fun explode_conj (@{term HOL.conj} $ t $ u) = explode_conj t @ explode_conj u |
58 | explode_conj t = [t] |
58 | explode_conj t = [t] |
94 Thm.prop_of (Rule_Cases.internalize_params st)) (map (rpair []) names)) |
94 Thm.prop_of (Rule_Cases.internalize_params st)) (map (rpair []) names)) |
95 all_tac st)) |
95 all_tac st)) |
96 in |
96 in |
97 val setup_boogie_cases = Method.setup @{binding boogie_cases} |
97 val setup_boogie_cases = Method.setup @{binding boogie_cases} |
98 (Scan.succeed boogie_cases) |
98 (Scan.succeed boogie_cases) |
99 "Prepares a set of Boogie assertions for case-based proofs" |
99 "prepare a set of Boogie assertions for case-based proofs" |
100 end |
100 end |
101 |
101 |
102 |
102 |
103 val setup = |
103 val setup = |
104 setup_boogie #> |
104 setup_boogie #> |