src/CTT/Bool.thy
changeset 60770 240563fbf41d
parent 58977 9576b510f6a2
child 61391 2332d9be352b
equal deleted inserted replaced
60769:cf7f3465eaf1 60770:240563fbf41d
     1 (*  Title:      CTT/Bool.thy
     1 (*  Title:      CTT/Bool.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1991  University of Cambridge
     3     Copyright   1991  University of Cambridge
     4 *)
     4 *)
     5 
     5 
     6 section {* The two-element type (booleans and conditionals) *}
     6 section \<open>The two-element type (booleans and conditionals)\<close>
     7 
     7 
     8 theory Bool
     8 theory Bool
     9 imports CTT
     9 imports CTT
    10 begin
    10 begin
    11 
    11 
    26   "cond(a,b,c) == when(a, \<lambda>u. b, \<lambda>u. c)"
    26   "cond(a,b,c) == when(a, \<lambda>u. b, \<lambda>u. c)"
    27 
    27 
    28 lemmas bool_defs = Bool_def true_def false_def cond_def
    28 lemmas bool_defs = Bool_def true_def false_def cond_def
    29 
    29 
    30 
    30 
    31 subsection {* Derivation of rules for the type Bool *}
    31 subsection \<open>Derivation of rules for the type Bool\<close>
    32 
    32 
    33 (*formation rule*)
    33 (*formation rule*)
    34 lemma boolF: "Bool type"
    34 lemma boolF: "Bool type"
    35 apply (unfold bool_defs)
    35 apply (unfold bool_defs)
    36 apply typechk
    36 apply typechk