isabelle: src/Pure/skip_proof.ML@eba34ff9671c (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
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
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	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.>>>
30ccec1e82fb more source positions; wenzelm parents: 56333 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;

author	wenzelm
	Tue, 29 Mar 2016 16:20:48 +0200
changeset 62749	eba34ff9671c
parent 61527	d05f3d86a758
child 64556	851ae0e7b09c
permissions	-rw-r--r--