isabelle: src/HOL/Real_Asymp/inst_existentials.ML@d85d0d41b2bd (annotated)

68630 c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	1	signature INST_EXISTENTIALS =
c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	2	sig
c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	3	val tac : Proof.context -> term list -> int -> tactic
c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	4	end
c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	5
c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	6	structure Inst_Existentials : INST_EXISTENTIALS =
c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	7	struct
c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	8
c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	9	fun tac ctxt [] = TRY o REPEAT_ALL_NEW (resolve_tac ctxt @{thms HOL.conjI})
c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	10	\| tac ctxt (t :: ts) =
c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	11	(TRY o REPEAT_ALL_NEW (resolve_tac ctxt @{thms HOL.conjI}))
c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	12	THEN_ALL_NEW (TRY o (
c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	13	let
c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	14	val thm = Drule.infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt t)] @{thm HOL.exI}
c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	15	in
c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	16	resolve_tac ctxt [thm] THEN' tac ctxt ts
c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	17	end))
c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	18
c55f6f0b3854 Added Real_Asymp package Manuel Eberl <eberlm@in.tum.de> parents: diff changeset	19	end

author	wenzelm
	Wed, 28 Jun 2023 12:25:54 +0200
changeset 78224	d85d0d41b2bd
parent 68630	c55f6f0b3854
permissions	-rw-r--r--