isabelle: src/Pure/skip_proof.ML@269a39b6c5f8 (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 =
71675 55cb4271858b less redundant markup reports; wenzelm parents: 70563 diff changeset	21	if Context_Position.reports_enabled 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
70563 61414c54a70c tuned comments; wenzelm parents: 70561 diff changeset	35	(* cheat_tac -- 'sorry' *)
11892 4a8834757140 moved prove_goalw_cterm to goals.ML; wenzelm parents: 11732 diff changeset	36
70561 0c1b08d0b1fe more accurate proposition for cheat_tac (command 'sorry'); wenzelm parents: 64677 diff changeset	37	fun cheat_tac ctxt = SUBGOAL (fn (goal, i) =>
0c1b08d0b1fe more accurate proposition for cheat_tac (command 'sorry'); wenzelm parents: 64677 diff changeset	38	let
0c1b08d0b1fe more accurate proposition for cheat_tac (command 'sorry'); wenzelm parents: 64677 diff changeset	39	val thy = Proof_Context.theory_of ctxt;
0c1b08d0b1fe more accurate proposition for cheat_tac (command 'sorry'); wenzelm parents: 64677 diff changeset	40	val assms = Assumption.all_assms_of ctxt;
0c1b08d0b1fe more accurate proposition for cheat_tac (command 'sorry'); wenzelm parents: 64677 diff changeset	41	val cheat = make_thm thy (Logic.list_implies (map Thm.term_of assms, goal));
0c1b08d0b1fe more accurate proposition for cheat_tac (command 'sorry'); wenzelm parents: 64677 diff changeset	42	val thm = Drule.implies_elim_list cheat (map Thm.assume assms);
0c1b08d0b1fe more accurate proposition for cheat_tac (command 'sorry'); wenzelm parents: 64677 diff changeset	43	in PRIMITIVE (Drule.with_subgoal i (Thm.elim_implies thm)) end);
26530 777f334ff652 Added prove_global. berghofe parents: 26463 diff changeset	44
6888 d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only); wenzelm parents: diff changeset	45	end;

author	wenzelm
	Fri, 01 Oct 2021 12:45:47 +0200
changeset 74400	269a39b6c5f8
parent 71675	55cb4271858b
child 78795	f7e972d567f3
permissions	-rw-r--r--