author  blanchet 
Mon, 26 Nov 2012 13:35:05 +0100  
changeset 50222  40e3c3be6bca 
parent 41959  b460124855b8 
child 58889  5b7a9633cfa8 
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 

17441  6 
header {* The twoelement type (booleans and conditionals) *} 
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) 

36 
apply (tactic "typechk_tac []") 

37 
done 

38 

39 

40 
(*introduction rules for true, false*) 

41 

42 
lemma boolI_true: "true : Bool" 

43 
apply (unfold bool_defs) 

44 
apply (tactic "typechk_tac []") 

45 
done 

46 

47 
lemma boolI_false: "false : Bool" 

48 
apply (unfold bool_defs) 

49 
apply (tactic "typechk_tac []") 

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) 

56 
apply (tactic "typechk_tac []") 

57 
apply (erule_tac [!] TE) 

58 
apply (tactic "typechk_tac []") 

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) 

75 
apply (tactic "typechk_tac []") 

76 
apply (erule_tac [!] TE) 

77 
apply (tactic "typechk_tac []") 

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) 

84 
apply (tactic "typechk_tac []") 

85 
apply (erule_tac [!] TE) 

86 
apply (tactic "typechk_tac []") 

87 
done 

17441  88 

0  89 
end 