This is the assumption insertion rule. It takes a boolean term and a theorem, and returns the same theorem but with the supplied term added to its assumptions. The returned theorem is the inputted theorem if the term is already in the assumptions. `q` A |- p ------------ A u {q} |- p

This is the beta-reducing universal elimination rule. It strips off the outermost universal quantifier from the supplied theorem, and replaces in the body each occurrence of the stripped binding variable with the supplied term. If the supplied term is a lambda abstraction, it also performs beta-reduction on each substituted occurrence that is applied to an argument. The type of the supplied term must equal the type of the stripped binding variable. `\y. t` A |- !x. p -------------------------------- A |- p[ \y.t / x; t[s/y] / x s ]

This is the existential elimination rule. It removes, from the assumptions of a supplied main theorem, the body of a supplied existential theorem (but with all occurrences of the binding variable replaced with a supplied variable), and adds the assumptions of the existential theorem. The supplied variable is not allowed to be free in existential theorem's conclusion or in the original main theorem's other assumptions or its conclusion. Note that the altered body of the existential theorem does not have to be present in the assumptions of the main theorem for the rule to succeed. `y` A1 |- ?x. p A2 |- q [ "y" not free in: ---------------------------- `?x. p`, `q` or `A2\{p[y/x]}` ] A1 u A2\{p[y/x]} |- q See also: exists_rule, mk_exists_rule.

Conditional The internal constant for conditional expressions is called "COND". It *) has special support in the parser/printer, so that *) `if c then t1 else t2` *) is parsed/printed for the internal term *) `COND c t1 t2`. *) |- COND = (\p (t1:'a) t2. @x. ((p <=> true) ==> x = t1) /\ ((p <=> false) ==> x = t2))

This is the conjunction introduction rule. It conjoins the two supplied theorems and unions their assumptions. A1 |- p A2 |- q ------------------ A1 u A2 |- p /\ q

This is the conjunction elimination rule for the LHS. It removes the RHS conjunct from the supplied conjunction theorem. A |- p /\ q ----------- A |- p See also: conjunct2_rule, conjunct_rule, mk_conj_rule.

This is the conjunction elimination rule for the RHS. It removes the LHS conjunct from the supplied conjunction theorem. A |- p /\ q ----------- A |- q See also: conjunct1_rule, conjunct_rule, mk_conj_rule.

This is the intuitionistic contradiction rule. It takes a boolean term and a theorem with falsity as its conclusion. It returns a theorem with the supplied term as its conclusion, under the same assumptions as the supplied theorem. `p` A |- false ---------------- A |- p See also: ccontr_rule, deduct_contrapos_rule.

This is the antisymmetry rule for deduction. It takes two theorem arguments. It returns a theorem stating that the supplied conclusions are equivalent, under the unioned assumptions but with each theorem's conclusion removed from the other's assumptions. A1 |- p A2 |- q -------------------------- A1\{q} u A2\{p} |- p <=> q See also: imp_antisym_rule, undisch_rule.

This is the contraposition rule for deduction. It swaps and logically negates the supplied assumption term and the conclusion of the supplied theorem. Note that the supplied term does not have to be present in the assumptions of the supplied theorem for the rule to succeed. If the logical negation of the supplied theorem's conclusion is the supplied term, then it will not occur in the resulting theorem's assumptions. `q` A |- p --------------------- (A u {~p})\{q} |- ~ q See also: not_intro_rule, disch_rule, contr_rule, ccontr_rule.

Breaks apart a negation, returning its body. dest_not is a term destructor for negations: "~t" |> parse_term |> dest_not returns "t". Fails if term is not a negation.

This is the disjunction introduction rule for the LHS. It disjoins the supplied boolean term to the RHS of the supplied theorem. A |- p `q` ------------ A |- p \/ q See also: disj2_rule, disj_cases_rule, mk_disj1_rule.

This is the disjunction introduction rule for the RHS. It disjoins the supplied boolean term to LHS of the supplied theorem. `p` A |- q ------------ A |- p \/ q Si veda anche: disj1_rule, disj_cases_rule, mk_disj2_rule.

This is the disjunction elimination rule. It takes a disjunction theorem and two extra theorems that share the same conclusion. It returns a theorem with the same conclusion as the extra theorems. The assumptions of the returned theorem union the assumptions of the extra theorems, but with the disjunction theorem's LHS removed from the first's assumptions and its RHS removed from the second's, unioned together with the disjunction theorem's assumptions. A |- p \/ q A1 |- r A2 |- r --------------------------------- A u A1\{p} u A2\{q} |- r See also: disj1_rule, disj2_rule, mk_disj_rule.

Disjunction |- $\/ = (\p1 p2. !p. (p1 ==> p) ==> (p2 ==> p) ==> p)

This is the first equivalence elimination rule. It takes a theorem stating the equivalence of two boolean terms, and returns a theorem stating that the LHS implies the RHS, under the same assumptions. A |- p <=> q ------------ A |- p ==> q See also: eq_imp_rule2, imp_antisym_rule, eq_mp_rule, undisch_rule, mk_imp_rule.

This is the second equivalence elimination rule. It takes a theorem stating the equivalence of two boolean terms, and returns a theorem stating that the RHS implies the LHS, under the same assumptions. A |- p <=> q ------------ A |- q ==> p See also: eq_imp_rule1, imp_antisym_rule, eq_mp_rule, undisch_rule, mk_imp_rule.

This is the falsity equivalence elimination rule. It takes an equality theorem with falsity on the RHS, and returns the logical negation of the LHS, under the same assumptions. A |- p <=> false ---------------- A |- ~ p See also: eqf_intro_rule, not_intro_rule, not_elim_rule, mk_not_rule, eqt_elim_rule, deduct_contrapos_rule.

This is the falsity equivalence introduction rule. It takes a theorem with logical negation at its top level, and returns a theorem stating that the body of the negation is equivalent to falsity, under the same assumptions. A |- ~ p ---------------- A |- p <=> false See also: eqf_elim_rule, not_elim_rule, not_intro_rule, mk_not_rule, eqt_intro_rule.

This is the truth equivalence elimination rule. It takes an equality theorem that has truth on the RHS, and returns a theorem stating that the LHS holds, under the same assumptions. A |- p <=> true --------------- A |- p See also: eqt_intro_rule, eqf_elim_rule.

This is the truth equivalence introduction rule. It takes any theorem, and returns the theorem stating that the conclusion is equivalent to truth, under the same assumptions. A |- p --------------- A |- p <=> true See also: eqt_elim_rule, eqf_intro_rule.

eta_conv : term -> thm This is the eta reduction rule. It takes a lambda abstraction term, where the body is a function application, and the binding variable is the argument subterm of the function application and not free in the function subterm. It returns a theorem stating that the term is equal to the function subterm, under no assumptions. `\x. f x` ---------------- |- (\x. f x) = f See also: beta_conv.

Falsity |- false <=> (!p. p)

|- !f g. f = g <=> (!x. f x = g x)

gen_rule : term -> thm -> thm This is the universal introduction rule. It universally quantifies the supplied theorem with the supplied binding variable, under the same assumptions. The binding variable must not occur free in the assumptions. `x` A |- p [ "x" not free in `A` ] ------------ A |- !x. p See also: list_gen_rule, spec_rule, mk_forall_rule.

This is the antisymmetry rule for implication. It takes two implication theorem arguments, where the LHS of each is the same (modulo alpha- equivalence) as the RHS of the other. It returns a theorem stating the logical equivalence of the two sides, under the unioned assumptions. A1 |- p ==> q A2 |- q ==> p ------------------------------ A1 u A2 |- p <=> q See also: eq_imp_rule1, eq_imp_rule2, deduct_antisym_rule, disch_rule, eqt_intro_rule.

imp_trans_rule : thm -> thm -> thm This is the transitivity rule for implication. It takes two implication theorem arguments, where the first theorem's RHS is the same (modulo alpha-equivalence) as the second theorem's LHS. It returns a theorem stating that the first theorem's LHS implies the second theorem's RHS, under the unioned assumptions of the two theorems. A1 |- p ==> q A2 |- q ==> r ------------------------------ A1 u A2 |- p ==> r See also: list_imp_trans_rule, eq_trans_rule, disch_rule, imp_anitsym_asm_rule.

checks for a bool equality theorem is_bool_eqthm not_true_thm returns true; is_bool_eqthm truth_thm returns false

Tests a term to see if it is a disjunction. is_disj ("t1 \/ t2" |> parse_term) returns true. If the term is not a disjunction the result is false. Never fails.

Tests a term to see if it is a logical negation. "~t" |> parse_term |> is_not returns true. If the term is not a logical negation the result is false. Never fails.

This is the compound universal elimination rule. It strips off an outermost universal quantifier from the supplied theorem for each item in the supplied term list, replacing each occurrence of a stripped binding variable in the body with its corresponding item in the term list. The type of each term in the term list must equal the type of its corresponding binding variable. [`t1`;`t2`;..] A |- !x1 x2 .. . p ----------------------------------- A |- p[t1/x1;t2/x2;..] See also: spec_rule, spec_all_rule, bspec_rule, list_gen_rule.

Force module evaluation

|- $~ = (\p. p ==> false)

This is the logical negation elimination rule. It takes a logical negation theorem, and returns an implication with the negated term on the LHS and falsity on the RHS, under the same assumptions. A |- ~ p ---------------- A |- p ==> false See also: not_intro_rule, eqf_intro_rule, eqf_elim_rule.

This is the logical negation introduction rule. It takes an implication theorem where the RHS is falsity, and returns the logical negation of the LHS, under the same assumptions. A |- p ==> false ---------------- A |- ~ p See also: not_elim_rule, eqf_elim_rule, eqf_intro_rule, deduct_contrapos_rule.

This is the assumption proving rule. It takes two theorems, and returns the second theorem but with the conclusion of the first theorem removed from the assumptions (if present) and the assumptions from the first theorem added. Note that the first theorem's conclusion does not have to be in the second's assumptions for the rule to succeed. A1 |- p A2 |- q ------------------ A1 u (A2\{p}) |- q See also: mp_rule, undisch_rule.

This is the compound default universal elimination rule. It strips off all the outer universal quantifiers from the supplied theorem. Note that the supplied theorem does not have to be a universal quantification for the rule to succeed (in which case the resulting theorem is the same as the supplied theorem). A |- !x1 x2 .. xn. p -------------------- A |- p See also: spec_rule, list_spec_rule, bspec_rule, list_gen_rule.

This is the universal elimination rule. It strips off the outermost universal quantifier from the supplied theorem, and replaces in the body each occurrence of the stripped binding variable with the supplied term. The type of the supplied term must equal the type of the stripped binding variable. `t` A |- !x. p ---------------- A |- p[t/x]

This is the symmetry conversion for equality. It transforms the supplied equality term by swapping its LHS with its RHS, under no assumptions. `t1 = t2` ---------------------- |- t1 = t2 <=> t2 = t1 See also: sym_rule, refl_conv.

|- true

Unique existential quantification |- $?! = (\(P:'a->bool). ?x. P x /\ (!y. P y ==> y = x))

This is the undischarge rule. It takes an implication theorem, and removes the antecedent from the conclusion and adds it to the assumptions. A |- p ==> q ------------ A u {p} |- q See also: disch_rule, mp_rule, prove_asm_rule.