1/* Untrusted predicates called from the kernel:
+ 2 * next_object next object to check
+ 3 * callback_proved proof completed
+ 4 * next_tactic next tactic to use
+ 5 * update_certificate get new certificate after tactic application
+ 6 * end_of_proof is the certificate/proof empty?
+ 7 * ppterm for pretty-printing messages
+ 8 * deftac tactic definition
+ 9 */
+ 10
+ 11/* Predicates exported from the trusted library:
+ 12 * append
+ 13 * fold2_append
+ 14 * put_binds
+ 15 */
+ 16
+ 17/* Predicates exported from the kernel:
+ 18 * proves
+ 19 * check
+ 20 */
+ 21
+ 22{ /***** Trusted code base *******/
+ 23
+ 24/***** Trusted library functions *****/
+ 25
+ 26/* The names with ' at the end are trusted; the ones without are
+ 27 exported and therefore untrusted. */
+ 28local append', fold2_append', put_binds'.
+ 29
+ 30append' [] L L.
+ 31append' [ X | XS ] L [ X | RES ] :- append' XS L RES.
+ 32append A B C :- append' A B C.
+ 33
+ 34fold2_append' [] [] _ [].
+ 35fold2_append' [ X | XS ] [ Y | YS ] F OUTS :-
+ 36 F X Y OUT, fold2_append' XS YS F OUTS2, append' OUT OUTS2 OUTS.
+ 37fold2_append A B C D :- fold2_append' A B C D.
+ 38
+ 39% put_binds : list 'b -> 'a -> 'c -> list (bounded 'b) -> o
+ 40% put_binds [ f1,...,fn ] x t [ bind t x \ f1,...,bind t x fn ]
+ 41% binding all the xs that occur in f1,...,fn
+ 42put_binds' [] _ _ [].
+ 43put_binds' [ YX | YSX ] X A [ bind A Y | YYS ] :-
+ 44 YX = Y X, put_binds' YSX X A YYS.
+ 45put_binds A B C D :- put_binds' A B C D.
+ 46
+ 47/***** The HOL kernel *****/
+ 48
+ 49local thm, provable, def0, term, typ, typ', loop, prove, check1,
+ 50 check1def, check1thm, check1axm, check1nbt,
+ 51 reterm, not_defined, check_hyps.
+ 52
+ 53proves T TY :- provable T TY.
+ 54
+ 55typ T :- !. % this line temporarily drops checking of well-formedness for types
+ 56 % to avoid too much slow down. It is ultimately due to re-typing
+ 57 % terms that should be recognized as already well typed.
+ 58typ T :- var T, !, declare_constraint (typ T) [ T ].
+ 59typ T :- typ' T.
+ 60typ' prop.
+ 61typ' (univ ## A ## B) :- typ A, typ B.
+ 62typ' (A --> B) :- typ A, typ B.
+ 63typ' (disj_union ## A ## B) :- typ A, typ B.
+ 64
+ 65pred term i:A, o:B.
+ 66term (lam A F) (A --> B) :- typ A, pi x\ term x A => term (F x) B.
+ 67term (F # T) B :- term F (A --> B), term T A.
+ 68term (eq ## A) (A --> A --> prop) :- typ A.
+ 69term (uvar as T) TY :- declare_constraint (term T TY) T.
+ 70
+ 71/* like term, but on terms that are already known to be well-typed */
+ 72pred reterm i:A, o:B.
+ 73reterm (lam A F) (A --> B) :- pi x\ reterm x A => reterm (F x) B.
+ 74reterm (F # T) B :- reterm F (A --> B).
+ 75reterm (eq ## A) (A --> A --> prop).
+ 76reterm (uvar as T) TY :- declare_constraint (reterm T TY) T.
+ 77
+ 78constraint term reterm { /* No propagation rules for now */}
+ 79
+ 80% thm : bounded tactic -> bounded sequent -> list (bounded sequent) -> o
+ 81thm C (seq Gamma G) _ :- debug, print Gamma "|- " G " := " C, fail.
+ 82
+ 83/* << HACKS FOR DEBUGGING */
+ 84thm daemon (seq Gamma F) [].
+ 85/* >> HACKS FOR DEBUGGING */
+ 86
+ 87thm r (seq Gamma (eq ## _ # X # X)) [].
+ 88thm (t Y) (seq Gamma (eq ## A # X # Z))
+ 89 [ seq Gamma (eq ## A # X # Y), seq Gamma (eq ## A # Y # Z) ] :- term Y A.
+ 90thm (m P) (seq Gamma Q) [ seq Gamma (eq ## prop # P # Q), seq Gamma P ] :- term P prop.
+ 91thm b (seq Gamma (eq ## _ # ((lam _ F) # X) # (F X))) [].
+ 92thm c (seq Gamma (eq ## B # (F # X) # (G # Y)))
+ 93 [ seq Gamma (eq ## (A --> B) # F # G) , seq Gamma (eq ## A # X # Y) ] :- reterm X A, reterm Y A.
+ 94thm k (seq Gamma (eq ## (A --> B) # (lam A S) # (lam A T)))
+ 95 [ bind A x \ seq Gamma (eq ## B # (S x) # (T x)) ].
+ 96thm s (seq Gamma (eq ## prop # P # Q)) [ seq (P :: Gamma) Q, seq (Q :: Gamma) P ].
+ 97thm (h IGN) (seq Gamma P) [] :- append' IGN [ P | Gamma2 ] Gamma.
+ 98
+ 99thm d (seq Gamma (eq ## _ # C # A)) [] :- def0 C A.
+ 100thm (th NAME) (seq _ G) [] :- provable NAME G.
+ 101
+ 102thm (thenll TAC1 TACN) SEQ SEQS :-
+ 103 thm TAC1 SEQ NEW,
+ 104 deftacl TACN NEW TACL,
+ 105 fold2_append' TACL NEW thm SEQS.
+ 106
+ 107/*debprint _ (then _ _) :- !.
+ 108debprint _ (thenl _ _) :- !.
+ 109debprint O T :- print O T.*/
+ 110
+ 111thm TAC SEQ SEQS :-
+ 112 deftac TAC SEQ XTAC,
+ 113 /*debprint "<<" TAC,
+ 114 (*/ thm XTAC SEQ SEQS /*, debprint ">>" TAC
+ 115 ; debprint "XX" TAC, fail)*/.
+ 116
+ 117thm (! TAC) SEQ SEQS :-
+ 118 thm TAC SEQ SEQS,
+ 119 !.
+ 120
+ 121thm id SEQ [ SEQ ].
+ 122
+ 123thm (wl Gamma1) (seq Gamma F) [ seq WGamma F ] :-
+ 124 append' Gamma1 [ P | Gamma2 ] Gamma,
+ 125 append' Gamma1 Gamma2 WGamma.
+ 126
+ 127thm (bind A TAC) (bind A SEQ) NEWL :-
+ 128 pi x \ term x A => reterm x A => thm (TAC x) (SEQ x) (NEW x), put_binds' (NEW x) x A NEWL.
+ 129
+ 130thm ww (bind A x \ SEQ) [ SEQ ].
+ 131
+ 132/* debuggin only, remove it */
+ 133%thm A B C :- print "FAILED " (thm A B C), fail.
+ 134
+ 135% loop : list (bounded sequent) -> certificate -> o
+ 136%loop SEQS TACS :- print "LOOP" (loop SEQS TACS), fail.
+ 137loop [] CERTIFICATE :- end_of_proof CERTIFICATE.
+ 138loop [ SEQ | OLD ] CERTIFICATE :-
+ 139 next_tactic [ SEQ | OLD ] CERTIFICATE ITAC,
+ 140 thm ITAC SEQ NEW,
+ 141 append' NEW OLD SEQS,
+ 142 update_certificate CERTIFICATE ITAC NEW NEW_CERTIFICATE,
+ 143 loop SEQS NEW_CERTIFICATE.
+ 144
+ 145prove G TACS :-
+ 146 (term G prop, ! ; ppterm PG G, print "Bad statement:" PG, fail),
+ 147% (TACS = (false,_), ! ;
+ 148 loop [ seq [] G ] TACS
+ 149. % ).
+ 150
+ 151not_defined P NAME :-
+ 152 not (P NAME _) ; print "Error:" NAME already defined, fail.
+ 153
+ 154check_hyps HS (typ' TYPE) :-
+ 155 (not (typ' TYPE) ; print "Error:" TYPE already defined, fail), print HS new TYPE.
+ 156check_hyps HS (def0 NAME DEF) :- ppterm PDEF DEF, print HS NAME "=" PDEF.
+ 157check_hyps HS (term NAME TYPE) :-
+ 158 not_defined term NAME, ppterm PTYPE TYPE, print HS NAME ":" PTYPE.
+ 159check_hyps HS (reterm _ _).
+ 160check_hyps HS (provable NAME TYPE) :-
+ 161 not_defined provable NAME, ppterm PTYPE TYPE, print HS NAME ":" PTYPE.
+ 162check_hyps HS (H1,H2) :- check_hyps HS H1, check_hyps HS H2.
+ 163check_hyps HS (pi H) :- pi x \ typ' x => check_hyps [x | HS] (H x).
+ 164check_hyps HS (_ => H2) :- check_hyps HS H2.
+ 165
+ 166/* check1 I O
+ 167 checks the declaration I
+ 168 returns the new assumption O */
+ 169check1 (theorem NAME GOALTACTICS) HYPS :- check1thm NAME GOALTACTICS HYPS, !.
+ 170check1 (axiom NAME ST) HYPS :- check1axm NAME ST HYPS, !.
+ 171check1 (new_basic_type TYPE REP ABS REPABS ABSREP PREPH P_TACTICS) HYPS :- check1nbt TYPE REP ABS REPABS ABSREP PREPH P_TACTICS true HYPS, !.
+ 172check1 (def NAME TYPDEF) HYPS :- check1def NAME TYPDEF true HYPS, !.
+ 173check1 (decl NAME TYP) HYPS :- check1decl NAME TYP true HYPS, !.
+ 174
+ 175check1def NAME (pi I) HYPSUCHTHAT (pi HYPS) :-
+ 176 pi x \ typ' x => check1def (NAME ## x) (I x) (HYPSUCHTHAT, typ x) (HYPS x).
+ 177check1def NAME (TYP,DEF) HYPSUCHTHAT HYPS :-
+ 178 typ TYP, term DEF TYP,
+ 179 HYPS = ((HYPSUCHTHAT => term NAME TYP), reterm NAME TYP, def0 NAME DEF).
+ 180
+ 181check1decl NAME (pi I) HYPSUCHTHAT (pi HYPS) :-
+ 182 pi x \ typ' x => check1decl (NAME ## x) (I x) (HYPSUCHTHAT, typ x) (HYPS x).
+ 183check1decl NAME TYP HYPSUCHTHAT HYPS :-
+ 184 typ TYP, HYPS = ((HYPSUCHTHAT => term NAME TYP), reterm NAME TYP).
+ 185
+ 186check1thm NAME (pi I) (pi HYPS) :-
+ 187 pi x \ typ' x => check1thm NAME (I x) (HYPS x).
+ 188check1thm NAME (GOAL,TACTICS) (provable NAME GOAL) :-
+ 189 prove GOAL TACTICS,
+ 190 callback_proved NAME GOAL TACTICS.
+ 191
+ 192check1axm NAME (pi I) (pi HYPS) :- !,
+ 193 pi x \ typ' x => check1axm NAME (I x) (HYPS x).
+ 194check1axm NAME GOAL (provable NAME GOAL) :-
+ 195 term GOAL prop, ! ; ppterm PGOAL GOAL, print "Bad statement:" PGOAL, fail.
+ 196
+ 197check1nbt TYPE REP ABS REPABS ABSREP PREPH (pi P_TACTICS) HYPSUCHTHAT (pi HYPS) :-
+ 198 pi x \ typ' x => check1nbt (TYPE ## x) (REP ## x) (ABS ## x) REPABS ABSREP PREPH (P_TACTICS x) (HYPSUCHTHAT, typ x) (HYPS x).
+ 199check1nbt TYPE REP ABS REPABS ABSREP PREPH (P,TACTICS) HYPSUCHTHAT HYPS :-
+ 200 term P (X --> prop),
+ 201 prove (exists ## _ # P ) TACTICS,
+ 202 callback_proved existence_condition (exists ## _ # P) TACTICS,
+ 203 REPTYP = (TYPE --> X),
+ 204 ABSTYP = (X --> TYPE),
+ 205 ABSREPTYP = (forall ## TYPE # lam TYPE x \ eq ## TYPE # (ABS # (REP # x)) # x),
+ 206 REPABSTYP = (forall ## X # lam X x \ impl # (P # x) # (eq ## X # (REP # (ABS # x)) # x)),
+ 207 PREPHTYP = (forall ## TYPE # lam TYPE x \ (P # (REP # x))),
+ 208 !,
+ 209 HYPS =
+ 210 ( (HYPSUCHTHAT => typ' TYPE)
+ 211 , (HYPSUCHTHAT => term REP REPTYP), reterm REP REPTYP
+ 212 , (HYPSUCHTHAT => term ABS ABSTYP), reterm ABS ABSTYP
+ 213 , provable ABSREP ABSREPTYP
+ 214 , provable REPABS REPABSTYP, provable PREPH PREPHTYP).
+ 215
+ 216check WHAT :-
+ 217 next_object WHAT C CONT,
+ 218 (C = stop, !, K = true ; check1 C H , check_hyps [] H, print_constraints, K = (H => check CONT)),
+ 219 !, K.
+ 220
+ 221}
+ 222
+ 223/************ parsing and pretty-printing ********/
+ 224% ppterm/parseterm
+ 225%ppterm X Y :- ppp X Y. parseterm X Y :- ppp X Y.
+ 226%ppp X Y :- var X, var Y, !, X = Y.
+ 227%ppp X (F # G) :- var X, (var F ; var G), !, X = (F # G).
+ 228%ppp X (F # G # H) :- var X, (var F ; var G ; var H), !,
+ 229% X = (F # G # H).
+ 230
+ 231mode (ppp o i) xas ppterm, (ppp i o) xas parseterm.
+ 232
+ 233ppp (! F2) (forall ## _ # lam _ F1) :- !, pi x \ ppp (F2 x) (F1 x).
+ 234ppp (! TY F2) (forall ## TY # lam TY F1) :- !, pi x \ ppp (F2 x) (F1 x).
+ 235ppp (? F2) (exists ## _ # lam _ F1) :- !, pi x \ ppp (F2 x) (F1 x).
+ 236ppp (? TY F2) (exists ## TY # lam TY F1) :- !, pi x \ ppp (F2 x) (F1 x).
+ 237ppp (F2 <=> G2) (eq ## prop # F1 # G1) :- !, ppp F2 F1, ppp G2 G1.
+ 238ppp (F2 = G2) (eq ## _ # F1 # G1) :- !, ppp F2 F1, ppp G2 G1.
+ 239ppp (F2 && G2) (and # F1 # G1) :- !, ppp F2 F1, ppp G2 G1.
+ 240ppp (F2 || G2) (or # F1 # G1) :- !, ppp F2 F1, ppp G2 G1.
+ 241ppp (F2 ==> G2) (impl # F1 # G1) :- !, ppp F2 F1, ppp G2 G1.
+ 242ppp (X2 #in S2) (in ## _ # X1 # S1) :- !, ppp X2 X1, ppp S2 S1.
+ 243ppp (U2 <<= V2) (subseteq ## _ # U1 # V1) :- !, ppp U2 U1, ppp V2 V1.
+ 244ppp (F2 + G2) (plus # F1 # G1) :- !, ppp F2 F1, ppp G2 G1.
+ 245ppp (F2 # G2) (F1 # G1) :- !, ppp F2 F1, ppp G2 G1.
+ 246ppp (lam A F2) (lam A F1) :- !, pi x \ ppp (F2 x) (F1 x).
+ 247ppp A A.
+ 248
+ 249/* safe_list_map that unifies the two lists if they are both flexible
+ 250 probably only useful for parsing/pretty-printing */
+ 251safe_list_map L1 _ L2 :- var L1, var L2, !, L1 = L2.
+ 252safe_list_map L1 F L2 :- list_map L1 F L2.
+ 253
+ 254% pptac(ppterm)/parsetac(parseterm)
+ 255% pptac X Y :- ppptac X Y. parsetac X Y :- ppptac X Y.
+ 256
+ 257mode (ppptac i o) xas parsetac(ppp -> parseterm),
+ 258 (ppptac o i) xas pptac(ppp -> ppterm).
+ 259
+ 260ppptac daemon daemon.
+ 261ppptac r r.
+ 262ppptac (t Y) (t PY) :- ppp Y PY.
+ 263ppptac (m Y) (m PY) :- ppp Y PY.
+ 264ppptac b b.
+ 265ppptac c c.
+ 266ppptac k k.
+ 267ppptac s s.
+ 268ppptac (h Gamma) (h PGamma) :- safe_list_map Gamma ppp PGamma.
+ 269ppptac d d.
+ 270ppptac (th NAME) (th NAME).
+ 271ppptac (thenll TAC1 TACN) (thenll PTAC1 PTACN) :-
+ 272 ppptac TAC1 PTAC1, ppptac TACN PTACN.
+ 273ppptac (! TAC) (! PTAC) :- ppptac TAC PTAC.
+ 274ppptac id id.
+ 275ppptac (wl Gamma) (wl PGamma) :- safe_list_map Gamma ppp PGamma.
+ 276ppptac (bind A TAC) (bind PA PTAC) :-
+ 277 ppp A PA, pi x \ ppptac (TAC x) (PTAC x).
+ 278ppptac ww ww.
+ 279
+ 280/************ interactive and non interactive loops ********/
+ 281
+ 282ppptac interactive interactive.
+ 283
+ 284parse_obj (theorem NAME PSTTAC) [theorem NAME STTAC] :-
+ 285 parse_thm NAME PSTTAC STTAC.
+ 286parse_obj (axiom NAME PTYP) [axiom NAME TYP] :- parse_axiom PTYP TYP.
+ 287parse_obj (new_basic_type TYPE REP ABS REPABS ABSREP PREP PP_TACTICS)
+ 288 [new_basic_type TYPE REP ABS REPABS ABSREP PREP P_TACTICS] :- parse_nbt PP_TACTICS P_TACTICS.
+ 289parse_obj (def NAME PTYBO) [def NAME TYBO] :- parse_def PTYBO TYBO.
+ 290parse_obj (decl NAME TY) [decl NAME TY].
+ 291parse_obj (inductive_def PRED PREDF PREDF_MON PRED_I PRED_E0 PRED_E K) EXP :-
+ 292 inductive_def_pkg PRED PREDF PREDF_MON PRED_I PRED_E0 PRED_E K EXP.
+ 293parse_obj stop [stop].
+ 294
+ 295parse_def (pi I) (pi O) :- pi x \ parse_def (I x) (O x).
+ 296parse_def (TY,PB) (TY,B) :- parseterm PB B.
+ 297
+ 298parse_axiom (pi I) (pi O) :- !, pi x \ parse_axiom (I x) (O x).
+ 299parse_axiom PST ST :- parseterm PST ST.
+ 300
+ 301parse_thm NAME (pi I) (pi O) :- pi x \ parse_thm NAME (I x) (O x).
+ 302parse_thm _ (PST,TAC) (ST,(false,TAC)) :- !, parseterm PST ST.
+ 303parse_thm NAME PST (ST,(true,[_])) :-
+ 304 (not (proves NAME _) ; print "Error:" NAME already defined, fail),
+ 305 parseterm PST ST.
+ 306
+ 307parse_nbt (pi I) (pi O) :- !, pi x \ parse_nbt (I x) (O x).
+ 308parse_nbt (PP,TACTICS) (P,(false,TACTICS)) :- parseterm PP P.
+ 309parse_nbt PP (P,(true,[_])) :- parseterm PP P.
+ 310
+ 311next_object [ C | NEXT ] CT CONTNEXT :-
+ 312 parse_obj C [ CT | CONT ], append CONT NEXT CONTNEXT.
+ 313next_object [] C CONT :-
+ 314 print "Welcome to HOL extra-light",
+ 315 toplevel_loop [ C | CONT ].
+ 316next_object toplevel C CONT :- toplevel_loop [ C | CONT ].
+ 317
+ 318read_cmd H :-
+ 319 print "Enter a command or \"stop.\"",
+ 320 flush std_out, $readterm std_in H,
+ 321 !.
+ 322read_cmd H :- read_cmd H.
+ 323
+ 324toplevel_loop G :-
+ 325 read_cmd H,
+ 326 ( H = stop, !, G = [stop]
+ 327 ; parse_obj H PH, !, (append PH toplevel G ; print "error", toplevel_loop G)
+ 328 ; print "bad command", toplevel_loop G ).
+ 329
+ 330callback_proved _ _ (false,_).
+ 331callback_proved NAME G (true, [ TAC ]) :-
+ 332 canonical TAC CANONICALTAC,
+ 333 pptac PCANONICALTAC CANONICALTAC,
+ 334 ppterm PG G,
+ 335 print (theorem NAME (PG , [ PCANONICALTAC ] )).
+ 336
+ 337end_of_proof (true, []) :- print "proof completed".
+ 338end_of_proof (false, []).
+ 339
+ 340next_tactic0 [ SEQ | OLD ] (true, [ _ | _ ]) ITAC :-
+ 341 print,
+ 342 list_iter_rev [ SEQ | OLD ] print_sequent,
+ 343 read_in_context SEQ ITAC BACKTRACK,
+ 344 BACKTRACK.
+ 345next_tactic0 SEQS (true, CERT) ITAC :-
+ 346 print "error",
+ 347 next_tactic SEQS (true, CERT) ITAC.
+ 348next_tactic0 SEQS (true_then_false, (_,INT_TACS,_)) ITAC :-
+ 349 next_tactic0 SEQS (true, INT_TACS) ITAC.
+ 350next_tactic0 SEQS (false, [ interactive | _ ]) ITAC :-
+ 351 next_tactic0 SEQS (true, [ _ ]) ITAC.
+ 352next_tactic0 [ SEQ | OLD ] (false, [ TAC | _ ]) TAC.
+ 353next_tactic0 _ (false, _) ITAC :-
+ 354 print "aborted",
+ 355 halt.
+ 356
+ 357next_tactic SEQS CERT TAC :- next_tactic0 SEQS CERT PTAC, parsetac PTAC TAC.
+ 358
+ 359update_certificate (true, [ TAC | OTHER_TACS ]) ITAC NEW (true, TACS) :-
+ 360 mk_script ITAC NEW NEW_TACS TAC,
+ 361 append NEW_TACS OTHER_TACS TACS.
+ 362update_certificate (false, [ interactive | NON_INTERACTIVE_TACS ]) ITAC NEW CERTIFICATE :-
+ 363 update_certificate (true_then_false, (SCRIPT, [ SCRIPT ], NON_INTERACTIVE_TACS)) ITAC NEW CERTIFICATE.
+ 364update_certificate (true_then_false, (SCRIPT,[ TAC | OTHER_TACS ],NON_INTERACTIVE_TACS)) ITAC NEW CERTIFICATE :- !,
+ 365 mk_script ITAC NEW NEW_INTERACTIVE_TACS TAC,
+ 366 append NEW_INTERACTIVE_TACS OTHER_TACS INTERACTIVE_TACS,
+ 367 ( INTERACTIVE_TACS = [ _ | _ ], !,
+ 368 CERTIFICATE =
+ 369 (true_then_false, (SCRIPT,INTERACTIVE_TACS,NON_INTERACTIVE_TACS))
+ 370 ; CERTIFICATE = (false, NON_INTERACTIVE_TACS),
+ 371 print "INTERACTIVE SUBPROOF COMPLETED",
+ 372 canonical SCRIPT CSCRIPT,
+ 373 pptac PSCRIPT CSCRIPT,
+ 374 print PSCRIPT).
+ 375update_certificate (false, [ _ | OTHER_TACS ]) _ _ (false, OTHER_TACS).
+ 376
+ 377mk_script (bind A T) NEW NEW_TACS (bind A T2) :- !,
+ 378 pi x \
+ 379 put_binds (NEW2 x) x A NEW,
+ 380 mk_script (T x) (NEW2 x) (NEWT x) (T2 x),
+ 381 put_binds (NEWT x) x A NEW_TACS.
+ 382mk_script ITAC NEW NEW_TACS (thenl ITAC NEW_TACS) :-
+ 383 mk_list_of_bounded_fresh NEW NEW_TACS.
+ 384
+ 385read_in_context (bind A K) (bind A TAC) BACKTRACK :-
+ 386 pi x \ /* term x A => reterm # x A => */ read_in_context (K x) (TAC x) BACKTRACK.
+ 387read_in_context (seq A B) TAC BACKTRACK :-
+ 388 flush std_out, $readterm std_in TAC,
+ 389 (TAC = backtrack, !, BACKTRACK = (!, fail) ; BACKTRACK = true).
+ 390
+ 391print_sequent (seq Gamma G) :-
+ 392 print,
+ 393 list_iter_rev Gamma (x \ sigma PX \ ppterm PX x, print PX),
+ 394 print "|------------------",
+ 395 ppterm PG G, print PG.
+ 396print_sequent (bind A F) :- pi x \ print_sequent (F x).
+ 397
+ 398/* turns thenl into then */
+ 399canonical (bind A T1) (bind A T2) :- !,
+ 400 pi x \ canonical (T1 x) (T2 x).
+ 401canonical (thenl T L) OTAC :- !,
+ 402 list_map L canonical L2,
+ 403 (mk_constant_list L2 S L2, !,
+ 404 (S = [], !, OTAC = T ; OTAC = then T S)
+ 405 ; OTAC = thenl T L2).
+ 406canonical T T.
+ 407
+ 408/************ inductive_def package ********/
+ 409parse_inductive_def_spec (pi F) (pi PF) :- !,
+ 410 pi A \ parse_inductive_def_spec (F A) (PF A).
+ 411parse_inductive_def_spec (param TY F) (param PTY PF) :- !,
+ 412 ppp TY PTY, pi x \ parse_inductive_def_spec (F x) (PF x).
+ 413parse_inductive_def_spec L PL :-
+ 414 (pi p \ list_map (L p)
+ 415 (x \ px \ sigma A \ sigma B \ sigma PB \ x = (A, B), parseterm B PB, px = (A, PB))
+ 416 (PL p)).
+ 417
+ 418build_quantified_predicate (pi I) (pi O) :- !,
+ 419 pi A \ build_quantified_predicate (I A) (O A).
+ 420build_quantified_predicate (param TY I) (TY --> TYP, lam TY BO) :- !,
+ 421 pi x \ build_quantified_predicate (I x) (TYP, BO x).
+ 422build_quantified_predicate L (_, lam _ p \ lam _ x \ P p x) :-
+ 423 pi p \ pi x \ build_predicate (L p) p x (P p x).
+ 424
+ 425build_predicate [ (_,K) ] P X R :- !,
+ 426 process_constructor K P X R.
+ 427build_predicate [ (_,K) | REST ] P X (or # Q # R) :-
+ 428 process_constructor K P X Q,
+ 429 build_predicate REST P X R.
+ 430
+ 431process_constructor (forall ## TY # lam TY Q) P X (exists ## TY # lam TY R) :-
+ 432 pi y \ process_constructor (Q y) P X (R y).
+ 433process_constructor (impl # H # K) P X (and # H # R) :-
+ 434 process_constructor K P X R.
+ 435process_constructor (P # T) P X (eq ## _ # X # T).
+ 436
+ 437prove_monotonicity_thm (pi F) PREDF APREDF (pi THM) :- !,
+ 438 pi A \ prove_monotonicity_thm (F A) PREDF (APREDF ## A) (THM A).
+ 439prove_monotonicity_thm (param TY F) PREDF APREDF (forall ## TY # lam TY STM, PROOF) :- !,
+ 440 pi x \ prove_monotonicity_thm (F x) PREDF (APREDF # x) (STM x, PROOF).
+ 441prove_monotonicity_thm _ PREDF APREDF THM :-
+ 442 THM =
+ 443 (monotone ## _ # APREDF,
+ 444 [ then inv (bind* (then (conv (depth_tac (dd [PREDF]))) auto_monotone)) ]).
+ 445
+ 446state_fixpoint_def (pi F) PREDF (pi DEF) :- !,
+ 447 pi A \ state_fixpoint_def (F A) (PREDF ## A) (DEF A).
+ 448state_fixpoint_def (param TY F) PREDF (_, lam TY BO) :- !,
+ 449 pi x \ state_fixpoint_def (F x) (PREDF # x) (_, BO x).
+ 450state_fixpoint_def _ PREDF (_, fixpoint ## _ # PREDF).
+ 451
+ 452prove_fix_intro_thm (pi F) PREDF PRED PREDF_MONOTONE (pi THM) :- !,
+ 453 pi A \ prove_fix_intro_thm (F A) (PREDF ## A) (PRED ## A) PREDF_MONOTONE (THM A).
+ 454prove_fix_intro_thm (param TY F) PREDF PRED PREDF_MONOTONE (forall ## TY # lam TY STM, [ then forall_i (bind _ PROOF) ]) :- !,
+ 455 pi x \ prove_fix_intro_thm (F x) (PREDF # x) (PRED # x) PREDF_MONOTONE (STM x, [ PROOF x ]).
+ 456prove_fix_intro_thm _ PREDF PRED PREDF_MONOTONE THM :-
+ 457 THM =
+ 458 ((! x \ PREDF # PRED # x ==> PRED # x),
+ 459 [then forall_i
+ 460 (bind _ x13 \
+ 461 then (conv (rand_tac (rator_tac dd)))
+ 462 (then (conv (land_tac (rator_tac (rand_tac dd))))
+ 463 (then inv
+ 464 (then (cutth fixpoint_is_prefixpoint)
+ 465 (then (lforall PREDF)
+ 466 (thenl lapply [applyth PREDF_MONOTONE,
+ 467 then
+ 468 (g
+ 469 (subseteq ## _ '
+ 470 (PREDF # (fixpoint ## _ # PREDF)) '
+ 471 (fixpoint ## _ # PREDF)))
+ 472 (then (conv (depth_tac (dd [subseteq])))
+ 473 (then (conv (depth_tac (dd [in])))
+ 474 (then (conv (depth_tac (dd [in])))(itaut 4))))]))))))]).
+ 475
+ 476prove_fix_elim_thm (pi F) PREDF PRED OPRED (pi THM) :- !,
+ 477 pi A \ prove_fix_elim_thm (F A) (PREDF ## A) (PRED ## A) OPRED (THM A).
+ 478prove_fix_elim_thm (param TY F) PREDF PRED OPRED (forall ## TY # lam TY STM, [ then forall_i (bind _ PROOF) ]) :- !,
+ 479 pi x \ prove_fix_elim_thm (F x) (PREDF # x) (PRED # x) OPRED (STM x, [ PROOF x ]).
+ 480prove_fix_elim_thm _ PREDF PRED OPRED THM :-
+ 481 THM =
+ 482 ((! x13 \
+ 483 (! x14 \ PREDF # x13 # x14 ==> x13 # x14) ==>
+ 484 (! x14 \ PRED # x14 ==> x13 # x14)) ,
+ 485 [then forall_i
+ 486 (bind _ x23 \
+ 487 then (cutth fixpoint_subseteq_any_prefixpoint)
+ 488 (then (lforall PREDF)
+ 489 (then (lforall x23)
+ 490 (then (conv (depth_tac (dd [OPRED])))
+ 491 (then inv
+ 492 (bind _ x24 \
+ 493 then
+ 494 (g
+ 495 (impl # (subseteq ## _ # (PREDF # x23) # x23) '
+ 496 (subseteq ## _ # (fixpoint ## _ # PREDF) # x23)))
+ 497 (then (conv (depth_tac (dd [subseteq])))
+ 498 (then (conv (depth_tac (dd [subseteq])))
+ 499 (then (conv (depth_tac (dd [in])))
+ 500 (then (conv (depth_tac (dd [in])))
+ 501 (then (conv (depth_tac (dd [in])))
+ 502 (then (conv (depth_tac (dd [in])))
+ 503 (then
+ 504 (w
+ 505 (impl '
+ 506 (subseteq ## _ # (PREDF # x23) # x23) '
+ 507 (subseteq ## _ '
+ 508 (fixpoint ## _ # PREDF) # x23)))
+ 509 (then inv
+ 510 (thenl lapply_last [h,
+ 511 then (lforall_last x24)
+ 512 (then lapply_last h)])))))))))))))))]).
+ 513
+ 514prove_intro_thms (pi F) PRED PRED_I INTROTHMS :- !,
+ 515 pi A \
+ 516 prove_intro_thms (F A) (PRED ## A) PRED_I (OUT A),
+ 517 list_map (OUT A)
+ 518 (i \ o \ sigma Y \ i = (theorem NAME (P A)), o = theorem NAME (pi P))
+ 519 INTROTHMS.
+ 520prove_intro_thms (param TY F) PRED PRED_I INTROTHMS :- !,
+ 521 pi x \
+ 522 prove_intro_thms (F x) (PRED # x) PRED_I (OUT x),
+ 523 list_map (OUT x)
+ 524 (i \ o \ sigma Y \
+ 525 i = (theorem NAME (STM x, [ PROOF x ])),
+ 526 o = theorem NAME (forall ## TY # lam TY STM, [ then forall_i (bind TY PROOF) ]))
+ 527 INTROTHMS.
+ 528prove_intro_thms L PRED PRED_I INTROTHMS :-
+ 529 list_map (L PRED) (mk_intro_thm PRED_I) INTROTHMS.
+ 530
+ 531mk_intro_thm PRED_I (NAME,ST)
+ 532 (theorem NAME (ST,
+ 533 [ daemon /*(then inv (bind* (then (applyth PRED_I) (then (conv dd) (itauteq 6)))))*/ /* TOO MANY GOALS DELAYED ON typ (?): USE daemon INSTEAD */ ])).
+ 534
+ 535inductive_def_pkg PRED PREDF PREDF_MONOTONE PRED_I PRED_E0 PRED_E L OUT :-
+ 536 parse_inductive_def_spec L PL,
+ 537 build_quantified_predicate PL F,
+ 538 prove_monotonicity_thm PL PREDF PREDF MONTHM,
+ 539 state_fixpoint_def PL PREDF FIXDEF,
+ 540 prove_fix_intro_thm PL PREDF PRED PREDF_MONOTONE INTROTHM,
+ 541 prove_intro_thms PL PRED PRED_I INTROTHMS,
+ 542 prove_fix_elim_thm PL PREDF PRED PRED ELIMTHM,
+ 543 OUT1 =
+ 544 [ def PREDF F
+ 545 , theorem PREDF_MONOTONE MONTHM
+ 546 , def PRED FIXDEF
+ 547 , theorem PRED_I INTROTHM
+ 548 , theorem PRED_E0 ELIMTHM ],
+ 549 append OUT1 INTROTHMS OUT.
+ 550
+ 551/************ library of basic data types ********/
+ 552mk_bounded_fresh (bind _ F) (bind _ G) :- !, pi x\ mk_bounded_fresh (F x) (G x).
+ 553mk_bounded_fresh _ X.
+ 554
+ 555mk_list_of_bounded_fresh [] [].
+ 556mk_list_of_bounded_fresh [S|L] [X|R] :-
+ 557 mk_bounded_fresh S X, mk_list_of_bounded_fresh L R.
+ 558
+ 559/* list functions */
+ 560
+ 561list_map [] _ [].
+ 562list_map [X|XS] F [Y|YS] :- F X Y, list_map XS F YS.
+ 563
+ 564list_iter_rev [] _.
+ 565list_iter_rev [X|XS] F :- list_iter_rev XS F, F X.
+ 566
+ 567mem [ X | _ ] X, !.
+ 568mem [ _ | XS ] X :- mem XS X.
+ 569
+ 570mk_constant_list [] _ [].
+ 571mk_constant_list [_|L] X [X|R] :- mk_constant_list L X R.
+ 572
+ 573bang P :- P, !.
+ 574
+ 575/********** tacticals ********/
+ 576
+ 577% BUG in runtime.ml if the sigma is uncommented out. It does not matter btw.
+ 578/*sigma ff \*/ deftac fail SEQ ff.
+ 579
+ 580ppptac (constant_tacl TACL) (constant_tacl PTACL) :-
+ 581 list_map TACL ppptac PTACL.
+ 582deftacl (constant_tacl TACL) SEQS TACL.
+ 583
+ 584ppptac (thenl TAC TACL) (thenl PTAC PTACL) :-
+ 585 ppptac TAC PTAC, list_map TACL ppptac PTACL.
+ 586deftac (thenl TAC TACL) SEQ XTAC :-
+ 587 XTAC = thenll TAC (constant_tacl TACL).
+ 588
+ 589ppptac (all_equals_list TAC) (all_equals_list PTAC) :- ppptac TAC PTAC.
+ 590deftacl (all_equals_list TAC2) SEQS TACL :-
+ 591 mk_constant_list SEQS TAC2 TACL.
+ 592
+ 593ppptac (then TAC1 TAC2) (then PTAC1 PTAC2) :-
+ 594 ppptac TAC1 PTAC1, ppptac TAC2 PTAC2.
+ 595deftac (then TAC1 TAC2) SEQ XTAC :-
+ 596 XTAC = thenll TAC1 (all_equals_list TAC2).
+ 597
+ 598ppptac (then! TAC1 TAC2) (then! PTAC1 PTAC2) :-
+ 599 ppptac TAC1 PTAC1, ppptac TAC2 PTAC2.
+ 600deftac (then! TAC1 TAC2) _ (then (! TAC1) TAC2).
+ 601
+ 602ppptac (orelse TAC1 TAC2) (orelse PTAC1 PTAC2) :-
+ 603 ppptac TAC1 PTAC1, ppptac TAC2 PTAC2.
+ 604deftac (orelse TAC1 TAC2) SEQ XTAC :-
+ 605 XTAC = TAC1 ; XTAC = TAC2.
+ 606
+ 607ppptac (orelse! TAC1 TAC2) (orelse! PTAC1 PTAC2) :-
+ 608 ppptac TAC1 PTAC1, ppptac TAC2 PTAC2.
+ 609deftac (orelse! TAC1 TAC2) _ (orelse (! TAC1) TAC2).
+ 610
+ 611ppptac (bind* TAC) (bind* PTAC) :- ppptac TAC PTAC.
+ 612deftac (bind* TAC) SEQ (orelse! (bind _ x \ bind* TAC) TAC).
+ 613
+ 614ppptac (repeat TAC) (repeat PTAC) :- ppptac TAC PTAC.
+ 615deftac (repeat TAC) SEQ XTAC :-
+ 616 ( XTAC = then TAC (repeat (bind* TAC))
+ 617 ; XTAC = id).
+ 618
+ 619ppptac (repeat! TAC) (repeat! PTAC) :- ppptac TAC PTAC.
+ 620deftac (repeat! TAC) SEQ (orelse! (then! TAC (repeat! (bind* TAC))) id).
+ 621
+ 622ppptac (pptac TAC) (pptac PTAC) :- ppptac TAC PTAC.
+ 623deftac (pptac TAC) SEQ TAC :-
+ 624 print "SEQ" SEQ ":=" TAC.
+ 625
+ 626ppptac (time TAC) (time PTAC) :- ppptac TAC PTAC.
+ 627deftac (time TAC) SEQ XTAC :-
+ 628 $gettimeofday B,
+ 629 XTAC = thenll TAC (time_after TAC B).
+ 630
+ 631ppptac (time_after TAC B) (time_after PTAC B) :- ppptac TAC PTAC.
+ 632deftacl (time_after TAC B) SEQS TACL :-
+ 633 $gettimeofday A,
+ 634 D is A - B,
+ 635 mk_constant_list SEQS id TACL,
+ 636 print "TIME SPENT " D "FOR" TAC.
+ 637
+ 638/* For debugging only (?) For capturing metavariables */
+ 639ppptac (inspect (seq Gamma F) TAC) (inspect (seq PGamma PF) PTAC) :-
+ 640 list_map SEQ ppp PSEQ, ppp F PF, ppptac TAC PTAC.
+ 641deftac (inspect SEQ TAC) SEQ TAC.
+ 642
+ 643/********** tactics ********/
+ 644
+ 645ppptac (w G) (w PG) :- ppp G PG.
+ 646deftac (w G) (seq Gamma _) (wl Gamma1) :-
+ 647 append Gamma1 [ G | _ ] Gamma.
+ 648
+ 649ppptac h h.
+ 650deftac h SEQ (h L).
+ 651
+ 652/*** eq ***/
+ 653
+ 654ppptac sym sym.
+ 655deftac sym (seq Gamma (eq ## T # L # R)) TAC :-
+ 656 TAC = thenl (m (eq ## T # R # R)) [ thenl c [ thenl c [ r , id ] , r ] , r ].
+ 657
+ 658ppptac eq_true_intro eq_true_intro.
+ 659deftac eq_true_intro (seq Gamma (eq ## prop # P # tt)) TAC :-
+ 660 TAC = thenl s [ th tt_intro, wl [] ].
+ 661
+ 662/*** true ***/
+ 663
+ 664/*** and ***/
+ 665
+ 666ppptac conj conj.
+ 667deftac conj (seq Gamma (and # P # Q)) TAC :-
+ 668 TAC =
+ 669 then
+ 670 (then (conv dd)
+ 671 (then k (bind _ x \
+ 672 thenl c
+ 673 [ thenl c [ r, eq_true_intro ] ,
+ 674 eq_true_intro ])))
+ 675 ww.
+ 676
+ 677/* Gamma "|-" q ---> Gamma "|-" and # p # q*/
+ 678ppptac (andr P) (andr PP) :- ppp P PP.
+ 679deftac (andr P) (seq Gamma Q) TAC :-
+ 680 TAC =
+ 681 (thenl (m ((lam _ f \ f # P # Q) # (lam _ x \ lam _ y \ y)))
+ 682 [ then
+ 683 %(repeat (conv (depth_tac b))) ROBUS VERSION LINE BELOW
+ 684 (then (conv (land_tac b)) (then (conv (land_tac (rator_tac b))) (conv (land_tac b))))
+ 685 r
+ 686 , thenl (conv (rator_tac id))
+ 687 [ then (thenl (t (lam _ f \ f # tt # tt)) [ id, r ])
+ 688 (thenl (m (and # P # Q)) [ dd , id ])
+ 689 , then (repeat (conv (depth_tac b))) (th tt_intro) ]]).
+ 690
+ 691/* (and # p # q) :: nil "|-" q */
+ 692ppptac andr andr.
+ 693deftac andr (seq Gamma Q) TAC :-
+ 694 mem Gamma (and # P # Q),
+ 695 TAC = then (andr P) h.
+ 696
+ 697/* Gamma "|-" p ---> Gamma "|-" and # p # q*/
+ 698ppptac (andl P) (andl PP) :- ppp P PP.
+ 699deftac (andl Q) (seq Gamma P) TAC :-
+ 700 TAC =
+ 701 (thenl (m ((lam _ f \ f # P # Q) # (lam _ x \ lam _ y \ x)))
+ 702 [ then
+ 703 %(repeat (conv (depth_tac b))) ROBUS VERSION LINE BELOW
+ 704 (then (conv (land_tac b)) (then (conv (land_tac (rator_tac b))) (conv (land_tac b))))
+ 705 r
+ 706 , thenl (conv (rator_tac id))
+ 707 [ then (thenl (t (lam _ f \ f # tt # tt)) [ id, r ])
+ 708 (thenl (m (and # P # Q)) [ dd , id ])
+ 709 , then (repeat (conv (depth_tac b))) (th tt_intro) ]]).
+ 710
+ 711/* (and # p # q) :: nil "|-" p */
+ 712ppptac andl andl.
+ 713deftac andl (seq Gamma P) TAC :-
+ 714 mem Gamma (and # P # Q),
+ 715 TAC = then (andl Q) h.
+ 716
+ 717
+ 718/*** forall ***/
+ 719
+ 720/* |- forall # F --> |- F # x */
+ 721ppptac forall_i forall_i.
+ 722deftac forall_i (seq Gamma (forall ## _ # lam _ G)) TAC :-
+ 723 TAC = then (conv dd) (then k (bind _ x \ eq_true_intro)).
+ 724
+ 725/* forall # F |- F # T */
+ 726ppptac forall_e forall_e.
+ 727deftac forall_e (seq Gamma GX) TAC :-
+ 728 mem Gamma (forall ## _ # (lam _ G)), GX = G X,
+ 729 TAC = thenl (m ((lam _ G) # X)) [ b, thenl (m ((lam _ z \ tt) # X))
+ 730 [ thenl c [ then sym (thenl (m (forall ## _ # lam _ G)) [dd,h ]), r ]
+ 731 , then (conv b) (th tt_intro) ] ].
+ 732
+ 733/* forall # F |- f --> F # a, forall # F |- f */
+ 734ppptac (lforall F A) (lforall PF PA) :- ppp F PF, ppp A PA.
+ 735deftac (lforall F A) (seq Gamma G) TAC :-
+ 736 TAC = thenl (m (impl # (F A) # G))
+ 737 [ thenl s [ then mp forall_e, then i h ] , then (w (forall ## _ # lam _ F)) i ].
+ 738
+ 739/* forall # F |- f --> F # a, forall # F |- f */
+ 740ppptac (lforall A) (lforall PA) :- ppp A PA.
+ 741deftac (lforall A) (seq Gamma G) (lforall F A) :-
+ 742 mem Gamma (forall ## _ # lam _ F).
+ 743
+ 744/* forall # F |- f --> F # a, forall # F |- f */
+ 745ppptac lforall lforall.
+ 746deftac lforall (seq Gamma G) (lforall A).
+ 747
+ 748/* forall # F |- f --> F # a, forall # F |- f */
+ 749ppptac (lforall_last A) (lforall_last PA) :- ppp A PA.
+ 750deftac (lforall_last A) (seq ((forall ## _ # lam _ F)::Gamma) G) (lforall F A).
+ 751
+ 752/*** false ***/
+ 753
+ 754/*** impl ***/
+ 755
+ 756/* |- p=>q --> p |- q */
+ 757ppptac i i.
+ 758deftac i (seq Gamma (impl # P # Q)) TAC :-
+ 759 TAC = then (conv dd) (thenl s [ andl, thenl conj [ h [], id ]]).
+ 760
+ 761/* p=>q |- q --> |- p */
+ 762ppptac (mp P) (mp PP) :- ppp P PP.
+ 763deftac (mp P) (seq Gamma Q) TAC :-
+ 764 TAC = then (andr P) (thenl (m P) [ then sym (thenl (m (impl # P # Q)) [ dd , h ]) , id ]).
+ 765
+ 766/* p=>q |- q --> |- p */
+ 767ppptac mp mp.
+ 768deftac mp (seq Gamma Q) (mp P) :-
+ 769 mem Gamma (impl # P # Q).
+ 770
+ 771/* |- q --> p |- q and |- p */
+ 772ppptac (cut P) (cut PP) :- ppp P PP.
+ 773deftac (cut P) (seq Gamma Q) TAC :-
+ 774 TAC = then (andr P) (thenl (m P) [then sym (thenl (m (impl # P # Q)) [then (conv (land_tac dd)) r, i] ) , id]).
+ 775
+ 776/* |-q --> p |- q where the theorem T proves p */
+ 777ppptac (cutth P) (cutth PP) :- ppp P PP.
+ 778deftac (cutth T) SEQ TAC :-
+ 779 proves T X,
+ 780 TAC = (thenl (cut X) [ id, th T ]).
+ 781
+ 782/* applies the theorem T */
+ 783ppptac (applyth P) (applyth PP) :- ppp P PP.
+ 784deftac (applyth T) SEQ (then (cutth T) apply_last).
+ 785
+ 786/* impl p q, Gamma |- f ---> /*impl q f*/ Gamma |- p , q, Gamma |- f */
+ 787ppptac (lapply P Q) (lapply PP PQ) :- ppp P PP, ppp Q PQ.
+ 788deftac (lapply P Q) (seq Gamma F) TAC :-
+ 789 TAC =
+ 790 thenl (m (impl # Q # F)) [ thenl s [ then (mp Q) (then (w (impl # Q # F)) (then (mp P) (w (impl # P # Q)))) , then i (h [A]) ] , then (w (impl # P # Q)) (then i id) ].
+ 791
+ 792/* impl p q, Gamma |- f ---> /*impl q f*/ Gamma |- p , q, Gamma |- f */
+ 793ppptac lapply lapply.
+ 794deftac lapply (seq Gamma F) (lapply P Q) :-
+ 795 mem Gamma (impl # P # Q).
+ 796
+ 797/* impl p q, Gamma |- f ---> /*impl q f*/ Gamma |- p , q, Gamma |- f */
+ 798ppptac lapply_last lapply_last.
+ 799deftac lapply_last (seq ((impl # P # Q)::Gamma) F) (lapply P Q).
+ 800
+ 801/* p |- f ---> p |- p ==> f */
+ 802ppptac (g P) (g PP) :- ppp P PP.
+ 803deftac (g P) (seq _ F) TAC :-
+ 804 TAC =
+ 805 (thenl (m (impl # P # F)) [thenl s [then mp h , then i h] , id ]).
+ 806
+ 807/*** not ***/
+ 808
+ 809/*** exists ***/
+ 810
+ 811/**** apply, i.e. forall + impl ****/
+ 812
+ 813ppptac (apply X) (apply PX) :- ppp X PX.
+ 814deftac (apply X) SEQ h :- var X, !.
+ 815deftac (apply X) SEQ h.
+ 816deftac (apply (impl # P # Q)) SEQ TAC :-
+ 817 TAC = thenl (lapply P Q) [ id, apply_last ].
+ 818deftac (apply (forall ## _ # lam _ G)) SEQ TAC :-
+ 819 TAC = then (lforall G X) apply_last.
+ 820
+ 821ppptac apply_last apply_last.
+ 822deftac apply_last (seq (H::Gamma) F) (apply H).
+ 823
+ 824ppptac apply apply.
+ 825deftac apply (seq Gamma F) (apply H) :-
+ 826 mem Gamma H.
+ 827
+ 828/********** conversion(als) ***********/
+ 829
+ 830strip_constant (I ## _) H :- !, strip_constant I H.
+ 831strip_constant H H.
+ 832
+ 833/* expands definitions, even if applied to arguments */
+ 834ppptac (dd L) (dd L).
+ 835deftac (dd L) (seq _ (eq ## _ # T # X)) d :- strip_constant T H, bang (mem L H).
+ 836deftac (dd L) (seq _ (eq ## _ # (D # T) # X))
+ 837 (thenl (t A) [thenl c [dd L , r], b]).
+ 838
+ 839ppptac dd dd.
+ 840deftac dd _ (dd L).
+ 841
+ 842ppptac beta_expand beta_expand.
+ 843deftac beta_expand (seq _ (eq ## _ # (lam _ x \ F x) # (lam _ x \ (lam _ F) # x))) TAC :-
+ 844 TAC = then k (bind _ x \ then sym b).
+ 845
+ 846/* folds a definition, even if applied to arguments */
+ 847/* BUG: it seems to fail with restriction errors in some cases */
+ 848ppptac f f.
+ 849deftac f SEQ (then sym dd).
+ 850
+ 851ppptac (rand_tac C) (rand_tac PC) :- ppptac C PC.
+ 852deftac (rand_tac C) SEQ TAC :-
+ 853 TAC = thenl c [ r , C ].
+ 854
+ 855ppptac (rator_tac C) (rator_tac PC) :- ppptac C PC.
+ 856deftac (rator_tac C) SEQ TAC :-
+ 857 TAC = thenl c [ C , r ].
+ 858
+ 859ppptac (abs_tac C) (abs_tac PC) :- ppptac C PC.
+ 860deftac (abs_tac C) SEQ TAC :-
+ 861 TAC = then k (bind A x \ C).
+ 862
+ 863ppptac (land_tac C) (land_tac PC) :- ppptac C PC.
+ 864deftac (land_tac C) SEQ TAC :-
+ 865 TAC = thenl c [ thenl c [ r, C ] , r ].
+ 866
+ 867ppptac (sub_tac C) (sub_tac PC) :- ppptac C PC.
+ 868deftac (sub_tac C) SEQ TAC :-
+ 869 TAC = orelse (rand_tac C) (orelse (rator_tac C) (abs_tac C)).
+ 870
+ 871ppptac (try TAC) (try PTAC) :- ppptac TAC PTAC.
+ 872deftac (try TAC) SEQ (orelse TAC id).
+ 873
+ 874ppptac (depth_tac C) (depth_tac PC) :- ppptac C PC.
+ 875deftac (depth_tac C) SEQ TAC :-
+ 876 TAC = then (try C) (sub_tac (depth_tac C)).
+ 877
+ 878ppptac (conv C) (conv PC) :- ppptac C PC.
+ 879deftac (conv C) (seq Gamma F) TAC :-
+ 880 TAC = thenl (m G) [ then sym C , id ].
+ 881
+ 882/********** Automation ***********/
+ 883/* TODO:
+ 884 1) our lforall gets rid of the hypothesis (bad) */
+ 885/* left tries to reduce the search space via focusing */
+ 886ppptac left left.
+ 887deftac left (seq Gamma _) TAC :-
+ 888 mem Gamma (not # F),
+ 889 TAC =
+ 890 (!
+ 891 (then (cutth not_e)
+ 892 (then (lforall_last F)
+ 893 (thenl lapply [ h, (w (not # F)) ])))).
+ 894deftac left (seq Gamma _) TAC :-
+ 895 /* A bit long because we want to beta-reduce the produced hypothesis.
+ 896 Maybe this should be automatized somewhere else. */
+ 897 mem Gamma (exists ## _ # F),
+ 898 TAC =
+ 899 (!
+ 900 (then (cutth exists_e)
+ 901 (then (lforall_last F)
+ 902 (thenl lapply [ h, then (w (exists ## _ # F)) (then apply_last (then forall_i (bind _ x \ then (try (conv (land_tac b))) i))) ])))).
+ 903deftac left (seq Gamma H) TAC :-
+ 904 mem Gamma (or # F # G),
+ 905 TAC =
+ 906 (!
+ 907 (then (cutth or_e)
+ 908 (then (lforall_last F)
+ 909 (then (lforall_last G)
+ 910 (then (lforall_last H)
+ 911 (thenl lapply [ h, then (w (or # F # G)) (then apply_last i)])))))).
+ 912deftac left (seq Gamma H) TAC :-
+ 913 mem Gamma (and # F # G),
+ 914 TAC =
+ 915 (!
+ 916 (then (cutth and_e)
+ 917 (then (lforall_last F)
+ 918 (then (lforall_last G)
+ 919 (then (lforall_last H)
+ 920 (thenl lapply [ h, then (w (and # F # G)) (then apply_last (then i i))])))))).
+ 921deftac left (seq Gamma H) TAC :-
+ 922 mem Gamma (eq ## TY # F # G),
+ 923 not (var TY), TY = prop,
+ 924 TAC =
+ 925 (then (g (eq ## TY # F # G))
+ 926 (then (conv (land_tac (then (applyth eq_to_impl) h)))
+ 927 (then i (w (eq ## TY # F # G))))).
+ 928
+ 929ppptac not_i not_i.
+ 930deftac not_i (seq _ (not # _)) (applyth not_i).
+ 931
+ 932ppptac inv inv.
+ 933deftac inv _ TAC :-
+ 934 TAC =
+ 935 (then!
+ 936 (repeat!
+ 937 (orelse! conj (orelse! forall_i (orelse! i (orelse! not_i s)))))
+ 938 (bind* (repeat! left))).
+ 939
+ 940ppptac (sync N) (sync N).
+ 941deftac (sync N) (seq _ tt) (th tt_intro).
+ 942deftac (sync N) (seq Gamma _) (then (applyth ff_elim) h) :-
+ 943 mem Gamma ff.
+ 944deftac (sync N) (seq _ (or # _ # _))
+ 945 (orelse (then (applyth orr) (itaut N)) (then (applyth orl) (itaut N))).
+ 946deftac (sync N) (seq _ (exists ## _ # _)) (then (applyth exists_i) (then (conv b) (itaut N2))) :-
+ 947 N2 is N - 2.
+ 948
+ 949ppptac (itaut N) (itaut N).
+ 950deftac (itaut N) SEQ fail :- N =< 0, !.
+ 951deftac (itaut N) SEQ TAC :-
+ 952 %print (itaut N) SEQ,
+ 953 N1 is N - 1,
+ 954 N2 is N - 2,
+ 955 TAC =
+ 956 (then! inv
+ 957 (bind*
+ 958 (orelse h
+ 959 (orelse (sync N)
+ 960 (orelse /* Hypothesis not moved to front */ (then lforall (itaut N2))
+ 961 (then lapply (itaut N1))))))).
+ 962
+ 963ppptac (itauteq N) (itauteq N).
+ 964deftac (itauteq N) _ (then (cutth eq_reflexive) (itaut N)).
+ 965
+ 966/********** inductive predicates package ********/
+ 967
+ 968ppptac monotone monotone.
+ 969deftac monotone (seq _ (impl # X # X)) (! (then i h)) :- !.
+ 970deftac monotone (seq [forall ## _ # lam _ x \ impl # (F # x) # (G # x)] (impl # (F # T) # (G # T))) (! apply) :- !.
+ 971deftac monotone (seq _ (impl # (and # _ # _) # _)) TAC :-
+ 972 TAC = then (applyth and_monotone) monotone.
+ 973deftac monotone (seq _ (impl # (or # _ # _) # _)) TAC :-
+ 974 TAC = then (applyth or_monotone) monotone.
+ 975deftac monotone (seq _ (impl # (impl # _ # _) # _)) TAC :-
+ 976 TAC = then (applyth impl_monotone) monotone.
+ 977deftac monotone (seq _ (impl # (not # _) # _)) TAC :-
+ 978 TAC = then (applyth not_monotone) monotone.
+ 979deftac monotone (seq _ (impl # (forall ## _ # lam _ _) # _)) TAC :-
+ 980 TAC =
+ 981 then (conv (land_tac (rand_tac beta_expand)))
+ 982 (then (conv (rand_tac (rand_tac beta_expand)))
+ 983 (then (applyth forall_monotone) (then forall_i (bind _ x \
+ 984 then (conv (depth_tac b)) (then (conv (depth_tac b)) monotone))))).
+ 985deftac monotone (seq _ (impl # (exists ## _ # lam _ _) # _)) TAC :-
+ 986 TAC =
+ 987 then (conv (land_tac (rand_tac beta_expand)))
+ 988 (then (conv (rand_tac (rand_tac beta_expand)))
+ 989 (then (applyth exists_monotone) (then forall_i (bind _ x \
+ 990 then (conv (depth_tac b)) (then (conv (depth_tac b)) monotone))))).
+ 991
+ 992/* expands "monotone # (lam _ f \ lam _ x \ X f x)" into
+ 993 "! x \ p # x ==> q # x |- X p y ==> X q y"
+ 994 and then calls the monotone tactic */
+ 995ppptac auto_monotone auto_monotone.
+ 996deftac auto_monotone _ TAC :-
+ 997 TAC =
+ 998 then (conv dd)
+ 999 (then forall_i (bind _ p \ (then forall_i (bind _ q \
+1000 then (conv (land_tac dd))
+1001 (then (conv (land_tac (depth_tac (dd [in]))))
+1002 (then (conv (land_tac (depth_tac (dd [in]))))
+1003 (then i
+1004 (then (conv dd)
+1005 (then forall_i (bind _ x \
+1006 (then (conv (land_tac dd))
+1007 (then (conv (rand_tac dd))
+1008 (then (conv (land_tac (rator_tac b)))
+1009 (then (conv (land_tac b))
+1010 (then (conv (rand_tac (rator_tac b)))
+1011 (then (conv (rand_tac b))
+1012 monotone)))))))))))))))).
+1013
+1014/********** the library ********/
+1015
+1016main :- the_library L, append L [stop] Lstop, check Lstop.
+1017
+1018go :- the_library L, check L.
+1019
+1020the_library L :-
+1021 L =
+1022 [ /******** Primivite operators hard-coded in the kernel ******/
+1023 % decl eq (pi A \ A --> A --> prop)
+1024
+1025 /********** Axiomatization of choice over types ********/
+1026 decl choose (pi A \ A)
+1027
+1028 /*********** Connectives and quantifiers ********/
+1029 , def tt (prop,((lam prop x \ x) = (lam prop x \ x)))
+1030 , def forall (pi A \ ((A --> prop) --> prop),
+1031 (lam (A --> prop) f \ f = (lam A g \ tt)))
+1032 , def ff (prop,(! x \ x))
+1033 , def and ((prop --> prop --> prop),
+1034 (lam _ x \ lam _ y \ (lam (prop --> prop --> prop) f \ f # x # y) = (lam _ f \ f # tt # tt)))
+1035 , def impl ((prop --> prop --> prop),(lam _ a \ lam _ b \ a && b <=> a))
+1036 , def exists (pi A \ ((A --> prop) --> prop),
+1037 (lam (A --> prop) f \ ! c \ (! a \ f # a ==> c) ==> c))
+1038 , def not ((prop --> prop),(lam _ x \ x ==> ff))
+1039 , def or ((prop --> prop --> prop),
+1040 (lam _ x \ lam _ y \ ! c \ (x ==> c) ==> (y ==> c) ==> c))
+1041 , theorem tt_intro (tt,[then (conv dd) (then k (bind _ x12 \ r))])
+1042 , theorem ff_elim ((! p \ ff ==> p),
+1043 [then forall_i (bind prop x3\ then (conv (land_tac dd)) (then i forall_e))])
+1044 , theorem sym ((! p \ ! q \ p = q ==> q = p),
+1045 [then forall_i
+1046 (bind prop x12 \
+1047 then forall_i
+1048 (bind prop x13 \
+1049 then i (then sym h)))])
+1050 , theorem not_e ((! p \ not # p ==> p ==> ff),
+1051 [then forall_i (bind prop x3 \ then (conv (land_tac dd)) (then i h))])
+1052 , theorem conj ((! p \ ! q \ p ==> q ==> p && q),
+1053 [then forall_i
+1054 (bind prop x12 \
+1055 then forall_i (bind prop x13 \ then i (then i (then conj h))))])
+1056 , theorem andl ((! p \ ! q \ p && q ==> p),
+1057 [then forall_i
+1058 (bind prop x12 \
+1059 then forall_i (bind prop x13 \ then i (then (andl x13) h)))])
+1060 , theorem andr ((! p \ ! q \ p && q ==> q),
+1061 [then forall_i
+1062 (bind prop x12 \
+1063 then forall_i (bind prop x13 \ then i (then (andr x12) h)))])
+1064 , theorem and_e ((! p \ ! q \ ! c \ p && q ==> (p ==> q ==> c) ==> c),
+1065 [then forall_i
+1066 (bind prop x12 \
+1067 then forall_i
+1068 (bind prop x13 \
+1069 then forall_i
+1070 (bind prop x14 \ then i (then i (thenl apply [andl, andr])))))])
+1071 , theorem not_i ((! p \ (p ==> ff) ==> not # p),
+1072 [then forall_i (bind prop x2 \ then i (then (conv dd) h))])
+1073 , theorem orl ((! p \ ! q \ p ==> p || q),
+1074 [then forall_i
+1075 (bind prop x12 \
+1076 then forall_i
+1077 (bind prop x13 \
+1078 then i
+1079 (then (conv dd)
+1080 (then forall_i (bind prop x14 \ then i (then i (then apply h)))))))])
+1081 , theorem orr ((! p \ ! q \ q ==> p || q),
+1082 [then forall_i
+1083 (bind prop x12 \
+1084 then forall_i
+1085 (bind prop x13 \
+1086 then i
+1087 (then (conv dd)
+1088 (then forall_i (bind prop x14 \ then i (then i (then apply h)))))))])
+1089 , theorem or_e ((! p \ ! q \ ! c \ p || q ==> (p ==> c) ==> (q ==> c) ==> c),
+1090 [then forall_i
+1091 (bind prop x12 \
+1092 then forall_i
+1093 (bind prop x13 \
+1094 then forall_i
+1095 (bind prop x14 \ then (conv (land_tac dd)) (then i forall_e))))])
+1096 , theorem exists_e (pi T \
+1097 (! f \ (exists ## T # f) ==> (! c \ (! x \ f # x ==> c) ==> c)),
+1098 [then forall_i (bind (T --> prop) x12 \ then (conv (land_tac dd)) (then i h))])
+1099 , theorem exists_i (pi T \ (! f \ ! w \ f # w ==> (exists ## T # f)),
+1100 [then forall_i
+1101 (bind (T --> prop) x12 \
+1102 then forall_i
+1103 (bind T x13 \
+1104 then i
+1105 (then (conv dd)
+1106 (then forall_i
+1107 (bind prop x14 \ then i (then (lforall x13) (then apply h)))))))])
+1108 , theorem eq_to_impl
+1109 ((! x13 \ ! x14 \ (x13 = x14) = ((x13 ==> x14) && (x14 ==> x13))),
+1110 [thenl inv [(bind prop x13 \ bind prop x14 \ then (conv (then sym h)) h),
+1111 (bind prop x13 \ bind prop x14 \ then (conv h) h),
+1112 (bind prop x13 \ bind prop x14 \ itaut 2),
+1113 (bind prop x13 \ bind prop x14 \ itaut 2)]])
+1114
+1115 /*********** Axiomatization of disjoint union ********/
+1116 , decl inj1_disj_union (pi A \pi B \ A --> disj_union ## A ## B)
+1117 , decl inj2_disj_union (pi A \ pi B \ B --> disj_union ## A ## B)
+1118 , decl case_disj_union (pi A \pi B \ pi C \ disj_union ## A ## B --> (A --> C) --> (B --> C) --> C)
+1119 , axiom case_disj_union_inj1 (pi A \ pi B \ pi C \ (! b \ ! (A --> C) e1 \ ! (B --> C) e2 \
+1120 case_disj_union ## A ## B ## C # (inj1_disj_union ## A ## B # b) # e1 # e2 = e1 # b))
+1121 , axiom case_disj_union_inj2 (pi A \ pi B \ pi C \ (! b \ ! (A --> C) e1 \ ! (B --> C) e2 \
+1122 case_disj_union ## A ## B ## C # (inj2_disj_union ## A ## B # b) # e1 # e2 = e2 # b))
+1123
+1124 /*********** Axiomatization of the universe ********/
+1125 , decl injection_univ (pi A \pi B \ A --> univ ## A ## B)
+1126 , decl ejection_univ (pi A \pi B \ univ ## A ## B --> A)
+1127 , decl inject_limit_univ (pi A \pi B \ (B --> univ ## A ## B) --> univ ## A ## B)
+1128 , decl eject_limit_univ (pi A \ pi B \ univ ## A ## B --> (B --> univ ## A ## B))
+1129 , decl pair_univ (pi A \pi B \ univ ## A ## B --> univ ## A ## B --> univ ## A ## B)
+1130 , decl proj1_univ (pi A \ pi B \ univ ## A ## B --> univ ## A ## B)
+1131 , decl proj2_univ (pi A \pi B \ univ ## A ## B --> univ ## A ## B)
+1132 , decl inj1_univ (pi A \pi B \ univ ## A ## B --> univ ## A ## B)
+1133 , decl inj2_univ (pi A \pi B \ univ ## A ## B --> univ ## A ## B)
+1134 , decl case_univ (pi A \pi B \ pi C \ univ ## A ## B --> (univ ## A ## B --> C) --> (univ ## A ## B --> C) --> C)
+1135 , axiom ejection_injection_univ (pi A \ pi B \
+1136 ! A p \ ejection_univ ## A ## B # (injection_univ ## A ## B # p) = p)
+1137 , axiom eject_inject_limit_univ (pi A \ pi B \
+1138 ! (B --> univ ## A ## B) p \ eject_limit_univ ## A ## B # (inject_limit_univ ## A ## B # p) = p)
+1139 , axiom proj1_pair_univ (pi A \ pi B \ ! (univ ## A ## B) p1 \ ! p2 \
+1140 proj1_univ ## A ## B # (pair_univ ## A ## B # p1 # p2) = p1)
+1141 , axiom proj2_pair_univ (pi A \ pi B \ ! p1 \ ! (univ ## A ## B) p2 \
+1142 proj2_univ ## A ## B # (pair_univ ## A ## B # p1 # p2) = p2)
+1143 , axiom case_univ_inj1 (pi A \ pi B \ pi C \ (! b \ ! (univ ## A ## B --> C) e1 \ ! e2 \
+1144 case_univ ## A ## B ## C # (inj1_univ ## A ## B # b) # e1 # e2 = e1 # b))
+1145 , axiom case_univ_inj2 (pi A \ pi B \ pi C \ (! b \ ! (univ ## A ## B --> C) e1 \ ! e2 \
+1146 case_univ ## A ## B ## C # (inj2_univ ## A ## B # b) # e1 # e2 = e2 # b))
+1147
+1148 /******************* Equality *****************/
+1149 , theorem eq_reflexive (pi A \ ((! A a \ a = a),
+1150 [ then forall_i (bind A x \ r) ]))
+1151
+1152 /******************* Logic *****************/
+1153 , theorem or_commutative ((! a \ ! b \ a || b <=> b || a),
+1154 [itaut 1])
+1155 , theorem or_ff ((! a \ a || ff <=> a),
+1156 [itaut 1])
+1157 , theorem or_tt ((! a \ a || tt <=> tt),
+1158 [itaut 1])
+1159 , theorem or_idempotent ((! a \ a || a <=> a),
+1160 [itaut 1])
+1161 , theorem or_associative ((! a \ ! b \ ! c \ a || (b || c) <=> (a || b) || c),
+1162 [itaut 1])
+1163 , theorem and_commutative ((! a \ ! b \ a && b <=> b && a),
+1164 [itaut 1])
+1165 , theorem and_tt ((! a \ a && tt <=> a),
+1166 [itaut 1])
+1167 , theorem and_ff ((! a \ a && ff <=> ff),
+1168 [itaut 1])
+1169 , theorem and_idempotent ((! a \ a && a <=> a),
+1170 [itaut 1])
+1171 , theorem and_associative ((! a \ ! b \ ! c \ a && (b && c) <=> (a && b) && c),
+1172 [itaut 1])
+1173 , theorem and_or ((! a \ ! b \ ! c \ a && (b || c) <=> (a && b) || (a && c)),
+1174 [itaut 1])
+1175 , theorem or_and ((! a \ ! b \ ! c \ a || (b && c) <=> (a || b) && (a || c)),
+1176 [itaut 1])
+1177 , theorem ads_or_and ((! a \ ! b \ (a && b) || b <=> b),
+1178 [itaut 1])
+1179 , theorem ads_and_or ((! a \ ! b \ (a || b) && b <=> b),
+1180 [itaut 1])
+1181 , theorem not_or ((! a \ ! b \ not # a && not # b <=> not # (a || b)),
+1182 [itaut 2])
+1183 , theorem not_and ((! a \ ! b \ not # a || not # b ==> not # (a && b)),
+1184 [itaut 2])
+1185 , theorem not_not_not ((! p \ not # (not # (not # p)) <=> not # p),
+1186 [itaut 3])
+1187 , theorem impl_not_not ((! a \ ! b \ (a ==> b) ==> (not # b ==> not # a)),
+1188 [itaut 3])
+1189 , theorem eq_to_impl_f ((! p \ ! q \ (p <=> q) ==> p ==> q),
+1190 [itaut 2])
+1191 , theorem eq_to_impl_b ((! p \ ! q \ (p <=> q) ==> q ==> p),
+1192 [itaut 2])
+1193
+1194/*************** Properties inj/disj/univ ***********/
+1195 , theorem pair_univ_inj_l
+1196 (pi A \ pi B \ (! (univ ## A ## B) x20 \ ! x21 \ ! x22 \ ! x23 \ pair_univ ## A ## B # x20 # x22 = pair_univ ## A ## B # x21 # x23 ==> x20 = x21) ,
+1197 [then (repeat forall_i)
+1198 (bind (univ ## A ## B) x22 \
+1199 bind (univ ## A ## B) x23 \
+1200 bind (univ ## A ## B) x24 \
+1201 bind (univ ## A ## B) x25 \
+1202 then i
+1203 (then (cutth proj1_pair_univ)
+1204 (then (lforall x22)
+1205 (then (conv (land_tac (then sym apply)))
+1206 (then (conv (depth_tac h)) (applyth proj1_pair_univ))))))])
+1207 , theorem pair_univ_inj_r
+1208 (pi A \ pi B \ (! (univ ## A ## B) x20 \ ! x21 \ ! x22 \ ! x23 \ pair_univ ## A ## B # x20 # x22 = pair_univ ## A ## B # x21 # x23 ==> x22 = x23) ,
+1209 [then (repeat forall_i)
+1210 (bind (univ ## A ## B) x22 \
+1211 bind (univ ## A ## B) x23 \
+1212 bind (univ ## A ## B) x24 \
+1213 bind (univ ## A ## B) x25 \
+1214 then i
+1215 (then (cutth proj2_pair_univ)
+1216 (then (lforall x22)
+1217 (then (conv (land_tac (then sym apply)))
+1218 (then (conv (depth_tac h)) (applyth proj2_pair_univ))))))])
+1219 , theorem injection_univ_inj
+1220 (pi A \ pi B \ (! A x20 \ ! x21 \ injection_univ ## A ## B # x20 = injection_univ ## A ## B # x21 ==> x20 = x21) ,
+1221 [then forall_i
+1222 (bind A x20 \
+1223 then forall_i
+1224 (bind A x21 \
+1225 then (then (cutth ejection_injection_univ) (lforall x21))
+1226 (then (then (cutth ejection_injection_univ) (lforall x20))
+1227 (then i
+1228 (thenl
+1229 (cut
+1230 (ejection_univ ## A ## B # (injection_univ ## A ## B # x20) =
+1231 ejection_univ ## A ## B # (injection_univ ## A ## B # x21)))
+1232 [thenl
+1233 (cut
+1234 ((ejection_univ ## A ## B # (injection_univ ## A ## B # x20) =
+1235 ejection_univ ## A ## B # (injection_univ ## A ## B # x21)) =
+1236 (x20 = x21)))
+1237 [then (conv (depth_tac (then sym h))) h,
+1238 thenl c [thenl c [r, h], h]], thenl c [r, h]])))))])
+1239 , theorem inj1_univ_inj
+1240 (pi A \ pi B \ (! (univ ## A ## B) x20 \ ! x21 \ inj1_univ ## A ## B # x20 = inj1_univ ## A ## B # x21 ==> x20 = x21) ,
+1241 [then inv
+1242 (bind (univ ## A ## B) x20 \ bind (univ ## A ## B) x21 \
+1243 thenl (t (case_univ ## A ## B ## (univ ## A ## B) # (inj1_univ ## A ## B # x20) '
+1244 (lam (univ ## A ## B) x22 \ x22) '
+1245 (lam (univ ## A ## B) x22 \ x22)))
+1246 [then sym
+1247 (then (conv (land_tac (applyth case_univ_inj1)))
+1248 (then (conv (land_tac b)) r)),
+1249 then (conv (depth_tac h))
+1250 (then (conv (land_tac (applyth case_univ_inj1)))
+1251 (then (conv (land_tac b)) r))])])
+1252 , theorem inj2_univ_inj
+1253 (pi A \ pi B \ (! (univ ## A ## B) x22 \ ! x23 \ inj2_univ ## A ## B # x22 = inj2_univ ## A ## B # x23 ==> x22 = x23) ,
+1254 [then inv
+1255 (bind (univ ## A ## B) x20 \ bind (univ ## A ## B) x21 \
+1256 thenl (t (case_univ ## A ## B ## (univ ## A ## B) # (inj2_univ ## A ## B # x20) '
+1257 (lam (univ ## A ## B) x22 \ x22) '
+1258 (lam (univ ## A ## B) x22 \ x22)))
+1259 [then sym
+1260 (then (conv (land_tac (applyth case_univ_inj2)))
+1261 (then (conv (land_tac b)) r)),
+1262 then (conv (depth_tac h))
+1263 (then (conv (land_tac (applyth case_univ_inj2)))
+1264 (then (conv (land_tac b)) r))])])
+1265 , theorem not_eq_inj1_inj2_univ
+1266 (pi A \ pi B \ (! (univ ## A ## B) x22 \ ! x23 \ inj1_univ ## A ## B # x22 = inj2_univ ## A ## B # x23 ==> ff) ,
+1267 [then inv
+1268 (bind (univ ## A ## B) x22 \
+1269 bind (univ ## A ## B) x23 \
+1270 then (cutth case_univ_inj1)
+1271 (then (lforall x22)
+1272 (then (lforall (lam (univ ## A ## B) x24 \ ff))
+1273 (then (lforall (lam (univ ## A ## B) x24 \ tt))
+1274 (thenl (m ((lam (univ ## A ## B) x24 \ ff) # x22)) [b,
+1275 then (conv (then sym h))
+1276 (then (wl [])
+1277 (then (conv (depth_tac h))
+1278 (then (wl [])
+1279 (then (conv (applyth case_univ_inj2))
+1280 (then (conv b) (itaut 1))))))])))))])
+1281 , theorem inj1_disj_union_inj (pi A \ pi B \
+1282 ((! x \ ! y \
+1283 inj1_disj_union ## A ## B # x = inj1_disj_union ## A ## B # y ==> x = y) ,
+1284 [then inv
+1285 (bind A x23 \
+1286 bind A x24 \
+1287 then (cutth case_disj_union_inj1)
+1288 (then (lforall x23)
+1289 (then (lforall (lam A x25 \ x25))
+1290 (then (lforall (lam B x25 \ choose ## A))
+1291 (thenl (t ((lam A x25 \ x25) # x23))
+1292 [then (conv (rand_tac b)) r,
+1293 then (conv (land_tac (then sym h)))
+1294 (then (wl [])
+1295 (then (conv (depth_tac h))
+1296 (then (wl [])
+1297 (then (conv (land_tac (applyth case_disj_union_inj1)))
+1298 b))))])))))]))
+1299 , theorem inj2_disj_union_inj (pi A \ pi B \
+1300 ((! x \ ! y \
+1301 inj2_disj_union ## A ## B # x = inj2_disj_union ## A ## B # y ==> x = y) ,
+1302 [then inv
+1303 (bind B x23 \
+1304 bind B x24 \
+1305 then (cutth case_disj_union_inj2)
+1306 (then (lforall x23)
+1307 (then (lforall (lam A x25 \ choose ## B))
+1308 (then (lforall (lam B x25 \ x25))
+1309 (thenl (t ((lam B x25 \ x25) # x23))
+1310 [then (conv (rand_tac b)) r,
+1311 then (conv (land_tac (then sym h)))
+1312 (then (wl [])
+1313 (then (conv (depth_tac h))
+1314 (then (wl [])
+1315 (then (conv (land_tac (applyth case_disj_union_inj2)))
+1316 b))))])))))]))
+1317
+1318 /********** Monotonicity of logical connectives *********/
+1319 , theorem and_monotone ((! a1 \ ! b1 \ ! a2 \ ! b2 \
+1320 (a1 ==> b1) ==> (a2 ==> b2) ==> a1 && a2 ==> b1 && b2),
+1321 [itaut 2])
+1322 , theorem or_monotone ((! a1 \ ! b1 \ ! a2 \ ! b2 \
+1323 (a1 ==> b1) ==> (a2 ==> b2) ==> a1 || a2 ==> b1 || b2),
+1324 [itaut 2])
+1325 , theorem impl_monotone ((! a1 \ ! b1 \ ! a2 \ ! b2 \
+1326 (b1 ==> a1) ==> (a2 ==> b2) ==> (a1 ==> a2) ==> (b1 ==> b2)),
+1327 [itaut 3])
+1328 , theorem not_monotone ((! p \ ! q \ (p ==> q) ==> (not # q) ==> (not # p)),
+1329 [itaut 3])
+1330 , theorem forall_monotone (pi A \ (! p \ ! q \
+1331 (! A x \ p # x ==> q # x) ==> (! x \ p # x) ==> (! x \ q # x)),
+1332 [itaut 6])
+1333 , theorem exists_monotone (pi A \ (! p \ ! q \
+1334 (! A x \ p # x ==> q # x) ==> (? x \ p # x) ==> (? x \ q # x)),
+1335 [itaut 6])
+1336
+1337 /********** Knaster-Tarski theorem *********/
+1338 , def in (pi A \ (A --> (A --> prop) --> prop),
+1339 (lam A x \ lam (A --> prop) j \ j # x))
+1340 , def subseteq (pi A \ ((A --> prop) --> (A --> prop) --> prop),
+1341 (lam (A --> prop) x \ lam (A --> prop) y \ ! z \ z #in x ==> z #in y))
+1342 , theorem in_subseteq (pi A \
+1343 (! s \ ! t \ ! x \ s <<= t ==> x #in s ==> x #in t),
+1344 [then forall_i
+1345 (bind (A --> prop) x9 \
+1346 then forall_i
+1347 (bind (A --> prop) x10 \
+1348 then forall_i (bind A x11 \ then (conv (land_tac dd)) (itaut 4))))])
+1349 , def monotone (pi A \ (((A --> prop) --> (A --> prop)) --> prop),
+1350 (lam (_ A) f \ ! x \ ! y \ x <<= y ==> f # x <<= f # y))
+1351 , def is_fixpoint (pi A \ (((A --> prop) --> (A --> prop)) --> ((A --> prop) --> prop)),
+1352 (lam (_ A) f \ lam (_ A) x \ (f # x) <<= x && x <<= (f # x)))
+1353 , def fixpoint (pi A \ (((A --> prop) --> (A --> prop)) --> (A --> prop)),
+1354 (lam (_ A) f \ lam A a \ ! e \ f # e <<= e ==> a #in e))
+1355 , theorem fixpoint_subseteq_any_prefixpoint (pi A \
+1356 (! f \ ! x\ f # x <<= x ==> fixpoint ## A # f <<= x),
+1357 [then inv
+1358 (bind ((A --> prop) --> (A --> prop)) x9 \
+1359 (bind (A --> prop) x10 \
+1360 then (conv (land_tac dd))
+1361 (then (conv dd)
+1362 (then forall_i
+1363 (bind A x11 \
+1364 then (conv (land_tac dd))
+1365 (then (conv (land_tac b)) (itaut 4)))))))])
+1366 , theorem fixpoint_subseteq_any_fixpoint (pi A \
+1367 (! f \ ! x\ is_fixpoint ## A # f # x ==> fixpoint ## A # f <<= x),
+1368 [then forall_i
+1369 (bind ((A --> prop) --> (A --> prop)) x9 \
+1370 then forall_i
+1371 (bind (A --> prop) x10 \
+1372 then (conv (land_tac dd))
+1373 (then (cutth fixpoint_subseteq_any_prefixpoint) (itaut 8))))])
+1374 , theorem prefixpoint_to_prefixpoint (pi A \
+1375 (! f \ ! x \ monotone ## A # f ==> f # x <<= x ==> f # (f # x) <<= f # x),
+1376 [then forall_i
+1377 (bind ((A --> prop) --> (A --> prop)) x9 \
+1378 then forall_i
+1379 (bind (A --> prop) x10 \ then (conv (land_tac dd)) (itaut 6)))])
+1380 , theorem fixpoint_is_prefixpoint (pi A \
+1381 (! f \ monotone ## A # f ==> f # (fixpoint ## A # f)<<= fixpoint ## A # f),
+1382 [then inv
+1383 (bind ((A --> prop) --> (A --> prop)) x9 \
+1384 then (conv dd)
+1385 (then inv
+1386 (bind A x10 \
+1387 then (conv (depth_tac (dd [fixpoint])))
+1388 (then (conv dd)
+1389 (then (conv b)
+1390 (then inv
+1391 (bind (A --> prop) x11 \
+1392 thenl (cut (fixpoint ## A # x9 <<= x11))
+1393 [thenl
+1394 (cut (x9 # (fixpoint ## A # x9) <<= x9 # x11))
+1395 [then (cutth in_subseteq)
+1396 (then (lforall_last (x9 # x11))
+1397 (then (lforall_last x11)
+1398 (thenl apply_last [h,
+1399 then (cutth in_subseteq) (itaut 10)]))),
+1400 thenl
+1401 (m (monotone ## A # x9 ==> x9 # (fixpoint ## A # x9) <<= x9 # x11))
+1402 [itaut 10, then (conv (land_tac dd)) (itaut 10)]],
+1403 then (applyth fixpoint_subseteq_any_prefixpoint) h])))))))])
+1404 , theorem fixpoint_is_fixpoint (pi A \
+1405 (! f \ monotone ## A # f ==> is_fixpoint ## A # f # (fixpoint ## A # f)),
+1406 [then inv
+1407 (bind ((A --> prop) --> (A --> prop)) x9 \
+1408 then (conv (depth_tac (dd [is_fixpoint])))
+1409 (thenl inv [then (applyth fixpoint_is_prefixpoint) h,
+1410 then (applyth fixpoint_subseteq_any_prefixpoint)
+1411 (then (g (monotone ## A # x9))
+1412 (then (conv (land_tac dd))
+1413 (then inv
+1414 (then apply (then (applyth fixpoint_is_prefixpoint) h)))))]))])
+1415
+1416 /*********** Axiomatization of well-founded recursion ********/
+1417 , decl rec (pi A \pi B \ ((A --> B) --> (A --> B)) --> (A --> B))
+1418 , inductive_def acc accF accF_monotone acc_i0 acc_e0 acc_e
+1419 (pi A \ param (A --> A --> prop) lt \ acc \
+1420 [ (acc_i, ! x \ (! y \ lt # y # x ==> acc # y) ==> acc # x) ])
+1421
+1422 , def well_founded (pi A \ ((A --> A --> prop) --> prop,
+1423 lam (_ A) lt \ ! x \ acc ## A # lt # x))
+1424
+1425 , axiom rec_is_fixpoint (pi A \ pi B \
+1426 (! lt \ well_founded ## A # lt ==>
+1427 ! ((A --> B) --> (A --> B)) h \
+1428 (! f \ ! g \ ! i \
+1429 (! p \ lt # p # i ==> f # p = g # p) ==> h # f # i = h # g # i) ==>
+1430 rec ## A ## B # h = h # (rec ## A ## B # h)))
+1431 /******************* TESTS *****************/
+1432 /* The first three tests are commented out because they require extra-hacks
+1433 in the kernel to avoid quantifying over p, q and g.
+1434 , theorem test_apply (p ==> (p ==> p ==> q) ==> q,
+1435 [then i (then i (then apply h))])
+1436 , theorem test_apply2 (p ==> (! x \ ! y \ x ==> x ==> y) ==> q,
+1437 [then i (then i (then apply h))])
+1438 , theorem test_itaut_1 (((? x \ g x) ==> ! x \ (! y \ g y ==> x) ==> x),
+1439 [itaut 4])*/
+1440 , theorem test_monotone1 (monotone ## _ # (lam _ p \ lam _ x \ not # (p # x) ==> tt && p # tt || p # x),
+1441 [ auto_monotone ])
+1442 , theorem test_monotone2 (monotone ## _ # (lam _ p \ lam _ x \ ? z \ not # (p # x) ==> tt && p # tt || z),
+1443 [ auto_monotone ])
+1444 , theorem test_monotone3 (monotone ## _ # (lam _ p \ lam _ x \ ! z \ ? y \ (not # (p # x) ==> z && p # y || y)),
+1445 [ auto_monotone ])
+1446 , inductive_def pnn pnnF pnnF_monotone pnn_i pnn_e0 pnn_e (pnn \
+1447 [ (pnn_tt, pnn # tt)
+1448 , (pnn_not, ! x \ pnn # x ==> pnn # (not # x))])
+1449 , theorem pnn_e
+1450 ((! x13 \
+1451 x13 # tt && (! x14 \ x13 # x14 ==> x13 # (not # x14)) ==>
+1452 (! x14 \ pnn # x14 ==> x13 # x14)) ,
+1453 [then forall_i
+1454 (bind (prop --> prop) x13 \
+1455 then (cutth pnn_e0)
+1456 (then (lforall x13)
+1457 (then i
+1458 (thenl lapply
+1459 [then (conv (depth_tac (dd [pnnF])))
+1460 (then forall_i
+1461 (bind prop x14 \
+1462 then i
+1463 % from now on the proof is ad-hoc + fragile
+1464 (thenl left [then (conv (depth_tac h)) (itaut 1),
+1465 then left
+1466 (bind prop x15 \
+1467 then left (then (conv (depth_tac h)) (itaut 8)))]))),
+1468 h]))))])
+1469 , theorem pnn_has_two_values
+1470 ((! x13 \ pnn # x13 ==> x13 = tt || x13 = ff) ,
+1471 % applying an elimination principle is hard: it should be automatized
+1472 [then (cutth pnn_e)
+1473 (then (lforall (lam prop x13 \ or # (eq ## prop # x13 # tt) # (eq ## prop # x13 # ff)))
+1474 (thenl lapply
+1475 [thenl conj [then (conv b) (itaut 1),
+1476 then (repeat (conv (depth_tac b)))
+1477 (then forall_i (bind prop x13 \ then i (then left (itaut 8))))],
+1478 then inv
+1479 (bind prop x13 \
+1480 then (lforall x13)
+1481 (thenl lapply [h,
+1482 then
+1483 (g
+1484 ((lam prop x14 \ or # (eq ## prop # x14 # tt) # (eq ## prop # x14 # ff)) '
+1485 x13))
+1486 (then (repeat (conv (depth_tac b)))
+1487 (then
+1488 (w
+1489 ((lam prop x14 \ or # (eq ## prop # x14 # tt) # (eq ## prop # x14 # ff))
+1490 # x13)) (then (w (pnn # x13)) (itaut 2))))]))]))])
+1491 , inductive_def in_two in_twoF in_twoF_monotone in_two_i in_two_e0 in_two_e (in_two \
+1492 [ (in_two_tt, in_two # tt)
+1493 , (in_two_ff, in_two # ff) ])
+1494 , new_basic_type bool2 myrep2 myabs2 myrepabs2 myabsrep2 myproprep2
+1495 (pnn,
+1496 [then (cutth pnn_tt) (then (applyth exists_i) h)])
+1497 , def mytt (bool2,(myabs2 # tt))
+1498 , def mynot ((bool2 --> bool2),(lam _ x \ myabs2 # (not # (myrep2 # x))))
+1499 , theorem mytt_transfer
+1500 (myrep2 # mytt = tt ,
+1501 [then (conv (depth_tac (dd [mytt])))
+1502 (then (applyth myrepabs2) (applyth pnn_tt))])
+1503 , theorem mynot_transfer
+1504 ((! x18 \ myrep2 # (mynot # x18) = not # (myrep2 # x18)) ,
+1505 [then (conv (depth_tac (dd [mynot])))
+1506 (then forall_i
+1507 (bind bool2 x18 \
+1508 then (applyth myrepabs2)
+1509 (then (applyth pnn_not) (applyth myproprep2))))])
+1510 , theorem mybool2_e
+1511 ((! x18 \
+1512 x18 # mytt && (! x19 \ x18 # x19 ==> x18 # (mynot # x19)) ==>
+1513 (! x19 \ x18 # x19)) ,
+1514 [thenl
+1515 (cut
+1516 (forall ## (bool2 --> prop) '
+1517 (lam (bool2 --> prop) x18 \
+1518 impl '
+1519 (and # (x18 # (myabs2 # (myrep2 # mytt))) '
+1520 (forall ## bool2 '
+1521 (lam bool2 x19 \
+1522 impl # (x18 # (myabs2 # (myrep2 # x19))) '
+1523 (x18 '
+1524 (myabs2 '
+1525 (myrep2 # (mynot # (myabs2 # (myrep2 # x19)))))))))
+1526 '
+1527 (forall ## bool2 '
+1528 (lam bool2 x19 \ x18 # (myabs2 # (myrep2 # x19)))))))
+1529 [then
+1530 (g
+1531 (forall ## (bool2 --> prop) '
+1532 (lam (bool2 --> prop) x18 \
+1533 impl '
+1534 (and # (x18 # (myabs2 # (myrep2 # mytt))) '
+1535 (forall ## bool2 '
+1536 (lam bool2 x19 \
+1537 impl # (x18 # (myabs2 # (myrep2 # x19))) '
+1538 (x18 '
+1539 (myabs2 '
+1540 (myrep2 # (mynot # (myabs2 # (myrep2 # x19)))))))))
+1541 '
+1542 (forall ## bool2 '
+1543 (lam bool2 x19 \ x18 # (myabs2 # (myrep2 # x19)))))))
+1544 (then
+1545 (w
+1546 (forall ## (bool2 --> prop) '
+1547 (lam (bool2 --> prop) x18 \
+1548 impl '
+1549 (and # (x18 # (myabs2 # (myrep2 # mytt))) '
+1550 (forall ## bool2 '
+1551 (lam bool2 x19 \
+1552 impl # (x18 # (myabs2 # (myrep2 # x19))) '
+1553 (x18 '
+1554 (myabs2 '
+1555 (myrep2 # (mynot # (myabs2 # (myrep2 # x19)))))))))
+1556 '
+1557 (forall ## bool2 '
+1558 (lam bool2 x19 \ x18 # (myabs2 # (myrep2 # x19)))))))
+1559 (then (repeat (conv (depth_tac (applyth myabsrep2)))) (then i h))),
+1560 then forall_i
+1561 (bind (bool2 --> prop) x18 \
+1562 then (cutth pnn_e)
+1563 (then
+1564 (lforall
+1565 (lam prop x19 \
+1566 exists ## bool2 '
+1567 (lam bool2 x20 \
+1568 and # (eq ## _ # x19 # (myrep2 # x20)) '
+1569 (x18 # (myabs2 # x19)))))
+1570 (then inv
+1571 (bind bool2 x19 \
+1572 thenl
+1573 (cut
+1574 ((lam prop x20 \
+1575 exists ## bool2 '
+1576 (lam bool2 x21 \
+1577 and # (eq ## _ # x20 # (myrep2 # x21)) '
+1578 (x18 # (myabs2 # x20)))) # (myrep2 # x19)))
+1579 [then
+1580 (g
+1581 ((lam prop x20 \
+1582 exists ## bool2 '
+1583 (lam bool2 x21 \
+1584 and # (eq ## _ # x20 # (myrep2 # x21)) '
+1585 (x18 # (myabs2 # x20)))) # (myrep2 # x19)))
+1586 (then (conv (depth_tac b)) inv),
+1587 thenl apply
+1588 [then (repeat (conv (depth_tac b)))
+1589 (thenl inv
+1590 [then (cutth exists_i)
+1591 (then
+1592 (lforall_last
+1593 (lam bool2 x20 \
+1594 and # (eq ## _ # tt # (myrep2 # x20)) '
+1595 (x18 # (myabs2 # tt))))
+1596 (then (lforall_last mytt)
+1597 (then apply_last (then (conv b)
+1598 (thenl inv
+1599 [then (cutth mytt_transfer)
+1600 (then (conv (depth_tac h)) (applyth tt_intro)),
+1601 (applyth tt_intro),
+1602 then (cutth mytt_transfer)
+1603 (then (g (x18 # (myabs2 # (myrep2 # mytt))))
+1604 (then (conv (depth_tac h)) (then i h)))]))))),
+1605 (bind prop x20 \
+1606 bind bool2 x21 \
+1607 then (cutth exists_i)
+1608 (then
+1609 (lforall_last
+1610 (lam bool2 x22 \
+1611 and # (eq ## _ # (not # x20) # (myrep2 # x22)) '
+1612 (x18 # (myabs2 # (not # x20)))))
+1613 (then (lforall_last (mynot # x21))
+1614 (then apply_last (then (conv b)
+1615 (thenl inv
+1616 [then (conv (applyth mynot_transfer))
+1617 (then (conv (depth_tac (dd [not]))) (then inv (itaut 3))),
+1618 then (g (myrep2 # (mynot # x21)))
+1619 (then (conv (land_tac (applyth mynot_transfer)))
+1620 (then (conv (depth_tac (dd [not]))) (then inv (itaut 3)))),
+1621 then (lforall (myabs2 # x20))
+1622 (thenl lapply [then (conv (depth_tac (applyth myabsrep2))) h,
+1623 then
+1624 (g
+1625 (x18 '
+1626 (myabs2 '
+1627 (myrep2 # (mynot # (myabs2 # (myrep2 # (myabs2 # x20))))))))
+1628 (then (conv (depth_tac (applyth myabsrep2)))
+1629 (then (conv (depth_tac (applyth myabsrep2)))
+1630 (thenl (cut (x20 = myrep2 # x21))
+1631 [then (conv (depth_tac h))
+1632 (then (conv (depth_tac h))
+1633 (then (conv (depth_tac (applyth myabsrep2)))
+1634 (then i
+1635 (then
+1636 (conv
+1637 (rand_tac
+1638 (rand_tac (then sym (applyth mynot_transfer)))))
+1639 (then (conv (depth_tac (applyth myabsrep2))) h))))),
+1640 itaut 2])))])]))))))]),
+1641 applyth myproprep2]]))))]])
+1642
+1643, theorem step0
+1644 ((! x13 \ mynot # (mynot # (mynot # x13)) = mynot # x13) ,
+1645 [then inv
+1646 (bind bool2 x13 \
+1647 then (repeat (conv (depth_tac (dd [mynot]))))
+1648 (thenl (conv (land_tac (rand_tac (rand_tac (applyth myrepabs2)))))
+1649 [then (cutth pnn_not)
+1650 (then (lforall (myrep2 # (myabs2 # (not # (myrep2 # x13)))))
+1651 (then (cutth myproprep2)
+1652 (then (lforall (myabs2 # (not # (myrep2 # x13))))
+1653 (then apply h)))),
+1654 thenl
+1655 (conv
+1656 (land_tac
+1657 (rand_tac (rand_tac (rand_tac (applyth myrepabs2))))))
+1658 [then (cutth pnn_not)
+1659 (then (lforall (myrep2 # x13))
+1660 (then (cutth myproprep2)
+1661 (then (lforall x13) (then apply h)))),
+1662 then (conv (land_tac (rand_tac (applyth not_not_not)))) r]]))])
+1663 , theorem mynot_mynot_mytt
+1664 (mynot # (mynot # mytt) = mytt ,
+1665 [then (conv (depth_tac (dd [mynot])))
+1666 (then (cutth mynot_transfer)
+1667 (then (lforall mytt)
+1668 (then (conv (depth_tac h))
+1669 (then (cutth mytt_transfer)
+1670 (then (conv (depth_tac h))
+1671 (then (conv (depth_tac (dd [mytt]))) (thenl c [r, itaut 3])))))))])
+1672 , theorem step1
+1673 ((! x18 \ x18 = mytt || x18 = mynot # mytt) ,
+1674 [then forall_i
+1675 (bind bool2 x18 \
+1676 then (cutth mybool2_e)
+1677 (thenl
+1678 (cut
+1679 ((lam bool2 x19 \
+1680 or # (eq ## _ # x19 # mytt) # (eq ## _ # x19 # (mynot # mytt))) # x18))
+1681 [then
+1682 (g
+1683 ((lam bool2 x19 \
+1684 or # (eq ## _ # x19 # mytt) # (eq ## _ # x19 # (mynot # mytt))) '
+1685 x18)) (then (conv (depth_tac b)) (then i h)),
+1686 then apply
+1687 (then (repeat (conv (depth_tac b)))
+1688 (thenl conj [then (applyth orl) r,
+1689 thenl inv
+1690 [(bind bool2 x19 \
+1691 then (applyth orr) (then (conv (depth_tac h)) r)),
+1692 (bind bool2 x19 \
+1693 then (applyth orl) (then (conv (depth_tac h)) (applyth mynot_mynot_mytt)))]]))]))])
+1694
+1695 /******* Cartesian product of types ******/
+1696 /* TODO: this is an inductive type as well: generalize
+1697 inductive_type to type abstractions */
+1698 , def is_pair (pi A \ pi B \
+1699 (univ ## (disj_union ## A ## B) ## prop --> prop),
+1700 lam (_ A B) p \ ? A a \ ? B b \
+1701 p =
+1702 pair_univ ## (_ A B) ## _ '
+1703 (injection_univ ## (_ A B) ## _ # (inj1_disj_union ## A ## B # a)) '
+1704 (injection_univ ## (_ A B) ## _ # (inj2_disj_union ## A ## B # b)))
+1705 , new_basic_type prod prod_rep prod_abs prod_repabs prod_absrep prod_proprep
+1706 (pi A \ pi B \ is_pair ## A ## B, [daemon])
+1707 , def pair (pi A \ pi B \
+1708 (A --> B --> prod ## A ## B,
+1709 lam A a \ lam B b \
+1710 prod_abs ## A ## B '
+1711 (pair_univ ## (_ A B) ## _ '
+1712 (injection_univ ## (_ A B) ## _ # (inj1_disj_union ## A ## B # a)) '
+1713 (injection_univ ## (_ A B) ## _ # (inj2_disj_union ## A ## B # b)))
+1714 ))
+1715 /* TODO: define fst and snd and prove the usual lemmas
+1716 fst # (pair # a # b) = a */
+1717
+1718 /************* Natural numbers ***************/
+1719 , inductive_def is_nat is_natF is_nat_monotone is_nat_i is_nat_e0 is_nat_e
+1720 (is_nat \
+1721 [ (is_nat_z, is_nat # (inj1_univ ## prop ## prop # (injection_univ ## prop ## prop # ff)))
+1722 , (is_nat_s, ! x \ is_nat # x ==> is_nat # (inj2_univ ## prop ## prop # x))])
+1723 , new_basic_type nat nat_rep nat_abs nat_repabs nat_absrep nat_proprep
+1724 (is_nat,
+1725 [then (cutth is_nat_z) (then (applyth exists_i) h)])
+1726 , def z (nat, nat_abs # (inj1_univ ## prop ## prop # (injection_univ ## prop ## prop # ff)))
+1727 , def s (nat --> nat,
+1728 (lam _ x \ nat_abs # (inj2_univ ## prop ## prop # (nat_rep # x))))
+1729 /* TODO: consequence of is_nat_e by transfer principles */
+1730 , theorem nat_e ((! p \ p # z ==> (! n \ p # n ==> p # (s # n)) ==> ! n \ p # n), [ daemon ])
+1731 , theorem nat_abs_inj
+1732 ((! x18 \
+1733 ! x19 \
+1734 is_nat # x18 ==>
+1735 is_nat # x19 ==> nat_abs # x18 = nat_abs # x19 ==> x18 = x19) ,
+1736 [then inv
+1737 (bind _ x18 \
+1738 bind _ x19 \
+1739 thenl (conv (land_tac (then sym (applyth nat_repabs)))) [h,
+1740 thenl (conv (rand_tac (then sym (applyth nat_repabs)))) [h,
+1741 then (conv (depth_tac h)) r]])])
+1742 , theorem nat_rep_inj
+1743 ((! x18 \ ! x19 \ nat_rep # x18 = nat_rep # x19 ==> x18 = x19) ,
+1744 [then inv
+1745 (bind nat x18 \
+1746 bind nat x19 \
+1747 then (conv (land_tac (then sym (applyth nat_absrep))))
+1748 (then (conv (rand_tac (then sym (applyth nat_absrep))))
+1749 (then (conv (depth_tac h)) r)))])
+1750 , theorem s_inj ((! x18 \ ! x19 \ s # x18 = s # x19 ==> x18 = x19) ,
+1751 [then (repeat (conv (depth_tac (dd [s]))))
+1752 (then inv
+1753 (bind nat x18 \
+1754 bind nat x19 \
+1755 then (applyth nat_rep_inj)
+1756 (then (applyth inj2_univ_inj)
+1757 (thenl (applyth nat_abs_inj)
+1758 [then (applyth is_nat_s) (applyth nat_proprep),
+1759 then (applyth is_nat_s) (applyth nat_proprep), h]))))])
+1760 , theorem not_equal_z_s ((! x20 \ not # (z = s # x20)) ,
+1761 [then (repeat (conv (depth_tac (dd [z]))))
+1762 (then (repeat (conv (depth_tac (dd [s]))))
+1763 (then (repeat (conv (depth_tac (dd [not]))))
+1764 (then inv
+1765 (bind nat x20 \
+1766 then (applyth not_eq_inj1_inj2_univ)
+1767 (thenl (thenl (applyth nat_abs_inj) [id, id, h])
+1768 [applyth is_nat_z,
+1769 then (applyth is_nat_s) (applyth nat_proprep)])))))])
+1770 , def nat_case (pi A \ (nat --> A --> (nat --> A) --> A,
+1771 lam _ n \ lam (_ A) a \ lam (_ A) f \
+1772 case_univ ## prop ## prop ## A # (nat_rep # n) # (lam _ x \ a) # (lam _ p \ f # (nat_abs # p))))
+1773 , theorem nat_case_z (pi A \ ((! x21 \ ! x22 \ nat_case ## A # z # x21 # x22 = x21) ,
+1774 [then (conv (depth_tac (dd [nat_case])))
+1775 (then (conv (depth_tac (dd [z])))
+1776 (then forall_i
+1777 (bind A x21 \
+1778 then forall_i
+1779 (bind (nat --> A) x22 \
+1780 thenl
+1781 (conv (land_tac (rator_tac (land_tac (applyth nat_repabs)))))
+1782 [applyth is_nat_z,
+1783 then (conv (depth_tac (applyth case_univ_inj1)))
+1784 (then (conv (depth_tac b)) r)]))))]))
+1785 , theorem nat_case_s
+1786 (pi A \ (! x21 \ ! x22 \ ! x23 \
+1787 nat_case ## A # (s # x21) # x22 # x23 = x23 # x21),
+1788 [then (conv (depth_tac (dd [nat_case])))
+1789 (then (conv (depth_tac (dd [s])))
+1790 (then forall_i
+1791 (bind nat x21 \
+1792 then forall_i
+1793 (bind A x22 \
+1794 then forall_i
+1795 (bind (nat --> A) x23 \
+1796 thenl
+1797 (conv (land_tac (rator_tac (land_tac (applyth nat_repabs)))))
+1798 [then (applyth is_nat_s) (applyth nat_proprep),
+1799 then (conv (depth_tac (applyth case_univ_inj2)))
+1800 (then (conv (depth_tac b))
+1801 (then (conv (depth_tac (applyth nat_absrep))) r))])))))])
+1802
+1803
+1804 , theorem pred_well_founded
+1805 (well_founded ## nat # (lam nat x21 \ lam nat x22 \ x22 = s # x21) ,
+1806 [then (conv dd)
+1807 (then forall_i
+1808 (bind nat x21 \
+1809 thenl (applyth nat_e)
+1810 [then (applyth acc_i)
+1811 (then (repeat (conv (depth_tac b)))
+1812 (then inv
+1813 (bind nat x22 \
+1814 then (applyth ff_elim) (then (cutth not_equal_z_s) (itaut 4))))),
+1815 then inv
+1816 (bind nat x22 \
+1817 then (applyth acc_i)
+1818 (then (repeat (conv (depth_tac b)))
+1819 (then inv
+1820 (bind nat x23 \
+1821 then (cutth s_inj)
+1822 (then (lforall x22)
+1823 (then (lforall x23)
+1824 (thenl lapply [h,
+1825 then (conv (rand_tac (then sym h))) h])))))))]))])
+1826 , def nat_recF (pi A \
+1827 A --> (nat --> A --> A) --> (nat --> A) --> (nat --> A)
+1828 , lam A a \ lam (_ A) f \ lam (_ A) rec \ lam _ n \
+1829 nat_case ## A # n # a # (lam _ p \ f # p # (rec # p)))
+1830 , def nat_rec (pi A \
+1831 A --> (nat --> A --> A) --> nat --> A
+1832 , lam A a \ lam (_ A) f \ rec ## nat ## A # (nat_recF ## A # a # f))
+1833 , theorem nat_rec_ok0 (pi A \
+1834 ((! a \ ! f \
+1835 nat_rec ## A # a # f = nat_recF ## A # a # f # (nat_rec ## A # a # f)) ,
+1836 [then inv
+1837 (bind A x22 \
+1838 bind (nat --> A --> A) x23 \
+1839 then (repeat (conv (depth_tac (dd [nat_rec]))))
+1840 (thenl (applyth rec_is_fixpoint) [applyth pred_well_founded,
+1841 then (repeat (conv (depth_tac b)))
+1842 (then (repeat (conv (depth_tac (dd [nat_recF]))))
+1843 (then forall_i
+1844 (bind (nat --> A) x24 \
+1845 then forall_i
+1846 (bind (nat --> A) x25 \
+1847 then (conv (rand_tac beta_expand))
+1848 (thenl (applyth nat_e)
+1849 [then (conv (depth_tac b))
+1850 (then inv
+1851 (then (conv (land_tac (applyth nat_case_z)))
+1852 (then (conv (rand_tac (applyth nat_case_z))) r))),
+1853 then (repeat (conv (depth_tac b)))
+1854 (then inv
+1855 (bind nat x26 \
+1856 then (conv (rand_tac (applyth nat_case_s)))
+1857 (then (conv (land_tac (applyth nat_case_s)))
+1858 (then (repeat (conv (depth_tac b)))
+1859 (then (lforall x26)
+1860 (thenl lapply [r,
+1861 then (conv (land_tac (rand_tac h))) r]))))))])))))]))]))
+1862 , theorem nat_rec_ok (pi A \
+1863 (! a \ ! f \ ! n \
+1864 nat_rec ## A # a # f # n =
+1865 nat_case ## A # n # a # (lam _ p \ f # p # (nat_rec ## A # a # f # p))),
+1866 [then inv
+1867 (bind A x22 \
+1868 bind (nat --> A --> A) x23 \
+1869 bind nat x24 \
+1870 then (conv (land_tac (rator_tac (applyth nat_rec_ok0))))
+1871 (then (conv (depth_tac (dd [nat_recF]))) r))])
+1872
+1873 /************* Arithmetics: plus ***************/
+1874 , def plus (nat --> nat --> nat,
+1875 lam _ n \ lam _ m \
+1876 nat_rec ## _ # m # (lam _ p \ lam _ sum \ s # sum)' n)
+1877 , theorem plus_z ((! n \ z + n = n),
+1878 [then (conv (depth_tac (dd [plus])))
+1879 (then inv
+1880 (bind nat x21 \
+1881 then (conv (land_tac (applyth nat_rec_ok)))
+1882 (then (conv (land_tac (applyth nat_case_z))) r)))])
+1883 , theorem plus_s ((! n \ ! m \ s # n + m = s # (n + m)),
+1884 [then (repeat (conv (depth_tac (dd [plus]))))
+1885 (then inv
+1886 (bind nat x21 \
+1887 bind nat x22 \
+1888 then (conv (land_tac (applyth nat_rec_ok)))
+1889 (then (conv (land_tac (applyth nat_case_s)))
+1890 (then (repeat (conv (depth_tac b))) r))))])
+1891 , theorem plus_n_z ((! n \ n + z = n),
+1892 [then (conv (rand_tac beta_expand))
+1893 (thenl (applyth nat_e) [then (conv b) (applyth plus_z),
+1894 then (repeat (conv (depth_tac b)))
+1895 (then inv
+1896 (bind nat x21 \
+1897 then (conv (land_tac (applyth plus_s)))
+1898 (then (conv (depth_tac h)) r)))])])
+1899 , theorem plus_n_s ((! n \ ! m \ n + (s # m) = s # (n + m)),
+1900 [then (conv (rand_tac beta_expand))
+1901 (thenl (applyth nat_e)
+1902 [then (conv b)
+1903 (then inv
+1904 (bind nat x21 \ then (repeat (conv (depth_tac (applyth plus_z)))) r)),
+1905 then (repeat (conv (depth_tac b)))
+1906 (then inv
+1907 (bind nat x21 \
+1908 bind nat x22 \
+1909 then (conv (land_tac (applyth plus_s)))
+1910 (thenl c [r,
+1911 then (conv (land_tac apply)) (then sym (applyth plus_s))])))])])
+1912 , theorem plus_comm ((! n \ ! m \ n + m = m + n),
+1913 [then (conv (rand_tac beta_expand))
+1914 (thenl (applyth nat_e)
+1915 [then (conv b)
+1916 (then inv
+1917 (bind nat x21 \
+1918 then (conv (land_tac (applyth plus_z)))
+1919 (then sym (applyth plus_n_z)))),
+1920 then (repeat (conv (depth_tac b)))
+1921 (then inv
+1922 (bind nat x21 \
+1923 bind nat x22 \
+1924 then (conv (land_tac (applyth plus_s)))
+1925 (then sym
+1926 (then (conv (land_tac (applyth plus_n_s)))
+1927 (thenl c [r, then sym apply])))))])])
+1928
+1929 ].
+1930
+1931/* Status and dependencies of the tactics:
+1932+dd:
+1933+sym:
+1934+eq_true_intro: (th tt_intro)
+1935+forall_i: dd eq_true_intro
+1936+conj: dd eq_true_intro
+1937+andr: dd tt_intro
+1938+andl: dd tt_intro
+1939+forall_e: sym dd
+1940+mp: andr sym dd
+1941+i: dd andl conj
+1942+cut: andr sym dd i
+1943+cutth: cut
+1944+lapply*: mp
+1945+lforall*: mp forall_e
+1946+apply*: lapply lforall
+1947+applyth: cutth apply*
+1948
+1949- f converional sometimes fails
+1950- conv (depth_tac) diverges when applied to terms that contain
+1951 metavariables
+1952- repeat is not implemented using progress, that is not even there
+1953*/
+1954
+1955/*
+1956-2.5) in the proof for myprop, at the end I provide the
+1957 witness (and X X) where X remains free (and it is not even pi-quantified).
+1958 If prop was empty, then X could not exist. On the other hand, if X was
+1959 empty, then there would be no need to provide the proof at all.
+1960 In any case, the symptom for X remaining free at the end of a proof is
+1961 one or more goals delayed on it. We never check for them and we have
+1962 no way atm to do that. See bug -3)
+1963
+1964-2) the test apply_2 is very slow: why?
+1965 same for the witness for myprop
+1966
+19670) definitions must not be recursive; typing should capture it
+1968 (but not if declare_constraint is commented out...)
+1969
+19700.25) occurr check in bind case still missing :-(
+1971
+19720.50) case AppUvar vs AppUVar in unification is bugged (e.g.)
+1973 X^2 x0 x1 = X^2 x0 x1
+1974
+19752) we need to fix the ELPI problems about handling of metavariables.
+1976 I have already discussed with Enrico about them and he could have a
+1977 shot at them. Namely:
+1978 a) occur check + optimization to avoid it when possible (IN PROGRESS)
+1979 b) unimplemented cases of restriction (IN PROGRESS)
+1980
+19813) once we let metavariables reach the goals, the current HOL-light
+1982 tactic implementation becomes too fragile. We should let the user
+1983 refer to hypotheses at least by number if not by name. But we better
+1984 have a bidirectional successor/predecessor via declare_constraint
+1985
+19865) we could implement an automated theorem prover in lambdaProlog
+1987 that works or is interfaced with the HOL-light code. There are
+1988 complete provers like leanCOP 2.0 that are only 10 lines of code,
+1989 but use some Prolog tricks.
+1990
+19916) we should do a small formalization, possibly developing a tactic,
+1992 to prove that everything is working. For example, a decision procedure
+1993 for rings or for linear inequations.
+1994
+1995*/
+