From bd2efacaf67ae84c41377e7af38dacc5aa64f405 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 14 Aug 2020 11:07:17 +0200 Subject: (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. --- spartan/core/elaborated_statement.ML | 31 ++++++++++++++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) (limited to 'spartan/core/elaborated_statement.ML') diff --git a/spartan/core/elaborated_statement.ML b/spartan/core/elaborated_statement.ML index 81f4a7d..33f88cf 100644 --- a/spartan/core/elaborated_statement.ML +++ b/spartan/core/elaborated_statement.ML @@ -416,6 +416,35 @@ val structured_statement = Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows)) +fun these_factss more_facts (named_factss, state) = + (named_factss, state |> Proof.set_facts (maps snd named_factss @ more_facts)) + +fun gen_assume prep_statement prep_att export raw_fixes raw_prems raw_concls state = + let + val ctxt = Proof.context_of state; + + val bindings = map (apsnd (map (prep_att ctxt)) o fst) raw_concls; + val {fixes = params, assumes = prems_propss, shows = concl_propss, result_binds, text, ...} = + #1 (prep_statement raw_fixes raw_prems (map snd raw_concls) ctxt); + val propss = (map o map) (Logic.close_prop params (flat prems_propss)) concl_propss; + in + state + |> Proof.assert_forward + |> Proof.map_context_result (fn ctxt => + ctxt + |> Proof_Context.augment text + |> fold Variable.maybe_bind_term result_binds + |> fold_burrow (Assumption.add_assms export o map (Thm.cterm_of ctxt)) propss + |-> (fn premss => fn ctxt => + (premss, Context_Facts.register_facts (flat premss) ctxt)) + |-> (fn premss => + Proof_Context.note_thmss "" (bindings ~~ (map o map) (fn th => ([th], [])) premss))) + |> these_factss [] |> #2 + end + +val assume = + gen_assume Proof_Context.cert_statement (K I) Assumption.assume_export + in val _ = Outer_Syntax.command \<^command_keyword>\assuming\ "elaborated assumption" @@ -433,7 +462,7 @@ val _ = Outer_Syntax.command \<^command_keyword>\assuming\ "elabora val c' = c |> map (fn ((b, atts), ss) => ((b, map (Attrib.attribute_cmd ctxt) atts), map read_terms ss)) val c'' = Elab.elaborate ctxt [] c' - in Proof.assume a' b' c'' state end))) + in assume a' b' c'' state end))) end -- cgit v1.2.3