src/CTT/Bool.thy
author krauss
Wed Sep 23 13:48:35 2009 +0200 (2009-09-23)
changeset 32654 5f9127407430
parent 21404 eb85850d3eb7
child 35762 af3ff2ba4c54
permissions -rw-r--r--
atbroy101 is long dead, use atbroy99; comment out broken SML test invocation
     1 (*  Title:      CTT/bool
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 *)
     6 
     7 header {* The two-element type (booleans and conditionals) *}
     8 
     9 theory Bool
    10 imports CTT
    11 begin
    12 
    13 definition
    14   Bool :: "t" where
    15   "Bool == T+T"
    16 
    17 definition
    18   true :: "i" where
    19   "true == inl(tt)"
    20 
    21 definition
    22   false :: "i" where
    23   "false == inr(tt)"
    24 
    25 definition
    26   cond :: "[i,i,i]=>i" where
    27   "cond(a,b,c) == when(a, %u. b, %u. c)"
    28 
    29 lemmas bool_defs = Bool_def true_def false_def cond_def
    30 
    31 
    32 subsection {* Derivation of rules for the type Bool *}
    33 
    34 (*formation rule*)
    35 lemma boolF: "Bool type"
    36 apply (unfold bool_defs)
    37 apply (tactic "typechk_tac []")
    38 done
    39 
    40 
    41 (*introduction rules for true, false*)
    42 
    43 lemma boolI_true: "true : Bool"
    44 apply (unfold bool_defs)
    45 apply (tactic "typechk_tac []")
    46 done
    47 
    48 lemma boolI_false: "false : Bool"
    49 apply (unfold bool_defs)
    50 apply (tactic "typechk_tac []")
    51 done
    52 
    53 (*elimination rule: typing of cond*)
    54 lemma boolE: 
    55     "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
    56 apply (unfold bool_defs)
    57 apply (tactic "typechk_tac []")
    58 apply (erule_tac [!] TE)
    59 apply (tactic "typechk_tac []")
    60 done
    61 
    62 lemma boolEL: 
    63     "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |]  
    64      ==> cond(p,a,b) = cond(q,c,d) : C(p)"
    65 apply (unfold bool_defs)
    66 apply (rule PlusEL)
    67 apply (erule asm_rl refl_elem [THEN TEL])+
    68 done
    69 
    70 (*computation rules for true, false*)
    71 
    72 lemma boolC_true: 
    73     "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
    74 apply (unfold bool_defs)
    75 apply (rule comp_rls)
    76 apply (tactic "typechk_tac []")
    77 apply (erule_tac [!] TE)
    78 apply (tactic "typechk_tac []")
    79 done
    80 
    81 lemma boolC_false: 
    82     "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
    83 apply (unfold bool_defs)
    84 apply (rule comp_rls)
    85 apply (tactic "typechk_tac []")
    86 apply (erule_tac [!] TE)
    87 apply (tactic "typechk_tac []")
    88 done
    89 
    90 end