106 fun string_of_proof_method meth = |
108 fun string_of_proof_method meth = |
107 (case meth of |
109 (case meth of |
108 Metis_Method (NONE, NONE) => "metis" |
110 Metis_Method (NONE, NONE) => "metis" |
109 | Metis_Method (type_enc_opt, lam_trans_opt) => |
111 | Metis_Method (type_enc_opt, lam_trans_opt) => |
110 "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")" |
112 "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")" |
|
113 | Meson_Method => "meson" |
|
114 | SMT_Method => "smt" |
111 | Simp_Method => "simp" |
115 | Simp_Method => "simp" |
112 | Simp_Size_Method => "simp add: size_ne_size_imp_ne" |
116 | Simp_Size_Method => "simp add: size_ne_size_imp_ne" |
113 | Auto_Method => "auto" |
117 | Auto_Method => "auto" |
114 | Fastforce_Method => "fastforce" |
118 | Fastforce_Method => "fastforce" |
115 | Force_Method => "force" |
119 | Force_Method => "force" |
116 | Arith_Method => "arith" |
120 | Arith_Method => "arith" |
117 | Blast_Method => "blast" |
121 | Blast_Method => "blast" |
118 | Meson_Method => "meson" |
|
119 | Algebra_Method => "algebra") |
122 | Algebra_Method => "algebra") |
120 |
123 |
121 fun steps_of_isar_proof (Proof (_, _, steps)) = steps |
124 fun steps_of_isar_proof (Proof (_, _, steps)) = steps |
122 |
125 |
123 fun label_of_isar_step (Prove (_, _, l, _, _, _, _)) = SOME l |
126 fun label_of_isar_step (Prove (_, _, l, _, _, _, _)) = SOME l |
289 fun by_facts meth ls ss = |
292 fun by_facts meth ls ss = |
290 "by " ^ with_facts (maybe_paren meth) (enclose ("(" ^ meth ^ " ") ")") ls ss |
293 "by " ^ with_facts (maybe_paren meth) (enclose ("(" ^ meth ^ " ") ")") ls ss |
291 |
294 |
292 fun is_direct_method (Metis_Method _) = true |
295 fun is_direct_method (Metis_Method _) = true |
293 | is_direct_method Meson_Method = true |
296 | is_direct_method Meson_Method = true |
|
297 | is_direct_method SMT_Method = true |
294 | is_direct_method _ = false |
298 | is_direct_method _ = false |
295 |
299 |
296 (* Local facts are always passed via "using", which affects "meson" and "metis". This is |
300 (* Local facts are always passed via "using", which affects "meson" and "metis". This is |
297 arguably stylistically superior, because it emphasises the structure of the proof. It is also |
301 arguably stylistically superior, because it emphasises the structure of the proof. It is also |
298 more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence" |
302 more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence" |