src/CTT/Bool.thy
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 58977 9576b510f6a2
child 60770 240563fbf41d
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm@41959
     1
(*  Title:      CTT/Bool.thy
clasohm@1474
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     3
    Copyright   1991  University of Cambridge
clasohm@0
     4
*)
clasohm@0
     5
wenzelm@58889
     6
section {* The two-element type (booleans and conditionals) *}
wenzelm@17441
     7
wenzelm@17441
     8
theory Bool
wenzelm@17441
     9
imports CTT
wenzelm@17441
    10
begin
clasohm@0
    11
wenzelm@19762
    12
definition
wenzelm@21404
    13
  Bool :: "t" where
wenzelm@19761
    14
  "Bool == T+T"
wenzelm@19761
    15
wenzelm@21404
    16
definition
wenzelm@21404
    17
  true :: "i" where
wenzelm@19761
    18
  "true == inl(tt)"
wenzelm@19761
    19
wenzelm@21404
    20
definition
wenzelm@21404
    21
  false :: "i" where
wenzelm@19761
    22
  "false == inr(tt)"
wenzelm@19761
    23
wenzelm@21404
    24
definition
wenzelm@58977
    25
  cond :: "[i,i,i]\<Rightarrow>i" where
wenzelm@58977
    26
  "cond(a,b,c) == when(a, \<lambda>u. b, \<lambda>u. c)"
wenzelm@19761
    27
wenzelm@19761
    28
lemmas bool_defs = Bool_def true_def false_def cond_def
wenzelm@19761
    29
wenzelm@19761
    30
wenzelm@19761
    31
subsection {* Derivation of rules for the type Bool *}
wenzelm@19761
    32
wenzelm@19761
    33
(*formation rule*)
wenzelm@19761
    34
lemma boolF: "Bool type"
wenzelm@19761
    35
apply (unfold bool_defs)
wenzelm@58972
    36
apply typechk
wenzelm@19761
    37
done
wenzelm@19761
    38
wenzelm@19761
    39
wenzelm@19761
    40
(*introduction rules for true, false*)
wenzelm@19761
    41
wenzelm@19761
    42
lemma boolI_true: "true : Bool"
wenzelm@19761
    43
apply (unfold bool_defs)
wenzelm@58972
    44
apply typechk
wenzelm@19761
    45
done
wenzelm@19761
    46
wenzelm@19761
    47
lemma boolI_false: "false : Bool"
wenzelm@19761
    48
apply (unfold bool_defs)
wenzelm@58972
    49
apply typechk
wenzelm@19761
    50
done
wenzelm@17441
    51
wenzelm@19761
    52
(*elimination rule: typing of cond*)
wenzelm@58977
    53
lemma boolE: "\<lbrakk>p:Bool; a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(p,a,b) : C(p)"
wenzelm@19761
    54
apply (unfold bool_defs)
wenzelm@58972
    55
apply typechk
wenzelm@19761
    56
apply (erule_tac [!] TE)
wenzelm@58972
    57
apply typechk
wenzelm@19761
    58
done
wenzelm@19761
    59
wenzelm@58977
    60
lemma boolEL: "\<lbrakk>p = q : Bool; a = c : C(true); b = d : C(false)\<rbrakk>
wenzelm@58977
    61
  \<Longrightarrow> 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@58977
    69
lemma boolC_true: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(true,a,b) = a : C(true)"
wenzelm@19761
    70
apply (unfold bool_defs)
wenzelm@19761
    71
apply (rule comp_rls)
wenzelm@58972
    72
apply typechk
wenzelm@19761
    73
apply (erule_tac [!] TE)
wenzelm@58972
    74
apply typechk
wenzelm@19761
    75
done
wenzelm@19761
    76
wenzelm@58977
    77
lemma boolC_false: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(false,a,b) = b : C(false)"
wenzelm@19761
    78
apply (unfold bool_defs)
wenzelm@19761
    79
apply (rule comp_rls)
wenzelm@58972
    80
apply typechk
wenzelm@19761
    81
apply (erule_tac [!] TE)
wenzelm@58972
    82
apply typechk
wenzelm@19761
    83
done
wenzelm@17441
    84
clasohm@0
    85
end