src/CTT/bool.ML
changeset 0 a5a9c433f639
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CTT/bool.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,79 @@
     1.4 +(*  Title: 	CTT/bool
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1991  University of Cambridge
     1.8 +
     1.9 +Theorems for bool.thy (booleans and conditionals)
    1.10 +*)
    1.11 +
    1.12 +open Bool;
    1.13 +
    1.14 +val bool_defs = [Bool_def,true_def,false_def,cond_def];
    1.15 +
    1.16 +(*Derivation of rules for the type Bool*)
    1.17 +
    1.18 +(*formation rule*)
    1.19 +val boolF = prove_goal Bool.thy 
    1.20 +    "Bool type"
    1.21 + (fn prems=>
    1.22 +  [ (rewrite_goals_tac bool_defs),
    1.23 +    (typechk_tac[]) ]);
    1.24 +
    1.25 +
    1.26 +(*introduction rules for true, false*)
    1.27 +
    1.28 +val boolI_true = prove_goal Bool.thy 
    1.29 +    "true : Bool"
    1.30 + (fn prems=>
    1.31 +  [ (rewrite_goals_tac bool_defs),
    1.32 +    (typechk_tac[]) ]);
    1.33 +
    1.34 +val boolI_false = prove_goal Bool.thy 
    1.35 +    "false : Bool"
    1.36 + (fn prems=>
    1.37 +  [ (rewrite_goals_tac bool_defs),
    1.38 +    (typechk_tac[]) ]);
    1.39 +
    1.40 +(*elimination rule: typing of cond*)
    1.41 +val boolE = prove_goal Bool.thy 
    1.42 +    "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
    1.43 + (fn prems=>
    1.44 +  [ (cut_facts_tac prems 1),
    1.45 +    (rewrite_goals_tac bool_defs),
    1.46 +    (typechk_tac prems),
    1.47 +    (ALLGOALS (etac TE)),
    1.48 +    (typechk_tac prems) ]);
    1.49 +
    1.50 +val boolEL = prove_goal Bool.thy 
    1.51 +    "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |] ==> \
    1.52 +\    cond(p,a,b) = cond(q,c,d) : C(p)"
    1.53 + (fn prems=>
    1.54 +  [ (cut_facts_tac prems 1),
    1.55 +    (rewrite_goals_tac bool_defs),
    1.56 +    (resolve_tac [PlusEL] 1),
    1.57 +    (REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ]);
    1.58 +
    1.59 +(*computation rules for true, false*)
    1.60 +
    1.61 +val boolC_true = prove_goal Bool.thy 
    1.62 +    "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
    1.63 + (fn prems=>
    1.64 +  [ (cut_facts_tac prems 1),
    1.65 +    (rewrite_goals_tac bool_defs),
    1.66 +    (resolve_tac comp_rls 1),
    1.67 +    (typechk_tac[]),
    1.68 +    (ALLGOALS (etac TE)),
    1.69 +    (typechk_tac prems) ]);
    1.70 +
    1.71 +val boolC_false = prove_goal Bool.thy 
    1.72 +    "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
    1.73 + (fn prems=>
    1.74 +  [ (cut_facts_tac prems 1),
    1.75 +    (rewrite_goals_tac bool_defs),
    1.76 +    (resolve_tac comp_rls 1),
    1.77 +    (typechk_tac[]),
    1.78 +    (ALLGOALS (etac TE)),
    1.79 +    (typechk_tac prems) ]);
    1.80 +
    1.81 +writeln"Reached end of file.";
    1.82 +