src/CTT/Bool.ML
author kleing
Wed Apr 14 14:13:05 2004 +0200 (2004-04-14)
changeset 14565 c6dc17aab88a
parent 9251 bd57acd44fc1
child 17441 5b5feca0344a
permissions -rw-r--r--
use more symbols in HTML output
     1 (*  Title:      CTT/Bool
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 The two-element type (booleans and conditionals)
     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*)
    14 Goalw bool_defs "Bool type";
    15 by (typechk_tac []) ;
    16 qed "boolF";
    17 
    18 
    19 (*introduction rules for true, false*)
    20 
    21 Goalw bool_defs "true : Bool";
    22 by (typechk_tac []) ;
    23 qed "boolI_true";
    24 
    25 Goalw bool_defs "false : Bool";
    26 by (typechk_tac []) ;
    27 qed "boolI_false";
    28 
    29 (*elimination rule: typing of cond*)
    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";
    36 
    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";
    43 
    44 (*computation rules for true, false*)
    45 
    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";
    53 
    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";
    61 
    62 writeln"Reached end of file.";
    63