aboutsummaryrefslogtreecommitdiff
path: root/spartan
diff options
context:
space:
mode:
Diffstat (limited to 'spartan')
-rw-r--r--spartan/core/Goals.thy199
1 files changed, 0 insertions, 199 deletions
diff --git a/spartan/core/Goals.thy b/spartan/core/Goals.thy
deleted file mode 100644
index f7bcaf5..0000000
--- a/spartan/core/Goals.thy
+++ /dev/null
@@ -1,199 +0,0 @@
-theory Goals
-imports Spartan
-
-begin
-
-ML \<open>
-val long_keyword =
- Parse_Spec.includes >> K "" ||
- Parse_Spec.long_statement_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)) =>
- (binding, includes, elems, concl))
-
-val short_statement =
- 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))
-
-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 _ =>
- let val stmt' = Attrib.map_specs (map prep_att) stmt
- in (([], prems, stmt', NONE), stmt_ctxt) end
- | Element.Obtains raw_obtains =>
- let
- val asms_ctxt = stmt_ctxt
- |> fold (fn ((name, _), asm) =>
- snd o Proof_Context.add_assms Assumption.assume_export
- [((name, [Context_Rules.intro_query NONE]), asm)]) stmt
- val that = Assumption.local_prems_of asms_ctxt stmt_ctxt
- val ([(_, that')], that_ctxt) = asms_ctxt
- |> Proof_Context.set_stmt true
- |> 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)), [])])
- ]
- in
- ((Obtain.obtains_attribs raw_obtains, prems, stmt', SOME that'),
- that_ctxt)
- end
- end
-
-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"
- | _ => ""))
- end
-
- val (prems, concl) =
- (Logic.strip_assums_hyp (Thm.prop_of th),
- Logic.strip_assums_concl (Thm.prop_of th))
- in
- if not (Lib.is_typing concl) then
- ([], lthy)
- else let
- val prems_vars = distinct Term.aconv (flat
- (map (Lib.collect_subterms is_Var) prems))
-
- val concl_vars = Lib.collect_subterms is_Var
- (Lib.term_of_typing concl)
-
- val params = inter Term.aconv concl_vars prems_vars
-
- 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'), lthy'') = Local_Theory.note
- ((make_name_binding (SOME "def") local_name, []), [def])
- lthy'
- in
- (def', lthy'')
- end
- end
- | define_proof_term _ _ _ = error
- ("Unimplemented: handling proof terms of multiple facts in"
- ^" single result")
-
-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 =
- let
- 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' =
- let
- val results' = burrow
- (map (Goal.norm_result lthy) o Proof_Context.export goal_ctxt' lthy)
- results
-
- val ((res, lthy'), substmts) =
- if forall (Binding.is_empty_atts o fst) stmt
- then ((map (pair "") results', lthy), false)
- else
- (Local_Theory.notes_kind kind
- (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results')
- lthy,
- true)
-
- val (res', lthy'') =
- if gen_prf
- 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 res_folded =
- map (apsnd (map (Local_Defs.fold lthy'' prf_tm_defs))) res
- in
- Local_Theory.notes_kind kind
- [((name, @{attributes [typechk]} @ atts),
- [(maps #2 res_folded, [])])]
- lthy''
- end
- else
- Local_Theory.notes_kind kind
- [((name, atts), [(maps #2 res, [])])]
- lthy'
-
- val _ = Proof_Display.print_results int 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''
- (("and", name), [("", ths)]))
- res
- else []
- in
- after_qed results' lthy''
- end
- in
- goal_ctxt
- |> not (null prems) ?
- (Proof_Context.note_thmss "" [((Binding.name prems_name, []), [(prems, [])])] #> snd)
- |> Proof.theorem before_qed after_qed' (map snd stmt)
- |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
- end
-
-val schematic_theorem_cmd =
- gen_schematic_theorem
- Bundle.includes_cmd
- Attrib.check_src
- Expression.read_statement
-\<close>
-
-
-
-end