# Theory Bool

Up to index of Isabelle/CTT

theory Bool
imports CTT
uses $ISABELLE_HOME/src/Provers/typedsimp.ML rew.ML [Bool.ML]
begin

    (*  Title:      CTT/bool
        ID:         $Id: Bool.thy,v 1.4 2005/09/16 21:01:30 wenzelm Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1991  University of Cambridge
    *)

    header {* The two-element type (booleans and conditionals) *}

    theory Bool
    imports CTT
    uses "~~/src/Provers/typedsimp.ML" "rew.ML"
    begin

    consts
      Bool        :: "t"
      true        :: "i"
      false       :: "i"
      cond        :: "[i,i,i]=>i"
    defs
      Bool_def:   "Bool == T+T"
      true_def:   "true == inl(tt)"
      false_def:  "false == inr(tt)"
      cond_def:   "cond(a,b,c) == when(a, %u. b, %u. c)"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem boolF:

      Bool type

theorem boolI_true:

      true ∈ Bool

theorem boolI_false:

      false ∈ Bool

theorem boolE:

      [| p ∈ Bool; a ∈ C(true); b ∈ C(false) |] ==> cond(p, a, b) ∈ C(p)

theorem boolEL:

      [| p = q ∈ Bool; a = c ∈ C(true); b = d ∈ C(false) |]
      ==> cond(p, a, b) = cond(q, c, d) ∈ C(p)

theorem boolC_true:

      [| a ∈ C(true); b ∈ C(false) |] ==> cond(true, a, b) = a ∈ C(true)

theorem boolC_false:

      [| a ∈ C(true); b ∈ C(false) |] ==> cond(false, a, b) = b ∈ C(false)