OpenTheoryReaderContextScript.sml

1(* ===================================================================== *)
2(* FILE          : OpenTheoryReaderContextScript.sml                     *)
3(* DESCRIPTION   : The OpenTheory base package's definitions of ==>, /\   *)
4(*                 and ?, which boolTheory states differently.           *)
5(*                 OpenTheoryReader.sml used to prove these as it        *)
6(*                 loaded, making its base_thms net a function of link   *)
7(*                 order rather than of its own source.                  *)
8(* ===================================================================== *)
9
10Theory OpenTheoryReaderContext[bare]
11Ancestors
12  bool
13Libs
14  HolKernel Parse boolLib BasicProvers metisLib
15
16Theorem imp_def:
17  $==> = (\p q. p /\ q <=> p)
18Proof
19  METIS_TAC []
20QED
21
22Theorem and_def:
23  $/\ = (\p q. (\f:bool->bool->bool. f p q) = (\f. f T T))
24Proof
25  SRW_TAC [][FUN_EQ_THM, EQ_IMP_THM]
26QED
27
28Theorem exists_def:
29  $? = (\P. !q. (!x. P x ==> q) ==> q)
30Proof
31  SRW_TAC [][FUN_EQ_THM] THEN
32  SUBST_TAC [GSYM (ISPEC “P:'a->bool” ETA_THM)] THEN
33  METIS_TAC []
34QED