(* ===================================================================== *) (* FILE : boolScript.sml *) (* DESCRIPTION : Definition of the logical constants and assertion of *) (* the axioms. *) (* AUTHORS : (c) Mike Gordon, University of Cambridge *) (* Tom Melham, Richard Boulton, John Harrison, *) (* Konrad Slind, Michael Norrish, Jim Grundy, Joe Hurd *) (* and probably others that don't immediately come to *) (* mind. *) (* ===================================================================== *) open HolKernel Parse open Unicode TexTokenMap val _ = new_theory "bool"; (*---------------------------------------------------------------------------* * BASIC DEFINITIONS * *---------------------------------------------------------------------------*) (* parsing/printing support for theory min *) val _ = unicode_version {u = UChar.imp, tmnm = "==>"} val _ = TeX_notation {hol = "==>", TeX = ("\\HOLTokenImp{}", 1)} val _ = TeX_notation {hol = UChar.imp, TeX = ("\\HOLTokenImp{}", 1)} val _ = TeX_notation {hol = "\\", TeX = ("\\HOLTokenLambda{}", 1)} val _ = TeX_notation {hol = UChar.lambda, TeX = ("\\HOLTokenLambda{}", 1)} val _ = TeX_notation {hol = "@", TeX = ("\\HOLTokenHilbert{}", 1)} (* iff *) val _ = overload_on ("<=>", “(=) : bool -> bool -> bool”) val _ = set_fixity "<=>" (Infix(NONASSOC, 100)) val _ = unicode_version {u = UChar.iff, tmnm = "<=>"} val _ = TeX_notation {hol = "<=>", TeX = ("\\HOLTokenEquiv{}",3)} val _ = TeX_notation {hol = UChar.iff, TeX = ("\\HOLTokenEquiv{}",3)} (* records *) val _ = TeX_notation {hol = "<|", TeX = ("\\HOLTokenLeftrec{}", 2)} val _ = TeX_notation {hol = "|>", TeX = ("\\HOLTokenRightrec{}", 2)} (* case expressions *) val _ = TeX_notation {hol = "case", TeX = ("\\HOLKeyword{case}", 4)} val _ = TeX_notation {hol = "of", TeX = ("\\HOLKeyword{of}", 2)} val _ = TeX_notation {hol = "=>", TeX = ("\\HOLTokenImp{}", 1)} (* let expressions *) val _ = TeX_notation {hol = "let", TeX = ("\\HOLKeyword{let}", 3)} val _ = TeX_notation {hol = "and", TeX = ("\\HOLKeyword{and}", 2)} val _ = TeX_notation {hol = "in", TeX = ("\\HOLKeyword{in}", 2)} (* if statements *) val _ = TeX_notation {hol = "if", TeX = ("\\HOLKeyword{if}", 2)} val _ = TeX_notation {hol = "then", TeX = ("\\HOLKeyword{then}", 4)} val _ = TeX_notation {hol = "else", TeX = ("\\HOLKeyword{else}", 4)} (* type syntax *) val _ = TeX_notation {hol = "->", TeX = ("\\HOLTokenMap{}", 1)} val _ = TeX_notation {hol = "'a", TeX = ("\\alpha{}", 1)} val _ = TeX_notation {hol = "'b", TeX = ("\\beta{}", 1)} val _ = TeX_notation {hol = "'c", TeX = ("\\gamma{}", 1)} val _ = TeX_notation {hol = "'d", TeX = ("\\delta{}", 1)} val _ = TeX_notation {hol = "'e", TeX = ("\\epsilon{}", 1)} (* past this point the Greek letters are likely to be more confusing than helpful *) fun mkloc(s,n) = DB_dtype.mkloc(s,n,true) fun def l (n,t) = Definition.located_new_definition {loc=mkloc l,name=n,def=t} fun thm l (n,th) = Theory.gen_save_thm{loc=mkloc l,name=n,private=false,thm=th} fun ax l (n,t) = Theory.gen_new_axiom(n,t,mkloc l) val T_DEF = def (#(FILE),#(LINE)) ("T_DEF", “T = ((\x:bool. x) = \x:bool. x)”); val FORALL_DEF = def (#(FILE), #(LINE)) ("FORALL_DEF", “! = \P:'a->bool. P = \x. T”) val _ = set_fixity "!" Binder val _ = unicode_version {u = UChar.forall, tmnm = "!"}; val _ = TeX_notation {hol = "!", TeX = ("\\HOLTokenForall{}",1)} val _ = TeX_notation {hol = UChar.forall, TeX = ("\\HOLTokenForall{}",1)} val EXISTS_DEF = def (#(FILE), #(LINE)) ("EXISTS_DEF", “? = \P:'a->bool. P ($@ P)”); val _ = set_fixity "?" Binder val _ = unicode_version {u = UChar.exists, tmnm = "?"} val _ = TeX_notation {hol = "?", TeX = ("\\HOLTokenExists{}",1)} val _ = TeX_notation {hol = UChar.exists, TeX = ("\\HOLTokenExists{}",1)} val AND_DEF = def (#(FILE), #(LINE)) ("AND_DEF", “/\ = \t1 t2. !t. (t1 ==> t2 ==> t) ==> t”); val _ = set_fixity "/\\" (Infixr 400); val _ = unicode_version {u = UChar.conj, tmnm = "/\\"}; val _ = TeX_notation {hol = "/\\", TeX = ("\\HOLTokenConj{}",1)} val _ = TeX_notation {hol = UChar.conj, TeX = ("\\HOLTokenConj{}",1)} val OR_DEF = def (#(FILE), #(LINE)) ("OR_DEF", “\/ = \t1 t2. !t. (t1 ==> t) ==> (t2 ==> t) ==> t”) val _ = set_fixity "\\/" (Infixr 300) val _ = unicode_version {u = UChar.disj, tmnm = "\\/"} val _ = TeX_notation {hol = "\\/", TeX = ("\\HOLTokenDisj{}",1)} val _ = TeX_notation {hol = UChar.disj, TeX = ("\\HOLTokenDisj{}",1)} val F_DEF = def (#(FILE), #(LINE)) ("F_DEF", “F = !t. t”); val NOT_DEF = def (#(FILE), #(LINE)) ("NOT_DEF", “~ = \t. t ==> F”); (* now allows parsing of not equal *) val _ = overload_on ("<>", “\x:'a y:'a. ~(x = y)”) val _ = set_fixity "<>" (Infix(NONASSOC, 450)) val _ = TeX_notation {hol="<>", TeX = ("\\HOLTokenNotEqual{}",1)} val _ = set_fixity UChar.neq (Infix(NONASSOC, 450)) val _ = overload_on (UChar.neq, “\x:'a y:'a. ~(x = y)”) val _ = TeX_notation {hol=UChar.neq, TeX = ("\\HOLTokenNotEqual{}",1)} val EXISTS_UNIQUE_DEF = def (#(FILE), #(LINE)) ("EXISTS_UNIQUE_DEF", “?! = \P:'a->bool. $? P /\ !x y. P x /\ P y ==> (x=y)”); val _ = set_fixity "?!" Binder val _ = unicode_version { u = UChar.exists ^ "!", tmnm = "?!"} val _ = TeX_notation {hol = "?!", TeX = ("\\HOLTokenUnique{}",2)} val _ = TeX_notation {hol = UChar.exists ^ "!", TeX = ("\\HOLTokenUnique{}",2)} val LET_DEF = def (#(FILE), #(LINE)) ("LET_DEF", “LET = λ(f:'a->'b) x. f x”); val COND_DEF = def (#(FILE), #(LINE)) ("COND_DEF", “COND = \t t1 t2. @x:'a. ((t=T) ==> (x=t1)) /\ ((t=F) ==> (x=t2))”); val _ = overload_on ("case", “COND”) val ONE_ONE_DEF = def (#(FILE), #(LINE)) ("ONE_ONE_DEF", “ONE_ONE = \f:'a->'b. !x1 x2. (f x1 = f x2) ==> (x1 = x2)”); val ONTO_DEF = def (#(FILE), #(LINE)) ("ONTO_DEF", “ONTO = \f:'a->'b. !y. ?x. y = f x”); val TYPE_DEFINITION = def (#(FILE), #(LINE)) ("TYPE_DEFINITION", “TYPE_DEFINITION = \P:'a->bool. \rep:'b->'a. (!x' x''. (rep x' = rep x'') ==> (x' = x'')) /\ (!x. P x = (?x'. x = rep x'))”); (*---------------------------------------------------------------------------* * Parsing directives for some of the basic operators. * *---------------------------------------------------------------------------*) open Portable; Overload "~" = “~” Overload "¬" = “~” val _ = add_rule {term_name = "~", fixity = Prefix 900, pp_elements = [TOK "~"], paren_style = OnlyIfNecessary, block_style = (AroundEachPhrase, (CONSISTENT, 0))}; val _ = add_rule {term_name = UChar.neg, fixity = Prefix 900, pp_elements = [TOK UChar.neg], paren_style = OnlyIfNecessary, block_style = (AroundEachPhrase, (CONSISTENT, 0))}; val _ = TeX_notation {hol = "~", TeX = ("\\HOLTokenNeg{}",1)} val _ = TeX_notation {hol = UChar.neg, TeX = ("\\HOLTokenNeg{}",1)} (* prettyprinting information here for "let" and "and" is completely ignored; the pretty-printer handles these specially. These declarations are only for the parser's benefit. *) val _ = add_rule { pp_elements = [TOK "let", ListForm { separator = [TOK ";"], cons = GrammarSpecials.letcons_special, nilstr = GrammarSpecials.letnil_special, block_info = (INCONSISTENT, 0) }, TOK "in"], term_name = GrammarSpecials.let_special, paren_style = OnlyIfNecessary, fixity = Prefix 8, block_style = (AroundEachPhrase, (CONSISTENT, 0))}; val _ = add_rule {term_name = GrammarSpecials.and_special, fixity = Infixl 9, pp_elements = [TOK "and"], paren_style = OnlyIfNecessary, block_style = (AroundEachPhrase, (INCONSISTENT, 0))} val _ = add_rule{term_name = "COND", fixity = Prefix 70, pp_elements = [PPBlock([TOK "if", BreakSpace(1,2), TM, BreakSpace(1,0), TOK "then"], (CONSISTENT, 0)), BreakSpace(1,2), TM, BreakSpace(1,0), TOK "else", BreakSpace(1,2)], paren_style = OnlyIfNecessary, block_style = (AroundEachPhrase, (CONSISTENT, 0))}; (*---------------------------------------------------------------------------* * AXIOMS * * * * Bruno Barras noticed that the axiom IMP_ANTISYM_AX from the original * * HOL logic was provable. * *---------------------------------------------------------------------------*) val BOOL_CASES_AX = ax(#(FILE), #(LINE)) ("BOOL_CASES_AX", “!t. (t=T) \/ (t=F)”); val ETA_AX = ax(#(FILE), #(LINE)) ("ETA_AX", “!t:'a->'b. (\x. t x) = t”); val SELECT_AX = ax(#(FILE), #(LINE)) ("SELECT_AX", “!(P:'a->bool) x. P x ==> P ($@ P)”); val INFINITY_AX = ax(#(FILE), #(LINE)) ("INFINITY_AX", “?f:ind->ind. ONE_ONE f /\ ~ONTO f”); (*---------------------------------------------------------------------------* * Miscellaneous utility definitions, of use in some packages. * *---------------------------------------------------------------------------*) val arb = new_constant("ARB",alpha); (* Doesn't have to be defined at all. *) val literal_case_DEF = def (#(FILE), #(LINE)) ("literal_case_DEF", “literal_case = λ(f:'a->'b) x. f x”); val _ = overload_on ("case", “bool$literal_case”); val IN_DEF = def (#(FILE), #(LINE)) ("IN_DEF", “IN = \x (f:'a->bool). f x”); val _ = set_fixity "IN" (Infix(NONASSOC, 425)) val _ = unicode_version {u = UChar.setelementof, tmnm = "IN"}; val _ = TeX_notation {hol = "IN", TeX = ("\\HOLTokenIn{}",1)} val _ = TeX_notation {hol = UChar.setelementof, TeX = ("\\HOLTokenIn{}",1)} val RES_FORALL_DEF = def (#(FILE), #(LINE)) ("RES_FORALL_DEF", “RES_FORALL = \p m. !x : 'a. x IN p ==> m x”); val _ = associate_restriction ("!", "RES_FORALL") val RES_EXISTS_DEF = def (#(FILE), #(LINE)) ("RES_EXISTS_DEF", “RES_EXISTS = \p m. ?x : 'a. x IN p /\ m x”); val _ = associate_restriction ("?", "RES_EXISTS") val RES_EXISTS_UNIQUE_DEF = def (#(FILE), #(LINE)) ("RES_EXISTS_UNIQUE_DEF", “RES_EXISTS_UNIQUE = \p m. (?(x : 'a) :: p. m x) /\ !x y :: p. m x /\ m y ==> (x = y)”); val _ = associate_restriction ("?!", "RES_EXISTS_UNIQUE"); val RES_SELECT_DEF = def (#(FILE), #(LINE)) ("RES_SELECT_DEF", “RES_SELECT = \p m. @x : 'a. x IN p /\ m x”); val _ = associate_restriction ("@", "RES_SELECT") (* Note: RES_ABSTRACT comes later, defined by new_specification *) (*---------------------------------------------------------------------------*) (* Experimental rewriting directives *) (*---------------------------------------------------------------------------*) val BOUNDED_DEF = def (#(FILE), #(LINE)) ("BOUNDED_DEF", “BOUNDED = λ(v:bool). T”); (*---------------------------------------------------------------------------*) (* Support for detecting datatypes in theory files *) (*---------------------------------------------------------------------------*) val DATATYPE_TAG_DEF = def (#(FILE), #(LINE)) ("DATATYPE_TAG_DEF", “DATATYPE = \x. T”); (*---------------------------------------------------------------------------* * THEOREMS * *---------------------------------------------------------------------------*) val op --> = Type.--> val ERR = Feedback.mk_HOL_ERR "boolScript" val F = “F” val T = “T”; val implication = prim_mk_const{Name="==>", Thy="min"} val select = prim_mk_const{Name="@", Thy="min"} val conjunction = prim_mk_const{Name="/\\", Thy="bool"} val disjunction = prim_mk_const{Name="\\/", Thy="bool"} val negation = prim_mk_const{Name="~", Thy="bool"} val universal = prim_mk_const{Name="!", Thy="bool"} val existential = prim_mk_const{Name="?", Thy="bool"} val exists1 = prim_mk_const{Name="?!", Thy="bool"} val in_tm = prim_mk_const{Name="IN", Thy="bool"}; val dest_neg = sdest_monop("~","bool") (ERR"dest_neg" ""); val dest_eq = sdest_binop("=","min") (ERR"dest_eq" ""); val dest_disj = sdest_binop("\\/","bool") (ERR"dest_disj" ""); val dest_conj = sdest_binop("/\\","bool") (ERR"dest_conj" ""); val dest_forall = sdest_binder("!","bool") (ERR"dest_forall" ""); val dest_exists = sdest_binder("?","bool") (ERR"dest_exists" ""); fun strip_forall fm = if can dest_forall fm then let val (Bvar,Body) = dest_forall fm val (bvs,core) = strip_forall Body in ((Bvar::bvs), core) end else ([],fm); val lhs = fst o dest_eq; val rhs = snd o dest_eq; local val imp = “$==>” val notc = “$~” in fun dest_imp M = let val (Rator,conseq) = dest_comb M in if is_comb Rator then let val (Rator,ant) = dest_comb Rator in if aconv Rator imp then (ant,conseq) else raise Fail "dest_imp" end else if aconv Rator notc then (conseq,F) else raise Fail "dest_imp" end end fun mk_neg M = “~^M”; fun mk_eq(lhs,rhs) = “^lhs = ^rhs”; fun mk_imp(ant,conseq) = “^ant ==> ^conseq”; fun mk_conj(conj1,conj2) = “^conj1 /\ ^conj2”; fun mk_disj(disj1,disj2) = “^disj1 \/ ^disj2”; fun mk_forall(Bvar,Body) = “!^Bvar. ^Body” fun mk_exists(Bvar,Body) = “?^Bvar. ^Body” fun mk_exists1(Bvar,Body) = “?!^Bvar. ^Body” val list_mk_forall = itlist (curry mk_forall) val list_mk_exists = itlist (curry mk_exists) (* also implemented in Drule *) fun ETA_CONV t = let val (var, cmb) = dest_abs t val tysubst = [alpha |-> type_of var, beta |-> type_of cmb] val th = SPEC (rator cmb) (INST_TYPE tysubst ETA_AX) in TRANS (ALPHA t (lhs (concl th))) th end; fun EXT th = let val (Bvar,_) = dest_forall(concl th) val th1 = SPEC Bvar th val (t1x, t2x) = dest_eq(concl th1) val x = rand t1x val th2 = ABS x th1 in TRANS (TRANS(SYM(ETA_CONV (mk_abs(x, t1x)))) th2) (ETA_CONV (mk_abs(x,t2x))) end; fun DISCH_ALL th = DISCH_ALL (DISCH (hd (hyp th)) th) handle _ => th; fun PROVE_HYP ath bth = MP (DISCH (concl ath) bth) ath; fun CONV_RULE conv th = EQ_MP (conv(concl th)) th; fun RAND_CONV conv tm = let val (Rator,Rand) = dest_comb tm in AP_TERM Rator (conv Rand) end; fun RATOR_CONV conv tm = let val (Rator,Rand) = dest_comb tm in AP_THM (conv Rator) Rand end; fun ABS_CONV conv tm = let val (Bvar,Body) = dest_abs tm in ABS Bvar (conv Body) end; fun QUANT_CONV conv = RAND_CONV(ABS_CONV conv); fun RIGHT_BETA th = TRANS th (BETA_CONV(snd(dest_eq(concl th)))); fun UNDISCH th = MP th (ASSUME(fst(dest_imp(concl th)))); fun FALSITY_CONV tm = DISCH F (SPEC tm (EQ_MP F_DEF (ASSUME F))) fun UNFOLD_OR_CONV tm = let val (disj1,disj2) = dest_disj tm in RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM OR_DEF disj1)) disj2) end; (* common variables used throughout what follows *) fun Av s = mk_var(s, alpha) fun Bv s = mk_var(s, bool) val tb = Bv "t" val t1b = Bv "t1" val t2b = Bv "t2" val Pb = Bv "P" val Qb = Bv "Q" val Pab = mk_var("P", alpha --> bool) val Qab = mk_var("Q", alpha --> bool) val fabt = mk_var("f", alpha --> beta) val xa = Av "x" val ya = Av "y" (*--------------------------------------------------------------------------- * |- T *---------------------------------------------------------------------------*) val TRUTH = thm (#(FILE),#(LINE)) ("TRUTH", EQ_MP (SYM T_DEF) (REFL “\x:bool. x”)); fun EQT_ELIM th = EQ_MP (SYM th) TRUTH; (* SPEC could be built here. *) (* GEN could be built here. *) (* auxiliary functions to do bool case splitting *) (* maps thm |- P[x\t] to |- y=t ==> P[x\y] *) fun CUT_EQUAL P x y t thm = let val e = mk_eq(y,t) in DISCH e (SUBST [(x|->SYM (ASSUME e))] P thm) end; (* given proofs of P[x\T] and P[x\F], proves P[x\t] *) fun BOOL_CASE P x t pt pf = let val th0 = SPEC t BOOL_CASES_AX val th1 = EQ_MP (UNFOLD_OR_CONV (concl th0)) th0 val th2 = SPEC (subst[(x|->t)] P) th1 in MP (MP th2 (CUT_EQUAL P x t T pt)) (CUT_EQUAL P x t F pf) end; fun EQT_INTRO th = let val t = concl th val x = genvar bool in BOOL_CASE “^x=T” x t (REFL T) (MP (FALSITY_CONV “F=T”) (EQ_MP (ASSUME“^t=F”) th)) end; (*--------------------------------------------------------------------------- * |- !t1 t2. (t1 ==> t2) ==> (t2 ==> t1) ==> (t1 = t2) *---------------------------------------------------------------------------*) infixr ==> val op==> = mk_imp infix == val op== = mk_eq val IMP_ANTISYM_AX = thm (#(FILE), #(LINE))( "IMP_ANTISYM_AX", let fun dsch t1 t2 th = DISCH (t2 ==> t1) (DISCH (t1 ==> t2) th) fun sch t1 t2 = (t1==>t2) ==> (t2==>t1) ==> (t1 == t2) val abs = MP (FALSITY_CONV (F == T)) (MP (ASSUME (T ==> F)) TRUTH) val tht = BOOL_CASE (sch T t2b) t2b t2b (dsch T T (REFL T)) (dsch F T (SYM abs)) val thf = BOOL_CASE (sch F t2b) t2b t2b (dsch T F abs) (dsch F F (REFL F)) in GEN t1b (GEN t2b (BOOL_CASE (sch t1b t2b) t1b t1b tht thf)) end); fun IMP_ANTISYM_RULE th1 th2 = let val (ant,conseq) = dest_imp(concl th1) in MP (MP (SPEC conseq (SPEC ant IMP_ANTISYM_AX)) th1) th2 end; (*--------------------------------------------------------------------------- * |- !t. F ==> t *---------------------------------------------------------------------------*) val FALSITY = thm (#(FILE), #(LINE))("FALSITY", GEN tb (FALSITY_CONV tb)) fun CONTR tm th = MP (SPEC tm FALSITY) th fun DISJ_IMP dth = let val (disj1,disj2) = dest_disj (concl dth) val nota = mk_neg disj1 in DISCH nota (DISJ_CASES dth (CONTR disj2 (MP (ASSUME nota) (ASSUME disj1))) (ASSUME disj2)) end fun EQF_INTRO th = IMP_ANTISYM_RULE (NOT_ELIM th) (DISCH “F” (CONTR (dest_neg (concl th)) (ASSUME “F”))); fun SELECT_EQ x = let val ty = type_of x val choose = mk_const("@", (ty --> Type.bool) --> ty) in fn th => AP_TERM choose (ABS x th) end fun GENL varl thm = itlist GEN varl thm; fun SPECL tm_list th = rev_itlist SPEC tm_list th fun GEN_ALL th = itlist GEN (op_set_diff aconv (free_vars(concl th)) (free_varsl (hyp th))) th; local fun f v (vs,l) = let val v' = variant vs v in (v'::vs, v'::l) end in fun SPEC_ALL th = let val (hvs,con) = (free_varsl ## I) (hyp th, concl th) val fvs = free_vars con and vars = fst(strip_forall con) in SPECL (snd(itlist f vars (hvs@fvs,[]))) th end end; fun SUBST_CONV theta template tm = let fun retheta {redex,residue} = (redex |-> genvar(type_of redex)) val theta0 = map retheta theta val theta1 = map (op |-> o (#residue ## #residue)) (zip theta0 theta) in SUBST theta1 (mk_eq(tm,subst theta0 template)) (REFL tm) end; local fun combine [] [] = [] | combine (v::rst1) (t::rst2) = (v |-> t) :: combine rst1 rst2 | combine _ _ = raise Fail "SUBS" in fun SUBS ths th = let val ls = map (lhs o concl) ths val vars = map (genvar o type_of) ls val w = subst (combine ls vars) (concl th) in SUBST (combine vars ths) w th end end; fun IMP_TRANS th1 th2 = let val (ant,conseq) = dest_imp(concl th1) in DISCH ant (MP th2 (MP th1 (ASSUME ant))) end; fun ADD_ASSUM t th = MP (DISCH t th) (ASSUME t); fun SPEC_VAR th = let val (Bvar,_) = dest_forall (concl th) val bv' = variant (free_varsl (hyp th)) Bvar in (bv', SPEC bv' th) end; fun MK_EXISTS bodyth = let val (x, sth) = SPEC_VAR bodyth val (a,b) = dest_eq (concl sth) val (abimp,baimp) = EQ_IMP_RULE sth fun HALF (p,q) pqimp = let val xp = mk_exists(x,p) and xq = mk_exists(x,q) in DISCH xp (CHOOSE (x, ASSUME xp) (EXISTS (xq,x) (MP pqimp (ASSUME p)))) end in IMP_ANTISYM_RULE (HALF (a,b) abimp) (HALF (b,a) baimp) end; fun SELECT_RULE th = let val (tm as (Bvar, Body)) = dest_exists(concl th) val v = genvar(type_of Bvar) val P = mk_abs tm val SELECT_AX' = INST_TYPE[alpha |-> type_of Bvar] SELECT_AX val th1 = SPEC v (SPEC P SELECT_AX') val (ant,conseq) = dest_imp(concl th1) val th2 = BETA_CONV ant and th3 = BETA_CONV conseq val th4 = EQ_MP th3 (MP th1 (EQ_MP(SYM th2) (ASSUME (rhs(concl th2))))) in CHOOSE (v,th) th4 end; (*--------------------------------------------------------------------------- ETA_THM = |- !M. (\x. M x) = M ---------------------------------------------------------------------------*) val ETA_THM = thm (#(FILE), #(LINE)) ("ETA_THM", GEN_ALL(ETA_CONV “\x:'a. (M x:'b)”)); (*--------------------------------------------------------------------------- * |- !t. t \/ ~t *---------------------------------------------------------------------------*) val EXCLUDED_MIDDLE = thm (#(FILE), #(LINE))( "EXCLUDED_MIDDLE", let val th1 = RIGHT_BETA(AP_THM NOT_DEF tb) val th2 = DISJ1 (EQT_ELIM (ASSUME (tb == T))) (mk_neg tb) and th3 = DISJ2 tb (EQ_MP (SYM th1) (DISCH tb (EQ_MP (ASSUME (tb == F)) (ASSUME tb)))) in GEN tb (DISJ_CASES (SPEC tb BOOL_CASES_AX) th2 th3) end) fun IMP_ELIM th = let val (ant,conseq) = dest_imp (concl th) val not_t1 = mk_neg ant in DISJ_CASES (SPEC ant EXCLUDED_MIDDLE) (DISJ2 not_t1 (MP th (ASSUME ant))) (DISJ1 (ASSUME not_t1) conseq) end; (*---------------------------------------------------------------------------* * |- !f y. (\x. f x) y = f y * *---------------------------------------------------------------------------*) val BETA_THM = thm (#(FILE), #(LINE))( "BETA_THM", GENL [fabt, ya] (BETA_CONV “(\x. (f:'a->'b) x) y”)) (*--------------------------------------------------------------------------- LET_THM = |- !f x. LET f x = f x ---------------------------------------------------------------------------*) val LET_THM = thm (#(FILE), #(LINE))( "LET_THM", GEN fabt (GEN xa (RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM LET_DEF fabt)) xa)))) (* |- $! f <=> !x. f x *) val FORALL_THM = thm (#(FILE), #(LINE))( "FORALL_THM", SYM (AP_TERM “$! :('a->bool)->bool” (ETA_CONV “\x:'a. f x:bool”))) (* |- $? f <=> ?x. f x *) val EXISTS_THM = thm (#(FILE), #(LINE))( "EXISTS_THM", SYM (AP_TERM “$? :('a->bool)->bool” (ETA_CONV “\x:'a. f x:bool”))); (*---------------------------------------------------------------------------* * |- !t1:'a. !t2:'b. (\x. t1) t2 = t1 * *---------------------------------------------------------------------------*) val ABS_SIMP = thm (#(FILE), #(LINE))("ABS_SIMP", GENL [“t1:'a”, “t2:'b”] (BETA_CONV “(\x:'b. t1:'a) t2”)); (*--------------------------------------------------------------------------- * |- !t. (!x.t) = t *---------------------------------------------------------------------------*) val FORALL_SIMP = thm (#(FILE), #(LINE))( "FORALL_SIMP", GEN tb (IMP_ANTISYM_RULE (DISCH “!^xa. ^tb” (SPEC xa (ASSUME “!^xa.^tb”))) (DISCH tb (GEN xa (ASSUME tb))))); (*--------------------------------------------------------------------------- * |- !t. (?x.t) = t *---------------------------------------------------------------------------*) val EXISTS_SIMP = thm (#(FILE), #(LINE))( "EXISTS_SIMP", let val ext = mk_exists(xa,tb) in GEN tb (IMP_ANTISYM_RULE (DISCH ext (CHOOSE(Av "p", ASSUME ext) (ASSUME tb))) (DISCH tb (EXISTS(ext, Av "r") (ASSUME tb)))) end); (*--------------------------------------------------------------------------- * |- !t1 t2. t1 ==> t2 ==> t1 /\ t2 *---------------------------------------------------------------------------*) val AND_INTRO_THM = thm (#(FILE), #(LINE))( "AND_INTRO_THM", let val t12 = t1b ==> t2b ==> tb val th1 = GEN tb (DISCH t12 (MP (MP (ASSUME t12) (ASSUME t1b)) (ASSUME t2b))) val th2 = RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM AND_DEF t1b)) t2b) in GEN t1b (GEN t2b (DISCH t1b (DISCH t2b (EQ_MP (SYM th2) th1)))) end); (*--------------------------------------------------------------------------- * |- !t1 t2. t1 /\ t2 ==> t1 *---------------------------------------------------------------------------*) val AND1_THM = thm (#(FILE), #(LINE))( "AND1_THM", let val t12 = mk_conj(t1b, t2b) val th2 = RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM AND_DEF t1b)) t2b) val th3 = SPEC t1b (EQ_MP th2 (ASSUME t12)) val th4 = DISCH t1b (DISCH t2b (ADD_ASSUM t2b (ASSUME t1b))) in GEN t1b (GEN t2b (DISCH t12 (MP th3 th4))) end); (*--------------------------------------------------------------------------- * |- !t1 t2. t1 /\ t2 ==> t2 *---------------------------------------------------------------------------*) val AND2_THM = thm (#(FILE), #(LINE))("AND2_THM", let val t1 = “t1:bool” and t2 = “t2:bool” val th1 = ASSUME “^t1 /\ ^t2” val th2 = RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM AND_DEF t1)) t2) val th3 = SPEC t2 (EQ_MP th2 th1) val th4 = DISCH t1 (DISCH t2 (ADD_ASSUM t1 (ASSUME t2))) in GEN t1 (GEN t2 (DISCH “^t1 /\ ^t2” (MP th3 th4))) end); (* CONJ, CONJUNCT1 and CONJUNCT2 should be built here.*) fun CONJ_PAIR thm = (CONJUNCT1 thm, CONJUNCT2 thm); fun CONJUNCTS th = (CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th)) handle _ => [th]; val LIST_CONJ = end_itlist CONJ (*--------------------------------------------------------------------------- * |- !t1 t2. (t1 /\ t2) = (t2 /\ t1) *---------------------------------------------------------------------------*) val CONJ_SYM = thm (#(FILE), #(LINE))("CONJ_SYM", let val t1 = “t1:bool” and t2 = “t2:bool” val th1 = ASSUME “^t1 /\ ^t2” and th2 = ASSUME “^t2 /\ ^t1” in GEN t1 (GEN t2 (IMP_ANTISYM_RULE (DISCH “^t1 /\ ^t2” (CONJ(CONJUNCT2 th1)(CONJUNCT1 th1))) (DISCH “^t2 /\ ^t1” (CONJ(CONJUNCT2 th2)(CONJUNCT1 th2))))) end); val _ = thm (#(FILE), #(LINE))("CONJ_COMM", CONJ_SYM); (*--------------------------------------------------------------------------- * |- !t1 t2 t3. t1 /\ (t2 /\ t3) = (t1 /\ t2) /\ t3 *---------------------------------------------------------------------------*) val CONJ_ASSOC = thm (#(FILE), #(LINE))("CONJ_ASSOC", let val t1 = “t1:bool” and t2 = “t2:bool” and t3 = “t3:bool” val th1 = ASSUME “^t1 /\ (^t2 /\ ^t3)” val th2 = ASSUME “(^t1 /\ ^t2) /\ ^t3” val th3 = DISCH “^t1 /\ (^t2 /\ ^t3)” (CONJ (CONJ(CONJUNCT1 th1) (CONJUNCT1(CONJUNCT2 th1))) (CONJUNCT2(CONJUNCT2 th1))) and th4 = DISCH “(^t1 /\ ^t2) /\ ^t3” (CONJ (CONJUNCT1(CONJUNCT1 th2)) (CONJ(CONJUNCT2(CONJUNCT1 th2)) (CONJUNCT2 th2))) in GEN t1 (GEN t2 (GEN t3 (IMP_ANTISYM_RULE th3 th4))) end); (*--------------------------------------------------------------------------- * |- !t1 t2. t1 ==> t1 \/ t2 *---------------------------------------------------------------------------*) val OR_INTRO_THM1 = thm (#(FILE), #(LINE))("OR_INTRO_THM1", let val t = “t:bool” and t1 = “t1:bool” and t2 = “t2:bool” val th1 = ADD_ASSUM “^t2 ==> ^t” (MP (ASSUME “^t1 ==> ^t”) (ASSUME t1)) val th2 = GEN t (DISCH “^t1 ==> ^t” (DISCH “^t2 ==> ^t” th1)) val th3 = RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM OR_DEF t1)) t2) in GEN t1 (GEN t2 (DISCH t1 (EQ_MP (SYM th3) th2))) end); (*--------------------------------------------------------------------------- * |- !t1 t2. t2 ==> t1 \/ t2 *---------------------------------------------------------------------------*) val OR_INTRO_THM2 = thm (#(FILE), #(LINE))("OR_INTRO_THM2", let val t = “t:bool” and t1 = “t1:bool” and t2 = “t2:bool” val th1 = ADD_ASSUM “^t1 ==> ^t” (MP (ASSUME “^t2 ==> ^t”) (ASSUME t2)) val th2 = GEN t (DISCH “^t1 ==> ^t” (DISCH “^t2 ==> ^t” th1)) val th3 = RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM OR_DEF t1)) t2) in GEN t1 (GEN t2 (DISCH t2 (EQ_MP (SYM th3) th2))) end); (*--------------------------------------------------------------------------- * |- !t t1 t2. (t1 \/ t2) ==> (t1 ==> t) ==> (t2 ==> t) ==> t *---------------------------------------------------------------------------*) val OR_ELIM_THM = thm (#(FILE), #(LINE))("OR_ELIM_THM", let val t = “t:bool” and t1 = “t1:bool” and t2 = “t2:bool” val th1 = ASSUME “^t1 \/ ^t2” val th2 = UNFOLD_OR_CONV (concl th1) val th3 = SPEC t (EQ_MP th2 th1) val th4 = MP (MP th3 (ASSUME “^t1 ==> ^t”)) (ASSUME “^t2 ==> ^t”) val th4 = DISCH “^t1 ==> ^t” (DISCH “^t2 ==> ^t” th4) in GEN t (GEN t1 (GEN t2 (DISCH “^t1 \/ ^t2” th4))) end); (* DISJ1, DISJ2, DISJ_CASES should be built here. *) fun DISJ_CASES_UNION dth ath bth = DISJ_CASES dth (DISJ1 ath (concl bth)) (DISJ2 (concl ath) bth); (*--------------------------------------------------------------------------- * |- !t. (t ==> F) ==> ~t *---------------------------------------------------------------------------*) val IMP_F = thm (#(FILE), #(LINE))("IMP_F", let val t = “t:bool” val th1 = RIGHT_BETA (AP_THM NOT_DEF t) in GEN t (DISCH “^t ==> F” (EQ_MP (SYM th1) (ASSUME “^t ==> F”))) end); (*--------------------------------------------------------------------------- * |- !t. ~t ==> (t ==> F) *---------------------------------------------------------------------------*) val F_IMP = thm (#(FILE), #(LINE))("F_IMP", let val t = “t:bool” val th1 = RIGHT_BETA(AP_THM NOT_DEF t) in GEN t (DISCH “~^t” (EQ_MP th1 (ASSUME “~^t”))) end); (*--------------------------------------------------------------------------- * |- !t. ~t ==> (t=F) *---------------------------------------------------------------------------*) val NOT_F = thm (#(FILE), #(LINE))("NOT_F", let val t = “t:bool” val th1 = MP (SPEC t F_IMP) (ASSUME “~ ^t”) and th2 = SPEC t FALSITY val th3 = IMP_ANTISYM_RULE th1 th2 in GEN t (DISCH “~^t” th3) end); (*--------------------------------------------------------------------------- * |- !t. ~(t /\ ~t) *---------------------------------------------------------------------------*) val NOT_AND = thm (#(FILE), #(LINE))("NOT_AND", let val th = ASSUME “t /\ ~t” in NOT_INTRO(DISCH “t /\ ~t” (MP (CONJUNCT2 th) (CONJUNCT1 th))) end); (*--------------------------------------------------------------------------- * |- !t. (T /\ t) = t *---------------------------------------------------------------------------*) val AND_CLAUSE1 = let val t = “t:bool” val th1 = DISCH “T /\ ^t” (CONJUNCT2(ASSUME “T /\ ^t”)) and th2 = DISCH t (CONJ TRUTH (ASSUME t)) in GEN t (IMP_ANTISYM_RULE th1 th2) end; (*--------------------------------------------------------------------------- * |- !t. (t /\ T) = t *---------------------------------------------------------------------------*) val AND_CLAUSE2 = let val t = “t:bool” val th1 = DISCH “^t /\ T” (CONJUNCT1(ASSUME “^t /\ T”)) and th2 = DISCH t (CONJ (ASSUME t) TRUTH) in GEN t (IMP_ANTISYM_RULE th1 th2) end; (*--------------------------------------------------------------------------- * |- !t. (F /\ t) = F *---------------------------------------------------------------------------*) val AND_CLAUSE3 = let val t = “t:bool” val th1 = IMP_TRANS (SPEC t (SPEC “F” AND1_THM)) (SPEC “F” FALSITY) and th2 = SPEC “F /\ ^t” FALSITY in GEN t (IMP_ANTISYM_RULE th1 th2) end; (*--------------------------------------------------------------------------- * |- !t. (t /\ F) = F *---------------------------------------------------------------------------*) val AND_CLAUSE4 = let val t = “t:bool” val th1 = IMP_TRANS (SPEC “F” (SPEC t AND2_THM)) (SPEC “F” FALSITY) and th2 = SPEC “^t /\ F” FALSITY in GEN t (IMP_ANTISYM_RULE th1 th2) end; (*--------------------------------------------------------------------------- * |- !t. (t /\ t) = t *---------------------------------------------------------------------------*) val AND_CLAUSE5 = let val t = “t:bool” val th1 = DISCH “^t /\ ^t” (CONJUNCT1(ASSUME “^t /\ ^t”)) and th2 = DISCH t (CONJ(ASSUME t)(ASSUME t)) in GEN t (IMP_ANTISYM_RULE th1 th2) end; (*--------------------------------------------------------------------------- * |- !t. (T /\ t) = t /\ * (t /\ T) = t /\ * (F /\ t) = F /\ * (t /\ F) = F /\ * (t /\ t) = t *---------------------------------------------------------------------------*) val AND_CLAUSES = thm (#(FILE), #(LINE))("AND_CLAUSES", let val t = “t:bool” in GEN t (LIST_CONJ [SPEC t AND_CLAUSE1, SPEC t AND_CLAUSE2, SPEC t AND_CLAUSE3, SPEC t AND_CLAUSE4, SPEC t AND_CLAUSE5]) end); (*--------------------------------------------------------------------------- * |- !t. (T \/ t) = T *---------------------------------------------------------------------------*) val OR_CLAUSE1 = let val t = “t:bool” val th1 = DISCH “T \/ ^t” TRUTH and th2 = DISCH “T” (DISJ1 TRUTH t) in GEN t (IMP_ANTISYM_RULE th1 th2) end; (*--------------------------------------------------------------------------- * |- !t. (t \/ T) = T *---------------------------------------------------------------------------*) val OR_CLAUSE2 = let val t = “t:bool” val th1 = DISCH “^t \/ T” TRUTH and th2 = DISCH “T” (DISJ2 t TRUTH) in GEN t (IMP_ANTISYM_RULE th1 th2) end; (*--------------------------------------------------------------------------- * |- (F \/ t) = t *---------------------------------------------------------------------------*) val OR_CLAUSE3 = let val t = “t:bool” val th1 = DISCH “F \/ ^t” (DISJ_CASES (ASSUME “F \/ ^t”) (UNDISCH (SPEC t FALSITY)) (ASSUME t)) and th2 = SPEC t (SPEC “F” OR_INTRO_THM2) in GEN t (IMP_ANTISYM_RULE th1 th2) end; (*--------------------------------------------------------------------------- * |- !t. (t \/ F) = t *---------------------------------------------------------------------------*) val OR_CLAUSE4 = let val t = “t:bool” val th1 = DISCH “^t \/ F” (DISJ_CASES (ASSUME “^t \/ F”) (ASSUME t) (UNDISCH (SPEC t FALSITY))) and th2 = SPEC “F” (SPEC t OR_INTRO_THM1) in GEN t (IMP_ANTISYM_RULE th1 th2) end; (*--------------------------------------------------------------------------- * |- !t. (t \/ t) = t *---------------------------------------------------------------------------*) val OR_CLAUSE5 = let val t = “t:bool” val th1 = DISCH “^t \/ ^t” (DISJ_CASES(ASSUME “^t \/ ^t”) (ASSUME t) (ASSUME t)) and th2 = DISCH t (DISJ1(ASSUME t)t) in GEN t (IMP_ANTISYM_RULE th1 th2) end; (*--------------------------------------------------------------------------- * |- !t. (T \/ t) = T /\ * (t \/ T) = T /\ * (F \/ t) = t /\ * (t \/ F) = t /\ * (t \/ t) = t *---------------------------------------------------------------------------*) val OR_CLAUSES = thm (#(FILE), #(LINE))("OR_CLAUSES", let val t = “t:bool” in GEN t (LIST_CONJ [SPEC t OR_CLAUSE1, SPEC t OR_CLAUSE2, SPEC t OR_CLAUSE3, SPEC t OR_CLAUSE4, SPEC t OR_CLAUSE5]) end); (*--------------------------------------------------------------------------- * |- !t. (T ==> t) = t *---------------------------------------------------------------------------*) val IMP_CLAUSE1 = let val t = “t:bool” val th1 = DISCH “T ==> ^t” (MP (ASSUME “T ==> ^t”) TRUTH) and th2 = DISCH t (DISCH “T” (ADD_ASSUM “T” (ASSUME t))) in GEN t (IMP_ANTISYM_RULE th1 th2) end; (*--------------------------------------------------------------------------- * |- !t. (F ==> t) = T *---------------------------------------------------------------------------*) val IMP_CLAUSE2 = let val t = “t:bool” in GEN t (EQT_INTRO(SPEC t FALSITY)) end; (*--------------------------------------------------------------------------- * |- !t. (t ==> T) = T *---------------------------------------------------------------------------*) val IMP_CLAUSE3 = let val t = “t:bool” in GEN t (EQT_INTRO(DISCH t (ADD_ASSUM t TRUTH))) end; (*--------------------------------------------------------------------------- * |- ((T ==> F) = F) /\ ((F ==> F) = T) *---------------------------------------------------------------------------*) val IMP_CLAUSE4 = let val th1 = DISCH “T ==> F” (MP (ASSUME “T ==> F”) TRUTH) and th2 = SPEC “T ==> F” FALSITY and th3 = EQT_INTRO(DISCH “F” (ASSUME “F”)) in CONJ(IMP_ANTISYM_RULE th1 th2) th3 end; (*--------------------------------------------------------------------------- * |- !t. (t ==> F) = ~t *---------------------------------------------------------------------------*) val IMP_CLAUSE5 = let val t = “t:bool” val th1 = SPEC t IMP_F and th2 = SPEC t F_IMP in GEN t (IMP_ANTISYM_RULE th1 th2) end; (*--------------------------------------------------------------------------- * |- !t. (T ==> t) = t /\ * (t ==> T) = T /\ * (F ==> t) = T /\ * (t ==> t) = t /\ * (t ==> F) = ~t *---------------------------------------------------------------------------*) val IMP_CLAUSES = thm (#(FILE), #(LINE))("IMP_CLAUSES", let val t = “t:bool” in GEN t (LIST_CONJ [SPEC t IMP_CLAUSE1, SPEC t IMP_CLAUSE3, SPEC t IMP_CLAUSE2, EQT_INTRO(DISCH t (ASSUME t)), SPEC t IMP_CLAUSE5]) end); (* ---------------------------------------------------------------------- |- !t1 t2. (t1 <=> t2) ==> (t1 ==> t2) ---------------------------------------------------------------------- *) val EQ_IMPLIES = let val impt1 = REFL $ mk_comb(implication, t1b) val eqt = mk_eq(t1b,t2b) val t1_eq_t2 = ASSUME eqt val th0 = MK_COMB(impt1,t1_eq_t2) val imp_refl = IMP_CLAUSES |> SPEC t1b |> CONJUNCTS |> el 4 |> EQT_ELIM in thm (#(FILE), #(LINE))( "EQ_IMPLIES", EQ_MP th0 imp_refl |> DISCH eqt |> GENL [t1b,t2b] ) end (*---------------------------------------------------------------------------- * |- (~~t = t) /\ (~T = F) /\ (~F = T) *---------------------------------------------------------------------------*) val NOT_CLAUSES = thm (#(FILE), #(LINE))("NOT_CLAUSES", CONJ (GEN “t:bool” (IMP_ANTISYM_RULE (DISJ_IMP(IMP_ELIM(DISCH “t:bool” (ASSUME “t:bool”)))) (DISCH “t:bool” (NOT_INTRO(DISCH “~t” (UNDISCH (NOT_ELIM(ASSUME “~t”)))))))) (CONJ (IMP_ANTISYM_RULE (DISCH “~T” (MP (MP (SPEC “T” F_IMP) (ASSUME “~T”)) TRUTH)) (SPEC “~T” FALSITY)) (IMP_ANTISYM_RULE (DISCH “~F” TRUTH) (DISCH “T” (MP (SPEC “F” IMP_F) (SPEC “F” FALSITY)))))); (*--------------------------------------------------------------------------- * |- !x. x=x *---------------------------------------------------------------------------*) val EQ_REFL = thm (#(FILE), #(LINE))("EQ_REFL", GEN “x : 'a” (REFL “x : 'a”)); (*--------------------------------------------------------------------------- * |- !x. (x=x) = T *---------------------------------------------------------------------------*) val REFL_CLAUSE = thm (#(FILE), #(LINE))("REFL_CLAUSE", GEN “x: 'a” (EQT_INTRO(SPEC “x:'a” EQ_REFL))); (*--------------------------------------------------------------------------- * |- !x y. x=y ==> y=x *---------------------------------------------------------------------------*) val EQ_SYM = thm (#(FILE), #(LINE))("EQ_SYM", let val x = “x:'a” and y = “y:'a” in GEN x (GEN y (DISCH “^x = ^y” (SYM(ASSUME “^x = ^y”)))) end); (*--------------------------------------------------------------------------- * |- !x y. (x = y) = (y = x) *---------------------------------------------------------------------------*) val EQ_SYM_EQ = thm (#(FILE), #(LINE))("EQ_SYM_EQ", GEN “x:'a” (GEN “y:'a” (IMP_ANTISYM_RULE (SPEC “y:'a” (SPEC “x:'a” EQ_SYM)) (SPEC “x:'a” (SPEC “y:'a” EQ_SYM))))); (*--------------------------------------------------------------------------- * |- !f g. (!x. f x = g x) ==> f=g *---------------------------------------------------------------------------*) val EQ_EXT = thm (#(FILE), #(LINE))("EQ_EXT", let val f = “f:'a->'b” and g = “g: 'a -> 'b” in GEN f (GEN g (DISCH “!x:'a. ^f (x:'a) = ^g (x:'a)” (EXT(ASSUME “!x:'a. ^f (x:'a) = ^g (x:'a)”)))) end); (*--------------------------------------------------------------------------- FUN_EQ_THM |- !f g. (f = g) = !x. f x = g x ---------------------------------------------------------------------------*) val FUN_EQ_THM = thm (#(FILE), #(LINE))("FUN_EQ_THM", let val f = mk_var("f", Type.alpha --> Type.beta) val g = mk_var("g", Type.alpha --> Type.beta) val x = mk_var("x", Type.alpha) val f_eq_g = mk_eq(f,g) val fx_eq_gx = mk_eq(mk_comb(f,x),mk_comb(g,x)) val uq_f_eq_g = mk_forall(x,fx_eq_gx) val th1 = GEN x (AP_THM (ASSUME f_eq_g) x); val th2 = MP (SPEC_ALL EQ_EXT) (ASSUME uq_f_eq_g); in GEN f (GEN g (IMP_ANTISYM_RULE (DISCH_ALL th1) (DISCH_ALL th2))) end); (*--------------------------------------------------------------------------- * |- !x y z. x=y /\ y=z ==> x=z *---------------------------------------------------------------------------*) val EQ_TRANS = thm (#(FILE), #(LINE))("EQ_TRANS", let val x = “x:'a” and y = “y:'a” and z = “z:'a” val xyyz = “(^x = ^y) /\ (^y = ^z)” in GEN x (GEN y (GEN z (DISCH xyyz (TRANS (CONJUNCT1(ASSUME xyyz)) (CONJUNCT2(ASSUME xyyz)))))) end); (*--------------------------------------------------------------------------- * |- ~(T=F) /\ ~(F=T) *---------------------------------------------------------------------------*) val BOOL_EQ_DISTINCT = thm (#(FILE), #(LINE))("BOOL_EQ_DISTINCT", let val TF = “T = F” and FT = “F = T” in CONJ (NOT_INTRO(DISCH TF (EQ_MP (ASSUME TF) TRUTH))) (NOT_INTRO(DISCH FT (EQ_MP (SYM(ASSUME FT)) TRUTH))) end); (*--------------------------------------------------------------------------- * |- !t. (T = t) = t *---------------------------------------------------------------------------*) val EQ_CLAUSE1 = let val t = “t:bool” val Tt = “T = ^t” val th1 = DISCH Tt (EQ_MP (ASSUME Tt) TRUTH) and th2 = DISCH t (SYM(EQT_INTRO(ASSUME t))) in GEN t (IMP_ANTISYM_RULE th1 th2) end; (*--------------------------------------------------------------------------- * |- !t. (t = T) = t *---------------------------------------------------------------------------*) val EQ_CLAUSE2 = let val t = “t:bool” val tT = “^t = T” val th1 = DISCH tT (EQ_MP (SYM (ASSUME tT)) TRUTH) and th2 = DISCH t (EQT_INTRO(ASSUME t)) in GEN t (IMP_ANTISYM_RULE th1 th2) end; (*--------------------------------------------------------------------------- * |- !t. (F = t) = ~t *---------------------------------------------------------------------------*) val EQ_CLAUSE3 = let val t = “t:bool” val Ft = “F = ^t” val tF = “^t = F” val th1 = DISCH Ft (MP (SPEC t IMP_F) (DISCH t (EQ_MP(SYM(ASSUME Ft)) (ASSUME t)))) and th2 = IMP_TRANS (SPEC t NOT_F) (DISCH tF (SYM(ASSUME tF))) in GEN t (IMP_ANTISYM_RULE th1 th2) end; (*--------------------------------------------------------------------------- * |- !t. (t = F) = ~t *---------------------------------------------------------------------------*) val EQ_CLAUSE4 = let val t = “t:bool” val tF = “^t = F” val th1 = DISCH tF (MP (SPEC t IMP_F) (DISCH t (EQ_MP(ASSUME tF) (ASSUME t)))) and th2 = SPEC t NOT_F in GEN t (IMP_ANTISYM_RULE th1 th2) end; (*--------------------------------------------------------------------------- * |- !t. (T = t) = t /\ * (t = T) = t /\ * (F = t) = ~t /\ * (t = F) = ~t *---------------------------------------------------------------------------*) val EQ_CLAUSES = thm (#(FILE), #(LINE))("EQ_CLAUSES", let val t = “t:bool” in GEN t (LIST_CONJ [SPEC t EQ_CLAUSE1, SPEC t EQ_CLAUSE2, SPEC t EQ_CLAUSE3, SPEC t EQ_CLAUSE4]) end); (*--------------------------------------------------------------------------- * |- !t1 t2 :'a. COND T t1 t2 = t1 *---------------------------------------------------------------------------*) val COND_CLAUSE1 = let val (x,t1,t2,v) = (“x:'a”, “t1:'a”, “t2:'a”, genvar Type.bool) val th1 = RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM COND_DEF “T”)) t1))t2) val TT = EQT_INTRO(REFL “T”) val th2 = SUBST [v |-> SYM TT] “(^v ==> (^x=^t1)) = (^x=^t1)” (CONJUNCT1 (SPEC “^x=^t1” IMP_CLAUSES)) and th3 = DISCH “T=F” (MP (SPEC “^x=^t2” FALSITY) (UNDISCH(MP (SPEC “T=F” F_IMP) (CONJUNCT1 BOOL_EQ_DISTINCT)))) val th4 = DISCH “^x=^t1” (CONJ(EQ_MP(SYM th2)(ASSUME “^x=^t1”))th3) and th5 = DISCH “((T=T) ==> (^x=^t1))/\((T=F) ==> (^x=^t2))” (MP (CONJUNCT1(ASSUME “((T=T) ==> (^x=^t1))/\ ((T=F) ==> (^x=^t2))”)) (REFL “T”)) val th6 = IMP_ANTISYM_RULE th4 th5 val th7 = TRANS th1 (SYM(SELECT_EQ x th6)) val th8 = EQ_MP (SYM(BETA_CONV “(\ ^x.^x = ^t1) ^t1”)) (REFL t1) val th9 = MP (SPEC t1 (SPEC “\ ^x.^x = ^t1” SELECT_AX)) th8 in GEN t1 (GEN t2 (TRANS th7 (EQ_MP (BETA_CONV(concl th9)) th9))) end; (*--------------------------------------------------------------------------- * |- !tm1 tm2:'a. COND F tm1 tm2 = tm2 * * Note that there is a bound variable conflict if we use use t1 * and t2 as the variable names. That would be a good test of the * substitution algorithm. *---------------------------------------------------------------------------*) val COND_CLAUSE2 = let val (x,t1,t2,v) = (“x:'a”, “tm1:'a”, “tm2:'a”, genvar Type.bool) val th1 = RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM COND_DEF “F”)) t1))t2) val FF = EQT_INTRO(REFL “F”) val th2 = SUBST [v |-> SYM FF] “(^v ==> (^x=^t2))=(^x=^t2)” (CONJUNCT1(SPEC “^x=^t2” IMP_CLAUSES)) and th3 = DISCH “F=T” (MP (SPEC “^x=^t1” FALSITY) (UNDISCH (MP (SPEC “F=T” F_IMP) (CONJUNCT2 BOOL_EQ_DISTINCT)))) val th4 = DISCH “^x=^t2” (CONJ th3 (EQ_MP(SYM th2)(ASSUME “^x=^t2”))) and th5 = DISCH “((F=T) ==> (^x=^t1)) /\ ((F=F) ==> (^x=^t2))” (MP (CONJUNCT2(ASSUME “((F=T) ==> (^x=^t1)) /\ ((F=F) ==> (^x=^t2))”)) (REFL “F”)) val th6 = IMP_ANTISYM_RULE th4 th5 val th7 = TRANS th1 (SYM(SELECT_EQ x th6)) val th8 = EQ_MP (SYM(BETA_CONV “(\ ^x.^x = ^t2) ^t2”)) (REFL t2) val th9 = MP (SPEC t2 (SPEC “\ ^x.^x = ^t2” SELECT_AX)) th8 in GEN t1 (GEN t2 (TRANS th7 (EQ_MP (BETA_CONV(concl th9)) th9))) end; (*--------------------------------------------------------------------------- * |- !t1:'a.!t2:'a. ((T => t1 | t2) = t1) /\ ((F => t1 | t2) = t2) *---------------------------------------------------------------------------*) val COND_CLAUSES = thm (#(FILE), #(LINE))("COND_CLAUSES", let val (t1,t2) = (“t1:'a”, “t2:'a”) in GEN t1 (GEN t2 (CONJ(SPEC t2(SPEC t1 COND_CLAUSE1)) (SPEC t2(SPEC t1 COND_CLAUSE2)))) end); (*--------------------------------------------------------------------- *) (* |- b. !t. (b => t | t) = t *) (* TFM 90.07.23 *) (*--------------------------------------------------------------------- *) val COND_ID = thm (#(FILE), #(LINE))("COND_ID", let val b = “b:bool” and t = “t:'a” val def = INST_TYPE [beta |-> alpha] COND_DEF val th1 = itlist (fn x => RIGHT_BETA o (C AP_THM x)) [t,t,b] def val p = genvar bool val asm1 = ASSUME “((^b=T)==>^p) /\ ((^b=F)==>^p)” val th2 = DISJ_CASES (SPEC b BOOL_CASES_AX) (UNDISCH (CONJUNCT1 asm1)) (UNDISCH (CONJUNCT2 asm1)) val imp1 = DISCH (concl asm1) th2 val asm2 = ASSUME p val imp2 = DISCH p (CONJ (DISCH “^b=T” (ADD_ASSUM “^b=T” asm2)) (DISCH “^b=F” (ADD_ASSUM “^b=F” asm2))) val lemma = SPEC “x:'a = ^t” (GEN p (IMP_ANTISYM_RULE imp1 imp2)) val th3 = TRANS th1 (SELECT_EQ “x:'a” lemma) val th4 = EQ_MP (SYM(BETA_CONV “(\x.x = ^t) ^t”)) (REFL t) val th5 = MP (SPEC t (SPEC “\x.x = ^t” SELECT_AX)) th4 val lemma2 = EQ_MP (BETA_CONV(concl th5)) th5 in GEN b (GEN t (TRANS th3 lemma2)) end); (*--------------------------------------------------------------------------- SELECT_THM = |- !P. P (@x. P x) = ?x. P x ---------------------------------------------------------------------------*) val SELECT_THM = thm (#(FILE), #(LINE))("SELECT_THM", GEN “P:'a->bool” (SYM (RIGHT_BETA(RIGHT_BETA (AP_THM EXISTS_DEF “\x:'a. P x:bool”))))); (* ---------------------------------------------------------------------*) (* SELECT_REFL = |- !x. (@y. y = x) = x *) (* ---------------------------------------------------------------------*) val SELECT_REFL = thm (#(FILE), #(LINE))("SELECT_REFL", let val th1 = SPEC “x:'a” (SPEC “\y:'a. y = x” SELECT_AX) val ths = map BETA_CONV [“(\y:'a. y = x) x”, “(\y:'a. y = x)(@y. y = x)”] val th2 = SUBST[“u:bool” |-> el 1 ths, “v:bool” |-> el 2 ths] “u ==> v” th1 in GEN “x:'a” (MP th2 (REFL “x:'a”)) end); val SELECT_REFL_2 = thm (#(FILE), #(LINE))("SELECT_REFL_2", let val x = mk_var("x", Type.alpha) val y = mk_var("y", Type.alpha) val th1 = REFL x val th2 = EXISTS (mk_exists(y,mk_eq(x,y)),x) th1 val th3 = SPEC y (SPEC (mk_abs(y,mk_eq(x,y))) SELECT_AX) val th4 = UNDISCH th3 val th5 = DISCH_ALL(SYM (EQ_MP (BETA_CONV (concl th4)) th4)) val th6 = UNDISCH(CONV_RULE (RATOR_CONV (RAND_CONV BETA_CONV)) th5) in GEN x (CHOOSE(y,th2) th6) end); (*---------------------------------------------------------------------------*) (* SELECT_UNIQUE = |- !P x. (!y. P y = (y = x)) ==> ($@ P = x) *) (*---------------------------------------------------------------------------*) val SELECT_UNIQUE = thm (#(FILE), #(LINE))("SELECT_UNIQUE", let fun mksym tm = DISCH tm (SYM(ASSUME tm)) val th0 = IMP_ANTISYM_RULE (mksym “y:'a = x”) (mksym “x:'a = y”) val th1 = SPEC “y:'a” (ASSUME “!y:'a. P y = (y = x)”) val th2 = EXT(GEN “y:'a” (TRANS th1 th0)) val th3 = AP_TERM “$@ :('a->bool)->'a” th2 val th4 = TRANS (BETA_CONV “(\y:'a. y = x) y”) th0 val th5 = AP_TERM “$@ :('a->bool)->'a” (EXT(GEN “y:'a” th4)) val th6 = TRANS (TRANS th3 (SYM th5)) (SPEC “x:'a” SELECT_REFL) in GENL [“P:'a->bool”, “x:'a”] (DISCH “!y:'a. P y = (y = x)” th6) end); (* ---------------------------------------------------------------------- SELECT_ELIM_THM = |- !P Q. (?x. P x) /\ (!x. P x ==> Q x) ==> Q ($@ P) ---------------------------------------------------------------------- *) val SELECT_ELIM_THM = let val P = mk_var("P", alpha --> bool) val Q = mk_var("Q", alpha --> bool) val x = mk_var("x", alpha) val Px = mk_comb(P, x) val Qx = mk_comb(Q, x) val PimpQ = mk_imp(Px, Qx) val allPimpQ = mk_forall(x, PimpQ) val exPx = mk_exists (x, Px) val selP = mk_comb(prim_mk_const{Thy = "min", Name = "@"}, P) val asm_t = mk_conj(exPx, allPimpQ) val asm = ASSUME asm_t val (ex_th, forall_th) = CONJ_PAIR asm val imp_th = SPEC selP forall_th val Px_th = ASSUME Px val PselP_th0 = UNDISCH (SPEC_ALL SELECT_AX) val PselP_th = CHOOSE(x, ex_th) PselP_th0 in thm (#(FILE), #(LINE))( "SELECT_ELIM_THM", GENL [P, Q] (DISCH_ALL (MP imp_th PselP_th)) ) end (* -------------------------------------------------------------------------*) (* NOT_FORALL_THM = |- !P. ~(!x. P x) = ?x. ~P x *) (* -------------------------------------------------------------------------*) val NOT_FORALL_THM = thm (#(FILE), #(LINE))("NOT_FORALL_THM", let val f = “P:'a->bool” val x = “x:'a” val t = mk_comb(f,x) val all = mk_forall(x,t) and exists = mk_exists(x,mk_neg t) val nott = ASSUME (mk_neg t) val th1 = DISCH all (MP nott (SPEC x (ASSUME all))) val imp1 = DISCH exists (CHOOSE (x, ASSUME exists) (NOT_INTRO th1)) val th2 = CCONTR t (MP (ASSUME(mk_neg exists)) (EXISTS(exists,x)nott)) val th3 = CCONTR exists (MP (ASSUME (mk_neg all)) (GEN x th2)) val imp2 = DISCH (mk_neg all) th3 in GEN f (IMP_ANTISYM_RULE imp2 imp1) end); (* ------------------------------------------------------------------------- *) (* NOT_EXISTS_THM = |- !P. ~(?x. P x) = (!x. ~P x) *) (* ------------------------------------------------------------------------- *) val NOT_EXISTS_THM = thm (#(FILE), #(LINE))("NOT_EXISTS_THM", let val f = “P:'a->bool” val x = “x:'a” val t = mk_comb(f,x) val tm = mk_neg(mk_exists(x,t)) val all = mk_forall(x,mk_neg t) val asm1 = ASSUME t val thm1 = MP (ASSUME tm) (EXISTS (rand tm, x) asm1) val imp1 = DISCH tm (GEN x (NOT_INTRO (DISCH t thm1))) val asm2 = ASSUME all and asm3 = ASSUME (rand tm) val thm2 = DISCH (rand tm) (CHOOSE (x,asm3) (MP (SPEC x asm2) asm1)) val imp2 = DISCH all (NOT_INTRO thm2) in GEN f (IMP_ANTISYM_RULE imp1 imp2) end); (* ------------------------------------------------------------------------- *) (* FORALL_AND_THM |- !P Q. (!x. P x /\ Q x) = ((!x. P x) /\ (!x. Q x)) *) (* ------------------------------------------------------------------------- *) val FORALL_AND_THM = thm (#(FILE), #(LINE))("FORALL_AND_THM", let val f = “P:'a->bool” val g = “Q:'a->bool” val x = “x:'a” val th1 = ASSUME “!x:'a. (P x) /\ (Q x)” val imp1 = (uncurry CONJ) ((GEN x ## GEN x) (CONJ_PAIR (SPEC x th1))) val th2 = ASSUME “(!x:'a. P x) /\ (!x:'a. Q x)” val imp2 = GEN x (uncurry CONJ ((SPEC x ## SPEC x) (CONJ_PAIR th2))) in GENL [f,g] (IMP_ANTISYM_RULE (DISCH_ALL imp1) (DISCH_ALL imp2)) end); (* ------------------------------------------------------------------------- *) (* LEFT_AND_FORALL_THM = |- !P Q. (!x. P x) /\ Q = (!x. P x /\ Q) *) (* ------------------------------------------------------------------------- *) val LEFT_AND_FORALL_THM = thm (#(FILE), #(LINE))("LEFT_AND_FORALL_THM", let val x = “x:'a” val f = “P:'a->bool” val Q = “Q:bool” val th1 = ASSUME “(!x:'a. P x) /\ Q” val imp1 = GEN x ((uncurry CONJ) ((SPEC x ## I) (CONJ_PAIR th1))) val th2 = ASSUME “!x:'a. P x /\ Q” val imp2 = (uncurry CONJ) ((GEN x ## I) (CONJ_PAIR (SPEC x th2))) in GENL [f,Q] (IMP_ANTISYM_RULE (DISCH_ALL imp1) (DISCH_ALL imp2)) end); (* ------------------------------------------------------------------------- *) (* RIGHT_AND_FORALL_THM = |- !P Q. P /\ (!x. Q x) = (!x. P /\ Q x) *) (* ------------------------------------------------------------------------- *) val RIGHT_AND_FORALL_THM = thm (#(FILE), #(LINE))("RIGHT_AND_FORALL_THM", let val x = “x:'a” val P = “P:bool” val g = “Q:'a->bool” val th1 = ASSUME “P /\ (!x:'a. Q x)” val imp1 = GEN x ((uncurry CONJ) ((I ## SPEC x) (CONJ_PAIR th1))) val th2 = ASSUME “!x:'a. P /\ Q x” val imp2 = (uncurry CONJ) ((I ## GEN x) (CONJ_PAIR (SPEC x th2))) in GENL [P,g] (IMP_ANTISYM_RULE (DISCH_ALL imp1) (DISCH_ALL imp2)) end); (* ------------------------------------------------------------------------- *) (* EXISTS_OR_THM |- !P Q. (?x. P x \/ Q x) = ((?x. P x) \/ (?x. Q x)) *) (* ------------------------------------------------------------------------- *) val EXISTS_OR_THM = thm (#(FILE), #(LINE))("EXISTS_OR_THM", let val f = “P:'a->bool” val g = “Q:'a->bool” val x = “x:'a” val P = mk_comb(f,x) val Q = mk_comb(g,x) val tm = mk_exists (x,mk_disj(P,Q)) val ep = mk_exists (x,P) and eq = mk_exists(x,Q) val Pth = EXISTS(ep,x)(ASSUME P) and Qth = EXISTS(eq,x)(ASSUME Q) val thm1 = DISJ_CASES_UNION (ASSUME(mk_disj(P,Q))) Pth Qth val imp1 = DISCH tm (CHOOSE (x,ASSUME tm) thm1) val t1 = DISJ1 (ASSUME P) Q and t2 = DISJ2 P (ASSUME Q) val th1 = EXISTS(tm,x) t1 and th2 = EXISTS(tm,x) t2 val e1 = CHOOSE (x,ASSUME ep) th1 and e2 = CHOOSE (x,ASSUME eq) th2 val thm2 = DISJ_CASES (ASSUME(mk_disj(ep,eq))) e1 e2 val imp2 = DISCH (mk_disj(ep,eq)) thm2 in GENL [f,g] (IMP_ANTISYM_RULE imp1 imp2) end); (* ------------------------------------------------------------------------- *) (* LEFT_OR_EXISTS_THM = |- (?x. P x) \/ Q = (?x. P x \/ Q) *) (* ------------------------------------------------------------------------- *) val LEFT_OR_EXISTS_THM = thm (#(FILE), #(LINE))("LEFT_OR_EXISTS_THM", let val x = “x:'a” val Q = “Q:bool” val f = “P:'a->bool” val P = mk_comb(f,x) val ep = mk_exists(x,P) val tm = mk_disj(ep,Q) val otm = mk_exists(x,mk_disj(P,Q)) val t1 = DISJ1 (ASSUME P) Q val t2 = DISJ2 P (ASSUME Q) val th1 = EXISTS(otm,x) t1 and th2 = EXISTS(otm,x) t2 val thm1 = DISJ_CASES (ASSUME tm) (CHOOSE(x,ASSUME ep)th1) th2 val imp1 = DISCH tm thm1 val Pth = EXISTS(ep,x)(ASSUME P) and Qth = ASSUME Q val thm2 = DISJ_CASES_UNION (ASSUME(mk_disj(P,Q))) Pth Qth val imp2 = DISCH otm (CHOOSE (x,ASSUME otm) thm2) in GENL [f,Q] (IMP_ANTISYM_RULE imp1 imp2) end); (* ------------------------------------------------------------------------- *) (* RIGHT_OR_EXISTS_THM = |- P \/ (?x. Q x) = (?x. P \/ Q x) *) (* ------------------------------------------------------------------------- *) val RIGHT_OR_EXISTS_THM = thm (#(FILE), #(LINE))("RIGHT_OR_EXISTS_THM", let val x = “x:'a” val P = “P:bool” val g = “Q:'a->bool” val Q = mk_comb(g,x) val eq = mk_exists(x,Q) val tm = mk_disj(P,eq) val otm = mk_exists(x,mk_disj(P,Q)) val t1 = DISJ1 (ASSUME P) Q and t2 = DISJ2 P (ASSUME Q) val th1 = EXISTS(otm,x) t1 and th2 = EXISTS(otm,x) t2 val thm1 = DISJ_CASES (ASSUME tm) th1 (CHOOSE(x,ASSUME eq)th2) val imp1 = DISCH tm thm1 val Qth = EXISTS(eq,x)(ASSUME Q) and Pth = ASSUME P val thm2 = DISJ_CASES_UNION (ASSUME(mk_disj(P,Q))) Pth Qth val imp2 = DISCH otm (CHOOSE (x,ASSUME otm) thm2) in GENL [P,g] (IMP_ANTISYM_RULE imp1 imp2) end); (* ------------------------------------------------------------------------- *) (* BOTH_EXISTS_AND_THM = |- !P Q. (?x. P /\ Q) = (?x. P) /\ (?x. Q) *) (* ------------------------------------------------------------------------- *) val BOTH_EXISTS_AND_THM = thm (#(FILE), #(LINE))("BOTH_EXISTS_AND_THM", let val x = “x:'a” val P = “P:bool” val Q = “Q:bool” val t = mk_conj(P,Q) val exi = mk_exists(x,t) val (t1,t2) = CONJ_PAIR (ASSUME t) val t11 = EXISTS ((mk_exists(x,P)),x) t1 val t21 = EXISTS ((mk_exists(x,Q)),x) t2 val imp1 = DISCH_ALL (CHOOSE (x, ASSUME (mk_exists(x,mk_conj(P,Q)))) (CONJ t11 t21)) val th21 = EXISTS (exi,x) (CONJ (ASSUME P) (ASSUME Q)) val th22 = CHOOSE(x,ASSUME(mk_exists(x,P))) th21 val th23 = CHOOSE(x,ASSUME(mk_exists(x,Q))) th22 val (u1,u2) = CONJ_PAIR (ASSUME (mk_conj(mk_exists(x,P),mk_exists(x,Q)))) val th24 = PROVE_HYP u1 (PROVE_HYP u2 th23) val imp2 = DISCH_ALL th24 in GENL [P,Q] (IMP_ANTISYM_RULE imp1 imp2) end); (* ------------------------------------------------------------------------- *) (* LEFT_EXISTS_AND_THM = |- !P Q. (?x. P x /\ Q) = (?x. P x) /\ Q *) (* ------------------------------------------------------------------------- *) val LEFT_EXISTS_AND_THM = thm (#(FILE), #(LINE))("LEFT_EXISTS_AND_THM", let val x = “x:'a” val f = “P:'a->bool” val P = mk_comb(f,x) val Q = “Q:bool” val t = mk_conj(P,Q) val exi = mk_exists(x,t) val (t1,t2) = CONJ_PAIR (ASSUME t) val t11 = EXISTS ((mk_exists(x,P)),x) t1 val imp1 = DISCH_ALL (CHOOSE (x, ASSUME (mk_exists(x,mk_conj(P,Q)))) (CONJ t11 t2)) val th21 = EXISTS (exi,x) (CONJ (ASSUME P) (ASSUME Q)) val th22 = CHOOSE(x,ASSUME(mk_exists(x,P))) th21 val (u1,u2) = CONJ_PAIR(ASSUME(mk_conj(mk_exists(x,P), Q))) val th23 = PROVE_HYP u1 (PROVE_HYP u2 th22) val imp2 = DISCH_ALL th23 in GENL [f,Q] (IMP_ANTISYM_RULE imp1 imp2) end); (* ------------------------------------------------------------------------- *) (* RIGHT_EXISTS_AND_THM = |- !P Q. (?x. P /\ Q x) = P /\ (?x. Q x) *) (* ------------------------------------------------------------------------- *) val RIGHT_EXISTS_AND_THM = thm (#(FILE), #(LINE))("RIGHT_EXISTS_AND_THM", let val x = “x:'a” val P = “P:bool” val g = “Q:'a->bool” val Q = mk_comb(g,x) val t = mk_conj(P,Q) val exi = mk_exists(x,t) val (t1,t2) = CONJ_PAIR (ASSUME t) val t21 = EXISTS ((mk_exists(x,Q)),x) t2 val imp1 = DISCH_ALL (CHOOSE (x, ASSUME (mk_exists(x,mk_conj(P,Q)))) (CONJ t1 t21)) val th21 = EXISTS (exi,x) (CONJ (ASSUME P) (ASSUME Q)) val th22 = CHOOSE(x,ASSUME(mk_exists(x,Q))) th21 val (u1,u2) = CONJ_PAIR (ASSUME (mk_conj(P, mk_exists(x,Q)))) val th23 = PROVE_HYP u1 (PROVE_HYP u2 th22) val imp2 = DISCH_ALL th23 in GENL [P,g] (IMP_ANTISYM_RULE imp1 imp2) end); (* ------------------------------------------------------------------------- *) (* BOTH_FORALL_OR_THM = |- !P Q. (!x. P \/ Q) = (!x. P) \/ (!x. Q) *) (* ------------------------------------------------------------------------- *) val BOTH_FORALL_OR_THM = thm (#(FILE), #(LINE))("BOTH_FORALL_OR_THM", let val x = “x:'a” val P = “P:bool” val Q = “Q:bool” val imp11 = DISCH_ALL (SPEC x (ASSUME (mk_forall(x,P)))) val imp12 = DISCH_ALL (GEN x (ASSUME P)) val fath = IMP_ANTISYM_RULE imp11 imp12 val th1 = REFL (mk_forall(x,mk_disj(P,Q))) val th2 = CONV_RULE (RAND_CONV (K (INST [P |-> mk_disj(P,Q)] fath))) th1 val th3 = CONV_RULE(RAND_CONV(RATOR_CONV(RAND_CONV(K(SYM fath))))) th2 val th4 = CONV_RULE(RAND_CONV(RAND_CONV(K(SYM(INST[P|->Q] fath))))) th3 in GENL [P,Q] th4 end); (* ------------------------------------------------------------------------- *) (* LEFT_FORALL_OR_THM = |- !P Q. (!x. P x \/ Q) = (!x. P x) \/ Q *) (* ------------------------------------------------------------------------- *) val LEFT_FORALL_OR_THM = thm (#(FILE), #(LINE))("LEFT_FORALL_OR_THM", let val x = “x:'a” val f = “P:'a->bool” val P = mk_comb(f,x) val Q = “Q:bool” val tm = mk_forall(x,mk_disj(P,Q)) val thm1 = SPEC x (ASSUME tm) val thm2 = CONTR P (MP (ASSUME (mk_neg Q)) (ASSUME Q)) val thm3 = DISJ1 (GEN x (DISJ_CASES thm1 (ASSUME P) thm2)) Q val thm4 = DISJ2 (mk_forall(x,P)) (ASSUME Q) val imp1 = DISCH tm (DISJ_CASES (SPEC Q EXCLUDED_MIDDLE) thm4 thm3) val thm5 = SPEC x (ASSUME (mk_forall(x,P))) val thm6 = ASSUME Q val imp2 = DISCH_ALL (GEN x (DISJ_CASES_UNION (ASSUME(mk_disj(mk_forall(x,P), Q))) thm5 thm6)) in GENL [f,Q] (IMP_ANTISYM_RULE imp1 imp2) end); (* ------------------------------------------------------------------------- *) (* RIGHT_FORALL_OR_THM = |- !P Q. (!x. P \/ Q x) = P \/ (!x. Q x) *) (* ------------------------------------------------------------------------- *) val RIGHT_FORALL_OR_THM = thm (#(FILE), #(LINE))("RIGHT_FORALL_OR_THM", let val x = “x:'a” val P = “P:bool” val g = “Q:'a->bool” val Q = mk_comb(g,x) val tm = mk_forall(x,mk_disj(P,Q)) val thm1 = SPEC x (ASSUME tm) val thm2 = CONTR Q (MP (ASSUME (mk_neg P)) (ASSUME P)) val thm3 = DISJ2 P (GEN x (DISJ_CASES thm1 thm2 (ASSUME Q))) val thm4 = DISJ1 (ASSUME P) (mk_forall(x,Q)) val imp1 = DISCH tm (DISJ_CASES (SPEC P EXCLUDED_MIDDLE) thm4 thm3) val thm5 = ASSUME P val thm6 = SPEC x (ASSUME (mk_forall(x,Q))) val imp2 = DISCH_ALL (GEN x (DISJ_CASES_UNION (ASSUME (mk_disj(P, mk_forall(x,Q)))) thm5 thm6)) in GENL [P,g] (IMP_ANTISYM_RULE imp1 imp2) end); (* ------------------------------------------------------------------------- *) (* BOTH_FORALL_IMP_THM = |- (!x. P ==> Q) = ((?x.P) ==> (!x.Q)) *) (* ------------------------------------------------------------------------- *) val BOTH_FORALL_IMP_THM = thm (#(FILE), #(LINE))("BOTH_FORALL_IMP_THM", let val x = “x:'a” val P = “P:bool” val Q = “Q:bool” val tm = mk_forall(x, mk_imp(P,Q)) val asm = mk_exists(x,P) val th1 = GEN x (CHOOSE(x,ASSUME asm)(UNDISCH(SPEC x (ASSUME tm)))) val imp1 = DISCH tm (DISCH asm th1) val cncl = rand(concl imp1) val th2 = SPEC x (MP (ASSUME cncl) (EXISTS (asm,x) (ASSUME P))) val imp2 = DISCH cncl (GEN x (DISCH P th2)) in GENL [P,Q] (IMP_ANTISYM_RULE imp1 imp2) end); (* ------------------------------------------------------------------------- *) (* LEFT_FORALL_IMP_THM = |- (!x. P[x]==>Q) = ((?x.P[x]) ==> Q) *) (* ------------------------------------------------------------------------- *) val LEFT_FORALL_IMP_THM = thm (#(FILE), #(LINE))("LEFT_FORALL_IMP_THM", let val x = “x:'a” val f = “P:'a->bool” val P = mk_comb(f,x) val Q = “Q:bool” val tm = mk_forall(x, mk_imp(P,Q)) val asm = mk_exists(x,P) val th1 = CHOOSE(x,ASSUME asm)(UNDISCH(SPEC x (ASSUME tm))) val imp1 = DISCH tm (DISCH asm th1) val cncl = rand(concl imp1) val th2 = MP (ASSUME cncl) (EXISTS (asm,x) (ASSUME P)) val imp2 = DISCH cncl (GEN x (DISCH P th2)) in GENL [f,Q] (IMP_ANTISYM_RULE imp1 imp2) end); (* ------------------------------------------------------------------------- *) (* RIGHT_FORALL_IMP_THM = |- (!x. P==>Q[x]) = (P ==> (!x.Q[x])) *) (* ------------------------------------------------------------------------- *) val RIGHT_FORALL_IMP_THM = thm (#(FILE), #(LINE))("RIGHT_FORALL_IMP_THM", let val x = “x:'a” val P = “P:bool” val g = “Q:'a->bool” val Q = mk_comb(g,x) val tm = mk_forall(x, mk_imp(P,Q)) val imp1 = DISCH P(GEN x(UNDISCH(SPEC x(ASSUME tm)))) val cncl = concl imp1 val imp2 = GEN x (DISCH P(SPEC x(UNDISCH (ASSUME cncl)))) in GENL [P,g] (IMP_ANTISYM_RULE (DISCH tm imp1) (DISCH cncl imp2)) end); (* ------------------------------------------------------------------------- *) (* BOTH_EXISTS_IMP_THM = |- (?x. P ==> Q) = ((!x.P) ==> (?x.Q)) *) (* ------------------------------------------------------------------------- *) val BOTH_EXISTS_IMP_THM = thm (#(FILE), #(LINE))("BOTH_EXISTS_IMP_THM", let val x = “x:'a” val P = “P:bool” val Q = “Q:bool” val tm = mk_exists(x,mk_imp(P,Q)) val eQ = mk_exists(x,Q) val aP = mk_forall(x,P) val thm1 = EXISTS(eQ,x)(UNDISCH(ASSUME(mk_imp(P,Q)))) val thm2 = DISCH aP (PROVE_HYP (SPEC x (ASSUME aP)) thm1) val imp1 = DISCH tm (CHOOSE(x,ASSUME tm) thm2) val thm2 = CHOOSE(x,UNDISCH (ASSUME (rand(concl imp1)))) (ASSUME Q) val thm3 = DISCH P (PROVE_HYP (GEN x (ASSUME P)) thm2) val imp2 = DISCH (rand(concl imp1)) (EXISTS(tm,x) thm3) in GENL [P,Q] (IMP_ANTISYM_RULE imp1 imp2) end); (* ------------------------------------------------------------------------- *) (* LEFT_EXISTS_IMP_THM = |- (?x. P[x] ==> Q) = ((!x.P[x]) ==> Q) *) (* ------------------------------------------------------------------------- *) val LEFT_EXISTS_IMP_THM = thm (#(FILE), #(LINE))("LEFT_EXISTS_IMP_THM", let val x = “x:'a” val f = “P:'a->bool” val P = mk_comb(f,x) val Q = “Q:bool” val tm = mk_exists(x, mk_imp(P,Q)) val allp = mk_forall(x,P) val th1 = SPEC x (ASSUME allp) val thm1 = MP (ASSUME(mk_imp(P,Q))) th1 val imp1 = DISCH tm (CHOOSE(x,ASSUME tm)(DISCH allp thm1)) val otm = rand(concl imp1) val thm2 = EXISTS(tm,x)(DISCH P (UNDISCH(ASSUME otm))) val nex = mk_exists(x,mk_neg P) val asm1 = EXISTS (nex, x) (ASSUME (mk_neg P)) val th2 = CCONTR P (MP (ASSUME (mk_neg nex)) asm1) val th3 = CCONTR nex (MP (ASSUME (mk_neg allp)) (GEN x th2)) val thm4 = DISCH P (CONTR Q (UNDISCH (ASSUME (mk_neg P)))) val thm5 = CHOOSE(x,th3)(EXISTS(tm,x)thm4) val thm6 = DISJ_CASES (SPEC allp EXCLUDED_MIDDLE) thm2 thm5 val imp2 = DISCH otm thm6 in GENL [f, Q] (IMP_ANTISYM_RULE imp1 imp2) end); (* ------------------------------------------------------------------------- *) (* RIGHT_EXISTS_IMP_THM = |- (?x. P ==> Q[x]) = (P ==> (?x.Q[x])) *) (* ------------------------------------------------------------------------- *) val RIGHT_EXISTS_IMP_THM = thm (#(FILE), #(LINE))("RIGHT_EXISTS_IMP_THM", let val x = “x:'a” val P = “P:bool” val g = “Q:'a->bool” val Q = mk_comb(g,x) val tm = mk_exists(x,mk_imp(P,Q)) val thm1 = EXISTS (mk_exists(x,Q),x) (UNDISCH(ASSUME(mk_imp(P,Q)))) val imp1 = DISCH tm (CHOOSE(x,ASSUME tm) (DISCH P thm1)) val thm2 = UNDISCH (ASSUME (rand(concl imp1))) val thm3 = CHOOSE (x,thm2) (EXISTS (tm,x) (DISCH P (ASSUME Q))) val thm4 = EXISTS(tm,x)(DISCH P(CONTR Q(UNDISCH(ASSUME(mk_neg P))))) val thm5 = DISJ_CASES (SPEC P EXCLUDED_MIDDLE) thm3 thm4 val imp2 = DISCH(rand(concl imp1)) thm5 in GENL [P,g] (IMP_ANTISYM_RULE imp1 imp2) end); (* --------------------------------------------------------------------- *) (* OR_IMP_THM = |- !A B. (A = B \/ A) = (B ==> A) *) (* [TFM 90.06.28] *) (* --------------------------------------------------------------------- *) val OR_IMP_THM = thm (#(FILE), #(LINE))("OR_IMP_THM", let val t1 = “A:bool” and t2 = “B:bool” val asm1 = ASSUME “^t1 = (^t2 \/ ^t1)” and asm2 = EQT_INTRO(ASSUME t2) val th1 = SUBST [t2 |-> asm2] (concl asm1) asm1 val th2 = TRANS th1 (CONJUNCT1 (SPEC t1 OR_CLAUSES)) val imp1 = DISCH (concl asm1) (DISCH t2 (EQT_ELIM th2)) val asm3 = ASSUME “^t2 ==> ^t1” and asm4 = ASSUME “^t2 \/ ^t1” val th3 = DISJ_CASES asm4 (MP asm3 (ASSUME t2)) (ASSUME t1) val th4 = DISCH (concl asm4) th3 and th5 = DISCH t1 (DISJ2 t2 (ASSUME t1)) val imp2 = DISCH “^t2 ==> ^t1” (IMP_ANTISYM_RULE th5 th4) in GEN t1 (GEN t2 (IMP_ANTISYM_RULE imp1 imp2)) end); (* --------------------------------------------------------------------- *) (* NOT_IMP = |- !A B. ~(A ==> B) = A /\ ~B *) (* [TFM 90.07.09] *) (* --------------------------------------------------------------------- *) val NOT_IMP = thm (#(FILE), #(LINE))("NOT_IMP", let val t1 = “A:bool” and t2 = “B:bool” val asm1 = ASSUME “~(^t1 ==> ^t2)” val thm1 = SUBST [t1 |-> EQF_INTRO (ASSUME (mk_neg t1))] (concl asm1) asm1 val thm2 = CCONTR t1 (MP thm1 (DISCH“F”(CONTR t2 (ASSUME“F”)))) val thm3 = SUBST [t2 |-> EQT_INTRO (ASSUME t2)] (concl asm1) asm1 val thm4 = NOT_INTRO(DISCH t2 (MP thm3 (DISCH t1 (ADD_ASSUM t1 TRUTH)))) val imp1 = DISCH (concl asm1) (CONJ thm2 thm4) val conj = ASSUME “^t1 /\ ~^t2” val (asm2,asm3) = (CONJUNCT1 conj, CONJUNCT2 conj) val asm4 = ASSUME “^t1 ==> ^t2” val thm5 = MP (SUBST [t2 |-> EQF_INTRO asm3] (concl asm4) asm4) asm2 val imp2 = DISCH “^t1 /\ ~ ^t2” (NOT_INTRO(DISCH “^t1 ==> ^t2” thm5)) in GEN t1 (GEN t2 (IMP_ANTISYM_RULE imp1 imp2)) end); (* --------------------------------------------------------------------- *) (* DISJ_ASSOC: |- !A B C. A \/ B \/ C = (A \/ B) \/ C *) (* --------------------------------------------------------------------- *) val DISJ_ASSOC = thm (#(FILE), #(LINE))("DISJ_ASSOC", let val t1 = “A:bool” and t2 = “B:bool” and t3 = “C:bool” val at1 = DISJ1 (DISJ1 (ASSUME t1) t2) t3 and at2 = DISJ1 (DISJ2 t1 (ASSUME t2)) t3 and at3 = DISJ2 (mk_disj(t1,t2)) (ASSUME t3) val thm = DISJ_CASES (ASSUME (mk_disj(t2,t3))) at2 at3 val thm1 = DISJ_CASES (ASSUME (mk_disj(t1,mk_disj(t2,t3)))) at1 thm val at1 = DISJ1 (ASSUME t1) (mk_disj(t2,t3)) and at2 = DISJ2 t1 (DISJ1 (ASSUME t2) t3) and at3 = DISJ2 t1 (DISJ2 t2 (ASSUME t3)) val thm = DISJ_CASES (ASSUME (mk_disj(t1,t2))) at1 at2 val thm2 = DISJ_CASES (ASSUME (mk_disj(mk_disj(t1,t2),t3))) thm at3 val imp1 = DISCH (mk_disj(t1,mk_disj(t2,t3))) thm1 and imp2 = DISCH (mk_disj(mk_disj(t1,t2),t3)) thm2 in GENL [t1,t2,t3] (IMP_ANTISYM_RULE imp1 imp2) end); (* --------------------------------------------------------------------- *) (* DISJ_SYM: |- !A B. A \/ B = B \/ A *) (* --------------------------------------------------------------------- *) val DISJ_SYM = thm (#(FILE), #(LINE))("DISJ_SYM", let val t1 = “A:bool” and t2 = “B:bool” val th1 = DISJ1 (ASSUME t1) t2 and th2 = DISJ2 t1 (ASSUME t2) val thm1 = DISJ_CASES (ASSUME(mk_disj(t2,t1))) th2 th1 val th1 = DISJ1 (ASSUME t2) t1 and th2 = DISJ2 t2 (ASSUME t1) val thm2 = DISJ_CASES (ASSUME(mk_disj(t1,t2))) th2 th1 val imp1 = DISCH (mk_disj(t2,t1)) thm1 and imp2 = DISCH (mk_disj(t1,t2)) thm2 in GENL [t1,t2] (IMP_ANTISYM_RULE imp2 imp1) end); val _ = thm (#(FILE), #(LINE))("DISJ_COMM", DISJ_SYM); (* --------------------------------------------------------------------- *) (* DE_MORGAN_THM: *) (* |- !A B. (~(t1 /\ t2) = ~t1 \/ ~t2) /\ (~(t1 \/ t2) = ~t1 /\ ~t2) *) (* --------------------------------------------------------------------- *) val DE_MORGAN_THM = thm (#(FILE), #(LINE))("DE_MORGAN_THM", let val t1 = “A:bool” and t2 = “B:bool” val thm1 = let val asm1 = ASSUME “~(^t1 /\ ^t2)” val cnj = MP asm1 (CONJ (ASSUME t1) (ASSUME t2)) val imp1 = let val case1 = DISJ2 “~^t1” (NOT_INTRO(DISCH t2 cnj)) val case2 = DISJ1 (ASSUME “~ ^t1”) “~ ^t2” in DISJ_CASES (SPEC t1 EXCLUDED_MIDDLE) case1 case2 end val th1 = MP (ASSUME “~^t1”) (CONJUNCT1 (ASSUME “^t1 /\ ^t2”)) val th2 = MP (ASSUME “~^t2”) (CONJUNCT2 (ASSUME “^t1 /\ ^t2”)) val imp2 = let val fth = DISJ_CASES (ASSUME “~^t1 \/ ~^t2”) th1 th2 in DISCH “~^t1 \/ ~^t2” (NOT_INTRO(DISCH “^t1 /\ ^t2” fth)) end in IMP_ANTISYM_RULE (DISCH “~(^t1 /\ ^t2)” imp1) imp2 end val thm2 = let val asm1 = ASSUME “~(^t1 \/ ^t2)” val imp1 = let val th1 = NOT_INTRO (DISCH t1(MP asm1 (DISJ1 (ASSUME t1) t2))) val th2 = NOT_INTRO (DISCH t2 (MP asm1 (DISJ2 t1 (ASSUME t2)))) in DISCH “~(^t1 \/ ^t2)” (CONJ th1 th2) end val imp2 = let val asm = ASSUME “^t1 \/ ^t2” val a1 = CONJUNCT1(ASSUME “~^t1 /\ ~^t2”) and a2 = CONJUNCT2(ASSUME “~^t1 /\ ~^t2”) val fth = DISJ_CASES asm (UNDISCH a1) (UNDISCH a2) in DISCH “~^t1 /\ ~^t2” (NOT_INTRO(DISCH “^t1 \/ ^t2” fth)) end in IMP_ANTISYM_RULE imp1 imp2 end in GEN t1 (GEN t2 (CONJ thm1 thm2)) end); (* -------------------------------------------------------------------------*) (* Distributive laws: *) (* *) (* LEFT_AND_OVER_OR |- !A B C. A /\ (B \/ C) = A /\ B \/ A /\ C *) (* *) (* RIGHT_AND_OVER_OR |- !A B C. (B \/ C) /\ A = B /\ A \/ C /\ A *) (* *) (* LEFT_OR_OVER_AND |- !A B C. A \/ B /\ C = (A \/ B) /\ (A \/ C) *) (* *) (* RIGHT_OR_OVER_AND |- !A B C. B /\ C \/ A = (B \/ A) /\ (C \/ A) *) (* -------------------------------------------------------------------------*) val LEFT_AND_OVER_OR = thm (#(FILE), #(LINE))("LEFT_AND_OVER_OR", let val t1 = “A:bool” and t2 = “B:bool” and t3 = “C:bool” val (th1,th2) = CONJ_PAIR(ASSUME (mk_conj(t1,mk_disj(t2,t3)))) val th3 = CONJ th1 (ASSUME t2) and th4 = CONJ th1 (ASSUME t3) val th5 = DISJ_CASES_UNION th2 th3 th4 val imp1 = DISCH (mk_conj(t1,mk_disj(t2,t3))) th5 val (th1,th2) = (I ## C DISJ1 t3) (CONJ_PAIR (ASSUME (mk_conj(t1,t2)))) val (th3,th4) = (I ## DISJ2 t2) (CONJ_PAIR (ASSUME (mk_conj(t1,t3)))) val th5 = CONJ th1 th2 and th6 = CONJ th3 th4 val th6 = DISJ_CASES (ASSUME (rand(concl imp1))) th5 th6 val imp2 = DISCH (rand(concl imp1)) th6 in GEN t1 (GEN t2 (GEN t3 (IMP_ANTISYM_RULE imp1 imp2))) end); val RIGHT_AND_OVER_OR = thm (#(FILE), #(LINE))("RIGHT_AND_OVER_OR", let val t1 = “A:bool” and t2 = “B:bool” and t3 = “C:bool” val (th1,th2) = CONJ_PAIR(ASSUME (mk_conj(mk_disj(t2,t3),t1))) val th3 = CONJ (ASSUME t2) th2 and th4 = CONJ (ASSUME t3) th2 val th5 = DISJ_CASES_UNION th1 th3 th4 val imp1 = DISCH (mk_conj(mk_disj(t2,t3),t1)) th5 val (th1,th2) = (C DISJ1 t3 ## I) (CONJ_PAIR (ASSUME (mk_conj(t2,t1)))) val (th3,th4) = (DISJ2 t2 ## I) (CONJ_PAIR (ASSUME (mk_conj(t3,t1)))) val th5 = CONJ th1 th2 and th6 = CONJ th3 th4 val th6 = DISJ_CASES (ASSUME (rand(concl imp1))) th5 th6 val imp2 = DISCH (rand(concl imp1)) th6 in GEN t1 (GEN t2 (GEN t3 (IMP_ANTISYM_RULE imp1 imp2))) end); val LEFT_OR_OVER_AND = thm (#(FILE), #(LINE))("LEFT_OR_OVER_AND", let val t1 = “A:bool” and t2 = “B:bool” and t3 = “C:bool” val th1 = ASSUME (mk_disj(t1,mk_conj(t2,t3))) val th2 = CONJ (DISJ1 (ASSUME t1) t2) (DISJ1 (ASSUME t1) t3) val (th3,th4) = CONJ_PAIR (ASSUME(mk_conj(t2,t3))) val th5 = CONJ (DISJ2 t1 th3) (DISJ2 t1 th4) val imp1 = DISCH (concl th1) (DISJ_CASES th1 th2 th5) val (th1,th2) = CONJ_PAIR (ASSUME (rand(concl imp1))) val th3 = DISJ1 (ASSUME t1) (mk_conj(t2,t3)) val (th4,th5) = CONJ_PAIR (ASSUME (mk_conj(t2,t3))) val th4 = DISJ2 t1 (CONJ (ASSUME t2) (ASSUME t3)) val th5 = DISJ_CASES th2 th3 (DISJ_CASES th1 th3 th4) val imp2 = DISCH (rand(concl imp1)) th5 in GEN t1 (GEN t2 (GEN t3 (IMP_ANTISYM_RULE imp1 imp2))) end); val RIGHT_OR_OVER_AND = thm (#(FILE), #(LINE))("RIGHT_OR_OVER_AND", let val t1 = “A:bool” and t2 = “B:bool” and t3 = “C:bool” val th1 = ASSUME (mk_disj(mk_conj(t2,t3),t1)) val th2 = CONJ (DISJ2 t2 (ASSUME t1)) (DISJ2 t3 (ASSUME t1)) val (th3,th4) = CONJ_PAIR (ASSUME(mk_conj(t2,t3))) val th5 = CONJ (DISJ1 th3 t1) (DISJ1 th4 t1) val imp1 = DISCH (concl th1) (DISJ_CASES th1 th5 th2) val (th1,th2) = CONJ_PAIR (ASSUME (rand(concl imp1))) val th3 = DISJ2 (mk_conj(t2,t3)) (ASSUME t1) val (th4,th5) = CONJ_PAIR (ASSUME (mk_conj(t2,t3))) val th4 = DISJ1 (CONJ (ASSUME t2) (ASSUME t3)) t1 val th5 = DISJ_CASES th2 (DISJ_CASES th1 th4 th3) th3 val imp2 = DISCH (rand(concl imp1)) th5 in GEN t1 (GEN t2 (GEN t3 (IMP_ANTISYM_RULE imp1 imp2))) end); (*---------------------------------------------------------------------------* * IMP_DISJ_THM = |- !A B. A ==> B = ~A \/ B * *---------------------------------------------------------------------------*) val IMP_DISJ_THM = thm (#(FILE), #(LINE))("IMP_DISJ_THM", let val A = “A:bool” val B = “B:bool” val th1 = ASSUME “A ==> B” val th2 = ASSUME A val th3 = MP th1 th2 val th4 = DISJ2 “~A” th3 val th5 = ASSUME “~A”; val th6 = ADD_ASSUM “A ==> B” th5 val th7 = DISJ1 th6 B val th8 = SPEC A EXCLUDED_MIDDLE val th9 = DISJ_CASES th8 th4 th7 val th10 = EQT_INTRO th2 val th11 = ASSUME “~A \/ B” val th12 = SUBST [A |-> th10] (concl th11) th11 val th13 = CONJUNCT1 (CONJUNCT2 NOT_CLAUSES) val th14 = SUBST [A |-> th13] (subst [“~T” |-> A] (concl th12)) th12 val th15 = CONJUNCT1 (CONJUNCT2(CONJUNCT2 (SPEC B OR_CLAUSES))) val th16 = SUBST [A |-> th15] A th14 val th17 = DISCH A th16 val th18 = DISCH (concl th11) th17 in GENL [A,B] (IMP_ANTISYM_RULE (DISCH (hd(hyp th9)) th9) th18) end); (*----------------------------------------------------------------------*) (* DISJ_IMP_THM = |- !P Q R. P \/ Q ==> R = (P ==> R) /\ (Q ==> R) *) (* MN 99.05.06 *) (*----------------------------------------------------------------------*) val DISJ_IMP_THM = let val P = “P:bool” val Q = “Q:bool” val R = “R:bool” val lhs = “P \/ Q ==> R” val rhs = “(P ==> R) /\ (Q ==> R)” val ass_lhs = ASSUME lhs val ass_P = ASSUME P val ass_Q = ASSUME Q val p_imp_r = DISCH P (MP ass_lhs (DISJ1 ass_P Q)) val q_imp_r = DISCH Q (MP ass_lhs (DISJ2 P ass_Q)) val lr_imp = DISCH lhs (CONJ p_imp_r q_imp_r) (* half way there! *) val ass_rhs = ASSUME rhs val porq = “P \/ Q” val ass_porq = ASSUME porq val my_and1 = SPECL [“P ==> R”, “Q ==> R”] AND1_THM val p_imp_r = MP my_and1 ass_rhs val r_from_p = MP p_imp_r ass_P val my_and2 = SPECL [“P ==> R”, “Q ==> R”] AND2_THM val q_imp_r = MP my_and2 ass_rhs val r_from_q = MP q_imp_r ass_Q val rl_imp = DISCH rhs (DISCH porq (DISJ_CASES ass_porq r_from_p r_from_q)) in thm (#(FILE), #(LINE))("DISJ_IMP_THM", GENL [P,Q,R] (IMP_ANTISYM_RULE lr_imp rl_imp)) end (* ---------------------------------------------------------------------- IMP_CONJ_THM = |- !P Q R. P ==> Q /\ R = (P ==> Q) /\ (P ==> R) MN 2002.10.06 ---------------------------------------------------------------------- *) val IMP_CONJ_THM = let val P = mk_var("P", bool) val Q = mk_var("Q", bool) val R = mk_var("R", bool) val QandR = mk_conj(Q,R) val PimpQandR = mk_imp(P, QandR) val PiQaR_th = ASSUME PimpQandR val P_th = ASSUME P val QaR_th = MP PiQaR_th P_th val (Q_th, R_th) = CONJ_PAIR QaR_th val PQ_th = DISCH P Q_th val PR_th = DISCH P R_th val L2R = DISCH PimpQandR (CONJ PQ_th PR_th) val PiQ = mk_imp(P, Q) val PiR = mk_imp(P, R) val PiQaPiR = mk_conj(PiQ, PiR) val PiQaPiR_th = ASSUME PiQaPiR val (PiQ_th, PiR_th) = CONJ_PAIR PiQaPiR_th val Q_th = MP PiQ_th P_th val R_th = MP PiR_th P_th val QaR_th = CONJ Q_th R_th val R2L = DISCH PiQaPiR (DISCH P QaR_th) in thm (#(FILE), #(LINE))("IMP_CONJ_THM", GENL [P,Q,R] (IMP_ANTISYM_RULE L2R R2L)) end (* ---------------------------------------------------------------------*) (* IMP_F_EQ_F *) (* *) (* |- !t. t ==> F = (t = F) *) (* RJB 92.09.26 *) (* ---------------------------------------------------------------------*) local fun nthCONJUNCT n cth = let val th = funpow (n-1) CONJUNCT2 cth in if (can dest_conj (concl th)) then CONJUNCT1 th else th end in val IMP_F_EQ_F = thm (#(FILE), #(LINE))("IMP_F_EQ_F", GEN “t:bool” (TRANS (nthCONJUNCT 5 (SPEC_ALL IMP_CLAUSES)) (SYM (nthCONJUNCT 4 (SPEC_ALL EQ_CLAUSES))))) end; (* ---------------------------------------------------------------------*) (* AND_IMP_INTRO *) (* *) (* |- !t1 t2 t3. t1 ==> t2 ==> t3 = t1 /\ t2 ==> t3 *) (* RJB 92.09.26 *) (* ---------------------------------------------------------------------*) val AND_IMP_INTRO = thm (#(FILE), #(LINE))("AND_IMP_INTRO", let val t1 = “t1:bool” and t2 = “t2:bool” and t3 = “t3:bool” and imp = “$==>” val [IMP1,IMP2,IMP3,_,IMP4] = map GEN_ALL(CONJUNCTS (SPEC_ALL IMP_CLAUSES)) and [AND1,AND2,AND3,AND4,_] = map GEN_ALL(CONJUNCTS (SPEC_ALL AND_CLAUSES)) val thTl = SPEC “t2 ==> t3” IMP1 and thFl = SPEC “t2 ==> t3” IMP3 val thTr = AP_THM (AP_TERM imp (SPEC t2 AND1)) t3 and thFr = TRANS (AP_THM (AP_TERM imp (SPEC t2 AND3)) t3)(SPEC t3 IMP3) val thT1 = TRANS thTl (SYM thTr) and thF1 = TRANS thFl (SYM thFr) val tm = “t1 ==> t2 ==> t3 <=> t1 /\ t2 ==> t3” val thT2 = SUBST_CONV [t1 |-> ASSUME “t1 = T”] tm tm and thF2 = SUBST_CONV [t1 |-> ASSUME “t1 = F”] tm tm val thT3 = EQ_MP (SYM thT2) thT1 and thF3 = EQ_MP (SYM thF2) thF1 in GENL [t1,t2,t3] (DISJ_CASES (SPEC t1 BOOL_CASES_AX) thT3 thF3) end); (* ---------------------------------------------------------------------*) (* EQ_IMP_THM *) (* *) (* |- !t1 t2. (t1 = t2) = (t1 ==> t2) /\ (t2 ==> t1) *) (* *) (* RJB 92.09.26 *) (* ---------------------------------------------------------------------*) val EQ_IMP_THM = thm (#(FILE), #(LINE))("EQ_IMP_THM", let val t1 = “t1:bool” and t2 = “t2:bool” val conj = “$/\” val [IMP1,IMP2,IMP3,_,IMP4] = map GEN_ALL(CONJUNCTS (SPEC_ALL IMP_CLAUSES)) and [AND1,AND2,AND3,AND4,_] = map GEN_ALL(CONJUNCTS (SPEC_ALL AND_CLAUSES)) and [EQ1,EQ2,EQ3,EQ4] = map GEN_ALL (CONJUNCTS (SPEC_ALL EQ_CLAUSES)) val thTl = SPEC t2 EQ1 and thFl = SPEC t2 EQ3 val thTr = TRANS (MK_COMB (AP_TERM conj (SPEC t2 IMP1), SPEC t2 IMP2)) (SPEC t2 AND2) and thFr = TRANS (MK_COMB (AP_TERM conj (SPEC t2 IMP3), SPEC t2 IMP4)) (SPEC (mk_neg t2) AND1) val thT1 = TRANS thTl (SYM thTr) and thF1 = TRANS thFl (SYM thFr) val tm = “(t1 = t2) <=> (t1 ==> t2) /\ (t2 ==> t1)” val thT2 = SUBST_CONV [t1 |-> ASSUME “t1 = T”] tm tm and thF2 = SUBST_CONV [t1 |-> ASSUME “t1 = F”] tm tm val thT3 = EQ_MP (SYM thT2) thT1 and thF3 = EQ_MP (SYM thF2) thF1 in GENL [t1,t2] (DISJ_CASES (SPEC t1 BOOL_CASES_AX) thT3 thF3) end); (* ---------------------------------------------------------------------*) (* EQ_EXPAND = |- !t1 t2. (t1 = t2) = ((t1 /\ t2) \/ (~t1 /\ ~t2)) *) (* RJB 92.09.26 *) (* ---------------------------------------------------------------------*) val EQ_EXPAND = thm (#(FILE), #(LINE))("EQ_EXPAND", let val t1 = “t1:bool” and t2 = “t2:bool” val conj = “$/\” and disj = “$\/” val [NOT1,NOT2] = tl (CONJUNCTS NOT_CLAUSES) and [EQ1,EQ2,EQ3,EQ4] = map GEN_ALL (CONJUNCTS (SPEC_ALL EQ_CLAUSES)) and [OR1,OR2,OR3,OR4,_] = map GEN_ALL (CONJUNCTS (SPEC_ALL OR_CLAUSES)) and [AND1,AND2,AND3,AND4,_] = map GEN_ALL (CONJUNCTS(SPEC_ALL AND_CLAUSES)) val thTl = SPEC t2 EQ1 and thFl = SPEC t2 EQ3 val thTr = TRANS (MK_COMB (AP_TERM disj (SPEC t2 AND1), TRANS (AP_THM (AP_TERM conj NOT1) (mk_neg t2)) (SPEC (mk_neg t2) AND3))) (SPEC t2 OR4) and thFr = TRANS (MK_COMB (AP_TERM disj (SPEC t2 AND3), TRANS (AP_THM (AP_TERM conj NOT2) (mk_neg t2)) (SPEC (mk_neg t2) AND1))) (SPEC (mk_neg t2) OR3) val thT1 = TRANS thTl (SYM thTr) and thF1 = TRANS thFl (SYM thFr) val tm = “(t1 = t2) <=> (t1 /\ t2) \/ (~t1 /\ ~t2)” val thT2 = SUBST_CONV [t1 |-> ASSUME “t1 = T”] tm tm and thF2 = SUBST_CONV [t1 |-> ASSUME “t1 = F”] tm tm val thT3 = EQ_MP (SYM thT2) thT1 and thF3 = EQ_MP (SYM thF2) thF1 in GENL [t1,t2] (DISJ_CASES (SPEC t1 BOOL_CASES_AX) thT3 thF3) end); (* ---------------------------------------------------------------------*) (* COND_RATOR |- !b (f:'a->'b) g x. (b => f | g) x = (b => f x | g x) *) (* *) (* RJB 92.09.26 *) (* ---------------------------------------------------------------------*) val COND_RATOR = thm (#(FILE), #(LINE))("COND_RATOR", let val f = “f: 'a -> 'b” val g = “g: 'a -> 'b” val x = “x:'a” and b = “b:bool” val fx = “^f ^x” and gx = “^g ^x” val t1 = “t1:'a” val t2 = “t2:'a” val theta1 = [“:'a” |-> “:'a -> 'b”] val theta2 = [“:'a” |-> “:'b”] val (COND_T,COND_F) = (GENL[t1,t2]##GENL[t1,t2]) (CONJ_PAIR(SPEC_ALL COND_CLAUSES)) val thTl = AP_THM (SPECL [f,g] (INST_TYPE theta1 COND_T)) x and thFl = AP_THM (SPECL [f,g] (INST_TYPE theta1 COND_F)) x val thTr = SPECL [fx,gx] (INST_TYPE theta2 COND_T) and thFr = SPECL [fx,gx] (INST_TYPE theta2 COND_F) val thT1 = TRANS thTl (SYM thTr) and thF1 = TRANS thFl (SYM thFr) val tm = “(if b then (f:'a->'b ) else g) x = (if b then f x else g x)” val thT2 = SUBST_CONV [b |-> ASSUME “b = T”] tm tm and thF2 = SUBST_CONV [b |-> ASSUME “b = F”] tm tm val thT3 = EQ_MP (SYM thT2) thT1 and thF3 = EQ_MP (SYM thF2) thF1 in GENL [b,f,g,x] (DISJ_CASES (SPEC b BOOL_CASES_AX) thT3 thF3) end); (* ---------------------------------------------------------------------*) (* COND_RAND *) (* *) (* |- !(f:'a->'b) b x y. f (b => x | y) = (b => f x | f y) *) (* *) (* RJB 92.09.26 *) (* ---------------------------------------------------------------------*) val COND_RAND = thm (#(FILE), #(LINE))("COND_RAND", let val f = “f: 'a -> 'b” val x = “x:'a” val y = “y:'a” and b = “b:bool” val fx = “^f ^x” and fy = “^f ^y” val t1 = “t1:'a” val t2 = “t2:'a” val theta = [Type.alpha |-> Type.beta] val (COND_T,COND_F) = (GENL[t1,t2]##GENL[t1,t2]) (CONJ_PAIR (SPEC_ALL COND_CLAUSES)) val thTl = AP_TERM f (SPECL [x,y] COND_T) and thFl = AP_TERM f (SPECL [x,y] COND_F) val thTr = SPECL [fx,fy] (INST_TYPE theta COND_T) and thFr = SPECL [fx,fy] (INST_TYPE theta COND_F) val thT1 = TRANS thTl (SYM thTr) and thF1 = TRANS thFl (SYM thFr) val tm = “(f:'a->'b ) (if b then x else y) = (if b then f x else f y)” val thT2 = SUBST_CONV [b |-> ASSUME “b = T”] tm tm and thF2 = SUBST_CONV [b |-> ASSUME “b = F”] tm tm val thT3 = EQ_MP (SYM thT2) thT1 and thF3 = EQ_MP (SYM thF2) thF1 in GENL [f,b,x,y] (DISJ_CASES (SPEC b BOOL_CASES_AX) thT3 thF3) end); (* ---------------------------------------------------------------------*) (* COND_ABS *) (* *) (* |- !b (f:'a->'b) g. (\x. (b => f(x) | g(x))) = (b => f | g) *) (* *) (* RJB 92.09.26 *) (* ---------------------------------------------------------------------*) val COND_ABS = thm (#(FILE), #(LINE))("COND_ABS", let val b = “b:bool” val f = “f:'a->'b” val g = “g:'a->'b” val x = “x:'a” in GENL [b,f,g] (TRANS (ABS x (SYM (SPECL [b,f,g,x] COND_RATOR))) (ETA_CONV “\ ^x. (if ^b then ^f else ^g) ^x”)) end); (* ---------------------------------------------------------------------*) (* COND_EXPAND *) (* *) (* |- !b t1 t2. (b => t1 | t2) = ((~b \/ t1) /\ (b \/ t2)) *) (* *) (* RJB 92.09.26 *) (* ---------------------------------------------------------------------*) val COND_EXPAND = thm (#(FILE), #(LINE))("COND_EXPAND", let val b = “b:bool” val t1 = “t1:bool” val t2 = “t2:bool” val conj = “$/\” val disj = “$\/” val theta = [“:'a” |-> Type.bool] val (COND_T,COND_F) = let val t1 = “t1:'a” and t2 = “t2:'a” in (GENL[t1,t2]##GENL[t1,t2]) (CONJ_PAIR(SPEC_ALL COND_CLAUSES)) end and [NOT1,NOT2] = tl (CONJUNCTS NOT_CLAUSES) and [OR1,OR2,OR3,OR4,_] = map GEN_ALL (CONJUNCTS (SPEC_ALL OR_CLAUSES)) and [AND1,AND2,AND3,AND4,_] = map GEN_ALL (CONJUNCTS(SPEC_ALL AND_CLAUSES)) val thTl = SPECL [t1,t2] (INST_TYPE theta COND_T) and thFl = SPECL [t1,t2] (INST_TYPE theta COND_F) val thTr = let val th1 = TRANS (AP_THM (AP_TERM disj NOT1) t1) (SPEC t1 OR3) and th2 = SPEC t2 OR1 in TRANS (MK_COMB (AP_TERM conj th1,th2)) (SPEC t1 AND2) end and thFr = let val th1 = TRANS (AP_THM (AP_TERM disj NOT2) t1) (SPEC t1 OR1) and th2 = SPEC t2 OR3 in TRANS (MK_COMB (AP_TERM conj th1,th2)) (SPEC t2 AND1) end val thT1 = TRANS thTl (SYM thTr) and thF1 = TRANS thFl (SYM thFr) val tm = “(if b then t1 else t2) = ((~b \/ t1) /\ (b \/ t2))” val thT2 = SUBST_CONV [b |-> ASSUME “b = T”] tm tm and thF2 = SUBST_CONV [b |-> ASSUME “b = F”] tm tm val thT3 = EQ_MP (SYM thT2) thT1 and thF3 = EQ_MP (SYM thF2) thF1 in GENL [b, t1, t2] (DISJ_CASES (SPEC b BOOL_CASES_AX) thT3 thF3) end); (* ---------------------------------------------------------------------*) (* COND_EXPAND_IMP *) (* *) (* |- !b t1 t2. (b => t1 | t2) = ((b ==> t1) /\ (~b ==> t2)) *) (* *) (* TT 09.03.18 *) (* ---------------------------------------------------------------------*) val COND_EXPAND_IMP = thm (#(FILE), #(LINE))("COND_EXPAND_IMP", let val b = “b:bool” val t1 = “t1:bool” val t2 = “t2:bool” val nb = mk_neg b; val nnb = mk_neg nb; val imp_th1 = SPECL [b, t1] IMP_DISJ_THM; val imp_th2a = SPECL [nb, t2] IMP_DISJ_THM val imp_th2b = SUBST_CONV [nnb |-> (SPEC b (CONJUNCT1 NOT_CLAUSES))] (mk_disj (nnb, t2)) (mk_disj (nnb, t2)) val imp_th2 = TRANS imp_th2a imp_th2b val new_rhs = “(b ==> t1) /\ (~b ==> t2)”; val subst = [mk_imp(b,t1) |-> imp_th1, mk_imp(nb,t2) |-> imp_th2] val th1 = SUBST_CONV subst new_rhs new_rhs val th2 = TRANS (SPECL [b,t1,t2] COND_EXPAND) (SYM th1) in GENL [b,t1,t2] th2 end); (* ---------------------------------------------------------------------*) (* COND_EXPAND_OR *) (* *) (* |- !b t1 t2. (b => t1 | t2) = ((b /\ t1) \/ (~b /\ t2)) *) (* *) (* TT 09.03.18 *) (* ---------------------------------------------------------------------*) val COND_EXPAND_OR = thm (#(FILE), #(LINE))("COND_EXPAND_OR", let val b = “b:bool” val t1 = “t1:bool” val t2 = “t2:bool” val conj = “$/\” val disj = “$\/” val theta = [“:'a” |-> Type.bool] val (COND_T,COND_F) = let val t1 = “t1:'a” and t2 = “t2:'a” in (GENL[t1,t2]##GENL[t1,t2]) (CONJ_PAIR(SPEC_ALL COND_CLAUSES)) end and [NOT1,NOT2] = tl (CONJUNCTS NOT_CLAUSES) and [OR1,OR2,OR3,OR4,_] = map GEN_ALL (CONJUNCTS (SPEC_ALL OR_CLAUSES)) and [AND1,AND2,AND3,AND4,_] = map GEN_ALL (CONJUNCTS(SPEC_ALL AND_CLAUSES)) val thTl = SPECL [t1,t2] (INST_TYPE theta COND_T) and thFl = SPECL [t1,t2] (INST_TYPE theta COND_F) val thTr = let val th2 = TRANS (AP_THM (AP_TERM conj NOT1) t2) (SPEC t2 AND3) and th1 = SPEC t1 AND1 in TRANS (MK_COMB (AP_TERM disj th1,th2)) (SPEC t1 OR4) end and thFr = let val th2 = TRANS (AP_THM (AP_TERM conj NOT2) t2) (SPEC t2 AND1) and th1 = SPEC t1 AND3 in TRANS (MK_COMB (AP_TERM disj th1,th2)) (SPEC t2 OR3) end val thT1 = TRANS thTl (SYM thTr) and thF1 = TRANS thFl (SYM thFr) val tm = “(if b then t1 else t2) = ((b /\ t1) \/ (~b /\ t2))” val thT2 = SUBST_CONV [b |-> ASSUME “b = T”] tm tm and thF2 = SUBST_CONV [b |-> ASSUME “b = F”] tm tm val thT3 = EQ_MP (SYM thT2) thT1 and thF3 = EQ_MP (SYM thF2) thF1 in GENL [b, t1, t2] (DISJ_CASES (SPEC b BOOL_CASES_AX) thT3 thF3) end); val TYPE_DEFINITION_THM = thm (#(FILE), #(LINE))("TYPE_DEFINITION_THM", let val P = “P:'a-> bool” val rep = “rep :'b -> 'a” in GEN P (GEN rep (RIGHT_BETA(AP_THM (RIGHT_BETA (AP_THM TYPE_DEFINITION P)) rep))) end); val ONTO_THM = thm (#(FILE), #(LINE))( "ONTO_THM", let val f = mk_var("f", Type.alpha --> Type.beta) in GEN f (RIGHT_BETA (AP_THM ONTO_DEF f)) end); val ONE_ONE_THM = thm (#(FILE), #(LINE))( "ONE_ONE_THM", let val f = mk_var("f", Type.alpha --> Type.beta) in GEN f (RIGHT_BETA (AP_THM ONE_ONE_DEF f)) end); (*---------------------------------------------------------------------------* * ABS_REP_THM * * |- !P. (?rep. TYPE_DEFINITION P rep) ==> * * ?rep abs. (!a. abs (rep a) = a) /\ !r. P r = (rep (abs r) = r) * *---------------------------------------------------------------------------*) val ABS_REP_THM = thm (#(FILE), #(LINE))("ABS_REP_THM", let val th1 = ASSUME “?rep:'b->'a. TYPE_DEFINITION P rep” val th2 = MK_EXISTS (SPEC “P:'a->bool” TYPE_DEFINITION_THM) val def = EQ_MP th2 th1 val asm = ASSUME (snd(dest_exists(concl def))) val (asm1,asm2) = CONJ_PAIR asm val rep_eq = let val th1 = DISCH “a:'b=a'” (AP_TERM “rep:'b->'a” (ASSUME “a:'b=a'”)) in IMP_ANTISYM_RULE (SPECL [“a:'b”,“a':'b”] asm1) th1 end val ABS = “\r:'a. @a:'b. r = rep a” val absd = RIGHT_BETA (AP_THM (REFL ABS) “rep (a:'b):'a”) val lem = SYM(SELECT_RULE(EXISTS (“?a':'b.a=a'”,“a:'b”) (REFL “a:'b”))) val TH1 = GEN “a:'b” (TRANS(TRANS absd (SELECT_EQ “a':'b” rep_eq)) lem) val t1 = SELECT_RULE(EQ_MP (SPEC “r:'a” asm2) (ASSUME “(P:'a->bool) r”)) val absd2 = RIGHT_BETA (AP_THM (REFL ABS) “r:'a”) val v = mk_var("v",type_of(rhs (concl absd2))) val (t1l,t1r) = dest_eq (concl t1) (* val rep = fst(strip_comb t1r) *) val rep = rator t1r val template = mk_eq(t1l, mk_comb(rep,v)) val imp1 = DISCH “(P:'a->bool) r” (SYM (SUBST [v |-> SYM absd2] template t1)) val t2 = EXISTS (“?a:'b. r:'a = rep a”, “^ABS r”) (SYM(ASSUME “rep(^ABS (r:'a):'b) = r”)) val imp2 = DISCH “rep(^ABS (r:'a):'b) = r” (EQ_MP (SYM (SPEC “r:'a” asm2)) t2) val TH2 = GEN “r:'a” (IMP_ANTISYM_RULE imp1 imp2) val CTH = CONJ TH1 TH2 val ath = subst [ABS |-> “abs:'a->'b”] (concl CTH) val eth1 = EXISTS (“?abs:'a->'b. ^ath”, ABS) CTH val eth2 = EXISTS (“?rep:'b->'a. ^(concl eth1)”, “rep:'b->'a”) eth1 val result = DISCH (concl th1) (CHOOSE (“rep:'b->'a”,def) eth2) in GEN “P:'a->bool” result end); (*--------------------------------------------------------------------------- LET_RAND = P (let x = M in N x) = (let x = M in P (N x)) ---------------------------------------------------------------------------*) val LET_RAND = thm (#(FILE), #(LINE))("LET_RAND", let val tm1 = “\x:'a. P (N x:'b):bool” val tm2 = “M:'a” val tm3 = “\x:'a. N x:'b” val P = “P:'b -> bool” val LET_THM1 = RIGHT_BETA (SPEC tm2 (SPEC tm1 (Thm.INST_TYPE [beta |-> bool] LET_THM))) val LET_THM2 = AP_TERM P (RIGHT_BETA (SPEC tm2 (SPEC tm3 LET_THM))) in TRANS LET_THM2 (SYM LET_THM1) end); (*--------------------------------------------------------------------------- LET_RATOR = (let x = M in N x) b = (let x = M in N x b) ---------------------------------------------------------------------------*) val LET_RATOR = thm (#(FILE), #(LINE))("LET_RATOR", let val M = “M:'a” val b = “b:'b” val tm1 = “\x:'a. N x:'b->'c” val tm2 = “\x:'a. N x ^b:'c” val LET_THM1 = AP_THM (RIGHT_BETA (SPEC M (SPEC tm1 (Thm.INST_TYPE [beta |-> (beta --> gamma)] LET_THM)))) b val LET_THM2 = RIGHT_BETA (SPEC M (SPEC tm2 (Thm.INST_TYPE [beta |-> gamma] LET_THM))) in TRANS LET_THM1 (SYM LET_THM2) end); (*--------------------------------------------------------------------------- !P. (!x y. P x y) = (!y x. P x y) ---------------------------------------------------------------------------*) val SWAP_FORALL_THM = thm (#(FILE), #(LINE))("SWAP_FORALL_THM", let val P = mk_var("P", “:'a->'b->bool”) val x = mk_var("x", Type.alpha) val y = mk_var("y", Type.beta) val Pxy = list_mk_comb (P,[x,y]) val th1 = ASSUME (list_mk_forall [x,y] Pxy) val th2 = DISCH_ALL (GEN y (GEN x (SPEC y (SPEC x th1)))) val th3 = ASSUME (list_mk_forall [y,x] Pxy) val th4 = DISCH_ALL (GEN x (GEN y (SPEC x (SPEC y th3)))) in GEN P (IMP_ANTISYM_RULE th2 th4) end); (*--------------------------------------------------------------------------- !P. (?x y. P x y) = (?y x. P x y) ---------------------------------------------------------------------------*) val SWAP_EXISTS_THM = thm (#(FILE), #(LINE))("SWAP_EXISTS_THM", let val P = mk_var("P", “:'a->'b->bool”) val x = mk_var("x", Type.alpha) val y = mk_var("y", Type.beta) val Pxy = list_mk_comb (P,[x,y]) val tm1 = list_mk_exists[x] Pxy val tm2 = list_mk_exists[y] tm1 val tm3 = list_mk_exists[y] Pxy val tm4 = list_mk_exists[x] tm3 val th1 = ASSUME Pxy val th2 = EXISTS(tm2,y) (EXISTS (tm1,x) th1) val th3 = ASSUME (list_mk_exists [y] Pxy) val th4 = CHOOSE(y,th3) th2 val th5 = CHOOSE(x,ASSUME (list_mk_exists [x,y] Pxy)) th4 val th6 = EXISTS(tm4,x) (EXISTS (tm3,y) th1) val th7 = ASSUME (list_mk_exists[x] Pxy) val th8 = CHOOSE(x,th7) th6 val th9 = CHOOSE(y,ASSUME (list_mk_exists [y,x] Pxy)) th8 in GEN P (IMP_ANTISYM_RULE (DISCH_ALL th5) (DISCH_ALL th9)) end); (*--------------------------------------------------------------------------- EXISTS_UNIQUE_THM (?!x. P x) = (?x. P x) /\ (!x y. P x /\ P y ==> (x = y)) ---------------------------------------------------------------------------*) val EXISTS_UNIQUE_THM = thm (#(FILE), #(LINE))("EXISTS_UNIQUE_THM", let val th1 = RIGHT_BETA (AP_THM EXISTS_UNIQUE_DEF “\x:'a. P x:bool”) val th2 = CONV_RULE (RAND_CONV (RAND_CONV (QUANT_CONV (QUANT_CONV (RATOR_CONV (RAND_CONV (RAND_CONV BETA_CONV))))))) th1 in CONV_RULE (RAND_CONV (RAND_CONV (QUANT_CONV (QUANT_CONV (RATOR_CONV (RAND_CONV (RATOR_CONV (RAND_CONV BETA_CONV)))))))) th2 end); (* ---------------------------------------------------------------------- EXISTS_UNIQUE_ALT' |- !P. (?!x. P x) <=> ?x. !y. P y <=> (y = x) ---------------------------------------------------------------------- *) val EXISTS_UNIQUE_ALT' = thm (#(FILE), #(LINE))( "EXISTS_UNIQUE_ALT'", let val eu_r = ASSUME (rhs (concl EXISTS_UNIQUE_THM)) val (eu1, eu2) = CONJ_PAIR eu_r val P = mk_var("P", alpha --> bool) val x = mk_var("x", alpha) val y = mk_var("y", alpha) val c = mk_var("c", alpha) val yeqx = mk_eq(y,x) val Px = mk_comb(P, x) val Py = mk_comb(P, y) val th1a = MP (SPECL [y,x] eu2) (CONJ (ASSUME Py) (ASSUME Px)) |> DISCH Py val th1b = EQ_MP (SYM (AP_TERM P (ASSUME yeqx))) (ASSUME Px) |> DISCH yeqx val th1_noex = IMP_ANTISYM_RULE th1a th1b |> GEN y val th1_noch = EXISTS(mk_exists(x,concl th1_noex), x) th1_noex val th1 = CHOOSE(x,eu1) th1_noch val pyyeq = concl th1 val pyyeqc = subst [x |-> c] (#2 (dest_exists pyyeq)) val pyyeqc_th = ASSUME pyyeqc val th2a = pyyeqc_th |> SPEC c |> C EQ_MP (REFL c) o SYM |> EXISTS(mk_exists(x,Px), c) val (pxy_x,pxy_y) = ASSUME (mk_conj(Px,Py)) |> CONJ_PAIR val th2b1 = pyyeqc_th |> SPEC x |> C EQ_MP (ASSUME Px) |> PROVE_HYP pxy_x val th2b2 = pyyeqc_th |> SPEC y |> C EQ_MP (ASSUME Py) |> PROVE_HYP pxy_y val th2b = TRANS th2b1 (SYM th2b2) |> DISCH (mk_conj(Px,Py)) |> GENL [x,y] val th2 = CHOOSE (c, ASSUME pyyeq) (CONJ th2a th2b) val eqn = IMP_ANTISYM_RULE (DISCH_ALL th1) (DISCH_ALL th2) in TRANS EXISTS_UNIQUE_THM eqn end); (*--------------------------------------------------------------------------- LET_CONG = |- !f g M N. (M = N) /\ (!x. (x = N) ==> (f x = g x)) ==> (LET f M = LET g N) ---------------------------------------------------------------------------*) val LET_CONG = thm (#(FILE), #(LINE))("LET_CONG", let val f = mk_var("f",alpha-->beta) val g = mk_var("g",alpha-->beta) val M = mk_var("M",alpha) val N = mk_var("N",alpha) val x = mk_var ("x",alpha) val MeqN = mk_eq(M,N) val x_eq_N = mk_eq(x,N) val fx_eq_gx = mk_eq(mk_comb(f,x),mk_comb(g,x)) val ctm = mk_forall(x, mk_imp(x_eq_N,fx_eq_gx)) val th = RIGHT_BETA(AP_THM(RIGHT_BETA(AP_THM LET_DEF f)) M) val th1 = ASSUME MeqN val th2 = MP (SPEC N (ASSUME ctm)) (REFL N) val th3 = SUBS [SYM th1] th2 val th4 = TRANS (TRANS th th3) (MK_COMB (REFL g,th1)) val th5 = RIGHT_BETA(AP_THM(RIGHT_BETA(AP_THM LET_DEF g)) N) val th6 = TRANS th4 (SYM th5) val th7 = SUBS [SPECL [MeqN, ctm, concl th6] AND_IMP_INTRO] (DISCH MeqN (DISCH ctm th6)) in GENL [f,g,M,N] th7 end); (*--------------------------------------------------------------------------- IMP_CONG = |- !x x' y y'. (x = x') /\ (x' ==> (y = y')) ==> (x ==> y = x' ==> y') ---------------------------------------------------------------------------*) val IMP_CONG = thm (#(FILE), #(LINE))("IMP_CONG", let val x = mk_var("x",Type.bool) val x' = mk_var("x'",Type.bool) val y = mk_var("y",Type.bool) val y' = mk_var("y'",Type.bool) val x_eq_x' = mk_eq(x,x') val ctm = mk_imp(x', mk_eq(y,y')) val x_imp_y = mk_imp(x,y) val x'_imp_y' = mk_imp(x',y') val th = ASSUME x_eq_x' val th1 = UNDISCH(ASSUME ctm) val th2 = ASSUME x_imp_y val th3 = DISCH x_imp_y (DISCH x' (UNDISCH(SUBS [th,th1] th2))) val th4 = ASSUME x'_imp_y' val th5 = UNDISCH (SUBS [SYM th] (DISCH x' th1)) val th6 = DISCH x'_imp_y' (DISCH x (UNDISCH(SUBS [SYM th,SYM th5] th4))) val th7 = IMP_ANTISYM_RULE th3 th6 val th8 = DISCH x_eq_x' (DISCH ctm th7) val th9 = SUBS [SPECL [x_eq_x', ctm, concl th7] AND_IMP_INTRO] th8 in GENL [x,x',y,y'] th9 end); (*--------------------------------------------------------------------------- AND_CONG = |- !P P' Q Q'. (Q ==> (P = P')) /\ (P' ==> (Q = Q')) ==> (P /\ Q = P' /\ Q') ---------------------------------------------------------------------------*) val AND_CONG = thm (#(FILE), #(LINE))("AND_CONG", let val P = mk_var("P",Type.bool) val P' = mk_var("P'",Type.bool) val Q = mk_var("Q",Type.bool) val Q' = mk_var("Q'",Type.bool) val PandQ = mk_conj(P,Q) val P'andQ' = mk_conj(P',Q') val ctm1 = mk_imp(Q, mk_eq(P,P')) val ctm2 = mk_imp(P', mk_eq(Q,Q')) val th1 = ASSUME PandQ val th2 = MP (ASSUME ctm1) (CONJUNCT2 th1) val th3 = MP (ASSUME ctm2) (SUBS [th2] (CONJUNCT1 th1)) val th4 = DISCH PandQ (SUBS[th2,th3] th1) val th5 = ASSUME P'andQ' val th6 = MP (ASSUME ctm2) (CONJUNCT1 th5) val th7 = MP (ASSUME ctm1) (SUBS [SYM th6] (CONJUNCT2 th5)) val th8 = DISCH P'andQ' (SUBS[SYM th6,SYM th7] th5) val th9 = IMP_ANTISYM_RULE th4 th8 val th10 = SUBS [SPECL [ctm1,ctm2,concl th9] AND_IMP_INTRO] (DISCH ctm1 (DISCH ctm2 th9)) in GENL [P,P',Q,Q'] th10 end); (*--------------------------------------------------------------------------- LEFT_AND_CONG = |- !P P' Q Q'. (P = P') /\ (P' ==> (Q = Q')) ==> (P /\ Q = P' /\ Q') ---------------------------------------------------------------------------*) val LEFT_AND_CONG = thm (#(FILE), #(LINE))("LEFT_AND_CONG", let val P = mk_var("P",Type.bool) val P' = mk_var("P'",Type.bool) val Q = mk_var("Q",Type.bool) val Q' = mk_var("Q'",Type.bool) val PandQ = mk_conj(P,Q) val P'andQ' = mk_conj(P',Q') val ctm1 = mk_eq(P,P') val ctm2 = mk_imp(P', mk_eq(Q,Q')) val th1 = ASSUME PandQ val th2 = ASSUME ctm1 val th3 = SUBS [th2] (CONJUNCT1 th1) val th3a = MP (ASSUME ctm2) th3 val th4 = DISCH PandQ (SUBS[th2,th3a] th1) val th5 = ASSUME P'andQ' val th6 = SUBS [SYM th2] (CONJUNCT1 th5) val th7 = SYM(MP (ASSUME ctm2) (CONJUNCT1 th5)) val th8 = DISCH P'andQ' (SUBS[SYM th2,th7] th5) val th9 = IMP_ANTISYM_RULE th4 th8 val th10 = SUBS [SPECL [ctm1,ctm2,concl th9] AND_IMP_INTRO] (DISCH ctm1 (DISCH ctm2 th9)) in GENL [P,P',Q,Q'] th10 end); (*--------------------------------------------------------------------------- val OR_CONG = |- !P P' Q Q'. (~Q ==> (P = P')) /\ (~P' ==> (Q = Q')) ==> (P \/ Q = P' \/ Q') ---------------------------------------------------------------------------*) val OR_CONG = thm (#(FILE), #(LINE))("OR_CONG", let val P = mk_var("P",Type.bool) val P' = mk_var("P'",Type.bool) val Q = mk_var("Q",Type.bool) val Q' = mk_var("Q'",Type.bool) val notQ = mk_neg Q val notP' = mk_neg P' val PorQ = mk_disj(P,Q) val P'orQ' = mk_disj(P',Q') val PeqP'= mk_eq(P,P') val QeqQ'= mk_eq(Q,Q') val ctm1 = mk_imp(notQ,PeqP') val ctm2 = mk_imp(notP',QeqQ') val th1 = ASSUME PorQ val th2 = ASSUME P val th3 = ASSUME Q val th4 = ASSUME ctm1 val th5 = ASSUME ctm2 val th6 = SUBS [SPEC Q (CONJUNCT1 NOT_CLAUSES)] (SUBS [SPECL[notQ, PeqP'] IMP_DISJ_THM] th4) val th7 = SUBS [SPEC P' (CONJUNCT1 NOT_CLAUSES)] (SUBS [SPECL[notP', QeqQ'] IMP_DISJ_THM] th5) val th8 = ASSUME P' val th9 = DISJ1 th8 Q' val th10 = ASSUME QeqQ' val th11 = SUBS [th10] th3 val th12 = DISJ2 P' th11 val th13 = ASSUME PeqP' val th14 = MK_COMB(REFL(mk_const("\\/",bool-->bool-->bool)),th13) val th15 = EQ_MP (MK_COMB (th14,th10)) th1 val th16 = DISJ_CASES th6 th12 th15 val th17 = DISCH PorQ (DISJ_CASES th7 th9 th16) val th18 = ASSUME P'orQ' val th19 = DISJ2 P th3 val th20 = DISJ1 (SUBS [SYM th13] th8) Q val th21 = EQ_MP (SYM (MK_COMB(th14,th10))) th18 val th22 = DISJ_CASES th7 th20 th21 val th23 = DISCH P'orQ' (DISJ_CASES th6 th19 th22) val th24 = IMP_ANTISYM_RULE th17 th23 val th25 = SUBS [SPECL [ctm1,ctm2,concl th24] AND_IMP_INTRO] (DISCH ctm1 (DISCH ctm2 th24)) in GENL [P,P',Q,Q'] th25 end); (*--------------------------------------------------------------------------- val LEFT_OR_CONG = |- !P P' Q Q'. (P = P') /\ (~P' ==> (Q = Q')) ==> (P \/ Q = P' \/ Q') ---------------------------------------------------------------------------*) val LEFT_OR_CONG = thm (#(FILE), #(LINE))("LEFT_OR_CONG", let fun mk_boolvar s = mk_var(s,Type.bool) val [P,P',Q,Q'] = map mk_boolvar ["P","P'","Q","Q'"] val notP = mk_neg P val notP' = mk_neg P' val PorQ = mk_disj(P,Q) val P'orQ' = mk_disj(P',Q') val PeqP' = mk_eq(P,P') val ctm = mk_imp(notP',mk_eq(Q,Q')) val th1 = ASSUME ctm val th2 = ASSUME PeqP' val th3 = DISJ1 (SUBS [th2] (ASSUME P)) Q' val th4 = MP th1 (SUBS [th2] (ASSUME notP)) val th5 = DISJ2 P' (SUBS [th4] (ASSUME Q)) val th6 = DISJ_CASES (SPEC P EXCLUDED_MIDDLE) th3 th5 val th7 = DISCH PorQ (DISJ_CASES (ASSUME PorQ) th3 th6) val th8 = DISJ1 (SUBS [SYM th2] (ASSUME P')) Q val th9 = MP th1 (ASSUME notP') val th10 = DISJ2 P (SUBS [SYM th9] (ASSUME Q')) val th11 = DISJ_CASES (SPEC P' EXCLUDED_MIDDLE) th8 th10 val th12 = DISCH P'orQ' (DISJ_CASES (ASSUME P'orQ') th8 th11) val th13 = DISCH PeqP' (DISCH ctm (IMP_ANTISYM_RULE th7 th12)) val th14 = SUBS[SPECL [PeqP',ctm,mk_eq(PorQ,P'orQ')] AND_IMP_INTRO] th13 in GENL [P,P',Q,Q'] th14 end); (*--------------------------------------------------------------------------- val COND_CONG = |- !P Q x x' y y'. (P = Q) /\ (Q ==> (x = x')) /\ (~Q ==> (y = y')) ==> ((if P then x else y) = (if Q then x' else y')) ---------------------------------------------------------------------------*) fun mk_cond {cond,larm,rarm} = “if ^cond then ^larm else ^rarm”; val COND_CONG = thm (#(FILE), #(LINE))("COND_CONG", let val P = mk_var("P",Type.bool) val Q = mk_var("Q",Type.bool) val x = mk_var("x",alpha) val x' = mk_var("x'",alpha) val y = mk_var("y",alpha) val y' = mk_var("y'",alpha) val PeqQ = mk_eq(P,Q) val ctm1 = mk_imp(Q, mk_eq(x,x')) val ctm2 = mk_imp(mk_neg Q, mk_eq(y,y')) val target = mk_eq(mk_cond{cond=P,larm=x,rarm=y}, mk_cond{cond=Q,larm=x',rarm=y'}) val OR_ELIM = MP (SPECL[target,P,mk_neg P] OR_ELIM_THM) (SPEC P EXCLUDED_MIDDLE) val th1 = ASSUME P val th2 = EQT_INTRO th1 val th3 = CONJUNCT1 (SPECL [x,y] COND_CLAUSES) val th3a = CONJUNCT1 (SPECL [x',y'] COND_CLAUSES) val th4 = SUBS [SYM th2] th3 val th4a = SUBS [SYM th2] th3a val th5 = ASSUME PeqQ val th6 = ASSUME ctm1 val th7 = ASSUME ctm2 val th8 = UNDISCH (SUBS [SYM th5] th6) val th9 = TRANS th4 th8 val th10 = TRANS th9 (SYM (SUBS [th5] th4a)) val th11 = EQF_INTRO (ASSUME (mk_neg P)) val th12 = CONJUNCT2 (SPECL [x,y] COND_CLAUSES) val th13 = CONJUNCT2 (SPECL [x',y'] COND_CLAUSES) val th14 = SUBS [SYM th11] th12 val th15 = SUBS [SYM th11] th13 val th16 = UNDISCH (SUBS [SYM th5] th7) val th17 = TRANS th14 th16 val th18 = TRANS th17 (SYM (SUBS [th5] th15)) val th19 = MP (MP OR_ELIM (DISCH P th10)) (DISCH (mk_neg P) th18) val th20 = DISCH PeqQ (DISCH ctm1 (DISCH ctm2 th19)) val th21 = SUBS [SPECL [ctm1, ctm2,concl th19] AND_IMP_INTRO] th20 val cnj = mk_conj(ctm1,ctm2) val th22 = SUBS [SPECL [PeqQ,cnj,concl th19] AND_IMP_INTRO] th21 in GENL [P,Q,x,x',y,y'] th22 end); (* ---------------------------------------------------------------------- RES_FORALL_CONG |- (P = Q) ==> (!x. x IN Q ==> (f x = g x)) ==> (RES_FORALL P f = RES_FORALL Q g) RES_EXISTS_CONG |- (P = Q) ==> (!x. x IN Q ==> (f x = g x)) ==> (RES_EXISTS P f = RES_EXISTS P g) ---------------------------------------------------------------------- *) val (RES_FORALL_CONG, RES_EXISTS_CONG) = let (* stuff in common to both *) val aset_ty = alpha --> bool val [P,Q,f,g] = map (fn s => mk_var(s, aset_ty)) ["P", "Q", "f", "g"] val PeqQ_t = mk_eq(P, Q) val PeqQ_th = ASSUME PeqQ_t val x = mk_var("x", alpha) val fx_t = mk_comb(f, x) val gx_t = mk_comb(g, x) val IN_t = prim_mk_const {Thy = "bool", Name = "IN"} val xINP_t = list_mk_comb(IN_t, [x, P]) val xINP_th = ASSUME xINP_t val xINQ_t = list_mk_comb(IN_t, [x, Q]) val xINQ_th = ASSUME xINQ_t val xINP_eq_xINQ_th = AP_TERM (mk_comb(IN_t, x)) PeqQ_th val (xINP_imp_xINQ, xINQ_imp_xINP) = EQ_IMP_RULE xINP_eq_xINQ_th val feqg_t = mk_forall(x, mk_imp(xINQ_t, mk_eq(mk_comb(f,x), mk_comb(g, x)))) val feqg_th = SPEC x (ASSUME feqg_t) val feqg_th = MP feqg_th xINQ_th val (f_imp_g_th, g_imp_f_th) = EQ_IMP_RULE feqg_th fun mk_res th args = List.foldl (RIGHT_BETA o uncurry (C AP_THM)) th args (* forall thm *) val resfa_t = prim_mk_const {Thy = "bool", Name = "RES_FORALL"} val res_pf_t = list_mk_comb(resfa_t, [P, f]) val res_qg_t = list_mk_comb(resfa_t, [Q, g]) val resfa_pf_eqn = mk_res RES_FORALL_DEF [P, f] val resfa_qg_eqn = mk_res RES_FORALL_DEF [Q, g] val resfa_pf_eq_th = SPEC x (EQ_MP resfa_pf_eqn (ASSUME res_pf_t)) val g_th = MP f_imp_g_th (MP resfa_pf_eq_th xINP_th) val xinq_imp_g_th = GEN x (DISCH xINQ_t (PROVE_HYP (UNDISCH xINQ_imp_xINP) g_th)) val rfa_pf_imp_rfa_qg = DISCH res_pf_t (EQ_MP (SYM resfa_qg_eqn) xinq_imp_g_th) val resfa_qg_eq_th = SPEC x (EQ_MP resfa_qg_eqn (ASSUME res_qg_t)) val f_th = MP g_imp_f_th (MP resfa_qg_eq_th xINQ_th) val xinp_imp_f_th = GEN x (DISCH xINP_t (PROVE_HYP (UNDISCH xINP_imp_xINQ) f_th)) val rfa_qg_imp_rfa_pf = DISCH res_qg_t (EQ_MP (SYM resfa_pf_eqn) xinp_imp_f_th) val fa_eqn = IMP_ANTISYM_RULE rfa_pf_imp_rfa_qg rfa_qg_imp_rfa_pf (* exists thm *) val resex_t = prim_mk_const {Thy = "bool", Name = "RES_EXISTS"} val res_pf_t = list_mk_comb(resex_t, [P, f]) val res_qg_t = list_mk_comb(resex_t, [Q, g]) val resex_pf_eqn = mk_res RES_EXISTS_DEF [P, f] val resex_qg_eqn = mk_res RES_EXISTS_DEF [Q, g] val pf_exbody_th = EQ_MP resex_pf_eqn (ASSUME res_pf_t) val pf_body_th = ASSUME(mk_conj(xINP_t, fx_t)) val (new_xINP_th, fx_th) = CONJ_PAIR pf_body_th val new_xINQ_th = MP xINP_imp_xINQ new_xINP_th val new_gx_th = PROVE_HYP new_xINQ_th (MP f_imp_g_th fx_th) val qg_exists = EXISTS(rhs (concl resex_qg_eqn), x) (CONJ new_xINQ_th new_gx_th) val pf_chosen = CHOOSE(x,EQ_MP resex_pf_eqn (ASSUME res_pf_t)) qg_exists val ex_pf_imp_qg = DISCH res_pf_t (EQ_MP (SYM resex_qg_eqn) pf_chosen) val qg_exbody_th = EQ_MP resex_qg_eqn (ASSUME res_qg_t) val qg_body_th = ASSUME(mk_conj(xINQ_t, gx_t)) val (new_xINQ_th, gx_th) = CONJ_PAIR qg_body_th val new_xINP_th = MP xINQ_imp_xINP new_xINQ_th val new_fx_th = PROVE_HYP new_xINQ_th (MP g_imp_f_th gx_th) val pf_exists = EXISTS (rhs (concl resex_pf_eqn), x) (CONJ new_xINP_th new_fx_th) val qg_chosen = CHOOSE(x, EQ_MP resex_qg_eqn (ASSUME res_qg_t)) pf_exists val ex_qg_imp_pf = DISCH res_qg_t (EQ_MP (SYM resex_pf_eqn) qg_chosen) val ex_eqn = IMP_ANTISYM_RULE ex_pf_imp_qg ex_qg_imp_pf in (thm (#(FILE), #(LINE))("RES_FORALL_CONG", DISCH PeqQ_t (DISCH feqg_t fa_eqn)), thm (#(FILE), #(LINE))("RES_EXISTS_CONG", DISCH PeqQ_t (DISCH feqg_t ex_eqn))) end (* ------------------------------------------------------------------------- *) (* Monotonicity. *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* MONO_AND |- (x ==> y) /\ (z ==> w) ==> (x /\ z ==> y /\ w) *) (* ------------------------------------------------------------------------- *) val MONO_AND = thm (#(FILE), #(LINE))("MONO_AND", let val tm1 = “x ==> y” val tm2 = “z ==> w” val tm3 = “x /\ z” val tm4 = “y /\ w” val th1 = ASSUME tm1 val th2 = ASSUME tm2 val th3 = ASSUME tm3 val th4 = CONJUNCT1 th3 val th5 = CONJUNCT2 th3 val th6 = MP th1 th4 val th7 = MP th2 th5 val th8 = CONJ th6 th7 val th9 = itlist DISCH [tm1,tm2,tm3] th8 val th10 = SPEC “^tm3 ==> ^tm4” (SPEC tm2 (SPEC tm1 AND_IMP_INTRO)) in EQ_MP th10 th9 end); (* ------------------------------------------------------------------------- *) (* MONO_OR |- (x ==> y) /\ (z ==> w) ==> (x \/ z ==> y \/ w) *) (* ------------------------------------------------------------------------- *) val MONO_OR = thm (#(FILE), #(LINE))("MONO_OR", let val tm1 = “x ==> y” val tm2 = “z ==> w” val tm3 = “x \/ z” val tm4 = “y \/ w” val th1 = ASSUME tm1 val th2 = ASSUME tm2 val th3 = ASSUME tm3 val th4 = DISJ1 (MP th1 (ASSUME “x:bool”)) “w:bool” val th5 = DISJ2 “y:bool” (MP th2 (ASSUME “z:bool”)) val th6 = DISJ_CASES th3 th4 th5 val th7 = DISCH tm1 (DISCH tm2 (DISCH tm3 th6)) val th8 = SPEC “^tm3 ==> ^tm4” (SPEC tm2 (SPEC tm1 AND_IMP_INTRO)) in EQ_MP th8 th7 end); (* ------------------------------------------------------------------------- *) (* MONO_IMP |- (y ==> x) /\ (z ==> w) ==> ((x ==> z) ==> (y ==> w)) *) (* ------------------------------------------------------------------------- *) val MONO_IMP = thm (#(FILE), #(LINE))("MONO_IMP", let val tm1 = “y ==> x” val tm2 = “z ==> w” val tm3 = “x ==> z” val tm4 = “y ==> w” val tm5 = “y:bool” val th1 = ASSUME tm1 val th2 = ASSUME tm2 val th3 = ASSUME tm3 val th4 = MP th1 (ASSUME tm5) val th5 = MP th3 th4 val th6 = MP th2 th5 val th7 = DISCH tm1 (DISCH tm2 (DISCH tm3 (DISCH tm5 th6))) val th8 = SPEC “^tm3 ==> ^tm4” (SPEC tm2 (SPEC tm1 AND_IMP_INTRO)) in EQ_MP th8 th7 end); (* ------------------------------------------------------------------------- *) (* MONO_NOT |- (y ==> x) ==> (~x ==> ~y) *) (* ------------------------------------------------------------------------- *) val MONO_NOT = thm (#(FILE), #(LINE))("MONO_NOT", let val tm1 = “y ==> x” val tm2 = “~x” val tm3 = “y:bool” val th1 = ASSUME tm1 val th2 = ASSUME tm2 val th3 = ASSUME tm3 val th4 = MP th1 th3 val th5 = DISCH tm3 (MP th2 th4) val th6 = EQ_MP (SYM (RIGHT_BETA (AP_THM NOT_DEF tm3))) th5 in DISCH tm1 (DISCH tm2 th6) end); (* ------------------------------------------------------------------------- *) (* MONO_NOT_EQ |- (y ==> x) = (~x ==> ~y) *) (* ------------------------------------------------------------------------- *) val MONO_NOT_EQ = thm (#(FILE), #(LINE))("MONO_NOT_EQ", let val tm1 = “x:bool” val tm2 = “y:bool” val th1 = INST [tm1 |-> mk_neg tm2, tm2 |-> mk_neg tm1] MONO_NOT val th2 = SUBST [“x1:bool” |-> SPEC tm1 (CONJUNCT1 NOT_CLAUSES), “x2:bool” |-> SPEC tm2 (CONJUNCT1 NOT_CLAUSES)] “(~x ==> ~y) ==> (x2 ==> x1)” th1 val th3 = IMP_ANTISYM_RULE MONO_NOT th2 in th3 end); (* ------------------------------------------------------------------------- *) (* MONO_ALL |- (!x. P x ==> Q x) ==> (!x. P x) ==> !x. Q x *) (* ------------------------------------------------------------------------- *) val MONO_ALL = thm (#(FILE), #(LINE))("MONO_ALL", let val tm1 = “!x:'a. P x ==> Q x” val tm2 = “!x:'a. P x” val tm3 = “x:'a” val th1 = ASSUME tm1 val th2 = ASSUME tm2 val th3 = SPEC tm3 th1 val th4 = SPEC tm3 th2 val th5 = GEN tm3 (MP th3 th4) in DISCH tm1 (DISCH tm2 th5) end); (* ------------------------------------------------------------------------- *) (* MONO_EXISTS = [] |- (!x. P x ==> Q x) ==> (?x. P x) ==> ?x. Q x *) (* ------------------------------------------------------------------------- *) val MONO_EXISTS = thm (#(FILE), #(LINE))("MONO_EXISTS", let val tm1 = “!x:'a. P x ==> Q x” val tm2 = “?x:'a. P x” val tm3 = “@x:'a. P x” val tm4 = “\x:'a. P x:bool” val th1 = ASSUME tm1 val th2 = ASSUME tm2 val th3 = SPEC tm3 th1 val th4 = RIGHT_BETA(RIGHT_BETA (AP_THM EXISTS_DEF tm4)) val th5 = EQ_MP th4 th2 val th6 = MP th3 th5 in DISCH tm1 (DISCH tm2 (EXISTS (“?x:'a. Q x”, tm3) th6)) end); (* ------------------------------------------------------------------------- *) (* MONO_COND |- (x ==> y) ==> (z ==> w) *) (* ==> (if b then x else z) ==> (if b then y else w) *) (* ------------------------------------------------------------------------- *) val MONO_COND = thm (#(FILE), #(LINE))("MONO_COND", let val tm1 = “x ==> y” val tm2 = “z ==> w” val tm3 = “if b then x else z:bool” val tm4 = “b:bool” val tm5 = “x:bool” val tm6 = “z:bool” val tm7 = “y:bool” val tm8 = “w:bool” val th1 = ASSUME tm1 val th2 = ASSUME tm2 val th3 = ASSUME tm3 val th4 = SPEC tm6 (SPEC tm5 (INST_TYPE [alpha |-> bool] COND_CLAUSES)) val th5 = CONJUNCT1 th4 val th6 = CONJUNCT2 th4 val th7 = SPEC tm4 BOOL_CASES_AX val th8 = ASSUME “b = T” val th9 = ASSUME “b = F” val th10 = SUBST [tm4 |-> th8] (concl th3) th3 val th11 = SUBST [tm4 |-> th9] (concl th3) th3 val th12 = EQ_MP th5 th10 val th13 = EQ_MP th6 th11 val th14 = MP th1 th12 val th15 = MP th2 th13 val th16 = INST [tm5 |-> tm7, tm6 |-> tm8] th4 val th17 = SYM (CONJUNCT1 th16) val th18 = SYM (CONJUNCT2 th16) val th19 = EQ_MP th17 th14 val th20 = EQ_MP th18 th15 val th21 = DISCH tm3 th19 val th22 = DISCH tm3 th20 val th23 = SUBST [tm4 |-> th8] (concl th21) th21 val th24 = SUBST [tm4 |-> th9] (concl th22) th22 val v = “v:bool” val T = mk_const("T",bool) val template = subst [T |-> v] (concl th23) val th25 = SUBST [v |-> SYM th8] template th23 val th26 = SUBST [v |-> SYM th9] template th24 in DISCH tm1 (DISCH tm2 (DISJ_CASES th7 th25 th26)) end); (* ------------------------------------------------------------------------- *) (* EXISTS_REFL |- !a. ?x. x = a *) (* ------------------------------------------------------------------------- *) val EXISTS_REFL = thm (#(FILE), #(LINE))("EXISTS_REFL", let val a = “a:'a” val th1 = REFL a val th2 = EXISTS (“?x:'a. x = a”, a) th1 in GEN a th2 end); (* ------------------------------------------------------------------------- *) (* EXISTS_UNIQUE_REFL |- !a. ?!x. x = a *) (* ------------------------------------------------------------------------- *) val EXISTS_UNIQUE_REFL = thm (#(FILE), #(LINE))("EXISTS_UNIQUE_REFL", let val a = “a:'a” val P = “\x:'a. x = a” val tmx = “^P x” val tmy= “^P y” val ex = “?x. ^P x” val th1 = SPEC a EXISTS_REFL val th2 = ABS “x:'a” (BETA_CONV tmx) val th3 = AP_TERM “$? :('a->bool)->bool” th2 val th4 = EQ_MP (SYM th3) th1 val th5 = ASSUME (mk_conj(tmx,tmy)) val th6 = CONJUNCT1 th5 val th7 = CONJUNCT2 th5 val th8 = EQ_MP (BETA_CONV (concl th6)) th6 val th9 = EQ_MP (BETA_CONV (concl th7)) th7 val th10 = TRANS th8 (SYM th9) val th11 = DISCH (hd(hyp th10)) th10 val th12 = GEN “x:'a” (GEN “y:'a” th11) val th13 = INST [“P:'a->bool” |-> P] EXISTS_UNIQUE_THM val th14 = EQ_MP (SYM th13) (CONJ th4 th12) val th15 = AP_TERM “$?! :('a->bool)->bool” th2 in GEN a (EQ_MP th15 th14) end); (* ---------------------------------------------------------------------- EXISTS_UNIQUE_FALSE |- (?!x. F) <=> F ---------------------------------------------------------------------- *) val EXISTS_UNIQUE_FALSE = thm (#(FILE), #(LINE))("EXISTS_UNIQUE_FALSE", let val BINDER_CONV = RAND_CONV o ABS_CONV val LAND_CONV = RATOR_CONV o RAND_CONV val P = mk_var("P", alpha --> bool) val x = mk_var("x", alpha) val th1 = INST [P |-> mk_abs(x, F)] EXISTS_UNIQUE_THM val th2 = CONV_RULE(RAND_CONV (LAND_CONV (BINDER_CONV BETA_CONV))) th1 val th3 = CONV_RULE(LAND_CONV (BINDER_CONV BETA_CONV)) th2 val uniqueness_t = th3 |> concl |> rhs |> rand val simp1 = AP_THM (AP_TERM conjunction (SPEC F EXISTS_SIMP)) uniqueness_t val th4 = TRANS th3 simp1 val simp2 = AND_CLAUSES |> SPEC uniqueness_t |> CONJUNCTS |> el 3 in TRANS th4 simp2 end); (* ------------------------------------------------------------------------- *) (* Unwinding. *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* UNWIND1_THM |- !P a. (?x. (a = x) /\ P x) = P a *) (* ------------------------------------------------------------------------- *) val UNWIND_THM1 = thm (#(FILE), #(LINE))("UNWIND_THM1", let val P = “P:'a->bool” val a = “a:'a” val Pa = “^P ^a” val v = “v:'a” val tm1 = “?x:'a. (a = x) /\ P x” val th1 = ASSUME tm1 val th2 = ASSUME “(a:'a = v) /\ P v” val th3 = CONJUNCT1 th2 val th4 = CONJUNCT2 th2 val th5 = SUBST [v |-> SYM th3] (concl th4) th4 val th6 = DISCH tm1 (CHOOSE (v,th1) th5) val th7 = ASSUME Pa val th8 = CONJ (REFL a) th7 val th9 = EXISTS (tm1,a) th8 val th10 = DISCH Pa th9 val th11 = SPEC Pa (SPEC tm1 IMP_ANTISYM_AX) in GEN P (GEN a (MP (MP th11 th6) th10)) end); (* ------------------------------------------------------------------------- *) (* UNWIND_THM2 |- !P a. (?x. (x = a) /\ P x) = P a *) (* ------------------------------------------------------------------------- *) val UNWIND_THM2 = thm (#(FILE), #(LINE))("UNWIND_THM2", let val P = “P:'a->bool” val a = “a:'a” val Px = “^P x” val Pa = “^P ^a” val u = “u:'a” val v = “v:'a” val a_eq_x = “a:'a = x” val x_eq_a = “x:'a = a” val th1 = SPEC a (SPEC P UNWIND_THM1) val th2 = REFL Pa val th3 = DISCH a_eq_x (SYM (ASSUME a_eq_x)) val th4 = DISCH x_eq_a (SYM (ASSUME x_eq_a)) val th5 = SPEC a_eq_x (SPEC x_eq_a IMP_ANTISYM_AX) val th6 = MP (MP th5 th4) th3 val th7 = MK_COMB (MK_COMB (REFL “$/\”, th6), REFL Px) val th8 = MK_COMB (REFL“$? :('a->bool)->bool”, ABS “x:'a” th7) val th9 = MK_COMB(MK_COMB (REFL“$= :bool->bool->bool”, th8),th2) val th10 = EQ_MP (SYM th9) th1 in GEN P (GEN a th10) end); (* ------------------------------------------------------------------------- *) (* UNWIND_FORALL_THM1 |- !f v. (!x. (v = x) ==> f x) = f v *) (* ------------------------------------------------------------------------- *) val UNWIND_FORALL_THM1 = thm (#(FILE), #(LINE))("UNWIND_FORALL_THM1", let val f = “f : 'a -> bool” val v = “v:'a” val fv = “^f ^v” val tm1 = “!x:'a. (v = x) ==> f x” val tm2 = “v:'a = x” val th1 = ASSUME tm1 val th2 = ASSUME fv val th3 = DISCH tm1 (MP (SPEC v th1) (REFL v)) val th4 = ASSUME tm2 val th5 = SUBST [v |-> th4] (concl th2) th2 val th6 = DISCH fv (GEN “x:'a” (DISCH tm2 th5)) val th7 = MP (MP (SPEC tm1 (SPEC fv IMP_ANTISYM_AX)) th6) th3 in GEN f (GEN v (SYM th7)) end); (* ------------------------------------------------------------------------- *) (* UNWIND_FORALL_THM2 |- !f v. (!x. (x = v) ==> f x) = f v *) (* ------------------------------------------------------------------------- *) val UNWIND_FORALL_THM2 = thm (#(FILE), #(LINE))("UNWIND_FORALL_THM2", let val f = “f:'a->bool” val v = “v:'a” val fv = “^f ^v” val tm1 = “!x:'a. (x = v) ==> f x” val tm2 = “x:'a = v” val th1 = ASSUME tm1 val th2 = ASSUME fv val th3 = DISCH tm1 (MP (SPEC v th1) (REFL v)) val th4 = ASSUME tm2 val th5 = SUBST [v |-> SYM th4] (concl th2) th2 val th6 = DISCH fv (GEN “x:'a” (DISCH tm2 th5)) val th7 = MP (MP (SPEC tm1 (SPEC fv IMP_ANTISYM_AX)) th6) th3 in GEN f (GEN v (SYM th7)) end); (* ------------------------------------------------------------------------- *) (* Skolemization: |- !P. (!x. ?y. P x y) <=> ?f. !x. P x (f x) *) (* ------------------------------------------------------------------------- *) val SKOLEM_THM = thm (#(FILE), #(LINE))("SKOLEM_THM", let val P = “P:'a -> 'b -> bool” val x = “x:'a” val y = “y:'b” val f = “f:'a->'b” val tm1 = “!x. ?y. ^P x y” val tm2 = “?f. !x. ^P x (f x)” val tm4 = “\x. @y. ^P x y” val tm5 = “(\x. @y. ^P x y) x” val th1 = ASSUME tm1 val th2 = ASSUME tm2 val th3 = SPEC x th1 val th4 = INST_TYPE [alpha |-> beta] SELECT_AX val th5 = SPEC y (SPEC “\y. ^P x y” th4) val th6 = BETA_CONV (fst(dest_imp(concl th5))) val th7 = BETA_CONV (snd(dest_imp(concl th5))) val th8 = MK_COMB (MK_COMB (REFL “$==>”,th6),th7) val th9 = EQ_MP th8 th5 val th10 = MP th9 (ASSUME(fst(dest_imp(concl th9)))) val th11 = CHOOSE (y,th3) th10 val th12 = SYM (BETA_CONV tm5) val th13 = SUBST [“v:'b” |-> th12] “^P x v” th11 val th14 = DISCH tm1 (EXISTS (tm2,tm4) (GEN x th13)) val th15 = ASSUME “!x. ^P x (f x)” val th16 = SPEC x th15 val th17 = GEN x (EXISTS(“?y. ^P x y”,“f (x:'a):'b”) th16) val th18 = DISCH tm2 (CHOOSE (f,th2) th17) val th19 = MP (MP (SPEC tm1 (SPEC tm2 IMP_ANTISYM_AX)) th18) th14 in GEN P (SYM th19) end); (*--------------------------------------------------------------------------- Support for pattern matching on booleans. bool_case_thm = |- (!e0 e1. bool_case e0 e1 T = e0) /\ !e0 e1. bool_case e0 e1 F = e1 ---------------------------------------------------------------------------*) val bool_case_thm = let val (vs,_) = strip_forall (concl COND_CLAUSES) in thm (#(FILE), #(LINE))("bool_case_thm", COND_CLAUSES |> SPECL vs |> CONJUNCTS |> map (GENL vs) |> LIST_CONJ) end (*--------------------------------------------------------------------------- bool_case_eq = |- (bool_case t1 t2 x = v) <=> (x <=> T) /\ t1 = v \/ (x <=> F) /\ t2 = v ---------------------------------------------------------------------------*) val bool_case_eq = thm (#(FILE), #(LINE))("bool_case_eq", let val x = “x:bool” val t1 = “t1:'a” val t2 = “t2:'a” val v = “v:'a” val eq = “$=” val conj = “$/\” val disj = “$\/” val tm1 = “t1 = v” val tm2 = “t2 = v” val [COND1, COND2] = (CONJUNCTS (SPEC t2 (SPEC t1 COND_CLAUSES))) and [OR1,OR2,OR3,OR4,_] = map GEN_ALL (CONJUNCTS (SPEC_ALL OR_CLAUSES)) and [AND1,AND2,AND3,AND4,_] = map GEN_ALL (CONJUNCTS(SPEC_ALL AND_CLAUSES)) val thmT1 = AP_THM (AP_TERM eq COND1) v val thmF1 = AP_THM (AP_TERM eq COND2) v val [TF,FT] = map EQF_INTRO (CONJUNCTS BOOL_EQ_DISTINCT) val [TT,FF] = map (EQT_INTRO o REFL) [“T”,“F”] val thmT2 = let val thml1 = AP_THM (AP_TERM conj TT) tm1 val thml2 = SPEC tm1 AND1 val thml = TRANS thml1 thml2 val thmr1 = AP_THM (AP_TERM conj TF) tm2 val thmr2 = SPEC tm2 AND3 val thmr = TRANS thmr1 thmr2 val thm1 = MK_COMB (AP_TERM disj thml, thmr) in TRANS thm1 (SPEC tm1 OR4) end val thmF2 = let val thmr1 = AP_THM (AP_TERM conj FF) tm2 val thmr2 = SPEC tm2 AND1 val thmr = TRANS thmr1 thmr2 val thml1 = AP_THM (AP_TERM conj FT) tm1 val thml2 = SPEC tm1 AND3 val thml = TRANS thml1 thml2 val thm1 = MK_COMB (AP_TERM disj thml, thmr) in TRANS thm1 (SPEC tm2 OR3) end val thmT3 = TRANS thmT1 (SYM thmT2) val thmF3 = TRANS thmF1 (SYM thmF2) val tm = “(if x then t1 else t2) = v <=> (((x <=> T) /\ t1 = v) \/ ((x <=> F) /\ t2 = v))” val thT4 = SUBST_CONV [x |-> ASSUME “x = T”] tm tm and thF4 = SUBST_CONV [x |-> ASSUME “x = F”] tm tm val thmT = EQ_MP (SYM thT4) thmT3 val thmF = EQ_MP (SYM thF4) thmF3 in DISJ_CASES (SPEC x BOOL_CASES_AX) thmT thmF end); (* ------------------------------------------------------------------------- *) (* bool_case_ID = |- !x. (x => T | F) = x *) (* ------------------------------------------------------------------------- *) val bool_case_ID = thm (#(FILE), #(LINE))("bool_case_ID", let val x = “x:bool” val (CONDT,CONDF) = INST_TYPE [alpha |-> bool] COND_CLAUSES |> SPECL [T,F] |> CONJ_PAIR val tm = “(if x then T else F) = x” val thT1 = SUBST_CONV [x |-> ASSUME “x = T”] tm tm val thF1 = SUBST_CONV [x |-> ASSUME “x = F”] tm tm val thmT = EQ_MP (SYM thT1) CONDT val thmF = EQ_MP (SYM thF1) CONDF in GEN x (DISJ_CASES (SPEC x BOOL_CASES_AX) thmT thmF) end); (* ------------------------------------------------------------------------- *) (* bool_case_CONST = |- !x b. bool_case x x b = x *) (* ------------------------------------------------------------------------- *) val bool_case_CONST = thm (#(FILE), #(LINE))("bool_case_CONST", COND_ID) (* ------------------------------------------------------------------------- *) (* boolAxiom |- !e0 e1. ?fn. (fn T = e0) /\ (fn F = e1) *) (* ------------------------------------------------------------------------- *) val boolAxiom = thm (#(FILE), #(LINE))("boolAxiom", let val ([e0,e1], _) = strip_forall (concl COND_CLAUSES) val (th2, th3) = CONJ_PAIR (SPECL [e0, e1] COND_CLAUSES) val f_t = “\b. if b then ^e0 else ^e1” val f_T = TRANS (BETA_CONV (mk_comb(f_t, T))) th2 val f_F = TRANS (BETA_CONV (mk_comb(f_t, F))) th3 val th4 = CONJ f_T f_F val th5 = EXISTS (“?fn. (fn T = ^e0) /\ (fn F = ^e1)”, f_t) th4 in GEN e0 (GEN e1 th5) end); (* ------------------------------------------------------------------------- *) (* bool_INDUCT |- !P. P T /\ P F ==> !b. P b *) (* ------------------------------------------------------------------------- *) val bool_INDUCT = thm (#(FILE), #(LINE))("bool_INDUCT", let val P = “P:bool -> bool” val b = “b:bool” val v = “v:bool” val tm1 = “^P T /\ ^P F” val th1 = SPEC b BOOL_CASES_AX val th2 = ASSUME tm1 val th3 = CONJUNCT1 th2 val th4 = CONJUNCT2 th2 val th5 = ASSUME “b = T” val th6 = ASSUME “b = F” val th7 = SUBST [v |-> SYM th5] “^P ^v” th3 val th8 = SUBST [v |-> SYM th6] “^P ^v” th4 val th9 = GEN b (DISJ_CASES th1 th7 th8) in GEN P (DISCH tm1 th9) end); (* --------------------------------------------------------------------------- |- !P Q x x' y y'. (P = Q) /\ (Q ==> (x = x')) /\ (~Q ==> (y = y')) ==> ((case P of T -> x || F -> y) = (case Q of T -> x' || F -> y')) --------------------------------------------------------------------------- *) val bool_case_CONG = thm (#(FILE), #(LINE))("bool_case_CONG", COND_CONG) val FORALL_BOOL = thm (#(FILE), #(LINE)) ("FORALL_BOOL", let val tm1 = “!b:bool. P b” val tm2 = “P T /\ P F” val th1 = ASSUME tm1 val th2 = CONJ (SPEC T th1) (SPEC F th1) val th3 = DISCH tm1 th2 val th4 = ASSUME tm2 val th5 = MP (SPEC “P:bool->bool” bool_INDUCT) th4 val th6 = DISCH tm2 th5 in IMP_ANTISYM_RULE th3 th6 end); (*--------------------------------------------------------------------------- Results about Unique existence. ---------------------------------------------------------------------------*) local val LAND_CONV = RATOR_CONV o RAND_CONV val P = mk_var("P", Type.alpha --> Type.bool) val p = mk_var("p", Type.bool) val q = mk_var("q", Type.bool) val Q = mk_var("Q", Type.alpha --> Type.bool) val x = mk_var("x", Type.alpha) val y = mk_var("y", Type.alpha) val Px = mk_comb(P, x) val Py = mk_comb(P, y) val Qx = mk_comb(Q, x) val Qy = mk_comb(Q, y) val uex_t = mk_const("?!", (alpha --> bool) --> bool) val exP = mk_exists(x, Px) val exQ = mk_exists(x, Qx) val uexP = mk_exists1(x, Px) val uexQ = mk_exists1(x, Qx) val pseudo_mp = let val lhs_t = mk_conj(p, mk_imp(p, q)) val rhs_t = mk_conj(p, q) val lhs_thm = ASSUME lhs_t val (p_thm, pimpq) = CONJ_PAIR lhs_thm val dir1 = DISCH_ALL (CONJ p_thm (MP pimpq p_thm)) val rhs_thm = ASSUME rhs_t val (p_thm, q_thm) = CONJ_PAIR rhs_thm val dir2 = DISCH_ALL (CONJ p_thm (DISCH p q_thm)) in IMP_ANTISYM_RULE dir1 dir2 end in val UEXISTS_OR_THM = let val subdisj_t = mk_abs(x, mk_disj(Px, Qx)) val lhs_t = mk_comb(uex_t, subdisj_t) val lhs_thm = ASSUME lhs_t val lhs_eq = AP_THM EXISTS_UNIQUE_DEF subdisj_t val lhs_expanded = CONV_RULE BETA_CONV (EQ_MP lhs_eq lhs_thm) val (expq0, univ) = CONJ_PAIR lhs_expanded val expq = EQ_MP (SPEC_ALL EXISTS_OR_THM) expq0 val univ1 = SPEC_ALL univ val univ2 = CONV_RULE (LAND_CONV (LAND_CONV BETA_CONV)) univ1 val univ3 = CONV_RULE (LAND_CONV (RAND_CONV BETA_CONV)) univ2 val P_half = let val asm = ASSUME (mk_conj(Px,Py)) val (Px_thm, Py_thm) = CONJ_PAIR asm val PxQx_thm = DISJ1 Px_thm Qx val PyQy_thm = DISJ1 Py_thm Qy val resolvent = CONJ PxQx_thm PyQy_thm val rhs = GENL [x,y] (DISCH (mk_conj(Px,Py)) (PROVE_HYP resolvent (UNDISCH univ3))) in DISJ1 (EQ_MP (SYM EXISTS_UNIQUE_THM) (CONJ (ASSUME exP) rhs)) uexQ end val Q_half = let val asm = ASSUME (mk_conj(Qx,Qy)) val (Qx_thm, Qy_thm) = CONJ_PAIR asm val PxQx_thm = DISJ2 Px Qx_thm val PyQy_thm = DISJ2 Py Qy_thm val resolvent = CONJ PxQx_thm PyQy_thm val rhs = GENL [x,y] (DISCH (mk_conj(Qx,Qy)) (PROVE_HYP resolvent (UNDISCH univ3))) val uex_expanded = SYM (INST [P |-> Q] EXISTS_UNIQUE_THM) in DISJ2 uexP (EQ_MP uex_expanded (CONJ (ASSUME exQ) rhs)) end in thm (#(FILE), #(LINE))( "UEXISTS_OR_THM", GENL [P, Q] (DISCH_ALL (DISJ_CASES expq P_half Q_half)) ) end; val UEXISTS_SIMP = let fun mCONV_RULE c thm = TRANS thm (c (rhs (concl thm))) val xeqy = mk_eq(x,y) val t = mk_var("t", bool) val abst = mk_abs(x, t) val uext_t = mk_exists1(x,t) val exp0 = AP_THM EXISTS_UNIQUE_DEF abst val exp1 = mCONV_RULE BETA_CONV exp0 val exp2 = mCONV_RULE (LAND_CONV (K (SPEC t EXISTS_SIMP))) exp1 val exp3 = mCONV_RULE (RAND_CONV (QUANT_CONV (QUANT_CONV (LAND_CONV (LAND_CONV BETA_CONV))))) exp2 val exp4 = mCONV_RULE (RAND_CONV (QUANT_CONV (QUANT_CONV (LAND_CONV (RAND_CONV BETA_CONV))))) exp3 val exp5 = mCONV_RULE (RAND_CONV (QUANT_CONV (QUANT_CONV (LAND_CONV (K (SPEC t AND_CLAUSE5)))))) exp4 val pushy0 = SPECL [t, mk_abs(y,xeqy)] RIGHT_FORALL_IMP_THM val pushy1 = CONV_RULE (LAND_CONV (QUANT_CONV (RAND_CONV BETA_CONV))) pushy0 val pushy2 = CONV_RULE (RAND_CONV (RAND_CONV (QUANT_CONV BETA_CONV))) pushy1 val exp6 = mCONV_RULE (RAND_CONV (QUANT_CONV (K pushy2))) exp5 val pushx0 = SPECL [t, mk_abs(x, mk_forall(y,xeqy))] RIGHT_FORALL_IMP_THM val pushx1 = CONV_RULE (LAND_CONV (QUANT_CONV (RAND_CONV BETA_CONV))) pushx0 val pushx2 = CONV_RULE (RAND_CONV (RAND_CONV (QUANT_CONV BETA_CONV))) pushx1 val exp7 = mCONV_RULE (RAND_CONV (K pushx2)) exp6 val mp' = Thm.INST [p |-> t, q |-> list_mk_forall [x,y] xeqy] pseudo_mp in thm (#(FILE), #(LINE))("UEXISTS_SIMP", mCONV_RULE (K mp') exp7) end end (*--------------------------------------------------------------------------- The definition of restricted abstraction. ---------------------------------------------------------------------------*) val RES_ABSTRACT_EXISTS = let fun B_CONV n = funpow n RATOR_CONV BETA_CONV fun RHS th = rhs (concl th) val p = “p : 'a -> bool” val m = “m : 'a -> 'b” val m1 = “m1 : 'a -> 'b” val m2 = “m2 : 'a -> 'b” val x = “x : 'a” val witness = “\p m x. if x IN p then ^m x else ARB x” val A1 = B_CONV 2 “^witness ^p ^m ^x” val A2 = TRANS A1 (B_CONV 1 (RHS A1)) val A3 = TRANS A2 (BETA_CONV (RHS A2)) val A4 = EQT_INTRO (ASSUME “^x IN ^p”) val A5 = RATOR_CONV (RATOR_CONV (RAND_CONV (K A4))) (RHS A3) val A6 = INST_TYPE [alpha |-> beta] COND_CLAUSE1 val A7 = SPECL [“^m ^x”, “ARB ^x : 'b”] A6 val A8 = DISCH “^x IN ^p” (TRANS (TRANS A3 A5) A7) val A9 = GENL [“^p”, “^m”, “^x”] A8 (* Completed the first clause of the definition *) val B1 = SPEC “^x IN ^p” EXCLUDED_MIDDLE val B2 = UNDISCH A8 val B3 = INST [m |-> m1] B2 val B4 = INST [m |-> m2] B2 val B5 = SPEC_ALL (ASSUME “!x. x IN ^p ==> (^m1 x = ^m2 x)”) val B6 = TRANS B3 (TRANS (UNDISCH B5) (SYM B4)) val B7 = INST [m |-> m1] A3 val B8 = INST [m |-> m2] A3 val B9 = SYM (SPEC “^x IN ^p” EQ_CLAUSE4) val B10 = EQ_MP B9 (ASSUME “~(^x IN ^p)”) val B11 = INST_TYPE [alpha |-> beta] COND_CLAUSE2 val B12 = RATOR_CONV (RATOR_CONV (RAND_CONV (K B10))) (RHS B7) val B13 = TRANS B12 (SPECL [“^m1 ^x”, “ARB ^x : 'b”] B11) val B14 = RATOR_CONV (RATOR_CONV (RAND_CONV (K B10))) (RHS B8) val B15 = TRANS B14 (SPECL [“^m2 ^x”, “ARB ^x : 'b”] B11) val B16 = TRANS (TRANS B7 B13) (SYM (TRANS B8 B15)) val B17 = DISJ_CASES B1 B6 B16 val B18 = ABS x B17 val B19 = CONV_RULE (RATOR_CONV (RAND_CONV ETA_CONV)) B18 val B20 = CONV_RULE (RAND_CONV ETA_CONV) B19 val B21 = DISCH “!x. x IN ^p ==> (^m1 x = ^m2 x)” B20 val B22 = GENL [p, m1, m2] B21 (* Cleaning up *) val C1 = CONJ A9 B22 val C2 = EXISTS (“?f. (!p (m : 'a -> 'b) x. x IN p ==> (f p m x = m x)) /\ (!p m1 m2. (!x. x IN p ==> (m1 x = m2 x)) ==> (f p m1 = f p m2))”, “\p (m : 'a -> 'b) x. (if x IN p then m x else ARB x)”) C1 in C2 end; val RES_ABSTRACT_DEF = Definition.new_specification ("RES_ABSTRACT_DEF", ["RES_ABSTRACT"], RES_ABSTRACT_EXISTS); val _ = associate_restriction ("\\", "RES_ABSTRACT"); val (RES_FORALL_THM, RES_EXISTS_THM, RES_EXISTS_UNIQUE_THM, RES_SELECT_THM) = let val Pf = map (fn s => mk_var(s, alpha --> bool)) ["P", "f"] fun mk_eq th = GENL Pf (List.foldl (RIGHT_BETA o uncurry (C AP_THM)) th Pf) in (thm (#(FILE), #(LINE))("RES_FORALL_THM", mk_eq RES_FORALL_DEF), thm (#(FILE), #(LINE))("RES_EXISTS_THM", mk_eq RES_EXISTS_DEF), thm (#(FILE), #(LINE))("RES_EXISTS_UNIQUE_THM", mk_eq RES_EXISTS_UNIQUE_DEF), thm (#(FILE), #(LINE))("RES_SELECT_THM", mk_eq RES_SELECT_DEF)) end (* (!x::P. T) = T *) val RES_FORALL_TRUE = let val x = mk_var("x", alpha) val T = concl TRUTH val KT = mk_abs(x, T) val P = mk_var("P", alpha --> bool) val th0 = SPECL[P,KT] RES_FORALL_THM val th1 = CONV_RULE (RAND_CONV (QUANT_CONV (RAND_CONV BETA_CONV))) th0 val xINP_t = (rand o rator o #2 o dest_forall o rhs o concl) th1 val timpT_th = List.nth(CONJUNCTS (SPEC xINP_t IMP_CLAUSES), 1) val th2 = CONV_RULE (RAND_CONV (QUANT_CONV (K timpT_th))) th1 in thm (#(FILE), #(LINE))("RES_FORALL_TRUE", TRANS th2 (SPEC T FORALL_SIMP)) end (* (?x::P. F) = F *) val RES_EXISTS_FALSE = let val x = mk_var("x", alpha) val F = prim_mk_const{Thy = "bool", Name = "F"} val KF = mk_abs(x, F) val P = mk_var("P", alpha --> bool) val th0 = SPECL [P, KF] RES_EXISTS_THM val th1 = CONV_RULE (RAND_CONV (QUANT_CONV (RAND_CONV BETA_CONV))) th0 val xINP_t = (rand o rator o #2 o dest_exists o rhs o concl) th1 val tandF_th = List.nth(CONJUNCTS (SPEC xINP_t AND_CLAUSES), 3) val th2 = CONV_RULE (RAND_CONV (QUANT_CONV (K tandF_th))) th1 in thm (#(FILE), #(LINE))("RES_EXISTS_FALSE", TRANS th2 (SPEC F EXISTS_SIMP)) end (*--------------------------------------------------------------------------- From Joe Hurd : case analysis on the (4) functions in the type :bool -> bool. val BOOL_FUN_CASES_THM = |- !f. (f = \b. T) \/ (f = \b. F) \/ (f = \b. b) \/ (f = \b. ~b) ---------------------------------------------------------------------------*) val BOOL_FUN_CASES_THM = let val x = mk_var("x",bool) val f = mk_var("f",bool-->bool) val KF = “\b:bool.F” val KT = “\b:bool.T” val Ibool = “\b:bool.b” val dual = “\b. ~b” val fT = mk_comb(f,T) val fF = mk_comb(f,F) val fT_eq_T = mk_eq(fT,T) val fF_eq_T = mk_eq(fF,T) val fT_eq_F = mk_eq(fT,F) val fF_eq_F = mk_eq(fF,F) val final = “(f = ^KT) \/ (f = ^KF) \/ (f = ^Ibool) \/ (f = ^dual)” val a0 = TRANS (ASSUME fT_eq_T) (SYM (BETA_CONV (mk_comb(KT,T)))) val a1 = TRANS (ASSUME fF_eq_T) (SYM (BETA_CONV (mk_comb(KT,F)))) val a2 = BOOL_CASE “f x = ^KT x” x x a0 a1 val a3 = EXT (GEN x a2) val a = DISJ1 a3 “(f = \b. F) \/ (f = \b. b) \/ (f = \b. ~b)” val b0 = TRANS (ASSUME fT_eq_F) (SYM (BETA_CONV (mk_comb(KF,T)))) val b1 = TRANS (ASSUME fF_eq_F) (SYM (BETA_CONV (mk_comb(KF,F)))) val b2 = BOOL_CASE “f x = ^KF x” x x b0 b1 val b3 = EXT (GEN x b2) val b4 = DISJ1 b3 “(f = ^Ibool) \/ (f = \b. ~b)” val b = DISJ2 “f = ^KT” b4 val c0 = TRANS (ASSUME fT_eq_T) (SYM (BETA_CONV (mk_comb(Ibool,T)))) val c1 = TRANS (ASSUME fF_eq_F) (SYM (BETA_CONV (mk_comb(Ibool,F)))) val c2 = BOOL_CASE “f x = ^Ibool x” x x c0 c1 val c3 = EXT (GEN x c2) val c4 = DISJ1 c3 “f = ^dual” val c5 = DISJ2 “f = ^KF” c4 val c = DISJ2 “f = ^KT” c5 val d0 = TRANS (ASSUME fT_eq_F) (TRANS (SYM (CONJUNCT1 (CONJUNCT2 NOT_CLAUSES))) (SYM (BETA_CONV (mk_comb(dual,T))))) val d1 = TRANS (ASSUME fF_eq_T) (TRANS (SYM (CONJUNCT2 (CONJUNCT2 NOT_CLAUSES))) (SYM (BETA_CONV (mk_comb(dual,F))))) val d2 = BOOL_CASE “f x = ^dual x” x x d0 d1 val d3 = EXT (GEN x d2) val d4 = DISJ2 “f = ^Ibool” d3 val d5 = DISJ2 “f = ^KF” d4 val d = DISJ2 “f = ^KT” d5 val ad0 = DISCH fT_eq_T a val ad1 = DISCH fT_eq_F d val ad2 = BOOL_CASE “(f T = x) ==> ^final” x x ad0 ad1 val ad3 = SPEC fT (GEN x ad2) val ad = MP ad3 (REFL fT) val bc0 = DISCH fT_eq_T c val bc1 = DISCH fT_eq_F b val bc2 = BOOL_CASE “(f T = x) ==> ^final” x x bc0 bc1 val bc3 = SPEC fT (GEN x bc2) val bc = MP bc3 (REFL fT) val abcd0 = DISCH fF_eq_T ad val abcd1 = DISCH fF_eq_F bc val abcd2 = BOOL_CASE “(f F = x) ==> ^final” x x abcd0 abcd1 val abcd3 = SPEC fF (GEN x abcd2) val abcd = MP abcd3 (REFL fF) in thm (#(FILE), #(LINE))("BOOL_FUN_CASES_THM", GEN f abcd) end; (*--------------------------------------------------------------------------- Another from Joe Hurd : consequence of BOOL_FUN_CASES_THM BOOL_FUN_INDUCT = |- !P. P (\b. T) /\ P (\b. F) /\ P (\b. b) /\ P (\b. ~b) ==> !f. P f ---------------------------------------------------------------------------*) fun or_imp th0 = let val (disj1, disj2) = dest_disj (concl th0) val th1 = SYM (SPEC disj1 (CONJUNCT1 NOT_CLAUSES)) val th2 = MK_COMB (REFL disjunction, th1) val th3 = MK_COMB (th2, REFL disj2) val th4 = EQ_MP th3 th0 val th5 = SYM (SPECL [mk_neg disj1, disj2] IMP_DISJ_THM) in EQ_MP th5 th4 end fun imp_and th0 = let val (ant, conseq) = dest_imp (concl th0) val (ant', conseq') = dest_imp conseq val th1 = SPECL [ant, ant', conseq'] AND_IMP_INTRO in EQ_MP th1 th0 end val BOOL_FUN_INDUCT = let val f = mk_var("f",bool-->bool) val g = mk_var("g",bool-->bool) val f_eq_g = mk_eq(f,g) val P = mk_var("P",(bool-->bool) --> bool) val KF = “\b:bool.F” val KT = “\b:bool.T” val Ibool = “\b:bool.b” val dual = “\b. ~b” val f0 = ASSUME (mk_neg(mk_comb(P,f))) val f1 = ASSUME (mk_neg(mk_neg(f_eq_g))) val f2 = EQ_MP (SPEC f_eq_g (CONJUNCT1 NOT_CLAUSES)) f1 val f3 = MK_COMB (REFL P, f2) val f4 = MK_COMB (REFL negation, f3) val f5 = UNDISCH (NOT_ELIM (EQ_MP f4 f0)) val f6 = CCONTR (mk_neg(f_eq_g)) f5 val f7 = GEN g (DISCH (mk_comb(P,g)) f6) val a0 = SPEC f BOOL_FUN_CASES_THM val a1 = MP (or_imp a0) (UNDISCH (SPEC KT f7)) val a2 = MP (or_imp a1) (UNDISCH (SPEC KF f7)) val a3 = MP (or_imp a2) (UNDISCH (SPEC Ibool f7)) val a = MP (NOT_ELIM (UNDISCH (SPEC dual f7))) a3 val b0 = CCONTR (mk_comb(P,f)) a val b1 = GEN f b0 val b2 = DISCH (mk_comb(P,dual)) b1 val b3 = imp_and (DISCH (mk_comb(P,Ibool)) b2) val b4 = imp_and (DISCH (mk_comb(P,KF)) b3) val b = imp_and (DISCH (mk_comb(P,KT)) b4) in thm (#(FILE), #(LINE))("BOOL_FUN_INDUCT", GEN P b) end; (*--------------------------------------------------------------------------- literal_case_THM = |- !f x. literal_case f x = f x ---------------------------------------------------------------------------*) val literal_case_THM = thm (#(FILE), #(LINE))("literal_case_THM", let val f = “f:'a->'b” val x = “x:'a” in GEN f (GEN x (RIGHT_BETA(AP_THM (RIGHT_BETA(AP_THM literal_case_DEF f)) x))) end); (*---------------------------------------------------------------------------*) (* literal_case_RAND = *) (* |- P (literal_case (\x. N x) M) = (literal_case (\x. P (N x)) M) *) (*---------------------------------------------------------------------------*) val literal_case_RAND = thm (#(FILE), #(LINE))("literal_case_RAND", let val tm1 = “\x:'a. P (N x:'b):'c” val tm2 = “M:'a” val tm3 = “\x:'a. N x:'b” val P = “P:'b ->'c” val literal_case_THM1 = RIGHT_BETA (SPEC tm2 (SPEC tm1 (Thm.INST_TYPE [beta |-> gamma] literal_case_THM))) val literal_case_THM2 = AP_TERM P (RIGHT_BETA (SPEC tm2 (SPEC tm3 literal_case_THM))) in TRANS literal_case_THM2 (SYM literal_case_THM1) end); (*---------------------------------------------------------------------------*) (* literal_case_RATOR = *) (* |- (literal_case (\x. N x) M) b = (literal_case (\x. N x b) M) *) (*---------------------------------------------------------------------------*) val literal_case_RATOR = thm (#(FILE), #(LINE))("literal_case_RATOR", let val M = “M:'a” val b = “b:'b” val tm1 = “\x:'a. N x:'b->'c” val tm2 = “\x:'a. N x ^b:'c” val literal_case_THM1 = AP_THM (RIGHT_BETA (SPEC M (SPEC tm1 (Thm.INST_TYPE [beta |-> (beta --> gamma)] literal_case_THM)))) b val literal_case_THM2 = RIGHT_BETA (SPEC M (SPEC tm2 (Thm.INST_TYPE [beta |-> gamma] literal_case_THM))) in TRANS literal_case_THM1 (SYM literal_case_THM2) end); (*--------------------------------------------------------------------------- literal_case_CONG = |- !f g M N. (M = N) /\ (!x. (x = N) ==> (f x = g x)) ==> (literal_case f M = literal_case g N) ---------------------------------------------------------------------------*) val literal_case_CONG = thm (#(FILE), #(LINE))("literal_case_CONG", let val f = mk_var("f",alpha-->beta) val g = mk_var("g",alpha-->beta) val M = mk_var("M",alpha) val N = mk_var("N",alpha) val x = mk_var ("x",alpha) val MeqN = mk_eq(M,N) val x_eq_N = mk_eq(x,N) val fx_eq_gx = mk_eq(mk_comb(f,x),mk_comb(g,x)) val ctm = mk_forall(x, mk_imp(x_eq_N,fx_eq_gx)) val th = RIGHT_BETA(AP_THM(RIGHT_BETA(AP_THM literal_case_DEF f)) M) val th1 = ASSUME MeqN val th2 = MP (SPEC N (ASSUME ctm)) (REFL N) val th3 = SUBS [SYM th1] th2 val th4 = TRANS (TRANS th th3) (MK_COMB (REFL g,th1)) val th5 = RIGHT_BETA(AP_THM(RIGHT_BETA(AP_THM literal_case_DEF g)) N) val th6 = TRANS th4 (SYM th5) val th7 = SUBS [SPECL [MeqN, ctm, concl th6] AND_IMP_INTRO] (DISCH MeqN (DISCH ctm th6)) in GENL [f,g,M,N] th7 end); (*---------------------------------------------------------------------------*) (* Sometime useful rewrite, but you will want a higher-order version. *) (* |- literal_case (\x. bool_case t u (x=a)) a = t *) (*---------------------------------------------------------------------------*) val literal_case_id = thm (#(FILE), #(LINE)) ("literal_case_id", let val a = mk_var("a", alpha) val x = mk_var("x", alpha) val t = mk_var("t",beta) val u = mk_var("u",beta) val eq = mk_eq(x,a) val bcase = inst [alpha |-> beta] (prim_mk_const{Name = "COND",Thy="bool"}) val g = mk_abs(x,list_mk_comb(bcase,[eq, t, u])) val lit_thm = RIGHT_BETA(SPEC a (SPEC g literal_case_THM)) val Teq = SYM (EQT_INTRO(REFL a)) val ifT = CONJUNCT1(SPECL[t,u] (INST_TYPE[alpha |-> beta] COND_CLAUSES)) val ifeq = SUBS [Teq] ifT in TRANS lit_thm ifeq end); (*--------------------------------------------------------------------------- Support for parsing "case" expressions ---------------------------------------------------------------------------*) val _ = new_constant(GrammarSpecials.core_case_special, “:'a -> ('a -> 'b) -> 'b”); val _ = new_constant(GrammarSpecials.case_split_special, “:('a -> 'b) -> ('a -> 'b) -> 'a -> 'b”); val _ = new_constant(GrammarSpecials.case_arrow_special, “:'a -> 'b -> 'a -> 'b”); val _ = let open GrammarSpecials in app (fn s => remove_ovl_mapping s {Name=s,Thy="bool"}) [case_split_special, case_arrow_special] end val _ = add_rule{pp_elements = [HardSpace 1, TOK "=>", BreakSpace(1,2)], fixity = Infix(NONASSOC, 12), (* allowing for insertion of .| infix at looser precedence level *) block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), paren_style = OnlyIfNecessary, term_name = GrammarSpecials.case_arrow_special} val _ = add_rule{pp_elements = [PPBlock([TOK "case", BreakSpace(1,2), TM, BreakSpace(1,2), TOK "of"], (PP.CONSISTENT, 0)), BreakSpace(1,2)], fixity = Prefix 1, block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), paren_style = Always, term_name = GrammarSpecials.core_case_special}; val _ = add_rule{pp_elements = [PPBlock([TOK "case", BreakSpace(1,2), TM, BreakSpace(1,2), TOK "of"], (PP.CONSISTENT, 0)), BreakSpace(1,2), TM, BreakSpace(1,0), TOK "|", HardSpace 1], fixity = Prefix 1, block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), paren_style = Always, term_name = GrammarSpecials.core_case_special}; val _ = add_rule{pp_elements = [PPBlock([TOK "case", BreakSpace(1,2), TM, BreakSpace(1,2), TOK "of"], (PP.CONSISTENT, 0)), TOK "|", HardSpace 1], fixity = Prefix 1, block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), paren_style = Always, term_name = GrammarSpecials.core_case_special}; val _ = add_rule{pp_elements = [PPBlock([TOK "case", BreakSpace(1,2), TM, BreakSpace(1,2), TOK "of"], (PP.CONSISTENT, 0)), BreakSpace(1,2), TM, BreakSpace(1,0), TOK "|", HardSpace 1, TM, BreakSpace(1,0), TOK "|", HardSpace 1], fixity = Prefix 1, block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), paren_style = Always, term_name = GrammarSpecials.core_case_special}; val BOUNDED_THM = thm (#(FILE), #(LINE))("BOUNDED_THM", let val v = “v:bool” in GEN v (RIGHT_BETA(AP_THM BOUNDED_DEF v)) end); (*---------------------------------------------------------------------------*) (* LCOMM_THM : derive "left-commutativity" from associativity and *) (* commutativity. Used in permutative rewriting, e.g., simpLib entrypoints *) (* *) (* LCOMM_THM |- !f. (!x y. f x y = f y x) ==> *) (* (!x y z. f x (f y z) = f (f x y) z) ==> *) (* (!x y z. f x (f y z) = f y (f x z)) *) (*---------------------------------------------------------------------------*) val LCOMM_THM = thm (#(FILE), #(LINE))("LCOMM_THM", let val x = mk_var("x",alpha) val y = mk_var("y",alpha) val z = mk_var("z",alpha) val f = mk_var("f",alpha --> alpha --> alpha) val comm = “!x y. ^f x y = f y x” val assoc = “!x y z. ^f x (f y z) = f (f x y) z” val comm_thm = ASSUME comm val assoc_thm = ASSUME assoc val th0 = SPEC (list_mk_comb(f,[y,z])) (SPEC x comm_thm) val th1 = SYM (SPECL [y,z,x] assoc_thm) val th2 = TRANS th0 th1 val th3 = AP_TERM (mk_comb(f,y)) (SPECL[z,x] comm_thm) in GEN f (DISCH assoc (DISCH comm (GENL [x,y,z] (TRANS th2 th3)))) end); val DATATYPE_TAG_THM = thm (#(FILE), #(LINE))("DATATYPE_TAG_THM", let val x = mk_var("x",alpha) in GEN x (RIGHT_BETA (AP_THM DATATYPE_TAG_DEF x)) end); val DATATYPE_BOOL = thm (#(FILE), #(LINE))("DATATYPE_BOOL", let val thm1 = INST_TYPE [alpha |-> bool] DATATYPE_TAG_THM val bvar = mk_var("bool",bool--> bool-->bool) in SPEC (list_mk_comb(bvar,[T,F])) thm1 end); (* ---------------------------------------------------------------------- Set up the "itself" type constructor and its one value ---------------------------------------------------------------------- *) val ITSELF_TYPE_DEF = let val itself_exists = SPEC “ARB:'a” EXISTS_REFL val eq_sym_eq' = AP_TERM “$? :('a -> bool) -> bool” (ABS “x:'a” (SPECL [“x:'a”, “ARB:'a”] EQ_SYM_EQ)) in new_type_definition("itself", EQ_MP eq_sym_eq' itself_exists) end val _ = new_constant("the_value", “:'a itself”) (* prove uniqueness of the itself value: |- !i:'a itself. i = (:'a) *) val ITSELF_UNIQUE = let val typedef_asm = ASSUME (#2 (dest_exists (concl ITSELF_TYPE_DEF))) val typedef_eq0 = AP_THM (INST_TYPE [beta |-> “:'a itself”] TYPE_DEFINITION) “$= (ARB:'a)” val typedef_eq0 = RIGHT_BETA typedef_eq0 val typedef_eq = AP_THM typedef_eq0 “rep:'a itself -> 'a” val typedef_eq = RIGHT_BETA typedef_eq val (typedef_11, typedef_onto) = CONJ_PAIR (EQ_MP typedef_eq typedef_asm) val onto' = INST [“x:'a” |-> “(rep:'a itself -> 'a) i”] (#2 (EQ_IMP_RULE (SPEC_ALL typedef_onto))) val allreps_arb = let val ex' = EXISTS (“?x':'a itself. rep i = rep x':'a”, “i:'a itself”) (REFL “(rep:'a itself -> 'a) i”) in SYM (MP onto' ex') end val allreps_repthevalue = TRANS allreps_arb (SYM (INST [“i:'a itself” |-> “bool$the_value”] allreps_arb)) val all_eq_thevalue = GEN_ALL (MP (SPECL [“i:'a itself”, “bool$the_value”] typedef_11) allreps_repthevalue) in thm (#(FILE), #(LINE))("ITSELF_UNIQUE", CHOOSE (“rep:'a itself -> 'a”, ITSELF_TYPE_DEF) all_eq_thevalue) end (* ITSELF_EQN_RWT = |- f (:'a) = e <=> !x. f x = e *) val ITSELF_EQN_RWT = let fun mk_itty ty = mk_thy_type{Args = [ty], Thy = "bool", Tyop = "itself"} val aitty = mk_itty alpha val f = mk_var("f", aitty --> beta) val e = mk_var("e", beta) val x = mk_var("x", aitty) val r = mk_forall(x, mk_eq(mk_comb(f,x), e)) val itv = mk_thy_const{Name = "the_value", Thy = "bool", Ty = aitty} val l = mk_eq(mk_comb(f,itv), e) val r2l = SPEC itv (ASSUME r) |> DISCH r val l2r = SPEC x ITSELF_UNIQUE |> AP_TERM f |> C TRANS (ASSUME l) |> GEN x |> DISCH l in thm (#(FILE), #(LINE))( "ITSELF_EQN_RWT", GENL [f,e] $ IMP_ANTISYM_RULE l2r r2l ) end (* prove a datatype axiom for the type, allowing definitions of the form f (:'a) = ... *) val itself_Axiom = let val witness = “(\x:'a itself. e : 'b)” val fn_behaves = BETA_CONV (mk_comb(witness, “(:'a)”)) val fn_exists = EXISTS (“?f:'a itself -> 'b. f (:'a) = e”, witness) fn_behaves in thm (#(FILE), #(LINE))("itself_Axiom", GEN_ALL fn_exists) end (* prove induction *) val itself_induction = let val pval = ASSUME “P (:'a) : bool” val pi = EQ_MP (SYM (AP_TERM “P:'a itself -> bool” (SPEC_ALL ITSELF_UNIQUE))) pval in thm (#(FILE), #(LINE))("itself_induction", GEN_ALL (DISCH_ALL (GEN_ALL pi))) end (* define case operator *) val itself_case_thm = let val witness = “λ(i:'a itself) (b:'b). b” val witness_applied1 = BETA_CONV (mk_comb(witness, “(:'a)”)) val witness_applied2 = RIGHT_BETA (AP_THM witness_applied1 “b:'b”) in located_new_specification{ name = "itself_case_thm", constnames = ["itself_case"], witness = EXISTS (“?f:'a itself -> 'b -> 'b. !b. f (:'a) b = b”, witness) (GEN_ALL witness_applied2), loc = mkloc(#(FILE), #(LINE)-5) } end val _ = overload_on("case", “itself_case”) (* FORALL_itself : |- (!x:'a itself. P x) <=> P (:'a) EXISTS_itself : |- (?x:'a itself. P x) <=> P (:'a) *) local val P = mk_var("P", “:'a itself -> bool”) val x = mk_var("x", “:'a itself”) val Px = mk_comb(P, x) val APx = mk_forall(x, Px) val itself = “(:'a)” val Pitself = mk_comb(P, itself) val imp1 = APx |> ASSUME |> SPEC itself |> DISCH_ALL val unique = AP_TERM P (ITSELF_UNIQUE |> SPEC x |> SYM) val imp2 = EQ_MP unique (ASSUME Pitself) |> GEN x |> DISCH_ALL val fa = IMP_ANTISYM_RULE imp1 imp2 val not_not = NOT_CLAUSES |> CONJUNCT1 |> SPEC Px (* exists half *) val imp1 = CHOOSE (x, ASSUME (mk_exists(x,Px))) (EQ_MP (SYM unique) (ASSUME Px)) |> DISCH_ALL val imp2 = EXISTS(mk_exists(x,Px),itself) (ASSUME Pitself) |> DISCH_ALL in val FORALL_itself = thm (#(FILE), #(LINE))("FORALL_itself", fa) val EXISTS_itself = thm (#(FILE), #(LINE)) ("EXISTS_itself", IMP_ANTISYM_RULE imp1 imp2) end; (*---------------------------------------------------------------------------*) (* Pulling FORALL and EXISTS up through /\ and ==> *) (*---------------------------------------------------------------------------*) local val flip = INST [Pb |-> Qb, Qab |-> Pab] val PULL_EXISTS1 = LEFT_FORALL_IMP_THM |> SPEC_ALL |> SYM val PULL_EXISTS2 = LEFT_EXISTS_AND_THM |> SPEC_ALL |> SYM val PULL_EXISTS3 = RIGHT_EXISTS_AND_THM |> SPEC_ALL |> SYM |> flip val PULL_FORALL1 = RIGHT_FORALL_IMP_THM |> SPEC_ALL |> SYM |> flip val PULL_FORALL2 = LEFT_AND_FORALL_THM |> SPEC_ALL val PULL_FORALL3 = RIGHT_AND_FORALL_THM |> SPEC_ALL |> flip in val PULL_EXISTS = thm (#(FILE), #(LINE))("PULL_EXISTS", LIST_CONJ [PULL_EXISTS1, PULL_EXISTS2, PULL_EXISTS3] |> GENL [Pab, Qb]) val PULL_FORALL = thm (#(FILE), #(LINE))("PULL_FORALL", LIST_CONJ [PULL_FORALL1, PULL_FORALL2, PULL_FORALL3] |> GENL [Pab, Qb]) end (*---------------------------------------------------------------------------*) (* PEIRCE = |- ((P ==> Q) ==> P) ==> P *) (*---------------------------------------------------------------------------*) val PEIRCE = thm (#(FILE), #(LINE)) ("PEIRCE", let val th1 = ASSUME “(P ==> Q) ==> P” val th2 = ASSUME “P:bool” val th3 = ASSUME “~P” val th4 = MP th3 th2 val th5 = MP (SPEC “Q:bool” FALSITY) th4 val th6 = DISCH “P:bool” th5 val th7 = MP th1 th6 val th8 = MP th3 th7 val th9 = DISCH “~P” th8 val th10 = MP (SPEC “~P” IMP_F) th9 val th11 = SUBS [SPEC “P:bool” (CONJUNCT1 NOT_CLAUSES)] th10 in DISCH “(P ==> Q) ==> P” th11 end); (* ---------------------------------------------------------------------- JRH_INDUCT_UTIL : !P t. (!x. (x = t) ==> P x) ==> $? P Used multiple times in places relevant to inductive definitions and/or algebraic types. ---------------------------------------------------------------------- *) val JRH_INDUCT_UTIL = let val asm_t = “!x:'a. (x = t) ==> P x” val asm = ASSUME asm_t val t = “t:'a” val P = “P : 'a -> bool” val Pt = MP (SPEC t asm) (REFL t) val ExPx = EXISTS (“?x:'a. P x”, t) Pt val P_eta = SPEC P (INST_TYPE [beta |-> bool] ETA_AX) val ExP_eta = AP_TERM “(?) : ('a -> bool) -> bool” P_eta in thm (#(FILE), #(LINE))("JRH_INDUCT_UTIL", GENL [P, t] (DISCH asm_t (EQ_MP ExP_eta ExPx))) end (* Parsing additions *) (* not an element of *) val _ = overload_on ("NOTIN", “\x:'a y:('a -> bool). ~(x IN y)”) val _ = set_fixity "NOTIN" (Infix(NONASSOC, 425)) val _ = unicode_version {u = UChar.not_elementof, tmnm = "NOTIN"} val _ = TeX_notation {hol="NOTIN", TeX = ("\\HOLTokenNotIn{}",1)} val _ = TeX_notation {hol=UChar.not_elementof, TeX = ("\\HOLTokenNotIn{}",1)} (* not iff *) val _ = overload_on ("<=/=>", “$<> : bool -> bool -> bool”) val _ = set_fixity "<=/=>" (Infix(NONASSOC, 100)) val _ = unicode_version {u = UChar.not_iff, tmnm = "<=/=>"} val _ = TeX_notation {hol="<=/=>", TeX = ("\\HOLTokenNotEquiv{}",3)} val _ = TeX_notation {hol=UChar.not_iff, TeX = ("\\HOLTokenNotEquiv{}",3)} local open boolpp in end val _ = add_ML_dependency "boolpp" val _ = add_user_printer ("bool.COND", “COND gd tr fl”) val _ = add_user_printer ("bool.LET", “LET f x”) val _ = add_absyn_postprocessor "bool.LET" (* |- |- !A B. A \/ B <=> ~A ==> B *) val DISJ_EQ_IMP = thm (#(FILE), #(LINE))("DISJ_EQ_IMP", let val lemma = NOT_CLAUSES |> CONJUNCT1 |> SPEC ``A:bool`` in IMP_DISJ_THM |> SPECL [``~A:bool``,``B:bool``] |> SYM |> CONV_RULE ((RATOR_CONV o RAND_CONV o RATOR_CONV o RAND_CONV) (fn tm => lemma)) |> GENL [``A:bool``,``B:bool``] end); (* ------------------------------------------------------------------------- *) (* CONTRAPOS_THM |- !t1 t2. (~t1 ==> ~t2) <=> (t2 ==> t1) *) (* (HOL-Light compatible) *) (* ------------------------------------------------------------------------- *) val CONTRAPOS_THM = thm (#(FILE), #(LINE)) ("CONTRAPOS_THM", MONO_NOT_EQ |> SYM |> INST [“x:bool” |-> “t1:bool”, “y:bool” |-> “t2:bool”] |> GENL [“t1:bool”, “t2:bool”]); val _ = export_theory();