This is the assumption rule. It takes a boolean term, and returns a theorem stating that the term holds under the single assumption of the term itself. `p` -------- {p} |- p

This is the beta reduction conversion. It takes a lambda abstraction application term, and returns a theorem stating that the application is equal to the lambda abstraction body but with all occurrences of the binding variable replaced with the application's argument, under no assumptions. `(\x. t) s` --------------------- |- (\x. t) s = t[s/x]

This is the implication introduction rule. It takes a boolean term and a theorem, and removes the term from the theorem's assumptions (if present) and adds it as an antecedent of the conclusion. Note that the term does not have to be in the assumptions of the supplied theorem for the rule to succeed. `p` A |- q ---------------- A\{p} |- p ==> q See also: undisch_rule, mp_rule.

This is the equality modus ponens rule. It takes an equality theorem and a second theorem, where the equality theorem's LHS is alpha-equivalent to the conclusion of the second theorem. It returns a theorem stating that the equality theorem's RHS holds, under the unioned assumptions of the supplied theorems. A1 |- p <=> q A2 |- p ------------------------ A1 u A2 |- q See also: mp_rule, eq_imp_rule1, eq_imp_rule2, imp_antisym_rule.

This is the variable instantiation rule. It takes a variable instantiation list and a theorem, and performs a single parallel instantiation of the free variables in the theorem's assumptions and conclusion, according to the instantiation list. All free occurrences of instantiation list domain elements in the theorem get replaced. Each instantiation list domain element must be a variable, and each range element must have the same type as its corresponding domain element. Binding variables in the resulting theorem are renamed as necessary to avoid variable capture. Note that instantiation list entries that do not apply are simply ignored, as are repeated entries for a given variable (beyond its first entry). If no instantiation list entries apply, then the returned theorem is the same as the input. [(x1,t1);(x2,t2);..] A |- p -------------------------------------- A[t1/x1,t2/x2,..] |- p[t1/x1,t2/x2,..] See also: inst_type_rule, subs_rule, subst_rule.

This is the type variable instantiation rule. It takes a type variable instantiation list and a theorem, and performs a single parallel instantiation of the type variables in the theorem's assumptions and conclusion, according to the instantiation list. All occurrences of instantiation list domain elements in the theorem get replaced. Each instantiation list domain element must be a type variable. Binding variables in the resulting theorem are renamed as necessary to avoid variable capture. Note that instantiation list entries that do not apply are simply ignored, as are repeated entries for a given type variable (beyond its first entry). If no instantiation list entries apply, then the returned theorem is the same as the input. [(tv1,ty1);(tv2,ty2);..] A |- p ---------------------------------------------- A[ty1/tv1,ty2/tv2,..] |- p[ty1/tv1,ty2/tv2,..] See also: inst_rule.

This is the equality congruence rule for lambda abstraction. It takes a variable and an equality theorem, and abstracts the variable from both sides of the theorem. The variable must not occur free in the assumptions of the supplied theorem. `x` A |- t1 = t2 [ "x" not free in 'A' ] ------------------------ A |- (\x. t1) = (\x. t2) See also: mk_comb_rule.

mk_comb_rule : thm -> thm -> thm [ Primitive ] This is the equality congruence rule for function application. It takes two equality theorems, and applies corresponding sides of the first theorem to the second, unioning the assumptions. The first theorem's LHS/RHS must be functions with domain type equal to the type of the second theorem's LHS/RHS. A1 |- f1 = f2 A2 |- t1 = t2 ------------------------------ A1 u A2 |- f1 t1 = f2 t2 See also: mk_comb1_rule, mk_comb2_rule, mk_bin_rule, mk_abs_rule.

This is the modus ponens rule. It takes an implication theorem and a second theorem, where the implication theorem's antecedent is alpha-equivalent to the conclusion of the second theorem. It returns a theorem stating that the implication theorem's consequent holds, under the unioned assumptions of the supplied theorems. A1 |- p ==> q A2 |- p ------------------------ A1 u A2 |- q See also: eq_mp_rule, disch_rule, undisch_rule, prove_asm_rule.

This is the reflexivity rule for equality. It takes a term, and returns a theorem stating that this term is equal to itself, under no assumptions. There are no restrictions on the supplied term. `t` -------- |- t = t See also: eq_sym_conv, eq_sym_rule, eq_trans_rule.