src/Pure/skip_proof.ML
author wenzelm
Fri, 21 Apr 2017 15:26:24 +0200
changeset 65534 b6250ee6ce79
parent 64677 8dc24130e8fe
child 70561 0c1b08d0b1fe
permissions -rw-r--r--
clarified local_theories: exclude ancestor sessions;
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 =
56294
85911b8a6868 prefer Context_Position where a context is available;
wenzelm
parents: 51552
diff changeset
    21
  if Context_Position.is_visible 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
51551
88d1d19fb74f tuned signature and module arrangement;
wenzelm
parents: 46045
diff changeset
    35
(* cheat_tac *)
11892
4a8834757140 moved prove_goalw_cterm to goals.ML;
wenzelm
parents: 11732
diff changeset
    36
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58837
diff changeset
    37
fun cheat_tac ctxt i st =
60820
d0a88a2182a8 clarified context;
wenzelm
parents: 59621
diff changeset
    38
  resolve_tac ctxt [make_thm (Proof_Context.theory_of ctxt) (Var (("A", 0), propT))] i st;
26530
777f334ff652 Added prove_global.
berghofe
parents: 26463
diff changeset
    39
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents:
diff changeset
    40
end;