diff options
| author | Josh Chen | 2020-08-14 11:07:17 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-08-14 11:07:17 +0200 |
| commit | bd2efacaf67ae84c41377e7af38dacc5aa64f405 (patch) | |
| tree | 7f213a432b28fc40cb8554bf13bb576f056f2bb7 /spartan/core/goals.ML | |
| parent | 8f4ff41d24dd8fa6844312456d47cad4be6cb239 (diff) | |
(FEAT) Context data slots for known types and conditional type rules, as well as a separate one for judgmental equality rules.
(REF) Goal statement assumptions are now put into the new context data slots.
(FEAT) `assuming` Isar keyword—like `assume` but puts assumptions into context data.
(REF) Typechecking and all other tactics refactored to use type information from the context data, as opposed to looking at all facts visible in context.
MINOR INCOMPATIBILITY: facts that were implicitly used in proofs now have to be annotated with [type] to make them visible throughout the context, else explicitly passed to methods via `using`, or declared with `assuming`.
(REF) Fixed incompatibilities in theories.
Diffstat (limited to 'spartan/core/goals.ML')
| -rw-r--r-- | spartan/core/goals.ML | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML index a04bd0e..7d52495 100644 --- a/spartan/core/goals.ML +++ b/spartan/core/goals.ML @@ -175,7 +175,8 @@ fun gen_schematic_theorem in goal_ctxt |> not (null prems) ? - (Proof_Context.note_thmss "" [((Binding.name prems_name, []), [(prems, [])])] #> snd) + (Proof_Context.note_thmss "" [((Binding.name prems_name, []), [(prems, [])])] + #> snd #> Context_Facts.register_facts prems) |> Proof.theorem before_qed gen_and_after_qed (map snd stmt) |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths) end @@ -188,12 +189,12 @@ val schematic_theorem_cmd = fun theorem spec descr = Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) - ( Scan.option (Args.parens (Args.$$$ "def")) + (Scan.option (Args.parens (Args.$$$ "def")) -- (long_statement || short_statement) >> (fn (opt_derive, (long, binding, includes, elems, concl)) => schematic_theorem_cmd (case opt_derive of SOME "def" => true | _ => false) - long descr NONE (K I) binding includes elems concl) ) + long descr NONE (K I) binding includes elems concl)) fun definition spec descr = Outer_Syntax.local_theory_to_proof' spec "definition via proof" |