src/CTT/Bool.thy
author wenzelm
Fri Nov 17 02:20:03 2006 +0100 (2006-11-17)
changeset 21404 eb85850d3eb7
parent 19762 957bcf55c98f
child 35762 af3ff2ba4c54
permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
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