(* ========================================================================= *)
(* Extensional, classical reasoning with AC starts now!                      *)
(*                                                                           *)
(*       John Harrison, University of Cambridge Computer Laboratory          *)
(*                                                                           *)
(*            (c) Copyright, University of Cambridge 1998                    *)
(*              (c) Copyright, John Harrison 1998-2007                       *)
(* ========================================================================= *)

needs "ind_defs.ml";;

(* ------------------------------------------------------------------------- *)
(* Eta-axiom, corresponding conversion, and extensionality.                  *)
(* ------------------------------------------------------------------------- *)

let ETA_AX = new_axiom
  `!t:A->B. (\x. t x) = t`;;

let ETA_CONV =
  let t = `t:A->B` in
  
let pth = 
prove(`(\x. (t:A->B) x) = t`,
MATCH_ACCEPT_TAC ETA_AX) in fun tm -> try let bv,bod = dest_abs tm in let l,r = dest_comb bod in if r = bv & not (vfree_in bv l) then TRANS (REFL tm) (PINST [type_of bv,aty; type_of bod,bty] [l,t] pth) else fail() with Failure _ -> failwith "ETA_CONV";
;
let EQ_EXT = 
prove (`!(f:A->B) g. (!x. f x = g x) ==> f = g`,
REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o ABS `x:A` o SPEC `x:A`) THEN REWRITE_TAC[ETA_AX]);;
let FUN_EQ_THM = 
prove (`!(f:A->B) g. f = g <=> (!x. f x = g x)`,
REPEAT GEN_TAC THEN EQ_TAC THENL [DISCH_THEN SUBST1_TAC THEN GEN_TAC THEN REFL_TAC; MATCH_ACCEPT_TAC EQ_EXT]);;
(* ------------------------------------------------------------------------- *) (* Indefinite descriptor (giving AC). *) (* ------------------------------------------------------------------------- *) new_constant("@",`:(A->bool)->A`);; parse_as_binder "@";; let is_select = is_binder "@";; let dest_select = dest_binder "@";; let mk_select = mk_binder "@";; let SELECT_AX = new_axiom `!P (x:A). P x ==> P((@) P)`;; (* ------------------------------------------------------------------------- *) (* Useful for compatibility. (The old EXISTS_DEF.) *) (* ------------------------------------------------------------------------- *)
let EXISTS_THM = 
prove (`(?) = \P:A->bool. P ((@) P)`,
MATCH_MP_TAC EQ_EXT THEN BETA_TAC THEN X_GEN_TAC `P:A->bool` THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM ETA_AX] THEN EQ_TAC THENL [DISCH_THEN(CHOOSE_THEN MP_TAC) THEN MATCH_ACCEPT_TAC SELECT_AX; DISCH_TAC THEN EXISTS_TAC `((@) P):A` THEN POP_ASSUM ACCEPT_TAC]);;
(* ------------------------------------------------------------------------- *) (* Rules and so on for the select operator. *) (* ------------------------------------------------------------------------- *) let SELECT_RULE = let P = `P:A->bool` in
let pth = 
prove (`(?) (P:A->bool) ==> P((@) P)`,
SIMP_TAC[SELECT_AX; ETA_AX]) in fun th -> try let abs = rand(concl th) in let ty = type_of(bndvar abs) in CONV_RULE BETA_CONV (MP (PINST [ty,aty] [abs,P] pth) th) with Failure _ -> failwith "SELECT_RULE";
; let SELECT_CONV = let P = `P:A->bool` in
let pth = 
prove (`(P:A->bool)((@) P) = (?) P`,
REWRITE_TAC[EXISTS_THM] THEN BETA_TAC THEN REFL_TAC) in fun tm -> try let is_epsok t = is_select t & let bv,bod = dest_select t in aconv tm (vsubst [t,bv] bod) in let pickeps = find_term is_epsok tm in let abs = rand pickeps in let ty = type_of (bndvar abs) in CONV_RULE (LAND_CONV BETA_CONV) (PINST [ty,aty] [abs,P] pth) with Failure _ -> failwith "SELECT_CONV";
; (* ------------------------------------------------------------------------- *) (* Some basic theorems. *) (* ------------------------------------------------------------------------- *)
let SELECT_REFL = 
prove (`!x:A. (@y. y = x) = x`,
GEN_TAC THEN CONV_TAC SELECT_CONV THEN EXISTS_TAC `x:A` THEN REFL_TAC);;
let SELECT_UNIQUE = 
prove (`!P x. (!y:A. P y = (y = x)) ==> ((@) P = x)`,
REPEAT STRIP_TAC THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM ETA_AX] THEN ASM_REWRITE_TAC[SELECT_REFL]);;
extend_basic_rewrites [SELECT_REFL];; (* ------------------------------------------------------------------------- *) (* Now we can derive type definitions from existence; check benignity. *) (* ------------------------------------------------------------------------- *) let the_type_definitions = ref ([]:((string*string*string)*(thm*thm))list);; let new_type_definition tyname (absname,repname) th = try let th',tth' = assoc (tyname,absname,repname) (!the_type_definitions) in if concl th' <> concl th then failwith "" else (warn true "Benign redefinition of type"; tth') with Failure _ -> let th0 = CONV_RULE (RATOR_CONV (REWR_CONV EXISTS_THM) THENC BETA_CONV) th in let th1,th2 = new_basic_type_definition tyname (absname,repname) th0 in let tth = CONJ (GEN_ALL th1) (GEN_ALL (CONV_RULE(LAND_CONV (TRY_CONV BETA_CONV)) th2)) in the_type_definitions := ((tyname,absname,repname),(th,tth)):: (!the_type_definitions); tth;; (* ------------------------------------------------------------------------- *) (* Derive excluded middle. The proof is an optimization due to Mark Adams of *) (* the original Diaconescu proof as presented in Beeson's book. *) (* ------------------------------------------------------------------------- *)
let EXCLUDED_MIDDLE = 
prove (`!t. t \/ ~t`,
GEN_TAC THEN SUBGOAL_THEN `(((@x. (x <=> F) \/ t) <=> F) \/ t) /\ (((@x. (x <=> T) \/ t) <=> T) \/ t)` MP_TAC THENL [CONJ_TAC THEN CONV_TAC SELECT_CONV THENL [EXISTS_TAC `F`; EXISTS_TAC `T`] THEN DISJ1_TAC THEN REFL_TAC; DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN TRY(DISJ1_TAC THEN FIRST_ASSUM ACCEPT_TAC) THEN DISJ2_TAC THEN DISCH_TAC THEN MP_TAC(ITAUT `~(T <=> F)`) THEN PURE_ONCE_ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[ITAUT `p \/ T <=> T`]]);;
let BOOL_CASES_AX = 
prove (`!t. (t <=> T) \/ (t <=> F)`,
GEN_TAC THEN DISJ_CASES_TAC(SPEC `t:bool` EXCLUDED_MIDDLE) THEN ASM_REWRITE_TAC[]);;
(* ------------------------------------------------------------------------- *) (* Classically based tactics. (See also COND_CASES_TAC later on.) *) (* ------------------------------------------------------------------------- *) let BOOL_CASES_TAC p = STRUCT_CASES_TAC (SPEC p BOOL_CASES_AX);; let ASM_CASES_TAC t = DISJ_CASES_TAC(SPEC t EXCLUDED_MIDDLE);; (* ------------------------------------------------------------------------- *) (* Set up a reasonable tautology checker for classical logic. *) (* ------------------------------------------------------------------------- *) let TAUT = let PROP_REWRITE_TAC = REWRITE_TAC[] in let RTAUT_TAC (asl,w) = let ok t = type_of t = bool_ty & can (find_term is_var) t & free_in t w in (PROP_REWRITE_TAC THEN W((fun t1 t2 -> t1 THEN t2) (REWRITE_TAC[]) o BOOL_CASES_TAC o hd o sort free_in o find_terms ok o snd)) (asl,w) in let TAUT_TAC = REPEAT(GEN_TAC ORELSE CONJ_TAC) THEN REPEAT RTAUT_TAC in fun tm -> prove(tm,TAUT_TAC);; (* ------------------------------------------------------------------------- *) (* A few useful classical tautologies. *) (* ------------------------------------------------------------------------- *) let DE_MORGAN_THM = TAUT `!t1 t2. (~(t1 /\ t2) <=> ~t1 \/ ~t2) /\ (~(t1 \/ t2) <=> ~t1 /\ ~t2)`;; let NOT_CLAUSES = TAUT `(!t. ~ ~t <=> t) /\ (~T <=> F) /\ (~F <=> T)`;; let NOT_IMP = TAUT `!t1 t2. ~(t1 ==> t2) <=> t1 /\ ~t2`;; let CONTRAPOS_THM = TAUT `!t1 t2. (~t1 ==> ~t2) <=> (t2 ==> t1)`;; extend_basic_rewrites [CONJUNCT1 NOT_CLAUSES];; (* ------------------------------------------------------------------------- *) (* Some classically based rules. *) (* ------------------------------------------------------------------------- *) let CCONTR = let P = `P:bool` in let pth = TAUT `(~P ==> F) ==> P` in fun tm th -> try let tm' = mk_neg tm in MP (INST [tm,P] pth) (DISCH tm' th) with Failure _ -> failwith "CCONTR";; let CONTRAPOS_CONV = let a = `a:bool` and b = `b:bool` in let pth = TAUT `(a ==> b) <=> (~b ==> ~a)` in fun tm -> try let P,Q = dest_imp tm in INST [P,a; Q,b] pth with Failure _ -> failwith "CONTRAPOS_CONV";; (* ------------------------------------------------------------------------- *) (* A classicalal "refutation" tactic. *) (* ------------------------------------------------------------------------- *) let REFUTE_THEN = let f_tm = `F` and conv = REWR_CONV(TAUT `p <=> ~p ==> F`) in fun ttac (asl,w as gl) -> if w = f_tm then ALL_TAC gl else if is_neg w then DISCH_THEN ttac gl else (CONV_TAC conv THEN DISCH_THEN ttac) gl;; (* ------------------------------------------------------------------------- *) (* Infinite de Morgan laws. *) (* ------------------------------------------------------------------------- *)
let NOT_EXISTS_THM = 
prove (`!P. ~(?x:A. P x) <=> (!x. ~(P x))`,
GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL [GEN_TAC THEN DISCH_TAC THEN UNDISCH_TAC `~(?x:A. P x)` THEN REWRITE_TAC[] THEN EXISTS_TAC `x:A` THEN POP_ASSUM ACCEPT_TAC; DISCH_THEN(CHOOSE_THEN MP_TAC) THEN ASM_REWRITE_TAC[]]);;
let EXISTS_NOT_THM = 
prove (`!P. (?x:A. ~(P x)) <=> ~(!x. P x)`,
ONCE_REWRITE_TAC[TAUT `(a <=> ~b) <=> (~a <=> b)`] THEN REWRITE_TAC[NOT_EXISTS_THM]);;
let NOT_FORALL_THM = 
prove (`!P. ~(!x. P x) <=> (?x:A. ~(P x))`,
MATCH_ACCEPT_TAC(GSYM EXISTS_NOT_THM));;
let FORALL_NOT_THM = 
prove (`!P. (!x. ~(P x)) <=> ~(?x:A. P x)`,
MATCH_ACCEPT_TAC(GSYM NOT_EXISTS_THM));;
(* ------------------------------------------------------------------------- *) (* Expand quantification over Booleans. *) (* ------------------------------------------------------------------------- *)
let FORALL_BOOL_THM = 
prove (`(!b. P b) <=> P T /\ P F`,
EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN BOOL_CASES_TAC `b:bool` THEN ASM_REWRITE_TAC[]);;
let EXISTS_BOOL_THM = 
prove (`(?b. P b) <=> P T \/ P F`,
MATCH_MP_TAC(TAUT `(~p <=> ~q) ==> (p <=> q)`) THEN REWRITE_TAC[DE_MORGAN_THM; NOT_EXISTS_THM; FORALL_BOOL_THM]);;
(* ------------------------------------------------------------------------- *) (* Universal quantifier and disjunction *) (* ------------------------------------------------------------------------- *)
let LEFT_FORALL_OR_THM = 
prove (`!P Q. (!x:A. P x \/ Q) <=> (!x. P x) \/ Q`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN REWRITE_TAC[NOT_FORALL_THM; DE_MORGAN_THM; LEFT_EXISTS_AND_THM]);;
let RIGHT_FORALL_OR_THM = 
prove (`!P Q. (!x:A. P \/ Q x) <=> P \/ (!x. Q x)`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN REWRITE_TAC[NOT_FORALL_THM; DE_MORGAN_THM; RIGHT_EXISTS_AND_THM]);;
let LEFT_OR_FORALL_THM = 
prove (`!P Q. (!x:A. P x) \/ Q <=> (!x. P x \/ Q)`,
MATCH_ACCEPT_TAC(GSYM LEFT_FORALL_OR_THM));;
let RIGHT_OR_FORALL_THM = 
prove (`!P Q. P \/ (!x:A. Q x) <=> (!x. P \/ Q x)`,
MATCH_ACCEPT_TAC(GSYM RIGHT_FORALL_OR_THM));;
(* ------------------------------------------------------------------------- *) (* Implication and quantifiers. *) (* ------------------------------------------------------------------------- *)
let LEFT_IMP_FORALL_THM = 
prove (`!P Q. ((!x:A. P x) ==> Q) <=> (?x. P x ==> Q)`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN REWRITE_TAC[NOT_EXISTS_THM; NOT_IMP; LEFT_AND_FORALL_THM]);;
let LEFT_EXISTS_IMP_THM = 
prove (`!P Q. (?x. P x ==> Q) <=> ((!x:A. P x) ==> Q)`,
MATCH_ACCEPT_TAC(GSYM LEFT_IMP_FORALL_THM));;
let RIGHT_IMP_EXISTS_THM = 
prove (`!P Q. (P ==> ?x:A. Q x) <=> (?x:A. P ==> Q x)`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN REWRITE_TAC[NOT_EXISTS_THM; NOT_IMP; RIGHT_AND_FORALL_THM]);;
let RIGHT_EXISTS_IMP_THM = 
prove (`!P Q. (?x:A. P ==> Q x) <=> (P ==> ?x:A. Q x)`,
MATCH_ACCEPT_TAC(GSYM RIGHT_IMP_EXISTS_THM));;
(* ------------------------------------------------------------------------- *) (* The conditional. *) (* ------------------------------------------------------------------------- *)
let COND_DEF = new_definition
  `COND = \t t1 t2. @x:A. ((t <=> T) ==> (x = t1)) /\
                          ((t <=> F) ==> (x = t2))`;;
let COND_CLAUSES = 
prove (`!(t1:A) t2. ((if T then t1 else t2) = t1) /\ ((if F then t1 else t2) = t2)`,
REWRITE_TAC[COND_DEF]);;
let is_cond tm = try fst(dest_const(rator(rator (rator tm)))) = "COND" with Failure _ -> false;; let mk_cond (b,x,y) = try let c = mk_const("COND",[type_of x,aty]) in mk_comb(mk_comb(mk_comb(c,b),x),y) with Failure _ -> failwith "mk_cond";; let dest_cond tm = try let tm1,y = dest_comb tm in let tm2,x = dest_comb tm1 in let c,b = dest_comb tm2 in if fst(dest_const c) = "COND" then (b,(x,y)) else fail() with Failure _ -> failwith "dest_cond";; extend_basic_rewrites [COND_CLAUSES];;
let COND_EXPAND = 
prove (`!b t1 t2. (if b then t1 else t2) <=> (~b \/ t1) /\ (b \/ t2)`,
REPEAT GEN_TAC THEN BOOL_CASES_TAC `b:bool` THEN REWRITE_TAC[]);;
let COND_ID = 
prove (`!b (t:A). (if b then t else t) = t`,
REPEAT GEN_TAC THEN BOOL_CASES_TAC `b:bool` THEN REWRITE_TAC[]);;
let COND_RAND = 
prove (`!b (f:A->B) x y. f (if b then x else y) = (if b then f x else f y)`,
REPEAT GEN_TAC THEN BOOL_CASES_TAC `b:bool` THEN REWRITE_TAC[]);;
let COND_RATOR = 
prove (`!b (f:A->B) g x. (if b then f else g)(x) = (if b then f x else g x)`,
REPEAT GEN_TAC THEN BOOL_CASES_TAC `b:bool` THEN REWRITE_TAC[]);;
let COND_ABS = 
prove (`!b (f:A->B) g. (\x. if b then f x else g x) = (if b then f else g)`,
REPEAT GEN_TAC THEN BOOL_CASES_TAC `b:bool` THEN REWRITE_TAC[ETA_AX]);;
(* ------------------------------------------------------------------------- *) (* Redefine TAUT to freeze in the rewrites including COND. *) (* ------------------------------------------------------------------------- *) let TAUT = let PROP_REWRITE_TAC = REWRITE_TAC[] in let RTAUT_TAC (asl,w) = let ok t = type_of t = bool_ty & can (find_term is_var) t & free_in t w in (PROP_REWRITE_TAC THEN W((fun t1 t2 -> t1 THEN t2) (REWRITE_TAC[]) o BOOL_CASES_TAC o hd o sort free_in o find_terms ok o snd)) (asl,w) in let TAUT_TAC = REPEAT(GEN_TAC ORELSE CONJ_TAC) THEN REPEAT RTAUT_TAC in fun tm -> prove(tm,TAUT_TAC);; (* ------------------------------------------------------------------------- *) (* Throw monotonicity in. *) (* ------------------------------------------------------------------------- *)
let MONO_COND = 
prove (`(A ==> B) /\ (C ==> D) ==> (if b then A else C) ==> (if b then B else D)`,
STRIP_TAC THEN BOOL_CASES_TAC `b:bool` THEN ASM_REWRITE_TAC[]);;
monotonicity_theorems := MONO_COND::(!monotonicity_theorems);; (* ------------------------------------------------------------------------- *) (* Tactic for splitting over an arbitrarily chosen conditional. *) (* ------------------------------------------------------------------------- *)
let COND_ELIM_THM = 
prove (`(P:A->bool) (if c then x else y) <=> (c ==> P x) /\ (~c ==> P y)`,
BOOL_CASES_TAC `c:bool` THEN REWRITE_TAC[]);;
let COND_ELIM_CONV = HIGHER_REWRITE_CONV[COND_ELIM_THM] true;; let (COND_CASES_TAC :tactic) = let DENEG_RULE = GEN_REWRITE_RULE I [TAUT `~ ~ p <=> p`] in CONV_TAC COND_ELIM_CONV THEN CONJ_TAC THENL [DISCH_THEN(fun th -> ASSUME_TAC th THEN SUBST1_TAC(EQT_INTRO th)); DISCH_THEN(fun th -> try let th' = DENEG_RULE th in ASSUME_TAC th' THEN SUBST1_TAC(EQT_INTRO th') with Failure _ -> ASSUME_TAC th THEN SUBST1_TAC(EQF_INTRO th))];; (* ------------------------------------------------------------------------- *) (* Skolemization. *) (* ------------------------------------------------------------------------- *)
let SKOLEM_THM = 
prove (`!P. (!x:A. ?y:B. P x y) <=> (?y. !x. P x (y x))`,
REPEAT(STRIP_TAC ORELSE EQ_TAC) THENL [EXISTS_TAC `\x:A. @y:B. P x y` THEN GEN_TAC THEN BETA_TAC THEN CONV_TAC SELECT_CONV; EXISTS_TAC `(y:A->B) x`] THEN POP_ASSUM MATCH_ACCEPT_TAC);;
let SKOLEM_THM_GEN = 
prove (`!P s. (!x. P x ==> ?y. R x y) <=> (?f. !x. P x ==> R x (f x))`,
(* ------------------------------------------------------------------------- *) (* NB: this one is true intutionistically and intensionally. *) (* ------------------------------------------------------------------------- *)
let UNIQUE_SKOLEM_ALT = 
prove (`!P:A->B->bool. (!x. ?!y. P x y) <=> ?f. !x y. P x y <=> (f x = y)`,
GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_ALT; SKOLEM_THM]);;
(* ------------------------------------------------------------------------- *) (* and this one intuitionistically and extensionally. *) (* ------------------------------------------------------------------------- *)
let UNIQUE_SKOLEM_THM = 
prove (`!P. (!x:A. ?!y:B. P x y) <=> (?!f. !x. P x (f x))`,
GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_THM; SKOLEM_THM; FORALL_AND_THM] THEN EQ_TAC THEN DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN ASM_REWRITE_TAC[] THENL [REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `x:A` THEN FIRST_ASSUM MATCH_MP_TAC THEN EXISTS_TAC `x:A` THEN ASM_REWRITE_TAC[]; MAP_EVERY X_GEN_TAC [`x:A`; `y1:B`; `y2:B`] THEN STRIP_TAC THEN FIRST_ASSUM(X_CHOOSE_TAC `f:A->B`) THEN SUBGOAL_THEN `(\z. if z = x then y1 else (f:A->B) z) = (\z. if z = x then y2 else (f:A->B) z)` MP_TAC THENL [FIRST_ASSUM MATCH_MP_TAC THEN REPEAT STRIP_TAC THEN BETA_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[]; DISCH_THEN(MP_TAC o C AP_THM `x:A`) THEN REWRITE_TAC[]]]);;
(* ------------------------------------------------------------------------- *) (* Extend default congruences for contextual rewriting. *) (* ------------------------------------------------------------------------- *) let COND_CONG = TAUT `(g = g') ==> (g' ==> (t = t')) ==> (~g' ==> (e = e')) ==> ((if g then t else e) = (if g' then t' else e'))` in extend_basic_congs [COND_CONG];;
let COND_EQ_CLAUSE = 
prove (`(if x = x then y else z) = y`,
REWRITE_TAC[]) in extend_basic_rewrites [COND_EQ_CLAUSE];;
(* ------------------------------------------------------------------------- *) (* We can now treat "bool" as an enumerated type for some purposes. *) (* ------------------------------------------------------------------------- *)
let bool_INDUCT = 
prove (`!P. P F /\ P T ==> !x. P x`,
REPEAT STRIP_TAC THEN DISJ_CASES_TAC(SPEC `x:bool` BOOL_CASES_AX) THEN ASM_REWRITE_TAC[]);;
let bool_RECURSION = 
prove (`!a b:A. ?f. f F = a /\ f T = b`,
REPEAT GEN_TAC THEN EXISTS_TAC `\x. if x then b:A else a` THEN REWRITE_TAC[]);;
let inductive_type_store = ref ["bool",(2,bool_INDUCT,bool_RECURSION)];;