31 subsection {* Derivation of rules for the type Bool *} |
31 subsection {* Derivation of rules for the type Bool *} |
32 |
32 |
33 (*formation rule*) |
33 (*formation rule*) |
34 lemma boolF: "Bool type" |
34 lemma boolF: "Bool type" |
35 apply (unfold bool_defs) |
35 apply (unfold bool_defs) |
36 apply (tactic "typechk_tac @{context} []") |
36 apply typechk |
37 done |
37 done |
38 |
38 |
39 |
39 |
40 (*introduction rules for true, false*) |
40 (*introduction rules for true, false*) |
41 |
41 |
42 lemma boolI_true: "true : Bool" |
42 lemma boolI_true: "true : Bool" |
43 apply (unfold bool_defs) |
43 apply (unfold bool_defs) |
44 apply (tactic "typechk_tac @{context} []") |
44 apply typechk |
45 done |
45 done |
46 |
46 |
47 lemma boolI_false: "false : Bool" |
47 lemma boolI_false: "false : Bool" |
48 apply (unfold bool_defs) |
48 apply (unfold bool_defs) |
49 apply (tactic "typechk_tac @{context} []") |
49 apply typechk |
50 done |
50 done |
51 |
51 |
52 (*elimination rule: typing of cond*) |
52 (*elimination rule: typing of cond*) |
53 lemma boolE: |
53 lemma boolE: |
54 "[| p:Bool; a : C(true); b : C(false) |] ==> cond(p,a,b) : C(p)" |
54 "[| p:Bool; a : C(true); b : C(false) |] ==> cond(p,a,b) : C(p)" |
55 apply (unfold bool_defs) |
55 apply (unfold bool_defs) |
56 apply (tactic "typechk_tac @{context} []") |
56 apply typechk |
57 apply (erule_tac [!] TE) |
57 apply (erule_tac [!] TE) |
58 apply (tactic "typechk_tac @{context} []") |
58 apply typechk |
59 done |
59 done |
60 |
60 |
61 lemma boolEL: |
61 lemma boolEL: |
62 "[| p = q : Bool; a = c : C(true); b = d : C(false) |] |
62 "[| p = q : Bool; a = c : C(true); b = d : C(false) |] |
63 ==> cond(p,a,b) = cond(q,c,d) : C(p)" |
63 ==> cond(p,a,b) = cond(q,c,d) : C(p)" |
70 |
70 |
71 lemma boolC_true: |
71 lemma boolC_true: |
72 "[| a : C(true); b : C(false) |] ==> cond(true,a,b) = a : C(true)" |
72 "[| a : C(true); b : C(false) |] ==> cond(true,a,b) = a : C(true)" |
73 apply (unfold bool_defs) |
73 apply (unfold bool_defs) |
74 apply (rule comp_rls) |
74 apply (rule comp_rls) |
75 apply (tactic "typechk_tac @{context} []") |
75 apply typechk |
76 apply (erule_tac [!] TE) |
76 apply (erule_tac [!] TE) |
77 apply (tactic "typechk_tac @{context} []") |
77 apply typechk |
78 done |
78 done |
79 |
79 |
80 lemma boolC_false: |
80 lemma boolC_false: |
81 "[| a : C(true); b : C(false) |] ==> cond(false,a,b) = b : C(false)" |
81 "[| a : C(true); b : C(false) |] ==> cond(false,a,b) = b : C(false)" |
82 apply (unfold bool_defs) |
82 apply (unfold bool_defs) |
83 apply (rule comp_rls) |
83 apply (rule comp_rls) |
84 apply (tactic "typechk_tac @{context} []") |
84 apply typechk |
85 apply (erule_tac [!] TE) |
85 apply (erule_tac [!] TE) |
86 apply (tactic "typechk_tac @{context} []") |
86 apply typechk |
87 done |
87 done |
88 |
88 |
89 end |
89 end |