author  wenzelm 
Tue, 11 Nov 2014 11:41:58 +0100  
changeset 58972  5b026cfc5f04 
parent 58963  26bf09b95dda 
child 58977  9576b510f6a2 
permissions  rwrr 
41959  1 
(* Title: CTT/Bool.thy 
1474  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  3 
Copyright 1991 University of Cambridge 
4 
*) 

5 

58889  6 
section {* The twoelement type (booleans and conditionals) *} 
17441  7 

8 
theory Bool 

9 
imports CTT 

10 
begin 

0  11 

19762  12 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19762
diff
changeset

13 
Bool :: "t" where 
19761  14 
"Bool == T+T" 
15 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19762
diff
changeset

16 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19762
diff
changeset

17 
true :: "i" where 
19761  18 
"true == inl(tt)" 
19 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19762
diff
changeset

20 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19762
diff
changeset

21 
false :: "i" where 
19761  22 
"false == inr(tt)" 
23 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19762
diff
changeset

24 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19762
diff
changeset

25 
cond :: "[i,i,i]=>i" where 
19761  26 
"cond(a,b,c) == when(a, %u. b, %u. c)" 
27 

28 
lemmas bool_defs = Bool_def true_def false_def cond_def 

29 

30 

31 
subsection {* Derivation of rules for the type Bool *} 

32 

33 
(*formation rule*) 

34 
lemma boolF: "Bool type" 

35 
apply (unfold bool_defs) 

58972  36 
apply typechk 
19761  37 
done 
38 

39 

40 
(*introduction rules for true, false*) 

41 

42 
lemma boolI_true: "true : Bool" 

43 
apply (unfold bool_defs) 

58972  44 
apply typechk 
19761  45 
done 
46 

47 
lemma boolI_false: "false : Bool" 

48 
apply (unfold bool_defs) 

58972  49 
apply typechk 
19761  50 
done 
17441  51 

19761  52 
(*elimination rule: typing of cond*) 
53 
lemma boolE: 

54 
"[ p:Bool; a : C(true); b : C(false) ] ==> cond(p,a,b) : C(p)" 

55 
apply (unfold bool_defs) 

58972  56 
apply typechk 
19761  57 
apply (erule_tac [!] TE) 
58972  58 
apply typechk 
19761  59 
done 
60 

61 
lemma boolEL: 

62 
"[ p = q : Bool; a = c : C(true); b = d : C(false) ] 

63 
==> cond(p,a,b) = cond(q,c,d) : C(p)" 

64 
apply (unfold bool_defs) 

65 
apply (rule PlusEL) 

66 
apply (erule asm_rl refl_elem [THEN TEL])+ 

67 
done 

68 

69 
(*computation rules for true, false*) 

70 

71 
lemma boolC_true: 

72 
"[ a : C(true); b : C(false) ] ==> cond(true,a,b) = a : C(true)" 

73 
apply (unfold bool_defs) 

74 
apply (rule comp_rls) 

58972  75 
apply typechk 
19761  76 
apply (erule_tac [!] TE) 
58972  77 
apply typechk 
19761  78 
done 
79 

80 
lemma boolC_false: 

81 
"[ a : C(true); b : C(false) ] ==> cond(false,a,b) = b : C(false)" 

82 
apply (unfold bool_defs) 

83 
apply (rule comp_rls) 

58972  84 
apply typechk 
19761  85 
apply (erule_tac [!] TE) 
58972  86 
apply typechk 
19761  87 
done 
17441  88 

0  89 
end 