isabelle: src/Pure/skip_proof.ML@aa50d903e0a7 (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 =
88d1d19fb74f tuned signature and module arrangement; wenzelm parents: 46045 diff changeset	21	Context_Position.if_visible ctxt Output.report
88d1d19fb74f tuned signature and module arrangement; wenzelm parents: 46045 diff changeset	22	(Markup.markup Markup.bad "Skipped proof");
88d1d19fb74f tuned signature and module arrangement; wenzelm parents: 46045 diff changeset	23
88d1d19fb74f tuned signature and module arrangement; wenzelm parents: 46045 diff changeset	24
11892 4a8834757140 moved prove_goalw_cterm to goals.ML; wenzelm parents: 11732 diff changeset	25	(* oracle setup *)
6888 d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only); wenzelm parents: diff changeset	26
42409 3e1e80df6a42 added more elementary Skip_Proof.make_thm_cterm; wenzelm parents: 42360 diff changeset	27	val (_, make_thm_cterm) =
3e1e80df6a42 added more elementary Skip_Proof.make_thm_cterm; wenzelm parents: 42360 diff changeset	28	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	29
3e1e80df6a42 added more elementary Skip_Proof.make_thm_cterm; wenzelm parents: 42360 diff changeset	30	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	31
11892 4a8834757140 moved prove_goalw_cterm to goals.ML; wenzelm parents: 11732 diff changeset	32
51551 88d1d19fb74f tuned signature and module arrangement; wenzelm parents: 46045 diff changeset	33	(* cheat_tac *)
11892 4a8834757140 moved prove_goalw_cterm to goals.ML; wenzelm parents: 11732 diff changeset	34
51552 c713c9505f68 clarified Skip_Proof.cheat_tac: more standard tactic; wenzelm parents: 51551 diff changeset	35	fun cheat_tac i st =
c713c9505f68 clarified Skip_Proof.cheat_tac: more standard tactic; wenzelm parents: 51551 diff changeset	36	rtac (make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))) i st;
26530 777f334ff652 Added prove_global. berghofe parents: 26463 diff changeset	37
6888 d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only); wenzelm parents: diff changeset	38	end;

author	blanchet
	Mon, 03 Mar 2014 12:48:20 +0100
changeset 55873	aa50d903e0a7
parent 51552	c713c9505f68
child 56294	85911b8a6868
permissions	-rw-r--r--