src/CTT/Bool.thy
author wenzelm
Fri Jun 02 18:15:38 2006 +0200 (2006-06-02)
changeset 19761 5cd82054c2c6
parent 17441 5b5feca0344a
child 19762 957bcf55c98f
permissions -rw-r--r--
removed obsolete ML files;
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@19761
    13
constdefs
wenzelm@19761
    14
  Bool :: "t"
wenzelm@19761
    15
  "Bool == T+T"
wenzelm@19761
    16
wenzelm@19761
    17
  true :: "i"
wenzelm@19761
    18
  "true == inl(tt)"
wenzelm@19761
    19
wenzelm@19761
    20
  false :: "i"
wenzelm@19761
    21
  "false == inr(tt)"
wenzelm@19761
    22
wenzelm@19761
    23
  cond :: "[i,i,i]=>i"
wenzelm@19761
    24
  "cond(a,b,c) == when(a, %u. b, %u. c)"
wenzelm@19761
    25
wenzelm@19761
    26
lemmas bool_defs = Bool_def true_def false_def cond_def
wenzelm@19761
    27
wenzelm@19761
    28
wenzelm@19761
    29
subsection {* Derivation of rules for the type Bool *}
wenzelm@19761
    30
wenzelm@19761
    31
(*formation rule*)
wenzelm@19761
    32
lemma boolF: "Bool type"
wenzelm@19761
    33
apply (unfold bool_defs)
wenzelm@19761
    34
apply (tactic "typechk_tac []")
wenzelm@19761
    35
done
wenzelm@19761
    36
wenzelm@19761
    37
wenzelm@19761
    38
(*introduction rules for true, false*)
wenzelm@19761
    39
wenzelm@19761
    40
lemma boolI_true: "true : Bool"
wenzelm@19761
    41
apply (unfold bool_defs)
wenzelm@19761
    42
apply (tactic "typechk_tac []")
wenzelm@19761
    43
done
wenzelm@19761
    44
wenzelm@19761
    45
lemma boolI_false: "false : Bool"
wenzelm@19761
    46
apply (unfold bool_defs)
wenzelm@19761
    47
apply (tactic "typechk_tac []")
wenzelm@19761
    48
done
wenzelm@17441
    49
wenzelm@19761
    50
(*elimination rule: typing of cond*)
wenzelm@19761
    51
lemma boolE: 
wenzelm@19761
    52
    "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
wenzelm@19761
    53
apply (unfold bool_defs)
wenzelm@19761
    54
apply (tactic "typechk_tac []")
wenzelm@19761
    55
apply (erule_tac [!] TE)
wenzelm@19761
    56
apply (tactic "typechk_tac []")
wenzelm@19761
    57
done
wenzelm@19761
    58
wenzelm@19761
    59
lemma boolEL: 
wenzelm@19761
    60
    "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |]  
wenzelm@19761
    61
     ==> cond(p,a,b) = cond(q,c,d) : C(p)"
wenzelm@19761
    62
apply (unfold bool_defs)
wenzelm@19761
    63
apply (rule PlusEL)
wenzelm@19761
    64
apply (erule asm_rl refl_elem [THEN TEL])+
wenzelm@19761
    65
done
wenzelm@19761
    66
wenzelm@19761
    67
(*computation rules for true, false*)
wenzelm@19761
    68
wenzelm@19761
    69
lemma boolC_true: 
wenzelm@19761
    70
    "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
wenzelm@19761
    71
apply (unfold bool_defs)
wenzelm@19761
    72
apply (rule comp_rls)
wenzelm@19761
    73
apply (tactic "typechk_tac []")
wenzelm@19761
    74
apply (erule_tac [!] TE)
wenzelm@19761
    75
apply (tactic "typechk_tac []")
wenzelm@19761
    76
done
wenzelm@19761
    77
wenzelm@19761
    78
lemma boolC_false: 
wenzelm@19761
    79
    "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
wenzelm@19761
    80
apply (unfold bool_defs)
wenzelm@19761
    81
apply (rule comp_rls)
wenzelm@19761
    82
apply (tactic "typechk_tac []")
wenzelm@19761
    83
apply (erule_tac [!] TE)
wenzelm@19761
    84
apply (tactic "typechk_tac []")
wenzelm@19761
    85
done
wenzelm@17441
    86
clasohm@0
    87
end