src/CTT/Bool.thy
author blanchet
Mon May 19 23:43:53 2014 +0200 (2014-05-19)
changeset 57008 10f68b83b474
parent 41959 b460124855b8
child 58889 5b7a9633cfa8
permissions -rw-r--r--
use E 1.8's auto scheduler option
     1 (*  Title:      CTT/Bool.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1991  University of Cambridge
     4 *)
     5 
     6 header {* 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]=>i" where
    26   "cond(a,b,c) == when(a, %u. b, %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 (tactic "typechk_tac []")
    37 done
    38 
    39 
    40 (*introduction rules for true, false*)
    41 
    42 lemma boolI_true: "true : Bool"
    43 apply (unfold bool_defs)
    44 apply (tactic "typechk_tac []")
    45 done
    46 
    47 lemma boolI_false: "false : Bool"
    48 apply (unfold bool_defs)
    49 apply (tactic "typechk_tac []")
    50 done
    51 
    52 (*elimination rule: typing of cond*)
    53 lemma boolE: 
    54     "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
    55 apply (unfold bool_defs)
    56 apply (tactic "typechk_tac []")
    57 apply (erule_tac [!] TE)
    58 apply (tactic "typechk_tac []")
    59 done
    60 
    61 lemma boolEL: 
    62     "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |]  
    63      ==> cond(p,a,b) = cond(q,c,d) : C(p)"
    64 apply (unfold bool_defs)
    65 apply (rule PlusEL)
    66 apply (erule asm_rl refl_elem [THEN TEL])+
    67 done
    68 
    69 (*computation rules for true, false*)
    70 
    71 lemma boolC_true: 
    72     "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
    73 apply (unfold bool_defs)
    74 apply (rule comp_rls)
    75 apply (tactic "typechk_tac []")
    76 apply (erule_tac [!] TE)
    77 apply (tactic "typechk_tac []")
    78 done
    79 
    80 lemma boolC_false: 
    81     "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
    82 apply (unfold bool_defs)
    83 apply (rule comp_rls)
    84 apply (tactic "typechk_tac []")
    85 apply (erule_tac [!] TE)
    86 apply (tactic "typechk_tac []")
    87 done
    88 
    89 end