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
paulson@9251
     1
(*  Title:      CTT/Bool
clasohm@0
     2
    ID:         $Id$
clasohm@1459
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1991  University of Cambridge
clasohm@0
     5
paulson@9251
     6
The two-element type (booleans and conditionals)
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
val bool_defs = [Bool_def,true_def,false_def,cond_def];
clasohm@0
    10
clasohm@0
    11
(*Derivation of rules for the type Bool*)
clasohm@0
    12
clasohm@0
    13
(*formation rule*)
paulson@9249
    14
Goalw bool_defs "Bool type";
paulson@9249
    15
by (typechk_tac []) ;
paulson@9249
    16
qed "boolF";
clasohm@0
    17
clasohm@0
    18
clasohm@0
    19
(*introduction rules for true, false*)
clasohm@0
    20
paulson@9249
    21
Goalw bool_defs "true : Bool";
paulson@9249
    22
by (typechk_tac []) ;
paulson@9249
    23
qed "boolI_true";
clasohm@0
    24
paulson@9249
    25
Goalw bool_defs "false : Bool";
paulson@9249
    26
by (typechk_tac []) ;
paulson@9249
    27
qed "boolI_false";
clasohm@0
    28
clasohm@0
    29
(*elimination rule: typing of cond*)
paulson@9249
    30
Goalw bool_defs 
paulson@9249
    31
    "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)";
paulson@9249
    32
by (typechk_tac []);
paulson@9249
    33
by (ALLGOALS (etac TE));
paulson@9249
    34
by (typechk_tac []) ;
paulson@9249
    35
qed "boolE";
clasohm@0
    36
paulson@9249
    37
Goalw bool_defs
paulson@9249
    38
    "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |] \
paulson@9249
    39
\    ==> cond(p,a,b) = cond(q,c,d) : C(p)";
paulson@9249
    40
by (rtac PlusEL 1);
paulson@9249
    41
by (REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ;
paulson@9249
    42
qed "boolEL";
clasohm@0
    43
clasohm@0
    44
(*computation rules for true, false*)
clasohm@0
    45
paulson@9249
    46
Goalw bool_defs 
paulson@9249
    47
    "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)";
paulson@9249
    48
by (resolve_tac comp_rls 1);
paulson@9249
    49
by (typechk_tac []);
paulson@9249
    50
by (ALLGOALS (etac TE));
paulson@9249
    51
by (typechk_tac []) ;
paulson@9249
    52
qed "boolC_true";
clasohm@0
    53
paulson@9249
    54
Goalw bool_defs
paulson@9249
    55
    "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)";
paulson@9249
    56
by (resolve_tac comp_rls 1);
paulson@9249
    57
by (typechk_tac []);
paulson@9249
    58
by (ALLGOALS (etac TE));
paulson@9249
    59
by (typechk_tac []) ;
paulson@9249
    60
qed "boolC_false";
clasohm@0
    61
clasohm@0
    62
writeln"Reached end of file.";
clasohm@0
    63