author  obua 
Fri, 16 Sep 2005 21:02:15 +0200  
changeset 17440  df77edc4f5d0 
parent 9251  bd57acd44fc1 
child 17441  5b5feca0344a 
permissions  rwrr 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

1 
(* Title: CTT/Bool 
0  2 
ID: $Id$ 
1459  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1991 University of Cambridge 
5 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

6 
The twoelement type (booleans and conditionals) 
0  7 
*) 
8 

9 
val bool_defs = [Bool_def,true_def,false_def,cond_def]; 

10 

11 
(*Derivation of rules for the type Bool*) 

12 

13 
(*formation rule*) 

9249  14 
Goalw bool_defs "Bool type"; 
15 
by (typechk_tac []) ; 

16 
qed "boolF"; 

0  17 

18 

19 
(*introduction rules for true, false*) 

20 

9249  21 
Goalw bool_defs "true : Bool"; 
22 
by (typechk_tac []) ; 

23 
qed "boolI_true"; 

0  24 

9249  25 
Goalw bool_defs "false : Bool"; 
26 
by (typechk_tac []) ; 

27 
qed "boolI_false"; 

0  28 

29 
(*elimination rule: typing of cond*) 

9249  30 
Goalw bool_defs 
31 
"[ p:Bool; a : C(true); b : C(false) ] ==> cond(p,a,b) : C(p)"; 

32 
by (typechk_tac []); 

33 
by (ALLGOALS (etac TE)); 

34 
by (typechk_tac []) ; 

35 
qed "boolE"; 

0  36 

9249  37 
Goalw bool_defs 
38 
"[ p = q : Bool; a = c : C(true); b = d : C(false) ] \ 

39 
\ ==> cond(p,a,b) = cond(q,c,d) : C(p)"; 

40 
by (rtac PlusEL 1); 

41 
by (REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ; 

42 
qed "boolEL"; 

0  43 

44 
(*computation rules for true, false*) 

45 

9249  46 
Goalw bool_defs 
47 
"[ a : C(true); b : C(false) ] ==> cond(true,a,b) = a : C(true)"; 

48 
by (resolve_tac comp_rls 1); 

49 
by (typechk_tac []); 

50 
by (ALLGOALS (etac TE)); 

51 
by (typechk_tac []) ; 

52 
qed "boolC_true"; 

0  53 

9249  54 
Goalw bool_defs 
55 
"[ a : C(true); b : C(false) ] ==> cond(false,a,b) = b : C(false)"; 

56 
by (resolve_tac comp_rls 1); 

57 
by (typechk_tac []); 

58 
by (ALLGOALS (etac TE)); 

59 
by (typechk_tac []) ; 

60 
qed "boolC_false"; 

0  61 

62 
writeln"Reached end of file."; 

63 