isabelle: src/Pure/skip_proof.ML@d20ca79d50e4 (annotated)

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
56438 7f6b2634d853 more source positions; wenzelm parents: 56436 diff changeset	7	val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", @{here});
7f6b2634d853 more source positions; wenzelm parents: 56436 diff changeset	8	val quick_and_dirty = Config.bool quick_and_dirty_raw;
7f6b2634d853 more source positions; wenzelm parents: 56436 diff changeset	9
6888 d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only); wenzelm parents: diff changeset	10	signature SKIP_PROOF =
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only); wenzelm parents: diff changeset	11	sig
51551 88d1d19fb74f tuned signature and module arrangement; wenzelm parents: 46045 diff changeset	12	val report: Proof.context -> unit
42409 3e1e80df6a42 added more elementary Skip_Proof.make_thm_cterm; wenzelm parents: 42360 diff changeset	13	val make_thm_cterm: cterm -> thm
11892 4a8834757140 moved prove_goalw_cterm to goals.ML; wenzelm parents: 11732 diff changeset	14	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	15	val cheat_tac: Proof.context -> int -> tactic
6888 d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only); wenzelm parents: diff changeset	16	end;
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only); wenzelm parents: diff changeset	17
32970 fbd2bb2489a8 operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode; wenzelm parents: 32966 diff changeset	18	structure Skip_Proof: SKIP_PROOF =
6888 d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only); wenzelm parents: diff changeset	19	struct
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only); wenzelm parents: diff changeset	20
51551 88d1d19fb74f tuned signature and module arrangement; wenzelm parents: 46045 diff changeset	21	(* report *)
88d1d19fb74f tuned signature and module arrangement; wenzelm parents: 46045 diff changeset	22
88d1d19fb74f tuned signature and module arrangement; wenzelm parents: 46045 diff changeset	23	fun report ctxt =
56294 85911b8a6868 prefer Context_Position where a context is available; wenzelm parents: 51552 diff changeset	24	if Context_Position.is_visible ctxt then
56333 38f1422ef473 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject; wenzelm parents: 56294 diff changeset	25	Output.report [Markup.markup Markup.bad "Skipped proof"]
56294 85911b8a6868 prefer Context_Position where a context is available; wenzelm parents: 51552 diff changeset	26	else ();
51551 88d1d19fb74f tuned signature and module arrangement; wenzelm parents: 46045 diff changeset	27
88d1d19fb74f tuned signature and module arrangement; wenzelm parents: 46045 diff changeset	28
11892 4a8834757140 moved prove_goalw_cterm to goals.ML; wenzelm parents: 11732 diff changeset	29	(* oracle setup *)
6888 d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only); wenzelm parents: diff changeset	30
42409 3e1e80df6a42 added more elementary Skip_Proof.make_thm_cterm; wenzelm parents: 42360 diff changeset	31	val (_, make_thm_cterm) =
56436 30ccec1e82fb more source positions; wenzelm parents: 56333 diff changeset	32	Context.>>>
30ccec1e82fb more source positions; wenzelm parents: 56333 diff changeset	33	(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	34
59621 291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context; wenzelm parents: 59498 diff changeset	35	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	36
11892 4a8834757140 moved prove_goalw_cterm to goals.ML; wenzelm parents: 11732 diff changeset	37
51551 88d1d19fb74f tuned signature and module arrangement; wenzelm parents: 46045 diff changeset	38	(* cheat_tac *)
11892 4a8834757140 moved prove_goalw_cterm to goals.ML; wenzelm parents: 11732 diff changeset	39
59498 50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 58837 diff changeset	40	fun cheat_tac ctxt i st =
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; wenzelm parents: 58837 diff changeset	41	resolve_tac ctxt [make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))] i st;
26530 777f334ff652 Added prove_global. berghofe parents: 26463 diff changeset	42
6888 d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only); wenzelm parents: diff changeset	43	end;

author	wenzelm
	Thu, 16 Apr 2015 15:22:44 +0200
changeset 60097	d20ca79d50e4
parent 59621	291934bac95e
child 60820	d0a88a2182a8
permissions	-rw-r--r--