isabelle: src/Pure/skip_proof.ML@386e4cb7ad68 (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
51552 c713c9505f68 clarified Skip_Proof.cheat_tac: more standard tactic; wenzelm parents: 51551 diff changeset	12	val cheat_tac: 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) =
3e1e80df6a42 added more elementary Skip_Proof.make_thm_cterm; wenzelm parents: 42360 diff changeset	29	Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "skip_proof", I)));
3e1e80df6a42 added more elementary Skip_Proof.make_thm_cterm; wenzelm parents: 42360 diff changeset	30
3e1e80df6a42 added more elementary Skip_Proof.make_thm_cterm; wenzelm parents: 42360 diff changeset	31	fun make_thm thy prop = make_thm_cterm (Thm.cterm_of thy prop);
6888 d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only); wenzelm parents: diff changeset	32
11892 4a8834757140 moved prove_goalw_cterm to goals.ML; wenzelm parents: 11732 diff changeset	33
51551 88d1d19fb74f tuned signature and module arrangement; wenzelm parents: 46045 diff changeset	34	(* cheat_tac *)
11892 4a8834757140 moved prove_goalw_cterm to goals.ML; wenzelm parents: 11732 diff changeset	35
51552 c713c9505f68 clarified Skip_Proof.cheat_tac: more standard tactic; wenzelm parents: 51551 diff changeset	36	fun cheat_tac i st =
c713c9505f68 clarified Skip_Proof.cheat_tac: more standard tactic; wenzelm parents: 51551 diff changeset	37	rtac (make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))) i st;
26530 777f334ff652 Added prove_global. berghofe parents: 26463 diff changeset	38
6888 d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only); wenzelm parents: diff changeset	39	end;

author	wenzelm
	Fri, 04 Apr 2014 12:07:48 +0200
changeset 56399	386e4cb7ad68
parent 56333	38f1422ef473
child 56436	30ccec1e82fb
permissions	-rw-r--r--