The text for most sessions in chapter 4 appears below, where the sessions in the tutorial are enclosed in boxes and labelled in the upper right hand corner.
- val th1 = BOOL_CASES_AX; val th1 = |- !t. (t = T) \/ (t = F) : thm - val th2 = SPEC (--`1=2`--) th1; val th2 = |- ((1 = 2) = T) \/ ((1 = 2) = F) : thm
- SPEC (--`1=2`--) th2; uncaught exception HOL_ERR - SPEC (--`1`--) th1; uncaught exception HOL_ERR
- val th3 = ASSUME (--`t1 ==> t2`--); val th3 = . |- t1 ==> t2 : thm - dest_thm th3; val it = ([(--`t1 ==> t2`--)],(--`t1 ==> t2`--)) : term list * term
- val th4 = DISCH (--`t1=>t2`--) th3; HOL parser error: syntax error Exception raised at Parse.first pass of parsing: syntax error uncaught exception HOL_ERR - val th4 = DISCH (--`t1==>t2`--) th3; val th4 = |- (t1 ==> t2) ==> t1 ==> t2 : thm
- DISCH (--`1=2`--) th3; val it = . |- (1 = 2) ==> t1 ==> t2 : thm - dest_thm it; val it = ([(--`t1 ==> t2`--)],(--`(1 = 2) ==> t1 ==> t2`--)) : term list * term
- val th5 = ASSUME (--`t1`--); Unconstrained type variable in the variable (t1 :?1) Exception raised at Preterm.typecheck_cleanup: uncaught exception HOL_ERR - val th5 = ASSUME (--`t1:bool`--); val th5 = . |- t1 : thm - val th6 = MP th3 th5; val th6 = .. |- t2 : thm
- hyp th6; val it = [(--`t1 ==> t2`--),(--`t1`--)] : term list
- Globals.show_assums := true; val it = () : unit - th5; val it = [t1] |- t1 : thm - th6; val it = [t1 ==> t2, t1] |- t2 : thmNote: typing "open Globals;" (no quotation marks) will give you a list of assignable flags in the system.
- val th7 = DISCH (--`t1==>t2`--) th6; val th7 = [t1] |- (t1 ==> t2) ==> t2 : thm - val th8 = DISCH (--`t1:bool`--) th7; val th8 = |- t1 ==> (t1 ==> t2) ==> t2 : thm
val th9 = [t3] |- t3 : thm - val th10 = DISCH (--`t3:bool`--) th6; val th10 = [t1 ==> t2, t1] |- t3 ==> t2 : thm - val th11 = MP th10 th9; val th11 = [t1, t1 ==> t2, t3] |- t2 : thm
- fun ADD_ASSUM t th = = let val th9 = ASSUME t = in = let val th10 = DISCH t th = in = MP th10 th9 = end = end = ; val ADD_ASSUM = fn : term -> thm -> thm - ADD_ASSUM (--`t3:bool`--) th6; val it = [t1, t1 ==> t2, t3] |- t2 : thm
- fun ADD_ASSUM t th = MP (DISCH t th) (ASSUME t); val ADD_ASSUM = fn : term -> thm -> thm - ADD_ASSUM (--`t3:bool`--) th6; val it = [t1, t1 ==> t2, t3] |- t2 : thm
- fun UNDISCH th = = MP th (ASSUME(#ant(dest_imp(concl th)))); val UNDISCH = fn : thm -> thm - th10; val it = [t1 ==> t2, t1] |- t3 ==> t2 : thm - UNDISCH th10; val it = [t1, t1 ==> t2, t3] |- t2 : thm - it = th11; val it = true : bool
add_theory_to_sml "arithmetic";Information about libraries in HOL90 can be found in doc/library.doc in the distribution. The names of the pre-existing theories can be found by looking in theories/ascii in the distribution.
- val rewrite_list = [ADD_CLAUSES,MULT_CLAUSES]; val rewrite_list = [|- (0 + m = m) /\ (m + 0 = m) /\ (SUC m + n = SUC (m + n)) /\ (m + SUC n = SUC (m + n)), |- !m n. (0 * m = 0) /\ (m * 0 = 0) /\ (1 * m = m) /\ (m * 1 = m) /\ (SUC m * n = m * n + n) /\ (m * SUC n = m + m * n)] : thm list
- REWRITE_RULE rewrite_list (ASSUME (--`(m+0)<(1*n)+(SUC 0)`--)); val it = [m + 0 < 1 * n + SUC 0] |- m < SUC n : thm
- add_theory_to_sml "prim_rec"; val num_Axiom = |- !e f. ?!fn1. (fn1 0 = e) /\ (!n. fn1 (SUC n) = f (fn1 n) n) : thm val PRE = |- (PRE 0 = 0) /\ (!m. PRE (SUC m) = m) : thm val LESS_SUC_SUC = |- !m. m < SUC m /\ m < SUC (SUC m) : thm val LESS_NOT_EQ = |- !m n. m < n ==> ~(m = n) : thm val NOT_LESS_EQ = |- !m n. (m = n) ==> ~(m < n) : thm val SUC_ID = |- !n. ~(SUC n = n) : thm val EQ_LESS = |- !n. (SUC m = n) ==> m < n : thm val LESS_0 = |- !n. 0 < SUC n : thm val LESS_SUC_IMP = |- !m n. m < SUC n ==> ~(m = n) ==> m < n : thm val LESS_THM = |- !m n. m < SUC n = (m = n) \/ m < n : thm val LESS_SUC = |- !m n. m < n ==> m < SUC n : thm val LESS_SUC_REFL = |- !n. n < SUC n : thm val LESS_MONO = |- !m n. m < n ==> SUC m < SUC n : thm val NOT_LESS_0 = |- !n. ~(n < 0) : thm val SUC_LESS = |- !m n. SUC m < n ==> m < n : thm val LESS_REFL = |- !n. ~(n < n) : thm val INV_SUC_EQ = |- !m n. (SUC m = SUC n) = m = n : thm val it = () : unit - REWRITE_RULE rewrite_list (ASSUME (--`(m+0)<(1*n)+(SUC 0)`--)); val it = [m + 0 < 1 * n + SUC 0] |- m < SUC n : thm - REWRITE_RULE [LESS_THM] it; val it = [m + 0 < 1 * n + SUC 0] |- (m = n) \/ m < n : thm
- REWRITE_RULE [] (ASSUME (--`(T /\ x) \/ F ==> F`--)); val it = [T /\ x \/ F ==> F] |- ~x : thm
- HOLdir; val it = ref "/usr/local/hol/hol90.6/" : string ref
- load_library{lib = Sys_lib.taut_lib, theory = "foo"};Read doc/library.doc in the documentation for more information as to what load_library does.