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