src/Pure/skip_proof.ML
author wenzelm
Tue, 23 Nov 2021 12:29:09 +0100
changeset 74832 c299abcf7081
parent 71675 55cb4271858b
child 78795 f7e972d567f3
permissions -rw-r--r--
clarified modules;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 46045
diff changeset
     1
(*  Title:      Pure/skip_proof.ML
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 46045
diff changeset
     2
    Author:     Makarius
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
     3
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 46045
diff changeset
     4
Skip proof via oracle invocation.
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
     5
*)
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
     6
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
     7
signature SKIP_PROOF =
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
     8
sig
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 46045
diff changeset
     9
  val report: Proof.context -> unit
42409
3e1e80df6a42 added more elementary Skip_Proof.make_thm_cterm;
wenzelm
parents: 42360
diff changeset
    10
  val make_thm_cterm: cterm -> thm
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    11
  val make_thm: theory -> term -> thm
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58837
diff changeset
    12
  val cheat_tac: Proof.context -> int -> tactic
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    13
end;
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    14
32970
fbd2bb2489a8 operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
wenzelm
parents: 32966
diff changeset
    15
structure Skip_Proof: SKIP_PROOF =
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    16
struct
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    17
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 46045
diff changeset
    18
(* report *)
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 46045
diff changeset
    19
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 46045
diff changeset
    20
fun report ctxt =
71675
55cb4271858b less redundant markup reports;
wenzelm
parents: 70563
diff changeset
    21
  if Context_Position.reports_enabled ctxt then
64677
8dc24130e8fe more uniform treatment of "bad" like other messages (with serial number);
wenzelm
parents: 64556
diff changeset
    22
    Output.report [Markup.markup (Markup.bad ()) "Skipped proof"]
56294
85911b8a6868 prefer Context_Position where a context is available;
wenzelm
parents: 51552
diff changeset
    23
  else ();
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 46045
diff changeset
    24
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 46045
diff changeset
    25
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    26
(* oracle setup *)
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    27
42409
3e1e80df6a42 added more elementary Skip_Proof.make_thm_cterm;
wenzelm
parents: 42360
diff changeset
    28
val (_, make_thm_cterm) =
56436
30ccec1e82fb more source positions;
wenzelm
parents: 56333
diff changeset
    29
  Context.>>>
64556
851ae0e7b09c more symbols;
wenzelm
parents: 61527
diff changeset
    30
    (Context.map_theory_result (Thm.add_oracle (Binding.make ("skip_proof", \<^here>), I)));
42409
3e1e80df6a42 added more elementary Skip_Proof.make_thm_cterm;
wenzelm
parents: 42360
diff changeset
    31
59621
291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents: 59498
diff changeset
    32
fun make_thm thy prop = make_thm_cterm (Thm.global_cterm_of thy prop);
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    33
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    34
70563
61414c54a70c tuned comments;
wenzelm
parents: 70561
diff changeset
    35
(* cheat_tac -- 'sorry' *)
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    36
70561
0c1b08d0b1fe more accurate proposition for cheat_tac (command 'sorry');
wenzelm
parents: 64677
diff changeset
    37
fun cheat_tac ctxt = SUBGOAL (fn (goal, i) =>
0c1b08d0b1fe more accurate proposition for cheat_tac (command 'sorry');
wenzelm
parents: 64677
diff changeset
    38
  let
0c1b08d0b1fe more accurate proposition for cheat_tac (command 'sorry');
wenzelm
parents: 64677
diff changeset
    39
    val thy = Proof_Context.theory_of ctxt;
0c1b08d0b1fe more accurate proposition for cheat_tac (command 'sorry');
wenzelm
parents: 64677
diff changeset
    40
    val assms = Assumption.all_assms_of ctxt;
0c1b08d0b1fe more accurate proposition for cheat_tac (command 'sorry');
wenzelm
parents: 64677
diff changeset
    41
    val cheat = make_thm thy (Logic.list_implies (map Thm.term_of assms, goal));
0c1b08d0b1fe more accurate proposition for cheat_tac (command 'sorry');
wenzelm
parents: 64677
diff changeset
    42
    val thm = Drule.implies_elim_list cheat (map Thm.assume assms);
0c1b08d0b1fe more accurate proposition for cheat_tac (command 'sorry');
wenzelm
parents: 64677
diff changeset
    43
  in PRIMITIVE (Drule.with_subgoal i (Thm.elim_implies thm)) end);
26530
777f334ff652 Added prove_global.
berghofe
parents: 26463
diff changeset
    44
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    45
end;