src/CTT/Bool.ML
author wenzelm
Fri Sep 16 23:01:29 2005 +0200 (2005-09-16)
changeset 17441 5b5feca0344a
parent 9251 bd57acd44fc1
permissions -rw-r--r--
converted to Isar theory format;
     1 (*  Title:      CTT/Bool
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 *)
     6 
     7 val bool_defs = [Bool_def,true_def,false_def,cond_def];
     8 
     9 (*Derivation of rules for the type Bool*)
    10 
    11 (*formation rule*)
    12 Goalw bool_defs "Bool type";
    13 by (typechk_tac []) ;
    14 qed "boolF";
    15 
    16 
    17 (*introduction rules for true, false*)
    18 
    19 Goalw bool_defs "true : Bool";
    20 by (typechk_tac []) ;
    21 qed "boolI_true";
    22 
    23 Goalw bool_defs "false : Bool";
    24 by (typechk_tac []) ;
    25 qed "boolI_false";
    26 
    27 (*elimination rule: typing of cond*)
    28 Goalw bool_defs
    29     "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)";
    30 by (typechk_tac []);
    31 by (ALLGOALS (etac TE));
    32 by (typechk_tac []) ;
    33 qed "boolE";
    34 
    35 Goalw bool_defs
    36     "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |] \
    37 \    ==> cond(p,a,b) = cond(q,c,d) : C(p)";
    38 by (rtac PlusEL 1);
    39 by (REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ;
    40 qed "boolEL";
    41 
    42 (*computation rules for true, false*)
    43 
    44 Goalw bool_defs
    45     "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)";
    46 by (resolve_tac comp_rls 1);
    47 by (typechk_tac []);
    48 by (ALLGOALS (etac TE));
    49 by (typechk_tac []) ;
    50 qed "boolC_true";
    51 
    52 Goalw bool_defs
    53     "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)";
    54 by (resolve_tac comp_rls 1);
    55 by (typechk_tac []);
    56 by (ALLGOALS (etac TE));
    57 by (typechk_tac []) ;
    58 qed "boolC_false";