Tactics (Calculemus)

Tactics Module

Namespace: Calculemus
Assembly: Calculemus.dll

Tactics and Mizar-style proofs.

Types

Type	Description
goals

Functions and values

Function or value	Description
`ante_disj th1 th2` Full Usage: `ante_disj th1 th2` Parameters: th1 : `thm` th2 : `thm` Returns: `thm`	th1 : `thm` th2 : `thm` Returns: `thm`
`assume lps gls` Full Usage: `assume lps gls` Parameters: lps : `(string * formula<fol>) list` gls : `goals` Returns: `goals`	lps : `(string * formula<fol>) list` gls : `goals` Returns: `goals`
`assumps asl` Full Usage: `assumps asl` Parameters: asl : `('a * formula<fol>) list` Returns: `('a * thm) list`	asl : `('a * formula<fol>) list` Returns: `('a * thm) list`
`assumptate gls th` Full Usage: `assumptate gls th` Parameters: gls : `goals` th : `thm` Returns: `thm`	gls : `goals` th : `thm` Returns: `thm`
`at once p gl` Full Usage: `at once p gl` Parameters: once : `'a` p : `'b` gl : `'c` Returns: `'d list`	once : `'a` p : `'b` gl : `'c` Returns: `'d list`
`auto_tac byfn hyps g` Full Usage: `auto_tac byfn hyps g` Parameters: byfn : `'a -> formula<fol> -> goals -> thm list` hyps : `'a` g : `goals` Returns: `goals`	byfn : `'a -> formula<fol> -> goals -> thm list` hyps : `'a` g : `goals` Returns: `goals`
`by hyps p gls` Full Usage: `by hyps p gls` Parameters: hyps : `string list` p : `'a` gls : `goals` Returns: `thm list`	hyps : `string list` p : `'a` gls : `goals` Returns: `thm list`
`cases fm byfn hyps g` Full Usage: `cases fm byfn hyps g` Parameters: fm : `formula<fol>` byfn : `'a -> formula<fol> -> goals -> thm list` hyps : `'a` g : `goals` Returns: `goals`	fm : `formula<fol>` byfn : `'a -> formula<fol> -> goals -> thm list` hyps : `'a` g : `goals` Returns: `goals`
`conclude p byfn hyps gl` Full Usage: `conclude p byfn hyps gl` Parameters: p : `formula<fol>` byfn : `'a -> formula<fol> -> goals -> thm list` hyps : `'a` gl : `goals` Returns: `goals`	p : `formula<fol>` byfn : `'a -> formula<fol> -> goals -> thm list` hyps : `'a` gl : `goals` Returns: `goals`
`conj_intro_tac gls` Full Usage: `conj_intro_tac gls` Parameters: gls : `goals` Returns: `goals`	gls : `goals` Returns: `goals`
`consider (x, p)` Full Usage: `consider (x, p)` Parameters: x : `string` p : `formula<fol>` Returns: `('a -> formula<fol> -> goals -> thm list) -> 'a -> goals -> goals`	x : `string` p : `formula<fol>` Returns: `('a -> formula<fol> -> goals -> thm list) -> 'a -> goals -> goals`
`disj_elim_tac l fm byfn hyps g` Full Usage: `disj_elim_tac l fm byfn hyps g` Parameters: l : `string` fm : `formula<fol>` byfn : `'a -> formula<fol> -> goals -> thm list` hyps : `'a` g : `goals` Returns: `goals`	l : `string` fm : `formula<fol>` byfn : `'a -> formula<fol> -> goals -> thm list` hyps : `'a` g : `goals` Returns: `goals`
`double_th th` Full Usage: `double_th th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`
`exists_elim_tac l fm byfn hyps g` Full Usage: `exists_elim_tac l fm byfn hyps g` Parameters: l : `string` fm : `formula<fol>` byfn : `'a -> formula<fol> -> goals -> thm list` hyps : `'a` g : `goals` Returns: `goals`	l : `string` fm : `formula<fol>` byfn : `'a -> formula<fol> -> goals -> thm list` hyps : `'a` g : `goals` Returns: `goals`
`exists_intro_tac t gls` Full Usage: `exists_intro_tac t gls` Parameters: t : `term` gls : `goals` Returns: `goals`	t : `term` gls : `goals` Returns: `goals`
`extract_thm gls` Full Usage: `extract_thm gls` Parameters: gls : `goals` Returns: `thm`	gls : `goals` Returns: `thm`
`firstassum asl` Full Usage: `firstassum asl` Parameters: asl : `('a * formula<fol>) list` Returns: `thm`	asl : `('a * formula<fol>) list` Returns: `thm`
`fix` Full Usage: `fix` Returns: `string -> goals -> goals`	Returns: `string -> goals -> goals`
`forall_intro_tac y gls` Full Usage: `forall_intro_tac y gls` Parameters: y : `string` gls : `goals` Returns: `goals`	y : `string` gls : `goals` Returns: `goals`
`fprint_goal sw` Full Usage: `fprint_goal sw` Parameters: sw : `TextWriter` Returns: `goals -> unit`	sw : `TextWriter` Returns: `goals -> unit`
`gen_right_alpha y x th` Full Usage: `gen_right_alpha y x th` Parameters: y : `string` x : `string` th : `thm` Returns: `thm`	y : `string` x : `string` th : `thm` Returns: `thm`
`have p` Full Usage: `have p` Parameters: p : `formula<fol>` Returns: `('a -> formula<fol> -> goals -> thm list) -> 'a -> goals -> goals`	p : `formula<fol>` Returns: `('a -> formula<fol> -> goals -> thm list) -> 'a -> goals -> goals`
`imp_intro_tac s gls` Full Usage: `imp_intro_tac s gls` Parameters: s : `string` gls : `goals` Returns: `goals`	s : `string` gls : `goals` Returns: `goals`
`jmodify jfn tfn xs` Full Usage: `jmodify jfn tfn xs` Parameters: jfn : `'a list -> 'b` tfn : `'a -> 'a` xs : `'a list` Returns: `'b`	jfn : `'a list -> 'b` tfn : `'a -> 'a` xs : `'a list` Returns: `'b`
`justify byfn hyps p g` Full Usage: `justify byfn hyps p g` Parameters: byfn : `'a -> formula<fol> -> goals -> thm list` hyps : `'a` p : `formula<fol>` g : `goals` Returns: `thm`	byfn : `'a -> formula<fol> -> goals -> thm list` hyps : `'a` p : `formula<fol>` g : `goals` Returns: `thm`
`lemma_tac s p byfn hyps g` Full Usage: `lemma_tac s p byfn hyps g` Parameters: s : `string` p : `formula<fol>` byfn : `'a -> formula<fol> -> goals -> thm list` hyps : `'a` g : `goals` Returns: `goals`	s : `string` p : `formula<fol>` byfn : `'a -> formula<fol> -> goals -> thm list` hyps : `'a` g : `goals` Returns: `goals`
`multishunt i th` Full Usage: `multishunt i th` Parameters: i : `int` th : `thm` Returns: `thm`	i : `int` th : `thm` Returns: `thm`
`note (l, p)` Full Usage: `note (l, p)` Parameters: l : `string` p : `formula<fol>` Returns: `('a -> formula<fol> -> goals -> thm list) -> 'a -> goals -> goals`	l : `string` p : `formula<fol>` Returns: `('a -> formula<fol> -> goals -> thm list) -> 'a -> goals -> goals`
`once` Full Usage: `once` Returns: `'a list`	Returns: `'a list`
`our thesis byfn hyps gl` Full Usage: `our thesis byfn hyps gl` Parameters: thesis : `'a` byfn : `'b -> formula<fol> -> goals -> thm list` hyps : `'b` gl : `goals` Returns: `goals`	thesis : `'a` byfn : `'b -> formula<fol> -> goals -> thm list` hyps : `'b` gl : `goals` Returns: `goals`
`print_goal g` Full Usage: `print_goal g` Parameters: g : `goals` Modifiers: inline	g : `goals`
`proof tacs p gls` Full Usage: `proof tacs p gls` Parameters: tacs : `(goals -> goals) list` p : `formula<fol>` gls : `goals` Returns: `thm list`	tacs : `(goals -> goals) list` p : `formula<fol>` gls : `goals` Returns: `thm list`
`prove p prf` Full Usage: `prove p prf` Parameters: p : `formula<fol>` prf : `(goals -> goals) list` Returns: `thm`	p : `formula<fol>` prf : `(goals -> goals) list` Returns: `thm`
`qed gl` Full Usage: `qed gl` Parameters: gl : `goals` Returns: `goals`	gl : `goals` Returns: `goals`
`right_exists x t p` Full Usage: `right_exists x t p` Parameters: x : `string` t : `term` p : `formula<fol>` Returns: `thm`	x : `string` t : `term` p : `formula<fol>` Returns: `thm`
`set_goal p` Full Usage: `set_goal p` Parameters: p : `formula<fol>` Returns: `goals`	p : `formula<fol>` Returns: `goals`
`so tac arg byfn` Full Usage: `so tac arg byfn` Parameters: tac : `'a -> ('b -> 'c -> goals -> thm list) -> 'd` arg : `'a` byfn : `'b -> 'c -> goals -> thm list` Returns: `'d`	tac : `'a -> ('b -> 'c -> goals -> thm list) -> 'd` arg : `'a` byfn : `'b -> 'c -> goals -> thm list` Returns: `'d`
`sprint_goal g` Full Usage: `sprint_goal g` Parameters: g : `goals` Returns: `string` Modifiers: inline	g : `goals` Returns: `string`
`tac_proof g prf` Full Usage: `tac_proof g prf` Parameters: g : `goals` prf : `(goals -> goals) list` Returns: `thm`	g : `goals` prf : `(goals -> goals) list` Returns: `thm`
`take` Full Usage: `take` Returns: `term -> goals -> goals`	Returns: `term -> goals -> goals`
`test001 n` Full Usage: `test001 n` Parameters: n : `'a` Returns: `thm -> thm`	n : `'a` Returns: `thm -> thm`
`test002 n` Full Usage: `test002 n` Parameters: n : `int` Returns: `thm * formula<fol>`	n : `int` Returns: `thm * formula<fol>`
`testcase n` Full Usage: `testcase n` Parameters: n : `int` Returns: `thm`	n : `int` Returns: `thm`
`thesis` Full Usage: `thesis` Returns: `string`	Returns: `string`
`using ths p g` Full Usage: `using ths p g` Parameters: ths : `thm list` p : `'a` g : `goals` Returns: `thm list`	ths : `thm list` p : `'a` g : `goals` Returns: `thm list`