src/CTT/Bool.ML
author paulson
Tue Apr 30 11:08:09 1996 +0200 (1996-04-30)
changeset 1702 4aa538e82f76
parent 1459 d12da312eff4
child 9249 c71db8c28727
permissions -rw-r--r--
Cosmetic re-ordering of declarations
     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 qed_goalw "boolF" Bool.thy bool_defs 
    17     "Bool type"
    18  (fn _ => [ (typechk_tac []) ]);
    19 
    20 
    21 (*introduction rules for true, false*)
    22 
    23 qed_goalw "boolI_true" Bool.thy bool_defs 
    24     "true : Bool"
    25  (fn _ => [ (typechk_tac []) ]);
    26 
    27 qed_goalw "boolI_false" Bool.thy bool_defs 
    28     "false : Bool"
    29  (fn _ => [ (typechk_tac []) ]);
    30 
    31 (*elimination rule: typing of cond*)
    32 qed_goalw "boolE" Bool.thy bool_defs 
    33     "!!C. [| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
    34  (fn _ =>
    35   [ (typechk_tac []),
    36     (ALLGOALS (etac TE)),
    37     (typechk_tac []) ]);
    38 
    39 qed_goalw "boolEL" Bool.thy bool_defs 
    40     "!!C. [| p = q : Bool;  a = c : C(true);  b = d : C(false) |] ==> \
    41 \         cond(p,a,b) = cond(q,c,d) : C(p)"
    42  (fn _ =>
    43   [ (rtac PlusEL 1),
    44     (REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ]);
    45 
    46 (*computation rules for true, false*)
    47 
    48 qed_goalw "boolC_true" Bool.thy bool_defs 
    49     "!!C. [| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
    50  (fn _ =>
    51   [ (resolve_tac comp_rls 1),
    52     (typechk_tac []),
    53     (ALLGOALS (etac TE)),
    54     (typechk_tac []) ]);
    55 
    56 qed_goalw "boolC_false" Bool.thy bool_defs 
    57     "!!C. [| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
    58  (fn _ =>
    59   [ (resolve_tac comp_rls 1),
    60     (typechk_tac []),
    61     (ALLGOALS (etac TE)),
    62     (typechk_tac []) ]);
    63 
    64 writeln"Reached end of file.";
    65