diff options
Diffstat (limited to '')
| -rw-r--r-- | spartan/core/goals.ML | 123 |
1 files changed, 56 insertions, 67 deletions
diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML index 4b53a7f..51a853e 100644 --- a/spartan/core/goals.ML +++ b/spartan/core/goals.ML @@ -15,27 +15,27 @@ val long_keyword = val long_statement = Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) - Binding.empty_atts -- - Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement - >> (fn ((binding, includes), (elems, concl)) => - (true, binding, includes, elems, concl)) + Binding.empty_atts + -- Scan.optional Parse_Spec.includes [] + -- Parse_Spec.long_statement >> + (fn ((binding, includes), (elems, concl)) => + (true, binding, includes, elems, concl)) val short_statement = - Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes - >> (fn ((shows, assumes), fixes) => + Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes >> + (fn ((shows, assumes), fixes) => (false, Binding.empty_atts, [], - [Element.Fixes fixes, Element.Assumes assumes], - Element.Shows shows)) + [Element.Fixes fixes, Element.Assumes assumes], Element.Shows shows) + ) fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt = let val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt val prems = Assumption.local_prems_of elems_ctxt ctxt - val stmt_ctxt = fold (fold (Proof_Context.augment o fst) o snd) - stmt elems_ctxt - in - case raw_stmt of - Element.Shows _ => + val stmt_ctxt = + fold (fold (Proof_Context.augment o fst) o snd) stmt elems_ctxt + in case raw_stmt + of Element.Shows _ => let val stmt' = Attrib.map_specs (map prep_att) stmt in (([], prems, stmt', NONE), stmt_ctxt) end | Element.Obtains raw_obtains => @@ -50,11 +50,8 @@ fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt = |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(that, [])])] ||> Proof_Context.restore_stmt asms_ctxt - - val stmt' = [ - (Binding.empty_atts, - [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])]) - ] + val stmt' = + [(Binding.empty_atts, [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])] in ((Obtain.obtains_attribs raw_obtains, prems, stmt', SOME that'), that_ctxt) @@ -65,23 +62,19 @@ fun define_proof_term name (local_name, [th]) lthy = let fun make_name_binding suffix local_name = let val base_local_name = Long_Name.base_name local_name - in - Binding.qualified_name - ((case base_local_name of - "" => name - | _ => base_local_name) - ^(case suffix of - SOME "prf" => "_prf" - | SOME "def" => "_def" - | _ => "")) + in Binding.qualified_name + ((case base_local_name of "" => name | _ => base_local_name) ^ + (case suffix + of SOME "prf" => "_prf" + | SOME "def" => "_def" + | _ => "")) end val (prems, concl) = (Logic.strip_assums_hyp (Thm.prop_of th), - Logic.strip_assums_concl (Thm.prop_of th)) + Logic.strip_assums_concl (Thm.prop_of th)) in - if not (Lib.is_typing concl) then - ([], lthy) + if not (Lib.is_typing concl) then ([], lthy) else let val prems_vars = distinct Term.aconv (flat (map (Lib.collect_subterms is_Var) prems)) @@ -91,18 +84,16 @@ fun define_proof_term name (local_name, [th]) lthy = val params = inter Term.aconv concl_vars prems_vars - val prf_tm = - fold_rev lambda params (Lib.term_of_typing concl) + val prf_tm = fold_rev lambda params (Lib.term_of_typing concl) val ((_, (_, raw_def)), lthy') = Local_Theory.define ((make_name_binding NONE local_name, Mixfix.NoSyn), ((make_name_binding (SOME "prf") local_name, []), prf_tm)) lthy - val def = - fold - (fn th1 => fn th2 => Thm.combination th2 th1) - (map (Thm.reflexive o Thm.cterm_of lthy) params) - raw_def + val def = fold + (fn th1 => fn th2 => Thm.combination th2 th1) + (map (Thm.reflexive o Thm.cterm_of lthy) params) + raw_def val ((_, def'), lthy'') = Local_Theory.note ((make_name_binding (SOME "def") local_name, []), [def]) @@ -112,26 +103,26 @@ fun define_proof_term name (local_name, [th]) lthy = end end | define_proof_term _ _ _ = error - ("Unimplemented: handling proof terms of multiple facts in" - ^" single result") + ("Unimplemented: proof terms for multiple facts in one statement") fun gen_schematic_theorem - bundle_includes prep_att prep_stmt - gen_prf long kind before_qed after_qed (name, raw_atts) - raw_includes raw_elems raw_concl int lthy = + bundle_includes prep_att prep_stmt + gen_prf_tm long kind + before_qed after_qed + (name, raw_atts) raw_includes raw_elems raw_concl + do_print lthy + = let - val _ = Local_Theory.assert lthy; - + val _ = Local_Theory.assert lthy val elems = raw_elems |> map (Element.map_ctxt_attrib (prep_att lthy)) val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy |> bundle_includes raw_includes |> prep_statement (prep_att lthy) prep_stmt elems raw_concl val atts = more_atts @ map (prep_att lthy) raw_atts val pos = Position.thread_data () - val prems_name = if long then Auto_Bind.assmsN else Auto_Bind.thatN - fun after_qed' results goal_ctxt' = + fun gen_and_after_qed results goal_ctxt' = let val results' = burrow (map (Goal.norm_result lthy) o Proof_Context.export goal_ctxt' lthy) @@ -147,35 +138,34 @@ fun gen_schematic_theorem true) val (res', lthy'') = - if gen_prf + if gen_prf_tm then let - val (prf_tm_defs, lthy'') = - fold - (fn result => fn (defs, lthy) => - apfst (fn new_defs => defs @ new_defs) - (define_proof_term (Binding.name_of name) result lthy)) - res ([], lthy') - + val (prf_tm_defs, new_lthy) = fold + (fn result => fn (defs, lthy) => + apfst (fn new_defs => defs @ new_defs) + (define_proof_term (Binding.name_of name) result lthy)) + res + ([], lthy') val res_folded = - map (apsnd (map (Local_Defs.fold lthy'' prf_tm_defs))) res + map (apsnd (map (Local_Defs.fold new_lthy prf_tm_defs))) res in Local_Theory.notes_kind kind [((name, @{attributes [typechk]} @ atts), [(maps #2 res_folded, [])])] - lthy'' + new_lthy end else Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy' - val _ = Proof_Display.print_results int pos lthy'' + val _ = Proof_Display.print_results do_print pos lthy'' ((kind, Binding.name_of name), map (fn (_, ths) => ("", ths)) res') val _ = if substmts then map - (fn (name, ths) => Proof_Display.print_results int pos lthy'' + (fn (name, ths) => Proof_Display.print_results do_print pos lthy'' (("and", name), [("", ths)])) res else [] @@ -186,7 +176,7 @@ fun gen_schematic_theorem goal_ctxt |> not (null prems) ? (Proof_Context.note_thmss "" [((Binding.name prems_name, []), [(prems, [])])] #> snd) - |> Proof.theorem before_qed after_qed' (map snd stmt) + |> Proof.theorem before_qed gen_and_after_qed (map snd stmt) |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths) end @@ -197,13 +187,13 @@ val schematic_theorem_cmd = Expression.read_statement fun theorem spec descr = - Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) - (Scan.option (Args.parens (Args.$$$ "derive")) - -- (long_statement || short_statement) >> - (fn (opt_derive, (long, binding, includes, elems, concl)) => - schematic_theorem_cmd - (case opt_derive of SOME "derive" => true | _ => false) - long descr NONE (K I) binding includes elems concl)) + Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) + ( Scan.option (Args.parens (Args.$$$ "derive")) + -- (long_statement || short_statement) >> + (fn (opt_derive, (long, binding, includes, elems, concl)) => + schematic_theorem_cmd + (case opt_derive of SOME "derive" => true | _ => false) + long descr NONE (K I) binding includes elems concl) ) fun definition spec descr = Outer_Syntax.local_theory_to_proof' spec "definition via proof" @@ -211,7 +201,6 @@ fun definition spec descr = (fn (long, binding, includes, elems, concl) => schematic_theorem_cmd true long descr NONE (K I) binding includes elems concl)) - in val _ = theorem \<^command_keyword>\<open>Theorem\<close> "Theorem" |