src/CTT/bool.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
permissions -rw-r--r--
Initial revision
     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