src/CTT/Bool.thy
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 58977 9576b510f6a2
child 60770 240563fbf41d
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
     1 (*  Title:      CTT/Bool.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1991  University of Cambridge
     4 *)
     5 
     6 section {* The two-element type (booleans and conditionals) *}
     7 
     8 theory Bool
     9 imports CTT
    10 begin
    11 
    12 definition
    13   Bool :: "t" where
    14   "Bool == T+T"
    15 
    16 definition
    17   true :: "i" where
    18   "true == inl(tt)"
    19 
    20 definition
    21   false :: "i" where
    22   "false == inr(tt)"
    23 
    24 definition
    25   cond :: "[i,i,i]\<Rightarrow>i" where
    26   "cond(a,b,c) == when(a, \<lambda>u. b, \<lambda>u. c)"
    27 
    28 lemmas bool_defs = Bool_def true_def false_def cond_def
    29 
    30 
    31 subsection {* Derivation of rules for the type Bool *}
    32 
    33 (*formation rule*)
    34 lemma boolF: "Bool type"
    35 apply (unfold bool_defs)
    36 apply typechk
    37 done
    38 
    39 
    40 (*introduction rules for true, false*)
    41 
    42 lemma boolI_true: "true : Bool"
    43 apply (unfold bool_defs)
    44 apply typechk
    45 done
    46 
    47 lemma boolI_false: "false : Bool"
    48 apply (unfold bool_defs)
    49 apply typechk
    50 done
    51 
    52 (*elimination rule: typing of cond*)
    53 lemma boolE: "\<lbrakk>p:Bool; a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(p,a,b) : C(p)"
    54 apply (unfold bool_defs)
    55 apply typechk
    56 apply (erule_tac [!] TE)
    57 apply typechk
    58 done
    59 
    60 lemma boolEL: "\<lbrakk>p = q : Bool; a = c : C(true); b = d : C(false)\<rbrakk>
    61   \<Longrightarrow> cond(p,a,b) = cond(q,c,d) : C(p)"
    62 apply (unfold bool_defs)
    63 apply (rule PlusEL)
    64 apply (erule asm_rl refl_elem [THEN TEL])+
    65 done
    66 
    67 (*computation rules for true, false*)
    68 
    69 lemma boolC_true: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(true,a,b) = a : C(true)"
    70 apply (unfold bool_defs)
    71 apply (rule comp_rls)
    72 apply typechk
    73 apply (erule_tac [!] TE)
    74 apply typechk
    75 done
    76 
    77 lemma boolC_false: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(false,a,b) = b : C(false)"
    78 apply (unfold bool_defs)
    79 apply (rule comp_rls)
    80 apply typechk
    81 apply (erule_tac [!] TE)
    82 apply typechk
    83 done
    84 
    85 end