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;
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
*)
clasohm@0
     6
clasohm@0
     7
val bool_defs = [Bool_def,true_def,false_def,cond_def];
clasohm@0
     8
clasohm@0
     9
(*Derivation of rules for the type Bool*)
clasohm@0
    10
clasohm@0
    11
(*formation rule*)
paulson@9249
    12
Goalw bool_defs "Bool type";
paulson@9249
    13
by (typechk_tac []) ;
paulson@9249
    14
qed "boolF";
clasohm@0
    15
clasohm@0
    16
clasohm@0
    17
(*introduction rules for true, false*)
clasohm@0
    18
paulson@9249
    19
Goalw bool_defs "true : Bool";
paulson@9249
    20
by (typechk_tac []) ;
paulson@9249
    21
qed "boolI_true";
clasohm@0
    22
paulson@9249
    23
Goalw bool_defs "false : Bool";
paulson@9249
    24
by (typechk_tac []) ;
paulson@9249
    25
qed "boolI_false";
clasohm@0
    26
clasohm@0
    27
(*elimination rule: typing of cond*)
wenzelm@17441
    28
Goalw bool_defs
paulson@9249
    29
    "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)";
paulson@9249
    30
by (typechk_tac []);
paulson@9249
    31
by (ALLGOALS (etac TE));
paulson@9249
    32
by (typechk_tac []) ;
paulson@9249
    33
qed "boolE";
clasohm@0
    34
paulson@9249
    35
Goalw bool_defs
paulson@9249
    36
    "[| p = q : Bool;  a = c : C(true);  b = d : C(false) |] \
paulson@9249
    37
\    ==> cond(p,a,b) = cond(q,c,d) : C(p)";
paulson@9249
    38
by (rtac PlusEL 1);
paulson@9249
    39
by (REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ;
paulson@9249
    40
qed "boolEL";
clasohm@0
    41
clasohm@0
    42
(*computation rules for true, false*)
clasohm@0
    43
wenzelm@17441
    44
Goalw bool_defs
paulson@9249
    45
    "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)";
paulson@9249
    46
by (resolve_tac comp_rls 1);
paulson@9249
    47
by (typechk_tac []);
paulson@9249
    48
by (ALLGOALS (etac TE));
paulson@9249
    49
by (typechk_tac []) ;
paulson@9249
    50
qed "boolC_true";
clasohm@0
    51
paulson@9249
    52
Goalw bool_defs
paulson@9249
    53
    "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)";
paulson@9249
    54
by (resolve_tac comp_rls 1);
paulson@9249
    55
by (typechk_tac []);
paulson@9249
    56
by (ALLGOALS (etac TE));
paulson@9249
    57
by (typechk_tac []) ;
paulson@9249
    58
qed "boolC_false";