src/CTT/Bool.thy
author blanchet
Mon May 19 23:43:53 2014 +0200 (2014-05-19)
changeset 57008 10f68b83b474
parent 41959 b460124855b8
child 58889 5b7a9633cfa8
permissions -rw-r--r--
use E 1.8's auto scheduler option
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@17441
     6
header {* 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@21404
    25
  cond :: "[i,i,i]=>i" where
wenzelm@19761
    26
  "cond(a,b,c) == when(a, %u. b, %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@19761
    36
apply (tactic "typechk_tac []")
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@19761
    44
apply (tactic "typechk_tac []")
wenzelm@19761
    45
done
wenzelm@19761
    46
wenzelm@19761
    47
lemma boolI_false: "false : Bool"
wenzelm@19761
    48
apply (unfold bool_defs)
wenzelm@19761
    49
apply (tactic "typechk_tac []")
wenzelm@19761
    50
done
wenzelm@17441
    51
wenzelm@19761
    52
(*elimination rule: typing of cond*)
wenzelm@19761
    53
lemma boolE: 
wenzelm@19761
    54
    "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
wenzelm@19761
    55
apply (unfold bool_defs)
wenzelm@19761
    56
apply (tactic "typechk_tac []")
wenzelm@19761
    57
apply (erule_tac [!] TE)
wenzelm@19761
    58
apply (tactic "typechk_tac []")
wenzelm@19761
    59
done
wenzelm@19761
    60
wenzelm@19761
    61
lemma boolEL: 
wenzelm@19761
    62
    "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |]  
wenzelm@19761
    63
     ==> cond(p,a,b) = cond(q,c,d) : C(p)"
wenzelm@19761
    64
apply (unfold bool_defs)
wenzelm@19761
    65
apply (rule PlusEL)
wenzelm@19761
    66
apply (erule asm_rl refl_elem [THEN TEL])+
wenzelm@19761
    67
done
wenzelm@19761
    68
wenzelm@19761
    69
(*computation rules for true, false*)
wenzelm@19761
    70
wenzelm@19761
    71
lemma boolC_true: 
wenzelm@19761
    72
    "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
wenzelm@19761
    73
apply (unfold bool_defs)
wenzelm@19761
    74
apply (rule comp_rls)
wenzelm@19761
    75
apply (tactic "typechk_tac []")
wenzelm@19761
    76
apply (erule_tac [!] TE)
wenzelm@19761
    77
apply (tactic "typechk_tac []")
wenzelm@19761
    78
done
wenzelm@19761
    79
wenzelm@19761
    80
lemma boolC_false: 
wenzelm@19761
    81
    "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
wenzelm@19761
    82
apply (unfold bool_defs)
wenzelm@19761
    83
apply (rule comp_rls)
wenzelm@19761
    84
apply (tactic "typechk_tac []")
wenzelm@19761
    85
apply (erule_tac [!] TE)
wenzelm@19761
    86
apply (tactic "typechk_tac []")
wenzelm@19761
    87
done
wenzelm@17441
    88
clasohm@0
    89
end