Up to index of Isabelle/CTT
theory Bool(* 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)