Theory Bool

Up to index of Isabelle/ZF

theory Bool
imports pair
`(*  Title:      ZF/Bool.thy    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory    Copyright   1992  University of Cambridge*)header{*Booleans in Zermelo-Fraenkel Set Theory*}theory Bool imports pair beginabbreviation  one  ("1") where  "1 == succ(0)"abbreviation  two  ("2") where  "2 == succ(1)"text{*2 is equal to bool, but is used as a number rather than a type.*}definition "bool == {0,1}"definition "cond(b,c,d) == if(b=1,c,d)"definition "not(b) == cond(b,0,1)"definition  "and"       :: "[i,i]=>i"      (infixl "and" 70)  where    "a and b == cond(a,b,0)"definition  or          :: "[i,i]=>i"      (infixl "or" 65)  where    "a or b == cond(a,1,b)"definition  xor         :: "[i,i]=>i"      (infixl "xor" 65) where    "a xor b == cond(a,not(b),b)"lemmas bool_defs = bool_def cond_deflemma singleton_0: "{0} = 1"by (simp add: succ_def)(* Introduction rules *)lemma bool_1I [simp,TC]: "1 ∈ bool"by (simp add: bool_defs )lemma bool_0I [simp,TC]: "0 ∈ bool"by (simp add: bool_defs)lemma one_not_0: "1≠0"by (simp add: bool_defs )(** 1=0 ==> R **)lemmas one_neq_0 = one_not_0 [THEN notE]lemma boolE:    "[| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P"by (simp add: bool_defs, blast)(** cond **)(*1 means true*)lemma cond_1 [simp]: "cond(1,c,d) = c"by (simp add: bool_defs )(*0 means false*)lemma cond_0 [simp]: "cond(0,c,d) = d"by (simp add: bool_defs )lemma cond_type [TC]: "[| b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)"by (simp add: bool_defs, blast)(*For Simp_tac and Blast_tac*)lemma cond_simple_type: "[| b: bool;  c: A;  d: A |] ==> cond(b,c,d): A"by (simp add: bool_defs )lemma def_cond_1: "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c"by simplemma def_cond_0: "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d"by simplemmas not_1 = not_def [THEN def_cond_1, simp]lemmas not_0 = not_def [THEN def_cond_0, simp]lemmas and_1 = and_def [THEN def_cond_1, simp]lemmas and_0 = and_def [THEN def_cond_0, simp]lemmas or_1 = or_def [THEN def_cond_1, simp]lemmas or_0 = or_def [THEN def_cond_0, simp]lemmas xor_1 = xor_def [THEN def_cond_1, simp]lemmas xor_0 = xor_def [THEN def_cond_0, simp]lemma not_type [TC]: "a:bool ==> not(a) ∈ bool"by (simp add: not_def)lemma and_type [TC]: "[| a:bool;  b:bool |] ==> a and b ∈ bool"by (simp add: and_def)lemma or_type [TC]: "[| a:bool;  b:bool |] ==> a or b ∈ bool"by (simp add: or_def)lemma xor_type [TC]: "[| a:bool;  b:bool |] ==> a xor b ∈ bool"by (simp add: xor_def)lemmas bool_typechecks = bool_1I bool_0I cond_type not_type and_type                         or_type xor_typesubsection{*Laws About 'not' *}lemma not_not [simp]: "a:bool ==> not(not(a)) = a"by (elim boolE, auto)lemma not_and [simp]: "a:bool ==> not(a and b) = not(a) or not(b)"by (elim boolE, auto)lemma not_or [simp]: "a:bool ==> not(a or b) = not(a) and not(b)"by (elim boolE, auto)subsection{*Laws About 'and' *}lemma and_absorb [simp]: "a: bool ==> a and a = a"by (elim boolE, auto)lemma and_commute: "[| a: bool; b:bool |] ==> a and b = b and a"by (elim boolE, auto)lemma and_assoc: "a: bool ==> (a and b) and c  =  a and (b and c)"by (elim boolE, auto)lemma and_or_distrib: "[| a: bool; b:bool; c:bool |] ==>       (a or b) and c  =  (a and c) or (b and c)"by (elim boolE, auto)subsection{*Laws About 'or' *}lemma or_absorb [simp]: "a: bool ==> a or a = a"by (elim boolE, auto)lemma or_commute: "[| a: bool; b:bool |] ==> a or b = b or a"by (elim boolE, auto)lemma or_assoc: "a: bool ==> (a or b) or c  =  a or (b or c)"by (elim boolE, auto)lemma or_and_distrib: "[| a: bool; b: bool; c: bool |] ==>           (a and b) or c  =  (a or c) and (b or c)"by (elim boolE, auto)definition  bool_of_o :: "o=>i" where   "bool_of_o(P) == (if P then 1 else 0)"lemma [simp]: "bool_of_o(True) = 1"by (simp add: bool_of_o_def)lemma [simp]: "bool_of_o(False) = 0"by (simp add: bool_of_o_def)lemma [simp,TC]: "bool_of_o(P) ∈ bool"by (simp add: bool_of_o_def)lemma [simp]: "(bool_of_o(P) = 1) <-> P"by (simp add: bool_of_o_def)lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"by (simp add: bool_of_o_def)end`