0

1 
(* Title: CTT/bool


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 


6 
Theorems for bool.thy (booleans and conditionals)


7 
*)


8 


9 
open Bool;


10 


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


12 


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


14 


15 
(*formation rule*)


16 
val boolF = prove_goal Bool.thy


17 
"Bool type"


18 
(fn prems=>


19 
[ (rewrite_goals_tac bool_defs),


20 
(typechk_tac[]) ]);


21 


22 


23 
(*introduction rules for true, false*)


24 


25 
val boolI_true = prove_goal Bool.thy


26 
"true : Bool"


27 
(fn prems=>


28 
[ (rewrite_goals_tac bool_defs),


29 
(typechk_tac[]) ]);


30 


31 
val boolI_false = prove_goal Bool.thy


32 
"false : Bool"


33 
(fn prems=>


34 
[ (rewrite_goals_tac bool_defs),


35 
(typechk_tac[]) ]);


36 


37 
(*elimination rule: typing of cond*)


38 
val boolE = prove_goal Bool.thy


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


40 
(fn prems=>


41 
[ (cut_facts_tac prems 1),


42 
(rewrite_goals_tac bool_defs),


43 
(typechk_tac prems),


44 
(ALLGOALS (etac TE)),


45 
(typechk_tac prems) ]);


46 


47 
val boolEL = prove_goal Bool.thy


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


49 
\ cond(p,a,b) = cond(q,c,d) : C(p)"


50 
(fn prems=>


51 
[ (cut_facts_tac prems 1),


52 
(rewrite_goals_tac bool_defs),


53 
(resolve_tac [PlusEL] 1),


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


55 


56 
(*computation rules for true, false*)


57 


58 
val boolC_true = prove_goal Bool.thy


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


60 
(fn prems=>


61 
[ (cut_facts_tac prems 1),


62 
(rewrite_goals_tac bool_defs),


63 
(resolve_tac comp_rls 1),


64 
(typechk_tac[]),


65 
(ALLGOALS (etac TE)),


66 
(typechk_tac prems) ]);


67 


68 
val boolC_false = prove_goal Bool.thy


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


70 
(fn prems=>


71 
[ (cut_facts_tac prems 1),


72 
(rewrite_goals_tac bool_defs),


73 
(resolve_tac comp_rls 1),


74 
(typechk_tac[]),


75 
(ALLGOALS (etac TE)),


76 
(typechk_tac prems) ]);


77 


78 
writeln"Reached end of file.";


79 
