(* ========================================================================= *)
(* Mizar-style proofs integrated with the HOL goalstack. *)
(* *)
(* John Harrison, University of Cambridge Computer Laboratory *)
(* *)
(* (c) Copyright, University of Cambridge 1998 *)
(* ========================================================================= *)
let old_parse_term = parse_term;;
(* ------------------------------------------------------------------------- *)
(* This version of CHOOSE is more convenient to "itlist". *)
(* ------------------------------------------------------------------------- *)
let IMP_CHOOSE_RULE =
let P = `P:A->bool`
and Q = `Q:bool`
and pth = prove
(`(!x:A. P x ==> Q) ==> ((?) P ==> Q)`,
GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV) [GSYM ETA_AX] THEN
REWRITE_TAC[LEFT_IMP_EXISTS_THM]) in
fun v th ->
let ant,con = dest_imp (concl th) in
let pred = mk_abs(v,ant) in
let tm = concl th in
let q = rand tm in
let th1 = BETA_CONV(mk_comb(pred,v)) in
let th2 = PINST [type_of v,aty] [pred,P; q,Q] pth in
let th3 = AP_THM (AP_TERM (rator(rator tm)) th1) q in
let th4 = GEN v (EQ_MP (SYM th3) th) in
MP th2 th4;;
(* ------------------------------------------------------------------------- *)
(* Some preterm operations we need. *)
(* ------------------------------------------------------------------------- *)
let rec split_ppair ptm =
match ptm with
Combp(Combp(Varp(",",dpty),ptm1),ptm2) -> ptm1::(split_ppair ptm2)
| _ -> [ptm];;
let pmk_conj(ptm1,ptm2) =
Combp(Combp(Varp("/\\",dpty),ptm1),ptm2);;
let pmk_exists(v,ptm) =
Combp(Varp("?",dpty),Absp(v,ptm));;
(* ------------------------------------------------------------------------- *)
(* Typecheck a preterm into a term in an environment of (typed) variables. *)
(* ------------------------------------------------------------------------- *)
let typecheck_in_env env ptm =
let penv = itlist
(fun v acc -> let n,ty = dest_var v in (n,pretype_of_type ty)::acc)
env [] in
(term_of_preterm o retypecheck penv) ptm;;
(* ------------------------------------------------------------------------- *)
(* Converts a labelled preterm (using "and"s) into a single conjunction. *)
(* ------------------------------------------------------------------------- *)
let delabel lfs = end_itlist (curry pmk_conj) (map snd lfs);;
(* ------------------------------------------------------------------------- *)
(* These special constants are replaced by useful bits when encountered: *)
(* *)
(* thesis -- Current thesis (i.e. conclusion of goal). *)
(* *)
(* antecedent -- antecedent of goal, if applicable *)
(* *)
(* contradiction -- falsity *)
(* *)
(* ... -- Right hand side of previous conclusion. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* This function performs the replacement, and typechecks in current env. *)
(* *)
(* The replacement of "..." is done specially, since it also adds a "then". *)
(* ------------------------------------------------------------------------- *)
let mizarate_term =
let atm = `antecedent`
and ttm = `thesis`
and ctm = `contradiction` in
let f_tm = `F` in
let filter_env fvs =
let env1 = map dest_var fvs in
let sizes = map
(fun (v,_) -> v,length (filter ((=) v o fst) env1)) env1 in
let env2 = filter (fun (v,_) -> assoc v sizes = 1) env1 in
map mk_var env2 in
let goal_lconsts (asl,w) =
itlist (union o frees o concl o snd) asl (frees w) in
fun (asl,w as gl) ptm ->
let lconsts = goal_lconsts gl in
let tm = typecheck_in_env (filter_env lconsts) ptm in
let ant = try fst(dest_imp w) with Failure _ -> atm in
subst [w,ttm; ant,atm; f_tm,ctm] tm;;
(* ------------------------------------------------------------------------- *)
(* The following is occasionally useful as a hack. *)
(* ------------------------------------------------------------------------- *)
let LIMITED_REWRITE_CONV =
let LIMITED_ONCE_REWRITE_CONV ths =
GEN_REWRITE_CONV ONCE_DEPTH_CONV ths THENC
GENERAL_REWRITE_CONV true TOP_DEPTH_CONV (basic_net()) [] in
fun n ths tm ->
funpow n (CONV_RULE(RAND_CONV(LIMITED_ONCE_REWRITE_CONV ths)))
(REFL tm);;
(* ------------------------------------------------------------------------- *)
(* The default prover. *)
(* ------------------------------------------------------------------------- *)
let DEFAULT_PROVER =
let FREEZE_THENL fn ths x =
let ths' = map (ASSUME o concl) ths in
let th = fn ths' x in
itlist PROVE_HYP ths th in
let REWRITE_PROVER ths tm =
if length ths < 2 then
EQT_ELIM(LIMITED_REWRITE_CONV 3 ths tm)
else
let ths' = tl ths in
let th' = CONV_RULE (LIMITED_REWRITE_CONV 4 ths') (hd ths) in
EQT_ELIM(LIMITED_REWRITE_CONV 4 (th'::ths') tm) in
fun ths tm ->
let sths = itlist (union o CONJUNCTS) ths [] in
try prove(tm,MAP_FIRST MATCH_ACCEPT_TAC sths)
with Failure _ -> try
FREEZE_THENL REWRITE_PROVER ths tm
with Failure _ ->
prove(tm,GEN_MESON_TAC 0 30 1 ths);;
let default_prover = ref DEFAULT_PROVER;;
let prover_list = ref
["rewriting",(fun ths tm -> EQT_ELIM(REWRITE_CONV ths tm))];;
(* ------------------------------------------------------------------------- *)
(* "arithmetic",(fun ths tm -> *)
(* let tm' = itlist (curry mk_imp o concl) ths tm in *)
(* let th = REAL_ARITH tm' in *)
(* rev_itlist (C MP) ths th);; *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Produce a "default" label for various constructs where applicable. *)
(* ------------------------------------------------------------------------- *)
let default_assumptions = ref false;;
let mklabel s =
if s = "" & !default_assumptions then "*"
else s;;
(* ------------------------------------------------------------------------- *)
(* Augment assumptions, throwing away an *unnamed* previous step. *)
(* ------------------------------------------------------------------------- *)
let augments =
let augment nw asl =
if asl = [] then [nw]
else if fst(hd asl) = "" then nw::(tl asl)
else nw::asl in
fun labs th asl ->
let ths,thl = nsplit CONJ_PAIR (tl labs) th in
itlist augment (zip (map mklabel labs) (ths@[thl])) asl;;
(* ------------------------------------------------------------------------- *)
(* Wrapper for labels in justification list (use K for preproved theorems). *)
(* ------------------------------------------------------------------------- *)
let L s asl =
if s = "" then snd(hd asl) else ((assoc s asl):thm);;
(* ------------------------------------------------------------------------- *)
(* Perform justification, given asl and target. *)
(* ------------------------------------------------------------------------- *)
let JUSTIFY (prover,tlist) asl tm =
let xthms = map (C I asl) tlist in
let proof_fn =
if prover = "" then !default_prover
else assoc prover (!prover_list) in
let ithms = map snd (filter ((=) "*" o fst) asl) in
proof_fn (xthms @ ithms) tm;;
(* ------------------------------------------------------------------------- *)
(* Either do justification or split off subproof then call ttac with result. *)
(* ------------------------------------------------------------------------- *)
let JUSTIFY_THEN wtm ((pr,tls) as jdata) ttac (asl,w as gl) =
if pr = "proof" then
SUBGOAL_THEN wtm ttac gl
else
let wth = JUSTIFY jdata asl wtm in
ttac wth gl;;
(* ------------------------------------------------------------------------- *)
(* Utilise a conclusion. *)
(* ------------------------------------------------------------------------- *)
let (MIZAR_CONCLUSION_TAC:thm_tactic) =
let t_tm = `T` in
let CONJ_ASSOC_RULE =
EQT_ELIM o
GEN_REWRITE_RULE RAND_CONV [EQT_INTRO(SPEC_ALL EQ_REFL)] o
PURE_REWRITE_CONV[GSYM CONJ_ASSOC] in
fun th (asl,w as gl) ->
let cjs = conjuncts(concl th) in
let cjs1,cjs2 = chop_list(length cjs) (conjuncts w) in
if cjs2 = [] then
let th' = EQ_MP (CONJ_ASSOC_RULE(mk_eq(concl th,w))) th in
null_meta,[asl,t_tm],fun i _ -> INSTANTIATE i th'
else
let w1 = list_mk_conj cjs1
and w2 = list_mk_conj cjs2 in
let w12 = mk_conj(w1,w2) in
let th' = EQ_MP (CONJ_ASSOC_RULE(mk_eq(concl th,w1))) th in
let wth = CONJ_ASSOC_RULE(mk_eq(w,w12)) in
(SUBST1_TAC wth THEN CONJ_TAC THENL [ACCEPT_TAC th'; ALL_TAC]) gl;;
(* ------------------------------------------------------------------------- *)
(* Transitivity chain stuff; store a list of useful transitivity theorems. *)
(* ------------------------------------------------------------------------- *)
let mizar_transitivity_net = ref empty_net;;
let add_mizar_transitivity_theorem th =
let pat = fst(dest_imp(snd(strip_forall(concl th)))) in
mizar_transitivity_net :=
enter [] (pat,MATCH_MP th) (!mizar_transitivity_net);;
let TRANSITIVITY_CHAIN th1 th2 ttac =
let tm1 = concl th1
and tm2 = concl th2 in
let th =
if is_eq tm1 then
EQ_MP (SYM (AP_THM (AP_TERM (rator(rator tm2)) th1) (rand tm2))) th2
else if is_eq tm2 then
EQ_MP (AP_TERM (rator tm1) th2) th1
else
let th12 = CONJ th1 th2 in
tryfind (fun rule -> rule th12)
(lookup (concl th12) (!mizar_transitivity_net)) in
ttac th;;
(* ------------------------------------------------------------------------- *)
(* Perform terminal or initial step. *)
(* ------------------------------------------------------------------------- *)
let MIZAR_SUBSTEP_TAC =
fun labs thm (asl,w) ->
let asl' = augments labs thm asl in
null_meta,[asl',w],
K(function [th] -> PROVE_HYP thm th | _ -> fail());;
let MIZAR_BISTEP_TAC =
fun termflag labs jth ->
if termflag then
MIZAR_SUBSTEP_TAC labs jth THEN
MIZAR_CONCLUSION_TAC jth
else
MIZAR_SUBSTEP_TAC labs jth;;
let MIZAR_STEP_TAC =
fun termflag lfs (pr,tls as jdata) (asl,w as gl) ->
let tm = mizarate_term gl (delabel lfs) in
if try fst(dest_const(lhand tm)) = "..." with Failure _ -> false then
let thp = snd(hd asl) in
let lhd = rand(concl thp) in
let tm' = mk_comb(mk_comb(rator(rator tm),lhd),rand tm) in
JUSTIFY_THEN tm' (pr,tls)
(fun th -> TRANSITIVITY_CHAIN thp th
(MIZAR_BISTEP_TAC termflag (map fst lfs))) gl
else
JUSTIFY_THEN tm (pr,tls)
(MIZAR_BISTEP_TAC termflag (map fst lfs)) gl;;
(* ------------------------------------------------------------------------- *)
(* Perform an "end": finish the trivial goal. *)
(* ------------------------------------------------------------------------- *)
let MIZAR_END_TAC = ACCEPT_TAC TRUTH;;
(* ------------------------------------------------------------------------- *)
(* Perform "assume <lform>" *)
(* ------------------------------------------------------------------------- *)
let (MIZAR_ASSUME_TAC: (string * preterm) list -> tactic) =
let f_tm = `F`
and CONTRA_HACK = CONV_RULE(REWR_CONV(TAUT `(~p ==> F) <=> p`)) in
fun lfs (asl,w as gl) ->
let tm = mizarate_term gl (delabel lfs) in
if try aconv (dest_neg tm) w with Failure _ -> false then
(null_meta,[augments (map fst lfs) (ASSUME tm) asl,f_tm],
(fun i -> function [th] -> CONTRA_HACK(DISCH (instantiate i tm) th)
| _ -> fail()))
else if try aconv tm (fst(dest_imp w)) with Failure _ -> false then
(null_meta,[augments (map fst lfs) (ASSUME tm) asl,rand w],
(fun i -> function [th] -> DISCH (instantiate i tm) th
| _ -> fail()))
else failwith "MIZAR_ASSUME_REF: Bad thesis";;
(* ------------------------------------------------------------------------- *)
(* Perform "let <v1>,...,<vn> [be <type>]" *)
(* ------------------------------------------------------------------------- *)
let (MIZAR_LET_TAC: preterm list * hol_type list -> tactic) =
fun (vlist,tys) (asl,w as gl) ->
let ty = if tys = [] then type_of(fst(dest_forall w)) else hd tys in
let pty = pretype_of_type ty in
let mk_varb v =
(term_of_preterm o retypecheck []) (Typing(v,pty)) in
let vs = map mk_varb vlist in
MAP_EVERY X_GEN_TAC vs gl;;
(* ------------------------------------------------------------------------- *)
(* Perform "take <tm>" *)
(* ------------------------------------------------------------------------- *)
let (MIZAR_TAKE_TAC: preterm -> tactic) =
fun ptm (asl,w as gl) ->
let ptm' = Typing(ptm,pretype_of_type(type_of(fst(dest_exists w)))) in
let tm = mizarate_term (asl,w) ptm' in
EXISTS_TAC tm gl;;
(* ------------------------------------------------------------------------- *)
(* Perform "suffices to prove <form> by <just>". *)
(* ------------------------------------------------------------------------- *)
let MIZAR_SUFFICES_TAC =
fun new0 ((pr,tlist) as jdata) (asl,w as gl) ->
let nw = mizarate_term gl (end_itlist (curry pmk_conj) new0) in
JUSTIFY_THEN (mk_imp(nw,w)) jdata
(fun jth (asl,w) ->
null_meta,[asl,nw],
(fun i -> function [th] -> MP (INSTANTIATE_ALL i jth) th
| _ -> fail())) gl;;
(* ------------------------------------------------------------------------- *)
(* Perform "set <lform>" *)
(* ------------------------------------------------------------------------- *)
let MIZAR_SET_TAC =
fun (lab,ptm) (asl,w as gl) ->
let tm = mizarate_term gl ptm in
let v,t = dest_eq tm in
CHOOSE_THEN (fun th -> SUBST_ALL_TAC th THEN
LABEL_TAC (mklabel lab) (SYM th))
(EXISTS(mk_exists(v,mk_eq(t,v)),t) (REFL t)) gl;;
(* ------------------------------------------------------------------------- *)
(* Perform "consider <vars> such that <lform> by <just>". *)
(* ------------------------------------------------------------------------- *)
let MIZAR_CONSIDER_TAC =
fun vars0 lfs ((pr,tls) as jdata) (asl,w as gl) ->
let ptm = itlist (curry pmk_exists) vars0 (delabel lfs) in
let etm = mizarate_term gl ptm in
let vars,tm = nsplit dest_exists vars0 etm in
JUSTIFY_THEN etm jdata
(fun jth (asl,w) ->
null_meta,[augments (map fst lfs) (ASSUME tm) asl,w],
(fun i -> function [th] -> MP (itlist IMP_CHOOSE_RULE vars
(DISCH (instantiate i tm) th)) jth
| _ -> fail())) gl;;
(* ------------------------------------------------------------------------- *)
(* Perform "given <terms> such that <lform>". *)
(* ------------------------------------------------------------------------- *)
let MIZAR_GIVEN_TAC =
fun vars0 lfs (asl,w as gl) ->
let ant = fst(dest_imp w) in
let gvars,gbod = nsplit dest_exists vars0 ant in
let tvars = map2
(fun p v -> Typing(p,pretype_of_type(snd(dest_var v)))) vars0 gvars in
let ptm = itlist (curry pmk_exists) tvars (delabel lfs) in
let etm = mizarate_term gl ptm in
let vars,tm = nsplit dest_exists vars0 etm in
if try aconv ant etm with Failure _ -> false then
null_meta,[augments (map fst lfs) (ASSUME tm) asl,rand w],
(fun i -> function [th] -> DISCH ant
(MP (itlist IMP_CHOOSE_RULE vars
(DISCH (instantiate i tm) th))
(ASSUME ant))
| _ -> fail())
else failwith "MIZAR_GIVEN_TAC: Bad thesis";;
(* ------------------------------------------------------------------------- *)
(* Initialize a case split. *)
(* ------------------------------------------------------------------------- *)
let MIZAR_PER_CASES_TAC =
fun jdata (asl,w as gl) ->
null_meta,[gl],
K(function [th] ->
let ghyps = itlist (union o hyp o snd) asl [] in
let rogues = subtract (hyp th) ghyps in
if rogues = [] then th
else if tl rogues = [] then
let thm = JUSTIFY jdata asl (hd rogues) in
PROVE_HYP thm th
else failwith "MIZAR_PER_CASES_ATAC: Too many suppositions"
| _ -> fail());;
(* ------------------------------------------------------------------------- *)
(* Perform a case split. NB! This tactic is not "valid" in the LCF sense. *)
(* We could make it so, but that would force classical logic! *)
(* ------------------------------------------------------------------------- *)
let MIZAR_SUPPOSE_TAC =
fun lfs (asl,w as gl) ->
let asm = mizarate_term gl (delabel lfs) in
let ghyps = itlist (union o hyp o snd) asl [] in
null_meta,
[augments (map fst lfs) (ASSUME asm) asl,w; gl],
K(function [th1; th2] ->
let hyp1 = hyp th1
and hyp2 = hyp th2 in
let asm1 = subtract hyp1 ghyps
and asm2 = subtract hyp2 ghyps in
if asm1 = [] then th1 else if asm2 = [] then th2
else if tl asm1 = [] & tl asm2 = [] then
DISJ_CASES (ASSUME(mk_disj(hd asm1,hd asm2))) th1 th2
else failwith "MIZAR_SUPPOSE_TAC: Too many suppositions"
| _ -> fail());;
let MIZAR_SUPPOSE_REF lfs =
by (MIZAR_SUPPOSE_TAC lfs) o by (TRY MIZAR_END_TAC);;
(* ------------------------------------------------------------------------- *)
(* Terminate a case split. *)
(* ------------------------------------------------------------------------- *)
let MIZAR_RAW_ENDCASE_TAC =
let pth = ITAUT `F ==> p`
and p = `p:bool` in
fun (asl,w) ->
let th = UNDISCH (INST [w,p] pth) in
null_meta,[],fun _ _ -> th;;
let MIZAR_ENDCASE_REF =
by MIZAR_RAW_ENDCASE_TAC o by (TRY MIZAR_END_TAC);;
(* ------------------------------------------------------------------------- *)
(* Parser-processor for textual version of Mizar proofs. *)
(* ------------------------------------------------------------------------- *)
let add_mizar_words,subtract_mizar_words =
let l = ["assume"; "take"; "set"; "given"; "such"; "that";
"proof"; "end"; "consider"; "suffices"; "to"; "show";
"per"; "cases"; "endcase"; "suppose"; "be";
"then"; "thus"; "hence"; "by"; "so"] in
(fun () -> reserve_words l),
(fun () -> unreserve_words l);;
let parse_preform l =
let ptm,rst = parse_preterm l in
let ptm' = Typing(ptm,Ptycon("bool",[])) in
ptm',rst;;
let parse_fulltype l =
let pty,rst = parse_pretype l in
type_of_pretype pty,rst;;
let parse_ident l =
match (hd l) with
Ident n -> n,tl l
| _ -> raise Noparse;;
let parse_string l =
match (hd l) with
Ident n -> n,tl l
| Resword n -> n,tl l;;
let rec parse_lform oldlab l =
match l with
(Ident n)::(Resword ":")::rst ->
if oldlab = "" then parse_lform n rst
else failwith "Too many labels"
| _ -> let fm,rst = parse_preform l in (oldlab,fm),rst;;
let parse_lforms oldlab =
listof (parse_lform oldlab) (a (Resword "and")) "labelled formula";;
let parse_just tlink l =
if l = [] then
if tlink then ("",[L""]),l
else ("",[]),l else
match (hd l) with
Resword "by" ->
let pot,rem = parse_string (tl l) in
if rem = [] or hd rem <> Ident "," & hd rem <> Ident "with" then
if can (assoc pot) (!prover_list) then
(pot,if tlink then [L""] else []),rem
else
("",if tlink then [L""; L pot] else [L pot]),rem
else if hd rem = Ident "," then
let oths,rst = listof parse_string (a (Ident ",")) "theorem name"
(tl rem) in
let ths = if tlink then ""::pot::oths else pot::oths in
("",map L ths),rst
else
let oths,rst = listof parse_string (a (Ident ",")) "theorem name"
(tl rem) in
let ths = if tlink then ""::oths else oths in
(pot,map L ths),rst
| Resword "proof" ->
("proof",[]),tl l
| _ ->
if tlink then ("",[L""]),l
else ("",[]),l;;
let rec parse_step tlink l =
(a (Resword "assume") ++ parse_lforms ""
>> (by o MIZAR_ASSUME_TAC o snd)
|| a (Resword "let") ++ (parse_preterm >> split_ppair) ++
possibly (a (Resword "be") ++ parse_fulltype >> snd)
>> (fun ((_,vnames),ty) -> by (MIZAR_LET_TAC (vnames,ty)))
|| a (Resword "take") ++ parse_preterm
>> (by o MIZAR_TAKE_TAC o snd)
|| a (Resword "set") ++ parse_lforms ""
>> (itlist (by o MIZAR_SET_TAC) o snd)
|| a (Resword "consider") ++
(parse_preterm >> split_ppair) ++
a (Resword "such") ++
a (Resword "that") ++
parse_lforms "" ++
parse_just tlink
>> (fun (((((_,vars),_),_),lf),jst) -> by (MIZAR_CONSIDER_TAC vars lf jst))
|| a (Resword "given") ++
(parse_preterm >> split_ppair) ++
a (Resword "such") ++
a (Resword "that") ++
parse_lforms ""
>> (fun ((((_,vars),_),_),lf) -> by (MIZAR_GIVEN_TAC vars lf))
|| a (Resword "suffices") ++
a (Resword "to") ++
a (Resword "show") ++
parse_lforms "" ++
parse_just tlink
>> (fun ((((_,_),_),lf),jst) -> by (MIZAR_SUFFICES_TAC (map snd lf) jst))
|| a (Resword "per") ++
a (Resword "cases") ++
parse_just tlink
>> (fun ((_,_),jst) -> by (MIZAR_PER_CASES_TAC jst))
|| a (Resword "suppose") ++
parse_lforms ""
>> (fun (_,lf) -> MIZAR_SUPPOSE_REF lf)
|| a (Resword "endcase")
>> K MIZAR_ENDCASE_REF
|| a (Resword "end")
>> K (by MIZAR_END_TAC)
|| a (Resword "then") ++ parse_step true
>> snd
|| a (Resword "so") ++ parse_step true
>> snd
|| a (Resword "hence") ++
parse_lforms "" ++
parse_just true
>> (fun ((_,lf),jst) -> by (MIZAR_STEP_TAC true lf jst))
|| a (Resword "thus") ++
parse_lforms "" ++
parse_just tlink
>> (fun ((_,lf),jst) -> by (MIZAR_STEP_TAC true lf jst))
|| parse_lforms "" ++ parse_just tlink
>> (fun (lf,jst) -> by (MIZAR_STEP_TAC false lf jst))) l;;
(* ------------------------------------------------------------------------- *)
(* From now on, quotations evaluate to preterms. *)
(* ------------------------------------------------------------------------- *)
let run_steps lexemes =
let rec compose_steps lexemes gs =
if lexemes = [] then gs else
let rf,rest = parse_step false lexemes in
let gs' = rf gs in
if rest <> [] & hd rest = Resword ";" then compose_steps (tl rest) gs'
else compose_steps rest gs' in
refine (compose_steps lexemes);;
(* ------------------------------------------------------------------------- *)
(* Include some theorems. *)
(* ------------------------------------------------------------------------- *)
do_list add_mizar_transitivity_theorem
[LE_TRANS; LT_TRANS; LET_TRANS; LTE_TRANS];;
do_list add_mizar_transitivity_theorem
[INT_LE_TRANS; INT_LT_TRANS; INT_LET_TRANS; INT_LTE_TRANS];;
do_list add_mizar_transitivity_theorem
[REAL_LE_TRANS; REAL_LT_TRANS; REAL_LET_TRANS; REAL_LTE_TRANS];;
do_list add_mizar_transitivity_theorem
[SUBSET_TRANS; PSUBSET_TRANS; PSUBSET_SUBSET_TRANS; SUBSET_PSUBSET_TRANS];;
(* ------------------------------------------------------------------------- *)
(* Simple example: Knaster-Tarski fixpoint theorem. *)
(* ------------------------------------------------------------------------- *)
add_mizar_words();;
hide_constant "<=";;
(*** Set up goal ***)
g `!f. (!x y. x <= y /\ y <= x ==> (x = y)) /\
(!x y z. x <= y /\ y <= z ==> x <= z) /\
(!x y. x <= y ==> f x <= f y) /\
(!X. ?s:A. (!x. x IN X ==> s <= x) /\
(!s'. (!x. x IN X ==> s' <= x) ==> s' <= s))
==> ?x. f x = x`;;
(*** Start parsing quotations as Mizar directives ***)
let parse_term = run_steps o lex o explode;;
(*** Label the external facts needed ***)
e(LABEL_TAC "IN_ELIM_THM" IN_ELIM_THM);;
e(LABEL_TAC "BETA_THM" BETA_THM);;
(*** The proof itself ***)
`let f be A->A;
assume L:antecedent;
antisymmetry: (!x y. x <= y /\ y <= x ==> (x = y)) by L;
transitivity: (!x y z. x <= y /\ y <= z ==> x <= z) by L;
monotonicity: (!x y. x <= y ==> f x <= f y) by L;
least_upper_bound:
(!X. ?s:A. (!x. x IN X ==> s <= x) /\
(!s'. (!x. x IN X ==> s' <= x) ==> s' <= s)) by L;
set Y_def: Y = {b | f b <= b};
Y_thm: !b. b IN Y <=> f b <= b by Y_def,IN_ELIM_THM,BETA_THM;
consider a such that
lub: (!x. x IN Y ==> a <= x) /\
(!a'. (!x. x IN Y ==> a' <= x) ==> a' <= a)
by least_upper_bound;
take a;
!b. b IN Y ==> f a <= b
proof
let b be A;
assume b_in_Y: b IN Y;
then L0: f b <= b by Y_thm;
a <= b by b_in_Y, lub;
so f a <= f b by monotonicity;
hence f a <= b by L0, transitivity;
end;
so Part1: f(a) <= a by lub;
so f(f(a)) <= f(a) by monotonicity;
so f(a) IN Y by Y_thm;
so a <= f(a) by lub;
hence thesis by Part1, antisymmetry;
end`;;
(*** Get the theorem ***)
top_thm();;
(* ------------------------------------------------------------------------- *)
(* Back to normal. *)
(* ------------------------------------------------------------------------- *)
let parse_term = old_parse_term;;