Hi everyone,
when using "assume" in structured proofs, one obviously needs to take
care that the assumptions fit one of the pending goals. In particular,
if the assumptions are more complex, we on can easily make an annoying
mistake there. This is particularly relevant in teaching, but I myself
also stumbled there a few times.
As an user, an easy method to test whether the current set of
assumptions still fit one of the pending goals is "fix P show P sorry".
As I don't know any scenario where wrong assumptions would have an
useful effect, I propose to embed this check into the assume command.
I attached a patch against 61e222517d06 to achieve this. The
modifications are based on the gen_show function in proof.ML, which
already implements a similar check.
This is just a proof of concept; some things most probably need to change:
* the check_goal function is a bit magic. This function should ensure
that there is an open goal (i.e., we are not just in a notepad) and
we are in the outermost block (in forward mode), which contains
this goal (i.e., the innermost block is not opened by "{", but by
"proof")).
* I shuffled around some sets of functions in proof.ML to get the new
call dependencies right. This needs more care to preserve the
internal structure of the file
* I fixed up all the callers of the assume functions by setting the
"int" flag to false (which disables the new check) -- this needs
closer investigation.
-- Lars
diff --git a/src/Pure/Isar/isar_syn.ML b/src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML
+++ b/src/Pure/Isar/isar_syn.ML
@@ -588,11 +588,11 @@
val _ =
Outer_Syntax.command @{command_spec "assume"} "assume propositions"
- (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
+ (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Proof.assume_cmd));
val _ =
Outer_Syntax.command @{command_spec "presume"} "assume propositions, to be established later"
- (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
+ (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Proof.presume_cmd));
val _ =
Outer_Syntax.command @{command_spec "def"} "local definition"
diff --git a/src/Pure/Isar/obtain.ML b/src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML
+++ b/src/Pure/Isar/obtain.ML
@@ -149,7 +149,7 @@
Proof.local_qed (NONE, false)
#> `Proof.the_fact #-> (fn rule =>
Proof.fix vars
- #> Proof.assm (obtain_export fix_ctxt rule (map cert parms)) asms);
+ #> Proof.assm (obtain_export fix_ctxt rule (map cert parms)) asms false);
in
state
|> Proof.enter_forward
@@ -158,7 +158,7 @@
|> Proof.proof (SOME Method.succeed_text) |> Seq.hd
|> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
|> Proof.assume
- [((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
+ [((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])] false
|> `Proof.the_facts
||> Proof.chain_facts chain_facts
||> Proof.show NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
@@ -293,7 +293,7 @@
|> Proof.map_context (K ctxt')
|> Proof.fix (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
|> `Proof.context_of |-> (fn fix_ctxt => Proof.assm
- (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
+ (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)] false)
|> Proof.bind_terms Auto_Bind.no_facts
end;
diff --git a/src/Pure/Isar/proof.ML b/src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML
+++ b/src/Pure/Isar/proof.ML
@@ -49,13 +49,14 @@
val fix: (binding * typ option * mixfix) list -> state -> state
val fix_cmd: (binding * string option * mixfix) list -> state -> state
val assm: Assumption.export ->
- (Thm.binding * (term * term list) list) list -> state -> state
+ (Thm.binding * (term * term list) list) list -> bool -> state -> state
val assm_cmd: Assumption.export ->
- (Attrib.binding * (string * string list) list) list -> state -> state
- val assume: (Thm.binding * (term * term list) list) list -> state -> state
- val assume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
- val presume: (Thm.binding * (term * term list) list) list -> state -> state
- val presume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
+ (Attrib.binding * (string * string list) list) list -> bool -> state -> state
+ val assume: (Thm.binding * (term * term list) list) list -> bool -> state -> state
+ val assume_cmd: (Attrib.binding * (string * string list) list) list -> bool -> state -> state
+ val presume: (Thm.binding * (term * term list) list) list -> bool -> state -> state
+ val presume_cmd: (Attrib.binding * (string * string list) list) list -> bool -> state -> state
+
val def: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
val chain: state -> state
@@ -606,28 +607,6 @@
end;
-(* assume etc. *)
-
-local
-
-fun gen_assume asm prep_att exp args state =
- state
- |> assert_forward
- |> map_context_result (asm exp (Attrib.map_specs (map (prep_att (context_of state))) args))
- |> these_factss [] |> #2;
-
-in
-
-val assm = gen_assume Proof_Context.add_assms_i (K I);
-val assm_cmd = gen_assume Proof_Context.add_assms Attrib.attribute_cmd;
-val assume = assm Assumption.assume_export;
-val assume_cmd = assm_cmd Assumption.assume_export;
-val presume = assm Assumption.presume_export;
-val presume_cmd = assm_cmd Assumption.presume_export;
-
-end;
-
-
(* def *)
local
@@ -737,34 +716,6 @@
end;
-(* case *)
-
-local
-
-fun qualified_binding a =
- Binding.qualify true (Long_Name.qualifier a) (Binding.name (Long_Name.base_name a));
-
-fun gen_invoke_case prep_att (name, xs, raw_atts) state =
- let
- val atts = map (prep_att (context_of state)) raw_atts;
- val (asms, state') = state |> map_context_result (fn ctxt =>
- ctxt |> Proof_Context.apply_case (Proof_Context.get_case ctxt name xs));
- val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
- in
- state'
- |> assume assumptions
- |> bind_terms Auto_Bind.no_facts
- |> `the_facts |-> (fn thms => note_thmss [((Binding.name name, []), [(thms, [])])])
- end;
-
-in
-
-val invoke_case = gen_invoke_case (K I);
-val invoke_case_cmd = gen_invoke_case Attrib.attribute_cmd;
-
-end;
-
-
(** proof structure **)
@@ -1048,6 +999,86 @@
end;
+(* assume etc. *)
+
+local
+
+fun gen_assume asm prep_att exp args int state =
+ let
+ val _ = tracing (PolyML.makestring (level state))
+ fun check_goal (State st) = can current_goal (State (Stack.pop st))
+ val fail_msg = "With this assumption, any local statement will fail to refine any pending goal"
+ fun test_assm state =
+ let
+ val (name_P, state') =
+ map_context_result (yield_singleton Variable.variant_fixes "P") state
+ fun after_qed' results =
+ refine_goals (fn _ => fn _ => ()) (context_of state') (flat results)
+ #> check_result "Failed to refine any pending goal"
+ val state'' =
+ state'
+ |> generic_goal Proof_Context.bind_propp_i "assume_show" NONE
+ (after_qed', K I) [[(Free (name_P, Type ("prop", [])), [])]]
+ val test_proof =
+ try (local_skip_proof true)
+ |> Exn.interruptible_capture
+ in
+ state'' |> test_proof
+ end
+ in
+ state
+ |> assert_forward
+ |> map_context_result (asm exp (Attrib.map_specs (map (prep_att (context_of state))) args))
+ |> these_factss [] |> #2
+ |> (int andalso check_goal state) ? (fn state =>
+ (case test_assm state of
+ Exn.Res (SOME _) => state
+ | Exn.Res NONE => error fail_msg
+ | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR fail_msg])))
+ end;
+
+in
+
+val assm = gen_assume Proof_Context.add_assms_i (K I);
+val assm_cmd = gen_assume Proof_Context.add_assms Attrib.attribute_cmd;
+val assume = assm Assumption.assume_export;
+val assume_cmd = assm_cmd Assumption.assume_export;
+val presume = assm Assumption.presume_export;
+val presume_cmd = assm_cmd Assumption.presume_export;
+
+end;
+
+
+(* case *)
+
+local
+
+fun qualified_binding a =
+ Binding.qualify true (Long_Name.qualifier a) (Binding.name (Long_Name.base_name a));
+
+fun gen_invoke_case prep_att (name, xs, raw_atts) state =
+ let
+ val atts = map (prep_att (context_of state)) raw_atts;
+ val (asms, state') = state |> map_context_result (fn ctxt =>
+ ctxt |> Proof_Context.apply_case (Proof_Context.get_case ctxt name xs));
+ val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
+ in
+ state'
+ |> assume assumptions false
+ |> bind_terms Auto_Bind.no_facts
+ |> `the_facts |-> (fn thms => note_thmss [((Binding.name name, []), [(thms, [])])])
+ end;
+
+in
+
+val invoke_case = gen_invoke_case (K I);
+val invoke_case_cmd = gen_invoke_case Attrib.attribute_cmd;
+
+end;
+
+
+
+
(** future proofs **)
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
