author  wenzelm 
Thu, 23 Jul 2015 14:25:05 +0200  
changeset 60770  240563fbf41d 
parent 58977  9576b510f6a2 
child 61391  2332d9be352b 
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 

60770  6 
section \<open>The twoelement type (booleans and conditionals)\<close> 
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 
58977  25 
cond :: "[i,i,i]\<Rightarrow>i" where 
26 
"cond(a,b,c) == when(a, \<lambda>u. b, \<lambda>u. c)" 

19761  27 

28 
lemmas bool_defs = Bool_def true_def false_def cond_def 

29 

30 

60770  31 
subsection \<open>Derivation of rules for the type Bool\<close> 
19761  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*) 
58977  53 
lemma boolE: "\<lbrakk>p:Bool; a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(p,a,b) : C(p)" 
19761  54 
apply (unfold bool_defs) 
58972  55 
apply typechk 
19761  56 
apply (erule_tac [!] TE) 
58972  57 
apply typechk 
19761  58 
done 
59 

58977  60 
lemma boolEL: "\<lbrakk>p = q : Bool; a = c : C(true); b = d : C(false)\<rbrakk> 
61 
\<Longrightarrow> cond(p,a,b) = cond(q,c,d) : C(p)" 

19761  62 
apply (unfold bool_defs) 
63 
apply (rule PlusEL) 

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

65 
done 

66 

67 
(*computation rules for true, false*) 

68 

58977  69 
lemma boolC_true: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(true,a,b) = a : C(true)" 
19761  70 
apply (unfold bool_defs) 
71 
apply (rule comp_rls) 

58972  72 
apply typechk 
19761  73 
apply (erule_tac [!] TE) 
58972  74 
apply typechk 
19761  75 
done 
76 

58977  77 
lemma boolC_false: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(false,a,b) = b : C(false)" 
19761  78 
apply (unfold bool_defs) 
79 
apply (rule comp_rls) 

58972  80 
apply typechk 
19761  81 
apply (erule_tac [!] TE) 
58972  82 
apply typechk 
19761  83 
done 
17441  84 

0  85 
end 