new encodings of booleans, two ways

encodings/bool_hol.lp

+// Definition based on implication
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+
+definition false ≔ forall {bool} (λx, x)
+definition true ≔ impd {false} (λ_, false)
+
+definition not P ≔ impd {P} (λ_, false)
+set prefix 5 "¬" ≔ not
+
+definition imp P Q ≔ impd {P} Q
+set infix 2 "⊃" ≔ imp
+
+definition {|and|} P Q ≔ ¬ (P ⊃ (λh, ¬ (Q h)))
+set infix 4 "∧" ≔ {|and|}
+definition or P Q ≔ (¬ P) ⊃ Q
+set infix 3 "∨" ≔ or
+
+set builtin "bot" ≔ false
+set builtin "top" ≔ true
+set builtin "not" ≔ not
+set builtin "imp" ≔ imp
+set builtin "and" ≔ {|and|}
+set builtin "or"  ≔ or
+
+symbol if {s: Set} p: (ε p ⇒ η s) ⇒ (ε (¬ p) ⇒ η s) ⇒ η s
+rule if {bool} &p &then &else → (&p ⊃ &then) ⊃ (λ_, ¬ &p ⊃ &else)

encodings/bool_pvs.lp

+// Close to PVS logic system: native equality,
+// true, false, and if
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+
+definition false ≔ forall {bool} (λx, x)
+definition true ≔ impd {false} (λ_, false)
+
+symbol eq {s: Set}: η s ⇒ η s ⇒ η bool
+set infix left 6 "=" ≔ eq
+
+definition not p ≔ eq {bool} p false
+set prefix 5 "¬" ≔ not
+
+constant symbol if {s: Set} p: (ε p ⇒ η s) ⇒ (ε (¬ p) ⇒ η s) ⇒ η s
+rule ε (if &p &then &else)
+   → (∀h: ε &p, ε (&then h)) ⇒ ∀h: ε (¬ &p), ε (&else h)
+
+definition {|and|} p q ≔ if {bool} p q (λ_, false)
+definition or p q ≔ if {bool} p (λ_, true) q
+definition imp p q ≔ if {bool} p q (λ_, true)
+set infix left 4 "∧" ≔ {|and|}
+set infix left 3 "∨" ≔ or
+set infix left 2 "⊃" ≔ imp
+
+set builtin "bot" ≔ false
+set builtin "top" ≔ true
+set builtin "not" ≔ not
+set builtin "imp" ≔ imp
+set builtin "and" ≔ {|and|}
+set builtin "or"  ≔ or

encodings/boolops_if.lp

 // Boolean operators defined from if.
-require open
-  personoj.encodings.lhol
-  personoj.encodings.pvs_cert
-  personoj.encodings.booleans
-  personoj.encodings.if
+require open personoj.encodings.lhol
+require open  personoj.encodings.pvs_cert
+require open  personoj.encodings.booleans
+require open  personoj.encodings.if
 
 // Definition of logical connectors with if3
 definition band p q ≔ if {bool} p q (λ_, false)

sandbox/boolops_if.lp

+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.bool_pvs
+
+theorem trivial (P: η bool): ε (P ⊃ (λ_, P))
+proof
+  assume P
+  refine λ_ _ f, f
+qed