author  wenzelm 
Wed, 15 Apr 2009 11:14:48 +0200  
changeset 30895  bad26d8f0adf 
parent 21404  eb85850d3eb7 
child 35762  af3ff2ba4c54 
permissions  rwrr 
1474  1 
(* Title: CTT/bool 
0  2 
ID: $Id$ 
1474  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1991 University of Cambridge 
5 
*) 

6 

17441  7 
header {* The twoelement type (booleans and conditionals) *} 
8 

9 
theory Bool 

10 
imports CTT 

11 
begin 

0  12 

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

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

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

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

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

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

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

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

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

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

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

29 
lemmas bool_defs = Bool_def true_def false_def cond_def 

30 

31 

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

33 

34 
(*formation rule*) 

35 
lemma boolF: "Bool type" 

36 
apply (unfold bool_defs) 

37 
apply (tactic "typechk_tac []") 

38 
done 

39 

40 

41 
(*introduction rules for true, false*) 

42 

43 
lemma boolI_true: "true : Bool" 

44 
apply (unfold bool_defs) 

45 
apply (tactic "typechk_tac []") 

46 
done 

47 

48 
lemma boolI_false: "false : Bool" 

49 
apply (unfold bool_defs) 

50 
apply (tactic "typechk_tac []") 

51 
done 

17441  52 

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

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

56 
apply (unfold bool_defs) 

57 
apply (tactic "typechk_tac []") 

58 
apply (erule_tac [!] TE) 

59 
apply (tactic "typechk_tac []") 

60 
done 

61 

62 
lemma boolEL: 

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

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

65 
apply (unfold bool_defs) 

66 
apply (rule PlusEL) 

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

68 
done 

69 

70 
(*computation rules for true, false*) 

71 

72 
lemma boolC_true: 

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

74 
apply (unfold bool_defs) 

75 
apply (rule comp_rls) 

76 
apply (tactic "typechk_tac []") 

77 
apply (erule_tac [!] TE) 

78 
apply (tactic "typechk_tac []") 

79 
done 

80 

81 
lemma boolC_false: 

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

83 
apply (unfold bool_defs) 

84 
apply (rule comp_rls) 

85 
apply (tactic "typechk_tac []") 

86 
apply (erule_tac [!] TE) 

87 
apply (tactic "typechk_tac []") 

88 
done 

17441  89 

0  90 
end 