lib: add ML_goal command
Sometimes we want to prove a fact, but the fact is painful or error-prone to type out manually. In these cases, we'd like to construct the goal fact using ML and then immediately enter a proof block. Previously, we could achieve something like this through careful use of `Thm.trivial` and `schematic_goal`, but this would clutter up the ML namespace and wouln't handle meta conjuncts (`&&&`). The new `ML_goal` command addresses both of these issues. Signed-off-by: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>
This commit is contained in:
Edward Pierzchalski
Gerwin Klein
parent
b153cb9571
commit
bd4392d132
|
|
@ -16,6 +16,7 @@ imports
|
|||
Match_Abbreviation
|
||||
Try_Methods
|
||||
Extract_Conjunct
|
||||
ML_Goal
|
||||
Eval_Bool
|
||||
NICTATools
|
||||
"HOL-Library.Prefix_Order"
|
||||
|
|
|
|||
|
|
@ -0,0 +1,135 @@
|
|||
(*
|
||||
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
|
||||
*
|
||||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
*)
|
||||
|
||||
theory ML_Goal
|
||||
imports Main
|
||||
keywords "ML_goal" :: thy_goal_stmt
|
||||
begin
|
||||
|
||||
\<comment>\<open>
|
||||
Defines a new command `ML_goal`. `ML_goal` is similar to @{command lemma}
|
||||
and @{command theorem} in that it specifies a goal and enters a proof state
|
||||
for you prove that goal.
|
||||
|
||||
However, instead of parsing goal terms from user input, `ML_goal` uses
|
||||
an ML block to produce a list of ML terms, and then sets up the proof state
|
||||
to prove those terms as goals.
|
||||
|
||||
Each goal term must be an instance of either @{typ bool} or @{typ prop}.
|
||||
|
||||
There are some concrete examples in @{file ML_Goal_Test.thy}.
|
||||
\<close>
|
||||
|
||||
ML \<open>
|
||||
|
||||
structure ML_goal_data = Proof_Data(
|
||||
type T = term list
|
||||
val init = K []
|
||||
);
|
||||
|
||||
local
|
||||
|
||||
\<comment>\<open>
|
||||
Why are we stashing something into a `Proof_Data` and then immediately
|
||||
taking it out again?
|
||||
|
||||
In @{ML "fn (pos, source, ctxt: Context.generic) =>
|
||||
ML_Context.expression pos source ctxt"},
|
||||
`source` is a fragment of ML code which gets evaluated in the ML context
|
||||
associated with `ctxt`, which in this case should be the proof context
|
||||
associated with the call to `ML_goal`. The result is a new generic context
|
||||
with a new ML context, updated with the effects of evaluating `source`.
|
||||
|
||||
This means the only way to extract information out of `source` is via
|
||||
its side-effects on the ML context. We have two main options:
|
||||
|
||||
- Declare an @{ML "Unsynchronized.ref"} in this file (ML_Goal), and stash
|
||||
the value described by `source` into that.
|
||||
- This is unlikely to play well with deferred or concurrent proofs.
|
||||
|
||||
- Use an instance of `Proof_Data` to declare some new state that's
|
||||
associated with all proof contexts (in this case "the result of
|
||||
the ML block passed to `ML_goal`"), and evaluate `source` in such a way
|
||||
as to store the result there.
|
||||
- This has more overhead compared to the `ref` solution, but it's
|
||||
still negligible.
|
||||
- This is the 'preferred' way to store 'local state' in contexts.
|
||||
- This is safe for deferred or concurrent proofs.
|
||||
\<close>
|
||||
fun evaluate_goals source =
|
||||
ML_Context.expression
|
||||
(Input.pos_of source)
|
||||
(ML_Lex.read "Theory.local_setup (ML_goal_data.put (("
|
||||
@ ML_Lex.read_source source
|
||||
@ ML_Lex.read "): term list))")
|
||||
|> Context.proof_map
|
||||
#> ML_goal_data.get;
|
||||
|
||||
fun err_msg_bad_type goal (typ: typ) ctxt =
|
||||
"The goal " ^ (@{make_string} (Syntax.pretty_term ctxt goal)) ^ " " ^
|
||||
"has unsupported type " ^ (@{make_string} typ) ^ ". " ^
|
||||
"The ML_goal command expects either a " ^ (@{make_string} @{typ bool}) ^ " " ^
|
||||
"or a " ^ (@{make_string} @{typ prop}) ^ ".";
|
||||
|
||||
fun begin_proof ((name, attrs): Attrib.binding, ml_block: Input.source) ctxt =
|
||||
let
|
||||
\<comment>\<open>
|
||||
In the very common case that a goal is a @{typ bool}, we wrap
|
||||
it in @{term Trueprop} to keep the Proof.theorem command happy.
|
||||
\<close>
|
||||
fun prop_wrap goal =
|
||||
case Term.type_of goal of
|
||||
@{typ bool} => goal |> HOLogic.mk_Trueprop
|
||||
| @{typ prop} => goal
|
||||
| other => error (err_msg_bad_type goal other ctxt);
|
||||
|
||||
val goals =
|
||||
evaluate_goals ml_block ctxt
|
||||
|> List.map prop_wrap
|
||||
|
||||
\<comment>\<open> Ensures free variables are type-consistent. \<close>
|
||||
|> Syntax.check_props ctxt
|
||||
|> List.map (rpair []);
|
||||
|
||||
\<comment>\<open>
|
||||
Figures out that the `folded` in `[folded foo]` means
|
||||
@{attribute folded}. Required for attributes to work.
|
||||
\<close>
|
||||
val parsed_attrs = map (Attrib.check_src ctxt) attrs;
|
||||
val binding = (name, parsed_attrs);
|
||||
|
||||
val start_pos = Position.thread_data ();
|
||||
|
||||
fun after_qed (results: thm list list) ctxt =
|
||||
let
|
||||
val thms = results |> hd;
|
||||
val ((res_name, res), ctxt') =
|
||||
Local_Theory.note (binding, thms) ctxt;
|
||||
val _ =
|
||||
Proof_Display.print_results true start_pos ctxt'
|
||||
(("theorem", res_name), [("", res)])
|
||||
in ctxt' end
|
||||
in
|
||||
Proof.theorem NONE
|
||||
after_qed
|
||||
[goals] ctxt
|
||||
end;
|
||||
|
||||
val ML_goal_cmd =
|
||||
Scan.optional (Parse_Spec.opt_thm_name ":") Binding.empty_atts
|
||||
-- Parse.ML_source
|
||||
>> begin_proof
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.local_theory_to_proof
|
||||
\<^command_keyword>\<open>ML_goal\<close>
|
||||
"ML-provided goal"
|
||||
ML_goal_cmd;
|
||||
|
||||
in end
|
||||
\<close>
|
||||
|
||||
end
|
||||
|
|
@ -0,0 +1,120 @@
|
|||
(*
|
||||
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
|
||||
*
|
||||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
*)
|
||||
|
||||
theory ML_Goal_Test
|
||||
imports
|
||||
ML_Goal
|
||||
"ml-helpers/MLUtils"
|
||||
begin
|
||||
experiment begin
|
||||
|
||||
\<comment>\<open>
|
||||
Basic usage.
|
||||
\<close>
|
||||
ML_goal test: \<open>
|
||||
[@{term "(P \<longrightarrow> Q) \<and> P \<longrightarrow> Q"}]
|
||||
\<close>
|
||||
apply clarsimp
|
||||
done
|
||||
|
||||
thm test
|
||||
|
||||
\<comment>\<open>
|
||||
A goal that we definitely don't want to write out by hand.
|
||||
|
||||
In this case, we're going to show that if x is less than 10,
|
||||
we "only" need to consider the cases when x = 0, or x = 1, or...
|
||||
\<close>
|
||||
ML_goal big_goal: \<open>
|
||||
let
|
||||
val var_x = Free ("x", @{typ nat});
|
||||
val var_P = Free ("P", @{typ bool});
|
||||
val max = 10;
|
||||
|
||||
\<comment>\<open>
|
||||
@{ML "HOLogic.mk_nat"} produces nested Suc's, which are pretty
|
||||
ugly, so we use this instead.
|
||||
\<close>
|
||||
val mk_nat = HOLogic.mk_number @{typ nat};
|
||||
|
||||
\<comment>\<open>
|
||||
Turns (i: int) into @{term "x = i \<Longrightarrow> P"}.
|
||||
\<close>
|
||||
fun mk_case i =
|
||||
let
|
||||
val prem = HOLogic.mk_eq (var_x, mk_nat i) |> HOLogic.mk_Trueprop;
|
||||
val conc = var_P |> HOLogic.mk_Trueprop;
|
||||
in Logic.mk_implies (prem, conc) end
|
||||
|
||||
val x_cases =
|
||||
ListExtras.range 0 max
|
||||
|> map mk_case;
|
||||
|
||||
val assm =
|
||||
HOLogic.mk_binrel @{const_name "less"}
|
||||
(var_x,
|
||||
(mk_nat max))
|
||||
|> HOLogic.mk_Trueprop;
|
||||
|
||||
val goal =
|
||||
Logic.list_implies (assm :: x_cases, var_P |> HOLogic.mk_Trueprop)
|
||||
|
||||
in [goal] end
|
||||
\<close>
|
||||
by force
|
||||
|
||||
\<comment>\<open>
|
||||
Names are optional.
|
||||
\<close>
|
||||
ML_goal \<open>
|
||||
[@{term "True"}]
|
||||
\<close>
|
||||
by (rule TrueI)
|
||||
|
||||
\<comment>\<open>
|
||||
Multiple goals are supported, and result in similar
|
||||
"list of fact" lemmas
|
||||
\<close>
|
||||
ML_goal multiple_goals: \<open>
|
||||
[@{term "(P \<Longrightarrow> Q \<Longrightarrow> P)"}, @{term "(P \<Longrightarrow> Q \<Longrightarrow> Q)"}]
|
||||
\<close>
|
||||
by simp+
|
||||
|
||||
thm multiple_goals[OF TrueI]
|
||||
|
||||
\<comment>\<open>
|
||||
Handles mixes of @{typ bool} and @{typ prop}.
|
||||
\<close>
|
||||
ML_goal \<open>
|
||||
[@{term "PROP A \<Longrightarrow> PROP A"}, @{term "B \<longrightarrow> B"}]
|
||||
\<close>
|
||||
by simp+
|
||||
|
||||
\<comment>\<open>
|
||||
Turns out a lemma name can refer to nothing as well!
|
||||
\<close>
|
||||
ML_goal nothing: \<open>[]\<close>
|
||||
done
|
||||
|
||||
thm nothing[OF TrueI]
|
||||
|
||||
\<comment>\<open>
|
||||
Attributes can be applied, just like normal lemmas.
|
||||
\<close>
|
||||
definition magic where "magic = (5 :: nat)"
|
||||
|
||||
ML_goal declared_with_an_attribute[folded magic_def, simp]: \<open>
|
||||
[@{term "(5 :: nat) = 2 + 3"}]
|
||||
\<close>
|
||||
by simp
|
||||
|
||||
lemma uses_our_new_magic_simp_rule:
|
||||
"magic = 1 + 4"
|
||||
by simp
|
||||
|
||||
end
|
||||
|
||||
end
|
||||
Loading…
Reference in New Issue